let pp_reduction_kind = pp_reduction_kind ~term_pp in
let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in
function
+ (* Higher order tactics *)
+ | Do (_, count, tac) ->
+ sprintf "do %d %s" count (pp_tactic ~term_pp ~lazy_term_pp tac)
+ | Repeat (_, tac) -> "repeat " ^ pp_tactic ~term_pp ~lazy_term_pp tac
+ | Seq (_, tacs) -> pp_tactics ~term_pp ~lazy_term_pp ~sep:"; " tacs
+ | Then (_, tac, tacs) ->
+ sprintf "%s; [%s]" (pp_tactic ~term_pp ~lazy_term_pp tac)
+ (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tacs)
+ | First (_, tacs) ->
+ sprintf "tries [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tacs)
+ | Try (_, tac) -> "try " ^ pp_tactic ~term_pp ~lazy_term_pp tac
+ | Solve (_, tac) ->
+ sprintf "solve [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tac)
+ | Progress (_, tac) -> "progress " ^ pp_tactic ~term_pp ~lazy_term_pp tac
+ (* First order tactics *)
| Absurd (_, term) -> "absurd" ^ term_pp term
| Apply (_, term) -> "apply " ^ term_pp term
| ApplyS (_, term, params) ->
| Generalize (_, pattern, ident) ->
sprintf "generalize %s%s" (pp_tactic_pattern pattern)
(match ident with None -> "" | Some id -> " as " ^ id)
- | Goal (_, n) -> "goal " ^ string_of_int n
| Fail _ -> "fail"
| Fourier _ -> "fourier"
| IdTac _ -> "id"
(List.map (function (id,term) -> "(" ^ id ^ ": " ^ term_pp term ^ ")")
args)
+and pp_tactics ~term_pp ~lazy_term_pp ~sep tacs =
+ String.concat sep (List.map (pp_tactic ~lazy_term_pp ~term_pp) tacs)
+
let pp_search_kind = function
| `Locate -> "locate"
| `Hint -> "hint"
| Print (_,s) -> "print " ^ s
| Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
-let rec pp_tactical ~term_pp ~lazy_term_pp =
- let pp_tactic = pp_tactic ~lazy_term_pp ~term_pp in
- let pp_tacticals = pp_tacticals ~lazy_term_pp ~term_pp in
+let pp_punctuation_tactical ~term_pp ~lazy_term_pp =
function
- | Tactic (_, tac) -> pp_tactic tac
- | Do (_, count, tac) ->
- sprintf "do %d %s" count (pp_tactical ~term_pp ~lazy_term_pp tac)
- | Repeat (_, tac) -> "repeat " ^ pp_tactical ~term_pp ~lazy_term_pp tac
- | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs
- | Then (_, tac, tacs) ->
- sprintf "%s; [%s]" (pp_tactical ~term_pp ~lazy_term_pp tac)
- (pp_tacticals ~sep:" | " tacs)
- | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
- | Try (_, tac) -> "try " ^ pp_tactical ~term_pp ~lazy_term_pp tac
- | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
- | Progress (_, tac) -> "progress " ^ pp_tactical ~term_pp ~lazy_term_pp tac
-
| Dot _ -> "."
| Semicolon _ -> ";"
| Branch _ -> "["
| Pos (_, i) -> sprintf "%s:" (String.concat "," (List.map string_of_int i))
| Wildcard _ -> "*:"
| Merge _ -> "]"
+
+let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp =
+ function
| Focus (_, goals) ->
sprintf "focus %s" (String.concat " " (List.map string_of_int goals))
| Unfocus _ -> "unfocus"
| Skip _ -> "skip"
-and pp_tacticals ~term_pp ~lazy_term_pp ~sep tacs =
- String.concat sep (List.map (pp_tactical~lazy_term_pp ~term_pp) tacs)
-
let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
function
| Macro (_, macro) -> pp_macro ~term_pp macro ^ "."
- | Tactical (_, tac, Some punct) ->
- pp_tactical ~lazy_term_pp ~term_pp tac
- ^ pp_tactical ~lazy_term_pp ~term_pp punct
- | Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac
+ | Tactic (_, Some tac, punct) ->
+ pp_tactic ~lazy_term_pp ~term_pp tac
+ ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+ | Tactic (_, None, punct) ->
+ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+ | NonPunctuationTactical (_, tac, punct) ->
+ pp_non_punctuation_tactical ~lazy_term_pp ~term_pp tac
+ ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
| Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ ".\n"
let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =