From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 6 May 2005 10:13:16 +0000 (+0000)
Subject: added syntax for rewrite (TODO no rewrite-in-Hyp syntax)
X-Git-Tag: single_binding~100
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1e18c75052e7839db7945b4cbd08f460aa57826c;p=helm.git

added syntax for rewrite (TODO no rewrite-in-Hyp syntax)
bold sequent line
more space between the sequent line and the formulae
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index e7506a15d..486c26a74 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -398,7 +398,10 @@ EXTEND
     | [ IDENT "replace" ];
       t1 = tactic_term; "with"; t2 = tactic_term ->
         TacticAst.Replace (loc, t1, t2)
-    (* TODO Rewrite *)
+    | [ IDENT "rewrite" ; IDENT "left" ] ; t = term ->
+        TacticAst.Rewrite (loc,`Left, t, None)
+    | [ IDENT "rewrite" ; IDENT "right" ] ; t = term ->
+        TacticAst.Rewrite (loc,`Right, t, None)
     (* TODO Replace_pattern *)
     | [ IDENT "right" ] -> TacticAst.Right loc
     | [ IDENT "ring" ] -> TacticAst.Ring loc
diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml
index afd2292ba..24a3487b8 100644
--- a/helm/ocaml/cic_transformations/sequent2pres.ml
+++ b/helm/ocaml/cic_transformations/sequent2pres.ml
@@ -85,11 +85,16 @@ let sequent2pres term2pres (_,_,context,ty) =
       []
       (context2pres context)) in
  let pres_goal = term2pres ty in 
- (Box.b_v
-    []
-    [pres_context;
-     b_ink [None,"width","4cm"; None,"height","1px"];
-     pres_goal])
+ (Box.b_h [] [
+   Box.b_space; 
+   (Box.b_v
+      []
+      [Box.b_space;
+       pres_context;
+       b_ink [None,"width","4cm"; None,"height","2px"]; (* sequent line *)
+       Box.b_space; 
+       pres_goal])
+ ])
 ;;
 
 (*
diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 99fc38553..f781ea3d7 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -87,7 +87,10 @@ let rec pp_tactic = function
   | Replace (_, t1, t2) ->
       sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2)
   | Replace_pattern (_, _, _) -> assert false  (* TODO *)
-  | Rewrite (_, _, _, _) -> assert false (* TODO *)
+  | Rewrite (_, pos, t, None) -> 
+      sprintf "rewrite %s %s" 
+        (if pos = `Left then "left" else "right") (pp_term_ast t)
+  | Rewrite _ -> assert false (* TODO *)
   | Right _ -> "right"
   | Ring _ -> "ring"
   | Split _ -> "split"