changed reduction tactics ast

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 775f13f7d7e0f8803baa7f1a58f9408fd17cc8fa..fddf27e9995a100f72df291fcc478def9cf601fd 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -240,9 +240,9 @@ EXTEND
     [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
   ];
   reduction_kind: [
-    [ "reduce" -> `Reduce
-    | "simpl" -> `Simpl
-    | "whd" -> `Whd ]
+    [ [ IDENT "reduce" | IDENT "Reduce" ] -> `Reduce
+    | [ IDENT "simplify" | IDENT "Simplify" ] -> `Simpl
+    | [ IDENT "whd" | IDENT "Whd" ] -> `Whd ]
   ];
   tactic: [
     [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term ->
@@ -296,7 +296,20 @@ EXTEND
     | [ "let" | "Let" ];
       t = tactic_term; "in"; where = IDENT ->
         return_tactic loc (TacticAst.LetIn (t, where))
-    (* TODO Reduce *)
+    | kind = reduction_kind;
+      pat = OPT [
+        "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] ->
+          pat
+      ];
+      terms = LIST0 term SEP SYMBOL "," ->
+        let tac =
+          (match (pat, terms) with
+          | None, [] -> TacticAst.Reduce (kind, None)
+          | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal))
+          | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat))
+          | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat)))
+        in
+        return_tactic loc tac
     | [ IDENT "reflexivity" | IDENT "Reflexivity" ] ->
         return_tactic loc TacticAst.Reflexivity
     | [ IDENT "replace" | IDENT "Replace" ];

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 7be8293da592073d748b4b37fbbf98307b5af39d..112d87b703860975b38f7626842f59bda7522a82 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -25,7 +25,10 @@
 
 type direction = [ `Left | `Right ]
 type reduction_kind = [ `Reduce | `Simpl | `Whd ]
-type 'term pattern = Pattern of 'term
+(* type 'term pattern = Pattern of 'term *)
+
+  (* everywhere includes goal and hypotheses *)
+type 'term pattern = [ `Goal | `Everywhere ]
 
   (* when an 'ident option is None, the default is to apply the tactic
   to the current goal *)
@@ -56,7 +59,12 @@ type ('term, 'ident) tactic =
   | Left
   | LetIn of 'term * 'ident
 (*   | Named_intros of 'ident list (* joined with Intros above *) *)
-  | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *)
+(*   | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *) *)
+  | Reduce of reduction_kind * ('term list * 'term pattern) option
+      (* kind, (what, where)
+      * if second argument is None, reduction is applied to the current goal,
+      * otherwise to each occurrence of terms given in list occuring in term
+      * pattern *)
   | Reflexivity
   | Replace of 'term * 'term (* what, with what *)
   | Replace_pattern of 'term pattern * 'term

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index 5afb38ca8a1c00f485137e251963710f423bafb0..80e3effce2e31c0580b3330a3ee09f36c6eeec43 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -78,7 +78,7 @@ let rec count_tactic current_size tac =
     | Left -> current_size + 4
     | LetIn (term, ident) ->
        countterm (current_size + 5 + String.length ident) term
-    | Reduce (_, _, _) -> assert false  (* TODO *)
+    | Reduce (_, _) -> assert false  (* TODO *)
     | Reflexivity -> current_size + 11
     | Replace (t1, t2) -> 
        let size1 = countterm (current_size + 14) t1 in (* replace, with *)
@@ -105,7 +105,7 @@ let rec small_tactic2box tac =
 
 let string_of_kind = function
   | `Reduce -> "reduce"
-  | `Simpl -> "simpl"
+  | `Simpl -> "simplify"
   | `Whd -> "whd"
 
 let dummy_tbl = Hashtbl.create 0
@@ -214,7 +214,7 @@ and big_tactic2box = function
                          Box.smallskip;
                          Box.Text([],"=")]);
                Box.indent (ast2astBox term)])
-  | Reduce (_, _, _) -> assert false  (* TODO *)
+  | Reduce (_, _) -> assert false  (* TODO *)
   | Reflexivity -> Box.Text([],"reflexivity")
   | Replace (t1, t2) -> 
       Box.V([],

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 76f1bbd5623961fa624a52e7253ba41027130d77..d0e87b0943e91055f4a4d48bb2091b5703a7d425 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -33,7 +33,7 @@ let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
 
 let pp_reduction_kind = function
   | `Reduce -> "reduce"
-  | `Simpl -> "simpl"
+  | `Simpl -> "simplify"
   | `Whd -> "whd"
 
 let rec pp_tactic = function
@@ -68,7 +68,16 @@ let rec pp_tactic = function
         (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
   | Left -> "left"
   | LetIn (term, ident) -> sprintf "let %s in %s" (pp_term term) ident
-  | Reduce (_, _, _) -> assert false  (* TODO *)
+  | Reduce (kind, None)
+  | Reduce (kind, Some ([], `Goal)) -> pp_reduction_kind kind
+  | Reduce (kind, Some ([], `Everywhere)) ->
+      sprintf "%s in hyp" (pp_reduction_kind kind)
+  | Reduce (kind, Some (terms, `Goal)) ->
+      sprintf "%s %s" (pp_reduction_kind kind)
+        (String.concat ", " (List.map pp_term terms))
+  | Reduce (kind, Some (terms, `Everywhere)) ->
+      sprintf "%s in hyp %s" (pp_reduction_kind kind)
+        (String.concat ", " (List.map pp_term terms))
   | Reflexivity -> "reflexivity"
   | Replace (t1, t2) -> sprintf "replace %s with %s" (pp_term t1) (pp_term t2)
   | Replace_pattern (_, _) -> assert false  (* TODO *)