Add an option to control the translation to error monad or state-error

monad

3 files changed, 26 insertions, 14 deletions

diff --git a/Makefile b/Makefile
index cdae532d..53382164 100644
--- a/Makefile
+++ b/Makefile
@@ -1,10 +1,10 @@
 all: build-test
 
-CHARON_HOME=../charon
-CHARON_EXEC=$(CHARON_HOME)/charon
-CHARON_TESTS_DIR=$(CHARON_HOME)/tests/cfim
-CHARON_OPTIONS= --dest ../tests/cfim --no-code-duplication
-DEST_DIR=tests
+CHARON_HOME = ../charon
+CHARON_EXEC = $(CHARON_HOME)/charon
+CHARON_TESTS_DIR = $(CHARON_HOME)/tests/cfim
+CHARON_OPTIONS = --dest ../tests/cfim --no-code-duplication
+DEST_DIR = tests
 
 # The user can specify additional translation options for Aeneas:
 OPTIONS ?=
@@ -12,8 +12,8 @@ OPTIONS ?=
 # Default translation options:
 # - insert calls to the normalizer in the translated code to test the
 #   generated unit functions
-TRANS_OPTIONS:=-test-trans-units $(OPTIONS)
-SUBDIR:=
+TRANS_OPTIONS := -test-trans-units $(OPTIONS)
+SUBDIR :=
 
 # Build the project and test it
 .PHONY: build-test
@@ -29,9 +29,10 @@ build:
 test: build translate-no_nested_borrows translate-hashmap translate-paper
 
 # Add specific options to some tests
-translate-no_nested_borrows translate-paper: TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split -no-decreases-clauses
+translate-no_nested_borrows translate-paper: \
+	TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split-files -no-decreases-clauses
 translate-no_nested_borrows translate-paper: SUBDIR:=misc
-translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses
+translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses -no-state
 translate-hashmap: SUBDIR:=hashmap
 
 # Generic rule to extract the CFIM from a rust file
diff --git a/src/Translate.ml b/src/Translate.ml
index ab9ed216..ac2ee38c 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -29,8 +29,14 @@ type config = {
           let _ = assert_norm (FUNCTION () = Success ())
           ```
        *)
+  use_state_monad : bool;
+      (** If `true`, use a state-error monad.
+          If `false`, only use an error monad.
+          
+          Using a state-error monad is necessary when modelling I/O, for instance.
+       *)
   extract_decreases_clauses : bool;
-      (** If true, insert `decreases` clauses for all the recursive definitions.
+      (** If `true`, insert `decreases` clauses for all the recursive definitions.
 
           The body of such clauses must be defined by the user.
        *)
diff --git a/src/main.ml b/src/main.ml
index 4a111a25..df2d1b0c 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -31,8 +31,9 @@ let () =
   let test_units = ref false in
   let test_trans_units = ref false in
   let no_decreases_clauses = ref false in
+  let no_state = ref false in
   let template_decreases_clauses = ref false in
-  let no_split = ref false in
+  let no_split_files = ref false in
   let no_check_inv = ref false in
 
   let spec =
@@ -68,13 +69,16 @@ let () =
       ( "-no-decreases-clauses",
         Arg.Set no_decreases_clauses,
         " Do not add decrease clauses to the recursive definitions" );
+      ( "-no-state",
+        Arg.Set no_state,
+        " Do not use state-error monads, simply use error monads" );
       ( "-template-clauses",
         Arg.Set template_decreases_clauses,
         " Generate templates for the required decreases clauses, in a\n\
         \                         dedicated file. Incompatible with \
          -no-decreases-clauses" );
-      ( "-no-split",
-        Arg.Set no_split,
+      ( "-no-split-files",
+        Arg.Set no_split_files,
         " Don't split the definitions between different files for types,\n\
         \                         functions, etc." );
       ( "-no-check-inv",
@@ -179,8 +183,9 @@ let () =
         {
           Translate.eval_config;
           mp_config = micro_passes_config;
-          split_files = not !no_split;
+          split_files = not !no_split_files;
           test_unit_functions;
+          use_state_monad = not !no_state;
           extract_decreases_clauses = not !no_decreases_clauses;
           extract_template_decreases_clauses = !template_decreases_clauses;
         }