From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 19 Sep 2008 16:36:32 +0000 (+0000)
Subject: snapshot, cicMsubst compiles
X-Git-Tag: make_still_working~4756
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ee2bbb5aa3f13fbea8cd758e69347d9f1f5ed6bb;p=helm.git

snapshot, cicMsubst compiles
---

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 121131f4d..b5a4646ba 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -155,57 +155,86 @@ exception NotInTheList;;
 let position n (shift, lc) =
   match lc with
   | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList
-  | NCic.Itl len -> n - shift
+  | NCic.Irl len -> n - shift
   | NCic.Ctx tl ->
       let rec aux k = function 
          | [] -> raise NotInTheList
-         | (Cic.Rel m)::_ when m + shift = n -> k
+         | (NCic.Rel m)::_ when m + shift = n -> k
          | _::tl -> aux (k+1) tl 
       in
        aux 1 tl
 ;;
 
+let pack_lc orig = 
+  let rec are_contiguous k = function
+    | [] -> true
+    | (NCic.Rel j) :: tl when j = k+1 -> are_contiguous j tl
+    | _ -> false
+  in
+  match orig with
+  | _, NCic.Ctx [] -> 0, NCic.Irl 0
+  | shift, NCic.Ctx (NCic.Rel k::tl as l) when are_contiguous k tl ->
+      shift+k-1, NCic.Irl (List.length l)
+  | _ -> orig
+;;
+
+let mk_restricted_irl shift len restrictions =
+  let rec aux n =
+    if n = 0 then [] else
+      if List.mem (n+shift) restrictions then aux (n-1)
+      else (NCic.Rel n)::aux (n-1)
+  in
+    pack_lc (shift, NCic.Ctx (List.rev (aux len)))
+;;
+
 exception Occur;;
 
 let rec force_does_not_occur metasenv subst restrictions t =
- let rec aux k = function
-    | C.Rel r when List.mem (r - k) restrictions -> raise Occur
-    | C.Meta (n, l) as t ->
+ let rec aux k (metasenv, subst as  ms) = function
+    | NCic.Rel r when List.mem (r - k) restrictions -> raise Occur
+    | NCic.Meta (n, l) as orig ->
        (* we ignore the subst since restrict will take care of already
         * instantiated/restricted metavariabels *)
-       let more_to_be_restricted = ref [] in
-       let l' =
-         let i = ref 0 in
-         HExtlib.map_option 
-           (fun t ->
-             incr i ;
-             try 
-               let (*subst, metasenv,*) t = aux k t in Some t
-             with Occur ->
-               more_to_be_restricted := !i :: !more_to_be_restricted; None)
-           l
+       let (metasenv,subst as ms), restrictions_for_n, l' =
+         match l with
+         | shift, NCic.Irl len -> 
+             let restrictions = 
+               List.filter 
+                (fun i -> i > shift && i <= shift + len) restrictions in
+             ms, restrictions, mk_restricted_irl shift len restrictions
+         | shift, NCic.Ctx l ->
+            let ms, _, restrictions_for_n, l =
+             List.fold_right
+               (fun t (ms, i, restrictions_for_n, l) ->
+                 try 
+                   let ms, t = aux (k-shift) ms t in
+                   ms, i-1, restrictions_for_n, t::l
+                 with Occur ->
+                   ms, i-1, i::restrictions_for_n, l)
+               l (ms, List.length l, [], [])
+            in
+             ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l)
        in
-       if !more_to_be_restricted = [] then
-         if l = l' then t else NCic.Meta (n, l')
+       if restrictions_for_n = [] then
+         ms, if l = l' then orig else NCic.Meta (n, l')
        else
          let metasenv, subst, newmeta = 
-           restrict metasenv subst n !more_to_be_restricted 
+           restrict metasenv subst n restrictions_for_n 
          in
-           (*metasenv, subst,*) NCic.Meta (newmeta, l')
-    | t -> NCicUtils.map (fun _ k -> k+1) k aux t
+           (metasenv, subst), NCic.Meta (newmeta, l')
+    | t -> NCicUtils.map_term_fold_a (fun _ k -> k+1) k aux ms t
  in
-   aux 0 t 
+   aux 0 (metasenv,subst) t 
 
 and force_does_not_occur_in_context metasenv subst restrictions = function
   | name, NCic.Decl t as orig ->
-      let metasenv, subst, t' =
-        force_does_not_occur metasenv subst restrictions t
-      in
+      let (metasenv, subst), t' =
+        force_does_not_occur metasenv subst restrictions t in
       metasenv, subst, (if t == t' then orig else (name,NCic.Decl t'))
   | name, NCic.Def (bo, ty) as orig ->
-      let metasenv, subst, bo' =
+      let (metasenv, subst), bo' =
         force_does_not_occur metasenv subst restrictions bo in
-      let metasenv, subst, ty' =
+      let (metasenv, subst), ty' =
         force_does_not_occur metasenv subst restrictions ty in
       metasenv, subst, 
        (if bo == bo' && ty == ty' then orig else (name, NCic.Def (bo', ty')))
@@ -214,88 +243,96 @@ and erase_in_context metasenv subst pos restrictions = function
   | [] -> metasenv, subst, restrictions, []
   | hd::tl as orig ->
       let metasenv, subst, restricted, tl' = 
-        erase_in_context metasenv subst (i+1) restrictions tl in
-      if List.mem i restricted then
+        erase_in_context metasenv subst (pos+1) restrictions tl in
+      if List.mem pos restricted then
         metasenv, subst, restricted, tl'
       else
         try
           let metasenv, subst, hd' =
-            let delifted_restricted = List.map ((+) ~-i) restricted in
-             force_does_not_occur_in_context 
-              metasenv susbst delifted_restricted hd
+            let delifted_restricted = 
+              List.map ((+) ~-pos) (List.filter ((<=) pos) restricted) in
+            force_does_not_occur_in_context 
+              metasenv subst delifted_restricted hd
           in
            metasenv, subst, restricted, 
             (if hd' == hd && tl' == tl then orig else (hd' :: tl'))
         with Occur ->
-            metasenv, subst, (i :: restricted), tl'
+            metasenv, subst, (pos :: restricted), tl'
 
 and restrict metasenv subst i restrictions =
   assert (restrictions <> []);
   try 
     let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in
       try 
-        let name, ctx, ty = NCicUtils.lookup_meta i metasenv in
         let metasenv, subst, restrictions, newctx = 
-          erase_in_context metasenv subst 1 restrictions in
-        let metasenv, subst, _ =  
+          erase_in_context metasenv subst 1 restrictions ctx in
+        let (metasenv, subst), newty =  
           force_does_not_occur metasenv subst restrictions ty in
-        let metasenv, subst, _ =  
+        let (metasenv, subst), newbo =  
           force_does_not_occur metasenv subst restrictions bo in
-        (* we don't care newly generated bo/tys since up to subst they are
-         * convertible (only metas are substituted for metas *)
-        metasenv, subst, ?
+        let j = newmeta () in
+        let subst_entry_j = j, (name, newctx, newty, newbo) in
+        let reloc_irl = mk_restricted_irl 0 (List.length ctx) restrictions in
+        let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
+        metasenv,
+        subst_entry_j :: List.map 
+          (fun (n,x) as orig -> if i = n then subst_entry_i else orig) subst,
+        j
       with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
             ("Cannot restrict the context of the metavariable ?%d over "^^
             "the hypotheses %s since ?%d is already instantiated "^^
             "with %s and at least one of the hypotheses occurs in "^^
-            "the substituted term" i  (String.concat ", " 
+            "the substituted term") i  (String.concat ", " 
             (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)) i
-            (NCicPp.ppterm ~metasenv ~subst ~context:ctx bo)))))
+            (NCicPp.ppterm ~metasenv ~subst ~context:ctx bo))))
   with NCicUtils.Subst_not_found _ -> 
     try 
       let name, ctx, ty = NCicUtils.lookup_meta i metasenv in
-      let metasenv, subst, restrictions, newctx = 
-        erase_in_context metasenv subst 1 restrictions in
-      let metasenv, subst, newty =  
-        force_does_not_occur metasenv subst restrictions ty in
-      let j = newmeta () in
-      let metasenv_entry = j, (name, newctx, newty) in
-      let subst_entry = i,(name,ctx, NCic.Meta (j, irl - restrictions), ty) in
-      List.map 
-        (fun (n,x) as orig -> if i = n then metasenv_entry else orig) metasenv,
-      subst_entry :: subst, j
+      try
+        let metasenv, subst, restrictions, newctx = 
+          erase_in_context metasenv subst 1 restrictions ctx in
+        let (metasenv, subst), newty =  
+          force_does_not_occur metasenv subst restrictions ty in
+        let j = newmeta () in
+        let metasenv_entry = j, (name, newctx, newty) in
+        let reloc_irl = mk_restricted_irl 0 (List.length ctx) restrictions in
+        let subst_entry = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
+        List.map 
+          (fun (n,x) as orig -> if i = n then metasenv_entry else orig) 
+          metasenv,
+        subst_entry :: subst, j
+      with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
+          ("Cannot restrict the context of the metavariable ?%d "^^
+          "over the hypotheses %s since metavariable's type depends "^^
+          "on at least one of them") i (String.concat ", " 
+          (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)))))
     with 
     | NCicUtils.Meta_not_found _ -> assert false
-    | Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
-        ("Cannot restrict the context of the metavariable ?%d "^^
-        "over the hypotheses %s since metavariable's type depends "^^
-        "on at least one of them" i (String.concat ", " 
-        (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions))))))
+;;
 
 (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), 
    otherwise the occur check does not make sense in case of unification
    of ?n with ?n *)
 let delift metasenv subst context n l t =
-  let to_be_restricted = ref [] in
-  let rec aux k = function
-    | NCic.Rel n as t when n <= k -> t
+  let rec aux k (metasenv, subst as ms) = function
+    | NCic.Rel n as t when n <= k -> ms, t
     | NCic.Rel n -> 
         (try
           match List.nth context (n-k-1) with
           | _,NCic.Def (bo,_) -> 
-                (try C.Rel ((position (n-k) l) + k)
+                (try ms, NCic.Rel ((position (n-k) l) + k)
                  with NotInTheList ->
                 (* CSC: This bit of reduction hurts performances since it is
                  * possible to  have an exponential explosion of the size of the
                  * proof. required for nat/nth_prime.ma *)
-                  aux k (NCicSubstitution.lift n bo))
-          | _,NCic.Decl _ -> NCic.Rel ((position (n-k) l) + k)
+                  aux k ms (NCicSubstitution.lift n bo))
+          | _,NCic.Decl _ -> ms, NCic.Rel ((position (n-k) l) + k)
         with Failure _ -> assert false) (*Unbound variable found in delift*)
     | NCic.Meta (i,l1) as orig ->
         (try
-           let _,_,t,_ = NCicUtil.lookup_subst i subst in
-           aux k (NCicSubstitution.subst_meta l1 t)
-         with NCicUtil.Subst_not_found _ ->
+           let _,_,t,_ = NCicUtils.lookup_subst i subst in
+           aux k ms (NCicSubstitution.subst_meta l1 t)
+         with NCicUtils.Subst_not_found _ ->
            (* see the top level invariant *)
            if (i = n) then 
             raise (MetaSubstFailure (lazy (Printf.sprintf (
@@ -313,33 +350,39 @@ let delift metasenv subst context n l t =
                      HExtlib.list_seq 1 (shift - shift1) @
                      HExtlib.list_seq (shift+len+1) (shift1+len1)
                   in
-                  let subst, metasenv, newmeta = 
+                  let metasenv, subst, newmeta = 
                      restrict metasenv subst i restrictions 
                   in
-                  (* return that meta *)
-                  assert false
-              | NCic.Irl len, NCic.Irl len1 when shift = 0 -> orig
+                  (metasenv, subst), 
+                  NCic.Meta(newmeta, mk_restricted_irl shift1 len1 restrictions)
+              | NCic.Irl len, NCic.Irl len1 when shift = 0 -> ms, orig
               | NCic.Irl len, NCic.Irl len1 ->
-                   NCic.Meta (i, (shift1 - shift, lc1))
+                   ms, NCic.Meta (i, (shift1 - shift, lc1))
               | _ -> 
+                  let to_be_restricted = ref [] in
                   let lc1 = NCicUtils.expand_local_context lc1 in
-                  let rec deliftl j = function
-                    | [] -> []
+                  let rec deliftl tbr j ms = function
+                    | [] -> ms, tbr, []
                     | t::tl ->
-                        let tl = deliftl (j+1) tl in
-                        try (aux (k+shift1) t)::tl
+                        let ms, tbr, tl = deliftl tbr (j+1) ms tl in
+                        try 
+                          let ms, t = aux (k-shift1) ms t in 
+                          ms, tbr, t::tl
                         with
-                        | NotInTheList | MetaSubstFailure _ ->
-                            to_be_restricted := (i,j)::!to_be_restricted; 
-                            tl
+                        | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl
                   in
-                  let l1 = deliftl 1 l1 in
-                  C.Meta(i,l1)) (* or another ?k and possibly compress l1 *)
-    | t -> NCicUtils.map (fun _ k -> k+1) k aux t
+                  let (metasenv, subst), to_be_r, lc1' = deliftl [] 1 ms lc1 in
+                  let l1 = pack_lc (shift, NCic.Ctx lc1') in
+                  if to_be_r = [] then
+                    (metasenv, subst), 
+                    (if lc1' = lc1 then orig else NCic.Meta (i,l1))
+                  else
+                    let metasenv, subst, newmeta = 
+                      restrict metasenv subst i to_be_r in
+                    (metasenv, subst), NCic.Meta(newmeta,l1))
+    | t -> NCicUtils.map_term_fold_a (fun _ k -> k+1) k aux ms t
   in
-  let t = aux 0 t in
-  let metasenv, subst = restrict subst !to_be_restricted metasenv in
-  metasenv, subst, t
+    aux 0 (metasenv,subst) t
 ;;
 
 (*
diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index 322330488..8f03ccb11 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.mli
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli
@@ -45,5 +45,5 @@ val restrict :
 val delift : 
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
   int -> NCic.local_context -> NCic.term ->
-    Cic.metasenv * Cic.substitution * Cic.term
+    (NCic.metasenv * NCic.substitution) * NCic.term