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
let pp_term_cic term = CicPp.ppterm term
in
pp_t t ^ " in " ^ pp_hyp_pattern hyp ^ " \\vdash " ^ pp_term_ast goal
+let pp_intros_specs = function
+ | None, [] -> ""
+ | Some num, [] -> Printf.sprintf " names %i" num
+ | None, idents -> Printf.sprintf " names %s" (pp_idents idents)
+ | Some num, idents -> Printf.sprintf " names %i %s" num (pp_idents idents)
+
let rec pp_tactic = function
| Absurd (_, term) -> "absurd" ^ pp_term_ast term
| Apply (_, term) -> "apply " ^ pp_term_ast term
| Decompose (_, term) ->
sprintf "decompose %s" (pp_term_ast term)
| Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
- | Elim (_, term, using) ->
+ | Elim (_, term, using, num, idents) ->
sprintf "elim " ^ pp_term_ast term ^
(match using with None -> "" | Some term -> " using " ^ pp_term_ast term)
- | ElimType (_, term) -> "elim type " ^ pp_term_ast term
+ ^ pp_intros_specs (num, idents)
+ | ElimType (_, term, using, num, idents) ->
+ sprintf "elim type " ^ pp_term_ast term ^
+ (match using with None -> "" | Some term -> " using " ^ pp_term_ast term)
+ ^ pp_intros_specs (num, idents)
| Exact (_, term) -> "exact " ^ pp_term_ast term
| Exists _ -> "exists"
| Fold (_, kind, term, pattern) ->
| Tactic (_, tac) -> pp_tactic tac
| Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac)
| Repeat (_, tac) -> "repeat " ^ pp_tactical tac
- | Seq (_, tacs) -> pp_tacticals tacs
+ | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs
| Then (_, tac, tacs) ->
- sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs)
- | Tries (_, tacs) -> sprintf "tries [%s]" (pp_tacticals tacs)
+ sprintf "%s; [%s]" (pp_tactical tac) (pp_tacticals ~sep:" | " tacs)
+ | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
| Try (_, tac) -> "try " ^ pp_tactical tac
+ | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
-and pp_tacticals tacs =
- String.concat (tactical_separator ^ " ") (List.map pp_tactical tacs)
+and pp_tacticals ~sep tacs =
+ String.concat sep (List.map pp_tactical tacs)
let pp_tactical tac = pp_tactical tac ^ tactical_terminator
let pp_tactic tac = pp_tactic tac ^ tactic_terminator