Syntax for coercion nocomposites fixed.

[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..b18364509db79f282b7d18372bee0d2cd189f87c 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) 
@@ -248,16 +259,16 @@ and restrict metasenv subst i (restrictions as orig) =
     | NCicUtils.Meta_not_found _ -> assert false
 ;;
 
-let rec flexible_arg context subst = function 
+let rec is_flexible context ~subst = function 
   | NCic.Meta (i,_) ->
       (try 
         let _,_,t,_ = List.assoc i subst in
-        flexible_arg context subst t
+        is_flexible context ~subst t
       with Not_found -> true)
   | NCic.Appl (NCic.Meta (i,_) :: args)-> 
       (try 
         let _,_,t,_ = List.assoc i subst in
-        flexible_arg context subst 
+        is_flexible context ~subst 
           (NCicReduction.head_beta_reduce ~delta:max_int 
             (NCic.Appl (t :: args)))
       with Not_found -> true)
@@ -272,7 +283,7 @@ let rec flexible_arg context subst = function
          match List.nth context (i-1)
          with 
          | _,NCic.Def (bo,_) ->
-               flexible_arg context subst
+               is_flexible context ~subst
                  (NCicSubstitution.lift i bo)
          | _ -> false
       with 
@@ -321,11 +332,11 @@ let delift ~unify metasenv subst context n l t =
     match l with
     | _, NCic.Irl _ -> fun _ _ _ _ _ -> None
     | shift, NCic.Ctx l -> fun metasenv subst context k t ->
-       if flexible_arg context subst t || contains_in_scope subst t then None else
+       if is_flexible context ~subst t || contains_in_scope subst t then None else
          let lb = 
            List.map (fun t -> 
             let t = NCicSubstitution.lift (k+shift) t in
-            t, flexible_arg context subst t) 
+            t, is_flexible context ~subst t) 
            l 
          in
          HExtlib.list_findopt