X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fcheck.ml;h=bd7f72e70b1d3040448f71290e097fc5a54f0964;hb=5c8de084e314e41f3dc2f605f6242283e930b803;hp=c1ce4260794ce9bb4388dc6a3f756f34eaa2ab5b;hpb=622b14b04e2076d75c283363969dab7d28380bfb;p=helm.git diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index c1ce42607..bd7f72e70 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -66,6 +66,7 @@ let mk_cprop n = let _ = + Sys.catch_break true; let do_old_logging = ref true in HelmLogger.register_log_callback (fun ?append_NL html_msg -> @@ -73,7 +74,6 @@ let _ = 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 @@ -169,6 +169,17 @@ let _ = 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 @@ -182,7 +193,7 @@ let _ = | 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 ) @@ -193,23 +204,129 @@ let _ = NCicTypeChecker.set_logger (fun _ -> ()); do_old_logging := false; prerr_endline "typechecking, first with the new and then with the old kernel"; - let prima = Unix.gettimeofday () in List.iter (fun u -> - let u= OCic2NCic.nuri_of_ouri u in + let u = OCic2NCic.nuri_of_ouri u in indent := 0; - NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u)) + match NCicLibrary.get_obj u with + | _,_,_,_,NCic.Constant (_,_,Some bo, ty, _) -> + let rec intros = function + | NCic.Prod (name, s, t) -> + let ctx, t = intros t in + ctx @ [(name, (NCic.Decl s))] , t + | t -> [], t + in + 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 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 +*) +(* + 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 rdb = { + NRstatus.uhint_db = NCicUnifHint.empty_db; + NRstatus.coerc_db = NCicCoercion.empty_db; + NRstatus.library_db = NCicLibrary.time0; + NRstatus.dump = fun x -> x + } in + let metasenv, subst, bo, infty = + NCicRefiner.typeof rdb [] [] [] bo None + in + let metasenv, subst = + try + NCicUnification.unify rdb 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; - let dopo = Unix.gettimeofday () in - Gc.compact (); - let dopo2 = Unix.gettimeofday () in - Printf.eprintf "NEW typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -. dopo); - CicEnvironment.invalidate (); - Gc.compact (); - let prima = Unix.gettimeofday () in - List.iter (fun u -> ignore (CicTypeChecker.typecheck u)) alluris; - let dopo = Unix.gettimeofday () in - Gc.compact (); - let dopo2 = Unix.gettimeofday () in - Printf.eprintf "OLD typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -. dopo) ;;