advances on cpx_lfxs_conf_fle

[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 13744017acc9d98125676b5bc8717a149be51af2..fcc76b0adc5bf72b38129bd36a3ddca7952d4676 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/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
@@ -566,24 +577,62 @@ 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.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 
+                    Some (List.fold_left2 
+                      (fun (m, s) t1 t2 -> 
+                        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
+           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)
 
@@ -827,7 +876,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