From: Enrico Tassi Date: Fri, 11 Sep 2009 12:13:03 +0000 (+0000) Subject: new tactic constructor: @[n] X-Git-Tag: make_still_working~3474 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a82bb964ad0bf0969dae008a4de854532846e455;p=helm.git new tactic constructor: @[n] --- diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index c84bf99fa..1d3b21392 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -55,6 +55,7 @@ type ntactic = | NCases of loc * CicNotationPt.term * npattern | NCase1 of loc * string | NChange of loc * npattern * CicNotationPt.term + | NConstructor of loc * int option | NElim of loc * CicNotationPt.term * npattern | NGeneralize of loc * npattern | NId of loc diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 89c4e3699..0ec8b9175 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -98,6 +98,8 @@ let rec pp_ntactic ~map_unicode_to_tex = | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^ assert false ^ " " ^ assert false + | NConstructor (_,None) -> "@" + | NConstructor (_,Some x) -> "@" ^ string_of_int x | NCase1 (_,n) -> "*" ^ n ^ ":" | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ " with " ^ CicNotationPp.pp_term wwhat diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index d0d58a6fe..2a04b7470 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -653,6 +653,7 @@ let eval_ng_tac tac = | GrafiteAst.NChange (_loc, pat, ww) -> NTactics.change_tac ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) + | GrafiteAst.NConstructor (_loc,num) -> NTactics.constructor_tac ?num | GrafiteAst.NDot _ -> NTactics.dot_tac | GrafiteAst.NElim (_loc, what, where) -> NTactics.elim_tac diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index c92e3175f..8232aa672 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -253,6 +253,9 @@ EXTEND G.NCases (loc, what, where) | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> G.NChange (loc, what, with_what) + | SYMBOL "@"; num = OPT NUMBER -> + G.NConstructor (loc, + match num with None -> None | Some x -> Some (int_of_string x)) | IDENT "nelim"; what = tactic_term ; where = pattern_spec -> G.NElim (loc, what, where) | IDENT "ngeneralize"; p=pattern_spec -> diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 152c729d0..d8a9fba5e 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -573,6 +573,16 @@ let case1_tac name = if name = "_clearme" then clear_tac ["_clearme"] else id_tac ] ;; +let constructor ?(num=1) status goal = + if num < 1 then fail (lazy "constructor numbers begin with 1"); + let gty = get_goalty status goal in + let status, (r,_,_,_) = analyse_indty status gty in + let ref = NReference.mk_constructor num r in + exec (apply_tac ("",0,Ast.NRef ref)) status goal +;; + +let constructor_tac ?num = distribute_tac (constructor ?num);; + let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> let gty = get_goalty status goal in let eq status ctx t1 t2 = diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index c81b1dd0b..b282b04ca 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -59,3 +59,5 @@ val assert_tac: val auto_tac: params:(NTacStatus.tactic_term list * (string * string) list) -> 's NTacStatus.tactic + +val constructor_tac : ?num:int -> 's NTacStatus.tactic