From: Enrico Tassi 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"