From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 22 Jan 2004 10:28:34 +0000 (+0000)
Subject: added CicMetaSubst module for metavariable instantiatiation
X-Git-Tag: V_0_5_1_3~10
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cc3d3e3f697e06026680bc94988c782ddd8eb33e;p=helm.git

added CicMetaSubst module for metavariable instantiatiation
---

diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend
index 0e37b8030..3a4c2eae9 100644
--- a/helm/ocaml/cic_unification/.depend
+++ b/helm/ocaml/cic_unification/.depend
@@ -1,7 +1,14 @@
-cicRefine.cmi: cicUnification.cmi 
-cicUnification.cmo: cicUnification.cmi 
-cicUnification.cmx: cicUnification.cmi 
-cicRefine.cmo: cicUnification.cmi cicRefine.cmi 
-cicRefine.cmx: cicUnification.cmx cicRefine.cmi 
 cicMkImplicit.cmo: cicMkImplicit.cmi 
 cicMkImplicit.cmx: cicMkImplicit.cmi 
+cicUnification.cmi: cicMetaSubst.cmi 
+cicRefine.cmi: cicMetaSubst.cmi 
+cicMkImplicit.cmo: cicMkImplicit.cmi 
+cicMkImplicit.cmx: cicMkImplicit.cmi 
+cicMetaSubst.cmo: cicMkImplicit.cmi cicMetaSubst.cmi 
+cicMetaSubst.cmx: cicMkImplicit.cmx cicMetaSubst.cmi 
+cicUnification.cmo: cicMetaSubst.cmi cicUnification.cmi 
+cicUnification.cmx: cicMetaSubst.cmx cicUnification.cmi 
+cicRefine.cmo: cicMetaSubst.cmi cicMkImplicit.cmi cicUnification.cmi \
+    cicRefine.cmi 
+cicRefine.cmx: cicMetaSubst.cmx cicMkImplicit.cmx cicUnification.cmx \
+    cicRefine.cmi 
diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile
index 1ce66e68d..a0bea2edd 100644
--- a/helm/ocaml/cic_unification/Makefile
+++ b/helm/ocaml/cic_unification/Makefile
@@ -2,7 +2,11 @@ PACKAGE = cic_unification
 REQUIRES = helm-cic_proof_checking
 PREDICATES =
 
-INTERFACE_FILES = cicMkImplicit.ml cicUnification.mli cicRefine.mli
+INTERFACE_FILES = \
+	cicMkImplicit.ml \
+	cicMetaSubst.mli \
+	cicUnification.mli \
+	cicRefine.mli
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL =
 
diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
new file mode 100644
index 000000000..04cf03c67
--- /dev/null
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -0,0 +1,500 @@
+
+open Printf
+
+exception AssertFailure of string
+exception MetaSubstFailure of string
+exception RelToHiddenHypothesis
+
+let debug_print = prerr_endline
+
+type substitution = (int * Cic.term) list
+
+let ppsubst subst =
+  String.concat "\n"
+    (List.map
+      (fun (idx, term) -> Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
+      subst)
+
+(**** DELIFT ****)
+
+(* the delift function takes in input an ordered list of optional terms       *)
+(* [t1,...,tn] and a term t, and substitutes every tk = Some (rel(nk)) with   *)
+(* rel(k). Typically, the list of optional terms is the explicit substitution *)
+(* that is applied to a metavariable occurrence and the result of the delift  *)
+(* function is a term the implicit variable can be substituted with to make   *)
+(* the term [t] unifiable with the metavariable occurrence.                   *)
+(* In general, the problem is undecidable if we consider equivalence in place *)
+(* of alpha convertibility. Our implementation, though, is even weaker than   *)
+(* alpha convertibility, since it replace the term [tk] if and only if [tk]   *)
+(* is a Rel (missing all the other cases). Does this matter in practice?      *)
+
+exception NotInTheList;;
+
+let position n =
+  let rec aux k =
+   function 
+       [] -> raise NotInTheList
+     | (Some (Cic.Rel m))::_ when m=n -> k
+     | _::tl -> aux (k+1) tl in
+  aux 1
+;;
+ 
+(*CSC: this restriction function is utterly wrong, since it does not check  *)
+(*CSC: that the variable that is going to be restricted does not occur free *)
+(*CSC: in a part of the sequent that is not going to be restricted.         *)
+(*CSC: In particular, the whole approach is wrong; if restriction can fail  *)
+(*CSC: (as indeed it is the case), we can not collect all the restrictions  *)
+(*CSC: and restrict everything at the end ;-(                               *)
+let restrict to_be_restricted =
+  let rec erase i n = 
+    function
+        [] -> []
+      |        _::tl when List.mem (n,i) to_be_restricted ->
+          None::(erase (i+1) n tl) 
+      | he::tl -> he::(erase (i+1) n tl) in
+  let rec aux =
+    function 
+        [] -> []
+      |        (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
+  aux
+;;
+
+(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
+let delift context metasenv l t =
+ let module S = CicSubstitution in
+  let to_be_restricted = ref [] in
+  let rec deliftaux k =
+   let module C = Cic in
+    function
+       C.Rel m -> 
+         if m <=k then
+          C.Rel m   (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
+                    (*CSC: deliftato la regola per il LetIn                 *)
+                    (*CSC: FALSO! La regola per il LetIn non lo fa          *)
+         else
+          (match List.nth context (m-k-1) with
+            Some (_,C.Def (t,_)) ->
+             (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
+             (*CSC: first order unification. Does it help or does it harm? *)
+             deliftaux k (S.lift m t)
+          | Some (_,C.Decl t) ->
+             (*CSC: The following check seems to be wrong!             *)
+             (*CSC: B:Set |- ?2 : Set                                  *)
+             (*CSC: A:Set ; x:?2[A/B] |- ?1[x/A] =?= x                 *)
+             (*CSC: Why should I restrict ?2 over B? The instantiation *)
+             (*CSC: ?1 := A is perfectly reasonable and well-typed.    *)
+             (*CSC: Thus I comment out the following two lines that    *)
+             (*CSC: are the incriminated ones.                         *)
+             (*(* It may augment to_be_restricted *)
+               ignore (deliftaux k (S.lift m t)) ;*)
+             (*CSC: end of bug commented out                           *)
+             C.Rel ((position (m-k) l) + k)
+          | None -> raise RelToHiddenHypothesis)
+     | C.Var (uri,exp_named_subst) ->
+        let exp_named_subst' =
+         List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
+        in
+         C.Var (uri,exp_named_subst')
+     | C.Meta (i, l1) as t -> 
+        let rec deliftl j =
+         function
+            [] -> []
+          | None::tl -> None::(deliftl (j+1) tl)
+          | (Some t)::tl ->
+             let l1' = (deliftl (j+1) tl) in
+              try
+               Some (deliftaux k t)::l1'
+              with
+                 RelToHiddenHypothesis
+               | NotInTheList ->
+                  to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
+        in
+         let l' = deliftl 1 l1 in
+          C.Meta(i,l')
+     | C.Sort _ as t -> t
+     | C.Implicit as t -> t
+     | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
+     | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
+     | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
+     | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
+     | C.Appl l -> C.Appl (List.map (deliftaux k) l)
+     | C.Const (uri,exp_named_subst) ->
+        let exp_named_subst' =
+         List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
+        in
+         C.Const (uri,exp_named_subst')
+     | C.MutInd (uri,typeno,exp_named_subst) ->
+        let exp_named_subst' =
+         List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
+        in
+         C.MutInd (uri,typeno,exp_named_subst')
+     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+        let exp_named_subst' =
+         List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
+        in
+         C.MutConstruct (uri,typeno,consno,exp_named_subst')
+     | C.MutCase (sp,i,outty,t,pl) ->
+        C.MutCase (sp, i, deliftaux k outty, deliftaux k t,
+         List.map (deliftaux k) pl)
+     | C.Fix (i, fl) ->
+        let len = List.length fl in
+        let liftedfl =
+         List.map
+          (fun (name, i, ty, bo) ->
+           (name, i, deliftaux k ty, deliftaux (k+len) bo))
+           fl
+        in
+         C.Fix (i, liftedfl)
+     | C.CoFix (i, fl) ->
+        let len = List.length fl in
+        let liftedfl =
+         List.map
+          (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
+           fl
+        in
+         C.CoFix (i, liftedfl)
+  in
+   let res =
+    try
+     deliftaux 0 t
+    with
+     NotInTheList ->
+      (* This is the case where we fail even first order unification. *)
+      (* The reason is that our delift function is weaker than first  *)
+      (* order (in the sense of alpha-conversion). See comment above  *)
+      (* related to the delift function.                              *)
+debug_print "!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
+      raise (MetaSubstFailure (sprintf
+        "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
+        (CicPp.ppterm t)
+        (String.concat "; "
+          (List.map
+            (function Some t -> CicPp.ppterm t | None -> "_")
+            l))))
+   in
+    res, restrict !to_be_restricted metasenv
+;;
+
+(**** END OF DELIFT ****)
+
+let rec unwind metasenv subst unwinded t =
+ let unwinded = ref unwinded in
+ let frozen = ref [] in
+ let rec um_aux metasenv =
+  let module C = Cic in
+  let module S = CicSubstitution in 
+   function
+      C.Rel _ as t -> t,metasenv
+    | C.Var _  as t -> t,metasenv
+    | C.Meta (i,l) -> 
+        (try
+          S.lift_meta l (List.assoc i !unwinded), metasenv
+         with Not_found ->
+           if List.mem i !frozen then
+             raise (MetaSubstFailure
+              "Failed to unify due to cyclic constraints (occur check)")
+           else
+            let saved_frozen = !frozen in 
+            frozen := i::!frozen ;
+            let res =
+             try
+              let t = List.assoc i subst in
+              let t',metasenv' = um_aux metasenv t in
+              let _,metasenv'' =
+               let (_,canonical_context,_) = 
+                List.find (function (m,_,_) -> m=i) metasenv
+               in
+                delift canonical_context metasenv' l t'
+              in
+               unwinded := (i,t')::!unwinded ;
+               S.lift_meta l t', metasenv'
+             with
+              Not_found ->
+               (* not constrained variable, i.e. free in subst*)
+               let l',metasenv' =
+                List.fold_right
+                 (fun t (tl,metasenv) ->
+                   match t with
+                      None -> None::tl,metasenv
+                    | Some t -> 
+                       let t',metasenv' = um_aux metasenv t in
+                        (Some t')::tl, metasenv'
+                 ) l ([],metasenv)
+               in
+                C.Meta (i,l'), metasenv'
+            in
+            frozen := saved_frozen ;
+            res
+        ) 
+    | C.Sort _
+    | C.Implicit as t -> t,metasenv
+    | C.Cast (te,ty) ->
+       let te',metasenv' = um_aux metasenv te in
+       let ty',metasenv'' = um_aux metasenv' ty in
+       C.Cast (te',ty'),metasenv''
+    | C.Prod (n,s,t) ->
+       let s',metasenv' = um_aux metasenv s in
+       let t',metasenv'' = um_aux metasenv' t in
+       C.Prod (n, s', t'), metasenv''
+    | C.Lambda (n,s,t) ->
+       let s',metasenv' = um_aux metasenv s in
+       let t',metasenv'' = um_aux metasenv' t in
+       C.Lambda (n, s', t'), metasenv''
+    | C.LetIn (n,s,t) ->
+       let s',metasenv' = um_aux metasenv s in
+       let t',metasenv'' = um_aux metasenv' t in
+       C.LetIn (n, s', t'), metasenv''
+    | C.Appl (he::tl) ->
+       let tl',metasenv' =
+        List.fold_right
+         (fun t (tl,metasenv) ->
+           let t',metasenv' = um_aux metasenv t in
+            t'::tl, metasenv'
+         ) tl ([],metasenv)
+       in
+        begin
+         match um_aux metasenv' he with
+            (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv''
+          | (he', metasenv'') -> C.Appl (he'::tl'),metasenv''
+        end
+    | C.Appl _ -> assert false
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst', metasenv' =
+        List.fold_right
+         (fun (uri,t) (tl,metasenv) ->
+           let t',metasenv' = um_aux metasenv t in
+            (uri,t')::tl, metasenv'
+         ) exp_named_subst ([],metasenv)
+       in
+        C.Const (uri,exp_named_subst'),metasenv'
+    | C.MutInd (uri,typeno,exp_named_subst) ->
+       let exp_named_subst', metasenv' =
+        List.fold_right
+         (fun (uri,t) (tl,metasenv) ->
+           let t',metasenv' = um_aux metasenv t in
+            (uri,t')::tl, metasenv'
+         ) exp_named_subst ([],metasenv)
+       in
+        C.MutInd (uri,typeno,exp_named_subst'),metasenv'
+    | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+       let exp_named_subst', metasenv' =
+        List.fold_right
+         (fun (uri,t) (tl,metasenv) ->
+           let t',metasenv' = um_aux metasenv t in
+            (uri,t')::tl, metasenv'
+         ) exp_named_subst ([],metasenv)
+       in
+        C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv'
+    | C.MutCase (sp,i,outty,t,pl) ->
+       let outty',metasenv' = um_aux metasenv outty in
+       let t',metasenv'' = um_aux metasenv' t in
+       let pl',metasenv''' =
+        List.fold_right
+         (fun p (pl,metasenv) ->
+           let p',metasenv' = um_aux metasenv p in
+            p'::pl, metasenv'
+         ) pl ([],metasenv'')
+       in
+        C.MutCase (sp, i, outty', t', pl'),metasenv'''
+    | C.Fix (i, fl) ->
+       let len = List.length fl in
+       let liftedfl,metasenv' =
+        List.fold_right
+         (fun (name, i, ty, bo) (fl,metasenv) ->
+           let ty',metasenv' = um_aux metasenv ty in
+           let bo',metasenv'' = um_aux metasenv' bo in
+            (name, i, ty', bo')::fl,metasenv''
+         ) fl ([],metasenv)
+       in
+        C.Fix (i, liftedfl),metasenv'
+    | C.CoFix (i, fl) ->
+       let len = List.length fl in
+       let liftedfl,metasenv' =
+        List.fold_right
+         (fun (name, ty, bo) (fl,metasenv) ->
+           let ty',metasenv' = um_aux metasenv ty in
+           let bo',metasenv'' = um_aux metasenv' bo in
+            (name, ty', bo')::fl,metasenv''
+         ) fl ([],metasenv)
+       in
+        C.CoFix (i, liftedfl),metasenv'
+ in
+  let t',metasenv' = um_aux metasenv t in
+   t',metasenv',!unwinded 
+
+let apply_subst subst t = 
+ (* metasenv will not be used nor modified. So, let's use a dummy empty one *)
+ let metasenv = [] in
+  let (t',_,_) = unwind metasenv [] subst t in
+   t'
+
+(* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
+(* performs as (apply_subst subst t) until it finds an application of   *)
+(* (META [meta_to_reduce]) that, once unwinding is performed, creates   *)
+(* a new beta-redex; in this case up to [reductions_no] consecutive     *)
+(* beta-reductions are performed.                                       *)
+(* Hint: this function is usually called when [reductions_no]           *)
+(*  eta-expansions have been performed and the head of the new          *)
+(*  application has been unified with (META [meta_to_reduce]):          *)
+(*  during the unwinding the eta-expansions are undone.                 *)
+
+let rec apply_subst_context subst =
+    List.map (function
+      | Some (n, Cic.Decl t) -> Some (n, Cic.Decl (apply_subst subst t))
+      | Some (n, Cic.Def (t, ty)) ->
+          let ty' =
+            match ty with
+            | None -> None
+            | Some ty -> Some (apply_subst subst ty)
+          in
+          Some (n, Cic.Def (apply_subst subst t, ty'))
+      | None -> None)
+
+let rec apply_subst_reducing subst meta_to_reduce t =
+ let rec um_aux =
+  let module C = Cic in
+  let module S = CicSubstitution in 
+   function
+      C.Rel _
+    | C.Var _  as t -> t
+    | C.Meta (i,l) as t ->
+       (try
+         S.lift_meta l (List.assoc i subst)
+        with Not_found ->
+          C.Meta (i,l))
+    | C.Sort _ as t -> t
+    | C.Implicit as t -> t
+    | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
+    | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
+    | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
+    | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
+    | C.Appl (he::tl) ->
+       let tl' = List.map um_aux tl in
+        let t' =
+         match um_aux he with
+            C.Appl l -> C.Appl (l@tl')
+          | _ as he' -> C.Appl (he'::tl')
+        in
+         begin
+          match meta_to_reduce,he with
+             Some (mtr,reductions_no), C.Meta (m,_) when m = mtr ->
+              let rec beta_reduce =
+               function
+                  (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
+                    let he'' = CicSubstitution.subst he' t in
+                     if tl' = [] then
+                      he''
+                     else
+                      beta_reduce (n-1,C.Appl(he''::tl'))
+                | (_,t) -> t
+              in
+               beta_reduce (reductions_no,t')
+           | _,_ -> t'
+         end
+    | C.Appl _ -> assert false
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
+       in
+        C.Const (uri,exp_named_subst')
+    | C.MutInd (uri,typeno,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
+       in
+        C.MutInd (uri,typeno,exp_named_subst')
+    | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
+       in
+        C.MutConstruct (uri,typeno,consno,exp_named_subst')
+    | C.MutCase (sp,i,outty,t,pl) ->
+       C.MutCase (sp, i, um_aux outty, um_aux t,
+        List.map um_aux pl)
+    | C.Fix (i, fl) ->
+       let len = List.length fl in
+       let liftedfl =
+        List.map
+         (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo))
+          fl
+       in
+        C.Fix (i, liftedfl)
+    | C.CoFix (i, fl) ->
+       let len = List.length fl in
+       let liftedfl =
+        List.map
+         (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo))
+          fl
+       in
+        C.CoFix (i, liftedfl)
+ in
+   um_aux t
+
+let ppcontext ?(sep = "\n") subst context =
+  String.concat sep
+    (List.rev_map (function
+      | Some (n, Cic.Decl t) ->
+          sprintf "%s : %s"
+            (CicPp.ppname n) (CicPp.ppterm (apply_subst subst t))
+      | Some (n, Cic.Def (t, ty)) ->
+          sprintf "%s : %s := %s"
+            (CicPp.ppname n)
+            (match ty with
+            | None -> "_"
+            | Some ty -> CicPp.ppterm (apply_subst subst ty))
+            (CicPp.ppterm (apply_subst subst t))
+      | None -> "_")
+      context)
+
+let ppmetasenv ?(sep = "\n") subst metasenv =
+  String.concat sep
+    (List.map
+      (fun (i, c, t) ->
+        sprintf "%s |- ?%d: %s" (ppcontext ~sep:"; " subst c) i
+          (CicPp.ppterm (apply_subst subst t)))
+      (List.filter
+        (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+        metasenv))
+
+(* UNWIND THE MGU INSIDE THE MGU *)
+let unwind_subst metasenv subst =
+  List.fold_left
+   (fun (unwinded,metasenv) (i,_) ->
+     let (_,canonical_context,_) =
+       List.find (function (m,_,_) -> m=i) metasenv
+     in
+     let identity_relocation_list =
+      CicMkImplicit.identity_relocation_list_for_metavariable canonical_context
+     in
+      let (_,metasenv',subst') =
+       unwind metasenv subst unwinded (Cic.Meta (i,identity_relocation_list))
+      in
+       subst',metasenv'
+   ) ([],metasenv) subst
+
+(* From now on we recreate a kernel abstraction where substitutions are part of
+ * the calculus *)
+
+let whd subst context term =
+  let term = apply_subst subst term in
+  let context = apply_subst_context subst context in
+  try
+    CicReduction.whd context term
+  with e ->
+    raise (MetaSubstFailure ("Weak head reduction failure: " ^
+      Printexc.to_string e))
+
+let type_of_aux' metasenv subst context term =
+  let term = apply_subst subst term in
+  let context = apply_subst_context subst context in
+  let metasenv =
+    List.map
+      (fun (i, c, t) -> (i, apply_subst_context subst c, apply_subst subst t))
+      (List.filter
+        (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+        metasenv)
+  in
+  try
+    CicTypeChecker.type_of_aux' metasenv context term
+  with CicTypeChecker.TypeCheckerFailure msg ->
+    raise (MetaSubstFailure ("Type checker failure: " ^ msg))
+
diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli
new file mode 100644
index 000000000..bfd279412
--- /dev/null
+++ b/helm/ocaml/cic_unification/cicMetaSubst.mli
@@ -0,0 +1,47 @@
+
+exception AssertFailure of string
+exception MetaSubstFailure of string
+
+(* The entry (i,t) in a substitution means that *)
+(* (META i) have been instantiated with t.      *)
+type substitution = (int * Cic.term) list
+
+(* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
+(* performs as (apply_subst subst t) until it finds an application of   *)
+(* (META [mtr]) that, once unwinding is performed, creates a new        *)
+(* beta-redex; in this case up to [reductions_no] consecutive           *)
+(* beta-reductions are performed.                                       *)
+(* Hint: this function is usually called when [reductions_no]           *)
+(*  eta-expansions have been performed and the head of the new          *)
+(*  application has been unified with (META [meta_to_reduce]):          *)
+(*  during the unwinding the eta-expansions are undone.                 *)
+(* [subst] must be already unwinded                                     *)
+val apply_subst_reducing :
+ substitution -> (int * int) option -> Cic.term -> Cic.term
+
+val apply_subst_context : substitution -> Cic.context -> Cic.context
+
+(* apply_subst subst t                     *)
+(* applies the substitution [subst] to [t] *)
+(* [subst] must be already unwinded        *)
+val apply_subst : substitution -> Cic.term -> Cic.term
+
+(* unwind_subst metasenv subst                         *)
+(* unwinds [subst] w.r.t. itself.                      *)
+(* It can restrict some metavariable in the [metasenv] *)
+val unwind_subst : Cic.metasenv -> substitution -> substitution * Cic.metasenv
+
+val delift : 
+ Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> Cic.term * Cic.metasenv
+
+val ppcontext: ?sep: string -> substitution -> Cic.context -> string
+val ppmetasenv: ?sep: string -> substitution -> Cic.metasenv -> string
+val ppsubst: substitution -> string
+
+(* From now on we recreate a kernel abstraction where substitutions are part of
+ * the calculus *)
+
+val whd: substitution -> Cic.context -> Cic.term -> Cic.term
+val type_of_aux':
+  Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term
+