| NCicTypeChecker.TypeCheckerFailure s
| NCicEnvironment.ObjectNotFound s
| NCicEnvironment.BadConstraint s
- | NCicEnvironment.BadDependency s as e ->
+ | NCicEnvironment.BadDependency (s,_) as e ->
prerr_endline ("######### " ^ Lazy.force s);
if not ignore_exc then raise e
)
(fun e ctx -> e::ctx) ctx perforate metasenv t
in
let rec curryfy ctx = function
+ | NCic.Lambda (name, (NCic.Sort _ as s), tgt) ->
+ NCic.Lambda (name, s, curryfy ((name,NCic.Decl s) :: ctx) tgt)
| NCic.Lambda (name, s, tgt) ->
let tgt = curryfy ((name,NCic.Decl s) :: ctx) tgt in
NCic.Lambda (name, NCic.Implicit `Type, tgt)
(NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx ity)
(NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx sty));
*)
- let metasenv, subst, bo, infty =
- let bo = curryfy [] bo in
- try NCicRefiner.typeof [] [] [] bo None
- with
- | NCicRefiner.RefineFailure msg
- | NCicRefiner.Uncertain msg ->
- let _, msg = Lazy.force msg in
- prerr_endline msg;
- assert false
- in
- let metasenv, subst =
- try
- NCicUnification.unify metasenv subst [] infty ty
- with
- | NCicUnification.Uncertain msg
- | NCicUnification.UnificationFailure msg
- | NCicMetaSubst.MetaSubstFailure msg ->
- prerr_endline (Lazy.force msg);
- metasenv, subst
- | Sys.Break -> metasenv, subst
- in
- if (NCicReduction.are_convertible ~subst [] infty ty)
- then
- prerr_endline ("OK: " ^ NUri.string_of_uri u)
- else
- (
- let ctx = [] in
- let right = infty in
- let left = ty in
-
- prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
- prerr_endline
- (Printf.sprintf
- ("\t\tRESULT OF UNIF\n\nsubst:\n%s\nmetasenv:\n%s\n" ^^
- "context:\n%s\nTERMS NO SUBST:\n%s\n==\n%s\n"^^
- "TERMS:\n%s\n==\n%s\n")
- (NCicPp.ppsubst ~metasenv subst)
- (NCicPp.ppmetasenv ~subst metasenv)
- (NCicPp.ppcontext ~metasenv ~subst ctx)
- (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx left)
- (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx right)
- (NCicPp.ppterm ~metasenv ~subst ~context:ctx left)
- (NCicPp.ppterm ~metasenv ~subst ~context:ctx right) ))
- (*let inferred_ty =
- NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
- in*)
+ prerr_endline ("start: " ^ NUri.string_of_uri u);
+ let bo = curryfy [] bo in
+ (try
+ let metasenv, subst, bo, infty =
+ NCicRefiner.typeof
+ ~look_for_coercion:(fun _ _ _ _ _ -> [])
+ NCicUnifHint.empty_db [] [] [] bo None
+ in
+ let metasenv, subst =
+ try
+ NCicUnification.unify NCicUnifHint.empty_db metasenv subst [] infty ty
+ with
+ | NCicUnification.Uncertain msg
+ | NCicUnification.UnificationFailure msg
+ | NCicMetaSubst.MetaSubstFailure msg ->
+ prerr_endline (Lazy.force msg);
+ metasenv, subst
+ | Sys.Break -> metasenv, subst
+ in
+ if (NCicReduction.are_convertible ~metasenv ~subst [] infty ty)
+ then
+ prerr_endline ("OK: " ^ NUri.string_of_uri u)
+ else
+ (
+ let ctx = [] in
+ let right = infty in
+ let left = ty in
+
+ prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
+ prerr_endline
+ (Printf.sprintf
+ ("\t\tRESULT OF UNIF\n\nsubst:\n%s\nmetasenv:\n%s\n" ^^
+ "context:\n%s\nTERMS NO SUBST:\n%s\n==\n%s\n"^^
+ "TERMS:\n%s\n==\n%s\n")
+ (NCicPp.ppsubst ~metasenv subst)
+ (NCicPp.ppmetasenv ~subst metasenv)
+ (NCicPp.ppcontext ~metasenv ~subst ctx)
+ (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx left)
+ (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx right)
+ (NCicPp.ppterm ~metasenv ~subst ~context:ctx left)
+ (NCicPp.ppterm ~metasenv ~subst ~context:ctx right) ))
+ (*let inferred_ty =
+ NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
+ in*)
+ with
+ | Sys.Break -> ()
+ | NCicRefiner.RefineFailure msg
+ | NCicRefiner.Uncertain msg ->
+ let _, msg = Lazy.force msg in
+ prerr_endline msg;
+ prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
+ | e ->
+ prerr_endline (Printexc.to_string e);
+ prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
+ )
| _ -> ())
alluris;
;;