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.
val count : t -> intval count_base : t -> intval count_locals : t -> intval count_bounds : t -> intval required_type_in_context : t -> type_in_contextmake 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.
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
val bound : int -> int -> t -> (t, type_in_context * type_in_context) resultbound level nargs bc
all (a: A) ... : RTmodule Product : sig ... endexp: tpmodule Typed : sig ... endf a b c ... module Application : sig ... end\ x y ... := tmodule Lambda : sig ... end