Command line parsing, the concept of publishing goals.

[goaljobs.git] / pa_goal.ml

diff --git a/pa_goal.ml b/pa_goal.ml
index 06b2ec8..723df1b 100644 (file)
--- a/pa_goal.ml
+++ b/pa_goal.ml
@@ -51,6 +51,8 @@ let rec function_parameters = function
  * of let statements.
  *)
 let generate_let_goal _loc (r : rec_flag) (lets : binding) =
+  let autopublish = ref [] in
+
   (* lets might be a single binding, or multiple bindings using BiAnd
    * ('let .. and').  Rewrite each individual goal in the list.
    *)
@@ -72,6 +74,15 @@ let generate_let_goal _loc (r : rec_flag) (lets : binding) =
       if params = [] then
         locfail _loc "goal must have some parameters; you probably want to put '()' here";
 
+      (* Is it a "zero-parameters" automatically published goal?  What
+       * this really means is it has exactly one unit parameter.
+       *)
+      (match params with
+      | [ _, PaId (_, IdUid (_, "()")) ] ->
+        autopublish := name :: !autopublish
+      | _ -> ()
+      );
+
       (* Put a try-clause around the body. *)
       let body = <:expr< try $body$ with Goal_result Goal_OK -> () >> in
 
@@ -89,7 +100,25 @@ let generate_let_goal _loc (r : rec_flag) (lets : binding) =
   let lets = rewrite lets in
 
   (* let [rec] ... and ... in () *)
-  Ast.StVal (_loc, r, lets)
+  let stmts = Ast.StVal (_loc, r, lets) in
+
+  (* Auto-published goals. *)
+  List.fold_left (
+    fun stmt name ->
+      let publish_name =
+        let gname = "goal_" ^ name in
+        <:str_item<
+          let () = publish $str:name$ (
+            function
+            | [] ->
+              Goaljobs.require ($lid:gname$ ())
+            | _ ->
+              failwith (Printf.sprintf "goal '%s' does not take any arguments"
+                          $str:name$);
+          )
+        >> in
+      StSem (_loc, stmt, publish_name)
+  ) stmts !autopublish
 
 (* Rewrite 'require (name args...)' as 'require (goal_name args)'.
  * 'expr' is a function call.