From 6f22190cba92a44b6c74bfcce8f5ed142a68e195 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 31 Aug 2023 12:47:43 +0200
Subject: Start adding support for traits

---
 compiler/Translate.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 70ef5e3d..ca661108 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -280,9 +280,7 @@ let translate_crate_to_pure (crate : A.crate) :
   log#ldebug (lazy "translate_crate_to_pure");
 
   (* Compute the type and function contexts *)
-  let type_context, fun_context, global_context =
-    compute_type_fun_global_contexts crate
-  in
+  let type_context, fun_context, global_context = compute_contexts crate in
   let fun_infos =
     FA.analyze_module crate fun_context.C.fun_decls
       global_context.C.global_decls !Config.use_state
-- 
cgit v1.2.3


From b42c0a8fa4708d6bf8424d63b6a7fe4964ba0e3d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 3 Sep 2023 15:18:36 +0200
Subject: Make progress on the extraction

---
 compiler/Translate.ml | 109 ++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 93 insertions(+), 16 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index ca661108..f4f59187 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -5,6 +5,7 @@ module T = Types
 module A = LlbcAst
 module SA = SymbolicAst
 module Micro = PureMicroPasses
+module C = Contexts
 open PureUtils
 open TranslateCore
 
@@ -28,18 +29,34 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl)
       ("translate_function_to_symbolics: "
       ^ Print.fun_name_to_string fdef.A.name));
 
-  let { type_context; fun_context; global_context } = trans_ctx in
+  let {
+    type_context;
+    fun_context;
+    global_context;
+    trait_decls_context;
+    trait_impls_context;
+  } =
+    trans_ctx
+  in
   let fun_context = { C.fun_decls = fun_context.fun_decls } in
 
+  (* TODO: we should merge trans_ctx and decls_ctx *)
+  let decls_ctx : C.decls_ctx =
+    {
+      C.type_ctx = type_context;
+      fun_ctx = fun_context;
+      global_ctx = global_context;
+      trait_decls_ctx = trait_decls_context;
+      trait_impls_ctx = trait_impls_context;
+    }
+  in
+
   match fdef.body with
   | None -> None
   | Some _ ->
       (* Evaluate *)
       let synthesize = true in
-      let inputs, symb =
-        evaluate_function_symbolic synthesize type_context fun_context
-          global_context fdef
-      in
+      let inputs, symb = evaluate_function_symbolic synthesize decls_ctx fdef in
       Some (inputs, Option.get symb)
 
 (** Translate a function, by generating its forward and backward translations.
@@ -57,7 +74,15 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
     (lazy
       ("translate_function_to_pure: " ^ Print.fun_name_to_string fdef.A.name));
 
-  let { type_context; fun_context; global_context } = trans_ctx in
+  let {
+    type_context;
+    fun_context;
+    global_context;
+    trait_decls_context;
+    trait_impls_context;
+  } =
+    trans_ctx
+  in
   let def_id = fdef.def_id in
 
   (* Compute the symbolic ASTs, if the function is transparent *)
@@ -148,6 +173,8 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       type_context;
       fun_context;
       global_context;
+      trait_decls_ctx = trait_decls_context.trait_decls;
+      trait_impls_ctx = trait_impls_context.trait_impls;
       fun_decl = fdef;
       forward_inputs = [];
       (* Empty for now *)
@@ -280,13 +307,21 @@ let translate_crate_to_pure (crate : A.crate) :
   log#ldebug (lazy "translate_crate_to_pure");
 
   (* Compute the type and function contexts *)
-  let type_context, fun_context, global_context = compute_contexts crate in
+  let decls_ctx = compute_contexts crate in
   let fun_infos =
-    FA.analyze_module crate fun_context.C.fun_decls
-      global_context.C.global_decls !Config.use_state
+    FA.analyze_module crate decls_ctx.fun_ctx.C.fun_decls
+      decls_ctx.global_ctx.C.global_decls !Config.use_state
+  in
+  let fun_context = { fun_decls = decls_ctx.fun_ctx.fun_decls; fun_infos } in
+  let trans_ctx =
+    {
+      type_context = decls_ctx.type_ctx;
+      fun_context;
+      global_context = decls_ctx.global_ctx;
+      trait_decls_context = decls_ctx.trait_decls_ctx;
+      trait_impls_context = decls_ctx.trait_impls_ctx;
+    }
   in
-  let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in
-  let trans_ctx = { type_context; fun_context; global_context } in
 
   (* Translate all the type definitions *)
   let type_decls =
@@ -323,7 +358,7 @@ let translate_crate_to_pure (crate : A.crate) :
   let sigs = List.append assumed_sigs local_sigs in
   let fun_sigs =
     SymbolicToPure.translate_fun_signatures fun_context.fun_infos
-      type_context.type_infos sigs
+      decls_ctx.type_ctx.type_infos sigs
   in
 
   (* Translate all the *transparent* functions *)
@@ -696,6 +731,36 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
           Extract.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd)
       pure_ls
 
+(** Export a trait declaration. *)
+let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
+    (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) : unit =
+  let trait_decl =
+    T.TraitDeclId.Map.find trait_decl_id
+      ctx.extract_ctx.trans_ctx.trait_decls_context.trait_decls
+  in
+  (* We translate the trait declaration on the fly (note that
+     trait declarations do not directly contain functions, constants,
+     etc.: they simply refer to them). *)
+  let type_infos = ctx.extract_ctx.trans_ctx.type_context.type_infos in
+  let trait_decl = SymbolicToPure.translate_trait_decl type_infos trait_decl in
+  let ctx = ctx.extract_ctx in
+  let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
+  Extract.extract_trait_decl ctx fmt trait_decl
+
+(** Export a trait implementation. *)
+let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
+    (ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit =
+  let trait_impl =
+    T.TraitImplId.Map.find trait_impl_id
+      ctx.extract_ctx.trans_ctx.trait_impls_context.trait_impls
+  in
+  (* We translate the trait implementation on the fly (note that
+     trait implementations do not directly contain functions, constants,
+     etc.: they simply refer to them). *)
+  let type_infos = ctx.extract_ctx.trans_ctx.type_context.type_infos in
+  let trait_impl = SymbolicToPure.translate_trait_impl type_infos trait_impl in
+  Extract.extract_trait_impl ctx.extract_ctx fmt trait_impl
+
 (** A generic utility to generate the extracted definitions: as we may want to
     split the definitions between different files (or not), we can control
     what is precisely extracted.
@@ -710,6 +775,8 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
   let export_functions_group = export_functions_group fmt config ctx in
   let export_global = export_global fmt config ctx in
   let export_types_group = export_types_group fmt config ctx in
+  let export_trait_decl = export_trait_decl fmt config ctx in
+  let export_trait_impl = export_trait_impl fmt config ctx in
 
   let export_state_type () : unit =
     let kind =
@@ -723,11 +790,18 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
     | Type (NonRec id) ->
         if config.extract_types then export_types_group false [ id ]
     | Type (Rec ids) -> if config.extract_types then export_types_group true ids
-    | Fun (NonRec id) ->
+    | Fun (NonRec id) -> (
         (* Lookup *)
         let pure_fun = A.FunDeclId.Map.find id ctx.trans_funs in
-        (* Translate *)
-        export_functions_group [ pure_fun ]
+        (* Special case: we skip trait method *declarations* (we will
+           extract their type directly in the records we generate for
+           the trait declarations themselves, there is no point in having
+           separate type definitions) *)
+        match (fst (fst (snd pure_fun))).Pure.kind with
+        | TraitMethodDecl _ -> ()
+        | _ ->
+            (* Translate *)
+            export_functions_group [ pure_fun ])
     | Fun (Rec ids) ->
         (* General case of mutually recursive functions *)
         (* Lookup *)
@@ -737,11 +811,13 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
         (* Translate *)
         export_functions_group pure_funs
     | Global id -> export_global id
+    | TraitDecl id -> export_trait_decl id
+    | TraitImpl id -> export_trait_impl id
   in
 
   (* If we need to export the state type: we try to export it after we defined
    * the type definitions, because if the user wants to define a model for the
-   * type, he might want to reuse those in the state type.
+   * type, they might want to reuse those in the state type.
    * More specifically: if we extract functions in the same file as the type,
    * we have no choice but to define the state type before the functions,
    * because they may reuse this state type: in this case, we define/declare
@@ -930,6 +1006,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       use_opaque_pre = !Config.split_files;
       use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
       fun_name_info = PureUtils.RegularFunIdMap.empty;
+      trait_decl_id = None (* None by default *);
     }
   in
 
-- 
cgit v1.2.3


From a2f19257651df3c8473e17ef73a5389b9cb89bbf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 3 Sep 2023 16:35:05 +0200
Subject: Make progress on the extraction

---
 compiler/Translate.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index f4f59187..790dbe14 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -1007,6 +1007,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
       fun_name_info = PureUtils.RegularFunIdMap.empty;
       trait_decl_id = None (* None by default *);
+      is_provided_method = false (* false by default *);
     }
   in
 
-- 
cgit v1.2.3


From 0e0f3d586e7e74003ebff129a1e91b87602467e7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 3 Sep 2023 16:51:36 +0200
Subject: Make more progress

---
 compiler/Translate.ml | 70 ++++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 52 insertions(+), 18 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 790dbe14..8df69961 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -301,8 +301,13 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
   (* Return *)
   (pure_forward, pure_backwards)
 
+(* TODO: factor out the return type *)
 let translate_crate_to_pure (crate : A.crate) :
-    trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list =
+    trans_ctx
+    * Pure.type_decl list
+    * (bool * pure_fun_translation) list
+    * Pure.trait_decl list
+    * Pure.trait_impl list =
   (* Debug *)
   log#ldebug (lazy "translate_crate_to_pure");
 
@@ -368,13 +373,28 @@ let translate_crate_to_pure (crate : A.crate) :
       (A.FunDeclId.Map.values crate.functions)
   in
 
+  (* Translate the trait declarations *)
+  let type_infos = trans_ctx.type_context.type_infos in
+  let trait_decls =
+    List.map
+      (SymbolicToPure.translate_trait_decl type_infos)
+      (T.TraitDeclId.Map.values trans_ctx.trait_decls_context.trait_decls)
+  in
+
+  (* Translate the trait implementations *)
+  let trait_impls =
+    List.map
+      (SymbolicToPure.translate_trait_impl type_infos)
+      (T.TraitImplId.Map.values trans_ctx.trait_impls_context.trait_impls)
+  in
+
   (* Apply the micro-passes *)
   let pure_translations =
     Micro.apply_passes_to_pure_fun_translations trans_ctx pure_translations
   in
 
   (* Return *)
-  (trans_ctx, type_decls, pure_translations)
+  (trans_ctx, type_decls, pure_translations, trait_decls, trait_impls)
 
 (** Extraction context *)
 type gen_ctx = {
@@ -735,14 +755,8 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
 let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
     (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) : unit =
   let trait_decl =
-    T.TraitDeclId.Map.find trait_decl_id
-      ctx.extract_ctx.trans_ctx.trait_decls_context.trait_decls
+    T.TraitDeclId.Map.find trait_decl_id ctx.extract_ctx.trans_trait_decls
   in
-  (* We translate the trait declaration on the fly (note that
-     trait declarations do not directly contain functions, constants,
-     etc.: they simply refer to them). *)
-  let type_infos = ctx.extract_ctx.trans_ctx.type_context.type_infos in
-  let trait_decl = SymbolicToPure.translate_trait_decl type_infos trait_decl in
   let ctx = ctx.extract_ctx in
   let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
   Extract.extract_trait_decl ctx fmt trait_decl
@@ -751,14 +765,8 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
 let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
     (ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit =
   let trait_impl =
-    T.TraitImplId.Map.find trait_impl_id
-      ctx.extract_ctx.trans_ctx.trait_impls_context.trait_impls
+    T.TraitImplId.Map.find trait_impl_id ctx.extract_ctx.trans_trait_impls
   in
-  (* We translate the trait implementation on the fly (note that
-     trait implementations do not directly contain functions, constants,
-     etc.: they simply refer to them). *)
-  let type_infos = ctx.extract_ctx.trans_ctx.type_context.type_infos in
-  let trait_impl = SymbolicToPure.translate_trait_impl type_infos trait_impl in
   Extract.extract_trait_impl ctx.extract_ctx fmt trait_impl
 
 (** A generic utility to generate the extracted definitions: as we may want to
@@ -978,7 +986,9 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
 let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
     unit =
   (* Translate the module to the pure AST *)
-  let trans_ctx, trans_types, trans_funs = translate_crate_to_pure crate in
+  let trans_ctx, trans_types, trans_funs, trans_trait_decls, trans_trait_impls =
+    translate_crate_to_pure crate
+  in
 
   (* Initialize the extraction context - for now we extract only to F*.
    * We initialize the names map by registering the keywords used in the
@@ -997,6 +1007,18 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   in
   (* Put everything in the context *)
   let ctx =
+    let trans_trait_decls =
+      T.TraitDeclId.Map.of_list
+        (List.map
+           (fun (d : Pure.trait_decl) -> (d.def_id, d))
+           trans_trait_decls)
+    in
+    let trans_trait_impls =
+      T.TraitImplId.Map.of_list
+        (List.map
+           (fun (d : Pure.trait_impl) -> (d.def_id, d))
+           trans_trait_impls)
+    in
     {
       ExtractBase.trans_ctx;
       names_map;
@@ -1008,6 +1030,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       fun_name_info = PureUtils.RegularFunIdMap.empty;
       trait_decl_id = None (* None by default *);
       is_provided_method = false (* false by default *);
+      trans_trait_decls;
+      trans_trait_impls;
     }
   in
 
@@ -1034,7 +1058,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   in
   let rec_functions = PureUtils.FunLoopIdSet.of_list rec_functions in
 
-  (* Register unique names for all the top-level types, globals and functions.
+  (* Register unique names for all the top-level types, globals, functions...
    * Note that the order in which we generate the names doesn't matter:
    * we just need to generate a mapping from identifier to name, and make
    * sure there are no name clashes. *)
@@ -1071,6 +1095,16 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       (A.GlobalDeclId.Map.values crate.globals)
   in
 
+  let ctx =
+    List.fold_left Extract.extract_trait_decl_register_names ctx
+      trans_trait_decls
+  in
+
+  let ctx =
+    List.fold_left Extract.extract_trait_impl_register_names ctx
+      trans_trait_impls
+  in
+
   (* Open the output file *)
   (* First compute the filename by replacing the extension and converting the
    * case (rust module names are snake case) *)
-- 
cgit v1.2.3


From 9fe9fc0ab70b8629722d60748bbede554017172c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 3 Sep 2023 18:59:19 +0200
Subject: Make progress on extracting trait decls and merge gen_ctx and
 extraction_ctx

---
 compiler/Translate.ml | 163 ++++++++++++++++++++++----------------------------
 1 file changed, 70 insertions(+), 93 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 8df69961..b26ce23b 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -396,14 +396,7 @@ let translate_crate_to_pure (crate : A.crate) :
   (* Return *)
   (trans_ctx, type_decls, pure_translations, trait_decls, trait_impls)
 
-(** Extraction context *)
-type gen_ctx = {
-  crate : A.crate;
-  extract_ctx : ExtractBase.extraction_ctx;
-  trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
-  trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t;
-  functions_with_decreases_clause : PureUtils.FunLoopIdSet.t;
-}
+type gen_ctx = ExtractBase.extraction_ctx
 
 type gen_config = {
   extract_types : bool;
@@ -482,9 +475,9 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     || ((not is_opaque) && config.extract_transparent)
   then (
     if extract_decl then
-      Extract.extract_type_decl ctx.extract_ctx fmt type_decl_group kind def;
+      Extract.extract_type_decl ctx fmt type_decl_group kind def;
     if extract_extra_info then
-      Extract.extract_type_decl_extra_info ctx.extract_ctx fmt kind def)
+      Extract.extract_type_decl_extra_info ctx fmt kind def)
 
 (** Export a group of types.
 
@@ -536,7 +529,7 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
        End
      ]}
   *)
-  Extract.start_type_decl_group ctx.extract_ctx fmt is_rec defs;
+  Extract.start_type_decl_group ctx fmt is_rec defs;
   List.iteri
     (fun i def ->
       let kind = kind_from_index i in
@@ -557,7 +550,7 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
  *)
 let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     (id : A.GlobalDeclId.id) : unit =
-  let global_decls = ctx.extract_ctx.trans_ctx.global_context.global_decls in
+  let global_decls = ctx.trans_ctx.global_context.global_decls in
   let global = A.GlobalDeclId.Map.find id global_decls in
   let _, ((body, loop_fwds), body_backs) =
     A.FunDeclId.Map.find global.body_id ctx.trans_funs
@@ -576,7 +569,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
        groups are always singletons, so the [extract_global_decl] function
        takes care of generating the delimiters.
     *)
-    Extract.extract_global_decl ctx.extract_ctx fmt global body config.interface
+    Extract.extract_global_decl ctx fmt global body config.interface
 
 (** Utility.
 
@@ -657,14 +650,13 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config)
         then
           Some
             (fun () ->
-              Extract.extract_fun_decl ctx.extract_ctx fmt kind has_decr_clause
-                def)
+              Extract.extract_fun_decl ctx fmt kind has_decr_clause def)
         else None)
       decls
   in
   let extract_defs = List.filter_map (fun x -> x) extract_defs in
   if extract_defs <> [] then (
-    Extract.start_fun_decl_group ctx.extract_ctx fmt is_rec decls;
+    Extract.start_fun_decl_group ctx fmt is_rec decls;
     List.iter (fun f -> f ()) extract_defs;
     Extract.end_fun_decl_group fmt is_rec decls)
 
@@ -700,11 +692,10 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
           if has_decr_clause then
             match !Config.backend with
             | Lean ->
-                Extract.extract_template_lean_termination_and_decreasing
-                  ctx.extract_ctx fmt decl
+                Extract.extract_template_lean_termination_and_decreasing ctx fmt
+                  decl
             | FStar ->
-                Extract.extract_template_fstar_decreases_clause ctx.extract_ctx
-                  fmt decl
+                Extract.extract_template_fstar_decreases_clause ctx fmt decl
             | Coq ->
                 raise (Failure "Coq doesn't have decreases/termination clauses")
             | HOL4 ->
@@ -747,27 +738,21 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   if config.test_trans_unit_functions then
     List.iter
       (fun (keep_fwd, ((fwd, _), _)) ->
-        if keep_fwd then
-          Extract.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd)
+        if keep_fwd then Extract.extract_unit_test_if_unit_fun ctx fmt fwd)
       pure_ls
 
 (** Export a trait declaration. *)
 let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
     (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) : unit =
-  let trait_decl =
-    T.TraitDeclId.Map.find trait_decl_id ctx.extract_ctx.trans_trait_decls
-  in
-  let ctx = ctx.extract_ctx in
+  let trait_decl = T.TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in
   let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
   Extract.extract_trait_decl ctx fmt trait_decl
 
 (** Export a trait implementation. *)
 let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
     (ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit =
-  let trait_impl =
-    T.TraitImplId.Map.find trait_impl_id ctx.extract_ctx.trans_trait_impls
-  in
-  Extract.extract_trait_impl ctx.extract_ctx fmt trait_impl
+  let trait_impl = T.TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in
+  Extract.extract_trait_impl ctx fmt trait_impl
 
 (** A generic utility to generate the extracted definitions: as we may want to
     split the definitions between different files (or not), we can control
@@ -790,7 +775,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
     let kind =
       if config.interface then ExtractBase.Declared else ExtractBase.Assumed
     in
-    Extract.extract_state_type fmt ctx.extract_ctx kind
+    Extract.extract_state_type fmt ctx kind
   in
 
   let export_decl_group (dg : A.declaration_group) : unit =
@@ -856,7 +841,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
       if config.extract_transparent then "Definitions" else "OpaqueDefs"
     in
     Format.pp_print_break fmt 0 0;
-    Format.pp_open_vbox fmt ctx.extract_ctx.indent_incr;
+    Format.pp_open_vbox fmt ctx.indent_incr;
     Format.pp_print_string fmt ("structure " ^ struct_name ^ " where");
     Format.pp_print_break fmt 0 0);
   List.iter export_decl_group ctx.crate.declarations;
@@ -1005,6 +990,43 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
     mk_formatter_and_names_map trans_ctx crate.name
       variant_concatenate_type_name
   in
+
+  (* We need to compute which functions are recursive, in order to know
+   * whether we should generate a decrease clause or not. *)
+  let rec_functions =
+    List.map
+      (fun (_, ((fwd, loop_fwds), _)) ->
+        let fwd =
+          if fwd.Pure.signature.info.effect_info.is_rec then
+            [ (fwd.def_id, None) ]
+          else []
+        in
+        let loop_fwds =
+          List.map
+            (fun (def : Pure.fun_decl) -> [ (def.def_id, def.loop_id) ])
+            loop_fwds
+        in
+        fwd :: loop_fwds)
+      trans_funs
+  in
+  let rec_functions : PureUtils.fun_loop_id list =
+    List.concat (List.concat rec_functions)
+  in
+  let rec_functions = PureUtils.FunLoopIdSet.of_list rec_functions in
+
+  (* Put the translated definitions in maps *)
+  let trans_types =
+    Pure.TypeDeclId.Map.of_list
+      (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types)
+  in
+  let trans_funs =
+    A.FunDeclId.Map.of_list
+      (List.map
+         (fun ((keep_fwd, (fd, bdl)) : bool * pure_fun_translation) ->
+           ((fst fd).def_id, (keep_fwd, (fd, bdl))))
+         trans_funs)
+  in
+
   (* Put everything in the context *)
   let ctx =
     let trans_trait_decls =
@@ -1020,7 +1042,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
            trans_trait_impls)
     in
     {
-      ExtractBase.trans_ctx;
+      ExtractBase.crate;
+      trans_ctx;
       names_map;
       unsafe_names_map = { id_to_name = ExtractBase.IdMap.empty };
       fmt;
@@ -1032,32 +1055,12 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       is_provided_method = false (* false by default *);
       trans_trait_decls;
       trans_trait_impls;
+      trans_types;
+      trans_funs;
+      functions_with_decreases_clause = rec_functions;
     }
   in
 
-  (* We need to compute which functions are recursive, in order to know
-   * whether we should generate a decrease clause or not. *)
-  let rec_functions =
-    List.map
-      (fun (_, ((fwd, loop_fwds), _)) ->
-        let fwd =
-          if fwd.Pure.signature.info.effect_info.is_rec then
-            [ (fwd.def_id, None) ]
-          else []
-        in
-        let loop_fwds =
-          List.map
-            (fun (def : Pure.fun_decl) -> [ (def.def_id, def.loop_id) ])
-            loop_fwds
-        in
-        fwd :: loop_fwds)
-      trans_funs
-  in
-  let rec_functions : PureUtils.fun_loop_id list =
-    List.concat (List.concat rec_functions)
-  in
-  let rec_functions = PureUtils.FunLoopIdSet.of_list rec_functions in
-
   (* Register unique names for all the top-level types, globals, functions...
    * Note that the order in which we generate the names doesn't matter:
    * we just need to generate a mapping from identifier to name, and make
@@ -1065,7 +1068,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   let ctx =
     List.fold_left
       (fun ctx def -> Extract.extract_type_decl_register_names ctx def)
-      ctx trans_types
+      ctx
+      (Pure.TypeDeclId.Map.values trans_types)
   in
 
   let ctx =
@@ -1087,7 +1091,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
         else
           Extract.extract_fun_decl_register_names ctx keep_fwd gen_decr_clause
             defs)
-      ctx trans_funs
+      ctx
+      (A.FunDeclId.Map.values trans_funs)
   in
 
   let ctx =
@@ -1133,19 +1138,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
         (namespace, crate_name, Filename.concat dest_dir crate_name)
   in
 
-  (* Put the translated definitions in maps *)
-  let trans_types =
-    Pure.TypeDeclId.Map.of_list
-      (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types)
-  in
-  let trans_funs =
-    A.FunDeclId.Map.of_list
-      (List.map
-         (fun ((keep_fwd, (fd, bdl)) : bool * pure_fun_translation) ->
-           ((fst fd).def_id, (keep_fwd, (fd, bdl))))
-         trans_funs)
-  in
-
   let mkdir_if dest_dir =
     if not (Sys.file_exists dest_dir) then (
       log#linfo (lazy ("Creating missing directory: " ^ dest_dir));
@@ -1201,16 +1193,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   in
 
   (* Extract the file(s) *)
-  let gen_ctx =
-    {
-      crate;
-      extract_ctx = ctx;
-      trans_types;
-      trans_funs;
-      functions_with_decreases_clause = rec_functions;
-    }
-  in
-
   let module_delimiter =
     match !Config.backend with
     | FStar -> "."
@@ -1257,7 +1239,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
 
      (* Check if there are opaque types and functions - in which case we need
       * to split *)
-     let has_opaque_types, has_opaque_funs = module_has_opaque_decls gen_ctx in
+     let has_opaque_types, has_opaque_funs = module_has_opaque_decls ctx in
      let has_opaque_types = has_opaque_types || !Config.use_state in
 
      (* Extract the types *)
@@ -1296,7 +1278,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
          custom_includes = [];
        }
      in
-     extract_file types_config gen_ctx file_info;
+     extract_file types_config ctx file_info;
 
      (* Extract the template clauses *)
      (if needs_clauses_module && !Config.extract_template_decreases_clauses then
@@ -1324,7 +1306,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
             custom_includes = [];
           }
         in
-        extract_file template_clauses_config gen_ctx file_info);
+        extract_file template_clauses_config ctx file_info);
 
      (* Extract the opaque functions, if needed *)
      let opaque_funs_module =
@@ -1359,12 +1341,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
              interface = true;
            }
          in
-         let gen_ctx =
-           {
-             gen_ctx with
-             extract_ctx = { gen_ctx.extract_ctx with use_opaque_pre = false };
-           }
-         in
+         let ctx = { ctx with use_opaque_pre = false } in
          let file_info =
            {
              filename = opaque_filename;
@@ -1378,7 +1355,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
              custom_includes = [ types_module ];
            }
          in
-         extract_file opaque_config gen_ctx file_info;
+         extract_file opaque_config ctx file_info;
          (* Return the additional dependencies *)
          [ opaque_imported_module ])
        else []
@@ -1417,7 +1394,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
            [ types_module ] @ opaque_funs_module @ clauses_module;
        }
      in
-     extract_file fun_config gen_ctx file_info)
+     extract_file fun_config ctx file_info)
    else
      let gen_config =
        {
@@ -1447,7 +1424,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
          custom_includes = [];
        }
      in
-     extract_file gen_config gen_ctx file_info);
+     extract_file gen_config ctx file_info);
 
   (* Generate the build file *)
   match !Config.backend with
-- 
cgit v1.2.3


From 9fb4886f9003f75e8d3aafaf51586ab5f9001744 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 3 Sep 2023 19:18:25 +0200
Subject: Update the type TranslateCore.fun_and_loops

---
 compiler/Translate.ml | 46 +++++++++++++++++++++++-----------------------
 1 file changed, 23 insertions(+), 23 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index b26ce23b..2f751693 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -439,8 +439,8 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
   in
   let has_opaque_funs =
     A.FunDeclId.Map.exists
-      (fun _ ((_, ((t_fwd, _), _)) : bool * pure_fun_translation) ->
-        Option.is_none t_fwd.body)
+      (fun _ ((_, (fwd, _)) : bool * pure_fun_translation) ->
+        Option.is_none fwd.f.body)
       ctx.trans_funs
   in
   (has_opaque_types, has_opaque_funs)
@@ -552,7 +552,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     (id : A.GlobalDeclId.id) : unit =
   let global_decls = ctx.trans_ctx.global_context.global_decls in
   let global = A.GlobalDeclId.Map.find id global_decls in
-  let _, ((body, loop_fwds), body_backs) =
+  let _, ({ f = body; loops = loop_fwds }, body_backs) =
     A.FunDeclId.Map.find global.body_id ctx.trans_funs
   in
   assert (body_backs = []);
@@ -676,7 +676,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   (* Extract the decrease clauses template bodies *)
   if config.extract_template_decreases_clauses then
     List.iter
-      (fun (_, ((fwd, loop_fwds), _)) ->
+      (fun (_, (fwd, _)) ->
         (* We only generate decreases clauses for the forward functions, because
            the termination argument should only depend on the forward inputs.
            The backward functions thus use the same decreases clauses as the
@@ -702,8 +702,8 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
                 raise
                   (Failure "HOL4 doesn't have decreases/termination clauses")
         in
-        extract_decrease fwd;
-        List.iter extract_decrease loop_fwds)
+        extract_decrease fwd.f;
+        List.iter extract_decrease fwd.loops)
       pure_ls;
 
   (* Concatenate the function definitions, filtering the useless forward
@@ -711,12 +711,12 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   let decls =
     List.concat
       (List.map
-         (fun (keep_fwd, ((fwd, fwd_loops), (back_ls : fun_and_loops list))) ->
-           let fwd = if keep_fwd then List.append fwd_loops [ fwd ] else [] in
+         (fun (keep_fwd, (fwd, (back_ls : fun_and_loops list))) ->
+           let fwd = if keep_fwd then List.append fwd.loops [ fwd.f ] else [] in
            let back : Pure.fun_decl list =
              List.concat
                (List.map
-                  (fun (back, loop_backs) -> List.append loop_backs [ back ])
+                  (fun back -> List.append back.loops [ back.f ])
                   back_ls)
            in
            List.append fwd back)
@@ -737,8 +737,8 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   (* Insert unit tests if necessary *)
   if config.test_trans_unit_functions then
     List.iter
-      (fun (keep_fwd, ((fwd, _), _)) ->
-        if keep_fwd then Extract.extract_unit_test_if_unit_fun ctx fmt fwd)
+      (fun (keep_fwd, (fwd, _)) ->
+        if keep_fwd then Extract.extract_unit_test_if_unit_fun ctx fmt fwd.f)
       pure_ls
 
 (** Export a trait declaration. *)
@@ -790,7 +790,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
            extract their type directly in the records we generate for
            the trait declarations themselves, there is no point in having
            separate type definitions) *)
-        match (fst (fst (snd pure_fun))).Pure.kind with
+        match (fst (snd pure_fun)).f.Pure.kind with
         | TraitMethodDecl _ -> ()
         | _ ->
             (* Translate *)
@@ -995,18 +995,18 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
    * whether we should generate a decrease clause or not. *)
   let rec_functions =
     List.map
-      (fun (_, ((fwd, loop_fwds), _)) ->
-        let fwd =
-          if fwd.Pure.signature.info.effect_info.is_rec then
-            [ (fwd.def_id, None) ]
+      (fun (_, (fwd, _)) ->
+        let fwd_f =
+          if fwd.f.Pure.signature.info.effect_info.is_rec then
+            [ (fwd.f.def_id, None) ]
           else []
         in
         let loop_fwds =
           List.map
             (fun (def : Pure.fun_decl) -> [ (def.def_id, def.loop_id) ])
-            loop_fwds
+            fwd.loops
         in
-        fwd :: loop_fwds)
+        fwd_f :: loop_fwds)
       trans_funs
   in
   let rec_functions : PureUtils.fun_loop_id list =
@@ -1019,11 +1019,11 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
     Pure.TypeDeclId.Map.of_list
       (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types)
   in
-  let trans_funs =
+  let trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t =
     A.FunDeclId.Map.of_list
       (List.map
-         (fun ((keep_fwd, (fd, bdl)) : bool * pure_fun_translation) ->
-           ((fst fd).def_id, (keep_fwd, (fd, bdl))))
+         (fun ((keep_fwd, (fwd, bdl)) : bool * pure_fun_translation) ->
+           (fwd.f.def_id, (keep_fwd, (fwd, bdl))))
          trans_funs)
   in
 
@@ -1074,10 +1074,10 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
 
   let ctx =
     List.fold_left
-      (fun ctx (keep_fwd, defs) ->
+      (fun ctx ((keep_fwd, defs) : bool * pure_fun_translation) ->
         (* If requested by the user, register termination measures and decreases
            proofs for all the recursive functions *)
-        let fwd_def = fst (fst defs) in
+        let fwd_def = (fst defs).f in
         let gen_decr_clause (def : Pure.fun_decl) =
           !Config.extract_decreases_clauses
           && PureUtils.FunLoopIdSet.mem
-- 
cgit v1.2.3


From cce09bb0fb64b07b07613d7db59857651e040c20 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 3 Sep 2023 19:29:11 +0200
Subject: Update TranslateCore.pure_fun_translation

---
 compiler/Translate.ml | 40 +++++++++++++++++++---------------------
 1 file changed, 19 insertions(+), 21 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 2f751693..7122e462 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -439,8 +439,8 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
   in
   let has_opaque_funs =
     A.FunDeclId.Map.exists
-      (fun _ ((_, (fwd, _)) : bool * pure_fun_translation) ->
-        Option.is_none fwd.f.body)
+      (fun _ ((_, trans) : bool * pure_fun_translation) ->
+        Option.is_none trans.fwd.f.body)
       ctx.trans_funs
   in
   (has_opaque_types, has_opaque_funs)
@@ -552,11 +552,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     (id : A.GlobalDeclId.id) : unit =
   let global_decls = ctx.trans_ctx.global_context.global_decls in
   let global = A.GlobalDeclId.Map.find id global_decls in
-  let _, ({ f = body; loops = loop_fwds }, body_backs) =
-    A.FunDeclId.Map.find global.body_id ctx.trans_funs
-  in
-  assert (body_backs = []);
-  assert (loop_fwds = []);
+  let _, trans = A.FunDeclId.Map.find global.body_id ctx.trans_funs in
+  assert (trans.fwd.loops = []);
+  assert (trans.backs = []);
+  let body = trans.fwd.f in
 
   let is_opaque = Option.is_none body.Pure.body in
   if
@@ -676,7 +675,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   (* Extract the decrease clauses template bodies *)
   if config.extract_template_decreases_clauses then
     List.iter
-      (fun (_, (fwd, _)) ->
+      (fun (_, { fwd; _ }) ->
         (* We only generate decreases clauses for the forward functions, because
            the termination argument should only depend on the forward inputs.
            The backward functions thus use the same decreases clauses as the
@@ -711,15 +710,13 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   let decls =
     List.concat
       (List.map
-         (fun (keep_fwd, (fwd, (back_ls : fun_and_loops list))) ->
+         (fun (keep_fwd, { fwd; backs }) ->
            let fwd = if keep_fwd then List.append fwd.loops [ fwd.f ] else [] in
-           let back : Pure.fun_decl list =
+           let backs : Pure.fun_decl list =
              List.concat
-               (List.map
-                  (fun back -> List.append back.loops [ back.f ])
-                  back_ls)
+               (List.map (fun back -> List.append back.loops [ back.f ]) backs)
            in
-           List.append fwd back)
+           List.append fwd backs)
          pure_ls)
   in
 
@@ -737,8 +734,9 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   (* Insert unit tests if necessary *)
   if config.test_trans_unit_functions then
     List.iter
-      (fun (keep_fwd, (fwd, _)) ->
-        if keep_fwd then Extract.extract_unit_test_if_unit_fun ctx fmt fwd.f)
+      (fun (keep_fwd, trans) ->
+        if keep_fwd then
+          Extract.extract_unit_test_if_unit_fun ctx fmt trans.fwd.f)
       pure_ls
 
 (** Export a trait declaration. *)
@@ -790,7 +788,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
            extract their type directly in the records we generate for
            the trait declarations themselves, there is no point in having
            separate type definitions) *)
-        match (fst (snd pure_fun)).f.Pure.kind with
+        match (snd pure_fun).fwd.f.Pure.kind with
         | TraitMethodDecl _ -> ()
         | _ ->
             (* Translate *)
@@ -995,7 +993,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
    * whether we should generate a decrease clause or not. *)
   let rec_functions =
     List.map
-      (fun (_, (fwd, _)) ->
+      (fun (_, { fwd; _ }) ->
         let fwd_f =
           if fwd.f.Pure.signature.info.effect_info.is_rec then
             [ (fwd.f.def_id, None) ]
@@ -1022,8 +1020,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   let trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t =
     A.FunDeclId.Map.of_list
       (List.map
-         (fun ((keep_fwd, (fwd, bdl)) : bool * pure_fun_translation) ->
-           (fwd.f.def_id, (keep_fwd, (fwd, bdl))))
+         (fun ((keep_fwd, { fwd; backs }) : bool * pure_fun_translation) ->
+           (fwd.f.def_id, (keep_fwd, { fwd; backs })))
          trans_funs)
   in
 
@@ -1077,7 +1075,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       (fun ctx ((keep_fwd, defs) : bool * pure_fun_translation) ->
         (* If requested by the user, register termination measures and decreases
            proofs for all the recursive functions *)
-        let fwd_def = (fst defs).f in
+        let fwd_def = defs.fwd.f in
         let gen_decr_clause (def : Pure.fun_decl) =
           !Config.extract_decreases_clauses
           && PureUtils.FunLoopIdSet.mem
-- 
cgit v1.2.3


From dfcbfab4030be2f03b159a4b298ed75ac2f236ae Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 3 Sep 2023 19:41:03 +0200
Subject: Add the keep_fwd field in TranslateCore.pure_fun_translation

---
 compiler/Translate.ml | 34 ++++++++++++++++------------------
 1 file changed, 16 insertions(+), 18 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 7122e462..835edd46 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -305,7 +305,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
 let translate_crate_to_pure (crate : A.crate) :
     trans_ctx
     * Pure.type_decl list
-    * (bool * pure_fun_translation) list
+    * pure_fun_translation list
     * Pure.trait_decl list
     * Pure.trait_impl list =
   (* Debug *)
@@ -439,8 +439,7 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
   in
   let has_opaque_funs =
     A.FunDeclId.Map.exists
-      (fun _ ((_, trans) : bool * pure_fun_translation) ->
-        Option.is_none trans.fwd.f.body)
+      (fun _ (trans : pure_fun_translation) -> Option.is_none trans.fwd.f.body)
       ctx.trans_funs
   in
   (has_opaque_types, has_opaque_funs)
@@ -552,7 +551,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     (id : A.GlobalDeclId.id) : unit =
   let global_decls = ctx.trans_ctx.global_context.global_decls in
   let global = A.GlobalDeclId.Map.find id global_decls in
-  let _, trans = A.FunDeclId.Map.find global.body_id ctx.trans_funs in
+  let trans = A.FunDeclId.Map.find global.body_id ctx.trans_funs in
   assert (trans.fwd.loops = []);
   assert (trans.backs = []);
   let body = trans.fwd.f in
@@ -665,7 +664,7 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config)
     check if the forward and backward functions are mutually recursive.
  *)
 let export_functions_group (fmt : Format.formatter) (config : gen_config)
-    (ctx : gen_ctx) (pure_ls : (bool * pure_fun_translation) list) : unit =
+    (ctx : gen_ctx) (pure_ls : pure_fun_translation list) : unit =
   (* Utility to check a function has a decrease clause *)
   let has_decreases_clause (def : Pure.fun_decl) : bool =
     PureUtils.FunLoopIdSet.mem (def.def_id, def.loop_id)
@@ -675,7 +674,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   (* Extract the decrease clauses template bodies *)
   if config.extract_template_decreases_clauses then
     List.iter
-      (fun (_, { fwd; _ }) ->
+      (fun { fwd; _ } ->
         (* We only generate decreases clauses for the forward functions, because
            the termination argument should only depend on the forward inputs.
            The backward functions thus use the same decreases clauses as the
@@ -710,7 +709,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   let decls =
     List.concat
       (List.map
-         (fun (keep_fwd, { fwd; backs }) ->
+         (fun { keep_fwd; fwd; backs } ->
            let fwd = if keep_fwd then List.append fwd.loops [ fwd.f ] else [] in
            let backs : Pure.fun_decl list =
              List.concat
@@ -734,8 +733,8 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   (* Insert unit tests if necessary *)
   if config.test_trans_unit_functions then
     List.iter
-      (fun (keep_fwd, trans) ->
-        if keep_fwd then
+      (fun trans ->
+        if trans.keep_fwd then
           Extract.extract_unit_test_if_unit_fun ctx fmt trans.fwd.f)
       pure_ls
 
@@ -788,7 +787,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
            extract their type directly in the records we generate for
            the trait declarations themselves, there is no point in having
            separate type definitions) *)
-        match (snd pure_fun).fwd.f.Pure.kind with
+        match pure_fun.fwd.f.Pure.kind with
         | TraitMethodDecl _ -> ()
         | _ ->
             (* Translate *)
@@ -993,7 +992,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
    * whether we should generate a decrease clause or not. *)
   let rec_functions =
     List.map
-      (fun (_, { fwd; _ }) ->
+      (fun { fwd; _ } ->
         let fwd_f =
           if fwd.f.Pure.signature.info.effect_info.is_rec then
             [ (fwd.f.def_id, None) ]
@@ -1017,11 +1016,10 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
     Pure.TypeDeclId.Map.of_list
       (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types)
   in
-  let trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t =
+  let trans_funs : pure_fun_translation A.FunDeclId.Map.t =
     A.FunDeclId.Map.of_list
       (List.map
-         (fun ((keep_fwd, { fwd; backs }) : bool * pure_fun_translation) ->
-           (fwd.f.def_id, (keep_fwd, { fwd; backs })))
+         (fun (trans : pure_fun_translation) -> (trans.fwd.f.def_id, trans))
          trans_funs)
   in
 
@@ -1072,10 +1070,10 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
 
   let ctx =
     List.fold_left
-      (fun ctx ((keep_fwd, defs) : bool * pure_fun_translation) ->
+      (fun ctx (trans : pure_fun_translation) ->
         (* If requested by the user, register termination measures and decreases
            proofs for all the recursive functions *)
-        let fwd_def = defs.fwd.f in
+        let fwd_def = trans.fwd.f in
         let gen_decr_clause (def : Pure.fun_decl) =
           !Config.extract_decreases_clauses
           && PureUtils.FunLoopIdSet.mem
@@ -1087,8 +1085,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
         let is_global = fwd_def.Pure.is_global_decl_body in
         if is_global then ctx
         else
-          Extract.extract_fun_decl_register_names ctx keep_fwd gen_decr_clause
-            defs)
+          Extract.extract_fun_decl_register_names ctx trans.keep_fwd
+            gen_decr_clause trans)
       ctx
       (A.FunDeclId.Map.values trans_funs)
   in
-- 
cgit v1.2.3


From e090e09725e3fd5c7f2a92813955ce2d81560227 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 3 Sep 2023 19:44:39 +0200
Subject: Do more cleanup

---
 compiler/Translate.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 835edd46..a4041751 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -1084,9 +1084,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
          * those are handled later *)
         let is_global = fwd_def.Pure.is_global_decl_body in
         if is_global then ctx
-        else
-          Extract.extract_fun_decl_register_names ctx trans.keep_fwd
-            gen_decr_clause trans)
+        else Extract.extract_fun_decl_register_names ctx gen_decr_clause trans)
       ctx
       (A.FunDeclId.Map.values trans_funs)
   in
-- 
cgit v1.2.3


From 8b18c0da053e069b5a2d9fbf06f45eae2f05a029 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 7 Sep 2023 15:28:06 +0200
Subject: Map some globals like u32::MAX to standard definitions

---
 compiler/Translate.ml | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index a4041751..90066163 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -430,19 +430,9 @@ type gen_config = {
 }
 
 (** Returns the pair: (has opaque type decls, has opaque fun decls) *)
-let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
-  let has_opaque_types =
-    Pure.TypeDeclId.Map.exists
-      (fun _ (d : Pure.type_decl) ->
-        match d.kind with Opaque -> true | _ -> false)
-      ctx.trans_types
-  in
-  let has_opaque_funs =
-    A.FunDeclId.Map.exists
-      (fun _ (trans : pure_fun_translation) -> Option.is_none trans.fwd.f.body)
-      ctx.trans_funs
-  in
-  (has_opaque_types, has_opaque_funs)
+let crate_has_opaque_decls (ctx : gen_ctx) : bool * bool =
+  let types, funs = LlbcAstUtils.crate_get_opaque_decls ctx.crate in
+  (types <> [], funs <> [])
 
 (** Export a type declaration.
 
@@ -557,11 +547,20 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
   let body = trans.fwd.f in
 
   let is_opaque = Option.is_none body.Pure.body in
-  if
+  (* Check if we extract the global *)
+  let extract =
     config.extract_globals
     && (((not is_opaque) && config.extract_transparent)
        || (is_opaque && config.extract_opaque))
-  then
+  in
+  (* Check if it is an assumed global - if yes, we ignore it because we
+     map the definition to one in the standard library *)
+  let open ExtractAssumed in
+  let sname = name_to_simple_name global.name in
+  let extract =
+    extract && SimpleNameMap.find_opt sname assumed_globals_map = None
+  in
+  if extract then
     (* We don't wrap global declaration groups between calls to functions
        [{start, end}_global_decl_group] (which don't exist): global declaration
        groups are always singletons, so the [extract_global_decl] function
@@ -828,7 +827,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
     config.extract_opaque && config.extract_fun_decls
     && !Config.wrap_opaque_in_sig
     &&
-    let _, opaque_funs = module_has_opaque_decls ctx in
+    let _, opaque_funs = crate_has_opaque_decls ctx in
     opaque_funs
   in
   if wrap_in_sig then (
@@ -1233,7 +1232,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
 
      (* Check if there are opaque types and functions - in which case we need
       * to split *)
-     let has_opaque_types, has_opaque_funs = module_has_opaque_decls ctx in
+     let has_opaque_types, has_opaque_funs = crate_has_opaque_decls ctx in
      let has_opaque_types = has_opaque_types || !Config.use_state in
 
      (* Extract the types *)
@@ -1302,7 +1301,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
         in
         extract_file template_clauses_config ctx file_info);
 
-     (* Extract the opaque functions, if needed *)
+     (* Extract the opaque declarations, if needed *)
      let opaque_funs_module =
        if has_opaque_funs then (
          (* In the case of Lean we generate a template file *)
@@ -1330,6 +1329,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
            {
              base_gen_config with
              extract_fun_decls = true;
+             extract_globals = true;
              extract_transparent = false;
              extract_opaque = true;
              interface = true;
-- 
cgit v1.2.3


From 515d95d786fed13c300b9e0d7619711ee6aaf971 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 16 Sep 2023 22:50:19 +0200
Subject: Add a strict_names_map in the extraction_ctx

---
 compiler/Translate.ml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 90066163..ebb0de0e 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -986,6 +986,19 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
     mk_formatter_and_names_map trans_ctx crate.name
       variant_concatenate_type_name
   in
+  let strict_names_map =
+    let open ExtractBase in
+    let ids =
+      List.filter
+        (fun (id, _) -> strict_collisions id)
+        (IdMap.bindings names_map.id_to_name)
+    in
+    let is_opaque = false in
+    List.fold_left
+      (* id_to_string: we shouldn't need to use it *)
+        (fun m (id, n) -> names_map_add show_id is_opaque id n m)
+      empty_names_map ids
+  in
 
   (* We need to compute which functions are recursive, in order to know
    * whether we should generate a decrease clause or not. *)
@@ -1041,6 +1054,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       trans_ctx;
       names_map;
       unsafe_names_map = { id_to_name = ExtractBase.IdMap.empty };
+      strict_names_map;
       fmt;
       indent_incr = 2;
       use_opaque_pre = !Config.split_files;
-- 
cgit v1.2.3


From 952c4c964e33eeb6956d84efce3ef1b7575f311f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 17 Sep 2023 00:56:51 +0200
Subject: Fix more issues with the extraction

---
 compiler/Translate.ml | 40 +++++++++++++++++++++++++++++++++-------
 1 file changed, 33 insertions(+), 7 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index ebb0de0e..4a4affea 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -403,6 +403,8 @@ type gen_config = {
   extract_decreases_clauses : bool;
   extract_template_decreases_clauses : bool;
   extract_fun_decls : bool;
+  extract_trait_decls : bool;
+  extract_trait_impls : bool;
   extract_transparent : bool;
       (** If [true], extract the transparent declarations, otherwise ignore. *)
   extract_opaque : bool;
@@ -429,9 +431,22 @@ type gen_config = {
   test_trans_unit_functions : bool;
 }
 
-(** Returns the pair: (has opaque type decls, has opaque fun decls) *)
-let crate_has_opaque_decls (ctx : gen_ctx) : bool * bool =
-  let types, funs = LlbcAstUtils.crate_get_opaque_decls ctx.crate in
+(** Returns the pair: (has opaque type decls, has opaque fun decls).
+
+    [filter_assumed]: if [true], do not consider as opaque the external definitions
+    that we will map to definitions from the standard library.
+ *)
+let crate_has_opaque_decls (ctx : gen_ctx) (filter_assumed : bool) : bool * bool
+    =
+  let types, funs =
+    LlbcAstUtils.crate_get_opaque_decls ctx.crate filter_assumed
+  in
+  log#ldebug
+    (lazy
+      ("Opaque decls:" ^ "\n- types:\n"
+      ^ String.concat ",\n" (List.map T.show_type_decl types)
+      ^ "\n- functions:\n"
+      ^ String.concat ",\n" (List.map A.show_fun_decl funs)));
   (types <> [], funs <> [])
 
 (** Export a type declaration.
@@ -800,8 +815,12 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
         (* Translate *)
         export_functions_group pure_funs
     | Global id -> export_global id
-    | TraitDecl id -> export_trait_decl id
-    | TraitImpl id -> export_trait_impl id
+    | TraitDecl id ->
+        if config.extract_trait_decls && config.extract_transparent then
+          export_trait_decl id
+    | TraitImpl id ->
+        if config.extract_trait_impls && config.extract_transparent then
+          export_trait_impl id
   in
 
   (* If we need to export the state type: we try to export it after we defined
@@ -827,7 +846,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
     config.extract_opaque && config.extract_fun_decls
     && !Config.wrap_opaque_in_sig
     &&
-    let _, opaque_funs = crate_has_opaque_decls ctx in
+    let _, opaque_funs = crate_has_opaque_decls ctx true in
     opaque_funs
   in
   if wrap_in_sig then (
@@ -1235,6 +1254,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
          extract_decreases_clauses = !Config.extract_decreases_clauses;
          extract_template_decreases_clauses = false;
          extract_fun_decls = false;
+         extract_trait_decls = false;
+         extract_trait_impls = false;
          extract_transparent = true;
          extract_opaque = false;
          extract_state_type = false;
@@ -1246,7 +1267,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
 
      (* Check if there are opaque types and functions - in which case we need
       * to split *)
-     let has_opaque_types, has_opaque_funs = crate_has_opaque_decls ctx in
+     let has_opaque_types, has_opaque_funs = crate_has_opaque_decls ctx true in
      let has_opaque_types = has_opaque_types || !Config.use_state in
 
      (* Extract the types *)
@@ -1267,6 +1288,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
        {
          base_gen_config with
          extract_types = true;
+         extract_trait_decls = true;
          extract_opaque = true;
          extract_state_type = !Config.use_state;
          interface = has_opaque_types;
@@ -1343,6 +1365,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
            {
              base_gen_config with
              extract_fun_decls = true;
+             extract_trait_impls = true;
              extract_globals = true;
              extract_transparent = false;
              extract_opaque = true;
@@ -1376,6 +1399,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
        {
          base_gen_config with
          extract_fun_decls = true;
+         extract_trait_impls = true;
          extract_globals = true;
          test_trans_unit_functions = !Config.test_trans_unit_functions;
        }
@@ -1411,6 +1435,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
          extract_template_decreases_clauses =
            !Config.extract_template_decreases_clauses;
          extract_fun_decls = true;
+         extract_trait_decls = true;
+         extract_trait_impls = true;
          extract_transparent = true;
          extract_opaque = true;
          extract_state_type = !Config.use_state;
-- 
cgit v1.2.3


From 47bc2ba74c90c1a29a081b8950022f74408f037e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 17 Sep 2023 05:15:18 +0200
Subject: Merge trans_ctx and decls_ctx

---
 compiler/Translate.ml | 79 +++++++++++----------------------------------------
 1 file changed, 17 insertions(+), 62 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 4a4affea..13e339ea 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -29,34 +29,12 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl)
       ("translate_function_to_symbolics: "
       ^ Print.fun_name_to_string fdef.A.name));
 
-  let {
-    type_context;
-    fun_context;
-    global_context;
-    trait_decls_context;
-    trait_impls_context;
-  } =
-    trans_ctx
-  in
-  let fun_context = { C.fun_decls = fun_context.fun_decls } in
-
-  (* TODO: we should merge trans_ctx and decls_ctx *)
-  let decls_ctx : C.decls_ctx =
-    {
-      C.type_ctx = type_context;
-      fun_ctx = fun_context;
-      global_ctx = global_context;
-      trait_decls_ctx = trait_decls_context;
-      trait_impls_ctx = trait_impls_context;
-    }
-  in
-
   match fdef.body with
   | None -> None
   | Some _ ->
       (* Evaluate *)
       let synthesize = true in
-      let inputs, symb = evaluate_function_symbolic synthesize decls_ctx fdef in
+      let inputs, symb = evaluate_function_symbolic synthesize trans_ctx fdef in
       Some (inputs, Option.get symb)
 
 (** Translate a function, by generating its forward and backward translations.
@@ -74,15 +52,6 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
     (lazy
       ("translate_function_to_pure: " ^ Print.fun_name_to_string fdef.A.name));
 
-  let {
-    type_context;
-    fun_context;
-    global_context;
-    trait_decls_context;
-    trait_impls_context;
-  } =
-    trans_ctx
-  in
   let def_id = fdef.def_id in
 
   (* Compute the symbolic ASTs, if the function is transparent *)
@@ -107,25 +76,25 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       (List.filter_map
          (fun (tid, g) ->
            match g with Charon.GAst.NonRec _ -> None | Rec _ -> Some tid)
-         (T.TypeDeclId.Map.bindings trans_ctx.type_context.type_decls_groups))
+         (T.TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups))
   in
   let type_context =
     {
-      SymbolicToPure.type_infos = type_context.type_infos;
-      llbc_type_decls = type_context.type_decls;
+      SymbolicToPure.type_infos = trans_ctx.type_ctx.type_infos;
+      llbc_type_decls = trans_ctx.type_ctx.type_decls;
       type_decls = pure_type_decls;
       recursive_decls = recursive_type_decls;
     }
   in
   let fun_context =
     {
-      SymbolicToPure.llbc_fun_decls = fun_context.fun_decls;
+      SymbolicToPure.llbc_fun_decls = trans_ctx.fun_ctx.fun_decls;
       fun_sigs;
-      fun_infos = fun_context.fun_infos;
+      fun_infos = trans_ctx.fun_ctx.fun_infos;
     }
   in
   let global_context =
-    { SymbolicToPure.llbc_global_decls = global_context.global_decls }
+    { SymbolicToPure.llbc_global_decls = trans_ctx.global_ctx.global_decls }
   in
 
   (* Compute the set of loops, and find better ids for them (starting at 0).
@@ -173,8 +142,8 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       type_context;
       fun_context;
       global_context;
-      trait_decls_ctx = trait_decls_context.trait_decls;
-      trait_impls_ctx = trait_impls_context.trait_impls;
+      trait_decls_ctx = trans_ctx.trait_decls_ctx.trait_decls;
+      trait_impls_ctx = trans_ctx.trait_impls_ctx.trait_impls;
       fun_decl = fdef;
       forward_inputs = [];
       (* Empty for now *)
@@ -311,22 +280,8 @@ let translate_crate_to_pure (crate : A.crate) :
   (* Debug *)
   log#ldebug (lazy "translate_crate_to_pure");
 
-  (* Compute the type and function contexts *)
-  let decls_ctx = compute_contexts crate in
-  let fun_infos =
-    FA.analyze_module crate decls_ctx.fun_ctx.C.fun_decls
-      decls_ctx.global_ctx.C.global_decls !Config.use_state
-  in
-  let fun_context = { fun_decls = decls_ctx.fun_ctx.fun_decls; fun_infos } in
-  let trans_ctx =
-    {
-      type_context = decls_ctx.type_ctx;
-      fun_context;
-      global_context = decls_ctx.global_ctx;
-      trait_decls_context = decls_ctx.trait_decls_ctx;
-      trait_impls_context = decls_ctx.trait_impls_ctx;
-    }
-  in
+  (* Compute the translation context *)
+  let trans_ctx = compute_contexts crate in
 
   (* Translate all the type definitions *)
   let type_decls =
@@ -362,8 +317,8 @@ let translate_crate_to_pure (crate : A.crate) :
   in
   let sigs = List.append assumed_sigs local_sigs in
   let fun_sigs =
-    SymbolicToPure.translate_fun_signatures fun_context.fun_infos
-      decls_ctx.type_ctx.type_infos sigs
+    SymbolicToPure.translate_fun_signatures trans_ctx.fun_ctx.fun_infos
+      trans_ctx.type_ctx.type_infos sigs
   in
 
   (* Translate all the *transparent* functions *)
@@ -374,18 +329,18 @@ let translate_crate_to_pure (crate : A.crate) :
   in
 
   (* Translate the trait declarations *)
-  let type_infos = trans_ctx.type_context.type_infos in
+  let type_infos = trans_ctx.type_ctx.type_infos in
   let trait_decls =
     List.map
       (SymbolicToPure.translate_trait_decl type_infos)
-      (T.TraitDeclId.Map.values trans_ctx.trait_decls_context.trait_decls)
+      (T.TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
   in
 
   (* Translate the trait implementations *)
   let trait_impls =
     List.map
       (SymbolicToPure.translate_trait_impl type_infos)
-      (T.TraitImplId.Map.values trans_ctx.trait_impls_context.trait_impls)
+      (T.TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
   in
 
   (* Apply the micro-passes *)
@@ -554,7 +509,7 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
  *)
 let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     (id : A.GlobalDeclId.id) : unit =
-  let global_decls = ctx.trans_ctx.global_context.global_decls in
+  let global_decls = ctx.trans_ctx.global_ctx.global_decls in
   let global = A.GlobalDeclId.Map.find id global_decls in
   let trans = A.FunDeclId.Map.find global.body_id ctx.trans_funs in
   assert (trans.fwd.loops = []);
-- 
cgit v1.2.3


From 80728093c432ba15eace9d6ce1cc9e3c56a80ff7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 17 Sep 2023 05:37:56 +0200
Subject: Make minor modifications

---
 compiler/Translate.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 13e339ea..e69abee1 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -316,10 +316,7 @@ let translate_crate_to_pure (crate : A.crate) :
       (A.FunDeclId.Map.values crate.functions)
   in
   let sigs = List.append assumed_sigs local_sigs in
-  let fun_sigs =
-    SymbolicToPure.translate_fun_signatures trans_ctx.fun_ctx.fun_infos
-      trans_ctx.type_ctx.type_infos sigs
-  in
+  let fun_sigs = SymbolicToPure.translate_fun_signatures trans_ctx sigs in
 
   (* Translate all the *transparent* functions *)
   let pure_translations =
-- 
cgit v1.2.3


From f11d5186b467df318f7c09eedf8b5629c165b453 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 20 Oct 2023 15:05:00 +0200
Subject: Start updating to handle function pointers

---
 compiler/Translate.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index e69abee1..8e01c869 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -61,7 +61,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
 
   (* Initialize the context *)
   let forward_sig =
-    RegularFunIdNotLoopMap.find (A.Regular def_id, None) fun_sigs
+    RegularFunIdNotLoopMap.find (E.Regular def_id, None) fun_sigs
   in
   let sv_to_var = V.SymbolicValueId.Map.empty in
   let var_counter = Pure.VarId.generator_zero in
@@ -200,7 +200,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
         (* Initialize the context - note that the ret_ty is not really
          * useful as we don't translate a body *)
         let backward_sg =
-          RegularFunIdNotLoopMap.find (A.Regular def_id, Some back_id) fun_sigs
+          RegularFunIdNotLoopMap.find (Regular def_id, Some back_id) fun_sigs
         in
         let ctx = { ctx with bid = Some back_id; sg = backward_sg.sg } in
 
@@ -211,7 +211,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
            variables required by the backward function.
         *)
         let backward_sg =
-          RegularFunIdNotLoopMap.find (A.Regular def_id, Some back_id) fun_sigs
+          RegularFunIdNotLoopMap.find (Regular def_id, Some back_id) fun_sigs
         in
         (* We need to ignore the forward inputs, and the state input (if there is) *)
         let backward_inputs =
@@ -298,7 +298,7 @@ let translate_crate_to_pure (crate : A.crate) :
   let assumed_sigs =
     List.map
       (fun (id, sg, _, _) ->
-        (A.Assumed id, List.map (fun _ -> None) (sg : A.fun_sig).inputs, sg))
+        (E.Assumed id, List.map (fun _ -> None) (sg : A.fun_sig).inputs, sg))
       Assumed.assumed_infos
   in
   let local_sigs =
@@ -312,7 +312,7 @@ let translate_crate_to_pure (crate : A.crate) :
                 (fun (v : A.var) -> v.name)
                 (LlbcAstUtils.fun_body_get_input_vars body)
         in
-        (A.Regular fdef.def_id, input_names, fdef.signature))
+        (E.Regular fdef.def_id, input_names, fdef.signature))
       (A.FunDeclId.Map.values crate.functions)
   in
   let sigs = List.append assumed_sigs local_sigs in
-- 
cgit v1.2.3


From 838cc86cb2efc8fb64a94a94b58b82d66844e7e4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 23 Oct 2023 13:47:39 +0200
Subject: Remove some assumed types and add more support for builtin
 definitions

---
 compiler/Translate.ml | 107 ++++++++++++++++++++++++++++++--------------------
 1 file changed, 65 insertions(+), 42 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 8e01c869..15297770 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -297,9 +297,11 @@ let translate_crate_to_pure (crate : A.crate) :
   (* Translate all the function *signatures* *)
   let assumed_sigs =
     List.map
-      (fun (id, sg, _, _) ->
-        (E.Assumed id, List.map (fun _ -> None) (sg : A.fun_sig).inputs, sg))
-      Assumed.assumed_infos
+      (fun (info : Assumed.assumed_fun_info) ->
+        ( E.Assumed info.fun_id,
+          List.map (fun _ -> None) info.fun_sig.inputs,
+          info.fun_sig ))
+      Assumed.assumed_fun_infos
   in
   let local_sigs =
     List.map
@@ -425,11 +427,15 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
         (true, kind)
   in
   (* Extract, if the config instructs to do so (depending on whether the type
-   * is opaque or not) *)
-  if
+     is opaque or not). Remark: we don't check if the definitions are builtin
+     here but in the function [export_types_group]: the reason is that if one
+     definition in the group is builtin, then we must check that all the
+     definitions are marked builtin *)
+  let extract =
     (is_opaque && config.extract_opaque)
     || ((not is_opaque) && config.extract_transparent)
-  then (
+  in
+  if extract then (
     if extract_decl then
       Extract.extract_type_decl ctx fmt type_decl_group kind def;
     if extract_extra_info then
@@ -464,41 +470,58 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
     List.map (fun id -> Pure.TypeDeclId.Map.find id ctx.trans_types) ids
   in
 
-  (* Extract the type declarations.
-
-     Because some declaration groups are delimited, we wrap the declarations
-     between [{start,end}_type_decl_group].
+  (* Check if the definition are builtin - if yes they must be ignored.
+     Note that if one definition in the group is builtin, then all the
+     definitions must be builtin *)
+  let builtin =
+    let open ExtractBuiltin in
+    let types_map = builtin_types_map () in
+    List.map
+      (fun (def : Pure.type_decl) ->
+        let sname = name_to_simple_name def.name in
+        SimpleNameMap.find_opt sname types_map <> None)
+      defs
+  in
 
-     Ex.:
-     ====
-     When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate
-     the [Datatype] and [End] delimiters in the snippet of code below:
+  if List.exists (fun b -> b) builtin then
+    (* Sanity check *)
+    assert (List.for_all (fun b -> b) builtin)
+  else (
+    (* Extract the type declarations.
+
+       Because some declaration groups are delimited, we wrap the declarations
+       between [{start,end}_type_decl_group].
+
+       Ex.:
+       ====
+       When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate
+       the [Datatype] and [End] delimiters in the snippet of code below:
+
+       {[
+         Datatype:
+           tree =
+             TLeaf 'a
+           | TNode node ;
+
+           node =
+             Node (tree list)
+         End
+       ]}
+    *)
+    Extract.start_type_decl_group ctx fmt is_rec defs;
+    List.iteri
+      (fun i def ->
+        let kind = kind_from_index i in
+        export_type_decl kind def)
+      defs;
+    Extract.end_type_decl_group fmt is_rec defs;
 
-     {[
-       Datatype:
-         tree =
-           TLeaf 'a
-         | TNode node ;
-
-         node =
-           Node (tree list)
-       End
-     ]}
-  *)
-  Extract.start_type_decl_group ctx fmt is_rec defs;
-  List.iteri
-    (fun i def ->
-      let kind = kind_from_index i in
-      export_type_decl kind def)
-    defs;
-  Extract.end_type_decl_group fmt is_rec defs;
-
-  (* Export the extra information (ex.: [Arguments] instructions in Coq) *)
-  List.iteri
-    (fun i def ->
-      let kind = kind_from_index i in
-      export_type_extra_info kind def)
-    defs
+    (* Export the extra information (ex.: [Arguments] instructions in Coq) *)
+    List.iteri
+      (fun i def ->
+        let kind = kind_from_index i in
+        export_type_extra_info kind def)
+      defs)
 
 (** Export a global declaration.
 
@@ -520,12 +543,12 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     && (((not is_opaque) && config.extract_transparent)
        || (is_opaque && config.extract_opaque))
   in
-  (* Check if it is an assumed global - if yes, we ignore it because we
+  (* Check if it is a builtin global - if yes, we ignore it because we
      map the definition to one in the standard library *)
-  let open ExtractAssumed in
+  let open ExtractBuiltin in
   let sname = name_to_simple_name global.name in
   let extract =
-    extract && SimpleNameMap.find_opt sname assumed_globals_map = None
+    extract && SimpleNameMap.find_opt sname builtin_globals_map = None
   in
   if extract then
     (* We don't wrap global declaration groups between calls to functions
-- 
cgit v1.2.3


From c486bd0675f489c5ac917749a68e2c71b55041ae Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 23 Oct 2023 17:29:15 +0200
Subject: Make progress on handling the builtins

---
 compiler/Translate.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 15297770..0871a305 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -731,8 +731,13 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
 let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
     (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) : unit =
   let trait_decl = T.TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in
-  let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
-  Extract.extract_trait_decl ctx fmt trait_decl
+  (* Check if the trait declaration is builtin, in which case we ignore it *)
+  let open ExtractBuiltin in
+  let sname = name_to_simple_name trait_decl.name in
+  if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then
+    let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
+    Extract.extract_trait_decl ctx fmt trait_decl
+  else ()
 
 (** Export a trait implementation. *)
 let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
-- 
cgit v1.2.3


From 63107911c16a9991f7d5cf8c6df621318a03ca3b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 14:32:38 +0200
Subject: Fix various issues with the builtins

---
 compiler/Translate.ml | 158 ++++++++++++++++++++++++++++----------------------
 1 file changed, 90 insertions(+), 68 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 0871a305..95252b61 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -654,78 +654,100 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config)
  *)
 let export_functions_group (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) (pure_ls : pure_fun_translation list) : unit =
-  (* Utility to check a function has a decrease clause *)
-  let has_decreases_clause (def : Pure.fun_decl) : bool =
-    PureUtils.FunLoopIdSet.mem (def.def_id, def.loop_id)
-      ctx.functions_with_decreases_clause
+  (* Check if the definition are builtin - if yes they must be ignored.
+     Note that if one definition in the group is builtin, then all the
+     definitions must be builtin *)
+  let builtin =
+    let open ExtractBuiltin in
+    let funs_map = builtin_funs_map () in
+    List.map
+      (fun (trans : pure_fun_translation) ->
+        let sname = name_to_simple_name trans.fwd.f.basename in
+        SimpleNameMap.find_opt sname funs_map <> None)
+      pure_ls
   in
 
-  (* Extract the decrease clauses template bodies *)
-  if config.extract_template_decreases_clauses then
-    List.iter
-      (fun { fwd; _ } ->
-        (* We only generate decreases clauses for the forward functions, because
-           the termination argument should only depend on the forward inputs.
-           The backward functions thus use the same decreases clauses as the
-           forward function.
-
-           Rem.: we might filter backward functions in {!PureMicroPasses}, but
-           we don't remove forward functions. Instead, we remember if we should
-           filter those functions at extraction time with a boolean (see the
-           type of the [pure_ls] input parameter).
-        *)
-        let extract_decrease decl =
-          let has_decr_clause = has_decreases_clause decl in
-          if has_decr_clause then
-            match !Config.backend with
-            | Lean ->
-                Extract.extract_template_lean_termination_and_decreasing ctx fmt
-                  decl
-            | FStar ->
-                Extract.extract_template_fstar_decreases_clause ctx fmt decl
-            | Coq ->
-                raise (Failure "Coq doesn't have decreases/termination clauses")
-            | HOL4 ->
-                raise
-                  (Failure "HOL4 doesn't have decreases/termination clauses")
-        in
-        extract_decrease fwd.f;
-        List.iter extract_decrease fwd.loops)
-      pure_ls;
-
-  (* Concatenate the function definitions, filtering the useless forward
-   * functions. *)
-  let decls =
-    List.concat
-      (List.map
-         (fun { keep_fwd; fwd; backs } ->
-           let fwd = if keep_fwd then List.append fwd.loops [ fwd.f ] else [] in
-           let backs : Pure.fun_decl list =
-             List.concat
-               (List.map (fun back -> List.append back.loops [ back.f ]) backs)
-           in
-           List.append fwd backs)
-         pure_ls)
-  in
+  if List.exists (fun b -> b) builtin then
+    (* Sanity check *)
+    assert (List.for_all (fun b -> b) builtin)
+  else
+    (* Utility to check a function has a decrease clause *)
+    let has_decreases_clause (def : Pure.fun_decl) : bool =
+      PureUtils.FunLoopIdSet.mem (def.def_id, def.loop_id)
+        ctx.functions_with_decreases_clause
+    in
+
+    (* Extract the decrease clauses template bodies *)
+    if config.extract_template_decreases_clauses then
+      List.iter
+        (fun { fwd; _ } ->
+          (* We only generate decreases clauses for the forward functions, because
+             the termination argument should only depend on the forward inputs.
+             The backward functions thus use the same decreases clauses as the
+             forward function.
+
+             Rem.: we might filter backward functions in {!PureMicroPasses}, but
+             we don't remove forward functions. Instead, we remember if we should
+             filter those functions at extraction time with a boolean (see the
+             type of the [pure_ls] input parameter).
+          *)
+          let extract_decrease decl =
+            let has_decr_clause = has_decreases_clause decl in
+            if has_decr_clause then
+              match !Config.backend with
+              | Lean ->
+                  Extract.extract_template_lean_termination_and_decreasing ctx
+                    fmt decl
+              | FStar ->
+                  Extract.extract_template_fstar_decreases_clause ctx fmt decl
+              | Coq ->
+                  raise
+                    (Failure "Coq doesn't have decreases/termination clauses")
+              | HOL4 ->
+                  raise
+                    (Failure "HOL4 doesn't have decreases/termination clauses")
+          in
+          extract_decrease fwd.f;
+          List.iter extract_decrease fwd.loops)
+        pure_ls;
+
+    (* Concatenate the function definitions, filtering the useless forward
+     * functions. *)
+    let decls =
+      List.concat
+        (List.map
+           (fun { keep_fwd; fwd; backs } ->
+             let fwd =
+               if keep_fwd then List.append fwd.loops [ fwd.f ] else []
+             in
+             let backs : Pure.fun_decl list =
+               List.concat
+                 (List.map
+                    (fun back -> List.append back.loops [ back.f ])
+                    backs)
+             in
+             List.append fwd backs)
+           pure_ls)
+    in
 
-  (* Extract the function definitions *)
-  (if config.extract_fun_decls then
-     (* Group the mutually recursive definitions *)
-     let subgroups = ReorderDecls.group_reorder_fun_decls decls in
+    (* Extract the function definitions *)
+    (if config.extract_fun_decls then
+       (* Group the mutually recursive definitions *)
+       let subgroups = ReorderDecls.group_reorder_fun_decls decls in
 
-     (* Extract the subgroups *)
-     let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit =
-       export_functions_group_scc fmt config ctx is_rec decls
-     in
-     List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups);
-
-  (* Insert unit tests if necessary *)
-  if config.test_trans_unit_functions then
-    List.iter
-      (fun trans ->
-        if trans.keep_fwd then
-          Extract.extract_unit_test_if_unit_fun ctx fmt trans.fwd.f)
-      pure_ls
+       (* Extract the subgroups *)
+       let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit =
+         export_functions_group_scc fmt config ctx is_rec decls
+       in
+       List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups);
+
+    (* Insert unit tests if necessary *)
+    if config.test_trans_unit_functions then
+      List.iter
+        (fun trans ->
+          if trans.keep_fwd then
+            Extract.extract_unit_test_if_unit_fun ctx fmt trans.fwd.f)
+        pure_ls
 
 (** Export a trait declaration. *)
 let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
-- 
cgit v1.2.3


From be70eed487b507dc002660a4c891397003165e75 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 15:01:55 +0200
Subject: Add support for builtin trait implementations

---
 compiler/Translate.ml | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 95252b61..74a8537f 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -764,8 +764,23 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
 (** Export a trait implementation. *)
 let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
     (ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit =
+  (* Lookup the definition *)
   let trait_impl = T.TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in
-  Extract.extract_trait_impl ctx fmt trait_impl
+  let trait_decl =
+    Pure.TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id
+      ctx.trans_trait_decls
+  in
+  (* Check if the trait implementation is builtin *)
+  let builtin_info =
+    let open ExtractBuiltin in
+    let type_sname = name_to_simple_name trait_impl.name in
+    let trait_sname = name_to_simple_name trait_decl.name in
+    SimpleNamePairMap.find_opt (type_sname, trait_sname)
+      (builtin_trait_impls_map ())
+  in
+  match builtin_info with
+  | None -> Extract.extract_trait_impl ctx fmt trait_impl
+  | Some _ -> ()
 
 (** A generic utility to generate the extracted definitions: as we may want to
     split the definitions between different files (or not), we can control
-- 
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/Translate.ml | 34 ++--------------------------------
 1 file changed, 2 insertions(+), 32 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 74a8537f..b3269aa2 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -851,37 +851,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
   if config.extract_state_type && config.extract_fun_decls then
     export_state_type ();
 
-  (* Obsolete: (TODO: remove) For Lean we parameterize the entire development by a section
-     variable called opaque_defs, of type OpaqueDefs. The code below emits the type
-     definition for OpaqueDefs, which is a structure, in which each field is one of the
-     functions marked as Opaque. We emit the `structure ...` bit here, then rely on
-     `extract_fun_decl` to be aware of this, and skip the keyword (e.g. "axiom" or "val")
-     so as to generate valid syntax for records.
-
-     We also generate such a structure only if there actually are opaque definitions. *)
-  let wrap_in_sig =
-    config.extract_opaque && config.extract_fun_decls
-    && !Config.wrap_opaque_in_sig
-    &&
-    let _, opaque_funs = crate_has_opaque_decls ctx true in
-    opaque_funs
-  in
-  if wrap_in_sig then (
-    (* We change the name of the structure depending on whether we *only*
-       extract opaque definitions, or if we extract all definitions *)
-    let struct_name =
-      if config.extract_transparent then "Definitions" else "OpaqueDefs"
-    in
-    Format.pp_print_break fmt 0 0;
-    Format.pp_open_vbox fmt ctx.indent_incr;
-    Format.pp_print_string fmt ("structure " ^ struct_name ^ " where");
-    Format.pp_print_break fmt 0 0);
   List.iter export_decl_group ctx.crate.declarations;
 
   if config.extract_state_type && not config.extract_fun_decls then
-    export_state_type ();
-
-  if wrap_in_sig then Format.pp_close_box fmt ()
+    export_state_type ()
 
 type extract_file_info = {
   filename : string;
@@ -1029,10 +1002,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
         (fun (id, _) -> strict_collisions id)
         (IdMap.bindings names_map.id_to_name)
     in
-    let is_opaque = false in
     List.fold_left
       (* id_to_string: we shouldn't need to use it *)
-        (fun m (id, n) -> names_map_add show_id is_opaque id n m)
+        (fun m (id, n) -> names_map_add show_id id n m)
       empty_names_map ids
   in
 
@@ -1093,7 +1065,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       strict_names_map;
       fmt;
       indent_incr = 2;
-      use_opaque_pre = !Config.split_files;
       use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
       fun_name_info = PureUtils.RegularFunIdMap.empty;
       trait_decl_id = None (* None by default *);
@@ -1389,7 +1360,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
              interface = true;
            }
          in
-         let ctx = { ctx with use_opaque_pre = false } in
          let file_info =
            {
              filename = opaque_filename;
-- 
cgit v1.2.3


From 9ddd174959970f87658191034b70d0cfa02ff451 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 15:49:54 +0200
Subject: Filter some type arguments for the builtin types/functions

---
 compiler/Translate.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index b3269aa2..35dff9e6 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -1074,6 +1074,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       trans_types;
       trans_funs;
       functions_with_decreases_clause = rec_functions;
+      types_filter_type_args_map = Pure.TypeDeclId.Map.empty;
+      funs_filter_type_args_map = Pure.FunDeclId.Map.empty;
     }
   in
 
-- 
cgit v1.2.3


From e3cb3646bbe3d50240aa0bf4763f8e816fb9a706 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 15:36:06 +0200
Subject: Fix some issues at extraction and add builtins

---
 compiler/Translate.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 35dff9e6..019a5c35 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -390,10 +390,10 @@ type gen_config = {
     [filter_assumed]: if [true], do not consider as opaque the external definitions
     that we will map to definitions from the standard library.
  *)
-let crate_has_opaque_decls (ctx : gen_ctx) (filter_assumed : bool) : bool * bool
-    =
+let crate_has_opaque_non_builtin_decls (ctx : gen_ctx) (filter_assumed : bool) :
+    bool * bool =
   let types, funs =
-    LlbcAstUtils.crate_get_opaque_decls ctx.crate filter_assumed
+    LlbcAstUtils.crate_get_opaque_non_builtin_decls ctx.crate filter_assumed
   in
   log#ldebug
     (lazy
@@ -1257,7 +1257,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
 
      (* Check if there are opaque types and functions - in which case we need
       * to split *)
-     let has_opaque_types, has_opaque_funs = crate_has_opaque_decls ctx true in
+     let has_opaque_types, has_opaque_funs =
+       crate_has_opaque_non_builtin_decls ctx true
+     in
      let has_opaque_types = has_opaque_types || !Config.use_state in
 
      (* Extract the types *)
-- 
cgit v1.2.3


From 81b7a7d706bc1a0f2f57bc254a8af158039a10cf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 18:44:28 +0200
Subject: Make the hashmap files typecheck again in Lean

---
 compiler/Translate.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 019a5c35..c5ac4e96 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -1076,6 +1076,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       functions_with_decreases_clause = rec_functions;
       types_filter_type_args_map = Pure.TypeDeclId.Map.empty;
       funs_filter_type_args_map = Pure.FunDeclId.Map.empty;
+      trait_impls_filter_type_args_map = Pure.TraitImplId.Map.empty;
     }
   in
 
-- 
cgit v1.2.3


From ca24c351f97a3f8989a6866de0868ef54241b194 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 26 Oct 2023 12:07:50 +0200
Subject: Make progress on fixing the extraction for Lean

---
 compiler/Translate.ml | 21 +++------------------
 1 file changed, 3 insertions(+), 18 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index c5ac4e96..cb23198a 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -990,23 +990,10 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   in
   (* Initialize the names map (we insert the names of the "primitives"
      declarations, and insert the names of the local declarations later) *)
-  let mk_formatter_and_names_map = Extract.mk_formatter_and_names_map in
-  let fmt, names_map =
-    mk_formatter_and_names_map trans_ctx crate.name
+  let fmt, names_maps =
+    Extract.mk_formatter_and_names_maps trans_ctx crate.name
       variant_concatenate_type_name
   in
-  let strict_names_map =
-    let open ExtractBase in
-    let ids =
-      List.filter
-        (fun (id, _) -> strict_collisions id)
-        (IdMap.bindings names_map.id_to_name)
-    in
-    List.fold_left
-      (* id_to_string: we shouldn't need to use it *)
-        (fun m (id, n) -> names_map_add show_id id n m)
-      empty_names_map ids
-  in
 
   (* We need to compute which functions are recursive, in order to know
    * whether we should generate a decrease clause or not. *)
@@ -1060,9 +1047,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
     {
       ExtractBase.crate;
       trans_ctx;
-      names_map;
-      unsafe_names_map = { id_to_name = ExtractBase.IdMap.empty };
-      strict_names_map;
+      names_maps;
       fmt;
       indent_incr = 2;
       use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
-- 
cgit v1.2.3


From 3a22c56e026ee4488bc5e2d16d2066853ae7ccb9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 16:22:09 +0100
Subject: Make the traits work for Coq

---
 compiler/Translate.ml | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index cb23198a..a3d96023 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -751,14 +751,17 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
 
 (** Export a trait declaration. *)
 let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
-    (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) : unit =
+    (ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) (extract_decl : bool)
+    (extract_extra_info : bool) : unit =
   let trait_decl = T.TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in
   (* Check if the trait declaration is builtin, in which case we ignore it *)
   let open ExtractBuiltin in
   let sname = name_to_simple_name trait_decl.name in
-  if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then
+  if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then (
     let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
-    Extract.extract_trait_decl ctx fmt trait_decl
+    if extract_decl then Extract.extract_trait_decl ctx fmt trait_decl;
+    if extract_extra_info then
+      Extract.extract_trait_decl_extra_info ctx fmt trait_decl)
   else ()
 
 (** Export a trait implementation. *)
@@ -796,7 +799,12 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
   let export_functions_group = export_functions_group fmt config ctx in
   let export_global = export_global fmt config ctx in
   let export_types_group = export_types_group fmt config ctx in
-  let export_trait_decl = export_trait_decl fmt config ctx in
+  let export_trait_decl_group id =
+    export_trait_decl fmt config ctx id true false
+  in
+  let export_trait_decl_group_extra_info id =
+    export_trait_decl fmt config ctx id false true
+  in
   let export_trait_impl = export_trait_impl fmt config ctx in
 
   let export_state_type () : unit =
@@ -833,8 +841,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
         export_functions_group pure_funs
     | Global id -> export_global id
     | TraitDecl id ->
-        if config.extract_trait_decls && config.extract_transparent then
-          export_trait_decl id
+        (* TODO: update to extract groups *)
+        if config.extract_trait_decls && config.extract_transparent then (
+          export_trait_decl_group id;
+          export_trait_decl_group_extra_info id)
     | TraitImpl id ->
         if config.extract_trait_impls && config.extract_transparent then
           export_trait_impl id
-- 
cgit v1.2.3