blob: ed59e9538b38df1c30c2fc63e4cebec87aa60f99 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Dynamic semantics %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The definitions in this file do *not* strictly correspond to any specific
% code in GHC. They are here to provide a reasonable operational semantic
% interpretation to the typing rules presented in the other ott files. Thus,
% your mileage may vary. In particular, there has been *no* attempt to
% write any formal proofs over these semantics.
%
% With that disclaimer disclaimed, these rules are a reasonable jumping-off
% point for an analysis of FC's operational semantics. If you don't want to
% worry about mutual recursion (and who does?), you can even drop the
% environment S.
grammar
defns
OpSem :: '' ::=
defn S |- e --> e' :: :: step :: 'S_' {{ com Single step semantics }}
{{ tex \begin{array}{l} [[S]] \labeledjudge{op} [[e]] [[-->]] [[e']] \end{array} }}
by
S(n) = e
----------------- :: Var
S |- n --> e
S |- e1 --> e1'
------------------- :: App
S |- e1 e2 --> e1' e2
----------------------------- :: Beta
S |- (\n.e1) e2 --> e1[n |-> e2]
g0 = sym (nth 0 g)
g1 = nth 1 g
not e2 is_a_type
not e2 is_a_coercion
----------------------------------------------- :: Push
S |- ((\n.e1) |> g) e2 --> (\n.e1 |> g1) (e2 |> g0)
---------------------------------------- :: TPush
S |- ((\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
------------------------------- :: CPush
S |- ((\n.e) |> g) g' --> (\n.e |> g2) (g0 ; g' ; g1)
--------------------------------------- :: Trans
S |- (e |> g1) |> g2 --> e |> (g1 ; g2)
S |- e --> e'
------------------------ :: Cast
S |- e |> g --> e' |> g
S |- e --> e'
------------------------------ :: Tick
S |- e { tick } --> e' { tick }
S |- e --> e'
--------------------------------------- :: Case
S |- case e as n return t of </ alti // i /> --> case e' as n return t of </ alti // i />
altj = K </ alphabb_kbb // bb /> </ xcc_tcc // cc /> -> u
u' = u[n |-> e] </ [alphabb_kbb |-> sbb] // bb /> </ [xcc_tcc |-> ecc] // cc />
-------------------------------------------------------------- :: MatchData
S |- case K </ t'aa // aa /> </ sbb // bb /> </ ecc // cc /> as n return t of </ alti // i /> --> u'
altj = lit -> u
---------------------------------------------------------------- :: MatchLit
S |- case lit as n return t of </ alti // i /> --> u[n |-> lit]
altj = _ -> u
no other case matches
------------------------------------------------------------ :: MatchDefault
S |- case e as n return t of </ alti // i /> --> u[n |-> e]
T </ taa // aa /> ~#k T </ t'aa // aa /> = coercionKind g
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 />
--------------------------- :: CasePush
S |- 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 />
----------------- :: LetNonRec
S |- let n = e1 in e2 --> e2[n |-> e1]
S, </ [ni |-> ei] // i /> |- u --> u'
------------------------------------ :: LetRec
S |- let rec </ ni = ei // i /> in u --> let rec </ ni = ei // i /> in u'
--------------- :: LetRecApp
S |- (let rec </ ni = ei // i /> in u) e' --> let rec </ ni = ei // i /> in (u e')
---------------- :: LetRecCast
S |- (let rec </ ni = ei // i /> in u) |> g --> let rec </ ni = ei // i /> in (u |> g)
--------------- :: LetRecCase
S |- case (let rec </ ni = ei // i /> in u) as n0 return t of </ altj // j /> --> \\ let rec </ ni = ei // i /> in (case u as n0 return t of </ altj // j />)
--------------- :: LetRecFlat
S |- let rec </ ni = ei // i /> in (let rec </ nj' = ej' // j /> in u) --> let rec </ ni = ei // i />;; </ nj' = ej' // j /> in u
fv(u) \inter </ ni // i /> = empty
--------------------------------- :: LetRecReturn
S |- let rec </ ni = ei // i /> in u --> u
|
