ShotDs.Data.Context (shot_ds v1.0.0)

Represents a type environment for parsing and type checking. Can also be created by using the ~e sigil from ShotDs.Hol.Sigils.

Examples

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

iex> Context.new() |> Context.put_var("X", Type.new(:o))
%ShotDs.Data.Context{
  vars: %{"X" => %ShotDs.Data.Type{goal: :o, args: []}},
  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() :: %ShotDs.Data.Context{
  constraints: MapSet.t({ShotDs.Data.Type.t(), ShotDs.Data.Type.t()}),
  consts: %{required(String.t()) => ShotDs.Data.Type.t()},
  vars: %{required(String.t()) => ShotDs.Data.Type.t()}
}

The type of the type environment.

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 ShotDs.Data.Type pairs.