| 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"
| `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"
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