Skip to content

Commit 2f90cd5

Browse files
jcp19jcp19
committed
progress
1 parent 3c99ed4 commit 2f90cd5

File tree

16 files changed

+31
-17
lines changed

16 files changed

+31
-17
lines changed

‎silver-sif-extension‎

‎src/main/antlr4/GobraLexer.g4‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,7 @@ IMPORT_PRE : 'importRequires';
9696
PROOF : 'proof';
9797
GHOST_EQUALS : '===';
9898
GHOST_NOT_EQUALS : '!==';
99+
CLOSURESPEC : 'closureSpec';
99100
WITH : 'with';
100101
OPAQUE : 'opaque' -> mode(NLSEMI);
101102
MAYINIT : 'mayInit' -> mode(NLSEMI);

‎src/main/antlr4/GobraParser.g4‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -252,9 +252,9 @@ new_: NEW L_PAREN type_ R_PAREN;
252252

253253
// Added specifications and parameter info
254254

255-
specMember: specification (functionDecl[$specification.trusted, $specification.pure, $specification.opaque] | methodDecl[$specification.trusted, $specification.pure, $specification.opaque]);
255+
specMember returns [boolean isClosureSpec = false;]: specification (functionDecl[$specification.trusted, $specification.pure, $specification.opaque] {$isClosureSpec = $functionDecl.isClosureSpec;} | methodDecl[$specification.trusted, $specification.pure, $specification.opaque]);
256256

257-
functionDecl[boolean trusted, boolean pure, boolean opaque]: FUNC IDENTIFIER (signature blockWithBodyParameterInfo?);
257+
functionDecl[boolean trusted, boolean pure, boolean opaque] returns [boolean isClosureSpec = false;]: (FUNC | CLOSURESPEC {$isClosureSpec = true;}) IDENTIFIER (signature blockWithBodyParameterInfo?);
258258

259259
methodDecl[boolean trusted, boolean pure, boolean opaque]: FUNC receiver IDENTIFIER (signature blockWithBodyParameterInfo?);
260260

‎src/main/scala/viper/gobra/ast/frontend/Ast.scala‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -182,6 +182,7 @@ case class PFunctionDecl(
182182
args: Vector[PParameter],
183183
result: PResult,
184184
spec: PFunctionSpec,
185+
isClosureSpec: Boolean,
185186
body: Option[(PBodyParameterInfo, PBlock)]
186187
) extends PFunctionOrClosureDecl with PFunctionOrMethodDecl with PCodeRootWithResult with PWithBody with PGhostifiableMember
187188

‎src/main/scala/viper/gobra/ast/frontend/AstPattern.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,7 @@ object AstPattern {
5757
def isPure: Boolean
5858
}
5959

60-
case class Function(id: PIdnUse, symb: st.Function) extends FunctionKind {
60+
case class Function(id: PIdnUse, symb: st.Function, isClosureSpec: Boolean) extends FunctionKind {
6161
override val isPure: Boolean = symb.isPure
6262
}
6363
case class Closure(id: PIdnUse, symb: st.Closure) extends FunctionKind {

‎src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -125,8 +125,9 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
125125
case n: PConstDecl => showConstDecl(n)
126126
case n: PVarDecl => showVarDecl(n)
127127
case n: PTypeDecl => showTypeDecl(n)
128-
case PFunctionDecl(id, args, res, spec, body) =>
129-
showSpec(spec) <> "func" <+> showId(id) <> parens(showParameterList(args)) <> showResult(res) <>
128+
case PFunctionDecl(id, args, res, spec, isClosureSpec, body) =>
129+
val kw = if (isClosureSpec) "closureSpec" else "func"
130+
showSpec(spec) <> kw <+> showId(id) <> parens(showParameterList(args)) <> showResult(res) <>
130131
opt(body)(b => space <> showBodyParameterInfoWithBlock(b._1, b._2))
131132
case PMethodDecl(id, rec, args, res, spec, body) =>
132133
showSpec(spec) <> "func" <+> showReceiver(rec) <+> showId(id) <> parens(showParameterList(args)) <> showResult(res) <>
@@ -786,8 +787,9 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter {
786787
case n: PConstDecl => showConstDecl(n)
787788
case n: PVarDecl => showVarDecl(n)
788789
case n: PTypeDecl => showTypeDecl(n)
789-
case PFunctionDecl(id, args, res, spec, _) =>
790-
showSpec(spec) <> "func" <+> showId(id) <> parens(showParameterList(args)) <> showResult(res)
790+
case PFunctionDecl(id, args, res, spec, isClosureSpec, _) =>
791+
val kw = if (isClosureSpec) "closureSpec" else "func"
792+
showSpec(spec) <> kw <+> showId(id) <> parens(showParameterList(args)) <> showResult(res)
791793
case PMethodDecl(id, rec, args, res, spec, _) =>
792794
showSpec(spec) <> "func" <+> showReceiver(rec) <+> showId(id) <> parens(showParameterList(args)) <> showResult(res)
793795
case ip: PImplementationProof =>

‎src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -861,7 +861,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
861861

862862
override def visitSpecMember(ctx: SpecMemberContext): PFunctionOrMethodDecl = super.visitSpecMember(ctx) match {
863863
case Vector(spec : PFunctionSpec, (id: PIdnDef, args: Vector[PParameter@unchecked], result: PResult, body: Option[(PBodyParameterInfo, PBlock)@unchecked]))
864-
=> PFunctionDecl(id, args, result, spec, body)
864+
=> PFunctionDecl(id, args, result, spec, ctx.isClosureSpec, body)
865865
case Vector(spec : PFunctionSpec, (id: PIdnDef, receiver: PReceiver, args: Vector[PParameter@unchecked], result: PResult, body: Option[(PBodyParameterInfo, PBlock)@unchecked]))
866866
=> PMethodDecl(id, receiver, args, result, spec, body)
867867
}

‎src/main/scala/viper/gobra/frontend/Parser.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -499,7 +499,7 @@ object Parser extends LazyLogging {
499499
strategyWithName[Any]("replaceTerminationMeasuresForFunctionsAndMethods", {
500500
// apply transformation only to the specification of function or method declaration (in particular, do not
501501
// apply the transformation to method signatures in interface declarations)
502-
case n: PFunctionDecl => Some(PFunctionDecl(n.id, n.args, n.result, replace(n.spec), n.body))
502+
case n: PFunctionDecl => Some(PFunctionDecl(n.id, n.args, n.result, replace(n.spec), n.isClosureSpec, n.body))
503503
case n: PMethodDecl => Some(PMethodDecl(n.id, n.receiver, n.args, n.result, replace(n.spec), n.body))
504504
case n: PMember => Some(n)
505505
})

‎src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ trait IdTyping extends BaseTyping { this: TypeInfoImpl =>
9696
}
9797
})
9898

99-
case Function(PFunctionDecl(_, args, r, _, _), _, _) => unsafeMessage(! {
99+
case Function(PFunctionDecl(_, args, r, _, _, _), _, _) => unsafeMessage(! {
100100
args.forall(wellDefMisc.valid) && miscType.valid(r)
101101
})
102102

@@ -212,7 +212,7 @@ trait IdTyping extends BaseTyping { this: TypeInfoImpl =>
212212
case t => violation(s"expected tuple but got $t")
213213
})
214214

215-
case Function(PFunctionDecl(_, args, r, _, _), _, context) =>
215+
case Function(PFunctionDecl(_, args, r, _, _, _), _, context) =>
216216
FunctionT(args map context.typ, context.typ(r))
217217

218218
case Closure(PFunctionLit(_, PClosureDecl(args, r, _, _)), _, context) =>

‎src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,8 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl =>
2626
wellDefIfPureFunction(n) ++
2727
wellDefIfInitBlock(n) ++
2828
wellDefIfMain(n) ++
29-
wellFoundedIfNeeded(n)
29+
wellFoundedIfNeeded(n) ++
30+
wellDefIfClosureSpec(n)
3031
case m: PMethodDecl =>
3132
wellDefVariadicArgs(m.args) ++
3233
isReceiverType.errors(miscType(m.receiver))(member) ++

0 commit comments

Comments
 (0)