Use ocamlbuild, no findlib required

4 files changed, 60 insertions, 14 deletions

diff --git a/src/Makefile b/src/Makefile
index ea1a47ae..59f9165c 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -1,21 +1,15 @@
-.PHONY: all doc doc-pdf doc-dot clean
+.PHONY: all test clean
 
-all:
-	ocamlbuild main.native
-	$(MAKE) -C lem_interp
+all: main.native test
 
-doc:
-	mkdir -p html-doc
-	ocamldoc -I _build/ *.mli ulib/*.mli -sort -html -d html-doc
+.PHONY: main.native
+main.native:
+	ocamlbuild main.native
 
-doc-pdf:
-	mkdir -p tex-doc
-	ocamldoc -I _build/ *.mli -latex -sort -d tex-doc -o tex-doc/lem-doc.tex; true
-	cd tex-doc; pdflatex lem-doc.tex
+TESTS=test/test1.native
 
-doc-dot:
-	ocamldoc -I _build/ *.ml *.mli ulib/*.ml -dot -sort -d tex-doc -dot-reduce -o dep.dot; true
-	dot -Tpdf -o dep.pdf dep.dot
+test:
+	ocamlbuild $(TESTS)
 
 clean:
 	-ocamlbuild -clean
diff --git a/src/_tags b/src/_tags
index 05e3b193..9fac32a1 100644
--- a/src/_tags
+++ b/src/_tags
@@ -1,3 +1,7 @@
 true: -traverse, debug
 <**/*.ml>: bin_annot, annot
+<lem_interp>: include
+# see http://caml.inria.fr/mantis/view.php?id=4943
+<lem_interp/*> and not <lem_interp/*.cmxa>: use_lem, use_nums
+<test/*> and not <test/*.cmxa>: use_lem, use_nums
 
diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml
new file mode 100644
index 00000000..3974e939
--- /dev/null
+++ b/src/myocamlbuild.ml
@@ -0,0 +1,35 @@
+open Ocamlbuild_plugin ;;
+open Command ;;
+open Pathname ;;
+open Outcome ;;
+
+(* paths relative to _build *)
+let lem_dir = "../../../lem" ;;
+let lem_libdir = lem_dir / "ocaml-lib/_build" ;;
+let lem_lib = lem_libdir / "extract" ;;
+let lem = lem_dir / "lem" ;;
+let interp_ast = "lem_interp/interp_ast.lem" ;;
+
+dispatch begin function
+| After_rules ->
+    (* ocaml_lib "lem_interp/interp"; *)
+    ocaml_lib ~extern:true ~dir:lem_libdir  ~tag_name:"use_lem" lem_lib;
+
+    rule "lem -> ml"
+    ~prod: "%.ml"
+    ~deps: ["%.lem"; interp_ast]
+    (fun env builder -> Seq [
+      Cmd (S [ P lem; A "-i"; P interp_ast; A "-ocaml"; P (env "%.lem") ]);
+      mv (basename (env "%.ml")) (dirname (env "%.ml"))
+      ]);
+
+    rule "sail -> lem"
+    ~prod: "%.lem"
+    ~deps: ["%.sail"; "main.native"]
+    (fun env builder -> Seq [
+      Cmd (S [ P "./main.native"; A "-lem_ast"; P (env "%.sail") ]);
+      mv (basename (env "%.lem")) (dirname (env "%.lem"))
+      ]);
+
+| _ -> ()
+end ;;
diff --git a/src/test/test1.sail b/src/test/test1.sail
new file mode 100644
index 00000000..29f479d6
--- /dev/null
+++ b/src/test/test1.sail
@@ -0,0 +1,13 @@
+default Nat i
+default Order o
+default bool b
+default forall a. (list a) b
+val forall a, b . ((a * b) -> b pure) snd
+val forall Type i, b. ((i * b) -> i pure) fst
+typedef int_list [name = "il"] = list nat
+typedef reco = const struct forall i, a, b. { (a[i]) v; b w; }
+typedef maybe = const union forall a. { unit None; a Some; }
+typedef colors = enumerate { red; green; blue }
+typedef creg = register bits [5:i] { 5 : h ; 6..7 : j}
+let bool e = true
+let unit x = main ()