Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow attributes on datatype fields #836

Merged
merged 2 commits into from
Jan 22, 2024
Merged

Allow attributes on datatype fields #836

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e8565f6
update
Jan 22, 2024
d15fc98
Merge branch 'master' into datatype-field-attrs
shazqadeer Jan 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Source/Concurrency/CivlCoreTypes.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,9 +42,9 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref
new DatatypeTypeCtorDecl(Token.NoToken, choiceDatatypeName, new List<TypeVariable>(), null);
PendingAsyncs.ForEach(elim =>
{
var field = new TypedIdent(Token.NoToken, elim.Name, elim.PendingAsyncType);
var field = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, elim.Name, elim.PendingAsyncType), true);
ChoiceDatatypeTypeCtorDecl.AddConstructor(Token.NoToken, $"{choiceDatatypeName}_{elim.Name}",
new List<TypedIdent>() { field });
new List<Variable>() { field });
});
civlTypeChecker.program.AddTopLevelDeclaration(ChoiceDatatypeTypeCtorDecl);
DesugarSetChoice(civlTypeChecker, ImplWithChoice);
Expand Down
5 changes: 2 additions & 3 deletions Source/Core/AST/Absy.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -891,11 +891,10 @@ public bool AddConstructor(DatatypeConstructor constructor)
return true;
}

public bool AddConstructor(IToken tok, string name, List<TypedIdent> fields)
public bool AddConstructor(IToken tok, string name, List<Variable> fields)
{
var returnType = new CtorType(this.tok, this, new List<Type>(this.typeParameters));
var function = new Function(tok, name, new List<TypeVariable>(this.typeParameters),
fields.Select(field => new Formal(field.tok, field, true)).ToList<Variable>(),
var function = new Function(tok, name, new List<TypeVariable>(this.typeParameters), fields,
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, returnType), false));
var constructor = new DatatypeConstructor(function);
return AddConstructor(constructor);
Expand Down
15 changes: 8 additions & 7 deletions Source/Core/BoogiePL.atg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -278,7 +278,7 @@ ProcFormals<.bool incoming, bool allowWhereClauses, out List<Variable>/*!*/ ds.>
var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals";
.)
"("
[ AttrsIdsTypeWheres<allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); }>
[ AttributesIdsTypeWheres<allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); }>
]
")"
.
Expand All @@ -290,7 +290,7 @@ BoundVars<.out List<Variable>/*!*/ ds.>
ds = new List<Variable>();
var dsx = ds;
.)
AttrsIdsTypeWheres<false, "bound variables", delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new BoundVariable(tyd.tok, tyd, kv)); } >
AttributesIdsTypeWheres<false, "bound variables", delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new BoundVariable(tyd.tok, tyd, kv)); } >
.

/*------------------------------------------------------------------------*/
Expand All @@ -306,8 +306,8 @@ IdsType<.out List<TypedIdent>/*!*/ tyds.>
.)
.

/* AttrsIdsTypeWheres is used with the declarations of formals and bound variables */
AttrsIdsTypeWheres<. bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action .>
/* AttributesIdsTypeWheres is used with the declarations of formals and bound variables */
AttributesIdsTypeWheres<. bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action .>
=
AttributesIdsTypeWhere<allowWhereClauses, context, action>
{ "," AttributesIdsTypeWhere<allowWhereClauses, context, action> }
Expand Down Expand Up @@ -626,10 +626,10 @@ Constructors<DatatypeTypeCtorDecl datatypeTypeCtorDecl>
.

Constructor<DatatypeTypeCtorDecl datatypeTypeCtorDecl>
= (. IToken name; List<TypedIdent> fields = new List<TypedIdent>(); .)
= (. IToken name; List<Variable> fields = new List<Variable>(); .)
Ident<out name>
"("
[ IdsTypeWheres<false, "datatype constructor", delegate(TypedIdent ti) { fields.Add(ti); }> ]
[ AttributesIdsTypeWheres<false, "datatype constructor", delegate(TypedIdent ti, QKeyValue kv) { fields.Add(new Formal(ti.tok, ti, true, kv)); }> ]
")"
(.
if (!datatypeTypeCtorDecl.AddConstructor(name, name.val, fields)) {
Expand Down Expand Up @@ -716,7 +716,8 @@ ActionDecl<bool isPure, out ActionDecl actionDecl, out Implementation impl, out
else
{
datatypeTypeCtorDecl = new DatatypeTypeCtorDecl(name, name.val, new List<TypeVariable>(), null);
datatypeTypeCtorDecl.AddConstructor(name, name.val, ins.Select(v => new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type)).ToList());
var fields = ins.Select(v => new Formal(v.tok, new TypedIdent(v.TypedIdent.tok, v.Name, v.TypedIdent.Type), true, v.Attributes)).ToList<Variable>();
datatypeTypeCtorDecl.AddConstructor(name, name.val, fields);
}
}
actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, elims, mods, datatypeTypeCtorDecl, kv);
Expand Down
15 changes: 8 additions & 7 deletions Source/Core/Parser.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -736,7 +736,8 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl,
else
{
datatypeTypeCtorDecl = new DatatypeTypeCtorDecl(name, name.val, new List<TypeVariable>(), null);
datatypeTypeCtorDecl.AddConstructor(name, name.val, ins.Select(v => new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type)).ToList());
var fields = ins.Select(v => new Formal(v.tok, new TypedIdent(v.TypedIdent.tok, v.Name, v.TypedIdent.Type), true, v.Attributes)).ToList<Variable>();
datatypeTypeCtorDecl.AddConstructor(name, name.val, fields);
}
}
actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, elims, mods, datatypeTypeCtorDecl, kv);
Expand Down Expand Up @@ -791,12 +792,12 @@ void ProcFormals(bool incoming, bool allowWhereClauses, out List<Variable>/*!*/

Expect(11);
if (StartOf(12)) {
AttrsIdsTypeWheres(allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); });
AttributesIdsTypeWheres(allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); });
}
Expect(12);
}

void AttrsIdsTypeWheres(bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
void AttributesIdsTypeWheres(bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
AttributesIdsTypeWhere(allowWhereClauses, context, action);
while (la.kind == 14) {
Get();
Expand All @@ -810,7 +811,7 @@ void BoundVars(out List<Variable>/*!*/ ds) {
ds = new List<Variable>();
var dsx = ds;

AttrsIdsTypeWheres(false, "bound variables", delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new BoundVariable(tyd.tok, tyd, kv)); } );
AttributesIdsTypeWheres(false, "bound variables", delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new BoundVariable(tyd.tok, tyd, kv)); } );
}

void IdsType(out List<TypedIdent>/*!*/ tyds) {
Expand Down Expand Up @@ -1076,11 +1077,11 @@ void Constructors(DatatypeTypeCtorDecl datatypeTypeCtorDecl) {
}

void Constructor(DatatypeTypeCtorDecl datatypeTypeCtorDecl) {
IToken name; List<TypedIdent> fields = new List<TypedIdent>();
IToken name; List<Variable> fields = new List<Variable>();
Ident(out name);
Expect(11);
if (StartOf(14)) {
IdsTypeWheres(false, "datatype constructor", delegate(TypedIdent ti) { fields.Add(ti); });
if (StartOf(12)) {
AttributesIdsTypeWheres(false, "datatype constructor", delegate(TypedIdent ti, QKeyValue kv) { fields.Add(new Formal(ti.tok, ti, true, kv)); });
}
Expect(12);
if (!datatypeTypeCtorDecl.AddConstructor(name, name.val, fields)) {
Expand Down
Loading