let pp_macro ~term_pp ~lazy_term_pp =
let term_pp = pp_arg ~term_pp in
- let style_pp = function
- | Declarative -> ""
- | Procedural None -> "procedural "
- | Procedural (Some i) -> Printf.sprintf "procedural %u " i
- in
- let prefix_pp prefix =
- if prefix = "" then "" else Printf.sprintf " \"%s\"" prefix
- in
let flavour_pp = function
- | None -> ""
- | Some `Definition -> " as definition"
- | Some `MutualDefinition -> " as mutual"
- | Some `Fact -> " as fact"
- | Some `Lemma -> " as lemma"
- | Some `Remark -> " as remark"
- | Some `Theorem -> " as theorem"
- | Some `Variant -> " as variant"
- | Some `Axiom -> " as axiom"
+ | `Definition -> "definition"
+ | `Fact -> "fact"
+ | `Lemma -> "lemma"
+ | `Remark -> "remark"
+ | `Theorem -> "theorem"
+ | `Variant -> "variant"
+ | `Axiom -> "axiom"
+ | `MutualDefinition -> assert false
+ in
+ let pp_inline_params l =
+ let pp_param = function
+ | IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\""
+ | IPAs flavour -> flavour_pp flavour
+ | IPProcedural -> "procedural"
+ | IPDepth depth -> "depth = " ^ string_of_int depth
+ | IPNoDefaults -> "nodefaults"
+ in
+ let s = String.concat " " (List.map pp_param l) in
+ if s = "" then s else " " ^ s
in
let pp_reduction_kind = pp_reduction_kind ~term_pp:lazy_term_pp in
function
| Hint (_, true) -> "hint rewrite"
| Hint (_, false) -> "hint"
| AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params
- | Inline (_, style, suri, prefix, flavour) ->
- Printf.sprintf "inline %s\"%s\"%s%s" (style_pp style) suri (prefix_pp prefix) (flavour_pp flavour)
+ | Inline (_, suri, params) ->
+ Printf.sprintf "inline \"%s\"%s" suri (pp_inline_params params)
let pp_associativity = function
| Gramext.LeftA -> "left associative"