From b0b6b600e029435bfce53f41cd267c669a1f8dc2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 2 Oct 2008 10:26:11 +0000 Subject: [PATCH] we can test the unification algorithm! --- helm/software/components/ng_kernel/nCicPp.ml | 7 ++- helm/software/components/ng_refiner/.depend | 4 +- helm/software/components/ng_refiner/check.ml | 54 +++++++++++++------ .../components/ng_refiner/nCicMetaSubst.ml | 27 ++++++++++ .../components/ng_refiner/nCicMetaSubst.mli | 8 +++ 5 files changed, 82 insertions(+), 18 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 00ea9f24e..5f29d25d8 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -132,7 +132,12 @@ let trivial_pp_term ~context ~subst:_ ~metasenv:_ ?(inside_fix=false) t = if not toplevel then F.fprintf f ")"; F.fprintf f "@]" | C.Implicit _ -> F.fprintf f "?" - | C.Meta (n,_) -> F.fprintf f "?%d" n + | C.Meta (n,(shift,C.Irl len)) -> + F.fprintf f "?%d(%d,%d)" n shift len + | C.Meta (n,(shift,C.Ctx l)) -> + F.fprintf f "?%d(%d,[" n shift; + List.iter (fun x -> aux ctx x; F.fprintf f ",") l; + F.fprintf f "])" | C.Sort C.Prop -> F.fprintf f "Prop" | C.Sort (C.Type []) -> F.fprintf f "IllFormedUniverse" | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u) diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index b71e499a1..42a02ebf1 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -2,7 +2,7 @@ nDiscriminationTree.cmo: nDiscriminationTree.cmi nDiscriminationTree.cmx: nDiscriminationTree.cmi nCicMetaSubst.cmo: nCicMetaSubst.cmi nCicMetaSubst.cmx: nCicMetaSubst.cmi -nCicUnification.cmo: nCicUnification.cmi -nCicUnification.cmx: nCicUnification.cmi +nCicUnification.cmo: nCicMetaSubst.cmi nCicUnification.cmi +nCicUnification.cmx: nCicMetaSubst.cmx nCicUnification.cmi nCicRefiner.cmo: nCicRefiner.cmi nCicRefiner.cmx: nCicRefiner.cmi diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index c1ce42607..4adff1569 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -193,23 +193,47 @@ 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 ctx, ity = intros ty in + let sty, menv, _ = + 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)); + [], [] + 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*) + | _ -> ()) 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) ;; diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index abc9eae6a..188d4dc20 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -547,3 +547,30 @@ let delift_rels subst metasenv n t = delift_rels_from subst metasenv 1 n t *) +let mk_meta ?name metasenv context ty = + let n = newmeta () in + let len = List.length context in + let menv_entry = (n, (name, context, ty)) in + menv_entry :: metasenv, NCic.Meta (n, (0,NCic.Irl len)) +;; + +let saturate ?(delta=0) metasenv context ty goal_arity = + assert (goal_arity >= 0); + let rec aux metasenv = function + | NCic.Prod (name,s,t) -> + let metasenv1, arg = mk_meta ~name:name metasenv context s in + let t, metasenv1, args, pno = + aux metasenv1 (NCicSubstitution.subst arg t) + in + if pno + 1 = goal_arity then + ty, metasenv, [], goal_arity+1 + else + t, metasenv1, arg::args, pno+1 + | ty -> + match NCicReduction.whd context ty ~delta with + | NCic.Prod _ as ty -> aux metasenv ty + | ty -> ty, metasenv, [], 0 + in + let res, newmetasenv, arguments, _ = aux metasenv ty in + res, newmetasenv, arguments +;; diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index 91752fbf7..6c6ddf554 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -52,3 +52,11 @@ val restrict: NCic.substitution -> int -> int list -> NCic.metasenv * NCic.substitution * int +val mk_meta: + ?name:string -> + NCic.metasenv -> NCic.context -> NCic.term -> NCic.metasenv * NCic.term + +val saturate: + ?delta:int -> NCic.metasenv -> NCic.context -> NCic.term -> int -> + NCic.term * NCic.metasenv * NCic.term list + -- 2.39.2