Factor out param_decl and improvements to AST printing.

diff --git a/src/ast.ml b/src/ast.ml
index f1a4137..62af833 100644 (file)
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -47,7 +47,8 @@ and expr =
   | EConstant of loc * constant
 and constant =
   | CString of string
-and goal = id list * pattern list * expr list * code option
+and goal = param_decl list * pattern list * expr list * code option
+and param_decl = id
 and id = string
 and code = substs
 and substs = subst list
@@ -142,29 +143,28 @@ let iter_with_commas
       f fp x
   ) xs
 
-let rec print_env fp env =
-  Env.iter (print_def fp) env
+let rec string_env () env =
+  let env = Env.bindings env in
+  String.concat "" (List.map (string_def ()) env)
 
-and print_def fp name expr =
+and print_env fp env = output_string fp (string_env () env)
+
+and string_def () (name, expr) =
   match expr with
-  | 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"
+  | EGoal (loc, goal) -> string_goal () (Some name, goal) ^ "\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 -> " = { ... }")
+
+and string_param_decl () name = name
 
 and string_pattern () = function
   | PTactic (loc, name, params) ->
@@ -175,12 +175,7 @@ and string_pattern () = function
 and print_pattern fp p = output_string fp (string_pattern () p)
 
 and string_expr () = function
-  | EGoal (loc, (params, patterns, exprs, code)) ->
-     sprintf "goal (%s) = %s : %s%s"
-       (String.concat ", " params)
-       (String.concat ", " (List.map (string_pattern ()) patterns))
-       (String.concat ", " (List.map (string_expr ()) exprs))
-       (match code with None -> "" | Some code -> " = { ... }")
+  | EGoal (loc, goal) -> string_goal () (None, goal)
   | ECall (loc, name, params) ->
      sprintf "%s (%s)"
        name (String.concat ", " (List.map (string_expr ()) params))

diff --git a/src/ast.mli b/src/ast.mli
index c59de00..978099e 100644 (file)
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -60,7 +60,9 @@ and expr =
   | EConstant of loc * constant
 and constant =
   | CString of string
-and goal = id list * pattern list * expr list * code option
+and goal = param_decl list * pattern list * expr list * code option
+  (** Goal parameter is the parameter name and an optional default value. *)
+and param_decl = id
 and id = string
 and code = substs
 and substs = subst list

diff --git a/src/parser.mly b/src/parser.mly
index 5a2ce9b..c47ac59 100644 (file)
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -71,12 +71,14 @@ stmt:
     ;
 
 goal_stmt:
-    | GOAL ID option(param_decl) EQUALS
+    | GOAL ID option(params_decl) EQUALS
     { $2, match $3 with None -> [] | Some ps -> ps }
     ;
-param_decl:
-    | LEFT_PAREN separated_list(COMMA, ID) RIGHT_PAREN { $2 }
+params_decl:
+    | LEFT_PAREN separated_list(COMMA, param_decl) RIGHT_PAREN { $2 }
     ;
+param_decl:
+    | ID         { $1 }
 
 patterns:
     | separated_list(COMMA, pattern) { $1 }