New demodulation tactics (mostly for debugging purposes).

[helm.git] / helm / software / components / ng_refiner / nCicMetaSubst.ml

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index ce0021d3d660d322b5cc1cf2466a2a5e93ffe066..549f06f85b57845c97737b609855b5b95fd016cc 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -133,27 +133,33 @@ let rec force_does_not_occur metasenv subst restrictions t =
          NCicUtils.Subst_not_found _ ->
           (* we ignore the subst since restrict will take care of already
            * instantiated/restricted metavariabels *)
-          let (metasenv,subst as ms), restrictions_for_n, l' =
-            let l = NCicUtils.expand_local_context lc in
-         
-            let ms, _, restrictions_for_n, l =
+          let l = NCicUtils.expand_local_context lc in
+          let sl = List.map (NCicSubstitution.lift shift) l in 
+          let (metasenv,subst as 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
+              (*pp (lazy ("L'ORLO DELLA FOSSA: k= " ^ string_of_int k ^ " shift=" ^
+               string_of_int shift ^ " t=" ^ NCicPp.ppterm ~metasenv ~subst ~context:[] t));*)
+                   let ms, t = aux k ms t in
+              (*pp (lazy ("LA FOSSA: " ^ NCicPp.ppterm ~metasenv ~subst ~context:[] t));*)
                    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)
+               sl (ms, List.length l, [], [])
           in
           if restrictions_for_n = [] then
-            ms, if l = l' then orig else NCic.Meta (n, l')
+            ms, if sl = l' then orig else (
+                (*pp (lazy ("FINITO: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[]
+                  ~context:[] (NCic.Meta (n,pack_lc (0, NCic.Ctx l')))));*)
+              NCic.Meta (n, pack_lc (0, NCic.Ctx l'))
+            )
           else
+            let l' = pack_lc (0, NCic.Ctx l') in
+            let _ = pp (lazy ("restrictions for n are:" ^ String.concat "," (List.map string_of_int restrictions_for_n))) in
             let metasenv, subst, newmeta, more_restricted = 
               restrict metasenv subst n restrictions_for_n in
+            let _ = pp (lazy ("more restricted: " ^String.concat "," (List.map string_of_int more_restricted))) 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
@@ -162,6 +168,8 @@ let rec force_does_not_occur metasenv subst restrictions t =
 
 and force_does_not_occur_in_context metasenv subst restrictions = function
   | name, NCic.Decl t as orig ->
+      (* pp (lazy ("CCC: hd is" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t ^
+      "\nCCC: restrictions are:" ^ String.concat "," (List.map string_of_int restrictions)));*)
       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'))
@@ -234,6 +242,9 @@ and restrict metasenv subst i (restrictions as orig) =
         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
+         (* pp (lazy ("BBB: dopo1 \n" ^  NCicPp.ppsubst ~metasenv [subst_entry]));
+          pp (lazy ("BBB: dopo2 \n" ^  NCicPp.ppsubst ~metasenv (subst_entry::subst)));
+          pp (lazy ("BBB: dopo metasenv\n" ^  NCicPp.ppmetasenv ~subst [metasenv_entry]));*)
         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)