type pos = Fmlib.Character_parser.Position.ttype type_in_context = int list * Alba_core.Term.typ * Alba_core.Gamma.tA 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.
val count : t -> intval count_base : t -> intval count_entries : t -> intval count_bounds : t -> intval required_type_in_context : t -> type_in_contextval make : Alba_core.Gamma.t -> tmake 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.
val final :
t ->
(t * Alba_core.Term.t * Alba_core.Term.typ,
int list * Alba_core.Term.typ * Alba_core.Gamma.t)
resultval base_candidate : range -> int -> Alba_core.Term.t -> int -> t -> t optionbase_candidate range variant 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
val find_last_ambiguous :
t list ->
range * (Alba_core.Term.t * Alba_core.Term.typ) listval bound : int -> int -> t -> (t, type_in_context * type_in_context) resultbound level nargs bc
val next_formal_argument :
string Fmlib.Character_parser.Located.t ->
bool ->
t ->
tAdd a bound variable based on the last argument type and push a placeholder for the next argument type or the result type. I.e. expect the next argument type or the result type.
all (a: A) ... : RTmodule Product : sig ... endexp: tpmodule Typed : sig ... endf a b c ... module Application : sig ... end\ x y ... := tmodule Lambda : sig ... endexp where f ... := valueThe where expression
exp where
f := valueis treated like
(\f := exp) valuei.e.
Appl ( Lambda (f, F, exp), value)i.e. a beta redex, and finally converted to
Where (f, F, exp, value)module Where : sig ... end