From 023b925489d007fc1a39087e2770aac4b2740159 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 14 Oct 2008 17:38:51 +0000 Subject: [PATCH] more work --- helm/software/components/extlib/hExtlib.ml | 1 + helm/software/components/ng_kernel/nCicPp.ml | 2 +- helm/software/components/ng_refiner/check.ml | 31 +++++-- .../components/ng_refiner/nCicMetaSubst.ml | 22 +++-- .../components/ng_refiner/nCicMetaSubst.mli | 8 +- .../components/ng_refiner/nCicRefiner.ml | 82 ++++++++++++------- .../components/ng_refiner/nCicUnification.ml | 29 ++++--- 7 files changed, 118 insertions(+), 57 deletions(-) diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index e2063e451..361587b7d 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -539,6 +539,7 @@ let rec mk_list x = function ;; let list_seq start stop = + if start > stop then [] else let rec aux pos = if pos = stop then [] else pos :: (aux (pos+1)) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index cde028be4..cebdaf0b2 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -137,7 +137,7 @@ let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t = end; F.fprintf f "])" | C.Sort C.Prop -> F.fprintf f "Prop" - | C.Sort (C.Type []) -> F.fprintf f "IllFormedUniverse" + | C.Sort (C.Type []) -> F.fprintf f "Type0" | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u) | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u) | C.Sort (C.Type l) -> diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index 569dcb7df..7fe8cf366 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -198,7 +198,7 @@ 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 @@ -209,25 +209,36 @@ let _ = | 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 a,b,_ = NCicMetaSubst.mk_meta menv ctx (`WithType ty) in a,b | t -> NCicUntrusted.map_term_fold_a (fun e ctx -> e::ctx) ctx perforate menv t in + let rec curryfy ctx = function + | 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 sty, menv, _ = 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 = @@ -243,9 +254,12 @@ let _ = (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity) (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty)); *) + let menv, subst, bo, infty = + NCicRefiner.typeof [] [] [] (curryfy [] bo) None + in let metasenv, subst = try - NCicUnification.unify menv [] ctx left right + NCicUnification.unify menv subst [] infty ty with | NCicUnification.Uncertain msg | NCicUnification.UnificationFailure msg @@ -254,11 +268,16 @@ let _ = [], [] | Sys.Break -> [],[] in - if (NCicReduction.are_convertible ~subst ctx left right) + if (NCicReduction.are_convertible ~subst [] infty ty) then prerr_endline ("OK: " ^ NUri.string_of_uri u) else - (prerr_endline ("FAIL: " ^ NUri.string_of_uri u); + ( + 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\nmenv:\n%s\n" ^^ diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 102958869..72151deb8 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -572,15 +572,22 @@ let delift_rels subst metasenv n t = let mk_meta ?name metasenv context ty = match ty with - | None -> - let len = List.length context in + | `Typeless -> + let n = newmeta () in + let ty = NCic.Implicit (`Typeof n) in + let menv_entry = (n, (name, context, ty)) in + menv_entry :: metasenv,NCic.Meta (n, (0,NCic.Irl (List.length context))), ty + | `Type + | `Term -> + let context_for_ty = if ty = `Type then [] else context in let n = newmeta () in - let ty_menv_entry = (n, (name, context, NCic.Implicit (`Typeof n))) in + let ty_menv_entry = (n, (name,context_for_ty, NCic.Implicit (`Typeof n))) in let m = newmeta () in - let ty = NCic.Meta (n, (0,NCic.Irl len)) in + let ty = NCic.Meta (n, (0,NCic.Irl (List.length context_for_ty))) in let menv_entry = (m, (name, context, ty)) in - menv_entry :: ty_menv_entry :: metasenv, NCic.Meta (m, (0,NCic.Irl len)), ty - | Some ty -> + menv_entry :: ty_menv_entry :: metasenv, + NCic.Meta (m, (0,NCic.Irl (List.length context))), ty + | `WithType ty -> let n = newmeta () in let len = List.length context in let menv_entry = (n, (name, context, ty)) in @@ -591,7 +598,8 @@ 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 (Some s) in + let metasenv1, arg,_ = + mk_meta ~name:name metasenv context (`WithType s) in let t, metasenv1, args, pno = aux metasenv1 (NCicSubstitution.subst arg t) in diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index 77c6d479c..ca2bfb714 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -52,10 +52,12 @@ val restrict: NCic.substitution -> int -> int list -> NCic.metasenv * NCic.substitution * int +(* bool = true if the type of the new meta is closed *) val mk_meta: - ?name:string -> - NCic.metasenv -> NCic.context -> NCic.term option -> - NCic.metasenv * NCic.term * NCic.term (* menv, instance, type *) + ?name:string -> + NCic.metasenv -> NCic.context -> + [ `WithType of NCic.term | `Term | `Type | `Typeless ] -> + NCic.metasenv * NCic.term * NCic.term (* menv, instance, type *) (* returns the resulting type, the metasenv and the arguments *) val saturate: diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index cae9cf54f..36e9b3d24 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -26,30 +26,37 @@ let wrap_exc msg = function ;; let exp_implicit metasenv context expty = + let foo x = match expty with Some t -> `WithType t | None -> x in function - | `Closed -> NCicMetaSubst.mk_meta metasenv [] expty - | `Type | `Term -> NCicMetaSubst.mk_meta metasenv context expty + | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Type) + | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type) + | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term) + | _ -> assert false +;; + +let force_to_sort metasenv subst context t = + match NCicReduction.whd ~subst context t with + | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) as t -> + metasenv, subst, t + | C.Meta (i,(_,lc)) as t -> + let len = match lc with C.Irl len->len | C.Ctx l->List.length l in + prerr_endline "RESTRICT"; + let metasenv, subst, _ = + NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 len) + in + metasenv, subst, t + | C.Sort _ -> metasenv, subst, t | _ -> assert false ;; let sort_of_prod localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) = - let restrict metasenv subst = function - | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) as t -> - metasenv, subst, t - | C.Meta (i,(_,lc)) as t -> - let len = match lc with C.Irl len->len | C.Ctx l->List.length l in - let metasenv, subst, _ = - NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 len) - in - metasenv, subst, t - | t -> metasenv, subst, t - in - let t1 = NCicReduction.whd ~subst context t1 in - let t2 = NCicReduction.whd ~subst ((name,C.Decl s)::context) t2 in - let metasenv, subst, t1 = restrict metasenv subst t1 in - let metasenv, subst, t2 = restrict metasenv subst t2 in + let metasenv, subst, t1 = force_to_sort metasenv subst context t1 in + let metasenv, subst, t2 = + force_to_sort metasenv subst ((name,C.Decl s)::context) t2 in + prerr_endline ("S1:"^NCicPp.ppterm ~metasenv ~subst ~context t1); + prerr_endline ("S2:"^NCicPp.ppterm ~metasenv ~subst ~context:((name,C.Decl s)::context) t2); match t1, t2 with | C.Sort _, C.Sort C.Prop -> metasenv, subst, t2 | C.Sort (C.Type u1), C.Sort (C.Type u2) -> @@ -80,7 +87,7 @@ let check_allowed_sort_elimination localise r orig = match arity1 with | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) -> let metasenv, meta, _ = - NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) None + NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Typeless in let metasenv, subst = try NCicUnification.unify metasenv subst context @@ -93,9 +100,11 @@ let check_allowed_sort_elimination localise r orig = aux metasenv subst ((name, C.Decl so1)::context) (mkapp (NCicSubstitution.lift 1 ind) (C.Rel 1)) de1 meta | C.Sort _ (* , t ==?== C.Prod _ *) -> - let metasenv, meta, _ = - NCicMetaSubst.mk_meta metasenv (("_",C.Decl ind)::context) None - in + let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Typeless in + prerr_endline ( + (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod ("_", ind, meta))) ^ " ==== " ^ + (NCicPp.ppterm ~subst ~metasenv ~context arity2) ^ "\nMENV:\n" + ^ NCicPp.ppmetasenv ~subst metasenv); let metasenv, subst = try NCicUnification.unify metasenv subst context (C.Prod ("_", ind, meta)) arity2 @@ -105,7 +114,8 @@ let check_allowed_sort_elimination localise r orig = (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc) in (try NCicTypeChecker.check_allowed_sort_elimination - ~metasenv ~subst r context ind arity1 arity2 + ~metasenv ~subst r context ind arity1 arity2; + metasenv, subst with exc -> raise (wrap_exc (lazy (localise orig, "Sort elimination not allowed ")) exc)) | _ -> assert false @@ -122,6 +132,10 @@ let rec typeof | C.Implicit _ | C.Lambda _ -> metasenv, subst, t, expty | _ -> + prerr_endline ("F:" ^ + (NCicPp.ppterm ~metasenv ~subst ~context infty) ^ " === " ^ + (NCicPp.ppterm ~metasenv ~subst ~context expty) ^ "\nMENV:\n" ^ + NCicPp.ppmetasenv ~subst metasenv); let metasenv, subst = try NCicUnification.unify metasenv subst context infty expty with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf @@ -134,7 +148,8 @@ let rec typeof | None -> metasenv, subst, t, infty in let rec typeof_aux metasenv subst context expty = - fun t as orig -> (*prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);*) + fun t as orig -> + prerr_endline ("R:"^NCicPp.ppterm ~metasenv ~subst ~context t); let metasenv, subst, t, infty = match t with | C.Rel n -> @@ -187,7 +202,9 @@ let rec typeof | C.Prod (_,s,t) -> Some s, Some t | _ -> None, None in - let metasenv, subst, s, _ = typeof_aux metasenv subst context None s in + let metasenv, subst, s, ty_s = + typeof_aux metasenv subst context None s in + let metasenv, subst, _ = force_to_sort metasenv subst context ty_s in let (metasenv,subst), exp_ty_t = match exp_s with | Some exp_s -> @@ -205,7 +222,9 @@ let rec typeof in metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t) | C.LetIn (n,ty,t,bo) -> - let metasenv, subst, ty, _ = typeof_aux metasenv subst context None ty in + let metasenv, subst, ty, ty_ty = + typeof_aux metasenv subst context None ty in + let metasenv, subst, _ = force_to_sort metasenv subst context ty_ty in let metasenv, subst, t, _ = typeof_aux metasenv subst context (Some ty) t in let context = (n, C.Def (t,ty)) :: context in @@ -238,8 +257,10 @@ let rec typeof else C.Appl ((C.Const r)::parameters) in let metasenv, subst, ind, ind_ty = typeof_aux metasenv subst context None ind in - check_allowed_sort_elimination localise r orig_term metasenv subst context - ind ind_ty outsort; + let metasenv, subst = + check_allowed_sort_elimination localise r orig_term metasenv subst + context ind ind_ty outsort + in (* let's check if the type of branches are right *) if List.length pl <> constructorsno then raise (RefineFailure (lazy (localise orig, @@ -286,9 +307,14 @@ and eat_prods localise metasenv subst context orig_he he ty_he args = typeof ~localise metasenv subst context arg None in let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv - (("_",C.Decl ty_arg) :: context) None + (("_",C.Decl ty_arg) :: context) `Type in let flex_prod = C.Prod ("_", ty_arg, meta) in + prerr_endline ("F:" ^ + (NCicPp.ppterm ~metasenv ~subst ~context t) ^ " === " ^ + (NCicPp.ppterm ~metasenv ~subst ~context flex_prod) ^ "\nMENV:\n" ^ + NCicPp.ppmetasenv ~subst metasenv ^ "\nCTX:\n" ^ + NCicPp.ppcontext ~metasenv ~subst context); let metasenv, subst = try NCicUnification.unify metasenv subst context t flex_prod with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index d34e3efcc..10bc29a62 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -147,19 +147,24 @@ and instantiate test_eq_only metasenv subst context n lc t swap = if swap then unify test_eq_only m s c t2 t1 else unify test_eq_only m s c t1 t2 in - let ty_t = - try NCicTypeChecker.typeof ~subst ~metasenv context t - with NCicTypeChecker.TypeCheckerFailure msg -> - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); - prerr_endline (Lazy.force msg); - assert false - in let name, ctx, ty = NCicUtils.lookup_meta n metasenv in - let lty = NCicSubstitution.subst_meta lc ty in - pp (lazy("On the types: " ^ - NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " - ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); - let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in + let metasenv, subst = + match ty with + | NCic.Implicit (`Typeof _) -> metasenv, subst + | _ -> + let lty = NCicSubstitution.subst_meta lc ty in + let ty_t = + try NCicTypeChecker.typeof ~subst ~metasenv context t + with NCicTypeChecker.TypeCheckerFailure msg -> + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); + prerr_endline (Lazy.force msg); + assert false + in + pp (lazy("On the types: " ^ + NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " + ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); + unify test_eq_only metasenv subst context lty ty_t + in let (metasenv, subst), t = try NCicMetaSubst.delift metasenv subst context n lc t with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg) -- 2.39.2