tacticals are really tactics now, they have an AST at the same level of

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 3b84353310afb0f6b65fb97c87f56eb9ad892d52..214a2d10e92d81b930945461993e8fcb7c5c2d9f 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -100,6 +100,30 @@ let mk_rec_corec ng ind_kind defs loc =
     G.Obj (loc, N.Theorem(flavour, name, ty,
      Some (N.LetRec (ind_kind, defs, body))))
 
+let npunct_of_punct = function
+  | G.Branch loc -> G.NBranch loc
+  | G.Shift loc -> G.NShift loc
+  | G.Pos (loc, i) -> G.NPos (loc, i)
+  | G.Wildcard loc -> G.NWildcard loc
+  | G.Merge loc -> G.NMerge loc
+  | G.Semicolon loc -> G.NSemicolon loc
+  | G.Dot loc -> G.NDot loc
+;;
+let nnon_punct_of_punct = function
+  | G.Skip loc -> G.NSkip loc
+  | G.Unfocus loc -> G.NUnfocus loc
+  | G.Focus (loc,l) -> G.NFocus (loc,l)
+;;
+let npunct_of_punct = function
+  | G.Branch loc -> G.NBranch loc
+  | G.Shift loc -> G.NShift loc
+  | G.Pos (loc, i) -> G.NPos (loc, i)
+  | G.Wildcard loc -> G.NWildcard loc
+  | G.Merge loc -> G.NMerge loc
+  | G.Semicolon loc -> G.NSemicolon loc
+  | G.Dot loc -> G.NDot loc
+;;
+
 type by_continuation =
    BYC_done
  | BYC_weproved of N.term * string option * N.term option
@@ -522,6 +546,17 @@ EXTEND
       | tac = tactic -> tac
         ]
       ];
+  npunctuation_tactical:
+    [
+      [ SYMBOL "[" -> G.NBranch loc
+      | SYMBOL "|" -> G.NShift loc
+      | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
+      | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
+      | SYMBOL "]" -> G.NMerge loc
+      | SYMBOL ";" -> G.NSemicolon loc
+      | SYMBOL "." -> G.NDot loc
+      ]
+    ];
   punctuation_tactical:
     [
       [ SYMBOL "[" -> G.Branch loc
@@ -866,14 +901,20 @@ EXTEND
     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
         G.Tactic (loc, Some tac, punct)
     | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
+    | tac = ntactic; SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
+        G.NTactic (loc, [tac; npunct_of_punct punct])
     | tac = ntactic; punct = punctuation_tactical ->
-        G.NTactic (loc, tac, punct)
-    | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
-        G.NTactic (loc, G.NId loc, punct)
+        G.NTactic (loc, [tac; npunct_of_punct punct])
+    | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
+        G.NTactic (loc, [punct])
     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
         G.NonPunctuationTactical (loc, tac, punct)
-    | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical; punct = punctuation_tactical ->
-        G.NNonPunctuationTactical (loc, tac, punct)
+    | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical; 
+        SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
+          G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
+    | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical; 
+        punct = punctuation_tactical ->
+          G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
     | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
     ]
   ];