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 (
"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
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 = "^
(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 =
let unify rdb ?(test_eq_only=false) =
indent := "";
unify rdb test_eq_only;;
+
+let fix_sorts = fix_sorts false (UnificationFailure (lazy "no sup"));;