Fix numerous typos
Signed-off-by: Danila Fedorin <daniel.fedorin@hpe.com>
This commit is contained in:
parent
985763d19c
commit
9c24aac627
@ -50,7 +50,7 @@ I have a story in three parts.
|
|||||||
- I had little background in Alloy, but some background in (formal) logic
|
- I had little background in Alloy, but some background in (formal) logic
|
||||||
|
|
||||||
3. This led me to discover a bug in the compiler that I then fixed.
|
3. This led me to discover a bug in the compiler that I then fixed.
|
||||||
- Re-creating the bug required some gymanstics that were unlikely to occur in practice.
|
- Re-creating the bug required some gymnastics that were unlikely to occur in practice.
|
||||||
|
|
||||||
---
|
---
|
||||||
|
|
||||||
@ -160,7 +160,7 @@ Here, we search the scope of `R` and `M1`, but **only for public symbols**.
|
|||||||
|
|
||||||
We want to:
|
We want to:
|
||||||
- Respect the priority order
|
- Respect the priority order
|
||||||
- Including prefering methods over non-methods
|
- Including preferring methods over non-methods
|
||||||
- As a result, we search the scopes multiple times
|
- As a result, we search the scopes multiple times
|
||||||
- Avoid any extra work
|
- Avoid any extra work
|
||||||
- This includes redundant re-searches
|
- This includes redundant re-searches
|
||||||
@ -208,7 +208,7 @@ Code notes `previousFilter` is an approximation.
|
|||||||
|
|
||||||
* `previousFilter` is an approximation.
|
* `previousFilter` is an approximation.
|
||||||
* For `previousFilter = PUBLIC` and `filter = METHOD_FIELD`, we get
|
* For `previousFilter = PUBLIC` and `filter = METHOD_FIELD`, we get
|
||||||
`previousFilter = 0`, indicating no more searches should be donne.
|
`previousFilter = 0`, indicating no more searches should be done.
|
||||||
* But we're missing private non-methods!
|
* But we're missing private non-methods!
|
||||||
* However, no case we knew of hit this combination of searches, or any like it.
|
* However, no case we knew of hit this combination of searches, or any like it.
|
||||||
* All of our language tests passed.
|
* All of our language tests passed.
|
||||||
@ -326,7 +326,7 @@ eventually theSunIsInTheSky
|
|||||||
|
|
||||||
# Search Configuration in Alloy
|
# Search Configuration in Alloy
|
||||||
|
|
||||||
Instead of duplcating `METHOD` and `NOT_METHOD`, use two sets of flags (the regular and the "not").
|
Instead of duplicating `METHOD` and `NOT_METHOD`, use two sets of flags (the regular and the "not").
|
||||||
|
|
||||||
```alloy
|
```alloy
|
||||||
enum Flag {Method, MethodOrField, Public}
|
enum Flag {Method, MethodOrField, Public}
|
||||||
@ -450,7 +450,7 @@ To combine several statements, we make it so that the "next" state of one statem
|
|||||||
</div>
|
</div>
|
||||||
</div>
|
</div>
|
||||||
|
|
||||||
This is reminiscent of sequencing hoare triples:
|
This is reminiscent of sequencing Hoare triples:
|
||||||
|
|
||||||
$$
|
$$
|
||||||
\{ P \} \; s_1 \; \{ Q \} \; s_2 \; \{ R \}
|
\{ P \} \; s_1 \; \{ Q \} \; s_2 \; \{ R \}
|
||||||
@ -634,13 +634,13 @@ wontFindNeeded: run {
|
|||||||
|
|
||||||

|

|
||||||
|
|
||||||
We need some gymnastics to figure out what varibles make this model possible.
|
We need some gymnastics to figure out what variables make this model possible.
|
||||||
|
|
||||||
Alloy has a nice visualizer, but it has a lot of information.
|
Alloy has a nice visualizer, but it has a lot of information.
|
||||||
|
|
||||||
In the interest of time, I found:
|
In the interest of time, I found:
|
||||||
|
|
||||||
* If the compiler searches a scope firt for `PUBLIC` symbols, ...
|
* If the compiler searches a scope first for `PUBLIC` symbols, ...
|
||||||
* ...then for `METHOD_OR_FIELD`, ...
|
* ...then for `METHOD_OR_FIELD`, ...
|
||||||
* ...then for any symbols, they will miss things!
|
* ...then for any symbols, they will miss things!
|
||||||
|
|
||||||
|
@ -62,7 +62,7 @@ Daniel Fedorin, HPE
|
|||||||
* Compile-time operations do not have mutable state.
|
* Compile-time operations do not have mutable state.
|
||||||
- Cannot change values of `param` or `type` variables.
|
- Cannot change values of `param` or `type` variables.
|
||||||
* Chapel's compile-time programming does not support loops.
|
* Chapel's compile-time programming does not support loops.
|
||||||
- `param` loops are kind of an aception, but are simply unrolled.
|
- `param` loops are kind of an exception, but are simply unrolled.
|
||||||
- Without mutability, this unrolling doesn't give us much.
|
- Without mutability, this unrolling doesn't give us much.
|
||||||
* Without state, our `type` and `param` functions are pure.
|
* Without state, our `type` and `param` functions are pure.
|
||||||
|
|
||||||
@ -103,7 +103,7 @@ Without mutability and loops, Haskell programmers use pattern-matching and recur
|
|||||||
|
|
||||||
# Evaluating Haskell
|
# Evaluating Haskell
|
||||||
|
|
||||||
Haskell simplifies calls to functions by pickign the case based on the arguments.
|
Haskell simplifies calls to functions by picking the case based on the arguments.
|
||||||
|
|
||||||
```Haskell
|
```Haskell
|
||||||
sum (Cons 1 (Cons 2 (Cons 3 Nil)))
|
sum (Cons 1 (Cons 2 (Cons 3 Nil)))
|
||||||
@ -251,7 +251,7 @@ y(t_0+h) & \approx y_0 + h \times y'(t_0) \\
|
|||||||
\end{align*}
|
\end{align*}
|
||||||
$$
|
$$
|
||||||
|
|
||||||
We can name the the first approximated $y$-value $y_1$, and set it:
|
We can name the first approximated $y$-value $y_1$, and set it:
|
||||||
|
|
||||||
$$
|
$$
|
||||||
y_1 = y_0 + h \times f(t_0, y_0)
|
y_1 = y_0 + h \times f(t_0, y_0)
|
||||||
@ -606,7 +606,7 @@ More work could be done to support more format specifiers, escapes, etc., but th
|
|||||||
# Algebraic Data Types
|
# Algebraic Data Types
|
||||||
|
|
||||||
* The kinds of data types that Haskell supports are called *algebraic data types*.
|
* The kinds of data types that Haskell supports are called *algebraic data types*.
|
||||||
* At a fundamental level, they can be built up from two operations: _cartesian product_ and _disjoint union_.
|
* At a fundamental level, they can be built up from two operations: _Cartesian product_ and _disjoint union_.
|
||||||
* There are other concepts to build recursive data types, but we won't need them in Chapel.
|
* There are other concepts to build recursive data types, but we won't need them in Chapel.
|
||||||
- To prove to you I know what I'm talking about, some jargon:
|
- To prove to you I know what I'm talking about, some jargon:
|
||||||
_initial algebras_, _the fixedpoint functor_, _catamorphisms_...
|
_initial algebras_, _the fixedpoint functor_, _catamorphisms_...
|
||||||
@ -622,7 +622,7 @@ li:nth-child(3) { color: lightgrey; }
|
|||||||
# Algebraic Data Types
|
# Algebraic Data Types
|
||||||
|
|
||||||
- The kinds of data types that Haskell supports are called *algebraic data types*.
|
- The kinds of data types that Haskell supports are called *algebraic data types*.
|
||||||
- At a fundamental level, they can be built up from two operations: _cartesian product_ and _disjoint union_.
|
- At a fundamental level, they can be built up from two operations: _Cartesian product_ and _disjoint union_.
|
||||||
- There are other concepts to build recursive data types, but we won't need them in Chapel.
|
- There are other concepts to build recursive data types, but we won't need them in Chapel.
|
||||||
- To prove to you I know what I'm talking about, some jargon:
|
- To prove to you I know what I'm talking about, some jargon:
|
||||||
_initial algebras_, _the fixedpoint functor_, _catamorphisms_...
|
_initial algebras_, _the fixedpoint functor_, _catamorphisms_...
|
||||||
@ -632,7 +632,7 @@ li:nth-child(3) { color: lightgrey; }
|
|||||||
---
|
---
|
||||||
|
|
||||||
# Cartesian Product
|
# Cartesian Product
|
||||||
For any two types, the _cartesian product_ of these two types defines all pairs of values from these types.
|
For any two types, the _Cartesian product_ of these two types defines all pairs of values from these types.
|
||||||
- This is like a two-element tuple _at the value level_ in Chapel.
|
- This is like a two-element tuple _at the value level_ in Chapel.
|
||||||
- We write this as $A \times B$ for two types $A$ and $B$.
|
- We write this as $A \times B$ for two types $A$ and $B$.
|
||||||
- In (type-level) Chapel and Haskell:
|
- In (type-level) Chapel and Haskell:
|
||||||
@ -698,7 +698,7 @@ For any two types, the _disjoint union_ of these two types defines values that a
|
|||||||
|
|
||||||
# Algebraic Data Types
|
# Algebraic Data Types
|
||||||
|
|
||||||
* We can build up more compelx types by combining these two operations.
|
* We can build up more complex types by combining these two operations.
|
||||||
* Need a triple of types $A$, $B$, and $C$? Use $A \times (B \times C)$.
|
* Need a triple of types $A$, $B$, and $C$? Use $A \times (B \times C)$.
|
||||||
* Similarly, "any one of three types" can be expressed as $A + (B + C)$.
|
* Similarly, "any one of three types" can be expressed as $A + (B + C)$.
|
||||||
* A `Result<T>` type (in Rust, or `optional<T>` in C++) is $T + \text{Unit}$.
|
* A `Result<T>` type (in Rust, or `optional<T>` in C++) is $T + \text{Unit}$.
|
||||||
|
Loading…
Reference in New Issue
Block a user