diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Expressions.ml | 5 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 14 | ||||
| -rw-r--r-- | src/LlbcOfJson.ml | 4 | ||||
| -rw-r--r-- | src/Print.ml | 12 | ||||
| -rw-r--r-- | src/Substitute.ml | 10 |
5 files changed, 37 insertions, 8 deletions
diff --git a/src/Expressions.ml b/src/Expressions.ml index a118ca67..61a2f95c 100644 --- a/src/Expressions.ml +++ b/src/Expressions.ml @@ -16,11 +16,8 @@ type projection_elem = [@@deriving show] type projection = projection_elem list [@@deriving show] - type place = { var_id : VarId.id; projection : projection } [@@deriving show] - type borrow_kind = Shared | Mut | TwoPhaseMut [@@deriving show] - type unop = Not | Neg [@@deriving show, ord] (** A binary operation @@ -118,6 +115,8 @@ type operand = *) type aggregate_kind = | AggregatedTuple + | AggregatedOption of VariantId.id * ety + (* TODO: AggregatedOption should be merged with AggregatedAdt *) | AggregatedAdt of TypeDeclId.id * VariantId.id option * erased_region list * ety list [@@deriving show] diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index f4d97b9d..e46ca721 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -608,6 +608,20 @@ let eval_rvalue_aggregate (config : C.config) let aggregated : V.typed_value = { V.value = v; ty } in (* Call the continuation *) cf aggregated ctx + | E.AggregatedOption (variant_id, ty) -> + (* Sanity check *) + if variant_id == T.option_none_id then assert (values == []) + else if variant_id == T.option_some_id then + assert (List.length values == 1) + else raise (Failure "Unreachable"); + (* Construt the value *) + let aty = T.Adt (T.Assumed T.Option, [], [ ty ]) in + let av : V.adt_value = + { V.variant_id = Some variant_id; V.field_values = values } + in + let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in + (* Call the continuation *) + cf aggregated ctx | E.AggregatedAdt (def_id, opt_variant_id, regions, types) -> (* Sanity checks *) let type_decl = C.ctx_lookup_type_decl ctx def_id in diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index 75e9cbf7..32ca802e 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -423,6 +423,10 @@ let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result = combine_error_msgs js "operand_kind_of_json" (match js with | `String "AggregatedTuple" -> Ok E.AggregatedTuple + | `Assoc [ ("AggregatedOption", `List [ variant_id; ty ]) ] -> + let* variant_id = T.VariantId.id_of_json variant_id in + let* ty = ety_of_json ty in + Ok (E.AggregatedOption (variant_id, ty)) | `Assoc [ ("AggregatedAdt", `List [ id; opt_variant_id; regions; tys ]) ] -> let* id = T.TypeDeclId.id_of_json id in diff --git a/src/Print.ml b/src/Print.ml index 8df3001f..0c4ef20a 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -12,7 +12,6 @@ let option_to_string (to_string : 'a -> string) (x : 'a option) : string = match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None" let name_to_string (name : name) : string = Names.name_to_string name - let fun_name_to_string (name : fun_name) : string = name_to_string name (** Pretty-printing for types *) @@ -48,9 +47,7 @@ module Types = struct } type stype_formatter = T.RegionVarId.id T.region type_formatter - type rtype_formatter = T.RegionId.id T.region type_formatter - type etype_formatter = T.erased_region type_formatter let integer_type_to_string = function @@ -906,6 +903,15 @@ module LlbcAst = struct let ops = List.map (operand_to_string fmt) ops in match akind with | E.AggregatedTuple -> "(" ^ String.concat ", " ops ^ ")" + | E.AggregatedOption (variant_id, _ty) -> + if variant_id == T.option_none_id then ( + assert (ops == []); + "@Option::None") + else if variant_id == T.option_some_id then ( + assert (List.length ops == 1); + let op = List.hd ops in + "@Option::Some(" ^ op ^ ")") + else raise (Failure "Unreachable") | E.AggregatedAdt (def_id, opt_variant_id, _regions, _types) -> let adt_name = fmt.type_decl_id_to_string def_id in let variant_name = diff --git a/src/Substitute.ml b/src/Substitute.ml index c76f1da4..711e438b 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -121,7 +121,10 @@ let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl) variants | T.Struct fields -> [ (None, fields) ] | T.Opaque -> - raise (Failure ("Can't retrieve the variants of an opaque type: " ^ Names.name_to_string def.name)) + raise + (Failure + ("Can't retrieve the variants of an opaque type: " + ^ Names.name_to_string def.name)) in List.map (fun (id, fields) -> @@ -243,8 +246,11 @@ let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety) (rv : E.rvalue) : let kind = match kind with | E.AggregatedTuple -> E.AggregatedTuple + | E.AggregatedOption (variant_id, ty) -> + let rsubst r = r in + E.AggregatedOption (variant_id, ty_substitute rsubst tsubst ty) | E.AggregatedAdt (def_id, variant_id, regions, tys) -> - let rsubst x = x in + let rsubst r = r in E.AggregatedAdt ( def_id, variant_id, |