From 4de9c41813fccd90be93cbeabc45ccc37b4d1e32 Mon Sep 17 00:00:00 2001 From: zerbina <100542850+zerbina@users.noreply.github.com> Date: Thu, 26 Sep 2024 20:07:29 +0000 Subject: [PATCH 1/4] spec: prepare for variables and parameters Summary ======= * subdivide expressions into l-value and r-value expressions * add definitions for values, locations, and cells * introduce the notion of linear, affine, and normal types Details ======= Some definitions and terminology was missing to be able to describe / specify the semantics of variables and assignments. This commit aims to extend the specification with the necessary bits. As a preparation for future resource management, linear and affine types are introduced already, though they're not of practical relevance yet. --- spec/spec.md | 77 ++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 71 insertions(+), 6 deletions(-) diff --git a/spec/spec.md b/spec/spec.md index 0c6943b..1d84e0b 100644 --- a/spec/spec.md +++ b/spec/spec.md @@ -11,6 +11,14 @@ the given name. An *expression* is a term or a control-flow instruction. All expressions have a *type*. +Expressions are further subdivided into: +* *l-value* expressions: an expression that refers to a location +* *r-value* expressions: an expression that produces a new value +* `void` expressions: control-flow instructions that don't produce a value + +> TODO: reorder the definitions such that the term "locations" is defined +> before it's used here + A *statement* is a computation without a type. > Note: at the moment, the grammar describes the grammar of the parse-tree, @@ -58,6 +66,40 @@ the same type. `union(...)` is the supertype of all its operand types. +### Values, Locations, and Cells + +A *value* is something that inhabits a type. They're either constructed +implicitly or are produced by terms. An *aggregate value* is a value +inhabiting a composite type. + +*Values* are stored in *locations*. If a location stores an aggregate value, +it consists of one or more sub-locations. A location not part of any other +location is called a *cell*. + +Every implicitly or explicitly constructed value has a unique *identity*, +meaning two separate values cannot be the *same*, but they can be *equal*. + +Changing the value stored in a sub-location also modifies the value of the +parent location, but without changing its *identity*. + +### Normal, Linear, and Affine Types + +How a value inhabiting a type is allowed to be used depends on whether the +type is a normal, linear, or affine type: + +| Type | No Use | Single Use | Multi Use | +| ------ | ------ | ---------- | --------- | +| Normal | Yes | Yes | Yes | +| Affine | Yes | Yes | No | +| Linear | No | Yes | No | + +What constitutes a *use* of a value is described in this document. + +Using an r-value expression means using the value it produces. Using an l- +value expression means using the value stored in the named location. + +> note: at the moment, all types are *normal* types + ### Lookup *Entities* are part of *scopes*. They're queried from their scope via their @@ -84,6 +126,9 @@ the `true` or `false` value, respectively. Otherwise, an error is reported. +**Expression kind**: r-value +**Uses**: nothing + #### Literals ```grammar @@ -94,6 +139,9 @@ expr += The `IntVal` expression always has type `int`, `FloatVal` always type `float`. +**Expression kind**: r-value +**Uses**: nothing + #### `Return` ```grammar @@ -109,6 +157,9 @@ is reported if: The type of the `Return` expression is `void`. It returns control from the current procedure to its caller. +**Expression kind**: `void` +**Uses**: `expr`, if present + #### `Unreachable` ```grammar @@ -122,6 +173,9 @@ an `Unreachable` expression within a procedure. The type of the `Unreachable` expression is `void`. +**Expression kind**: `void` +**Uses**: nothing + #### Calls ```grammar @@ -149,21 +203,29 @@ After evaluating the arguments (if any), control is passed to the callee. > TODO: specification for the built-in operations is missing +**Expression kind**: r-value or `void`, depending on the return type +**Uses**: each argument expression + #### Tuple Constructors ```grammar -expr += (TupleCons) # first form - | (TupleCons +) # second form +expr += (TupleCons) ``` -The first form constructs a value of type `unit`. +Constructs a value of type `unit`. -The second form construct a value of type `tuple(T1..Tn)`, where `T1` is the -type of the first expression, `T2` the type of the second expression (if any), -and so on. +```grammar +expr += (TupleCons +) +``` + +Constructs a value of type `tuple(T0..Tn)`, where `T0` is the type of the first +expression, `T1` the type of the second expression (if any), and so on. An error is reported if any `Tx` is `void`. +**Expression kind**: r-value +**Uses**: each operand expression + #### Tuple Elimination ```grammar @@ -179,6 +241,9 @@ to the number of positions in the tuple type `T`, an error is reported. Given type `tuple(T[0], .., T[n])` for `T`, the type of the expression is `T[index]`. +**Expression kind**: same as `tup` +**Uses**: nothing + ### Type Expressions ```grammar From f7097d5d691d0c238d0dbf56892e0f0f728bc1bf Mon Sep 17 00:00:00 2001 From: zerbina <100542850+zerbina@users.noreply.github.com> Date: Fri, 27 Sep 2024 21:01:08 +0000 Subject: [PATCH 2/4] spec: don't overload "value"; use "object" instead "object" is also not ideal, but it's a bit better than "value" and should do for now. --- spec/spec.md | 36 ++++++++++++++++++++++-------------- 1 file changed, 22 insertions(+), 14 deletions(-) diff --git a/spec/spec.md b/spec/spec.md index 1d84e0b..7a663f5 100644 --- a/spec/spec.md +++ b/spec/spec.md @@ -66,26 +66,34 @@ the same type. `union(...)` is the supertype of all its operand types. -### Values, Locations, and Cells +### Values, Objects, Locations, and Cells -A *value* is something that inhabits a type. They're either constructed -implicitly or are produced by terms. An *aggregate value* is a value +A *value* is something that inhabits a type. An *aggregate value* is a value inhabiting a composite type. -*Values* are stored in *locations*. If a location stores an aggregate value, -it consists of one or more sub-locations. A location not part of any other -location is called a *cell*. +An *object* represents a *value*. If an object represents an aggregate value, +it has *sub-objects*. *Object*s are stored in *locations*, which can have +sub-locations storing the sub-objects, if any. A location not part of any +other location is called a *cell*. -Every implicitly or explicitly constructed value has a unique *identity*, -meaning two separate values cannot be the *same*, but they can be *equal*. +Each object constructed at some point has a unique identity, even if it +represents the same value as another object. An object can only be stored in +a single location at a time (which is referred to as its *owner*), but can +move locations (thereby changing the owner). -Changing the value stored in a sub-location also modifies the value of the +Changing the object stored in a sub-location also modifies the object of the parent location, but without changing its *identity*. +> Note: the term "object" is intended as a placeholder until a better, +> less overloaded term is found. + +> Note: "constructing a value" is sometimes used interchangeably with +> "constructing an object" + ### Normal, Linear, and Affine Types -How a value inhabiting a type is allowed to be used depends on whether the -type is a normal, linear, or affine type: +How an object representing a value inhabiting a type is allowed to be used +depends on whether the type is a normal, linear, or affine type: | Type | No Use | Single Use | Multi Use | | ------ | ------ | ---------- | --------- | @@ -93,10 +101,10 @@ type is a normal, linear, or affine type: | Affine | Yes | Yes | No | | Linear | No | Yes | No | -What constitutes a *use* of a value is described in this document. +What constitutes a *use* of an object is described in this document. -Using an r-value expression means using the value it produces. Using an l- -value expression means using the value stored in the named location. +Using an r-value expression means using the object it produces. Using an l- +value expression means using the object stored in the named location. > note: at the moment, all types are *normal* types From 1e394774cf8393edd65d8de59196507505329934 Mon Sep 17 00:00:00 2001 From: zerbina <100542850+zerbina@users.noreply.github.com> Date: Sun, 6 Oct 2024 16:04:43 +0000 Subject: [PATCH 3/4] spec: specify expression kind for `Exprs` --- spec/spec.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/spec/spec.md b/spec/spec.md index abed921..d6fb7d0 100644 --- a/spec/spec.md +++ b/spec/spec.md @@ -265,6 +265,9 @@ expression is any type outside of `unit` or `void`. The type of the expression list is inferred as `void` if any non-trailing expression is `void`, otherwise the type is that of the trailing expression. +**Expression kind**: same as that of the trailing expression +**Uses**: nothing + ### Type Expressions ```grammar From 243b4341acda7b1faa044f0a5b65accb006ee2a6 Mon Sep 17 00:00:00 2001 From: zerbina <100542850+zerbina@users.noreply.github.com> Date: Tue, 8 Oct 2024 16:42:49 +0000 Subject: [PATCH 4/4] spec: specify expression kind for `If` --- spec/spec.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/spec/spec.md b/spec/spec.md index 258065f..b251449 100644 --- a/spec/spec.md +++ b/spec/spec.md @@ -169,6 +169,9 @@ there's no `else`). An error is reported if: The type of the `If` expression is the common type between `A` and `B`. +**Expression kind**: r-value +**Uses**: `cond`, `body`, and - if present - `else` + #### `Return` ```grammar