X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fcheck.ml;h=2ab8185ab0e2e4725efb8f5eee309bf74852ab7c;hb=8bc5bc0e8375a85736f6a5df317d129d5efa8de4;hp=569dcb7df91b0a7cd84c9f1ae15f1f5ba86cc62c;hpb=5c7b30c4b1033352578c6e38e4fcff4eb0930c44;p=helm.git diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index 569dcb7df..2ab8185ab 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -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 ) @@ -198,36 +209,50 @@ let _ = let u = OCic2NCic.nuri_of_ouri u in indent := 0; match NCicLibrary.get_obj u with - | _,_,_,_,NCic.Constant (_,_,_, ty, _) -> + | _,_,_,_,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 menv = function + 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 menv, ty = perforate ctx menv ty in - let a,b,_ = NCicMetaSubst.mk_meta menv ctx (Some ty) in a,b + 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 menv t + (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 menv, pty = perforate ctx [] pty in + let metasenv, pty = perforate ctx [] pty in +*) (* - let sty, menv, _ = + 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 = @@ -240,39 +265,63 @@ let _ = (* prerr_endline (Printf.sprintf "%s == %s" - (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity) - (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty)); + (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx ity) + (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx sty)); *) - let metasenv, subst = - try - NCicUnification.unify menv [] ctx left right - with - | NCicUnification.Uncertain msg - | NCicUnification.UnificationFailure msg - | NCicMetaSubst.MetaSubstFailure msg -> - prerr_endline (Lazy.force msg); - [], [] - | Sys.Break -> [],[] - in - if (NCicReduction.are_convertible ~subst ctx left right) - then - prerr_endline ("OK: " ^ NUri.string_of_uri u) - else - (prerr_endline ("FAIL: " ^ NUri.string_of_uri u); - prerr_endline - (Printf.sprintf - ("\t\tRESULT OF UNIF\n\nsubst:\n%s\nmenv:\n%s\n" ^^ - "context:\n%s\n%s == %s\n%s == %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 rdb = new NRstatus.status 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; ;;