Skip to content

Commit

Permalink
update
Browse files Browse the repository at this point in the history
  • Loading branch information
Shaz Qadeer committed Jan 22, 2024
1 parent 2f8cbde commit e8565f6
Show file tree
Hide file tree
Showing 4 changed files with 20 additions and 19 deletions.
4 changes: 2 additions & 2 deletions Source/Concurrency/CivlCoreTypes.cs
View file
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
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
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
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

0 comments on commit e8565f6

Please sign in to comment.