2 exception AssertFailure of string
3 exception MetaSubstFailure of string
5 (* The entry (i,t) in a substitution means that *)
6 (* (META i) have been instantiated with t. *)
7 type substitution = (int * Cic.term) list
9 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t *)
10 (* performs as (apply_subst subst t) until it finds an application of *)
11 (* (META [mtr]) that, once unwinding is performed, creates a new *)
12 (* beta-redex; in this case up to [reductions_no] consecutive *)
13 (* beta-reductions are performed. *)
14 (* Hint: this function is usually called when [reductions_no] *)
15 (* eta-expansions have been performed and the head of the new *)
16 (* application has been unified with (META [meta_to_reduce]): *)
17 (* during the unwinding the eta-expansions are undone. *)
18 (* [subst] must be already unwinded *)
19 val apply_subst_reducing :
20 substitution -> (int * int) option -> Cic.term -> Cic.term
22 val apply_subst_context : substitution -> Cic.context -> Cic.context
24 (* apply_subst subst t *)
25 (* applies the substitution [subst] to [t] *)
26 (* [subst] must be already unwinded *)
27 val apply_subst : substitution -> Cic.term -> Cic.term
29 (* unwind_subst metasenv subst *)
30 (* unwinds [subst] w.r.t. itself. *)
31 (* It can restrict some metavariable in the [metasenv] *)
32 val unwind_subst : Cic.metasenv -> substitution -> substitution * Cic.metasenv
35 Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> Cic.term * Cic.metasenv
37 val ppcontext: ?sep: string -> substitution -> Cic.context -> string
38 val ppmetasenv: ?sep: string -> substitution -> Cic.metasenv -> string
39 val ppsubst: substitution -> string
41 (* From now on we recreate a kernel abstraction where substitutions are part of
44 val whd: substitution -> Cic.context -> Cic.term -> Cic.term
46 Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term