From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Core/AbsyType.cs | 7812 +++++++++++++++++++++++------------------------ 1 file changed, 3906 insertions(+), 3906 deletions(-) (limited to 'Source/Core/AbsyType.cs') diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 5d41a8dd..96de5c0b 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -1,3907 +1,3907 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -//--------------------------------------------------------------------------------------------- -// BoogiePL - Absy.cs -//--------------------------------------------------------------------------------------------- - -namespace Microsoft.Boogie { - using System; - using System.Collections; - using System.Diagnostics; - using System.Linq; - using System.Collections.Generic; - using Microsoft.Boogie.AbstractInterpretation; - using System.Diagnostics.Contracts; - - //===================================================================== - //--------------------------------------------------------------------- - // Types - [ContractClass(typeof(TypeContracts))] - public abstract class Type : Absy { - public Type(IToken/*!*/ token) - : base(token) { - Contract.Requires(token != null); - } - - //----------- Cloning ---------------------------------- - // We implement our own clone-method, because bound type variables - // have to be created in the right way. It is /not/ ok to just clone - // everything recursively. Applying Clone to a type will return - // a type in which all bound variables have been replaced with new - // variables, whereas free variables have not changed - - public override Absy Clone() { - Contract.Ensures(Contract.Result() != null); - return this.Clone(new Dictionary()); - } - - public abstract Type/*!*/ Clone(IDictionary/*!*/ varMap); - - /// - /// Clones the type, but only syntactically. Anything resolved in the source - /// type is left unresolved (that is, with just the name) in the destination type. - /// - public abstract Type/*!*/ CloneUnresolved(); - - //----------- Linearisation ---------------------------------- - - public void Emit(TokenTextWriter stream) { - Contract.Requires(stream != null); - this.Emit(stream, 0); - } - - public abstract void Emit(TokenTextWriter/*!*/ stream, int contextBindingStrength); - - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - System.IO.StringWriter buffer = new System.IO.StringWriter(); - using (TokenTextWriter stream = new TokenTextWriter("", buffer, /*setTokens=*/false, /*pretty=*/ false)) { - this.Emit(stream); - } - return buffer.ToString(); - } - - //----------- Equality ---------------------------------- - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object that) { - if (ReferenceEquals(this, that)) - return true; - Type thatType = that as Type; - return thatType != null && this.Equals(thatType, - new List(), - new List()); - } - - [Pure] - public abstract bool Equals(Type/*!*/ that, - List/*!*/ thisBoundVariables, - List/*!*/ thatBoundVariables); - - // used to skip leading type annotations (subexpressions of the - // resulting type might still contain annotations) - internal virtual Type/*!*/ Expanded { - get { - Contract.Ensures(Contract.Result() != null); - - return this; - } - } - - //----------- Unification of types ----------- - - /// - /// Add a constraint that this==that, if possible, and return true. - /// If not possible, return false (which may have added some partial constraints). - /// No error is printed. - /// - public bool Unify(Type that) { - Contract.Requires(that != null); - return Unify(that, new List(), new Dictionary()); - } - - public abstract bool Unify(Type/*!*/ that, - List/*!*/ unifiableVariables, - // an idempotent substitution that describes the - // unification result up to a certain point - IDictionary/*!*/ unifier); - - - [Pure] - public static bool IsIdempotent(IDictionary/*!*/ unifier) { - Contract.Requires(cce.NonNullDictionaryAndValues(unifier)); - return unifier.Values.All(val => val.FreeVariables.All(var => !unifier.ContainsKey(var))); - } - - -#if OLD_UNIFICATION - // Compute a most general unification of two types. null is returned if - // no such unifier exists. The unifier is not allowed to subtitute any - // type variables other than the ones in "unifiableVariables" - public IDictionary Unify(Type! that, - List! unifiableVariables) { - Dictionary! result = new Dictionary (); - try { - this.Unify(that, unifiableVariables, - new List (), new List (), result); - } catch (UnificationFailedException) { - return null; - } - return result; - } - - // Compute an idempotent most general unifier and add the result to the argument - // unifier. The result is true iff the unification succeeded - public bool Unify(Type! that, - List! unifiableVariables, - // given mappings that need to be taken into account - // the old unifier has to be idempotent as well - IDictionary! unifier) - { - Contract.Requires(Contract.ForAll(unifier.Keys , key=> unifiableVariables.Has(key))); - Contract.Requires(IsIdempotent(unifier)); - try { - this.Unify(that, unifiableVariables, - new List (), new List (), unifier); - } catch (UnificationFailedException) { - return false; - } - return true; - } - - public abstract void Unify(Type! that, - List! unifiableVariables, - List! thisBoundVariables, - List! thatBoundVariables, - // an idempotent substitution that describes the - // unification result up to a certain point - IDictionary! result); -#endif - - //----------- Substitution of free variables with types not containing bound variables ----------------- - - public abstract Type/*!*/ Substitute(IDictionary/*!*/ subst); - - //----------- Hashcodes ---------------------------------- - - // Hack to be able to access the hashcode of superclasses further up - // (from the subclasses of this class) - [Pure] - protected int GetBaseHashCode() { - return base.GetHashCode(); - } - - [Pure] - public override int GetHashCode() { - return this.GetHashCode(new List()); - } - - [Pure] - public abstract int GetHashCode(List/*!*/ boundVariables); - - //----------- Resolution ---------------------------------- - - public override void Resolve(ResolutionContext rc) { - //Contract.Requires(rc != null); - System.Diagnostics.Debug.Fail("Type.Resolve should never be called." + - " Use Type.ResolveType instead"); - } - - public abstract Type/*!*/ ResolveType(ResolutionContext/*!*/ rc); - - public override void Typecheck(TypecheckingContext tc) { - //Contract.Requires(tc != null); - System.Diagnostics.Debug.Fail("Type.Typecheck should never be called"); - } - - // determine the free variables in a type, in the order in which the variables occur - public abstract List/*!*/ FreeVariables { - get; - } - - // determine the free type proxies in a type, in the order in which they occur - public abstract List/*!*/ FreeProxies { - get; - } - - protected static void AppendWithoutDups(List a, List b) { - Contract.Requires(b != null); - Contract.Requires(a != null); - foreach (A x in b) - if (!a.Contains(x)) - a.Add(x); - } - - public bool IsClosed { - get { - return FreeVariables.Count == 0; - } - } - - //----------- Getters/Issers ---------------------------------- - - // the following methods should be used instead of simple casts or the - // C# "is" operator, because they handle type synonym annotations and - // type proxies correctly - - public virtual bool IsBasic { - get { - return false; - } - } - public virtual bool IsInt { - get { - return false; - } - } - public virtual bool IsReal { - get { - return false; - } - } - public virtual bool IsFloat { - get { - return false; - } - } - public virtual bool IsBool { - get { - return false; - } - } - - public virtual bool IsVariable { - get { - return false; - } - } - public virtual TypeVariable/*!*/ AsVariable { - get { - Contract.Ensures(Contract.Result() != null); - - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // Type.AsVariable should never be called - } - } - public virtual bool IsCtor { - get { - return false; - } - } - public virtual CtorType/*!*/ AsCtor { - get { - Contract.Ensures(Contract.Result() != null); - - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // Type.AsCtor should never be called - } - } - public virtual bool IsMap { - get { - return false; - } - } - public virtual MapType/*!*/ AsMap { - get { - Contract.Ensures(Contract.Result() != null); - - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // Type.AsMap should never be called - } - } - public virtual int MapArity { - get { - - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // Type.MapArity should never be called - } - } - public virtual bool IsUnresolved { - get { - return false; - } - } - public virtual UnresolvedTypeIdentifier/*!*/ AsUnresolved { - get { - Contract.Ensures(Contract.Result() != null); - - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // Type.AsUnresolved should never be called - } - } - - public virtual bool isFloat { - get { - return false; - } - } - public virtual int FloatExponent - { - get - { - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // Type.FloatExponent should never be called - } - } - public virtual int FloatMantissa { - get { - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // Type.FloatMantissa should never be called - } - } - public virtual bool IsBv { - get { - return false; - } - } - public virtual int BvBits { - get { - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // Type.BvBits should never be called - } - } - - public static readonly Type/*!*/ Int = new BasicType(SimpleType.Int); - public static readonly Type/*!*/ Real = new BasicType(SimpleType.Real); - public static readonly Type/*!*/ Bool = new BasicType(SimpleType.Bool); - private static BvType[] bvtypeCache; - - static public BvType GetBvType(int sz) { - Contract.Requires(0 <= sz); - Contract.Ensures(Contract.Result() != null); - - if (bvtypeCache == null) { - bvtypeCache = new BvType[128]; - } - if (sz < bvtypeCache.Length) { - BvType t = bvtypeCache[sz]; - if (t == null) { - t = new BvType(sz); - bvtypeCache[sz] = t; - } - return t; - } else { - return new BvType(sz); - } - } - - static public FloatType GetFloatType(int exp, int man) { - Contract.Requires(0 <= exp); - Contract.Requires(0 <= man); - Contract.Ensures(Contract.Result() != null); - - return new FloatType(exp, man); - } - - //------------ Match formal argument types on actual argument types - //------------ and return the resulting substitution of type variables - -#if OLD_UNIFICATION - public static IDictionary! - MatchArgumentTypes(List! typeParams, - List! formalArgs, - List! actualArgs, - List formalOuts, - List actualOuts, - string! opName, - TypecheckingContext! tc) - { - Contract.Requires(formalArgs.Length == actualArgs.Length); - Contract.Requires(formalOuts == null <==> actualOuts == null); - Contract.Requires(formalOuts != null ==> formalOuts.Length == actualOuts.Length); - List! boundVarSeq0 = new List (); - List! boundVarSeq1 = new List (); - Dictionary! subst = new Dictionary(); - - for (int i = 0; i < formalArgs.Length; ++i) { - try { - Type! actualType = cce.NonNull((!)actualArgs[i]).Type; - // if the type variables to be matched occur in the actual - // argument types, something has gone very wrong - Contract.Assert(forall{TypeVariable! var in typeParams); - !actualType.FreeVariables.Has(var)}; - formalArgs[i].Unify(actualType, - typeParams, - boundVarSeq0, boundVarSeq1, - subst); - } catch (UnificationFailedException) { - tc.Error(actualArgs[i], - "invalid type for argument {0} in {1}: {2} (expected: {3})", - i, opName, actualArgs[i].Type, - // we insert the type parameters that have already been - // chosen to get a more precise error message - formalArgs[i].Substitute(subst)); - // the bound variable sequences should be empty ... - // so that we can continue with the unification - Contract.Assert(boundVarSeq0.Length == 0 && boundVarSeq1.Length == 0); - } - } - - if (formalOuts != null) { - for (int i = 0; i < formalOuts.Length; ++i) { - try { - Type! actualType = cce.NonNull((!)actualOuts[i]).Type; - // if the type variables to be matched occur in the actual - // argument types, something has gone very wrong - Contract.Assert(forall{TypeVariable! var in typeParams); - !actualType.FreeVariables.Has(var)}; - formalOuts[i].Unify(actualType, - typeParams, - boundVarSeq0, boundVarSeq1, - subst); - } catch (UnificationFailedException) { - tc.Error(actualOuts[i], - "invalid type for result {0} in {1}: {2} (expected: {3})", - i, opName, actualOuts[i].Type, - // we insert the type parameters that have already been - // chosen to get a more precise error message - formalOuts[i].Substitute(subst)); - // the bound variable sequences should be empty ... - // so that we can continue with the unification - Contract.Assert(boundVarSeq0.Length == 0 && boundVarSeq1.Length == 0); - } - } - } - - // we only allow type parameters to be substituted - Contract.Assert(Contract.ForAll(subst.Keys , var=> typeParams.Has(var))); - - return subst; - } -#else - public static IDictionary/*!*/ - MatchArgumentTypes(List/*!*/ typeParams, - List/*!*/ formalArgs, - IList/*!*/ actualArgs, - List formalOuts, - List actualOuts, - string/*!*/ opName, - TypecheckingContext/*!*/ tc) { - Contract.Requires(typeParams != null); - Contract.Requires(formalArgs != null); - Contract.Requires(actualArgs != null); - Contract.Requires(opName != null); - Contract.Requires(tc != null); - Contract.Requires(formalArgs.Count == actualArgs.Count); - Contract.Requires((formalOuts == null) == (actualOuts == null)); - Contract.Requires(formalOuts == null || formalOuts.Count == cce.NonNull(actualOuts).Count); - Contract.Requires(tc == null || opName != null);//Redundant - Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result>())); - - // requires "actualArgs" and "actualOuts" to have been type checked - - Dictionary subst = new Dictionary(); - foreach (TypeVariable/*!*/ tv in typeParams) { - Contract.Assert(tv != null); - TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name); - subst.Add(tv, proxy); - } - - for (int i = 0; i < formalArgs.Count; i++) { - Type formal = formalArgs[i].Substitute(subst); - Type actual = cce.NonNull(cce.NonNull(actualArgs[i]).Type); - // if the type variables to be matched occur in the actual - // argument types, something has gone very wrong - Contract.Assert(Contract.ForAll(0, typeParams.Count, index => !actual.FreeVariables.Contains(typeParams[index]))); - - if (!formal.Unify(actual)) { - Contract.Assume(tc != null); // caller expected no errors - Contract.Assert(opName != null); // follows from precondition - tc.Error(cce.NonNull(actualArgs[i]), - "invalid type for argument {0} in {1}: {2} (expected: {3})", - i, opName, actual, formalArgs[i]); - } - } - - if (formalOuts != null) { - for (int i = 0; i < formalOuts.Count; ++i) { - Type formal = formalOuts[i].Substitute(subst); - Type actual = cce.NonNull(cce.NonNull(actualOuts)[i].Type); - // if the type variables to be matched occur in the actual - // argument types, something has gone very wrong - Contract.Assert(Contract.ForAll(0, typeParams.Count, var => !actual.FreeVariables.Contains(typeParams[var]))); - - if (!formal.Unify(actual)) { - Contract.Assume(tc != null); // caller expected no errors - Contract.Assert(opName != null); // follows from precondition - tc.Error(actualOuts[i], - "invalid type for out-parameter {0} in {1}: {2} (expected: {3})", - i, opName, actual, formal); - } - } - } - - return subst; - } -#endif - - //------------ Match formal argument types of a function or map - //------------ on concrete types, substitute the result into the - //------------ result type. Null is returned for type errors - - public static List CheckArgumentTypes(List/*!*/ typeParams, - out List/*!*/ actualTypeParams, - List/*!*/ formalIns, - IList/*!*/ actualIns, - List/*!*/ formalOuts, - List actualOuts, - IToken/*!*/ typeCheckingSubject, - string/*!*/ opName, - TypecheckingContext/*!*/ tc) - // requires "actualIns" and "actualOuts" to have been type checked - { - Contract.Requires(typeParams != null); - - Contract.Requires(formalIns != null); - Contract.Requires(formalOuts != null); - Contract.Requires(actualIns != null); - Contract.Requires(typeCheckingSubject != null); - Contract.Requires(opName != null);Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out actualTypeParams))); - actualTypeParams = new List(); - - if (formalIns.Count != actualIns.Count) { - tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1}", - opName, actualIns.Count); - // if there are no type parameters, we can still return the result - // type and hope that the type checking proceeds - return typeParams.Count == 0 ? formalOuts : null; - } else if (actualOuts != null && formalOuts.Count != actualOuts.Count) { - tc.Error(typeCheckingSubject, "wrong number of result variables in {0}: {1}", - opName, actualOuts.Count); - // if there are no type parameters, we can still return the result - // type and hope that the type checking proceeds - actualTypeParams = new List(); - return typeParams.Count == 0 ? formalOuts : null; - } - - int previousErrorCount = tc.ErrorCount; - IDictionary subst = - MatchArgumentTypes(typeParams, formalIns, actualIns, - actualOuts != null ? formalOuts : null, actualOuts, opName, tc); - Contract.Assert(cce.NonNullDictionaryAndValues(subst)); - foreach (TypeVariable/*!*/ var in typeParams) { - Contract.Assert(var != null); - actualTypeParams.Add(subst[var]); - } - - List/*!*/ actualResults = new List(); - foreach (Type/*!*/ t in formalOuts) { - Contract.Assert(t != null); - actualResults.Add(t.Substitute(subst)); - } - List resultFreeVars = FreeVariablesIn(actualResults); - if (previousErrorCount != tc.ErrorCount) { - // errors occured when matching the formal arguments - // in case we have been able to substitute all type parameters, - // we can still return the result type and hope that the - // type checking proceeds in a meaningful manner - if (typeParams.All(param => !resultFreeVars.Contains(param))) - return actualResults; - else - // otherwise there is no point in returning the result type, - // type checking would only get confused even further - return null; - } - - Contract.Assert(Contract.ForAll(0, typeParams.Count, index => !resultFreeVars.Contains(typeParams[index]))); - return actualResults; - } - - /////////////////////////////////////////////////////////////////////////// - - // about the same as Type.CheckArgumentTypes, but without - // detailed error reports - public static Type/*!*/ InferValueType(List/*!*/ typeParams, - List/*!*/ formalArgs, - Type/*!*/ formalResult, - List/*!*/ actualArgs) { - Contract.Requires(typeParams != null); - Contract.Requires(formalArgs != null); - Contract.Requires(formalResult != null); - Contract.Requires(actualArgs != null); - Contract.Ensures(Contract.Result() != null); - - IDictionary/*!*/ subst = - InferTypeParameters(typeParams, formalArgs, actualArgs); - Contract.Assert(cce.NonNullDictionaryAndValues(subst)); - - Type/*!*/ res = formalResult.Substitute(subst); - Contract.Assert(res != null); - // all type parameters have to be substituted with concrete types - List/*!*/ resFreeVars = res.FreeVariables; - Contract.Assert(resFreeVars != null); - Contract.Assert(Contract.ForAll(0, typeParams.Count, var => !resFreeVars.Contains(typeParams[var]))); - return res; - } - -#if OLD_UNIFICATION - public static IDictionary! - InferTypeParameters(List! typeParams, - List! formalArgs, - List! actualArgs) - { - Contract.Requires(formalArgs.Length == actualArgs.Length); - - List! boundVarSeq0 = new List (); - List! boundVarSeq1 = new List (); - Dictionary! subst = new Dictionary(); - - for (int i = 0; i < formalArgs.Length; ++i) { - try { - Contract.Assert(forall{TypeVariable! var in typeParams); - !actualArgs[i].FreeVariables.Has(var)}; - formalArgs[i].Unify(actualArgs[i], typeParams, - boundVarSeq0, boundVarSeq1, subst); - } catch (UnificationFailedException) { - System.Diagnostics.Debug.Fail("Type unification failed: " + - formalArgs[i] + " vs " + actualArgs[i]); - } - } - - // we only allow type parameters to be substituted - Contract.Assert(Contract.ForAll(subst.Keys , var=> typeParams.Has(var))); - return subst; - } -#else - /// - /// like Type.CheckArgumentTypes, but assumes no errors - /// (and only does arguments, not results; and takes actuals as List, not List) - /// - public static IDictionary/*!*/ - InferTypeParameters(List/*!*/ typeParams, - List/*!*/ formalArgs, - List/*!*/ actualArgs) { - Contract.Requires(typeParams != null); - Contract.Requires(formalArgs != null); - Contract.Requires(actualArgs != null);Contract.Requires(formalArgs.Count == actualArgs.Count); - Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result>())); - - - List proxies = new List(); - Dictionary/*!*/ subst = new Dictionary(); - foreach (TypeVariable/*!*/ tv in typeParams) { - Contract.Assert(tv != null); - TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name); - proxies.Add(proxy); - subst.Add(tv, proxy); - } - - for (int i = 0; i < formalArgs.Count; i++) { - Type formal = formalArgs[i].Substitute(subst); - Type actual = actualArgs[i]; - // if the type variables to be matched occur in the actual - // argument types, something has gone very wrong - Contract.Assert(Contract.ForAll(0, typeParams.Count, index => !actual.FreeVariables.Contains(typeParams[index]))); - - if (!formal.Unify(actual)) { - Contract.Assume(false); // caller expected no errors - } - } - - return subst; - } -#endif - - //----------- Helper methods to deal with bound type variables --------------- - - public static void EmitOptionalTypeParams(TokenTextWriter stream, List typeParams) { - Contract.Requires(typeParams != null); - Contract.Requires(stream != null); - if (typeParams.Count > 0) { - stream.Write("<"); - typeParams.Emit(stream, ","); // default binding strength of 0 is ok - stream.Write(">"); - } - } - - // Sort the type parameters according to the order of occurrence in the argument types - public static List/*!*/ SortTypeParams(List/*!*/ typeParams, List/*!*/ argumentTypes, Type resultType) { - Contract.Requires(typeParams != null); - Contract.Requires(argumentTypes != null); - Contract.Ensures(Contract.Result>() != null); - - Contract.Ensures(Contract.Result>().Count == typeParams.Count); - if (typeParams.Count == 0) { - return typeParams; - } - - List freeVarsInUse = FreeVariablesIn(argumentTypes); - if (resultType != null) { - freeVarsInUse.AppendWithoutDups(resultType.FreeVariables); - } - // "freeVarsInUse" is already sorted, but it may contain type variables not in "typeParams". - // So, project "freeVarsInUse" onto "typeParams": - List sortedTypeParams = new List(); - foreach (TypeVariable/*!*/ var in freeVarsInUse) { - Contract.Assert(var != null); - if (typeParams.Contains(var)) { - sortedTypeParams.Add(var); - } - } - - if (sortedTypeParams.Count < typeParams.Count) - // add the type parameters not mentioned in "argumentTypes" in - // the end of the list (this can happen for quantifiers) - sortedTypeParams.AppendWithoutDups(typeParams); - - return sortedTypeParams; - } - - // Check that each of the type parameters occurs in at least one argument type. - // Return true if some type parameters appear only among "moreArgumentTypes" and - // not in "argumentTypes". - [Pure] - public static bool CheckBoundVariableOccurrences(List/*!*/ typeParams, - List/*!*/ argumentTypes, - List moreArgumentTypes, - IToken/*!*/ resolutionSubject, - string/*!*/ subjectName, - ResolutionContext/*!*/ rc) { - Contract.Requires(typeParams != null); - Contract.Requires(argumentTypes != null); - Contract.Requires(resolutionSubject != null); - Contract.Requires(subjectName != null); - Contract.Requires(rc != null); - List freeVarsInArgs = FreeVariablesIn(argumentTypes); - List moFreeVarsInArgs = moreArgumentTypes == null ? null : FreeVariablesIn(moreArgumentTypes); - bool someTypeParamsAppearOnlyAmongMo = false; - foreach (TypeVariable/*!*/ var in typeParams) { - Contract.Assert(var != null); - if (rc.LookUpTypeBinder(var.Name) == var) // avoid to complain twice about variables that are bound multiple times - { - if (freeVarsInArgs.Contains(var)) { - // cool - } else if (moFreeVarsInArgs != null && moFreeVarsInArgs.Contains(var)) { - someTypeParamsAppearOnlyAmongMo = true; - } else { - rc.Error(resolutionSubject, - "type variable must occur in {0}: {1}", - subjectName, var); - } - } - } - return someTypeParamsAppearOnlyAmongMo; - } - - [Pure] - public static List FreeVariablesIn(List arguments) { - Contract.Requires(arguments != null); - Contract.Ensures(Contract.Result>() != null); - List/*!*/ res = new List(); - foreach (Type/*!*/ t in arguments) { - Contract.Assert(t != null); - res.AppendWithoutDups(t.FreeVariables); - } - return res; - } - } - [ContractClassFor(typeof(Type))] - public abstract class TypeContracts : Type { - public TypeContracts() :base(null){ - - } - public override List FreeProxies { - get { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - throw new NotImplementedException(); - } - } - public override List FreeVariables { - get { - Contract.Ensures(Contract.Result>() != null); - throw new NotImplementedException(); - } - } - public override Type Clone(IDictionary varMap) { - Contract.Requires(cce.NonNullDictionaryAndValues(varMap)); - Contract.Ensures(Contract.Result() != null); - - throw new NotImplementedException(); - } - public override Type CloneUnresolved() { - Contract.Ensures(Contract.Result() != null); - - throw new NotImplementedException(); - } - public override void Emit(TokenTextWriter stream, int contextBindingStrength) { - Contract.Requires(stream != null); - throw new NotImplementedException(); - } - public override bool Equals(Type that, List thisBoundVariables, List thatBoundVariables) { - Contract.Requires(that != null); - Contract.Requires(thisBoundVariables != null); - Contract.Requires(thatBoundVariables != null); - throw new NotImplementedException(); - } - public override bool Unify(Type that, List unifiableVariables, IDictionary unifier) { - Contract.Requires(that != null); - Contract.Requires(unifiableVariables != null); - Contract.Requires(cce.NonNullDictionaryAndValues(unifier)); - Contract.Requires(Contract.ForAll(unifier.Keys, key => unifiableVariables.Contains(key))); - Contract.Requires(IsIdempotent(unifier)); - throw new NotImplementedException(); - } - public override Type Substitute(IDictionary subst) { - Contract.Requires(cce.NonNullDictionaryAndValues(subst)); - Contract.Ensures(Contract.Result() != null); - - throw new NotImplementedException(); - } - public override Type ResolveType(ResolutionContext rc) { - Contract.Requires(rc != null); - Contract.Ensures(Contract.Result() != null); - - throw new NotImplementedException(); - } - public override int GetHashCode(List boundVariables) { - Contract.Requires(boundVariables != null); - throw new NotImplementedException(); - } - } - //===================================================================== - - public class BasicType : Type { - public readonly SimpleType T; - public BasicType(IToken/*!*/ token, SimpleType t) - : base(token) { - Contract.Requires(token != null); - T = t; - } - public BasicType(SimpleType t) - : base(Token.NoToken) { - T = t; - } - - //----------- Cloning ---------------------------------- - // We implement our own clone-method, because bound type variables - // have to be created in the right way. It is /not/ ok to just clone - // everything recursively. - - public override Type Clone(IDictionary/*!*/ varMap) { - //Contract.Requires(cce.NonNullElements(varMap)); - Contract.Ensures(Contract.Result() != null); - // BasicTypes are immutable anyway, we do not clone - return this; - } - - public override Type CloneUnresolved() { - Contract.Ensures(Contract.Result() != null); - return this; - } - - //----------- Linearisation ---------------------------------- - - public override void Emit(TokenTextWriter stream, int contextBindingStrength) { - //Contract.Requires(stream != null); - // no parentheses are necessary for basic types - stream.SetToken(this); - stream.Write("{0}", this); - } - - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - switch (T) { - case SimpleType.Int: - return "int"; - case SimpleType.Real: - return "real"; - case SimpleType.Bool: - return "bool"; - } - Debug.Assert(false, "bad type " + T); - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // make compiler happy - } - - //----------- Equality ---------------------------------- - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object that) { - // shortcut - Type thatType = that as Type; - if (thatType == null) - return false; - BasicType thatBasicType = TypeProxy.FollowProxy(thatType.Expanded) as BasicType; - return thatBasicType != null && this.T == thatBasicType.T; - } - - [Pure] - public override bool Equals(Type that, List thisBoundVariables, List thatBoundVariables) { - //Contract.Requires(thatBoundVariables != null); - //Contract.Requires(thisBoundVariables != null); - //Contract.Requires(that != null); - return this.Equals(that); - } - - //----------- Unification of types ----------- - - public override bool Unify(Type that, List unifiableVariables, IDictionary/*!*/ unifier) { - //Contract.Requires(unifiableVariables != null); - //Contract.Requires(that != null); - //Contract.Requires(cce.NonNullElements(unifier)); - // an idempotent substitution that describes the - // unification result up to a certain point - - that = that.Expanded; - if (that is TypeProxy || that is TypeVariable) { - return that.Unify(this, unifiableVariables, unifier); - } else { - return this.Equals(that); - } - } - -#if OLD_UNIFICATION - public override void Unify(Type! that, - List! unifiableVariables, - List! thisBoundVariables, - List! thatBoundVariables, - IDictionary! result) { - that = that.Expanded; - if (that is TypeVariable) { - that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result); - } else { - if (!this.Equals(that)) - throw UNIFICATION_FAILED; - } - } -#endif - - //----------- Substitution of free variables with types not containing bound variables ----------------- - - public override Type Substitute(IDictionary/*!*/ subst) { - //Contract.Requires(cce.NonNullElements(subst)); - Contract.Ensures(Contract.Result() != null); - return this; - } - - //----------- Hashcodes ---------------------------------- - - [Pure] - public override int GetHashCode(List boundVariables) { - //Contract.Requires(boundVariables != null); - return this.T.GetHashCode(); - } - - //----------- Resolution ---------------------------------- - - public override Type ResolveType(ResolutionContext rc) { - //Contract.Requires(rc != null); - Contract.Ensures(Contract.Result() != null); - // nothing to resolve - return this; - } - - // determine the free variables in a type, in the order in which the variables occur - public override List/*!*/ FreeVariables { - get { - Contract.Ensures(Contract.Result>() != null); - - return new List(); // basic type are closed - } - } - - public override List/*!*/ FreeProxies { - get { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return new List(); - } - } - - //----------- Getters/Issers ---------------------------------- - - public override bool IsBasic { - get { - return true; - } - } - public override bool IsInt { - get { - return this.T == SimpleType.Int; - } - } - public override bool IsReal { - get { - return this.T == SimpleType.Real; - } - } - public override bool IsBool { - get { - return this.T == SimpleType.Bool; - } - } - - public override Absy StdDispatch(StandardVisitor visitor) { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitBasicType(this); - } - } - - //===================================================================== - - //Note that the functions in this class were directly copied from the BV class just below - public class FloatType : Type { - public readonly int Mantissa; //Size of mantissa in bits - public readonly int Exponent; //Size of exponent in bits - - public FloatType(IToken token, int exponent, int mantissa) - : base(token) { - Contract.Requires(token != null); - Exponent = exponent; - Mantissa = mantissa; - } - - public FloatType(int exponent, int mantissa) - : base(Token.NoToken) { - Exponent = exponent; - Mantissa = mantissa; - } - - //----------- Cloning ---------------------------------- - // We implement our own clone-method, because bound type variables - // have to be created in the right way. It is /not/ ok to just clone - // everything recursively. - - public override Type Clone(IDictionary/*!*/ varMap) - { - //Contract.Requires(cce.NonNullElements(varMap)); - Contract.Ensures(Contract.Result() != null); - // FloatTypes are immutable anyway, we do not clone - return this; - } - - public override Type CloneUnresolved() - { - Contract.Ensures(Contract.Result() != null); - return this; - } - - //----------- Linearisation ---------------------------------- - - public override void Emit(TokenTextWriter stream, int contextBindingStrength) - { - //Contract.Requires(stream != null); - // no parentheses are necessary for bitvector-types - stream.SetToken(this); - stream.Write("{0}", this); - } - - public override string ToString() - { - Contract.Ensures(Contract.Result() != null); - return "float (" + Exponent + " " + Mantissa + ")"; - } - - //----------- Equality ---------------------------------- - - [Pure] - public override bool Equals(Type/*!*/ that, - List/*!*/ thisBoundVariables, - List/*!*/ thatBoundVariables) - { - FloatType thatFloatType = TypeProxy.FollowProxy(that.Expanded) as FloatType; - return thatFloatType != null && this.Mantissa == thatFloatType.Mantissa && this.Exponent == thatFloatType.Exponent; - } - - //----------- Unification of types ----------- - - public override bool Unify(Type/*!*/ that, - List/*!*/ unifiableVariables, - // an idempotent substitution that describes the - // unification result up to a certain point - IDictionary/*!*/ unifier) - { - //Contract.Requires(that != null); - //Contract.Requires(unifiableVariables != null); - //Contract.Requires(cce.NonNullElements(unifier)); - that = that.Expanded; - if (that is TypeProxy || that is TypeVariable) { - return that.Unify(this, unifiableVariables, unifier); - } - else { - return this.Equals(that); - } - } - - //----------- Substitution of free variables with types not containing bound variables ----------------- - - public override Type Substitute(IDictionary/*!*/ subst) - { - Contract.Ensures(Contract.Result() != null); - return this; - } - - //----------- Hashcodes ---------------------------------- - - [Pure] - public override int GetHashCode(List boundVariables) - { - return this.Mantissa.GetHashCode() + this.Exponent.GetHashCode(); - } - - //----------- Resolution ---------------------------------- - - public override Type ResolveType(ResolutionContext rc) - { - //Contract.Requires(rc != null); - Contract.Ensures(Contract.Result() != null); - // nothing to resolve - return this; - } - - // determine the free variables in a type, in the order in which the variables occur - public override List/*!*/ FreeVariables - { - get - { - Contract.Ensures(Contract.Result>() != null); - - return new List(); // bitvector-type are closed - } - } - - public override List/*!*/ FreeProxies - { - get - { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return new List(); - } - } - - //----------- Getters/Issers ---------------------------------- - - public override bool IsFloat { - get { - return true; - } - } - public override int FloatMantissa { - get { - return Mantissa; - } - } - public override int FloatExponent { - get { - return Exponent; - } - } - - public override Absy StdDispatch(StandardVisitor visitor) - { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitFloatType(this); - } - - } - - //===================================================================== - - public class BvType : Type { - public readonly int Bits; - - public BvType(IToken token, int bits) - : base(token) { - Contract.Requires(token != null); - Bits = bits; - } - - public BvType(int bits) - : base(Token.NoToken) { - Bits = bits; - } - - //----------- Cloning ---------------------------------- - // We implement our own clone-method, because bound type variables - // have to be created in the right way. It is /not/ ok to just clone - // everything recursively. - - public override Type Clone(IDictionary/*!*/ varMap) { - //Contract.Requires(cce.NonNullElements(varMap)); - Contract.Ensures(Contract.Result() != null); - // BvTypes are immutable anyway, we do not clone - return this; - } - - public override Type CloneUnresolved() { - Contract.Ensures(Contract.Result() != null); - return this; - } - - //----------- Linearisation ---------------------------------- - - public override void Emit(TokenTextWriter stream, int contextBindingStrength) { - //Contract.Requires(stream != null); - // no parentheses are necessary for bitvector-types - stream.SetToken(this); - stream.Write("{0}", this); - } - - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - return "bv" + Bits; - } - - //----------- Equality ---------------------------------- - - [Pure] - public override bool Equals(Type/*!*/ that, - List/*!*/ thisBoundVariables, - List/*!*/ thatBoundVariables) { - //Contract.Requires(thisBoundVariables != null); - //Contract.Requires(thatBoundVariables != null); - //Contract.Requires(that != null); - BvType thatBvType = TypeProxy.FollowProxy(that.Expanded) as BvType; - return thatBvType != null && this.Bits == thatBvType.Bits; - } - - //----------- Unification of types ----------- - - public override bool Unify(Type/*!*/ that, - List/*!*/ unifiableVariables, - // an idempotent substitution that describes the - // unification result up to a certain point - IDictionary/*!*/ unifier) { - //Contract.Requires(that != null); - //Contract.Requires(unifiableVariables != null); - //Contract.Requires(cce.NonNullElements(unifier)); - that = that.Expanded; - if (that is TypeProxy || that is TypeVariable) { - return that.Unify(this, unifiableVariables, unifier); - } else { - return this.Equals(that); - } - } - -#if OLD_UNIFICATION - public override void Unify(Type that, - List! unifiableVariables, - List! thisBoundVariables, - List! thatBoundVariables, - IDictionary result){ -Contract.Requires(result != null); -Contract.Requires(that != null); - that = that.Expanded; - if (that is TypeVariable) { - that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result); - } else { - if (!this.Equals(that)) - throw UNIFICATION_FAILED; - } - } -#endif - - //----------- Substitution of free variables with types not containing bound variables ----------------- - - public override Type Substitute(IDictionary/*!*/ subst) { - //Contract.Requires(cce.NonNullElements(subst)); - Contract.Ensures(Contract.Result() != null); - return this; - } - - //----------- Hashcodes ---------------------------------- - - [Pure] - public override int GetHashCode(List boundVariables) { - //Contract.Requires(boundVariables != null); - return this.Bits.GetHashCode(); - } - - //----------- Resolution ---------------------------------- - - public override Type ResolveType(ResolutionContext rc) { - //Contract.Requires(rc != null); - Contract.Ensures(Contract.Result() != null); - // nothing to resolve - return this; - } - - // determine the free variables in a type, in the order in which the variables occur - public override List/*!*/ FreeVariables { - get { - Contract.Ensures(Contract.Result>() != null); - - return new List(); // bitvector-type are closed - } - } - - public override List/*!*/ FreeProxies { - get { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return new List(); - } - } - - //----------- Getters/Issers ---------------------------------- - - public override bool IsBv { - get { - return true; - } - } - public override int BvBits { - get { - return Bits; - } - } - - public override Absy StdDispatch(StandardVisitor visitor) { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitBvType(this); - } - } - - //===================================================================== - - // An AST node containing an identifier and a sequence of type arguments, which - // will be turned either into a TypeVariable, into a CtorType or into a BvType - // during the resolution phase - public class UnresolvedTypeIdentifier : Type { - public readonly string/*!*/ Name; - public readonly List/*!*/ Arguments; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Name != null); - Contract.Invariant(Arguments != null); - } - - - public UnresolvedTypeIdentifier(IToken token, string name) - : this(token, name, new List()) { - Contract.Requires(name != null); - Contract.Requires(token != null); - } - - public UnresolvedTypeIdentifier(IToken token, string name, List arguments) - : base(token) { - Contract.Requires(arguments != null); - Contract.Requires(name != null); - Contract.Requires(token != null); - this.Name = name; - this.Arguments = arguments; - } - - //----------- Cloning ---------------------------------- - // We implement our own clone-method, because bound type variables - // have to be created in the right way. It is /not/ ok to just clone - // everything recursively - - public override Type Clone(IDictionary/*!*/ varMap) { - //Contract.Requires(cce.NonNullElements(varMap)); - Contract.Ensures(Contract.Result() != null); - List/*!*/ newArgs = new List(); - foreach (Type/*!*/ t in Arguments) { - Contract.Assert(t != null); - newArgs.Add(t.Clone(varMap)); - } - return new UnresolvedTypeIdentifier(tok, Name, newArgs); - } - - public override Type CloneUnresolved() { - Contract.Ensures(Contract.Result() != null); - List/*!*/ newArgs = new List(); - foreach (Type/*!*/ t in Arguments) { - Contract.Assert(t != null); - newArgs.Add(t.CloneUnresolved()); - } - return new UnresolvedTypeIdentifier(tok, Name, newArgs); - } - - //----------- Equality ---------------------------------- - - [Pure] - public override bool Equals(Type that, - List/*!*/ thisBoundVariables, - List/*!*/ thatBoundVariables) { - //Contract.Requires(thisBoundVariables != null); - //Contract.Requires(thatBoundVariables != null); - //Contract.Requires(that != null); - System.Diagnostics.Debug.Fail("UnresolvedTypeIdentifier.Equals should never be called"); - return false; // to make the compiler happy - } - - //----------- Unification of types ----------- - - public override bool Unify(Type that, - List/*!*/ unifiableVariables, - IDictionary result) { - //Contract.Requires(unifiableVariables != null); - //Contract.Requires(cce.NonNullElements(result)); - //Contract.Requires(that != null); - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // UnresolvedTypeIdentifier.Unify should never be called - } - -#if OLD_UNIFICATION - public override void Unify(Type that, - List! unifiableVariables, - List! thisBoundVariables, - List! thatBoundVariables, - IDictionary result){ -Contract.Requires(result != null); -Contract.Requires(that != null); - System.Diagnostics.Debug.Fail("UnresolvedTypeIdentifier.Unify should never be called"); - } -#endif - - //----------- Substitution of free variables with types not containing bound variables ----------------- - - public override Type Substitute(IDictionary/*!*/ subst) { - //Contract.Requires(cce.NonNullElements(subst)); - Contract.Ensures(Contract.Result() != null); - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // UnresolvedTypeIdentifier.Substitute should never be called - } - - //----------- Hashcodes ---------------------------------- - - [Pure] - public override int GetHashCode(List boundVariables) { - //Contract.Requires(boundVariables != null); - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // UnresolvedTypeIdentifier.GetHashCode should never be called - } - - //----------- Resolution ---------------------------------- - - public override Type ResolveType(ResolutionContext rc) { - //Contract.Requires(rc != null); - Contract.Ensures(Contract.Result() != null); - // first case: the type name denotes a bitvector-type - if (Name.StartsWith("bv") && Name.Length > 2) { - bool is_bv = true; - for (int i = 2; i < Name.Length; ++i) { - if (!char.IsDigit(Name[i])) { - is_bv = false; - break; - } - } - if (is_bv) { - if (Arguments.Count > 0) { - rc.Error(this, - "bitvector types must not be applied to arguments: {0}", - Name); - } - return new BvType(tok, int.Parse(Name.Substring(2))); - } - } - - // second case: the identifier is resolved to a type variable - TypeVariable var = rc.LookUpTypeBinder(Name); - if (var != null) { - if (Arguments.Count > 0) { - rc.Error(this, - "type variables must not be applied to arguments: {0}", - var); - } - return var; - } - - // third case: the identifier denotes a type constructor and we - // recursively resolve the arguments - TypeCtorDecl ctorDecl = rc.LookUpType(Name); - if (ctorDecl != null) { - if (Arguments.Count != ctorDecl.Arity) { - rc.Error(this, - "type constructor received wrong number of arguments: {0}", - ctorDecl); - return this; - } - return new CtorType(tok, ctorDecl, ResolveArguments(rc)); - } - - // fourth case: the identifier denotes a type synonym - TypeSynonymDecl synDecl = rc.LookUpTypeSynonym(Name); - if (synDecl != null) { - if (Arguments.Count != synDecl.TypeParameters.Count) { - rc.Error(this, - "type synonym received wrong number of arguments: {0}", - synDecl); - return this; - } - List/*!*/ resolvedArgs = ResolveArguments(rc); - Contract.Assert(resolvedArgs != null); - - return new TypeSynonymAnnotation(this.tok, synDecl, resolvedArgs); - - } - - // otherwise: this name is not declared anywhere - rc.Error(this, "undeclared type: {0}", Name); - return this; - } - - private List ResolveArguments(ResolutionContext rc) { - Contract.Requires(rc != null); - Contract.Ensures(Contract.Result>() != null); - List/*!*/ resolvedArgs = new List(); - foreach (Type/*!*/ t in Arguments) { - Contract.Assert(t != null); - resolvedArgs.Add(t.ResolveType(rc)); - } - return resolvedArgs; - } - - public override List/*!*/ FreeVariables { - get { - Contract.Ensures(Contract.Result>() != null); - - return new List(); - } - } - - public override List/*!*/ FreeProxies { - get { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return new List(); - } - } - - //----------- Linearisation ---------------------------------- - - public override void Emit(TokenTextWriter stream, int contextBindingStrength) { - //Contract.Requires(stream != null); - stream.SetToken(this); - // PR: should unresolved types be syntactically distinguished from resolved types? - CtorType.EmitCtorType(this.Name, Arguments, stream, contextBindingStrength); - } - - //----------- Getters/Issers ---------------------------------- - - public override bool IsUnresolved { - get { - return true; - } - } - public override UnresolvedTypeIdentifier/*!*/ AsUnresolved { - get { - Contract.Ensures(Contract.Result() != null); - return this; - } - } - - public override Absy StdDispatch(StandardVisitor visitor) { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitUnresolvedTypeIdentifier(this); - } - } - - //===================================================================== - - public class TypeVariable : Type { - public readonly string/*!*/ Name; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Name != null); - } - - - public TypeVariable(IToken token, string name) - : base(token) { - Contract.Requires(name != null); - Contract.Requires(token != null); - this.Name = name; - } - - //----------- Cloning ---------------------------------- - // We implement our own clone-method, because bound type variables - // have to be created in the right way. It is /not/ ok to just clone - // everything recursively - - public override Type Clone(IDictionary/*!*/ varMap) { - //Contract.Requires(cce.NonNullElements(varMap)); - Contract.Ensures(Contract.Result() != null); - // if this variable is mapped to some new variable, we take the new one - // otherwise, return this - TypeVariable res; - varMap.TryGetValue(this, out res); - if (res == null) - return this; - else - return res; - } - - public override Type CloneUnresolved() { - Contract.Ensures(Contract.Result() != null); - return this; - } - - //----------- Equality ---------------------------------- - - [Pure] - public override bool Equals(Type that, - List/*!*/ thisBoundVariables, - List/*!*/ thatBoundVariables) { - //Contract.Requires(thisBoundVariables != null); - //Contract.Requires(thatBoundVariables != null); - //Contract.Requires(that != null); - TypeVariable thatAsTypeVar = TypeProxy.FollowProxy(that.Expanded) as TypeVariable; - - if (thatAsTypeVar == null) - return false; - - int thisIndex = thisBoundVariables.LastIndexOf(this); - int thatIndex = thatBoundVariables.LastIndexOf(thatAsTypeVar); - return (thisIndex >= 0 && thisIndex == thatIndex) || - (thisIndex == -1 && thatIndex == -1 && - Object.ReferenceEquals(this, thatAsTypeVar)); - } - - //----------- Unification of types ----------- - - public override bool Unify(Type/*!*/ that, - List/*!*/ unifiableVariables, - // an idempotent substitution that describes the - // unification result up to a certain point - IDictionary/*!*/ unifier) { - //Contract.Requires(that != null); - //Contract.Requires(unifiableVariables != null); - //Contract.Requires(cce.NonNullElements(unifier)); - that = that.Expanded; - if (that is TypeProxy && !(that is ConstrainedProxy)) - return that.Unify(this, unifiableVariables, unifier); - - if (this.Equals(that)) - return true; - - if (unifiableVariables.Contains(this)) { - Type previousSubst; - unifier.TryGetValue(this, out previousSubst); - if (previousSubst == null) { - return addSubstitution(unifier, that); - } else { - // we have to unify the old instantiation with the new one - return previousSubst.Unify(that, unifiableVariables, unifier); - } - } - - // this cannot be instantiated with anything - // but that possibly can ... - - TypeVariable tv = that as TypeVariable; - - return tv != null && - unifiableVariables.Contains(tv) && - that.Unify(this, unifiableVariables, unifier); - } - - // TODO: the following might cause problems, because when applying substitutions - // to type proxies the substitutions are not propagated to the proxy - // constraints (right now at least) - private bool addSubstitution(IDictionary/*!*/ oldSolution, - // the type that "this" is instantiated with - Type/*!*/ newSubst) { - Contract.Requires(cce.NonNullDictionaryAndValues(oldSolution)); - Contract.Requires(newSubst != null); - Contract.Requires(!oldSolution.ContainsKey(this)); - - Dictionary/*!*/ newMapping = new Dictionary(); - // apply the old (idempotent) substitution to the new instantiation - Type/*!*/ substSubst = newSubst.Substitute(oldSolution); - Contract.Assert(substSubst != null); - // occurs check - if (substSubst.FreeVariables.Contains(this)) - return false; - newMapping.Add(this, substSubst); - - // apply the new substitution to the old ones to ensure idempotence - List/*!*/ keys = new List(); - keys.AddRange(oldSolution.Keys); - foreach (TypeVariable/*!*/ var in keys) { - Contract.Assert(var != null); - oldSolution[var] = oldSolution[var].Substitute(newMapping); - } - oldSolution.Add(this, substSubst); - - Contract.Assert(IsIdempotent(oldSolution)); - return true; - } - -#if OLD_UNIFICATION - public override void Unify(Type that, - List! unifiableVariables, - List! thisBoundVariables, - List! thatBoundVariables, - IDictionary result){ -Contract.Requires(result != null); -Contract.Requires(that != null); - that = that.Expanded; - int thisIndex = thisBoundVariables.LastIndexOf(this); - if (thisIndex == -1) { - // this is not a bound variable and can possibly be matched on that - // that must not contain any bound variables - List! thatFreeVars = that.FreeVariables; - if (thatBoundVariables.Any(var=> thatFreeVars.Has(var))) - throw UNIFICATION_FAILED; - - // otherwise, in case that is a typevariable it cannot be bound and - // we can just check for equality - if (this.Equals(that)) - return; - - if (!unifiableVariables.Has(this)) { - // this cannot be instantiated with anything - // but that possibly can ... - if ((that is TypeVariable) && - unifiableVariables.Has(that as TypeVariable)) { - that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result); - return; - } else { - throw UNIFICATION_FAILED; - } - } - - Type previousSubst; - result.TryGetValue(this, out previousSubst); - if (previousSubst == null) { - addSubstitution(result, that); - } else { - // we have to unify the old instantiation with the new one - previousSubst.Unify(that, unifiableVariables, thisBoundVariables, thatBoundVariables, result); - } - } else { - // this is a bound variable, that also has to be one (with the same index) - if (!(that is TypeVariable) || - thatBoundVariables.LastIndexOf(that) != thisIndex) - throw UNIFICATION_FAILED; - } - } - -#endif - - //----------- Substitution of free variables with types not containing bound variables ----------------- - - public override Type Substitute(IDictionary/*!*/ subst) { - //Contract.Requires(cce.NonNullElements(subst)); - Contract.Ensures(Contract.Result() != null); - Type res; - if (subst.TryGetValue(this, out res)) { - Contract.Assert(res != null); - return res; - } else { - return this; - } - } - - //----------- Hashcodes ---------------------------------- - - [Pure] - public override int GetHashCode(List boundVariables) { - //Contract.Requires(boundVariables != null); - int thisIndex = boundVariables.LastIndexOf(this); - if (thisIndex == -1) - return GetBaseHashCode(); - return thisIndex * 27473671; - } - - //----------- Linearisation ---------------------------------- - - public override void Emit(TokenTextWriter stream, int contextBindingStrength) { - //Contract.Requires(stream != null); - // never put parentheses around variables - stream.SetToken(this); - stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(this.Name)); - } - - //----------- Resolution ---------------------------------- - - public override Type ResolveType(ResolutionContext rc) { - //Contract.Requires(rc != null); - //Contract.Ensures(Contract.Result() != null); - // nothing to resolve - return this; - } - - public override List/*!*/ FreeVariables { - get { - Contract.Ensures(Contract.Result>() != null); - return new List { this }; - } - } - - public override List/*!*/ FreeProxies { - get { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return new List(); - } - } - - //----------- Getters/Issers ---------------------------------- - - public override bool IsVariable { - get { - return true; - } - } - public override TypeVariable/*!*/ AsVariable { - get { - Contract.Ensures(Contract.Result() != null); - return this; - } - } - - public override Absy StdDispatch(StandardVisitor visitor) { - //Contract.Requires(visitor != null); - //Contract.Ensures(Contract.Result() != null); - return visitor.VisitTypeVariable(this); - } - } - - //===================================================================== - - public class TypeProxy : Type { - static int proxies = 0; - protected readonly string/*!*/ Name; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Name != null); - } - - - public TypeProxy(IToken token, string givenName) - : this(token, givenName, "proxy") { - Contract.Requires(givenName != null); - Contract.Requires(token != null); - } - - protected TypeProxy(IToken token, string givenName, string kind) - : base(token) { - Contract.Requires(kind != null); - Contract.Requires(givenName != null); - Contract.Requires(token != null); - Name = givenName + "$" + kind + "#" + proxies; - proxies++; - } - - private Type proxyFor; - public Type ProxyFor { - // apply path shortening, and then return the value of proxyFor - get { - TypeProxy anotherProxy = proxyFor as TypeProxy; - if (anotherProxy != null && anotherProxy.proxyFor != null) { - // apply path shortening by bypassing "anotherProxy" (and possibly others) - proxyFor = anotherProxy.ProxyFor; - Contract.Assert(proxyFor != null); - } - return proxyFor; - } - } - - [Pure] - [Reads(ReadsAttribute.Reads.Everything)] - public static Type FollowProxy(Type t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); - Contract.Ensures(!(Contract.Result() is TypeProxy) || ((TypeProxy)Contract.Result()).proxyFor == null); - if (t is TypeProxy) { - Type p = ((TypeProxy)t).ProxyFor; - if (p != null) { - return p; - } - } - return t; - } - - protected void DefineProxy(Type ty) { - Contract.Requires(ty != null); - Contract.Requires(ProxyFor == null); - // follow ty down to the leaf level, so that we can avoid creating a cycle - ty = FollowProxy(ty); - if (!object.ReferenceEquals(this, ty)) { - proxyFor = ty; - } - } - - //----------- Cloning ---------------------------------- - - public override Type Clone(IDictionary/*!*/ varMap) { - //Contract.Requires(cce.NonNullElements(varMap)); - Contract.Ensures(Contract.Result() != null); - Type p = ProxyFor; - if (p != null) { - return p.Clone(varMap); - } else { - return new TypeProxy(this.tok, this.Name); // the clone will have a name that ends with $proxy$proxy - } - } - - public override Type CloneUnresolved() { - Contract.Ensures(Contract.Result() != null); - return new TypeProxy(this.tok, this.Name); // the clone will have a name that ends with $proxy$proxy - } - - //----------- Equality ---------------------------------- - - [Pure] - public override bool Equals(Type that, - List/*!*/ thisBoundVariables, - List/*!*/ thatBoundVariables) { - //Contract.Requires(thisBoundVariables != null); - //Contract.Requires(thatBoundVariables != null); - //Contract.Requires(that != null); - if (object.ReferenceEquals(this, that)) { - return true; - } - Type p = ProxyFor; - if (p != null) { - return p.Equals(that, thisBoundVariables, thatBoundVariables); - } else { - // This proxy could be made to be equal to anything, so what to return? - return false; - } - } - - //----------- Unification of types ----------- - - // determine whether the occurs check fails: this is a strict subtype of that - protected bool ReallyOccursIn(Type that) { - Contract.Requires(that != null); - that = FollowProxy(that.Expanded); - return that.FreeProxies.Contains(this) && - (that.IsCtor || that.IsMap && this != that && this.ProxyFor != that); - } - - public override bool Unify(Type that, - List/*!*/ unifiableVariables, - IDictionary result) { - //Contract.Requires(cce.NonNullElements(result)); - //Contract.Requires(unifiableVariables != null); - //Contract.Requires(that != null); - Type p = ProxyFor; - if (p != null) { - return p.Unify(that, unifiableVariables, result); - } else { - // unify this with that - if (this.ReallyOccursIn(that)) - return false; - DefineProxy(that.Expanded); - return true; - } - } - - //----------- Substitution of free variables with types not containing bound variables ----------------- - - public override Type Substitute(IDictionary/*!*/ subst) { - //Contract.Requires(cce.NonNullElements(subst)); - Contract.Ensures(Contract.Result() != null); - Type p = ProxyFor; - if (p != null) { - return p.Substitute(subst); - } else { - return this; - } - } - - //----------- Hashcodes ---------------------------------- - - [Pure] - public override int GetHashCode(List boundVariables) { - //Contract.Requires(boundVariables != null); - Type p = ProxyFor; - if (p != null) { - return p.GetHashCode(boundVariables); - } else { - return GetBaseHashCode(); - } - } - - //----------- Linearisation ---------------------------------- - - public override void Emit(TokenTextWriter stream, int contextBindingStrength) { - //Contract.Requires(stream != null); - Type p = ProxyFor; - if (p != null) { - p.Emit(stream, contextBindingStrength); - } else { - // no need for parentheses - stream.SetToken(this); - stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(this.Name)); - } - } - - //----------- Resolution ---------------------------------- - - public override Type ResolveType(ResolutionContext rc) { - //Contract.Requires(rc != null); - Contract.Ensures(Contract.Result() != null); - Type p = ProxyFor; - if (p != null) { - return p.ResolveType(rc); - } else { - return this; - } - } - - public override List/*!*/ FreeVariables { - get { - Contract.Ensures(Contract.Result>() != null); - - Type p = ProxyFor; - if (p != null) { - return p.FreeVariables; - } else { - return new List(); - } - } - } - - public override List/*!*/ FreeProxies { - get { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - Type p = ProxyFor; - if (p != null) { - return p.FreeProxies; - } else { - List/*!*/ res = new List(); - res.Add(this); - return res; - } - } - } - - //----------- Getters/Issers ---------------------------------- - - public override bool IsBasic { - get { - Type p = ProxyFor; - return p != null && p.IsBasic; - } - } - public override bool IsInt { - get { - Type p = ProxyFor; - return p != null && p.IsInt; - } - } - public override bool IsReal { - get { - Type p = ProxyFor; - return p != null && p.IsReal; - } - } - public override bool IsFloat { - get { - Type p = ProxyFor; - return p != null && p.IsFloat; - } - } - public override bool IsBool { - get { - Type p = ProxyFor; - return p != null && p.IsBool; - } - } - - public override bool IsVariable { - get { - Type p = ProxyFor; - return p != null && p.IsVariable; - } - } - public override TypeVariable/*!*/ AsVariable { - get { - Contract.Ensures(Contract.Result() != null); - - Type p = ProxyFor; - Contract.Assume(p != null); - return p.AsVariable; - } - } - - public override bool IsCtor { - get { - Type p = ProxyFor; - return p != null && p.IsCtor; - } - } - public override CtorType/*!*/ AsCtor { - get { - Contract.Ensures(Contract.Result() != null); - - Type p = ProxyFor; - Contract.Assume(p != null); - return p.AsCtor; - } - } - public override bool IsMap { - get { - Type p = ProxyFor; - return p != null && p.IsMap; - } - } - public override MapType/*!*/ AsMap { - get { - Contract.Ensures(Contract.Result() != null); - - Type p = ProxyFor; - Contract.Assume(p != null); - return p.AsMap; - } - } - public override int MapArity { - get { - Type p = ProxyFor; - Contract.Assume(p != null); - return p.MapArity; - } - } - public override bool IsUnresolved { - get { - Type p = ProxyFor; - return p != null && p.IsUnresolved; - } - } - public override UnresolvedTypeIdentifier/*!*/ AsUnresolved { - get { - Contract.Ensures(Contract.Result() != null); - - Type p = ProxyFor; - Contract.Assume(p != null); - return p.AsUnresolved; - } - } - - public override bool IsBv { - get { - Type p = ProxyFor; - return p != null && p.IsBv; - } - } - public override int BvBits { - get { - Type p = ProxyFor; - Contract.Assume(p != null); - return p.BvBits; - } - } - - public override Absy StdDispatch(StandardVisitor visitor) { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitTypeProxy(this); - } - } - - public abstract class ConstrainedProxy : TypeProxy { - protected ConstrainedProxy(IToken token, string givenName, string kind) - : base(token, givenName, kind) { - Contract.Requires(kind != null); - Contract.Requires(givenName != null); - Contract.Requires(token != null); - } - } - - /// - /// Each instance of this class represents a set of bitvector types. In particular, it represents - /// a bitvector type bvN iff - /// minBits ATMOST N and - /// foreach constraint (t0,t1), the types represented by t0 and t1 are bitvector types whose - /// number of bits add up to N. - /// This means that the size of a BvTypeProxy p is constrained not only by p.minBits, but also - /// by the size of various t0 and t1 types that are transitively part of BvTypeProxy constraints. - /// If such a t0 or t1 were to get its ProxyFor field defined, then p would have to be further - /// constrained too. This doesn't seem like it would ever occur in a Boogie 2 program, because: - /// the only place where a BvTypeProxy with constraints can occur is as the type of a - /// BvConcatExpr, and - /// the types of all local variables are explicitly declared, which means that the types of - /// subexpressions of a BvConcatExpr are not going to change other than via the type of the - /// BvConcatExpr. - /// So, this implementation of BvTypeProxy does not keep track of where a BvTypeProxy may occur - /// transitively in some other BvTypeProxy's constraints. - /// - public class BvTypeProxy : ConstrainedProxy { - public int MinBits; - List constraints; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(constraints, true)); - } - - class BvTypeConstraint { - public Type/*!*/ T0; - public Type/*!*/ T1; - public BvTypeConstraint(Type t0, Type t1) { - Contract.Requires(t1 != null); - Contract.Requires(t0 != null); - Contract.Requires(t0.IsBv && t1.IsBv); - T0 = t0; - T1 = t1; - } - } - - public BvTypeProxy(IToken token, string name, int minBits) - : base(token, name, "bv" + minBits + "proxy") { - Contract.Requires(name != null); - Contract.Requires(token != null); - this.MinBits = minBits; - } - - /// - /// Requires that any further constraints to be placed on t0 and t1 go via the object to - /// be constructed. - /// - public BvTypeProxy(IToken token, string name, Type t0, Type t1) - : base(token, name, "bvproxy") { - Contract.Requires(t1 != null); - Contract.Requires(t0 != null); - Contract.Requires(name != null); - Contract.Requires(token != null); - Contract.Requires(t0.IsBv && t1.IsBv); - t0 = FollowProxy(t0); - t1 = FollowProxy(t1); - this.MinBits = MinBitsFor(t0) + MinBitsFor(t1); - List list = new List(); - list.Add(new BvTypeConstraint(t0, t1)); - this.constraints = list; - } - - /// - /// Construct a BvTypeProxy like p, but with minBits. - /// - private BvTypeProxy(BvTypeProxy p, int minBits) - : base(p.tok, p.Name, "") { - Contract.Requires(p != null); - this.MinBits = minBits; - this.constraints = p.constraints; - } - - private BvTypeProxy(IToken token, string name, int minBits, List constraints) - : base(token, name, "") { - Contract.Requires(cce.NonNullElements(constraints, true)); - Contract.Requires(name != null); - Contract.Requires(token != null); - this.MinBits = minBits; - this.constraints = constraints; - } - - [Pure] - [Reads(ReadsAttribute.Reads.Everything)] - private static int MinBitsFor(Type t) { - Contract.Requires(t != null); - Contract.Requires(t.IsBv); - Contract.Ensures(0 <= Contract.Result()); - - if (t is TypeSynonymAnnotation) { - return MinBitsFor(((TypeSynonymAnnotation)t).ExpandedType); - } - - if (t is BvType) { - return t.BvBits; - } else { - return ((BvTypeProxy)t).MinBits; - } - } - - //----------- Cloning ---------------------------------- - - public override Type Clone(IDictionary/*!*/ varMap) { - //Contract.Requires(cce.NonNullElements(varMap)); - Contract.Ensures(Contract.Result() != null); - Type p = ProxyFor; - if (p != null) { - return p.Clone(varMap); - } else { - return new BvTypeProxy(this.tok, this.Name, this.MinBits, this.constraints); // the clone will have a name that ends with $bvproxy$bvproxy - } - } - - public override Type CloneUnresolved() { - Contract.Ensures(Contract.Result() != null); - return new BvTypeProxy(this.tok, this.Name, this.MinBits, this.constraints); // the clone will have a name that ends with $bvproxy$bvproxy - } - - //----------- Unification of types ----------- - - public override bool Unify(Type that, - List unifiableVariables, - IDictionary result) { - //Contract.Requires(cce.NonNullElements(result)); - //Contract.Requires(unifiableVariables != null); - //Contract.Requires(that != null); - Type p = ProxyFor; - if (p != null) { - return p.Unify(that, unifiableVariables, result); - } - - // unify this with that, if possible - that = that.Expanded; - that = FollowProxy(that); - - if (this.ReallyOccursIn(that)) - return false; - - TypeVariable tv = that as TypeVariable; - - if (tv != null && unifiableVariables.Contains(tv)) - return that.Unify(this, unifiableVariables, result); - - if (object.ReferenceEquals(this, that)) { - return true; - } else if (that is BvType) { - if (MinBits <= that.BvBits) { - if (constraints != null) { - foreach (BvTypeConstraint btc in constraints) { - int minT1 = MinBitsFor(btc.T1); - int left = IncreaseBits(btc.T0, that.BvBits - minT1); - left = IncreaseBits(btc.T1, minT1 + left); - Contract.Assert(left == 0); // because it should always be possible to increase the total size of a BvTypeConstraint pair (t0,t1) arbitrarily - } - } - DefineProxy(that); - return true; - } - } else if (that is BvTypeProxy) { - BvTypeProxy bt = (BvTypeProxy)that; - // keep the proxy with the stronger constraint (that is, the higher minBits), but if either - // has a constraints list, then concatenate both constraints lists and define the previous - // proxies to the new one - if (this.constraints != null || bt.constraints != null) { - List list = new List(); - if (this.constraints != null) { - list.AddRange(this.constraints); - } - if (bt.constraints != null) { - list.AddRange(bt.constraints); - } - BvTypeProxy np = new BvTypeProxy(this.tok, this.Name, Math.Max(this.MinBits, bt.MinBits), list); - this.DefineProxy(np); - bt.DefineProxy(np); - } else if (this.MinBits <= bt.MinBits) { - this.DefineProxy(bt); - } else { - bt.DefineProxy(this); - } - return true; - } else if (that is ConstrainedProxy) { - // only bitvector proxies can be unified with this BvTypeProxy - return false; - } else if (that is TypeProxy) { - // define: that.ProxyFor := this; - return that.Unify(this, unifiableVariables, result); - } - return false; - } - - private static int IncreaseBits(Type t, int to) { - Contract.Requires(t != null); - Contract.Requires(t.IsBv && 0 <= to && MinBitsFor(t) <= to); - Contract.Ensures(0 <= Contract.Result() && Contract.Result() <= to); - - if(t is TypeSynonymAnnotation) { - return IncreaseBits(((TypeSynonymAnnotation)t).ExpandedType, to); - } - - t = FollowProxy(t); - if (t is BvType) { - return to - t.BvBits; - } else { - BvTypeProxy p = (BvTypeProxy)t; - Contract.Assert(p.MinBits <= to); - if (p.MinBits < to) { - BvTypeProxy q = new BvTypeProxy(p, to); - p.DefineProxy(q); - } - return 0; // we were able to satisfy the request completely - } - } - - //----------- Substitution of free variables with types not containing bound variables ----------------- - - public override Type Substitute(IDictionary/*!*/ subst) { - //Contract.Requires(cce.NonNullElements(subst)); - Contract.Ensures(Contract.Result() != null); - if (this.ProxyFor == null) { - // check that the constraints are clean and do not contain any - // of the substituted variables (otherwise, we are in big trouble) - Contract.Assert(Contract.ForAll(constraints, c => - Contract.ForAll(subst.Keys, var => - !c.T0.FreeVariables.Contains(var) && !c.T1.FreeVariables.Contains(var)))); - } - return base.Substitute(subst); - } - - //----------- Getters/Issers ---------------------------------- - - public override bool IsBv { - get { - return true; - } - } - public override int BvBits { - get { - // This method is supposed to return the number of bits supplied, but unless the proxy has been resolved, - // we only have a lower bound on the number of bits supplied. But this method is not supposed to be - // called until type checking has finished, at which time the minBits is stable. - Type p = ProxyFor; - if (p != null) { - return p.BvBits; - } else { - return MinBits; - } - } - } - - public override Absy StdDispatch(StandardVisitor visitor) { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitBvTypeProxy(this); - } - } - - // Proxy representing map types with a certain arity. Apart from the arity, - // a number of constraints on the index and value type of the map type may - // be known (such constraints result from applied select and store operations). - // Because map type can be polymorphic (in the most general case, each index or - // value type is described by a separate type parameter) any combination of - // constraints can be satisfied. - public class MapTypeProxy : ConstrainedProxy { - public readonly int Arity; - private readonly List/*!*/ constraints = new List(); - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(constraints != null); - } - - - // each constraint specifies that the given combination of argument/result - // types must be a possible instance of the formal map argument/result types - private struct Constraint { - public readonly List/*!*/ Arguments; - public readonly Type/*!*/ Result; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Arguments != null); - Contract.Invariant(Result != null); - } - - - public Constraint(List arguments, Type result) { - Contract.Requires(result != null); - Contract.Requires(arguments != null); - Arguments = arguments; - Result = result; - } - - public Constraint Clone(IDictionary/*!*/ varMap) { - Contract.Requires(cce.NonNullDictionaryAndValues(varMap)); - List/*!*/ args = new List(); - foreach (Type/*!*/ t in Arguments) { - Contract.Assert(t != null); - args.Add(t.Clone(varMap)); - } - Type/*!*/ res = Result.Clone(varMap); - Contract.Assert(res != null); - return new Constraint(args, res); - } - - public bool Unify(MapType that, - List/*!*/ unifiableVariables, - IDictionary/*!*/ result) { - Contract.Requires(unifiableVariables != null); - Contract.Requires(cce.NonNullDictionaryAndValues(result)); - Contract.Requires(that != null); - Contract.Requires(Arguments.Count == that.Arguments.Count); - Dictionary/*!*/ subst = new Dictionary(); - foreach (TypeVariable/*!*/ tv in that.TypeParameters) { - Contract.Assert(tv != null); - TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name); - subst.Add(tv, proxy); - } - - bool good = true; - for (int i = 0; i < that.Arguments.Count; i++) { - Type t0 = that.Arguments[i].Substitute(subst); - Type t1 = this.Arguments[i]; - good &= t0.Unify(t1, unifiableVariables, result); - } - good &= that.Result.Substitute(subst).Unify(this.Result, unifiableVariables, result); - return good; - } - } - - public MapTypeProxy(IToken token, string name, int arity) - : base(token, name, "mapproxy") { - Contract.Requires(name != null); - Contract.Requires(token != null); - Contract.Requires(0 <= arity); - this.Arity = arity; - } - - private void AddConstraint(Constraint c) { - Contract.Requires(c.Arguments.Count == Arity); - - Type f = ProxyFor; - MapType mf = f as MapType; - if (mf != null) { - bool success = c.Unify(mf, new List(), new Dictionary()); - Contract.Assert(success); - return; - } - - MapTypeProxy mpf = f as MapTypeProxy; - if (mpf != null) { - mpf.AddConstraint(c); - return; - } - - Contract.Assert(f == null); // no other types should occur as specialisations of this proxy - - constraints.Add(c); - } - - public Type CheckArgumentTypes(List/*!*/ actualArgs, - out TypeParamInstantiation/*!*/ tpInstantiation, - IToken/*!*/ typeCheckingSubject, - string/*!*/ opName, - TypecheckingContext/*!*/ tc) { - Contract.Requires(actualArgs != null); - Contract.Requires(typeCheckingSubject != null); - Contract.Requires(opName != null); - Contract.Requires(tc != null); - Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); - - - - Type f = ProxyFor; - MapType mf = f as MapType; - if (mf != null) - return mf.CheckArgumentTypes(actualArgs, out tpInstantiation, typeCheckingSubject, opName, tc); - - MapTypeProxy mpf = f as MapTypeProxy; - if (mpf != null) - return mpf.CheckArgumentTypes(actualArgs, out tpInstantiation, typeCheckingSubject, opName, tc); - - Contract.Assert(f == null); // no other types should occur as specialisations of this proxy - - // otherwise, we just record the constraints given by this usage of the map type - List/*!*/ arguments = new List(); - foreach (Expr/*!*/ e in actualArgs) { - Contract.Assert(e != null); - arguments.Add(e.Type); - } - Type/*!*/ result = new TypeProxy(tok, "result"); - Contract.Assert(result != null); - AddConstraint(new Constraint(arguments, result)); - - List/*!*/ argumentsResult = new List(); - foreach (Expr/*!*/ e in actualArgs) { - Contract.Assert(e != null); - argumentsResult.Add(e.Type); - } - argumentsResult.Add(result); - - tpInstantiation = new MapTypeProxyParamInstantiation(this, argumentsResult); - return result; - } - - //----------- Cloning ---------------------------------- - - public override Type Clone(IDictionary/*!*/ varMap) { - //Contract.Requires(cce.NonNullElements(varMap)); - Contract.Ensures(Contract.Result() != null); - Type p = ProxyFor; - if (p != null) { - return p.Clone(varMap); - } else { - MapTypeProxy p2 = new MapTypeProxy(tok, Name, Arity); - foreach (Constraint c in constraints) - p2.AddConstraint(c.Clone(varMap)); - return p2; // the clone will have a name that ends with $mapproxy$mapproxy (hopefully) - } - } - - //----------- Linearisation ---------------------------------- - - public override void Emit(TokenTextWriter stream, int contextBindingStrength) { - //Contract.Requires(stream != null); - Type p = ProxyFor; - if (p != null) { - p.Emit(stream, contextBindingStrength); - } else { - stream.Write("["); - string/*!*/ sep = ""; - for (int i = 0; i < Arity; ++i) { - stream.Write(sep); - sep = ", "; - stream.Write("?"); - } - stream.Write("]?"); - } - } - - //----------- Unification of types ----------- - - public override bool Unify(Type/*!*/ that, - List/*!*/ unifiableVariables, - IDictionary/*!*/ result) { - //Contract.Requires(that != null); - //Contract.Requires(unifiableVariables != null); - //Contract.Requires(cce.NonNullElements(result)); - Type p = ProxyFor; - if (p != null) { - return p.Unify(that, unifiableVariables, result); - } - - // unify this with that, if possible - that = that.Expanded; - that = FollowProxy(that); - - if (this.ReallyOccursIn(that)) - return false; - - TypeVariable tv = that as TypeVariable; - - if (tv != null && unifiableVariables.Contains(tv)) - return that.Unify(this, unifiableVariables, result); - - if (object.ReferenceEquals(this, that)) { - return true; - } else if (that is MapType) { - MapType mapType = (MapType)that; - if (mapType.Arguments.Count == Arity) { - bool good = true; - foreach (Constraint c in constraints) - good &= c.Unify(mapType, unifiableVariables, result); - if (good) { - DefineProxy(mapType); - return true; - } - } - } else if (that is MapTypeProxy) { - MapTypeProxy mt = (MapTypeProxy)that; - if (mt.Arity == this.Arity) { - // we propagate the constraints of this proxy to the more specific one - foreach (Constraint c in constraints) - mt.AddConstraint(c); - DefineProxy(mt); - return true; - } - } else if (that is ConstrainedProxy) { - // only map-type proxies can be unified with this MapTypeProxy - return false; - } else if (that is TypeProxy) { - // define: that.ProxyFor := this; - return that.Unify(this, unifiableVariables, result); - } - return false; - } - - //----------- Substitution of free variables with types not containing bound variables ----------------- - - public override Type Substitute(IDictionary/*!*/ subst) { - //Contract.Requires(cce.NonNullElements(subst)); - Contract.Ensures(Contract.Result() != null); - if (this.ProxyFor == null) { - // check that the constraints are clean and do not contain any - // of the substituted variables (otherwise, we are in big trouble) - Contract.Assert(Contract.ForAll(constraints, c => - Contract.ForAll(subst.Keys, var => - Contract.ForAll(0, c.Arguments.Count, t => !c.Arguments[t].FreeVariables.Contains(var)) && - !c.Result.FreeVariables.Contains(var)))); - } - return base.Substitute(subst); - } - - //----------- Getters/Issers ---------------------------------- - - public override bool IsMap { - get { - return true; - } - } - public override MapType/*!*/ AsMap { - get { - Contract.Ensures(Contract.Result() != null); - - Type p = ProxyFor; - if (p != null) { - return p.AsMap; - } else { - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } // what to do now? - } - } - } - public override int MapArity { - get { - return Arity; - } - } - - public override Absy StdDispatch(StandardVisitor visitor) { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitMapTypeProxy(this); - } - } - - //===================================================================== - - // Used to annotate types with type synoyms that were used in the - // original unresolved types. Such types should be considered as - // equivalent to ExpandedType, the annotations are only used to enable - // better pretty-printing - public class TypeSynonymAnnotation : Type { - public Type/*!*/ ExpandedType; - - public readonly List/*!*/ Arguments; - // is set during resolution and determines whether the right number of arguments is given - public readonly TypeSynonymDecl/*!*/ Decl; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(ExpandedType != null); - Contract.Invariant(Arguments != null); - Contract.Invariant(Decl != null); - } - - - public TypeSynonymAnnotation(IToken/*!*/ token, TypeSynonymDecl/*!*/ decl, List/*!*/ arguments) - : base(token) { - Contract.Requires(token != null); - Contract.Requires(decl != null); - Contract.Requires(arguments != null); - Contract.Requires(arguments.Count == decl.TypeParameters.Count); - this.Decl = decl; - this.Arguments = arguments; - - // build a substitution that can be applied to the definition of - // the type synonym - IDictionary/*!*/ subst = - new Dictionary(); - for (int i = 0; i < arguments.Count; ++i) - subst.Add(decl.TypeParameters[i], arguments[i]); - - ExpandedType = decl.Body.Substitute(subst); - } - - private TypeSynonymAnnotation(IToken/*!*/ token, TypeSynonymDecl/*!*/ decl, List/*!*/ arguments, - Type/*!*/ expandedType) - : base(token) { - Contract.Requires(token != null); - Contract.Requires(decl != null); - Contract.Requires(arguments != null); - Contract.Requires(expandedType != null); - - this.Decl = decl; - this.Arguments = arguments; - this.ExpandedType = expandedType; - } - - //----------- Cloning ---------------------------------- - // We implement our own clone-method, because bound type variables - // have to be created in the right way. It is /not/ ok to just clone - // everything recursively - - public override Type Clone(IDictionary/*!*/ varMap) { - //Contract.Requires(cce.NonNullElements(varMap)); - Contract.Ensures(Contract.Result() != null); - List/*!*/ newArgs = new List(); - foreach (Type/*!*/ t in Arguments) { - Contract.Assert(t != null); - newArgs.Add(t.Clone(varMap)); - } - Type/*!*/ newExpandedType = ExpandedType.Clone(varMap); - Contract.Assert(newExpandedType != null); - return new TypeSynonymAnnotation(tok, Decl, newArgs, newExpandedType); - } - - public override Type CloneUnresolved() { - Contract.Ensures(Contract.Result() != null); - List/*!*/ newArgs = new List(); - foreach (Type/*!*/ t in Arguments) { - Contract.Assert(t != null); - newArgs.Add(t.CloneUnresolved()); - } - return new TypeSynonymAnnotation(tok, Decl, newArgs); - } - - //----------- Equality ---------------------------------- - - [Pure] - public override bool Equals(Type/*!*/ that, - List/*!*/ thisBoundVariables, - List/*!*/ thatBoundVariables) { - //Contract.Requires(that != null); - //Contract.Requires(thisBoundVariables != null); - //Contract.Requires(thatBoundVariables != null); - return ExpandedType.Equals(that, thisBoundVariables, thatBoundVariables); - } - - // used to skip leading type annotations - internal override Type/*!*/ Expanded { - get { - Contract.Ensures(Contract.Result() != null); - - return ExpandedType.Expanded; - } - } - - //----------- Unification of types ----------- - - public override bool Unify(Type/*!*/ that, - List/*!*/ unifiableVariables, - IDictionary/*!*/ result) { - //Contract.Requires(that != null); - //Contract.Requires(unifiableVariables != null); - //Contract.Requires(cce.NonNullElements(result)); - return ExpandedType.Unify(that, unifiableVariables, result); - } - -#if OLD_UNIFICATION - public override void Unify(Type! that, - List! unifiableVariables, - List! thisBoundVariables, - List! thatBoundVariables, - IDictionary! result) { - ExpandedType.Unify(that, unifiableVariables, - thisBoundVariables, thatBoundVariables, result); - } -#endif - - //----------- Substitution of free variables with types not containing bound variables ----------------- - - public override Type Substitute(IDictionary/*!*/ subst) { - //Contract.Requires(cce.NonNullElements(subst)); - Contract.Ensures(Contract.Result() != null); - if (subst.Count == 0) - return this; - List newArgs = new List(); - foreach (Type/*!*/ t in Arguments) { - Contract.Assert(t != null); - newArgs.Add(t.Substitute(subst)); - } - Type/*!*/ newExpandedType = ExpandedType.Substitute(subst); - Contract.Assert(newExpandedType != null); - return new TypeSynonymAnnotation(tok, Decl, newArgs, newExpandedType); - } - - //----------- Hashcodes ---------------------------------- - - [Pure] - public override int GetHashCode(List boundVariables) { - //Contract.Requires(boundVariables != null); - return ExpandedType.GetHashCode(boundVariables); - } - - //----------- Linearisation ---------------------------------- - - public override void Emit(TokenTextWriter stream, int contextBindingStrength) { - //Contract.Requires(stream != null); - stream.SetToken(this); - CtorType.EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength); - } - - //----------- Resolution ---------------------------------- - - public override Type ResolveType(ResolutionContext rc) { - //Contract.Requires(rc != null); - Contract.Ensures(Contract.Result() != null); - List resolvedArgs = new List(); - foreach (Type/*!*/ t in Arguments) { - Contract.Assert(t != null); - resolvedArgs.Add(t.ResolveType(rc)); - } - return new TypeSynonymAnnotation(tok, Decl, resolvedArgs); - } - - public override List/*!*/ FreeVariables { - get { - Contract.Ensures(Contract.Result>() != null); - - return ExpandedType.FreeVariables; - } - } - - public override List/*!*/ FreeProxies { - get { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return ExpandedType.FreeProxies; - } - } - - //----------- Getters/Issers ---------------------------------- - - public override bool IsBasic { - get { - return ExpandedType.IsBasic; - } - } - public override bool IsInt { - get { - return ExpandedType.IsInt; - } - } - public override bool IsReal - { - get - { - return ExpandedType.IsReal; - } - } - public override bool IsFloat - { - get - { - return ExpandedType.IsFloat; - } - } - public override bool IsBool { - get { - return ExpandedType.IsBool; - } - } - - public override bool IsVariable { - get { - return ExpandedType.IsVariable; - } - } - public override TypeVariable/*!*/ AsVariable { - get { - Contract.Ensures(Contract.Result() != null); - return ExpandedType.AsVariable; - } - } - public override bool IsCtor { - get { - return ExpandedType.IsCtor; - } - } - public override CtorType/*!*/ AsCtor { - get { - Contract.Ensures(Contract.Result() != null); - return ExpandedType.AsCtor; - } - } - public override bool IsMap { - get { - return ExpandedType.IsMap; - } - } - public override MapType/*!*/ AsMap { - get { - Contract.Ensures(Contract.Result() != null); - return ExpandedType.AsMap; - } - } - public override bool IsUnresolved { - get { - return ExpandedType.IsUnresolved; - } - } - public override UnresolvedTypeIdentifier/*!*/ AsUnresolved { - get { - Contract.Ensures(Contract.Result() != null); - - return ExpandedType.AsUnresolved; - } - } - - public override bool IsBv { - get { - return ExpandedType.IsBv; - } - } - public override int BvBits { - get { - return ExpandedType.BvBits; - } - } - - public override Absy StdDispatch(StandardVisitor visitor) { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitTypeSynonymAnnotation(this); - } - } - - //===================================================================== - - public class CtorType : Type { - public readonly List/*!*/ Arguments; - // is set during resolution and determines whether the right number of arguments is given - public readonly TypeCtorDecl/*!*/ Decl; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Arguments != null); - Contract.Invariant(Decl != null); - } - - - public CtorType(IToken/*!*/ token, TypeCtorDecl/*!*/ decl, List/*!*/ arguments) - : base(token) { - Contract.Requires(token != null); - Contract.Requires(decl != null); - Contract.Requires(arguments != null); - Contract.Requires(arguments.Count == decl.Arity); - this.Decl = decl; - this.Arguments = arguments; - } - - public bool IsDatatype() { - return QKeyValue.FindBoolAttribute(Decl.Attributes, "datatype"); - } - - //----------- Cloning ---------------------------------- - // We implement our own clone-method, because bound type variables - // have to be created in the right way. It is /not/ ok to just clone - // everything recursively - - public override Type Clone(IDictionary/*!*/ varMap) { - //Contract.Requires(cce.NonNullElements(varMap)); - Contract.Ensures(Contract.Result() != null); - List/*!*/ newArgs = new List(); - foreach (Type/*!*/ t in Arguments) { - Contract.Assert(t != null); - newArgs.Add(t.Clone(varMap)); - } - return new CtorType(tok, Decl, newArgs); - } - - public override Type CloneUnresolved() { - Contract.Ensures(Contract.Result() != null); - List/*!*/ newArgs = new List(); - foreach (Type/*!*/ t in Arguments) { - Contract.Assert(t != null); - newArgs.Add(t.CloneUnresolved()); - } - return new CtorType(tok, Decl, newArgs); - } - - //----------- Equality ---------------------------------- - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object that) { - Type thatType = that as Type; - if (thatType == null) - return false; - thatType = TypeProxy.FollowProxy(thatType.Expanded); - // shortcut - CtorType thatCtorType = thatType as CtorType; - if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl)) - return false; - if (Arguments.Count == 0) - return true; - return base.Equals(thatType); - } - - [Pure] - public override bool Equals(Type/*!*/ that, - List/*!*/ thisBoundVariables, - List/*!*/ thatBoundVariables) { - that = TypeProxy.FollowProxy(that.Expanded); - CtorType thatCtorType = that as CtorType; - if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl)) - return false; - for (int i = 0; i < Arguments.Count; ++i) { - if (!Arguments[i].Equals(thatCtorType.Arguments[i], - thisBoundVariables, thatBoundVariables)) - return false; - } - return true; - } - - //----------- Unification of types ----------- - - public override bool Unify(Type/*!*/ that, - List/*!*/ unifiableVariables, - IDictionary/*!*/ result) { - that = that.Expanded; - if (that is TypeProxy || that is TypeVariable) - return that.Unify(this, unifiableVariables, result); - - CtorType thatCtorType = that as CtorType; - if (thatCtorType == null || !thatCtorType.Decl.Equals(Decl)) { - return false; - } else { - bool good = true; - for (int i = 0; i < Arguments.Count; ++i) - good &= Arguments[i].Unify(thatCtorType.Arguments[i], unifiableVariables, result); - return good; - } - } - -#if OLD_UNIFICATION - public override void Unify(Type! that, - List! unifiableVariables, - List! thisBoundVariables, - List! thatBoundVariables, - IDictionary! result) { - that = that.Expanded; - if (that is TypeVariable) { - that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result); - return; - } - - CtorType thatCtorType = that as CtorType; - if (thatCtorType == null || !thatCtorType.Decl.Equals(Decl)) - throw UNIFICATION_FAILED; - for (int i = 0; i < Arguments.Length; ++i) - Arguments[i].Unify(thatCtorType.Arguments[i], - unifiableVariables, - thisBoundVariables, thatBoundVariables, - result); - } -#endif - - //----------- Substitution of free variables with types not containing bound variables ----------------- - - public override Type Substitute(IDictionary/*!*/ subst) { - //Contract.Requires(cce.NonNullElements(subst)); - Contract.Ensures(Contract.Result() != null); - if (subst.Count == 0) - return this; - List newArgs = new List(); - lock (Arguments) - { - foreach (Type/*!*/ t in Arguments) - { - Contract.Assert(t != null); - newArgs.Add(t.Substitute(subst)); - } - } - return new CtorType(tok, Decl, newArgs); - } - - //----------- Hashcodes ---------------------------------- - - [Pure] - public override int GetHashCode(List boundVariables) { - //Contract.Requires(boundVariables != null); - int res = 1637643879 * Decl.GetHashCode(); - foreach (Type/*!*/ t in Arguments.ToArray()) { - Contract.Assert(t != null); - res = res * 3 + t.GetHashCode(boundVariables); - } - return res; - } - - //----------- Linearisation ---------------------------------- - - public override void Emit(TokenTextWriter stream, int contextBindingStrength) { - //Contract.Requires(stream != null); - stream.SetToken(this); - EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength); - } - - internal static void EmitCtorType(string name, List args, TokenTextWriter stream, int contextBindingStrength) { - Contract.Requires(stream != null); - Contract.Requires(args != null); - Contract.Requires(name != null); - int opBindingStrength = args.Count > 0 ? 0 : 2; - if (opBindingStrength < contextBindingStrength) - stream.Write("("); - - stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(name)); - int i = args.Count; - foreach (Type/*!*/ t in args) { - Contract.Assert(t != null); - stream.Write(" "); - // use a lower binding strength for the last argument - // to allow map-types without parentheses - t.Emit(stream, i == 1 ? 1 : 2); - i = i - 1; - } - - if (opBindingStrength < contextBindingStrength) - stream.Write(")"); - } - - //----------- Resolution ---------------------------------- - - public override Type ResolveType(ResolutionContext rc) { - //Contract.Requires(rc != null); - Contract.Ensures(Contract.Result() != null); - List resolvedArgs = new List(); - foreach (Type/*!*/ t in Arguments) { - Contract.Assert(t != null); - resolvedArgs.Add(t.ResolveType(rc)); - } - return new CtorType(tok, Decl, resolvedArgs); - } - - public override List/*!*/ FreeVariables { - get { - List/*!*/ res = new List(); - foreach (Type/*!*/ t in Arguments.ToArray()) { - Contract.Assert(t != null); - res.AppendWithoutDups(t.FreeVariables); - } - return res; - } - } - - public override List/*!*/ FreeProxies { - get { - List/*!*/ res = new List(); - foreach (Type/*!*/ t in Arguments.ToArray()) { - Contract.Assert(t != null); - AppendWithoutDups(res, t.FreeProxies); - } - return res; - } - } - - //----------- Getters/Issers ---------------------------------- - - public override bool IsCtor { - get { - return true; - } - } - public override CtorType/*!*/ AsCtor { - get { - return this; - } - } - - public override Absy StdDispatch(StandardVisitor visitor) { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitCtorType(this); - } - } - - //===================================================================== - - public class MapType : Type { - // an invariant is that each of the type parameters has to occur as - // free variable in at least one of the arguments - public readonly List/*!*/ TypeParameters; - public readonly List/*!*/ Arguments; - public Type/*!*/ Result; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(TypeParameters != null); - Contract.Invariant(Arguments != null); - Contract.Invariant(Result != null); - } - - - public MapType(IToken/*!*/ token, List/*!*/ typeParameters, List/*!*/ arguments, Type/*!*/ result) - : base(token) { - Contract.Requires(token != null); - Contract.Requires(typeParameters != null); - Contract.Requires(arguments != null); - Contract.Requires(result != null); - - this.TypeParameters = typeParameters; - this.Result = result; - this.Arguments = arguments; - } - - //----------- Cloning ---------------------------------- - // We implement our own clone-method, because bound type variables - // have to be created in the right way. It is /not/ ok to just clone - // everything recursively - - public override Type Clone(IDictionary/*!*/ varMap) { - //Contract.Requires(cce.NonNullElements(varMap)); - Contract.Ensures(Contract.Result() != null); - IDictionary/*!*/ newVarMap = - new Dictionary(); - foreach (KeyValuePair p in varMap) { - Contract.Assert(cce.NonNullElements(p)); - if (!TypeParameters.Contains(p.Key)) - newVarMap.Add(p); - } - - List/*!*/ newTypeParams = new List(); - foreach (TypeVariable/*!*/ var in TypeParameters) { - Contract.Assert(var != null); - TypeVariable/*!*/ newVar = new TypeVariable(var.tok, var.Name); - Contract.Assert(newVar != null); - newVarMap.Add(var, newVar); - newTypeParams.Add(newVar); - } - - List/*!*/ newArgs = new List(); - foreach (Type/*!*/ t in Arguments) { - Contract.Assert(t != null); - newArgs.Add(t.Clone(newVarMap)); - } - Type/*!*/ newResult = Result.Clone(newVarMap); - Contract.Assert(newResult != null); - - return new MapType(this.tok, newTypeParams, newArgs, newResult); - } - - public override Type CloneUnresolved() { - Contract.Ensures(Contract.Result() != null); - List/*!*/ newTypeParams = new List(); - foreach (TypeVariable/*!*/ var in TypeParameters) { - Contract.Assert(var != null); - TypeVariable/*!*/ newVar = new TypeVariable(var.tok, var.Name); - Contract.Assert(newVar != null); - newTypeParams.Add(newVar); - } - - List/*!*/ newArgs = new List(); - foreach (Type/*!*/ t in Arguments) { - Contract.Assert(t != null); - newArgs.Add(t.CloneUnresolved()); - } - Type/*!*/ newResult = Result.CloneUnresolved(); - Contract.Assert(newResult != null); - - return new MapType(this.tok, newTypeParams, newArgs, newResult); - } - - //----------- Equality ---------------------------------- - - [Pure] - public override bool Equals(Type/*!*/ that, - List/*!*/ thisBoundVariables, - List/*!*/ thatBoundVariables) - { - that = TypeProxy.FollowProxy(that.Expanded); - MapType thatMapType = that as MapType; - if (thatMapType == null || - this.TypeParameters.Count != thatMapType.TypeParameters.Count || - this.Arguments.Count != thatMapType.Arguments.Count) - return false; - - thisBoundVariables = thisBoundVariables.ToList(); - foreach (TypeVariable/*!*/ var in this.TypeParameters) - { - Contract.Assert(var != null); - thisBoundVariables.Add(var); - } - thatBoundVariables = thatBoundVariables.ToList(); - foreach (TypeVariable/*!*/ var in thatMapType.TypeParameters) - { - Contract.Assert(var != null); - thatBoundVariables.Add(var); - } - - for (int i = 0; i < Arguments.Count; ++i) - { - if (!Arguments[i].Equals(thatMapType.Arguments[i], - thisBoundVariables, thatBoundVariables)) - return false; - } - - return this.Result.Equals(thatMapType.Result, - thisBoundVariables, thatBoundVariables); - } - - //----------- Unification of types ----------- - - public override bool Unify(Type/*!*/ that, - List/*!*/ unifiableVariables, - IDictionary/*!*/ result) { - that = that.Expanded; - if (that is TypeProxy || that is TypeVariable) - return that.Unify(this, unifiableVariables, result); - - MapType thatMapType = that as MapType; - if (thatMapType == null || - this.TypeParameters.Count != thatMapType.TypeParameters.Count || - this.Arguments.Count != thatMapType.Arguments.Count) - return false; - - // treat the bound variables of the two map types as equal... - Dictionary/*!*/ subst0 = - new Dictionary(); - Dictionary/*!*/ subst1 = - new Dictionary(); - List freshies = new List(); - for (int i = 0; i < this.TypeParameters.Count; i++) { - TypeVariable tp0 = this.TypeParameters[i]; - TypeVariable tp1 = thatMapType.TypeParameters[i]; - TypeVariable freshVar = new TypeVariable(tp0.tok, tp0.Name); - freshies.Add(freshVar); - subst0.Add(tp0, freshVar); - subst1.Add(tp1, freshVar); - } - // ... and then unify the domain and range types - bool good = true; - for (int i = 0; i < this.Arguments.Count; i++) { - Type t0 = this.Arguments[i].Substitute(subst0); - Type t1 = thatMapType.Arguments[i].Substitute(subst1); - good &= t0.Unify(t1, unifiableVariables, result); - } - Type r0 = this.Result.Substitute(subst0); - Type r1 = thatMapType.Result.Substitute(subst1); - good &= r0.Unify(r1, unifiableVariables, result); - - // Finally, check that none of the bound variables has escaped - if (good && freshies.Count != 0) { - // This is done by looking for occurrences of the fresh variables in the - // non-substituted types ... - List freeVars = this.FreeVariables; - foreach (TypeVariable fr in freshies) - if (freeVars.Contains(fr)) { - return false; - } // fresh variable escaped - freeVars = thatMapType.FreeVariables; - foreach (TypeVariable fr in freshies) - if (freeVars.Contains(fr)) { - return false; - } // fresh variable escaped - - // ... and in the resulting unifier of type variables - foreach (KeyValuePair pair in result) { - Contract.Assert(cce.NonNullElements(pair)); - freeVars = pair.Value.FreeVariables; - foreach (TypeVariable fr in freshies) - if (freeVars.Contains(fr)) { - return false; - } // fresh variable escaped - } - } - - return good; - } - -#if OLD_UNIFICATION - public override void Unify(Type! that, - List! unifiableVariables, - List! thisBoundVariables, - List! thatBoundVariables, - IDictionary! result) { - that = that.Expanded; - if (that is TypeVariable) { - that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result); - return; - } - - MapType thatMapType = that as MapType; - if (thatMapType == null || - this.TypeParameters.Length != thatMapType.TypeParameters.Length || - this.Arguments.Length != thatMapType.Arguments.Length) - throw UNIFICATION_FAILED; - - // ensure that no collisions occur - if (this.collisionsPossible(result)) { - ((MapType)this.Clone()) - .Unify(that, unifiableVariables, - thisBoundVariables, thatBoundVariables, result); - return; - } - if (thatMapType.collisionsPossible(result)) - thatMapType = (MapType)that.Clone(); - - foreach(TypeVariable/*!*/ var in this.TypeParameters){ -Contract.Assert(var != null); - thisBoundVariables.Add(var);} - foreach(TypeVariable/*!*/ var in thatMapType.TypeParameters){ -Contract.Assert(var != null); - thatBoundVariables.Add(var);} - - try { - - for (int i = 0; i < Arguments.Length; ++i) - Arguments[i].Unify(thatMapType.Arguments[i], - unifiableVariables, - thisBoundVariables, thatBoundVariables, - result); - Result.Unify(thatMapType.Result, - unifiableVariables, - thisBoundVariables, thatBoundVariables, - result); - - } finally { - // make sure that the bound variables are removed again - for (int i = 0; i < this.TypeParameters.Length; ++i) { - thisBoundVariables.Remove(); - thatBoundVariables.Remove(); - } - } - } -#endif - - //----------- Substitution of free variables with types not containing bound variables ----------------- - - [Pure] - private bool collisionsPossible(IDictionary/*!*/ subst) { - Contract.Requires(cce.NonNullDictionaryAndValues(subst)); - // PR: could be written more efficiently - return TypeParameters.Any(param => subst.ContainsKey(param) || subst.Values.Any(val => val.FreeVariables.Contains(param))); - } - - public override Type Substitute(IDictionary/*!*/ subst) { - //Contract.Requires(cce.NonNullElements(subst)); - Contract.Ensures(Contract.Result() != null); - if (subst.Count == 0) - return this; - - // there are two cases in which we have to be careful: - // * a variable to be substituted is shadowed by a variable binder - // * a substituted term contains variables that are bound in the - // type (variable capture) - // - // in both cases, we first clone the type to ensure that bound - // variables are fresh - - if (collisionsPossible(subst)) { - MapType/*!*/ newType = (MapType)this.Clone(); - Contract.Assert(newType != null); - Contract.Assert(newType.Equals(this) && !newType.collisionsPossible(subst)); - return newType.Substitute(subst); - } - - List newArgs = new List(); - lock (Arguments) - { - foreach (Type/*!*/ t in Arguments) - { - Contract.Assert(t != null); - newArgs.Add(t.Substitute(subst)); - } - } - Type/*!*/ newResult = Result.Substitute(subst); - Contract.Assert(newResult != null); - - return new MapType(tok, TypeParameters, newArgs, newResult); - } - - //----------- Hashcodes ---------------------------------- - - [Pure] - public override int GetHashCode(List boundVariables) { - //Contract.Requires(boundVariables != null); - int res = 7643761 * TypeParameters.Count + 65121 * Arguments.Count; - - boundVariables = boundVariables.ToList(); - foreach (TypeVariable/*!*/ var in this.TypeParameters) { - Contract.Assert(var != null); - boundVariables.Add(var); - } - - foreach (Type/*!*/ t in Arguments.ToArray()) { - Contract.Assert(t != null); - res = res * 5 + t.GetHashCode(boundVariables); - } - res = res * 7 + Result.GetHashCode(boundVariables); - - return res; - } - - //----------- Linearisation ---------------------------------- - - public override void Emit(TokenTextWriter stream, int contextBindingStrength) { - //Contract.Requires(stream != null); - stream.SetToken(this); - - const int opBindingStrength = 1; - if (opBindingStrength < contextBindingStrength) - stream.Write("("); - - EmitOptionalTypeParams(stream, TypeParameters); - - stream.Write("["); - Arguments.Emit(stream, ","); // default binding strength of 0 is ok - stream.Write("]"); - Result.Emit(stream); // default binding strength of 0 is ok - - if (opBindingStrength < contextBindingStrength) - stream.Write(")"); - } - - //----------- Resolution ---------------------------------- - - public override Type ResolveType(ResolutionContext rc) { - //Contract.Requires(rc != null); - Contract.Ensures(Contract.Result() != null); - int previousState = rc.TypeBinderState; - try { - foreach (TypeVariable/*!*/ v in TypeParameters) { - Contract.Assert(v != null); - rc.AddTypeBinder(v); - } - - List resolvedArgs = new List(); - foreach (Type/*!*/ ty in Arguments) { - Contract.Assert(ty != null); - resolvedArgs.Add(ty.ResolveType(rc)); - } - - Type resolvedResult = Result.ResolveType(rc); - - CheckBoundVariableOccurrences(TypeParameters, - resolvedArgs, new List { resolvedResult }, - this.tok, "map arguments", - rc); - - // sort the type parameters so that they are bound in the order of occurrence - List/*!*/ sortedTypeParams = SortTypeParams(TypeParameters, resolvedArgs, resolvedResult); - Contract.Assert(sortedTypeParams != null); - return new MapType(tok, sortedTypeParams, resolvedArgs, resolvedResult); - } finally { - rc.TypeBinderState = previousState; - } - } - - public override List/*!*/ FreeVariables { - get { - List/*!*/ res = FreeVariablesIn(Arguments.ToList()); - Contract.Assert(res != null); - res.AppendWithoutDups(Result.FreeVariables); - foreach (TypeVariable/*!*/ v in TypeParameters.ToArray()) { - Contract.Assert(v != null); - res.Remove(v); - } - return res; - } - } - - public override List/*!*/ FreeProxies { - get { - List/*!*/ res = new List(); - foreach (Type/*!*/ t in Arguments.ToArray()) { - Contract.Assert(t != null); - AppendWithoutDups(res, t.FreeProxies); - } - AppendWithoutDups(res, Result.FreeProxies); - return res; - } - } - - //----------- Getters/Issers ---------------------------------- - - public override bool IsMap { - get { - return true; - } - } - public override MapType/*!*/ AsMap { - get { - return this; - } - } - public override int MapArity { - get { - return Arguments.Count; - } - } - - //------------ Match formal argument types of the map - //------------ on concrete types, substitute the result into the - //------------ result type. Null is returned if so many type checking - //------------ errors occur that the situation is hopeless - - public Type CheckArgumentTypes(List/*!*/ actualArgs, - out TypeParamInstantiation/*!*/ tpInstantiation, - IToken/*!*/ typeCheckingSubject, - string/*!*/ opName, - TypecheckingContext/*!*/ tc) { - Contract.Requires(actualArgs != null); - Contract.Requires(typeCheckingSubject != null); - - Contract.Requires(opName != null); - Contract.Requires(tc != null); -Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); - List/*!*/ actualTypeParams; - List actualResult = - Type.CheckArgumentTypes(TypeParameters, out actualTypeParams, Arguments, actualArgs, - new List { Result }, null, typeCheckingSubject, opName, tc); - if (actualResult == null) { - tpInstantiation = SimpleTypeParamInstantiation.EMPTY; - return null; - } else { - Contract.Assert(actualResult.Count == 1); - tpInstantiation = SimpleTypeParamInstantiation.From(TypeParameters, actualTypeParams); - return actualResult[0]; - } - } - - public override Absy StdDispatch(StandardVisitor visitor) { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitMapType(this); - } - } - - //--------------------------------------------------------------------- - - public enum SimpleType { - Int, - Real, - Bool - }; - - - //===================================================================== - - // Interface for representing the instantiations of type parameters of - // polymorphic functions or maps. We introduce an own interface for this - // instead of using a simple list or dictionary, because in some cases - // (due to the type proxies for map types) the actual number and instantiation - // of type parameters can only be determined very late. - [ContractClass(typeof(TypeParamInstantiationContracts))] - public interface TypeParamInstantiation { - // return what formal type parameters there are - List/*!*/ FormalTypeParams { - get; - } - // given a formal type parameter, return the actual instantiation - Type/*!*/ this[TypeVariable/*!*/ var] { - get; - } - } - [ContractClassFor(typeof(TypeParamInstantiation))] - public abstract class TypeParamInstantiationContracts : TypeParamInstantiation { - #region TypeParamInstantiation Members - - public List FormalTypeParams { - - get { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - throw new NotImplementedException(); - } - } - - public Type this[TypeVariable var] { - get { - Contract.Requires(var != null); - Contract.Ensures(Contract.Result() != null); - - throw new NotImplementedException(); - } - } - - #endregion - } - - - public class SimpleTypeParamInstantiation : TypeParamInstantiation { - private readonly List/*!*/ TypeParams; - [ContractInvariantMethod] - void TypeParamsInvariantMethod() { - Contract.Invariant(cce.NonNullElements(TypeParams)); - } - private readonly IDictionary/*!*/ Instantiations; - [ContractInvariantMethod] - void InstantiationsInvariantMethod() { - Contract.Invariant(cce.NonNullDictionaryAndValues(Instantiations)); - } - - public SimpleTypeParamInstantiation(List/*!*/ typeParams, - IDictionary/*!*/ instantiations) { - Contract.Requires(cce.NonNullElements(typeParams)); - Contract.Requires(cce.NonNullDictionaryAndValues(instantiations)); - this.TypeParams = typeParams; - this.Instantiations = instantiations; - } - - public static TypeParamInstantiation/*!*/ From(List typeParams, List/*!*/ actualTypeParams) { - Contract.Requires(cce.NonNullElements(actualTypeParams)); - Contract.Requires(typeParams != null); - Contract.Requires(typeParams.Count == actualTypeParams.Count); - Contract.Ensures(Contract.Result() != null); - - if (typeParams.Count == 0) - return EMPTY; - - List/*!*/ typeParamList = new List(); - IDictionary/*!*/ dict = new Dictionary(); - for (int i = 0; i < typeParams.Count; ++i) { - typeParamList.Add(typeParams[i]); - dict.Add(typeParams[i], actualTypeParams[i]); - } - return new SimpleTypeParamInstantiation(typeParamList, dict); - } - - public static readonly TypeParamInstantiation EMPTY = - new SimpleTypeParamInstantiation(new List(), - new Dictionary()); - - // return what formal type parameters there are - public List/*!*/ FormalTypeParams { - get { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return TypeParams; - } - } - // given a formal type parameter, return the actual instantiation - public Type/*!*/ this[TypeVariable/*!*/ var] { - get { - return Instantiations[var]; - } - } - } - - // Implementation of TypeParamInstantiation that refers to the current - // value of a MapTypeProxy. This means that the values return by the - // methods of this implementation can change in case the MapTypeProxy - // receives further unifications. - class MapTypeProxyParamInstantiation : TypeParamInstantiation { - private readonly MapTypeProxy/*!*/ Proxy; - - // the argument and result type of this particular usage of the map - // type. these are necessary to derive the values of the type parameters - private readonly List/*!*/ ArgumentsResult; - - // field that is initialised once all necessary information is available - // (the MapTypeProxy is instantiated to an actual type) and the instantiation - // of a type parameter is queried - private IDictionary Instantiations = null; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Proxy != null); - Contract.Invariant(ArgumentsResult != null); - Contract.Invariant(Instantiations == null || cce.NonNullDictionaryAndValues(Instantiations)); - } - - - public MapTypeProxyParamInstantiation(MapTypeProxy/*!*/ proxy, - List/*!*/ argumentsResult) { - Contract.Requires(proxy != null); - Contract.Requires(argumentsResult != null); - this.Proxy = proxy; - this.ArgumentsResult = argumentsResult; - } - - // return what formal type parameters there are - public List/*!*/ FormalTypeParams { - get { - MapType realType = Proxy.ProxyFor as MapType; - if (realType == null) - // no instantiation of the map type is known, which means - // that the map type is assumed to be monomorphic - return new List(); - else - return realType.TypeParameters.ToList(); - } - } - - // given a formal type parameter, return the actual instantiation - public Type/*!*/ this[TypeVariable/*!*/ var] { - get { - // then there has to be an instantiation that is a polymorphic map type - if (Instantiations == null) { - MapType realType = Proxy.ProxyFor as MapType; - Contract.Assert(realType != null); - List/*!*/ formalArgs = new List(); - foreach (Type/*!*/ t in realType.Arguments) { - Contract.Assert(t != null); - formalArgs.Add(t); - } - formalArgs.Add(realType.Result); - Instantiations = - Type.InferTypeParameters(realType.TypeParameters, formalArgs, ArgumentsResult); - } - return Instantiations[var]; - } - } - } +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +//--------------------------------------------------------------------------------------------- +// BoogiePL - Absy.cs +//--------------------------------------------------------------------------------------------- + +namespace Microsoft.Boogie { + using System; + using System.Collections; + using System.Diagnostics; + using System.Linq; + using System.Collections.Generic; + using Microsoft.Boogie.AbstractInterpretation; + using System.Diagnostics.Contracts; + + //===================================================================== + //--------------------------------------------------------------------- + // Types + [ContractClass(typeof(TypeContracts))] + public abstract class Type : Absy { + public Type(IToken/*!*/ token) + : base(token) { + Contract.Requires(token != null); + } + + //----------- Cloning ---------------------------------- + // We implement our own clone-method, because bound type variables + // have to be created in the right way. It is /not/ ok to just clone + // everything recursively. Applying Clone to a type will return + // a type in which all bound variables have been replaced with new + // variables, whereas free variables have not changed + + public override Absy Clone() { + Contract.Ensures(Contract.Result() != null); + return this.Clone(new Dictionary()); + } + + public abstract Type/*!*/ Clone(IDictionary/*!*/ varMap); + + /// + /// Clones the type, but only syntactically. Anything resolved in the source + /// type is left unresolved (that is, with just the name) in the destination type. + /// + public abstract Type/*!*/ CloneUnresolved(); + + //----------- Linearisation ---------------------------------- + + public void Emit(TokenTextWriter stream) { + Contract.Requires(stream != null); + this.Emit(stream, 0); + } + + public abstract void Emit(TokenTextWriter/*!*/ stream, int contextBindingStrength); + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result() != null); + System.IO.StringWriter buffer = new System.IO.StringWriter(); + using (TokenTextWriter stream = new TokenTextWriter("", buffer, /*setTokens=*/false, /*pretty=*/ false)) { + this.Emit(stream); + } + return buffer.ToString(); + } + + //----------- Equality ---------------------------------- + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object that) { + if (ReferenceEquals(this, that)) + return true; + Type thatType = that as Type; + return thatType != null && this.Equals(thatType, + new List(), + new List()); + } + + [Pure] + public abstract bool Equals(Type/*!*/ that, + List/*!*/ thisBoundVariables, + List/*!*/ thatBoundVariables); + + // used to skip leading type annotations (subexpressions of the + // resulting type might still contain annotations) + internal virtual Type/*!*/ Expanded { + get { + Contract.Ensures(Contract.Result() != null); + + return this; + } + } + + //----------- Unification of types ----------- + + /// + /// Add a constraint that this==that, if possible, and return true. + /// If not possible, return false (which may have added some partial constraints). + /// No error is printed. + /// + public bool Unify(Type that) { + Contract.Requires(that != null); + return Unify(that, new List(), new Dictionary()); + } + + public abstract bool Unify(Type/*!*/ that, + List/*!*/ unifiableVariables, + // an idempotent substitution that describes the + // unification result up to a certain point + IDictionary/*!*/ unifier); + + + [Pure] + public static bool IsIdempotent(IDictionary/*!*/ unifier) { + Contract.Requires(cce.NonNullDictionaryAndValues(unifier)); + return unifier.Values.All(val => val.FreeVariables.All(var => !unifier.ContainsKey(var))); + } + + +#if OLD_UNIFICATION + // Compute a most general unification of two types. null is returned if + // no such unifier exists. The unifier is not allowed to subtitute any + // type variables other than the ones in "unifiableVariables" + public IDictionary Unify(Type! that, + List! unifiableVariables) { + Dictionary! result = new Dictionary (); + try { + this.Unify(that, unifiableVariables, + new List (), new List (), result); + } catch (UnificationFailedException) { + return null; + } + return result; + } + + // Compute an idempotent most general unifier and add the result to the argument + // unifier. The result is true iff the unification succeeded + public bool Unify(Type! that, + List! unifiableVariables, + // given mappings that need to be taken into account + // the old unifier has to be idempotent as well + IDictionary! unifier) + { + Contract.Requires(Contract.ForAll(unifier.Keys , key=> unifiableVariables.Has(key))); + Contract.Requires(IsIdempotent(unifier)); + try { + this.Unify(that, unifiableVariables, + new List (), new List (), unifier); + } catch (UnificationFailedException) { + return false; + } + return true; + } + + public abstract void Unify(Type! that, + List! unifiableVariables, + List! thisBoundVariables, + List! thatBoundVariables, + // an idempotent substitution that describes the + // unification result up to a certain point + IDictionary! result); +#endif + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + public abstract Type/*!*/ Substitute(IDictionary/*!*/ subst); + + //----------- Hashcodes ---------------------------------- + + // Hack to be able to access the hashcode of superclasses further up + // (from the subclasses of this class) + [Pure] + protected int GetBaseHashCode() { + return base.GetHashCode(); + } + + [Pure] + public override int GetHashCode() { + return this.GetHashCode(new List()); + } + + [Pure] + public abstract int GetHashCode(List/*!*/ boundVariables); + + //----------- Resolution ---------------------------------- + + public override void Resolve(ResolutionContext rc) { + //Contract.Requires(rc != null); + System.Diagnostics.Debug.Fail("Type.Resolve should never be called." + + " Use Type.ResolveType instead"); + } + + public abstract Type/*!*/ ResolveType(ResolutionContext/*!*/ rc); + + public override void Typecheck(TypecheckingContext tc) { + //Contract.Requires(tc != null); + System.Diagnostics.Debug.Fail("Type.Typecheck should never be called"); + } + + // determine the free variables in a type, in the order in which the variables occur + public abstract List/*!*/ FreeVariables { + get; + } + + // determine the free type proxies in a type, in the order in which they occur + public abstract List/*!*/ FreeProxies { + get; + } + + protected static void AppendWithoutDups(List a, List b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + foreach (A x in b) + if (!a.Contains(x)) + a.Add(x); + } + + public bool IsClosed { + get { + return FreeVariables.Count == 0; + } + } + + //----------- Getters/Issers ---------------------------------- + + // the following methods should be used instead of simple casts or the + // C# "is" operator, because they handle type synonym annotations and + // type proxies correctly + + public virtual bool IsBasic { + get { + return false; + } + } + public virtual bool IsInt { + get { + return false; + } + } + public virtual bool IsReal { + get { + return false; + } + } + public virtual bool IsFloat { + get { + return false; + } + } + public virtual bool IsBool { + get { + return false; + } + } + + public virtual bool IsVariable { + get { + return false; + } + } + public virtual TypeVariable/*!*/ AsVariable { + get { + Contract.Ensures(Contract.Result() != null); + + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.AsVariable should never be called + } + } + public virtual bool IsCtor { + get { + return false; + } + } + public virtual CtorType/*!*/ AsCtor { + get { + Contract.Ensures(Contract.Result() != null); + + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.AsCtor should never be called + } + } + public virtual bool IsMap { + get { + return false; + } + } + public virtual MapType/*!*/ AsMap { + get { + Contract.Ensures(Contract.Result() != null); + + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.AsMap should never be called + } + } + public virtual int MapArity { + get { + + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.MapArity should never be called + } + } + public virtual bool IsUnresolved { + get { + return false; + } + } + public virtual UnresolvedTypeIdentifier/*!*/ AsUnresolved { + get { + Contract.Ensures(Contract.Result() != null); + + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.AsUnresolved should never be called + } + } + + public virtual bool isFloat { + get { + return false; + } + } + public virtual int FloatExponent + { + get + { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.FloatExponent should never be called + } + } + public virtual int FloatMantissa { + get { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.FloatMantissa should never be called + } + } + public virtual bool IsBv { + get { + return false; + } + } + public virtual int BvBits { + get { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.BvBits should never be called + } + } + + public static readonly Type/*!*/ Int = new BasicType(SimpleType.Int); + public static readonly Type/*!*/ Real = new BasicType(SimpleType.Real); + public static readonly Type/*!*/ Bool = new BasicType(SimpleType.Bool); + private static BvType[] bvtypeCache; + + static public BvType GetBvType(int sz) { + Contract.Requires(0 <= sz); + Contract.Ensures(Contract.Result() != null); + + if (bvtypeCache == null) { + bvtypeCache = new BvType[128]; + } + if (sz < bvtypeCache.Length) { + BvType t = bvtypeCache[sz]; + if (t == null) { + t = new BvType(sz); + bvtypeCache[sz] = t; + } + return t; + } else { + return new BvType(sz); + } + } + + static public FloatType GetFloatType(int exp, int man) { + Contract.Requires(0 <= exp); + Contract.Requires(0 <= man); + Contract.Ensures(Contract.Result() != null); + + return new FloatType(exp, man); + } + + //------------ Match formal argument types on actual argument types + //------------ and return the resulting substitution of type variables + +#if OLD_UNIFICATION + public static IDictionary! + MatchArgumentTypes(List! typeParams, + List! formalArgs, + List! actualArgs, + List formalOuts, + List actualOuts, + string! opName, + TypecheckingContext! tc) + { + Contract.Requires(formalArgs.Length == actualArgs.Length); + Contract.Requires(formalOuts == null <==> actualOuts == null); + Contract.Requires(formalOuts != null ==> formalOuts.Length == actualOuts.Length); + List! boundVarSeq0 = new List (); + List! boundVarSeq1 = new List (); + Dictionary! subst = new Dictionary(); + + for (int i = 0; i < formalArgs.Length; ++i) { + try { + Type! actualType = cce.NonNull((!)actualArgs[i]).Type; + // if the type variables to be matched occur in the actual + // argument types, something has gone very wrong + Contract.Assert(forall{TypeVariable! var in typeParams); + !actualType.FreeVariables.Has(var)}; + formalArgs[i].Unify(actualType, + typeParams, + boundVarSeq0, boundVarSeq1, + subst); + } catch (UnificationFailedException) { + tc.Error(actualArgs[i], + "invalid type for argument {0} in {1}: {2} (expected: {3})", + i, opName, actualArgs[i].Type, + // we insert the type parameters that have already been + // chosen to get a more precise error message + formalArgs[i].Substitute(subst)); + // the bound variable sequences should be empty ... + // so that we can continue with the unification + Contract.Assert(boundVarSeq0.Length == 0 && boundVarSeq1.Length == 0); + } + } + + if (formalOuts != null) { + for (int i = 0; i < formalOuts.Length; ++i) { + try { + Type! actualType = cce.NonNull((!)actualOuts[i]).Type; + // if the type variables to be matched occur in the actual + // argument types, something has gone very wrong + Contract.Assert(forall{TypeVariable! var in typeParams); + !actualType.FreeVariables.Has(var)}; + formalOuts[i].Unify(actualType, + typeParams, + boundVarSeq0, boundVarSeq1, + subst); + } catch (UnificationFailedException) { + tc.Error(actualOuts[i], + "invalid type for result {0} in {1}: {2} (expected: {3})", + i, opName, actualOuts[i].Type, + // we insert the type parameters that have already been + // chosen to get a more precise error message + formalOuts[i].Substitute(subst)); + // the bound variable sequences should be empty ... + // so that we can continue with the unification + Contract.Assert(boundVarSeq0.Length == 0 && boundVarSeq1.Length == 0); + } + } + } + + // we only allow type parameters to be substituted + Contract.Assert(Contract.ForAll(subst.Keys , var=> typeParams.Has(var))); + + return subst; + } +#else + public static IDictionary/*!*/ + MatchArgumentTypes(List/*!*/ typeParams, + List/*!*/ formalArgs, + IList/*!*/ actualArgs, + List formalOuts, + List actualOuts, + string/*!*/ opName, + TypecheckingContext/*!*/ tc) { + Contract.Requires(typeParams != null); + Contract.Requires(formalArgs != null); + Contract.Requires(actualArgs != null); + Contract.Requires(opName != null); + Contract.Requires(tc != null); + Contract.Requires(formalArgs.Count == actualArgs.Count); + Contract.Requires((formalOuts == null) == (actualOuts == null)); + Contract.Requires(formalOuts == null || formalOuts.Count == cce.NonNull(actualOuts).Count); + Contract.Requires(tc == null || opName != null);//Redundant + Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result>())); + + // requires "actualArgs" and "actualOuts" to have been type checked + + Dictionary subst = new Dictionary(); + foreach (TypeVariable/*!*/ tv in typeParams) { + Contract.Assert(tv != null); + TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name); + subst.Add(tv, proxy); + } + + for (int i = 0; i < formalArgs.Count; i++) { + Type formal = formalArgs[i].Substitute(subst); + Type actual = cce.NonNull(cce.NonNull(actualArgs[i]).Type); + // if the type variables to be matched occur in the actual + // argument types, something has gone very wrong + Contract.Assert(Contract.ForAll(0, typeParams.Count, index => !actual.FreeVariables.Contains(typeParams[index]))); + + if (!formal.Unify(actual)) { + Contract.Assume(tc != null); // caller expected no errors + Contract.Assert(opName != null); // follows from precondition + tc.Error(cce.NonNull(actualArgs[i]), + "invalid type for argument {0} in {1}: {2} (expected: {3})", + i, opName, actual, formalArgs[i]); + } + } + + if (formalOuts != null) { + for (int i = 0; i < formalOuts.Count; ++i) { + Type formal = formalOuts[i].Substitute(subst); + Type actual = cce.NonNull(cce.NonNull(actualOuts)[i].Type); + // if the type variables to be matched occur in the actual + // argument types, something has gone very wrong + Contract.Assert(Contract.ForAll(0, typeParams.Count, var => !actual.FreeVariables.Contains(typeParams[var]))); + + if (!formal.Unify(actual)) { + Contract.Assume(tc != null); // caller expected no errors + Contract.Assert(opName != null); // follows from precondition + tc.Error(actualOuts[i], + "invalid type for out-parameter {0} in {1}: {2} (expected: {3})", + i, opName, actual, formal); + } + } + } + + return subst; + } +#endif + + //------------ Match formal argument types of a function or map + //------------ on concrete types, substitute the result into the + //------------ result type. Null is returned for type errors + + public static List CheckArgumentTypes(List/*!*/ typeParams, + out List/*!*/ actualTypeParams, + List/*!*/ formalIns, + IList/*!*/ actualIns, + List/*!*/ formalOuts, + List actualOuts, + IToken/*!*/ typeCheckingSubject, + string/*!*/ opName, + TypecheckingContext/*!*/ tc) + // requires "actualIns" and "actualOuts" to have been type checked + { + Contract.Requires(typeParams != null); + + Contract.Requires(formalIns != null); + Contract.Requires(formalOuts != null); + Contract.Requires(actualIns != null); + Contract.Requires(typeCheckingSubject != null); + Contract.Requires(opName != null);Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out actualTypeParams))); + actualTypeParams = new List(); + + if (formalIns.Count != actualIns.Count) { + tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1}", + opName, actualIns.Count); + // if there are no type parameters, we can still return the result + // type and hope that the type checking proceeds + return typeParams.Count == 0 ? formalOuts : null; + } else if (actualOuts != null && formalOuts.Count != actualOuts.Count) { + tc.Error(typeCheckingSubject, "wrong number of result variables in {0}: {1}", + opName, actualOuts.Count); + // if there are no type parameters, we can still return the result + // type and hope that the type checking proceeds + actualTypeParams = new List(); + return typeParams.Count == 0 ? formalOuts : null; + } + + int previousErrorCount = tc.ErrorCount; + IDictionary subst = + MatchArgumentTypes(typeParams, formalIns, actualIns, + actualOuts != null ? formalOuts : null, actualOuts, opName, tc); + Contract.Assert(cce.NonNullDictionaryAndValues(subst)); + foreach (TypeVariable/*!*/ var in typeParams) { + Contract.Assert(var != null); + actualTypeParams.Add(subst[var]); + } + + List/*!*/ actualResults = new List(); + foreach (Type/*!*/ t in formalOuts) { + Contract.Assert(t != null); + actualResults.Add(t.Substitute(subst)); + } + List resultFreeVars = FreeVariablesIn(actualResults); + if (previousErrorCount != tc.ErrorCount) { + // errors occured when matching the formal arguments + // in case we have been able to substitute all type parameters, + // we can still return the result type and hope that the + // type checking proceeds in a meaningful manner + if (typeParams.All(param => !resultFreeVars.Contains(param))) + return actualResults; + else + // otherwise there is no point in returning the result type, + // type checking would only get confused even further + return null; + } + + Contract.Assert(Contract.ForAll(0, typeParams.Count, index => !resultFreeVars.Contains(typeParams[index]))); + return actualResults; + } + + /////////////////////////////////////////////////////////////////////////// + + // about the same as Type.CheckArgumentTypes, but without + // detailed error reports + public static Type/*!*/ InferValueType(List/*!*/ typeParams, + List/*!*/ formalArgs, + Type/*!*/ formalResult, + List/*!*/ actualArgs) { + Contract.Requires(typeParams != null); + Contract.Requires(formalArgs != null); + Contract.Requires(formalResult != null); + Contract.Requires(actualArgs != null); + Contract.Ensures(Contract.Result() != null); + + IDictionary/*!*/ subst = + InferTypeParameters(typeParams, formalArgs, actualArgs); + Contract.Assert(cce.NonNullDictionaryAndValues(subst)); + + Type/*!*/ res = formalResult.Substitute(subst); + Contract.Assert(res != null); + // all type parameters have to be substituted with concrete types + List/*!*/ resFreeVars = res.FreeVariables; + Contract.Assert(resFreeVars != null); + Contract.Assert(Contract.ForAll(0, typeParams.Count, var => !resFreeVars.Contains(typeParams[var]))); + return res; + } + +#if OLD_UNIFICATION + public static IDictionary! + InferTypeParameters(List! typeParams, + List! formalArgs, + List! actualArgs) + { + Contract.Requires(formalArgs.Length == actualArgs.Length); + + List! boundVarSeq0 = new List (); + List! boundVarSeq1 = new List (); + Dictionary! subst = new Dictionary(); + + for (int i = 0; i < formalArgs.Length; ++i) { + try { + Contract.Assert(forall{TypeVariable! var in typeParams); + !actualArgs[i].FreeVariables.Has(var)}; + formalArgs[i].Unify(actualArgs[i], typeParams, + boundVarSeq0, boundVarSeq1, subst); + } catch (UnificationFailedException) { + System.Diagnostics.Debug.Fail("Type unification failed: " + + formalArgs[i] + " vs " + actualArgs[i]); + } + } + + // we only allow type parameters to be substituted + Contract.Assert(Contract.ForAll(subst.Keys , var=> typeParams.Has(var))); + return subst; + } +#else + /// + /// like Type.CheckArgumentTypes, but assumes no errors + /// (and only does arguments, not results; and takes actuals as List, not List) + /// + public static IDictionary/*!*/ + InferTypeParameters(List/*!*/ typeParams, + List/*!*/ formalArgs, + List/*!*/ actualArgs) { + Contract.Requires(typeParams != null); + Contract.Requires(formalArgs != null); + Contract.Requires(actualArgs != null);Contract.Requires(formalArgs.Count == actualArgs.Count); + Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result>())); + + + List proxies = new List(); + Dictionary/*!*/ subst = new Dictionary(); + foreach (TypeVariable/*!*/ tv in typeParams) { + Contract.Assert(tv != null); + TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name); + proxies.Add(proxy); + subst.Add(tv, proxy); + } + + for (int i = 0; i < formalArgs.Count; i++) { + Type formal = formalArgs[i].Substitute(subst); + Type actual = actualArgs[i]; + // if the type variables to be matched occur in the actual + // argument types, something has gone very wrong + Contract.Assert(Contract.ForAll(0, typeParams.Count, index => !actual.FreeVariables.Contains(typeParams[index]))); + + if (!formal.Unify(actual)) { + Contract.Assume(false); // caller expected no errors + } + } + + return subst; + } +#endif + + //----------- Helper methods to deal with bound type variables --------------- + + public static void EmitOptionalTypeParams(TokenTextWriter stream, List typeParams) { + Contract.Requires(typeParams != null); + Contract.Requires(stream != null); + if (typeParams.Count > 0) { + stream.Write("<"); + typeParams.Emit(stream, ","); // default binding strength of 0 is ok + stream.Write(">"); + } + } + + // Sort the type parameters according to the order of occurrence in the argument types + public static List/*!*/ SortTypeParams(List/*!*/ typeParams, List/*!*/ argumentTypes, Type resultType) { + Contract.Requires(typeParams != null); + Contract.Requires(argumentTypes != null); + Contract.Ensures(Contract.Result>() != null); + + Contract.Ensures(Contract.Result>().Count == typeParams.Count); + if (typeParams.Count == 0) { + return typeParams; + } + + List freeVarsInUse = FreeVariablesIn(argumentTypes); + if (resultType != null) { + freeVarsInUse.AppendWithoutDups(resultType.FreeVariables); + } + // "freeVarsInUse" is already sorted, but it may contain type variables not in "typeParams". + // So, project "freeVarsInUse" onto "typeParams": + List sortedTypeParams = new List(); + foreach (TypeVariable/*!*/ var in freeVarsInUse) { + Contract.Assert(var != null); + if (typeParams.Contains(var)) { + sortedTypeParams.Add(var); + } + } + + if (sortedTypeParams.Count < typeParams.Count) + // add the type parameters not mentioned in "argumentTypes" in + // the end of the list (this can happen for quantifiers) + sortedTypeParams.AppendWithoutDups(typeParams); + + return sortedTypeParams; + } + + // Check that each of the type parameters occurs in at least one argument type. + // Return true if some type parameters appear only among "moreArgumentTypes" and + // not in "argumentTypes". + [Pure] + public static bool CheckBoundVariableOccurrences(List/*!*/ typeParams, + List/*!*/ argumentTypes, + List moreArgumentTypes, + IToken/*!*/ resolutionSubject, + string/*!*/ subjectName, + ResolutionContext/*!*/ rc) { + Contract.Requires(typeParams != null); + Contract.Requires(argumentTypes != null); + Contract.Requires(resolutionSubject != null); + Contract.Requires(subjectName != null); + Contract.Requires(rc != null); + List freeVarsInArgs = FreeVariablesIn(argumentTypes); + List moFreeVarsInArgs = moreArgumentTypes == null ? null : FreeVariablesIn(moreArgumentTypes); + bool someTypeParamsAppearOnlyAmongMo = false; + foreach (TypeVariable/*!*/ var in typeParams) { + Contract.Assert(var != null); + if (rc.LookUpTypeBinder(var.Name) == var) // avoid to complain twice about variables that are bound multiple times + { + if (freeVarsInArgs.Contains(var)) { + // cool + } else if (moFreeVarsInArgs != null && moFreeVarsInArgs.Contains(var)) { + someTypeParamsAppearOnlyAmongMo = true; + } else { + rc.Error(resolutionSubject, + "type variable must occur in {0}: {1}", + subjectName, var); + } + } + } + return someTypeParamsAppearOnlyAmongMo; + } + + [Pure] + public static List FreeVariablesIn(List arguments) { + Contract.Requires(arguments != null); + Contract.Ensures(Contract.Result>() != null); + List/*!*/ res = new List(); + foreach (Type/*!*/ t in arguments) { + Contract.Assert(t != null); + res.AppendWithoutDups(t.FreeVariables); + } + return res; + } + } + [ContractClassFor(typeof(Type))] + public abstract class TypeContracts : Type { + public TypeContracts() :base(null){ + + } + public override List FreeProxies { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + throw new NotImplementedException(); + } + } + public override List FreeVariables { + get { + Contract.Ensures(Contract.Result>() != null); + throw new NotImplementedException(); + } + } + public override Type Clone(IDictionary varMap) { + Contract.Requires(cce.NonNullDictionaryAndValues(varMap)); + Contract.Ensures(Contract.Result() != null); + + throw new NotImplementedException(); + } + public override Type CloneUnresolved() { + Contract.Ensures(Contract.Result() != null); + + throw new NotImplementedException(); + } + public override void Emit(TokenTextWriter stream, int contextBindingStrength) { + Contract.Requires(stream != null); + throw new NotImplementedException(); + } + public override bool Equals(Type that, List thisBoundVariables, List thatBoundVariables) { + Contract.Requires(that != null); + Contract.Requires(thisBoundVariables != null); + Contract.Requires(thatBoundVariables != null); + throw new NotImplementedException(); + } + public override bool Unify(Type that, List unifiableVariables, IDictionary unifier) { + Contract.Requires(that != null); + Contract.Requires(unifiableVariables != null); + Contract.Requires(cce.NonNullDictionaryAndValues(unifier)); + Contract.Requires(Contract.ForAll(unifier.Keys, key => unifiableVariables.Contains(key))); + Contract.Requires(IsIdempotent(unifier)); + throw new NotImplementedException(); + } + public override Type Substitute(IDictionary subst) { + Contract.Requires(cce.NonNullDictionaryAndValues(subst)); + Contract.Ensures(Contract.Result() != null); + + throw new NotImplementedException(); + } + public override Type ResolveType(ResolutionContext rc) { + Contract.Requires(rc != null); + Contract.Ensures(Contract.Result() != null); + + throw new NotImplementedException(); + } + public override int GetHashCode(List boundVariables) { + Contract.Requires(boundVariables != null); + throw new NotImplementedException(); + } + } + //===================================================================== + + public class BasicType : Type { + public readonly SimpleType T; + public BasicType(IToken/*!*/ token, SimpleType t) + : base(token) { + Contract.Requires(token != null); + T = t; + } + public BasicType(SimpleType t) + : base(Token.NoToken) { + T = t; + } + + //----------- Cloning ---------------------------------- + // We implement our own clone-method, because bound type variables + // have to be created in the right way. It is /not/ ok to just clone + // everything recursively. + + public override Type Clone(IDictionary/*!*/ varMap) { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result() != null); + // BasicTypes are immutable anyway, we do not clone + return this; + } + + public override Type CloneUnresolved() { + Contract.Ensures(Contract.Result() != null); + return this; + } + + //----------- Linearisation ---------------------------------- + + public override void Emit(TokenTextWriter stream, int contextBindingStrength) { + //Contract.Requires(stream != null); + // no parentheses are necessary for basic types + stream.SetToken(this); + stream.Write("{0}", this); + } + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result() != null); + switch (T) { + case SimpleType.Int: + return "int"; + case SimpleType.Real: + return "real"; + case SimpleType.Bool: + return "bool"; + } + Debug.Assert(false, "bad type " + T); + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // make compiler happy + } + + //----------- Equality ---------------------------------- + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object that) { + // shortcut + Type thatType = that as Type; + if (thatType == null) + return false; + BasicType thatBasicType = TypeProxy.FollowProxy(thatType.Expanded) as BasicType; + return thatBasicType != null && this.T == thatBasicType.T; + } + + [Pure] + public override bool Equals(Type that, List thisBoundVariables, List thatBoundVariables) { + //Contract.Requires(thatBoundVariables != null); + //Contract.Requires(thisBoundVariables != null); + //Contract.Requires(that != null); + return this.Equals(that); + } + + //----------- Unification of types ----------- + + public override bool Unify(Type that, List unifiableVariables, IDictionary/*!*/ unifier) { + //Contract.Requires(unifiableVariables != null); + //Contract.Requires(that != null); + //Contract.Requires(cce.NonNullElements(unifier)); + // an idempotent substitution that describes the + // unification result up to a certain point + + that = that.Expanded; + if (that is TypeProxy || that is TypeVariable) { + return that.Unify(this, unifiableVariables, unifier); + } else { + return this.Equals(that); + } + } + +#if OLD_UNIFICATION + public override void Unify(Type! that, + List! unifiableVariables, + List! thisBoundVariables, + List! thatBoundVariables, + IDictionary! result) { + that = that.Expanded; + if (that is TypeVariable) { + that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result); + } else { + if (!this.Equals(that)) + throw UNIFICATION_FAILED; + } + } +#endif + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + public override Type Substitute(IDictionary/*!*/ subst) { + //Contract.Requires(cce.NonNullElements(subst)); + Contract.Ensures(Contract.Result() != null); + return this; + } + + //----------- Hashcodes ---------------------------------- + + [Pure] + public override int GetHashCode(List boundVariables) { + //Contract.Requires(boundVariables != null); + return this.T.GetHashCode(); + } + + //----------- Resolution ---------------------------------- + + public override Type ResolveType(ResolutionContext rc) { + //Contract.Requires(rc != null); + Contract.Ensures(Contract.Result() != null); + // nothing to resolve + return this; + } + + // determine the free variables in a type, in the order in which the variables occur + public override List/*!*/ FreeVariables { + get { + Contract.Ensures(Contract.Result>() != null); + + return new List(); // basic type are closed + } + } + + public override List/*!*/ FreeProxies { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return new List(); + } + } + + //----------- Getters/Issers ---------------------------------- + + public override bool IsBasic { + get { + return true; + } + } + public override bool IsInt { + get { + return this.T == SimpleType.Int; + } + } + public override bool IsReal { + get { + return this.T == SimpleType.Real; + } + } + public override bool IsBool { + get { + return this.T == SimpleType.Bool; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitBasicType(this); + } + } + + //===================================================================== + + //Note that the functions in this class were directly copied from the BV class just below + public class FloatType : Type { + public readonly int Mantissa; //Size of mantissa in bits + public readonly int Exponent; //Size of exponent in bits + + public FloatType(IToken token, int exponent, int mantissa) + : base(token) { + Contract.Requires(token != null); + Exponent = exponent; + Mantissa = mantissa; + } + + public FloatType(int exponent, int mantissa) + : base(Token.NoToken) { + Exponent = exponent; + Mantissa = mantissa; + } + + //----------- Cloning ---------------------------------- + // We implement our own clone-method, because bound type variables + // have to be created in the right way. It is /not/ ok to just clone + // everything recursively. + + public override Type Clone(IDictionary/*!*/ varMap) + { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result() != null); + // FloatTypes are immutable anyway, we do not clone + return this; + } + + public override Type CloneUnresolved() + { + Contract.Ensures(Contract.Result() != null); + return this; + } + + //----------- Linearisation ---------------------------------- + + public override void Emit(TokenTextWriter stream, int contextBindingStrength) + { + //Contract.Requires(stream != null); + // no parentheses are necessary for bitvector-types + stream.SetToken(this); + stream.Write("{0}", this); + } + + public override string ToString() + { + Contract.Ensures(Contract.Result() != null); + return "float (" + Exponent + " " + Mantissa + ")"; + } + + //----------- Equality ---------------------------------- + + [Pure] + public override bool Equals(Type/*!*/ that, + List/*!*/ thisBoundVariables, + List/*!*/ thatBoundVariables) + { + FloatType thatFloatType = TypeProxy.FollowProxy(that.Expanded) as FloatType; + return thatFloatType != null && this.Mantissa == thatFloatType.Mantissa && this.Exponent == thatFloatType.Exponent; + } + + //----------- Unification of types ----------- + + public override bool Unify(Type/*!*/ that, + List/*!*/ unifiableVariables, + // an idempotent substitution that describes the + // unification result up to a certain point + IDictionary/*!*/ unifier) + { + //Contract.Requires(that != null); + //Contract.Requires(unifiableVariables != null); + //Contract.Requires(cce.NonNullElements(unifier)); + that = that.Expanded; + if (that is TypeProxy || that is TypeVariable) { + return that.Unify(this, unifiableVariables, unifier); + } + else { + return this.Equals(that); + } + } + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + public override Type Substitute(IDictionary/*!*/ subst) + { + Contract.Ensures(Contract.Result() != null); + return this; + } + + //----------- Hashcodes ---------------------------------- + + [Pure] + public override int GetHashCode(List boundVariables) + { + return this.Mantissa.GetHashCode() + this.Exponent.GetHashCode(); + } + + //----------- Resolution ---------------------------------- + + public override Type ResolveType(ResolutionContext rc) + { + //Contract.Requires(rc != null); + Contract.Ensures(Contract.Result() != null); + // nothing to resolve + return this; + } + + // determine the free variables in a type, in the order in which the variables occur + public override List/*!*/ FreeVariables + { + get + { + Contract.Ensures(Contract.Result>() != null); + + return new List(); // bitvector-type are closed + } + } + + public override List/*!*/ FreeProxies + { + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return new List(); + } + } + + //----------- Getters/Issers ---------------------------------- + + public override bool IsFloat { + get { + return true; + } + } + public override int FloatMantissa { + get { + return Mantissa; + } + } + public override int FloatExponent { + get { + return Exponent; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) + { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitFloatType(this); + } + + } + + //===================================================================== + + public class BvType : Type { + public readonly int Bits; + + public BvType(IToken token, int bits) + : base(token) { + Contract.Requires(token != null); + Bits = bits; + } + + public BvType(int bits) + : base(Token.NoToken) { + Bits = bits; + } + + //----------- Cloning ---------------------------------- + // We implement our own clone-method, because bound type variables + // have to be created in the right way. It is /not/ ok to just clone + // everything recursively. + + public override Type Clone(IDictionary/*!*/ varMap) { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result() != null); + // BvTypes are immutable anyway, we do not clone + return this; + } + + public override Type CloneUnresolved() { + Contract.Ensures(Contract.Result() != null); + return this; + } + + //----------- Linearisation ---------------------------------- + + public override void Emit(TokenTextWriter stream, int contextBindingStrength) { + //Contract.Requires(stream != null); + // no parentheses are necessary for bitvector-types + stream.SetToken(this); + stream.Write("{0}", this); + } + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result() != null); + return "bv" + Bits; + } + + //----------- Equality ---------------------------------- + + [Pure] + public override bool Equals(Type/*!*/ that, + List/*!*/ thisBoundVariables, + List/*!*/ thatBoundVariables) { + //Contract.Requires(thisBoundVariables != null); + //Contract.Requires(thatBoundVariables != null); + //Contract.Requires(that != null); + BvType thatBvType = TypeProxy.FollowProxy(that.Expanded) as BvType; + return thatBvType != null && this.Bits == thatBvType.Bits; + } + + //----------- Unification of types ----------- + + public override bool Unify(Type/*!*/ that, + List/*!*/ unifiableVariables, + // an idempotent substitution that describes the + // unification result up to a certain point + IDictionary/*!*/ unifier) { + //Contract.Requires(that != null); + //Contract.Requires(unifiableVariables != null); + //Contract.Requires(cce.NonNullElements(unifier)); + that = that.Expanded; + if (that is TypeProxy || that is TypeVariable) { + return that.Unify(this, unifiableVariables, unifier); + } else { + return this.Equals(that); + } + } + +#if OLD_UNIFICATION + public override void Unify(Type that, + List! unifiableVariables, + List! thisBoundVariables, + List! thatBoundVariables, + IDictionary result){ +Contract.Requires(result != null); +Contract.Requires(that != null); + that = that.Expanded; + if (that is TypeVariable) { + that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result); + } else { + if (!this.Equals(that)) + throw UNIFICATION_FAILED; + } + } +#endif + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + public override Type Substitute(IDictionary/*!*/ subst) { + //Contract.Requires(cce.NonNullElements(subst)); + Contract.Ensures(Contract.Result() != null); + return this; + } + + //----------- Hashcodes ---------------------------------- + + [Pure] + public override int GetHashCode(List boundVariables) { + //Contract.Requires(boundVariables != null); + return this.Bits.GetHashCode(); + } + + //----------- Resolution ---------------------------------- + + public override Type ResolveType(ResolutionContext rc) { + //Contract.Requires(rc != null); + Contract.Ensures(Contract.Result() != null); + // nothing to resolve + return this; + } + + // determine the free variables in a type, in the order in which the variables occur + public override List/*!*/ FreeVariables { + get { + Contract.Ensures(Contract.Result>() != null); + + return new List(); // bitvector-type are closed + } + } + + public override List/*!*/ FreeProxies { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return new List(); + } + } + + //----------- Getters/Issers ---------------------------------- + + public override bool IsBv { + get { + return true; + } + } + public override int BvBits { + get { + return Bits; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitBvType(this); + } + } + + //===================================================================== + + // An AST node containing an identifier and a sequence of type arguments, which + // will be turned either into a TypeVariable, into a CtorType or into a BvType + // during the resolution phase + public class UnresolvedTypeIdentifier : Type { + public readonly string/*!*/ Name; + public readonly List/*!*/ Arguments; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Name != null); + Contract.Invariant(Arguments != null); + } + + + public UnresolvedTypeIdentifier(IToken token, string name) + : this(token, name, new List()) { + Contract.Requires(name != null); + Contract.Requires(token != null); + } + + public UnresolvedTypeIdentifier(IToken token, string name, List arguments) + : base(token) { + Contract.Requires(arguments != null); + Contract.Requires(name != null); + Contract.Requires(token != null); + this.Name = name; + this.Arguments = arguments; + } + + //----------- Cloning ---------------------------------- + // We implement our own clone-method, because bound type variables + // have to be created in the right way. It is /not/ ok to just clone + // everything recursively + + public override Type Clone(IDictionary/*!*/ varMap) { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result() != null); + List/*!*/ newArgs = new List(); + foreach (Type/*!*/ t in Arguments) { + Contract.Assert(t != null); + newArgs.Add(t.Clone(varMap)); + } + return new UnresolvedTypeIdentifier(tok, Name, newArgs); + } + + public override Type CloneUnresolved() { + Contract.Ensures(Contract.Result() != null); + List/*!*/ newArgs = new List(); + foreach (Type/*!*/ t in Arguments) { + Contract.Assert(t != null); + newArgs.Add(t.CloneUnresolved()); + } + return new UnresolvedTypeIdentifier(tok, Name, newArgs); + } + + //----------- Equality ---------------------------------- + + [Pure] + public override bool Equals(Type that, + List/*!*/ thisBoundVariables, + List/*!*/ thatBoundVariables) { + //Contract.Requires(thisBoundVariables != null); + //Contract.Requires(thatBoundVariables != null); + //Contract.Requires(that != null); + System.Diagnostics.Debug.Fail("UnresolvedTypeIdentifier.Equals should never be called"); + return false; // to make the compiler happy + } + + //----------- Unification of types ----------- + + public override bool Unify(Type that, + List/*!*/ unifiableVariables, + IDictionary result) { + //Contract.Requires(unifiableVariables != null); + //Contract.Requires(cce.NonNullElements(result)); + //Contract.Requires(that != null); + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // UnresolvedTypeIdentifier.Unify should never be called + } + +#if OLD_UNIFICATION + public override void Unify(Type that, + List! unifiableVariables, + List! thisBoundVariables, + List! thatBoundVariables, + IDictionary result){ +Contract.Requires(result != null); +Contract.Requires(that != null); + System.Diagnostics.Debug.Fail("UnresolvedTypeIdentifier.Unify should never be called"); + } +#endif + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + public override Type Substitute(IDictionary/*!*/ subst) { + //Contract.Requires(cce.NonNullElements(subst)); + Contract.Ensures(Contract.Result() != null); + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // UnresolvedTypeIdentifier.Substitute should never be called + } + + //----------- Hashcodes ---------------------------------- + + [Pure] + public override int GetHashCode(List boundVariables) { + //Contract.Requires(boundVariables != null); + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // UnresolvedTypeIdentifier.GetHashCode should never be called + } + + //----------- Resolution ---------------------------------- + + public override Type ResolveType(ResolutionContext rc) { + //Contract.Requires(rc != null); + Contract.Ensures(Contract.Result() != null); + // first case: the type name denotes a bitvector-type + if (Name.StartsWith("bv") && Name.Length > 2) { + bool is_bv = true; + for (int i = 2; i < Name.Length; ++i) { + if (!char.IsDigit(Name[i])) { + is_bv = false; + break; + } + } + if (is_bv) { + if (Arguments.Count > 0) { + rc.Error(this, + "bitvector types must not be applied to arguments: {0}", + Name); + } + return new BvType(tok, int.Parse(Name.Substring(2))); + } + } + + // second case: the identifier is resolved to a type variable + TypeVariable var = rc.LookUpTypeBinder(Name); + if (var != null) { + if (Arguments.Count > 0) { + rc.Error(this, + "type variables must not be applied to arguments: {0}", + var); + } + return var; + } + + // third case: the identifier denotes a type constructor and we + // recursively resolve the arguments + TypeCtorDecl ctorDecl = rc.LookUpType(Name); + if (ctorDecl != null) { + if (Arguments.Count != ctorDecl.Arity) { + rc.Error(this, + "type constructor received wrong number of arguments: {0}", + ctorDecl); + return this; + } + return new CtorType(tok, ctorDecl, ResolveArguments(rc)); + } + + // fourth case: the identifier denotes a type synonym + TypeSynonymDecl synDecl = rc.LookUpTypeSynonym(Name); + if (synDecl != null) { + if (Arguments.Count != synDecl.TypeParameters.Count) { + rc.Error(this, + "type synonym received wrong number of arguments: {0}", + synDecl); + return this; + } + List/*!*/ resolvedArgs = ResolveArguments(rc); + Contract.Assert(resolvedArgs != null); + + return new TypeSynonymAnnotation(this.tok, synDecl, resolvedArgs); + + } + + // otherwise: this name is not declared anywhere + rc.Error(this, "undeclared type: {0}", Name); + return this; + } + + private List ResolveArguments(ResolutionContext rc) { + Contract.Requires(rc != null); + Contract.Ensures(Contract.Result>() != null); + List/*!*/ resolvedArgs = new List(); + foreach (Type/*!*/ t in Arguments) { + Contract.Assert(t != null); + resolvedArgs.Add(t.ResolveType(rc)); + } + return resolvedArgs; + } + + public override List/*!*/ FreeVariables { + get { + Contract.Ensures(Contract.Result>() != null); + + return new List(); + } + } + + public override List/*!*/ FreeProxies { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return new List(); + } + } + + //----------- Linearisation ---------------------------------- + + public override void Emit(TokenTextWriter stream, int contextBindingStrength) { + //Contract.Requires(stream != null); + stream.SetToken(this); + // PR: should unresolved types be syntactically distinguished from resolved types? + CtorType.EmitCtorType(this.Name, Arguments, stream, contextBindingStrength); + } + + //----------- Getters/Issers ---------------------------------- + + public override bool IsUnresolved { + get { + return true; + } + } + public override UnresolvedTypeIdentifier/*!*/ AsUnresolved { + get { + Contract.Ensures(Contract.Result() != null); + return this; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitUnresolvedTypeIdentifier(this); + } + } + + //===================================================================== + + public class TypeVariable : Type { + public readonly string/*!*/ Name; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Name != null); + } + + + public TypeVariable(IToken token, string name) + : base(token) { + Contract.Requires(name != null); + Contract.Requires(token != null); + this.Name = name; + } + + //----------- Cloning ---------------------------------- + // We implement our own clone-method, because bound type variables + // have to be created in the right way. It is /not/ ok to just clone + // everything recursively + + public override Type Clone(IDictionary/*!*/ varMap) { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result() != null); + // if this variable is mapped to some new variable, we take the new one + // otherwise, return this + TypeVariable res; + varMap.TryGetValue(this, out res); + if (res == null) + return this; + else + return res; + } + + public override Type CloneUnresolved() { + Contract.Ensures(Contract.Result() != null); + return this; + } + + //----------- Equality ---------------------------------- + + [Pure] + public override bool Equals(Type that, + List/*!*/ thisBoundVariables, + List/*!*/ thatBoundVariables) { + //Contract.Requires(thisBoundVariables != null); + //Contract.Requires(thatBoundVariables != null); + //Contract.Requires(that != null); + TypeVariable thatAsTypeVar = TypeProxy.FollowProxy(that.Expanded) as TypeVariable; + + if (thatAsTypeVar == null) + return false; + + int thisIndex = thisBoundVariables.LastIndexOf(this); + int thatIndex = thatBoundVariables.LastIndexOf(thatAsTypeVar); + return (thisIndex >= 0 && thisIndex == thatIndex) || + (thisIndex == -1 && thatIndex == -1 && + Object.ReferenceEquals(this, thatAsTypeVar)); + } + + //----------- Unification of types ----------- + + public override bool Unify(Type/*!*/ that, + List/*!*/ unifiableVariables, + // an idempotent substitution that describes the + // unification result up to a certain point + IDictionary/*!*/ unifier) { + //Contract.Requires(that != null); + //Contract.Requires(unifiableVariables != null); + //Contract.Requires(cce.NonNullElements(unifier)); + that = that.Expanded; + if (that is TypeProxy && !(that is ConstrainedProxy)) + return that.Unify(this, unifiableVariables, unifier); + + if (this.Equals(that)) + return true; + + if (unifiableVariables.Contains(this)) { + Type previousSubst; + unifier.TryGetValue(this, out previousSubst); + if (previousSubst == null) { + return addSubstitution(unifier, that); + } else { + // we have to unify the old instantiation with the new one + return previousSubst.Unify(that, unifiableVariables, unifier); + } + } + + // this cannot be instantiated with anything + // but that possibly can ... + + TypeVariable tv = that as TypeVariable; + + return tv != null && + unifiableVariables.Contains(tv) && + that.Unify(this, unifiableVariables, unifier); + } + + // TODO: the following might cause problems, because when applying substitutions + // to type proxies the substitutions are not propagated to the proxy + // constraints (right now at least) + private bool addSubstitution(IDictionary/*!*/ oldSolution, + // the type that "this" is instantiated with + Type/*!*/ newSubst) { + Contract.Requires(cce.NonNullDictionaryAndValues(oldSolution)); + Contract.Requires(newSubst != null); + Contract.Requires(!oldSolution.ContainsKey(this)); + + Dictionary/*!*/ newMapping = new Dictionary(); + // apply the old (idempotent) substitution to the new instantiation + Type/*!*/ substSubst = newSubst.Substitute(oldSolution); + Contract.Assert(substSubst != null); + // occurs check + if (substSubst.FreeVariables.Contains(this)) + return false; + newMapping.Add(this, substSubst); + + // apply the new substitution to the old ones to ensure idempotence + List/*!*/ keys = new List(); + keys.AddRange(oldSolution.Keys); + foreach (TypeVariable/*!*/ var in keys) { + Contract.Assert(var != null); + oldSolution[var] = oldSolution[var].Substitute(newMapping); + } + oldSolution.Add(this, substSubst); + + Contract.Assert(IsIdempotent(oldSolution)); + return true; + } + +#if OLD_UNIFICATION + public override void Unify(Type that, + List! unifiableVariables, + List! thisBoundVariables, + List! thatBoundVariables, + IDictionary result){ +Contract.Requires(result != null); +Contract.Requires(that != null); + that = that.Expanded; + int thisIndex = thisBoundVariables.LastIndexOf(this); + if (thisIndex == -1) { + // this is not a bound variable and can possibly be matched on that + // that must not contain any bound variables + List! thatFreeVars = that.FreeVariables; + if (thatBoundVariables.Any(var=> thatFreeVars.Has(var))) + throw UNIFICATION_FAILED; + + // otherwise, in case that is a typevariable it cannot be bound and + // we can just check for equality + if (this.Equals(that)) + return; + + if (!unifiableVariables.Has(this)) { + // this cannot be instantiated with anything + // but that possibly can ... + if ((that is TypeVariable) && + unifiableVariables.Has(that as TypeVariable)) { + that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result); + return; + } else { + throw UNIFICATION_FAILED; + } + } + + Type previousSubst; + result.TryGetValue(this, out previousSubst); + if (previousSubst == null) { + addSubstitution(result, that); + } else { + // we have to unify the old instantiation with the new one + previousSubst.Unify(that, unifiableVariables, thisBoundVariables, thatBoundVariables, result); + } + } else { + // this is a bound variable, that also has to be one (with the same index) + if (!(that is TypeVariable) || + thatBoundVariables.LastIndexOf(that) != thisIndex) + throw UNIFICATION_FAILED; + } + } + +#endif + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + public override Type Substitute(IDictionary/*!*/ subst) { + //Contract.Requires(cce.NonNullElements(subst)); + Contract.Ensures(Contract.Result() != null); + Type res; + if (subst.TryGetValue(this, out res)) { + Contract.Assert(res != null); + return res; + } else { + return this; + } + } + + //----------- Hashcodes ---------------------------------- + + [Pure] + public override int GetHashCode(List boundVariables) { + //Contract.Requires(boundVariables != null); + int thisIndex = boundVariables.LastIndexOf(this); + if (thisIndex == -1) + return GetBaseHashCode(); + return thisIndex * 27473671; + } + + //----------- Linearisation ---------------------------------- + + public override void Emit(TokenTextWriter stream, int contextBindingStrength) { + //Contract.Requires(stream != null); + // never put parentheses around variables + stream.SetToken(this); + stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(this.Name)); + } + + //----------- Resolution ---------------------------------- + + public override Type ResolveType(ResolutionContext rc) { + //Contract.Requires(rc != null); + //Contract.Ensures(Contract.Result() != null); + // nothing to resolve + return this; + } + + public override List/*!*/ FreeVariables { + get { + Contract.Ensures(Contract.Result>() != null); + return new List { this }; + } + } + + public override List/*!*/ FreeProxies { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return new List(); + } + } + + //----------- Getters/Issers ---------------------------------- + + public override bool IsVariable { + get { + return true; + } + } + public override TypeVariable/*!*/ AsVariable { + get { + Contract.Ensures(Contract.Result() != null); + return this; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + //Contract.Ensures(Contract.Result() != null); + return visitor.VisitTypeVariable(this); + } + } + + //===================================================================== + + public class TypeProxy : Type { + static int proxies = 0; + protected readonly string/*!*/ Name; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Name != null); + } + + + public TypeProxy(IToken token, string givenName) + : this(token, givenName, "proxy") { + Contract.Requires(givenName != null); + Contract.Requires(token != null); + } + + protected TypeProxy(IToken token, string givenName, string kind) + : base(token) { + Contract.Requires(kind != null); + Contract.Requires(givenName != null); + Contract.Requires(token != null); + Name = givenName + "$" + kind + "#" + proxies; + proxies++; + } + + private Type proxyFor; + public Type ProxyFor { + // apply path shortening, and then return the value of proxyFor + get { + TypeProxy anotherProxy = proxyFor as TypeProxy; + if (anotherProxy != null && anotherProxy.proxyFor != null) { + // apply path shortening by bypassing "anotherProxy" (and possibly others) + proxyFor = anotherProxy.ProxyFor; + Contract.Assert(proxyFor != null); + } + return proxyFor; + } + } + + [Pure] + [Reads(ReadsAttribute.Reads.Everything)] + public static Type FollowProxy(Type t) { + Contract.Requires(t != null); + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(!(Contract.Result() is TypeProxy) || ((TypeProxy)Contract.Result()).proxyFor == null); + if (t is TypeProxy) { + Type p = ((TypeProxy)t).ProxyFor; + if (p != null) { + return p; + } + } + return t; + } + + protected void DefineProxy(Type ty) { + Contract.Requires(ty != null); + Contract.Requires(ProxyFor == null); + // follow ty down to the leaf level, so that we can avoid creating a cycle + ty = FollowProxy(ty); + if (!object.ReferenceEquals(this, ty)) { + proxyFor = ty; + } + } + + //----------- Cloning ---------------------------------- + + public override Type Clone(IDictionary/*!*/ varMap) { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result() != null); + Type p = ProxyFor; + if (p != null) { + return p.Clone(varMap); + } else { + return new TypeProxy(this.tok, this.Name); // the clone will have a name that ends with $proxy$proxy + } + } + + public override Type CloneUnresolved() { + Contract.Ensures(Contract.Result() != null); + return new TypeProxy(this.tok, this.Name); // the clone will have a name that ends with $proxy$proxy + } + + //----------- Equality ---------------------------------- + + [Pure] + public override bool Equals(Type that, + List/*!*/ thisBoundVariables, + List/*!*/ thatBoundVariables) { + //Contract.Requires(thisBoundVariables != null); + //Contract.Requires(thatBoundVariables != null); + //Contract.Requires(that != null); + if (object.ReferenceEquals(this, that)) { + return true; + } + Type p = ProxyFor; + if (p != null) { + return p.Equals(that, thisBoundVariables, thatBoundVariables); + } else { + // This proxy could be made to be equal to anything, so what to return? + return false; + } + } + + //----------- Unification of types ----------- + + // determine whether the occurs check fails: this is a strict subtype of that + protected bool ReallyOccursIn(Type that) { + Contract.Requires(that != null); + that = FollowProxy(that.Expanded); + return that.FreeProxies.Contains(this) && + (that.IsCtor || that.IsMap && this != that && this.ProxyFor != that); + } + + public override bool Unify(Type that, + List/*!*/ unifiableVariables, + IDictionary result) { + //Contract.Requires(cce.NonNullElements(result)); + //Contract.Requires(unifiableVariables != null); + //Contract.Requires(that != null); + Type p = ProxyFor; + if (p != null) { + return p.Unify(that, unifiableVariables, result); + } else { + // unify this with that + if (this.ReallyOccursIn(that)) + return false; + DefineProxy(that.Expanded); + return true; + } + } + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + public override Type Substitute(IDictionary/*!*/ subst) { + //Contract.Requires(cce.NonNullElements(subst)); + Contract.Ensures(Contract.Result() != null); + Type p = ProxyFor; + if (p != null) { + return p.Substitute(subst); + } else { + return this; + } + } + + //----------- Hashcodes ---------------------------------- + + [Pure] + public override int GetHashCode(List boundVariables) { + //Contract.Requires(boundVariables != null); + Type p = ProxyFor; + if (p != null) { + return p.GetHashCode(boundVariables); + } else { + return GetBaseHashCode(); + } + } + + //----------- Linearisation ---------------------------------- + + public override void Emit(TokenTextWriter stream, int contextBindingStrength) { + //Contract.Requires(stream != null); + Type p = ProxyFor; + if (p != null) { + p.Emit(stream, contextBindingStrength); + } else { + // no need for parentheses + stream.SetToken(this); + stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(this.Name)); + } + } + + //----------- Resolution ---------------------------------- + + public override Type ResolveType(ResolutionContext rc) { + //Contract.Requires(rc != null); + Contract.Ensures(Contract.Result() != null); + Type p = ProxyFor; + if (p != null) { + return p.ResolveType(rc); + } else { + return this; + } + } + + public override List/*!*/ FreeVariables { + get { + Contract.Ensures(Contract.Result>() != null); + + Type p = ProxyFor; + if (p != null) { + return p.FreeVariables; + } else { + return new List(); + } + } + } + + public override List/*!*/ FreeProxies { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Type p = ProxyFor; + if (p != null) { + return p.FreeProxies; + } else { + List/*!*/ res = new List(); + res.Add(this); + return res; + } + } + } + + //----------- Getters/Issers ---------------------------------- + + public override bool IsBasic { + get { + Type p = ProxyFor; + return p != null && p.IsBasic; + } + } + public override bool IsInt { + get { + Type p = ProxyFor; + return p != null && p.IsInt; + } + } + public override bool IsReal { + get { + Type p = ProxyFor; + return p != null && p.IsReal; + } + } + public override bool IsFloat { + get { + Type p = ProxyFor; + return p != null && p.IsFloat; + } + } + public override bool IsBool { + get { + Type p = ProxyFor; + return p != null && p.IsBool; + } + } + + public override bool IsVariable { + get { + Type p = ProxyFor; + return p != null && p.IsVariable; + } + } + public override TypeVariable/*!*/ AsVariable { + get { + Contract.Ensures(Contract.Result() != null); + + Type p = ProxyFor; + Contract.Assume(p != null); + return p.AsVariable; + } + } + + public override bool IsCtor { + get { + Type p = ProxyFor; + return p != null && p.IsCtor; + } + } + public override CtorType/*!*/ AsCtor { + get { + Contract.Ensures(Contract.Result() != null); + + Type p = ProxyFor; + Contract.Assume(p != null); + return p.AsCtor; + } + } + public override bool IsMap { + get { + Type p = ProxyFor; + return p != null && p.IsMap; + } + } + public override MapType/*!*/ AsMap { + get { + Contract.Ensures(Contract.Result() != null); + + Type p = ProxyFor; + Contract.Assume(p != null); + return p.AsMap; + } + } + public override int MapArity { + get { + Type p = ProxyFor; + Contract.Assume(p != null); + return p.MapArity; + } + } + public override bool IsUnresolved { + get { + Type p = ProxyFor; + return p != null && p.IsUnresolved; + } + } + public override UnresolvedTypeIdentifier/*!*/ AsUnresolved { + get { + Contract.Ensures(Contract.Result() != null); + + Type p = ProxyFor; + Contract.Assume(p != null); + return p.AsUnresolved; + } + } + + public override bool IsBv { + get { + Type p = ProxyFor; + return p != null && p.IsBv; + } + } + public override int BvBits { + get { + Type p = ProxyFor; + Contract.Assume(p != null); + return p.BvBits; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitTypeProxy(this); + } + } + + public abstract class ConstrainedProxy : TypeProxy { + protected ConstrainedProxy(IToken token, string givenName, string kind) + : base(token, givenName, kind) { + Contract.Requires(kind != null); + Contract.Requires(givenName != null); + Contract.Requires(token != null); + } + } + + /// + /// Each instance of this class represents a set of bitvector types. In particular, it represents + /// a bitvector type bvN iff + /// minBits ATMOST N and + /// foreach constraint (t0,t1), the types represented by t0 and t1 are bitvector types whose + /// number of bits add up to N. + /// This means that the size of a BvTypeProxy p is constrained not only by p.minBits, but also + /// by the size of various t0 and t1 types that are transitively part of BvTypeProxy constraints. + /// If such a t0 or t1 were to get its ProxyFor field defined, then p would have to be further + /// constrained too. This doesn't seem like it would ever occur in a Boogie 2 program, because: + /// the only place where a BvTypeProxy with constraints can occur is as the type of a + /// BvConcatExpr, and + /// the types of all local variables are explicitly declared, which means that the types of + /// subexpressions of a BvConcatExpr are not going to change other than via the type of the + /// BvConcatExpr. + /// So, this implementation of BvTypeProxy does not keep track of where a BvTypeProxy may occur + /// transitively in some other BvTypeProxy's constraints. + /// + public class BvTypeProxy : ConstrainedProxy { + public int MinBits; + List constraints; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(constraints, true)); + } + + class BvTypeConstraint { + public Type/*!*/ T0; + public Type/*!*/ T1; + public BvTypeConstraint(Type t0, Type t1) { + Contract.Requires(t1 != null); + Contract.Requires(t0 != null); + Contract.Requires(t0.IsBv && t1.IsBv); + T0 = t0; + T1 = t1; + } + } + + public BvTypeProxy(IToken token, string name, int minBits) + : base(token, name, "bv" + minBits + "proxy") { + Contract.Requires(name != null); + Contract.Requires(token != null); + this.MinBits = minBits; + } + + /// + /// Requires that any further constraints to be placed on t0 and t1 go via the object to + /// be constructed. + /// + public BvTypeProxy(IToken token, string name, Type t0, Type t1) + : base(token, name, "bvproxy") { + Contract.Requires(t1 != null); + Contract.Requires(t0 != null); + Contract.Requires(name != null); + Contract.Requires(token != null); + Contract.Requires(t0.IsBv && t1.IsBv); + t0 = FollowProxy(t0); + t1 = FollowProxy(t1); + this.MinBits = MinBitsFor(t0) + MinBitsFor(t1); + List list = new List(); + list.Add(new BvTypeConstraint(t0, t1)); + this.constraints = list; + } + + /// + /// Construct a BvTypeProxy like p, but with minBits. + /// + private BvTypeProxy(BvTypeProxy p, int minBits) + : base(p.tok, p.Name, "") { + Contract.Requires(p != null); + this.MinBits = minBits; + this.constraints = p.constraints; + } + + private BvTypeProxy(IToken token, string name, int minBits, List constraints) + : base(token, name, "") { + Contract.Requires(cce.NonNullElements(constraints, true)); + Contract.Requires(name != null); + Contract.Requires(token != null); + this.MinBits = minBits; + this.constraints = constraints; + } + + [Pure] + [Reads(ReadsAttribute.Reads.Everything)] + private static int MinBitsFor(Type t) { + Contract.Requires(t != null); + Contract.Requires(t.IsBv); + Contract.Ensures(0 <= Contract.Result()); + + if (t is TypeSynonymAnnotation) { + return MinBitsFor(((TypeSynonymAnnotation)t).ExpandedType); + } + + if (t is BvType) { + return t.BvBits; + } else { + return ((BvTypeProxy)t).MinBits; + } + } + + //----------- Cloning ---------------------------------- + + public override Type Clone(IDictionary/*!*/ varMap) { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result() != null); + Type p = ProxyFor; + if (p != null) { + return p.Clone(varMap); + } else { + return new BvTypeProxy(this.tok, this.Name, this.MinBits, this.constraints); // the clone will have a name that ends with $bvproxy$bvproxy + } + } + + public override Type CloneUnresolved() { + Contract.Ensures(Contract.Result() != null); + return new BvTypeProxy(this.tok, this.Name, this.MinBits, this.constraints); // the clone will have a name that ends with $bvproxy$bvproxy + } + + //----------- Unification of types ----------- + + public override bool Unify(Type that, + List unifiableVariables, + IDictionary result) { + //Contract.Requires(cce.NonNullElements(result)); + //Contract.Requires(unifiableVariables != null); + //Contract.Requires(that != null); + Type p = ProxyFor; + if (p != null) { + return p.Unify(that, unifiableVariables, result); + } + + // unify this with that, if possible + that = that.Expanded; + that = FollowProxy(that); + + if (this.ReallyOccursIn(that)) + return false; + + TypeVariable tv = that as TypeVariable; + + if (tv != null && unifiableVariables.Contains(tv)) + return that.Unify(this, unifiableVariables, result); + + if (object.ReferenceEquals(this, that)) { + return true; + } else if (that is BvType) { + if (MinBits <= that.BvBits) { + if (constraints != null) { + foreach (BvTypeConstraint btc in constraints) { + int minT1 = MinBitsFor(btc.T1); + int left = IncreaseBits(btc.T0, that.BvBits - minT1); + left = IncreaseBits(btc.T1, minT1 + left); + Contract.Assert(left == 0); // because it should always be possible to increase the total size of a BvTypeConstraint pair (t0,t1) arbitrarily + } + } + DefineProxy(that); + return true; + } + } else if (that is BvTypeProxy) { + BvTypeProxy bt = (BvTypeProxy)that; + // keep the proxy with the stronger constraint (that is, the higher minBits), but if either + // has a constraints list, then concatenate both constraints lists and define the previous + // proxies to the new one + if (this.constraints != null || bt.constraints != null) { + List list = new List(); + if (this.constraints != null) { + list.AddRange(this.constraints); + } + if (bt.constraints != null) { + list.AddRange(bt.constraints); + } + BvTypeProxy np = new BvTypeProxy(this.tok, this.Name, Math.Max(this.MinBits, bt.MinBits), list); + this.DefineProxy(np); + bt.DefineProxy(np); + } else if (this.MinBits <= bt.MinBits) { + this.DefineProxy(bt); + } else { + bt.DefineProxy(this); + } + return true; + } else if (that is ConstrainedProxy) { + // only bitvector proxies can be unified with this BvTypeProxy + return false; + } else if (that is TypeProxy) { + // define: that.ProxyFor := this; + return that.Unify(this, unifiableVariables, result); + } + return false; + } + + private static int IncreaseBits(Type t, int to) { + Contract.Requires(t != null); + Contract.Requires(t.IsBv && 0 <= to && MinBitsFor(t) <= to); + Contract.Ensures(0 <= Contract.Result() && Contract.Result() <= to); + + if(t is TypeSynonymAnnotation) { + return IncreaseBits(((TypeSynonymAnnotation)t).ExpandedType, to); + } + + t = FollowProxy(t); + if (t is BvType) { + return to - t.BvBits; + } else { + BvTypeProxy p = (BvTypeProxy)t; + Contract.Assert(p.MinBits <= to); + if (p.MinBits < to) { + BvTypeProxy q = new BvTypeProxy(p, to); + p.DefineProxy(q); + } + return 0; // we were able to satisfy the request completely + } + } + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + public override Type Substitute(IDictionary/*!*/ subst) { + //Contract.Requires(cce.NonNullElements(subst)); + Contract.Ensures(Contract.Result() != null); + if (this.ProxyFor == null) { + // check that the constraints are clean and do not contain any + // of the substituted variables (otherwise, we are in big trouble) + Contract.Assert(Contract.ForAll(constraints, c => + Contract.ForAll(subst.Keys, var => + !c.T0.FreeVariables.Contains(var) && !c.T1.FreeVariables.Contains(var)))); + } + return base.Substitute(subst); + } + + //----------- Getters/Issers ---------------------------------- + + public override bool IsBv { + get { + return true; + } + } + public override int BvBits { + get { + // This method is supposed to return the number of bits supplied, but unless the proxy has been resolved, + // we only have a lower bound on the number of bits supplied. But this method is not supposed to be + // called until type checking has finished, at which time the minBits is stable. + Type p = ProxyFor; + if (p != null) { + return p.BvBits; + } else { + return MinBits; + } + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitBvTypeProxy(this); + } + } + + // Proxy representing map types with a certain arity. Apart from the arity, + // a number of constraints on the index and value type of the map type may + // be known (such constraints result from applied select and store operations). + // Because map type can be polymorphic (in the most general case, each index or + // value type is described by a separate type parameter) any combination of + // constraints can be satisfied. + public class MapTypeProxy : ConstrainedProxy { + public readonly int Arity; + private readonly List/*!*/ constraints = new List(); + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(constraints != null); + } + + + // each constraint specifies that the given combination of argument/result + // types must be a possible instance of the formal map argument/result types + private struct Constraint { + public readonly List/*!*/ Arguments; + public readonly Type/*!*/ Result; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Arguments != null); + Contract.Invariant(Result != null); + } + + + public Constraint(List arguments, Type result) { + Contract.Requires(result != null); + Contract.Requires(arguments != null); + Arguments = arguments; + Result = result; + } + + public Constraint Clone(IDictionary/*!*/ varMap) { + Contract.Requires(cce.NonNullDictionaryAndValues(varMap)); + List/*!*/ args = new List(); + foreach (Type/*!*/ t in Arguments) { + Contract.Assert(t != null); + args.Add(t.Clone(varMap)); + } + Type/*!*/ res = Result.Clone(varMap); + Contract.Assert(res != null); + return new Constraint(args, res); + } + + public bool Unify(MapType that, + List/*!*/ unifiableVariables, + IDictionary/*!*/ result) { + Contract.Requires(unifiableVariables != null); + Contract.Requires(cce.NonNullDictionaryAndValues(result)); + Contract.Requires(that != null); + Contract.Requires(Arguments.Count == that.Arguments.Count); + Dictionary/*!*/ subst = new Dictionary(); + foreach (TypeVariable/*!*/ tv in that.TypeParameters) { + Contract.Assert(tv != null); + TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name); + subst.Add(tv, proxy); + } + + bool good = true; + for (int i = 0; i < that.Arguments.Count; i++) { + Type t0 = that.Arguments[i].Substitute(subst); + Type t1 = this.Arguments[i]; + good &= t0.Unify(t1, unifiableVariables, result); + } + good &= that.Result.Substitute(subst).Unify(this.Result, unifiableVariables, result); + return good; + } + } + + public MapTypeProxy(IToken token, string name, int arity) + : base(token, name, "mapproxy") { + Contract.Requires(name != null); + Contract.Requires(token != null); + Contract.Requires(0 <= arity); + this.Arity = arity; + } + + private void AddConstraint(Constraint c) { + Contract.Requires(c.Arguments.Count == Arity); + + Type f = ProxyFor; + MapType mf = f as MapType; + if (mf != null) { + bool success = c.Unify(mf, new List(), new Dictionary()); + Contract.Assert(success); + return; + } + + MapTypeProxy mpf = f as MapTypeProxy; + if (mpf != null) { + mpf.AddConstraint(c); + return; + } + + Contract.Assert(f == null); // no other types should occur as specialisations of this proxy + + constraints.Add(c); + } + + public Type CheckArgumentTypes(List/*!*/ actualArgs, + out TypeParamInstantiation/*!*/ tpInstantiation, + IToken/*!*/ typeCheckingSubject, + string/*!*/ opName, + TypecheckingContext/*!*/ tc) { + Contract.Requires(actualArgs != null); + Contract.Requires(typeCheckingSubject != null); + Contract.Requires(opName != null); + Contract.Requires(tc != null); + Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + + + + Type f = ProxyFor; + MapType mf = f as MapType; + if (mf != null) + return mf.CheckArgumentTypes(actualArgs, out tpInstantiation, typeCheckingSubject, opName, tc); + + MapTypeProxy mpf = f as MapTypeProxy; + if (mpf != null) + return mpf.CheckArgumentTypes(actualArgs, out tpInstantiation, typeCheckingSubject, opName, tc); + + Contract.Assert(f == null); // no other types should occur as specialisations of this proxy + + // otherwise, we just record the constraints given by this usage of the map type + List/*!*/ arguments = new List(); + foreach (Expr/*!*/ e in actualArgs) { + Contract.Assert(e != null); + arguments.Add(e.Type); + } + Type/*!*/ result = new TypeProxy(tok, "result"); + Contract.Assert(result != null); + AddConstraint(new Constraint(arguments, result)); + + List/*!*/ argumentsResult = new List(); + foreach (Expr/*!*/ e in actualArgs) { + Contract.Assert(e != null); + argumentsResult.Add(e.Type); + } + argumentsResult.Add(result); + + tpInstantiation = new MapTypeProxyParamInstantiation(this, argumentsResult); + return result; + } + + //----------- Cloning ---------------------------------- + + public override Type Clone(IDictionary/*!*/ varMap) { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result() != null); + Type p = ProxyFor; + if (p != null) { + return p.Clone(varMap); + } else { + MapTypeProxy p2 = new MapTypeProxy(tok, Name, Arity); + foreach (Constraint c in constraints) + p2.AddConstraint(c.Clone(varMap)); + return p2; // the clone will have a name that ends with $mapproxy$mapproxy (hopefully) + } + } + + //----------- Linearisation ---------------------------------- + + public override void Emit(TokenTextWriter stream, int contextBindingStrength) { + //Contract.Requires(stream != null); + Type p = ProxyFor; + if (p != null) { + p.Emit(stream, contextBindingStrength); + } else { + stream.Write("["); + string/*!*/ sep = ""; + for (int i = 0; i < Arity; ++i) { + stream.Write(sep); + sep = ", "; + stream.Write("?"); + } + stream.Write("]?"); + } + } + + //----------- Unification of types ----------- + + public override bool Unify(Type/*!*/ that, + List/*!*/ unifiableVariables, + IDictionary/*!*/ result) { + //Contract.Requires(that != null); + //Contract.Requires(unifiableVariables != null); + //Contract.Requires(cce.NonNullElements(result)); + Type p = ProxyFor; + if (p != null) { + return p.Unify(that, unifiableVariables, result); + } + + // unify this with that, if possible + that = that.Expanded; + that = FollowProxy(that); + + if (this.ReallyOccursIn(that)) + return false; + + TypeVariable tv = that as TypeVariable; + + if (tv != null && unifiableVariables.Contains(tv)) + return that.Unify(this, unifiableVariables, result); + + if (object.ReferenceEquals(this, that)) { + return true; + } else if (that is MapType) { + MapType mapType = (MapType)that; + if (mapType.Arguments.Count == Arity) { + bool good = true; + foreach (Constraint c in constraints) + good &= c.Unify(mapType, unifiableVariables, result); + if (good) { + DefineProxy(mapType); + return true; + } + } + } else if (that is MapTypeProxy) { + MapTypeProxy mt = (MapTypeProxy)that; + if (mt.Arity == this.Arity) { + // we propagate the constraints of this proxy to the more specific one + foreach (Constraint c in constraints) + mt.AddConstraint(c); + DefineProxy(mt); + return true; + } + } else if (that is ConstrainedProxy) { + // only map-type proxies can be unified with this MapTypeProxy + return false; + } else if (that is TypeProxy) { + // define: that.ProxyFor := this; + return that.Unify(this, unifiableVariables, result); + } + return false; + } + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + public override Type Substitute(IDictionary/*!*/ subst) { + //Contract.Requires(cce.NonNullElements(subst)); + Contract.Ensures(Contract.Result() != null); + if (this.ProxyFor == null) { + // check that the constraints are clean and do not contain any + // of the substituted variables (otherwise, we are in big trouble) + Contract.Assert(Contract.ForAll(constraints, c => + Contract.ForAll(subst.Keys, var => + Contract.ForAll(0, c.Arguments.Count, t => !c.Arguments[t].FreeVariables.Contains(var)) && + !c.Result.FreeVariables.Contains(var)))); + } + return base.Substitute(subst); + } + + //----------- Getters/Issers ---------------------------------- + + public override bool IsMap { + get { + return true; + } + } + public override MapType/*!*/ AsMap { + get { + Contract.Ensures(Contract.Result() != null); + + Type p = ProxyFor; + if (p != null) { + return p.AsMap; + } else { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // what to do now? + } + } + } + public override int MapArity { + get { + return Arity; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitMapTypeProxy(this); + } + } + + //===================================================================== + + // Used to annotate types with type synoyms that were used in the + // original unresolved types. Such types should be considered as + // equivalent to ExpandedType, the annotations are only used to enable + // better pretty-printing + public class TypeSynonymAnnotation : Type { + public Type/*!*/ ExpandedType; + + public readonly List/*!*/ Arguments; + // is set during resolution and determines whether the right number of arguments is given + public readonly TypeSynonymDecl/*!*/ Decl; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(ExpandedType != null); + Contract.Invariant(Arguments != null); + Contract.Invariant(Decl != null); + } + + + public TypeSynonymAnnotation(IToken/*!*/ token, TypeSynonymDecl/*!*/ decl, List/*!*/ arguments) + : base(token) { + Contract.Requires(token != null); + Contract.Requires(decl != null); + Contract.Requires(arguments != null); + Contract.Requires(arguments.Count == decl.TypeParameters.Count); + this.Decl = decl; + this.Arguments = arguments; + + // build a substitution that can be applied to the definition of + // the type synonym + IDictionary/*!*/ subst = + new Dictionary(); + for (int i = 0; i < arguments.Count; ++i) + subst.Add(decl.TypeParameters[i], arguments[i]); + + ExpandedType = decl.Body.Substitute(subst); + } + + private TypeSynonymAnnotation(IToken/*!*/ token, TypeSynonymDecl/*!*/ decl, List/*!*/ arguments, + Type/*!*/ expandedType) + : base(token) { + Contract.Requires(token != null); + Contract.Requires(decl != null); + Contract.Requires(arguments != null); + Contract.Requires(expandedType != null); + + this.Decl = decl; + this.Arguments = arguments; + this.ExpandedType = expandedType; + } + + //----------- Cloning ---------------------------------- + // We implement our own clone-method, because bound type variables + // have to be created in the right way. It is /not/ ok to just clone + // everything recursively + + public override Type Clone(IDictionary/*!*/ varMap) { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result() != null); + List/*!*/ newArgs = new List(); + foreach (Type/*!*/ t in Arguments) { + Contract.Assert(t != null); + newArgs.Add(t.Clone(varMap)); + } + Type/*!*/ newExpandedType = ExpandedType.Clone(varMap); + Contract.Assert(newExpandedType != null); + return new TypeSynonymAnnotation(tok, Decl, newArgs, newExpandedType); + } + + public override Type CloneUnresolved() { + Contract.Ensures(Contract.Result() != null); + List/*!*/ newArgs = new List(); + foreach (Type/*!*/ t in Arguments) { + Contract.Assert(t != null); + newArgs.Add(t.CloneUnresolved()); + } + return new TypeSynonymAnnotation(tok, Decl, newArgs); + } + + //----------- Equality ---------------------------------- + + [Pure] + public override bool Equals(Type/*!*/ that, + List/*!*/ thisBoundVariables, + List/*!*/ thatBoundVariables) { + //Contract.Requires(that != null); + //Contract.Requires(thisBoundVariables != null); + //Contract.Requires(thatBoundVariables != null); + return ExpandedType.Equals(that, thisBoundVariables, thatBoundVariables); + } + + // used to skip leading type annotations + internal override Type/*!*/ Expanded { + get { + Contract.Ensures(Contract.Result() != null); + + return ExpandedType.Expanded; + } + } + + //----------- Unification of types ----------- + + public override bool Unify(Type/*!*/ that, + List/*!*/ unifiableVariables, + IDictionary/*!*/ result) { + //Contract.Requires(that != null); + //Contract.Requires(unifiableVariables != null); + //Contract.Requires(cce.NonNullElements(result)); + return ExpandedType.Unify(that, unifiableVariables, result); + } + +#if OLD_UNIFICATION + public override void Unify(Type! that, + List! unifiableVariables, + List! thisBoundVariables, + List! thatBoundVariables, + IDictionary! result) { + ExpandedType.Unify(that, unifiableVariables, + thisBoundVariables, thatBoundVariables, result); + } +#endif + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + public override Type Substitute(IDictionary/*!*/ subst) { + //Contract.Requires(cce.NonNullElements(subst)); + Contract.Ensures(Contract.Result() != null); + if (subst.Count == 0) + return this; + List newArgs = new List(); + foreach (Type/*!*/ t in Arguments) { + Contract.Assert(t != null); + newArgs.Add(t.Substitute(subst)); + } + Type/*!*/ newExpandedType = ExpandedType.Substitute(subst); + Contract.Assert(newExpandedType != null); + return new TypeSynonymAnnotation(tok, Decl, newArgs, newExpandedType); + } + + //----------- Hashcodes ---------------------------------- + + [Pure] + public override int GetHashCode(List boundVariables) { + //Contract.Requires(boundVariables != null); + return ExpandedType.GetHashCode(boundVariables); + } + + //----------- Linearisation ---------------------------------- + + public override void Emit(TokenTextWriter stream, int contextBindingStrength) { + //Contract.Requires(stream != null); + stream.SetToken(this); + CtorType.EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength); + } + + //----------- Resolution ---------------------------------- + + public override Type ResolveType(ResolutionContext rc) { + //Contract.Requires(rc != null); + Contract.Ensures(Contract.Result() != null); + List resolvedArgs = new List(); + foreach (Type/*!*/ t in Arguments) { + Contract.Assert(t != null); + resolvedArgs.Add(t.ResolveType(rc)); + } + return new TypeSynonymAnnotation(tok, Decl, resolvedArgs); + } + + public override List/*!*/ FreeVariables { + get { + Contract.Ensures(Contract.Result>() != null); + + return ExpandedType.FreeVariables; + } + } + + public override List/*!*/ FreeProxies { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return ExpandedType.FreeProxies; + } + } + + //----------- Getters/Issers ---------------------------------- + + public override bool IsBasic { + get { + return ExpandedType.IsBasic; + } + } + public override bool IsInt { + get { + return ExpandedType.IsInt; + } + } + public override bool IsReal + { + get + { + return ExpandedType.IsReal; + } + } + public override bool IsFloat + { + get + { + return ExpandedType.IsFloat; + } + } + public override bool IsBool { + get { + return ExpandedType.IsBool; + } + } + + public override bool IsVariable { + get { + return ExpandedType.IsVariable; + } + } + public override TypeVariable/*!*/ AsVariable { + get { + Contract.Ensures(Contract.Result() != null); + return ExpandedType.AsVariable; + } + } + public override bool IsCtor { + get { + return ExpandedType.IsCtor; + } + } + public override CtorType/*!*/ AsCtor { + get { + Contract.Ensures(Contract.Result() != null); + return ExpandedType.AsCtor; + } + } + public override bool IsMap { + get { + return ExpandedType.IsMap; + } + } + public override MapType/*!*/ AsMap { + get { + Contract.Ensures(Contract.Result() != null); + return ExpandedType.AsMap; + } + } + public override bool IsUnresolved { + get { + return ExpandedType.IsUnresolved; + } + } + public override UnresolvedTypeIdentifier/*!*/ AsUnresolved { + get { + Contract.Ensures(Contract.Result() != null); + + return ExpandedType.AsUnresolved; + } + } + + public override bool IsBv { + get { + return ExpandedType.IsBv; + } + } + public override int BvBits { + get { + return ExpandedType.BvBits; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitTypeSynonymAnnotation(this); + } + } + + //===================================================================== + + public class CtorType : Type { + public readonly List/*!*/ Arguments; + // is set during resolution and determines whether the right number of arguments is given + public readonly TypeCtorDecl/*!*/ Decl; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Arguments != null); + Contract.Invariant(Decl != null); + } + + + public CtorType(IToken/*!*/ token, TypeCtorDecl/*!*/ decl, List/*!*/ arguments) + : base(token) { + Contract.Requires(token != null); + Contract.Requires(decl != null); + Contract.Requires(arguments != null); + Contract.Requires(arguments.Count == decl.Arity); + this.Decl = decl; + this.Arguments = arguments; + } + + public bool IsDatatype() { + return QKeyValue.FindBoolAttribute(Decl.Attributes, "datatype"); + } + + //----------- Cloning ---------------------------------- + // We implement our own clone-method, because bound type variables + // have to be created in the right way. It is /not/ ok to just clone + // everything recursively + + public override Type Clone(IDictionary/*!*/ varMap) { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result() != null); + List/*!*/ newArgs = new List(); + foreach (Type/*!*/ t in Arguments) { + Contract.Assert(t != null); + newArgs.Add(t.Clone(varMap)); + } + return new CtorType(tok, Decl, newArgs); + } + + public override Type CloneUnresolved() { + Contract.Ensures(Contract.Result() != null); + List/*!*/ newArgs = new List(); + foreach (Type/*!*/ t in Arguments) { + Contract.Assert(t != null); + newArgs.Add(t.CloneUnresolved()); + } + return new CtorType(tok, Decl, newArgs); + } + + //----------- Equality ---------------------------------- + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object that) { + Type thatType = that as Type; + if (thatType == null) + return false; + thatType = TypeProxy.FollowProxy(thatType.Expanded); + // shortcut + CtorType thatCtorType = thatType as CtorType; + if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl)) + return false; + if (Arguments.Count == 0) + return true; + return base.Equals(thatType); + } + + [Pure] + public override bool Equals(Type/*!*/ that, + List/*!*/ thisBoundVariables, + List/*!*/ thatBoundVariables) { + that = TypeProxy.FollowProxy(that.Expanded); + CtorType thatCtorType = that as CtorType; + if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl)) + return false; + for (int i = 0; i < Arguments.Count; ++i) { + if (!Arguments[i].Equals(thatCtorType.Arguments[i], + thisBoundVariables, thatBoundVariables)) + return false; + } + return true; + } + + //----------- Unification of types ----------- + + public override bool Unify(Type/*!*/ that, + List/*!*/ unifiableVariables, + IDictionary/*!*/ result) { + that = that.Expanded; + if (that is TypeProxy || that is TypeVariable) + return that.Unify(this, unifiableVariables, result); + + CtorType thatCtorType = that as CtorType; + if (thatCtorType == null || !thatCtorType.Decl.Equals(Decl)) { + return false; + } else { + bool good = true; + for (int i = 0; i < Arguments.Count; ++i) + good &= Arguments[i].Unify(thatCtorType.Arguments[i], unifiableVariables, result); + return good; + } + } + +#if OLD_UNIFICATION + public override void Unify(Type! that, + List! unifiableVariables, + List! thisBoundVariables, + List! thatBoundVariables, + IDictionary! result) { + that = that.Expanded; + if (that is TypeVariable) { + that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result); + return; + } + + CtorType thatCtorType = that as CtorType; + if (thatCtorType == null || !thatCtorType.Decl.Equals(Decl)) + throw UNIFICATION_FAILED; + for (int i = 0; i < Arguments.Length; ++i) + Arguments[i].Unify(thatCtorType.Arguments[i], + unifiableVariables, + thisBoundVariables, thatBoundVariables, + result); + } +#endif + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + public override Type Substitute(IDictionary/*!*/ subst) { + //Contract.Requires(cce.NonNullElements(subst)); + Contract.Ensures(Contract.Result() != null); + if (subst.Count == 0) + return this; + List newArgs = new List(); + lock (Arguments) + { + foreach (Type/*!*/ t in Arguments) + { + Contract.Assert(t != null); + newArgs.Add(t.Substitute(subst)); + } + } + return new CtorType(tok, Decl, newArgs); + } + + //----------- Hashcodes ---------------------------------- + + [Pure] + public override int GetHashCode(List boundVariables) { + //Contract.Requires(boundVariables != null); + int res = 1637643879 * Decl.GetHashCode(); + foreach (Type/*!*/ t in Arguments.ToArray()) { + Contract.Assert(t != null); + res = res * 3 + t.GetHashCode(boundVariables); + } + return res; + } + + //----------- Linearisation ---------------------------------- + + public override void Emit(TokenTextWriter stream, int contextBindingStrength) { + //Contract.Requires(stream != null); + stream.SetToken(this); + EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength); + } + + internal static void EmitCtorType(string name, List args, TokenTextWriter stream, int contextBindingStrength) { + Contract.Requires(stream != null); + Contract.Requires(args != null); + Contract.Requires(name != null); + int opBindingStrength = args.Count > 0 ? 0 : 2; + if (opBindingStrength < contextBindingStrength) + stream.Write("("); + + stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(name)); + int i = args.Count; + foreach (Type/*!*/ t in args) { + Contract.Assert(t != null); + stream.Write(" "); + // use a lower binding strength for the last argument + // to allow map-types without parentheses + t.Emit(stream, i == 1 ? 1 : 2); + i = i - 1; + } + + if (opBindingStrength < contextBindingStrength) + stream.Write(")"); + } + + //----------- Resolution ---------------------------------- + + public override Type ResolveType(ResolutionContext rc) { + //Contract.Requires(rc != null); + Contract.Ensures(Contract.Result() != null); + List resolvedArgs = new List(); + foreach (Type/*!*/ t in Arguments) { + Contract.Assert(t != null); + resolvedArgs.Add(t.ResolveType(rc)); + } + return new CtorType(tok, Decl, resolvedArgs); + } + + public override List/*!*/ FreeVariables { + get { + List/*!*/ res = new List(); + foreach (Type/*!*/ t in Arguments.ToArray()) { + Contract.Assert(t != null); + res.AppendWithoutDups(t.FreeVariables); + } + return res; + } + } + + public override List/*!*/ FreeProxies { + get { + List/*!*/ res = new List(); + foreach (Type/*!*/ t in Arguments.ToArray()) { + Contract.Assert(t != null); + AppendWithoutDups(res, t.FreeProxies); + } + return res; + } + } + + //----------- Getters/Issers ---------------------------------- + + public override bool IsCtor { + get { + return true; + } + } + public override CtorType/*!*/ AsCtor { + get { + return this; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitCtorType(this); + } + } + + //===================================================================== + + public class MapType : Type { + // an invariant is that each of the type parameters has to occur as + // free variable in at least one of the arguments + public readonly List/*!*/ TypeParameters; + public readonly List/*!*/ Arguments; + public Type/*!*/ Result; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(TypeParameters != null); + Contract.Invariant(Arguments != null); + Contract.Invariant(Result != null); + } + + + public MapType(IToken/*!*/ token, List/*!*/ typeParameters, List/*!*/ arguments, Type/*!*/ result) + : base(token) { + Contract.Requires(token != null); + Contract.Requires(typeParameters != null); + Contract.Requires(arguments != null); + Contract.Requires(result != null); + + this.TypeParameters = typeParameters; + this.Result = result; + this.Arguments = arguments; + } + + //----------- Cloning ---------------------------------- + // We implement our own clone-method, because bound type variables + // have to be created in the right way. It is /not/ ok to just clone + // everything recursively + + public override Type Clone(IDictionary/*!*/ varMap) { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result() != null); + IDictionary/*!*/ newVarMap = + new Dictionary(); + foreach (KeyValuePair p in varMap) { + Contract.Assert(cce.NonNullElements(p)); + if (!TypeParameters.Contains(p.Key)) + newVarMap.Add(p); + } + + List/*!*/ newTypeParams = new List(); + foreach (TypeVariable/*!*/ var in TypeParameters) { + Contract.Assert(var != null); + TypeVariable/*!*/ newVar = new TypeVariable(var.tok, var.Name); + Contract.Assert(newVar != null); + newVarMap.Add(var, newVar); + newTypeParams.Add(newVar); + } + + List/*!*/ newArgs = new List(); + foreach (Type/*!*/ t in Arguments) { + Contract.Assert(t != null); + newArgs.Add(t.Clone(newVarMap)); + } + Type/*!*/ newResult = Result.Clone(newVarMap); + Contract.Assert(newResult != null); + + return new MapType(this.tok, newTypeParams, newArgs, newResult); + } + + public override Type CloneUnresolved() { + Contract.Ensures(Contract.Result() != null); + List/*!*/ newTypeParams = new List(); + foreach (TypeVariable/*!*/ var in TypeParameters) { + Contract.Assert(var != null); + TypeVariable/*!*/ newVar = new TypeVariable(var.tok, var.Name); + Contract.Assert(newVar != null); + newTypeParams.Add(newVar); + } + + List/*!*/ newArgs = new List(); + foreach (Type/*!*/ t in Arguments) { + Contract.Assert(t != null); + newArgs.Add(t.CloneUnresolved()); + } + Type/*!*/ newResult = Result.CloneUnresolved(); + Contract.Assert(newResult != null); + + return new MapType(this.tok, newTypeParams, newArgs, newResult); + } + + //----------- Equality ---------------------------------- + + [Pure] + public override bool Equals(Type/*!*/ that, + List/*!*/ thisBoundVariables, + List/*!*/ thatBoundVariables) + { + that = TypeProxy.FollowProxy(that.Expanded); + MapType thatMapType = that as MapType; + if (thatMapType == null || + this.TypeParameters.Count != thatMapType.TypeParameters.Count || + this.Arguments.Count != thatMapType.Arguments.Count) + return false; + + thisBoundVariables = thisBoundVariables.ToList(); + foreach (TypeVariable/*!*/ var in this.TypeParameters) + { + Contract.Assert(var != null); + thisBoundVariables.Add(var); + } + thatBoundVariables = thatBoundVariables.ToList(); + foreach (TypeVariable/*!*/ var in thatMapType.TypeParameters) + { + Contract.Assert(var != null); + thatBoundVariables.Add(var); + } + + for (int i = 0; i < Arguments.Count; ++i) + { + if (!Arguments[i].Equals(thatMapType.Arguments[i], + thisBoundVariables, thatBoundVariables)) + return false; + } + + return this.Result.Equals(thatMapType.Result, + thisBoundVariables, thatBoundVariables); + } + + //----------- Unification of types ----------- + + public override bool Unify(Type/*!*/ that, + List/*!*/ unifiableVariables, + IDictionary/*!*/ result) { + that = that.Expanded; + if (that is TypeProxy || that is TypeVariable) + return that.Unify(this, unifiableVariables, result); + + MapType thatMapType = that as MapType; + if (thatMapType == null || + this.TypeParameters.Count != thatMapType.TypeParameters.Count || + this.Arguments.Count != thatMapType.Arguments.Count) + return false; + + // treat the bound variables of the two map types as equal... + Dictionary/*!*/ subst0 = + new Dictionary(); + Dictionary/*!*/ subst1 = + new Dictionary(); + List freshies = new List(); + for (int i = 0; i < this.TypeParameters.Count; i++) { + TypeVariable tp0 = this.TypeParameters[i]; + TypeVariable tp1 = thatMapType.TypeParameters[i]; + TypeVariable freshVar = new TypeVariable(tp0.tok, tp0.Name); + freshies.Add(freshVar); + subst0.Add(tp0, freshVar); + subst1.Add(tp1, freshVar); + } + // ... and then unify the domain and range types + bool good = true; + for (int i = 0; i < this.Arguments.Count; i++) { + Type t0 = this.Arguments[i].Substitute(subst0); + Type t1 = thatMapType.Arguments[i].Substitute(subst1); + good &= t0.Unify(t1, unifiableVariables, result); + } + Type r0 = this.Result.Substitute(subst0); + Type r1 = thatMapType.Result.Substitute(subst1); + good &= r0.Unify(r1, unifiableVariables, result); + + // Finally, check that none of the bound variables has escaped + if (good && freshies.Count != 0) { + // This is done by looking for occurrences of the fresh variables in the + // non-substituted types ... + List freeVars = this.FreeVariables; + foreach (TypeVariable fr in freshies) + if (freeVars.Contains(fr)) { + return false; + } // fresh variable escaped + freeVars = thatMapType.FreeVariables; + foreach (TypeVariable fr in freshies) + if (freeVars.Contains(fr)) { + return false; + } // fresh variable escaped + + // ... and in the resulting unifier of type variables + foreach (KeyValuePair pair in result) { + Contract.Assert(cce.NonNullElements(pair)); + freeVars = pair.Value.FreeVariables; + foreach (TypeVariable fr in freshies) + if (freeVars.Contains(fr)) { + return false; + } // fresh variable escaped + } + } + + return good; + } + +#if OLD_UNIFICATION + public override void Unify(Type! that, + List! unifiableVariables, + List! thisBoundVariables, + List! thatBoundVariables, + IDictionary! result) { + that = that.Expanded; + if (that is TypeVariable) { + that.Unify(this, unifiableVariables, thatBoundVariables, thisBoundVariables, result); + return; + } + + MapType thatMapType = that as MapType; + if (thatMapType == null || + this.TypeParameters.Length != thatMapType.TypeParameters.Length || + this.Arguments.Length != thatMapType.Arguments.Length) + throw UNIFICATION_FAILED; + + // ensure that no collisions occur + if (this.collisionsPossible(result)) { + ((MapType)this.Clone()) + .Unify(that, unifiableVariables, + thisBoundVariables, thatBoundVariables, result); + return; + } + if (thatMapType.collisionsPossible(result)) + thatMapType = (MapType)that.Clone(); + + foreach(TypeVariable/*!*/ var in this.TypeParameters){ +Contract.Assert(var != null); + thisBoundVariables.Add(var);} + foreach(TypeVariable/*!*/ var in thatMapType.TypeParameters){ +Contract.Assert(var != null); + thatBoundVariables.Add(var);} + + try { + + for (int i = 0; i < Arguments.Length; ++i) + Arguments[i].Unify(thatMapType.Arguments[i], + unifiableVariables, + thisBoundVariables, thatBoundVariables, + result); + Result.Unify(thatMapType.Result, + unifiableVariables, + thisBoundVariables, thatBoundVariables, + result); + + } finally { + // make sure that the bound variables are removed again + for (int i = 0; i < this.TypeParameters.Length; ++i) { + thisBoundVariables.Remove(); + thatBoundVariables.Remove(); + } + } + } +#endif + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + [Pure] + private bool collisionsPossible(IDictionary/*!*/ subst) { + Contract.Requires(cce.NonNullDictionaryAndValues(subst)); + // PR: could be written more efficiently + return TypeParameters.Any(param => subst.ContainsKey(param) || subst.Values.Any(val => val.FreeVariables.Contains(param))); + } + + public override Type Substitute(IDictionary/*!*/ subst) { + //Contract.Requires(cce.NonNullElements(subst)); + Contract.Ensures(Contract.Result() != null); + if (subst.Count == 0) + return this; + + // there are two cases in which we have to be careful: + // * a variable to be substituted is shadowed by a variable binder + // * a substituted term contains variables that are bound in the + // type (variable capture) + // + // in both cases, we first clone the type to ensure that bound + // variables are fresh + + if (collisionsPossible(subst)) { + MapType/*!*/ newType = (MapType)this.Clone(); + Contract.Assert(newType != null); + Contract.Assert(newType.Equals(this) && !newType.collisionsPossible(subst)); + return newType.Substitute(subst); + } + + List newArgs = new List(); + lock (Arguments) + { + foreach (Type/*!*/ t in Arguments) + { + Contract.Assert(t != null); + newArgs.Add(t.Substitute(subst)); + } + } + Type/*!*/ newResult = Result.Substitute(subst); + Contract.Assert(newResult != null); + + return new MapType(tok, TypeParameters, newArgs, newResult); + } + + //----------- Hashcodes ---------------------------------- + + [Pure] + public override int GetHashCode(List boundVariables) { + //Contract.Requires(boundVariables != null); + int res = 7643761 * TypeParameters.Count + 65121 * Arguments.Count; + + boundVariables = boundVariables.ToList(); + foreach (TypeVariable/*!*/ var in this.TypeParameters) { + Contract.Assert(var != null); + boundVariables.Add(var); + } + + foreach (Type/*!*/ t in Arguments.ToArray()) { + Contract.Assert(t != null); + res = res * 5 + t.GetHashCode(boundVariables); + } + res = res * 7 + Result.GetHashCode(boundVariables); + + return res; + } + + //----------- Linearisation ---------------------------------- + + public override void Emit(TokenTextWriter stream, int contextBindingStrength) { + //Contract.Requires(stream != null); + stream.SetToken(this); + + const int opBindingStrength = 1; + if (opBindingStrength < contextBindingStrength) + stream.Write("("); + + EmitOptionalTypeParams(stream, TypeParameters); + + stream.Write("["); + Arguments.Emit(stream, ","); // default binding strength of 0 is ok + stream.Write("]"); + Result.Emit(stream); // default binding strength of 0 is ok + + if (opBindingStrength < contextBindingStrength) + stream.Write(")"); + } + + //----------- Resolution ---------------------------------- + + public override Type ResolveType(ResolutionContext rc) { + //Contract.Requires(rc != null); + Contract.Ensures(Contract.Result() != null); + int previousState = rc.TypeBinderState; + try { + foreach (TypeVariable/*!*/ v in TypeParameters) { + Contract.Assert(v != null); + rc.AddTypeBinder(v); + } + + List resolvedArgs = new List(); + foreach (Type/*!*/ ty in Arguments) { + Contract.Assert(ty != null); + resolvedArgs.Add(ty.ResolveType(rc)); + } + + Type resolvedResult = Result.ResolveType(rc); + + CheckBoundVariableOccurrences(TypeParameters, + resolvedArgs, new List { resolvedResult }, + this.tok, "map arguments", + rc); + + // sort the type parameters so that they are bound in the order of occurrence + List/*!*/ sortedTypeParams = SortTypeParams(TypeParameters, resolvedArgs, resolvedResult); + Contract.Assert(sortedTypeParams != null); + return new MapType(tok, sortedTypeParams, resolvedArgs, resolvedResult); + } finally { + rc.TypeBinderState = previousState; + } + } + + public override List/*!*/ FreeVariables { + get { + List/*!*/ res = FreeVariablesIn(Arguments.ToList()); + Contract.Assert(res != null); + res.AppendWithoutDups(Result.FreeVariables); + foreach (TypeVariable/*!*/ v in TypeParameters.ToArray()) { + Contract.Assert(v != null); + res.Remove(v); + } + return res; + } + } + + public override List/*!*/ FreeProxies { + get { + List/*!*/ res = new List(); + foreach (Type/*!*/ t in Arguments.ToArray()) { + Contract.Assert(t != null); + AppendWithoutDups(res, t.FreeProxies); + } + AppendWithoutDups(res, Result.FreeProxies); + return res; + } + } + + //----------- Getters/Issers ---------------------------------- + + public override bool IsMap { + get { + return true; + } + } + public override MapType/*!*/ AsMap { + get { + return this; + } + } + public override int MapArity { + get { + return Arguments.Count; + } + } + + //------------ Match formal argument types of the map + //------------ on concrete types, substitute the result into the + //------------ result type. Null is returned if so many type checking + //------------ errors occur that the situation is hopeless + + public Type CheckArgumentTypes(List/*!*/ actualArgs, + out TypeParamInstantiation/*!*/ tpInstantiation, + IToken/*!*/ typeCheckingSubject, + string/*!*/ opName, + TypecheckingContext/*!*/ tc) { + Contract.Requires(actualArgs != null); + Contract.Requires(typeCheckingSubject != null); + + Contract.Requires(opName != null); + Contract.Requires(tc != null); +Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + List/*!*/ actualTypeParams; + List actualResult = + Type.CheckArgumentTypes(TypeParameters, out actualTypeParams, Arguments, actualArgs, + new List { Result }, null, typeCheckingSubject, opName, tc); + if (actualResult == null) { + tpInstantiation = SimpleTypeParamInstantiation.EMPTY; + return null; + } else { + Contract.Assert(actualResult.Count == 1); + tpInstantiation = SimpleTypeParamInstantiation.From(TypeParameters, actualTypeParams); + return actualResult[0]; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitMapType(this); + } + } + + //--------------------------------------------------------------------- + + public enum SimpleType { + Int, + Real, + Bool + }; + + + //===================================================================== + + // Interface for representing the instantiations of type parameters of + // polymorphic functions or maps. We introduce an own interface for this + // instead of using a simple list or dictionary, because in some cases + // (due to the type proxies for map types) the actual number and instantiation + // of type parameters can only be determined very late. + [ContractClass(typeof(TypeParamInstantiationContracts))] + public interface TypeParamInstantiation { + // return what formal type parameters there are + List/*!*/ FormalTypeParams { + get; + } + // given a formal type parameter, return the actual instantiation + Type/*!*/ this[TypeVariable/*!*/ var] { + get; + } + } + [ContractClassFor(typeof(TypeParamInstantiation))] + public abstract class TypeParamInstantiationContracts : TypeParamInstantiation { + #region TypeParamInstantiation Members + + public List FormalTypeParams { + + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + throw new NotImplementedException(); + } + } + + public Type this[TypeVariable var] { + get { + Contract.Requires(var != null); + Contract.Ensures(Contract.Result() != null); + + throw new NotImplementedException(); + } + } + + #endregion + } + + + public class SimpleTypeParamInstantiation : TypeParamInstantiation { + private readonly List/*!*/ TypeParams; + [ContractInvariantMethod] + void TypeParamsInvariantMethod() { + Contract.Invariant(cce.NonNullElements(TypeParams)); + } + private readonly IDictionary/*!*/ Instantiations; + [ContractInvariantMethod] + void InstantiationsInvariantMethod() { + Contract.Invariant(cce.NonNullDictionaryAndValues(Instantiations)); + } + + public SimpleTypeParamInstantiation(List/*!*/ typeParams, + IDictionary/*!*/ instantiations) { + Contract.Requires(cce.NonNullElements(typeParams)); + Contract.Requires(cce.NonNullDictionaryAndValues(instantiations)); + this.TypeParams = typeParams; + this.Instantiations = instantiations; + } + + public static TypeParamInstantiation/*!*/ From(List typeParams, List/*!*/ actualTypeParams) { + Contract.Requires(cce.NonNullElements(actualTypeParams)); + Contract.Requires(typeParams != null); + Contract.Requires(typeParams.Count == actualTypeParams.Count); + Contract.Ensures(Contract.Result() != null); + + if (typeParams.Count == 0) + return EMPTY; + + List/*!*/ typeParamList = new List(); + IDictionary/*!*/ dict = new Dictionary(); + for (int i = 0; i < typeParams.Count; ++i) { + typeParamList.Add(typeParams[i]); + dict.Add(typeParams[i], actualTypeParams[i]); + } + return new SimpleTypeParamInstantiation(typeParamList, dict); + } + + public static readonly TypeParamInstantiation EMPTY = + new SimpleTypeParamInstantiation(new List(), + new Dictionary()); + + // return what formal type parameters there are + public List/*!*/ FormalTypeParams { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return TypeParams; + } + } + // given a formal type parameter, return the actual instantiation + public Type/*!*/ this[TypeVariable/*!*/ var] { + get { + return Instantiations[var]; + } + } + } + + // Implementation of TypeParamInstantiation that refers to the current + // value of a MapTypeProxy. This means that the values return by the + // methods of this implementation can change in case the MapTypeProxy + // receives further unifications. + class MapTypeProxyParamInstantiation : TypeParamInstantiation { + private readonly MapTypeProxy/*!*/ Proxy; + + // the argument and result type of this particular usage of the map + // type. these are necessary to derive the values of the type parameters + private readonly List/*!*/ ArgumentsResult; + + // field that is initialised once all necessary information is available + // (the MapTypeProxy is instantiated to an actual type) and the instantiation + // of a type parameter is queried + private IDictionary Instantiations = null; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Proxy != null); + Contract.Invariant(ArgumentsResult != null); + Contract.Invariant(Instantiations == null || cce.NonNullDictionaryAndValues(Instantiations)); + } + + + public MapTypeProxyParamInstantiation(MapTypeProxy/*!*/ proxy, + List/*!*/ argumentsResult) { + Contract.Requires(proxy != null); + Contract.Requires(argumentsResult != null); + this.Proxy = proxy; + this.ArgumentsResult = argumentsResult; + } + + // return what formal type parameters there are + public List/*!*/ FormalTypeParams { + get { + MapType realType = Proxy.ProxyFor as MapType; + if (realType == null) + // no instantiation of the map type is known, which means + // that the map type is assumed to be monomorphic + return new List(); + else + return realType.TypeParameters.ToList(); + } + } + + // given a formal type parameter, return the actual instantiation + public Type/*!*/ this[TypeVariable/*!*/ var] { + get { + // then there has to be an instantiation that is a polymorphic map type + if (Instantiations == null) { + MapType realType = Proxy.ProxyFor as MapType; + Contract.Assert(realType != null); + List/*!*/ formalArgs = new List(); + foreach (Type/*!*/ t in realType.Arguments) { + Contract.Assert(t != null); + formalArgs.Add(t); + } + formalArgs.Add(realType.Result); + Instantiations = + Type.InferTypeParameters(realType.TypeParameters, formalArgs, ArgumentsResult); + } + return Instantiations[var]; + } + } + } } \ No newline at end of file -- cgit v1.2.3