Skip to content

Commit ced19d5

Browse files
robby-phdrobby-phd
committed
Updated Slang LL2 parsers.
1 parent 12e8462 commit ced19d5

File tree

8 files changed

+3255
-2811
lines changed

8 files changed

+3255
-2811
lines changed

‎ast/shared/src/main/scala/org/sireum/lang/ast/SlangLl2PrettyPrinter.scala‎

Lines changed: 99 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -200,13 +200,13 @@ object SlangLl2PrettyPrinter {
200200
}
201201
@strictpure def printIfElse(elseBody: AST.Body): ST = {
202202
elseBody.stmts match {
203-
case ISZ() => st""
203+
case ISZ() => st"}"
204204
case ISZ(ifStmt: AST.Stmt.If) =>
205-
st""" else if ${printExp(ifStmt.cond)} {
205+
st"""} else if ${printExp(ifStmt.cond)} {
206206
| ${(for (stmt <- ifStmt.thenBody.stmts) yield printStmt(F, stmt), lineSep)}
207207
|}${printIfElse(ifStmt.elseBody)}"""
208208
case _ =>
209-
st""" else {
209+
st"""} else {
210210
| ${(for (stmt <- elseBody.stmts) yield printStmt(F, stmt), lineSep)}
211211
|}"""
212212
}
@@ -252,6 +252,48 @@ object SlangLl2PrettyPrinter {
252252
return r
253253
}
254254
}
255+
@strictpure def printLiteral(o: AST.Lit): ST = o.prettyST
256+
@strictpure def printPattern(o: AST.Pattern): ST = o match {
257+
case o: AST.Pattern.Literal => printLiteral(o.lit)
258+
case o: AST.Pattern.LitInterpolate =>
259+
val attr = AST.Attr(o.posOpt)
260+
o.prefix match {
261+
case string"string" => AST.Exp.LitString(o.value, attr).prettyST
262+
case string"s" => AST.Exp.LitString(o.value, attr).prettyST
263+
case string"z" => AST.Exp.LitZ(Z(o.value).get, attr).prettyST
264+
case string"r" => AST.Exp.LitR(R(o.value).get, attr).prettyST
265+
case string"c" => AST.Exp.LitC(ops.StringOps(o.value).first, attr).prettyST
266+
case prefix => st"${o.value}$prefix"
267+
}
268+
case o: AST.Pattern.Ref => st".${printName(o.name)}"
269+
case _: AST.Pattern.SeqWildcard => st"*"
270+
case o: AST.Pattern.Structure =>
271+
val id: ST = o.idOpt match {
272+
case Some(idAt) => st"$idAt@"
273+
case _ => st""
274+
}
275+
val name: ST = o.nameOpt match {
276+
case Some(n) => printName(n)
277+
case _ => st""
278+
}
279+
st"$id$name(${(for (p <- o.patterns) yield printPattern(p), ", ")})"
280+
case o: AST.Pattern.VarBinding => o.tipeOpt match {
281+
case Some(t) => st"${o.id.value}: ${printType(t)}"
282+
case _ => st"${o.id.value}"
283+
}
284+
case o: AST.Pattern.Wildcard => o.typeOpt match {
285+
case Some(t) => st"_: ${printType(t)}"
286+
case _ => st"_"
287+
}
288+
}
289+
@strictpure def printCase(isExp: B, cas: AST.Case): ST = {
290+
val cond: ST = cas.condOpt match {
291+
case Some(cond) => st" if ${printExp(cond)}"
292+
case _ => st""
293+
}
294+
st"""case ${printPattern(cas.pattern)}$cond =>
295+
| ${(for (stmt <- cas.body.stmts) yield printStmt(isExp, stmt), "\n")}"""
296+
}
255297
@strictpure def printStmt(isExp: B, o: AST.Stmt): ST = o match {
256298
case o: AST.Stmt.Adt => halt(s"TODO: $o")
257299
case o: AST.Stmt.Assign => st"${printExp(o.lhs)} = ${printAssignExp(o.rhs)}"
@@ -262,31 +304,51 @@ object SlangLl2PrettyPrinter {
262304
case o: AST.Stmt.DataRefinement => halt(s"TODO: $o")
263305
case o: AST.Stmt.DeduceSequent => halt(s"TODO: $o")
264306
case o: AST.Stmt.DeduceSteps => printDeduceSteps(o)
265-
case o: AST.Stmt.Enum => halt(s"TODO: $o")
307+
case o: AST.Stmt.Enum =>
308+
st"""type @enum ${o.id.value}: {
309+
| ${(for (element <- o.elements) yield element.value, "\n")}
310+
|}"""
266311
case o: AST.Stmt.Expr => if (!isExp && shouldAddDo(o.exp)) st"do ${printExp(o.exp)}" else printExp(o.exp)
267312
case o: AST.Stmt.ExtMethod => halt(s"TODO: $o")
268313
case o: AST.Stmt.Fact =>
269314
val tparams: ST = printTypeParams(o.typeParams)
315+
val desc: ST = o.descOpt match {
316+
case Some(d) =>
317+
st""" @[Desc(
318+
| ${d.prettyST}
319+
|)]"""
320+
case _ => st""
321+
}
270322
val (params, claims): (ST, ISZ[ST]) = if (o.isFun) {
271323
val first = o.claims(0).asInstanceOf[AST.Exp.Quant]
272324
(st"(${(for (p <- first.fun.params) yield st"${p.idOpt.get.value}: ${printType(p.tipeOpt.get)}", ", ")})", ISZ(printAssignExp(first.fun.exp)))
273325
} else {
274326
(st"", for (claim <- o.claims) yield printExp(claim))
275327
}
276-
st"""def ${if (o.typeParams.nonEmpty) st"$tparams " else st""}@fact ${o.id.value}$params = (
328+
st"""def @fact ${o.id.value}$tparams$params$desc = (
277329
| ${(claims, ",\n")}
278330
|)"""
279331
case o: AST.Stmt.For => halt(s"TODO: $o")
280332
case o: AST.Stmt.Havoc => halt(s"TODO: $o")
281333
case o: AST.Stmt.If =>
282334
st"""if ${printExp(o.cond)} {
283335
| ${(for (stmt <- o.thenBody.stmts) yield printStmt(F, stmt), lineSep)}
284-
|}${printIfElse(o.elseBody)}"""
336+
|${printIfElse(o.elseBody)}"""
285337
case o: AST.Stmt.Import => printImport(o)
286338
case o: AST.Stmt.Induct => halt(s"TODO: $o")
287339
case o: AST.Stmt.Inv => halt(s"TODO: $o")
288340
case o: AST.Stmt.JustMethod => halt(s"TODO: $o")
289-
case o: AST.Stmt.Match => halt(s"TODO: $o")
341+
case o: AST.Stmt.Match =>
342+
val cases: ISZ[ST] = for (c <- o.cases) yield printCase(isExp, c)
343+
if (isExp) {
344+
st"""(${printExp(o.exp)}? {
345+
| ${(cases, "\n")}
346+
|})"""
347+
} else {
348+
st"""match ${printExp(o.exp)} {
349+
| ${(cases, "\n")}
350+
|}"""
351+
}
290352
case o: AST.Stmt.Method =>
291353
val tparams: ST = printTypeParams(o.sig.typeParams)
292354
val params: ST = printParams(o.sig.hasParams, o.sig.params)
@@ -306,18 +368,44 @@ object SlangLl2PrettyPrinter {
306368
case o: AST.Stmt.Return => st"return${if (o.expOpt.isEmpty) st"" else st" ${printExp(o.expOpt.get)}"}"
307369
case o: AST.Stmt.RsVal => halt(s"TODO: $o")
308370
case o: AST.Stmt.Sig => halt(s"TODO: $o")
309-
case o: AST.Stmt.SpecBlock => halt(s"TODO: $o")
371+
case o: AST.Stmt.SpecBlock =>
372+
st"""do @spec {
373+
| ${(for (stmt <- o.block.body.stmts) yield printStmt(F, stmt), "\n")}
374+
|}"""
310375
case o: AST.Stmt.SpecLabel => halt(s"TODO: $o")
311376
case o: AST.Stmt.SpecMethod =>
312377
val tparams: ST = printTypeParams(o.sig.typeParams)
313378
val params: ST = printParams(o.sig.hasParams, o.sig.params)
314379
st"def @spec ${o.sig.id.value}$tparams$params: ${printType(o.sig.returnType)}"
315380
case o: AST.Stmt.SpecVar => halt(s"TODO: $o")
316381
case o: AST.Stmt.SubZ => halt(s"TODO: $o")
317-
case o: AST.Stmt.Theorem => halt(s"TODO: $o")
318-
case o: AST.Stmt.TypeAlias => halt(s"TODO: $o")
382+
case o: AST.Stmt.Theorem =>
383+
val tparams: ST = printTypeParams(o.typeParams)
384+
val desc: ST = o.descOpt match {
385+
case Some(d) =>
386+
st""" @[Desc(
387+
| ${d.prettyST}
388+
|)]"""
389+
case _ => st""
390+
}
391+
val (params, claim): (ST, ST) = if (o.isFun) {
392+
val first = o.claim.asInstanceOf[AST.Exp.Quant]
393+
(st"(${(for (p <- first.fun.params) yield st"${p.idOpt.get.value}: ${printType(p.tipeOpt.get)}", ", ")})", printAssignExp(first.fun.exp))
394+
} else {
395+
(st"", printExp(o.claim))
396+
}
397+
st"""def ${if (o.isLemma) "@lemma" else "@theorem"} ${o.id.value}$tparams$params$desc =
398+
| $claim"""
399+
case o: AST.Stmt.TypeAlias =>
400+
val tparams: ST = printTypeParams(o.typeParams)
401+
st"type @alias ${o.id.value}$tparams = ${printType(o.tipe)}"
319402
case o: AST.Stmt.Var => st"${if (o.isVal) "val" else "var"}${if (o.isSpec) " @spec" else ""} ${o.id.value}${if (o.tipeOpt.isEmpty) st"" else st": ${printType(o.tipeOpt.get)}"}${if (o.initOpt.isEmpty) "" else st" = ${printAssignExp(o.initOpt.get)}"}"
320-
case o: AST.Stmt.VarPattern => halt(s"TODO: $o")
403+
case o: AST.Stmt.VarPattern =>
404+
val tipe: ST = o.tipeOpt match {
405+
case Some(t) => st": ${printType(t)}"
406+
case _ => st""
407+
}
408+
st"var ${printPattern(o.pattern)}$tipe = ${printAssignExp(o.init)}"
321409
case o: AST.Stmt.While =>
322410
if (o.contract.isEmpty) {
323411
st"""while ${printExp(o.cond)} {

‎parser/jvm/src/main/java/org/sireum/lang/parser/antlrv4/SlangLl2.interp‎

Lines changed: 5 additions & 3 deletions
Large diffs are not rendered by default.

‎parser/jvm/src/main/java/org/sireum/lang/parser/antlrv4/SlangLl2Lexer.interp‎

Lines changed: 1 addition & 1 deletion
Large diffs are not rendered by default.

0 commit comments

Comments
 (0)