basic_rg: improved interface, unwind removed from applicability check

[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 be7a2fe4cab899551151f4745d5fed2851d57cd1..ed650a3c326cd5dedc0ff605f877a638a024453c 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -143,7 +143,6 @@ let rec lambda_intros rdb metasenv subst context t args =
   List.map
   (fun arg -> arg, NCicTypeChecker.typeof ~metasenv ~subst context arg) args in
  let context_of_args = context in
- let mk_appl = function [] -> assert false | [t] -> t | l -> NCic.Appl l in
  let rec mk_lambda metasenv subst context n processed_args = function
    | [] ->
        let metasenv, _, bo, _ = 
@@ -155,7 +154,8 @@ let rec lambda_intros rdb metasenv subst context t args =
        let name = "HBeta"^string_of_int n in
        let metasenv,_,instance,_ =
         NCicMetaSubst.mk_meta metasenv context_of_args `Term in
-       let meta_applied = mk_appl (instance::List.rev processed_args) in
+       let meta_applied =
+        NCicUntrusted.mk_appl instance (List.rev processed_args) in
 let metasenv,subst,_,_ =
  !refiner_typeof ((rdb :> NRstatus.status)#set_coerc_db NCicCoercion.empty_db) metasenv subst context_of_args meta_applied None
 in
@@ -163,7 +163,8 @@ in
         unify rdb true metasenv subst context_of_args meta_applied ty in
        let telescopic_ty = NCicSubstitution.lift n instance in
        let telescopic_ty =
-        mk_appl (telescopic_ty :: mk_irl (List.length processed_args)) in
+        NCicUntrusted.mk_appl
+         telescopic_ty (mk_irl (List.length processed_args)) in
        let metasenv, subst, bo =
         mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1)
          (arg::processed_args) tail
@@ -343,9 +344,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
        | _, NCic.Meta (n, _) when is_locked n subst ->
            (let (metasenv, subst), i = 
               match NCicReduction.whd ~subst context t1 with
-              | NCic.Appl (NCic.Meta (i,l)::args) when
-                  not (NCicMetaSubst.flexible subst args) 
-                ->
+              | NCic.Appl (NCic.Meta (i,l)::args) ->
                  let metasenv, subst, lambda_Mj =
                    lambda_intros rdb metasenv subst context t1 args
                  in
@@ -423,45 +422,41 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
             with Invalid_argument _ -> 
               raise (fail_exc metasenv subst context t1 t2))
 
-       | NCic.Appl (NCic.Meta (i,l)::args), _ when 
-         not (NCicMetaSubst.flexible subst args) ->
-           (* we verify that none of the args is a Meta, 
-              since beta expanding w.r.t a metavariable makes no sense  *)
-              let metasenv, subst, lambda_Mj =
-                lambda_intros rdb metasenv subst context t1 args
-              in
-              let metasenv, subst = 
-                unify rdb test_eq_only metasenv subst context 
-                  (C.Meta (i,l)) lambda_Mj
-              in
-              let metasenv, subst = 
-                unify rdb test_eq_only metasenv subst context t1 t2 
-              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 (i,l)::args) when 
-         not(NCicMetaSubst.flexible subst args) ->
-              let metasenv, subst, lambda_Mj =
-                lambda_intros rdb metasenv subst context t2 args
-              in
-              let metasenv, subst =
-                unify rdb test_eq_only metasenv subst context 
-                 lambda_Mj (C.Meta (i,l))
-              in
-              let metasenv, subst = 
-                unify rdb test_eq_only metasenv subst context t1 t2 
-              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 (i,l)::args), _ ->
+          let metasenv, subst, lambda_Mj =
+            lambda_intros rdb metasenv subst context t1 args
+          in
+          let metasenv, subst = 
+            unify rdb test_eq_only metasenv subst context 
+              (C.Meta (i,l)) lambda_Mj
+          in
+          let metasenv, subst = 
+            unify rdb test_eq_only metasenv subst context t1 t2 
+          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 (i,l)::args) ->
+         let metasenv, subst, lambda_Mj =
+           lambda_intros rdb metasenv subst context t2 args
+         in
+         let metasenv, subst =
+           unify rdb test_eq_only metasenv subst context 
+            lambda_Mj (C.Meta (i,l))
+         in
+         let metasenv, subst = 
+           unify rdb test_eq_only metasenv subst context t1 t2 
+         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)
 
        (* processing this case here we avoid a useless small delta step *)
        | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))