From e7827041f1a561885335bdd15cb4cc2b6481ce94 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 7 Sep 2022 16:51:17 +0200 Subject: [PATCH 001/301] Added git-split.sh --- Scripts/git-split.sh | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100755 Scripts/git-split.sh diff --git a/Scripts/git-split.sh b/Scripts/git-split.sh new file mode 100755 index 00000000000..170c7a72f34 --- /dev/null +++ b/Scripts/git-split.sh @@ -0,0 +1,16 @@ +src=$1 +dst=$2 +temp_branch=git-cp-$RANDOM + +git checkout -b "$temp_branch" +git mv "$src" "$dst" +git commit -m "git: mv $src $dst" + +# This commit makes `git rebase --rebase-merges` work. +git checkout HEAD~ "$src" +git commit -m "git: checkout $src" +# -- + +git checkout - +git merge --no-ff -m "git: cp $src $dst" "$temp_branch" +git branch -d "$temp_branch" From a5ec01313746929ed8dcc7c29223c9c54fc5a404 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 7 Sep 2022 16:53:51 +0200 Subject: [PATCH 002/301] git: mv Source/Dafny/AST/DafnyAst.cs Source/Dafny/AST/Statements.cs --- Source/Dafny/AST/{DafnyAst.cs => Statements.cs} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename Source/Dafny/AST/{DafnyAst.cs => Statements.cs} (100%) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/Statements.cs similarity index 100% rename from Source/Dafny/AST/DafnyAst.cs rename to Source/Dafny/AST/Statements.cs From 1351c753e1cf5a05b04ca194fd57019b7e68d9f9 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 7 Sep 2022 16:53:51 +0200 Subject: [PATCH 003/301] git: checkout Source/Dafny/AST/DafnyAst.cs --- Source/Dafny/AST/DafnyAst.cs | 13310 +++++++++++++++++++++++++++++++++ 1 file changed, 13310 insertions(+) create mode 100644 Source/Dafny/AST/DafnyAst.cs diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs new file mode 100644 index 00000000000..14aee1ffdc1 --- /dev/null +++ b/Source/Dafny/AST/DafnyAst.cs @@ -0,0 +1,13310 @@ +#define TI_DEBUG_PRINT +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT +// +//----------------------------------------------------------------------------- +using System; +using System.Collections; +using System.Text; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Numerics; +using System.Linq; +using System.Diagnostics; +using System.Reflection; +using System.Threading; +using Microsoft.Boogie; + +namespace Microsoft.Dafny { + [System.AttributeUsage(System.AttributeTargets.Field)] + public class FilledInDuringResolutionAttribute : System.Attribute { } + + public interface IToken : Microsoft.Boogie.IToken { + /* + int kind { get; set; } + int pos { get; set; } + int col { get; set; } + int line { get; set; } + string val { get; set; } + bool IsValid { get; }*/ + string Boogie.IToken.filename { + get => Filename; + set => Filename = value; + } + + string Filename { get; set; } + + /// + /// TrailingTrivia contains everything after the token, + /// until and including two newlines between which there is no commment + /// All the remaining trivia is for the LeadingTrivia of the next token + /// + /// ``` + /// const /*for const*/ x /*for x*/ := /* for := */ 1/* for 1 */ + /// // for 1 again + /// // for 1 again + /// + /// // Two newlines, now all the trivia is for var y + /// // this line as well. + /// var y := 2 + /// ``` + /// + string TrailingTrivia { get; set; } + string LeadingTrivia { get; set; } + } + + /// + /// Has one-indexed line and column fields + /// + public record Token : IToken { + public Token peekedTokens; // Used only internally by Coco when the scanner "peeks" tokens. Normallly null at the end of parsing + public static readonly IToken NoToken = (IToken)new Token(); + + public Token() : this(0, 0) { } + + public Token(int linenum, int colnum) { + this.line = linenum; + this.col = colnum; + this.val = ""; + } + + public int kind { get; set; } // Used by coco, so we can't rename it to Kind + + public string Filename { get; set; } + + public int pos { get; set; } // Used by coco, so we can't rename it to Pos + + /// + /// One-indexed + /// + public int col { get; set; } // Used by coco, so we can't rename it to Col + + /// + /// One-indexed + /// + public int line { get; set; } // Used by coco, so we can't rename it to Line + + public string val { get; set; } // Used by coco, so we can't rename it to Val + + public string LeadingTrivia { get; set; } + + public string TrailingTrivia { get; set; } + + public bool IsValid => this.Filename != null; + } + + + public class Program { + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(FullName != null); + Contract.Invariant(DefaultModule != null); + } + + public readonly string FullName; + [FilledInDuringResolution] public Dictionary ModuleSigs; + // Resolution essentially flattens the module hierarchy, for + // purposes of translation and compilation. + [FilledInDuringResolution] public List CompileModules; + // Contains the definitions to be used for compilation. + + public Method MainMethod; // Method to be used as main if compiled + public readonly ModuleDecl DefaultModule; + public readonly ModuleDefinition DefaultModuleDef; + public readonly BuiltIns BuiltIns; + public ErrorReporter Reporter { get; set; } + + public Program(string name, [Captured] ModuleDecl module, [Captured] BuiltIns builtIns, ErrorReporter reporter) { + Contract.Requires(name != null); + Contract.Requires(module != null); + Contract.Requires(module is LiteralModuleDecl); + Contract.Requires(reporter != null); + FullName = name; + DefaultModule = module; + DefaultModuleDef = (DefaultModuleDecl)((LiteralModuleDecl)module).ModuleDef; + BuiltIns = builtIns; + this.Reporter = reporter; + ModuleSigs = new Dictionary(); + CompileModules = new List(); + } + + //Set appropriate visibilty before presenting module + public IEnumerable Modules() { + + foreach (var msig in ModuleSigs) { + Type.PushScope(msig.Value.VisibilityScope); + yield return msig.Key; + Type.PopScope(msig.Value.VisibilityScope); + } + + } + + public IEnumerable RawModules() { + return ModuleSigs.Keys; + } + + public string Name { + get { + try { + return System.IO.Path.GetFileName(FullName); + } catch (ArgumentException) { + return FullName; + } + } + } + + public IToken GetFirstTopLevelToken() { + return DefaultModuleDef.GetFirstTopLevelToken(); + } + } + + public class Include : IComparable { + public readonly IToken tok; + public string IncluderFilename { get; } + public string IncludedFilename { get; } + public string CanonicalPath { get; } + public bool CompileIncludedCode { get; } + public bool ErrorReported; + + public Include(IToken tok, string includer, string theFilename, bool compileIncludedCode) { + this.tok = tok; + this.IncluderFilename = includer; + this.IncludedFilename = theFilename; + this.CanonicalPath = DafnyFile.Canonicalize(theFilename); + this.ErrorReported = false; + CompileIncludedCode = compileIncludedCode; + } + + public int CompareTo(object obj) { + var i = obj as Include; + if (i != null) { + return this.CanonicalPath.CompareTo(i.CanonicalPath); + } else { + throw new NotImplementedException(); + } + } + } + + /// + /// An expression introducting bound variables + /// + public interface IBoundVarsBearingExpression : IRegion { + public IEnumerable AllBoundVars { + get; + } + } + + /// + /// A class implementing this interface is one that can carry attributes. + /// + public interface IAttributeBearingDeclaration { + Attributes Attributes { get; } + } + + public class Attributes { + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Name != null); + Contract.Invariant(cce.NonNullElements(Args)); + } + + public string Name; + /*Frozen*/ + public readonly List Args; + public readonly Attributes Prev; + + public Attributes(string name, [Captured] List args, Attributes prev) { + Contract.Requires(name != null); + Contract.Requires(cce.NonNullElements(args)); + Name = name; + Args = args; + Prev = prev; + } + + public static IEnumerable SubExpressions(Attributes attrs) { + return attrs.AsEnumerable().SelectMany(aa => aa.Args); + } + + public static bool Contains(Attributes attrs, string nm) { + Contract.Requires(nm != null); + return attrs.AsEnumerable().Any(aa => aa.Name == nm); + } + + /// + /// Returns first occurrence of an attribute named nm, or null if there is no such + /// attribute. + /// + [Pure] + public static Attributes/*?*/ Find(Attributes attrs, string nm) { + Contract.Requires(nm != null); + return attrs.AsEnumerable().FirstOrDefault(attr => attr.Name == nm); + } + + /// + /// Returns true if "nm" is a specified attribute. If it is, then: + /// - if the attribute is {:nm true}, then value==true + /// - if the attribute is {:nm false}, then value==false + /// - if the attribute is anything else, then value returns as whatever it was passed in as. + /// + [Pure] + public static bool ContainsBool(Attributes attrs, string nm, ref bool value) { + Contract.Requires(nm != null); + foreach (var attr in attrs.AsEnumerable()) { + if (attr.Name == nm) { + if (attr.Args.Count == 1) { + var arg = attr.Args[0] as LiteralExpr; + if (arg != null && arg.Value is bool) { + value = (bool)arg.Value; + } + } + return true; + } + } + return false; + } + + /// + /// Checks whether a Boolean attribute has been set on the declaration itself, + /// the enclosing class, or any enclosing module. Settings closer to the declaration + /// override those further away. + /// + public static bool ContainsBoolAtAnyLevel(MemberDecl decl, string attribName) { + bool setting = true; + if (Attributes.ContainsBool(decl.Attributes, attribName, ref setting)) { + return setting; + } + + if (Attributes.ContainsBool(decl.EnclosingClass.Attributes, attribName, ref setting)) { + return setting; + } + + // Check the entire stack of modules + var mod = decl.EnclosingClass.EnclosingModuleDefinition; + while (mod != null) { + if (Attributes.ContainsBool(mod.Attributes, attribName, ref setting)) { + return setting; + } + mod = mod.EnclosingModule; + } + + return false; + } + + /// + /// Returns list of expressions if "nm" is a specified attribute: + /// - if the attribute is {:nm e1,...,en}, then returns (e1,...,en) + /// Otherwise, returns null. + /// + public static List FindExpressions(Attributes attrs, string nm) { + Contract.Requires(nm != null); + foreach (var attr in attrs.AsEnumerable()) { + if (attr.Name == nm) { + return attr.Args; + } + } + return null; + } + + /// + /// Same as FindExpressions, but returns all matches + /// + public static List> FindAllExpressions(Attributes attrs, string nm) { + Contract.Requires(nm != null); + List> ret = null; + for (; attrs != null; attrs = attrs.Prev) { + if (attrs.Name == nm) { + ret = ret ?? new List>(); // Avoid allocating the list in the common case where we don't find nm + ret.Add(attrs.Args); + } + } + return ret; + } + + /// + /// Returns true if "nm" is a specified attribute whose arguments match the "allowed" parameter. + /// - if "nm" is not found in attrs, return false and leave value unmodified. Otherwise, + /// - if "allowed" contains Empty and the Args contains zero elements, return true and leave value unmodified. Otherwise, + /// - if "allowed" contains Bool and Args contains one bool literal, return true and set value to the bool literal. Otherwise, + /// - if "allowed" contains Int and Args contains one BigInteger literal, return true and set value to the BigInteger literal. Otherwise, + /// - if "allowed" contains String and Args contains one string literal, return true and set value to the string literal. Otherwise, + /// - if "allowed" contains Expression and Args contains one element, return true and set value to the one element (of type Expression). Otherwise, + /// - return false, leave value unmodified, and call reporter with an error string. + /// + public enum MatchingValueOption { Empty, Bool, Int, String, Expression } + public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object value, IEnumerable allowed, Action reporter) { + Contract.Requires(nm != null); + Contract.Requires(allowed != null); + Contract.Requires(reporter != null); + List args = FindExpressions(attrs, nm); + if (args == null) { + return false; + } else if (args.Count == 0) { + if (allowed.Contains(MatchingValueOption.Empty)) { + return true; + } else { + reporter("Attribute " + nm + " requires one argument"); + return false; + } + } else if (args.Count == 1) { + Expression arg = args[0]; + StringLiteralExpr stringLiteral = arg as StringLiteralExpr; + LiteralExpr literal = arg as LiteralExpr; + if (literal != null && literal.Value is bool && allowed.Contains(MatchingValueOption.Bool)) { + value = literal.Value; + return true; + } else if (literal != null && literal.Value is BigInteger && allowed.Contains(MatchingValueOption.Int)) { + value = literal.Value; + return true; + } else if (stringLiteral != null && stringLiteral.Value is string && allowed.Contains(MatchingValueOption.String)) { + value = stringLiteral.Value; + return true; + } else if (allowed.Contains(MatchingValueOption.Expression)) { + value = arg; + return true; + } else { + reporter("Attribute " + nm + " expects an argument in one of the following categories: " + String.Join(", ", allowed)); + return false; + } + } else { + reporter("Attribute " + nm + " cannot have more than one argument"); + return false; + } + } + } + + public static class AttributesExtensions { + /// + /// By making this an extension method, it can also be invoked for a null receiver. + /// + public static IEnumerable AsEnumerable(this Attributes attr) { + while (attr != null) { + yield return attr; + attr = attr.Prev; + } + } + } + + public class UserSuppliedAttributes : Attributes { + public readonly IToken tok; // may be null, if the attribute was constructed internally + public readonly IToken OpenBrace; + public readonly IToken CloseBrace; + public bool Recognized; // set to true to indicate an attribute that is processed by some part of Dafny; this allows it to be colored in the IDE + public UserSuppliedAttributes(IToken tok, IToken openBrace, IToken closeBrace, List args, Attributes prev) + : base(tok.val, args, prev) { + Contract.Requires(tok != null); + Contract.Requires(openBrace != null); + Contract.Requires(closeBrace != null); + Contract.Requires(args != null); + this.tok = tok; + OpenBrace = openBrace; + CloseBrace = closeBrace; + } + } + + // ------------------------------------------------------------------------------------------------------ + + public abstract class Type { + public static readonly BoolType Bool = new BoolType(); + public static readonly CharType Char = new CharType(); + public static readonly IntType Int = new IntType(); + public static readonly RealType Real = new RealType(); + public static Type Nat() { return new UserDefinedType(Token.NoToken, "nat", null); } // note, this returns an unresolved type + public static Type String() { return new UserDefinedType(Token.NoToken, "string", null); } // note, this returns an unresolved type + public static readonly BigOrdinalType BigOrdinal = new BigOrdinalType(); + + private static AsyncLocal> _scopes = new(); + private static List Scopes => _scopes.Value ??= new(); + + [ThreadStatic] + private static bool scopesEnabled = false; + + public static void PushScope(VisibilityScope scope) { + Scopes.Add(scope); + } + + public static void ResetScopes() { + _scopes.Value = new(); + scopesEnabled = false; + } + + public static void PopScope() { + Contract.Assert(Scopes.Count > 0); + Scopes.RemoveAt(Scopes.Count - 1); + } + + public static void PopScope(VisibilityScope expected) { + Contract.Assert(Scopes.Count > 0); + Contract.Assert(Scopes[^1] == expected); + PopScope(); + } + + public static VisibilityScope GetScope() { + if (scopesEnabled && Scopes.Count > 0) { + return Scopes[^1]; + } + return null; + } + + public static void EnableScopes() { + Contract.Assert(!scopesEnabled); + scopesEnabled = true; + } + + public static void DisableScopes() { + Contract.Assert(scopesEnabled); + scopesEnabled = false; + } + + public static string TypeArgsToString(ModuleDefinition/*?*/ context, List typeArgs, bool parseAble = false) { + Contract.Requires(typeArgs == null || + (typeArgs.All(ty => ty != null && ty.TypeName(context, parseAble) != null) && + (typeArgs.All(ty => ty.TypeName(context, parseAble).StartsWith("_")) || + typeArgs.All(ty => !ty.TypeName(context, parseAble).StartsWith("_"))))); + + if (typeArgs != null && typeArgs.Count > 0 && + (!parseAble || !typeArgs[0].TypeName(context, parseAble).StartsWith("_"))) { + return string.Format("<{0}>", Util.Comma(typeArgs, ty => ty.TypeName(context, parseAble))); + } + return ""; + } + + public static string TypeArgsToString(List typeArgs, bool parseAble = false) { + return TypeArgsToString(null, typeArgs, parseAble); + } + + public string TypeArgsToString(ModuleDefinition/*?*/ context, bool parseAble = false) { + return Type.TypeArgsToString(context, this.TypeArgs, parseAble); + } + + // Type arguments to the type + public List TypeArgs = new List(); + + /// + /// Add to "tps" the free type parameters in "this". + /// Requires the type to be resolved. + /// + public void AddFreeTypeParameters(ISet tps) { + Contract.Requires(tps != null); + var ty = this.NormalizeExpandKeepConstraints(); + var tp = ty.AsTypeParameter; + if (tp != null) { + tps.Add(tp); + } + foreach (var ta in ty.TypeArgs) { + ta.AddFreeTypeParameters(tps); + } + } + + [Pure] + public abstract string TypeName(ModuleDefinition/*?*/ context, bool parseAble = false); + [Pure] + public override string ToString() { + return TypeName(null, false); + } + + /// + /// Return the most constrained version of "this", getting to the bottom of proxies. + /// + /// Here is a description of the Normalize(), NormalizeExpandKeepConstraints(), and NormalizeExpand() methods: + /// * Any .Type field in the AST can, in general, be an AST node that is not really a type, but an AST node that has + /// a field where the type is filled in, once the type has been inferred. Such "types" are called "type proxies". + /// To follow a .Type (or other variable denoting a type) past its chain of type proxies, you call .Normalize(). + /// If you do this after type inference (more precisely, after the CheckTypeInference calls in Pass 1 of the + /// Resolver), then you will get back a NonProxyType. + /// * That may not be enough. Even after calling .Normalize(), you may get a type that denotes a type synonym. If + /// you compare it with, say, is SetType, you will get false if the type you're looking at is a type synonym for + /// a SetType. Therefore, to go past both type proxies and type synonyms, you call .NormalizeExpandKeepConstraints(). + /// * Actually, that may not be enough, either. Because .NormalizeExpandKeepConstraints() may return a subset type + /// whose base type is what you're looking for. If you want to go all the way to the base type, then you should + /// call .NormalizeExpand(). This is what is done most commonly when something is trying to look for a specific type. + /// * So, in conclusion: Usually you have to call .NormalizeExpand() on a type to unravel type proxies, type synonyms, + /// and subset types. But in other places (in particular, in the verifier) where you want to know about any type + /// constraints, then you call .NormalizeExpandKeepConstraints(). + /// + public Type Normalize() { + Contract.Ensures(Contract.Result() != null); + Type type = this; + while (true) { + var pt = type as TypeProxy; + if (pt != null && pt.T != null) { + type = pt.T; + } else { + return type; + } + } + } + + /// + /// Return the type that "this" stands for, getting to the bottom of proxies and following type synonyms. + /// + /// For more documentation, see method Normalize(). + /// + [Pure] + public Type NormalizeExpand(bool keepConstraints = false) { + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(!(Contract.Result() is TypeProxy) || ((TypeProxy)Contract.Result()).T == null); // return a proxy only if .T == null + Type type = this; + while (true) { + + var pt = type as TypeProxy; + if (pt != null && pt.T != null) { + type = pt.T; + continue; + } + + var scope = Type.GetScope(); + var rtd = type.AsRevealableType; + if (rtd != null) { + var udt = (UserDefinedType)type; + + if (!rtd.AsTopLevelDecl.IsVisibleInScope(scope)) { + // This can only mean "rtd" is a class/trait that is only provided, not revealed. For a provided class/trait, + // it is the non-null type declaration that is visible, not the class/trait declaration itself. + if (rtd is ClassDecl cl) { + Contract.Assert(cl.NonNullTypeDecl != null); + Contract.Assert(cl.NonNullTypeDecl.IsVisibleInScope(scope)); + } else { + Contract.Assert(rtd is OpaqueTypeDecl); + } + } + + if (rtd.IsRevealedInScope(scope)) { + if (rtd is TypeSynonymDecl && (!(rtd is SubsetTypeDecl) || !keepConstraints)) { + type = ((TypeSynonymDecl)rtd).RhsWithArgumentIgnoringScope(udt.TypeArgs); + continue; + } else { + return type; + } + } else { // type is hidden, no more normalization is possible + return rtd.SelfSynonym(type.TypeArgs); + } + } + + // A hidden type may become visible in another scope + var isyn = type.AsInternalTypeSynonym; + if (isyn != null) { + var udt = (UserDefinedType)type; + + if (!isyn.IsVisibleInScope(scope)) { + // This can only mean "isyn" refers to a class/trait that is only provided, not revealed. For a provided class/trait, + // it is the non-null type declaration that is visible, not the class/trait declaration itself. + var rhs = isyn.RhsWithArgumentIgnoringScope(udt.TypeArgs); + Contract.Assert(rhs is UserDefinedType); + var cl = ((UserDefinedType)rhs).ResolvedClass as ClassDecl; + Contract.Assert(cl != null && cl.NonNullTypeDecl != null); + Contract.Assert(cl.NonNullTypeDecl.IsVisibleInScope(scope)); + } + + if (isyn.IsRevealedInScope(scope)) { + type = isyn.RhsWithArgument(udt.TypeArgs); + continue; + } else { + return type; + } + } + + return type; + } + } + + /// + /// Return the type that "this" stands for, getting to the bottom of proxies and following type synonyms, but does + /// not follow subset types. + /// + /// For more documentation, see method Normalize(). + /// + [Pure] + public Type NormalizeExpandKeepConstraints() { + return NormalizeExpand(true); + } + + /// + /// Return "the type that "this" stands for, getting to the bottom of proxies and following type synonyms. + /// + public Type UseInternalSynonym() { + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(!(Contract.Result() is TypeProxy) || ((TypeProxy)Contract.Result()).T == null); // return a proxy only if .T == null + + Type type = Normalize(); + var scope = Type.GetScope(); + var rtd = type.AsRevealableType; + if (rtd != null) { + var udt = (UserDefinedType)type; + if (!rtd.AsTopLevelDecl.IsVisibleInScope(scope)) { + // This can only mean "rtd" is a class/trait that is only provided, not revealed. For a provided class/trait, + // it is the non-null type declaration that is visible, not the class/trait declaration itself. + var cl = rtd as ClassDecl; + Contract.Assert(cl != null && cl.NonNullTypeDecl != null); + Contract.Assert(cl.NonNullTypeDecl.IsVisibleInScope(scope)); + } + if (!rtd.IsRevealedInScope(scope)) { + return rtd.SelfSynonym(type.TypeArgs, udt.NamePath); + } + } + + return type; + } + + /// + /// Returns whether or not "this" and "that" denote the same type, modulo proxies and type synonyms and subset types. + /// + [Pure] + public abstract bool Equals(Type that, bool keepConstraints = false); + + public bool IsBoolType { get { return NormalizeExpand() is BoolType; } } + public bool IsCharType { get { return NormalizeExpand() is CharType; } } + public bool IsIntegerType { get { return NormalizeExpand() is IntType; } } + public bool IsRealType { get { return NormalizeExpand() is RealType; } } + public bool IsBigOrdinalType { get { return NormalizeExpand() is BigOrdinalType; } } + public bool IsBitVectorType { get { return AsBitVectorType != null; } } + public BitvectorType AsBitVectorType { get { return NormalizeExpand() as BitvectorType; } } + public bool IsNumericBased() { + var t = NormalizeExpand(); + return t.IsIntegerType || t.IsRealType || t.AsNewtype != null; + } + public enum NumericPersuasion { Int, Real } + [Pure] + public bool IsNumericBased(NumericPersuasion p) { + Type t = this; + while (true) { + t = t.NormalizeExpand(); + if (t.IsIntegerType) { + return p == NumericPersuasion.Int; + } else if (t.IsRealType) { + return p == NumericPersuasion.Real; + } + var d = t.AsNewtype; + if (d == null) { + return false; + } + t = d.BaseType; + } + } + + /// + /// This property returns true if the type is known to be nonempty. + /// This property should be used only after successful resolution. It is assumed that all type proxies have + /// been resolved and that all recursion through types comes to an end. + /// Note, HasCompilableValue ==> IsNonEmpty. + /// + public bool IsNonempty => GetAutoInit() != AutoInitInfo.MaybeEmpty; + + /// + /// This property returns true if the type has a known compilable value. + /// This property should be used only after successful resolution. It is assumed that all type proxies have + /// been resolved and that all recursion through types comes to an end. + /// Note, HasCompilableValue ==> IsNonEmpty. + /// + public bool HasCompilableValue => GetAutoInit() == AutoInitInfo.CompilableValue; + + public bool KnownToHaveToAValue(bool ghostContext) { + return ghostContext ? IsNonempty : HasCompilableValue; + } + + public enum AutoInitInfo { MaybeEmpty, Nonempty, CompilableValue } + + /// + /// This property returns + /// - CompilableValue, if the type has a known compilable value + /// - Nonempty, if the type is known to contain some value + /// - MaybeEmpty, otherwise + /// This property should be used only after successful resolution. It is assumed that all type proxies have + /// been resolved and that all recursion through types comes to an end. + /// + public AutoInitInfo GetAutoInit(List/*?*/ coDatatypesBeingVisited = null) { + var t = NormalizeExpandKeepConstraints(); + Contract.Assume(t is NonProxyType); // precondition + + AutoInitInfo CharacteristicToAutoInitInfo(TypeParameter.TypeParameterCharacteristics c) { + if (c.HasCompiledValue) { + return AutoInitInfo.CompilableValue; + } else if (c.IsNonempty) { + return AutoInitInfo.Nonempty; + } else { + return AutoInitInfo.MaybeEmpty; + } + } + + if (t is BoolType || t is CharType || t is IntType || t is BigOrdinalType || t is RealType || t is BitvectorType) { + return AutoInitInfo.CompilableValue; + } else if (t is CollectionType) { + return AutoInitInfo.CompilableValue; + } + + var udt = (UserDefinedType)t; + var cl = udt.ResolvedClass; + Contract.Assert(cl != null); + if (cl is OpaqueTypeDecl) { + var otd = (OpaqueTypeDecl)cl; + return CharacteristicToAutoInitInfo(otd.Characteristics); + } else if (cl is TypeParameter) { + var tp = (TypeParameter)cl; + return CharacteristicToAutoInitInfo(tp.Characteristics); + } else if (cl is InternalTypeSynonymDecl) { + var isyn = (InternalTypeSynonymDecl)cl; + return CharacteristicToAutoInitInfo(isyn.Characteristics); + } else if (cl is NewtypeDecl) { + var td = (NewtypeDecl)cl; + switch (td.WitnessKind) { + case SubsetTypeDecl.WKind.CompiledZero: + case SubsetTypeDecl.WKind.Compiled: + return AutoInitInfo.CompilableValue; + case SubsetTypeDecl.WKind.Ghost: + return AutoInitInfo.Nonempty; + case SubsetTypeDecl.WKind.OptOut: + return AutoInitInfo.MaybeEmpty; + case SubsetTypeDecl.WKind.Special: + default: + Contract.Assert(false); // unexpected case + throw new cce.UnreachableException(); + } + } else if (cl is SubsetTypeDecl) { + var td = (SubsetTypeDecl)cl; + switch (td.WitnessKind) { + case SubsetTypeDecl.WKind.CompiledZero: + case SubsetTypeDecl.WKind.Compiled: + return AutoInitInfo.CompilableValue; + case SubsetTypeDecl.WKind.Ghost: + return AutoInitInfo.Nonempty; + case SubsetTypeDecl.WKind.OptOut: + return AutoInitInfo.MaybeEmpty; + case SubsetTypeDecl.WKind.Special: + // WKind.Special is only used with -->, ->, and non-null types: + Contract.Assert(ArrowType.IsPartialArrowTypeName(td.Name) || ArrowType.IsTotalArrowTypeName(td.Name) || td is NonNullTypeDecl); + if (ArrowType.IsPartialArrowTypeName(td.Name)) { + // partial arrow + return AutoInitInfo.CompilableValue; + } else if (ArrowType.IsTotalArrowTypeName(td.Name)) { + // total arrow + return udt.TypeArgs.Last().GetAutoInit(coDatatypesBeingVisited); + } else if (((NonNullTypeDecl)td).Class is ArrayClassDecl) { + // non-null array type; we know how to initialize them + return AutoInitInfo.CompilableValue; + } else { + // non-null (non-array) type + return AutoInitInfo.MaybeEmpty; + } + default: + Contract.Assert(false); // unexpected case + throw new cce.UnreachableException(); + } + } else if (cl is ClassDecl) { + return AutoInitInfo.CompilableValue; // null is a value of this type + } else if (cl is DatatypeDecl) { + var dt = (DatatypeDecl)cl; + var subst = Resolver.TypeSubstitutionMap(dt.TypeArgs, udt.TypeArgs); + var r = AutoInitInfo.CompilableValue; // assume it's compilable, until we find out otherwise + if (cl is CoDatatypeDecl) { + if (coDatatypesBeingVisited != null) { + if (coDatatypesBeingVisited.Exists(coType => udt.Equals(coType))) { + // This can be compiled into a lazy constructor call + return AutoInitInfo.CompilableValue; + } else if (coDatatypesBeingVisited.Exists(coType => dt == coType.ResolvedClass)) { + // This requires more recursion and bookkeeping than we care to try out + return AutoInitInfo.MaybeEmpty; + } + coDatatypesBeingVisited = new List(coDatatypesBeingVisited); + } else { + coDatatypesBeingVisited = new List(); + } + coDatatypesBeingVisited.Add(udt); + } + foreach (var formal in dt.GetGroundingCtor().Formals) { + var autoInit = Resolver.SubstType(formal.Type, subst).GetAutoInit(coDatatypesBeingVisited); + if (autoInit == AutoInitInfo.MaybeEmpty) { + return AutoInitInfo.MaybeEmpty; + } else if (formal.IsGhost) { + // cool + } else if (autoInit == AutoInitInfo.CompilableValue) { + // cool + } else { + r = AutoInitInfo.Nonempty; + } + } + return r; + } else { + Contract.Assert(false); // unexpected type + throw new cce.UnreachableException(); + } + } + + public bool HasFinitePossibleValues { + get { + if (IsBoolType || IsCharType || IsRefType) { + return true; + } + var st = AsSetType; + if (st != null && st.Arg.HasFinitePossibleValues) { + return true; + } + var mt = AsMapType; + if (mt != null && mt.Domain.HasFinitePossibleValues) { + return true; + } + var dt = AsDatatype; + if (dt != null && dt.HasFinitePossibleValues) { + return true; + } + return false; + } + } + + public CollectionType AsCollectionType { get { return NormalizeExpand() as CollectionType; } } + public SetType AsSetType { get { return NormalizeExpand() as SetType; } } + public MultiSetType AsMultiSetType { get { return NormalizeExpand() as MultiSetType; } } + public SeqType AsSeqType { get { return NormalizeExpand() as SeqType; } } + public MapType AsMapType { get { return NormalizeExpand() as MapType; } } + + public bool IsRefType { + get { + var udt = NormalizeExpand() as UserDefinedType; + return udt != null && udt.ResolvedClass is ClassDecl && !(udt.ResolvedClass is ArrowTypeDecl); + } + } + + public bool IsTopLevelTypeWithMembers { + get { + return AsTopLevelTypeWithMembers != null; + } + } + public TopLevelDeclWithMembers/*?*/ AsTopLevelTypeWithMembers { + get { + var udt = NormalizeExpand() as UserDefinedType; + return udt?.ResolvedClass as TopLevelDeclWithMembers; + } + } + public TopLevelDeclWithMembers/*?*/ AsTopLevelTypeWithMembersBypassInternalSynonym { + get { + var udt = NormalizeExpand() as UserDefinedType; + if (udt != null && udt.ResolvedClass is InternalTypeSynonymDecl isyn) { + udt = isyn.RhsWithArgumentIgnoringScope(udt.TypeArgs) as UserDefinedType; + if (udt?.ResolvedClass is NonNullTypeDecl nntd) { + return nntd.Class; + } + } + return udt?.ResolvedClass as TopLevelDeclWithMembers; + } + } + /// + /// Returns "true" if the type represents the type "object?". + /// + public bool IsObjectQ { + get { + var udt = NormalizeExpandKeepConstraints() as UserDefinedType; + return udt != null && udt.ResolvedClass is ClassDecl && ((ClassDecl)udt.ResolvedClass).IsObjectTrait; + } + } + /// + /// Returns "true" if the type represents the type "object". + /// + public bool IsObject { + get { + var nn = AsNonNullRefType; + if (nn != null) { + var nonNullRefDecl = (NonNullTypeDecl)nn.ResolvedClass; + return nonNullRefDecl.Class.IsObjectTrait; + } + return false; + } + } + /// + /// Returns "true" if the type is a non-null type or any subset type thereof. + /// + public bool IsNonNullRefType { + get { + return AsNonNullRefType != null; + } + } + /// + /// If the type is a non-null type or any subset type thereof, return the UserDefinedType whose + /// .ResolvedClass value is a NonNullTypeDecl. + /// Otherwise, return "null". + /// + public UserDefinedType AsNonNullRefType { + get { + var t = this; + while (true) { + var udt = t.NormalizeExpandKeepConstraints() as UserDefinedType; + if (udt == null) { + return null; + } + if (udt.ResolvedClass is NonNullTypeDecl) { + return udt; + } + var sst = udt.ResolvedClass as SubsetTypeDecl; + if (sst != null) { + t = sst.RhsWithArgument(udt.TypeArgs); // continue the search up the chain of subset types + } else { + return null; + } + } + } + } + /// + /// Returns the type "parent", where "X" is a list of type parameters that makes "parent" a supertype of "this". + /// Requires "this" to be some type "C" and "parent" to be among the reflexive, transitive parent traits of "C". + /// + public UserDefinedType AsParentType(TopLevelDecl parent) { + Contract.Requires(parent != null); + + var udt = (UserDefinedType)NormalizeExpand(); + if (udt.ResolvedClass is InternalTypeSynonymDecl isyn) { + udt = isyn.RhsWithArgumentIgnoringScope(udt.TypeArgs) as UserDefinedType; + } + TopLevelDeclWithMembers cl; + if (udt.ResolvedClass is NonNullTypeDecl nntd) { + cl = (TopLevelDeclWithMembers)nntd.ViewAsClass; + } else { + cl = (TopLevelDeclWithMembers)udt.ResolvedClass; + } + if (cl == parent) { + return udt; + } + var typeMapParents = cl.ParentFormalTypeParametersToActuals; + var typeMapUdt = Resolver.TypeSubstitutionMap(cl.TypeArgs, udt.TypeArgs); + var typeArgs = parent.TypeArgs.ConvertAll(tp => Resolver.SubstType(typeMapParents[tp], typeMapUdt)); + return new UserDefinedType(udt.tok, parent.Name, parent, typeArgs); + } + public bool IsTraitType { + get { + return AsTraitType != null; + } + } + public TraitDecl/*?*/ AsTraitType { + get { + var udt = NormalizeExpand() as UserDefinedType; + return udt?.ResolvedClass as TraitDecl; + } + } + + public SubsetTypeDecl /*?*/ AsSubsetType { + get { + var std = NormalizeExpand(true) as UserDefinedType; + return std?.ResolvedClass as SubsetTypeDecl; + } + } + + public bool IsArrayType { + get { + return AsArrayType != null; + } + } + public ArrayClassDecl/*?*/ AsArrayType { + get { + var t = NormalizeExpand(); + var udt = UserDefinedType.DenotesClass(t); + return udt?.ResolvedClass as ArrayClassDecl; + } + } + /// + /// Returns "true" if the type is one of the 3 built-in arrow types. + /// + public bool IsBuiltinArrowType { + get { + var t = Normalize(); // but don't expand synonyms or strip off constraints + if (t is ArrowType) { + return true; + } + var udt = t as UserDefinedType; + return udt != null && (ArrowType.IsPartialArrowTypeName(udt.Name) || ArrowType.IsTotalArrowTypeName(udt.Name)); + } + } + /// + /// Returns "true" if the type is a partial arrow or any subset type thereof. + /// + public bool IsArrowTypeWithoutReadEffects { + get { + var t = this; + while (true) { + var udt = t.NormalizeExpandKeepConstraints() as UserDefinedType; + if (udt == null) { + return false; + } else if (ArrowType.IsPartialArrowTypeName(udt.Name)) { + return true; + } + var sst = udt.ResolvedClass as SubsetTypeDecl; + if (sst != null) { + t = sst.RhsWithArgument(udt.TypeArgs); // continue the search up the chain of subset types + } else { + return false; + } + } + } + } + /// + /// Returns "true" if the type is a total arrow or any subset type thereof. + /// + public bool IsArrowTypeWithoutPreconditions { + get { + var t = this; + while (true) { + var udt = t.NormalizeExpandKeepConstraints() as UserDefinedType; + if (udt == null) { + return false; + } else if (ArrowType.IsTotalArrowTypeName(udt.Name)) { + return true; + } + var sst = udt.ResolvedClass as SubsetTypeDecl; + if (sst != null) { + t = sst.RhsWithArgument(udt.TypeArgs); // continue the search up the chain of subset types + } else { + return false; + } + } + } + } + public bool IsArrowType { + get { return AsArrowType != null; } + } + public ArrowType AsArrowType { + get { + var t = NormalizeExpand(); + return t as ArrowType; + } + } + + public bool IsMapType { + get { + var t = NormalizeExpand() as MapType; + return t != null && t.Finite; + } + } + public bool IsIMapType { + get { + var t = NormalizeExpand() as MapType; + return t != null && !t.Finite; + } + } + public bool IsISetType { + get { + var t = NormalizeExpand() as SetType; + return t != null && !t.Finite; + } + } + public NewtypeDecl AsNewtype { + get { + var udt = NormalizeExpand() as UserDefinedType; + return udt == null ? null : udt.ResolvedClass as NewtypeDecl; + } + } + public TypeSynonymDecl AsTypeSynonym { + get { + var udt = this as UserDefinedType; // note, it is important to use 'this' here, not 'this.NormalizeExpand()' + if (udt == null) { + return null; + } else { + return udt.ResolvedClass as TypeSynonymDecl; + } + } + } + public InternalTypeSynonymDecl AsInternalTypeSynonym { + get { + var udt = this as UserDefinedType; // note, it is important to use 'this' here, not 'this.NormalizeExpand()' + if (udt == null) { + return null; + } else { + return udt.ResolvedClass as InternalTypeSynonymDecl; + } + } + } + public RedirectingTypeDecl AsRedirectingType { + get { + var udt = this as UserDefinedType; // Note, it is important to use 'this' here, not 'this.NormalizeExpand()'. This property getter is intended to be used during resolution, or with care thereafter. + if (udt == null) { + return null; + } else { + return (RedirectingTypeDecl)(udt.ResolvedClass as TypeSynonymDecl) ?? udt.ResolvedClass as NewtypeDecl; + } + } + } + public RevealableTypeDecl AsRevealableType { + get { + var udt = this as UserDefinedType; + if (udt == null) { + return null; + } else { + return (udt.ResolvedClass as RevealableTypeDecl); + } + } + } + public bool IsRevealableType { + get { return AsRevealableType != null; } + } + public bool IsDatatype { + get { + return AsDatatype != null; + } + } + public DatatypeDecl AsDatatype { + get { + var udt = NormalizeExpand() as UserDefinedType; + if (udt == null) { + return null; + } else { + return udt.ResolvedClass as DatatypeDecl; + } + } + } + public bool IsIndDatatype { + get { + return AsIndDatatype != null; + } + } + public IndDatatypeDecl AsIndDatatype { + get { + var udt = NormalizeExpand() as UserDefinedType; + if (udt == null) { + return null; + } else { + return udt.ResolvedClass as IndDatatypeDecl; + } + } + } + public bool IsCoDatatype { + get { + return AsCoDatatype != null; + } + } + public CoDatatypeDecl AsCoDatatype { + get { + var udt = NormalizeExpand() as UserDefinedType; + if (udt == null) { + return null; + } else { + return udt.ResolvedClass as CoDatatypeDecl; + } + } + } + public bool InvolvesCoDatatype { + get { + return IsCoDatatype; // TODO: should really check structure of the type recursively + } + } + public bool IsTypeParameter { + get { + return AsTypeParameter != null; + } + } + public bool IsInternalTypeSynonym { + get { return AsInternalTypeSynonym != null; } + } + public TypeParameter AsTypeParameter { + get { + var ct = NormalizeExpandKeepConstraints() as UserDefinedType; + return ct?.ResolvedClass as TypeParameter; + } + } + public bool IsOpaqueType { + get { return AsOpaqueType != null; } + } + public OpaqueTypeDecl AsOpaqueType { + get { + var udt = this.Normalize() as UserDefinedType; // note, it is important to use 'this.Normalize()' here, not 'this.NormalizeExpand()' + return udt?.ResolvedClass as OpaqueTypeDecl; + } + } + public virtual bool SupportsEquality { + get { + return true; + } + } + + public bool MayInvolveReferences => ComputeMayInvolveReferences(null); + + /// + /// This is an auxiliary method used to compute the value of MayInvolveReferences (above). It is + /// needed to handle datatypes, because determining whether or not a datatype contains references + /// involves recursing over the types in the datatype's constructor parameters. Since those types + /// may be mutually dependent on the datatype itself, care must be taken to avoid infinite recursion. + /// + /// Parameter visitedDatatypes is used to prevent infinite recursion. It is passed in as null + /// (the "first phase") as long as no datatype has been encountered. From the time a first datatype + /// is encountered and through all subsequent recursive calls to ComputeMayInvolveReferences that + /// are performed on the types of the parameters of the datatype's constructors, the method enters + /// a "second phase", where visitedDatatypes is passed in as a set that records all datatypes visited. + /// By not recursing through a datatype that's already being visited, infinite recursion is prevented. + /// + /// The type parameters to recursive uses of datatypes may be passed in in different ways. In fact, + /// there is no bound on the set of different instantiations one can encounter with the recursive uses + /// of the datatypes. Rather than keeping track of type instantiations in (some variation of) + /// visitedDatatypes, the type arguments passed to a datatype are checked separately. If the datatype + /// uses all the type parameters it declares, then this will have the same effect. During the second + /// phase, formal type parameters (which necessarily are ones declared in datatypes) are ignored. + /// + public abstract bool ComputeMayInvolveReferences(ISet /*?*/ visitedDatatypes); + + /// + /// Returns true if it is known how to meaningfully compare the type's inhabitants. + /// + public bool IsOrdered { + get { + var ct = NormalizeExpand(); + return !ct.IsTypeParameter && !ct.IsOpaqueType && !ct.IsInternalTypeSynonym && !ct.IsCoDatatype && !ct.IsArrowType && !ct.IsIMapType && !ct.IsISetType; + } + } + + /// + /// Returns "true" if: Given a value of type "this", can we determine at run time if the + /// value is a member of type "target"? + /// + public bool IsTestableToBe(Type target) { + Contract.Requires(target != null); + + // First up, we know how to check for null, so let's expand "target" and "source" + // past any type synonyms and also past any (built-in) non-null constraint. + var source = this.NormalizeExpandKeepConstraints(); + if (source is UserDefinedType && ((UserDefinedType)source).ResolvedClass is NonNullTypeDecl) { + source = source.NormalizeExpand(); // also lop off non-null constraint + } + target = target.NormalizeExpandKeepConstraints(); + if (target is UserDefinedType && ((UserDefinedType)target).ResolvedClass is NonNullTypeDecl) { + target = target.NormalizeExpand(); // also lop off non-null constraint + } + + if (source.IsSubtypeOf(target, false, true)) { + // Every value of "source" (except possibly "null") is also a member of type "target", + // so no run-time test is needed (except possibly a null check). + return true; +#if SOON // include in a coming PR that sorts this one in the compilers + } else if (target is UserDefinedType udt && (udt.ResolvedClass is SubsetTypeDecl || udt.ResolvedClass is NewtypeDecl)) { + // The type of the bound variable has a constraint. Such a constraint is a ghost expression, so it cannot + // (in general) by checked at run time. (A possible enhancement here would be to look at the type constraint + // to if it is compilable after all.) + var constraints = target.GetTypeConstraints(); + return false; +#endif + } else if (target.TypeArgs.Count == 0) { + // No type parameters. So, we just need to check the run-time class/interface type. + return true; + } else { + // We give up. + return false; + } + } + + /// + /// Returns "true" iff "sub" is a subtype of "super". + /// Expects that neither "super" nor "sub" is an unresolved proxy. + /// + public static bool IsSupertype(Type super, Type sub) { + Contract.Requires(super != null); + Contract.Requires(sub != null); + return sub.IsSubtypeOf(super, false, false); + } + + /// + /// Expects that "type" has already been normalized. + /// + public static List GetPolarities(Type type) { + Contract.Requires(type != null); + if (type is BasicType || type is ArtificialType) { + // there are no type parameters + return new List(); + } else if (type is MapType) { + return new List { TypeParameter.TPVariance.Co, TypeParameter.TPVariance.Co }; + } else if (type is CollectionType) { + return new List { TypeParameter.TPVariance.Co }; + } else { + var udf = (UserDefinedType)type; + if (udf.TypeArgs.Count == 0) { + return new List(); + } + // look up the declaration of the formal type parameters + var cl = udf.ResolvedClass; + return cl.TypeArgs.ConvertAll(tp => tp.Variance); + } + } + + public static bool FromSameHead_Subtype(Type t, Type u, BuiltIns builtIns, out Type a, out Type b) { + Contract.Requires(t != null); + Contract.Requires(u != null); + Contract.Requires(builtIns != null); + if (FromSameHead(t, u, out a, out b)) { + return true; + } + t = t.NormalizeExpand(); + u = u.NormalizeExpand(); + if (t.IsRefType && u.IsRefType) { + if (t.IsObjectQ) { + a = b = t; + return true; + } else if (u.IsObjectQ) { + a = b = u; + return true; + } + var tt = ((UserDefinedType)t).ResolvedClass as ClassDecl; + var uu = ((UserDefinedType)u).ResolvedClass as ClassDecl; + if (uu.HeadDerivesFrom(tt)) { + a = b = t; + return true; + } else if (tt.HeadDerivesFrom(uu)) { + a = b = u; + return true; + } + } + return false; + } + + public static bool FromSameHead(Type t, Type u, out Type a, out Type b) { + a = t; + b = u; + var towerA = GetTowerOfSubsetTypes(a); + var towerB = GetTowerOfSubsetTypes(b); + for (var n = Math.Min(towerA.Count, towerB.Count); 0 <= --n;) { + a = towerA[n]; + b = towerB[n]; + if (SameHead(a, b)) { + return true; + } + } + return false; + } + + /// + /// Returns true if t and u have the same head type. + /// It is assumed that t and u have been normalized and expanded by the caller, according + /// to its purposes. + /// The value of "allowNonNull" matters only if both "t" and "u" denote reference types. + /// If "t" is a non-null reference type "T" or a possibly-null type "T?" + /// and "u" is a non-null reference type "U" or a possibly-null type "U?", then + /// SameHead returns: + /// !allowNonNull allowNonNull + /// T? U? true true + /// T? U false true + /// T U? false false + /// T U true true + /// + public static bool SameHead(Type t, Type u) { + Contract.Requires(t != null); + Contract.Requires(u != null); + if (t is TypeProxy) { + return t == u; + } else if (t.TypeArgs.Count == 0) { + return Equal_Improved(t, u); + } else if (t is SetType) { + return u is SetType && t.IsISetType == u.IsISetType; + } else if (t is SeqType) { + return u is SeqType; + } else if (t is MultiSetType) { + return u is MultiSetType; + } else if (t is MapType) { + return u is MapType && t.IsIMapType == u.IsIMapType; + } else { + var udtT = (UserDefinedType)t; + var udtU = u as UserDefinedType; + return udtU != null && udtT.ResolvedClass == udtU.ResolvedClass; + } + } + + /// + /// Returns "true" iff the head symbols of "sub" can be a subtype of the head symbol of "super". + /// Expects that neither "super" nor "sub" is an unresolved proxy type (but their type arguments are + /// allowed to be, since this method does not inspect the type arguments). + /// + public static bool IsHeadSupertypeOf(Type super, Type sub) { + Contract.Requires(super != null); + Contract.Requires(sub != null); + super = super.NormalizeExpandKeepConstraints(); // expand type synonyms + var origSub = sub; + sub = sub.NormalizeExpand(); // expand type synonyms AND constraints + if (super is TypeProxy) { + return super == sub; + } else if (super is BoolType) { + return sub is BoolType; + } else if (super is CharType) { + return sub is CharType; + } else if (super is IntType) { + return sub is IntType; + } else if (super is RealType) { + return sub is RealType; + } else if (super is BitvectorType) { + var bitvectorSuper = (BitvectorType)super; + var bitvectorSub = sub as BitvectorType; + return bitvectorSub != null && bitvectorSuper.Width == bitvectorSub.Width; + } else if (super is IntVarietiesSupertype) { + while (sub.AsNewtype != null) { + sub = sub.AsNewtype.BaseType.NormalizeExpand(); + } + return sub.IsIntegerType || sub is BitvectorType || sub is BigOrdinalType; + } else if (super is RealVarietiesSupertype) { + while (sub.AsNewtype != null) { + sub = sub.AsNewtype.BaseType.NormalizeExpand(); + } + return sub is RealType; + } else if (super is BigOrdinalType) { + return sub is BigOrdinalType; + } else if (super is SetType) { + return sub is SetType && (super.IsISetType || !sub.IsISetType); + } else if (super is SeqType) { + return sub is SeqType; + } else if (super is MultiSetType) { + return sub is MultiSetType; + } else if (super is MapType) { + return sub is MapType && (super.IsIMapType || !sub.IsIMapType); + } else if (super is ArrowType) { + var asuper = (ArrowType)super; + var asub = sub as ArrowType; + return asub != null && asuper.Arity == asub.Arity; + } else if (super.IsObjectQ) { + var clSub = sub as UserDefinedType; + return sub.IsObjectQ || (clSub != null && clSub.ResolvedClass is ClassDecl); + } else if (super is UserDefinedType) { + var udtSuper = (UserDefinedType)super; + Contract.Assert(udtSuper.ResolvedClass != null); + if (udtSuper.ResolvedClass is TypeParameter) { + return udtSuper.ResolvedClass == sub.AsTypeParameter; + } else { + sub = origSub; // get back to the starting point + while (true) { + sub = sub.NormalizeExpandKeepConstraints(); // skip past proxies and type synonyms + var udtSub = sub as UserDefinedType; + if (udtSub == null) { + return false; + } else if (udtSuper.ResolvedClass == udtSub.ResolvedClass) { + return true; + } else if (udtSub.ResolvedClass is SubsetTypeDecl) { + sub = ((SubsetTypeDecl)udtSub.ResolvedClass).RhsWithArgument(udtSub.TypeArgs); + if (udtSub.ResolvedClass is NonNullTypeDecl && udtSuper.ResolvedClass is NonNullTypeDecl) { + // move "super" up the base-type chain, as was done with "sub", because non-nullness is essentially a co-variant type constructor + var possiblyNullSuper = ((SubsetTypeDecl)udtSuper.ResolvedClass).RhsWithArgument(udtSuper.TypeArgs); + udtSuper = (UserDefinedType)possiblyNullSuper; // applying .RhsWithArgument to a NonNullTypeDecl should always yield a UserDefinedType + if (udtSuper.IsObjectQ) { + return true; + } + } + } else if (udtSub.ResolvedClass is ClassDecl) { + var cl = (ClassDecl)udtSub.ResolvedClass; + return cl.HeadDerivesFrom(udtSuper.ResolvedClass); + } else { + return false; + } + } + } + } else { + Contract.Assert(false); // unexpected kind of type + return true; // to please the compiler + } + } + + /// + /// Returns "true" iff "a" and "b" denote the same type, expanding type synonyms (but treating types with + /// constraints as being separate types). + /// Expects that neither "a" nor "b" is or contains an unresolved proxy type. + /// + public static bool Equal_Improved(Type a, Type b) { + Contract.Requires(a != null); + Contract.Requires(b != null); + a = a.NormalizeExpandKeepConstraints(); // expand type synonyms + b = b.NormalizeExpandKeepConstraints(); // expand type synonyms + if (a is BoolType) { + return b is BoolType; + } else if (a is CharType) { + return b is CharType; + } else if (a is IntType) { + return b is IntType; + } else if (a is RealType) { + return b is RealType; + } else if (a is BitvectorType) { + var bitvectorSuper = (BitvectorType)a; + var bitvectorSub = b as BitvectorType; + return bitvectorSub != null && bitvectorSuper.Width == bitvectorSub.Width; + } else if (a is BigOrdinalType) { + return b is BigOrdinalType; + } else if (a is SetType) { + return b is SetType && Equal_Improved(a.TypeArgs[0], b.TypeArgs[0]) && (a.IsISetType == b.IsISetType); + } else if (a is SeqType) { + return b is SeqType && Equal_Improved(a.TypeArgs[0], b.TypeArgs[0]); + } else if (a is MultiSetType) { + return b is MultiSetType && Equal_Improved(a.TypeArgs[0], b.TypeArgs[0]); + } else if (a is MapType) { + return b is MapType && Equal_Improved(a.TypeArgs[0], b.TypeArgs[0]) && Equal_Improved(a.TypeArgs[1], b.TypeArgs[1]) && (a.IsIMapType == b.IsIMapType); + } else if (a is ArrowType) { + var asuper = (ArrowType)a; + var asub = b as ArrowType; + return asub != null && asuper.Arity == asub.Arity; + } else if (a is UserDefinedType) { + var udtA = (UserDefinedType)a; + Contract.Assert(udtA.ResolvedClass != null); + if (udtA.ResolvedClass is TypeParameter) { + Contract.Assert(udtA.TypeArgs.Count == 0); + return udtA.ResolvedClass == b.AsTypeParameter; + } else { + var udtB = b as UserDefinedType; + if (udtB == null) { + return false; + } else if (udtA.ResolvedClass != udtB.ResolvedClass) { + return false; + } else { + Contract.Assert(udtA.TypeArgs.Count == udtB.TypeArgs.Count); + for (int i = 0; i < udtA.TypeArgs.Count; i++) { + if (!Equal_Improved(udtA.TypeArgs[i], udtB.TypeArgs[i])) { + return false; + } + } + return true; + } + } + } else if (a is Resolver_IdentifierExpr.ResolverType_Module) { + return b is Resolver_IdentifierExpr.ResolverType_Module; + } else if (a is Resolver_IdentifierExpr.ResolverType_Type) { + return b is Resolver_IdentifierExpr.ResolverType_Type; + } else { + // this is an unexpected type; however, it may be that we get here during the resolution of an erroneous + // program, so we'll just return false + return false; + } + } + + public static Type HeadWithProxyArgs(Type t) { + Contract.Requires(t != null); + Contract.Requires(!(t is TypeProxy)); + if (t.TypeArgs.Count == 0) { + return t; + } else if (t is SetType) { + var s = (SetType)t; + return new SetType(s.Finite, new InferredTypeProxy()); + } else if (t is MultiSetType) { + return new MultiSetType(new InferredTypeProxy()); + } else if (t is SeqType) { + return new SeqType(new InferredTypeProxy()); + } else if (t is MapType) { + var s = (MapType)t; + return new MapType(s.Finite, new InferredTypeProxy(), new InferredTypeProxy()); + } else if (t is ArrowType) { + var s = (ArrowType)t; + var args = s.TypeArgs.ConvertAll(_ => (Type)new InferredTypeProxy()); + return new ArrowType(s.tok, (ArrowTypeDecl)s.ResolvedClass, args); + } else { + var s = (UserDefinedType)t; + var args = s.TypeArgs.ConvertAll(_ => (Type)new InferredTypeProxy()); + return new UserDefinedType(s.tok, s.Name, s.ResolvedClass, args); + } + } + + /// + /// Returns a stack of base types leading to "type". More precisely, of the tower returned, + /// tower[0] == type.NormalizeExpand() + /// tower.Last == type.NormalizeExpandKeepConstraints() + /// In between, for consecutive indices i and i+1: + /// tower[i] is the base type (that is, .Rhs) of the subset type tower[i+1] + /// The tower thus has the property that: + /// tower[0] is not a UserDefinedType with .ResolvedClass being a SubsetTypeDecl, + /// but all other tower[i] (for i > 0) are. + /// + public static List GetTowerOfSubsetTypes(Type type) { + Contract.Requires(type != null); + type = type.NormalizeExpandKeepConstraints(); + List tower; + if (type is UserDefinedType { ResolvedClass: SubsetTypeDecl sst }) { + var parent = sst.RhsWithArgument(type.TypeArgs); + tower = GetTowerOfSubsetTypes(parent); + } else { + tower = new List(); + } + tower.Add(type); + return tower; + } + + /// + /// For each i, computes some combination of a[i] and b[i], according to direction[i]. + /// For a negative direction (Contra), computes Join(a[i], b[i]), provided this join exists. + /// For a zero direction (Inv), uses a[i], provided a[i] and b[i] are equal. + /// For a positive direction (Co), computes Meet(a[i], b[i]), provided this meet exists. + /// Returns null if any operation fails. + /// + public static List ComputeExtrema(List directions, List a, List b, BuiltIns builtIns) { + Contract.Requires(directions != null); + Contract.Requires(a != null); + Contract.Requires(b != null); + Contract.Requires(directions.Count == a.Count); + Contract.Requires(directions.Count == b.Count); + Contract.Requires(builtIns != null); + var n = directions.Count; + var r = new List(n); + for (int i = 0; i < n; i++) { + if (a[i].Normalize() is TypeProxy) { + r.Add(b[i]); + } else if (b[i].Normalize() is TypeProxy) { + r.Add(a[i]); + } else if (directions[i] == TypeParameter.TPVariance.Non) { + if (a[i].Equals(b[i])) { + r.Add(a[i]); + } else { + return null; + } + } else { + var t = directions[i] == TypeParameter.TPVariance.Contra ? Join(a[i], b[i], builtIns) : Meet(a[i], b[i], builtIns); + if (t == null) { + return null; + } + r.Add(t); + } + } + return r; + } + + /// + /// Does a best-effort to compute the join of "a" and "b", returning "null" if not successful. + /// + /// Since some type parameters may still be proxies, it could be that the returned type is not + /// really a join, so the caller should set up additional constraints that the result is + /// assignable to both a and b. + /// + public static Type Join(Type a, Type b, BuiltIns builtIns) { + Contract.Requires(a != null); + Contract.Requires(b != null); + Contract.Requires(builtIns != null); + var j = JoinX(a, b, builtIns); + if (DafnyOptions.O.TypeInferenceDebug) { + Console.WriteLine("DEBUG: Join( {0}, {1} ) = {2}", a, b, j); + } + return j; + } + public static Type JoinX(Type a, Type b, BuiltIns builtIns) { + Contract.Requires(a != null); + Contract.Requires(b != null); + Contract.Requires(builtIns != null); + + // As a special-case optimization, check for equality here, which will better preserve un-expanded type synonyms + if (a.Equals(b, true)) { + return a; + } + + // Before we do anything else, make a note of whether or not both "a" and "b" are non-null types. + var abNonNullTypes = a.IsNonNullRefType && b.IsNonNullRefType; + + var towerA = GetTowerOfSubsetTypes(a); + var towerB = GetTowerOfSubsetTypes(b); + for (var n = Math.Min(towerA.Count, towerB.Count); 1 <= --n;) { + a = towerA[n]; + b = towerB[n]; + var udtA = (UserDefinedType)a; + var udtB = (UserDefinedType)b; + if (udtA.ResolvedClass == udtB.ResolvedClass) { + // We have two subset types with equal heads + if (a.Equals(b)) { // optimization for a special case, which applies for example when there are no arguments or when the types happen to be the same + return a; + } + Contract.Assert(a.TypeArgs.Count == b.TypeArgs.Count); + var directions = udtA.ResolvedClass.TypeArgs.ConvertAll(tp => TypeParameter.Negate(tp.Variance)); + var typeArgs = ComputeExtrema(directions, a.TypeArgs, b.TypeArgs, builtIns); + if (typeArgs == null) { + return null; + } + return new UserDefinedType(udtA.tok, udtA.Name, udtA.ResolvedClass, typeArgs); + } + } + // We exhausted all possibilities of subset types being equal, so use the base-most types. + a = towerA[0]; + b = towerB[0]; + + if (a is IntVarietiesSupertype) { + return b is IntVarietiesSupertype || b.IsNumericBased(NumericPersuasion.Int) || b.IsBigOrdinalType || b.IsBitVectorType ? b : null; + } else if (b is IntVarietiesSupertype) { + return a.IsNumericBased(NumericPersuasion.Int) || a.IsBigOrdinalType || a.IsBitVectorType ? a : null; + } else if (a.IsBoolType || a.IsCharType || a.IsBitVectorType || a.IsBigOrdinalType || a.IsTypeParameter || a.IsInternalTypeSynonym || a is TypeProxy) { + return a.Equals(b) ? a : null; + } else if (a is RealVarietiesSupertype) { + return b is RealVarietiesSupertype || b.IsNumericBased(NumericPersuasion.Real) ? b : null; + } else if (b is RealVarietiesSupertype) { + return a.IsNumericBased(NumericPersuasion.Real) ? a : null; + } else if (a.IsNumericBased()) { + // Note, for join, we choose not to step down to IntVarietiesSupertype or RealVarietiesSupertype + return a.Equals(b) ? a : null; + } else if (a.IsBitVectorType) { + return a.Equals(b) ? a : null; + } else if (a is SetType) { + var aa = (SetType)a; + var bb = b as SetType; + if (bb == null || aa.Finite != bb.Finite) { + return null; + } + // sets are co-variant in their argument type + var typeArg = Join(a.TypeArgs[0], b.TypeArgs[0], builtIns); + return typeArg == null ? null : new SetType(aa.Finite, typeArg); + } else if (a is MultiSetType) { + var aa = (MultiSetType)a; + var bb = b as MultiSetType; + if (bb == null) { + return null; + } + // multisets are co-variant in their argument type + var typeArg = Join(a.TypeArgs[0], b.TypeArgs[0], builtIns); + return typeArg == null ? null : new MultiSetType(typeArg); + } else if (a is SeqType) { + var aa = (SeqType)a; + var bb = b as SeqType; + if (bb == null) { + return null; + } + // sequences are co-variant in their argument type + var typeArg = Join(a.TypeArgs[0], b.TypeArgs[0], builtIns); + return typeArg == null ? null : new SeqType(typeArg); + } else if (a is MapType) { + var aa = (MapType)a; + var bb = b as MapType; + if (bb == null || aa.Finite != bb.Finite) { + return null; + } + // maps are co-variant in both argument types + var typeArgDomain = Join(a.TypeArgs[0], b.TypeArgs[0], builtIns); + var typeArgRange = Join(a.TypeArgs[1], b.TypeArgs[1], builtIns); + return typeArgDomain == null || typeArgRange == null ? null : new MapType(aa.Finite, typeArgDomain, typeArgRange); + } else if (a.IsDatatype) { + var aa = a.AsDatatype; + if (aa != b.AsDatatype) { + return null; + } + if (a.Equals(b)) { // optimization for a special case, which applies for example when there are no arguments or when the types happen to be the same + return a; + } + Contract.Assert(a.TypeArgs.Count == b.TypeArgs.Count); + var directions = aa.TypeArgs.ConvertAll(tp => TypeParameter.Negate(tp.Variance)); + var typeArgs = ComputeExtrema(directions, a.TypeArgs, b.TypeArgs, builtIns); + if (typeArgs == null) { + return null; + } + var udt = (UserDefinedType)a; + return new UserDefinedType(udt.tok, udt.Name, aa, typeArgs); + } else if (a.AsArrowType != null) { + var aa = a.AsArrowType; + var bb = b.AsArrowType; + if (bb == null || aa.Arity != bb.Arity) { + return null; + } + int arity = aa.Arity; + Contract.Assert(a.TypeArgs.Count == arity + 1); + Contract.Assert(b.TypeArgs.Count == arity + 1); + Contract.Assert(((ArrowType)a).ResolvedClass == ((ArrowType)b).ResolvedClass); + var directions = new List(); + for (int i = 0; i < arity; i++) { + directions.Add(TypeParameter.Negate(TypeParameter.TPVariance.Contra)); // arrow types are contra-variant in the argument types, so compute joins of these + } + directions.Add(TypeParameter.Negate(TypeParameter.TPVariance.Co)); // arrow types are co-variant in the result type, so compute the meet of these + var typeArgs = ComputeExtrema(directions, a.TypeArgs, b.TypeArgs, builtIns); + if (typeArgs == null) { + return null; + } + var arr = (ArrowType)aa; + return new ArrowType(arr.tok, (ArrowTypeDecl)arr.ResolvedClass, typeArgs); + } else if (b.IsObjectQ) { + var udtB = (UserDefinedType)b; + return !a.IsRefType ? null : abNonNullTypes ? UserDefinedType.CreateNonNullType(udtB) : udtB; + } else if (a.IsObjectQ) { + var udtA = (UserDefinedType)a; + return !b.IsRefType ? null : abNonNullTypes ? UserDefinedType.CreateNonNullType(udtA) : udtA; + } else { + // "a" is a class, trait, or opaque type + var aa = ((UserDefinedType)a).ResolvedClass; + Contract.Assert(aa != null); + if (!(b is UserDefinedType)) { + return null; + } + var bb = ((UserDefinedType)b).ResolvedClass; + if (a.Equals(b)) { // optimization for a special case, which applies for example when there are no arguments or when the types happen to be the same + return a; + } else if (aa == bb) { + Contract.Assert(a.TypeArgs.Count == b.TypeArgs.Count); + var directions = aa.TypeArgs.ConvertAll(tp => TypeParameter.Negate(tp.Variance)); + var typeArgs = ComputeExtrema(directions, a.TypeArgs, b.TypeArgs, builtIns); + if (typeArgs == null) { + return null; + } + var udt = (UserDefinedType)a; + var xx = new UserDefinedType(udt.tok, udt.Name, aa, typeArgs); + return abNonNullTypes ? UserDefinedType.CreateNonNullType(xx) : xx; + } else if (aa is ClassDecl && bb is ClassDecl) { + var A = (ClassDecl)aa; + var B = (ClassDecl)bb; + if (A.HeadDerivesFrom(B)) { + var udtB = (UserDefinedType)b; + return abNonNullTypes ? UserDefinedType.CreateNonNullType(udtB) : udtB; + } else if (B.HeadDerivesFrom(A)) { + var udtA = (UserDefinedType)a; + return abNonNullTypes ? UserDefinedType.CreateNonNullType(udtA) : udtA; + } + // A and B are classes or traits. They always have object as a common supertype, but they may also both be extending some other + // trait. If such a trait is unique, pick it. (Unfortunately, this makes the join operation not associative.) + var commonTraits = TopLevelDeclWithMembers.CommonTraits(A, B); + if (commonTraits.Count == 1) { + var typeMap = Resolver.TypeSubstitutionMap(A.TypeArgs, a.TypeArgs); + var r = (UserDefinedType)Resolver.SubstType(commonTraits[0], typeMap); + return abNonNullTypes ? UserDefinedType.CreateNonNullType(r) : r; + } else { + // the unfortunate part is when commonTraits.Count > 1 here :( + return abNonNullTypes ? UserDefinedType.CreateNonNullType(builtIns.ObjectQ()) : builtIns.ObjectQ(); + } + } else { + return null; + } + } + } + + /// + /// Does a best-effort to compute the meet of "a" and "b", returning "null" if not successful. + /// + /// Since some type parameters may still be proxies, it could be that the returned type is not + /// really a meet, so the caller should set up additional constraints that the result is + /// assignable to both a and b. + /// + public static Type Meet(Type a, Type b, BuiltIns builtIns) { + Contract.Requires(a != null); + Contract.Requires(b != null); + Contract.Requires(builtIns != null); + a = a.NormalizeExpandKeepConstraints(); + b = b.NormalizeExpandKeepConstraints(); + + var joinNeedsNonNullConstraint = false; + Type j; + if (a is UserDefinedType { ResolvedClass: NonNullTypeDecl aClass }) { + joinNeedsNonNullConstraint = true; + j = MeetX(aClass.RhsWithArgument(a.TypeArgs), b, builtIns); + } else if (b is UserDefinedType { ResolvedClass: NonNullTypeDecl bClass }) { + joinNeedsNonNullConstraint = true; + j = MeetX(a, bClass.RhsWithArgument(b.TypeArgs), builtIns); + } else { + j = MeetX(a, b, builtIns); + } + if (j != null && joinNeedsNonNullConstraint && !j.IsNonNullRefType) { + // try to make j into a non-null type; if that's not possible, then there is no meet + var udt = j as UserDefinedType; + if (udt != null && udt.ResolvedClass is ClassDecl) { + // add the non-null constraint back in + j = UserDefinedType.CreateNonNullType(udt); + } else { + // the original a and b have no meet + j = null; + } + } + if (DafnyOptions.O.TypeInferenceDebug) { + Console.WriteLine("DEBUG: Meet( {0}, {1} ) = {2}", a, b, j); + } + return j; + } + public static Type MeetX(Type a, Type b, BuiltIns builtIns) { + Contract.Requires(a != null); + Contract.Requires(b != null); + Contract.Requires(builtIns != null); + + a = a.NormalizeExpandKeepConstraints(); + b = b.NormalizeExpandKeepConstraints(); + if (a is IntVarietiesSupertype) { + return b is IntVarietiesSupertype || b.IsNumericBased(NumericPersuasion.Int) || b.IsBigOrdinalType || b.IsBitVectorType ? b : null; + } else if (b is IntVarietiesSupertype) { + return a.IsNumericBased(NumericPersuasion.Int) || a.IsBigOrdinalType || a.IsBitVectorType ? a : null; + } else if (a is RealVarietiesSupertype) { + return b is RealVarietiesSupertype || b.IsNumericBased(NumericPersuasion.Real) ? b : null; + } else if (b is RealVarietiesSupertype) { + return a.IsNumericBased(NumericPersuasion.Real) ? a : null; + } + + var towerA = GetTowerOfSubsetTypes(a); + var towerB = GetTowerOfSubsetTypes(b); + if (towerB.Count < towerA.Count) { + // make A be the shorter tower + var tmp0 = a; a = b; b = tmp0; + var tmp1 = towerA; towerA = towerB; towerB = tmp1; + } + var n = towerA.Count; + Contract.Assert(1 <= n); // guaranteed by GetTowerOfSubsetTypes + if (towerA.Count < towerB.Count) { + // B is strictly taller. The meet exists only if towerA[n-1] is a supertype of towerB[n-1], and + // then the meet is "b". + return Type.IsSupertype(towerA[n - 1], towerB[n - 1]) ? b : null; + } + Contract.Assert(towerA.Count == towerB.Count); + a = towerA[n - 1]; + b = towerB[n - 1]; + if (2 <= n) { + var udtA = (UserDefinedType)a; + var udtB = (UserDefinedType)b; + if (udtA.ResolvedClass == udtB.ResolvedClass) { + // We have two subset types with equal heads + if (a.Equals(b)) { // optimization for a special case, which applies for example when there are no arguments or when the types happen to be the same + return a; + } + Contract.Assert(a.TypeArgs.Count == b.TypeArgs.Count); + var directions = udtA.ResolvedClass.TypeArgs.ConvertAll(tp => tp.Variance); + var typeArgs = ComputeExtrema(directions, a.TypeArgs, b.TypeArgs, builtIns); + if (typeArgs == null) { + return null; + } + return new UserDefinedType(udtA.tok, udtA.Name, udtA.ResolvedClass, typeArgs); + } else { + // The two subset types do not have the same head, so there is no meet + return null; + } + } + Contract.Assert(towerA.Count == 1 && towerB.Count == 1); + + if (a.IsBoolType || a.IsCharType || a.IsNumericBased() || a.IsBitVectorType || a.IsBigOrdinalType || a.IsTypeParameter || a.IsInternalTypeSynonym || a is TypeProxy) { + return a.Equals(b) ? a : null; + } else if (a is SetType) { + var aa = (SetType)a; + var bb = b as SetType; + if (bb == null || aa.Finite != bb.Finite) { + return null; + } + // sets are co-variant in their argument type + var typeArg = Meet(a.TypeArgs[0], b.TypeArgs[0], builtIns); + return typeArg == null ? null : new SetType(aa.Finite, typeArg); + } else if (a is MultiSetType) { + var aa = (MultiSetType)a; + var bb = b as MultiSetType; + if (bb == null) { + return null; + } + // multisets are co-variant in their argument type + var typeArg = Meet(a.TypeArgs[0], b.TypeArgs[0], builtIns); + return typeArg == null ? null : new MultiSetType(typeArg); + } else if (a is SeqType) { + var aa = (SeqType)a; + var bb = b as SeqType; + if (bb == null) { + return null; + } + // sequences are co-variant in their argument type + var typeArg = Meet(a.TypeArgs[0], b.TypeArgs[0], builtIns); + return typeArg == null ? null : new SeqType(typeArg); + } else if (a is MapType) { + var aa = (MapType)a; + var bb = b as MapType; + if (bb == null || aa.Finite != bb.Finite) { + return null; + } + // maps are co-variant in both argument types + var typeArgDomain = Meet(a.TypeArgs[0], b.TypeArgs[0], builtIns); + var typeArgRange = Meet(a.TypeArgs[1], b.TypeArgs[1], builtIns); + return typeArgDomain == null || typeArgRange == null ? null : new MapType(aa.Finite, typeArgDomain, typeArgRange); + } else if (a.IsDatatype) { + var aa = a.AsDatatype; + if (aa != b.AsDatatype) { + return null; + } + if (a.Equals(b)) { // optimization for a special case, which applies for example when there are no arguments or when the types happen to be the same + return a; + } + Contract.Assert(a.TypeArgs.Count == b.TypeArgs.Count); + var directions = aa.TypeArgs.ConvertAll(tp => tp.Variance); + var typeArgs = ComputeExtrema(directions, a.TypeArgs, b.TypeArgs, builtIns); + if (typeArgs == null) { + return null; + } + var udt = (UserDefinedType)a; + return new UserDefinedType(udt.tok, udt.Name, aa, typeArgs); + } else if (a.AsArrowType != null) { + var aa = a.AsArrowType; + var bb = b.AsArrowType; + if (bb == null || aa.Arity != bb.Arity) { + return null; + } + int arity = aa.Arity; + Contract.Assert(a.TypeArgs.Count == arity + 1); + Contract.Assert(b.TypeArgs.Count == arity + 1); + Contract.Assert(((ArrowType)a).ResolvedClass == ((ArrowType)b).ResolvedClass); + var directions = new List(); + for (int i = 0; i < arity; i++) { + directions.Add(TypeParameter.TPVariance.Contra); // arrow types are contra-variant in the argument types, so compute joins of these + } + directions.Add(TypeParameter.TPVariance.Co); // arrow types are co-variant in the result type, so compute the meet of these + var typeArgs = ComputeExtrema(directions, a.TypeArgs, b.TypeArgs, builtIns); + if (typeArgs == null) { + return null; + } + var arr = (ArrowType)aa; + return new ArrowType(arr.tok, (ArrowTypeDecl)arr.ResolvedClass, typeArgs); + } else if (b.IsObjectQ) { + return a.IsRefType ? a : null; + } else if (a.IsObjectQ) { + return b.IsRefType ? b : null; + } else { + // "a" is a class, trait, or opaque type + var aa = ((UserDefinedType)a).ResolvedClass; + Contract.Assert(aa != null); + if (!(b is UserDefinedType)) { + return null; + } + var bb = ((UserDefinedType)b).ResolvedClass; + if (a.Equals(b)) { // optimization for a special case, which applies for example when there are no arguments or when the types happen to be the same + return a; + } else if (aa == bb) { + Contract.Assert(a.TypeArgs.Count == b.TypeArgs.Count); + var directions = aa.TypeArgs.ConvertAll(tp => tp.Variance); + var typeArgs = ComputeExtrema(directions, a.TypeArgs, b.TypeArgs, builtIns); + if (typeArgs == null) { + return null; + } + var udt = (UserDefinedType)a; + return new UserDefinedType(udt.tok, udt.Name, aa, typeArgs); + } else if (aa is ClassDecl && bb is ClassDecl) { + if (a.IsSubtypeOf(b, false, false)) { + return a; + } else if (b.IsSubtypeOf(a, false, false)) { + return b; + } else { + return null; + } + } else { + return null; + } + } + } + + public void ForeachTypeComponent(Action action) { + action(this); + TypeArgs.ForEach(x => x.ForeachTypeComponent(action)); + } + + public bool ContainsProxy(TypeProxy proxy) { + Contract.Requires(proxy != null && proxy.T == null); + if (this == proxy) { + return true; + } else { + return TypeArgs.Exists(t => t.ContainsProxy(proxy)); + } + } + + public virtual List ParentTypes() { + return new List(); + } + + /// + /// Return whether or not "this" is a subtype of "super". + /// If "ignoreTypeArguments" is "true", then proceed as if the type arguments were equal. + /// If "ignoreNullity" is "true", then the difference between a non-null reference type C + /// and the corresponding nullable reference type C? is ignored. + /// + public virtual bool IsSubtypeOf(Type super, bool ignoreTypeArguments, bool ignoreNullity) { + Contract.Requires(super != null); + + super = super.NormalizeExpandKeepConstraints(); + var sub = NormalizeExpandKeepConstraints(); + bool equivalentHeads = SameHead(sub, super); + if (!equivalentHeads && ignoreNullity) { + if (super is UserDefinedType a && sub is UserDefinedType b) { + var clA = (a.ResolvedClass as NonNullTypeDecl)?.Class ?? a.ResolvedClass; + var clB = (b.ResolvedClass as NonNullTypeDecl)?.Class ?? b.ResolvedClass; + equivalentHeads = clA == clB; + } + } + if (equivalentHeads) { + return ignoreTypeArguments || CompatibleTypeArgs(super, sub); + } + + return sub.ParentTypes().Any(parentType => parentType.IsSubtypeOf(super, ignoreTypeArguments, ignoreNullity)); + } + + public static bool CompatibleTypeArgs(Type super, Type sub) { + var polarities = GetPolarities(super); + Contract.Assert(polarities.Count == super.TypeArgs.Count && polarities.Count == sub.TypeArgs.Count); + var allGood = true; + for (int i = 0; allGood && i < polarities.Count; i++) { + switch (polarities[i]) { + case TypeParameter.TPVariance.Co: + allGood = IsSupertype(super.TypeArgs[i], sub.TypeArgs[i]); + break; + case TypeParameter.TPVariance.Contra: + allGood = IsSupertype(sub.TypeArgs[i], super.TypeArgs[i]); + break; + case TypeParameter.TPVariance.Non: + default: // "default" shouldn't ever happen + allGood = Equal_Improved(super.TypeArgs[i], sub.TypeArgs[i]); + break; + } + } + return allGood; + } + } + + /// + /// An ArtificialType is only used during type checking. It should never be assigned as the type of any expression. + /// It works as a supertype to numeric literals. For example, the literal 6 can be an "int", a "bv16", a + /// newtype based on integers, or an "ORDINAL". Type inference thus uses an "artificial" supertype of all of + /// these types as the type of literal 6, until a more precise (and non-artificial) type is inferred for it. + /// + public abstract class ArtificialType : Type { + public override bool ComputeMayInvolveReferences(ISet/*?*/ visitedDatatypes) { + // ArtificialType's are used only with numeric types. + return false; + } + } + /// + /// The type "IntVarietiesSupertype" is used to denote a decimal-less number type, namely an int-based type + /// or a bitvector type. + /// + public class IntVarietiesSupertype : ArtificialType { + [Pure] + public override string TypeName(ModuleDefinition context, bool parseAble) { + return "int"; + } + public override bool Equals(Type that, bool keepConstraints = false) { + return keepConstraints ? this.GetType() == that.GetType() : that is IntVarietiesSupertype; + } + } + public class RealVarietiesSupertype : ArtificialType { + [Pure] + public override string TypeName(ModuleDefinition context, bool parseAble) { + return "real"; + } + public override bool Equals(Type that, bool keepConstraints = false) { + return keepConstraints ? this.GetType() == that.GetType() : that is RealVarietiesSupertype; + } + } + + /// + /// A NonProxy type is a fully constrained type. It may contain members. + /// + public abstract class NonProxyType : Type { + } + + public abstract class BasicType : NonProxyType { + public override bool ComputeMayInvolveReferences(ISet/*?*/ visitedDatatypes) { + return false; + } + } + + public class BoolType : BasicType { + [Pure] + public override string TypeName(ModuleDefinition context, bool parseAble) { + return "bool"; + } + public override bool Equals(Type that, bool keepConstraints = false) { + return that.IsBoolType; + } + } + + public class CharType : BasicType { + public const char DefaultValue = 'D'; + public const string DefaultValueAsString = "'D'"; + [Pure] + public override string TypeName(ModuleDefinition context, bool parseAble) { + return "char"; + } + public override bool Equals(Type that, bool keepConstraints = false) { + return that.IsCharType; + } + } + + public class IntType : BasicType { + [Pure] + public override string TypeName(ModuleDefinition context, bool parseAble) { + return "int"; + } + public override bool Equals(Type that, bool keepConstraints = false) { + return that.NormalizeExpand(keepConstraints) is IntType; + } + public override bool IsSubtypeOf(Type super, bool ignoreTypeArguments, bool ignoreNullity) { + if (super is IntVarietiesSupertype) { + return true; + } + return base.IsSubtypeOf(super, ignoreTypeArguments, ignoreNullity); + } + } + + public class RealType : BasicType { + [Pure] + public override string TypeName(ModuleDefinition context, bool parseAble) { + return "real"; + } + public override bool Equals(Type that, bool keepConstraints = false) { + return that.NormalizeExpand(keepConstraints) is RealType; + } + public override bool IsSubtypeOf(Type super, bool ignoreTypeArguments, bool ignoreNullity) { + if (super is RealVarietiesSupertype) { + return true; + } + return base.IsSubtypeOf(super, ignoreTypeArguments, ignoreNullity); + } + } + + public class BigOrdinalType : BasicType { + [Pure] + public override string TypeName(ModuleDefinition context, bool parseAble) { + return "ORDINAL"; + } + public override bool Equals(Type that, bool keepConstraints = false) { + return that.NormalizeExpand(keepConstraints) is BigOrdinalType; + } + public override bool IsSubtypeOf(Type super, bool ignoreTypeArguments, bool ignoreNullity) { + if (super is IntVarietiesSupertype) { + return true; + } + return base.IsSubtypeOf(super, ignoreTypeArguments, ignoreNullity); + } + } + + public class BitvectorType : BasicType { + public readonly int Width; + public readonly NativeType NativeType; + public BitvectorType(int width) + : base() { + Contract.Requires(0 <= width); + Width = width; + foreach (var nativeType in Resolver.NativeTypes) { + if (DafnyOptions.O.Compiler.SupportedNativeTypes.Contains(nativeType.Name) && width <= nativeType.Bitwidth) { + NativeType = nativeType; + break; + } + } + } + + [Pure] + public override string TypeName(ModuleDefinition context, bool parseAble) { + return "bv" + Width; + } + public override bool Equals(Type that, bool keepConstraints = false) { + var bv = that.NormalizeExpand(keepConstraints) as BitvectorType; + return bv != null && bv.Width == Width; + } + public override bool IsSubtypeOf(Type super, bool ignoreTypeArguments, bool ignoreNullity) { + if (super is IntVarietiesSupertype) { + return true; + } + return base.IsSubtypeOf(super, ignoreTypeArguments, ignoreNullity); + } + } + + public class SelfType : NonProxyType { + public TypeParameter TypeArg; + public Type ResolvedType; + public SelfType() : base() { + TypeArg = new TypeParameter(Token.NoToken, "selfType", TypeParameter.TPVarianceSyntax.NonVariant_Strict); + } + + [Pure] + public override string TypeName(ModuleDefinition context, bool parseAble) { + return "selftype"; + } + public override bool Equals(Type that, bool keepConstraints = false) { + return that.NormalizeExpand(keepConstraints) is SelfType; + } + + public override bool ComputeMayInvolveReferences(ISet/*?*/ visitedDatatypes) { + // SelfType is used only with bitvector types + return false; + } + } + + public class ArrowType : UserDefinedType { + public List Args { + get { return TypeArgs.GetRange(0, Arity); } + } + + public Type Result { + get { return TypeArgs[Arity]; } + } + + public int Arity { + get { return TypeArgs.Count - 1; } + } + + /// + /// Constructs a(n unresolved) arrow type. + /// + public ArrowType(IToken tok, List args, Type result) + : base(tok, ArrowTypeName(args.Count), Util.Snoc(args, result)) { + Contract.Requires(tok != null); + Contract.Requires(args != null); + Contract.Requires(result != null); + } + /// + /// Constructs and returns a resolved arrow type. + /// + public ArrowType(IToken tok, ArrowTypeDecl atd, List typeArgsAndResult) + : base(tok, ArrowTypeName(atd.Arity), atd, typeArgsAndResult) { + Contract.Requires(tok != null); + Contract.Requires(atd != null); + Contract.Requires(typeArgsAndResult != null); + Contract.Requires(typeArgsAndResult.Count == atd.Arity + 1); + } + /// + /// Constructs and returns a resolved arrow type. + /// + public ArrowType(IToken tok, ArrowTypeDecl atd, List typeArgs, Type result) + : this(tok, atd, Util.Snoc(typeArgs, result)) { + Contract.Requires(tok != null); + Contract.Requires(atd != null); + Contract.Requires(typeArgs != null); + Contract.Requires(typeArgs.Count == atd.Arity); + Contract.Requires(result != null); + } + + public const string Arrow_FullCompileName = "Func"; // this is the same for all arities + + public static string ArrowTypeName(int arity) { + return "_#Func" + arity; + } + + [Pure] + public static bool IsArrowTypeName(string s) { + return s.StartsWith("_#Func"); + } + + public static string PartialArrowTypeName(int arity) { + return "_#PartialFunc" + arity; + } + + [Pure] + public static bool IsPartialArrowTypeName(string s) { + return s.StartsWith("_#PartialFunc"); + } + + public static string TotalArrowTypeName(int arity) { + return "_#TotalFunc" + arity; + } + + [Pure] + public static bool IsTotalArrowTypeName(string s) { + return s.StartsWith("_#TotalFunc"); + } + + public const string ANY_ARROW = "~>"; + public const string PARTIAL_ARROW = "-->"; + public const string TOTAL_ARROW = "->"; + + public override string TypeName(ModuleDefinition context, bool parseAble) { + return PrettyArrowTypeName(ANY_ARROW, Args, Result, context, parseAble); + } + + /// + /// Pretty prints an arrow type. If "result" is null, then all arguments, including the result type are expected in "typeArgs". + /// If "result" is non-null, then only the in-arguments are in "typeArgs". + /// + public static string PrettyArrowTypeName(string arrow, List typeArgs, Type result, ModuleDefinition context, bool parseAble) { + Contract.Requires(arrow != null); + Contract.Requires(typeArgs != null); + Contract.Requires(result != null || 1 <= typeArgs.Count); + + int arity = result == null ? typeArgs.Count - 1 : typeArgs.Count; + var domainNeedsParens = false; + if (arity != 1) { + // 0 or 2-or-more arguments: need parentheses + domainNeedsParens = true; + } else if (typeArgs[0].IsBuiltinArrowType) { + // arrows are right associative, so we need parentheses around the domain type + domainNeedsParens = true; + } else { + // if the domain type consists of a single tuple type, then an extra set of parentheses is needed + // Note, we do NOT call .AsDatatype or .AsIndDatatype here, because those calls will do a NormalizeExpand(). Instead, we do the check manually. + var udt = typeArgs[0].Normalize() as UserDefinedType; // note, we do Normalize(), not NormalizeExpand(), since the TypeName will use any synonym + if (udt != null && ((udt.FullName != null && BuiltIns.IsTupleTypeName(udt.FullName)) || udt.ResolvedClass is TupleTypeDecl)) { + domainNeedsParens = true; + } + } + string s = ""; + if (domainNeedsParens) { s += "("; } + s += Util.Comma(typeArgs.Take(arity), arg => arg.TypeName(context, parseAble)); + if (domainNeedsParens) { s += ")"; } + s += " " + arrow + " "; + s += (result ?? typeArgs.Last()).TypeName(context, parseAble); + return s; + } + + public override bool SupportsEquality { + get { + return false; + } + } + } + + public abstract class CollectionType : NonProxyType { + public abstract string CollectionTypeName { get; } + public override string TypeName(ModuleDefinition context, bool parseAble) { + Contract.Ensures(Contract.Result() != null); + var targs = HasTypeArg() ? this.TypeArgsToString(context, parseAble) : ""; + return CollectionTypeName + targs; + } + public Type Arg { + get { + Contract.Ensures(Contract.Result() != null); // this is true only after "arg" has really been set (i.e., it follows from the precondition) + Contract.Assume(arg != null); // This is really a precondition. Don't call Arg until "arg" has been set. + return arg; + } + } // denotes the Domain type for a Map + private Type arg; + // The following methods, HasTypeArg and SetTypeArg/SetTypeArgs, are to be called during resolution to make sure that "arg" becomes set. + public bool HasTypeArg() { + return arg != null; + } + public void SetTypeArg(Type arg) { + Contract.Requires(arg != null); + Contract.Requires(1 <= this.TypeArgs.Count); // this is actually an invariant of all collection types + Contract.Assume(this.arg == null); // Can only set it once. This is really a precondition. + this.arg = arg; + this.TypeArgs[0] = arg; + } + public virtual void SetTypeArgs(Type arg, Type other) { + Contract.Requires(arg != null); + Contract.Requires(other != null); + Contract.Requires(this.TypeArgs.Count == 2); + Contract.Assume(this.arg == null); // Can only set it once. This is really a precondition. + this.arg = arg; + this.TypeArgs[0] = arg; + this.TypeArgs[1] = other; + } + [ContractInvariantMethod] + void ObjectInvariant() { + // Contract.Invariant(Contract.ForAll(TypeArgs, tp => tp != null)); + // After resolution, the following is invariant: Contract.Invariant(Arg != null); + // However, it may not be true until then. + } + /// + /// This constructor is a collection types with 1 type argument + /// + protected CollectionType(Type arg) { + this.arg = arg; + this.TypeArgs = new List { arg }; + } + /// + /// This constructor is a collection types with 2 type arguments + /// + protected CollectionType(Type arg, Type other) { + this.arg = arg; + this.TypeArgs = new List { arg, other }; + } + + public override bool ComputeMayInvolveReferences(ISet visitedDatatypes) { + return Arg.ComputeMayInvolveReferences(visitedDatatypes); + } + } + + public class SetType : CollectionType { + private bool finite; + + public bool Finite { + get { return finite; } + set { finite = value; } + } + + public SetType(bool finite, Type arg) : base(arg) { + this.finite = finite; + } + public override string CollectionTypeName { get { return finite ? "set" : "iset"; } } + [Pure] + public override bool Equals(Type that, bool keepConstraints = false) { + var t = that.NormalizeExpand(keepConstraints) as SetType; + return t != null && Finite == t.Finite && Arg.Equals(t.Arg, keepConstraints); + } + public override bool SupportsEquality { + get { + // Sets always support equality, because there is a check that the set element type always does. + return true; + } + } + } + + public class MultiSetType : CollectionType { + public MultiSetType(Type arg) : base(arg) { + } + public override string CollectionTypeName { get { return "multiset"; } } + public override bool Equals(Type that, bool keepConstraints = false) { + var t = that.NormalizeExpand(keepConstraints) as MultiSetType; + return t != null && Arg.Equals(t.Arg, keepConstraints); + } + public override bool SupportsEquality { + get { + // Multisets always support equality, because there is a check that the set element type always does. + return true; + } + } + } + + public class SeqType : CollectionType { + public SeqType(Type arg) : base(arg) { + } + public override string CollectionTypeName { get { return "seq"; } } + public override bool Equals(Type that, bool keepConstraints = false) { + var t = that.NormalizeExpand(keepConstraints) as SeqType; + return t != null && Arg.Equals(t.Arg, keepConstraints); + } + public override bool SupportsEquality { + get { + // The sequence type supports equality if its element type does + return Arg.SupportsEquality; + } + } + } + public class MapType : CollectionType { + public bool Finite { + get { return finite; } + set { finite = value; } + } + private bool finite; + public Type Range { + get { return range; } + } + private Type range; + public override void SetTypeArgs(Type domain, Type range) { + base.SetTypeArgs(domain, range); + Contract.Assume(this.range == null); // Can only set once. This is really a precondition. + this.range = range; + } + public MapType(bool finite, Type domain, Type range) : base(domain, range) { + Contract.Requires((domain == null && range == null) || (domain != null && range != null)); + this.finite = finite; + this.range = range; + } + public Type Domain { + get { return Arg; } + } + public override string CollectionTypeName { get { return finite ? "map" : "imap"; } } + [Pure] + public override string TypeName(ModuleDefinition context, bool parseAble) { + Contract.Ensures(Contract.Result() != null); + var targs = HasTypeArg() ? this.TypeArgsToString(context, parseAble) : ""; + return CollectionTypeName + targs; + } + public override bool Equals(Type that, bool keepConstraints = false) { + var t = that.NormalizeExpand(keepConstraints) as MapType; + return t != null && Finite == t.Finite && Arg.Equals(t.Arg, keepConstraints) && Range.Equals(t.Range, keepConstraints); + } + public override bool SupportsEquality { + get { + // A map type supports equality if both its Keys type and Values type does. It is checked + // that the Keys type always supports equality, so we only need to check the Values type here. + return range.SupportsEquality; + } + } + public override bool ComputeMayInvolveReferences(ISet visitedDatatypes) { + return Domain.ComputeMayInvolveReferences(visitedDatatypes) || Range.ComputeMayInvolveReferences(visitedDatatypes); + } + } + + public class UserDefinedType : NonProxyType { + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(tok != null); + Contract.Invariant(Name != null); + Contract.Invariant(cce.NonNullElements(TypeArgs)); + Contract.Invariant(NamePath is NameSegment || NamePath is ExprDotName); + Contract.Invariant(!ArrowType.IsArrowTypeName(Name) || this is ArrowType); + } + + public readonly Expression NamePath; // either NameSegment or ExprDotName (with the inner expression satisfying this same constraint) + public readonly IToken tok; // token of the Name + public readonly string Name; + [Rep] + + public string FullName { + get { + if (ResolvedClass?.EnclosingModuleDefinition?.IsDefaultModule == false) { + return ResolvedClass.EnclosingModuleDefinition.Name + "." + Name; + } else { + return Name; + } + } + } + + string compileName; + public string CompileName => compileName ??= ResolvedClass.CompileName; + + public string FullCompanionCompileName { + get { + Contract.Requires(ResolvedClass is TraitDecl || (ResolvedClass is NonNullTypeDecl nntd && nntd.Class is TraitDecl)); + var m = ResolvedClass.EnclosingModuleDefinition; + var s = m.IsDefaultModule ? "" : m.CompileName + "."; + return s + "_Companion_" + ResolvedClass.CompileName; + } + } + + [FilledInDuringResolution] public TopLevelDecl ResolvedClass; // if Name denotes a class/datatype/iterator and TypeArgs match the type parameters of that class/datatype/iterator + + public UserDefinedType(IToken tok, string name, List optTypeArgs) + : this(tok, new NameSegment(tok, name, optTypeArgs)) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(optTypeArgs == null || optTypeArgs.Count > 0); // this is what it means to be syntactically optional + } + + public UserDefinedType(IToken tok, Expression namePath) { + Contract.Requires(tok != null); + Contract.Requires(namePath is NameSegment || namePath is ExprDotName); + this.tok = tok; + if (namePath is NameSegment) { + var n = (NameSegment)namePath; + this.Name = n.Name; + this.TypeArgs = n.OptTypeArguments; + } else { + var n = (ExprDotName)namePath; + this.Name = n.SuffixName; + this.TypeArgs = n.OptTypeArguments; + } + if (this.TypeArgs == null) { + this.TypeArgs = new List(); // TODO: is this really the thing to do? + } + this.NamePath = namePath; + } + + /// + /// Constructs a Type (in particular, a UserDefinedType) from a TopLevelDecl denoting a type declaration. If + /// the given declaration takes type parameters, these are filled as references to the formal type parameters + /// themselves. (Usually, this method is called when the type parameters in the result don't matter, other + /// than that they need to be filled in, so as to make a properly resolved UserDefinedType.) + /// If "typeArgs" is non-null, then its type parameters are used in constructing the returned type. + /// If "typeArgs" is null, then the formal type parameters of "cd" are used. + /// + public static UserDefinedType FromTopLevelDecl(IToken tok, TopLevelDecl cd, List typeArgs = null) { + Contract.Requires(tok != null); + Contract.Requires(cd != null); + Contract.Assert((cd is ArrowTypeDecl) == ArrowType.IsArrowTypeName(cd.Name)); + var args = (typeArgs ?? cd.TypeArgs).ConvertAll(tp => (Type)new UserDefinedType(tp)); + if (cd is ArrowTypeDecl) { + return new ArrowType(tok, (ArrowTypeDecl)cd, args); + } else if (cd is ClassDecl && !(cd is DefaultClassDecl)) { + return new UserDefinedType(tok, cd.Name + "?", cd, args); + } else { + return new UserDefinedType(tok, cd.Name, cd, args); + } + } + + public static UserDefinedType FromTopLevelDeclWithAllBooleanTypeParameters(TopLevelDecl cd) { + Contract.Requires(cd != null); + Contract.Requires(!(cd is ArrowTypeDecl)); + + var typeArgs = cd.TypeArgs.ConvertAll(tp => (Type)Type.Bool); + return new UserDefinedType(cd.tok, cd.Name, cd, typeArgs); + } + + /// + /// If "member" is non-null, then: + /// Return the upcast of "receiverType" that has base type "member.EnclosingClass". + /// Assumes that "receiverType" normalizes to a UserDefinedFunction with a .ResolveClass that is a subtype + /// of "member.EnclosingClass". + /// Otherwise: + /// Return "receiverType" (expanded). + /// + public static Type UpcastToMemberEnclosingType(Type receiverType, MemberDecl/*?*/ member) { + Contract.Requires(receiverType != null); + if (member != null && member.EnclosingClass != null && !(member.EnclosingClass is ValuetypeDecl)) { + return receiverType.AsParentType(member.EnclosingClass); + } + return receiverType.NormalizeExpandKeepConstraints(); + } + + /// + /// This constructor constructs a resolved class/datatype/iterator/subset-type/newtype type + /// + public UserDefinedType(IToken tok, string name, TopLevelDecl cd, [Captured] List typeArgs, Expression/*?*/ namePath = null) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(cd != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cd.TypeArgs.Count == typeArgs.Count); + Contract.Requires(namePath == null || namePath is NameSegment || namePath is ExprDotName); + // The following is almost a precondition. In a few places, the source program names a class, not a type, + // and in then name==cd.Name for a ClassDecl. + //Contract.Requires(!(cd is ClassDecl) || cd is DefaultClassDecl || cd is ArrowTypeDecl || name == cd.Name + "?"); + Contract.Requires(!(cd is ArrowTypeDecl) || name == cd.Name); + Contract.Requires(!(cd is DefaultClassDecl) || name == cd.Name); + this.tok = tok; + this.Name = name; + this.ResolvedClass = cd; + this.TypeArgs = typeArgs; + if (namePath == null) { + var ns = new NameSegment(tok, name, typeArgs.Count == 0 ? null : typeArgs); + var r = new Resolver_IdentifierExpr(tok, cd, typeArgs); + ns.ResolvedExpression = r; + ns.Type = r.Type; + this.NamePath = ns; + } else { + this.NamePath = namePath; + } + } + + public static UserDefinedType CreateNonNullType(UserDefinedType udtNullableType) { + Contract.Requires(udtNullableType != null); + Contract.Requires(udtNullableType.ResolvedClass is ClassDecl); + var cl = (ClassDecl)udtNullableType.ResolvedClass; + return new UserDefinedType(udtNullableType.tok, cl.NonNullTypeDecl.Name, cl.NonNullTypeDecl, udtNullableType.TypeArgs); + } + + public static UserDefinedType CreateNullableType(UserDefinedType udtNonNullType) { + Contract.Requires(udtNonNullType != null); + Contract.Requires(udtNonNullType.ResolvedClass is NonNullTypeDecl); + var nntd = (NonNullTypeDecl)udtNonNullType.ResolvedClass; + return new UserDefinedType(udtNonNullType.tok, nntd.Class.Name + "?", nntd.Class, udtNonNullType.TypeArgs); + } + + /// + /// This constructor constructs a resolved type parameter + /// + public UserDefinedType(TypeParameter tp) + : this(tp.tok, tp) { + Contract.Requires(tp != null); + } + + /// + /// This constructor constructs a resolved type parameter (but shouldn't be called if "tp" denotes + /// the .TheType of an opaque type -- use the (OpaqueType_AsParameter, OpaqueTypeDecl, List(Type)) + /// constructor for that). + /// + public UserDefinedType(IToken tok, TypeParameter tp) { + Contract.Requires(tok != null); + Contract.Requires(tp != null); + this.tok = tok; + this.Name = tp.Name; + this.TypeArgs = new List(); + this.ResolvedClass = tp; + var ns = new NameSegment(tok, tp.Name, null); + var r = new Resolver_IdentifierExpr(tok, tp); + ns.ResolvedExpression = r; + ns.Type = r.Type; + this.NamePath = ns; + } + + public override bool Equals(Type that, bool keepConstraints = false) { + var i = NormalizeExpand(keepConstraints); + if (i is UserDefinedType) { + var ii = (UserDefinedType)i; + var t = that.NormalizeExpand(keepConstraints) as UserDefinedType; + if (t == null || ii.ResolvedClass != t.ResolvedClass || ii.TypeArgs.Count != t.TypeArgs.Count) { + return false; + } else { + for (int j = 0; j < ii.TypeArgs.Count; j++) { + if (!ii.TypeArgs[j].Equals(t.TypeArgs[j], keepConstraints)) { + return false; + } + } + return true; + } + } else { + // TODO?: return i.Equals(that.NormalizeExpand()); + return i.Equals(that, keepConstraints); + } + } + + /// + /// If type denotes a resolved class type, then return that class type. + /// Otherwise, return null. + /// + public static UserDefinedType DenotesClass(Type type) { + Contract.Requires(type != null); + Contract.Ensures(Contract.Result() == null || Contract.Result().ResolvedClass is ClassDecl); + type = type.NormalizeExpand(); + UserDefinedType ct = type as UserDefinedType; + if (ct != null && ct.ResolvedClass is ClassDecl) { + return ct; + } else { + return null; + } + } + + public static Type ArrayElementType(Type type) { + Contract.Requires(type != null); + Contract.Requires(type.IsArrayType); + Contract.Ensures(Contract.Result() != null); + + UserDefinedType udt = DenotesClass(type); + Contract.Assert(udt != null); + Contract.Assert(udt.TypeArgs.Count == 1); // holds true of all array types + return udt.TypeArgs[0]; + } + + [Pure] + public override string TypeName(ModuleDefinition context, bool parseAble) { + Contract.Ensures(Contract.Result() != null); + if (BuiltIns.IsTupleTypeName(Name)) { + // Unfortunately, ResolveClass may be null, so Name is all we have. Reverse-engineer the string name. + IEnumerable argumentGhostness = BuiltIns.ArgumentGhostnessFromString(Name, TypeArgs.Count); + return "(" + Util.Comma(System.Linq.Enumerable.Zip(TypeArgs, argumentGhostness), + (ty_u) => Resolver.GhostPrefix(ty_u.Item2) + ty_u.Item1.TypeName(context, parseAble)) + ")"; + } else if (ArrowType.IsPartialArrowTypeName(Name)) { + return ArrowType.PrettyArrowTypeName(ArrowType.PARTIAL_ARROW, TypeArgs, null, context, parseAble); + } else if (ArrowType.IsTotalArrowTypeName(Name)) { + return ArrowType.PrettyArrowTypeName(ArrowType.TOTAL_ARROW, TypeArgs, null, context, parseAble); + } else { +#if TEST_TYPE_SYNONYM_TRANSPARENCY + if (Name == "type#synonym#transparency#test" && ResolvedClass is TypeSynonymDecl) { + return ((TypeSynonymDecl)ResolvedClass).Rhs.TypeName(context); + } +#endif + var s = Printer.ExprToString(NamePath); + if (ResolvedClass != null) { + var optionalTypeArgs = NamePath is NameSegment ? ((NameSegment)NamePath).OptTypeArguments : ((ExprDotName)NamePath).OptTypeArguments; + if (optionalTypeArgs == null && TypeArgs != null && TypeArgs.Count != 0) { + s += this.TypeArgsToString(context, parseAble); + } + } + return s; + } + } + + public override bool SupportsEquality { + get { + if (ResolvedClass is ClassDecl || ResolvedClass is NewtypeDecl) { + return ResolvedClass.IsRevealedInScope(Type.GetScope()); + } else if (ResolvedClass is CoDatatypeDecl) { + return false; + } else if (ResolvedClass is IndDatatypeDecl) { + var dt = (IndDatatypeDecl)ResolvedClass; + Contract.Assume(dt.EqualitySupport != IndDatatypeDecl.ES.NotYetComputed); + if (!dt.IsRevealedInScope(Type.GetScope())) { + return false; + } + if (dt.EqualitySupport == IndDatatypeDecl.ES.Never) { + return false; + } + Contract.Assert(dt.TypeArgs.Count == TypeArgs.Count); + var i = 0; + foreach (var tp in dt.TypeArgs) { + if (tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype && !TypeArgs[i].SupportsEquality) { + return false; + } + i++; + } + return true; + } else if (ResolvedClass is TypeSynonymDeclBase) { + var t = (TypeSynonymDeclBase)ResolvedClass; + if (t.SupportsEquality) { + return true; + } else if (t.IsRevealedInScope(Type.GetScope())) { + return t.RhsWithArgument(TypeArgs).SupportsEquality; + } else { + return false; + } + } else if (ResolvedClass is TypeParameter) { + return ((TypeParameter)ResolvedClass).SupportsEquality; + } else if (ResolvedClass is OpaqueTypeDecl) { + return ((OpaqueTypeDecl)ResolvedClass).SupportsEquality; + } + Contract.Assume(false); // the SupportsEquality getter requires the Type to have been successfully resolved + return true; + } + } + + public override bool ComputeMayInvolveReferences(ISet visitedDatatypes) { + if (ResolvedClass is ArrowTypeDecl) { + return TypeArgs.Any(ta => ta.ComputeMayInvolveReferences(visitedDatatypes)); + } else if (ResolvedClass is ClassDecl) { + return true; + } else if (ResolvedClass is NewtypeDecl) { + return false; + } else if (ResolvedClass is DatatypeDecl) { + // Datatype declarations do not support explicit (!new) annotations. Instead, whether or not + // a datatype involves references depends on the definition and parametrization of the type. + // See ComputeMayInvolveReferences in class Type for more information. + // In particular, if one of the datatype's constructors mentions a type that involves + // references, then so does the datatype. And if one of the datatype's type arguments involves + // references, then we consider the datatype to do so as well (without regard to whether or + // not the type parameter is actually used in the definition of the datatype). + var dt = (DatatypeDecl)ResolvedClass; + if (!dt.IsRevealedInScope(Type.GetScope())) { + // The type's definition is hidden from the current scope, so we + // have to assume the type may involve references. + return true; + } else if (TypeArgs.Any(ta => ta.ComputeMayInvolveReferences(visitedDatatypes))) { + return true; + } else if (visitedDatatypes != null && visitedDatatypes.Contains(dt)) { + // we're in the middle of looking through the types involved in dt's definition + return false; + } else { + visitedDatatypes ??= new HashSet(); + visitedDatatypes.Add(dt); + return dt.Ctors.Any(ctor => ctor.Formals.Any(f => f.Type.ComputeMayInvolveReferences(visitedDatatypes))); + } + } else if (ResolvedClass is TypeSynonymDeclBase) { + var t = (TypeSynonymDeclBase)ResolvedClass; + if (t.Characteristics.ContainsNoReferenceTypes) { + // There's an explicit "(!new)" annotation on the type. + return false; + } else if (t.IsRevealedInScope(Type.GetScope())) { + // The type's definition is available in the scope, so consult the RHS type + return t.RhsWithArgument(TypeArgs).ComputeMayInvolveReferences(visitedDatatypes); + } else { + // The type's definition is hidden from the current scope and there's no explicit "(!new)", so we + // have to assume the type may involve references. + return true; + } + } else if (ResolvedClass is TypeParameter typeParameter) { + if (visitedDatatypes != null) { + // Datatypes look at the type arguments passed in, so we ignore their formal type parameters. + // See comment above and in Type.ComputeMayInvolveReferences. + Contract.Assert(typeParameter.Parent is DatatypeDecl); + return false; + } else { + return !typeParameter.Characteristics.ContainsNoReferenceTypes; + } + } else if (ResolvedClass is OpaqueTypeDecl opaqueTypeDecl) { + return !opaqueTypeDecl.Characteristics.ContainsNoReferenceTypes; + } + Contract.Assume(false); // unexpected or not successfully resolved Type + return true; + } + + public override List ParentTypes() { + return ResolvedClass != null ? ResolvedClass.ParentTypes(TypeArgs) : base.ParentTypes(); + } + + public override bool IsSubtypeOf(Type super, bool ignoreTypeArguments, bool ignoreNullity) { + super = super.NormalizeExpandKeepConstraints(); + + // Specifically handle object as the implicit supertype of classes and traits. + // "object?" is handled by Builtins rather than the Type hierarchy, so unfortunately + // it can't be returned in ParentTypes(). + if (super.IsObjectQ) { + return IsRefType; + } else if (super.IsObject) { + return ignoreNullity ? IsRefType : IsNonNullRefType; + } + + return base.IsSubtypeOf(super, ignoreTypeArguments, ignoreNullity); + } + } + + public abstract class TypeProxy : Type { + [FilledInDuringResolution] public Type T; + public readonly List SupertypeConstraints = new List(); + public readonly List SubtypeConstraints = new List(); + public IEnumerable Supertypes { + get { + foreach (var c in SupertypeConstraints) { + if (c.KeepConstraints) { + yield return c.Super.NormalizeExpandKeepConstraints(); + } else { + yield return c.Super.NormalizeExpand(); + } + } + } + } + public IEnumerable SupertypesKeepConstraints { + get { + foreach (var c in SupertypeConstraints) { + yield return c.Super.NormalizeExpandKeepConstraints(); + } + } + } + public void AddSupertype(TypeConstraint c) { + Contract.Requires(c != null); + Contract.Requires(c.Sub == this); + SupertypeConstraints.Add(c); + } + public IEnumerable Subtypes { + get { + foreach (var c in SubtypeConstraints) { + if (c.KeepConstraints) { + yield return c.Sub.NormalizeExpandKeepConstraints(); + } else { + yield return c.Sub.NormalizeExpand(); + } + } + } + } + + public IEnumerable SubtypesKeepConstraints { + get { + foreach (var c in SubtypeConstraints) { + yield return c.Sub.NormalizeExpandKeepConstraints(); + } + } + } + + public IEnumerable SubtypesKeepConstraints_WithAssignable(List allXConstraints) { + Contract.Requires(allXConstraints != null); + foreach (var c in SubtypeConstraints) { + yield return c.Sub.NormalizeExpandKeepConstraints(); + } + foreach (var xc in allXConstraints) { + if (xc.ConstraintName == "Assignable") { + if (xc.Types[0].Normalize() == this) { + yield return xc.Types[1].NormalizeExpandKeepConstraints(); + } + } + } + } + + public void AddSubtype(TypeConstraint c) { + Contract.Requires(c != null); + Contract.Requires(c.Super == this); + SubtypeConstraints.Add(c); + } + + public enum Family { Unknown, Bool, Char, IntLike, RealLike, Ordinal, BitVector, ValueType, Ref, Opaque } + public Family family = Family.Unknown; + public static Family GetFamily(Type t) { + Contract.Ensures(Contract.Result() != Family.Unknown || t is TypeProxy || t is Resolver_IdentifierExpr.ResolverType); // return Unknown ==> t is TypeProxy || t is ResolverType + if (t.IsBoolType) { + return Family.Bool; + } else if (t.IsCharType) { + return Family.Char; + } else if (t.IsNumericBased(NumericPersuasion.Int) || t is IntVarietiesSupertype) { + return Family.IntLike; + } else if (t.IsNumericBased(NumericPersuasion.Real) || t is RealVarietiesSupertype) { + return Family.RealLike; + } else if (t.IsBigOrdinalType) { + return Family.Ordinal; + } else if (t.IsBitVectorType) { + return Family.BitVector; + } else if (t.AsCollectionType != null || t.AsArrowType != null || t.IsDatatype) { + return Family.ValueType; + } else if (t.IsRefType) { + return Family.Ref; + } else if (t.IsTypeParameter || t.IsOpaqueType || t.IsInternalTypeSynonym) { + return Family.Opaque; + } else if (t is TypeProxy) { + return ((TypeProxy)t).family; + } else { + return Family.Unknown; + } + } + + internal TypeProxy() { + } + +#if TI_DEBUG_PRINT + static int _id = 0; + int id = _id++; +#endif + [Pure] + public override string TypeName(ModuleDefinition context, bool parseAble) { + Contract.Ensures(Contract.Result() != null); +#if TI_DEBUG_PRINT + if (DafnyOptions.O.TypeInferenceDebug) { + return T == null ? "?" + id : T.TypeName(context); + } +#endif + return T == null ? "?" : T.TypeName(context, parseAble); + } + public override bool SupportsEquality { + get { + if (T != null) { + return T.SupportsEquality; + } else { + return base.SupportsEquality; + } + } + } + public override bool ComputeMayInvolveReferences(ISet visitedDatatypes) { + if (T != null) { + return T.ComputeMayInvolveReferences(visitedDatatypes); + } else { + return true; + } + } + public override bool Equals(Type that, bool keepConstraints = false) { + var i = NormalizeExpand(keepConstraints); + if (i is TypeProxy) { + var u = that.NormalizeExpand(keepConstraints) as TypeProxy; + return u != null && object.ReferenceEquals(i, u); + } else { + return i.Equals(that, keepConstraints); + } + } + + [Pure] + internal static bool IsSupertypeOfLiteral(Type t) { + Contract.Requires(t != null); + return t is ArtificialType; + } + internal Type InClusterOfArtificial(List allXConstraints) { + Contract.Requires(allXConstraints != null); + return InClusterOfArtificial_aux(new HashSet(), allXConstraints); + } + private Type InClusterOfArtificial_aux(ISet visitedProxies, List allXConstraints) { + Contract.Requires(visitedProxies != null); + Contract.Requires(allXConstraints != null); + if (visitedProxies.Contains(this)) { + return null; + } + visitedProxies.Add(this); + foreach (var c in SupertypeConstraints) { + var sup = c.Super.Normalize(); + if (sup is IntVarietiesSupertype) { + return Type.Int; + } else if (sup is RealVarietiesSupertype) { + return Type.Real; + } else if (sup is TypeProxy) { + var a = ((TypeProxy)sup).InClusterOfArtificial_aux(visitedProxies, allXConstraints); + if (a != null) { + return a; + } + } + } + foreach (var su in SubtypesKeepConstraints_WithAssignable(allXConstraints)) { + var pr = su as TypeProxy; + if (pr != null) { + var a = pr.InClusterOfArtificial_aux(visitedProxies, allXConstraints); + if (a != null) { + return a; + } + } + } + return null; + } + } + + /// + /// This proxy stands for any type. + /// + public class InferredTypeProxy : TypeProxy { + public bool KeepConstraints; + public InferredTypeProxy() : base() { + KeepConstraints = false; // whether the typeProxy should be inferred to base type or as subset type + } + } + + /// + /// This proxy stands for any type, but it originates from an instantiated type parameter. + /// + public class ParamTypeProxy : TypeProxy { + public TypeParameter orig; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(orig != null); + } + + public ParamTypeProxy(TypeParameter orig) { + Contract.Requires(orig != null); + this.orig = orig; + } + } + + // ------------------------------------------------------------------------------------------------------ + + /// + /// This interface is used by the Dafny IDE. + /// + public interface IRegion { + IToken BodyStartTok { get; } + IToken BodyEndTok { get; } + } + + public interface INamedRegion : IRegion { + string Name { get; } + } + + public abstract class Declaration : INamedRegion, IAttributeBearingDeclaration { + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(tok != null); + Contract.Invariant(Name != null); + } + + public static string IdProtect(string name) { + return DafnyOptions.O.Compiler.PublicIdProtect(name); + } + + public IToken tok; + public IToken BodyStartTok = Token.NoToken; + public IToken BodyEndTok = Token.NoToken; + public IToken StartToken = Token.NoToken; + public IToken EndToken = Token.NoToken; + public IToken TokenWithTrailingDocString = Token.NoToken; + public readonly string Name; + public bool IsRefining; + IToken IRegion.BodyStartTok { get { return BodyStartTok; } } + IToken IRegion.BodyEndTok { get { return BodyEndTok; } } + string INamedRegion.Name { get { return Name; } } + + private VisibilityScope opaqueScope = new VisibilityScope(); + private VisibilityScope revealScope = new VisibilityScope(); + + private bool scopeIsInherited = false; + + public virtual bool CanBeExported() { + return true; + } + + public virtual bool CanBeRevealed() { + return false; + } + + public bool ScopeIsInherited { get { return scopeIsInherited; } } + + public void AddVisibilityScope(VisibilityScope scope, bool IsOpaque) { + if (IsOpaque) { + opaqueScope.Augment(scope); + } else { + revealScope.Augment(scope); + } + } + + public void InheritVisibility(Declaration d, bool onlyRevealed = true) { + Contract.Assert(opaqueScope.IsEmpty()); + Contract.Assert(revealScope.IsEmpty()); + scopeIsInherited = false; + + revealScope = d.revealScope; + + if (!onlyRevealed) { + opaqueScope = d.opaqueScope; + } + scopeIsInherited = true; + + } + + public bool IsRevealedInScope(VisibilityScope scope) { + return revealScope.VisibleInScope(scope); + } + + public bool IsVisibleInScope(VisibilityScope scope) { + return IsRevealedInScope(scope) || opaqueScope.VisibleInScope(scope); + } + + protected string sanitizedName; + public virtual string SanitizedName => sanitizedName ??= NonglobalVariable.SanitizeName(Name); + + protected string compileName; + public virtual string CompileName { + get { + if (compileName == null) { + IsExtern(out _, out compileName); + compileName ??= SanitizedName; + } + return compileName; + } + } + + public bool IsExtern(out string/*?*/ qualification, out string/*?*/ name) { + // ensures result==false ==> qualification == null && name == null + Contract.Ensures(Contract.Result() || (Contract.ValueAtReturn(out qualification) == null && Contract.ValueAtReturn(out name) == null)); + // ensures result==true ==> qualification != null ==> name != null + Contract.Ensures(!Contract.Result() || Contract.ValueAtReturn(out qualification) == null || Contract.ValueAtReturn(out name) != null); + + qualification = null; + name = null; + if (!DafnyOptions.O.DisallowExterns) { + var externArgs = Attributes.FindExpressions(this.Attributes, "extern"); + if (externArgs != null) { + if (externArgs.Count == 0) { + return true; + } else if (externArgs.Count == 1 && externArgs[0] is StringLiteralExpr) { + name = externArgs[0].AsStringLiteral(); + return true; + } else if (externArgs.Count == 2 && externArgs[0] is StringLiteralExpr && externArgs[1] is StringLiteralExpr) { + qualification = externArgs[0].AsStringLiteral(); + name = externArgs[1].AsStringLiteral(); + return true; + } + } + } + return false; + } + public Attributes Attributes; // readonly, except during class merging in the refinement transformations and when changed by Compiler.MarkCapitalizationConflict + Attributes IAttributeBearingDeclaration.Attributes => Attributes; + + public Declaration(IToken tok, string name, Attributes attributes, bool isRefining) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + this.tok = tok; + this.Name = name; + this.Attributes = attributes; + this.IsRefining = isRefining; + } + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result() != null); + return Name; + } + + internal FreshIdGenerator IdGenerator = new FreshIdGenerator(); + } + + public class TypeParameter : TopLevelDecl { + public interface ParentType { + string FullName { get; } + } + + public override string WhatKind => "type parameter"; + + ParentType parent; + public ParentType Parent { + get { + return parent; + } + set { + Contract.Requires(Parent == null); // set it only once + Contract.Requires(value != null); + parent = value; + } + } + + public override string SanitizedName { + get { + if (sanitizedName == null) { + var name = Name; + if (parent is MemberDecl && !name.StartsWith("_")) { + // prepend "_" to type parameters of functions and methods, to ensure they don't clash with type parameters of the enclosing type + name = "_" + name; + } + sanitizedName = NonglobalVariable.SanitizeName(name); + } + return sanitizedName; + } + } + + public override string CompileName => SanitizedName; // Ignore :extern + + /// + /// NonVariant_Strict (default) - non-variant, no uses left of an arrow + /// NonVariant_Permissive ! - non-variant + /// Covariant_Strict + - co-variant, no uses left of an arrow + /// Covariant_Permissive * - co-variant + /// Contravariant - - contra-variant + /// + public enum TPVarianceSyntax { NonVariant_Strict, NonVariant_Permissive, Covariant_Strict, Covariant_Permissive, Contravariance } + public enum TPVariance { Co, Non, Contra } + public static TPVariance Negate(TPVariance v) { + switch (v) { + case TPVariance.Co: + return TPVariance.Contra; + case TPVariance.Contra: + return TPVariance.Co; + default: + return v; + } + } + public static int Direction(TPVariance v) { + switch (v) { + case TPVariance.Co: + return 1; + case TPVariance.Contra: + return -1; + default: + return 0; + } + } + public TPVarianceSyntax VarianceSyntax; + public TPVariance Variance { + get { + switch (VarianceSyntax) { + case TPVarianceSyntax.Covariant_Strict: + case TPVarianceSyntax.Covariant_Permissive: + return TPVariance.Co; + case TPVarianceSyntax.NonVariant_Strict: + case TPVarianceSyntax.NonVariant_Permissive: + return TPVariance.Non; + case TPVarianceSyntax.Contravariance: + return TPVariance.Contra; + default: + Contract.Assert(false); // unexpected VarianceSyntax + throw new cce.UnreachableException(); + } + } + } + public bool StrictVariance { + get { + switch (VarianceSyntax) { + case TPVarianceSyntax.Covariant_Strict: + case TPVarianceSyntax.NonVariant_Strict: + return true; + case TPVarianceSyntax.Covariant_Permissive: + case TPVarianceSyntax.NonVariant_Permissive: + case TPVarianceSyntax.Contravariance: + return false; + default: + Contract.Assert(false); // unexpected VarianceSyntax + throw new cce.UnreachableException(); + } + } + } + + public enum EqualitySupportValue { Required, InferredRequired, Unspecified } + public struct TypeParameterCharacteristics { + public EqualitySupportValue EqualitySupport; // the resolver may change this value from Unspecified to InferredRequired (for some signatures that may immediately imply that equality support is required) + public Type.AutoInitInfo AutoInit; + public bool HasCompiledValue => AutoInit == Type.AutoInitInfo.CompilableValue; + public bool IsNonempty => AutoInit != Type.AutoInitInfo.MaybeEmpty; + public bool ContainsNoReferenceTypes; + public TypeParameterCharacteristics(bool dummy) { + EqualitySupport = EqualitySupportValue.Unspecified; + AutoInit = Type.AutoInitInfo.MaybeEmpty; + ContainsNoReferenceTypes = false; + } + public TypeParameterCharacteristics(EqualitySupportValue eqSupport, Type.AutoInitInfo autoInit, bool containsNoReferenceTypes) { + EqualitySupport = eqSupport; + AutoInit = autoInit; + ContainsNoReferenceTypes = containsNoReferenceTypes; + } + } + public TypeParameterCharacteristics Characteristics; + public bool SupportsEquality { + get { return Characteristics.EqualitySupport != EqualitySupportValue.Unspecified; } + } + + public bool NecessaryForEqualitySupportOfSurroundingInductiveDatatype = false; // computed during resolution; relevant only when Parent denotes an IndDatatypeDecl + + public bool IsToplevelScope { // true if this type parameter is on a toplevel (ie. class C), and false if it is on a member (ie. method m(...)) + get { return parent is TopLevelDecl; } + } + public int PositionalIndex; // which type parameter this is (ie. in C, S is 0, T is 1 and U is 2). + + public TypeParameter(IToken tok, string name, TPVarianceSyntax varianceS, TypeParameterCharacteristics characteristics) + : base(tok, name, null, new List(), null, false) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Characteristics = characteristics; + VarianceSyntax = varianceS; + } + + public TypeParameter(IToken tok, string name, TPVarianceSyntax varianceS) + : this(tok, name, varianceS, new TypeParameterCharacteristics(false)) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + } + + public TypeParameter(IToken tok, string name, int positionalIndex, ParentType parent) + : this(tok, name, TPVarianceSyntax.NonVariant_Strict) { + PositionalIndex = positionalIndex; + Parent = parent; + } + + public override string FullName { + get { + // when debugging, print it all: + return /* Parent.FullName + "." + */ Name; + } + } + + public static TypeParameterCharacteristics GetExplicitCharacteristics(TopLevelDecl d) { + Contract.Requires(d != null); + TypeParameterCharacteristics characteristics = new TypeParameterCharacteristics(false); + if (d is OpaqueTypeDecl) { + var dd = (OpaqueTypeDecl)d; + characteristics = dd.Characteristics; + } else if (d is TypeSynonymDecl) { + var dd = (TypeSynonymDecl)d; + characteristics = dd.Characteristics; + } + if (characteristics.EqualitySupport == EqualitySupportValue.InferredRequired) { + return new TypeParameterCharacteristics(EqualitySupportValue.Unspecified, characteristics.AutoInit, characteristics.ContainsNoReferenceTypes); + } else { + return characteristics; + } + } + } + + // Represents a submodule declaration at module level scope + abstract public class ModuleDecl : TopLevelDecl { + public override string WhatKind { get { return "module"; } } + [FilledInDuringResolution] public ModuleSignature Signature; // filled in topological order. + public virtual ModuleSignature AccessibleSignature(bool ignoreExports) { + Contract.Requires(Signature != null); + return Signature; + } + public virtual ModuleSignature AccessibleSignature() { + Contract.Requires(Signature != null); + return Signature; + } + public int Height; + + public readonly bool Opened; + + public ModuleDecl(IToken tok, string name, ModuleDefinition parent, bool opened, bool isRefining) + : base(tok, name, parent, new List(), null, isRefining) { + Height = -1; + Signature = null; + Opened = opened; + } + public abstract object Dereference(); + + public int? ResolvedHash { get; set; } + } + // Represents module X { ... } + public class LiteralModuleDecl : ModuleDecl { + public readonly ModuleDefinition ModuleDef; + + [FilledInDuringResolution] public ModuleSignature DefaultExport; // the default export set of the module. + + private ModuleSignature emptySignature; + public override ModuleSignature AccessibleSignature(bool ignoreExports) { + if (ignoreExports) { + return Signature; + } + return this.AccessibleSignature(); + } + public override ModuleSignature AccessibleSignature() { + if (DefaultExport == null) { + if (emptySignature == null) { + emptySignature = new ModuleSignature(); + } + return emptySignature; + } + return DefaultExport; + } + + public LiteralModuleDecl(ModuleDefinition module, ModuleDefinition parent) + : base(module.tok, module.Name, parent, false, false) { + ModuleDef = module; + StartToken = module.StartToken; + TokenWithTrailingDocString = module.TokenWithTrailingDocString; + } + public override object Dereference() { return ModuleDef; } + } + // Represents "module name = path;", where name is an identifier and path is a possibly qualified name. + public class AliasModuleDecl : ModuleDecl { + public readonly ModuleQualifiedId TargetQId; // generated by the parser, this is looked up + public readonly List Exports; // list of exports sets + [FilledInDuringResolution] public bool ShadowsLiteralModule; // initialized early during Resolution (and used not long after that); true for "import opened A = A" where "A" is a literal module in the same scope + + public AliasModuleDecl(ModuleQualifiedId path, IToken name, ModuleDefinition parent, bool opened, List exports) + : base(name, name.val, parent, opened, false) { + Contract.Requires(path != null && path.Path.Count > 0); + Contract.Requires(exports != null); + Contract.Requires(exports.Count == 0 || path.Path.Count == 1); + TargetQId = path; + Exports = exports; + } + public override object Dereference() { return Signature.ModuleDef; } + } + + // Represents "module name as path [ = compilePath];", where name is a identifier and path is a possibly qualified name. + // Used to be called ModuleFacadeDecl -- renamed to be like LiteralModuleDecl, AliasModuleDecl + public class AbstractModuleDecl : ModuleDecl { + public readonly ModuleQualifiedId QId; + public readonly List Exports; // list of exports sets + public ModuleDecl CompileRoot; + public ModuleSignature OriginalSignature; + + public AbstractModuleDecl(ModuleQualifiedId qid, IToken name, ModuleDefinition parent, bool opened, List exports) + : base(name, name.val, parent, opened, false) { + Contract.Requires(qid != null && qid.Path.Count > 0); + Contract.Requires(exports != null); + + QId = qid; + Exports = exports; + } + public override object Dereference() { return this; } + } + + // Represents the exports of a module. + public class ModuleExportDecl : ModuleDecl { + public readonly bool IsDefault; + public List Exports; // list of TopLevelDecl that are included in the export + public List Extends; // list of exports that are extended + [FilledInDuringResolution] public readonly List ExtendDecls = new List(); + [FilledInDuringResolution] public readonly HashSet> ExportDecls = new HashSet>(); + public bool RevealAll; // only kept for initial rewriting, then discarded + public bool ProvideAll; + + public readonly VisibilityScope ThisScope; + public ModuleExportDecl(IToken tok, ModuleDefinition parent, + List exports, List extends, bool provideAll, bool revealAll, bool isDefault, bool isRefining) + : base(tok, (isDefault || tok.val == "export") ? parent.Name : tok.val, parent, false, isRefining) { + Contract.Requires(exports != null); + IsDefault = isDefault; + Exports = exports; + Extends = extends; + ProvideAll = provideAll; + RevealAll = revealAll; + ThisScope = new VisibilityScope(this.FullSanitizedName); + } + + public ModuleExportDecl(IToken tok, string name, ModuleDefinition parent, + List exports, List extends, bool provideAll, bool revealAll, bool isDefault, bool isRefining) + : base(tok, name, parent, false, isRefining) { + Contract.Requires(exports != null); + IsDefault = isDefault; + Exports = exports; + Extends = extends; + ProvideAll = provideAll; + RevealAll = revealAll; + ThisScope = new VisibilityScope(this.FullSanitizedName); + } + + public void SetupDefaultSignature() { + Contract.Requires(this.Signature == null); + var sig = new ModuleSignature(); + sig.ModuleDef = this.EnclosingModuleDefinition; + sig.IsAbstract = this.EnclosingModuleDefinition.IsAbstract; + sig.VisibilityScope = new VisibilityScope(); + sig.VisibilityScope.Augment(ThisScope); + this.Signature = sig; + } + + public override object Dereference() { return this; } + public override bool CanBeExported() { + return false; + } + + } + + public class ExportSignature { + public readonly IToken Tok; + public readonly IToken ClassIdTok; + public readonly bool Opaque; + public readonly string ClassId; + public readonly string Id; + + [FilledInDuringResolution] public Declaration Decl; + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Tok != null); + Contract.Invariant(Id != null); + Contract.Invariant((ClassId != null) == (ClassIdTok != null)); + } + + public ExportSignature(IToken prefixTok, string prefix, IToken idTok, string id, bool opaque) { + Contract.Requires(prefixTok != null); + Contract.Requires(prefix != null); + Contract.Requires(idTok != null); + Contract.Requires(id != null); + Tok = idTok; + ClassIdTok = prefixTok; + ClassId = prefix; + Id = id; + Opaque = opaque; + } + + public ExportSignature(IToken idTok, string id, bool opaque) { + Contract.Requires(idTok != null); + Contract.Requires(id != null); + Tok = idTok; + Id = id; + Opaque = opaque; + } + + public override string ToString() { + if (ClassId != null) { + return ClassId + "." + Id; + } + return Id; + } + } + + public class ModuleSignature { + public VisibilityScope VisibilityScope = null; + public readonly Dictionary TopLevels = new Dictionary(); + public readonly Dictionary ExportSets = new Dictionary(); + public readonly Dictionary> Ctors = new Dictionary>(); + public readonly Dictionary StaticMembers = new Dictionary(); + public ModuleDefinition ModuleDef = null; // Note: this is null if this signature does not correspond to a specific definition (i.e. + // it is abstract). Otherwise, it points to that definition. + public ModuleSignature CompileSignature = null; // This is the version of the signature that should be used at compile time. + public ModuleSignature Refines = null; + public bool IsAbstract = false; + public ModuleSignature() { } + public int? ResolvedHash { get; set; } + + // Qualified accesses follow module imports + public bool FindImport(string name, out ModuleDecl decl) { + TopLevelDecl top; + if (TopLevels.TryGetValue(name, out top) && top is ModuleDecl) { + decl = (ModuleDecl)top; + return true; + } else { + decl = null; + return false; + } + } + } + + public class ModuleQualifiedId { + public readonly List Path; // Path != null && Path.Count > 0 + + public ModuleQualifiedId(List path) { + Contract.Assert(path != null && path.Count > 0); + this.Path = path; // note that the list is aliased -- not to be modified after construction + } + + // Creates a clone, including a copy of the list; + // if the argument is true, resolution information is included + public ModuleQualifiedId Clone(bool includeResInfo) { + List newlist = new List(Path); + ModuleQualifiedId cl = new ModuleQualifiedId(newlist); + if (includeResInfo) { + cl.Root = this.Root; + cl.Decl = this.Decl; + cl.Def = this.Def; + cl.Sig = this.Sig; + Contract.Assert(this.Def == this.Sig.ModuleDef); + } + return cl; + } + + public string rootName() { + return Path[0].val; + } + + public IToken rootToken() { + return Path[0]; + } + + override public string ToString() { + string s = Path[0].val; + for (int i = 1; i < Path.Count; ++i) { + s = s + "." + Path[i].val; + } + + return s; + } + + public void SetRoot(ModuleDecl m) { + this.Root = m; + } + + public void Set(ModuleDecl m) { + if (m == null) { + this.Decl = null; + this.Def = null; + this.Sig = null; + } else { + this.Decl = m; + this.Def = ((LiteralModuleDecl)m).ModuleDef; + this.Sig = m.Signature; + } + } + + // The following are filled in during resolution + // Note that the root (first path segment) is resolved initially, + // as it is needed to determine dependency relationships. + // Then later the rest of the path is resolved, at which point all of the + // ids in the path have been fully resolved + // Note also that the resolution of the root depends on the syntactice location + // of the qualified id; the resolution of subsequent ids depends on the + // default export set of the previous id. + [FilledInDuringResolution] public ModuleDecl Root; // the module corresponding to Path[0].val + [FilledInDuringResolution] public ModuleDecl Decl; // the module corresponding to the full path + [FilledInDuringResolution] public ModuleDefinition Def; // the module definition corresponding to the full path + [FilledInDuringResolution] public ModuleSignature Sig; // the module signature corresponding to the full path + } + + public class ModuleDefinition : INamedRegion, IAttributeBearingDeclaration { + public readonly IToken tok; + public IToken BodyStartTok = Token.NoToken; + public IToken BodyEndTok = Token.NoToken; + public IToken StartToken = Token.NoToken; + public IToken TokenWithTrailingDocString = Token.NoToken; + public readonly string DafnyName; // The (not-qualified) name as seen in Dafny source code + public readonly string Name; // (Last segment of the) module name + public string FullDafnyName { + get { + if (EnclosingModule == null) { + return ""; + } + + string n = EnclosingModule.FullDafnyName; + return (n.Length == 0 ? n : (n + ".")) + DafnyName; + } + } + public string FullName { + get { + if (EnclosingModule == null || EnclosingModule.IsDefaultModule) { + return Name; + } else { + return EnclosingModule.FullName + "." + Name; + } + } + } + public readonly List PrefixIds; // The qualified module name, except the last segment when a + // nested module declaration is outside its enclosing module + IToken IRegion.BodyStartTok { get { return BodyStartTok; } } + IToken IRegion.BodyEndTok { get { return BodyEndTok; } } + string INamedRegion.Name { get { return Name; } } + public ModuleDefinition EnclosingModule; // readonly, except can be changed by resolver for prefix-named modules when the real parent is discovered + public readonly Attributes Attributes; + Attributes IAttributeBearingDeclaration.Attributes => Attributes; + public ModuleQualifiedId RefinementQId; // full qualified ID of the refinement parent, null if no refinement base + public bool SuccessfullyResolved; // set to true upon successful resolution; modules that import an unsuccessfully resolved module are not themselves resolved + + public List Includes; + + [FilledInDuringResolution] public readonly List TopLevelDecls = new List(); // filled in by the parser; readonly after that, except for the addition of prefix-named modules, which happens in the resolver + [FilledInDuringResolution] public readonly List, LiteralModuleDecl>> PrefixNamedModules = new List, LiteralModuleDecl>>(); // filled in by the parser; emptied by the resolver + [FilledInDuringResolution] public readonly Graph CallGraph = new Graph(); + [FilledInDuringResolution] public int Height; // height in the topological sorting of modules; + public readonly bool IsAbstract; + public readonly bool IsFacade; // True iff this module represents a module facade (that is, an abstract interface) + private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled. + public readonly bool IsToBeVerified; + public readonly bool IsToBeCompiled; + + public int? ResolvedHash { get; set; } + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(TopLevelDecls)); + Contract.Invariant(CallGraph != null); + } + + public ModuleDefinition(IToken tok, string name, List prefixIds, bool isAbstract, bool isFacade, + ModuleQualifiedId refinementQId, ModuleDefinition parent, Attributes attributes, bool isBuiltinName, + bool isToBeVerified, bool isToBeCompiled) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + this.tok = tok; + this.DafnyName = tok.val; + this.Name = name; + this.PrefixIds = prefixIds; + this.Attributes = attributes; + this.EnclosingModule = parent; + this.RefinementQId = refinementQId; + this.IsAbstract = isAbstract; + this.IsFacade = isFacade; + this.Includes = new List(); + this.IsBuiltinName = isBuiltinName; + this.IsToBeVerified = isToBeVerified; + this.IsToBeCompiled = isToBeCompiled; + } + + VisibilityScope visibilityScope; + public VisibilityScope VisibilityScope => + visibilityScope ??= new VisibilityScope(this.SanitizedName); + + public virtual bool IsDefaultModule { + get { + return false; + } + } + + private string sanitizedName = null; + + public string SanitizedName { + get { + if (sanitizedName == null) { + if (IsBuiltinName) { + sanitizedName = Name; + } else if (EnclosingModule != null && EnclosingModule.Name != "_module") { + // Include all names in the module tree path, to disambiguate when compiling + // a flat list of modules. + // Use an "underscore-escaped" character as a module name separator, since + // underscores are already used as escape characters in SanitizeName() + sanitizedName = EnclosingModule.SanitizedName + "_m" + NonglobalVariable.SanitizeName(Name); + } else { + sanitizedName = NonglobalVariable.SanitizeName(Name); + } + } + return sanitizedName; + } + } + + string compileName; + public string CompileName { + get { + if (compileName == null) { + var externArgs = DafnyOptions.O.DisallowExterns ? null : Attributes.FindExpressions(this.Attributes, "extern"); + if (externArgs != null && 1 <= externArgs.Count && externArgs[0] is StringLiteralExpr) { + compileName = (string)((StringLiteralExpr)externArgs[0]).Value; + } else if (externArgs != null) { + compileName = Name; + } else { + compileName = SanitizedName; + } + } + return compileName; + } + } + + /// + /// Determines if "a" and "b" are in the same strongly connected component of the call graph, that is, + /// if "a" and "b" are mutually recursive. + /// Assumes that CallGraph has already been filled in for the modules containing "a" and "b". + /// + public static bool InSameSCC(ICallable a, ICallable b) { + Contract.Requires(a != null); + Contract.Requires(b != null); + if (a is SpecialFunction || b is SpecialFunction) { return false; } + var module = a.EnclosingModule; + return module == b.EnclosingModule && module.CallGraph.GetSCCRepresentative(a) == module.CallGraph.GetSCCRepresentative(b); + } + + /// + /// Return the representative elements of the SCCs that contain any member declaration in a + /// class in "declarations". + /// Note, the representative element may in some cases be a Method, not necessarily a Function. + /// + public static IEnumerable AllFunctionSCCs(List declarations) { + var set = new HashSet(); + foreach (var d in declarations) { + var cl = d as TopLevelDeclWithMembers; + if (cl != null) { + var module = cl.EnclosingModuleDefinition; + foreach (var member in cl.Members) { + var fn = member as Function; + if (fn != null) { + var repr = module.CallGraph.GetSCCRepresentative(fn); + set.Add(repr); + } + } + } + } + return set; + } + + public static IEnumerable AllFunctions(List declarations) { + foreach (var d in declarations) { + var cl = d as TopLevelDeclWithMembers; + if (cl != null) { + foreach (var member in cl.Members) { + var fn = member as Function; + if (fn != null) { + yield return fn; + } + } + } + } + } + + public static IEnumerable AllFields(List declarations) { + foreach (var d in declarations) { + var cl = d as TopLevelDeclWithMembers; + if (cl != null) { + foreach (var member in cl.Members) { + var fn = member as Field; + if (fn != null) { + yield return fn; + } + } + } + } + } + + public static IEnumerable AllClasses(List declarations) { + foreach (var d in declarations) { + if (d is ClassDecl cl) { + yield return cl; + } + } + } + + public static IEnumerable AllTypesWithMembers(List declarations) { + foreach (var d in declarations) { + if (d is TopLevelDeclWithMembers cl) { + yield return cl; + } + } + } + + /// + /// Yields all functions and methods that are members of some type in the given list of + /// declarations. + /// Note, an iterator declaration is a type, in this sense. + /// Note, if the given list are the top-level declarations of a module, the yield will include + /// greatest lemmas but not their associated prefix lemmas (which are tucked into the greatest lemma's + /// .PrefixLemma field). + /// + public static IEnumerable AllCallables(List declarations) { + foreach (var d in declarations) { + var cl = d as TopLevelDeclWithMembers; + if (cl != null) { + foreach (var member in cl.Members) { + var clbl = member as ICallable; + if (clbl != null && !(member is ConstantField)) { + yield return clbl; + if (clbl is Function f && f.ByMethodDecl != null) { + yield return f.ByMethodDecl; + } + } + } + } + } + } + + /// + /// Yields all functions and methods that are members of some non-iterator type in the given + /// list of declarations, as well as any IteratorDecl's in that list. + /// + public static IEnumerable AllItersAndCallables(List declarations) { + foreach (var d in declarations) { + if (d is IteratorDecl) { + var iter = (IteratorDecl)d; + yield return iter; + } else if (d is TopLevelDeclWithMembers) { + var cl = (TopLevelDeclWithMembers)d; + foreach (var member in cl.Members) { + var clbl = member as ICallable; + if (clbl != null) { + yield return clbl; + if (clbl is Function f && f.ByMethodDecl != null) { + yield return f.ByMethodDecl; + } + } + } + } + } + } + + public static IEnumerable AllIteratorDecls(List declarations) { + foreach (var d in declarations) { + var iter = d as IteratorDecl; + if (iter != null) { + yield return iter; + } + } + } + + /// + /// Emits the declarations in "declarations", but for each such declaration that is a class with + /// a corresponding non-null type, also emits that non-null type *after* the class declaration. + /// + public static IEnumerable AllDeclarationsAndNonNullTypeDecls(List declarations) { + foreach (var d in declarations) { + yield return d; + var cl = d as ClassDecl; + if (cl != null && cl.NonNullTypeDecl != null) { + yield return cl.NonNullTypeDecl; + } + } + } + + public static IEnumerable AllExtremeLemmas(List declarations) { + foreach (var d in declarations) { + var cl = d as TopLevelDeclWithMembers; + if (cl != null) { + foreach (var member in cl.Members) { + var m = member as ExtremeLemma; + if (m != null) { + yield return m; + } + } + } + } + } + + public bool IsEssentiallyEmptyModuleBody() { + foreach (var d in TopLevelDecls) { + if (d is ModuleDecl) { + // modules don't count + continue; + } else if (d is ClassDecl) { + var cl = (ClassDecl)d; + if (cl.Members.Count == 0) { + // the class is empty, so it doesn't count + continue; + } + } + return false; + } + return true; + } + + public IToken GetFirstTopLevelToken() { + return TopLevelDecls.OfType() + .SelectMany(classDecl => classDecl.Members) + .Where(member => member.tok.line > 0) + .Select(member => member.tok) + .Concat(TopLevelDecls.OfType() + .Select(moduleDecl => moduleDecl.ModuleDef.GetFirstTopLevelToken()) + .Where(tok => tok.line > 0) + ).FirstOrDefault(Token.NoToken); + } + } + + public class DefaultModuleDecl : ModuleDefinition { + public DefaultModuleDecl() + : base(Token.NoToken, "_module", new List(), false, false, null, null, null, true, true, true) { + } + public override bool IsDefaultModule { + get { + return true; + } + } + } + + public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType { + public abstract string WhatKind { get; } + public readonly ModuleDefinition EnclosingModuleDefinition; + public readonly List TypeArgs; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(TypeArgs)); + } + + public TopLevelDecl(IToken tok, string name, ModuleDefinition enclosingModule, List typeArgs, Attributes attributes, bool isRefining) + : base(tok, name, attributes, isRefining) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + EnclosingModuleDefinition = enclosingModule; + TypeArgs = typeArgs; + } + + public string FullDafnyName { + get { + if (Name == "_module") { + return ""; + } + + if (Name == "_default") { + return EnclosingModuleDefinition.FullDafnyName; + } + + string n = EnclosingModuleDefinition.FullDafnyName; + return (n.Length == 0 ? n : (n + ".")) + Name; + } + } + public virtual string FullName { + get { + return EnclosingModuleDefinition.FullName + "." + Name; + } + } + public string FullSanitizedName { + get { + return EnclosingModuleDefinition.SanitizedName + "." + SanitizedName; + } + } + + public string FullNameInContext(ModuleDefinition context) { + if (EnclosingModuleDefinition == context) { + return Name; + } else { + return EnclosingModuleDefinition.Name + "." + Name; + } + } + public string FullCompileName { + get { + var externArgs = Attributes.FindExpressions(this.Attributes, "extern"); + if (!DafnyOptions.O.DisallowExterns && externArgs != null) { + if (externArgs.Count == 2 && externArgs[0] is StringLiteralExpr && externArgs[1] is StringLiteralExpr) { + return externArgs[0].AsStringLiteral() + "." + externArgs[1].AsStringLiteral(); + } + } + + return DafnyOptions.O.Compiler.GetCompileName(EnclosingModuleDefinition.IsDefaultModule, + EnclosingModuleDefinition.CompileName, CompileName); + } + } + + public TopLevelDecl ViewAsClass { + get { + if (this is NonNullTypeDecl) { + return ((NonNullTypeDecl)this).Class; + } else { + return this; + } + } + } + + /// + /// Return the list of parent types of "this", where the type parameters + /// of "this" have been instantiated by "typeArgs". For example, for a subset + /// type, the return value is the RHS type, appropriately instantiated. As + /// two other examples, given + /// class C extends J + /// C.ParentTypes(real) = J // non-null types C and J + /// C?.ParentTypes(real) = J? // possibly-null type C? and J? + /// + public virtual List ParentTypes(List typeArgs) { + Contract.Requires(typeArgs != null); + Contract.Requires(this.TypeArgs.Count == typeArgs.Count); + return new List(); + } + + public bool AllowsAllocation => true; + } + + public abstract class TopLevelDeclWithMembers : TopLevelDecl { + public readonly List Members; + + // The following fields keep track of parent traits + public readonly List InheritedMembers = new List(); // these are instance members declared in parent traits + public readonly List ParentTraits; // these are the types that are parsed after the keyword 'extends'; note, for a successfully resolved program, these are UserDefinedType's where .ResolvedClas is NonNullTypeDecl + public readonly Dictionary ParentFormalTypeParametersToActuals = new Dictionary(); // maps parent traits' type parameters to actuals + + /// + /// TraitParentHeads contains the head of each distinct trait parent. It is initialized during resolution. + /// + public readonly List ParentTraitHeads = new List(); + + [FilledInDuringResolution] public InheritanceInformationClass ParentTypeInformation; + public class InheritanceInformationClass { + private readonly Dictionary /*via this parent path*/)>> info = new Dictionary)>>(); + + /// + /// Returns a subset of the trait's ParentTraits, but not repeating any head type. + /// Assumes the declaration has been successfully resolved. + /// + public List UniqueParentTraits() { + return info.ToList().ConvertAll(entry => entry.Value[0].Item1); + } + + public void Record(TraitDecl traitHead, UserDefinedType parentType) { + Contract.Requires(traitHead != null); + Contract.Requires(parentType != null); + Contract.Requires(parentType.ResolvedClass is NonNullTypeDecl nntd && nntd.ViewAsClass == traitHead); + + if (!info.TryGetValue(traitHead, out var list)) { + list = new List<(Type, List)>(); + info.Add(traitHead, list); + } + list.Add((parentType, new List())); + } + + public void Extend(TraitDecl parent, InheritanceInformationClass parentInfo, Dictionary typeMap) { + Contract.Requires(parent != null); + Contract.Requires(parentInfo != null); + Contract.Requires(typeMap != null); + + foreach (var entry in parentInfo.info) { + var traitHead = entry.Key; + if (!info.TryGetValue(traitHead, out var list)) { + list = new List<(Type, List)>(); + info.Add(traitHead, list); + } + foreach (var pair in entry.Value) { + var ty = Resolver.SubstType(pair.Item1, typeMap); + // prepend the path with "parent" + var parentPath = new List() { parent }; + parentPath.AddRange(pair.Item2); + list.Add((ty, parentPath)); + } + } + } + + public IEnumerable)>> GetTypeInstantiationGroups() { + foreach (var pair in info.Values) { + yield return pair; + } + } + } + + public TopLevelDeclWithMembers(IToken tok, string name, ModuleDefinition module, List typeArgs, List members, Attributes attributes, bool isRefining, List/*?*/ traits = null) + : base(tok, name, module, typeArgs, attributes, isRefining) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cce.NonNullElements(members)); + Members = members; + ParentTraits = traits ?? new List(); + } + + public static List CommonTraits(TopLevelDeclWithMembers a, TopLevelDeclWithMembers b) { + Contract.Requires(a != null); + Contract.Requires(b != null); + var aa = a.TraitAncestors(); + var bb = b.TraitAncestors(); + aa.IntersectWith(bb); + var types = new List(); + foreach (var t in aa) { + var typeArgs = t.TypeArgs.ConvertAll(tp => a.ParentFormalTypeParametersToActuals[tp]); + var u = new UserDefinedType(t.tok, t.Name + "?", t, typeArgs); + types.Add(u); + } + return types; + } + + /// + /// Returns the set of transitive parent traits (not including "this" itself). + /// This method assumes the .ParentTraits fields have been checked for various cycle restrictions. + /// + public ISet TraitAncestors() { + var s = new HashSet(); + AddTraitAncestors(s); + return s; + } + /// + /// Adds to "s" the transitive parent traits (not including "this" itself). + /// This method assumes the .ParentTraits fields have been checked for various cycle restrictions. + /// + private void AddTraitAncestors(ISet s) { + Contract.Requires(s != null); + foreach (var parent in ParentTraits) { + var udt = (UserDefinedType)parent; // in a successfully resolved program, we expect all .ParentTraits to be a UserDefinedType + var nntd = (NonNullTypeDecl)udt.ResolvedClass; // we expect the trait type to be the non-null version of the trait type + var tr = (TraitDecl)nntd.Class; + s.Add(tr); + tr.AddTraitAncestors(s); + } + } + } + + public class TraitDecl : ClassDecl { + public override string WhatKind { get { return "trait"; } } + public bool IsParent { set; get; } + public TraitDecl(IToken tok, string name, ModuleDefinition module, + List typeArgs, [Captured] List members, Attributes attributes, bool isRefining, List/*?*/ traits) + : base(tok, name, module, typeArgs, members, attributes, isRefining, traits) { } + } + + public class ClassDecl : TopLevelDeclWithMembers, RevealableTypeDecl { + public override string WhatKind { get { return "class"; } } + public override bool CanBeRevealed() { return true; } + [FilledInDuringResolution] public bool HasConstructor; // filled in (early) during resolution; true iff there exists a member that is a Constructor + public readonly NonNullTypeDecl NonNullTypeDecl; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(Members)); + Contract.Invariant(ParentTraits != null); + } + + public ClassDecl(IToken tok, string name, ModuleDefinition module, + List typeArgs, [Captured] List members, Attributes attributes, bool isRefining, List/*?*/ traits) + : base(tok, name, module, typeArgs, members, attributes, isRefining, traits) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(module != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cce.NonNullElements(members)); + Contract.Assume(!(this is ArrowTypeDecl)); // this is also a precondition, really, but "this" cannot be mentioned in Requires of a constructor; ArrowTypeDecl should use the next constructor + if (!IsDefaultClass) { + NonNullTypeDecl = new NonNullTypeDecl(this); + } + this.NewSelfSynonym(); + } + /// + /// The following constructor is supposed to be called by the ArrowTypeDecl subtype, in order to avoid + /// the call to this.NewSelfSynonym() (because NewSelfSynonym() depends on the .Arity field having been + /// set, which it hasn't during the base call of the ArrowTypeDecl constructor). Instead, the ArrowTypeDecl + /// constructor will do that call. + /// + protected ClassDecl(IToken tok, string name, ModuleDefinition module, + List typeArgs, [Captured] List members, Attributes attributes, bool isRefining) + : base(tok, name, module, typeArgs, members, attributes, isRefining, null) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(module != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cce.NonNullElements(members)); + Contract.Assume(this is ArrowTypeDecl); // this is also a precondition, really, but "this" cannot be mentioned in Requires of a constructor + } + public virtual bool IsDefaultClass { + get { + return false; + } + } + + public bool IsObjectTrait { + get => Name == "object"; + } + + internal bool HeadDerivesFrom(TopLevelDecl b) { + Contract.Requires(b != null); + return this == b || this.ParentTraitHeads.Exists(tr => tr.HeadDerivesFrom(b)); + } + + public List NonNullTraitsWithArgument(List typeArgs) { + Contract.Requires(typeArgs != null); + Contract.Requires(typeArgs.Count == TypeArgs.Count); + + // Instantiate with the actual type arguments + if (typeArgs.Count == 0) { + // this optimization seems worthwhile + return ParentTraits; + } else { + var subst = Resolver.TypeSubstitutionMap(TypeArgs, typeArgs); + return ParentTraits.ConvertAll(traitType => Resolver.SubstType(traitType, subst)); + } + } + + public List PossiblyNullTraitsWithArgument(List typeArgs) { + Contract.Requires(typeArgs != null); + Contract.Requires(typeArgs.Count == TypeArgs.Count); + // Instantiate with the actual type arguments + var subst = Resolver.TypeSubstitutionMap(TypeArgs, typeArgs); + return ParentTraits.ConvertAll(traitType => (Type)UserDefinedType.CreateNullableType((UserDefinedType)Resolver.SubstType(traitType, subst))); + } + + public override List ParentTypes(List typeArgs) { + return PossiblyNullTraitsWithArgument(typeArgs); + } + + public TopLevelDecl AsTopLevelDecl => this; + public TypeDeclSynonymInfo SynonymInfo { get; set; } + } + + public class DefaultClassDecl : ClassDecl { + public DefaultClassDecl(ModuleDefinition module, [Captured] List members) + : base(Token.NoToken, "_default", module, new List(), members, null, false, null) { + Contract.Requires(module != null); + Contract.Requires(cce.NonNullElements(members)); + } + public override bool IsDefaultClass { + get { + return true; + } + } + } + + public class ArrayClassDecl : ClassDecl { + public override string WhatKind { get { return "array type"; } } + public readonly int Dims; + public ArrayClassDecl(int dims, ModuleDefinition module, Attributes attrs) + : base(Token.NoToken, BuiltIns.ArrayClassName(dims), module, + new List(new TypeParameter[] { new TypeParameter(Token.NoToken, "arg", TypeParameter.TPVarianceSyntax.NonVariant_Strict) }), + new List(), attrs, false, null) { + Contract.Requires(1 <= dims); + Contract.Requires(module != null); + + Dims = dims; + // Resolve type parameter + Contract.Assert(TypeArgs.Count == 1); + var tp = TypeArgs[0]; + tp.Parent = this; + tp.PositionalIndex = 0; + } + } + + public class ArrowTypeDecl : ClassDecl { + public override string WhatKind { get { return "function type"; } } + public readonly int Arity; + public readonly Function Requires; + public readonly Function Reads; + + public ArrowTypeDecl(List tps, Function req, Function reads, ModuleDefinition module, Attributes attributes) + : base(Token.NoToken, ArrowType.ArrowTypeName(tps.Count - 1), module, tps, + new List { req, reads }, attributes, false) { + Contract.Requires(tps != null && 1 <= tps.Count); + Contract.Requires(req != null); + Contract.Requires(reads != null); + Contract.Requires(module != null); + Arity = tps.Count - 1; + Requires = req; + Reads = reads; + Requires.EnclosingClass = this; + Reads.EnclosingClass = this; + this.NewSelfSynonym(); + } + } + + public abstract class DatatypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, ICallable { + public override bool CanBeRevealed() { return true; } + public readonly List Ctors; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(Ctors)); + Contract.Invariant(1 <= Ctors.Count); + } + + public DatatypeDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, + [Captured] List ctors, List members, Attributes attributes, bool isRefining) + : base(tok, name, module, typeArgs, members, attributes, isRefining) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(module != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cce.NonNullElements(ctors)); + Contract.Requires(cce.NonNullElements(members)); + Contract.Requires((isRefining && ctors.Count == 0) || (!isRefining && 1 <= ctors.Count)); + Ctors = ctors; + this.NewSelfSynonym(); + } + public bool HasFinitePossibleValues { + get { + return (TypeArgs.Count == 0 && Ctors.TrueForAll(ctr => ctr.Formals.Count == 0)); + } + } + + public bool IsRecordType { + get { return this is IndDatatypeDecl && Ctors.Count == 1; } + } + + public TopLevelDecl AsTopLevelDecl => this; + public TypeDeclSynonymInfo SynonymInfo { get; set; } + + bool ICodeContext.IsGhost { get { return true; } } + List ICodeContext.TypeArgs { get { return TypeArgs; } } + List ICodeContext.Ins { get { return new List(); } } + ModuleDefinition ICodeContext.EnclosingModule { get { return EnclosingModuleDefinition; } } + bool ICodeContext.MustReverify { get { return false; } } + bool ICodeContext.AllowsNontermination { get { return false; } } + IToken ICallable.Tok { get { return tok; } } + string ICallable.NameRelativeToModule { get { return Name; } } + Specification ICallable.Decreases { + get { + // The resolver checks that a NewtypeDecl sits in its own SSC in the call graph. Therefore, + // the question of what its Decreases clause is should never arise. + throw new cce.UnreachableException(); + } + } + bool ICallable.InferredDecreases { + get { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases + set { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases + } + + public abstract DatatypeCtor GetGroundingCtor(); + } + + public class IndDatatypeDecl : DatatypeDecl { + public override string WhatKind { get { return "datatype"; } } + public DatatypeCtor GroundingCtor; // set during resolution + + public override DatatypeCtor GetGroundingCtor() { + return GroundingCtor; + } + + public bool[] TypeParametersUsedInConstructionByGroundingCtor; // set during resolution; has same length as the number of type arguments + + public enum ES { NotYetComputed, Never, ConsultTypeArguments } + public ES EqualitySupport = ES.NotYetComputed; + + public IndDatatypeDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, + [Captured] List ctors, List members, Attributes attributes, bool isRefining) + : base(tok, name, module, typeArgs, ctors, members, attributes, isRefining) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(module != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cce.NonNullElements(ctors)); + Contract.Requires(cce.NonNullElements(members)); + Contract.Requires((isRefining && ctors.Count == 0) || (!isRefining && 1 <= ctors.Count)); + } + } + + public class CoDatatypeDecl : DatatypeDecl { + public override string WhatKind { get { return "codatatype"; } } + [FilledInDuringResolution] public CoDatatypeDecl SscRepr; + + public CoDatatypeDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, + [Captured] List ctors, List members, Attributes attributes, bool isRefining) + : base(tok, name, module, typeArgs, ctors, members, attributes, isRefining) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(module != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cce.NonNullElements(ctors)); + Contract.Requires(cce.NonNullElements(members)); + Contract.Requires((isRefining && ctors.Count == 0) || (!isRefining && 1 <= ctors.Count)); + } + + public override DatatypeCtor GetGroundingCtor() { + return Ctors[0]; + } + } + + /// + /// The "ValuetypeDecl" class models the built-in value types (like bool, int, set, and seq. + /// Its primary function is to hold the formal type parameters and built-in members of these types. + /// + public class ValuetypeDecl : TopLevelDecl { + public override string WhatKind { get { return Name; } } + public readonly Dictionary Members = new Dictionary(); + readonly Func typeTester; + readonly Func, Type>/*?*/ typeCreator; + + public ValuetypeDecl(string name, ModuleDefinition module, int typeParameterCount, Func typeTester, Func, Type>/*?*/ typeCreator) + : base(Token.NoToken, name, module, new List(), null, false) { + Contract.Requires(name != null); + Contract.Requires(module != null); + Contract.Requires(0 <= typeParameterCount); + Contract.Requires(typeTester != null); + // fill in the type parameters + for (int i = 0; i < typeParameterCount; i++) { + TypeArgs.Add(new TypeParameter(Token.NoToken, ((char)('T' + i)).ToString(), i, this)); + } + this.typeTester = typeTester; + this.typeCreator = typeCreator; + } + + public bool IsThisType(Type t) { + Contract.Assert(t != null); + return typeTester(t); + } + + public Type CreateType(List typeArgs) { + Contract.Requires(typeArgs != null); + Contract.Requires(typeArgs.Count == TypeArgs.Count); + Contract.Assume(typeCreator != null); // can only call CreateType for a ValuetypeDecl with a type creator (this is up to the caller to ensure) + return typeCreator(typeArgs); + } + } + + public class DatatypeCtor : Declaration, TypeParameter.ParentType { + public readonly List Formals; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(Formals)); + Contract.Invariant(Destructors != null); + Contract.Invariant( + Destructors.Count == 0 || // this is until resolution + Destructors.Count == Formals.Count); // after resolution + } + + // TODO: One could imagine having a precondition on datatype constructors + [FilledInDuringResolution] public DatatypeDecl EnclosingDatatype; + [FilledInDuringResolution] public SpecialField QueryField; + [FilledInDuringResolution] public List Destructors = new List(); // includes both implicit (not mentionable in source) and explicit destructors + + public DatatypeCtor(IToken tok, string name, [Captured] List formals, Attributes attributes) + : base(tok, name, attributes, false) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(cce.NonNullElements(formals)); + this.Formals = formals; + } + + public string FullName { + get { + Contract.Ensures(Contract.Result() != null); + Contract.Assume(EnclosingDatatype != null); + + return "#" + EnclosingDatatype.FullName + "." + Name; + } + } + } + + /// + /// An ICodeContext is an ICallable or a NoContext. + /// + public interface ICodeContext { + bool IsGhost { get; } + List TypeArgs { get; } + List Ins { get; } + ModuleDefinition EnclosingModule { get; } // to be called only after signature-resolution is complete + bool MustReverify { get; } + string FullSanitizedName { get; } + bool AllowsNontermination { get; } + } + + /// + /// Some declarations have more than one context. For example, a subset type has a constraint + /// (which is a ghost context) and a witness (which may be a compiled context). To distinguish + /// between these two, the declaration is wrapped inside a CodeContextWrapper. + /// + public class CodeContextWrapper : ICodeContext { + protected readonly ICodeContext inner; + private readonly bool isGhostContext; + public CodeContextWrapper(ICodeContext inner, bool isGhostContext) { + this.inner = inner; + this.isGhostContext = isGhostContext; + } + + public bool IsGhost => isGhostContext; + public List TypeArgs => inner.TypeArgs; + public List Ins => inner.Ins; + public ModuleDefinition EnclosingModule => inner.EnclosingModule; + public bool MustReverify => inner.MustReverify; + public string FullSanitizedName => inner.FullSanitizedName; + public bool AllowsNontermination => inner.AllowsNontermination; + + public static ICodeContext Unwrap(ICodeContext codeContext) { + while (codeContext is CodeContextWrapper ccw) { + codeContext = ccw.inner; + } + return codeContext; + } + } + + /// + /// An ICallable is a Function, Method, IteratorDecl, or (less fitting for the name ICallable) RedirectingTypeDecl or DatatypeDecl. + /// + public interface ICallable : ICodeContext { + IToken Tok { get; } + string WhatKind { get; } + string NameRelativeToModule { get; } + Specification Decreases { get; } + /// + /// The InferredDecreases property says whether or not a process was attempted to provide a default decreases + /// clause. If such a process was attempted, even if the resulting decreases clause turned out to be empty, + /// the property will get the value "true". This is so that a useful error message can be provided. + /// + bool InferredDecreases { get; set; } + bool AllowsAllocation { get; } + } + + /// + /// This class allows an ICallable to be treated as ghost/compiled according to the "isGhostContext" + /// parameter. + /// + /// This class is to ICallable what CodeContextWrapper is to ICodeContext. + /// + public class CallableWrapper : CodeContextWrapper, ICallable { + public CallableWrapper(ICallable callable, bool isGhostContext) + : base(callable, isGhostContext) { + } + + protected ICallable cwInner => (ICallable)inner; + public IToken Tok => cwInner.Tok; + public string WhatKind => cwInner.WhatKind; + public string NameRelativeToModule => cwInner.NameRelativeToModule; + public Specification Decreases => cwInner.Decreases; + + public bool InferredDecreases { + get => cwInner.InferredDecreases; + set { cwInner.InferredDecreases = value; } + } + + public bool AllowsAllocation => cwInner.AllowsAllocation; + } + + public class DontUseICallable : ICallable { + public string WhatKind { get { throw new cce.UnreachableException(); } } + public bool IsGhost { get { throw new cce.UnreachableException(); } } + public List TypeArgs { get { throw new cce.UnreachableException(); } } + public List Ins { get { throw new cce.UnreachableException(); } } + public ModuleDefinition EnclosingModule { get { throw new cce.UnreachableException(); } } + public bool MustReverify { get { throw new cce.UnreachableException(); } } + public string FullSanitizedName { get { throw new cce.UnreachableException(); } } + public bool AllowsNontermination { get { throw new cce.UnreachableException(); } } + public IToken Tok { get { throw new cce.UnreachableException(); } } + public string NameRelativeToModule { get { throw new cce.UnreachableException(); } } + public Specification Decreases { get { throw new cce.UnreachableException(); } } + public bool InferredDecreases { + get { throw new cce.UnreachableException(); } + set { throw new cce.UnreachableException(); } + } + public bool AllowsAllocation => throw new cce.UnreachableException(); + } + /// + /// An IMethodCodeContext is a Method or IteratorDecl. + /// + public interface IMethodCodeContext : ICallable { + List Outs { get; } + Specification Modifies { get; } + } + + /// + /// Applies when we are not inside an ICallable. In particular, a NoContext is used to resolve the attributes of declarations with no other context. + /// + public class NoContext : ICodeContext { + public readonly ModuleDefinition Module; + public NoContext(ModuleDefinition module) { + this.Module = module; + } + bool ICodeContext.IsGhost { get { return true; } } + List ICodeContext.TypeArgs { get { return new List(); } } + List ICodeContext.Ins { get { return new List(); } } + ModuleDefinition ICodeContext.EnclosingModule { get { return Module; } } + bool ICodeContext.MustReverify { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } + public string FullSanitizedName { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } + public bool AllowsNontermination { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } + public bool AllowsAllocation => true; + } + + public class IteratorDecl : ClassDecl, IMethodCodeContext { + public override string WhatKind { get { return "iterator"; } } + public readonly List Ins; + public readonly List Outs; + public readonly Specification Reads; + public readonly Specification Modifies; + public readonly Specification Decreases; + public readonly List Requires; + public readonly List Ensures; + public readonly List YieldRequires; + public readonly List YieldEnsures; + public readonly BlockStmt Body; + public bool SignatureIsOmitted { get { return SignatureEllipsis != null; } } + public readonly IToken SignatureEllipsis; + public readonly List OutsFields; + public readonly List OutsHistoryFields; // these are the 'xs' variables + [FilledInDuringResolution] public readonly List DecreasesFields; + [FilledInDuringResolution] public SpecialField Member_Modifies; + [FilledInDuringResolution] public SpecialField Member_Reads; + [FilledInDuringResolution] public SpecialField Member_New; + [FilledInDuringResolution] public Constructor Member_Init; // created during registration phase of resolution; + [FilledInDuringResolution] public Predicate Member_Valid; // created during registration phase of resolution; + [FilledInDuringResolution] public Method Member_MoveNext; // created during registration phase of resolution; + public readonly LocalVariable YieldCountVariable; + + public IteratorDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, + List ins, List outs, + Specification reads, Specification mod, Specification decreases, + List requires, + List ensures, + List yieldRequires, + List yieldEnsures, + BlockStmt body, Attributes attributes, IToken signatureEllipsis) + : base(tok, name, module, typeArgs, new List(), attributes, signatureEllipsis != null, null) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(module != null); + Contract.Requires(typeArgs != null); + Contract.Requires(ins != null); + Contract.Requires(outs != null); + Contract.Requires(reads != null); + Contract.Requires(mod != null); + Contract.Requires(decreases != null); + Contract.Requires(requires != null); + Contract.Requires(ensures != null); + Contract.Requires(yieldRequires != null); + Contract.Requires(yieldEnsures != null); + Ins = ins; + Outs = outs; + Reads = reads; + Modifies = mod; + Decreases = decreases; + Requires = requires; + Ensures = ensures; + YieldRequires = yieldRequires; + YieldEnsures = yieldEnsures; + Body = body; + SignatureEllipsis = signatureEllipsis; + + OutsFields = new List(); + OutsHistoryFields = new List(); + DecreasesFields = new List(); + + YieldCountVariable = new LocalVariable(tok, tok, "_yieldCount", new EverIncreasingType(), true); + YieldCountVariable.type = YieldCountVariable.OptionalType; // resolve YieldCountVariable here + } + + /// + /// Returns the non-null expressions of this declaration proper (that is, do not include the expressions of substatements). + /// Does not include the generated class members. + /// + public virtual IEnumerable SubExpressions { + get { + foreach (var e in Attributes.SubExpressions(Attributes)) { + yield return e; + } + foreach (var e in Attributes.SubExpressions(Reads.Attributes)) { + yield return e; + } + foreach (var e in Reads.Expressions) { + yield return e.E; + } + foreach (var e in Attributes.SubExpressions(Modifies.Attributes)) { + yield return e; + } + foreach (var e in Modifies.Expressions) { + yield return e.E; + } + foreach (var e in Attributes.SubExpressions(Decreases.Attributes)) { + yield return e; + } + foreach (var e in Decreases.Expressions) { + yield return e; + } + foreach (var e in Requires) { + yield return e.E; + } + foreach (var e in Ensures) { + yield return e.E; + } + foreach (var e in YieldRequires) { + yield return e.E; + } + foreach (var e in YieldEnsures) { + yield return e.E; + } + } + } + + /// + /// This Dafny type exists only for the purpose of giving the yield-count variable a type, so + /// that the type can be recognized during translation of Dafny into Boogie. It represents + /// an integer component in a "decreases" clause whose order is (\lambda x,y :: x GREATER y), + /// not the usual (\lambda x,y :: x LESS y AND 0 ATMOST y). + /// + public class EverIncreasingType : BasicType { + [Pure] + public override string TypeName(ModuleDefinition context, bool parseAble) { + Contract.Assert(parseAble == false); + + return "_increasingInt"; + } + public override bool Equals(Type that, bool keepConstraints = false) { + return that.NormalizeExpand(keepConstraints) is EverIncreasingType; + } + } + + bool ICodeContext.IsGhost { get { return false; } } + List ICodeContext.TypeArgs { get { return this.TypeArgs; } } + List ICodeContext.Ins { get { return this.Ins; } } + List IMethodCodeContext.Outs { get { return this.Outs; } } + Specification IMethodCodeContext.Modifies { get { return this.Modifies; } } + IToken ICallable.Tok { get { return this.tok; } } + string ICallable.NameRelativeToModule { get { return this.Name; } } + Specification ICallable.Decreases { get { return this.Decreases; } } + bool _inferredDecr; + bool ICallable.InferredDecreases { + set { _inferredDecr = value; } + get { return _inferredDecr; } + } + + ModuleDefinition ICodeContext.EnclosingModule { get { return this.EnclosingModuleDefinition; } } + bool ICodeContext.MustReverify { get { return false; } } + public bool AllowsNontermination { + get { + return Contract.Exists(Decreases.Expressions, e => e is WildcardExpr); + } + } + } + + public abstract class MemberDecl : Declaration { + public abstract string WhatKind { get; } + public virtual string WhatKindMentionGhost => (IsGhost ? "ghost " : "") + WhatKind; + public readonly bool HasStaticKeyword; + public virtual bool IsStatic { + get { + return HasStaticKeyword || (EnclosingClass is ClassDecl && ((ClassDecl)EnclosingClass).IsDefaultClass); + } + } + protected readonly bool isGhost; + public bool IsGhost { get { return isGhost; } } + + /// + /// The term "instance independent" can be confusing. It means that the constant does not get its value in + /// a constructor. (But the RHS of the const's declaration may mention "this".) + /// + public bool IsInstanceIndependentConstant => this is ConstantField cf && cf.Rhs != null; + + public TopLevelDecl EnclosingClass; // filled in during resolution + [FilledInDuringResolution] public MemberDecl RefinementBase; // filled in during the pre-resolution refinement transformation; null if the member is new here + [FilledInDuringResolution] public MemberDecl OverriddenMember; // non-null if the member overrides a member in a parent trait + public virtual bool IsOverrideThatAddsBody => OverriddenMember != null; + + /// + /// Returns "true" if "this" is a (possibly transitive) override of "possiblyOverriddenMember". + /// + public bool Overrides(MemberDecl possiblyOverriddenMember) { + Contract.Requires(possiblyOverriddenMember != null); + for (var th = this; th != null; th = th.OverriddenMember) { + if (th == possiblyOverriddenMember) { + return true; + } + } + return false; + } + + public MemberDecl(IToken tok, string name, bool hasStaticKeyword, bool isGhost, Attributes attributes, bool isRefining) + : base(tok, name, attributes, isRefining) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + HasStaticKeyword = hasStaticKeyword; + this.isGhost = isGhost; + } + /// + /// Returns className+"."+memberName. Available only after resolution. + /// + public virtual string FullDafnyName { + get { + Contract.Requires(EnclosingClass != null); + Contract.Ensures(Contract.Result() != null); + string n = EnclosingClass.FullDafnyName; + return (n.Length == 0 ? n : (n + ".")) + Name; + } + } + public virtual string FullName { + get { + Contract.Requires(EnclosingClass != null); + Contract.Ensures(Contract.Result() != null); + + return EnclosingClass.FullName + "." + Name; + } + } + + public override string SanitizedName => + (Name == EnclosingClass.Name ? "_" : "") + base.SanitizedName; + + public override string CompileName => + (Name == EnclosingClass.Name ? "_" : "") + base.CompileName; + + public virtual string FullSanitizedName { + get { + Contract.Requires(EnclosingClass != null); + Contract.Ensures(Contract.Result() != null); + + if (Name == "requires") { + return Translator.Requires(((ArrowTypeDecl)EnclosingClass).Arity); + } else if (Name == "reads") { + return Translator.Reads(((ArrowTypeDecl)EnclosingClass).Arity); + } else { + return EnclosingClass.FullSanitizedName + "." + SanitizedName; + } + } + } + + public virtual IEnumerable SubExpressions => Enumerable.Empty(); + } + + public class Field : MemberDecl { + public override string WhatKind => "field"; + public readonly bool IsMutable; // says whether or not the field can ever change values + public readonly bool IsUserMutable; // says whether or not code is allowed to assign to the field (IsUserMutable implies IsMutable) + public readonly Type Type; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Type != null); + Contract.Invariant(!IsUserMutable || IsMutable); // IsUserMutable ==> IsMutable + } + + public Field(IToken tok, string name, bool isGhost, Type type, Attributes attributes) + : this(tok, name, false, isGhost, true, true, type, attributes) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(type != null); + } + + public Field(IToken tok, string name, bool hasStaticKeyword, bool isGhost, bool isMutable, bool isUserMutable, Type type, Attributes attributes) + : base(tok, name, hasStaticKeyword, isGhost, attributes, false) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(type != null); + Contract.Requires(!isUserMutable || isMutable); + IsMutable = isMutable; + IsUserMutable = isUserMutable; + Type = type; + } + } + + public class SpecialFunction : Function, ICodeContext, ICallable { + readonly ModuleDefinition Module; + public SpecialFunction(IToken tok, string name, ModuleDefinition module, bool hasStaticKeyword, bool isGhost, + List typeArgs, List formals, Type resultType, + List req, List reads, List ens, Specification decreases, + Expression body, Attributes attributes, IToken signatureEllipsis) + : base(tok, name, hasStaticKeyword, isGhost, typeArgs, formals, null, resultType, req, reads, ens, decreases, body, null, null, attributes, signatureEllipsis) { + Module = module; + } + ModuleDefinition ICodeContext.EnclosingModule { get { return this.Module; } } + string ICallable.NameRelativeToModule { get { return Name; } } + } + + public class SpecialField : Field { + public enum ID { + UseIdParam, // IdParam is a string + ArrayLength, // IdParam is null for .Length; IdParam is an int "x" for GetLength(x) + ArrayLengthInt, // same as ArrayLength, but produces int instead of BigInteger + Floor, + IsLimit, + IsSucc, + Offset, + IsNat, + Keys, + Values, + Items, + Reads, + Modifies, + New, + } + public readonly ID SpecialId; + public readonly object IdParam; + public SpecialField(IToken tok, string name, ID specialId, object idParam, + bool isGhost, bool isMutable, bool isUserMutable, Type type, Attributes attributes) + : this(tok, name, specialId, idParam, false, isGhost, isMutable, isUserMutable, type, attributes) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(!isUserMutable || isMutable); + Contract.Requires(type != null); + } + + public SpecialField(IToken tok, string name, ID specialId, object idParam, + bool hasStaticKeyword, bool isGhost, bool isMutable, bool isUserMutable, Type type, Attributes attributes) + : base(tok, name, hasStaticKeyword, isGhost, isMutable, isUserMutable, type, attributes) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(!isUserMutable || isMutable); + Contract.Requires(type != null); + + SpecialId = specialId; + IdParam = idParam; + } + + public override string FullName { + get { + Contract.Ensures(Contract.Result() != null); + return EnclosingClass != null ? EnclosingClass.FullName + "." + Name : Name; + } + } + + public override string FullSanitizedName { // Override beacuse EnclosingClass may be null + get { + Contract.Ensures(Contract.Result() != null); + return EnclosingClass != null ? EnclosingClass.FullSanitizedName + "." + SanitizedName : SanitizedName; + } + } + + public override string CompileName { + get { + Contract.Ensures(Contract.Result() != null); + return EnclosingClass != null ? base.CompileName : Name; + } + } + } + + public class DatatypeDestructor : SpecialField { + public readonly List EnclosingCtors = new List(); // is always a nonempty list + public readonly List CorrespondingFormals = new List(); // is always a nonempty list + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(EnclosingCtors != null); + Contract.Invariant(CorrespondingFormals != null); + Contract.Invariant(EnclosingCtors.Count > 0); + Contract.Invariant(EnclosingCtors.Count == CorrespondingFormals.Count); + } + + public DatatypeDestructor(IToken tok, DatatypeCtor enclosingCtor, Formal correspondingFormal, string name, string compiledName, bool isGhost, Type type, Attributes attributes) + : base(tok, name, SpecialField.ID.UseIdParam, compiledName, isGhost, false, false, type, attributes) { + Contract.Requires(tok != null); + Contract.Requires(enclosingCtor != null); + Contract.Requires(correspondingFormal != null); + Contract.Requires(name != null); + Contract.Requires(type != null); + EnclosingCtors.Add(enclosingCtor); // more enclosing constructors may be added later during resolution + CorrespondingFormals.Add(correspondingFormal); // more corresponding formals may be added later during resolution + } + + /// + /// To be called only by the resolver. Called to share this datatype destructor between multiple constructors + /// of the same datatype. + /// + internal void AddAnotherEnclosingCtor(DatatypeCtor ctor, Formal formal) { + Contract.Requires(ctor != null); + Contract.Requires(formal != null); + EnclosingCtors.Add(ctor); // more enclosing constructors may be added later during resolution + CorrespondingFormals.Add(formal); // more corresponding formals may be added later during resolution + } + + internal string EnclosingCtorNames(string grammaticalConjunction) { + Contract.Requires(grammaticalConjunction != null); + return PrintableCtorNameList(EnclosingCtors, grammaticalConjunction); + } + + static internal string PrintableCtorNameList(List ctors, string grammaticalConjunction) { + Contract.Requires(ctors != null); + Contract.Requires(grammaticalConjunction != null); + var n = ctors.Count; + if (n == 1) { + return string.Format("'{0}'", ctors[0].Name); + } else if (n == 2) { + return string.Format("'{0}' {1} '{2}'", ctors[0].Name, grammaticalConjunction, ctors[1].Name); + } else { + var s = ""; + for (int i = 0; i < n - 1; i++) { + s += string.Format("'{0}', ", ctors[i].Name); + } + return s + string.Format("{0} '{1}'", grammaticalConjunction, ctors[n - 1].Name); + } + } + } + + public class ConstantField : SpecialField, ICallable { + public override string WhatKind => "const field"; + public readonly Expression Rhs; + public ConstantField(IToken tok, string name, Expression/*?*/ rhs, bool hasStaticKeyword, bool isGhost, Type type, Attributes attributes) + : base(tok, name, SpecialField.ID.UseIdParam, NonglobalVariable.SanitizeName(name), hasStaticKeyword, isGhost, false, false, type, attributes) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(type != null); + this.Rhs = rhs; + } + + public override bool CanBeRevealed() { + return true; + } + + // + public new bool IsGhost { get { return this.isGhost; } } + public List TypeArgs { get { return new List(); } } + public List Ins { get { return new List(); } } + public ModuleDefinition EnclosingModule { get { return this.EnclosingClass.EnclosingModuleDefinition; } } + public bool MustReverify { get { return false; } } + public bool AllowsNontermination { get { throw new cce.UnreachableException(); } } + public IToken Tok { get { return tok; } } + public string NameRelativeToModule { + get { + if (EnclosingClass is DefaultClassDecl) { + return Name; + } else { + return EnclosingClass.Name + "." + Name; + } + } + } + public Specification Decreases { get { throw new cce.UnreachableException(); } } + public bool InferredDecreases { + get { throw new cce.UnreachableException(); } + set { throw new cce.UnreachableException(); } + } + public bool AllowsAllocation => true; + } + + public class OpaqueTypeDecl : TopLevelDeclWithMembers, TypeParameter.ParentType, RevealableTypeDecl { + public override string WhatKind { get { return "opaque type"; } } + public override bool CanBeRevealed() { return true; } + public readonly TypeParameter.TypeParameterCharacteristics Characteristics; + public bool SupportsEquality { + get { return Characteristics.EqualitySupport != TypeParameter.EqualitySupportValue.Unspecified; } + } + + public OpaqueTypeDecl(IToken tok, string name, ModuleDefinition module, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, List members, Attributes attributes, bool isRefining) + : base(tok, name, module, typeArgs, members, attributes, isRefining) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(module != null); + Contract.Requires(typeArgs != null); + Characteristics = characteristics; + this.NewSelfSynonym(); + } + + public TopLevelDecl AsTopLevelDecl => this; + public TypeDeclSynonymInfo SynonymInfo { get; set; } + } + + public interface RedirectingTypeDecl : ICallable { + string Name { get; } + + IToken tok { get; } + Attributes Attributes { get; } + ModuleDefinition Module { get; } + BoundVar/*?*/ Var { get; } + Expression/*?*/ Constraint { get; } + SubsetTypeDecl.WKind WitnessKind { get; } + Expression/*?*/ Witness { get; } // non-null iff WitnessKind is Compiled or Ghost + FreshIdGenerator IdGenerator { get; } + } + + public class NativeType { + public readonly string Name; + public readonly BigInteger LowerBound; + public readonly BigInteger UpperBound; + public readonly int Bitwidth; // for unassigned types, this shows the number of bits in the type; else is 0 + public enum Selection { Byte, SByte, UShort, Short, UInt, Int, Number, ULong, Long } + public readonly Selection Sel; + public NativeType(string Name, BigInteger LowerBound, BigInteger UpperBound, int bitwidth, Selection sel) { + Contract.Requires(Name != null); + Contract.Requires(0 <= bitwidth && (bitwidth == 0 || LowerBound == 0)); + this.Name = Name; + this.LowerBound = LowerBound; + this.UpperBound = UpperBound; + this.Bitwidth = bitwidth; + this.Sel = sel; + } + } + + public class TypeDeclSynonymInfo { + public readonly InternalTypeSynonymDecl SelfSynonymDecl; + + public TypeDeclSynonymInfo(TopLevelDecl d) { + var thisType = UserDefinedType.FromTopLevelDecl(d.tok, d); + SelfSynonymDecl = new InternalTypeSynonymDecl(d.tok, d.Name, TypeParameter.GetExplicitCharacteristics(d), + d.TypeArgs, d.EnclosingModuleDefinition, thisType, d.Attributes); + SelfSynonymDecl.InheritVisibility(d, false); + } + + public UserDefinedType SelfSynonym(List args, Expression /*?*/ namePath = null) { + return new UserDefinedType(SelfSynonymDecl.tok, SelfSynonymDecl.Name, SelfSynonymDecl, args, namePath); + } + } + + public static class RevealableTypeDeclHelper { + public static InternalTypeSynonymDecl SelfSynonymDecl(this RevealableTypeDecl rtd) => + rtd.SynonymInfo.SelfSynonymDecl; + + public static UserDefinedType SelfSynonym(this RevealableTypeDecl rtd, List args, Expression /*?*/ namePath = null) => + rtd.SynonymInfo.SelfSynonym(args, namePath); + + //Internal implementations are called before extensions, so this is safe + public static bool IsRevealedInScope(this RevealableTypeDecl rtd, VisibilityScope scope) => + rtd.AsTopLevelDecl.IsRevealedInScope(scope); + + public static void NewSelfSynonym(this RevealableTypeDecl rtd) { + rtd.SynonymInfo = new TypeDeclSynonymInfo(rtd.AsTopLevelDecl); + } + } + + public interface RevealableTypeDecl { + TopLevelDecl AsTopLevelDecl { get; } + TypeDeclSynonymInfo SynonymInfo { get; set; } + } + + public class NewtypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, RedirectingTypeDecl { + public override string WhatKind { get { return "newtype"; } } + public override bool CanBeRevealed() { return true; } + public Type BaseType { get; set; } // null when refining + public BoundVar Var { get; set; } // can be null (if non-null, then object.ReferenceEquals(Var.Type, BaseType)) + public Expression Constraint { get; set; } // is null iff Var is + public SubsetTypeDecl.WKind WitnessKind { get; set; } = SubsetTypeDecl.WKind.CompiledZero; + public Expression/*?*/ Witness { get; set; } // non-null iff WitnessKind is Compiled or Ghost + [FilledInDuringResolution] public NativeType NativeType; // non-null for fixed-size representations (otherwise, use BigIntegers for integers) + public NewtypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, List members, Attributes attributes, bool isRefining) + : base(tok, name, module, new List(), members, attributes, isRefining) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(module != null); + Contract.Requires(isRefining ^ (baseType != null)); + Contract.Requires(members != null); + BaseType = baseType; + } + public NewtypeDecl(IToken tok, string name, ModuleDefinition module, BoundVar bv, Expression constraint, SubsetTypeDecl.WKind witnessKind, Expression witness, List members, Attributes attributes, bool isRefining) + : base(tok, name, module, new List(), members, attributes, isRefining) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(module != null); + Contract.Requires(bv != null && bv.Type != null); + Contract.Requires((witnessKind == SubsetTypeDecl.WKind.Compiled || witnessKind == SubsetTypeDecl.WKind.Ghost) == (witness != null)); + Contract.Requires(members != null); + BaseType = bv.Type; + Var = bv; + Constraint = constraint; + Witness = witness; + WitnessKind = witnessKind; + this.NewSelfSynonym(); + } + + public TopLevelDecl AsTopLevelDecl => this; + public TypeDeclSynonymInfo SynonymInfo { get; set; } + + public TypeParameter.EqualitySupportValue EqualitySupport { + get { + if (this.BaseType.SupportsEquality) { + return TypeParameter.EqualitySupportValue.Required; + } else { + return TypeParameter.EqualitySupportValue.Unspecified; + } + } + } + + string RedirectingTypeDecl.Name { get { return Name; } } + IToken RedirectingTypeDecl.tok { get { return tok; } } + Attributes RedirectingTypeDecl.Attributes { get { return Attributes; } } + ModuleDefinition RedirectingTypeDecl.Module { get { return EnclosingModuleDefinition; } } + BoundVar RedirectingTypeDecl.Var { get { return Var; } } + Expression RedirectingTypeDecl.Constraint { get { return Constraint; } } + SubsetTypeDecl.WKind RedirectingTypeDecl.WitnessKind { get { return WitnessKind; } } + Expression RedirectingTypeDecl.Witness { get { return Witness; } } + FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } } + + bool ICodeContext.IsGhost { + get { throw new NotSupportedException(); } // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper + } + List ICodeContext.TypeArgs { get { return new List(); } } + List ICodeContext.Ins { get { return new List(); } } + ModuleDefinition ICodeContext.EnclosingModule { get { return EnclosingModuleDefinition; } } + bool ICodeContext.MustReverify { get { return false; } } + bool ICodeContext.AllowsNontermination { get { return false; } } + IToken ICallable.Tok { get { return tok; } } + string ICallable.NameRelativeToModule { get { return Name; } } + Specification ICallable.Decreases { + get { + // The resolver checks that a NewtypeDecl sits in its own SSC in the call graph. Therefore, + // the question of what its Decreases clause is should never arise. + throw new cce.UnreachableException(); + } + } + bool ICallable.InferredDecreases { + get { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases + set { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases + } + } + + public abstract class TypeSynonymDeclBase : TopLevelDecl, RedirectingTypeDecl { + public override string WhatKind { get { return "type synonym"; } } + public TypeParameter.TypeParameterCharacteristics Characteristics; // the resolver may change the .EqualitySupport component of this value from Unspecified to InferredRequired (for some signatures that may immediately imply that equality support is required) + public bool SupportsEquality { + get { return Characteristics.EqualitySupport != TypeParameter.EqualitySupportValue.Unspecified; } + } + public readonly Type Rhs; + public TypeSynonymDeclBase(IToken tok, string name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, Type rhs, Attributes attributes) + : base(tok, name, module, typeArgs, attributes, false) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(typeArgs != null); + Contract.Requires(module != null); + Contract.Requires(rhs != null); + Characteristics = characteristics; + Rhs = rhs; + } + /// + /// Return .Rhs instantiated with "typeArgs", but only look at the part of .Rhs that is in scope. + /// + public Type RhsWithArgument(List typeArgs) { + Contract.Requires(typeArgs != null); + Contract.Requires(typeArgs.Count == TypeArgs.Count); + var scope = Type.GetScope(); + var rtd = Rhs.AsRevealableType; + if (rtd != null) { + Contract.Assume(rtd.AsTopLevelDecl.IsVisibleInScope(scope)); + if (!rtd.IsRevealedInScope(scope)) { + // type is actually hidden in this scope + return rtd.SelfSynonym(typeArgs); + } + } + return RhsWithArgumentIgnoringScope(typeArgs); + } + /// + /// Returns the declared .Rhs but with formal type arguments replaced by the given actuals. + /// + public Type RhsWithArgumentIgnoringScope(List typeArgs) { + Contract.Requires(typeArgs != null); + Contract.Requires(typeArgs.Count == TypeArgs.Count); + // Instantiate with the actual type arguments + if (typeArgs.Count == 0) { + // this optimization seems worthwhile + return Rhs; + } else { + var subst = Resolver.TypeSubstitutionMap(TypeArgs, typeArgs); + return Resolver.SubstType(Rhs, subst); + } + } + + string RedirectingTypeDecl.Name { get { return Name; } } + IToken RedirectingTypeDecl.tok { get { return tok; } } + Attributes RedirectingTypeDecl.Attributes { get { return Attributes; } } + ModuleDefinition RedirectingTypeDecl.Module { get { return EnclosingModuleDefinition; } } + BoundVar RedirectingTypeDecl.Var { get { return null; } } + Expression RedirectingTypeDecl.Constraint { get { return null; } } + SubsetTypeDecl.WKind RedirectingTypeDecl.WitnessKind { get { return SubsetTypeDecl.WKind.CompiledZero; } } + Expression RedirectingTypeDecl.Witness { get { return null; } } + FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } } + + bool ICodeContext.IsGhost { + get { throw new NotSupportedException(); } // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper + } + List ICodeContext.TypeArgs { get { return TypeArgs; } } + List ICodeContext.Ins { get { return new List(); } } + ModuleDefinition ICodeContext.EnclosingModule { get { return EnclosingModuleDefinition; } } + bool ICodeContext.MustReverify { get { return false; } } + bool ICodeContext.AllowsNontermination { get { return false; } } + IToken ICallable.Tok { get { return tok; } } + string ICallable.NameRelativeToModule { get { return Name; } } + Specification ICallable.Decreases { + get { + // The resolver checks that a NewtypeDecl sits in its own SSC in the call graph. Therefore, + // the question of what its Decreases clause is should never arise. + throw new cce.UnreachableException(); + } + } + bool ICallable.InferredDecreases { + get { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases + set { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases + } + public override bool CanBeRevealed() { + return true; + } + } + + public class TypeSynonymDecl : TypeSynonymDeclBase, RedirectingTypeDecl, RevealableTypeDecl { + public TypeSynonymDecl(IToken tok, string name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, Type rhs, Attributes attributes) + : base(tok, name, characteristics, typeArgs, module, rhs, attributes) { + this.NewSelfSynonym(); + } + public TopLevelDecl AsTopLevelDecl => this; + public TypeDeclSynonymInfo SynonymInfo { get; set; } + } + + public class InternalTypeSynonymDecl : TypeSynonymDeclBase, RedirectingTypeDecl { + public InternalTypeSynonymDecl(IToken tok, string name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, Type rhs, Attributes attributes) + : base(tok, name, characteristics, typeArgs, module, rhs, attributes) { + } + } + + + public class SubsetTypeDecl : TypeSynonymDecl, RedirectingTypeDecl { + public override string WhatKind { get { return "subset type"; } } + public readonly BoundVar Var; + public readonly Expression Constraint; + public enum WKind { CompiledZero, Compiled, Ghost, OptOut, Special } + public readonly SubsetTypeDecl.WKind WitnessKind; + public readonly Expression/*?*/ Witness; // non-null iff WitnessKind is Compiled or Ghost + [FilledInDuringResolution] public bool ConstraintIsCompilable; + [FilledInDuringResolution] public bool CheckedIfConstraintIsCompilable = false; // Set to true lazily by the Resolver when the Resolver fills in "ConstraintIsCompilable". + public SubsetTypeDecl(IToken tok, string name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, + BoundVar id, Expression constraint, WKind witnessKind, Expression witness, + Attributes attributes) + : base(tok, name, characteristics, typeArgs, module, id.Type, attributes) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(typeArgs != null); + Contract.Requires(module != null); + Contract.Requires(id != null && id.Type != null); + Contract.Requires(constraint != null); + Contract.Requires((witnessKind == WKind.Compiled || witnessKind == WKind.Ghost) == (witness != null)); + Var = id; + Constraint = constraint; + Witness = witness; + WitnessKind = witnessKind; + } + BoundVar RedirectingTypeDecl.Var { get { return Var; } } + Expression RedirectingTypeDecl.Constraint { get { return Constraint; } } + WKind RedirectingTypeDecl.WitnessKind { get { return WitnessKind; } } + Expression RedirectingTypeDecl.Witness { get { return Witness; } } + + public override List ParentTypes(List typeArgs) { + return new List { RhsWithArgument(typeArgs) }; + } + } + + public class NonNullTypeDecl : SubsetTypeDecl { + public override string WhatKind { get { return "non-null type"; } } + public readonly ClassDecl Class; + /// + /// The public constructor is NonNullTypeDecl(ClassDecl cl). The rest is pretty crazy: There are stages of "this"-constructor calls + /// in order to build values that depend on previously computed parameters. + /// + public NonNullTypeDecl(ClassDecl cl) + : this(cl, cl.TypeArgs.ConvertAll(tp => new TypeParameter(tp.tok, tp.Name, tp.VarianceSyntax, tp.Characteristics))) { + Contract.Requires(cl != null); + } + + private NonNullTypeDecl(ClassDecl cl, List tps) + : this(cl, tps, + new BoundVar(cl.tok, "c", new UserDefinedType(cl.tok, cl.Name + "?", tps.Count == 0 ? null : tps.ConvertAll(tp => (Type)new UserDefinedType(tp))))) { + Contract.Requires(cl != null); + Contract.Requires(tps != null); + } + + private NonNullTypeDecl(ClassDecl cl, List tps, BoundVar id) + : base(cl.tok, cl.Name, new TypeParameter.TypeParameterCharacteristics(), tps, cl.EnclosingModuleDefinition, id, + new BinaryExpr(cl.tok, BinaryExpr.Opcode.Neq, new IdentifierExpr(cl.tok, id), new LiteralExpr(cl.tok)), + SubsetTypeDecl.WKind.Special, null, BuiltIns.AxiomAttribute()) { + Contract.Requires(cl != null); + Contract.Requires(tps != null); + Contract.Requires(id != null); + Class = cl; + } + + public override List ParentTypes(List typeArgs) { + List result = new List(base.ParentTypes(typeArgs)); + + foreach (var rhsParentType in Class.ParentTypes(typeArgs)) { + var rhsParentUdt = (UserDefinedType)rhsParentType; // all parent types of .Class are expected to be possibly-null class types + Contract.Assert(rhsParentUdt.ResolvedClass is ClassDecl); + result.Add(UserDefinedType.CreateNonNullType(rhsParentUdt)); + } + + return result; + } + } + + [ContractClass(typeof(IVariableContracts))] + public interface IVariable { + string Name { + get; + } + string DisplayName { // what the user thinks he wrote + get; + } + string UniqueName { + get; + } + bool HasBeenAssignedUniqueName { // unique names are not assigned until the Translator; if you don't already know if that stage has run, this boolean method will tell you + get; + } + static FreshIdGenerator CompileNameIdGenerator = new FreshIdGenerator(); + string AssignUniqueName(FreshIdGenerator generator); + string SanitizedName { + get; + } + string CompileName { + get; + } + Type Type { + get; + } + Type OptionalType { + get; + } + bool IsMutable { + get; + } + bool IsGhost { + get; + } + void MakeGhost(); + IToken Tok { + get; + } + } + [ContractClassFor(typeof(IVariable))] + public abstract class IVariableContracts : IVariable { + public string Name { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here + } + } + public string DisplayName { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here + } + } + public string UniqueName { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here + } + } + public bool HasBeenAssignedUniqueName { + get { + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here + } + } + public string SanitizedName { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here + } + } + public string CompileName { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here + } + } + public Type Type { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here + } + } + public Type OptionalType { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here + } + } + public bool IsMutable { + get { + throw new NotImplementedException(); + } + } + public bool IsGhost { + get { + throw new NotImplementedException(); + } + } + public void MakeGhost() { + throw new NotImplementedException(); + } + public IToken Tok { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } + public string AssignUniqueName(FreshIdGenerator generator) { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } + + public abstract class NonglobalVariable : IVariable { + public readonly IToken tok; + readonly string name; + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(tok != null); + Contract.Invariant(name != null); + Contract.Invariant(type != null); + } + + public string Name { + get { + Contract.Ensures(Contract.Result() != null); + return name; + } + } + public string DisplayName => + LocalVariable.DisplayNameHelper(this); + + private string uniqueName; + public string UniqueName => uniqueName; + public bool HasBeenAssignedUniqueName => uniqueName != null; + public string AssignUniqueName(FreshIdGenerator generator) { + return uniqueName ??= generator.FreshId(Name + "#"); + } + + static char[] specialChars = { '\'', '_', '?', '\\', '#' }; + /// + /// Mangle name nm by replacing and escaping characters most likely to cause issues when compiling and + /// when translating to Boogie. This transformation is injective. + /// + /// A string uniquely determined from nm, containing none of the characters in + /// specialChars. + public static string SanitizeName(string nm) { + if ('0' <= nm[0] && nm[0] <= '9') { + // the identifier is one that consists of just digits + return "_" + nm; + } + string name = null; + int i = 0; + while (true) { + int j = nm.IndexOfAny(specialChars, i); + if (j == -1) { + if (i == 0) { + return nm; // this is the common case + } else { + return name + nm.Substring(i); + } + } else { + string nxt = nm.Substring(i, j - i); + name = name == null ? nxt : name + nxt; + switch (nm[j]) { + case '\'': name += "_k"; break; + case '_': name += "__"; break; + case '?': name += "_q"; break; + case '\\': name += "_b"; break; + case '#': name += "_h"; break; + default: + Contract.Assume(false); // unexpected character + break; + } + i = j + 1; + if (i == nm.Length) { + return name; + } + } + } + } + + private string sanitizedName; + public virtual string SanitizedName => + sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizeName(Name)}"; + + protected string compileName; + public virtual string CompileName => + compileName ??= SanitizedName; + + Type type; + public Type SyntacticType { get { return type; } } // returns the non-normalized type + public Type Type { + get { + Contract.Ensures(Contract.Result() != null); + return type.Normalize(); + } + } + Type IVariable.OptionalType { + get { return Type; } // same as Type for NonglobalVariable + } + public abstract bool IsMutable { + get; + } + bool isGhost; // readonly after resolution + public bool IsGhost { + get { + return isGhost; + } + set { + isGhost = value; + } + } + public void MakeGhost() { + IsGhost = true; + } + public IToken Tok { + get { + return tok; + } + } + + public NonglobalVariable(IToken tok, string name, Type type, bool isGhost) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(type != null); + this.tok = tok; + this.name = name; + this.type = type; + this.isGhost = isGhost; + } + } + + public class Formal : NonglobalVariable { + public readonly bool InParam; // true to in-parameter, false for out-parameter + public override bool IsMutable { + get { + return !InParam; + } + } + public readonly bool IsOld; + public readonly Expression DefaultValue; + public readonly bool IsNameOnly; + public readonly bool IsOlder; + public readonly string NameForCompilation; + + public Formal(IToken tok, string name, Type type, bool inParam, bool isGhost, Expression defaultValue, + bool isOld = false, bool isNameOnly = false, bool isOlder = false, string nameForCompilation = null) + : base(tok, name, type, isGhost) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(type != null); + Contract.Requires(inParam || defaultValue == null); + Contract.Requires(!isNameOnly || (inParam && !name.StartsWith("#"))); + InParam = inParam; + IsOld = isOld; + DefaultValue = defaultValue; + IsNameOnly = isNameOnly; + IsOlder = isOlder; + NameForCompilation = nameForCompilation ?? name; + } + + public bool HasName { + get { + return !Name.StartsWith("#"); + } + } + + private string sanitizedName; + public override string SanitizedName => + sanitizedName ??= SanitizeName(Name); // No unique-ification + public override string CompileName => + compileName ??= SanitizeName(NameForCompilation); + } + + /// + /// An ImplicitFormal is a parameter that is declared implicitly, in particular the "_k" depth parameter + /// of each extreme lemma (for use in the extreme-method body only, not the specification). + /// + public class ImplicitFormal : Formal { + public ImplicitFormal(IToken tok, string name, Type type, bool inParam, bool isGhost) + : base(tok, name, type, inParam, isGhost, null) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(type != null); + } + } + + /// + /// ThisSurrogate represents the implicit parameter "this". It is used to allow more uniform handling of + /// parameters. A pointer value of a ThisSurrogate object is not important, only the fact that it is + /// a ThisSurrogate is. ThisSurrogate objects are only used in specially marked places in the Dafny + /// implementation. + /// + public class ThisSurrogate : ImplicitFormal { + public ThisSurrogate(IToken tok, Type type) + : base(tok, "this", type, true, false) { + Contract.Requires(tok != null); + Contract.Requires(type != null); + } + } + + [DebuggerDisplay("Bound<{name}>")] + public class BoundVar : NonglobalVariable { + public override bool IsMutable { + get { + return false; + } + } + + public BoundVar(IToken tok, string name, Type type) + : base(tok, name, type, false) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(type != null); + } + } + + /// + /// A QuantifiedVar is a bound variable used in a quantifier such as "forall x :: ...", + /// a comprehension such as "set x | 0 <= x < 10", etc. + /// In addition to its type, which may be inferred, it can have an optional domain collection expression + /// (x <- C) and an optional range boolean expressions (x | E). + /// + [DebuggerDisplay("Quantified<{name}>")] + public class QuantifiedVar : BoundVar { + public readonly Expression Domain; + public readonly Expression Range; + + public QuantifiedVar(IToken tok, string name, Type type, Expression domain, Expression range) + : base(tok, name, type) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(type != null); + Domain = domain; + Range = range; + } + + /// + /// Map a list of quantified variables to an eqivalent list of bound variables plus a single range expression. + /// The transformation looks like this in general: + /// + /// x1 <- C1 | E1, ..., xN <- CN | EN + /// + /// becomes: + /// + /// x1, ... xN | x1 in C1 && E1 && ... && xN in CN && EN + /// + /// Note the result will be null rather than "true" if there are no such domains or ranges. + /// Some quantification contexts (such as comprehensions) will replace this with "true". + /// + public static void ExtractSingleRange(List qvars, out List bvars, out Expression range) { + bvars = new List(); + range = null; + + foreach (var qvar in qvars) { + BoundVar bvar = new BoundVar(qvar.tok, qvar.Name, qvar.SyntacticType); + bvars.Add(bvar); + + if (qvar.Domain != null) { + // Attach a token wrapper so we can produce a better error message if the domain is not a collection + var domainWithToken = QuantifiedVariableDomainCloner.Instance.CloneExpr(qvar.Domain); + var inDomainExpr = new BinaryExpr(domainWithToken.tok, BinaryExpr.Opcode.In, new IdentifierExpr(bvar.tok, bvar), domainWithToken); + range = range == null ? inDomainExpr : new BinaryExpr(domainWithToken.tok, BinaryExpr.Opcode.And, range, inDomainExpr); + } + + if (qvar.Range != null) { + // Attach a token wrapper so we can produce a better error message if the range is not a boolean expression + var rangeWithToken = QuantifiedVariableRangeCloner.Instance.CloneExpr(qvar.Range); + range = range == null ? qvar.Range : new BinaryExpr(rangeWithToken.tok, BinaryExpr.Opcode.And, range, rangeWithToken); + } + } + } + } + + public class ActualBinding { + public readonly IToken /*?*/ FormalParameterName; + public readonly Expression Actual; + public readonly bool IsGhost; + + public ActualBinding(IToken /*?*/ formalParameterName, Expression actual, bool isGhost = false) { + Contract.Requires(actual != null); + FormalParameterName = formalParameterName; + Actual = actual; + IsGhost = isGhost; + } + } + + public class ActualBindings { + public readonly List ArgumentBindings; + + public ActualBindings(List argumentBindings) { + Contract.Requires(argumentBindings != null); + ArgumentBindings = argumentBindings; + } + + public ActualBindings(List actuals) { + Contract.Requires(actuals != null); + ArgumentBindings = actuals.ConvertAll(actual => new ActualBinding(null, actual)); + } + + private List arguments; // set by ResolveActualParameters during resolution + + public bool WasResolved => arguments != null; + + public List Arguments { + get { + Contract.Requires(WasResolved); + return arguments; + } + } + + public void AcceptArgumentExpressionsAsExactParameterList(List args = null) { + Contract.Requires(!WasResolved); // this operation should be done at most once + Contract.Assume(ArgumentBindings.TrueForAll(arg => arg.Actual.WasResolved())); + arguments = args ?? ArgumentBindings.ConvertAll(binding => binding.Actual); + } + } + + public class Function : MemberDecl, TypeParameter.ParentType, ICallable { + public override string WhatKind => "function"; + + public string FunctionDeclarationKeywords { + get { + string k; + if (this is TwoStateFunction || this is ExtremePredicate || this.ByMethodBody != null) { + k = WhatKind; + } else if (this is PrefixPredicate) { + k = "predicate"; + } else if (DafnyOptions.O.FunctionSyntax == DafnyOptions.FunctionSyntaxOptions.ExperimentalPredicateAlwaysGhost && + (this is Predicate || !IsGhost)) { + k = WhatKind; + } else if (DafnyOptions.O.FunctionSyntax != DafnyOptions.FunctionSyntaxOptions.Version4 && !IsGhost) { + k = WhatKind + " method"; + } else if (DafnyOptions.O.FunctionSyntax != DafnyOptions.FunctionSyntaxOptions.Version3 && IsGhost) { + k = "ghost " + WhatKind; + } else { + k = WhatKind; + } + return HasStaticKeyword ? "static " + k : k; + } + } + + public override bool CanBeRevealed() { return true; } + [FilledInDuringResolution] public bool IsRecursive; + [FilledInDuringResolution] public TailStatus TailRecursion = TailStatus.NotTailRecursive; // NotTailRecursive = no tail recursion; TriviallyTailRecursive is never used here + public bool IsTailRecursive => TailRecursion != TailStatus.NotTailRecursive; + public bool IsAccumulatorTailRecursive => IsTailRecursive && TailRecursion != Function.TailStatus.TailRecursive; + [FilledInDuringResolution] public bool IsFueled; // if anyone tries to adjust this function's fuel + public readonly List TypeArgs; + public readonly List Formals; + public readonly Formal Result; + public readonly Type ResultType; + public readonly List Req; + public readonly List Reads; + public readonly List Ens; + public readonly Specification Decreases; + public Expression Body; // an extended expression; Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution + public IToken/*?*/ ByMethodTok; // null iff ByMethodBody is null + public BlockStmt/*?*/ ByMethodBody; + [FilledInDuringResolution] public Method/*?*/ ByMethodDecl; // if ByMethodBody is non-null + public bool SignatureIsOmitted { get { return SignatureEllipsis != null; } } // is "false" for all Function objects that survive into resolution + public readonly IToken SignatureEllipsis; + public Function OverriddenFunction; + public Function Original => OverriddenFunction == null ? this : OverriddenFunction.Original; + public override bool IsOverrideThatAddsBody => base.IsOverrideThatAddsBody && Body != null; + public bool AllowsAllocation => true; + + public bool containsQuantifier; + public bool ContainsQuantifier { + set { containsQuantifier = value; } + get { return containsQuantifier; } + } + + public enum TailStatus { + TriviallyTailRecursive, // contains no recursive calls (in non-ghost expressions) + TailRecursive, // all recursive calls (in non-ghost expressions) are tail calls + NotTailRecursive, // contains some non-ghost recursive call outside of a tail-call position + // E + F or F + E, where E has no tail call and F is a tail call + Accumulate_Add, + AccumulateRight_Sub, + Accumulate_Mul, + Accumulate_SetUnion, + AccumulateRight_SetDifference, + Accumulate_MultiSetUnion, + AccumulateRight_MultiSetDifference, + AccumulateLeft_Concat, + AccumulateRight_Concat, + } + + public override IEnumerable SubExpressions { + get { + foreach (var formal in Formals.Where(f => f.DefaultValue != null)) { + yield return formal.DefaultValue; + } + foreach (var e in Req) { + yield return e.E; + } + foreach (var e in Reads) { + yield return e.E; + } + foreach (var e in Ens) { + yield return e.E; + } + foreach (var e in Decreases.Expressions) { + yield return e; + } + if (Body != null) { + yield return Body; + } + } + } + + public Type GetMemberType(ArrowTypeDecl atd) { + Contract.Requires(atd != null); + Contract.Requires(atd.Arity == Formals.Count); + + // Note, the following returned type can contain type parameters from the function and its enclosing class + return new ArrowType(tok, atd, Formals.ConvertAll(f => f.Type), ResultType); + } + + public bool AllowsNontermination { + get { + return Contract.Exists(Decreases.Expressions, e => e is WildcardExpr); + } + } + + /// + /// The "AllCalls" field is used for non-ExtremePredicate, non-PrefixPredicate functions only (so its value should not be relied upon for ExtremePredicate and PrefixPredicate functions). + /// It records all function calls made by the Function, including calls made in the body as well as in the specification. + /// The field is filled in during resolution (and used toward the end of resolution, to attach a helpful "decreases" prefix to functions in clusters + /// with co-recursive calls. + /// + public readonly List AllCalls = new List(); + public enum CoCallClusterInvolvement { + None, // the SCC containing the function does not involve any co-recursive calls + IsMutuallyRecursiveTarget, // the SCC contains co-recursive calls, and this function is the target of some non-self recursive call + CoRecursiveTargetAllTheWay, // the SCC contains co-recursive calls, and this function is the target only of self-recursive calls and co-recursive calls + } + public CoCallClusterInvolvement CoClusterTarget = CoCallClusterInvolvement.None; + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(TypeArgs)); + Contract.Invariant(cce.NonNullElements(Formals)); + Contract.Invariant(ResultType != null); + Contract.Invariant(cce.NonNullElements(Req)); + Contract.Invariant(cce.NonNullElements(Reads)); + Contract.Invariant(cce.NonNullElements(Ens)); + Contract.Invariant(Decreases != null); + } + + public Function(IToken tok, string name, bool hasStaticKeyword, bool isGhost, + List typeArgs, List formals, Formal result, Type resultType, + List req, List reads, List ens, Specification decreases, + Expression/*?*/ body, IToken/*?*/ byMethodTok, BlockStmt/*?*/ byMethodBody, + Attributes attributes, IToken/*?*/ signatureEllipsis) + : base(tok, name, hasStaticKeyword, isGhost, attributes, signatureEllipsis != null) { + + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cce.NonNullElements(formals)); + Contract.Requires(resultType != null); + Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(cce.NonNullElements(reads)); + Contract.Requires(cce.NonNullElements(ens)); + Contract.Requires(decreases != null); + Contract.Requires(byMethodBody == null || (!isGhost && body != null)); // function-by-method has a ghost expr and non-ghost stmt, but to callers appears like a functiion-method + this.IsFueled = false; // Defaults to false. Only set to true if someone mentions this function in a fuel annotation + this.TypeArgs = typeArgs; + this.Formals = formals; + this.Result = result; + this.ResultType = result != null ? result.Type : resultType; + this.Req = req; + this.Reads = reads; + this.Ens = ens; + this.Decreases = decreases; + this.Body = body; + this.ByMethodTok = byMethodTok; + this.ByMethodBody = byMethodBody; + this.SignatureEllipsis = signatureEllipsis; + + if (attributes != null) { + List args = Attributes.FindExpressions(attributes, "fuel"); + if (args != null) { + if (args.Count == 1) { + LiteralExpr literal = args[0] as LiteralExpr; + if (literal != null && literal.Value is BigInteger) { + this.IsFueled = true; + } + } else if (args.Count == 2) { + LiteralExpr literalLow = args[0] as LiteralExpr; + LiteralExpr literalHigh = args[1] as LiteralExpr; + + if (literalLow != null && literalLow.Value is BigInteger && literalHigh != null && literalHigh.Value is BigInteger) { + this.IsFueled = true; + } + } + } + } + } + + bool ICodeContext.IsGhost { get { return this.IsGhost; } } + List ICodeContext.TypeArgs { get { return this.TypeArgs; } } + List ICodeContext.Ins { get { return this.Formals; } } + IToken ICallable.Tok { get { return this.tok; } } + string ICallable.NameRelativeToModule { + get { + if (EnclosingClass is DefaultClassDecl) { + return Name; + } else { + return EnclosingClass.Name + "." + Name; + } + } + } + Specification ICallable.Decreases { get { return this.Decreases; } } + bool _inferredDecr; + bool ICallable.InferredDecreases { + set { _inferredDecr = value; } + get { return _inferredDecr; } + } + ModuleDefinition ICodeContext.EnclosingModule { get { return this.EnclosingClass.EnclosingModuleDefinition; } } + bool ICodeContext.MustReverify { get { return false; } } + + [Pure] + public bool IsFuelAware() { return IsRecursive || IsFueled || (OverriddenFunction != null && OverriddenFunction.IsFuelAware()); } + public virtual bool ReadsHeap { get { return Reads.Count != 0; } } + } + + public class Predicate : Function { + public override string WhatKind => "predicate"; + public enum BodyOriginKind { + OriginalOrInherited, // this predicate definition is new (and the predicate may or may not have a body), or the predicate's body (whether or not it exists) is being inherited unmodified (from the previous refinement--it may be that the inherited body was itself an extension, for example) + DelayedDefinition, // this predicate declaration provides, for the first time, a body--the declaration refines a previously declared predicate, but the previous one had no body + Extension // this predicate extends the definition of a predicate with a body in a module being refined + } + public readonly BodyOriginKind BodyOrigin; + public Predicate(IToken tok, string name, bool hasStaticKeyword, bool isGhost, + List typeArgs, List formals, + Formal result, + List req, List reads, List ens, Specification decreases, + Expression body, BodyOriginKind bodyOrigin, IToken/*?*/ byMethodTok, BlockStmt/*?*/ byMethodBody, Attributes attributes, IToken signatureEllipsis) + : base(tok, name, hasStaticKeyword, isGhost, typeArgs, formals, result, Type.Bool, req, reads, ens, decreases, body, byMethodTok, byMethodBody, attributes, signatureEllipsis) { + Contract.Requires(bodyOrigin == Predicate.BodyOriginKind.OriginalOrInherited || body != null); + BodyOrigin = bodyOrigin; + } + } + + /// + /// An PrefixPredicate is the inductive unrolling P# implicitly declared for every extreme predicate P. + /// + public class PrefixPredicate : Function { + public override string WhatKind => "prefix predicate"; + public override string WhatKindMentionGhost => WhatKind; + public readonly Formal K; + public readonly ExtremePredicate ExtremePred; + public PrefixPredicate(IToken tok, string name, bool hasStaticKeyword, + List typeArgs, Formal k, List formals, + List req, List reads, List ens, Specification decreases, + Expression body, Attributes attributes, ExtremePredicate extremePred) + : base(tok, name, hasStaticKeyword, true, typeArgs, formals, null, Type.Bool, req, reads, ens, decreases, body, null, null, attributes, null) { + Contract.Requires(k != null); + Contract.Requires(extremePred != null); + Contract.Requires(formals != null && 1 <= formals.Count && formals[0] == k); + K = k; + ExtremePred = extremePred; + } + } + + public abstract class ExtremePredicate : Function { + public override string WhatKindMentionGhost => WhatKind; + public enum KType { Unspecified, Nat, ORDINAL } + public readonly KType TypeOfK; + public bool KNat { + get { + return TypeOfK == KType.Nat; + } + } + [FilledInDuringResolution] public readonly List Uses = new List(); // used by verifier + [FilledInDuringResolution] public PrefixPredicate PrefixPredicate; // (name registration) + + public ExtremePredicate(IToken tok, string name, bool hasStaticKeyword, KType typeOfK, + List typeArgs, List formals, Formal result, + List req, List reads, List ens, + Expression body, Attributes attributes, IToken signatureEllipsis) + : base(tok, name, hasStaticKeyword, true, typeArgs, formals, result, Type.Bool, + req, reads, ens, new Specification(new List(), null), body, null, null, attributes, signatureEllipsis) { + TypeOfK = typeOfK; + } + + /// + /// For the given call P(s), return P#[depth](s). The resulting expression shares some of the subexpressions + /// with 'fexp' (that is, what is returned is not necessarily a clone). + /// + public FunctionCallExpr CreatePrefixPredicateCall(FunctionCallExpr fexp, Expression depth) { + Contract.Requires(fexp != null); + Contract.Requires(fexp.Function == this); + Contract.Requires(depth != null); + Contract.Ensures(Contract.Result() != null); + + var args = new List() { depth }; + args.AddRange(fexp.Args); + var prefixPredCall = new FunctionCallExpr(fexp.tok, this.PrefixPredicate.Name, fexp.Receiver, fexp.OpenParen, fexp.CloseParen, args); + prefixPredCall.Function = this.PrefixPredicate; // resolve here + prefixPredCall.TypeApplication_AtEnclosingClass = fexp.TypeApplication_AtEnclosingClass; // resolve here + prefixPredCall.TypeApplication_JustFunction = fexp.TypeApplication_JustFunction; // resolve here + prefixPredCall.Type = fexp.Type; // resolve here + prefixPredCall.CoCall = fexp.CoCall; // resolve here + return prefixPredCall; + } + } + + public class LeastPredicate : ExtremePredicate { + public override string WhatKind => "least predicate"; + public LeastPredicate(IToken tok, string name, bool hasStaticKeyword, KType typeOfK, + List typeArgs, List formals, Formal result, + List req, List reads, List ens, + Expression body, Attributes attributes, IToken signatureEllipsis) + : base(tok, name, hasStaticKeyword, typeOfK, typeArgs, formals, result, + req, reads, ens, body, attributes, signatureEllipsis) { + } + } + + public class GreatestPredicate : ExtremePredicate { + public override string WhatKind => "greatest predicate"; + public GreatestPredicate(IToken tok, string name, bool hasStaticKeyword, KType typeOfK, + List typeArgs, List formals, Formal result, + List req, List reads, List ens, + Expression body, Attributes attributes, IToken signatureEllipsis) + : base(tok, name, hasStaticKeyword, typeOfK, typeArgs, formals, result, + req, reads, ens, body, attributes, signatureEllipsis) { + } + } + + public class TwoStateFunction : Function { + public override string WhatKind => "twostate function"; + public override string WhatKindMentionGhost => WhatKind; + public TwoStateFunction(IToken tok, string name, bool hasStaticKeyword, + List typeArgs, List formals, Formal result, Type resultType, + List req, List reads, List ens, Specification decreases, + Expression body, Attributes attributes, IToken signatureEllipsis) + : base(tok, name, hasStaticKeyword, true, typeArgs, formals, result, resultType, req, reads, ens, decreases, body, null, null, attributes, signatureEllipsis) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(typeArgs != null); + Contract.Requires(formals != null); + Contract.Requires(resultType != null); + Contract.Requires(req != null); + Contract.Requires(reads != null); + Contract.Requires(ens != null); + Contract.Requires(decreases != null); + } + public override bool ReadsHeap { get { return true; } } + } + + public class TwoStatePredicate : TwoStateFunction { + public override string WhatKind => "twostate predicate"; + public TwoStatePredicate(IToken tok, string name, bool hasStaticKeyword, + List typeArgs, List formals, Formal result, + List req, List reads, List ens, Specification decreases, + Expression body, Attributes attributes, IToken signatureEllipsis) + : base(tok, name, hasStaticKeyword, typeArgs, formals, result, Type.Bool, req, reads, ens, decreases, body, attributes, signatureEllipsis) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(typeArgs != null); + Contract.Requires(formals != null); + Contract.Requires(req != null); + Contract.Requires(reads != null); + Contract.Requires(ens != null); + Contract.Requires(decreases != null); + } + } + + public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext { + public override string WhatKind => "method"; + public bool SignatureIsOmitted { get { return SignatureEllipsis != null; } } + public readonly IToken SignatureEllipsis; + public readonly bool IsByMethod; + public bool MustReverify; + public bool IsEntryPoint = false; + public readonly List TypeArgs; + public readonly List Ins; + public readonly List Outs; + public readonly List Req; + public readonly Specification Mod; + public readonly List Ens; + public readonly Specification Decreases; + private BlockStmt methodBody; // Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution (note that "methodBody" is a "DividedBlockStmt" for any "Method" that is a "Constructor") + [FilledInDuringResolution] public bool IsRecursive; + [FilledInDuringResolution] public bool IsTailRecursive; + public readonly ISet AssignedAssumptionVariables = new HashSet(); + public Method OverriddenMethod; + public Method Original => OverriddenMethod == null ? this : OverriddenMethod.Original; + public override bool IsOverrideThatAddsBody => base.IsOverrideThatAddsBody && Body != null; + private static BlockStmt emptyBody = new BlockStmt(Token.NoToken, Token.NoToken, new List()); + + public override IEnumerable SubExpressions { + get { + foreach (var formal in Ins.Where(f => f.DefaultValue != null)) { + yield return formal.DefaultValue; + } + foreach (var e in Req) { + yield return e.E; + } + foreach (var e in Mod.Expressions) { + yield return e.E; + } + foreach (var e in Ens) { + yield return e.E; + } + foreach (var e in Decreases.Expressions) { + yield return e; + } + } + } + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(TypeArgs)); + Contract.Invariant(cce.NonNullElements(Ins)); + Contract.Invariant(cce.NonNullElements(Outs)); + Contract.Invariant(cce.NonNullElements(Req)); + Contract.Invariant(Mod != null); + Contract.Invariant(cce.NonNullElements(Ens)); + Contract.Invariant(Decreases != null); + } + + public Method(IToken tok, string name, + bool hasStaticKeyword, bool isGhost, + [Captured] List typeArgs, + [Captured] List ins, [Captured] List outs, + [Captured] List req, [Captured] Specification mod, + [Captured] List ens, + [Captured] Specification decreases, + [Captured] BlockStmt body, + Attributes attributes, IToken signatureEllipsis, bool isByMethod = false) + : base(tok, name, hasStaticKeyword, isGhost, attributes, signatureEllipsis != null) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cce.NonNullElements(ins)); + Contract.Requires(cce.NonNullElements(outs)); + Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(mod != null); + Contract.Requires(cce.NonNullElements(ens)); + Contract.Requires(decreases != null); + this.TypeArgs = typeArgs; + this.Ins = ins; + this.Outs = outs; + this.Req = req; + this.Mod = mod; + this.Ens = ens; + this.Decreases = decreases; + this.methodBody = body; + this.SignatureEllipsis = signatureEllipsis; + this.IsByMethod = isByMethod; + MustReverify = false; + } + + bool ICodeContext.IsGhost { get { return this.IsGhost; } } + List ICodeContext.TypeArgs { get { return this.TypeArgs; } } + List ICodeContext.Ins { get { return this.Ins; } } + List IMethodCodeContext.Outs { get { return this.Outs; } } + Specification IMethodCodeContext.Modifies { get { return Mod; } } + IToken ICallable.Tok { get { return this.tok; } } + string ICallable.NameRelativeToModule { + get { + if (EnclosingClass is DefaultClassDecl) { + return Name; + } else { + return EnclosingClass.Name + "." + Name; + } + } + } + Specification ICallable.Decreases { get { return this.Decreases; } } + bool _inferredDecr; + bool ICallable.InferredDecreases { + set { _inferredDecr = value; } + get { return _inferredDecr; } + } + + public virtual bool AllowsAllocation => true; + + ModuleDefinition ICodeContext.EnclosingModule { + get { + Contract.Assert(this.EnclosingClass != null); // this getter is supposed to be called only after signature-resolution is complete + return this.EnclosingClass.EnclosingModuleDefinition; + } + } + bool ICodeContext.MustReverify { get { return this.MustReverify; } } + public bool AllowsNontermination { + get { + return Contract.Exists(Decreases.Expressions, e => e is WildcardExpr); + } + } + + public override string CompileName { + get { + var nm = base.CompileName; + if (nm == Dafny.Compilers.SinglePassCompiler.DefaultNameMain && IsStatic && !IsEntryPoint) { + // for a static method that is named "Main" but is not a legal "Main" method, + // change its name. + nm = EnclosingClass.Name + "_" + nm; + } + return nm; + } + } + + public BlockStmt Body { + get { + // Lemma from included files do not need to be resolved and translated + // so we return emptyBody. This is to speed up resolver and translator. + if (methodBody != null && IsLemmaLike && this.tok is IncludeToken && !DafnyOptions.O.VerifyAllModules) { + return Method.emptyBody; + } else { + return methodBody; + } + } + set { + methodBody = value; + } + } + + public bool IsLemmaLike => this is Lemma || this is TwoStateLemma || this is ExtremeLemma || this is PrefixLemma; + + public BlockStmt BodyForRefinement { + // For refinement, we still need to merge in the body + // a lemma that is in the refinement base that is defined + // in a include file. + get { + return methodBody; + } + } + } + + public class Lemma : Method { + public override string WhatKind => "lemma"; + public override string WhatKindMentionGhost => WhatKind; + public Lemma(IToken tok, string name, + bool hasStaticKeyword, + [Captured] List typeArgs, + [Captured] List ins, [Captured] List outs, + [Captured] List req, [Captured] Specification mod, + [Captured] List ens, + [Captured] Specification decreases, + [Captured] BlockStmt body, + Attributes attributes, IToken signatureEllipsis) + : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) { + } + + public override bool AllowsAllocation => false; + } + + public class TwoStateLemma : Method { + public override string WhatKind => "twostate lemma"; + public override string WhatKindMentionGhost => WhatKind; + + public TwoStateLemma(IToken tok, string name, + bool hasStaticKeyword, + [Captured] List typeArgs, + [Captured] List ins, [Captured] List outs, + [Captured] List req, + [Captured] Specification mod, + [Captured] List ens, + [Captured] Specification decreases, + [Captured] BlockStmt body, + Attributes attributes, IToken signatureEllipsis) + : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(typeArgs != null); + Contract.Requires(ins != null); + Contract.Requires(outs != null); + Contract.Requires(req != null); + Contract.Requires(mod != null); + Contract.Requires(ens != null); + Contract.Requires(decreases != null); + } + + public override bool AllowsAllocation => false; + } + + public class Constructor : Method { + public override string WhatKind => "constructor"; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Body == null || Body is DividedBlockStmt); + } + public List BodyInit { // first part of Body's statements + get { + if (Body == null) { + return null; + } else { + return ((DividedBlockStmt)Body).BodyInit; + } + } + } + public List BodyProper { // second part of Body's statements + get { + if (Body == null) { + return null; + } else { + return ((DividedBlockStmt)Body).BodyProper; + } + } + } + public Constructor(IToken tok, string name, + bool isGhost, + List typeArgs, + List ins, + List req, [Captured] Specification mod, + List ens, + Specification decreases, + DividedBlockStmt body, + Attributes attributes, IToken signatureEllipsis) + : base(tok, name, false, isGhost, typeArgs, ins, new List(), req, mod, ens, decreases, body, attributes, signatureEllipsis) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cce.NonNullElements(ins)); + Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(mod != null); + Contract.Requires(cce.NonNullElements(ens)); + Contract.Requires(decreases != null); + } + + public bool HasName { + get { + return Name != "_ctor"; + } + } + } + + /// + /// A PrefixLemma is the inductive unrolling M# implicitly declared for every extreme lemma M. + /// + public class PrefixLemma : Method { + public override string WhatKind => "prefix lemma"; + public override string WhatKindMentionGhost => WhatKind; + + public readonly Formal K; + public readonly ExtremeLemma ExtremeLemma; + public PrefixLemma(IToken tok, string name, bool hasStaticKeyword, + List typeArgs, Formal k, List ins, List outs, + List req, Specification mod, List ens, Specification decreases, + BlockStmt body, Attributes attributes, ExtremeLemma extremeLemma) + : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, null) { + Contract.Requires(k != null); + Contract.Requires(ins != null && 1 <= ins.Count && ins[0] == k); + Contract.Requires(extremeLemma != null); + K = k; + ExtremeLemma = extremeLemma; + } + + public override bool AllowsAllocation => false; + } + + public abstract class ExtremeLemma : Method { + public override string WhatKindMentionGhost => WhatKind; + public readonly ExtremePredicate.KType TypeOfK; + public bool KNat { + get { + return TypeOfK == ExtremePredicate.KType.Nat; + } + } + [FilledInDuringResolution] public PrefixLemma PrefixLemma; // (name registration) + + public ExtremeLemma(IToken tok, string name, + bool hasStaticKeyword, ExtremePredicate.KType typeOfK, + List typeArgs, + List ins, [Captured] List outs, + List req, [Captured] Specification mod, + List ens, + Specification decreases, + BlockStmt body, + Attributes attributes, IToken signatureEllipsis) + : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cce.NonNullElements(ins)); + Contract.Requires(cce.NonNullElements(outs)); + Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(mod != null); + Contract.Requires(cce.NonNullElements(ens)); + Contract.Requires(decreases != null); + TypeOfK = typeOfK; + } + + public override bool AllowsAllocation => false; + } + + public class LeastLemma : ExtremeLemma { + public override string WhatKind => "least lemma"; + + public LeastLemma(IToken tok, string name, + bool hasStaticKeyword, ExtremePredicate.KType typeOfK, + List typeArgs, + List ins, [Captured] List outs, + List req, [Captured] Specification mod, + List ens, + Specification decreases, + BlockStmt body, + Attributes attributes, IToken signatureEllipsis) + : base(tok, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cce.NonNullElements(ins)); + Contract.Requires(cce.NonNullElements(outs)); + Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(mod != null); + Contract.Requires(cce.NonNullElements(ens)); + Contract.Requires(decreases != null); + } + } + + public class GreatestLemma : ExtremeLemma { + public override string WhatKind => "greatest lemma"; + + public GreatestLemma(IToken tok, string name, + bool hasStaticKeyword, ExtremePredicate.KType typeOfK, + List typeArgs, + List ins, [Captured] List outs, + List req, [Captured] Specification mod, + List ens, + Specification decreases, + BlockStmt body, + Attributes attributes, IToken signatureEllipsis) + : base(tok, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cce.NonNullElements(ins)); + Contract.Requires(cce.NonNullElements(outs)); + Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(mod != null); + Contract.Requires(cce.NonNullElements(ens)); + Contract.Requires(decreases != null); + } + } + + // ------------------------------------------------------------------------------------------------------ + + public abstract class Statement : IAttributeBearingDeclaration { + public readonly IToken Tok; + public readonly IToken EndTok; // typically a terminating semi-colon or end-curly-brace + public LList