From a82bb964ad0bf0969dae008a4de854532846e455 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Sep 2009 12:13:03 +0000
Subject: [PATCH] new tactic constructor: @[n]

---
 helm/software/components/grafite/grafiteAst.ml         |  1 +
 helm/software/components/grafite/grafiteAstPp.ml       |  2 ++
 .../components/grafite_engine/grafiteEngine.ml         |  1 +
 .../components/grafite_parser/grafiteParser.ml         |  3 +++
 helm/software/components/ng_tactics/nTactics.ml        | 10 ++++++++++
 helm/software/components/ng_tactics/nTactics.mli       |  2 ++
 6 files changed, 19 insertions(+)

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
-- 
2.39.2