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
|
% - we add binding in a case
% - the Case constructor and rule names have "Sm" appended to avoid a clash with variants
grammar
T {{ hol Typ }}, S, U :: Ty ::= {{ com types: }}
| T1 + T2 :: :: Sum {{ com sum type }}
t :: Tm ::= {{ com terms: }}
| inl t :: :: Inl {{ com tagging (left) }}
| inr t :: :: Inr {{ com tagging (right) }}
| case t of inl x1 => t1 | inr x2 => t2 :: :: CaseSm
(+ bind x1 in t1 +) (+ bind x2 in t2 +) {{ com case }}
v :: Va ::= {{ com values: }}
| inl v :: :: Inl {{ com tagged value (left) }}
| inr v :: :: Inr {{ com tagged value (right) }}
defns
Jop :: '' ::=
defn
t --> t' :: :: red :: E_ {{ com Evaluation }} by
----------------------------------------------------------------- :: CaseInl
case ( inl v0 ) of inl x1=>t1 | inr x2=>t2 --> [x1 |-> v0]t1
----------------------------------------------------------------- :: CaseInr
case ( inr v0 ) of inl x1=>t1 | inr x2=>t2 --> [x2 |-> v0]t2
t0 --> t0'
-------------------------------------------------------------------------- :: CaseSm
case t0 of inl x1=>t1 | inr x2=>t2 --> case t0' of inl x1=>t1 | inr x2=>t2
t1 --> t1'
------------------ :: Inl
inl t1 --> inl t1'
t1 --> t1'
------------------ :: Inr
inr t1 --> inr t1'
defns
Jtype :: '' ::=
defn
G |- t : T :: :: typing :: T_ {{ com Typing }} by
G |- t1 : T1
------------------ :: Inl
G|- inl t1 : T1+T2
G |- t1 : T2
------------------ :: Inr
G|- inr t1 : T1+T2
G |- t0 : T1+T2
G,x1:T1|- t1:T
G,x2:T2|- t2:T
------------------------------------------ :: CaseSm
G|- case t0 of inl x1=>t1 | inr x2=>t2 : T
|
