Use an AST for strategy names.

3 files changed, 44 insertions, 30 deletions

diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index b715be9e6..5c46fdf2a 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -79,22 +79,22 @@ ARGUMENT EXTEND rewstrategy
 
     [ glob(c) ] -> [ StratConstr (c, true) ]
   | [ "<-" constr(c) ] -> [ StratConstr (c, false) ]
-  | [ "subterms" rewstrategy(h) ] -> [ StratUnary ("all_subterms", h) ]
-  | [ "subterm" rewstrategy(h) ] -> [ StratUnary ("one_subterm", h) ]
-  | [ "innermost" rewstrategy(h) ] -> [ StratUnary("innermost", h) ]
-  | [ "outermost" rewstrategy(h) ] -> [ StratUnary("outermost", h) ]
-  | [ "bottomup" rewstrategy(h) ] -> [ StratUnary("bottomup", h) ]
-  | [ "topdown" rewstrategy(h) ] -> [ StratUnary("topdown", h) ]
+  | [ "subterms" rewstrategy(h) ] -> [ StratUnary (Subterms, h) ]
+  | [ "subterm" rewstrategy(h) ] -> [ StratUnary (Subterm, h) ]
+  | [ "innermost" rewstrategy(h) ] -> [ StratUnary(Innermost, h) ]
+  | [ "outermost" rewstrategy(h) ] -> [ StratUnary(Outermost, h) ]
+  | [ "bottomup" rewstrategy(h) ] -> [ StratUnary(Bottomup, h) ]
+  | [ "topdown" rewstrategy(h) ] -> [ StratUnary(Topdown, h) ]
   | [ "id" ] -> [ StratId ]
   | [ "fail" ] -> [ StratFail ]
   | [ "refl" ] -> [ StratRefl ]
-  | [ "progress" rewstrategy(h) ] -> [ StratUnary ("progress", h) ]
-  | [ "try" rewstrategy(h) ] -> [ StratUnary ("try", h) ]
-  | [ "any" rewstrategy(h) ] -> [ StratUnary ("any", h) ]
-  | [ "repeat" rewstrategy(h) ] -> [ StratUnary ("repeat", h) ]
-  | [ rewstrategy(h) ";" rewstrategy(h') ] -> [ StratBinary ("compose", h, h') ]
+  | [ "progress" rewstrategy(h) ] -> [ StratUnary (Progress, h) ]
+  | [ "try" rewstrategy(h) ] -> [ StratUnary (Try, h) ]
+  | [ "any" rewstrategy(h) ] -> [ StratUnary (Any, h) ]
+  | [ "repeat" rewstrategy(h) ] -> [ StratUnary (Repeat, h) ]
+  | [ rewstrategy(h) ";" rewstrategy(h') ] -> [ StratBinary (Compose, h, h') ]
   | [ "(" rewstrategy(h) ")" ] -> [ h ]
-  | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ StratBinary ("choice", h, h') ]
+  | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ StratBinary (Choice, h, h') ]
   | [ "old_hints" preident(h) ] -> [ StratHints (true, h) ]
   | [ "hints" preident(h) ] -> [ StratHints (false, h) ]
   | [ "terms" constr_list(h) ] -> [ StratTerms h ]
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index b23bce8be..bd58b0651 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1606,10 +1606,18 @@ let interp_glob_constr_list env sigma =
 
 (* Syntax for rewriting with strategies *)
 
+type unary_strategy = 
+    Subterms | Subterm | Innermost | Outermost
+  | Bottomup | Topdown | Progress | Try | Any | Repeat
+
+type binary_strategy = 
+  | Compose | Choice
+
 type ('constr,'redexpr) strategy_ast = 
   | StratId | StratFail | StratRefl
-  | StratUnary of string * ('constr,'redexpr) strategy_ast
-  | StratBinary of string * ('constr,'redexpr) strategy_ast * ('constr,'redexpr) strategy_ast
+  | StratUnary of unary_strategy * ('constr,'redexpr) strategy_ast
+  | StratBinary of binary_strategy 
+    * ('constr,'redexpr) strategy_ast * ('constr,'redexpr) strategy_ast
   | StratConstr of 'constr * bool
   | StratTerms of 'constr list
   | StratHints of bool * string
@@ -1633,25 +1641,23 @@ let rec strategy_of_ast = function
   | StratUnary (f, s) -> 
     let s' = strategy_of_ast s in
     let f' = match f with
-      | "all_subterms" -> all_subterms
-      | "one_subterm" -> one_subterm
-      | "innermost" -> Strategies.innermost
-      | "outermost" -> Strategies.outermost
-      | "bottomup" -> Strategies.bu
-      | "topdown" -> Strategies.td
-      | "progress" -> Strategies.progress
-      | "try" -> Strategies.try_
-      | "any" -> Strategies.any
-      | "repeat" -> Strategies.repeat
-      | _ -> anomaly ~label:"strategy_of_ast" (str"Unkwnon strategy: " ++ str f)
+      | Subterms -> all_subterms
+      | Subterm -> one_subterm
+      | Innermost -> Strategies.innermost
+      | Outermost -> Strategies.outermost
+      | Bottomup -> Strategies.bu
+      | Topdown -> Strategies.td
+      | Progress -> Strategies.progress
+      | Try -> Strategies.try_
+      | Any -> Strategies.any
+      | Repeat -> Strategies.repeat
     in f' s'
   | StratBinary (f, s, t) ->
     let s' = strategy_of_ast s in
     let t' = strategy_of_ast t in
     let f' = match f with
-      | "compose" -> Strategies.seq
-      | "choice" -> Strategies.choice
-      | _ -> anomaly ~label:"strategy_of_ast" (str"Unkwnon strategy: " ++ str f)
+      | Compose -> Strategies.seq
+      | Choice -> Strategies.choice
     in f' s' t'
   | StratConstr (c, b) -> apply_glob_constr (fst c) b AllOccurrences
   | StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index 926081bbb..05eff00bb 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -18,10 +18,18 @@ open Tacinterp
 
 (** TODO: document and clean me! *)
 
+type unary_strategy = 
+    Subterms | Subterm | Innermost | Outermost
+  | Bottomup | Topdown | Progress | Try | Any | Repeat
+
+type binary_strategy = 
+  | Compose | Choice
+
 type ('constr,'redexpr) strategy_ast = 
   | StratId | StratFail | StratRefl
-  | StratUnary of string * ('constr,'redexpr) strategy_ast
-  | StratBinary of string * ('constr,'redexpr) strategy_ast * ('constr,'redexpr) strategy_ast
+  | StratUnary of unary_strategy * ('constr,'redexpr) strategy_ast
+  | StratBinary of binary_strategy 
+    * ('constr,'redexpr) strategy_ast * ('constr,'redexpr) strategy_ast
   | StratConstr of 'constr * bool
   | StratTerms of 'constr list
   | StratHints of bool * string