let _ =
+ Sys.catch_break true;
let do_old_logging = ref true in
HelmLogger.register_log_callback
(fun ?append_NL html_msg ->
prerr_endline (HelmLogger.string_of_html_msg html_msg));
CicParser.impredicative_set := false;
NCicTypeChecker.set_logger logger;
- NCicPp.set_ppterm NCicPp.trivial_pp_term;
Helm_registry.load_from "conf.xml";
let alluris =
try
in
prerr_endline "ranked....";
prerr_endline (NCicEnvironment.pp_constraints ());
+(*
+ let [_,type0_uri] = mk_type 0 in
+ let [_,type1_uri] = mk_type 1 in
+ let [_,type2_uri] = mk_type 2 in
+ prerr_endline
+ ("Min:" ^
+ (match NCicEnvironment.sup [true,type0_uri;true,type2_uri] with
+ | None -> "NO SUP"
+ | Some t -> NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[]
+ (NCic.Sort (NCic.Type t))));
+*)
HExtlib.profiling_enabled := false;
List.iter (fun uu ->
let uu= OCic2NCic.nuri_of_ouri uu in
ctx @ [(name, (NCic.Decl s))] , t
| t -> [], t
in
- let ctx, ity = intros ty in
- let sty, menv, _ =
+ let rec perforate ctx metasenv = function
+ | NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
+ when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
+ let metasenv, ty = perforate ctx metasenv ty in
+ let a,b,_ = NCicMetaSubst.mk_meta metasenv ctx (`WithType ty) in a,b
+ | t ->
+ NCicUntrusted.map_term_fold_a
+ (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)
+ | t ->
+ NCicUtils.map
+ (fun e ctx -> e::ctx) ctx curryfy t
+ in
+(*
+ let ctx, pty = intros ty in
+ let metasenv, pty = perforate ctx [] pty in
+*)
+(*
+ let sty, metasenv, _ =
NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
in
- let ctx, ty = intros ty in
- let metasenv, subst =
- try
- NCicUnification.unify menv [] ctx ity sty
- with
- | NCicUnification.Uncertain msg
- | NCicUnification.UnificationFailure msg
- | NCicMetaSubst.MetaSubstFailure msg ->
- prerr_endline (Lazy.force msg);
- prerr_endline
- (Printf.sprintf "RESULT OF UNIF\n%s\n%s == %s\n"
- (NCicPp.ppcontext ~metasenv:menv ~subst:[] ctx)
- (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
- (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
- [], []
+*)
+(* let ctx, ty = intros ty in *)
+(*
+ let left, right =
+ match NCicReduction.whd ~delta:max_int ctx pty with
+ | NCic.Appl [eq;t;a;b] -> a, b
+ | _-> assert false
+ in
+*)
+
+(*
+ let whd ty =
+ match ty with
+ | NCic.Appl [eq;t;a;b] ->
+ NCic.Appl [eq;t;NCicReduction.whd ~delta:0 ctx a;b]
+ | t -> NCicReduction.whd ~delta:0 ctx t
in
- if (NCicReduction.are_convertible
- ~subst (fun ~subst:_ _ _ _ ->[]) ctx ity sty)
- then
- prerr_endline ("OK: " ^ NUri.string_of_uri u)
- else
- prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
- (*let inferred_ty =
- NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
- in*)
+*)
+(*
+ prerr_endline
+ (Printf.sprintf "%s == %s"
+ (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx ity)
+ (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx sty));
+*)
+ 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 _ _ _ _ _ -> []) [] [] [] bo None
+ 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 ~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;
;;