let tactical_terminator = "."
let tactic_terminator = tactical_terminator
+let command_terminator = tactical_terminator
let tactical_separator = ";"
let pp_term_ast term = CicAstPp.pp_term term
| `Reduce -> "reduce"
| `Simpl -> "simplify"
| `Whd -> "whd"
+ | `Normalize -> "normalize"
let rec pp_tactic = function
| Absurd (_, term) -> "absurd" ^ pp_term_ast term
| `Elim -> "elim"
let pp_macro pp_term = function
- | Abort _ -> "Abort"
+ (* 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
+(* | Redo (_, None) -> "Redo"
+ | Redo (_, Some n) -> sprintf "Redo %d" n *)
| Search_pat (_, kind, pat) ->
sprintf "search %s \"%s\"" (pp_search_kind kind) pat
| Search_term (_, kind, term) ->
sprintf "search %s %s" (pp_search_kind kind) (pp_term term)
- | Undo (_, None) -> "Undo"
- | Undo (_, Some n) -> sprintf "Undo %d" n
+(* | Undo (_, None) -> "Undo"
+ | Undo (_, Some n) -> sprintf "Undo %d" n *)
| Print (_, name) -> sprintf "Print \"%s\"" name
| Quit _ -> "Quit"
- | Instance _
- | Match _ -> assert false
let pp_macro_ast = pp_macro pp_term_ast
let pp_macro_cic = pp_macro pp_term_cic
sprintf "alias num (instance %d) = \"%s\"" instance desc
let pp_command = function
- | Qed _ -> "Qed"
+ | Qed _ -> "qed"
| Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value
| Inductive (_, params, types) ->
let pp_params = function
let pp_tactical tac = pp_tactical tac ^ tactical_terminator
let pp_tactic tac = pp_tactic tac ^ tactic_terminator
+let pp_command tac = pp_command tac ^ command_terminator
let pp_executable = function
| Macro (_,x) -> pp_macro_ast x