Bug fixed: restrict used to take the list of positions to be restricted, but

it did not return the (potentially bigger) set of actually restricted positions.
Thus, it was possible to create a local context longer then the canonical one.

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index f63aa9a30759d4a36acae98f99f892738e444dfd..ce0021d3d660d322b5cc1cf2466a2a5e93ffe066 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -96,6 +96,27 @@ let mk_perforated_irl shift len restrictions =
 
 exception Occur;;
 
+let purge_restricted restrictions more_restrictions l =
+ if more_restrictions = [] then l
+ else
+  begin
+   pp (lazy ("TO BE RESTRICTED: " ^ 
+    (String.concat "," (List.map string_of_int restrictions))));
+   pp (lazy ("MORE RESTRICTIONS: " ^ 
+    (String.concat "," (List.map string_of_int more_restrictions))));
+   let shift,lc = l in
+   let lc = NCicUtils.expand_local_context lc in
+    let rec aux n lc =
+     match lc with
+        [] -> []
+      | _ when List.mem n restrictions -> aux (n+1) lc
+      | _::tl when List.mem n more_restrictions -> aux (n+1) tl
+      | he::tl -> he::aux (n+1) tl
+    in
+    pack_lc (shift, NCic.Ctx (aux 1 lc))
+  end
+;;
+
 let rec force_does_not_occur metasenv subst restrictions t =
  let rec aux k ms = function
     | NCic.Rel r when List.mem (r - k) restrictions -> raise Occur
@@ -131,9 +152,9 @@ let rec force_does_not_occur metasenv subst restrictions t =
           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 restrictions_for_n 
-            in
+            let metasenv, subst, newmeta, more_restricted = 
+              restrict metasenv subst n restrictions_for_n in
+            let l' = purge_restricted restrictions more_restricted l' in
               (metasenv, subst), NCic.Meta (newmeta, l'))
     | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
  in
@@ -172,7 +193,7 @@ and erase_in_context metasenv subst pos restrictions = function
         with Occur ->
             metasenv, subst, (pos :: restricted), tl'
 
-and restrict metasenv subst i restrictions =
+and restrict metasenv subst i (restrictions as orig) =
   assert (restrictions <> []);
   try 
     let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in
@@ -191,16 +212,8 @@ and restrict metasenv subst i restrictions =
           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
+        let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
+        metasenv, new_subst, j, diff
       with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
             ("Cannot restrict the context of the metavariable ?%d over "^^
             "the hypotheses %s since ?%d is already instantiated "^^
@@ -221,10 +234,11 @@ and restrict metasenv subst i restrictions =
         let reloc_irl = 
           mk_perforated_irl 0 (List.length ctx) restrictions in
         let subst_entry = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
+        let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
         List.map 
           (fun (n,_) as orig -> if i = n then metasenv_entry else orig) 
           metasenv,
-        subst_entry :: subst, j
+        subst_entry :: subst, j, diff
       with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
           ("Cannot restrict the context of the metavariable ?%d "^^
           "over the hypotheses %s since metavariable's type depends "^^
@@ -372,11 +386,11 @@ let delift ~unify metasenv subst context n l t =
               | NCic.Irl len, NCic.Irl len1 
                 when shift1 + len1 < shift || shift1 > shift + len ->
                   let restrictions = HExtlib.list_seq 1 (len1 + 1) in
-                  let metasenv, subst, newmeta = 
-                     restrict metasenv subst i restrictions 
-                  in
-                  (metasenv, subst), 
-                    NCic.Meta (newmeta, (0,NCic.Irl (max 0 (k-shift1))))
+                  let metasenv, subst, newmeta, more_restricted = 
+                   restrict metasenv subst i restrictions in
+                  let l' = (0,NCic.Irl (max 0 (k-shift1))) in
+                  let l' = purge_restricted restrictions more_restricted l' in
+                  (metasenv, subst),NCic.Meta (newmeta,l')
               | NCic.Irl len, NCic.Irl len1 ->
                   let low_restrictions, new_shift = 
                     if k <= shift1 && shift1 < shift then 
@@ -400,27 +414,12 @@ let delift ~unify metasenv subst context n l t =
                     if shift = k then ms, orig
                     else ms, NCic.Meta (i, (new_shift, lc1))
                   else
-                    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 metasenv, subst, newmeta, more_restricted = 
+                     restrict metasenv subst i restrictions in
                     let newlc_len = len1 - List.length restrictions in 
-                    let meta = 
-                       NCic.Meta(newmeta,(new_shift, NCic.Irl newlc_len))
-                    in
-                    assert (
-                      let _, cctx, _ = NCicUtils.lookup_meta newmeta metasenv in
-                      List.length cctx = newlc_len);
-                    (metasenv, subst), meta
+                    let l' = new_shift, NCic.Irl newlc_len in
+                    let l' = purge_restricted restrictions more_restricted l' in
+                    (metasenv, subst),NCic.Meta(newmeta,l')
 
               | _ ->
                   let lc1 = NCicUtils.expand_local_context lc1 in
@@ -446,9 +445,10 @@ let delift ~unify metasenv subst context n l t =
                     (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))
+                    let metasenv, subst, newmeta, more_restricted = 
+                     restrict metasenv subst i to_be_r in
+                    let l1 = purge_restricted to_be_r more_restricted l1 in
+                     (metasenv, subst), NCic.Meta(newmeta,l1))
 
     | t -> 
         NCicUntrusted.map_term_fold_a 

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index 94a77f287e40b76d21f141e46a012f000da9f255..fd101414df75853f61fe6eabb926ead6ab559036 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.mli
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli
@@ -41,10 +41,15 @@ val delift :
   int -> NCic.local_context -> NCic.term ->
     (NCic.metasenv * NCic.substitution) * NCic.term
 
+(* restrict metasenv subst n l
+   returns metasenv, subst, created meta and l' where l' is the list of
+   additional (i.e. l' does not intersects l) positions whose restriction was
+   forced because of type dependencies *)
 val restrict: 
     NCic.metasenv ->
     NCic.substitution ->
-      int -> int list -> NCic.metasenv * NCic.substitution * int
+    int -> int list ->
+     NCic.metasenv * NCic.substitution * int * int list
 
 (* bool = true if the type of the new meta is closed *)
 val mk_meta: 

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index fdb9c2137332b3c5196b3b10349f1a046b983723..d75fd6ab0948d02129234c44213bf3af89ef2357 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -457,10 +457,10 @@ and force_to_sort rdb metasenv subst context t orig_t localise ty =
      metasenv, subst, t, C.Meta(i,(0,C.Irl 0)) *)
   | C.Meta (i,(_,lc)) ->
      let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
-     let metasenv, subst, newmeta = 
+     let metasenv, subst, newmeta, _ = 
        if len > 0 then
-         NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1)) 
-       else metasenv, subst, i
+         NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1))
+       else metasenv, subst, i, []
      in
      metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0))
   | C.Sort _ as ty -> metasenv, subst, t, ty 

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 1a667770b4ec47b762c8c3d27e090310d2f16f4b..0f73dbc5c9e5f0fd268010092448dbce9c5b9e48 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -453,7 +453,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
              l1 l2 (metasenv, subst, [], List.length l1)
            in
            if to_restrict <> [] then
-             let metasenv, subst, _ = 
+             let metasenv, subst, _, _ = 
                NCicMetaSubst.restrict metasenv subst n1 to_restrict
              in
                metasenv, subst

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index a4a72a18054810b6dead6999ede95b6b0e881baa..6011d912d8f7201fa5e20018ca50b619e3625ff3 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -314,7 +314,7 @@ let clear_tac names =
      names
    in
    let n,h,metasenv,subst,o = status#obj in
-   let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
+   let metasenv,subst,_,_ = NCicMetaSubst.restrict metasenv subst goal js in
     status#set_obj (n,h,metasenv,subst,o))
 ;;