Merge remote-tracking branch 'origin/master' into experiments

20 files changed, 22 insertions, 14 deletions

diff --git a/risc-v/Makefile b/risc-v/Makefile
index 8449c7c4..bc46e4c2 100644
--- a/risc-v/Makefile
+++ b/risc-v/Makefile
@@ -1,14 +1,22 @@
-
 SAIL:=../src/sail.native
+LEM:=../../lem/lem
+
 SOURCES:=riscv_types.sail riscv.sail ../etc/regfp.sail riscv_regfp.sail
-all: lem_ast shallow
 
-lem_ast: $(SOURCES) $(SAIL)
-	$(SAIL) -lem_ast $(SOURCES) -o riscv
 
-shallow: $(SOURCES) $(SAIL)
-	$(SAIL) -lem_lib Riscv_extras_embed -lem $(SOURCES) -o riscv
+all: riscv.lem riscv.ml riscv_embed.lem
+
+riscv.lem: $(SOURCES)
+	$(SAIL) -lem_ast -o riscv $(SOURCES)
+
+riscv.ml: riscv.lem ../src/lem_interp/interp_ast.lem
+	$(LEM) -ocaml -lib ../src/lem_interp/ $<
+
+
+riscv_embed.lem: $(SOURCES)
+# also generates riscv_embed_sequential.lem, riscv_embed_types.lem, riscv_toFromInterp.lem
+	$(SAIL) -lem -lem_lib Riscv_extras_embed -o riscv $(SOURCES)
 
 clean:
-	rm -f riscv.lem riscv_embed*.lem riscv_toFromInterp.lem
-	rm -f riscv_type*.lem
+	rm -f riscv.lem riscv.ml
+	rm -f riscv_embed*.lem riscv_toFromInterp.lem
diff --git a/risc-v/hgen/ast.hgen b/risc-v/gen/ast.hgen
index b1968173..b1968173 100644
--- a/risc-v/hgen/ast.hgen
+++ b/risc-v/gen/ast.hgen
diff --git a/risc-v/hgen/fold.hgen b/risc-v/gen/fold.hgen
index 4c51e114..4c51e114 100644
--- a/risc-v/hgen/fold.hgen
+++ b/risc-v/gen/fold.hgen
diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/gen/herdtools_ast_to_shallow_ast.hgen
index 07c1d082..07c1d082 100644
--- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/risc-v/gen/herdtools_ast_to_shallow_ast.hgen
diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/gen/herdtools_types_to_shallow_types.hgen
index e6edd24d..e6edd24d 100644
--- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen
+++ b/risc-v/gen/herdtools_types_to_shallow_types.hgen
diff --git a/risc-v/hgen/lexer.hgen b/risc-v/gen/lexer.hgen
index e42b8a62..e42b8a62 100644
--- a/risc-v/hgen/lexer.hgen
+++ b/risc-v/gen/lexer.hgen
diff --git a/risc-v/hgen/map.hgen b/risc-v/gen/map.hgen
index bab5ced8..bab5ced8 100644
--- a/risc-v/hgen/map.hgen
+++ b/risc-v/gen/map.hgen
diff --git a/risc-v/hgen/parser.hgen b/risc-v/gen/parser.hgen
index 210e38fb..210e38fb 100644
--- a/risc-v/hgen/parser.hgen
+++ b/risc-v/gen/parser.hgen
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/gen/pretty.hgen
index fc1c0000..fc1c0000 100644
--- a/risc-v/hgen/pretty.hgen
+++ b/risc-v/gen/pretty.hgen
diff --git a/risc-v/hgen/pretty_xml.hgen b/risc-v/gen/pretty_xml.hgen
index b0306161..b0306161 100644
--- a/risc-v/hgen/pretty_xml.hgen
+++ b/risc-v/gen/pretty_xml.hgen
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/gen/sail_trans_out.hgen
index 2f9a80f1..2f9a80f1 100644
--- a/risc-v/hgen/sail_trans_out.hgen
+++ b/risc-v/gen/sail_trans_out.hgen
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/gen/shallow_ast_to_herdtools_ast.hgen
index 3025992e..3025992e 100644
--- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/risc-v/gen/shallow_ast_to_herdtools_ast.hgen
diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/gen/shallow_types_to_herdtools_types.hgen
index 6b3b7f51..6b3b7f51 100644
--- a/risc-v/hgen/shallow_types_to_herdtools_types.hgen
+++ b/risc-v/gen/shallow_types_to_herdtools_types.hgen
diff --git a/risc-v/hgen/token_types.hgen b/risc-v/gen/token_types.hgen
index f29e318d..f29e318d 100644
--- a/risc-v/hgen/token_types.hgen
+++ b/risc-v/gen/token_types.hgen
diff --git a/risc-v/hgen/tokens.hgen b/risc-v/gen/tokens.hgen
index f812adbd..f812adbd 100644
--- a/risc-v/hgen/tokens.hgen
+++ b/risc-v/gen/tokens.hgen
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/gen/trans_sail.hgen
index 8b7cbe11..8b7cbe11 100644
--- a/risc-v/hgen/trans_sail.hgen
+++ b/risc-v/gen/trans_sail.hgen
diff --git a/risc-v/hgen/types.hgen b/risc-v/gen/types.hgen
index a0b75606..a0b75606 100644
--- a/risc-v/hgen/types.hgen
+++ b/risc-v/gen/types.hgen
diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/gen/types_sail_trans_out.hgen
index 66a2020c..66a2020c 100644
--- a/risc-v/hgen/types_sail_trans_out.hgen
+++ b/risc-v/gen/types_sail_trans_out.hgen
diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/gen/types_trans_sail.hgen
index 238c7e5b..238c7e5b 100644
--- a/risc-v/hgen/types_trans_sail.hgen
+++ b/risc-v/gen/types_trans_sail.hgen
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem
index 30043779..4ca5f9b7 100644
--- a/risc-v/riscv_extras.lem
+++ b/risc-v/riscv_extras.lem
@@ -31,7 +31,7 @@ let memory_parameter_transformer_option_address _mode v =
   end
 
 
-let read_memory_functions : memory_reads =
+let riscv_read_memory_functions : memory_reads =
   [ ("MEMr",                  (MR Read_plain                  memory_parameter_transformer));
     ("MEMr_acquire",          (MR Read_RISCV_acquire          memory_parameter_transformer));
     ("MEMr_strong_acquire",   (MR Read_RISCV_strong_acquire   memory_parameter_transformer));
@@ -41,10 +41,10 @@ let read_memory_functions : memory_reads =
                               (MR Read_RISCV_reserved_acquire memory_parameter_transformer));
   ]
 
-let memory_writes : memory_writes =
+let riscv_memory_writes : memory_writes =
   []
 
-let memory_eas : memory_write_eas =
+let riscv_memory_eas : memory_write_eas =
   [ ("MEMea",                     (MEA Write_plain                     memory_parameter_transformer));
     ("MEMea_release",             (MEA Write_RISCV_release             memory_parameter_transformer));
     ("MEMea_strong_release",      (MEA Write_RISCV_strong_release      memory_parameter_transformer));
@@ -55,7 +55,7 @@ let memory_eas : memory_write_eas =
                                                                        memory_parameter_transformer));
   ]
 
-let memory_vals : memory_write_vals =
+let riscv_memory_vals : memory_write_vals =
   [ ("MEMval",                    (MV memory_parameter_transformer_option_address Nothing));
     ("MEMval_release",            (MV memory_parameter_transformer_option_address Nothing));
     ("MEMval_strong_release",     (MV memory_parameter_transformer_option_address Nothing));
@@ -66,14 +66,14 @@ let memory_vals : memory_write_vals =
 
   ]
 
-let speculate_conditional_success : excl_res =
+let riscv_speculate_conditional_success : excl_res =
   let f = fun (IState interp context) b ->
     let bool_res = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in
     IState (Interp.add_answer_to_stack interp bool_res) context
   in
   Just ("speculate_conditional_success", (ER (Just f)))
 
-let barrier_functions =
+let riscv_barrier_functions =
   [ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw);
     ("MEM_fence_r_rw",  Barrier_RISCV_r_rw);
     ("MEM_fence_r_r",   Barrier_RISCV_r_r);