Skip to content

Commit 5eecbf8

Browse files
ilya-klyuchnikovilya-klyuchnikov
committed
cosmetics
1 parent 844865f commit 5eecbf8

File tree

2 files changed

+69
-57
lines changed

2 files changed

+69
-57
lines changed

‎src/main/scala/tapl/fullsimple/parser.scala

Lines changed: 30 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -50,14 +50,17 @@ object FullSimpleParsers extends StandardTokenParsers with PackratParsers with I
5050
"\\",
5151
)
5252

53-
lazy val lcid: PackratParser[String] = ident ^? { case id if id.charAt(0).isLower => id }
54-
lazy val ucid: PackratParser[String] = ident ^? { case id if id.charAt(0).isUpper => id }
55-
lazy val eof: PackratParser[String] = elem("<eof>", _ == lexical.EOF) ^^ { _.chars }
53+
private lazy val lcid: PackratParser[String] =
54+
ident ^? { case id if id.charAt(0).isLower => id }
55+
private lazy val ucid: PackratParser[String] =
56+
ident ^? { case id if id.charAt(0).isUpper => id }
57+
private lazy val eof: PackratParser[String] =
58+
elem("<eof>", _ == lexical.EOF) ^^ { _.chars }
5659

5760
type Res[A] = Context => A
5861
type Res1[A] = Context => (A, Context)
5962

60-
lazy val topLevel: PackratParser[Res1[List[Command]]] =
63+
private lazy val topLevel: PackratParser[Res1[List[Command]]] =
6164
((command <~ ";") ~ topLevel) ^^ {
6265
case f ~ g =>
6366
ctx: Context =>
@@ -66,7 +69,7 @@ object FullSimpleParsers extends StandardTokenParsers with PackratParsers with I
6669
(cmd1 :: cmds, ctx2)
6770
} | success { ctx: Context => (List(), ctx) }
6871

69-
lazy val command: PackratParser[Res1[Command]] =
72+
private lazy val command: PackratParser[Res1[Command]] =
7073
lcid ~ binder ^^ { case id ~ bind => ctx: Context => (Bind(id, bind(ctx)), ctx.addName(id)) } |
7174
ucid ~ tyBinder ^^ {
7275
case id ~ bind => ctx: Context => (Bind(id, bind(ctx)), ctx.addName(id))
@@ -75,15 +78,16 @@ object FullSimpleParsers extends StandardTokenParsers with PackratParsers with I
7578
val t1 = t(ctx); (Eval(t1), ctx)
7679
}
7780

78-
lazy val binder: Parser[Context => Binding] =
81+
private lazy val binder: Parser[Context => Binding] =
7982
":" ~> typ ^^ { t => ctx: Context => VarBind(t(ctx)) } |
8083
"=" ~> term ^^ { t => ctx: Context => TmAbbBind(t(ctx), None) }
81-
lazy val tyBinder: Parser[Context => Binding] =
84+
private lazy val tyBinder: Parser[Context => Binding] =
8285
("=" ~> typ) ^^ { ty => ctx: Context => TyAbbBind(ty(ctx)) } |
8386
success({ ctx: Context => TyVarBind })
8487

85-
lazy val typ: PackratParser[Res[Ty]] = arrowType
86-
lazy val aType: PackratParser[Res[Ty]] =
88+
private lazy val typ: PackratParser[Res[Ty]] =
89+
arrowType
90+
private lazy val aType: PackratParser[Res[Ty]] =
8791
"(" ~> typ <~ ")" |
8892
ucid ^^ { tn => ctx: Context =>
8993
if (ctx.isNameBound(tn)) TyVar(ctx.name2index(tn), ctx.length) else TyId(tn)
@@ -95,21 +99,21 @@ object FullSimpleParsers extends StandardTokenParsers with PackratParsers with I
9599
"{" ~> fieldTypes <~ "}" ^^ { ft => ctx: Context => TyRecord(ft(ctx)) } |
96100
"Nat" ^^ { _ => ctx: Context => TyNat }
97101

98-
lazy val fieldTypes: PackratParser[Res[List[(String, Ty)]]] =
102+
private lazy val fieldTypes: PackratParser[Res[List[(String, Ty)]]] =
99103
repsep(fieldType, ",") ^^ { fs => ctx: Context =>
100104
fs.zipWithIndex.map { case (ft, i) => ft(ctx, i + 1) }
101105
}
102106

103-
lazy val fieldType: PackratParser[(Context, Int) => (String, Ty)] =
107+
private lazy val fieldType: PackratParser[(Context, Int) => (String, Ty)] =
104108
lcid ~ (":" ~> typ) ^^ { case id ~ ty => (ctx: Context, i: Int) => (id, ty(ctx)) } |
105109
typ ^^ { ty => (ctx: Context, i: Int) => (i.toString, ty(ctx)) }
106110

107-
lazy val arrowType: PackratParser[Res[Ty]] =
111+
private lazy val arrowType: PackratParser[Res[Ty]] =
108112
(aType <~ "->") ~ arrowType ^^ { case t1 ~ t2 => ctx: Context => TyArr(t1(ctx), t2(ctx)) } |
109113
aType
110114

111115
// TERMS
112-
lazy val term: PackratParser[Res[Term]] =
116+
private lazy val term: PackratParser[Res[Term]] =
113117
appTerm |
114118
("if" ~> term) ~ ("then" ~> term) ~ ("else" ~> term) ^^ {
115119
case t1 ~ t2 ~ t3 => ctx: Context => TmIf(t1(ctx), t2(ctx), t3(ctx))
@@ -130,30 +134,30 @@ object FullSimpleParsers extends StandardTokenParsers with PackratParsers with I
130134
}
131135
}
132136

133-
lazy val appTerm: PackratParser[Res[Term]] =
137+
private lazy val appTerm: PackratParser[Res[Term]] =
134138
appTerm ~ pathTerm ^^ { case t1 ~ t2 => ctx: Context => TmApp(t1(ctx), t2(ctx)) } |
135139
"fix" ~> pathTerm ^^ { t => ctx: Context => TmFix(t(ctx)) } |
136140
"succ" ~> pathTerm ^^ { t => ctx: Context => TmSucc(t(ctx)) } |
137141
"pred" ~> pathTerm ^^ { t => ctx: Context => TmPred(t(ctx)) } |
138142
"iszero" ~> pathTerm ^^ { t => ctx: Context => TmIsZero(t(ctx)) } |
139143
pathTerm
140144

141-
lazy val ascribeTerm: PackratParser[Res[Term]] =
145+
private lazy val ascribeTerm: PackratParser[Res[Term]] =
142146
aTerm ~ ("as" ~> typ) ^^ { case t ~ ty => ctx: Context => TmAscribe(t(ctx), ty(ctx)) } |
143147
aTerm
144148

145-
lazy val pathTerm: PackratParser[Res[Term]] =
149+
private lazy val pathTerm: PackratParser[Res[Term]] =
146150
pathTerm ~ ("." ~> lcid) ^^ { case t1 ~ l => ctx: Context => TmProj(t1(ctx), l) } |
147151
pathTerm ~ ("." ~> numericLit) ^^ { case t1 ~ l => ctx: Context => TmProj(t1(ctx), l) } |
148152
ascribeTerm
149153

150-
lazy val termSeq: PackratParser[Res[Term]] =
154+
private lazy val termSeq: PackratParser[Res[Term]] =
151155
term ~ (";" ~> termSeq) ^^ {
152156
case t ~ ts => ctx: Context => TmApp(TmAbs("_", TyUnit, ts(ctx.addName("_"))), t(ctx))
153157
} |
154158
term
155159

156-
lazy val aTerm: PackratParser[Res[Term]] =
160+
private lazy val aTerm: PackratParser[Res[Term]] =
157161
"(" ~> termSeq <~ ")" |
158162
"true" ^^ { _ => ctx: Context => TmTrue } |
159163
"false" ^^ { _ => ctx: Context => TmFalse } |
@@ -166,18 +170,20 @@ object FullSimpleParsers extends StandardTokenParsers with PackratParsers with I
166170
"{" ~> fields <~ "}" ^^ { fs => ctx: Context => TmRecord(fs(ctx)) } |
167171
numericLit ^^ { x => ctx: Context => num(x.toInt) }
168172

169-
lazy val cases: PackratParser[Res[List[(String, String, Term)]]] =
173+
private lazy val cases: PackratParser[Res[List[(String, String, Term)]]] =
170174
rep1sep(`case`, "|") ^^ { cs => ctx: Context => cs.map { c => c(ctx) } }
171-
lazy val `case`: PackratParser[Res[(String, String, Term)]] =
175+
176+
private lazy val `case`: PackratParser[Res[(String, String, Term)]] =
172177
("<" ~> lcid <~ "=") ~ (lcid <~ ">") ~ ("==>" ~> term) ^^ {
173178
case l1 ~ l2 ~ t => ctx: Context => (l1, l2, t(ctx.addName(l2)))
174179
}
175180

176-
lazy val fields: PackratParser[Res[List[(String, Term)]]] =
181+
private lazy val fields: PackratParser[Res[List[(String, Term)]]] =
177182
repsep(field, ",") ^^ { fs => ctx: Context =>
178183
fs.zipWithIndex.map { case (ft, i) => ft(ctx, i + 1) }
179184
}
180-
lazy val field: PackratParser[(Context, Int) => (String, Term)] =
185+
186+
private lazy val field: PackratParser[(Context, Int) => (String, Term)] =
181187
lcid ~ ("=" ~> term) ^^ { case id ~ t => (ctx: Context, i: Int) => (id, t(ctx)) } |
182188
term ^^ { t => (ctx: Context, i: Int) => (i.toString, t(ctx)) }
183189

@@ -187,7 +193,8 @@ object FullSimpleParsers extends StandardTokenParsers with PackratParsers with I
187193
case _ => TmSucc(num(x - 1))
188194
}
189195

190-
lazy val phraseTopLevel: PackratParser[Res1[List[Command]]] = phrase(topLevel)
196+
private lazy val phraseTopLevel: PackratParser[Res1[List[Command]]] =
197+
phrase(topLevel)
191198

192199
def input(s: String): Res1[List[Command]] =
193200
phraseTopLevel(new lexical.Scanner(s)) match {

‎src/main/scala/tapl/fullsimple/syntax.scala

Lines changed: 39 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -145,7 +145,7 @@ object Syntax {
145145
def typeShift(d: Int, ty: Ty): Ty =
146146
typeShiftAbove(d, 0, ty)
147147

148-
def bindingShift(d: Int, bind: Binding) =
148+
def bindingShift(d: Int, bind: Binding): Binding =
149149
bind match {
150150
case NameBind => NameBind
151151
case TyVarBind => TyVarBind
@@ -170,7 +170,7 @@ object Syntax {
170170
termShift(-1, termSubst(0, termShift(1, s), t))
171171

172172
// [j -> tyS]
173-
private def typeSubst(tyS: Ty, j: Int, tyT: Ty) = {
173+
private def typeSubst(tyS: Ty, j: Int, tyT: Ty): Ty = {
174174
val onVar = { (c: Int, v: TyVar) =>
175175
if (v.i == c) typeShift(c, tyS) else v
176176
}
@@ -182,20 +182,18 @@ object Syntax {
182182
typeShift(-1, typeSubst(typeShift(1, tyS), 0, tyT))
183183

184184
// really this is for system F only
185-
private def tytermSubst(tyS: Ty, j: Int, t: Term) =
185+
private def tytermSubst(tyS: Ty, j: Int, t: Term): Term =
186186
tmMap((c, tv) => tv, (j, tyT) => typeSubst(tyS, j, tyT), j, t)
187187

188188
// really this is for system F only
189189
def tyTermSubstTop(tyS: Ty, t: Term): Term =
190190
termShift(-1, tytermSubst(typeShift(1, tyS), 0, t))
191-
192191
}
193192

194-
import util.Document
195-
import util.Document._
196-
197-
// outer means that the term is the top-level term
193+
// NB: outer means that the term is the top-level term
198194
object PrettyPrinter {
195+
import util.Document
196+
import util.Document._
199197
import util.Print._
200198

201199
def ptyType(outer: Boolean, ctx: Context, ty: Ty): Document =
@@ -206,7 +204,7 @@ object PrettyPrinter {
206204
def ptyArrowType(outer: Boolean, ctx: Context, tyT: Ty): Document =
207205
tyT match {
208206
case TyArr(tyT1, tyT2) =>
209-
g2(ptyAType(false, ctx, tyT1) :: " ->" :/: ptyArrowType(outer, ctx, tyT2))
207+
g2(ptyAType(outer = false, ctx, tyT1) :: " ->" :/: ptyArrowType(outer, ctx, tyT2))
210208
case tyT =>
211209
ptyAType(outer, ctx, tyT)
212210
}
@@ -222,10 +220,10 @@ object PrettyPrinter {
222220
"Bool"
223221
case TyVariant(fields) =>
224222
def pf(i: Int, li: String, tyTi: Ty): Document =
225-
if (i.toString() == li) {
226-
ptyType(false, ctx, tyTi)
223+
if (i.toString == li) {
224+
ptyType(outer = false, ctx, tyTi)
227225
} else {
228-
li :: ":" :/: ptyType(false, ctx, tyTi)
226+
li :: ":" :/: ptyType(outer = false, ctx, tyTi)
229227
}
230228
"<" :: fields.zipWithIndex
231229
.map { case ((li, tyTi), i) => pf(i + 1, li, tyTi) }
@@ -237,10 +235,10 @@ object PrettyPrinter {
237235
"Unit"
238236
case TyRecord(fields) =>
239237
def pf(i: Int, li: String, tyTi: Ty): Document =
240-
if (i.toString() == li) {
241-
ptyType(false, ctx, tyTi)
238+
if (i.toString == li) {
239+
ptyType(outer = false, ctx, tyTi)
242240
} else {
243-
g0(li :: ":" :/: ptyType(false, ctx, tyTi))
241+
g0(li :: ":" :/: ptyType(outer = false, ctx, tyTi))
244242
}
245243
g2(
246244
"{" :: fields.zipWithIndex
@@ -254,7 +252,8 @@ object PrettyPrinter {
254252
"(" :: ptyType(outer, ctx, tyT) :: ")"
255253
}
256254

257-
def ptyTy(ctx: Context, ty: Ty) = ptyType(true, ctx, ty)
255+
def ptyTy(ctx: Context, ty: Ty): Document =
256+
ptyType(outer = true, ctx, ty)
258257

259258
def ptmTerm(outer: Boolean, ctx: Context, t: Term): Document =
260259
t match {
@@ -267,55 +266,55 @@ object PrettyPrinter {
267266
case TmCase(t, cases) =>
268267
def pc(li: String, xi: String, ti: Term): Document = {
269268
val (ctx1, x1) = ctx.pickFreshName(xi)
270-
"<" :: li :: "=" :: xi :: ">==>" :: ptmTerm(false, ctx1, ti)
269+
"<" :: li :: "=" :: xi :: ">==>" :: ptmTerm(outer = false, ctx1, ti)
271270
}
272271
g2(
273-
"case " :: ptmTerm(false, ctx, t) :: " of" :/:
272+
"case " :: ptmTerm(outer = false, ctx, t) :: " of" :/:
274273
cases.map { case (x, y, z) => pc(x, y, z) }.foldRight(empty: Document)(_ :/: "|" :: _)
275274
)
276275
case TmAbs(x, tyT1, t2) =>
277276
val (ctx1, x1) = ctx.pickFreshName(x)
278-
val abs = g0("lambda" :/: x1 :: ":" :/: ptyType(false, ctx, tyT1) :: ".")
277+
val abs = g0("lambda" :/: x1 :: ":" :/: ptyType(outer = false, ctx, tyT1) :: ".")
279278
val body = ptmTerm(outer, ctx1, t2)
280279
g2(abs :/: body)
281280
case TmLet(x, t1, t2) =>
282281
g0(
283-
"let " :: x :: " = " :: ptmTerm(false, ctx, t1) :/: "in" :/: ptmTerm(
284-
false,
282+
"let " :: x :: " = " :: ptmTerm(outer = false, ctx, t1) :/: "in" :/: ptmTerm(
283+
outer = false,
285284
ctx.addName(x),
286285
t2,
287286
)
288287
)
289288
case TmFix(t1) =>
290-
g2("fix " :: ptmTerm(false, ctx, t1))
289+
g2("fix " :: ptmTerm(outer = false, ctx, t1))
291290
case t => ptmAppTerm(outer, ctx, t)
292291

293292
}
294293

295294
def ptmAppTerm(outer: Boolean, ctx: Context, t: Term): Document =
296295
t match {
297296
case TmApp(t1, t2) =>
298-
g2(ptmAppTerm(false, ctx, t1) :/: ptmATerm(false, ctx, t2))
297+
g2(ptmAppTerm(outer = false, ctx, t1) :/: ptmATerm(outer = false, ctx, t2))
299298
case TmPred(t1) =>
300-
"pred " :: ptmATerm(false, ctx, t1)
299+
"pred " :: ptmATerm(outer = false, ctx, t1)
301300
case TmIsZero(t1) =>
302-
"iszero " :: ptmATerm(false, ctx, t1)
301+
"iszero " :: ptmATerm(outer = false, ctx, t1)
303302
case t =>
304303
ptmPathTerm(outer, ctx, t)
305304
}
306305

307306
def ptmPathTerm(outer: Boolean, ctx: Context, t: Term): Document =
308307
t match {
309308
case TmProj(t1, l) =>
310-
ptmATerm(false, ctx, t1) :: "." :: l
309+
ptmATerm(outer = false, ctx, t1) :: "." :: l
311310
case t1 =>
312311
ptmAscribeTerm(outer, ctx, t1)
313312
}
314313

315314
def ptmAscribeTerm(outer: Boolean, ctx: Context, t: Term): Document =
316315
t match {
317316
case TmAscribe(t1, tyT1) =>
318-
g0(ptmAppTerm(false, ctx, t1) :/: "as " :: ptyType(false, ctx, tyT1))
317+
g0(ptmAppTerm(outer = false, ctx, t1) :/: "as " :: ptyType(outer = false, ctx, tyT1))
319318
case t1 =>
320319
ptmATerm(outer, ctx, t1)
321320
}
@@ -327,7 +326,13 @@ object PrettyPrinter {
327326
case TmFalse =>
328327
"false"
329328
case TmTag(l, t, ty) =>
330-
g2("<" :: l :: "=" :: ptmTerm(false, ctx, t) :: ">" :/: "as " :: ptyType(outer, ctx, ty))
329+
g2(
330+
"<" :: l :: "=" :: ptmTerm(outer = false, ctx, t) :: ">" :/: "as " :: ptyType(
331+
outer,
332+
ctx,
333+
ty,
334+
)
335+
)
331336
case TmVar(x, n) =>
332337
if (ctx.length == n) ctx.index2Name(x)
333338
else text("[bad index: " + x + "/" + n + " in {" + ctx.l.mkString(", ") + "}]")
@@ -337,10 +342,10 @@ object PrettyPrinter {
337342
"unit"
338343
case TmRecord(fields) =>
339344
def pf(i: Int, li: String, t: Term): Document =
340-
if (i.toString() == li) {
341-
ptmTerm(false, ctx, t)
345+
if (i.toString == li) {
346+
ptmTerm(outer = false, ctx, t)
342347
} else {
343-
li :: "=" :: ptmTerm(false, ctx, t)
348+
li :: "=" :: ptmTerm(outer = false, ctx, t)
344349
}
345350
"{" :: fields.zipWithIndex
346351
.map { case ((li, tyTi), i) => pf(i + 1, li, tyTi) }
@@ -356,14 +361,15 @@ object PrettyPrinter {
356361
case TmSucc(s) =>
357362
pf(i + 1, s)
358363
case _ =>
359-
"(succ " :: ptmATerm(false, ctx, t1) :: ")"
364+
"(succ " :: ptmATerm(outer = false, ctx, t1) :: ")"
360365
}
361366
pf(1, t1)
362367
case t =>
363368
"(" :: ptmTerm(outer, ctx, t) :: ")"
364369
}
365370

366-
def ptm(ctx: Context, t: Term) = ptmTerm(true, ctx, t)
371+
def ptm(ctx: Context, t: Term): Document =
372+
ptmTerm(outer = true, ctx, t)
367373

368374
def pBinding(ctx: Context, bind: Binding): Document =
369375
bind match {
@@ -394,5 +400,4 @@ object PrettyPrinter {
394400
case TyAbbBind(ty) =>
395401
":: *"
396402
}
397-
398403
}

0 commit comments

Comments
 (0)