From c61b32393508479657b51b777a0b4816815a55a5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 31 Aug 2023 19:10:00 +0200
Subject: Make progress on Extract and ExtractBase

---
 compiler/Config.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index bd80769f..ccbb4c75 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -323,3 +323,11 @@ let wrap_opaque_in_sig = ref false
     information), we use short names (i.e., the original field names).
  *)
 let record_fields_short_names = ref false
+
+(** Parameterize the traits with their associated types, so as not to use
+    types as first class objects.
+
+    This is useful for some backends with limited expressiveness like HOL4,
+    and to account for type constraints (like [fn f<T : Foo>(...) where T::bar = usize]).
+ *)
+let parameterize_trait_types = ref false
-- 
cgit v1.2.3


From d556b2439ad858fbbf612f433d25363a8f4a7c83 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Sep 2023 18:43:23 +0200
Subject: Fix more issues

---
 compiler/Config.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index ccbb4c75..508746d9 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -331,3 +331,11 @@ let record_fields_short_names = ref false
     and to account for type constraints (like [fn f<T : Foo>(...) where T::bar = usize]).
  *)
 let parameterize_trait_types = ref false
+
+(** For sanity check: type check the generated pure code (activates checks in
+    several places).
+
+    TODO: deactivated for now because we need to implement the normalization of
+    trait associated types in the pure code.
+ *)
+let type_check_pure_code = ref false
-- 
cgit v1.2.3


From e8aa3804ef0134631cc16b257775ad8f98690c29 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 14 Sep 2023 00:42:46 +0200
Subject: Make progress on the extraction

---
 compiler/Config.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 508746d9..62f6c300 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -339,3 +339,7 @@ let parameterize_trait_types = ref false
     trait associated types in the pure code.
  *)
 let type_check_pure_code = ref false
+
+(** Shall we fail hard if there is an issue at code-generation time?
+    We may not want in case outputting a code with holes helps debugging *)
+let extract_fail_hard = ref false
-- 
cgit v1.2.3


From b631875f8166b3db81187a179eef2f21f52db2bd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 15:26:41 +0200
Subject: Remove the possibility of generating opaque module signatures

---
 compiler/Config.ml | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 62f6c300..cd0903b6 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -306,13 +306,6 @@ let filter_useless_monadic_calls = ref true
  *)
 let filter_useless_functions = ref true
 
-(** Obsolete. TODO: remove.
-
-    For Lean we used to parameterize the entire development by a section variable
-    called opaque_defs, of type OpaqueDefs.
-  *)
-let wrap_opaque_in_sig = ref false
-
 (** Use short names for the record fields.
 
     Some backends can't disambiguate records when their field names have collisions.
-- 
cgit v1.2.3


From 9df1d191cfaf929b755e9d26d55811531acd939d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 11:21:53 +0100
Subject: Fix a small issue in AssociatedTypes

---
 compiler/Config.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index cd0903b6..8483c879 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -333,6 +333,6 @@ let parameterize_trait_types = ref false
  *)
 let type_check_pure_code = ref false
 
-(** Shall we fail hard if there is an issue at code-generation time?
-    We may not want in case outputting a code with holes helps debugging *)
-let extract_fail_hard = ref false
+(** Shall we fail hard if we encounter an issue, or should we attempt to go
+    as far as possible while leaving "holes" in the generated code? *)
+let fail_hard = ref true
-- 
cgit v1.2.3


From c57dec640d4e12c3dc66969d626bbbca2eb733fd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 11:43:47 +0100
Subject: Modify some options and update the Makefile

---
 compiler/Config.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 8483c879..a487f9e2 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -124,7 +124,7 @@ let always_deconstruct_adts_with_matches = ref false
 (** Controls whether we need to use a state to model the external world
     (I/O, for instance).
  *)
-let use_state = ref true
+let use_state = ref false
 
 (** Controls whether we use fuel to control termination.
  *)
@@ -160,7 +160,7 @@ let backward_no_state_update = ref false
     files for the types, clauses and functions, or if we group them in
     one file.
  *)
-let split_files = ref true
+let split_files = ref false
 
 (** Generate the library entry point, if the crate is split between different files.
 
-- 
cgit v1.2.3


From b916f696c5265dc4f5af4a67b118b005a7ed8612 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 17:24:50 +0100
Subject: Reorganize the "Extract" files

---
 compiler/Config.ml | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index a487f9e2..fe110ee4 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -336,3 +336,30 @@ let type_check_pure_code = ref false
 (** Shall we fail hard if we encounter an issue, or should we attempt to go
     as far as possible while leaving "holes" in the generated code? *)
 let fail_hard = ref true
+
+(** if true, add the type name as a prefix
+    to the variant names.
+    Ex.:
+    In Rust:
+      {[
+        enum List = {
+          Cons(u32, Box<List>),x
+          Nil,
+        }
+      ]}
+
+    F*, if option activated:
+      {[
+        type list =
+        | ListCons : u32 -> list -> list
+        | ListNil : list
+      ]}
+
+    F*, if option not activated:
+      {[
+        type list =
+        | Cons : u32 -> list -> list
+        | Nil : list
+      ]}
+ *)
+let variant_concatenate_type_name = ref true
-- 
cgit v1.2.3


From fdb8555cf6bc21ea230141373920196b078bdd28 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 13:48:46 +0100
Subject: Do not activate the sanity (invariant) checks by default

---
 compiler/Config.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index fe110ee4..48ee0a06 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -35,11 +35,11 @@ let backend = ref FStar
 
 (** {1 Interpreter} *)
 
-(** Check that invariants are maintained whenever we execute a statement
-
-    TODO: rename to sanity_checks.
+(** Activate the sanity checks, and in particular the invariant checks
+    that are performed at every evaluation step. This is very expensive
+    (~100x slow down) but very efficient to catch mistakes early.
  *)
-let check_invariants = ref true
+let sanity_checks = ref false
 
 (** Expand all symbolic values containing borrows upon introduction - allows
     to use restrict ourselves to a simpler model for the projectors over
-- 
cgit v1.2.3


From 8a6c26355ef82de725ed643f4a3c40ed54d1b4c7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 14:19:12 +0100
Subject: Update a comment

---
 compiler/Config.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 48ee0a06..1a00656d 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -52,7 +52,8 @@ let greedy_expand_symbolics_with_borrows = true
 
 (** Experimental.
 
-    TODO: remove (always true now)
+    TODO: remove (always true now), but check that when we panic/call a function
+    there is no bottom below a borrow.
 
     We sometimes want to temporarily break the invariant that there is no
     bottom value below a borrow. If this value is true, we don't check
-- 
cgit v1.2.3


From 6f8f1213e056804eda4c521922cdf45f4e92a509 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 15:57:55 +0100
Subject: Fix the issues with the cross-references for OCaml doc

---
 compiler/Config.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 1a00656d..364ef748 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -289,7 +289,7 @@ let unfold_monadic_let_bindings = ref false
     we later filter the useless *forward* calls in the micro-passes, where it is
     more natural to do.
 
-    See the comments for {!val:PureMicroPasses.expression_contains_child_call_in_all_paths}
+    See the comments for {!PureMicroPasses.expression_contains_child_call_in_all_paths}
     for additional explanations.
  *)
 let filter_useless_monadic_calls = ref true
-- 
cgit v1.2.3