Module Albalib.Build_contextSource

Sourcetype t
Sourcetype type_in_context = int list * Term.typ * Gamma.t

A build context consists of a context with holes and a stack of to be constructed terms.

There is always a next to be constructed term. The term is either in a function position or an argument position.

Sourceval count : t -> int
Sourceval count_base : t -> int
Sourceval count_locals : t -> int
Sourceval count_bounds : t -> int
Sourceval required_type_in_context : t -> type_in_context
Sourceval make : Gamma.t -> t

make gamma

Make a build context based on gamma. Push 2 holes onto the context to get

Gamma, E: Any(2), e: E

The next to be constructed term points to e.

Sourceval final : t -> (Term.t * Term.typ, int list * Term.typ * Gamma.t) result

Terminals

Sourceval base_candidate : Term.t -> int -> t -> t option

base_candidate term nargs bc

Receive the term term as a candidate for the next to be constructed term. The candidate is from the base context and in applied to nargs arguments.

Base candidates are either

  • Literals (Numbers, characters, strings)
  • Variables from the base context
Sourceval bound : int -> int -> t -> (t, type_in_context * type_in_context) result

bound level nargs bc

Product all (a: A) ... : RT

Sourcemodule Product : sig ... end

Typed expression exp: tp

Sourcemodule Typed : sig ... end

Function Application f a b c ...

Sourcemodule Application : sig ... end

Function Abstraction \ x y ... := t

Sourcemodule Lambda : sig ... end