Modernize S_TPush in the core spec
authorRyan Scott <ryan.gl.scott@gmail.com>
Mon, 16 Jul 2018 22:10:01 +0000 (18:10 -0400)
committerRyan Scott <ryan.gl.scott@gmail.com>
Mon, 16 Jul 2018 22:10:02 +0000 (18:10 -0400)
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

docs/core-spec/OpSem.ott
docs/core-spec/core-spec.pdf

index efed85a..389c5e8 100644 (file)
@@ -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
index 97694dc..21a8852 100644 (file)
Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ