- 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)'.