- | EGoal (loc, (params, patterns, exprs, code)) ->
- fprintf fp "goal %s (%s) =\n" name (String.concat ", " params);
- fprintf fp " ";
- iter_with_commas fp print_pattern patterns;
- fprintf fp " : ";
- iter_with_commas fp print_expr exprs;
- (match code with
- | None -> ()
- | Some code ->
- fprintf fp " {\n";
- print_code fp code;
- fprintf fp "\n }"
- );
- fprintf fp "\n"
- | expr ->
- fprintf fp "let %s = " name;
- print_expr fp expr;
- fprintf fp "\n"
-
-and print_pattern fp = function
+ | EGoalDefn (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
+ | EFuncDefn (loc, func) -> string_func () (Some name, func) ^ "\n"
+ | ETacticDefn (loc, tactic) -> string_tactic () (Some name, tactic) ^ "\n"
+ | expr -> sprintf "let %s = %a\n" name string_expr expr;
+
+and print_def fp name expr = output_string fp (string_def () (name, expr))
+
+and string_goal () (name, (param_decls, patterns, exprs, code)) =
+ sprintf "goal%s (%s) = %s : %s%s"
+ (match name with None -> "" | Some name -> " " ^ name)
+ (String.concat ", " (List.map (string_param_decl ()) param_decls))
+ (String.concat ", " (List.map (string_pattern ()) patterns))
+ (String.concat ", " (List.map (string_expr ()) exprs))
+ (match code with None -> ""
+ | Some (code, false) -> " = { ... }"
+ | Some (code, true) -> " = @{ ... }")
+
+and string_func () (name, (param_decls, returning, pure, (code, quiet))) =
+ sprintf "%sfunction%s returning %s (%s) = %s{ ... }"
+ (if pure then "pure " else "")
+ (match name with None -> "" | Some name -> " " ^ name)
+ (match returning with RetExpr -> "expression"
+ | RetString -> "string"
+ | RetStrings -> "strings")
+ (String.concat ", " (List.map (string_param_decl ()) param_decls))
+ (if quiet then "@" else "")
+
+and string_tactic () (name, (param_decls, (code, quiet))) =
+ sprintf "tactic%s (%s) = %s{ ... }"
+ (match name with None -> "" | Some name -> " " ^ name)
+ (String.concat ", " (List.map (string_param_decl ()) param_decls))
+ (if quiet then "@" else "")
+
+and string_param_decl () name = name
+
+and string_pattern () = function