- alpha conversion check added to the brg kernel (succeeds 1/4 of the times)

[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 795b8504296249d2e624d8005a776c2cd2eaa4cb..fc6eea759313223b30c57a7b6215470ea12c24d5 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -104,13 +104,14 @@ let ppmetasenv ~subst:_subst _metasenv = "...";;
 
 let pp _ = ();;
 
-let fix_sorts swap metasenv subst context meta t =
+let fix_sorts swap exc t =
   let rec aux () = function
     | NCic.Sort (NCic.Type u) as orig ->
         if swap then
          match NCicEnvironment.sup u with
-         | None -> prerr_endline "no sup for" ;
-            raise (fail_exc metasenv subst context meta t)
+         | None ->
+            prerr_endline ("no sup for " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] orig) ;
+            raise exc
          | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
         else
          NCic.Sort (NCic.Type (
@@ -143,7 +144,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 +155,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 +164,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
@@ -191,12 +193,13 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
          "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
           ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
           ppmetasenv ~subst metasenv));
+       let exc_to_be = fail_exc metasenv subst context (NCic.Meta (n,lc)) t in
        let t, ty_t = 
          try t, NCicTypeChecker.typeof ~subst ~metasenv context t 
          with 
          | NCicTypeChecker.AssertFailure msg -> 
            (pp (lazy "fine typeof (fallimento)");
-           let ft=fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t in
+           let ft = fix_sorts swap exc_to_be t in
            if ft == t then 
              (prerr_endline ( ("ILLTYPED: " ^ 
                 NCicPp.ppterm ~metasenv ~subst ~context t
@@ -227,7 +230,12 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
            NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
             ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
           let metasenv,subst = 
-            unify test_eq_only metasenv subst context lty ty_t in
+           try
+            unify test_eq_only metasenv subst context lty ty_t
+           with NCicEnvironment.BadConstraint _ as exc ->
+            let ty_t = fix_sorts swap exc_to_be ty_t in 
+             try unify test_eq_only metasenv subst context lty ty_t
+             with _ -> raise exc in
           metasenv, subst, t
   in
          pp (lazy(string_of_int n ^ " := 111 = "^
@@ -351,7 +359,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                     (C.Meta (i,l)) lambda_Mj,
                    i
               | NCic.Meta (i,_) -> (metasenv, subst), i
-              | _ -> assert false
+              | _ ->
+                 raise (UnificationFailure (lazy "Locked term vs non
+                  flexible term; probably not saturated enough yet!"))
              in
               let t1 = NCicReduction.whd ~subst context t1 in
               let j, lj = 
@@ -664,3 +674,5 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
 let unify rdb ?(test_eq_only=false) = 
   indent := "";      
   unify rdb test_eq_only;;
+
+let fix_sorts = fix_sorts false (UnificationFailure (lazy "no sup"));;