BeHOLd.Data.Context (behold v1.1.3)

A data structure to declare and track variable types and declared constants. Also contains type constraints needed for parsing.

Examples

iex> Context.new()
%BeHOLd.Data.Context{vars: %{}, consts: %{}, constraints: MapSet.new([])}

iex> Context.new() |> Context.put_var("X", HOL.Data.mk_type(:o))
%BeHOLd.Data.Context{
  vars: %{"X" => {:type, :o, []}},
  consts: %{},
  constraints: MapSet.new([])
}

Summary

Functions

add_constraint(ctx, t1, t2)

Adds a type constraint to the context.

get_type(ctx, name)

Returns the type of the given name of a constant or variable. Returns nil if the name is not present in the context.

new()

Creates an empty context.

put_const(ctx, name, type)

Associates the constant with the given name with the given type in the context. Overwrites the old value if present.

put_var(ctx, name, type)

Associates the variable with the given name with the given type in the context. Overwrites the old value if present.

Types

t()

@type t() :: %BeHOLd.Data.Context{
  constraints: MapSet.t({HOL.Data.type(), HOL.Data.type()}),
  consts: %{required(String.t()) => HOL.Data.type()},
  vars: %{required(String.t()) => HOL.Data.type()}
}

The type of the context.

A context contains the type of variables (:vars) as a Map from its name to its type. Likewise for the constants (:consts). The type constraints are represented as a MapSet of HOL.Data.type() pairs.