Skip to content

Commit e6df1ef

Browse files
flupeflupe
committed
fix compilation of case with unreachable branches
1 parent 3dde0c8 commit e6df1ef

File tree

12 files changed

+1938
-19
lines changed

12 files changed

+1938
-19
lines changed

‎agda2lambox.cabal‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@ executable agda2lambox
1616
hs-source-dirs: src
1717
main-is: Main.hs
1818
other-modules: Agda.Utils,
19+
Agda.Utils.Treeless,
20+
Agda.Utils.EliminateDefaults,
1921
Agda2Lambox.Compile.Target,
2022
Agda2Lambox.Compile.Utils,
2123
Agda2Lambox.Compile.Monad,

‎build/STLC.txt‎

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
Nat:
2+
mutual inductive(s):
3+
Nat
4+
constructors:
5+
zero (0 arg(s))
6+
suc (1 arg(s))
7+
8+
add:
9+
constant declaration:
10+
body: μ rec ->
11+
λ _ _ →
12+
let _ = □
13+
in case<Nat{0},0> @2 of
14+
λ<[]> @1
15+
λ<[_]> Nat{0}{1} (@4 @0 @2)
16+
17+
Type:
18+
mutual inductive(s):
19+
Type
20+
constructors:
21+
ℕ (0 arg(s))
22+
_⇒_ (2 arg(s))
23+
24+
Ctx:
25+
mutual inductive(s):
26+
Ctx
27+
constructors:
28+
[] (0 arg(s))
29+
_▷_ (3 arg(s))
30+
31+
_∋_:
32+
mutual inductive(s):
33+
_∋_
34+
constructors:
35+
here (3 arg(s))
36+
there (5 arg(s))
37+
38+
Tm:
39+
mutual inductive(s):
40+
Tm
41+
constructors:
42+
var (2 arg(s))
43+
lam (3 arg(s))
44+
app (4 arg(s))
45+
lit (1 arg(s))
46+
_`+_ (2 arg(s))
47+
48+
⟦_⟧: constant declaration: body: μ rec -> □
49+
50+
Env:
51+
mutual inductive(s):
52+
Env
53+
constructors:
54+
[] (0 arg(s))
55+
_▷_ (5 arg(s))
56+
57+
lookupEnv:
58+
constant declaration:
59+
body: μ rec ->
60+
λ _ _ _ _ _ →
61+
let _ = □
62+
in case<Env{0},0> @2 of
63+
λ<[]> @0
64+
λ<[_, _, _, _, _]>
65+
let _ = □
66+
in case<Nat{0},0> @11 of
67+
λ<[]> @0
68+
λ<[_]>
69+
let _ = □
70+
in case<Ctx{0},0> @12 of
71+
λ<[]> @0
72+
λ<[_, _, _]>
73+
let _ = □
74+
in case<_∋_{0},0> @13 of
75+
λ<[_, _, _]> @10
76+
λ<[_, _, _, _, _]> @23 @10 @7 □ @13 @0
77+
78+
eval:
79+
constant declaration:
80+
body: μ rec ->
81+
λ _ _ _ _ _ →
82+
let _ = □
83+
in case<Tm{0},0> @1 of
84+
λ<[_, _]> lookupEnv @7 @6 □ @4 @0
85+
λ<[_, _, _]>
86+
let _ = □
87+
in case<Type{0},0> @7 of
88+
λ<[]> @0
89+
λ<[_, _]>
90+
λ _ →
91+
@13 Nat{0}{1} @12 Ctx{0}{1} □ @11 @2 @1 Env{0}{1} □ □ □ @9 @0 @4
92+
λ<[_, _, _, _]>
93+
@10 @9 @8 Type{0}{1} @3 @7 @6 @1 (@10 @9 @8 @3 @6 @0)
94+
λ<[_]> @0
95+
λ<[_, _]>
96+
add (@8 @7 @6 Type{0}{0} @4 @1) (@8 @7 @6 Type{0}{0} @4 @0)
97+
98+
test:
99+
constant declaration:
100+
body: eval Nat{0}{0} Ctx{0}{0} Type{0}{0} Env{0}{0}
101+
Tm{0}{2}
102+
Type{0}{0}
103+
□
104+
Tm{0}{1}
105+
□
106+
□
107+
Tm{0}{4} Tm{0}{3} Nat{0}{1} Nat{0}{0} Tm{0}{0} □ _∋_{0}{0} □ □ □
108+
Tm{0}{3} Nat{0}{1} Nat{0}{0}

‎build/STLC.v‎

Lines changed: 386 additions & 0 deletions
Large diffs are not rendered by default.

‎build/STLCTyped.txt‎

Lines changed: 157 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,157 @@
1+
Nat:
2+
mutual inductive(s):
3+
Nat
4+
type variables: []
5+
constructors:
6+
zero (0 arg(s))
7+
suc (1 arg(s))
8+
n : Nat
9+
10+
add:
11+
constant declaration:
12+
type variables: []
13+
type: Nat → Nat → Nat
14+
body: μ rec ->
15+
λ _ _ →
16+
let _ = □
17+
in case<Nat{0},0> @2 of
18+
λ<[]> @1
19+
λ<[_]> Nat{0}{1} (@4 @0 @2)
20+
21+
Type:
22+
mutual inductive(s):
23+
Type
24+
type variables: []
25+
constructors:
26+
ℕ (0 arg(s))
27+
_⇒_ (2 arg(s))
28+
_ : Type
29+
_ : Type
30+
31+
Ctx:
32+
mutual inductive(s):
33+
Ctx
34+
type variables: []
35+
constructors:
36+
[] (0 arg(s))
37+
_▷_ (3 arg(s))
38+
n : Nat
39+
_ : Ctx
40+
_ : Type
41+
42+
_∋_:
43+
mutual inductive(s):
44+
_∋_
45+
type variables: []
46+
constructors:
47+
here (3 arg(s))
48+
Γ.n : Nat
49+
Γ : Ctx
50+
α : Type
51+
there (5 arg(s))
52+
Γ.n : Nat
53+
Γ : Ctx
54+
α : Type
55+
β : Type
56+
_ : _∋_
57+
58+
Tm:
59+
mutual inductive(s):
60+
Tm
61+
type variables: [n, Γ]
62+
constructors:
63+
var (2 arg(s))
64+
α : Type
65+
_ : _∋_
66+
lam (3 arg(s))
67+
α : Type
68+
β : Type
69+
_ : Tm 𝕋 𝕋
70+
app (4 arg(s))
71+
α : Type
72+
β : Type
73+
_ : Tm @0 @1
74+
_ : Tm @0 @1
75+
lit (1 arg(s))
76+
_ : Nat
77+
_`+_ (2 arg(s))
78+
_ : Tm @0 @1
79+
_ : Tm @0 @1
80+
81+
⟦_⟧:
82+
constant declaration:
83+
type variables: []
84+
type: Type → □
85+
body: μ rec -> □
86+
87+
Env:
88+
mutual inductive(s):
89+
Env
90+
type variables: []
91+
constructors:
92+
[] (0 arg(s))
93+
_▷_ (5 arg(s))
94+
Γ.n : Nat
95+
Γ : Ctx
96+
α : Type
97+
_ : Env
98+
_ : 𝕋
99+
100+
lookupEnv:
101+
constant declaration:
102+
type variables: []
103+
type: Nat → Ctx → Type → Env → _∋_ → 𝕋
104+
body: μ rec ->
105+
λ _ _ _ _ _ →
106+
let _ = □
107+
in case<Env{0},0> @2 of
108+
λ<[]> @0
109+
λ<[_, _, _, _, _]>
110+
let _ = □
111+
in case<Nat{0},0> @11 of
112+
λ<[]> @0
113+
λ<[_]>
114+
let _ = □
115+
in case<Ctx{0},0> @12 of
116+
λ<[]> @0
117+
λ<[_, _, _]>
118+
let _ = □
119+
in case<_∋_{0},0> @13 of
120+
λ<[_, _, _]> @10
121+
λ<[_, _, _, _, _]> @23 @10 @7 □ @13 @0
122+
123+
eval:
124+
constant declaration:
125+
type variables: []
126+
type: Nat → Ctx → Type → Env → Tm 𝕋 𝕋 → 𝕋
127+
body: μ rec ->
128+
λ _ _ _ _ _ →
129+
let _ = □
130+
in case<Tm{0},0> @1 of
131+
λ<[_, _]> lookupEnv @7 @6 □ @4 @0
132+
λ<[_, _, _]>
133+
let _ = □
134+
in case<Type{0},0> @7 of
135+
λ<[]> @0
136+
λ<[_, _]>
137+
λ _ →
138+
@13 Nat{0}{1} @12 Ctx{0}{1} □ @11 @2 @1 Env{0}{1} □ □ □ @9 @0 @4
139+
λ<[_, _, _, _]>
140+
@10 @9 @8 Type{0}{1} @3 @7 @6 @1 (@10 @9 @8 @3 @6 @0)
141+
λ<[_]> @0
142+
λ<[_, _]>
143+
add (@8 @7 @6 Type{0}{0} @4 @1) (@8 @7 @6 Type{0}{0} @4 @0)
144+
145+
test:
146+
constant declaration:
147+
type variables: []
148+
type: Nat
149+
body: eval Nat{0}{0} Ctx{0}{0} Type{0}{0} Env{0}{0}
150+
Tm{0}{2}
151+
Type{0}{0}
152+
□
153+
Tm{0}{1}
154+
□
155+
□
156+
Tm{0}{4} Tm{0}{3} Nat{0}{1} Nat{0}{0} Tm{0}{0} □ _∋_{0}{0} □ □ □
157+
Tm{0}{3} Nat{0}{1} Nat{0}{0}

0 commit comments

Comments
 (0)