diff options
| author | Ryan Scott <ryan.gl.scott@gmail.com> | 2018-07-16 18:10:01 -0400 |
|---|---|---|
| committer | Ryan Scott <ryan.gl.scott@gmail.com> | 2018-07-16 18:10:02 -0400 |
| commit | 7fe4993673e43e5b21f38d79ecc8b5163e97ee84 (patch) | |
| tree | b1c11b20e1a3f58566dd793c18ba1287b8d3d250 | |
| parent | beba89a0f16681c85d39fc8a894bde4162ff492a (diff) | |
| download | haskell-7fe4993673e43e5b21f38d79ecc8b5163e97ee84.tar.gz | |
Modernize S_TPush in the core spec
Summary:
The specification for the `S_TPush` rule in the core spec's
operational semantics is woefully out-of-date. Let's bring it in line
with the presentation in //System FC with Explicit Kind Equality//.
Test Plan: Read it
Reviewers: goldfire, bgamari
Reviewed By: goldfire
Subscribers: rwbarton, thomie, carter
Differential Revision: https://phabricator.haskell.org/D4970
| -rw-r--r-- | docs/core-spec/OpSem.ott | 10 | ||||
| -rw-r--r-- | docs/core-spec/core-spec.pdf | bin | 354450 -> 354354 bytes |
2 files changed, 8 insertions, 2 deletions
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott index efed85a5f5..389c5e8106 100644 --- a/docs/core-spec/OpSem.ott +++ b/docs/core-spec/OpSem.ott @@ -45,8 +45,14 @@ not e2 is_a_coercion ----------------------------------------------- :: Push ((\n.e1) |> g) e2 --> (\n.e1 |> g1) (e2 |> g0) ----------------------------------------- :: TPush -((\n.e) |> g) t --> (\n.(e |> g n)) t +% g : (forall (a : k1). t1) ~Rep# (forall (a : k2). t2) +% t : k2 +% g' : k2 ~# k1 +% t' : k1 +g' = sym (nth Nom 0 g) +t' = t |> g' +-------------------------------------------------------- :: TPush +((\n.e) |> g) t --> ((\n.e) t') |> (g @ (<t>_Nom |> g')) % g : ((t1 ~rho# t2) -> t3) ~Rep# ((t4 ~rho# t5) -> t6) % g2 : t3 ~Rep# t6 diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf Binary files differindex 97694dcfc2..21a8852d04 100644 --- a/docs/core-spec/core-spec.pdf +++ b/docs/core-spec/core-spec.pdf |