diff options
Diffstat (limited to 'compiler/Values.ml')
| -rw-r--r-- | compiler/Values.ml | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/compiler/Values.ml b/compiler/Values.ml index 5473ce3e..e7b96051 100644 --- a/compiler/Values.ml +++ b/compiler/Values.ml @@ -153,11 +153,11 @@ and typed_value = { value : value; ty : ty } (** "Meta"-value: information we store for the synthesis. - Note that we never automatically visit the meta-values with the - visitors: they really are meta information, and shouldn't be considered + Note that we never automatically visit the span-values with the + visitors: they really are span information, and shouldn't be considered as part of the environment during a symbolic execution. - TODO: we may want to create wrappers, to prevent accidently mixing meta + TODO: we may want to create wrappers, to prevent accidently mixing span values and regular values. *) type mvalue = typed_value [@@deriving show, ord] @@ -166,7 +166,7 @@ type mvalue = typed_value [@@deriving show, ord] See the explanations for {!mvalue} - TODO: we may want to create wrappers, to prevent mixing meta values + TODO: we may want to create wrappers, to prevent mixing span values and regular values. *) type msymbolic_value = symbolic_value [@@deriving show, ord] @@ -270,7 +270,7 @@ and aproj = 'a and one for 'b. We accumulate those values in the list of projections (note that - the meta value stores the value which was given back). + the span value stores the value which was given back). We can later end the projector of loans if [s@0] is not referenced anywhere in the context below a projector of borrows which intersects @@ -282,14 +282,14 @@ and aproj = Also note that once given to a borrow projection, a symbolic value can't get updated/expanded: this means that we don't need to save - any meta-value here. + any span-value here. *) | AEndedProjLoans of msymbolic_value * (msymbolic_value * aproj) list (** An ended projector of loans over a symbolic value. See the explanations for {!AProjLoans} - Note that we keep the original symbolic value as a meta-value. + Note that we keep the original symbolic value as a span-value. *) | AEndedProjBorrows of msymbolic_value (** The only purpose of {!AEndedProjBorrows} is to store, for synthesis @@ -376,7 +376,7 @@ and aloan_content = | AEndedMutLoan of { child : typed_avalue; given_back : typed_avalue; - given_back_meta : mvalue; + given_back_span : mvalue; } (** An ended mutable loan in an abstraction. We need it because abstractions must keep track of the values @@ -401,7 +401,7 @@ and aloan_content = After ending [l0]: {[ - abs0 { a_ended_mut_loan { child = _; given_back = _; given_back_meta = U32 3; } + abs0 { a_ended_mut_loan { child = _; given_back = _; given_back_span = U32 3; } x -> ⊥ ]} @@ -420,7 +420,7 @@ and aloan_content = a_ended_mut_loan { child = _; given_back = a_mut_borrow l1 _; - given_back_meta = (mut_borrow l1 (U32 3)); + given_back_span = (mut_borrow l1 (U32 3)); } } ... @@ -464,7 +464,7 @@ and aloan_content = a_ended_ignored_mut_loan { child = a_mut_loan l1 _; given_back = a_mut_borrow l1 _; - given_back_meta = mut_borrow l1 @s1 + given_back_span = mut_borrow l1 @s1 } } x -> ⊥ @@ -474,7 +474,7 @@ and aloan_content = | AEndedIgnoredMutLoan of { child : typed_avalue; given_back : typed_avalue; - given_back_meta : mvalue; + given_back_span : mvalue; } (** Similar to {!AEndedMutLoan}, for ignored loans. See the comments for {!AIgnoredMutLoan}. @@ -613,7 +613,7 @@ and aborrow_content = *) | AEndedMutBorrow of msymbolic_value * typed_avalue (** The sole purpose of {!AEndedMutBorrow} is to store the (symbolic) value - that we gave back as a meta-value, to help with the synthesis. + that we gave back as a span-value, to help with the synthesis. *) | AEndedSharedBorrow (** We don't really need {!AEndedSharedBorrow}: we simply want to be @@ -622,8 +622,8 @@ and aborrow_content = | AEndedIgnoredMutBorrow of { child : typed_avalue; given_back : typed_avalue; - given_back_meta : msymbolic_value; - (** [given_back_meta] is used to store the (symbolic) value we gave back + given_back_span : msymbolic_value; + (** [given_back_span] is used to store the (symbolic) value we gave back upon ending the borrow. Rk.: *DO NOT* use [visit_AEndedIgnoredMutLoan]. |