From 5fa31e43ffe25aa7b1539653b137968b5cf9899a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 1 Apr 2009 22:37:06 +0000 Subject: [PATCH] New tactic "case1_tac" that make "intro" followed by case of the first argument. It is now possible to write things like: napply t; ## [ #H | *W; #K1 #K2 ] --- .../software/components/grafite/grafiteAst.ml | 1 + .../components/grafite/grafiteAstPp.ml | 3 +- .../grafite_engine/grafiteEngine.ml | 1 + .../grafite_parser/grafiteParser.ml | 3 ++ .../components/ng_tactics/nTactics.ml | 34 ++++++++++++++++++- .../components/ng_tactics/nTactics.mli | 1 + helm/software/matita/tests/a.ma | 5 +-- 7 files changed, 44 insertions(+), 4 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 4f86ff6eb..2deacf2ac 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -51,6 +51,7 @@ type 'term just = type ntactic = | NApply of loc * CicNotationPt.term + | NCase1 of loc * string | NChange of loc * npattern * CicNotationPt.term | NElim of loc * CicNotationPt.term * npattern | NId of loc diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 6a493f834..347eab2da 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -91,12 +91,13 @@ let pp_just ~term_pp = let pp_ntactic ~map_unicode_to_tex = function | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t + | NCase1 (_,n) -> "*" ^ n ^ ":" | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ " with " ^ CicNotationPp.pp_term wwhat | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^ assert false ^ " " ^ assert false | NId _ -> "nid" - | NIntro (_,n) -> n + | NIntro (_,n) -> "#" ^ n ;; let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index b3560150e..634ccc769 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -586,6 +586,7 @@ let eval_ng_punct (_text, _prefix_len, punct) = let eval_ng_tac (text, prefix_len, tac) = match tac with | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) + | GrafiteAst.NCase1 (_loc,n) -> NTactics.case1_tac n | GrafiteAst.NChange (_loc, pat, ww) -> NTactics.change_tac ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index b3bbaf3f8..fa2680811 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -187,6 +187,9 @@ EXTEND | IDENT "nelim"; what = tactic_term ; where = pattern_spec -> GrafiteAst.NElim (loc, what, where) | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n) + | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_") + | SYMBOL "*"; n=IDENT -> + GrafiteAst.NCase1 (loc,n) ] ]; tactic: [ diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 40a490d6b..87be3279f 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -288,6 +288,14 @@ let typeof status where t = None, ctx, ty ;; +let whd status ?delta where t = + let _,_,metasenv,subst,_ = status.pstatus in + let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in + let _,_,t = relocate ctx t in + let t = NCicReduction.whd ~subst ?delta ctx t in + None, ctx, t +;; + let unify status where a b = let n,h,metasenv,subst,o = status.pstatus in let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in @@ -521,4 +529,28 @@ let intro_tac name = exact_tac ("",0,(CicNotationPt.Binder (`Lambda, (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit))) -;; +;; + +let case status goal = + let _,ctx,_ = get_goal status goal in + let ty = typeof status (`Ctx ctx) ("",ctx,NCic.Rel 1) in + let ref = + match whd status (`Ctx ctx) ty with + _,_,NCic.Const ref + | _,_,NCic.Appl (NCic.Const ref :: _) -> ref + | _,_,_ -> fail (lazy ("not an inductive type")) in + let _,_,tl,_,i = NCicEnvironment.get_checked_indtys ref in + let _,_,_,cl = List.nth tl i in + let consno = List.length cl in + let t = + NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1,HExtlib.mk_list (NCic.Implicit `Term) consno) + in + let status,t,ty = refine status (`Ctx ctx) ("",ctx,t) None in + instantiate status goal t +;; + +let case_tac = distribute_tac case;; + +let case1_tac name = + block_tac [ intro_tac name; case_tac ] +;; diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index de8c24738..fbebd4cbb 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -47,5 +47,6 @@ val apply_tac: tactic_term -> tactic val change_tac: where:tactic_pattern -> with_what:tactic_term -> tactic val elim_tac: what:tactic_term -> where:tactic_pattern -> tactic val intro_tac: string -> tactic +val case1_tac: string -> tactic val pp_tac_status: tac_status -> unit diff --git a/helm/software/matita/tests/a.ma b/helm/software/matita/tests/a.ma index 8ca9e669a..29432d2d3 100644 --- a/helm/software/matita/tests/a.ma +++ b/helm/software/matita/tests/a.ma @@ -18,13 +18,14 @@ axiom C : Prop. axiom a: A. axiom b: B. +include "logic/connectives.ma". notation "#" non associative with precedence 90 for @{ 'sharp }. interpretation "a" 'sharp = a. interpretation "b" 'sharp = b. -ntheorem prova : ((A → A → B) → (A → B) → C) → C. +ntheorem prova : ((A ∧ A → B) → (A → B) → C) → C. # H; -napply (H ? ?) [#L | #K1; #K2] +napply (H ? ?) [#L | *w; #K1; #K2] napply #. nqed. \ No newline at end of file -- 2.39.2