]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nCicMetaSubst.ml
- mk_restricted_irl removed, the non-optimized code was the same
[helm.git] / helm / software / components / ng_refiner / nCicMetaSubst.ml
index aa49a84ee726db1edafa785df5b5cd686aa261f9..12fe977083ec04a2c9ee309c116e2cb22419929b 100644 (file)
@@ -179,15 +179,6 @@ let pack_lc orig =
 ;;
 
 
-let mk_restricted_irl shift len restrictions =
-  let rec aux n =
-    if n = 0 then 0 else
-     if List.mem (n+shift) restrictions then aux (n-1)
-     else 1+aux (n-1)
-  in
-    pack_lc (shift, NCic.Irl (aux len))
-;;
-
 
 let mk_perforated_irl shift len restrictions =
   let rec aux n =
@@ -208,28 +199,22 @@ let rec force_does_not_occur metasenv subst restrictions t =
           List.length (List.filter (fun x -> x < r - k) restrictions) 
         in
         if amount > 0 then ms, NCic.Rel (r - amount) else ms, orig
-    | NCic.Meta (n, l) as orig ->
+    | NCic.Meta (n, (shift,lc as l)) as orig ->
        (* we ignore the subst since restrict will take care of already
         * instantiated/restricted metavariabels *)
        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)
+         let l = NCicUtils.expand_local_context lc in
+         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 restrictions_for_n = [] then
          ms, if l = l' then orig else NCic.Meta (n, l')
@@ -287,13 +272,23 @@ and restrict metasenv subst i restrictions =
         let (metasenv, subst), newbo =  
           force_does_not_occur metasenv subst restrictions bo in
         let j = newmeta () in
-        let subst_entry_j = j, (name, newctx, newty, newbo) in
+        let subst_entry_j = j, (name, newctx, newbo, newty) in
         let reloc_irl = mk_perforated_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,_) as orig -> if i = n then subst_entry_i else orig) subst,
-        j
+        let new_subst = 
+          subst_entry_j :: List.map 
+            (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst
+        in
+(*
+    prerr_endline ("restringo nella subst: " ^string_of_int i ^ " -> " ^ 
+      string_of_int j ^ "\n" ^ 
+      NCicPp.ppsubst ~metasenv [subst_entry_j] ^ "\n\n" ^
+      NCicPp.ppsubst ~metasenv [subst_entry_i] ^ "\n" ^
+      NCicPp.ppterm ~metasenv ~subst ~context:ctx bo ^ " ---- " ^
+      NCicPp.ppterm ~metasenv ~subst ~context:newctx newbo
+            );
+*)
+        metasenv, new_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 "^^
@@ -362,11 +357,9 @@ let delift metasenv subst context n l t =
               let shift1,lc1 = l1 in
               let shift,lc = l in
               let shift = shift + k in
-              let _ = prerr_endline ("XXX restringo " ^ string_of_int i) in
               match lc, lc1 with
               | NCic.Irl len, NCic.Irl len1 
                 when shift1 + len1 < shift || shift1 > shift + len ->
-                        prerr_endline "WWW 1";
                   let restrictions = HExtlib.list_seq 1 (len1 + 1) in
                   let metasenv, subst, newmeta = 
                      restrict metasenv subst i restrictions 
@@ -376,7 +369,6 @@ let delift metasenv subst context n l t =
               | NCic.Irl len, NCic.Irl len1 
                 when shift1 < shift || len1 + shift1 > len + shift ->
                   (* C. Hoare. Premature optimization is the root of all evil*)
-                        prerr_endline ("WWW 2 : " ^ string_of_int i);
                   let stop = shift + len in
                   let stop1 = shift1 + len1 in
                   let low_gap = max 0 (shift - shift1) in
@@ -388,23 +380,26 @@ let delift metasenv subst context n l t =
                     let metasenv, subst, newmeta = 
                        restrict metasenv subst i restrictions 
                     in
+(*
                   prerr_endline ("RESTRICTIONS FOR: " ^ 
-                  NCicPp.ppterm ~metasenv ~subst ~context:[] 
-                    (NCic.Meta (i,l1)) ^ 
-                    " that was part of a term unified with " ^
                     NCicPp.ppterm ~metasenv ~subst ~context:[] 
-                    (NCic.Meta (n,l)) ^ " ====> " ^ 
-                    String.concat "," (List.map string_of_int restrictions)
-                    ^ "\nMENV:\n" ^ NCicPp.ppmetasenv ~subst metasenv
-                    ^ "\nSUBST:\n" ^ NCicPp.ppsubst subst ~metasenv
-                    );
-                  let newlc = 
-                    assert (if shift1 > k then shift1 + low_gap - shift = 0 else
-                    true);
-                    NCic.Irl (len1 - low_gap - high_gap + max 0 (k - shift1)) in
+                    (NCic.Meta (i,l1))^" that was part of a term unified with "
+                    ^ NCicPp.ppterm ~metasenv ~subst ~context:[] (NCic.Meta
+                    (n,l)) ^ " ====> " ^ String.concat "," (List.map
+                    string_of_int restrictions) ^ "\nMENV:\n" ^
+                    NCicPp.ppmetasenv ~subst metasenv ^ "\nSUBST:\n" ^
+                    NCicPp.ppsubst subst ~metasenv);
+*)
+                  let newlc_len = 
+                    len1 - low_gap - high_gap + max 0 (k - shift1) in
+                  assert (if shift1 > k then 
+                    shift1 + low_gap - shift = 0 else true);
                   let meta = 
-                     NCic.Meta(newmeta,(shift1 + low_gap - shift, newlc))
+                     NCic.Meta(newmeta,(shift1 + low_gap - shift, 
+                       NCic.Irl newlc_len))
                   in
+                  let _, cctx, _ = NCicUtils.lookup_meta newmeta metasenv in
+                  assert (List.length cctx = newlc_len);
                     (metasenv, subst), meta
                   
               | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig
@@ -412,12 +407,13 @@ let delift metasenv subst context n l t =
                    ms, NCic.Meta (i, (max 0 (shift1 - shift), lc1))
               | _ ->
                   let lc1 = NCicUtils.expand_local_context lc1 in
+                  let lc1 = List.map (NCicSubstitution.lift shift1) lc1 in
                   let rec deliftl tbr j ms = function
                     | [] -> ms, tbr, []
                     | t::tl ->
                         let ms, tbr, tl = deliftl tbr (j+1) ms tl in
                         try 
-                          let ms, t = aux (k-shift1) ms t in 
+                          let ms, t = aux k ms t in 
                           ms, tbr, t::tl
                         with
                         | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl
@@ -427,7 +423,11 @@ let delift metasenv subst context n l t =
                   prerr_endline ("TO BE RESTRICTED: " ^ 
                    (String.concat "," (List.map string_of_int to_be_r)));
 *)
-                  let l1 = pack_lc (shift, NCic.Ctx lc1') in
+                  let l1 = pack_lc (0, NCic.Ctx lc1') in
+(*
+                  prerr_endline ("newmeta:" ^ NCicPp.ppterm
+                   ~metasenv ~subst ~context (NCic.Meta (999,l1)));
+*)
                   if to_be_r = [] then
                     (metasenv, subst), 
                     (if lc1' = lc1 then orig else NCic.Meta (i,l1))
@@ -435,6 +435,7 @@ let delift metasenv subst context n l t =
                     let metasenv, subst, newmeta = 
                       restrict metasenv subst i to_be_r in
                     (metasenv, subst), NCic.Meta(newmeta,l1))
+
     | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
   in
    try aux 0 (metasenv,subst) t