diff options
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 3 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 3 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 2 | ||||
| -rw-r--r-- | compiler/Print.ml | 1 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 4 | ||||
| -rw-r--r-- | compiler/Values.ml | 13 |
7 files changed, 3 insertions, 25 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 64f379be..c71abe25 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -1595,7 +1595,7 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool) (av : V.typed_avalue) : unit = let ty = av.V.ty in match av.V.value with - | V.APrimitive _ | ABottom | AIgnored -> () + | ABottom | AIgnored -> () | AAdt adt -> (* Simply explore the children *) List.iter (list_avalues allow_borrows push) adt.field_values diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 142bf4e7..f0a7fdbd 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -674,9 +674,6 @@ module Match (M : Matcher) = struct let match_arec = match_typed_avalues ctx in let ty = M.match_rtys v0.V.ty v1.V.ty in match (v0.V.value, v1.V.value) with - | V.APrimitive _, V.APrimitive _ -> - (* We simply ignore - those are actually not used *) - mk_aignored ty | V.AAdt av0, V.AAdt av1 -> if av0.variant_id = av1.variant_id then let fields = List.combine av0.field_values av1.field_values in diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index 335ebcf4..a69052cb 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -102,8 +102,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) else let value : V.avalue = match (v.V.value, ty) with - | V.Primitive cv, (T.Bool | T.Char | T.Integer _ | T.Str) -> - V.APrimitive cv + | V.Primitive _, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.AIgnored | V.Adt adt, T.Adt (id, region_params, tys) -> (* Retrieve the types of the fields *) let field_types = diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 370b0d01..3fdb963a 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -501,8 +501,6 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = method! visit_typed_avalue info atv = (* Check the current pair (value, type) *) (match (atv.V.value, atv.V.ty) with - | V.APrimitive cv, ty -> - check_primitive_value_type cv (Subst.erase_regions ty) (* ADT case *) | V.AAdt av, T.Adt (T.AdtId def_id, regions, tys) -> (* Retrieve the definition to check the variant id, the number of diff --git a/compiler/Print.ml b/compiler/Print.ml index 1de1bf9c..88d33bce 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -178,7 +178,6 @@ module Values = struct string = let ty_fmt : PT.rtype_formatter = value_to_rtype_formatter fmt in match v.value with - | APrimitive cv -> PPV.primitive_value_to_string cv | AAdt av -> ( let field_values = List.map (typed_avalue_to_string fmt) av.field_values diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 3f654a1d..81cc22e1 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -875,7 +875,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) (** Explore an abstraction value and convert it to a consumed value by collecting all the meta-values from the ended *loans*. - Consumed values are rvalues, because when an abstraction ends, we + Consumed values are rvalues because when an abstraction ends we introduce a call to a backward function in the synthesized program, which takes as inputs those consumed values: {[ @@ -892,7 +892,6 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) let translate = typed_avalue_to_consumed ctx ectx in let value = match av.value with - | APrimitive _ -> raise (Failure "Unreachable") | AAdt adt_v -> ( (* Translate the field values *) let field_values = List.filter_map translate adt_v.field_values in @@ -1027,7 +1026,6 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) (ctx : bs_ctx) : bs_ctx * typed_pattern option = let ctx, value = match av.value with - | APrimitive _ -> raise (Failure "Unreachable") | AAdt adt_v -> ( (* Translate the field values *) (* For now we forget the meta-place information so that it doesn't get used diff --git a/compiler/Values.ml b/compiler/Values.ml index 30e4f05d..7f6808ae 100644 --- a/compiler/Values.ml +++ b/compiler/Values.ml @@ -482,19 +482,6 @@ class ['self] map_typed_avalue_base = part of it is thus "abstracted" away. *) type avalue = - | APrimitive of primitive_value - (** TODO: remove. We actually don't use that for the synthesis, but the - meta-values. - - Note that this case is not used in the projections to keep track of the - borrow graph (because there are no borrows in "concrete" values!) but - to correctly instantiate the backward functions (we may give back some - values at different moments: we need to remember what those values were - precisely). Also note that even though avalues and values are not the - same, once values are projected to avalues, those avalues still have - the structure of the original values (this is necessary, again, to - correctly instantiate the backward functions) - *) | AAdt of adt_avalue | ABottom | ALoan of aloan_content |