From b71fd4c0029678140d2496ac52f7b79f1ad96fe1 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Sun, 15 Sep 2013 21:39:12 +0100 Subject: [PATCH] First published version. --- .depend | 3 + .gitignore | 28 +++++++++ Makefile.am | 29 ++++----- NOTES | 1 - common-rules.mk | 30 +++++++++ configure.ac | 1 + examples/Makefile.am | 2 + examples/compile-c/.depend | 2 + examples/compile-c/Makefile.am | 49 +++++++++++++++ examples/compile-c/README | 11 ++++ examples/compile-c/compile.ml | 30 +++++++++ examples/compile-c/main.c | 14 +++++ examples/compile-c/utils.c | 9 +++ goaljobs.ml | 90 ++++++++++++++++++++++----- goaljobs.mli | 137 ++++++++++++++++++++++++++++++++++------- m4/.gitignore | 5 ++ pa_goal.ml | 130 ++++++++++++++++++++++++++++++++++++++ 17 files changed, 516 insertions(+), 55 deletions(-) create mode 100644 .depend create mode 100644 common-rules.mk create mode 100644 examples/compile-c/.depend create mode 100644 examples/compile-c/Makefile.am create mode 100644 examples/compile-c/README create mode 100644 examples/compile-c/compile.ml create mode 100644 examples/compile-c/main.c create mode 100644 examples/compile-c/utils.c create mode 100644 m4/.gitignore create mode 100644 pa_goal.ml diff --git a/.depend b/.depend new file mode 100644 index 0000000..1c95889 --- /dev/null +++ b/.depend @@ -0,0 +1,3 @@ +goaljobs.cmi : +goaljobs.cmo : goaljobs.cmi +goaljobs.cmx : goaljobs.cmi diff --git a/.gitignore b/.gitignore index b25c15b..5613406 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,29 @@ *~ +*.cmi +*.cmo +*.cmx +*.cma +*.cmxa +*.o +*.a + +Makefile.in +Makefile + +/aclocal.m4 +/autom4te.cache +/compile +/config.guess +/config.h +/config.h.in +/config.log +/config.status +/config.sub +/configure +/examples/compile-c/compile +/examples/compile-c/program +/install-sh +/libtool +/ltmain.sh +/missing +/stamp-h1 diff --git a/Makefile.am b/Makefile.am index 11997d7..b995c23 100644 --- a/Makefile.am +++ b/Makefile.am @@ -15,6 +15,8 @@ # along with this program; if not, write to the Free Software # Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. +include common-rules.mk + ACLOCAL_AMFLAGS = -I m4 EXTRA_DIST = \ @@ -23,35 +25,28 @@ EXTRA_DIST = \ README \ $(sources) -CLEANFILES = *~ - -OCAMLCFLAGS = -g -package unix -OCAMLOPTFLAGS = $(OCAMLCFLAGS) - SUBDIRS = . examples tests sources = \ - test.ml \ goaljobs.ml \ goaljobs.mli -noinst_SCRIPTS = test +noinst_SCRIPTS = goaljobs.cmxa pa_goal.cmo -test: goaljobs.cmx - $(OCAMLFIND) ocamlopt $(OCAMLOPTFLAGS) $< -o $@ +# Library. +goaljobs.cmxa: goaljobs.cmx + $(OCAMLFIND) ocamlopt -a -o $@ $(OCAMLOPTFLAGS) $(OCAMLOPTPACKAGES) $< -# Dependencies. +# Preprocessor for goaljobs scripts. +pa_goal.cmo: pa_goal.ml + $(OCAMLFIND) ocamlc $(OCAMLCFLAGS) -package camlp4.lib -linkpkg \ + -pp $(CAMLP4OF) -c $< -o $@ -%.cmi: %.mli - $(OCAMLFIND) ocamlc $(OCAMLCFLAGS) -c $< -o $@ -%.cmo: %.ml - $(OCAMLFIND) ocamlc $(OCAMLCFLAGS) -c $< -o $@ -%.cmx: %.ml - $(OCAMLFIND) ocamlopt $(OCAMLOPTFLAGS) -c $< -o $@ +# Dependencies. depend: .depend -.depend: $(wildcard $(abs_srcdir)/*.mli) $(wildcard $(abs_srcdir)/*.ml) +.depend: $(sources) rm -f $@ $@-t $(OCAMLFIND) ocamldep -I $(abs_srcdir) $^ | \ $(SED) 's/ *$$//' | \ diff --git a/NOTES b/NOTES index 14afc95..18dccbe 100644 --- a/NOTES +++ b/NOTES @@ -77,4 +77,3 @@ Example program: git describe --tags --abbrev=0 --match='v*' " package in require (website_updated version) - diff --git a/common-rules.mk b/common-rules.mk new file mode 100644 index 0000000..692c906 --- /dev/null +++ b/common-rules.mk @@ -0,0 +1,30 @@ +# goaljobs +# Copyright (C) 2013 Red Hat Inc. +# +# This program is free software; you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program; if not, write to the Free Software +# Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. + +CLEANFILES = *~ *.cmi *.cmo *.cmx *.cma *.cmxa *.o + +OCAMLCFLAGS = -g -warn-error CDEFLMPSUVYZX +OCAMLCPACKAGES = -package unix -I $(top_builddir) +OCAMLOPTFLAGS = $(OCAMLCFLAGS) +OCAMLOPTPACKAGES = $(OCAMLCPACKAGES) + +%.cmi: %.mli + $(OCAMLFIND) ocamlc $(OCAMLCFLAGS) $(OCAMLCPACKAGES) -c $< -o $@ +%.cmo: %.ml + $(OCAMLFIND) ocamlc $(OCAMLCFLAGS) $(OCAMLCPACKAGES) -c $< -o $@ +%.cmx: %.ml + $(OCAMLFIND) ocamlopt $(OCAMLOPTFLAGS) $(OCAMLOPTPACKAGES) -c $< -o $@ diff --git a/configure.ac b/configure.ac index 1f3189b..6ca6f32 100644 --- a/configure.ac +++ b/configure.ac @@ -87,5 +87,6 @@ fi AC_CONFIG_HEADERS([config.h]) AC_CONFIG_FILES([Makefile examples/Makefile + examples/compile-c/Makefile tests/Makefile]) AC_OUTPUT diff --git a/examples/Makefile.am b/examples/Makefile.am index 9445514..457c3a2 100644 --- a/examples/Makefile.am +++ b/examples/Makefile.am @@ -15,3 +15,5 @@ # along with this program; if not, write to the Free Software # Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. +SUBDIRS = \ + compile-c diff --git a/examples/compile-c/.depend b/examples/compile-c/.depend new file mode 100644 index 0000000..a95aa04 --- /dev/null +++ b/examples/compile-c/.depend @@ -0,0 +1,2 @@ +compile.cmo : ../../goaljobs.cmi +compile.cmx : ../../goaljobs.cmx diff --git a/examples/compile-c/Makefile.am b/examples/compile-c/Makefile.am new file mode 100644 index 0000000..51a996a --- /dev/null +++ b/examples/compile-c/Makefile.am @@ -0,0 +1,49 @@ +# goaljobs +# Copyright (C) 2013 Red Hat Inc. +# +# This program is free software; you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program; if not, write to the Free Software +# Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. + +include ../../common-rules.mk + +EXTRA_DIST = main.c utils.c $(sources) + +sources = compile.ml + +noinst_SCRIPTS = compile + +compile: ../../goaljobs.cmxa compile.cmx + $(OCAMLFIND) ocamlopt $(OCAMLOPTFLAGS) \ + $(OCAMLOPTPACKAGES) -linkpkg $^ -o $@ + +compile.cmx: compile.ml ../../pa_goal.cmo + $(OCAMLFIND) ocamlopt $(OCAMLOPTFLAGS) $(OCAMLOPTPACKAGES) \ + -pp "$(CAMLP4O) ../../pa_goal.cmo" -c $< -o $@ + +# Dependencies. + +depend: .depend + +.depend: $(sources) + rm -f $@ $@-t + $(OCAMLFIND) ocamldep -I $(abs_srcdir) -I $(top_builddir) $^ | \ + $(SED) 's/ *$$//' | \ + $(SED) -e :a -e '/ *\\$$/N; s/ *\\\n */ /; ta' | \ + $(SED) -e 's,$(abs_srcdir)/,$(builddir)/,g' | \ + sort > $@-t + mv $@-t $@ + +-include .depend + +SUFFIXES = .cmo .cmi .cmx .ml .mli .mll .mly diff --git a/examples/compile-c/README b/examples/compile-c/README new file mode 100644 index 0000000..94f5a18 --- /dev/null +++ b/examples/compile-c/README @@ -0,0 +1,11 @@ +Very trivial example of compiling a C program. + +It compiled 'main.c' & 'utils.c' into 'program' (these are just +dummy C files which don't do anything interesting). + +To try it out, do: + +./compile + +You can also try deleting intermediate files (eg. rm main.o) +and see which files get rebuilt. diff --git a/examples/compile-c/compile.ml b/examples/compile-c/compile.ml new file mode 100644 index 0000000..6cd2e88 --- /dev/null +++ b/examples/compile-c/compile.ml @@ -0,0 +1,30 @@ +open Goaljobs (* will be implicit *) + +let rec goal all () = + require (built "program" ["main.c"; "utils.c"]) + +(* Goal: build the final program from source files. *) +and built program sources = + target (more_recent [program] sources); + List.iter (fun s -> require (compiled s)) sources; + + let objects = List.map (change_file_extension "o") sources in + sh "cc %s -o %s" (String.concat " " objects) program + +(* Goal: Make sure a C file is compiled (to an object file). *) +and compiled c_file = + let o_file = change_file_extension "o" c_file in + target (more_recent [o_file] [c_file]); + require (file_exists c_file); + sh "cc -c %s -o %s" c_file o_file + +(* XXX IMPLICIT *) +let () = + try goal_all () + with + | Goal_result (Goal_failed msg) -> + prerr_endline ("error: " ^ msg); + exit 1 + | exn -> + prerr_endline (Printexc.to_string exn); + exit 1 diff --git a/examples/compile-c/main.c b/examples/compile-c/main.c new file mode 100644 index 0000000..9b45b5f --- /dev/null +++ b/examples/compile-c/main.c @@ -0,0 +1,14 @@ +/* This is just a dummy C program to test building. */ + +#include +#include + +extern void do_utility (void); + +int +main () +{ + printf ("hello, world\n"); + do_utility (); + exit (0); +} diff --git a/examples/compile-c/utils.c b/examples/compile-c/utils.c new file mode 100644 index 0000000..fcbb298 --- /dev/null +++ b/examples/compile-c/utils.c @@ -0,0 +1,9 @@ +/* This is just a dummy C program to test building. */ + +#include + +void +do_utility (void) +{ + printf ("this is the utils.c function\n"); +} diff --git a/goaljobs.ml b/goaljobs.ml index 45422d2..282c29e 100644 --- a/goaljobs.ml +++ b/goaljobs.ml @@ -26,9 +26,9 @@ let goal_failed msg = raise (Goal_result (Goal_failed msg)) let target v = if v then raise (Goal_result Goal_OK) -let require = function - | Goal_OK -> () - | r -> raise (Goal_result r) +let target_all vs = target (List.fold_left (&&) true vs) +let target_exists vs = target (List.fold_left (||) false vs) +let require () = () let file_exists = Sys.file_exists @@ -43,7 +43,7 @@ let file_newer_than f1 f2 = in let s1 = stat f1 and s2 = stat f2 in match s1 with - | None -> () + | None -> false | Some s1 -> match s2 with | None -> @@ -52,45 +52,105 @@ let file_newer_than f1 f2 = | Some s2 -> s1.st_mtime >= s2.st_mtime +let more_recent objs srcs = + if not (List.for_all file_exists objs) then false + else ( + List.for_all ( + fun obj -> List.for_all (file_newer_than obj) srcs + ) objs + ) + let url_exists url = goal_failed "url_exists not implemented!" let sh fs = let do_sh cmd = - print_endline cmd; - let cmd = "set -e\n\n" ^ cmd in - let r = System.command cmd in + let cmd = "set -e\nset -x\n\n" ^ cmd in + let r = Sys.command cmd in if r <> 0 then ( - let msg = sprintf "sh: external command failed with code %d" r in + let msg = sprintf "external command failed with code %d" r in goal_failed msg ) in ksprintf do_sh fs -(* -val shout : ('a, unit, string) format -> 'a -val shlines : ('a, unit, string) format -> 'a +let do_shlines cmd = + let cmd = "set -e\nset -x\n\n" ^ cmd in + let chan = open_process_in cmd in + let lines = ref [] in + let rec loop () = + let line = input_line chan in + lines := line :: !lines; + loop () + in + (try loop () with End_of_file -> ()); + let r = close_process_in chan in + match r with + | WEXITED 0 -> List.rev !lines + | WEXITED i -> + let msg = sprintf "external command failed with code %d" i in + goal_failed msg + | WSIGNALED i -> + let msg = sprintf "external command was killed by signal %d" i in + goal_failed msg + | WSTOPPED i -> + let msg = sprintf "external command was stopped by signal %d" i in + goal_failed msg +let shlines fs = ksprintf do_shlines fs + +let do_shout cmd = + let lines = do_shlines cmd in + String.concat "\n" lines +let shout fs = ksprintf do_shout fs +(* val shell : string ref *) (* val replace_substring : string -> string -> string -> string -val change_file_extension : string -> string -> string +*) + +let change_file_extension ext filename = + let i = + try String.rindex filename '.' + with Not_found -> String.length filename in + String.sub filename 0 i ^ "." ^ ext + +(* val filter_file_extension : string -> string list -> string *) +(* XXX The Memory is not actually persistent yet. *) +let memory = Hashtbl.create 13 + +let memory_exists = Hashtbl.mem memory +let memory_set = Hashtbl.replace memory +let memory_get k = try Some (Hashtbl.find memory k) with Not_found -> None +let memory_delete = Hashtbl.remove memory + let goal_file_exists filename = if not (file_exists filename) then ( - let msg = sprintf "file_exists: %s: file not found" filename in + let msg = sprintf "file '%s' required but not found" filename in goal_failed msg ) let goal_file_newer_than f1 f2 = if not (file_newer_than f1 f2) then ( - let msg = sprintf "file %s is not newer than %s" f1 f2 in + let msg = sprintf "file %s is required to be newer than %s" f1 f2 in + goal_failed msg + ) +let goal_more_recent objs srcs = + if not (more_recent objs srcs) then ( + let msg = sprintf "object(s) %s are required to be newer than source(s) %s" + (String.concat " " objs) (String.concat " " srcs) in goal_failed msg ) let goal_url_exists url = if not (url_exists url) then ( - let msg = sprintf "url_exists: %s: URL does not exist" url in + let msg = sprintf "url_exists: URL '%s' required but does not exist" url in + goal_failed msg + ) +let goal_memory_exists k = + if not (memory_exists k) then ( + let msg = sprintf "memory_exists: key '%s' required but does not exist" k in goal_failed msg ) diff --git a/goaljobs.mli b/goaljobs.mli index 6839108..752e9b7 100644 --- a/goaljobs.mli +++ b/goaljobs.mli @@ -35,8 +35,7 @@ {v let goal compiled c_file = let o_file = change_file_extension "o" c_file in - target (file_exists o_file); - target (file_newer_than o_file c_file); + target (more_recent [o_file] [c_file]); sh "cc -c %s -o %s" c_file o_file } @@ -46,20 +45,19 @@ before it can link the final program: {v - let goal built program sources = - target (file_exists program); - target (file_newer_than program sources); + let goal built program source = + target (more_recent [program] [source]); - List.iter (fun s -> require (compiled s)) sources; + require (compiled source); - let objects = List.map (change_file_extension "o") sources in - sh "cc %s -o %s" (String.concat " " objects) program + let object = change_file_extension "o" source in + sh "cc %s -o %s" object program } *) val target : bool -> unit - (** [target] {i predicate} defines the target condition that will + (** [target] {i condition} defines the target condition that {b will} be met once the current rule has run. Goaljobs is much more flexible than [make]. In [make] only a @@ -71,8 +69,8 @@ val target : bool -> unit ... let goal compiled () = - target (file_exists "foo.o"); - target (file_newer_than "foo.o" "foo.c"); + target (more_recent ["foo.o"] ["foo.c"]); + requires (file_exists "foo.c"); ... } @@ -80,7 +78,13 @@ val target : bool -> unit can have any number of different targets. Almost every rule should have one or more targets, which should - accurately state the outcome once the rule has been run + accurately state the outcome once the rule has been run. + + If you have more than one [target]s then it's as if they have + been ORed together ({b not} ANDed which you might expect). + You can make this explicit by using a single target and [&&] + or [||] between the expressions. See also {!target_all} + and {!target_exists}. Normally you put the target(s) early on in the rule, before any running code and before any [require]s. This is not a @@ -88,6 +92,14 @@ val target : bool -> unit ensure the rule runs most efficiently since if the target is met already then the rest of the rule doesn't run. *) +val target_all : bool list -> unit + (** [target_all [t1; t2; ...]] is the same as writing + [target (t1 && t2 && ...)] *) + +val target_exists : bool list -> unit + (** [target_exists [t1; t2; ...]] is the same as writing + [target (t1 || t2 || ...)] *) + val require : unit -> unit (** [require] {!goal} defines the requirements of this rule, that is, other goals that have to be met before this rule is able to run. @@ -96,7 +108,7 @@ val require : unit -> unit right hand side after the [:], but in goaljobs the requirements can be much richer than simply "that file must exist". - Some simple rules don't need any [require]s. Unlike with [make], + Some very simple rules don't need any [require]s. Unlike with [make], the requirements of a rule can be placed anywhere within the rule, as long as you put them before they are needed. *) @@ -117,6 +129,27 @@ val file_newer_than : string -> string -> bool newer than [file_b]. Note that if [file_a] does not exist, it returns false. If [file_b] does not exist, it is an error. *) +val more_recent : string list -> string list -> bool + (** [more_recent objects sources] expresses the [make] relationship: + + {v object(s) ...: source(s) ...} + + in a convenient way: + + {v + let goal built objects sources = + target (more_recent objects sources); + ... code to rebuild ... + } + + It is roughly equivalent to checking that all the object files + exist and are newer than all of the source files. + + Note that both parameters are lists (since in [make] you can + have a list of source files and a list of object files). If you + don't want a list, pass a single-element list containing the + single the object/source file. *) + val url_exists : string -> bool (** The URL is tested to see if it exists. @@ -165,19 +198,22 @@ val url_exists : string -> bool {v cd $HOME/data/ } *) -val sh : ('a, unit, string, unit) format4 -> 'a -> unit +val sh : ('a, unit, string, unit) format4 -> 'a (** Run the command(s). *) -(* -val shout : ('a, unit, string) format -> 'a - (** Run the command(s). Anything printed on stdout is returned - as a single string (the trailing [\n] character, if any, - is not returned). *) +val shout : ('a, unit, string, string) format4 -> 'a + (** Run the command(s). + + Anything printed on stdout is returned as a string. + The trailing [\n] character, if any, is not returned. *) -val shlines : ('a, unit, string) format -> 'a - (** Run the command(s). Any lines printed to stdout are returned - as a list of strings. Trailing [\n] characters not returned. *) +val shlines : ('a, unit, string, string list) format4 -> 'a + (** Run the command(s). + Any lines printed to stdout is returned as a list of strings. + Trailing [\n] characters are not returned. *) + +(* val shell : string ref (** Set this variable to override the default shell ([/bin/sh]). *) *) @@ -188,9 +224,11 @@ val shell : string ref library (see the module [String]). For convenience some extra functions are provided here. *) +(* val replace_substring : string -> string -> string -> string (** [replace_substring patt repl string] replaces all occurrences of [patt] with [repl] in [string]. *) +*) val change_file_extension : string -> string -> string (** [change_file_extension ext filename] changes the file extension @@ -199,11 +237,60 @@ val change_file_extension : string -> string -> string If the original filename has no extension, this function adds the extension. *) +(* val filter_file_extension : string -> string list -> string (** [filter_file_extension ext filenames] returns only those filenames in the list which have the given file extension. For example [filter_file_extension "o" ["foo.c"; "bar.o"]] would return [["bar.o"]] (a single element list). *) +*) + +(** {2 Memory (persistent key/value storage) + + "The Memory" is key/value storage which persists across goaljobs + sessions. It is stored in the file [$HOME/.goaljobs-memory] + (which is a binary file, but you can delete it if you want). + + The Memory is locked during accesses, so it is safe to read + or write it from multiple parallel goaljobs sessions. + + Keys and values are strings. The keys should be globally + unique, so it is suggested you use some application-specific + prefix. eg: "myapp-key" + + A common pattern is: + + {v + let goal tested version = + let key = "myapp-tested-" ^ version in + target (memory_exists key); + + ... some work to test version ... + + memory_set key "1" + } + + Note in that example the value ["1"] is arbitrary. You just + want to store {i any} value so that a later call to {!memory_exists} + will succeed. +*) + +val memory_exists : string -> bool + (** [memory_exists key] checks that the named [key] exists in + the Memory. It doesn't matter what value it has. + + This is also available as a goal, so you can write + [requires (memory_exists key)] *) + +val memory_set : string -> string -> unit + (** Set [key] to [value] in the Memory. *) + +val memory_get : string -> string option + (** Return the current value of [key] in the Memory. Returns [None] + if the key has never been set or was deleted. *) + +val memory_delete : string -> unit + (** Delete the [key]. If the key doesn't exist, has no effect. *) (**/**) @@ -215,4 +302,10 @@ val filter_file_extension : string -> string list -> string *) val goal_file_exists : string -> unit val goal_file_newer_than : string -> string -> unit +val goal_more_recent : string list -> string list -> unit val goal_url_exists : string -> unit +val goal_memory_exists : string -> unit + +(* Export this so the macros can catch these exceptions. *) +type goal_result_t = Goal_OK | Goal_failed of string +exception Goal_result of goal_result_t diff --git a/m4/.gitignore b/m4/.gitignore new file mode 100644 index 0000000..94e6f26 --- /dev/null +++ b/m4/.gitignore @@ -0,0 +1,5 @@ +/libtool.m4 +/ltoptions.m4 +/ltsugar.m4 +/ltversion.m4 +/lt~obsolete.m4 diff --git a/pa_goal.ml b/pa_goal.ml new file mode 100644 index 0000000..06b2ec8 --- /dev/null +++ b/pa_goal.ml @@ -0,0 +1,130 @@ +(* goaljobs + * Copyright (C) 2013 Red Hat Inc. + * + * This program is free software; you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation; either version 2 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License along + * with this program; if not, write to the Free Software Foundation, Inc., + * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. + *) + +(* For general information about camlp4, see: + * http://brion.inria.fr/gallium/index.php/Camlp4 + * + * For information about quotations, see: + * http://brion.inria.fr/gallium/index.php/Quotation + *) + +open Printf + +open Camlp4.PreCast +open Syntax +open Ast + +let locfail _loc msg = Loc.raise _loc (Failure msg) + +(* 'expr' is a function expression (RHS of a binding). It has the + * form 'fun a -> fun b -> ...'. Return the parameters and the body of + * the function. + *) +let rec function_parameters = function + (* fun patt -> expr *) + | ExFun (_loc, McArr (_ploc, param, ExNil _, expr)) -> + let params, body = function_parameters expr in + ((_ploc, param) :: params), body + (* patt when expr -> expr *) + | ExFun (_loc, McArr (_, _, _, expr)) -> + locfail _loc "not supported: goal function uses when-clause" + | body -> [], body + +(* Define one or more 'let [rec] goal ... [and ...]' expressions. + * + * 'r' is Some _ if the rec keyword was defined. 'lets' is the list + * of let statements. + *) +let generate_let_goal _loc (r : rec_flag) (lets : binding) = + (* lets might be a single binding, or multiple bindings using BiAnd + * ('let .. and'). Rewrite each individual goal in the list. + *) + let rec rewrite = function + | BiNil _loc -> BiNil _loc + + (* let goal left = ... and right = ... *) + | BiAnd (_loc, left, right) -> + BiAnd (_loc, rewrite left, rewrite right) + + (* let goal name = expr *) + | BiEq (_loc, PaId (_, (IdLid (_, name))), expr) -> + (* Rename the function to goal_. *) + let gname = "goal_" ^ name in + + (* Split the function into parameters and body. *) + let params, body = function_parameters expr in + + if params = [] then + locfail _loc "goal must have some parameters; you probably want to put '()' here"; + + (* Put a try-clause around the body. *) + let body = <:expr< try $body$ with Goal_result Goal_OK -> () >> in + + (* Recreate the function with parameters. *) + let expr = + List.fold_right ( + fun (_ploc, param) rest -> + ExFun (_loc, McArr (_ploc, param, ExNil _ploc, rest)) + ) params body in + + <:binding< $lid:gname$ = $expr$ >> + | _ -> + locfail _loc "cannot parse 'let goal' expression" + in + let lets = rewrite lets in + + (* let [rec] ... and ... in () *) + Ast.StVal (_loc, r, lets) + +(* Rewrite 'require (name args...)' as 'require (goal_name args)'. + * 'expr' is a function call. + *) +let generate_require _loc expr = + (* Note that 'f a b c' is parsed as '((f a) b) c' so the actually + * function name is buried deeply in the tree. Rewrite the name. + *) + let rec rewrite = function + | ExApp (_loc, ExId (_loc1, IdLid (_loc2, name)), right) -> + let gname = "goal_" ^ name in + ExApp (_loc, ExId (_loc1, IdLid (_loc2, gname)), right) + | ExApp (_loc, (ExApp _ as expr), right) -> + ExApp (_loc, rewrite expr, right) + | _ -> + locfail _loc "require (...) expression must contain a call to a goal" + in + let expr = rewrite expr in + <:expr< Goaljobs.require ($expr$) >> + +;; + +EXTEND Gram + GLOBAL: expr str_item; + + (* Rewrite 'require (name args...)'. *) + expr: LEVEL "apply" [ + [ "require"; e = expr -> + generate_require _loc e ] + ]; + + (* "str_item" is a top level statement in an OCaml program. *) + str_item: LEVEL "top" [ + [ "let"; r = opt_rec; "goal"; ls = binding -> + generate_let_goal _loc r ls ] + ]; + +END -- 1.8.3.1