Skip to content

Commit d937f50

Browse files
tgengtgeng
committed
fix parameter binding during translation
1 parent 91ddfb7 commit d937f50

File tree

5 files changed

+126
-147
lines changed

5 files changed

+126
-147
lines changed

‎src/test/resources/com/github/tgeng/archon/core/ir/testing/tterm/t_declaration_spec/data_eq/translation_output.scala

+11-16
Original file line numberDiff line numberDiff line change
@@ -11,37 +11,32 @@ List(
1111
),
1212
(
1313
Binding(
14-
ty = Let(
15-
t = Def(qn = qn"__unresolved__.l") @ "l",
16-
tBinding = Binding(ty = Auto() @ "ε", usage = Auto()) @ "$v",
17-
eff = Auto(),
18-
body = Redex(
19-
t = Def(qn = qn"__unresolved__.Type") @ "Type",
20-
elims = List(ETerm(v = Var(idx = 0) @ "l"))
21-
) @ "Type l"
22-
) @ "ε",
14+
ty = Redex(
15+
t = Def(qn = qn"__unresolved__.Type") @ "Type",
16+
elims = List(ETerm(v = Var(idx = 0) @ "l"))
17+
) @ "Type l",
2318
usage = Def(qn = qn"archon.builtin.type.Usage.uAny")
2419
) @ "A",
2520
INVARIANT
2621
),
2722
(
2823
Binding(
29-
ty = Def(qn = qn"__unresolved__.A") @ "A",
24+
ty = Return(v = Var(idx = 0) @ "A", usage = Auto() @ "ε") @ "A",
3025
usage = Def(qn = qn"archon.builtin.type.Usage.uAny")
3126
) @ "x",
3227
INVARIANT
3328
)
3429
),
3530
ty = FunctionType(
3631
binding = Binding(
37-
ty = Collapse(cTm = Def(qn = qn"__unresolved__.A") @ "A") @ "A",
32+
ty = Var(idx = 1) @ "A",
3833
usage = Collapse(cTm = Def(qn = qn"archon.builtin.type.Usage.uAny")) @ "ε"
3934
) @ "_",
4035
bodyTy = F(
4136
vTy = Collapse(
4237
cTm = Redex(
4338
t = Def(qn = qn"__unresolved__.Type") @ "Type",
44-
elims = List(ETerm(v = Collapse(cTm = Def(qn = qn"__unresolved__.l") @ "l") @ "l"))
39+
elims = List(ETerm(v = Var(idx = 3) @ "l"))
4540
) @ "Type l"
4641
) @ "Type l",
4742
effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total") @ "ε") @ "ε",
@@ -57,10 +52,10 @@ List(
5752
cTm = Redex(
5853
t = Return(v = DataType(qn = qn"test.Eq", args = List()) @ "Eq", usage = Auto()) @ "Eq",
5954
elims = List(
60-
ETerm(v = Collapse(cTm = Def(qn = qn"__unresolved__.l") @ "l") @ "l"),
61-
ETerm(v = Collapse(cTm = Def(qn = qn"__unresolved__.A") @ "A") @ "A"),
62-
ETerm(v = Collapse(cTm = Def(qn = qn"__unresolved__.x") @ "x") @ "x"),
63-
ETerm(v = Collapse(cTm = Def(qn = qn"__unresolved__.x") @ "x") @ "x")
55+
ETerm(v = Var(idx = 2) @ "l"),
56+
ETerm(v = Var(idx = 1) @ "A"),
57+
ETerm(v = Var(idx = 0) @ "x"),
58+
ETerm(v = Var(idx = 0) @ "x")
6459
)
6560
) @ "Eq l A x x"
6661
) @ "Eq l A x x",

‎src/test/resources/com/github/tgeng/archon/core/ir/testing/tterm/t_declaration_spec/data_vec/input.tdecl

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
data Vec (l: Level) +(t: Type l): Nat -> Type l
2-
Nil: Vec l t Zero
3-
Succ: n: Nat -> t -> Vec l t n -> Vec l t (Succ n)
2+
Nil: Vec#{l t Zero}
3+
Succ: n: Nat -> t -> Vec#{l t n} -> Vec#{l t Succ#{n}}

‎src/test/resources/com/github/tgeng/archon/core/ir/testing/tterm/t_declaration_spec/data_vec/parse_output.scala

+20-33
Original file line numberDiff line numberDiff line change
@@ -36,17 +36,13 @@ List(
3636
TConstructor(
3737
name = "Nil",
3838
ty = TF(
39-
ty = TRedex(
40-
c = TId(id = "Vec") @ "Vec",
41-
elims = List(
42-
ETerm(v = TId(id = "l")),
43-
ETerm(v = TId(id = "t") @ "t"),
44-
ETerm(v = TId(id = "Zero") @ "Zero")
45-
)
46-
) @ "Vec l t Zero",
39+
ty = TCon(
40+
name = "Vec",
41+
args = List(TId(id = "l"), TId(id = "t") @ "t", TId(id = "Zero") @ "Zero")
42+
) @ "Vec#{l t Zero}",
4743
effects = TDef(qn = qn"archon.builtin.effects.total"),
4844
usage = TDef(qn = qn"archon.builtin.type.Usage.u1")
49-
) @ "Vec l t Zero"
45+
) @ "Vec#{l t Zero}"
5046
),
5147
TConstructor(
5248
name = "Succ",
@@ -65,39 +61,30 @@ List(
6561
bodyType = TFunctionType(
6662
arg = TBinding(
6763
name = "_",
68-
ty = TRedex(
69-
c = TId(id = "Vec"),
70-
elims = List(
71-
ETerm(v = TId(id = "l")),
72-
ETerm(v = TId(id = "t")),
73-
ETerm(v = TId(id = "n") @ "n")
74-
)
75-
) @ "Vec l t n",
64+
ty = TCon(
65+
name = "Vec",
66+
args = List(TId(id = "l"), TId(id = "t"), TId(id = "n") @ "n")
67+
) @ "Vec#{l t n}",
7668
usage = TDef(qn = qn"archon.builtin.type.Usage.uAny")
7769
),
7870
bodyType = TF(
79-
ty = TRedex(
80-
c = TId(id = "Vec"),
81-
elims = List(
82-
ETerm(v = TId(id = "l")),
83-
ETerm(v = TId(id = "t")),
84-
ETerm(
85-
v = TRedex(
86-
c = TId(id = "Succ") @ "Succ",
87-
elims = List(ETerm(v = TId(id = "n")))
88-
) @ "Succ n"
89-
)
71+
ty = TCon(
72+
name = "Vec",
73+
args = List(
74+
TId(id = "l"),
75+
TId(id = "t"),
76+
TCon(name = "Succ", args = List(TId(id = "n"))) @ "Succ#{n}"
9077
)
91-
) @ "Vec l t (Succ n)",
78+
) @ "Vec#{l t Succ#{n}}",
9279
effects = TDef(qn = qn"archon.builtin.effects.total"),
9380
usage = TDef(qn = qn"archon.builtin.type.Usage.u1")
94-
) @ "Vec l t (Succ n)",
81+
) @ "Vec#{l t Succ#{n}}",
9582
effects = TDef(qn = qn"archon.builtin.effects.total")
96-
) @ "Vec l t n -> Vec l t (Succ n)",
83+
) @ "Vec#{l t n} -> Vec#{l t Succ#{n}}",
9784
effects = TDef(qn = qn"archon.builtin.effects.total")
98-
) @ "t -> Vec l t n -> Vec l t (Succ n)",
85+
) @ "t -> Vec#{l t n} -> Vec#{l t Succ#{n}}",
9986
effects = TDef(qn = qn"archon.builtin.effects.total")
100-
) @ "n: Nat -> t -> Vec l t n -> Vec l t (Succ n)"
87+
) @ "n: Nat -> t -> Vec#{l t n} -> Vec#{l t Succ#{n}}"
10188
)
10289
)
10390
)

‎src/test/resources/com/github/tgeng/archon/core/ir/testing/tterm/t_declaration_spec/data_vec/translation_output.scala

+31-62
Original file line numberDiff line numberDiff line change
@@ -11,15 +11,10 @@ List(
1111
),
1212
(
1313
Binding(
14-
ty = Let(
15-
t = Def(qn = qn"__unresolved__.l") @ "l",
16-
tBinding = Binding(ty = Auto() @ "ε", usage = Auto()) @ "$v",
17-
eff = Auto(),
18-
body = Redex(
19-
t = Def(qn = qn"__unresolved__.Type") @ "Type",
20-
elims = List(ETerm(v = Var(idx = 0) @ "l"))
21-
) @ "Type l"
22-
) @ "ε",
14+
ty = Redex(
15+
t = Def(qn = qn"__unresolved__.Type") @ "Type",
16+
elims = List(ETerm(v = Var(idx = 0) @ "l"))
17+
) @ "Type l",
2318
usage = Def(qn = qn"archon.builtin.type.Usage.uAny")
2419
) @ "t",
2520
COVARIANT
@@ -34,7 +29,7 @@ List(
3429
vTy = Collapse(
3530
cTm = Redex(
3631
t = Def(qn = qn"__unresolved__.Type") @ "Type",
37-
elims = List(ETerm(v = Collapse(cTm = Def(qn = qn"__unresolved__.l") @ "l") @ "l"))
32+
elims = List(ETerm(v = Var(idx = 2) @ "l"))
3833
) @ "Type l"
3934
) @ "Type l",
4035
effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total") @ "ε") @ "ε",
@@ -46,19 +41,17 @@ List(
4641
PreConstructor(
4742
name = n"Nil",
4843
ty = F(
49-
vTy = Collapse(
50-
cTm = Redex(
51-
t = Return(v = DataType(qn = qn"test.Vec", args = List()) @ "Vec", usage = Auto()) @ "Vec",
52-
elims = List(
53-
ETerm(v = Collapse(cTm = Def(qn = qn"__unresolved__.l") @ "l") @ "l"),
54-
ETerm(v = Collapse(cTm = Def(qn = qn"__unresolved__.t") @ "t") @ "t"),
55-
ETerm(v = Collapse(cTm = Def(qn = qn"__unresolved__.Zero") @ "Zero") @ "Zero")
56-
)
57-
) @ "Vec l t Zero"
58-
) @ "Vec l t Zero",
44+
vTy = Con(
45+
name = n"Vec",
46+
args = List(
47+
Var(idx = 1) @ "l",
48+
Var(idx = 0) @ "t",
49+
Collapse(cTm = Def(qn = qn"__unresolved__.Zero") @ "Zero") @ "Zero"
50+
)
51+
) @ "Vec#{l t Zero}",
5952
effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total")),
6053
usage = Collapse(cTm = Def(qn = qn"archon.builtin.type.Usage.u1"))
61-
) @ "Vec l t Zero"
54+
) @ "Vec#{l t Zero}"
6255
),
6356
PreConstructor(
6457
name = n"Succ",
@@ -69,59 +62,35 @@ List(
6962
) @ "n",
7063
bodyTy = FunctionType(
7164
binding = Binding(
72-
ty = Collapse(cTm = Def(qn = qn"__unresolved__.t") @ "t") @ "t",
65+
ty = Var(idx = 1) @ "t",
7366
usage = Collapse(cTm = Def(qn = qn"archon.builtin.type.Usage.uAny"))
7467
) @ "_",
7568
bodyTy = FunctionType(
7669
binding = Binding(
77-
ty = Collapse(
78-
cTm = Redex(
79-
t = Return(
80-
v = DataType(qn = qn"test.Vec", args = List()) @ "Vec",
81-
usage = Auto()
82-
) @ "Vec",
83-
elims = List(
84-
ETerm(v = Collapse(cTm = Def(qn = qn"__unresolved__.l") @ "l") @ "l"),
85-
ETerm(v = Collapse(cTm = Def(qn = qn"__unresolved__.t") @ "t") @ "t"),
86-
ETerm(v = Var(idx = 1) @ "n")
87-
)
88-
) @ "Vec l t n"
89-
) @ "Vec l t n",
70+
ty = Con(
71+
name = n"Vec",
72+
args = List(Var(idx = 3) @ "l", Var(idx = 2) @ "t", Var(idx = 1) @ "n")
73+
) @ "Vec#{l t n}",
9074
usage = Collapse(cTm = Def(qn = qn"archon.builtin.type.Usage.uAny"))
9175
) @ "_",
9276
bodyTy = F(
93-
vTy = Collapse(
94-
cTm = Redex(
95-
t = Return(
96-
v = DataType(qn = qn"test.Vec", args = List()) @ "Vec",
97-
usage = Auto()
98-
) @ "Vec",
99-
elims = List(
100-
ETerm(v = Collapse(cTm = Def(qn = qn"__unresolved__.l") @ "l") @ "l"),
101-
ETerm(v = Collapse(cTm = Def(qn = qn"__unresolved__.t") @ "t") @ "t"),
102-
ETerm(
103-
v = Collapse(
104-
cTm = Redex(
105-
t = Return(
106-
v = Con(name = n"Succ", args = List()) @ "Succ",
107-
usage = Auto()
108-
) @ "Succ",
109-
elims = List(ETerm(v = Var(idx = 2) @ "n"))
110-
) @ "Succ n"
111-
) @ "Succ n"
112-
)
113-
)
114-
) @ "Vec l t (Succ n)"
115-
) @ "Vec l t (Succ n)",
77+
vTy = Con(
78+
name = n"Vec",
79+
args = List(
80+
Var(idx = 4) @ "l",
81+
Var(idx = 3) @ "t",
82+
Con(name = n"Succ", args = List(Var(idx = 2) @ "n")) @ "Succ#{n}"
83+
)
84+
) @ "Vec#{l t Succ#{n}}",
11685
effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total")),
11786
usage = Collapse(cTm = Def(qn = qn"archon.builtin.type.Usage.u1"))
118-
) @ "Vec l t (Succ n)",
87+
) @ "Vec#{l t Succ#{n}}",
11988
effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total"))
120-
) @ "Vec l t n -> Vec l t (Succ n)",
89+
) @ "Vec#{l t n} -> Vec#{l t Succ#{n}}",
12190
effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total"))
122-
) @ "t -> Vec l t n -> Vec l t (Succ n)",
91+
) @ "t -> Vec#{l t n} -> Vec#{l t Succ#{n}}",
12392
effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total"))
124-
) @ "n: Nat -> t -> Vec l t n -> Vec l t (Succ n)"
93+
) @ "n: Nat -> t -> Vec#{l t n} -> Vec#{l t Succ#{n}}"
12594
)
12695
)
12796
)

‎src/test/scala/com/github/tgeng/archon/core/ir/testing/tterm/translation.scala

+62-34
Original file line numberDiff line numberDiff line change
@@ -298,7 +298,7 @@ extension (tps: Seq[TCoPattern])
298298
ctx.globalDefs.get(name) match
299299
// skip existing data type and value constructors
300300
case Some(_: (GData | GDataValue)) =>
301-
case _ => names.addOne(name)
301+
case _ => names.addOne(name)
302302
case TpXConstructor(_, _, args) =>
303303
args.foreach(processPattern)
304304
case _ =>
@@ -312,41 +312,69 @@ extension (td: TDeclaration)
312312
def toPreDeclaration(using ctx: TranslationContext): PreDeclaration =
313313
td match
314314
case TData(name, tParamTys, ty, constructors) =>
315-
val tParamTysCTerm = tParamTys.map:
316-
case (TBinding(name, ty, usage), variance) =>
317-
(Binding(ty.toCTerm, usage.toCTerm)(Name.Normal(name)), variance)
318-
val tyCTerm = ty.toCTerm
319-
val constructorCTerms = constructors.map(_.toPreConstructor)
320-
PreDeclaration.PreData(
321-
ctx.moduleQn / name,
322-
tParamTysCTerm.toList,
323-
tyCTerm,
324-
constructorCTerms.toList,
325-
)
315+
val tParamTysCTerm = translateTParamTysWithVariance(tParamTys.toList)
316+
{
317+
given TranslationContext = ctx.bindLocal(tParamTys.map(_._1.name)*)
318+
val tyCTerm = ty.toCTerm
319+
val constructorCTerms = constructors.map(_.toPreConstructor)
320+
PreDeclaration.PreData(
321+
ctx.moduleQn / name,
322+
tParamTysCTerm,
323+
tyCTerm,
324+
constructorCTerms.toList,
325+
)
326+
}
326327
case TRecord(selfName, name, tParamTys, ty, fields) =>
327-
val tParamTysCTerm = tParamTys.map:
328-
case (TBinding(name, ty, usage), variance) =>
329-
(Binding(ty.toCTerm, usage.toCTerm)(Name.Normal(name)), variance)
330-
val tyCTerm = ty.toCTerm
331-
val fieldCTerms = fields.map(_.toPreField)
332-
PreDeclaration.PreRecord(
333-
ctx.moduleQn / name,
334-
tParamTysCTerm.toList,
335-
tyCTerm,
336-
fieldCTerms.toList,
337-
)
328+
val tParamTysCTerm = translateTParamTysWithVariance(tParamTys.toList)
329+
{
330+
given TranslationContext = ctx.bindLocal(tParamTys.map(_._1.name)*)
331+
val tyCTerm = ty.toCTerm
332+
val fieldCTerms = fields.map(_.toPreField)
333+
PreDeclaration.PreRecord(
334+
ctx.moduleQn / name,
335+
tParamTysCTerm,
336+
tyCTerm,
337+
fieldCTerms.toList,
338+
)
339+
}
338340
case TDefinition(name, tParamTys, ty, clauses) =>
339-
val tParamTysCTerm = tParamTys.map:
340-
case TBinding(name, ty, usage) =>
341-
Binding(ty.toCTerm, usage.toCTerm)(Name.Normal(name))
342-
val tyCTerm = ty.toCTerm
343-
val clauseCTerms = clauses.map(_.toPreClause)
344-
PreDeclaration.PreDefinition(
345-
ctx.moduleQn / name,
346-
tParamTysCTerm.toList,
347-
tyCTerm,
348-
clauseCTerms.toList,
349-
)
341+
val tParamTysCTerm = translateTParamTys(tParamTys.toList)
342+
{
343+
given TranslationContext = ctx.bindLocal(tParamTys.map(_.name)*)
344+
val tyCTerm = ty.toCTerm
345+
val clauseCTerms = clauses.map(_.toPreClause)
346+
PreDeclaration.PreDefinition(
347+
ctx.moduleQn / name,
348+
tParamTysCTerm,
349+
tyCTerm,
350+
clauseCTerms.toList,
351+
)
352+
}
353+
354+
private def translateTParamTys
355+
(bindings: List[TBinding])
356+
(using ctx: TranslationContext)
357+
: List[Binding[CTerm]] =
358+
bindings match
359+
case Nil => Nil
360+
case TBinding(name, ty, usage) :: rest =>
361+
Binding(ty.toCTerm, usage.toCTerm)(Name.Normal(name)) :: translateTParamTys(rest)(using
362+
ctx.bindLocal(name),
363+
)
364+
365+
private def translateTParamTysWithVariance
366+
(bindings: List[(TBinding, Variance)])
367+
(using ctx: TranslationContext)
368+
: List[(Binding[CTerm], Variance)] =
369+
bindings match
370+
case Nil => Nil
371+
case (TBinding(name, ty, usage), variance) :: rest =>
372+
(
373+
Binding(ty.toCTerm, usage.toCTerm)(Name.Normal(name)),
374+
variance,
375+
) :: translateTParamTysWithVariance(rest)(using
376+
ctx.bindLocal(name),
377+
)
350378

351379
extension (tc: TConstructor)
352380
def toPreConstructor(using ctx: TranslationContext): PreConstructor =

0 commit comments

Comments
 (0)