From e8565f6c4857e427febff79c1724065d01c1132e Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sun, 21 Jan 2024 17:47:33 -0800 Subject: [PATCH] update --- Source/Concurrency/CivlCoreTypes.cs | 4 ++-- Source/Core/AST/Absy.cs | 5 ++--- Source/Core/BoogiePL.atg | 15 ++++++++------- Source/Core/Parser.cs | 15 ++++++++------- 4 files changed, 20 insertions(+), 19 deletions(-) diff --git a/Source/Concurrency/CivlCoreTypes.cs b/Source/Concurrency/CivlCoreTypes.cs index 598613278..c17c80b70 100644 --- a/Source/Concurrency/CivlCoreTypes.cs +++ b/Source/Concurrency/CivlCoreTypes.cs @@ -42,9 +42,9 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref new DatatypeTypeCtorDecl(Token.NoToken, choiceDatatypeName, new List(), 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() { field }); + new List() { field }); }); civlTypeChecker.program.AddTopLevelDeclaration(ChoiceDatatypeTypeCtorDecl); DesugarSetChoice(civlTypeChecker, ImplWithChoice); diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 70e683001..4968586ae 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -891,11 +891,10 @@ public bool AddConstructor(DatatypeConstructor constructor) return true; } - public bool AddConstructor(IToken tok, string name, List fields) + public bool AddConstructor(IToken tok, string name, List fields) { var returnType = new CtorType(this.tok, this, new List(this.typeParameters)); - var function = new Function(tok, name, new List(this.typeParameters), - fields.Select(field => new Formal(field.tok, field, true)).ToList(), + var function = new Function(tok, name, new List(this.typeParameters), fields, new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, returnType), false)); var constructor = new DatatypeConstructor(function); return AddConstructor(constructor); diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index ab76a6c77..6f1f0c676 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -278,7 +278,7 @@ ProcFormals<.bool incoming, bool allowWhereClauses, out List/*!*/ ds.> var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals"; .) "(" - [ AttrsIdsTypeWheres + [ AttributesIdsTypeWheres ] ")" . @@ -290,7 +290,7 @@ BoundVars<.out List/*!*/ ds.> ds = new List(); var dsx = ds; .) - AttrsIdsTypeWheres + AttributesIdsTypeWheres . /*------------------------------------------------------------------------*/ @@ -306,8 +306,8 @@ IdsType<.out List/*!*/ tyds.> .) . -/* AttrsIdsTypeWheres is used with the declarations of formals and bound variables */ -AttrsIdsTypeWheres<. bool allowWhereClauses, string context, System.Action action .> +/* AttributesIdsTypeWheres is used with the declarations of formals and bound variables */ +AttributesIdsTypeWheres<. bool allowWhereClauses, string context, System.Action action .> = AttributesIdsTypeWhere { "," AttributesIdsTypeWhere } @@ -626,10 +626,10 @@ Constructors . Constructor -= (. IToken name; List fields = new List(); .) += (. IToken name; List fields = new List(); .) Ident "(" - [ IdsTypeWheres ] + [ AttributesIdsTypeWheres ] ")" (. if (!datatypeTypeCtorDecl.AddConstructor(name, name.val, fields)) { @@ -716,7 +716,8 @@ ActionDecl(), 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(); + datatypeTypeCtorDecl.AddConstructor(name, name.val, fields); } } actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, elims, mods, datatypeTypeCtorDecl, kv); diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 6eefe668f..871576e28 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -736,7 +736,8 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl, else { datatypeTypeCtorDecl = new DatatypeTypeCtorDecl(name, name.val, new List(), 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(); + datatypeTypeCtorDecl.AddConstructor(name, name.val, fields); } } actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, elims, mods, datatypeTypeCtorDecl, kv); @@ -791,12 +792,12 @@ void ProcFormals(bool incoming, bool allowWhereClauses, out List/*!*/ 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 action ) { + void AttributesIdsTypeWheres(bool allowWhereClauses, string context, System.Action action ) { AttributesIdsTypeWhere(allowWhereClauses, context, action); while (la.kind == 14) { Get(); @@ -810,7 +811,7 @@ void BoundVars(out List/*!*/ ds) { ds = new List(); 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/*!*/ tyds) { @@ -1076,11 +1077,11 @@ void Constructors(DatatypeTypeCtorDecl datatypeTypeCtorDecl) { } void Constructor(DatatypeTypeCtorDecl datatypeTypeCtorDecl) { - IToken name; List fields = new List(); + IToken name; List fields = new List(); 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)) {