Gamma_holes is a context with holes which can be filled later. A hole is a local unnamed variable with a type (i.e. an assumption that an element with this type exists), initially without value. Later on the value can be provided.
val count : t -> intThe size of the context.
val count_base : t -> intThe size of the base context.
val count_bounds : t -> intThe number of bound variables which have been entered.
val count_entries : t -> intThe number of holes and bound variable which have been entered.
val is_valid_index : int -> t -> boolval name_of_index : int -> t -> stringval index_of_level : int -> t -> intval is_hole : int -> t -> boolIs the variable a hole?
val is_bound : int -> t -> boolIs the variable a bound variable?
val bound_number : int -> t -> intbound_number idx gh
Return the number of the bound variable at idx.
Precondition:
is_bound idx ghvariable_of_bound i gh
Compute the variable corresponding to the ith bound variable.
Precondition:
i < count_bounds ghval has_value : int -> t -> boolHas the variable a value i.e. is it a hole with value.
val unfilled_holes : int -> Term.t -> t -> Fmlib.Common.Int_set.tunfilled_holes cnt0 term gh
List of unfilled holes in term starting at level cnt0.
The returned list contains the De Bruijn levels of the unfilled holes.
Precondition:
cnt0 <= count ghexpand term gh Replace all holes in term with its values, if available.
is_expanded term gh Is the term term expanded i.e. does it not contain any filled holes?
term_of_term_n tn gh
Lift the term tn into the context and expand it.
fill_hole0 idx value beta_reduce gh
Fill the hole at idx with value. In case that value is a function abstraction appearing in a function position and the flag beta_reduce is set, do a beta reduction.
Preconditions:
is_unfilled idx ghfill_hole idx value gh Fill the hole at idx with value.
Preconditions:
is_unfilled idx ghval fold_entries :
(int -> int -> string -> Term.typ -> bool -> Term.t option -> 'a -> 'a) ->
t ->
'a ->
'afold_entries f gh a fold all entries with the folding function f.
f is called with the following arguments:
f level idx name typ is_hole value_opt a
push_hole name typ gh Add a hole with name name of type typ to gh.
push_bound name is_typed gh adds a bound variable to the context. The bound variable can be later used to construct binders like Pi (arg_tp, res_tp,
info or Lambda (arg_tp, exp, info. is_typed is used to construct the binder.
push_local name typ gh is synonym for push_bound name true gh
type_of_variable idx gh
Return the expanded type of the variable idx.
val type_of_literal : Term.Value.t -> t -> Term.typpi nbounds result_tp gh
Compute a product type with result_tp using the last nbounds bound variables.
all (a: A) (b: B) ... : RTPreconditions:
nbounds <= count_bounds ghlambda nbounds exp gh
Compute a function term with the inner expression exp using the last nbounds bound variables.
\ (a: A) (b: B) ... := expPreconditions:
nbounds <= count_bounds gh