New functorialization: paramod is abstracted over a Orderings.Blob, that is like...

[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 1a2b5471b0cf76910eb0666c1cba0fb96a59b7bb..26dc85cacebadc948661b90ae084159a7499ba78 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -14,9 +14,10 @@
 exception MetaSubstFailure of string Lazy.t
 exception Uncertain of string Lazy.t
 
-let newmeta = 
+let newmeta,maxmeta = 
   let maxmeta = ref 0 in
-  fun () -> incr maxmeta; !maxmeta
+  (fun () -> incr maxmeta; !maxmeta),
+  (fun () -> !maxmeta)
 ;;
 
 exception NotInTheList;;
@@ -220,30 +221,58 @@ let int_of_out_scope_tag tag =
 ;;
 
 
+exception Found;;
+
 (* 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 ~unify metasenv subst context n l t =
-  let unify_list in_scope = 
+  let is_in_scope_meta subst = function
+    | NCic.Meta (i,_) ->
+        (try 
+           let tag, _, _, _ = NCicUtils.lookup_subst i subst in 
+           tag = Some in_scope_tag 
+        with NCicUtils.Subst_not_found _ -> false)
+    | _ -> false
+  in
+  let contains_in_scope subst t = 
+    let rec aux _ () = function
+      | NCic.Meta _ as t ->
+          if is_in_scope_meta subst t then raise Found
+          else ()
+      | t -> 
+          if is_in_scope_meta subst t then raise Found
+          else NCicUtils.fold (fun _ () -> ()) () aux () t
+    in
+    try aux () () t; false with Found -> true
+  in
+  let unify_list ~alpha in_scope = 
     match l with
     | _, NCic.Irl _ -> fun _ _ _ _ _ -> None
     | shift, NCic.Ctx l -> fun metasenv subst context k t ->
-       if flexible_arg subst t then None else
+       if flexible_arg subst t || contains_in_scope subst t then None else
          let lb = List.map (fun t -> t, flexible_arg subst t) l in
          HExtlib.list_findopt
           (fun (li,flexible) i ->
             if flexible || i < in_scope then None else
              let li = NCicSubstitution.lift (k+shift) li in
-             match unify metasenv subst context li t with
-             | Some (metasenv,subst) -> 
-                 Some ((metasenv, subst), NCic.Rel (i+1+k))
-             | None -> None)
+              if alpha then
+               if NCicReduction.alpha_eq metasenv subst context li t then
+                Some ((metasenv,subst), NCic.Rel (i+1+k))
+               else
+                None
+              else
+               match unify metasenv subst context li t with
+               | Some (metasenv,subst) -> 
+                   Some ((metasenv, subst), NCic.Rel (i+1+k))
+               | None -> None)
           lb
   in
   let rec aux (context,k,in_scope) (metasenv, subst as ms) t = 
-   match unify_list in_scope metasenv subst context k t with
+   match unify_list ~alpha:true in_scope metasenv subst context k t with
    | Some x -> x
    | None -> 
+   try
     match t with 
     | NCic.Rel n as t when n <= k -> ms, t
     | NCic.Rel n -> 
@@ -266,12 +295,18 @@ let delift ~unify metasenv subst context n l t =
             (NCicPp.ppterm ~context ~metasenv ~subst t))))
     | NCic.Meta (i,l1) as orig ->
         (try
-           let tag,_,t,_ = NCicUtils.lookup_subst i subst in
-           let in_scope = 
+           let tag,c,t,ty = NCicUtils.lookup_subst i subst in
+           let in_scope, clear = 
              match tag with 
-             | Some tag when tag = in_scope_tag -> 0
-             | Some tag when is_out_scope_tag tag -> int_of_out_scope_tag tag
-             | _ -> in_scope
+             | Some tag when tag = in_scope_tag -> 0, true
+             | Some tag when is_out_scope_tag tag->int_of_out_scope_tag tag,true
+             | _ -> in_scope, false
+           in
+           let ms = 
+             if not clear then ms
+             else 
+               metasenv, 
+               (i,(None,c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst
            in
            aux (context,k,in_scope) ms (NCicSubstitution.subst_meta l1 t)
          with NCicUtils.Subst_not_found _ ->
@@ -368,6 +403,10 @@ let delift ~unify metasenv subst context n l t =
     | t -> 
         NCicUntrusted.map_term_fold_a 
           (fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t
+   with NotInTheList ->
+    match unify_list ~alpha:false in_scope metasenv subst context k t with
+    | Some x -> x
+    | None -> raise NotInTheList
   in
    try aux (context,0,0) (metasenv,subst) t
    with NotInTheList ->
@@ -386,10 +425,7 @@ let delift ~unify metasenv subst context n l t =
       let lc = NCicUtils.expand_local_context lc in
       let l = List.map (NCicSubstitution.lift shift) lc in
        if
-         List.exists
-          (fun t -> 
-                  NCicUntrusted.metas_of_term subst context t = [])
-            l
+        List.exists (fun t-> NCicUntrusted.metas_of_term subst context t = []) l
        then
         raise (Uncertain msg)
        else