exception Uncertain of string Lazy.t;;
exception AssertFailure of string Lazy.t;;
-let refiner_typeof =
- ref (fun _ ?localise _ _ _ _ _ -> ignore localise; assert false);;
-let set_refiner_typeof f = refiner_typeof := f
-;;
-
let (===) x y = Pervasives.compare x y = 0 ;;
let uncert_exc metasenv subst context t1 t2 =
in
metasenv, subst, bo
| (arg,ty)::tail ->
+ pp(lazy("arg{ " ^
+ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args arg ^ ":" ^
+ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args ty));
let metasenv, subst, telescopic_ty =
-(* XXX if processed_args = [] then metasenv, subst, ty else *)
+ if processed_args = [] then metasenv, subst, ty else
+ let _ = pp(lazy("delift")) in
delift_type_wrt_terms rdb metasenv subst context_of_args ty
(List.rev processed_args)
in
+ pp(lazy("arg}"));
let name = "HBeta"^string_of_int n in
let metasenv, subst, bo =
mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1)
in
metasenv, subst, NCic.Lambda (name, telescopic_ty, bo)
in
+ pp(lazy("LAMBDA_INTROS{ " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t ^ ":" ^
+ NCicPp.ppterm ~metasenv ~subst ~context tty ^ " over " ^
+ String.concat "," (List.map (NCicPp.ppterm ~metasenv ~subst ~context)args)));
let rc = mk_lambda metasenv subst context 0 [] argsty in
+ pp(lazy("LAMBDA_INTROS}"));
rc
and instantiate rdb test_eq_only metasenv subst context n lc t swap =
assert false)
| NCicTypeChecker.TypeCheckerFailure msg ->
prerr_endline (Lazy.force msg);
+ prerr_endline (
+ "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
+ ppcontext ~metasenv ~subst context ^
+ ppmetasenv ~subst metasenv);
pp msg; assert false
in
let lty = NCicSubstitution.subst_meta lc ty in
(*D*) in outside(); rc with exn -> outside (); raise exn
and delift_type_wrt_terms rdb metasenv subst context t args =
- let metasenv, _, instance, _ =
- NCicMetaSubst.mk_meta metasenv context `Type in
- let meta_applied = NCicUntrusted.mk_appl instance args in
- let metasenv,subst,meta_applied,_ =
- !refiner_typeof ((rdb:> NRstatus.status)#set_coerc_db NCicCoercion.empty_db)
- metasenv subst context meta_applied None
+ let (metasenv, subst), t =
+ try
+ NCicMetaSubst.delift
+ ~unify:(fun m s c t1 t2 ->
+ let ind = !indent in
+ let res =
+ try Some (unify rdb false m s c t1 t2 )
+ with UnificationFailure _ | Uncertain _ -> None
+ in
+ indent := ind; res)
+ metasenv subst context 0 (0,NCic.Ctx (args @
+ List.rev (mk_irl (List.length context)))) t
+ with NCicMetaSubst.MetaSubstFailure _ -> (metasenv, subst), t
in
- let metasenv, subst =
- unify rdb true metasenv subst context meta_applied t in
- let t = NCicSubstitution.lift (List.length args) instance in
- let t = NCicUntrusted.mk_appl t (mk_irl (List.length args)) in
metasenv, subst, t
;;