delift moved from cicSubstitution to cicUnification

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

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'