Skip to content

Commit e3e6921

Browse files
tgengtgeng
committed
remove special syntax for constructor
1 parent b532524 commit e3e6921

File tree

12 files changed

+95
-83
lines changed

12 files changed

+95
-83
lines changed

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

+8-10
Original file line numberDiff line numberDiff line change
@@ -48,16 +48,14 @@ List(
4848
PreConstructor(
4949
name = n"Refl",
5050
ty = F(
51-
vTy = Collapse(
52-
cTm = Redex(
53-
t = Return(v = DataType(qn = qn"test.Eq", args = List()) @ "Eq", usage = Auto()) @ "Eq",
54-
elims = List(
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")
59-
)
60-
) @ "Eq l A x x"
51+
vTy = DataType(
52+
qn = qn"test.Eq",
53+
args = List(
54+
Var(idx = 2) @ "l",
55+
Var(idx = 1) @ "A",
56+
Var(idx = 0) @ "x",
57+
Var(idx = 0) @ "x"
58+
)
6159
) @ "Eq l A x x",
6260
effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total")),
6361
usage = Collapse(cTm = Def(qn = qn"archon.builtin.type.Usage.u1"))

‎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

+33-20
Original file line numberDiff line numberDiff line change
@@ -36,13 +36,17 @@ List(
3636
TConstructor(
3737
name = "Nil",
3838
ty = TF(
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}",
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",
4347
effects = TDef(qn = qn"archon.builtin.effects.total"),
4448
usage = TDef(qn = qn"archon.builtin.type.Usage.u1")
45-
) @ "Vec#{l t Zero}"
49+
) @ "Vec l t Zero"
4650
),
4751
TConstructor(
4852
name = "Succ",
@@ -61,30 +65,39 @@ List(
6165
bodyType = TFunctionType(
6266
arg = TBinding(
6367
name = "_",
64-
ty = TCon(
65-
name = "Vec",
66-
args = List(TId(id = "l"), TId(id = "t"), TId(id = "n") @ "n")
67-
) @ "Vec#{l t n}",
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",
6876
usage = TDef(qn = qn"archon.builtin.type.Usage.uAny")
6977
),
7078
bodyType = TF(
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}"
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+
)
7790
)
78-
) @ "Vec#{l t Succ#{n}}",
91+
) @ "Vec l t (Succ n)",
7992
effects = TDef(qn = qn"archon.builtin.effects.total"),
8093
usage = TDef(qn = qn"archon.builtin.type.Usage.u1")
81-
) @ "Vec#{l t Succ#{n}}",
94+
) @ "Vec l t (Succ n)",
8295
effects = TDef(qn = qn"archon.builtin.effects.total")
83-
) @ "Vec#{l t n} -> Vec#{l t Succ#{n}}",
96+
) @ "Vec l t n -> Vec l t (Succ n)",
8497
effects = TDef(qn = qn"archon.builtin.effects.total")
85-
) @ "t -> Vec#{l t n} -> Vec#{l t Succ#{n}}",
98+
) @ "t -> Vec l t n -> Vec l t (Succ n)",
8699
effects = TDef(qn = qn"archon.builtin.effects.total")
87-
) @ "n: Nat -> t -> Vec#{l t n} -> Vec#{l t Succ#{n}}"
100+
) @ "n: Nat -> t -> Vec l t n -> Vec l t (Succ n)"
88101
)
89102
)
90103
)

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

+9-9
Original file line numberDiff line numberDiff line change
@@ -48,10 +48,10 @@ List(
4848
Var(idx = 0) @ "t",
4949
Collapse(cTm = Def(qn = qn"__unresolved__.Zero") @ "Zero") @ "Zero"
5050
)
51-
) @ "Vec#{l t Zero}",
51+
) @ "Vec l t Zero",
5252
effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total")),
5353
usage = Collapse(cTm = Def(qn = qn"archon.builtin.type.Usage.u1"))
54-
) @ "Vec#{l t Zero}"
54+
) @ "Vec l t Zero"
5555
),
5656
PreConstructor(
5757
name = n"Succ",
@@ -70,7 +70,7 @@ List(
7070
ty = DataType(
7171
qn = qn"test.Vec",
7272
args = List(Var(idx = 3) @ "l", Var(idx = 2) @ "t", Var(idx = 1) @ "n")
73-
) @ "Vec#{l t n}",
73+
) @ "Vec l t n",
7474
usage = Collapse(cTm = Def(qn = qn"archon.builtin.type.Usage.uAny"))
7575
) @ "_",
7676
bodyTy = F(
@@ -79,18 +79,18 @@ List(
7979
args = List(
8080
Var(idx = 4) @ "l",
8181
Var(idx = 3) @ "t",
82-
Con(name = n"Succ", args = List(Var(idx = 2) @ "n")) @ "Succ#{n}"
82+
Con(name = n"Succ", args = List(Var(idx = 2) @ "n")) @ "Succ n"
8383
)
84-
) @ "Vec#{l t Succ#{n}}",
84+
) @ "Vec l t (Succ n)",
8585
effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total")),
8686
usage = Collapse(cTm = Def(qn = qn"archon.builtin.type.Usage.u1"))
87-
) @ "Vec#{l t Succ#{n}}",
87+
) @ "Vec l t (Succ n)",
8888
effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total"))
89-
) @ "Vec#{l t n} -> Vec#{l t Succ#{n}}",
89+
) @ "Vec l t n -> Vec l t (Succ n)",
9090
effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total"))
91-
) @ "t -> Vec#{l t n} -> Vec#{l t Succ#{n}}",
91+
) @ "t -> Vec l t n -> Vec l t (Succ n)",
9292
effects = Collapse(cTm = Def(qn = qn"archon.builtin.effects.total"))
93-
) @ "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)"
9494
)
9595
)
9696
)

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ Succ: Nat -> Nat
44

55
def plus: Nat -> Nat -> <> Nat
66
Zero n = n
7-
Succ#{m} n = Succ#{(plus m n)}
7+
(Succ m) n = Succ (plus m n)

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

+10-8
Original file line numberDiff line numberDiff line change
@@ -77,15 +77,17 @@ List(
7777
TcPattern(pattern = TpId(name = "n"))
7878
),
7979
body = Some(
80-
value = TCon(
81-
name = "Succ",
82-
args = List(
83-
TRedex(
84-
c = TId(id = "plus") @ "plus",
85-
elims = List(ETerm(v = TId(id = "m") @ "m"), ETerm(v = TId(id = "n")))
86-
) @ "plus m n"
80+
value = TRedex(
81+
c = TId(id = "Succ") @ "Succ",
82+
elims = List(
83+
ETerm(
84+
v = TRedex(
85+
c = TId(id = "plus") @ "plus",
86+
elims = List(ETerm(v = TId(id = "m") @ "m"), ETerm(v = TId(id = "n")))
87+
) @ "plus m n"
88+
)
8789
)
88-
) @ "Succ#{(plus m n)}"
90+
) @ "Succ (plus m n)"
8991
)
9092
)
9193
)

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -86,9 +86,9 @@ List(
8686
tBinding = Binding(ty = Auto(), usage = Auto()) @ "$v",
8787
eff = Auto(),
8888
body = Return(
89-
v = Con(name = n"Succ", args = List(Var(idx = 0) @ "plus m n")) @ "Succ#{(plus m n)}",
89+
v = Con(name = n"Succ", args = List(Var(idx = 0) @ "plus m n")) @ "Succ (plus m n)",
9090
usage = Auto()
91-
) @ "Succ#{(plus m n)}"
91+
) @ "Succ (plus m n)"
9292
) @ "ε"
9393
)
9494
)

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ Succ: Nat -> Nat
44

55
def prec: Nat -> <> Nat
66
Zero = Zero
7-
Succ#{m} = m
7+
(Succ m) = m

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

+8-10
Original file line numberDiff line numberDiff line change
@@ -27,13 +27,9 @@ class Parser(val text: String, val path: Option[Path], val indent: Int):
2727
PT(("." ~~ id).repX(1).!)(s => TTerm.TDef(QualifiedName.from(s.drop(1))))
2828
private def tU[$: P]: P[TTerm] = PT("U" ~/ atom)(TTerm.TU(_))
2929
private def tForce[$: P]: P[TTerm] = PT("force" ~/ atom)(TTerm.TForce(_))
30-
// TODO[P0]: add special syntax for constructor, projection, and operation, and remove derived
31-
// definitions from data, record, and effect.
32-
private def tCon[$: P]: P[TTerm] = PT(id ~ "#{" ~/ atom.rep ~ "}"):
33-
case (name, args) => TTerm.TCon(name, args.toList)
3430

3531
private def atom[$: P]: P[TTerm] = P(
36-
"(" ~/ tTerm ~ ")" | tAuto | tDef | tLevelLiteral | tForce | tU | tCon | tId,
32+
"(" ~/ tTerm ~ ")" | tAuto | tDef | tLevelLiteral | tForce | tU | tId,
3733
)
3834
private def tThunk[$: P]: P[TTerm] = PT("thunk" ~/ tTerm)(TTerm.TThunk(_))
3935
private def tF[$: P]: P[TTerm] =
@@ -68,7 +64,7 @@ class Parser(val text: String, val path: Option[Path], val indent: Int):
6864
case Left(t) => Elimination.ETerm(t)
6965
case Right(n) => Elimination.EProj(Name.Normal(n))
7066

71-
private def tRedex[$: P]: P[TTerm] = PT((atom ~ indented(_.elim.rep))):
67+
private def tRedex[$: P]: P[TTerm] = PT(atom ~ indented(_.elim.rep)):
7268
case (f, elims) =>
7369
if elims.isEmpty then f else TTerm.TRedex(f, elims.toList)
7470

@@ -130,7 +126,7 @@ class Parser(val text: String, val path: Option[Path], val indent: Int):
130126
private def tTermEnd[$: P]: P[TTerm] = P(tTerm ~ End)
131127

132128
private def tBindingAndVariance[$: P]: P[(TBinding, Variance)] = P(
133-
(("+" | "-").!.? ~ "(" ~ tBinding ~ ")").map:
129+
(("+" | "-").!.? ~ "(" ~/ tBinding ~ ")").map:
134130
case (Some("+"), b) => (b, Variance.COVARIANT)
135131
case (Some("-"), b) => (b, Variance.CONTRAVARIANT)
136132
case (None, b) => (b, Variance.INVARIANT)
@@ -162,17 +158,19 @@ class Parser(val text: String, val path: Option[Path], val indent: Int):
162158

163159
private def tpVar[$: P]: P[TPattern] = PT(id)(TPattern.TpId.apply)
164160
private def tpXConstructor[$: P]: P[TPattern] =
165-
PT(".".!.?.map(_.isDefined) ~ id ~ "#{" ~/ tPattern.rep ~ "}")(TPattern.TpXConstructor.apply)
161+
PT(".".!.?.map(_.isDefined) ~ id ~ tPattern.rep)(TPattern.TpXConstructor.apply)
166162
private def tpForced[$: P]: P[TPattern] = PT("." ~ "(" ~/ tTerm ~ ")")(TPattern.TpForced.apply)
167163
private def tpAbsurd[$: P]: P[TPattern] = PT("()")(_ => TPattern.TPAbsurd())
168-
private def tPattern[$: P]: P[TPattern] = P(tpAbsurd | tpForced | tpXConstructor | tpVar)
164+
private def tPattern[$: P]: P[TPattern] = P(
165+
tpAbsurd | "(" ~/ tpXConstructor ~ ")" | tpVar | tpForced,
166+
)
169167

170168
private def tCoPattern[$: P]: P[TCoPattern] = P(
171169
tProjection | tPattern.map(TCoPattern.TcPattern.apply),
172170
)
173171

174172
private def tClause[$: P]: P[TClause] = P(
175-
(tCoPattern.rep ~ "=" ~ indented(_.tTerm).?).map(TClause.apply),
173+
(NoCut(tCoPattern).rep ~ "=" ~ indented(_.tTerm).?).map(TClause.apply),
176174
)
177175

178176
private def tDefinition[$: P]: P[TDeclaration] = P(

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

-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ enum TTerm(val sourceInfo: SourceInfo):
1515
case TThunk(t: TTerm)(using sourceInfo: SourceInfo) extends TTerm(sourceInfo)
1616
case TLevelLiteral(level: Nat)(using sourceInfo: SourceInfo) extends TTerm(sourceInfo)
1717
case TAuto()(using sourceInfo: SourceInfo) extends TTerm(sourceInfo)
18-
case TCon(name: String, args: List[TTerm])(using sourceInfo: SourceInfo) extends TTerm(sourceInfo)
1918
case TF(ty: TTerm, effects: TTerm, usage: TTerm)(using sourceInfo: SourceInfo)
2019
extends TTerm(sourceInfo)
2120
case TLet

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

+15-13
Original file line numberDiff line numberDiff line change
@@ -104,17 +104,7 @@ extension (tTerm: TTerm)
104104
def toCTerm(using ctx: TranslationContext): CTerm =
105105
given SourceInfo = tTerm.sourceInfo
106106
tTerm match
107-
case TAuto() => Return(Auto())
108-
case TCon(name, args) =>
109-
translate(args*) { case args =>
110-
given SourceInfo = tTerm.sourceInfo
111-
ctx.globalDefs.get(name) match
112-
case Some(GData(qn)) => Return(DataType(qn, args.toList))
113-
case Some(GDataValue(n)) => Return(Con(n, args.toList))
114-
case Some(GEffect(qn)) => Return(EffectsLiteral(Set((qn, args.toList))))
115-
case Some(GRecord(qn)) => RecordType(qn, args.toList)
116-
case _ => throw UnresolvedSymbol(name)
117-
}
107+
case TAuto() => Return(Auto())
118108
case TU(t) => Return(U(t.toCTerm(using ctx.copy(isTypeLevel = true))))
119109
case TThunk(t) => Return(Thunk(t.toCTerm))
120110
case TLevelLiteral(level) => Return(LevelLiteral(level))
@@ -146,7 +136,7 @@ extension (tTerm: TTerm)
146136
body.toCTerm(using ctx.bindLocal(name)),
147137
)
148138
}
149-
case TRedex(c, elims) =>
139+
case r@TRedex(c, elims) =>
150140
translate(elims.flatMap {
151141
case Elimination.ETerm(t) => Seq(t)
152142
case _ => Seq.empty
@@ -160,7 +150,19 @@ extension (tTerm: TTerm)
160150
index = index + 1
161151
Elimination.ETerm[VTerm](arg)
162152
case Elimination.EProj(name) => Elimination.EProj[VTerm](name)
163-
redex(c.toCTerm, translatedElims)
153+
c match
154+
case TId(id) =>
155+
given SourceInfo = r.sourceInfo
156+
lazy val args = translatedElims.map:
157+
case Elimination.ETerm(v) => v
158+
case _ => throw new IllegalArgumentException("Unexpected projection")
159+
ctx.lookup(id) match
160+
case Right(GData(qn)) => Return(DataType(qn, args))
161+
case Right(GDataValue(n)) => Return(Con(n, args))
162+
case Right(GRecord(qn)) => RecordType(qn, args)
163+
case Right(GEffect(qn)) => Return(EffectsLiteral(Set((qn, args))))
164+
case _ => redex(c.toCTerm, translatedElims)
165+
case _ => redex(c.toCTerm, translatedElims)
164166
case TFunctionType(arg, bodyType, effects) =>
165167
given TranslationContext = ctx.copy(isTypeLevel = true)
166168
translate(arg.ty, arg.usage, effects) { case Seq(ty, usage, effects) =>

‎src/test/scala/com/github/tgeng/archon/core/ir/typing/BasicTypeCheckSpec.scala

+6-6
Original file line numberDiff line numberDiff line change
@@ -130,23 +130,23 @@ class BasicTypeCheckSpec extends AnyFreeSpec:
130130
data Nat: Type 0L
131131
Zero: Nat
132132
Succ: Nat -> Nat
133-
133+
134134
def prec: Nat -> <> Nat
135135
Zero = Zero
136-
Succ#{m} = m
136+
(Succ m) = m
137137

138138
data Vec (l: Level) +(t: Type l): Nat -> Type l
139-
Nil: Vec#{l t Zero}
140-
Succ: n: Nat -> t -> Vec#{l t n} -> Vec#{l t Succ#{n}}
139+
Nil: Vec l t Zero
140+
Succ: n: Nat -> t -> Vec l t n -> Vec l t (Succ n)
141141
""".inUse:
142142
assertVType(vt"Nat", Type(Top(LevelLiteral(0))))
143143
assertVType(vt"Zero", vt"Nat")
144144
assertCType(
145-
ct"prec (Succ #{Zero})",
145+
ct"prec (Succ Zero)",
146146
ct"<> Nat",
147147
)
148148
assertCConvertible(
149-
ct"prec (Succ #{Zero})",
149+
ct"prec (Succ Zero)",
150150
ct"Zero",
151151
Some(ct"<> Nat"),
152152
)

0 commit comments

Comments
 (0)