delift moved from cicSubstitution to cicUnification

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 68276d74bac39f9a68b34cc5349c463908eae610..ae51f35803e20cfd6467b54983afbe6b0dd5747d 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -233,105 +233,3 @@ let lift_meta l t =
  in
   aux 0 t          
 ;;
-
-(************************************************************************)
-(*CSC: spostare in cic_unification *)
-
-(* the delift function takes in input an ordered list of integers [n1,...,nk]
-   and a term t, and relocates rel(nk) to k. Typically, the list of integers 
-   is a parameter of a metavariable occurrence. *)
-
-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
-;;
- 
-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
-;;
-
-
-let delift context metasenv l t =
- 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                 *)
-        else
-        (match List.nth context (m-k-1) with
-          Some (_,C.Def t) -> deliftaux k (lift m t)
-        | Some (_,C.Decl t) ->
-            (* It may augment to_be_restricted *)
-            ignore (deliftaux k (lift m t)) ;
-            C.Rel ((position (m-k) l) + k)
-        | None -> raise RelToHiddenHypothesis)
-    | C.Var _  as t -> t
-    | 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 _ as t -> t
-    | C.Abst _  as t -> t
-    | C.MutInd _ as t -> t
-    | C.MutConstruct _ as t -> t
-    | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
-       C.MutCase (sp, cookingsno, 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 = deliftaux 0 t in
-   res, restrict !to_be_restricted metasenv
-;;

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
index 641d36fee45b4f3fea23cb005206c2b6baa99a58..8915b814ad5b3af609c1013232edd1dd01a69301 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
@@ -26,6 +26,4 @@
 val lift : int -> Cic.term -> Cic.term
 val subst : Cic.term -> Cic.term -> Cic.term
 val lift_meta : (Cic.term option) list -> Cic.term -> Cic.term
-val delift : 
- Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> Cic.term * Cic.metasenv
 val undebrujin_inductive_def : UriManager.uri -> Cic.obj -> Cic.obj

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 2f27bea85adac6a996c5152d40d5b7635996d1c0..4a2cb243066b0a1b3efb0be2a7f88a54aaee65b4 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -29,6 +29,111 @@ exception OccurCheck;;
 exception RelToHiddenHypothesis;;
 exception OpenTerm;;
 
+(**** DELIFT ****)
+
+(* the delift function takes in input an ordered list of integers [n1,...,nk]
+   and a term t, and relocates rel(nk) to k. Typically, the list of integers 
+   is a parameter of a metavariable occurrence. *)
+
+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
+;;
+ 
+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
+;;
+
+
+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                 *)
+         else
+         (match List.nth context (m-k-1) with
+           Some (_,C.Def t) -> deliftaux k (S.lift m t)
+         | Some (_,C.Decl t) ->
+             (* It may augment to_be_restricted *)
+             ignore (deliftaux k (S.lift m t)) ;
+             C.Rel ((position (m-k) l) + k)
+         | None -> raise RelToHiddenHypothesis)
+     | C.Var _  as t -> t
+     | 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 _ as t -> t
+     | C.Abst _  as t -> t
+     | C.MutInd _ as t -> t
+     | C.MutConstruct _ as t -> t
+     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
+        C.MutCase (sp, cookingsno, 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 = deliftaux 0 t in
+    res, restrict !to_be_restricted metasenv
+;;
+
+(**** END OF DELIFT ****)
+
 type substitution = (int * Cic.term) list
 
 (* NUOVA UNIFICAZIONE *)
@@ -76,7 +181,7 @@ let fo_unif_new metasenv context t1 t2 =
 prerr_endline ("DELIFT2(" ^ CicPp.ppterm t ^ ")") ; flush stderr ;
 List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ;
 prerr_endline "<DELIFT2" ; flush stderr ;
-              let t',metasenv' = S.delift context metasenv l t in
+              let t',metasenv' = delift context metasenv l t in
               (n, t')::subst, metasenv'
           in
            let (_,_,meta_type) = 
@@ -194,7 +299,7 @@ let check_accessibility metasenv i =
    List.map
     (function t ->
       let =
-       S.delift canonical_context metasenv ? t
+       delift canonical_context metasenv ? t
     ) canonical_context
 CSCSCS
 
@@ -287,7 +392,7 @@ let unwind metasenv subst unwinded t =
 prerr_endline ("DELIFT(" ^ CicPp.ppterm t' ^ ")") ; flush stderr ;
 List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ;
 prerr_endline "<DELIFT" ; flush stderr ;
-                S.delift canonical_context metasenv' l t'
+                delift canonical_context metasenv' l t'
               in
                unwinded := (i,t')::!unwinded ;
                S.lift_meta l t', metasenv'

diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli
index 2ec49722e412b951241f5275635c021ff830f90c..464927a2d05ff6738da9132c83698febb26d31a4 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.mli
+++ b/helm/ocaml/cic_unification/cicUnification.mli
@@ -27,6 +27,9 @@ exception UnificationFailed
 exception Free
 exception OccurCheck
 
+val delift : 
+ Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> Cic.term * Cic.metasenv
+
 (* The entry (i,t) in a substitution means that *)
 (* (META i) have been instantiated with t.      *)
 type substitution = (int * Cic.term) list