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/SymbolicAst.ml | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

(limited to 'compiler/SymbolicAst.ml')

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 7dc94dcd..17cdcabc 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -79,6 +79,9 @@ class ['self] iter_expression_base =
     method visit_loop_id : 'env -> V.loop_id -> unit = fun _ _ -> ()
     method visit_variant_id : 'env -> variant_id -> unit = fun _ _ -> ()
 
+    method visit_const_generic_var_id : 'env -> T.const_generic_var_id -> unit =
+      fun _ _ -> ()
+
     method visit_symbolic_value_id : 'env -> V.symbolic_value_id -> unit =
       fun _ _ -> ()
 
@@ -171,14 +174,14 @@ type expression =
       * expression
       (** We introduce a new symbolic value, equal to some other value.
 
-        This is used for instance when reorganizing the environment to compute
-        fixed points: we duplicate some shared symbolic values to destructure
-        the shared values, in order to make the environment a bit more general
-        (while losing precision of course).
+          This is used for instance when reorganizing the environment to compute
+          fixed points: we duplicate some shared symbolic values to destructure
+          the shared values, in order to make the environment a bit more general
+          (while losing precision of course).
 
-        The context is the evaluation context from before introducing the new
-        value. It has the same purpose as for the {!Return} case.
-      *)
+          The context is the evaluation context from before introducing the new
+          value. It has the same purpose as for the {!Return} case.
+       *)
   | ForwardEnd of
       Contexts.eval_ctx
       * V.typed_value symbolic_value_id_map option
@@ -253,6 +256,9 @@ and value_aggregate =
   | SingleValue of V.typed_value  (** Regular case *)
   | Array of V.typed_value list
       (** This is used when introducing array aggregates *)
+  | ConstGenericValue of T.const_generic_var_id
+      (** This is used when evaluating a const generic value: in the interpreter,
+          we introduce a fresh symbolic value. *)
 [@@deriving
   show,
     visitors
-- 
cgit v1.2.3


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/SymbolicAst.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'compiler/SymbolicAst.ml')

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 17cdcabc..0f107897 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -43,10 +43,7 @@ type call = {
           borrows (we need to perform lookups).
        *)
   abstractions : V.AbstractionId.id list;
-  (* TODO: rename to "...args" *)
-  type_params : T.ety list;
-  (* TODO: rename to "...args" *)
-  const_generic_params : T.const_generic list;
+  generics : T.egeneric_args;
   args : V.typed_value list;
   args_places : mplace option list;  (** Meta information *)
   dest : V.symbolic_value;
-- 
cgit v1.2.3


From c6b88a2e54b7697262ad3677ad7500471c68e332 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 10 Sep 2023 21:07:06 +0200
Subject: Add support for the trait associated constants

---
 compiler/SymbolicAst.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'compiler/SymbolicAst.ml')

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 0f107897..b170ebe5 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -120,6 +120,9 @@ class ['self] iter_expression_base =
 
     method visit_symbolic_expansion : 'env -> V.symbolic_expansion -> unit =
       fun _ _ -> ()
+
+    method visit_etrait_ref : 'env -> T.etrait_ref -> unit = fun _ _ -> ()
+    method visit_egeneric_args : 'env -> T.egeneric_args -> unit = fun _ _ -> ()
   end
 
 (** **Rem.:** here, {!expression} is not at all equivalent to the expressions
@@ -174,7 +177,8 @@ type expression =
           This is used for instance when reorganizing the environment to compute
           fixed points: we duplicate some shared symbolic values to destructure
           the shared values, in order to make the environment a bit more general
-          (while losing precision of course).
+          (while losing precision of course). We also use it to introduce symbolic
+          values when evaluating constant generics, or trait constants.
 
           The context is the evaluation context from before introducing the new
           value. It has the same purpose as for the {!Return} case.
@@ -256,6 +260,8 @@ and value_aggregate =
   | ConstGenericValue of T.const_generic_var_id
       (** This is used when evaluating a const generic value: in the interpreter,
           we introduce a fresh symbolic value. *)
+  | TraitConstValue of T.etrait_ref * T.egeneric_args * string
+      (** A trait constant value *)
 [@@deriving
   show,
     visitors
-- 
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/SymbolicAst.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/SymbolicAst.ml')

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index b170ebe5..4df8fec7 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -29,7 +29,7 @@ type mplace = {
 [@@deriving show]
 
 type call_id =
-  | Fun of A.fun_id * V.FunCallId.id
+  | Fun of A.fun_id_or_trait_method_ref * V.FunCallId.id
       (** A "regular" function (i.e., a function which is not a primitive operation) *)
   | Unop of E.unop
   | Binop of E.binop
-- 
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/SymbolicAst.ml | 40 +++++++++++++---------------------------
 1 file changed, 13 insertions(+), 27 deletions(-)

(limited to 'compiler/SymbolicAst.ml')

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 4df8fec7..927544b2 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -43,7 +43,7 @@ type call = {
           borrows (we need to perform lookups).
        *)
   abstractions : V.AbstractionId.id list;
-  generics : T.egeneric_args;
+  generics : T.generic_args;
   args : V.typed_value list;
   args_places : mplace option list;  (** Meta information *)
   dest : V.symbolic_value;
@@ -65,30 +65,22 @@ type global_decl_id = A.GlobalDeclId.id [@@deriving show]
 type 'a symbolic_value_id_map = 'a V.SymbolicValueId.Map.t [@@deriving show]
 type 'a region_group_id_map = 'a T.RegionGroupId.Map.t [@@deriving show]
 
-(** Ancestor for {!expression} iter visitor *)
+(** Ancestor for {!expression} iter visitor.
+
+    We could make it inherit the visitor for {!eval_ctx}, but in all the uses
+    of this visitor we don't need to explore {!eval_ctx}, so we make it inherit
+    the abstraction visitors instead.
+ *)
 class ['self] iter_expression_base =
   object (self : 'self)
-    inherit [_] VisitorsRuntime.iter
+    inherit [_] V.iter_abs
     method visit_eval_ctx : 'env -> Contexts.eval_ctx -> unit = fun _ _ -> ()
-    method visit_typed_value : 'env -> V.typed_value -> unit = fun _ _ -> ()
     method visit_call : 'env -> call -> unit = fun _ _ -> ()
-    method visit_abs : 'env -> V.abs -> unit = fun _ _ -> ()
     method visit_loop_id : 'env -> V.loop_id -> unit = fun _ _ -> ()
-    method visit_variant_id : 'env -> variant_id -> unit = fun _ _ -> ()
-
-    method visit_const_generic_var_id : 'env -> T.const_generic_var_id -> unit =
-      fun _ _ -> ()
-
-    method visit_symbolic_value_id : 'env -> V.symbolic_value_id -> unit =
-      fun _ _ -> ()
-
-    method visit_symbolic_value : 'env -> V.symbolic_value -> unit =
-      fun _ _ -> ()
 
     method visit_region_group_id : 'env -> T.RegionGroupId.id -> unit =
       fun _ _ -> ()
 
-    method visit_global_decl_id : 'env -> global_decl_id -> unit = fun _ _ -> ()
     method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
     method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
 
@@ -115,14 +107,8 @@ class ['self] iter_expression_base =
       fun env s ->
         V.SymbolicValueId.Set.iter (self#visit_symbolic_value_id env) s
 
-    method visit_integer_type : 'env -> T.integer_type -> unit = fun _ _ -> ()
-    method visit_scalar_value : 'env -> V.scalar_value -> unit = fun _ _ -> ()
-
     method visit_symbolic_expansion : 'env -> V.symbolic_expansion -> unit =
       fun _ _ -> ()
-
-    method visit_etrait_ref : 'env -> T.etrait_ref -> unit = fun _ _ -> ()
-    method visit_egeneric_args : 'env -> T.egeneric_args -> unit = fun _ _ -> ()
   end
 
 (** **Rem.:** here, {!expression} is not at all equivalent to the expressions
@@ -224,7 +210,7 @@ and loop = {
   fresh_svalues : V.symbolic_value_id_set;
       (** The symbolic values introduced by the loop fixed-point *)
   rg_to_given_back_tys :
-    ((T.RegionId.Set.t * T.rty list) T.RegionGroupId.Map.t[@opaque]);
+    ((T.RegionId.Set.t * T.ty list) T.RegionGroupId.Map.t[@opaque]);
       (** The map from region group ids to the types of the values given back
           by the corresponding loop abstractions.
        *)
@@ -254,13 +240,13 @@ and expansion =
 (* Remark: this type doesn't have to be mutually recursive with the other
    types, but it makes it easy to generate the visitors *)
 and value_aggregate =
-  | SingleValue of V.typed_value  (** Regular case *)
-  | Array of V.typed_value list
+  | VaSingleValue of V.typed_value  (** Regular case *)
+  | VaArray of V.typed_value list
       (** This is used when introducing array aggregates *)
-  | ConstGenericValue of T.const_generic_var_id
+  | VaConstGenericValue of T.const_generic_var_id
       (** This is used when evaluating a const generic value: in the interpreter,
           we introduce a fresh symbolic value. *)
-  | TraitConstValue of T.etrait_ref * T.egeneric_args * string
+  | VaTraitConstValue of T.trait_ref * T.generic_args * string
       (** A trait constant value *)
 [@@deriving
   show,
-- 
cgit v1.2.3


From 0a5859fbb7bcd99bfa221eaf1af029ff660bf963 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 19:35:24 +0100
Subject: Rename some variants

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

(limited to 'compiler/SymbolicAst.ml')

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 927544b2..d114f18d 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -243,7 +243,7 @@ and value_aggregate =
   | VaSingleValue of V.typed_value  (** Regular case *)
   | VaArray of V.typed_value list
       (** This is used when introducing array aggregates *)
-  | VaConstGenericValue of T.const_generic_var_id
+  | VaCGValue of T.const_generic_var_id
       (** This is used when evaluating a const generic value: in the interpreter,
           we introduce a fresh symbolic value. *)
   | VaTraitConstValue of T.trait_ref * T.generic_args * string
-- 
cgit v1.2.3


From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 15 Nov 2023 22:03:21 +0100
Subject: Start updating the name type, cleanup the names and the module
 abbrevs

---
 compiler/SymbolicAst.ml | 91 ++++++++++++++++++++++++-------------------------
 1 file changed, 44 insertions(+), 47 deletions(-)

(limited to 'compiler/SymbolicAst.ml')

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index d114f18d..7c5d28a7 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -3,10 +3,10 @@
     the symbolic execution: we later apply transformations to generate the
     pure AST that we export. *)
 
-module T = Types
-module V = Values
-module E = Expressions
-module A = LlbcAst
+open Types
+open Expressions
+open Values
+open LlbcAst
 
 (** "Meta"-place: a place stored as meta-data.
 
@@ -23,16 +23,16 @@ type mplace = {
           because the most important information in a place is the name of the
           variable!
        *)
-  projection : E.projection;
+  projection : projection;
       (** We store the projection because we can, but it is actually not that useful *)
 }
 [@@deriving show]
 
 type call_id =
-  | Fun of A.fun_id_or_trait_method_ref * V.FunCallId.id
+  | Fun of fun_id_or_trait_method_ref * FunCallId.id
       (** A "regular" function (i.e., a function which is not a primitive operation) *)
-  | Unop of E.unop
-  | Binop of E.binop
+  | Unop of unop
+  | Binop of binop
 [@@deriving show, ord]
 
 type call = {
@@ -42,11 +42,11 @@ type call = {
           evaluated). We need it to compute the translated values for shared
           borrows (we need to perform lookups).
        *)
-  abstractions : V.AbstractionId.id list;
-  generics : T.generic_args;
-  args : V.typed_value list;
+  abstractions : AbstractionId.id list;
+  generics : generic_args;
+  args : typed_value list;
   args_places : mplace option list;  (** Meta information *)
-  dest : V.symbolic_value;
+  dest : symbolic_value;
   dest_place : mplace option;  (** Meta information *)
 }
 [@@deriving show]
@@ -56,14 +56,14 @@ type call = {
  *)
 
 type meta =
-  | Assignment of Contexts.eval_ctx * mplace * V.typed_value * mplace option
+  | Assignment of Contexts.eval_ctx * mplace * typed_value * mplace option
       (** We generated an assignment (destination, assigned value, src) *)
 [@@deriving show]
 
-type variant_id = T.VariantId.id [@@deriving show]
-type global_decl_id = A.GlobalDeclId.id [@@deriving show]
-type 'a symbolic_value_id_map = 'a V.SymbolicValueId.Map.t [@@deriving show]
-type 'a region_group_id_map = 'a T.RegionGroupId.Map.t [@@deriving show]
+type variant_id = VariantId.id [@@deriving show]
+type global_decl_id = GlobalDeclId.id [@@deriving show]
+type 'a symbolic_value_id_map = 'a SymbolicValueId.Map.t [@@deriving show]
+type 'a region_group_id_map = 'a RegionGroupId.Map.t [@@deriving show]
 
 (** Ancestor for {!expression} iter visitor.
 
@@ -73,12 +73,12 @@ type 'a region_group_id_map = 'a T.RegionGroupId.Map.t [@@deriving show]
  *)
 class ['self] iter_expression_base =
   object (self : 'self)
-    inherit [_] V.iter_abs
+    inherit [_] iter_abs
     method visit_eval_ctx : 'env -> Contexts.eval_ctx -> unit = fun _ _ -> ()
     method visit_call : 'env -> call -> unit = fun _ _ -> ()
-    method visit_loop_id : 'env -> V.loop_id -> unit = fun _ _ -> ()
+    method visit_loop_id : 'env -> loop_id -> unit = fun _ _ -> ()
 
-    method visit_region_group_id : 'env -> T.RegionGroupId.id -> unit =
+    method visit_region_group_id : 'env -> RegionGroupId.id -> unit =
       fun _ _ -> ()
 
     method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
@@ -87,7 +87,7 @@ class ['self] iter_expression_base =
     method visit_region_group_id_map
         : 'a. ('env -> 'a -> unit) -> 'env -> 'a region_group_id_map -> unit =
       fun f env m ->
-        T.RegionGroupId.Map.iter
+        RegionGroupId.Map.iter
           (fun id x ->
             self#visit_region_group_id env id;
             f env x)
@@ -96,18 +96,16 @@ class ['self] iter_expression_base =
     method visit_symbolic_value_id_map
         : 'a. ('env -> 'a -> unit) -> 'env -> 'a symbolic_value_id_map -> unit =
       fun f env m ->
-        V.SymbolicValueId.Map.iter
+        SymbolicValueId.Map.iter
           (fun id x ->
             self#visit_symbolic_value_id env id;
             f env x)
           m
 
-    method visit_symbolic_value_id_set : 'env -> V.symbolic_value_id_set -> unit
-        =
-      fun env s ->
-        V.SymbolicValueId.Set.iter (self#visit_symbolic_value_id env) s
+    method visit_symbolic_value_id_set : 'env -> symbolic_value_id_set -> unit =
+      fun env s -> SymbolicValueId.Set.iter (self#visit_symbolic_value_id env) s
 
-    method visit_symbolic_expansion : 'env -> V.symbolic_expansion -> unit =
+    method visit_symbolic_expansion : 'env -> symbolic_expansion -> unit =
       fun _ _ -> ()
   end
 
@@ -116,7 +114,7 @@ class ['self] iter_expression_base =
     lambda-calculus expressions.
  *)
 type expression =
-  | Return of Contexts.eval_ctx * V.typed_value option
+  | Return of Contexts.eval_ctx * typed_value option
       (** There are two cases:
           - the AST is for a forward function: the typed value should contain
             the value which was in the return variable
@@ -128,22 +126,22 @@ type expression =
        *)
   | Panic
   | FunCall of call * expression
-  | EndAbstraction of Contexts.eval_ctx * V.abs * expression
+  | EndAbstraction of Contexts.eval_ctx * abs * expression
       (** The context is the evaluation context upon ending the abstraction,
           just after we removed the abstraction from the context.
 
           The context is the evaluation context from after evaluating the asserted
           value. It has the same purpose as for the {!Return} case.
        *)
-  | EvalGlobal of global_decl_id * V.symbolic_value * expression
+  | EvalGlobal of global_decl_id * symbolic_value * expression
       (** Evaluate a global to a fresh symbolic value *)
-  | Assertion of Contexts.eval_ctx * V.typed_value * expression
+  | Assertion of Contexts.eval_ctx * typed_value * expression
       (** An assertion.
 
           The context is the evaluation context from after evaluating the asserted
           value. It has the same purpose as for the {!Return} case.
        *)
-  | Expansion of mplace option * V.symbolic_value * expansion
+  | Expansion of mplace option * symbolic_value * expansion
       (** Expansion of a symbolic value.
     
           The place is "meta": it gives the path to the symbolic value (if available)
@@ -155,7 +153,7 @@ type expression =
   | IntroSymbolic of
       Contexts.eval_ctx
       * mplace option
-      * V.symbolic_value
+      * symbolic_value
       * value_aggregate
       * expression
       (** We introduce a new symbolic value, equal to some other value.
@@ -171,7 +169,7 @@ type expression =
        *)
   | ForwardEnd of
       Contexts.eval_ctx
-      * V.typed_value symbolic_value_id_map option
+      * typed_value symbolic_value_id_map option
       * expression
       * expression region_group_id_map
       (** We use this delimiter to indicate at which point we switch to the
@@ -193,7 +191,7 @@ type expression =
           comments for the {!Return} variant).
        *)
   | Loop of loop  (** Loop *)
-  | ReturnWithLoop of V.loop_id * bool
+  | ReturnWithLoop of loop_id * bool
       (** End the function with a call to a loop function.
 
           This encompasses the cases when we synthesize a function body
@@ -205,12 +203,12 @@ type expression =
   | Meta of meta * expression  (** Meta information *)
 
 and loop = {
-  loop_id : V.loop_id;
-  input_svalues : V.symbolic_value list;  (** The input symbolic values *)
-  fresh_svalues : V.symbolic_value_id_set;
+  loop_id : loop_id;
+  input_svalues : symbolic_value list;  (** The input symbolic values *)
+  fresh_svalues : symbolic_value_id_set;
       (** The symbolic values introduced by the loop fixed-point *)
   rg_to_given_back_tys :
-    ((T.RegionId.Set.t * T.ty list) T.RegionGroupId.Map.t[@opaque]);
+    ((RegionId.Set.t * ty list) RegionGroupId.Map.t[@opaque]);
       (** The map from region group ids to the types of the values given back
           by the corresponding loop abstractions.
        *)
@@ -220,7 +218,7 @@ and loop = {
 }
 
 and expansion =
-  | ExpandNoBranch of V.symbolic_expansion * expression
+  | ExpandNoBranch of symbolic_expansion * expression
       (** A symbolic expansion which doesn't generate a branching.
           Includes:
           - concrete expansion
@@ -228,25 +226,24 @@ and expansion =
           *Doesn't* include:
           - expansion of ADTs with one variant
        *)
-  | ExpandAdt of (variant_id option * V.symbolic_value list * expression) list
+  | ExpandAdt of (variant_id option * symbolic_value list * expression) list
       (** ADT expansion *)
   | ExpandBool of expression * expression
       (** A boolean expansion (i.e, an [if ... then ... else ...]) *)
-  | ExpandInt of
-      T.integer_type * (V.scalar_value * expression) list * expression
+  | ExpandInt of integer_type * (scalar_value * expression) list * expression
       (** An integer expansion (i.e, a switch over an integer). The last
           expression is for the "otherwise" branch. *)
 
 (* Remark: this type doesn't have to be mutually recursive with the other
    types, but it makes it easy to generate the visitors *)
 and value_aggregate =
-  | VaSingleValue of V.typed_value  (** Regular case *)
-  | VaArray of V.typed_value list
+  | VaSingleValue of typed_value  (** Regular case *)
+  | VaArray of typed_value list
       (** This is used when introducing array aggregates *)
-  | VaCGValue of T.const_generic_var_id
+  | VaCGValue of const_generic_var_id
       (** This is used when evaluating a const generic value: in the interpreter,
           we introduce a fresh symbolic value. *)
-  | VaTraitConstValue of T.trait_ref * T.generic_args * string
+  | VaTraitConstValue of trait_ref * generic_args * string
       (** A trait constant value *)
 [@@deriving
   show,
-- 
cgit v1.2.3


From 672ceef25203ebd5fcf5a55e294a4ebfe65648d6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 20 Nov 2023 21:58:25 +0100
Subject: Use the name matcher implemented in Charon

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

(limited to 'compiler/SymbolicAst.ml')

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 7c5d28a7..c9820ba5 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -240,7 +240,7 @@ and value_aggregate =
   | VaSingleValue of typed_value  (** Regular case *)
   | VaArray of typed_value list
       (** This is used when introducing array aggregates *)
-  | VaCGValue of const_generic_var_id
+  | VaCgValue of const_generic_var_id
       (** This is used when evaluating a const generic value: in the interpreter,
           we introduce a fresh symbolic value. *)
   | VaTraitConstValue of trait_ref * generic_args * string
-- 
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/SymbolicAst.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'compiler/SymbolicAst.ml')

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index c9820ba5..a9f45926 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -51,11 +51,10 @@ type call = {
 }
 [@@deriving show]
 
-(** Meta information, not necessary for synthesis but useful to guide it to
-    generate a pretty output.
+(** Meta information for expressions, not necessary for synthesis but useful to
+    guide it to generate a pretty output.
  *)
-
-type meta =
+type emeta =
   | Assignment of Contexts.eval_ctx * mplace * typed_value * mplace option
       (** We generated an assignment (destination, assigned value, src) *)
 [@@deriving show]
@@ -82,7 +81,8 @@ class ['self] iter_expression_base =
       fun _ _ -> ()
 
     method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
-    method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
+    method visit_emeta : 'env -> emeta -> unit = fun _ _ -> ()
+    method visit_meta : 'env -> Meta.meta -> unit = fun _ _ -> ()
 
     method visit_region_group_id_map
         : 'a. ('env -> 'a -> unit) -> 'env -> 'a region_group_id_map -> unit =
@@ -200,7 +200,7 @@ type expression =
 
           The boolean is [is_continue].
        *)
-  | Meta of meta * expression  (** Meta information *)
+  | Meta of emeta * expression  (** Meta information *)
 
 and loop = {
   loop_id : loop_id;
@@ -215,6 +215,7 @@ and loop = {
   end_expr : expression;
       (** The end of the function (upon the moment it enters the loop) *)
   loop_expr : expression;  (** The symbolically executed loop body *)
+  meta : Meta.meta;  (** Information about where the origin of the loop body *)
 }
 
 and expansion =
-- 
cgit v1.2.3


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

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

(limited to 'compiler/SymbolicAst.ml')

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index a9f45926..53f99b7f 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -66,8 +66,8 @@ type 'a region_group_id_map = 'a RegionGroupId.Map.t [@@deriving show]
 
 (** Ancestor for {!expression} iter visitor.
 
-    We could make it inherit the visitor for {!eval_ctx}, but in all the uses
-    of this visitor we don't need to explore {!eval_ctx}, so we make it inherit
+    We could make it inherit the visitor for {!Contexts.eval_ctx}, but in all the uses
+    of this visitor we don't need to explore {!Contexts.eval_ctx}, so we make it inherit
     the abstraction visitors instead.
  *)
 class ['self] iter_expression_base =
-- 
cgit v1.2.3