- | Left -> "left"
- | LetIn (term, ident) -> sprintf "let %s in %s" (pp_term term) ident
- | Reduce (_, _, _) -> assert false (* TODO *)
- | Reflexivity -> "reflexivity"
- | Replace (t1, t2) -> sprintf "replace %s with %s" (pp_term t1) (pp_term t2)
- | Replace_pattern (_, _) -> assert false (* TODO *)
- | Rewrite (_, _, _) -> assert false (* TODO *)
- | Right -> "right"
- | Ring -> "ring"
- | Split -> "split"
- | Symmetry -> "symmetry"
- | Transitivity term -> "transitivity " ^ pp_term term
+ | Left _ -> "left"
+ | LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident
+ | Reduce (_, kind, None)
+ | Reduce (_, kind, Some ([], `Goal)) -> pp_reduction_kind kind
+ | Reduce (_, kind, Some ([], `Everywhere)) ->
+ sprintf "%s in hyp" (pp_reduction_kind kind)
+ | Reduce (_, kind, Some (terms, `Goal)) ->
+ sprintf "%s %s" (pp_reduction_kind kind)
+ (String.concat ", " (List.map pp_term_ast terms))
+ | Reduce (_, kind, Some (terms, `Everywhere)) ->
+ sprintf "%s in hyp %s" (pp_reduction_kind kind)
+ (String.concat ", " (List.map pp_term_ast terms))
+ | Reflexivity _ -> "reflexivity"
+ | Replace (_, t1, t2) ->
+ sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2)
+ | Replace_pattern (_, _, _) -> assert false (* TODO *)
+ | Rewrite (_, pos, t, None) ->
+ sprintf "rewrite %s %s"
+ (if pos = `Left then "left" else "right") (pp_term_ast t)
+ | Rewrite _ -> assert false (* TODO *)
+ | Right _ -> "right"
+ | Ring _ -> "ring"
+ | Split _ -> "split"
+ | Symmetry _ -> "symmetry"
+ | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term