From 26c25bf375742cf4d5a0ab160b9646e90c067f18 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 18 Aug 2023 10:27:55 +0200
Subject: Update following the introduction of ConstantExpr

---
 compiler/PureMicroPasses.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index b6025df4..65dc7ff2 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -376,8 +376,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     let ty = e.ty in
     let ctx, e =
       match e.e with
-      | Var _ -> (* Nothing to do *) (ctx, e.e)
-      | Const _ -> (* Nothing to do *) (ctx, e.e)
+      | Var _ | CVar _ | Const _ -> (* Nothing to do *) (ctx, e.e)
       | App (app, arg) ->
           let ctx, app = update_texpression app ctx in
           let ctx, arg = update_texpression arg ctx in
@@ -834,7 +833,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
 
       method! visit_texpression env e =
         match e.e with
-        | Var _ | Const _ -> fun _ -> false
+        | Var _ | CVar _ | Const _ -> fun _ -> false
         | StructUpdate _ ->
             (* There shouldn't be monadic calls in structure updates - also
                note that by returning [false] we are conservative: we might
@@ -930,7 +929,7 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
 
       method! visit_expression env e =
         match e with
-        | Var _ | Const _ | App _ | Qualif _
+        | Var _ | CVar _ | Const _ | App _ | Qualif _
         | Switch (_, _)
         | Meta (_, _)
         | StructUpdate _ | Abs _ ->
-- 
cgit v1.2.3


From a9c256fe95523842a1ff025e73f6e9ce7c2db38a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 18 Aug 2023 10:44:01 +0200
Subject: Add tests which use const generics as values

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

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 65dc7ff2..b2f3bb9f 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -681,8 +681,8 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
               | _ -> false
             in
             (* And either:
-             * 2.1 the right-expression is a variable or a global *)
-            let var_or_global = is_var re || is_global re in
+             * 2.1 the right-expression is a variable, a global or a const generic var *)
+            let var_or_global = is_var re || is_cvar re || is_global re in
             (* Or:
              * 2.2 the right-expression is a constant value, an ADT value,
              *     a projection or a primitive function call *and* the flag
-- 
cgit v1.2.3


From aed317881d3083bba6a2cf154289486ef47ddf85 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 1 Sep 2023 16:57:07 +0200
Subject: Update PureMicroPasses

---
 compiler/PureMicroPasses.ml | 61 +++++++++++++--------------------------------
 1 file changed, 18 insertions(+), 43 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index b2f3bb9f..45e4ea98 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -583,8 +583,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
             | Qualif
                 {
                   id = AdtCons { adt_id = AdtId adt_id; variant_id = None };
-                  type_args = _;
-                  const_generic_args = _;
+                  generics = _;
                 } ->
                 (* Lookup the def *)
                 let decl =
@@ -767,9 +766,9 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
  *)
 let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
     (id0 : A.fun_id) (lp_id0 : LoopId.id option)
-    (rg_id0 : T.RegionGroupId.id option) (tys0 : ty list)
+    (rg_id0 : T.RegionGroupId.id option) (generics0 : generic_args)
     (args0 : texpression list) (e : texpression) : bool =
-  let check_call (fun_id1 : fun_or_op_id) (tys1 : ty list)
+  let check_call (fun_id1 : fun_or_op_id) (generics1 : generic_args)
       (args1 : texpression list) : bool =
     (* Check the fun_ids, to see if call1's function is a child of call0's function *)
     match fun_id1 with
@@ -816,8 +815,8 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
             let input_eq (v0, v1) =
               PureUtils.remove_meta v0 = PureUtils.remove_meta v1
             in
-            (* Compare the input types and the prefix of the input arguments *)
-            tys0 = tys1 && List.for_all input_eq args
+            (* Compare the generics and the prefix of the input arguments *)
+            generics0 = generics1 && List.for_all input_eq args
           else (* Not a child *)
             false
         else (* Not the same function *)
@@ -843,8 +842,8 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
         | Let (_, _, re, e) -> (
             match opt_destruct_function_call re with
             | None -> fun () -> self#visit_texpression env e ()
-            | Some (func1, tys1, args1) ->
-                let call_is_child = check_call func1 tys1 args1 in
+            | Some (func1, generics1, args1) ->
+                let call_is_child = check_call func1 generics1 args1 in
                 if call_is_child then fun () -> true
                 else fun () -> self#visit_texpression env e ())
         | App _ -> (
@@ -1085,8 +1084,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
             | Qualif
                 {
                   id = AdtCons { adt_id = AdtId adt_id; variant_id = None };
-                  type_args;
-                  const_generic_args;
+                  generics;
                 } ->
                 (* This is a struct *)
                 (* Retrieve the definiton, to find how many fields there are *)
@@ -1107,7 +1105,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                    * [x.field] for some variable [x], and where the projection
                    * is for the proper ADT *)
                   let to_var_proj (i : int) (arg : texpression) :
-                      (ty list * const_generic list * var_id) option =
+                      (generic_args * var_id) option =
                     match arg.e with
                     | App (proj, x) -> (
                         match (proj.e, x.e) with
@@ -1115,16 +1113,14 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                               {
                                 id =
                                   Proj { adt_id = AdtId proj_adt_id; field_id };
-                                type_args = proj_type_args;
-                                const_generic_args = proj_const_generic_args;
+                                generics = proj_generics;
                               },
                             Var v ) ->
                             (* We check that this is the proper ADT, and the proper field *)
                             if
                               proj_adt_id = adt_id
                               && FieldId.to_int field_id = i
-                            then
-                              Some (proj_type_args, proj_const_generic_args, v)
+                            then Some (proj_generics, v)
                             else None
                         | _ -> None)
                     | _ -> None
@@ -1135,14 +1131,13 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                   if List.length args = num_fields then
                     (* Check that this is the same variable we project from -
                      * note that we checked above that there is at least one field *)
-                    let (_, _, x), end_args = Collections.List.pop args in
-                    if List.for_all (fun (_, _, y) -> y = x) end_args then (
+                    let (_, x), end_args = Collections.List.pop args in
+                    if List.for_all (fun (_, y) -> y = x) end_args then (
                       (* We can substitute *)
                       (* Sanity check: all types correct *)
                       assert (
                         List.for_all
-                          (fun (tys, cgs, _) ->
-                            tys = type_args && cgs = const_generic_args)
+                          (fun (generics1, _) -> generics1 = generics)
                           args);
                       { e with e = Var x })
                     else super#visit_texpression env e
@@ -1161,8 +1156,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                   | ( Qualif
                         {
                           id = Proj { adt_id = AdtId proj_adt_id; field_id };
-                          type_args = _;
-                          const_generic_args = _;
+                          generics = _;
                         },
                       Var v ) ->
                       (* We check that this is the proper ADT, and the proper field *)
@@ -1360,8 +1354,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
 
             let loop_sig =
               {
-                type_params = fun_sig.type_params;
-                const_generic_params = fun_sig.const_generic_params;
+                generics = fun_sig.generics;
                 inputs = inputs_tys;
                 output;
                 doutputs;
@@ -2142,16 +2135,7 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
           let num_filtered =
             List.length (List.filter (fun b -> not b) used_info)
           in
-          let {
-            type_params;
-            const_generic_params;
-            inputs;
-            output;
-            doutputs;
-            info;
-          } =
-            decl.signature
-          in
+          let { generics; inputs; output; doutputs; info } = decl.signature in
           let {
             has_fuel;
             num_fwd_inputs_with_fuel_no_state;
@@ -2177,16 +2161,7 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
               effect_info;
             }
           in
-          let signature =
-            {
-              type_params;
-              const_generic_params;
-              inputs;
-              output;
-              doutputs;
-              info;
-            }
-          in
+          let signature = { generics; inputs; output; doutputs; info } in
 
           { decl with signature }
     in
-- 
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/PureMicroPasses.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 45e4ea98..93609695 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1355,6 +1355,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
             let loop_sig =
               {
                 generics = fun_sig.generics;
+                preds = fun_sig.preds;
                 inputs = inputs_tys;
                 output;
                 doutputs;
@@ -1419,6 +1420,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
             let loop_def =
               {
                 def_id = def.def_id;
+                kind = def.kind;
                 num_loops;
                 loop_id = Some loop.loop_id;
                 back_id = def.back_id;
@@ -2135,7 +2137,9 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
           let num_filtered =
             List.length (List.filter (fun b -> not b) used_info)
           in
-          let { generics; inputs; output; doutputs; info } = decl.signature in
+          let { generics; preds; inputs; output; doutputs; info } =
+            decl.signature
+          in
           let {
             has_fuel;
             num_fwd_inputs_with_fuel_no_state;
@@ -2161,7 +2165,7 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
               effect_info;
             }
           in
-          let signature = { generics; inputs; output; doutputs; info } in
+          let signature = { generics; preds; inputs; output; doutputs; info } in
 
           { decl with signature }
     in
-- 
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/PureMicroPasses.ml | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 93609695..72e3d05e 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1461,7 +1461,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
     altogether.
   *)
 let keep_forward (trans : pure_fun_translation) : bool =
-  let (fwd, _), backs = trans in
+  let { f = fwd; _ }, backs = trans in
   (* Note that at this point, the output types are no longer seen as tuples:
    * they should be lists of length 1. *)
   if
@@ -1908,7 +1908,7 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl =
     [ctx]: used only for printing.
  *)
 let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) :
-    (fun_decl * fun_decl list) option =
+    fun_and_loops option =
   (* Debug *)
   log#ldebug
     (lazy
@@ -1949,9 +1949,9 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) :
       let def, loops = decompose_loops def in
 
       (* Apply the remaining passes *)
-      let def = apply_end_passes_to_def ctx def in
+      let f = apply_end_passes_to_def ctx def in
       let loops = List.map (apply_end_passes_to_def ctx) loops in
-      Some (def, loops)
+      Some { f; loops }
 
 (** Small utility for {!filter_loop_inputs} *)
 let filter_prefix (keep : bool list) (ls : 'a list) : 'a list =
@@ -1996,10 +1996,11 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
       (List.concat
          (List.concat
             (List.map
-               (fun (_, ((fwd, loops_fwd), backs)) ->
+               (fun (_, ({ f = fwd; loops = loops_fwd }, backs)) ->
                  [ fwd :: loops_fwd ]
                  :: List.map
-                      (fun (back, loops_back) -> [ back :: loops_back ])
+                      (fun { f = back; loops = loops_back } ->
+                        [ back :: loops_back ])
                       backs)
                transl)))
   in
@@ -2246,8 +2247,8 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
   let transl =
     List.map
       (fun (b, (fwd, backs)) ->
-        let filter_fun_and_loops (f, fl) =
-          (filter_in_one f, List.map filter_in_one fl)
+        let filter_fun_and_loops f =
+          { f = filter_in_one f.f; loops = List.map filter_in_one f.loops }
         in
         let fwd = filter_fun_and_loops fwd in
         let backs = List.map filter_fun_and_loops backs in
-- 
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/PureMicroPasses.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 72e3d05e..e97a9cd7 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1461,12 +1461,12 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
     altogether.
   *)
 let keep_forward (trans : pure_fun_translation) : bool =
-  let { f = fwd; _ }, backs = trans in
+  let { fwd; backs } = trans in
   (* Note that at this point, the output types are no longer seen as tuples:
    * they should be lists of length 1. *)
   if
     !Config.filter_useless_functions
-    && fwd.signature.output = mk_result_ty mk_unit_ty
+    && fwd.f.signature.output = mk_result_ty mk_unit_ty
     && backs <> []
   then false
   else true
@@ -1996,8 +1996,8 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
       (List.concat
          (List.concat
             (List.map
-               (fun (_, ({ f = fwd; loops = loops_fwd }, backs)) ->
-                 [ fwd :: loops_fwd ]
+               (fun (_, { fwd; backs }) ->
+                 [ fwd.f :: fwd.loops ]
                  :: List.map
                       (fun { f = back; loops = loops_back } ->
                         [ back :: loops_back ])
@@ -2246,13 +2246,13 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
   in
   let transl =
     List.map
-      (fun (b, (fwd, backs)) ->
+      (fun (b, { fwd; backs }) ->
         let filter_fun_and_loops f =
           { f = filter_in_one f.f; loops = List.map filter_in_one f.loops }
         in
         let fwd = filter_fun_and_loops fwd in
         let backs = List.map filter_fun_and_loops backs in
-        (b, (fwd, backs)))
+        (b, { fwd; backs }))
       transl
   in
 
@@ -2278,10 +2278,10 @@ let apply_passes_to_pure_fun_translations (ctx : trans_ctx)
   let apply_to_one (trans : fun_decl * fun_decl list) :
       bool * pure_fun_translation =
     (* Apply the passes to the individual functions *)
-    let forward, backwards = trans in
-    let forward = Option.get (apply_passes_to_def ctx forward) in
-    let backwards = List.filter_map (apply_passes_to_def ctx) backwards in
-    let trans = (forward, backwards) in
+    let fwd, backs = trans in
+    let fwd = Option.get (apply_passes_to_def ctx fwd) in
+    let backs = List.filter_map (apply_passes_to_def ctx) backs in
+    let trans = { fwd; backs } in
     (* Compute whether we need to filter the forward function or not *)
     (keep_forward trans, trans)
   in
-- 
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/PureMicroPasses.ml | 28 +++++++++++++---------------
 1 file changed, 13 insertions(+), 15 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index e97a9cd7..6c9c3a91 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1460,8 +1460,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
     In such situation, we can remove the forward function definition
     altogether.
   *)
-let keep_forward (trans : pure_fun_translation) : bool =
-  let { fwd; backs } = trans in
+let keep_forward (fwd : fun_and_loops) (backs : fun_and_loops list) : bool =
   (* Note that at this point, the output types are no longer seen as tuples:
    * they should be lists of length 1. *)
   if
@@ -1977,8 +1976,8 @@ end
 module FunLoopIdMap = Collections.MakeMap (FunLoopIdOrderedType)
 
 (** Filter the useless loop input parameters. *)
-let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
-    (bool * pure_fun_translation) list =
+let filter_loop_inputs (transl : pure_fun_translation list) :
+    pure_fun_translation list =
   (* We need to explore groups of mutually recursive functions. In order
      to compute which parameters are useless, we need to explore the
      functions by groups of mutually recursive definitions.
@@ -1996,7 +1995,7 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
       (List.concat
          (List.concat
             (List.map
-               (fun (_, { fwd; backs }) ->
+               (fun { fwd; backs; _ } ->
                  [ fwd.f :: fwd.loops ]
                  :: List.map
                       (fun { f = back; loops = loops_back } ->
@@ -2246,13 +2245,13 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
   in
   let transl =
     List.map
-      (fun (b, { fwd; backs }) ->
+      (fun trans ->
         let filter_fun_and_loops f =
           { f = filter_in_one f.f; loops = List.map filter_in_one f.loops }
         in
-        let fwd = filter_fun_and_loops fwd in
-        let backs = List.map filter_fun_and_loops backs in
-        (b, { fwd; backs }))
+        let fwd = filter_fun_and_loops trans.fwd in
+        let backs = List.map filter_fun_and_loops trans.backs in
+        { trans with fwd; backs })
       transl
   in
 
@@ -2273,18 +2272,17 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
     but convenient.
  *)
 let apply_passes_to_pure_fun_translations (ctx : trans_ctx)
-    (transl : (fun_decl * fun_decl list) list) :
-    (bool * pure_fun_translation) list =
-  let apply_to_one (trans : fun_decl * fun_decl list) :
-      bool * pure_fun_translation =
+    (transl : (fun_decl * fun_decl list) list) : pure_fun_translation list =
+  let apply_to_one (trans : fun_decl * fun_decl list) : pure_fun_translation =
     (* Apply the passes to the individual functions *)
     let fwd, backs = trans in
     let fwd = Option.get (apply_passes_to_def ctx fwd) in
     let backs = List.filter_map (apply_passes_to_def ctx) backs in
-    let trans = { fwd; backs } in
     (* Compute whether we need to filter the forward function or not *)
-    (keep_forward trans, trans)
+    let keep_fwd = keep_forward fwd backs in
+    { keep_fwd; fwd; backs }
   in
+
   let transl = List.map apply_to_one transl in
 
   (* Filter the useless inputs in the loop functions *)
-- 
cgit v1.2.3


From 5921be8e2e8955db5101354d8bf29ae6a3693f48 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 11 Sep 2023 06:35:07 +0200
Subject: Make progress on correctly handling trait method calls in the
 symbolic execution

---
 compiler/PureMicroPasses.ml | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 6c9c3a91..53148dbb 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -765,7 +765,7 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
     In this situation, we can remove the call [f@fwd x].
  *)
 let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
-    (id0 : A.fun_id) (lp_id0 : LoopId.id option)
+    (id0 : fun_id_or_trait_method_ref) (lp_id0 : LoopId.id option)
     (rg_id0 : T.RegionGroupId.id option) (generics0 : generic_args)
     (args0 : texpression list) (e : texpression) : bool =
   let check_call (fun_id1 : fun_or_op_id) (generics1 : generic_args)
@@ -791,6 +791,11 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
                   (* We need to use the regions hierarchy *)
                   (* First, lookup the signature of the LLBC function *)
                   let sg =
+                    let id0 =
+                      match id0 with
+                      | FunId fun_id -> fun_id
+                      | TraitMethod (_, _, fun_decl_id) -> A.Regular fun_decl_id
+                    in
                     LlbcAstUtils.lookup_fun_sig id0 ctx.fun_context.fun_decls
                   in
                   (* Compute the set of ancestors of the function in call1 *)
@@ -1521,7 +1526,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
         match opt_destruct_function_call e with
         | Some (fun_id, _tys, args) -> (
             match fun_id with
-            | Fun (FromLlbc (A.Assumed aid, _lp_id, rg_id)) -> (
+            | Fun (FromLlbc (FunId (A.Assumed aid), _lp_id, rg_id)) -> (
                 (* Below, when dealing with the arguments: we consider the very
                  * general case, where functions could be boxed (meaning we
                  * could have: [box_new f x])
@@ -2024,7 +2029,6 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
      additional parameters.
   *)
   let used_map = ref FunLoopIdMap.empty in
-  let fun_id_to_fun_loop_id (fid, loop_id, _) = (fid, loop_id) in
 
   (* We start by computing the filtering information, for each function *)
   let compute_one_filter_info (decl : fun_decl) =
@@ -2069,8 +2073,8 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
               match e_app.e with
               | Qualif qualif -> (
                   match qualif.id with
-                  | FunOrOp (Fun (FromLlbc fun_id')) ->
-                      if fun_id_to_fun_loop_id fun_id' = fun_id then (
+                  | FunOrOp (Fun (FromLlbc (FunId fun_id', loop_id', _))) ->
+                      if (fun_id', loop_id') = fun_id then (
                         (* For each argument, check if it is exactly the original
                            input parameter. Note that there shouldn't be partial
                            applications of loop functions: the number of arguments
@@ -2129,9 +2133,9 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
   (* We then apply the filtering to all the function definitions at once *)
   let filter_in_one (decl : fun_decl) : fun_decl =
     (* Filter the function signature *)
-    let fun_id = (A.Regular decl.def_id, decl.loop_id, decl.back_id) in
+    let fun_id = (A.Regular decl.def_id, decl.loop_id) in
     let decl =
-      match FunLoopIdMap.find_opt (fun_id_to_fun_loop_id fun_id) !used_map with
+      match FunLoopIdMap.find_opt fun_id !used_map with
       | None -> (* Nothing to filter *) decl
       | Some used_info ->
           let num_filtered =
@@ -2179,9 +2183,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
           let { inputs; inputs_lvs; body } = body in
 
           let inputs, inputs_lvs =
-            match
-              FunLoopIdMap.find_opt (fun_id_to_fun_loop_id fun_id) !used_map
-            with
+            match FunLoopIdMap.find_opt fun_id !used_map with
             | None -> (* Nothing to filter *) (inputs, inputs_lvs)
             | Some used_info ->
                 let inputs = filter_prefix used_info inputs in
@@ -2201,11 +2203,10 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
                     match e_app.e with
                     | Qualif qualif -> (
                         match qualif.id with
-                        | FunOrOp (Fun (FromLlbc fun_id)) -> (
+                        | FunOrOp (Fun (FromLlbc (FunId fun_id, loop_id, _)))
+                          -> (
                             match
-                              FunLoopIdMap.find_opt
-                                (fun_id_to_fun_loop_id fun_id)
-                                !used_map
+                              FunLoopIdMap.find_opt (fun_id, loop_id) !used_map
                             with
                             | None -> super#visit_texpression env e
                             | Some used_info ->
-- 
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/PureMicroPasses.ml | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 53148dbb..2130d5c2 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -586,9 +586,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                   generics = _;
                 } ->
                 (* Lookup the def *)
-                let decl =
-                  TypeDeclId.Map.find adt_id ctx.type_context.type_decls
-                in
+                let decl = TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls in
                 (* Check that there are as many arguments as there are fields - note
                    that the def should have a body (otherwise we couldn't use the
                    constructor) *)
@@ -597,8 +595,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                   (* Check if the definition is recursive *)
                   let is_rec =
                     match
-                      TypeDeclId.Map.find adt_id
-                        ctx.type_context.type_decls_groups
+                      TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls_groups
                     with
                     | NonRec _ -> false
                     | Rec _ -> true
@@ -796,7 +793,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
                       | FunId fun_id -> fun_id
                       | TraitMethod (_, _, fun_decl_id) -> A.Regular fun_decl_id
                     in
-                    LlbcAstUtils.lookup_fun_sig id0 ctx.fun_context.fun_decls
+                    LlbcAstUtils.lookup_fun_sig id0 ctx.fun_ctx.fun_decls
                   in
                   (* Compute the set of ancestors of the function in call1 *)
                   let call1_ancestors =
@@ -1094,7 +1091,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 (* This is a struct *)
                 (* Retrieve the definiton, to find how many fields there are *)
                 let adt_decl =
-                  TypeDeclId.Map.find adt_id ctx.type_context.type_decls
+                  TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls
                 in
                 let fields =
                   match adt_decl.kind with
-- 
cgit v1.2.3


From 0f0e4be7dc746e2676db33f850bbeddf239eaec8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 13 Oct 2023 00:40:37 +0200
Subject: Add sup

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

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 2130d5c2..cedc3559 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1563,7 +1563,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     | ArraySubsliceMut | SliceIndexShared | SliceIndexMut
                     | SliceSubsliceShared | SliceSubsliceMut | ArrayIndexShared
                     | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
-                    | SliceLen ),
+                    | ArrayRepeat | SliceLen ),
                     _ ) ->
                     super#visit_texpression env e)
             | _ -> super#visit_texpression env e)
-- 
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/PureMicroPasses.ml | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index cedc3559..b00509a6 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -791,7 +791,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
                     let id0 =
                       match id0 with
                       | FunId fun_id -> fun_id
-                      | TraitMethod (_, _, fun_decl_id) -> A.Regular fun_decl_id
+                      | TraitMethod (_, _, fun_decl_id) -> Regular fun_decl_id
                     in
                     LlbcAstUtils.lookup_fun_sig id0 ctx.fun_ctx.fun_decls
                   in
@@ -1523,29 +1523,29 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
         match opt_destruct_function_call e with
         | Some (fun_id, _tys, args) -> (
             match fun_id with
-            | Fun (FromLlbc (FunId (A.Assumed aid), _lp_id, rg_id)) -> (
+            | Fun (FromLlbc (FunId (Assumed aid), _lp_id, rg_id)) -> (
                 (* Below, when dealing with the arguments: we consider the very
                  * general case, where functions could be boxed (meaning we
                  * could have: [box_new f x])
                  * *)
                 match (aid, rg_id) with
-                | A.BoxNew, _ ->
+                | BoxNew, _ ->
                     assert (rg_id = None);
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
-                | A.BoxDeref, None ->
+                | BoxDeref, None ->
                     (* [Box::deref] forward is the identity *)
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
-                | A.BoxDeref, Some _ ->
+                | BoxDeref, Some _ ->
                     (* [Box::deref] backward is [()] (doesn't give back anything) *)
                     assert (args = []);
                     mk_unit_rvalue
-                | A.BoxDerefMut, None ->
+                | BoxDerefMut, None ->
                     (* [Box::deref_mut] forward is the identity *)
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
-                | A.BoxDerefMut, Some _ ->
+                | BoxDerefMut, Some _ ->
                     (* [Box::deref_mut] back is almost the identity:
                      * let box_deref_mut (x_init : t) (x_back : t) : t = x_back
                      * *)
@@ -1555,15 +1555,15 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
                       | _ -> raise (Failure "Unreachable")
                     in
                     mk_apps arg args
-                | A.BoxFree, _ ->
+                | BoxFree, _ ->
                     assert (args = []);
                     mk_unit_rvalue
-                | ( ( A.Replace | VecNew | VecPush | VecInsert | VecLen
-                    | VecIndex | VecIndexMut | ArraySubsliceShared
-                    | ArraySubsliceMut | SliceIndexShared | SliceIndexMut
-                    | SliceSubsliceShared | SliceSubsliceMut | ArrayIndexShared
-                    | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
-                    | ArrayRepeat | SliceLen ),
+                | ( ( Replace | VecNew | VecPush | VecInsert | VecLen | VecIndex
+                    | VecIndexMut | ArraySubsliceShared | ArraySubsliceMut
+                    | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
+                    | SliceSubsliceMut | ArrayIndexShared | ArrayIndexMut
+                    | ArrayToSliceShared | ArrayToSliceMut | ArrayRepeat
+                    | SliceLen ),
                     _ ) ->
                     super#visit_texpression env e)
             | _ -> super#visit_texpression env e)
@@ -2046,7 +2046,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
     let inputs_set = VarId.Set.of_list (List.map var_get_id inputs_prefix) in
     assert (Option.is_some decl.loop_id);
 
-    let fun_id = (A.Regular decl.def_id, decl.loop_id) in
+    let fun_id = (E.Regular decl.def_id, decl.loop_id) in
 
     let set_used vid =
       used := List.map (fun (vid', b) -> (vid', b || vid = vid')) !used
@@ -2130,7 +2130,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
   (* We then apply the filtering to all the function definitions at once *)
   let filter_in_one (decl : fun_decl) : fun_decl =
     (* Filter the function signature *)
-    let fun_id = (A.Regular decl.def_id, decl.loop_id) in
+    let fun_id = (E.Regular decl.def_id, decl.loop_id) in
     let decl =
       match FunLoopIdMap.find_opt fun_id !used_map with
       | None -> (* Nothing to filter *) decl
-- 
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/PureMicroPasses.ml | 42 ++++++++++++++++++++++--------------------
 1 file changed, 22 insertions(+), 20 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index b00509a6..a326d19e 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1513,7 +1513,7 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl =
     function calls, and when translating end abstractions. Here, we can do
     something simpler, in one micro-pass.
  *)
-let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
+let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
   (* The map visitor *)
   let obj =
     object
@@ -1522,30 +1522,42 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
       method! visit_texpression env e =
         match opt_destruct_function_call e with
         | Some (fun_id, _tys, args) -> (
+            (* Below, when dealing with the arguments: we consider the very
+             * general case, where functions could be boxed (meaning we
+             * could have: [box_new f x])
+             * *)
             match fun_id with
             | Fun (FromLlbc (FunId (Assumed aid), _lp_id, rg_id)) -> (
-                (* Below, when dealing with the arguments: we consider the very
-                 * general case, where functions could be boxed (meaning we
-                 * could have: [box_new f x])
-                 * *)
                 match (aid, rg_id) with
                 | BoxNew, _ ->
                     assert (rg_id = None);
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
-                | BoxDeref, None ->
+                | BoxFree, _ ->
+                    assert (args = []);
+                    mk_unit_rvalue
+                | ( ( SliceIndexShared | SliceIndexMut | ArrayIndexShared
+                    | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
+                    | ArrayRepeat | SliceLen ),
+                    _ ) ->
+                    super#visit_texpression env e)
+            | Fun (FromLlbc (FunId (Regular fid), _lp_id, rg_id)) -> (
+                (* Lookup the function name *)
+                let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in
+                match (Names.name_to_string def.name, rg_id) with
+                | "alloc::box::Boxed::deref", None ->
                     (* [Box::deref] forward is the identity *)
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
-                | BoxDeref, Some _ ->
+                | "alloc::box::Boxed::deref", Some _ ->
                     (* [Box::deref] backward is [()] (doesn't give back anything) *)
                     assert (args = []);
                     mk_unit_rvalue
-                | BoxDerefMut, None ->
+                | "alloc::box::Boxed::deref_mut", None ->
                     (* [Box::deref_mut] forward is the identity *)
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
-                | BoxDerefMut, Some _ ->
+                | "alloc::box::Boxed::deref_mut", Some _ ->
                     (* [Box::deref_mut] back is almost the identity:
                      * let box_deref_mut (x_init : t) (x_back : t) : t = x_back
                      * *)
@@ -1555,17 +1567,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
                       | _ -> raise (Failure "Unreachable")
                     in
                     mk_apps arg args
-                | BoxFree, _ ->
-                    assert (args = []);
-                    mk_unit_rvalue
-                | ( ( Replace | VecNew | VecPush | VecInsert | VecLen | VecIndex
-                    | VecIndexMut | ArraySubsliceShared | ArraySubsliceMut
-                    | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
-                    | SliceSubsliceMut | ArrayIndexShared | ArrayIndexMut
-                    | ArrayToSliceShared | ArrayToSliceMut | ArrayRepeat
-                    | SliceLen ),
-                    _ ) ->
-                    super#visit_texpression env e)
+                | _ -> super#visit_texpression env e)
             | _ -> super#visit_texpression env e)
         | _ -> super#visit_texpression env e
     end
-- 
cgit v1.2.3


From 6eebc66e34561bc6985b5866d49c8314a6fbaee9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 17:47:39 +0200
Subject: Start taking into account non-fallible functions like
 core::mem::replace

---
 compiler/PureMicroPasses.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index a326d19e..f3e6cbe2 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1544,20 +1544,22 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
             | Fun (FromLlbc (FunId (Regular fid), _lp_id, rg_id)) -> (
                 (* Lookup the function name *)
                 let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in
-                match (Names.name_to_string def.name, rg_id) with
-                | "alloc::box::Boxed::deref", None ->
+                match
+                  (Names.name_no_disambiguators_to_string def.name, rg_id)
+                with
+                | "alloc::boxed::Box::deref", None ->
                     (* [Box::deref] forward is the identity *)
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
-                | "alloc::box::Boxed::deref", Some _ ->
+                | "alloc::boxed::Box::deref", Some _ ->
                     (* [Box::deref] backward is [()] (doesn't give back anything) *)
                     assert (args = []);
                     mk_unit_rvalue
-                | "alloc::box::Boxed::deref_mut", None ->
+                | "alloc::boxed::Box::deref_mut", None ->
                     (* [Box::deref_mut] forward is the identity *)
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
-                | "alloc::box::Boxed::deref_mut", Some _ ->
+                | "alloc::boxed::Box::deref_mut", Some _ ->
                     (* [Box::deref_mut] back is almost the identity:
                      * let box_deref_mut (x_init : t) (x_back : t) : t = x_back
                      * *)
-- 
cgit v1.2.3


From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 19:28:56 +0100
Subject: Remove the 'r type variable from the ty type definition

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

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index f3e6cbe2..d62a028e 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -791,7 +791,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
                     let id0 =
                       match id0 with
                       | FunId fun_id -> fun_id
-                      | TraitMethod (_, _, fun_decl_id) -> Regular fun_decl_id
+                      | TraitMethod (_, _, fun_decl_id) -> FRegular fun_decl_id
                     in
                     LlbcAstUtils.lookup_fun_sig id0 ctx.fun_ctx.fun_decls
                   in
@@ -1527,7 +1527,7 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
              * could have: [box_new f x])
              * *)
             match fun_id with
-            | Fun (FromLlbc (FunId (Assumed aid), _lp_id, rg_id)) -> (
+            | Fun (FromLlbc (FunId (FAssumed aid), _lp_id, rg_id)) -> (
                 match (aid, rg_id) with
                 | BoxNew, _ ->
                     assert (rg_id = None);
@@ -1541,7 +1541,7 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     | ArrayRepeat | SliceLen ),
                     _ ) ->
                     super#visit_texpression env e)
-            | Fun (FromLlbc (FunId (Regular fid), _lp_id, rg_id)) -> (
+            | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> (
                 (* Lookup the function name *)
                 let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in
                 match
@@ -2050,7 +2050,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
     let inputs_set = VarId.Set.of_list (List.map var_get_id inputs_prefix) in
     assert (Option.is_some decl.loop_id);
 
-    let fun_id = (E.Regular decl.def_id, decl.loop_id) in
+    let fun_id = (E.FRegular decl.def_id, decl.loop_id) in
 
     let set_used vid =
       used := List.map (fun (vid', b) -> (vid', b || vid = vid')) !used
@@ -2134,7 +2134,7 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
   (* We then apply the filtering to all the function definitions at once *)
   let filter_in_one (decl : fun_decl) : fun_decl =
     (* Filter the function signature *)
-    let fun_id = (E.Regular decl.def_id, decl.loop_id) in
+    let fun_id = (E.FRegular decl.def_id, decl.loop_id) in
     let decl =
       match FunLoopIdMap.find_opt fun_id !used_map with
       | None -> (* Nothing to filter *) decl
-- 
cgit v1.2.3


From 6ef68fa9ffd4caec09677ee2800a778080d6da34 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 20:04:11 +0100
Subject: Prefix variants related to types with "T"

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

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index d62a028e..8872571f 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -582,7 +582,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
             match app.e with
             | Qualif
                 {
-                  id = AdtCons { adt_id = AdtId adt_id; variant_id = None };
+                  id = AdtCons { adt_id = TAdtId adt_id; variant_id = None };
                   generics = _;
                 } ->
                 (* Lookup the def *)
@@ -606,7 +606,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     (!Config.backend <> Lean && !Config.backend <> Coq)
                     || not is_rec
                   then
-                    let struct_id = AdtId adt_id in
+                    let struct_id = TAdtId adt_id in
                     let init = None in
                     let updates =
                       FieldId.mapi
@@ -1085,7 +1085,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
             match app.e with
             | Qualif
                 {
-                  id = AdtCons { adt_id = AdtId adt_id; variant_id = None };
+                  id = AdtCons { adt_id = TAdtId adt_id; variant_id = None };
                   generics;
                 } ->
                 (* This is a struct *)
@@ -1114,7 +1114,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                         | ( Qualif
                               {
                                 id =
-                                  Proj { adt_id = AdtId proj_adt_id; field_id };
+                                  Proj { adt_id = TAdtId proj_adt_id; field_id };
                                 generics = proj_generics;
                               },
                             Var v ) ->
@@ -1157,13 +1157,13 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                   match (proj.e, x.e) with
                   | ( Qualif
                         {
-                          id = Proj { adt_id = AdtId proj_adt_id; field_id };
+                          id = Proj { adt_id = TAdtId proj_adt_id; field_id };
                           generics = _;
                         },
                       Var v ) ->
                       (* We check that this is the proper ADT, and the proper field *)
                       if
-                        AdtId proj_adt_id = struct_id
+                        TAdtId proj_adt_id = struct_id
                         && field_id = fid && x.ty = adt_ty
                       then Some v
                       else None
-- 
cgit v1.2.3


From 6c88d30031255c0ac612b67bb5b3c20c2f07e563 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 13 Nov 2023 13:27:02 +0100
Subject: Add RegionsHierarchy.ml

---
 compiler/PureMicroPasses.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 8872571f..d2747a4b 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -786,18 +786,19 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
                 if rg_id0 = rg_id1 then true
                 else
                   (* We need to use the regions hierarchy *)
-                  (* First, lookup the signature of the LLBC function *)
-                  let sg =
+                  let regions_hierarchy =
                     let id0 =
                       match id0 with
                       | FunId fun_id -> fun_id
                       | TraitMethod (_, _, fun_decl_id) -> FRegular fun_decl_id
                     in
-                    LlbcAstUtils.lookup_fun_sig id0 ctx.fun_ctx.fun_decls
+                    LlbcAstUtils.FunIdMap.find id0
+                      ctx.fun_ctx.regions_hierarchies
                   in
                   (* Compute the set of ancestors of the function in call1 *)
                   let call1_ancestors =
-                    LlbcAstUtils.list_ancestor_region_groups sg rg_id1
+                    LlbcAstUtils.list_ancestor_region_groups regions_hierarchy
+                      rg_id1
                   in
                   (* Check if the function used in call0 is inside *)
                   T.RegionGroupId.Set.mem rg_id0 call1_ancestors
-- 
cgit v1.2.3


From a27efd1ed08bc9583752445d9eda7a693c0c7379 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 16 Nov 2023 10:13:28 +0100
Subject: Finish propagating the changes to the names and cleaning

---
 compiler/PureMicroPasses.ml | 29 +++++++++++++++++------------
 1 file changed, 17 insertions(+), 12 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index d2747a4b..2106c206 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -3,10 +3,13 @@
 open Pure
 open PureUtils
 open TranslateCore
-module V = Values
 
 (** The local logger *)
-let log = L.pure_micro_passes_log
+let log = Logging.pure_micro_passes_log
+
+let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
+  let fmt = trans_ctx_to_pure_fmt_env ctx in
+  PrintPure.fun_decl_to_string fmt def
 
 (** Small utility.
 
@@ -597,8 +600,8 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     match
                       TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls_groups
                     with
-                    | NonRec _ -> false
-                    | Rec _ -> true
+                    | NonRecGroup _ -> false
+                    | RecGroup _ -> true
                   in
                   (* Convert, if possible - note that for now for Lean and Coq
                      we don't support the structure syntax on recursive structures *)
@@ -1420,14 +1423,15 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
 
             let loop_body = { inputs; inputs_lvs; body = loop_body } in
 
-            let loop_def =
+            let loop_def : fun_decl =
               {
                 def_id = def.def_id;
                 kind = def.kind;
                 num_loops;
                 loop_id = Some loop.loop_id;
                 back_id = def.back_id;
-                basename = def.basename;
+                llbc_name = def.llbc_name;
+                name = def.name;
                 signature = loop_sig;
                 is_global_decl_body = def.is_global_decl_body;
                 body = Some loop_body;
@@ -1539,10 +1543,12 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     mk_unit_rvalue
                 | ( ( SliceIndexShared | SliceIndexMut | ArrayIndexShared
                     | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
-                    | ArrayRepeat | SliceLen ),
+                    | ArrayRepeat ),
                     _ ) ->
                     super#visit_texpression env e)
-            | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> (
+            | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) ->
+                failwith "TODO"
+                (*
                 (* Lookup the function name *)
                 let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in
                 match
@@ -1570,7 +1576,8 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                       | _ -> raise (Failure "Unreachable")
                     in
                     mk_apps arg args
-                | _ -> super#visit_texpression env e)
+                | _ -> super#visit_texpression env e
+                       *)
             | _ -> super#visit_texpression env e)
         | _ -> super#visit_texpression env e
     end
@@ -1918,9 +1925,7 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) :
   (* Debug *)
   log#ldebug
     (lazy
-      ("PureMicroPasses.apply_passes_to_def: "
-      ^ Print.fun_name_to_string def.basename
-      ^ " ("
+      ("PureMicroPasses.apply_passes_to_def: " ^ def.name ^ " ("
       ^ Print.option_to_string T.RegionGroupId.to_string def.back_id
       ^ ")"));
 
-- 
cgit v1.2.3


From 9ab6a034aaadacac62d241474af3cf28bf6ac928 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 16 Nov 2023 10:52:28 +0100
Subject: Update SymbolicToPure.eliminate_box_functions

---
 compiler/PureMicroPasses.ml | 75 +++++++++++++++++++++++++++------------------
 1 file changed, 45 insertions(+), 30 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 2106c206..50a50815 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1546,38 +1546,53 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     | ArrayRepeat ),
                     _ ) ->
                     super#visit_texpression env e)
-            | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) ->
-                failwith "TODO"
-                (*
+            | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> (
+                (* TODO: use a more general matching mechanism *)
                 (* Lookup the function name *)
                 let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in
-                match
-                  (Names.name_no_disambiguators_to_string def.name, rg_id)
-                with
-                | "alloc::boxed::Box::deref", None ->
-                    (* [Box::deref] forward is the identity *)
-                    let arg, args = Collections.List.pop args in
-                    mk_apps arg args
-                | "alloc::boxed::Box::deref", Some _ ->
-                    (* [Box::deref] backward is [()] (doesn't give back anything) *)
-                    assert (args = []);
-                    mk_unit_rvalue
-                | "alloc::boxed::Box::deref_mut", None ->
-                    (* [Box::deref_mut] forward is the identity *)
-                    let arg, args = Collections.List.pop args in
-                    mk_apps arg args
-                | "alloc::boxed::Box::deref_mut", Some _ ->
-                    (* [Box::deref_mut] back is almost the identity:
-                     * let box_deref_mut (x_init : t) (x_back : t) : t = x_back
-                     * *)
-                    let arg, args =
-                      match args with
-                      | _ :: given_back :: args -> (given_back, args)
-                      | _ -> raise (Failure "Unreachable")
-                    in
-                    mk_apps arg args
-                | _ -> super#visit_texpression env e
-                       *)
+                (* We first need to check if the name is "alloc::boxed::Box::_" *)
+                match def.name with
+                | [
+                 PeIdent ("alloc", _);
+                 PeIdent ("boxed", _);
+                 PeImpl impl;
+                 PeIdent (fname, _);
+                ] -> (
+                    match impl.ty with
+                    | TAdt
+                        ( TAssumed TBox,
+                          {
+                            regions = [];
+                            types = [ TVar _ ];
+                            const_generics = [];
+                            trait_refs = [];
+                          } ) -> (
+                        match (fname, rg_id) with
+                        | "deref", None ->
+                            (* [Box::deref] forward is the identity *)
+                            let arg, args = Collections.List.pop args in
+                            mk_apps arg args
+                        | "deref", Some _ ->
+                            (* [Box::deref] backward is [()] (doesn't give back anything) *)
+                            assert (args = []);
+                            mk_unit_rvalue
+                        | "deref_mut", None ->
+                            (* [Box::deref_mut] forward is the identity *)
+                            let arg, args = Collections.List.pop args in
+                            mk_apps arg args
+                        | "deref_mut", Some _ ->
+                            (* [Box::deref_mut] back is almost the identity:
+                             * let box_deref_mut (x_init : t) (x_back : t) : t = x_back
+                             * *)
+                            let arg, args =
+                              match args with
+                              | _ :: given_back :: args -> (given_back, args)
+                              | _ -> raise (Failure "Unreachable")
+                            in
+                            mk_apps arg args
+                        | _ -> super#visit_texpression env e)
+                    | _ -> super#visit_texpression env e)
+                | _ -> super#visit_texpression env e)
             | _ -> super#visit_texpression env e)
         | _ -> super#visit_texpression env e
     end
-- 
cgit v1.2.3


From 5aa37b3a0a539f9ae37a119b9ce7c8dee504125e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 20 Nov 2023 22:38:58 +0100
Subject: Fix minor issues

---
 compiler/PureMicroPasses.ml | 66 +++++++++------------------------------------
 1 file changed, 13 insertions(+), 53 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 50a50815..96421925 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1250,6 +1250,7 @@ let filter_if_backward_with_no_outputs (def : fun_decl) : fun_decl option =
     !Config.filter_useless_functions
     && Option.is_some def.back_id
     && def.signature.output = mk_result_ty mk_unit_ty
+    || def.signature.output = mk_unit_ty
   then None
   else Some def
 
@@ -1508,8 +1509,8 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl =
       let body = Some { body with body = body_exp; inputs_lvs } in
       { def with body }
 
-(** Eliminate the box functions like [Box::new], [Box::deref], etc. Most of them
-    are translated to identity, and [Box::free] is translated to [()].
+(** Eliminate the box functions like [Box::new] (which is translated to the
+    identity) and [Box::free] (which is translated to [()]).
 
     Note that the box types have already been eliminated during the translation
     from symbolic to pure.
@@ -1518,7 +1519,7 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl =
     function calls, and when translating end abstractions. Here, we can do
     something simpler, in one micro-pass.
  *)
-let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
+let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
   (* The map visitor *)
   let obj =
     object
@@ -1546,53 +1547,6 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     | ArrayRepeat ),
                     _ ) ->
                     super#visit_texpression env e)
-            | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> (
-                (* TODO: use a more general matching mechanism *)
-                (* Lookup the function name *)
-                let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in
-                (* We first need to check if the name is "alloc::boxed::Box::_" *)
-                match def.name with
-                | [
-                 PeIdent ("alloc", _);
-                 PeIdent ("boxed", _);
-                 PeImpl impl;
-                 PeIdent (fname, _);
-                ] -> (
-                    match impl.ty with
-                    | TAdt
-                        ( TAssumed TBox,
-                          {
-                            regions = [];
-                            types = [ TVar _ ];
-                            const_generics = [];
-                            trait_refs = [];
-                          } ) -> (
-                        match (fname, rg_id) with
-                        | "deref", None ->
-                            (* [Box::deref] forward is the identity *)
-                            let arg, args = Collections.List.pop args in
-                            mk_apps arg args
-                        | "deref", Some _ ->
-                            (* [Box::deref] backward is [()] (doesn't give back anything) *)
-                            assert (args = []);
-                            mk_unit_rvalue
-                        | "deref_mut", None ->
-                            (* [Box::deref_mut] forward is the identity *)
-                            let arg, args = Collections.List.pop args in
-                            mk_apps arg args
-                        | "deref_mut", Some _ ->
-                            (* [Box::deref_mut] back is almost the identity:
-                             * let box_deref_mut (x_init : t) (x_back : t) : t = x_back
-                             * *)
-                            let arg, args =
-                              match args with
-                              | _ :: given_back :: args -> (given_back, args)
-                              | _ -> raise (Failure "Unreachable")
-                            in
-                            mk_apps arg args
-                        | _ -> super#visit_texpression env e)
-                    | _ -> super#visit_texpression env e)
-                | _ -> super#visit_texpression env e)
             | _ -> super#visit_texpression env e)
         | _ -> super#visit_texpression env e
     end
@@ -1966,11 +1920,17 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) :
    * Note that the calls to those functions should already have been removed,
    * when translating from symbolic to pure. Here, we remove the definitions
    * altogether, because they are now useless *)
-  let def = filter_if_backward_with_no_outputs def in
+  let name = def.name ^ PrintPure.fun_suffix def.loop_id def.back_id in
+  let opt_def = filter_if_backward_with_no_outputs def in
 
-  match def with
-  | None -> None
+  match opt_def with
+  | None ->
+      log#ldebug (lazy ("filtered (backward with no outputs): " ^ name ^ "\n"));
+      None
   | Some def ->
+      log#ldebug
+        (lazy ("not filtered (not backward with no outputs): " ^ name ^ "\n"));
+
       (* Extract the loop definitions by removing the {!Loop} node *)
       let def, loops = decompose_loops def in
 
-- 
cgit v1.2.3


From e94cd72ffa63dbc5fc40c7c1a422c1a70ba4a7e5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 13:55:46 +0100
Subject: Add an `is_local` field to declarations

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

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 96421925..1565f252 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1427,6 +1427,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
             let loop_def : fun_decl =
               {
                 def_id = def.def_id;
+                is_local = def.is_local;
                 kind = def.kind;
                 num_loops;
                 loop_id = Some loop.loop_id;
-- 
cgit v1.2.3


From 77ba13b371cccbe8098e432ebd287108d5373666 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 14:43:12 +0100
Subject: Add span information to the generated code

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

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 1565f252..8463f56c 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -391,7 +391,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       | Switch (scrut, body) -> update_switch_body scrut body ctx
       | Loop loop -> update_loop loop ctx
       | StructUpdate supd -> update_struct_update supd ctx
-      | Meta (meta, e) -> update_meta meta e ctx
+      | Meta (meta, e) -> update_emeta meta e ctx
     in
     (ctx, { e; ty })
   (* *)
@@ -449,6 +449,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     let {
       fun_end;
       loop_id;
+      meta;
       fuel0;
       fuel;
       input_state;
@@ -467,6 +468,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       {
         fun_end;
         loop_id;
+        meta;
         fuel0;
         fuel;
         input_state;
@@ -490,7 +492,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     let supd = { struct_id; init; updates } in
     (ctx, StructUpdate supd)
   (* *)
-  and update_meta (meta : meta) (e : texpression) (ctx : pn_ctx) :
+  and update_emeta (meta : emeta) (e : texpression) (ctx : pn_ctx) :
       pn_ctx * expression =
     let ctx =
       match meta with
@@ -516,7 +518,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       | Tag _ -> ctx
     in
     let ctx, e = update_texpression e ctx in
-    let e = mk_meta meta e in
+    let e = mk_emeta meta e in
     (ctx, e.e)
   in
 
@@ -1428,6 +1430,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
               {
                 def_id = def.def_id;
                 is_local = def.is_local;
+                meta = loop.meta;
                 kind = def.kind;
                 num_loops;
                 loop_id = Some loop.loop_id;
-- 
cgit v1.2.3


From ba66f35a0e196c17757e06187cf2563abec253e5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 22 Nov 2023 09:09:46 +0100
Subject: Improve further the generation of parent clause/trait clause names

---
 compiler/PureMicroPasses.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 8463f56c..d0741b29 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1364,6 +1364,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
             let loop_sig =
               {
                 generics = fun_sig.generics;
+                llbc_generics = fun_sig.llbc_generics;
                 preds = fun_sig.preds;
                 inputs = inputs_tys;
                 output;
@@ -2127,7 +2128,8 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
           let num_filtered =
             List.length (List.filter (fun b -> not b) used_info)
           in
-          let { generics; preds; inputs; output; doutputs; info } =
+          let { generics; llbc_generics; preds; inputs; output; doutputs; info }
+              =
             decl.signature
           in
           let {
@@ -2155,7 +2157,9 @@ let filter_loop_inputs (transl : pure_fun_translation list) :
               effect_info;
             }
           in
-          let signature = { generics; preds; inputs; output; doutputs; info } in
+          let signature =
+            { generics; llbc_generics; preds; inputs; output; doutputs; info }
+          in
 
           { decl with signature }
     in
-- 
cgit v1.2.3