1. rewrite_* and rewrite_back_* merged into one function

2. signature of rewrite_* improved
3. concrete syntax for the rewrite direction fixed to ">" and "<"

NOTE: rewrite_* is still no longer working.

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index fc46cc725e8626ee62f5b0bf0bd949ee4386cc7a..9f6476d281981b3a2970f7e7fe1b417da49aa742 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -351,10 +351,8 @@ EXTEND
           wanted, hyp_paths, goal_path ]
   ];
   direction: [
-    [ IDENT "left" -> `Left
-    | SYMBOL ">" -> `Left
-    | IDENT "right" -> `Right
-    | SYMBOL "<" -> `Right ]
+    [ SYMBOL ">" -> `LeftToRight
+    | SYMBOL "<" -> `RightToLeft ]
   ];
   tactic: [
     [ IDENT "absurd"; t = tactic_term ->

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 15961702dcf2e4bfdc192a50c3f8d62fe9e57e6d..d9f909a5fa2eba9abf4f26d78c86ef23bae75f90 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -23,7 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-type direction = [ `Left | `Right ]
+type direction = [ `LeftToRight | `RightToLeft ]
 type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
 
 type loc = CicAst.location

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 33b5e8ade73c04e40d161f74f8fb4c72b66f9dd4..83fdaf0829d7238c20faa991b08f96b373b3201f 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -104,7 +104,8 @@ let rec pp_tactic = function
       sprintf "replace %s with %s" (pp_pattern pattern) (pp_term_ast t)
   | Rewrite (_, pos, t, pattern) -> 
       sprintf "rewrite %s %s %s" 
-        (if pos = `Left then "left" else "right") (pp_term_ast t)
+        (if pos = `LeftToRight then ">" else "<")
+        (pp_term_ast t)
         (pp_pattern pattern)
   | Right _ -> "right"
   | Ring _ -> "ring"

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 05344e0abf93d9debb2135047c297a6528d3dbab..ffc6a9e8176889059623bdb1ae259e5227d5f255 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -183,7 +183,11 @@ and injection1_tac ~term ~i =
                        ))
                      ~continuation:
                        (T.then_
-                         ~start:(EqualityTactics.rewrite_simpl_tac ~term ())
+                         ~start:
+                           (EqualityTactics.rewrite_simpl_tac
+                             ~direction:`LeftToRight
+                             ~pattern:(ProofEngineTypes.conclusion_pattern None)
+                             term)
                          ~continuation:EqualityTactics.reflexivity_tac
                        )
                    ])     
@@ -314,8 +318,11 @@ let discriminate'_tac ~term =
                              ~continuation:
                               (
                                  T.then_
-                                   ~start:(EqualityTactics.rewrite_back_simpl_tac
-                                   ~term ())
+                                   ~start:
+                                     (EqualityTactics.rewrite_simpl_tac
+                                       ~direction:`RightToLeft
+                                       ~pattern:(ProofEngineTypes.conclusion_pattern None)
+                                       term)
                                    ~continuation:(IntroductionTactics.constructor_tac ~n:1) 
                               ))
                              (proof',goal')

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 94f62a955a5297dd2a57c4896185053cbc46b08b..5bbfa33a6f3d27fb04ee3f39401bf5c165e933f5 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -24,7 +24,8 @@
  *)
  
 
-let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) =
+let rewrite_tac ~direction ~pattern equality =
+ let rewrite_tac ~direction ~pattern equality status =
 (*
   let module C = Cic in
   let module U = UriManager in
@@ -33,6 +34,7 @@ let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) =
   let module PEH = ProofEngineHelpers in
   let module PT = PrimitiveTactics in
   let module HLO = HelmLibraryObjects in
+  let proof,goal = status in
   let if_left a b = 
     match direction with
     | `Right -> b
@@ -106,45 +108,22 @@ let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) =
   in
   assert (List.length goals = 0) ;
   (proof',[fresh_meta])
-*) assert false
+  ProofEngineTypes.mk_tactic (rewrite_tac ?where ~term)
+*) assert false in
+ ProofEngineTypes.mk_tactic (rewrite_tac ~direction ~pattern equality)
   
  
-let rewrite_tac ?where ~term () =
-  let rewrite_tac ?where ~term status =
-    rewrite ?where ~term ~direction:`Right status
-  in
-  ProofEngineTypes.mk_tactic (rewrite_tac ?where ~term)
-
-let rewrite_simpl_tac ?where ~term () =
- let rewrite_simpl_tac ?where ~term status =
+let rewrite_simpl_tac ~direction ~pattern equality =
+ let rewrite_simpl_tac ~direction ~pattern equality status =
   ProofEngineTypes.apply_tactic
   (Tacticals.then_ 
-   ~start:(rewrite_tac ?where ~term ())
+   ~start:(rewrite_tac ~direction:`LeftToRight ~pattern equality)
    ~continuation:
      (ReductionTactics.simpl_tac
        ~pattern:(ProofEngineTypes.conclusion_pattern None)))
    status
  in
-   ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
-;;
-
-let rewrite_back_tac ?where ~term () =
-  let rewrite_back_tac ?where ~term status =
-    rewrite ?where ~term ~direction:`Left status
-  in
-  ProofEngineTypes.mk_tactic (rewrite_back_tac ?where ~term)
-
-let rewrite_back_simpl_tac ?where ~term () =
- let rewrite_back_simpl_tac ?where ~term status =
-  ProofEngineTypes.apply_tactic
-   (Tacticals.then_ 
-    ~start:(rewrite_back_tac ?where ~term ())
-    ~continuation:
-     (ReductionTactics.simpl_tac
-       ~pattern:(ProofEngineTypes.conclusion_pattern None)))
-   status
- in
-  ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term)
+   ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~direction ~pattern equality)
 ;;
 
 let replace_tac ~pattern ~with_what =

diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli
index d156ae440d0199940fa8f8b0d47e849c8f74e759..a9b4d1d0b39ed0f7d876005a3b1441d8ffcee030 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.mli
+++ b/helm/ocaml/tactics/equalityTactics.mli
@@ -24,17 +24,11 @@
  *)
 
 val rewrite_tac: 
-  ?where:ProofEngineTypes.pattern -> 
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
+  direction:[`LeftToRight | `RightToLeft] ->
+  pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
 val rewrite_simpl_tac: 
-  ?where:ProofEngineTypes.pattern -> 
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite_back_tac: 
-  ?where:ProofEngineTypes.pattern -> 
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite_back_simpl_tac: 
-  ?where:ProofEngineTypes.pattern -> 
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
+  direction:[`LeftToRight | `RightToLeft] ->
+  pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
   
 val replace_tac: 
   pattern:ProofEngineTypes.pattern ->

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index e6fa4edcd6275e92be398a3f358cf37a8fbcaba6..2fbba97ad5b7d905d48b8ddde2c96bf40a252136 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -886,7 +886,10 @@ let equality_replace a b =
     let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
  debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
     let (proof,goals) = apply_tactic 
-     (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) ())
+     (EqualityTactics.rewrite_simpl_tac
+       ~direction:`LeftToRight
+       ~pattern:(ProofEngineTypes.conclusion_pattern None)
+       (C.Meta (fresh_meta,irl)))
      ((curi,metasenv',pbo,pty),goal)
     in
     let new_goals = fresh_meta::goals in

diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml
index fc2c1c75dc39e7e4d54cd1e188183d95b4270042..055c00528139b5defa52843582d2e7b1a8d5dbec 100644 (file)
--- a/helm/ocaml/tactics/tactics.ml
+++ b/helm/ocaml/tactics/tactics.ml
@@ -58,8 +58,6 @@ let reduce = ReductionTactics.reduce_tac
 let reflexivity = EqualityTactics.reflexivity_tac
 let replace = EqualityTactics.replace_tac
 let rewrite = EqualityTactics.rewrite_tac
-let rewrite_back = EqualityTactics.rewrite_back_tac
-let rewrite_back_simpl = EqualityTactics.rewrite_back_simpl_tac
 let rewrite_simpl = EqualityTactics.rewrite_simpl_tac
 let right = IntroductionTactics.right_tac
 let ring = Ring.ring_tac

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index a8730287e732fabd7b792a86a69a27940179578c..f78624c979849da21ae4b9f95c4769d1c67b0918 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -59,17 +59,11 @@ val replace :
   pattern:ProofEngineTypes.pattern ->
   with_what:Cic.term -> ProofEngineTypes.tactic
 val rewrite :
-  ?where:ProofEngineTypes.pattern ->
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite_back :
-  ?where:ProofEngineTypes.pattern ->
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite_back_simpl :
-  ?where:ProofEngineTypes.pattern ->
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
+  direction:[ `LeftToRight | `RightToLeft ] ->
+  pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
 val rewrite_simpl :
-  ?where:ProofEngineTypes.pattern ->
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
+  direction:[ `LeftToRight | `RightToLeft ] ->
+  pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
 val right : ProofEngineTypes.tactic
 val ring : ProofEngineTypes.tactic
 val set_goal : int -> ProofEngineTypes.tactic