delift moved from cicSubstitution to cicUnification

[helm.git] / helm / ocaml / cic_proof_checking / cicSubstitution.ml

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
-;;