let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
+let pp_terms_ast terms = String.concat ", " (List.map pp_term_ast terms)
+
let pp_reduction_kind = function
| `Reduce -> "reduce"
| `Simpl -> "simplify"
| Exists _ -> "exists"
| Fold (_, kind, pattern) ->
sprintf "fold %s %s" (pp_reduction_kind kind) (pp_pattern pattern)
+ | FwdSimpl (_, hyp, idents) ->
+ sprintf "fwd %s%s" hyp
+ (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
| Generalize (_, pattern, ident) ->
sprintf "generalize %s%s" (pp_pattern pattern)
(match ident with None -> "" | Some id -> " as " ^ id)
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 ^ " ")
+ (pp_term_ast term)
+ (match terms with [] -> "" | _ -> " to " ^ pp_terms_ast terms)
+ (match ident_opt with None -> "" | Some ident -> " using " ^ ident)
| Left _ -> "left"
| LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident
| Reduce (_, kind, pat) ->
| Split _ -> "split"
| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ pp_term_ast term
- | FwdSimpl (_, term) -> sprintf "fwd %s" (pp_term_ast term)
- | LApply (_, term_opt, term, ident) ->
- sprintf "lapply %s%s%s" (pp_term_ast term)
- (match term_opt with None -> "" | Some t -> " to " ^ pp_term_ast t)
- (match ident with None -> "" | Some id -> " using " ^ id)
let pp_flavour = function
| `Definition -> "Definition"