diff --git a/Source/DafnyCore/AST/AstVisitor.cs b/Source/DafnyCore/AST/AstVisitor.cs index 08bcd71bf56..3a56c49698a 100644 --- a/Source/DafnyCore/AST/AstVisitor.cs +++ b/Source/DafnyCore/AST/AstVisitor.cs @@ -230,6 +230,9 @@ protected virtual void VisitExpression(Expression expr, VisitorContext context) } } + foreach (var pattern in letExpr.LHSs) { + VisitCasePattern(pattern); + } } else if (expr is QuantifierExpr quantifierExpr) { foreach (BoundVar v in quantifierExpr.BoundVars) { VisitUserProvidedType(v.Type, context); @@ -260,6 +263,10 @@ protected virtual void VisitExpression(Expression expr, VisitorContext context) foreach (var mc in nestedMatchExpr.Cases) { VisitExtendedPattern(mc.Pat, context); } + + if (nestedMatchExpr.Flattened != null) { + VisitExpression(nestedMatchExpr.Flattened, context); + } } // Visit substatements @@ -336,6 +343,8 @@ protected virtual void VisitStatement(Statement stmt, VisitorContext context) { VisitUserProvidedType(local.SyntacticType, context); } + VisitCasePattern(varDeclPattern.LHS); + } else if (stmt is SingleAssignStmt assignStmt) { if (assignStmt.Rhs is TypeRhs typeRhs) { if (typeRhs.EType != null) { @@ -358,6 +367,9 @@ protected virtual void VisitStatement(Statement stmt, VisitorContext context) { VisitExtendedPattern(mc.Pat, context); } + if (nestedMatchStmt.Flattened != null) { + VisitStatement(nestedMatchStmt.Flattened, context); + } } else if (stmt is MatchStmt matchStmt) { foreach (MatchCaseStmt mc in matchStmt.Cases) { if (mc.Arguments != null) { @@ -378,6 +390,16 @@ protected virtual void VisitStatement(Statement stmt, VisitorContext context) { } } + protected virtual void VisitCasePattern(CasePattern pattern) where T : class, IVariable { + if (pattern.Arguments == null) { + return; + } + + foreach (var argument in pattern.Arguments) { + VisitCasePattern(argument); + } + } + /// /// Visits the given statement. /// Returns "true" to request that the caller diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs index 92c82e9d14b..1fd0cf06763 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs @@ -55,7 +55,15 @@ public override IEnumerable SubExpressions { } } - public override IEnumerable Children => new[] { Source }.Concat(Cases); + public override IEnumerable Children { + get { + var result = new[] { Source }.Concat(Cases); + if (Flattened != null) { + result = result.Concat(new[] { Flattened }); + } + return result; + } + } public void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext) { diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs index 23d00478a22..cc7d9b60b99 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs @@ -43,7 +43,15 @@ public NestedMatchStmt(Cloner cloner, NestedMatchStmt original) : base(cloner, o } } - public override IEnumerable Children => new[] { Source }.Concat(Cases); + public override IEnumerable Children { + get { + var result = new[] { Source }.Concat(Cases); + if (Flattened != null) { + result = result.Concat(new[] { Flattened }); + } + return result; + } + } public override IEnumerable SubStatements { get { diff --git a/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs index a71fd261412..d0c96b8e3e6 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny; public class LetExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBearingExpression, ICloneable, ICanFormat { - public readonly List> LHSs; + public List> LHSs; public readonly List RHSs; public readonly Expression Body; public readonly bool Exact; // Exact==true means a regular let expression; Exact==false means an assign-such-that expression diff --git a/Source/DafnyCore/AST/Members/MethodOrFunction.cs b/Source/DafnyCore/AST/Members/MethodOrFunction.cs index 2b5167ed426..92cef76a9e0 100644 --- a/Source/DafnyCore/AST/Members/MethodOrFunction.cs +++ b/Source/DafnyCore/AST/Members/MethodOrFunction.cs @@ -20,7 +20,7 @@ static MethodOrFunction() { public readonly List Req; public readonly List Ens; public readonly Specification Decreases; - public readonly List Ins; + public List Ins; protected MethodOrFunction(RangeToken rangeToken, Name name, bool hasStaticKeyword, bool isGhost, Attributes attributes, bool isRefining, List typeArgs, List ins, diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs index 7b5f3bde91d..e2a38a88fcc 100644 --- a/Source/DafnyCore/AST/SystemModuleManager.cs +++ b/Source/DafnyCore/AST/SystemModuleManager.cs @@ -18,6 +18,8 @@ public class SystemModuleManager { public readonly Dictionary TotalArrowTypeDecls = new(); // same keys as arrowTypeDecl readonly Dictionary, TupleTypeDecl> tupleTypeDecls = new(new Dafny.IEnumerableComparer()); + public IEnumerable TupleTypeDecls => tupleTypeDecls.Values; + internal readonly ValuetypeDecl[] valuetypeDecls; /// diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs index 854e6dc79f3..34e6157f44d 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs @@ -7,7 +7,7 @@ namespace Microsoft.Dafny; public class DatatypeCtor : Declaration, TypeParameter.ParentType, IHasDocstring, ICanVerify { public readonly bool IsGhost; - public readonly List Formals; + public List Formals; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(Formals)); diff --git a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs index a975a0afba7..99fd194cf49 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs @@ -8,7 +8,7 @@ namespace Microsoft.Dafny; public abstract class TopLevelDeclWithMembers : TopLevelDecl, IHasSymbolChildren { - public readonly List Members; + public List Members; // TODO remove this and instead clone the AST after parsing. public ImmutableList MembersBeforeResolution; diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 430eb8cc3c2..5ea6ef4c139 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -458,7 +458,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete Constructor ct = constructors[0]; foreach (var member in iter.Members) { - if (member is Field f && !f.IsGhost) { + if (member is Field f) { cw.DeclareField(IdName(f), iter, false, false, f.Type, f.tok, PlaceboValue(f.Type, w, f.tok, true), f); } } @@ -466,7 +466,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete w.WriteLine("System.Collections.Generic.IEnumerator _iter;"); // here we rely on the parameters and the corresponding fields having the same names - var nonGhostFormals = ct.Ins.Where(p => !p.IsGhost).ToList(); + var nonGhostFormals = ct.Ins.ToList(); var parameters = nonGhostFormals.Comma(p => $"{TypeName(p.Type, w, p.tok)} {IdName(p)}"); // here's the initializer method @@ -623,11 +623,10 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { var wDefaultArguments = wDefault.Write(DtCreateName(groundingCtor)).ForkInParens(); wDefaultArguments.Append(wDefaultTypeArguments); - var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost).ToList(); - if (defaultMethodTypeDescriptorCount != 0 && nonGhostFormals.Count != 0) { + if (defaultMethodTypeDescriptorCount != 0 && groundingCtor.Formals.Count != 0) { wDefaultArguments.Write(", "); } - wDefaultArguments.Write(nonGhostFormals.Comma(f => DefaultValue(f.Type, wDefault, f.tok))); + wDefaultArguments.Write(groundingCtor.Formals.Comma(f => DefaultValue(f.Type, wDefault, f.tok))); } EmitTypeDescriptorMethod(dt, wr); @@ -645,7 +644,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { var formalCount = WriteFormals(typeDescriptorCount > 0 ? ", " : "", ctor.Formals, wr); var sep = typeDescriptorCount > 0 && formalCount > 0 ? ", " : ""; wr.NewBlock(")") - .WriteLine($"return new {DtCtorDeclarationName(ctor)}{DtT_TypeArgs}({wCallArguments}{sep}{ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});"); + .WriteLine($"return new {DtCtorDeclarationName(ctor)}{DtT_TypeArgs}({wCallArguments}{sep}{ctor.Formals.Comma(FormalName)});"); } if (dt.IsRecordType) { @@ -659,7 +658,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { var formalCount = WriteFormals(typeDescriptorCount > 0 ? ", " : "", ctor.Formals, wr); var sep = typeDescriptorCount > 0 && formalCount > 0 ? ", " : ""; wr.NewBlock(")") - .WriteLine($"return create({wCallArguments}{sep}{ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});"); + .WriteLine($"return create({wCallArguments}{sep}{ctor.Formals.Comma(FormalName)});"); } // query properties @@ -721,7 +720,7 @@ bool InvalidType(Type ty, bool refTy) => (ty.AsTypeParameter != null && refTy && datatype.TypeArgs.Contains(ty.AsTypeParameter)) || ty.TypeArgs.Exists(arg => InvalidType(arg, refTy || ty.IsRefType)); - if (datatype.Ctors.Any(ctor => ctor.Formals.Any(f => !f.IsGhost && InvalidType(f.SyntacticType, false)))) { + if (datatype.Ctors.Any(ctor => ctor.Formals.Any(f => InvalidType(f.SyntacticType, false)))) { return; } @@ -845,7 +844,7 @@ string PrintInvocation(Formal f, int i) { var typeDescriptorArgumentsStrings = wCallArguments.ToString(); string constructorArgs; if (!lazy) { - constructorArgs = ctor.Formals.Where(f => !f.IsGhost).Comma(PrintInvocation); + constructorArgs = ctor.Formals.Comma(PrintInvocation); } else if (customReceiver) { var sep0 = typeDescriptorCount != 0 ? ", " : ""; var sep1 = converters.Length != 0 ? ", " : ""; @@ -855,7 +854,7 @@ string PrintInvocation(Formal f, int i) { var sep0 = typeDescriptorCount != 0 && converters.Length != 0 ? ", " : ""; constructorArgs = $"() => _Get().DowncastClone{uTypeArgs}({typeDescriptorArgumentsStrings}{sep0}{converters})"; } - var sep = typeDescriptorCount != 0 && (lazy || ctor.Formals.Any(f => !f.IsGhost)) ? ", " : ""; + var sep = typeDescriptorCount != 0 && (lazy || ctor.Formals.Any()) ? ", " : ""; var className = lazy ? lazyClass : DtCtorDeclarationName(ctor); wBody.WriteLine($"return new {className}{uTypeArgs}({typeDescriptorArgumentsStrings}{sep}{constructorArgs});"); } @@ -875,7 +874,8 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre if (!arg.IsGhost) { var DtorM = arg.HasName ? InternalFieldPrefix + arg.CompileName : FieldName(arg, index); // TN dtor_QDtorM { get; } - interfaceTree.WriteLine($"{TypeName(arg.Type, wr, arg.tok)} {DestructorGetterName(arg, ctor, index)} {{ get; }}"); + interfaceTree.WriteLine( + $"{TypeName(arg.Type, wr, arg.tok)} {DestructorGetterName(arg, ctor, index)} {{ get; }}"); // public TN dtor_QDtorM { get { // var d = this; // for inductive datatypes @@ -909,6 +909,7 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre if (ctor_i.IsGhost) { continue; } + var type = $"{dt.GetCompileName(Options)}_{ctor_i.GetCompileName(Options)}{DtT_TypeArgs}"; // TODO use pattern matching to replace cast. var returnTheValue = $"return (({type})d).{IdProtect(DtorM)};"; @@ -917,9 +918,11 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre } else { wGet.WriteLine(returnTheValue); } + compiledConstructorsProcessed++; } } + index++; } } @@ -929,7 +932,7 @@ private void CompileDatatypeDestructorsAndAddToInterface(DatatypeDecl dt, Concre private void CompileDatatypeInterfaceMembers(DatatypeDecl dt, ConcreteSyntaxTree interfaceTree) { foreach (var member in dt.Members) { - if (member.IsGhost || member.IsStatic) { continue; } + if (member.IsStatic) { continue; } if (member is Function fn && !NeedsCustomReceiver(member)) { CreateFunction(IdName(fn), CombineAllTypeArguments(fn), fn.Ins, fn.ResultType, fn.tok, fn.IsStatic, false, fn, interfaceTree, false, false); @@ -957,7 +960,7 @@ public override bool NeedsCustomReceiverInDatatype(MemberDecl member) { foreach (var tp in d.TypeArgs) { bool InvalidType(Type ty) => (ty.AsTypeParameter != null && ty.AsTypeParameter.Equals(tp)) || ty.TypeArgs.Exists(InvalidType); - bool InvalidFormal(Formal f) => !f.IsGhost && InvalidType(f.SyntacticType); + bool InvalidFormal(Formal f) => InvalidType(f.SyntacticType); switch (tp.Variance) { //Can only be in output case TypeParameter.TPVariance.Co: @@ -1060,10 +1063,8 @@ void DatatypeFieldsAndConstructor(DatatypeCtor ctor, int constructorIndex, Concr var i = 0; foreach (Formal arg in ctor.Formals) { - if (!arg.IsGhost) { - wr.WriteLine($"public readonly {TypeName(arg.Type, wr, arg.tok)} {FieldName(arg, i)};"); - i++; - } + wr.WriteLine($"public readonly {TypeName(arg.Type, wr, arg.tok)} {FieldName(arg, i)};"); + i++; } var typeDescriptorCount = EmitTypeDescriptorsForClass(dt.TypeArgs, dt, out var wTypeFields, out var wCtorParams, out var wBaseCallArguments, out var wCtorBody); @@ -1080,10 +1081,8 @@ void DatatypeFieldsAndConstructor(DatatypeCtor ctor, int constructorIndex, Concr var w = wCtorBody; i = 0; foreach (Formal arg in ctor.Formals) { - if (!arg.IsGhost) { - w.WriteLine($"this.{FieldName(arg, i)} = {FormalName(arg, i)};"); - i++; - } + w.WriteLine($"this.{FieldName(arg, i)} = {FormalName(arg, i)};"); + i++; } } @@ -1102,14 +1101,12 @@ void DatatypeFieldsAndConstructor(DatatypeCtor ctor, int constructorIndex, Concr w.Write("return oth != null"); i = 0; foreach (var arg in ctor.Formals) { - if (!arg.IsGhost) { - var nm = FieldName(arg, i); - w.Write(IsDirectlyComparable(DatatypeWrapperEraser.SimplifyType(Options, arg.Type)) - ? $" && this.{nm} == oth.{nm}" - : $" && object.Equals(this.{nm}, oth.{nm})"); + var nm = FieldName(arg, i); + w.Write(IsDirectlyComparable(DatatypeWrapperEraser.SimplifyType(Options, arg.Type)) + ? $" && this.{nm} == oth.{nm}" + : $" && object.Equals(this.{nm}, oth.{nm})"); - i++; - } + i++; } w.WriteLine(";"); @@ -1122,11 +1119,9 @@ void DatatypeFieldsAndConstructor(DatatypeCtor ctor, int constructorIndex, Concr w.WriteLine($"hash = ((hash << 5) + hash) + {constructorIndex};"); i = 0; foreach (Formal arg in ctor.Formals) { - if (!arg.IsGhost) { - string nm = FieldName(arg, i); - w.WriteLine($"hash = ((hash << 5) + hash) + ((ulong){DafnyHelpersClass}.GetHashCode(this.{nm}));"); - i++; - } + string nm = FieldName(arg, i); + w.WriteLine($"hash = ((hash << 5) + hash) + ((ulong){DafnyHelpersClass}.GetHashCode(this.{nm}));"); + i++; } w.WriteLine("return (int) hash;"); @@ -1156,19 +1151,17 @@ void DatatypeFieldsAndConstructor(DatatypeCtor ctor, int constructorIndex, Concr w.WriteLine($"{tempVar} += \"(\";"); i = 0; foreach (var arg in ctor.Formals) { - if (!arg.IsGhost) { - if (i != 0) { - w.WriteLine($"{tempVar} += \", \";"); - } - - if (arg.Type.IsStringType && UnicodeCharEnabled) { - w.WriteLine($"{tempVar} += this.{FieldName(arg, i)}.ToVerbatimString(true);"); - } else { - w.WriteLine($"{tempVar} += {DafnyHelpersClass}.ToString(this.{FieldName(arg, i)});"); - } + if (i != 0) { + w.WriteLine($"{tempVar} += \", \";"); + } - i++; + if (arg.Type.IsStringType && UnicodeCharEnabled) { + w.WriteLine($"{tempVar} += this.{FieldName(arg, i)}.ToVerbatimString(true);"); + } else { + w.WriteLine($"{tempVar} += {DafnyHelpersClass}.ToString(this.{FieldName(arg, i)});"); } + + i++; } w.WriteLine($"{tempVar} += \")\";"); @@ -2658,14 +2651,12 @@ protected override ILvalue EmitMemberSelect(Action obj, Type lambdaHeader.Write(" => "); foreach (var arg in fn.Ins) { - if (!arg.IsGhost) { - var name = idGenerator.FreshId("_eta"); - var ty = arg.Type.Subst(typeMap); - arguments.Write($"{prefixSep}{TypeName(ty, arguments, arg.tok)} {name}"); - callArguments.Write($"{sep}{name}"); - sep = ", "; - prefixSep = ", "; - } + var name = idGenerator.FreshId("_eta"); + var ty = arg.Type.Subst(typeMap); + arguments.Write($"{prefixSep}{TypeName(ty, arguments, arg.tok)} {name}"); + callArguments.Write($"{sep}{name}"); + sep = ", "; + prefixSep = ", "; } return EnclosedLvalue(lambdaHeader.ToString(), obj, $".{wr}"); } diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index 8c333c37386..9f7907fd539 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -342,11 +342,9 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT var i = 0; var argNames = new List(); foreach (Formal arg in ctor.Formals) { - if (!arg.IsGhost) { - ws.WriteLine("{0} {1};", TypeName(arg.Type, wdecl, arg.tok), FormalName(arg, i)); - argNames.Add(FormalName(arg, i)); - i++; - } + ws.WriteLine("{0} {1};", TypeName(arg.Type, wdecl, arg.tok), FormalName(arg, i)); + argNames.Add(FormalName(arg, i)); + i++; } if (argNames.Count > 0) { @@ -367,9 +365,7 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT ws.WriteLine("{0}();", DtT_protected); var wc = wdef.NewNamedBlock("{1}\n{0}{2}::{0}()", DtT_protected, DeclareTemplate(dt.TypeArgs), InstantiateTemplate(dt.TypeArgs)); foreach (var arg in ctor.Formals) { - if (!arg.IsGhost) { - wc.WriteLine("{0} = {1};", arg.CompileName, DefaultValue(arg.Type, wc, arg.tok)); - } + wc.WriteLine("{0} = {1};", arg.CompileName, DefaultValue(arg.Type, wc, arg.tok)); } // Overload the comparison operator @@ -392,9 +388,7 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT var owr = hwr.NewBlock(string.Format("std::size_t operator()(const {0}& x) const", fullName)); owr.WriteLine("size_t seed = 0;"); foreach (var arg in ctor.Formals) { - if (!arg.IsGhost) { - owr.WriteLine("hash_combine<{0}>(seed, x.{1});", TypeName(arg.Type, owr, dt.tok), arg.CompileName); - } + owr.WriteLine("hash_combine<{0}>(seed, x.{1});", TypeName(arg.Type, owr, dt.tok), arg.CompileName); } owr.WriteLine("return seed;"); } else { @@ -406,14 +400,12 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT // Declare the struct members var i = 0; foreach (Formal arg in ctor.Formals) { - if (!arg.IsGhost) { - if (arg.Type is UserDefinedType udt && udt.ResolvedClass == dt) { // Recursive declaration needs to use a pointer - wstruct.WriteLine("std::shared_ptr<{0}> {1};", TypeName(arg.Type, wdecl, arg.tok), FormalName(arg, i)); - } else { - wstruct.WriteLine("{0} {1};", TypeName(arg.Type, wdecl, arg.tok), FormalName(arg, i)); - } - i++; + if (arg.Type is UserDefinedType udt && udt.ResolvedClass == dt) { // Recursive declaration needs to use a pointer + wstruct.WriteLine("std::shared_ptr<{0}> {1};", TypeName(arg.Type, wdecl, arg.tok), FormalName(arg, i)); + } else { + wstruct.WriteLine("{0} {1};", TypeName(arg.Type, wdecl, arg.tok), FormalName(arg, i)); } + i++; } // Overload the comparison operator @@ -423,14 +415,12 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT wstruct.Write("\treturn true "); i = 0; foreach (Formal arg in ctor.Formals) { - if (!arg.IsGhost) { - if (arg.Type is UserDefinedType udt && udt.ResolvedClass == dt) { // Recursive destructor needs to use a pointer - wstruct.WriteLine("\t\t&& *(left.{0}) == *(right.{0})", FormalName(arg, i)); - } else { - wstruct.WriteLine("\t\t&& left.{0} == right.{0}", FormalName(arg, i)); - } - i++; + if (arg.Type is UserDefinedType udt && udt.ResolvedClass == dt) { // Recursive destructor needs to use a pointer + wstruct.WriteLine("\t\t&& *(left.{0}) == *(right.{0})", FormalName(arg, i)); + } else { + wstruct.WriteLine("\t\t&& left.{0} == right.{0}", FormalName(arg, i)); } + i++; } if (i == 0) { // Avoid a warning from the C++ compiler @@ -450,15 +440,13 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT owr.WriteLine("size_t seed = 0;"); int argCount = 0; foreach (var arg in ctor.Formals) { - if (!arg.IsGhost) { - if (arg.Type is UserDefinedType udt && udt.ResolvedClass == dt) { - // Recursive destructor needs to use a pointer - owr.WriteLine("hash_combine>(seed, x.{1});", TypeName(arg.Type, owr, dt.tok), arg.CompileName); - } else { - owr.WriteLine("hash_combine<{0}>(seed, x.{1});", TypeName(arg.Type, owr, dt.tok), arg.CompileName); - } - argCount++; + if (arg.Type is UserDefinedType udt && udt.ResolvedClass == dt) { + // Recursive destructor needs to use a pointer + owr.WriteLine("hash_combine>(seed, x.{1});", TypeName(arg.Type, owr, dt.tok), arg.CompileName); + } else { + owr.WriteLine("hash_combine<{0}>(seed, x.{1});", TypeName(arg.Type, owr, dt.tok), arg.CompileName); } + argCount++; } if (argCount == 0) { owr.WriteLine("(void)x;"); @@ -479,14 +467,12 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT wc.WriteLine("{0} COMPILER_result_subStruct;", DatatypeSubStructName(ctor, true)); foreach (Formal arg in ctor.Formals) { - if (!arg.IsGhost) { - if (arg.Type is UserDefinedType udt && udt.ResolvedClass == dt) { - // This is a recursive destuctor, so we need to allocate space and copy the input in - wc.WriteLine("COMPILER_result_subStruct.{0} = std::make_shared<{1}>({0});", arg.CompileName, - DtT_protected); - } else { - wc.WriteLine("COMPILER_result_subStruct.{0} = {0};", arg.CompileName); - } + if (arg.Type is UserDefinedType udt && udt.ResolvedClass == dt) { + // This is a recursive destuctor, so we need to allocate space and copy the input in + wc.WriteLine("COMPILER_result_subStruct.{0} = std::make_shared<{1}>({0});", arg.CompileName, + DtT_protected); + } else { + wc.WriteLine("COMPILER_result_subStruct.{0} = {0};", arg.CompileName); } } @@ -500,10 +486,8 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT var default_ctor = dt.Ctors[0]; // Arbitrarily choose the first one wd.WriteLine("{0} COMPILER_result_subStruct;", DatatypeSubStructName(default_ctor, true)); foreach (Formal arg in default_ctor.Formals) { - if (!arg.IsGhost) { - wd.WriteLine("COMPILER_result_subStruct.{0} = {1};", arg.CompileName, - DefaultValue(arg.Type, wd, arg.tok)); - } + wd.WriteLine("COMPILER_result_subStruct.{0} = {1};", arg.CompileName, + DefaultValue(arg.Type, wd, arg.tok)); } wd.WriteLine("v = COMPILER_result_subStruct;"); @@ -542,7 +526,7 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT foreach (var dtor in ctor.Destructors) { if (dtor.EnclosingCtors[0] == ctor) { var arg = dtor.CorrespondingFormals[0]; - if (!arg.IsGhost && arg.HasName) { + if (arg.HasName) { var returnType = TypeName(arg.Type, ws, arg.tok); if (arg.Type is UserDefinedType udt && udt.ResolvedClass == dt) { // This is a recursive destuctor, so return a pointer @@ -1170,15 +1154,13 @@ private string DeclareFormals(List formals) { var ret = ""; var sep = ""; foreach (Formal arg in formals) { - if (!arg.IsGhost) { - string name = FormalName(arg, i); - string decl = DeclareFormalString(sep, name, arg.Type, arg.tok, arg.InParam); - if (decl != null) { - ret += decl; - sep = ", "; - } - i++; + string name = FormalName(arg, i); + string decl = DeclareFormalString(sep, name, arg.Type, arg.tok, arg.InParam); + if (decl != null) { + ret += decl; + sep = ", "; } + i++; } return ret; } @@ -1412,12 +1394,9 @@ protected override void EmitNew(Type type, IToken tok, CallStmt initCall /*?*/, if (ctor != null && ctor.IsExtern(Options, out var q, out var n)) { // the arguments of any external constructor are placed here for (int i = 0; i < ctor.Ins.Count; i++) { - Formal p = ctor.Ins[i]; - if (!p.IsGhost) { - wr.Write(sep); - wr.Append(Expr(initCall.Args[i], false, wStmts)); - sep = ", "; - } + wr.Write(sep); + wr.Append(Expr(initCall.Args[i], false, wStmts)); + sep = ", "; } } wr.Write(")"); diff --git a/Source/DafnyCore/Backends/DafnyExecutableBackend.cs b/Source/DafnyCore/Backends/DafnyExecutableBackend.cs index 00efe28dca5..0651450ac13 100644 --- a/Source/DafnyCore/Backends/DafnyExecutableBackend.cs +++ b/Source/DafnyCore/Backends/DafnyExecutableBackend.cs @@ -3,6 +3,7 @@ using System.IO; using System.Linq; using Dafny; +using DafnyCore.Backends; namespace Microsoft.Dafny.Compilers; @@ -48,6 +49,7 @@ public IEnumerable ImportFiles(string dafnyProgramName) { } public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) { + GhostEraser.EraseGhostCode(dafnyProgram); ProcessTranslationRecords(dafnyProgram, dafnyProgramName, output); CheckInstantiationReplaceableModules(dafnyProgram); ProcessOuterModules(dafnyProgram); diff --git a/Source/DafnyCore/Backends/ExecutableBackend.cs b/Source/DafnyCore/Backends/ExecutableBackend.cs index 78aba798902..440c8b83179 100644 --- a/Source/DafnyCore/Backends/ExecutableBackend.cs +++ b/Source/DafnyCore/Backends/ExecutableBackend.cs @@ -7,6 +7,7 @@ using System.Linq; using System.Text; using System.Threading.Tasks; +using DafnyCore.Backends; using DafnyCore.Options; using Microsoft.Dafny.Compilers; using Microsoft.Dafny.Plugins; @@ -28,6 +29,7 @@ protected ExecutableBackend(DafnyOptions options) : base(options) { public override string ModuleSeparator => CodeGenerator.ModuleSeparator; public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) { + GhostEraser.EraseGhostCode(dafnyProgram); ProcessTranslationRecords(dafnyProgram, dafnyProgramName, output); CheckInstantiationReplaceableModules(dafnyProgram); ProcessOuterModules(dafnyProgram); diff --git a/Source/DafnyCore/Backends/GhostEraser.cs b/Source/DafnyCore/Backends/GhostEraser.cs new file mode 100644 index 00000000000..026c28df3b6 --- /dev/null +++ b/Source/DafnyCore/Backends/GhostEraser.cs @@ -0,0 +1,159 @@ +using System.Collections.Generic; +using System.Linq; +using System.Threading; +using Microsoft.Dafny; +using Microsoft.Dafny.LanguageServer.Workspace; +using Microsoft.Extensions.Logging.Abstractions; + +namespace DafnyCore.Backends; + +public static class GhostEraser { + class GhostCodeRemover : ASTVisitor { + protected override bool VisitOneStatement(Statement stmt, ICodeContext context) { + if (stmt is BlockStmt blockStmt) { + var statements = blockStmt.Body; + RemoveGhostStatements(statements); + } + + if (stmt is AssignStatement assignStatement) { + RemoveGhostStatements(assignStatement.ResolvedStatements); + } + return base.VisitOneStatement(stmt, context); + } + + protected override bool VisitOneExpression(Expression expr, ICodeContext context) { + if (expr is LetExpr letExpr) { + letExpr.LHSs = letExpr.LHSs.Where(lhs => !lhs.Var.IsGhost).ToList(); + } + return base.VisitOneExpression(expr, context); + } + + protected override void VisitCasePattern(CasePattern pattern) { + pattern.Arguments = pattern.Arguments?.Where(lhs => !lhs.Var.IsGhost).ToList(); + base.VisitCasePattern(pattern); + } + + private static void RemoveGhostStatements(List statements) { + for (int i = statements.Count - 1; i >= 0; i--) { + if (statements[i].IsGhost) { + statements.RemoveAt(i); + } + } + } + + public override ICodeContext GetContext(IASTVisitorContext astVisitorContext, bool inFunctionPostcondition) { + return (ICodeContext)astVisitorContext; + } + } + + public static void EraseGhostCode(Program program) { + var symbolTable = SymbolTable.CreateFrom(NullLogger.Instance, program, CancellationToken.None); + foreach (var compileModule in program.CompileModules) { + foreach (var topLevelDecl in compileModule.TopLevelDecls) { + if (topLevelDecl is DatatypeDecl datatypeDecl) { + foreach (var constructor in datatypeDecl.Ctors) { + var removalLocations = RemoveGhostParameters(program, symbolTable, constructor, constructor.Formals); + RemoveElementsAtGhostPositions(constructor.Destructors, removalLocations); + } + } + if (topLevelDecl is TopLevelDeclWithMembers withMembers) { + for (int i = withMembers.Members.Count - 1; i >= 0; i--) { + var member = withMembers.Members[i]; + if (member.IsGhost) { + if (member is Method && Attributes.Contains(member.Attributes, "test")) { + program.Reporter.Error(MessageSource.Compiler, GeneratorErrors.ErrorId.c_test_function_must_be_compilable, member.tok, + $"Function {member.FullName} must be compiled to use the {{:test}} attribute"); + } + + withMembers.Members.RemoveAt(i); + } + } + + foreach (var member in withMembers.Members) { + switch (member) { + case MethodOrFunction methodOrFunction: { + + RemoveGhostParameters(program, symbolTable, member, methodOrFunction.Ins); + if (methodOrFunction is Function { ByMethodDecl: not null } function) { + new GhostCodeRemover().VisitMethod(function.ByMethodDecl); + } + if (methodOrFunction is Method method) { + new GhostCodeRemover().VisitMethod(method); + // Remove ghost outs. + } + break; + } + } + } + } + } + + foreach (var decl in compileModule.TopLevelDecls) { + if (decl is TopLevelDeclWithMembers withMembers) { + foreach (var member in withMembers.Members) { + if (member is MethodOrFunction methodOrFunction) { + methodOrFunction.Ins = methodOrFunction.Ins.Where(i => !i.IsGhost).ToList(); + } + } + } + } + } + + } + + private static List RemoveGhostParameters(Program program, SymbolTable symbolTable, IHasNavigationToken member, + List formals) { + var removalLocations = new List(); + for (var index = formals.Count - 1; index >= 0; index--) { + var formal = formals[index]; + if (formal.IsGhost) { + removalLocations.Add(index); + } + } + + for (int i = formals.Count - 1; i >= 0; i--) { + if (formals[i].IsGhost) { + formals.RemoveAt(i); + } + } + + RemoveGhostParameters(program, symbolTable, member, removalLocations); + return removalLocations; + } + + private static void RemoveGhostParameters(Program program, SymbolTable symbolTable, IHasNavigationToken member, List removalLocations) + { + var references = symbolTable.GetReferences(member); + foreach (var reference in references) { + if (reference is MatchCase matchCase) { + RemoveElementsAtGhostPositions(matchCase.Arguments, removalLocations); + } + if (reference is IdPattern idPattern) { + RemoveElementsAtGhostPositions(idPattern.Arguments, removalLocations); + } + if (reference is DatatypeValue datatypeValue) { + RemoveElementsAtGhostPositions(datatypeValue.Arguments, removalLocations); + } + if (reference is FunctionCallExpr functionCallExpr) { + RemoveElementsAtGhostPositions(functionCallExpr.Args, removalLocations); + + } + if (reference is MemberSelectExpr memberSelectExpr) { + var applySuffix = program.FindNode(memberSelectExpr.Tok.Uri, memberSelectExpr.Tok.ToDafnyPosition()); + if (applySuffix != null) { + if (applySuffix.Lhs == memberSelectExpr) { + RemoveElementsAtGhostPositions(applySuffix.Args, removalLocations); + } + } + } + } + + return; + + } + static void RemoveElementsAtGhostPositions(List list, List removalLocations) { + foreach (var index in removalLocations) { + list.RemoveAt(index); + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index 7edddd6163a..5fd09521264 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -574,7 +574,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete Constructor ct = null; foreach (var member in iter.Members) { - if (member is Field f && !f.IsGhost) { + if (member is Field f) { cw.DeclareField(IdName(f), iter, false, false, f.Type, f.tok, PlaceboValue(f.Type, wr, f.tok, true), f); } else if (member is Constructor c) { Contract.Assert(ct == null); @@ -586,11 +586,9 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete cw.ConcreteMethodWriter.Write("func (_this * {0}) {1}(", IdName(iter), IdName(ct)); string sep = ""; foreach (var p in ct.Ins) { - if (!p.IsGhost) { - // here we rely on the parameters and the corresponding fields having the same names - cw.ConcreteMethodWriter.Write("{0}{1} {2}", sep, IdName(p), TypeName(p.Type, wr, p.tok)); - sep = ", "; - } + // here we rely on the parameters and the corresponding fields having the same names + cw.ConcreteMethodWriter.Write("{0}{1} {2}", sep, IdName(p), TypeName(p.Type, wr, p.tok)); + sep = ", "; } var wCtor = cw.ConcreteMethodWriter.NewBlock(")"); wCtor.WriteLine("_cont := make(chan struct{})"); diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs index c84c401d0aa..700ea343ce3 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs @@ -4408,6 +4408,7 @@ protected override void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSynta if (match.Cases.Count == 0) { base.EmitNestedMatchStmt(match, writer); } else { + // If we can get rid if this, we won't have to update NestedMatch.Children TrStmt(match.Flattened, writer); } } diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs index 9366be441ec..7d557f6a9c0 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs @@ -259,14 +259,11 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn WriteTypeDescriptors(dtv.Ctor.EnclosingDatatype, dtv.InferredTypeArgs, wTypeDescriptorArguments, ref sep); sep = ""; for (var i = 0; i < dtv.Arguments.Count; i++) { - var formal = dtv.Ctor.Formals[i]; - if (!formal.IsGhost) { - wrArgumentList.Write(sep); - var w = EmitCoercionIfNecessary(from: dtv.Arguments[i].Type, to: dtv.Ctor.Formals[i].Type.Subst(typeSubst), - toOrig: dtv.Ctor.Formals[i].Type, tok: dtv.tok, wr: wrArgumentList); - EmitExpr(dtv.Arguments[i], inLetExprBody, w, wStmts); - sep = ", "; - } + wrArgumentList.Write(sep); + var w = EmitCoercionIfNecessary(from: dtv.Arguments[i].Type, to: dtv.Ctor.Formals[i].Type.Subst(typeSubst), + toOrig: dtv.Ctor.Formals[i].Type, tok: dtv.tok, wr: wrArgumentList); + EmitExpr(dtv.Arguments[i], inLetExprBody, w, wStmts); + sep = ", "; } EmitDatatypeValue(dtv, wTypeDescriptorArguments.ToString(), wrArgumentList.ToString(), wr); @@ -328,7 +325,7 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn var w = wr; for (int i = 0; i < e.LHSs.Count; i++) { var lhs = e.LHSs[i]; - if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) { + if (lhs.Vars.Any()) { var rhsName = $"_pat_let{GetUniqueAstNumber(e)}_{i}"; w = CreateIIFE_ExprBody(rhsName, e.RHSs[i].Type, e.RHSs[i].tok, e.RHSs[i], inLetExprBody, e.Body.Type, e.Body.tok, w, ref wStmts); diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs index 8ae0c901eb5..696e09c7cbd 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs @@ -40,9 +40,6 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts ??= wr.Fork(); - if (stmt.IsGhost) { - return; - } switch (stmt) { case PrintStmt printStmt: { var s = printStmt; @@ -87,7 +84,7 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree if (resolved.Count == 1) { TrStmt(resolved[0], wr); } else { - var assignStmts = resolved.Cast().Where(assignStmt => !assignStmt.IsGhost).ToList(); + var assignStmts = resolved.Cast().ToList(); var lhss = new List(); var rhss = new List(); @@ -734,10 +731,6 @@ private ConcreteSyntaxTree EmitNestedMatchStmtCaseConstructor(string sourceName, for (int index = 0; index < ctor.Formals.Count; index++) { var arg = ctor.Formals[index]; - if (arg.IsGhost) { - continue; - } - var type = arg.Type.Subst(typeSubstMap); // ((Dt_Ctor0)source._D).a0; var destructor = new ConcreteSyntaxTree(); diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index ad76e859e1e..5b5ee9dd6ca 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -762,9 +762,7 @@ protected string ConstructorArguments(CallStmt initCall, ConcreteSyntaxTree wStm var arguments = Enumerable.Empty(); if (ctor != null && ctor.IsExtern(Options, out _, out _)) { // the arguments of any external constructor are placed here - arguments = ctor.Ins.Select((f, i) => (f, i)) - .Where(tp => !tp.f.IsGhost) - .Select(tp => Expr(initCall.Args[tp.i], false, wStmts).ToString()); + arguments = initCall.Args.Select(arg => Expr(arg, false, wStmts).ToString()); } return (arguments.Any() ? sep : "") + arguments.Comma(); } @@ -1533,7 +1531,7 @@ public void Compile(Program program, ConcreteSyntaxTree wrx) { if (include) { classIsExtern = !Options.DisallowExterns && Attributes.Contains(cl.Attributes, "extern"); if (classIsExtern && cl.Members.TrueForAll(member => - member.IsGhost || Attributes.Contains(member.Attributes, "extern"))) { + Attributes.Contains(member.Attributes, "extern"))) { include = false; } } @@ -1542,7 +1540,7 @@ public void Compile(Program program, ConcreteSyntaxTree wrx) { } protected bool HasCompilationMaterial(MemberDecl memberDecl) { - return !memberDecl.IsGhost && (Options.DisallowExterns || !Attributes.Contains(memberDecl.Attributes, "extern")); + return Options.DisallowExterns || !Attributes.Contains(memberDecl.Attributes, "extern"); } protected (bool classIsExtern, bool included) GetIsExternAndIncluded(DefaultClassDecl defaultClassDecl) { @@ -1554,7 +1552,7 @@ protected bool HasCompilationMaterial(MemberDecl memberDecl) { (!Options.DisallowExterns && Attributes.Contains(defaultClassDecl.Attributes, "extern")) || Attributes.Contains(defaultClassDecl.EnclosingModuleDefinition.Attributes, "extern"); if (classIsExtern && defaultClassDecl.Members.TrueForAll(member => - member.IsGhost || Attributes.Contains(member.Attributes, "extern"))) { + Attributes.Contains(member.Attributes, "extern"))) { include = false; } } @@ -1821,14 +1819,12 @@ protected string GenVarName(string root, List formals) { finished = true; int i = 0; foreach (var arg in formals) { - if (!arg.IsGhost) { - // FormalName returns a protected name, so we compare a protected version of "root" to it - if (IdProtect(root).Equals(FormalName(arg, i))) { - root += root; - finished = false; - } - i++; + // FormalName returns a protected name, so we compare a protected version of "root" to it + if (IdProtect(root).Equals(FormalName(arg, i))) { + root += root; + finished = false; } + i++; } } return root; @@ -1843,11 +1839,12 @@ protected int WriteFormals(string sep, List formals, ConcreteSyntaxTree int n = 0; for (var i = 0; i < formals.Count; i++) { var arg = formals[i]; - if (!arg.IsGhost) { + if (!arg.IsGhost) { // Can be removed when we clean up outs string name = FormalName(useTheseNamesForFormals == null ? arg : useTheseNamesForFormals[i], n); if (DeclareFormal(sep, name, arg.Type, arg.tok, arg.InParam, wr)) { sep = ", "; } + n++; } } @@ -2024,6 +2021,7 @@ public static bool IsPermittedAsMain(Program program, Method m, out String reaso } } if (!m.Ins.TrueForAll(f => f.IsGhost)) { + // This is run before GhostEraser var nonGhostFormals = m.Ins.Where(f => !f.IsGhost).ToList(); if (nonGhostFormals.Count > 1) { reason = "the method has two or more non-ghost parameters"; @@ -2140,9 +2138,7 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite foreach (var member in inheritedMembers.Select(memberx => (memberx as Function)?.ByMethodDecl ?? memberx)) { enclosingDeclaration = member; Contract.Assert(!member.IsStatic); // only instance members should ever be added to .InheritedMembers - if (member.IsGhost) { - // skip - } else if (c is TraitDecl) { + if (c is TraitDecl) { RedeclareInheritedMember(member, classWriter); } else if (member is ConstantField) { var cf = (ConstantField)member; @@ -2214,16 +2210,14 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite thisContext = c; } if (c is TraitDecl && member.OverriddenMember != null && !member.IsOverrideThatAddsBody) { - if (!member.IsGhost && TraitRepeatsInheritedDeclarations) { + if (TraitRepeatsInheritedDeclarations) { RedeclareInheritedMember(member, classWriter); } else { // emit nothing in the trait; this member will be emitted in the classes that extend this trait } } else if (member is Field) { var f = (Field)member; - if (f.IsGhost) { - // emit nothing - } else if (!Options.DisallowExterns && Attributes.Contains(f.Attributes, "extern")) { + if (!Options.DisallowExterns && Attributes.Contains(f.Attributes, "extern")) { // emit nothing } else if (f is ConstantField) { var cf = (ConstantField)f; @@ -2293,12 +2287,7 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite } } else if (member is Function) { var f = (Function)member; - if (f.IsGhost) { - if (Attributes.Contains(f.Attributes, "test")) { - Error(ErrorId.c_test_function_must_be_compilable, f.tok, - "Function {0} must be compiled to use the {{:test}} attribute", errorWr, f.FullName); - } - } else if (f.IsVirtual) { + if (f.IsVirtual) { if (f.OverriddenMember == null) { var w = classWriter.CreateFunction(IdName(f), CombineAllTypeArguments(f), f.Ins, f.ResultType, f.tok, false, false, f, false, false); Contract.Assert(w == null); // since we requested no body @@ -2332,7 +2321,6 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite "Method {0} is annotated with :synthesize but is not static, has a body, or does not return anything", errorWr, m.FullName); } - } else if (m.IsGhost) { } else if (m.IsVirtual) { if (m.OverriddenMember == null) { var w = classWriter.CreateMethod(m, CombineAllTypeArguments(m), false, false, false); @@ -2475,13 +2463,11 @@ protected void EmitCallToInheritedFunction(Function f, [CanBeNull] TopLevelDeclW for (int j = 0, l = 0; j < f.Ins.Count; j++) { var p = f.Ins[j]; - if (!p.IsGhost) { - wr.Write(sep); - w = EmitCoercionIfNecessary(f.Original.Ins[j].Type, f.Ins[j].Type, f.tok, wr); - w.Write(IdName(p)); - sep = ", "; - l++; - } + wr.Write(sep); + w = EmitCoercionIfNecessary(f.Original.Ins[j].Type, f.Ins[j].Type, f.tok, wr); + w.Write(IdName(p)); + sep = ", "; + l++; } wr.Write(")"); } @@ -2494,14 +2480,11 @@ protected virtual void EmitMultiReturnTuple(List outs, List outTyp var wrReturn = EmitReturnExpr(wr); var sep = ""; for (int j = 0, l = 0; j < outs.Count; j++) { - var p = outs[j]; - if (!p.IsGhost) { - wrReturn.Write(sep); - var w = EmitCoercionIfNecessary(outs[j].Type, outTypes[l], methodToken, wrReturn); - w.Write(outTmps[l]); - sep = ", "; - l++; - } + wrReturn.Write(sep); + var w = EmitCoercionIfNecessary(outs[j].Type, outTypes[l], methodToken, wrReturn); + w.Write(outTmps[l]); + sep = ", "; + l++; } } @@ -2561,13 +2544,11 @@ protected virtual void EmitCallToInheritedMethod(Method method, [CanBeNull] TopL for (int j = 0, l = 0; j < method.Ins.Count; j++) { var p = method.Ins[j]; - if (!p.IsGhost) { - wr.Write(sep); - w = EmitCoercionIfNecessary(method.Original.Ins[j].Type, method.Ins[j].Type, method.tok, wr); - EmitIdentifier(IdName(p), w); - sep = ", "; - l++; - } + wr.Write(sep); + w = EmitCoercionIfNecessary(method.Original.Ins[j].Type, method.Ins[j].Type, method.tok, wr); + EmitIdentifier(IdName(p), w); + sep = ", "; + l++; } if (!returnStyleOuts) { @@ -2916,16 +2897,11 @@ void TrCasePatternOpt(CasePattern pat, Expression rhs, Action bv.IsGhost)); - } else { - Type targetType = formal.Type.Subst(substMap); - TrCasePatternOpt(arg, null, sw => + Type targetType = formal.Type.Subst(substMap); + TrCasePatternOpt(arg, null, sw => EmitDestructor(wr => EmitIdentifier(tmp_name, wr), formal, k, ctor, () => dtv.InferredTypeArgs, arg.Expr.Type, sw), - targetType, pat.Expr.tok, wr, inLetExprBody); - k++; - } + targetType, pat.Expr.tok, wr, inLetExprBody); + k++; } } } diff --git a/Source/DafnyLanguageServer/Workspace/SymbolTable.cs b/Source/DafnyCore/Backends/SymbolTable.cs similarity index 90% rename from Source/DafnyLanguageServer/Workspace/SymbolTable.cs rename to Source/DafnyCore/Backends/SymbolTable.cs index 0d5abc385ad..66ebc174bd5 100644 --- a/Source/DafnyLanguageServer/Workspace/SymbolTable.cs +++ b/Source/DafnyCore/Backends/SymbolTable.cs @@ -110,19 +110,25 @@ private SymbolTable(IReadOnlyList references, IReadOnlyList GetReferences(Uri uri, Position position) { if (nodePositions.TryGetValue(uri, out var forFile)) { - return forFile.Query(position). - SelectMany(node => NodeToReferences.GetOrDefault(node, () => (ISet)new HashSet())). - Select(u => new Location { Uri = u.NavigationToken.Filepath, Range = u.NavigationToken.GetLspRange() }).Distinct(); + return forFile.Query(position).SelectMany(GetReferenceLocations).Distinct(); } return Enumerable.Empty(); } + public IEnumerable GetReferences(IHasNavigationToken node) { + return NodeToReferences.GetOrDefault(node, () => (ISet)new HashSet()); + } + + public IEnumerable GetReferenceLocations(IHasNavigationToken node) { + return GetReferences(node).Select(u => new Location { Uri = u.NavigationToken.Filepath, Range = u.NavigationToken.GetLspRange() }); + } + public Location? GetDeclaration(Uri uri, Position position) { var node = GetDeclarationNode(uri, position); return node == null ? null : NodeToLocation(node); } - internal static Location? NodeToLocation(IHasNavigationToken node) { + public static Location? NodeToLocation(IHasNavigationToken node) { if (node.NavigationToken.Uri == null) { return null; } diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 73318352a5e..cf6db207f50 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -31,6 +31,7 @@ +