Add Arthur's lambda example and update makefile for it

generator/.gitignore

+*.cmi
+*.log.js
+*.unlog.js
+*.pre

generator/Makefile

@@ -8,12 +8,15 @@
 
 STD_DIR	    := stdlib_ml
 TEST_DIR    := tests
-TEST_DIR_JS := tests/js
 ML_TESTS    := $(wildcard $(TEST_DIR)/*.ml)
 
-CC          := ocamlc -c
 OCAMLBUILD  := ocamlbuild -j 4 -classic-display -use-ocamlfind
 
+# Used for stdlib and generator dependency generation
+CC          := ocamlc -c
+OCAMLDEP    := ocamldep -one-line
+DEPSED      := sed -e "s/cmo/log.js/; s/cmo/cmi/g; /cmx/ d"
+
 all: main.byte
 
 debug: main.d.byte
@@ -31,14 +34,22 @@ stdlib:
 	$(OCAMLBUILD) $@
 	cp _build/$@ .
 
-tests: main.byte stdlib
-	# TODO: Figure out why dependencies required to be translated first
-	./main.byte -I tests tests/stack.ml
-	./main.byte -I tests tests/calc.ml
-	# Delete the above once figured out.
-	$(foreach mlfile, $(ML_TESTS), ./main.byte -I tests $(mlfile);)
-	mkdir -p $(TEST_DIR_JS) 
-	mv $(TEST_DIR)/*.js $(TEST_DIR_JS)
+.PRECIOUS: tests/%.ml
+tests/%.ml tests/%.ml.d: tests/%.v
+	$(MAKE) -C $(CURDIR)/../../../lib/tlc/src
+	cd $(<D) && coqc -I $(CURDIR)/../../../lib/tlc/src $(<F)
+	cd $(<D) && rm *.mli
+	$(OCAMLDEP) -I $(<D) $(<D)/*.ml | $(DEPSED) > tests/$*.ml.d
+
+tests/%.ml.d: tests/%.ml
+	$(OCAMLDEP) -I $(<D) $< | $(DEPSED) > $@
+
+tests/%.cmi tests/%.log.js tests/%.unlog.js: tests/%.ml main.byte stdlib
+	./main.byte -I $(<D) $<
+
+tests: $(ML_TESTS:.ml=.log.js)
+
+tests/lambda: tests/lambda/Lambda.log.js
 
 clean_stdlib:
 	rm -f $(STD_DIR)/*.cmi
@@ -46,9 +57,9 @@ clean_stdlib:
 clean_tests:
 	rm -f $(TEST_DIR)/*.cmi
 	rm -f $(TEST_DIR)/*.js.pre
-	# Temp rule to remove artifacts during manual/debug creation
 	rm -f $(TEST_DIR)/*.js
-	rm -f $(TEST_DIR_JS)/*.js
+	rm -f $(TEST_DIR)/*.d
+	rm -f $(TEST_DIR)/lambda/*.{ml,mli,glob,vo,d}
 
 clean:
 	rm -rf _build
@@ -56,3 +67,11 @@ clean:
 
 clean_cmi: clean_tests clean_stdlib
 cleanall: clean clean_cmi
+
+ifeq ($(filter clean%,$(MAKECMDGOALS)),)
+-include $(ML_TESTS:.ml=.ml.d)
+endif
+
+ifeq ($(MAKECMDGOALS),tests/lambda)
+-include tests/lambda/Lambda.ml.d
+endif

generator/tests/lambda/.gitignore

+*.ml
+*.mli

generator/tests/lambda/Lambda.v

+(************************************************************
+* Wrapper around the library TLC                            *
+*************************************************************)
+
+Set Implicit Arguments.
+Require Export LibTactics LibCore LibVar LibEnv.
+Generalizable Variables A B.
+
+
+(*==========================================================*)
+(* * Definitions *)
+
+(************************************************************)
+(* ** Syntax *)
+
+(** Grammar of values and terms *)
+
+Inductive val : Type :=
+  | val_int : int -> val
+  | val_clo : var -> trm -> val
+  | val_err : val
+
+with trm : Type :=
+  | trm_val : val -> trm
+  | trm_var : var -> trm
+  | trm_abs : var -> trm -> trm
+  | trm_app : trm -> trm -> trm
+  | trm_try : trm -> trm -> trm
+  | trm_raise : trm -> trm.
+
+Coercion trm_val : val >-> trm.
+
+(** Substitution *)
+
+Fixpoint subst (x:var) (v:val) (t:trm) : trm :=
+  let s := subst x v in
+  match t with
+  | trm_val v => t
+  | trm_var y => If x = y then trm_val v else t
+  | trm_abs y t3 => trm_abs y (If x = y then t3 else s t3)
+  | trm_app t1 t2 => trm_app (s t1) (s t2)  
+  | trm_try t1 t2 => trm_try (s t1) (s t2) 
+  | trm_raise t1 => trm_raise (s t1)
+  end.
+
+
+(************************************************************)
+(* ** Definition shared by the semantics *)
+
+Inductive beh :=
+  | beh_ret : val -> beh
+  | beh_exn : val -> beh
+  | beh_err : beh.
+  
+Coercion beh_ret : val >-> beh.
+
+
+(*==========================================================*)
+(* * Definitions *)
+
+Implicit Types v : val.
+Implicit Types t : trm.
+Implicit Types b : beh.
+
+
+(************************************************************)
+(* ** Results *)
+
+(** Grammar of results of the interpreter *)
+
+Inductive res :=
+  | res_return : beh -> res
+  | res_bottom : res.
+
+Coercion res_return : beh >-> res.
+Implicit Types r : res.
+
+
+(************************************************************)
+(* ** Monadic operators *)
+
+(** Bind-style operators *)
+
+Definition if_success (r:res) (k:val->res) : res :=
+  match r with
+  | res_return (beh_ret v) => k v
+  | _ => r
+  end.
+
+Definition if_fault (r:res) (k:val->res) : res :=
+  match r with
+  | res_return (beh_exn v) => k v
+  | _ => r
+  end.
+
+Definition if_isclo (v:val) (k:var->trm->res) : res :=
+  match v with
+  | val_clo x t => k x t
+  | _ => beh_err
+  end.
+
+
+(************************************************************)
+(* ** Interpreter *)
+
+(** Definition of the interpreter *)
+
+Fixpoint run (n:nat) (t:trm) : res :=
+  match n with 
+  | O => res_bottom
+  | S m => 
+    match t with
+    | trm_val v => v
+    | trm_abs x t1 => val_clo x t1
+    | trm_var x => beh_err
+    | trm_app t1 t2 => 
+       if_success (run m t1) (fun v1 =>
+         if_success (run m t2) (fun v2 =>
+            if_isclo v1 (fun x t3 =>
+              run m (subst x v2 t3))))
+    | trm_try t1 t2 =>
+       if_fault (run m t1) (fun v => run m (trm_app t2 v))
+    | trm_raise t1 => 
+       if_success (run m t1) (fun v1 => beh_exn v1)
+    end
+  end.
+
+Unset Extraction Optimize.
+Unset Extraction KeepSingleton.
+Unset Extraction AutoInline.
+Separate Extraction run.
+