Introduce lvalues and rvalues in Pure.ml

2 files changed, 91 insertions, 56 deletions

diff --git a/src/Pure.ml b/src/Pure.ml
index 869729a1..504f2c11 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -15,9 +15,6 @@ module SynthPhaseId = IdGen ()
 (** We give an identifier to every phase of the synthesis (forward, backward
     for group of regions 0, etc.) *)
 
-module BackwardFunId = IdGen ()
-(** Every backward function has its identifier *)
-
 module VarId = IdGen ()
 (** Pay attention to the fact that we also define a [VarId] module in Values *)
 
@@ -66,7 +63,7 @@ type symbolic_value = {
           symbolic value was introduced.
        *)
 }
-(** TODO: remove? *)
+(** TODO: remove *)
 
 type value = Concrete of constant_value | Adt of adt_value
 
@@ -83,11 +80,14 @@ type var = { id : VarId.id; ty : ty }
     itself
  *)
 
-(** Sometimes, when introducing several variables in an assignment (because
-    deconstructing a tuple) we can ignore some of the values: in such situation
-    we introduce dummy variables (extracted to "_").
- *)
-type var_or_dummy = Var of var | Dummy
+type var_or_dummy = Var of var | Dummy  (** Ignored value: `_` *)
+
+(** A left value (which appears on the left of assignments *)
+type lvalue =
+  | LvVar of var_or_dummy
+  | LvTuple of lvalue list  (** Rk.: for now we don't support general ADTs *)
+
+and typed_lvalue = { value : lvalue; ty : ty }
 
 type projection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id }
 
@@ -95,34 +95,41 @@ type projection = projection_elem list
 
 type place = { var : VarId.id; projection : projection }
 
-(* TODO: this doesn't make sense: value can contain variables... *)
-type operand = Value of typed_value | Place of place
+type rvalue =
+  | RvPlace of place
+  | RvConcrete of constant_value
+  | RvAdt of adt_rvalue
 
-(* type assertion = { cond : operand; expected : bool } *)
+and adt_rvalue = {
+  variant_id : (VariantId.id option[@opaque]);
+  field_values : typed_rvalue list;
+}
+
+and typed_rvalue = { value : rvalue; ty : ty }
+(** In most situations we won't use the type in [typed_rvalue].
+    Note that it is still necessary to have some useful informations
+    about ADTs, though.
+ *)
 
 type fun_id =
-  | Local of A.FunDefId.id * BackwardFunId.id option
+  | Regular of A.fun_id * T.RegionGroupId.id option
       (** Backward id: `Some` if the function is a backward function, `None`
           if it is a forward function *)
-  | Assumed of A.assumed_fun_id
   | Unop of E.unop
   | Binop of E.binop
 
-type call = { func : fun_id; type_params : ty list; args : operand list }
+type call = { func : fun_id; type_params : ty list; args : typed_rvalue list }
 
 type left_value = unit
 (** TODO: assignment left value *)
 
-type lvalue = typed_value
-(* TODO: define that *)
-
 type let_bindings =
-  | Call of lvalue list * call
+  | Call of typed_lvalue list * call
       (** The called function and the tuple of returned values. *)
-  | Assignment of var * operand
+  | Assignment of var * typed_rvalue
       (** Variable assignment: the introduced variable and the place we read *)
   | Deconstruct of
-      var_or_dummy list * (TypeDefId.id * VariantId.id) option * operand
+      var_or_dummy list * (TypeDefId.id * VariantId.id) option * typed_rvalue
       (** This is used in two cases.
 
           1. When deconstructing a tuple:
@@ -159,11 +166,11 @@ type let_bindings =
     more general than the CFIM statements, in a sense.
  *)
 type expression =
-  | Return of operand
+  | Return of typed_rvalue
   | Panic
   | Let of let_bindings * expression
       (** Let bindings include the let-bindings introduced because of function calls *)
-  | Switch of operand * switch_body
+  | Switch of typed_rvalue * switch_body
 
 and switch_body =
   | If of expression * expression
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 97d9baf1..a8e5be0d 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -97,6 +97,24 @@ let translate_fun_name (fdef : A.fun_def) (bid : T.RegionGroupId.id option) :
 (** Generates a name for a type (simply reuses the name in the definition) *)
 let translate_type_name (def : T.type_def) : Id.name = def.T.name
 
+(* TODO: move *)
+let mk_place_from_var (v : var) : place = { var = v.id; projection = [] }
+
+let mk_typed_rvalue_from_var (v : var) : typed_rvalue =
+  let value = RvPlace (mk_place_from_var v) in
+  let ty = v.ty in
+  { value; ty }
+
+(* TODO: move *)
+let type_def_is_enum (def : T.type_def) : bool =
+  match def.kind with T.Struct _ -> false | Enum _ -> true
+
+(* TODO: move *)
+let mk_typed_lvalue_from_var (v : var) : typed_lvalue =
+  let value = LvVar (Var v) in
+  let ty = v.ty in
+  { value; ty }
+
 type type_context = {
   types_infos : TA.type_infos;
   cfim_type_defs : T.type_def TypeDefId.Map.t;
@@ -154,7 +172,8 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
   let calls = V.FunCallId.Map.add call_id info calls in
   { ctx with calls }
 
-let bs_ctx_register_backward_call (abs : V.abs) (ctx : bs_ctx) : bs_ctx =
+let bs_ctx_register_backward_call (abs : V.abs) (ctx : bs_ctx) : bs_ctx * fun_id
+    =
   (* Insert the abstraction in the call informations *)
   let back_id = Option.get abs.back_id in
   let info = V.FunCallId.Map.find abs.call_id ctx.calls in
@@ -166,8 +185,14 @@ let bs_ctx_register_backward_call (abs : V.abs) (ctx : bs_ctx) : bs_ctx =
   let abstractions = ctx.abstractions in
   assert (not (V.AbstractionId.Map.mem abs.abs_id abstractions));
   let abstractions = V.AbstractionId.Map.add abs.abs_id abs abstractions in
-  (* Update the context *)
-  { ctx with calls; abstractions }
+  (* Retrieve the fun_id *)
+  let fun_id =
+    match info.forward.call_id with
+    | S.Fun (fid, _) -> Regular (fid, Some (Option.get abs.back_id))
+    | S.Unop _ | S.Binop _ -> failwith "Unreachable"
+  in
+  (* Update the context and return *)
+  ({ ctx with calls; abstractions }, fun_id)
 
 let rec translate_sty (ty : T.sty) : ty =
   let translate = translate_sty in
@@ -447,7 +472,8 @@ let translate_fun_sig (ctx : bs_ctx) (def : A.fun_def)
     - end abstraction
     - return
  *)
-let translate_typed_value (ctx : bs_ctx) (v : V.typed_value) : typed_value =
+let translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) :
+    typed_rvalue =
   raise Unimplemented
 
 let fresh_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) :
@@ -461,25 +487,19 @@ let fresh_vars_for_symbolic_values (svl : V.symbolic_value list) (ctx : bs_ctx)
 let get_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
   raise Unimplemented
 
-(* TODO: move *)
-let mk_place_from_var (v : var) : place = { var = v.id; projection = [] }
-
-(* TODO: move *)
-let type_def_is_enum (def : T.type_def) : bool =
-  match def.kind with T.Struct _ -> false | Enum _ -> true
-
 let typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
-    typed_value option =
+    typed_rvalue option =
   raise Unimplemented
 
-let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : typed_value list =
+let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : typed_rvalue list =
   List.filter_map (typed_avalue_to_consumed ctx) abs.avalues
 
 let typed_avalue_to_given_back (av : V.typed_avalue) (ctx : bs_ctx) :
-    bs_ctx * lvalue option =
+    bs_ctx * typed_lvalue option =
   raise Unimplemented
 
-let abs_to_given_back (abs : V.abs) (ctx : bs_ctx) : bs_ctx * lvalue list =
+let abs_to_given_back (abs : V.abs) (ctx : bs_ctx) : bs_ctx * typed_lvalue list
+    =
   let ctx, values =
     List.fold_left_map
       (fun ctx av -> typed_avalue_to_given_back av ctx)
@@ -501,8 +521,8 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) : S.call * V.abs list =
 let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression =
   match e with
   | S.Return v ->
-      let v = translate_typed_value ctx v in
-      Return (Value v)
+      let v = translate_typed_value_to_rvalue ctx v in
+      Return v
   | Panic -> Panic
   | FunCall (call, e) -> translate_function_call call e ctx
   | EndAbstraction (abs, e) -> translate_end_abstraction abs e ctx
@@ -515,8 +535,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     expression =
   (* Translate the function call *)
   let type_params = List.map (translate_fwd_ty ctx) call.type_params in
-  let args = List.map (translate_typed_value ctx) call.args in
-  let args = List.map (fun v -> Value v) args in
+  let args = List.map (translate_typed_value_to_rvalue ctx) call.args in
   let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
   (* Retrieve the function id, and register the function call in the context
    * if necessary *)
@@ -524,11 +543,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     match call.call_id with
     | S.Fun (fid, call_id) ->
         let ctx = bs_ctx_register_forward_call call_id call ctx in
-        let func =
-          match fid with
-          | A.Local fid -> Local (fid, None)
-          | A.Assumed fid -> Assumed fid
-        in
+        let func = Regular (fid, None) in
         (ctx, func)
     | S.Unop unop -> (ctx, Unop unop)
     | S.Binop binop -> (ctx, Binop binop)
@@ -537,7 +552,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
   (* Translate the next expression *)
   let e = translate_expression e ctx in
   (* Put together *)
-  Let (Call ([ Var dest ], call), e)
+  Let (Call ([ mk_typed_lvalue_from_var dest ], call), e)
 
 and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
     expression =
@@ -546,24 +561,32 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
       (* There are no nested borrows for now: we shouldn't get there *)
       raise Unimplemented
   | V.FunCall ->
+      let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in
+      let call = call_info.forward in
+      let type_params = List.map (translate_fwd_ty ctx) call.type_params in
       (* Retrive the orignal call and the parent abstractions *)
       let forward, backwards = get_abs_ancestors ctx abs in
       (* Retrieve the values consumed when we called the forward function and
        * ended the parent backward functions: those give us part of the input
        * values *)
-      let fwd_inputs = List.map (translate_typed_value ctx) forward.args in
+      let fwd_inputs =
+        List.map (translate_typed_value_to_rvalue ctx) forward.args
+      in
       let back_ancestors_inputs =
-        List.concat (List.map abs_to_consumed backwards)
+        List.concat (List.map (abs_to_consumed ctx) backwards)
       in
       (* Retrieve the values consumed upon ending the loans inside this
        * abstraction: those give us the remaining input values *)
-      let back_inputs = abs_to_consumed abs in
+      let back_inputs = abs_to_consumed ctx abs in
       let inputs =
         List.concat [ fwd_inputs; back_ancestors_inputs; back_inputs ]
       in
       (* Retrieve the values given back by this function: those are the output
        * values *)
       let ctx, outputs = abs_to_given_back abs ctx in
+      (* Retrieve the function id, and register the function call in the context
+       * if necessary *)
+      let ctx, func = bs_ctx_register_backward_call abs ctx in
       (* Translate the next expression *)
       let e = translate_expression e ctx in
       (* Put everything together *)
@@ -577,7 +600,7 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
     (ctx : bs_ctx) : expression =
   (* Translate the scrutinee *)
   let scrutinee_var = get_var_for_symbolic_value sv ctx in
-  let scrutinee = Place (mk_place_from_var scrutinee_var) in
+  let scrutinee = mk_typed_rvalue_from_var scrutinee_var in
   (* Translate the branches *)
   match exp with
   | ExpandNoBranch (sexp, e) -> (
@@ -617,18 +640,23 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
                     branch )
               else
                 (* This is not an enumeration: introduce let-bindings for every
-                 * field *)
-                let gen_field_proj (field_id : FieldId.id) : operand =
+                 * field.
+                 * We use the [dest] variable in order not to have to recompute
+                 * the type of the result of the projection... *)
+                let gen_field_proj (field_id : FieldId.id) (dest : var) :
+                    typed_rvalue =
                   let pkind = E.ProjAdt (adt_id, None) in
                   let pe : projection_elem = { pkind; field_id } in
                   let projection = [ pe ] in
                   let place = { var = scrutinee_var.id; projection } in
-                  Place place
+                  let value = RvPlace place in
+                  let ty = dest.ty in
+                  { value; ty }
                 in
                 let id_var_pairs = FieldId.mapi (fun fid v -> (fid, v)) vars in
                 List.fold_right
                   (fun (fid, var) e ->
-                    let field_proj = gen_field_proj fid in
+                    let field_proj = gen_field_proj fid var in
                     Let (Assignment (var, field_proj), e))
                   id_var_pairs branch
           | T.Tuple ->