let tactic_terminator = tactical_terminator
let command_terminator = tactical_terminator
-let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
+let pp_idents idents = "(" ^ String.concat " " idents ^ ")"
let pp_reduction_kind ~term_pp = function
| `Normalize -> "normalize"
let pp_macro ~term_pp =
let term_pp = pp_arg ~term_pp in
+ let style_pp = function
+ | Declarative -> ""
+ | Procedural -> "procedural "
+ in
+ let prefix_pp prefix =
+ if prefix = "" then "" else sprintf " \"%s\"" prefix
+ in
function
(* Whelp *)
| WInstance (_, term) -> "whelp instance " ^ term_pp term
(* real macros *)
| Check (_, term) -> sprintf "check %s" (term_pp term)
| Hint _ -> "hint"
- | Inline (_, suri, "") -> sprintf "inline \"%s\"" suri
- | Inline (_, suri, prefix) -> sprintf "inline \"%s\" \"%s\"" suri prefix
+ | Inline (_, style, suri, prefix) ->
+ sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix)
let pp_associativity = function
| Gramext.LeftA -> "left associative"
let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
function
- | Note (_,str) -> sprintf "(* %s *)" str
+ | Note (_,str) -> sprintf "(* %s *)\n" str
| Code (_,code) ->
- sprintf "(** %s. **)" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
+ sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
let pp_statement ~term_pp ~lazy_term_pp ~obj_pp =
function