backport of patches to unification

diff --git a/matita/components/ng_paramodulation/orderings.ml b/matita/components/ng_paramodulation/orderings.ml
index 1e143605b99f13127a80b72a202a56d7851bdb91..f7062b3abebbe2b4d95956ec6f024fd4b46dcb07 100644 (file)
--- a/matita/components/ng_paramodulation/orderings.ml
+++ b/matita/components/ng_paramodulation/orderings.ml
@@ -40,7 +40,8 @@ let rec eq_foterm f x y =
     match x, y with
     | Terms.Leaf t1, Terms.Leaf t2 -> f t1 t2
     | Terms.Var i, Terms.Var j -> i = j
-    | Terms.Node l1, Terms.Node l2 -> List.for_all2 (eq_foterm f) l1 l2
+    | Terms.Node l1, Terms.Node l2 when List.length l1 = List.length l2 -> 
+        List.for_all2 (eq_foterm f) l1 l2
     | _ -> false
 ;;
   

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index 8bc281953ad050ea3a484581a01f9f189cef6a26..b18364509db79f282b7d18372bee0d2cd189f87c 100644 (file)
--- a/matita/components/ng_refiner/nCicMetaSubst.ml
+++ b/matita/components/ng_refiner/nCicMetaSubst.ml
@@ -259,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)
@@ -283,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 
@@ -332,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
@@ -349,9 +349,6 @@ let delift ~unify metasenv subst context n l t =
           lb
   in
   let rec aux (context,k,in_scope) (metasenv, subst as ms) t = 
-   (* XXX if t is closed, we should just terminate. Speeds up hints! *)
-   if NCicUntrusted.looks_closed t then ms, t
-   else 
    match unify_list in_scope metasenv subst context k t with
    | Some x -> x
    | None -> 

diff --git a/matita/components/ng_refiner/nCicMetaSubst.mli b/matita/components/ng_refiner/nCicMetaSubst.mli
index a195a2fd8d55cfcaf7bd88e7946655d3f0fa6fab..1c96577a74121d90639bbc6905dd7345bd5d647a 100644 (file)
--- a/matita/components/ng_refiner/nCicMetaSubst.mli
+++ b/matita/components/ng_refiner/nCicMetaSubst.mli
@@ -71,3 +71,5 @@ val pack_lc : int * NCic.lc_kind -> int * NCic.lc_kind
 
 val is_out_scope_tag : NCic.meta_attrs -> bool
 val int_of_out_scope_tag : NCic.meta_attrs -> int
+
+val is_flexible : NCic.context -> subst:NCic.substitution -> NCic.term -> bool

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index 13744017acc9d98125676b5bc8717a149be51af2..dd1e4b80c520b71e6d96b0e915f98f86e3716659 100644 (file)
--- a/matita/components/ng_refiner/nCicUnification.ml
+++ b/matita/components/ng_refiner/nCicUnification.ml
@@ -566,24 +566,58 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
           instantiate rdb test_eq_only metasenv subst context n lc 
            (NCicReduction.head_beta_reduce ~subst t) (not swap)
 
+       (* higher order unification case *)
        | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
-          let metasenv, lambda_Mj =
-            lambda_intros rdb metasenv subst context (List.length args)
-             (NCicTypeChecker.typeof ~metasenv ~subst context meta)
-          in
-          let metasenv, subst = 
-           unify rdb test_eq_only metasenv subst context 
-            (C.Meta (i,l)) lambda_Mj swap
-          in
-          let metasenv, subst = 
-            unify rdb test_eq_only metasenv subst context t1 t2 swap
-          in
-          (try
-            let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
-            let term = eta_reduce subst term in
-            let subst = List.filter (fun (j,_) -> j <> i) subst in
-            metasenv, ((i, (name, ctx, term, ty)) :: subst)
-          with Not_found -> assert false)
+           (* this easy_case handles "(? ?) =?= (f a)", same number of 
+            * args, preferring the instantiation "f" over "\_.f a" for the
+            * metavariable in head position. Since the arguments of the meta
+            * are flexible, delift would ignore them generating a constant
+            * function even in the easy case above *)
+           let easy_case = 
+             match t2 with
+             | NCic.Appl (f :: f_args)  
+               when List.length args = List.length f_args && 
+               List.exists (NCicMetaSubst.is_flexible context ~subst) args ->
+                 (try 
+                    let metasenv, subst = 
+                      unify rdb test_eq_only metasenv subst context meta f swap
+                    in
+                    Some (List.fold_left2 
+                      (fun (m, s) t1 t2 -> 
+                        unify rdb test_eq_only m s context t1 t2 swap)
+                        (metasenv, subst) args f_args)
+                  with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
+                    None) 
+             | _ -> None
+           in
+           (match easy_case with
+           | Some ms -> ms
+           | None ->
+               (* This case handles "(?_f ..ti..) =?= t2", abstracting every
+                * non flexible ti (delift skips local context items that are
+                * flexible) from t2 in two steps:
+                *  1) ?_f := \..xi.. .?
+                *  2) ?_f ..ti..  =?= t2 --unif_machines-->
+                      ?_f[..ti..] =?= t2 --instantiate-->
+                      delift [..ti..] t2 *)
+               let metasenv, lambda_Mj =
+                 lambda_intros rdb metasenv subst context (List.length args)
+                  (NCicTypeChecker.typeof ~metasenv ~subst context meta)
+               in
+               let metasenv, subst = 
+                 unify rdb test_eq_only metasenv subst context 
+                   (C.Meta (i,l)) lambda_Mj swap
+               in
+               let metasenv, subst = 
+                 unify rdb test_eq_only metasenv subst context t1 t2 swap
+               in
+               (try
+                 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+                 let term = eta_reduce subst term in
+                 let subst = List.filter (fun (j,_) -> j <> i) subst in
+                 metasenv, ((i, (name, ctx, term, ty)) :: subst)
+               with Not_found -> assert false))
+
        | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
            unify rdb test_eq_only metasenv subst context t2 t1 (not swap)