Skip to content

Commit ca0dbcc

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

File tree

6 files changed

+3202
-4750
lines changed

6 files changed

+3202
-4750
lines changed

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

Lines changed: 66 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -80,44 +80,75 @@ object SlangLl2PrettyPrinter {
8080
AST.Exp.Binary.prettyST(op, o.isRightAssoc, printExp(o.left), leftOpOpt, o.left.isInstanceOf[AST.Exp.If],
8181
printExp(o.right), rightOpOpt, o.right.isInstanceOf[AST.Exp.If])
8282
}
83+
@strictpure def printRange(o: AST.EnumGen.Range): ST = o match {
84+
case o: AST.EnumGen.Range.Expr => printExp(o.exp)
85+
case o: AST.EnumGen.Range.Step =>
86+
val byOpt: ST = o.byOpt match {
87+
case Some(by) => st" by ${printExp(by)}"
88+
case _ => st""
89+
}
90+
st"${printExp(o.start)} ${if (o.isInclusive) ".." else "..<"} ${printExp(o.end)}$byOpt"
91+
}
92+
@strictpure def printLoopContract(o: AST.LoopContract): ST = {
93+
val modifies: ISZ[ST] = for (m <- o.modifies) yield printExp(m.asExp)
94+
val contracts: ISZ[ST] = (if (modifies.isEmpty) ISZ[ST]() else ISZ(st"Modifies(${(modifies, ", ")})")) ++
95+
(for (inv <- o.invariants) yield printExp(inv))
96+
if (o.isEmpty) st"" else
97+
st""" @[
98+
| ${(contracts, s",$lineSep")}
99+
|]"""
100+
}
101+
102+
@strictpure def printEnumGen(o: AST.EnumGen.For): ST = {
103+
val idOpt: String = o.idOpt match {
104+
case Some(id) => id.value
105+
case _ => "_"
106+
}
107+
val condOpt: ST = o.condOpt match {
108+
case Some(cond) => st" if ${printExp(cond)}"
109+
case _ => st""
110+
}
111+
st"$idOpt: ${printRange(o.range)}$condOpt${printLoopContract(o.contract)}"
112+
}
113+
83114
@strictpure def printExp(o: AST.Exp): ST = o match {
84115
case o: AST.Exp.AssertAgree => halt(s"TODO: $o")
85116
case o: AST.Exp.AssumeAgree => halt(s"TODO: $o")
117+
case o: AST.Exp.InfoFlowInvariant => halt(s"TODO: $o")
118+
case o: AST.Exp.Fun => halt(s"TODO: $o")
86119
case o: AST.Exp.At => halt(s"TODO: $o")
120+
case o: AST.Exp.Labeled => halt(s"TODO: $o")
121+
case o: AST.Exp.LoopIndex => halt(s"TODO: $o")
122+
case o: AST.Exp.RS => halt(s"TODO: $o")
123+
case o: AST.Exp.StateSeq => halt(s"TODO: $o")
124+
case o: AST.Exp.StrictPureBlock => halt(s"TODO: $o")
125+
case o: AST.Exp.StringInterpolate => halt(s"TODO: $o")
126+
case o: AST.Exp.Sym => halt(s"TODO: $o")
127+
case o: AST.Exp.TypeCond => halt(s"TODO: $o")
87128
case o: AST.Exp.Binary => printBinary(o)
88129
case o: AST.Exp.Eta => st"${printExp(o.ref.asExp)} _"
89-
case o: AST.Exp.ForYield => halt(s"TODO: $o")
90-
case o: AST.Exp.Fun => halt(s"TODO: $o")
130+
case o: AST.Exp.ForYield => st"yield ${(for (g <- o.enumGens) yield printEnumGen(g), ", ")} => ${printExp(o.exp)}"
91131
case o: AST.Exp.Ident => st"${o.id.value}"
92132
case o: AST.Exp.If => st"(${printExp(o.cond)}? ${printExp(o.thenExp)} : ${printExp(o.elseExp)})"
93-
case o: AST.Exp.InfoFlowInvariant => halt(s"TODO: $o")
94133
case o: AST.Exp.Input => st"In(${printExp(o.exp)})"
95134
case o: AST.Exp.Invoke => printInvoke(o)
96135
case o: AST.Exp.InvokeNamed => printInvokeNamed(o)
97-
case o: AST.Exp.Labeled => halt(s"TODO: $o")
98136
case o: AST.Exp.LitB => o.prettyST
99137
case o: AST.Exp.LitC => o.prettyST
100138
case o: AST.Exp.LitF32 => o.prettyST
101139
case o: AST.Exp.LitF64 => o.prettyST
102140
case o: AST.Exp.LitR => o.prettyST
103141
case o: AST.Exp.LitString => o.prettyST
104142
case o: AST.Exp.LitZ => o.prettyST
105-
case o: AST.Exp.LoopIndex => halt(s"TODO: $o")
106143
case o: AST.Exp.Old => st"Old(${printExp(o.exp)})"
107144
case o: AST.Exp.QuantEach => st"${if (o.isForall) "∀" else "∃"} ${(for (p <- o.fun.params) yield st"${p.idOpt.get.value}: ${printExp(o.seq)}", ", ")} => ${printAssignExp(o.fun.exp)}"
108145
case o: AST.Exp.QuantRange => st"${if (o.isForall) "∀" else "∃"} ${(for (p <- o.fun.params) yield st"${p.idOpt.get.value}: ${printExp(o.lo)} ${if (o.hiExact) ".." else "..<"} ${printExp(o.hi)}", ", ")} => ${printAssignExp(o.fun.exp)}"
109146
case o: AST.Exp.QuantType => st"${if (o.isForall) "∀" else "∃"} ${(for (p <- o.fun.params) yield st"${p.idOpt.get.value}: ${printType(p.tipeOpt.get)}", ", ")} => ${printAssignExp(o.fun.exp)}"
110147
case _: AST.Exp.Result => st"Res"
111-
case o: AST.Exp.RS => halt(s"TODO: $o")
112148
case o: AST.Exp.Select => st"${if (o.receiverOpt.isEmpty) st"" else st"${printExp(o.receiverOpt.get)}."}${o.id.value}${if (o.targs.isEmpty) st"" else st"[${(for (t <- o.targs) yield printType(t), ", ")}]"}"
113-
case o: AST.Exp.StateSeq => halt(s"TODO: $o")
114-
case o: AST.Exp.StrictPureBlock => halt(s"TODO: $o")
115-
case o: AST.Exp.StringInterpolate => halt(s"TODO: $o")
116149
case _: AST.Exp.Super => st"super"
117-
case o: AST.Exp.Sym => halt(s"TODO: $o")
118150
case _: AST.Exp.This => st"this"
119151
case o: AST.Exp.Tuple => st"(${(for (exp <- o.args) yield printExp(exp), ", ")})"
120-
case o: AST.Exp.TypeCond => halt(s"TODO: $o")
121152
case o: AST.Exp.Unary =>
122153
val paren: B = o.exp match {
123154
case _: Exp.Ident => F
@@ -292,24 +323,35 @@ object SlangLl2PrettyPrinter {
292323
case _ => st""
293324
}
294325
st"""case ${printPattern(cas.pattern)}$cond =>
295-
| ${(for (stmt <- cas.body.stmts) yield printStmt(isExp, stmt), "\n")}"""
326+
| ${(for (stmt <- cas.body.stmts) yield printStmt(isExp, stmt), lineSep)}"""
296327
}
297328
@strictpure def printStmt(isExp: B, o: AST.Stmt): ST = o match {
329+
case o: AST.Stmt.DataRefinement => halt(s"TODO: $o")
298330
case o: AST.Stmt.Adt => halt(s"TODO: $o")
331+
case o: AST.Stmt.DeduceSequent => halt(s"TODO: $o")
332+
case o: AST.Stmt.ExtMethod => halt(s"TODO: $o")
333+
case o: AST.Stmt.For => halt(s"TODO: $o")
334+
case o: AST.Stmt.Havoc => halt(s"TODO: $o")
335+
case o: AST.Stmt.Induct => halt(s"TODO: $o")
336+
case o: AST.Stmt.Inv => halt(s"TODO: $o")
337+
case o: AST.Stmt.JustMethod => halt(s"TODO: $o")
338+
case o: AST.Stmt.Object => halt(s"TODO: $o")
339+
case o: AST.Stmt.RsVal => halt(s"TODO: $o")
340+
case o: AST.Stmt.Sig => halt(s"TODO: $o")
341+
case o: AST.Stmt.SpecLabel => halt(s"TODO: $o")
342+
case o: AST.Stmt.SpecVar => halt(s"TODO: $o")
343+
case o: AST.Stmt.SubZ => halt(s"TODO: $o")
299344
case o: AST.Stmt.Assign => st"${printExp(o.lhs)} = ${printAssignExp(o.rhs)}"
300345
case o: AST.Stmt.Block =>
301346
st"""${if (isExp) "" else "do "}{
302347
| ${(for (stmt <- o.body.stmts) yield printStmt(F, stmt), lineSep)}
303348
|}"""
304-
case o: AST.Stmt.DataRefinement => halt(s"TODO: $o")
305-
case o: AST.Stmt.DeduceSequent => halt(s"TODO: $o")
306349
case o: AST.Stmt.DeduceSteps => printDeduceSteps(o)
307350
case o: AST.Stmt.Enum =>
308351
st"""type @enum ${o.id.value}: {
309-
| ${(for (element <- o.elements) yield element.value, "\n")}
352+
| ${(for (element <- o.elements) yield element.value, lineSep)}
310353
|}"""
311354
case o: AST.Stmt.Expr => if (!isExp && shouldAddDo(o.exp)) st"do ${printExp(o.exp)}" else printExp(o.exp)
312-
case o: AST.Stmt.ExtMethod => halt(s"TODO: $o")
313355
case o: AST.Stmt.Fact =>
314356
val tparams: ST = printTypeParams(o.typeParams)
315357
val desc: ST = o.descOpt match {
@@ -326,29 +368,18 @@ object SlangLl2PrettyPrinter {
326368
(st"", for (claim <- o.claims) yield printExp(claim))
327369
}
328370
st"""def @fact ${o.id.value}$tparams$params$desc = (
329-
| ${(claims, ",\n")}
371+
| ${(claims, s",$lineSep")}
330372
|)"""
331-
case o: AST.Stmt.For => halt(s"TODO: $o")
332-
case o: AST.Stmt.Havoc => halt(s"TODO: $o")
333373
case o: AST.Stmt.If =>
334374
st"""if ${printExp(o.cond)} {
335375
| ${(for (stmt <- o.thenBody.stmts) yield printStmt(F, stmt), lineSep)}
336376
|${printIfElse(o.elseBody)}"""
337377
case o: AST.Stmt.Import => printImport(o)
338-
case o: AST.Stmt.Induct => halt(s"TODO: $o")
339-
case o: AST.Stmt.Inv => halt(s"TODO: $o")
340-
case o: AST.Stmt.JustMethod => halt(s"TODO: $o")
341378
case o: AST.Stmt.Match =>
342379
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-
}
380+
st"""match ${printExp(o.exp)} {
381+
| ${(cases, lineSep)}
382+
|}"""
352383
case o: AST.Stmt.Method =>
353384
val tparams: ST = printTypeParams(o.sig.typeParams)
354385
val params: ST = printParams(o.sig.hasParams, o.sig.params)
@@ -364,21 +395,15 @@ object SlangLl2PrettyPrinter {
364395
|}"""
365396
case _ => header
366397
}
367-
case o: AST.Stmt.Object => halt(s"TODO: $o")
368398
case o: AST.Stmt.Return => st"return${if (o.expOpt.isEmpty) st"" else st" ${printExp(o.expOpt.get)}"}"
369-
case o: AST.Stmt.RsVal => halt(s"TODO: $o")
370-
case o: AST.Stmt.Sig => halt(s"TODO: $o")
371399
case o: AST.Stmt.SpecBlock =>
372400
st"""do @spec {
373-
| ${(for (stmt <- o.block.body.stmts) yield printStmt(F, stmt), "\n")}
401+
| ${(for (stmt <- o.block.body.stmts) yield printStmt(F, stmt), lineSep)}
374402
|}"""
375-
case o: AST.Stmt.SpecLabel => halt(s"TODO: $o")
376403
case o: AST.Stmt.SpecMethod =>
377404
val tparams: ST = printTypeParams(o.sig.typeParams)
378405
val params: ST = printParams(o.sig.hasParams, o.sig.params)
379406
st"def @spec ${o.sig.id.value}$tparams$params: ${printType(o.sig.returnType)}"
380-
case o: AST.Stmt.SpecVar => halt(s"TODO: $o")
381-
case o: AST.Stmt.SubZ => halt(s"TODO: $o")
382407
case o: AST.Stmt.Theorem =>
383408
val tparams: ST = printTypeParams(o.typeParams)
384409
val desc: ST = o.descOpt match {
@@ -407,20 +432,9 @@ object SlangLl2PrettyPrinter {
407432
}
408433
st"var ${printPattern(o.pattern)}$tipe = ${printAssignExp(o.init)}"
409434
case o: AST.Stmt.While =>
410-
if (o.contract.isEmpty) {
411-
st"""while ${printExp(o.cond)} {
412-
| ${(for (stmt <- o.body.stmts) yield printStmt(F, stmt), lineSep)}
413-
|}"""
414-
} else {
415-
val modifies: ISZ[ST] = for (m <- o.contract.modifies) yield printExp(m.asExp)
416-
val contracts: ISZ[ST] = (if (modifies.isEmpty) ISZ[ST]() else ISZ(st"Modifies(${(modifies, ", ")})")) ++
417-
(for (inv <- o.contract.invariants) yield printExp(inv))
418-
st"""while ${printExp(o.cond)} @[
419-
| ${(contracts, s",$lineSep")}
420-
|] {
421-
| ${(for (stmt <- o.body.stmts) yield printStmt(F, stmt), lineSep)}
422-
|}"""
423-
}
435+
st"""while ${printExp(o.cond)}${printLoopContract(o.contract)} {
436+
| ${(for (stmt <- o.body.stmts) yield printStmt(F, stmt), lineSep)}
437+
|}"""
424438
}
425439
val packageOpt: Option[ST] = if (ast.packageName.ids.isEmpty) None() else Some(st"package ${printName(ast.packageName)}")
426440
val r =

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

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

0 commit comments

Comments
 (0)