snapshot (first version in which some extensions work, e.g. infix +)

[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 1a28fa578004b6d0a71b3df0ceea1ab9e7a1aee2..f10443c2d01896c004e750b1e3903dba096c27c5 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -65,7 +65,6 @@ let rec pp_tactic = function
       sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term_ast term)
   | Goal (_, n) -> "goal " ^ string_of_int n
   | Fourier _ -> "fourier"
-  | Hint _ -> "hint"
   | Injection (_, ident) -> "injection " ^ ident
   | Intros (_, None, []) -> "intro"
   | Intros (_, num, idents) ->
@@ -88,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"
@@ -110,8 +112,16 @@ let pp_search_kind = function
   | `Elim -> "elim"
 
 let pp_macro pp_term = function 
+  (* Whelp *)
+  | WInstance (_, term) -> "whelp instance " ^ pp_term term
+  | WHint (_, t) -> "whelp hint " ^ pp_term t
+  | WLocate (_, s) -> "whelp locate " ^ s
+  | WElim (_, t) -> "whelp elim " ^ pp_term t
+  | WMatch (_, term) -> "whelp match " ^ pp_term term
+  (* real macros *)
   | Abort _ -> "Abort"
   | Check (_, term) -> sprintf "Check %s" (pp_term term)
+  | Hint _ -> "hint"
   | Redo (_, None) -> "Redo"
   | Redo (_, Some n) -> sprintf "Redo %d" n
   | Search_pat (_, kind, pat) ->
@@ -195,3 +205,15 @@ and pp_tacticals tacs =
 let pp_tactical tac = pp_tactical tac ^ tactical_terminator
 let pp_tactic tac = pp_tactic tac ^ tactic_terminator
 
+let pp_executable = function
+  | Macro (_,x) -> pp_macro_ast x
+  | Tactical (_,x) -> pp_tactical x
+  | Command (_,x) -> pp_command x
+                      
+let pp_comment = function
+  | Note (_,str) -> sprintf "(* %s *)" str
+  | Code (_,code) -> sprintf "(** %s. **)" (pp_executable code)
+
+let pp_statement = function
+  | Executable (_, ex) -> pp_executable ex
+  | Comment (_, c) -> pp_comment c