X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;ds=sidebyside;f=pa_goal.ml;h=86f67db8aac6fef0bb419a5e3a233dca1a86b7f7;hb=9a049cb107efab5b03dae694d8c7bf9b97655450;hp=06b2ec81e9ffec265585dda466ec89b6e8db92ad;hpb=b71fd4c0029678140d2496ac52f7b79f1ad96fe1;p=goaljobs.git

diff --git a/pa_goal.ml b/pa_goal.ml
index 06b2ec8..86f67db 100644
--- 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,9 +100,27 @@ let generate_let_goal _loc (r : rec_flag) (lets : binding) =
   let lets = rewrite lets in
 
   (* let [rec] ... and ... in () *)
-  Ast.StVal (_loc, r, lets)
-
-(* Rewrite 'require (name args...)' as 'require (goal_name args)'.
+  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 (fun () -> goal_name args)'.
  * 'expr' is a function call.
  *)
 let generate_require _loc expr =
@@ -108,7 +137,7 @@ let generate_require _loc expr =
       locfail _loc "require (...) expression must contain a call to a goal"
   in
   let expr = rewrite expr in
-  <:expr< Goaljobs.require ($expr$) >>
+  <:expr< Goaljobs.require (fun () -> $expr$) >>
 
 ;;