1. New paramodulation function

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

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 805ea859f8beef8be33eb03d123b850f37a5c48e..c7b487461963a179bd6333232cefb7ce13385bbf 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -241,9 +241,11 @@ let tipify exc metasenv subst context t ty =
         if is_type attrs then
          metasenv,subst,true
         else
+         let _,cc,ty = NCicUtils.lookup_meta n metasenv in
+         let metasenv,subst,ty = sortfy exc metasenv subst cc ty in
          let metasenv = 
            NCicUntrusted.replace_in_metasenv n
-            (fun attrs,cc,ty -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
+            (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
             metasenv 
          in
           metasenv,subst,false
@@ -253,9 +255,11 @@ let tipify exc metasenv subst context t ty =
          if is_type attrs then
           metasenv,subst,true
          else
+          let _,cc,_,ty = NCicUtils.lookup_subst n subst in
+          let metasenv,subst,ty = sortfy exc metasenv subst cc ty in
           let subst = 
             NCicUntrusted.replace_in_subst n
-             (fun attrs,cc,bo,ty->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
+              (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
              subst 
           in
            optimize_meta metasenv subst (NCicSubstitution.subst_meta lc bo))
@@ -354,8 +358,8 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
        | _ -> assert false)
   | `IsType
   | `IsTerm ->
-     (match ty,t with
-         NCic.Implicit (`Typeof _), _ ->
+     (match ty with
+         NCic.Implicit (`Typeof _) ->
           let (metasenv, subst), ty_t = 
             try 
               NCicMetaSubst.delift 
@@ -375,7 +379,7 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
           in
            delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv
             subst 
-       | _, _ ->
+       | _ ->
         let lty = NCicSubstitution.subst_meta lc ty in
         pp (lazy ("On the types: " ^
           ppterm ~metasenv ~subst ~context lty ^ "=<=" ^
@@ -546,6 +550,15 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
        | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
             unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
 
+       | C.Meta (n,_), C.Meta (m,lc') when 
+           let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
+           let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
+            (n < m && cc1 = cc2) ||
+             let len1 = List.length cc1 in
+             let len2 = List.length cc2 in
+              len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
+          instantiate rdb test_eq_only metasenv subst context m lc'
+            (NCicReduction.head_beta_reduce ~subst t1) (not swap)
        | C.Meta (n,lc), t -> 
           instantiate rdb test_eq_only metasenv subst context n lc 
             (NCicReduction.head_beta_reduce ~subst t) swap