From: Richard W.M. Jones <rjones@redhat.com>
Date: Mon, 23 Dec 2019 20:44:01 +0000 (+0000)
Subject: Begin converting Ast print functions so they can be used with format %a.
X-Git-Tag: v'0.2'~137
X-Git-Url: http://git.annexia.org/?a=commitdiff_plain;h=70be8e48106b13883da29574e7735ca85d8192cc;p=goals.git

Begin converting Ast print functions so they can be used with format %a.
---

diff --git a/src/ast.ml b/src/ast.ml
index 885eefe..819e9ee 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -108,12 +108,13 @@ and print_def fp name expr =
      print_expr fp expr;
      fprintf fp "\n"
 
-and print_pattern fp = function
+and string_pattern () = function
   | PTactic (loc, name, params) ->
-     fprintf fp "*%s (" name;
-     iter_with_commas fp print_substs params;
-     fprintf fp ")"
-  | PVar (loc, id) -> print_id fp id
+     sprintf "*%s (%s)" name (String.concat ", "
+                                (List.map (string_substs ()) params));
+  | PVar (loc, id) -> id
+
+and print_pattern fp p = output_string fp (string_pattern () p)
 
 and print_expr fp = function
   | EGoal _ -> assert false (* printed above *)
@@ -138,14 +139,16 @@ and print_constant fp = function
 
 and print_id = output_string
 
-and print_substs fp xs =
-  let xs =
+and string_substs () ss =
+  let ss =
     List.map (
       function
       | SString s -> sprintf "%S" s
       | SVar id -> id
-    ) xs in
-  fprintf fp "%s" (String.concat "+" xs)
+    ) ss in
+  (String.concat "+" ss)
+
+and print_substs fp ss = output_string fp (string_substs () ss)
 
 and print_code fp xs =
   List.iter (
diff --git a/src/ast.mli b/src/ast.mli
index c7e3be4..3a42ec4 100644
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -80,3 +80,5 @@ module Substs : sig
 end
 
 val print_env : out_channel -> env -> unit
+
+val string_pattern : unit -> pattern -> string