From a9c8d96d47a5895c99bca2fe93decf464bca62c3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 18 May 2009 11:59:53 +0000 Subject: [PATCH] 1) GrafiteAst.NEval => GrafiteAst.NReduce 2) new tactic "nnormalize" implemented 3) "ngeneralize" now uses "wanted" when no term is selected (so that it is possible to use ngeneralize to move an hypothesis down) 4) new syntax for non punctuational tinycals was missing --- .../software/components/grafite/grafiteAst.ml | 2 +- .../grafite_engine/grafiteEngine.ml | 4 +-- .../grafite_parser/grafiteParser.ml | 15 +++++--- helm/software/components/ng_tactics/.depend | 6 ++-- .../components/ng_tactics/.depend.opt | 6 ++-- .../components/ng_tactics/nTactics.ml | 36 ++++++++++++------- .../components/ng_tactics/nTactics.mli | 4 +-- 7 files changed, 48 insertions(+), 25 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 6e48074ad..a2d1ef655 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -56,11 +56,11 @@ type ntactic = | NCase1 of loc * string | NChange of loc * npattern * CicNotationPt.term | NElim of loc * CicNotationPt.term * npattern - | NEval of loc * npattern * [ `Whd of bool ] | NGeneralize of loc * npattern | NId of loc | NIntro of loc * string | NLetIn of loc * npattern * CicNotationPt.term * string + | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern | NRewrite of loc * direction * CicNotationPt.term * npattern type ('term, 'lazy_term, 'reduction, 'ident) tactic = diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 89f50c8fd..ccd02981f 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -616,8 +616,6 @@ let eval_ng_tac (text, prefix_len, tac) = NTactics.elim_tac ~what:(text,prefix_len,what) ~where:(text,prefix_len,where) - | GrafiteAst.NEval (_loc, where, reduction) -> - NTactics.eval_tac ~reduction ~where:(text,prefix_len,where) | GrafiteAst.NGeneralize (_loc, where) -> NTactics.generalize_tac ~where:(text,prefix_len,where) | GrafiteAst.NId _ -> (fun x -> x) @@ -625,6 +623,8 @@ let eval_ng_tac (text, prefix_len, tac) = | GrafiteAst.NLetIn (_loc,where,what,name) -> NTactics.letin_tac ~where:(text,prefix_len,where) ~what:(text,prefix_len,what) name + | GrafiteAst.NReduce (_loc, reduction, where) -> + NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where) | GrafiteAst.NRewrite (_loc,dir,what,where) -> NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what) ~where:(text,prefix_len,where) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 547e51025..742e538fe 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -131,6 +131,15 @@ EXTEND | IDENT "unfold"; t = OPT tactic_term -> `Unfold t | IDENT "whd" -> `Whd ] ]; + nreduction_kind: [ + [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] -> + let delta = match delta with None -> true | _ -> false in + `Normalize delta + (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*) + | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] -> + let delta = match delta with None -> true | _ -> false in + `Whd delta] + ]; sequent_pattern_spec: [ [ hyp_paths = LIST0 @@ -222,12 +231,10 @@ EXTEND | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode> ; t = tactic_term; where = pattern_spec -> G.NLetIn (loc,where,t,name) + | kind = nreduction_kind; p = pattern_spec -> + G.NReduce (loc, kind, p) | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec -> G.NRewrite (loc, dir, what, where) - | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ]; - where = pattern_spec -> - let delta = match delta with None -> true | _ -> false in - G.NEval (loc, where, `Whd delta) | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n) | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_") | SYMBOL "*" -> G.NCase1 (loc,"_") diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend index a4351be54..2e34a62a9 100644 --- a/helm/software/components/ng_tactics/.depend +++ b/helm/software/components/ng_tactics/.depend @@ -1,6 +1,8 @@ +nTacStatus.cmi: nTactics.cmi: nTacStatus.cmi -nTacStatus.cmo: nTacStatus.cmi -nTacStatus.cmx: nTacStatus.cmi +nCicElim.cmi: +nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi +nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi nTactics.cmo: nTacStatus.cmi nTactics.cmi nTactics.cmx: nTacStatus.cmx nTactics.cmi nCicElim.cmo: nCicElim.cmi diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt index a4351be54..2e34a62a9 100644 --- a/helm/software/components/ng_tactics/.depend.opt +++ b/helm/software/components/ng_tactics/.depend.opt @@ -1,6 +1,8 @@ +nTacStatus.cmi: nTactics.cmi: nTacStatus.cmi -nTacStatus.cmo: nTacStatus.cmi -nTacStatus.cmx: nTacStatus.cmi +nCicElim.cmi: +nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi +nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi nTactics.cmo: nTacStatus.cmi nTactics.cmi nTactics.cmx: nTacStatus.cmx nTactics.cmi nCicElim.cmo: nCicElim.cmi diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 7937e8b4b..a0d8eba48 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -336,25 +336,37 @@ let generalize_tac ~where = select_tac ~where ~job:(`Collect l) true; print_tac true "ha selezionato?"; (fun s -> distribute_tac (fun status goal -> - if !l = [] then fail (lazy "No term to generalize"); - let goalty = get_goalty status goal in - let canon = List.hd !l in - let status = + let goalty = get_goalty status goal in + let status,canon,rest = + match !l with + [] -> + (match where with + _,_,(None,_,_) -> fail (lazy "No term to generalize") + | txt,txtlen,(Some what,_,_) -> + let status, what = + disambiguate status (txt,txtlen,what) None (ctx_of goalty) + in + status,what,[] + ) + | he::tl -> status,he,tl in + let status = List.fold_left - (fun s t -> unify s (ctx_of goalty) canon t) status (List.tl !l) - in - let status, canon = term_of_cic_term status canon (ctx_of goalty) in - instantiate status goal - (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ])) + (fun s t -> unify s (ctx_of goalty) canon t) status rest in + let status, canon = term_of_cic_term status canon (ctx_of goalty) in + instantiate status goal + (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ])) ) s) ] ;; -let eval_tac ~reduction ~where = +let reduce_tac ~reduction ~where = let change status t = match reduction with + | `Normalize perform_delta -> + normalize status + ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t | `Whd perform_delta -> - whd status - ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t + whd status + ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t in let where = GrafiteDisambiguate.disambiguate_npattern where in select0_tac ~where ~job:(`ChangeWith change) diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index b558b4c9b..3e13035eb 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -41,8 +41,8 @@ val rewrite_tac: what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> NTacStatus.tactic val generalize_tac : where:NTacStatus.tactic_pattern -> NTacStatus.tactic -val eval_tac: - reduction:[ `Whd of bool ] -> +val reduce_tac: + reduction:[ `Normalize of bool | `Whd of bool ] -> where:NTacStatus.tactic_pattern -> NTacStatus.tactic val letin_tac: where:NTacStatus.tactic_pattern -> -- 2.39.2