Back-porting from new Matita:

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

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index dd1e4b80c520b71e6d96b0e915f98f86e3716659..a74172ca0e463b3e449f4fc970f877c677afc677 100644 (file)
--- a/matita/components/ng_refiner/nCicUnification.ml
+++ b/matita/components/ng_refiner/nCicUnification.ml
@@ -382,8 +382,8 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
        | _ ->
         let lty = NCicSubstitution.subst_meta lc ty in
         pp (lazy ("On the types: " ^
-          ppterm ~metasenv ~subst ~context lty ^ "=<=" ^
-          ppterm ~metasenv ~subst ~context ty_t)); 
+          ppterm ~metasenv ~subst ~context ty_t ^ "=<=" ^
+          ppterm ~metasenv ~subst ~context lty)); 
         let metasenv, subst = 
           unify rdb false metasenv subst context ty_t lty false
         in
@@ -559,6 +559,17 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
               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), C.Meta (m,lc') when
+          let _,_,tyn = NCicUtils.lookup_meta n metasenv in
+          let _,_,tym = NCicUtils.lookup_meta m metasenv in
+          let tyn = NCicSubstitution.subst_meta lc tyn in
+          let tym = NCicSubstitution.subst_meta lc tym in
+           match tyn,tym with
+              NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
+               NCicEnvironment.universe_lt u1 u2
+            | _,_ -> false ->
+          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
@@ -575,17 +586,21 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
             * 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 && 
+             | NCic.Appl (f :: f_args)
+               when 
                List.exists (NCicMetaSubst.is_flexible context ~subst) args ->
+                let mlen = List.length args in
+                let flen = List.length f_args in
+                let min_len = min mlen flen in
+                let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
+                let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
                  (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)
+                        unify rdb test_eq_only m s context t1 t2 swap
+                      ) (metasenv,subst)
+                        ((NCicUntrusted.mk_appl meta mhe)::margs)
+                        ((NCicUntrusted.mk_appl f fhe)::fargs))
                   with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
                     None) 
              | _ -> None
@@ -823,10 +838,10 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
            ppterm ~metasenv ~subst ~context 
              (NCicReduction.unwind (k2,e2,t2,s2))));
          pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
-          let relevance = [] (* TO BE UNDERSTOOD 
+          let relevance =
             match t1 with
             | C.Const r -> NCicEnvironment.get_relevance r
-            | _ -> [] *) in
+            | _ -> [] in
           let unif_from_stack (metasenv, subst) (t1, t2, b) =
               try
                 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
@@ -839,7 +854,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
             match l1,l2,r with
             | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
             | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
-            | l1, l2, _ -> 
+            | l1, l2, _ ->
                NCicReduction.unwind (k1,e1,t1,List.rev l1),
                 NCicReduction.unwind (k2,e2,t2,List.rev l2),
                 todo
@@ -848,10 +863,11 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
             match t1, t2 with
             | NCic.Meta _, _ | _, NCic.Meta _ ->
                 (NCicReduction.unwind (k1,e1,t1,s1)),
-                (NCicReduction.unwind (k2,e2,t2,s2)),[]     
+                (NCicReduction.unwind (k2,e2,t2,s2)),[]
             | _ -> check_stack l1 l2 r []
           in
-        let hh1,hh2,todo = check_stack (List.rev s1) (List.rev s2) relevance in
+        let hh1,hh2,todo =
+          check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in
         try
           fo_unif_heads_and_cont_or_unwind_and_hints
             test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) 
@@ -861,7 +877,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
          | KeepReducing _ -> assert false
          | KeepReducingThis _ ->
             assert (not (norm1 && norm2));
-           unif_machines metasenv subst (small_delta_step ~subst m1 m2)
+            unif_machines metasenv subst (small_delta_step ~subst m1 m2)
          | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
            -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
          | UnificationFailure msg