From 7d470885cbbe8c7c102c390eef61e26bff1686c0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 6 Oct 2008 15:02:12 +0000 Subject: [PATCH] 3 nasty bugs fixed: - mk_restricted_irl has been duplicated - mk_restricted_irl generates an irl - mk_perforated_irl generates a restricted local context suitable for a new meta - a wrong optimization in psubst was lifting of a bad amount - force_does_not_occurr was not delifting rels to hypotheses to be cancelled --- .../components/ng_refiner/.depend.opt | 4 +-- helm/software/components/ng_refiner/check.ml | 36 +++++++++++++------ .../software/components/ng_refiner/esempio.ma | 12 ++++++- .../components/ng_refiner/nCicMetaSubst.ml | 33 ++++++++++++++--- .../components/ng_refiner/nCicUnification.ml | 2 +- 5 files changed, 68 insertions(+), 19 deletions(-) diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt index b71e499a1..42a02ebf1 100644 --- a/helm/software/components/ng_refiner/.depend.opt +++ b/helm/software/components/ng_refiner/.depend.opt @@ -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 6f1c9293a..1da400206 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -208,25 +208,35 @@ let _ = let rec perforate ctx menv = 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 NCicMetaSubst.mk_meta menv ctx ty | t -> NCicUntrusted.map_term_fold_a (fun e ctx -> e::ctx) ctx perforate menv t in - let ctx, ity = intros ty in - let menv, pty = perforate [] [] ty 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 = 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" @@ -236,25 +246,31 @@ let _ = let metasenv, subst = try (* prerr_endline ("INIZIO: " ^ NUri.string_of_uri u); *) - NCicUnification.unify menv [] ctx ity pty + NCicUnification.unify menv [] ctx left right 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 pty)); [], [] | Sys.Break -> [],[] in - if (NCicReduction.are_convertible ~subst ctx ity pty) + 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 ("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*) diff --git a/helm/software/components/ng_refiner/esempio.ma b/helm/software/components/ng_refiner/esempio.ma index e686e7eee..613448a61 100644 --- a/helm/software/components/ng_refiner/esempio.ma +++ b/helm/software/components/ng_refiner/esempio.ma @@ -16,8 +16,18 @@ include "nat/plus.ma". definition hole : ∀A:Type.A → A ≝ λA.λx.x. +axiom foo: + ∀P:Type.∀f:P→P→Prop.∀x:P. + (λw. ((∀e:P.f x (w x)) = (∀y:P. f x (hole ? y)))) + (λw:P.hole ? w). (* OK *) + +axiom foo: + ∀P:Type.∀f:P→P→P.∀x,y:P. + (λw.(f x (w x) = f x (w y))) (λw:P.hole ? w). (* OK, restringe Rel1 *) + +axiom foo: (λx,y.(λz. z (x+y) + z x) (λw:nat.hole ? w)) = λx,y.x. (* OK *) axiom foo: (λx,y.(λz. z x + z (x+y)) (λw:nat.hole ? w)) = λx,y.x. (* KO, delift rels only *) -axiom foo: (λx,y.(λz. z (x+y) + z x) (λw:nat.hole ? w)) = λx,y.x. (* OK *) + axiom foo: (λx,y.(λz. z x + z y) (λw:nat.hole ? w)) = λx,y.x. (* OK *) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 188d4dc20..967074a56 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -178,11 +178,22 @@ let pack_lc orig = | _ -> orig ;; + let mk_restricted_irl shift len restrictions = + let rec aux n = + if n = 0 then 0 else + if List.mem (n+shift) restrictions then aux (n-1) + else 1+aux (n-1) + in + pack_lc (shift, NCic.Irl (aux len)) +;; + + +let mk_perforated_irl shift len restrictions = let rec aux n = if n = 0 then [] else - if List.mem (n+shift) restrictions then aux (n-1) - else (NCic.Rel n)::aux (n-1) + if List.mem (n+shift) restrictions then aux (n-1) + else (NCic.Rel n) :: aux (n-1) in pack_lc (shift, NCic.Ctx (List.rev (aux len))) ;; @@ -192,6 +203,11 @@ exception Occur;; let rec force_does_not_occur metasenv subst restrictions t = let rec aux k ms = function | NCic.Rel r when List.mem (r - k) restrictions -> raise Occur + | NCic.Rel r as orig -> + let amount = + List.length (List.filter (fun x -> x < r - k) restrictions) + in + if amount > 0 then ms, NCic.Rel (r - amount) else ms, orig | NCic.Meta (n, l) as orig -> (* we ignore the subst since restrict will take care of already * instantiated/restricted metavariabels *) @@ -272,7 +288,7 @@ and restrict metasenv subst i restrictions = force_does_not_occur metasenv subst restrictions bo in let j = newmeta () in let subst_entry_j = j, (name, newctx, newty, newbo) in - let reloc_irl = mk_restricted_irl 0 (List.length ctx) restrictions in + let reloc_irl = mk_perforated_irl 0 (List.length ctx) restrictions in let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in metasenv, subst_entry_j :: List.map @@ -295,7 +311,12 @@ and restrict metasenv subst i restrictions = force_does_not_occur metasenv subst restrictions ty in let j = newmeta () in let metasenv_entry = j, (name, newctx, newty) in - let reloc_irl = mk_restricted_irl 0 (List.length ctx) restrictions in + prerr_endline ("restricting ?" ^ string_of_int i ^ " to ?" ^ + string_of_int j ^ " : " ^ NCicPp.ppterm ~metasenv ~context:newctx + ~subst newty ^" in a shorter context:\n" ^ + NCicPp.ppcontext ~metasenv ~subst newctx); + let reloc_irl = + mk_perforated_irl 0 (List.length ctx) restrictions in let subst_entry = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in List.map (fun (n,_) as orig -> if i = n then metasenv_entry else orig) @@ -354,7 +375,7 @@ let delift metasenv subst context n l t = restrict metasenv subst i restrictions in (metasenv, subst), - NCic.Meta(newmeta, mk_restricted_irl shift1 len1 restrictions) + NCic.Meta(newmeta, mk_perforated_irl shift1 len1 restrictions) | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig | NCic.Irl _, NCic.Irl _ -> ms, NCic.Meta (i, (shift1 - shift, lc1)) @@ -371,6 +392,8 @@ let delift metasenv subst context n l t = | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl in let (metasenv, subst), to_be_r, lc1' = deliftl [] 1 ms lc1 in + prerr_endline ("TO BE RESTRICTED: " ^ + (String.concat "," (List.map string_of_int to_be_r))); let l1 = pack_lc (shift, NCic.Ctx lc1') in if to_be_r = [] then (metasenv, subst), diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index fcc0b953e..d4a136597 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -171,7 +171,7 @@ and instantiate test_eq_only metasenv subst context n lc t swap = * we could ? := Type_j with j <= i... *) let subst = (n, (name, ctx, t, ty)) :: subst in pp ("?"^string_of_int n^" := "^NCicPp.ppterm - ~metasenv ~subst ~context:ctx t); + ~metasenv ~subst ~context:ctx (NCicSubstitution.subst_meta lc t)); let metasenv = List.filter (fun (m,_) -> not (n = m)) metasenv in -- 2.39.2