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 (
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, _ =
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
-prerr_endline ("########################## LI1: " ^ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args meta_applied ^ " vs " ^ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args ty);
-prerr_endline (NCicPp.ppcontext ~metasenv ~subst context_of_args);
-prerr_endline (NCicPp.ppmetasenv metasenv ~subst);
let metasenv,subst =
unify rdb true metasenv subst context_of_args meta_applied ty in
-prerr_endline "UNIFY FINITA";
let telescopic_ty = NCicSubstitution.lift n instance in
let telescopic_ty =
- mk_appl (telescopic_ty :: mk_irl (List.length processed_args)) in
-prerr_endline ("########################## LI: " ^ NCicPp.ppterm ~metasenv ~subst ~context telescopic_ty);
+ 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
"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 = "^
| _, 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
-prerr_endline ("XXXXXXXXX " ^ NCicPp.ppterm ~metasenv ~subst ~context lambda_Mj);
unify rdb test_eq_only metasenv subst context
(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 =
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))
let unify rdb ?(test_eq_only=false) =
indent := "";
unify rdb test_eq_only;;
+
+let fix_sorts = fix_sorts false (UnificationFailure (lazy "no sup"));;
projects / helm.git / blobdiff