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