let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
let pp_reduction_kind ~term_pp = function
- | `Demodulate -> "demodulate"
| `Normalize -> "normalize"
| `Reduce -> "reduce"
| `Simpl -> "simplify"
in
let types = List.rev_map to_ident types in
sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names))
+ | Demodulate _ -> "demodulate"
| Discriminate (_, term) -> "discriminate " ^ term_pp term
| Elim (_, term, using, num, idents) ->
sprintf "elim " ^ term_pp term ^
sprintf "intros%s%s"
(match num with None -> "" | Some num -> " " ^ string_of_int num)
(match idents with [] -> "" | idents -> " " ^ pp_idents idents)
- | LApply (_, level_opt, terms, term, ident_opt) ->
- sprintf "lapply %s%s%s%s"
- (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")
+ | LApply (_, linear, level_opt, terms, term, ident_opt) ->
+ sprintf "lapply %s%s%s%s%s"
+ (if linear then " linear " else "")
+ (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")
(term_pp term)
(match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
(match ident_opt with None -> "" | Some ident -> " as " ^ ident)
| Split _ -> "split"
| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ term_pp term
-
-let pp_search_kind = function
+
+ let pp_search_kind = function
| `Locate -> "locate"
| `Hint -> "hint"
| `Match -> "match"
(* real macros *)
| Check (_, term) -> sprintf "Check %s" (term_pp term)
| Hint _ -> "hint"
- | Search_pat (_, kind, pat) ->
- sprintf "search %s \"%s\"" (pp_search_kind kind) pat
- | Search_term (_, kind, term) ->
- sprintf "search %s %s" (pp_search_kind kind) (term_pp term)
- | Print (_, name) -> sprintf "Print \"%s\"" name
- | Quit _ -> "Quit"
let pp_associativity = function
| Gramext.LeftA -> "left associative"
| Include (_,path) -> "include \"" ^ path ^ "\""
| Qed _ -> "qed"
| Drop _ -> "drop"
+ | Print (_,s) -> "print " ^ s
| Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
| Coercion (_, uri, do_composites) -> pp_coercion uri do_composites
| Obj (_,obj) -> obj_pp obj