diff options
Diffstat (limited to 'docs/core-spec')
-rw-r--r-- | docs/core-spec/CoreSyn.ott | 3 | ||||
-rw-r--r-- | docs/core-spec/OpSem.ott | 29 | ||||
-rw-r--r-- | docs/core-spec/core-spec.pdf | bin | 355711 -> 354450 bytes |
3 files changed, 25 insertions, 7 deletions
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott index c8615ad8a6..57ed6e261d 100644 --- a/docs/core-spec/CoreSyn.ott +++ b/docs/core-spec/CoreSyn.ott @@ -275,6 +275,7 @@ ind, I {{ tex i }} :: 'Ind_' ::= {{ com Indices, numbers }} | 0 :: M :: zero | 1 :: M :: one | 2 :: M :: two + | 3 :: M :: three terms :: 'Terms_' ::= {{ com List of terms }} | </ ei // i /> :: :: List @@ -388,6 +389,7 @@ terminals :: 'terminals_' ::= | validDcRoles :: :: validDcRoles {{ tex \textsf{validDcRoles} }} | --> :: :: steps {{ tex \longrightarrow }} | coercionKind :: :: coercionKind {{ tex \textsf{coercionKind} }} + | coercionRole :: :: coercionRole {{ tex \textsf{coercionRole} }} | take :: :: take {{ tex \textsf{take}\! }} | coaxrProves :: :: coaxrProves {{ tex \textsf{coaxrProves} }} | Just :: :: Just {{ tex \textsf{Just} }} @@ -465,6 +467,7 @@ formula :: 'formula_' ::= | no other case matches :: :: no_other_case {{ tex \text{no other case matches} }} | t = coercionKind g :: :: coercionKind + | R = coercionRole g :: :: coercionRole | Just ( t1 , t2 ) = coaxrProves mu </ si // i /> </ ( s'j , s''j ) // j /> :: :: coaxrProves | mu1 = mu2 :: :: mu_rewrite diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott index 03be476bbb..efed85a5f5 100644 --- a/docs/core-spec/OpSem.ott +++ b/docs/core-spec/OpSem.ott @@ -34,8 +34,12 @@ e1 e2 --> e1' e2 ----------------------------- :: Beta (\n.e1) e2 --> e1[n |-> e2] -g0 = sym (nth 0 g) -g1 = nth 1 g +% g : (t1 -> t2) ~Rep# (t3 -> t4) +% e2 : t3 +% g0 : t3 ~Rep# t1 +% g1 : t2 ~Rep# t4 +g0 = sym (nth Rep 2 g) +g1 = nth Rep 3 g not e2 is_a_type not e2 is_a_coercion ----------------------------------------------- :: Push @@ -44,9 +48,19 @@ not e2 is_a_coercion ---------------------------------------- :: TPush ((\n.e) |> g) t --> (\n.(e |> g n)) t -g0 = nth 1 (nth 0 g) -g1 = sym (nth 2 (nth 0 g)) -g2 = nth 1 g +% g : ((t1 ~rho# t2) -> t3) ~Rep# ((t4 ~rho# t5) -> t6) +% g2 : t3 ~Rep# t6 +% g' : t4 ~rho# t5 +% g0 : t1 ~rho# t4 +% g1 : t5 ~rho# t2 +% recall that (->) :: forall r1 r2. TYPE r1 -> TYPE r2 -> Type +% and that (~#) :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep '[]) +% so pulling out the first visible argument for both is argument 2, +% and the second visible argument for both is argument 3 +R = coercionRole g' +g0 = nth R 2 (nth Rep 2 g) +g1 = sym (nth R 3 (nth Rep 2 g)) +g2 = nth Rep 3 g ------------------------------- :: CPush ((\n.e) |> g) g' --> (\n.e |> g2) (g0 ; g' ; g1) @@ -80,9 +94,10 @@ no other case matches ------------------------------------------------------------ :: MatchDefault case e as n return t of </ alti // i /> --> u[n |-> e] -T </ taa // aa /> k'~#k T </ t'aa // aa /> = coercionKind g +T </ taa // aa /> k'~Rep# k T </ t'aa // aa /> = coercionKind g +</ Raa // aa /> = tyConRoles T forall </ alphaaa_kaa // aa />. forall </ betabb_k'bb // bb />. </ t1cc // cc /> $ -> T </ alphaaa_kaa // aa /> = dataConRepType K -</ e'cc = ecc |> (t1cc $ </ [alphaaa_kaa |-> nth aa g] // aa /> </ [betabb_k'bb |-> <sbb>_Nom] // bb />) // cc /> +</ e'cc = ecc |> (t1cc $ </ [alphaaa_kaa |-> nth Raa aa g] // aa /> </ [betabb_k'bb |-> <sbb>_Nom] // bb />) // cc /> --------------------------- :: CasePush case (K </ taa // aa /> </ sbb // bb /> </ ecc // cc />) |> g as n return t2 of </ alti // i /> --> \\ case K </ t'aa // aa /> </ sbb // bb /> </ e'cc // cc /> as n return t2 of </ alti // i /> diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf Binary files differindex 372a18dff8..97694dcfc2 100644 --- a/docs/core-spec/core-spec.pdf +++ b/docs/core-spec/core-spec.pdf |