diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Pure.ml | 8 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 49 |
2 files changed, 18 insertions, 39 deletions
diff --git a/src/Pure.ml b/src/Pure.ml index 566ba46b..fd1e7763 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -22,7 +22,10 @@ type ty = | Adt of T.type_id * ty list (** [Adt] encodes ADTs, tuples and assumed types. - TODO: what about the ended regions? + TODO: what about the ended regions? (ADTs may be parameterized + with several region variables. When giving back an ADT value, we may + be able to only give back part of the ADT. We need a way to encode + such "partial" ADTs. *) | TypeVar of TypeVarId.id | Bool @@ -110,9 +113,6 @@ type fun_id = type call = { func : fun_id; type_params : ty list; args : typed_rvalue list } -type left_value = unit -(** TODO: assignment left value *) - type let_bindings = | Call of typed_lvalue list * call (** The called function and the tuple of returned values. *) diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index dc792701..a77a64ca 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -79,9 +79,7 @@ let translate_fun_name (fdef : A.fun_def) (bid : T.RegionGroupId.id option) : (* Exactly one backward function *) "_back" | _ -> - (* Several backward functions - note that **we use the backward function id - * as if it were a region group id** (there is a direct mapping between the - * two - TODO: merge them) *) + (* Several backward functions *) let rg = T.RegionGroupId.nth sg.regions_hierarchy bid in "_back" ^ rg_to_string rg) in @@ -126,15 +124,6 @@ type fun_context = { fun_defs : fun_def FunDefId.Map.t; } -(* TODO: do we really need that actually? *) -type synth_ctx = { - names : NameMap.t; - (* TODO: remove? *) - type_context : type_context; - fun_context : fun_context; - declarations : M.declaration_group list; -} - type call_info = { forward : S.call; backwards : V.abs T.RegionGroupId.Map.t; @@ -382,8 +371,6 @@ let rec translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool) (** Small utility: list the transitive parents of a region var group. We don't do that in an efficient manner, but it doesn't matter. - - TODO: remove? *) let rec list_parent_region_groups (def : A.fun_def) (gid : T.RegionGroupId.id) : T.RegionGroupId.Set.t = @@ -401,10 +388,7 @@ let rec list_parent_region_groups (def : A.fun_def) (gid : T.RegionGroupId.id) : in parents -(** Small utility: same as [list_parent_region_groups], but returns an ordered list. - - TODO: remove? - *) +(** Small utility: same as [list_parent_region_groups], but returns an ordered list. *) let list_ordered_parent_region_groups (def : A.fun_def) (gid : T.RegionGroupId.id) : T.RegionGroupId.id list = let pset = list_parent_region_groups def gid in @@ -531,8 +515,7 @@ let fresh_vars_for_symbolic_values (svl : V.symbolic_value list) (ctx : bs_ctx) : bs_ctx * var list = List.fold_left_map (fun ctx sv -> fresh_var_for_symbolic_value sv ctx) ctx svl -(* TODO: rename *) -let get_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var = +let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var = V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var (** Translate a typed value. @@ -553,12 +536,10 @@ let get_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var = TODO: we have a problem with shared borrows. I think the shared borrows should carry the shared value as a meta-value. - - TODO: rename: remove the "translate_" prefix *) -let rec translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : - typed_rvalue = - let translate = translate_typed_value_to_rvalue ctx in +let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue + = + let translate = typed_value_to_rvalue ctx in let value = match v.value with | V.Concrete cv -> RvConcrete cv @@ -581,7 +562,7 @@ let rec translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : (* Borrows are the identity in the extraction *) (translate v).value) | Symbolic sv -> - let var = get_var_for_symbolic_value sv ctx in + let var = lookup_var_for_symbolic_value sv ctx in (mk_typed_rvalue_from_var var).value in let ty = translate_fwd_ty ctx v.ty in @@ -637,7 +618,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (lc : V.aloan_content) : | AMutLoan (_, _) | ASharedLoan (_, _, _) -> failwith "Unreachable" | AEndedMutLoan { child = _; given_back = _; given_back_meta } -> (* Return the meta-value *) - Some (translate_typed_value_to_rvalue ctx given_back_meta) + Some (typed_value_to_rvalue ctx given_back_meta) | AEndedSharedLoan (_, _) -> (* We don't dive into shared loans: there is nothing to give back * inside (note that there could be a mutable borrow in the shared @@ -674,12 +655,12 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : typed_rvalue option = match aproj with | V.AEndedProjLoans (msv, []) -> (* The symbolic value was left unchanged *) - let var = get_var_for_symbolic_value msv ctx in + let var = lookup_var_for_symbolic_value msv ctx in Some (mk_typed_rvalue_from_var var) | V.AEndedProjLoans (_, [ (mnv, child_aproj) ]) -> assert (child_aproj = AIgnoredProjBorrows); (* The symbolic value was updated *) - let var = get_var_for_symbolic_value mnv ctx in + let var = lookup_var_for_symbolic_value mnv ctx in Some (mk_typed_rvalue_from_var var) | V.AEndedProjLoans (_, _) -> (* The symbolic value was updated, and the given back values come from sevearl @@ -819,7 +800,7 @@ 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_to_rvalue ctx v in + let v = typed_value_to_rvalue ctx v in Return v | Panic -> Panic | FunCall (call, e) -> translate_function_call call e ctx @@ -833,7 +814,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_to_rvalue ctx) call.args in + let args = List.map (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 *) @@ -867,9 +848,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : (* 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_to_rvalue ctx) forward.args - in + let fwd_inputs = List.map (typed_value_to_rvalue ctx) forward.args in let back_ancestors_inputs = List.concat (List.map (abs_to_consumed ctx) backwards) in @@ -943,7 +922,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : 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_var = lookup_var_for_symbolic_value sv ctx in let scrutinee = mk_typed_rvalue_from_var scrutinee_var in (* Translate the branches *) match exp with |