let opt_string_pp = function
| None -> ""
| Some what -> what ^ " "
+
+let pp_auto_params ~term_pp (univ, params) =
+ String.concat " "
+ (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) ^
+ if univ <> [] then
+ (if params <> [] then " " else "") ^ "by " ^
+ String.concat " " (List.map term_pp univ)
+ else ""
+;;
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
let pp_terms = pp_terms ~term_pp in
| Absurd (_, term) -> "absurd" ^ term_pp term
| Apply (_, term) -> "apply " ^ term_pp term
| ApplyS (_, term, params) ->
- "applyS " ^ term_pp term ^
- String.concat " "
- (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
- | AutoBatch (_,params) -> "auto batch " ^
- String.concat " "
- (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
+ "applyS " ^ term_pp term ^ pp_auto_params ~term_pp params
+ | AutoBatch (_,params) -> "autobatch " ^
+ pp_auto_params ~term_pp params
| Assumption _ -> "assumption"
| Cases (_, term, specs) -> Printf.sprintf "cases " ^ term_pp term ^
pp_intros_specs "names " specs
| Decompose (_, names) ->
Printf.sprintf "decompose%s"
(pp_intros_specs "names " (None, names))
- | Demodulate _ -> "demodulate"
+ | Demodulate (_, params) -> "demodulate " ^ pp_auto_params ~term_pp params
| Destruct (_, None) -> "destruct"
| Destruct (_, Some terms) -> "destruct " ^ pp_terms terms
| Elim (_, what, using, pattern, specs) ->
| Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term
| ExistsElim (_, term0, ident, term, ident1, term1) -> "by " ^ (match term0 with None -> "_" | Some term -> term_pp term) ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_term_pp term1 ^ "(" ^ ident1 ^ ")"
| AndElim (_, term, ident1, term1, ident2, term2) -> "by " ^ term_pp term ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")"
- | RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some (None,term) -> "conclude " ^ term_pp term | Some (Some name,term) -> "obtain (" ^ name ^ ") " ^ term_pp term) ^ "=" ^ term_pp term1 ^ " by " ^ (match term2 with `Auto params -> "_" ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | `Term term2 -> term_pp term2 | `Proof -> "proof") ^ (if cont then " done" else "")
+ | RewritingStep (_, term, term1, term2, cont) ->
+ (match term with
+ | None -> " "
+ | Some (None,term) -> "conclude " ^ term_pp term
+ | Some (Some name,term) ->
+ "obtain (" ^ name ^ ") " ^ term_pp term)
+ ^ "=" ^
+ term_pp term1 ^
+ (match term2 with
+ | `Auto params -> pp_auto_params ~term_pp params
+ | `Term term2 -> " exact " ^ term_pp term2
+ | `Proof -> " proof"
+ | `SolveWith term -> " using " ^ term_pp term)
+ ^ (if cont then " done" else "")
| Case (_, id, args) ->
"case" ^ id ^
String.concat " "
| Check (_, term) -> Printf.sprintf "check %s" (term_pp term)
| Hint (_, true) -> "hint rewrite"
| Hint (_, false) -> "hint"
- | AutoInteractive (_,params) -> "auto " ^
- String.concat " "
- (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
+ | AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params
| Inline (_, style, suri, prefix) ->
Printf.sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix)