summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterBorrows.ml2
-rw-r--r--compiler/InterpreterLoops.ml3
-rw-r--r--compiler/InterpreterProjectors.ml3
-rw-r--r--compiler/Invariants.ml2
-rw-r--r--compiler/Print.ml1
-rw-r--r--compiler/SymbolicToPure.ml4
-rw-r--r--compiler/Values.ml13
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