diff options
| author |  tabarbe <unknown> | 2010-08-20 22:29:44 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-20 22:29:44 +0000 |
| commit | b617dda87871573b826dada4af73fc48dce94f15 (patch) | |
| tree | 453088d59b99376c0b14035e76463a4561d6ec1c /Source/Core/AbsyType.cs | |
| parent | 0d77cf304b9bd2b2152fe1a733e4533536c883c0 (diff) | |
Boogie: Renaming core sources in preparation for port commit
Diffstat (limited to 'Source/Core/AbsyType.cs')
| -rw-r--r-- | Source/Core/AbsyType.cs | 2857 |
1 files changed, 2857 insertions, 0 deletions
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs new file mode 100644 index 00000000..55b8913f --- /dev/null +++ b/Source/Core/AbsyType.cs @@ -0,0 +1,2857 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+//---------------------------------------------------------------------------------------------
+// BoogiePL - Absy.cs
+//---------------------------------------------------------------------------------------------
+
+namespace Microsoft.Boogie
+{
+ using System;
+ using System.Collections;
+ using System.Diagnostics;
+ using System.Collections.Generic;
+ using Microsoft.Boogie.AbstractInterpretation;
+ using AI = Microsoft.AbstractInterpretationFramework;
+ using Microsoft.Contracts;
+
+ //=====================================================================
+ //---------------------------------------------------------------------
+ // Types
+
+ public abstract class Type : Absy {
+ public Type(IToken! token)
+ : base(token)
+ {
+ }
+
+ //----------- 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() {
+ return this.Clone(new Dictionary<TypeVariable!, TypeVariable!> ());
+ }
+
+ public abstract Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap);
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ public abstract Type! CloneUnresolved();
+
+ //----------- Linearisation ----------------------------------
+
+ public void Emit(TokenTextWriter! stream) {
+ this.Emit(stream, 0);
+ }
+
+ public abstract void Emit(TokenTextWriter! stream, int contextBindingStrength);
+
+ [Pure]
+ public override string! ToString() {
+ System.IO.StringWriter buffer = new System.IO.StringWriter();
+ using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, 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 TypeVariableSeq (),
+ new TypeVariableSeq ());
+ }
+
+ [Pure]
+ public abstract bool Equals(Type! that,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables);
+
+ // used to skip leading type annotations (subexpressions of the
+ // resulting type might still contain annotations)
+ internal virtual Type! Expanded { get {
+ return this;
+ } }
+
+ //----------- Unification of types -----------
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ public bool Unify(Type! that) {
+ return Unify(that, new TypeVariableSeq(), new Dictionary<TypeVariable!, Type!> ());
+ }
+
+ public abstract bool Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ // an idempotent substitution that describes the
+ // unification result up to a certain point
+ IDictionary<TypeVariable!, Type!>! unifier);
+ requires forall{TypeVariable key in unifier.Keys; unifiableVariables.Has(key)};
+ requires IsIdempotent(unifier);
+
+ [Pure]
+ public static bool IsIdempotent(IDictionary<TypeVariable!, Type!>! unifier) {
+ return forall{Type! t in unifier.Values;
+ forall{TypeVariable! var in t.FreeVariables;
+ !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<TypeVariable!, Type!> Unify(Type! that,
+ TypeVariableSeq! unifiableVariables) {
+ Dictionary<TypeVariable!, Type!>! result = new Dictionary<TypeVariable!, Type!> ();
+ try {
+ this.Unify(that, unifiableVariables,
+ new TypeVariableSeq (), new TypeVariableSeq (), 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,
+ TypeVariableSeq! unifiableVariables,
+ // given mappings that need to be taken into account
+ // the old unifier has to be idempotent as well
+ IDictionary<TypeVariable!, Type!>! unifier)
+ requires forall{TypeVariable key in unifier.Keys; unifiableVariables.Has(key)};
+ requires IsIdempotent(unifier);
+ {
+ try {
+ this.Unify(that, unifiableVariables,
+ new TypeVariableSeq (), new TypeVariableSeq (), unifier);
+ } catch (UnificationFailedException) {
+ return false;
+ }
+ return true; + }
+
+ public abstract void Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables,
+ // an idempotent substitution that describes the
+ // unification result up to a certain point
+ IDictionary<TypeVariable!, Type!>! result);
+#endif
+
+ //----------- Substitution of free variables with types not containing bound variables -----------------
+
+ public abstract Type! Substitute(IDictionary<TypeVariable!, Type!>! 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 TypeVariableSeq ());
+ }
+
+ [Pure]
+ public abstract int GetHashCode(TypeVariableSeq! boundVariables);
+
+ //----------- Resolution ----------------------------------
+
+ public override void Resolve(ResolutionContext! rc)
+ {
+ 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)
+ {
+ 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 TypeVariableSeq! FreeVariables { get; }
+
+ // determine the free type proxies in a type, in the order in which they occur
+ public abstract List<TypeProxy!>! FreeProxies { get; }
+
+ protected static void AppendWithoutDups<A>(List<A>! a, List<A>! b) {
+ foreach (A x in b)
+ if (!a.Contains(x))
+ a.Add(x);
+ }
+
+ public bool IsClosed { get {
+ return FreeVariables.Length == 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 IsBool { get { return false; } }
+
+ public virtual bool IsVariable { get { return false; } }
+ public virtual TypeVariable! AsVariable { get {
+ assert false; // Type.AsVariable should never be called
+ } }
+ public virtual bool IsCtor { get { return false; } }
+ public virtual CtorType! AsCtor { get {
+ assert false; // Type.AsCtor should never be called
+ } }
+ public virtual bool IsMap { get { return false; } }
+ public virtual MapType! AsMap { get {
+ assert false; // Type.AsMap should never be called
+ } }
+ public virtual int MapArity { get {
+ assert false; // Type.MapArity should never be called
+ } }
+ public virtual bool IsUnresolved { get { return false; } }
+ public virtual UnresolvedTypeIdentifier! AsUnresolved { get {
+ assert false; // Type.AsUnresolved should never be called
+ } }
+
+ public virtual bool IsBv { get { return false; } }
+ public virtual int BvBits { get {
+ assert false; // Type.BvBits should never be called
+ } }
+
+ public static readonly Type! Int = new BasicType(SimpleType.Int);
+ public static readonly Type! Bool = new BasicType(SimpleType.Bool);
+ private static BvType[] bvtypeCache;
+
+ static public BvType! GetBvType(int sz)
+ requires 0 <= sz;
+ {
+ 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);
+ }
+ }
+
+ //------------ Match formal argument types on actual argument types
+ //------------ and return the resulting substitution of type variables
+
+#if OLD_UNIFICATION
+ public static IDictionary<TypeVariable!, Type!>!
+ MatchArgumentTypes(TypeVariableSeq! typeParams,
+ TypeSeq! formalArgs,
+ ExprSeq! actualArgs,
+ TypeSeq formalOuts,
+ IdentifierExprSeq actualOuts,
+ string! opName,
+ TypecheckingContext! tc)
+ requires formalArgs.Length == actualArgs.Length;
+ requires formalOuts == null <==> actualOuts == null;
+ requires formalOuts != null ==> formalOuts.Length == actualOuts.Length;
+ {
+ TypeVariableSeq! boundVarSeq0 = new TypeVariableSeq ();
+ TypeVariableSeq! boundVarSeq1 = new TypeVariableSeq ();
+ Dictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!>();
+
+ for (int i = 0; i < formalArgs.Length; ++i) {
+ try {
+ Type! actualType = (!)((!)actualArgs[i]).Type;
+ // if the type variables to be matched occur in the actual
+ // argument types, something has gone very wrong
+ 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
+ assert boundVarSeq0.Length == 0 && boundVarSeq1.Length == 0;
+ }
+ }
+
+ if (formalOuts != null) {
+ for (int i = 0; i < formalOuts.Length; ++i) {
+ try {
+ Type! actualType = (!)((!)actualOuts[i]).Type;
+ // if the type variables to be matched occur in the actual
+ // argument types, something has gone very wrong
+ 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
+ assert boundVarSeq0.Length == 0 && boundVarSeq1.Length == 0;
+ }
+ }
+ }
+
+ // we only allow type parameters to be substituted
+ assert forall{TypeVariable! var in subst.Keys; typeParams.Has(var)};
+
+ return subst;
+ }
+#else
+ public static IDictionary<TypeVariable!, Type!>!
+ MatchArgumentTypes(TypeVariableSeq! typeParams,
+ TypeSeq! formalArgs,
+ ExprSeq! actualArgs,
+ TypeSeq formalOuts,
+ IdentifierExprSeq actualOuts,
+ string! opName,
+ TypecheckingContext! tc)
+ requires formalArgs.Length == actualArgs.Length;
+ requires formalOuts == null <==> actualOuts == null;
+ requires formalOuts != null ==> formalOuts.Length == ((!)actualOuts).Length;
+ requires tc != null ==> opName != null;
+ // requires "actualArgs" and "actualOuts" to have been type checked
+ {
+ Dictionary<TypeVariable!, Type!> subst = new Dictionary<TypeVariable!, Type!>();
+ foreach (TypeVariable! tv in typeParams) {
+ TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name);
+ subst.Add(tv, proxy);
+ }
+
+ for (int i = 0; i < formalArgs.Length; i++) {
+ Type formal = formalArgs[i].Substitute(subst);
+ Type actual = (!)((!)actualArgs[i]).Type;
+ // if the type variables to be matched occur in the actual
+ // argument types, something has gone very wrong
+ assert forall{TypeVariable! var in typeParams; !actual.FreeVariables.Has(var)};
+
+ if (!formal.Unify(actual)) {
+ assume tc != null; // caller expected no errors
+ assert opName != null; // follows from precondition
+ tc.Error((!)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.Length; ++i) {
+ Type formal = formalOuts[i].Substitute(subst);
+ Type actual = (!)((!)actualOuts)[i].Type;
+ // if the type variables to be matched occur in the actual
+ // argument types, something has gone very wrong
+ assert forall{TypeVariable! var in typeParams; !actual.FreeVariables.Has(var)};
+
+ if (!formal.Unify(actual)) {
+ assume tc != null; // caller expected no errors
+ 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 TypeSeq CheckArgumentTypes(TypeVariableSeq! typeParams,
+ out List<Type!>! actualTypeParams,
+ TypeSeq! formalIns,
+ ExprSeq! actualIns,
+ TypeSeq! formalOuts,
+ IdentifierExprSeq actualOuts,
+ IToken! typeCheckingSubject,
+ string! opName,
+ TypecheckingContext! tc)
+ // requires "actualIns" and "actualOuts" to have been type checked
+ {
+ actualTypeParams = new List<Type!> ();
+
+ if (formalIns.Length != actualIns.Length) {
+ tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1}",
+ opName, actualIns.Length);
+ // if there are no type parameters, we can still return the result
+ // type and hope that the type checking proceeds
+ return typeParams.Length == 0 ? formalOuts : null;
+ } else if (actualOuts != null && formalOuts.Length != actualOuts.Length) {
+ tc.Error(typeCheckingSubject, "wrong number of result variables in {0}: {1}",
+ opName, actualOuts.Length);
+ // if there are no type parameters, we can still return the result
+ // type and hope that the type checking proceeds
+ actualTypeParams = new List<Type!> ();
+ return typeParams.Length == 0 ? formalOuts : null;
+ }
+
+ int previousErrorCount = tc.ErrorCount;
+ IDictionary<TypeVariable!, Type!> subst =
+ MatchArgumentTypes(typeParams, formalIns, actualIns,
+ actualOuts != null ? formalOuts : null, actualOuts, opName, tc);
+
+ foreach (TypeVariable! var in typeParams)
+ actualTypeParams.Add(subst[var]);
+
+ TypeSeq! actualResults = new TypeSeq ();
+ foreach (Type! t in formalOuts) {
+ actualResults.Add(t.Substitute(subst));
+ }
+ TypeVariableSeq 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 (forall{TypeVariable! var in typeParams; !resultFreeVars.Has(var)})
+ return actualResults;
+ else
+ // otherwise there is no point in returning the result type,
+ // type checking would only get confused even further
+ return null;
+ }
+
+ assert forall{TypeVariable! var in typeParams; !resultFreeVars.Has(var)};
+ return actualResults;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+
+ // about the same as Type.CheckArgumentTypes, but without
+ // detailed error reports
+ public static Type! InferValueType(TypeVariableSeq! typeParams,
+ TypeSeq! formalArgs,
+ Type! formalResult,
+ TypeSeq! actualArgs) {
+ IDictionary<TypeVariable!, Type!>! subst =
+ InferTypeParameters(typeParams, formalArgs, actualArgs);
+
+ Type! res = formalResult.Substitute(subst);
+ // all type parameters have to be substituted with concrete types
+ TypeVariableSeq! resFreeVars = res.FreeVariables;
+ assert forall{TypeVariable! var in typeParams; !resFreeVars.Has(var)};
+ return res;
+ }
+
+#if OLD_UNIFICATION
+ public static IDictionary<TypeVariable!, Type!>!
+ InferTypeParameters(TypeVariableSeq! typeParams,
+ TypeSeq! formalArgs,
+ TypeSeq! actualArgs)
+ requires formalArgs.Length == actualArgs.Length; {
+
+ TypeVariableSeq! boundVarSeq0 = new TypeVariableSeq ();
+ TypeVariableSeq! boundVarSeq1 = new TypeVariableSeq ();
+ Dictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!>();
+
+ for (int i = 0; i < formalArgs.Length; ++i) {
+ try {
+ 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
+ assert forall{TypeVariable! var in subst.Keys; typeParams.Has(var)};
+ return subst; + }
+#else
+ /// <summary>
+ /// like Type.CheckArgumentTypes, but assumes no errors
+ /// (and only does arguments, not results; and takes actuals as TypeSeq, not ExprSeq)
+ /// </summary>
+ public static IDictionary<TypeVariable!, Type!>!
+ InferTypeParameters(TypeVariableSeq! typeParams,
+ TypeSeq! formalArgs,
+ TypeSeq! actualArgs)
+ requires formalArgs.Length == actualArgs.Length;
+ {
+ TypeSeq proxies = new TypeSeq();
+ Dictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!>();
+ foreach (TypeVariable! tv in typeParams) {
+ TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name);
+ proxies.Add(proxy);
+ subst.Add(tv, proxy);
+ }
+
+ for (int i = 0; i < formalArgs.Length; 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
+ assert forall{TypeVariable! var in typeParams; !actual.FreeVariables.Has(var)};
+
+ if (!formal.Unify(actual)) {
+ assume false; // caller expected no errors
+ }
+ }
+
+ return subst;
+ }
+#endif
+
+ //----------- Helper methods to deal with bound type variables ---------------
+
+ public static void EmitOptionalTypeParams(TokenTextWriter! stream, TypeVariableSeq! typeParams) {
+ if (typeParams.Length > 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 TypeVariableSeq! SortTypeParams(TypeVariableSeq! typeParams,
+ TypeSeq! argumentTypes, Type resultType)
+ ensures result.Length == typeParams.Length; {
+ if (typeParams.Length == 0) {
+ return typeParams;
+ }
+
+ TypeVariableSeq 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":
+ TypeVariableSeq! sortedTypeParams = new TypeVariableSeq ();
+ foreach (TypeVariable! var in freeVarsInUse) {
+ if (typeParams.Has(var)) {
+ sortedTypeParams.Add(var);
+ }
+ }
+
+ if (sortedTypeParams.Length < typeParams.Length)
+ // 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(TypeVariableSeq! typeParams,
+ TypeSeq! argumentTypes,
+ TypeSeq moreArgumentTypes,
+ IToken! resolutionSubject,
+ string! subjectName,
+ ResolutionContext! rc) {
+ TypeVariableSeq freeVarsInArgs = FreeVariablesIn(argumentTypes);
+ TypeVariableSeq moFreeVarsInArgs = moreArgumentTypes == null ? null : FreeVariablesIn(moreArgumentTypes);
+ bool someTypeParamsAppearOnlyAmongMo = false;
+ foreach (TypeVariable! var in typeParams) {
+ if (rc.LookUpTypeBinder(var.Name) == var) // avoid to complain twice about variables that are bound multiple times
+ {
+ if (freeVarsInArgs.Has(var)) {
+ // cool
+ } else if (moFreeVarsInArgs != null && moFreeVarsInArgs.Has(var)) {
+ someTypeParamsAppearOnlyAmongMo = true;
+ } else {
+ rc.Error(resolutionSubject,
+ "type variable must occur in {0}: {1}",
+ subjectName, var);
+ }
+ }
+ }
+ return someTypeParamsAppearOnlyAmongMo;
+ }
+
+ [Pure]
+ public static TypeVariableSeq! FreeVariablesIn(TypeSeq! arguments) {
+ TypeVariableSeq! res = new TypeVariableSeq ();
+ foreach (Type! t in arguments)
+ res.AppendWithoutDups(t.FreeVariables);
+ return res;
+ }
+ }
+
+ //=====================================================================
+
+ public class BasicType : Type
+ {
+ public readonly SimpleType T;
+ public BasicType(IToken! token, SimpleType t)
+ : base(token)
+ {
+ T = t;
+ // base(token);
+ }
+ public BasicType(SimpleType t)
+ : base(Token.NoToken)
+ {
+ T = t;
+ // base(Token.NoToken);
+ }
+
+ //----------- 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<TypeVariable!, TypeVariable!>! varMap) {
+ // BasicTypes are immutable anyway, we do not clone
+ return this;
+ }
+
+ public override Type! CloneUnresolved() {
+ return this;
+ }
+
+ //----------- Linearisation ----------------------------------
+
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
+ {
+ // no parentheses are necessary for basic types
+ stream.SetToken(this);
+ stream.Write("{0}", this);
+ }
+
+ [Pure]
+ public override string! ToString()
+ {
+ switch (T)
+ {
+ case SimpleType.Int: return "int";
+ case SimpleType.Bool: return "bool";
+ }
+ Debug.Assert(false, "bad type " + T);
+ assert false; // 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,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables) {
+ return this.Equals(that);
+ }
+
+ //----------- Unification of types -----------
+
+ public override bool Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ // an idempotent substitution that describes the
+ // unification result up to a certain point
+ IDictionary<TypeVariable!, Type!>! 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,
+ TypeVariableSeq! unifiableVariables,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables,
+ IDictionary<TypeVariable!, Type!>! 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<TypeVariable!, Type!>! subst) {
+ return this;
+ }
+
+ //----------- Hashcodes ----------------------------------
+
+ [Pure]
+ public override int GetHashCode(TypeVariableSeq! boundVariables)
+ {
+ return this.T.GetHashCode();
+ }
+
+ //----------- Resolution ----------------------------------
+
+ public override Type! ResolveType(ResolutionContext! rc) {
+ // nothing to resolve
+ return this;
+ }
+
+ // determine the free variables in a type, in the order in which the variables occur
+ public override TypeVariableSeq! FreeVariables {
+ get {
+ return new TypeVariableSeq (); // basic type are closed
+ }
+ }
+
+ public override List<TypeProxy!>! FreeProxies { get {
+ return new List<TypeProxy!> ();
+ } }
+
+ //----------- Getters/Issers ----------------------------------
+
+ public override bool IsBasic { get { return true; } }
+ public override bool IsInt { get { return this.T == SimpleType.Int; } }
+ public override bool IsBool { get { return this.T == SimpleType.Bool; } }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitBasicType(this);
+ }
+ }
+
+ //=====================================================================
+
+ public class BvType : Type
+ {
+ public readonly int Bits;
+
+ public BvType(IToken! token, int bits)
+ : base(token)
+ {
+ 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<TypeVariable!, TypeVariable!>! varMap) {
+ // BvTypes are immutable anyway, we do not clone
+ return this;
+ }
+
+ public override Type! CloneUnresolved() {
+ return this;
+ }
+
+ //----------- Linearisation ----------------------------------
+
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
+ {
+ // no parentheses are necessary for bitvector-types
+ stream.SetToken(this);
+ stream.Write("{0}", this);
+ }
+
+ [Pure]
+ public override string! ToString()
+ {
+ return "bv" + Bits;
+ }
+
+ //----------- Equality ----------------------------------
+
+ [Pure]
+ public override bool Equals(Type! that,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables) {
+ BvType thatBvType = TypeProxy.FollowProxy(that.Expanded) as BvType;
+ return thatBvType != null && this.Bits == thatBvType.Bits;
+ }
+
+ //----------- Unification of types -----------
+
+ public override bool Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ // an idempotent substitution that describes the
+ // unification result up to a certain point
+ IDictionary<TypeVariable!, Type!>! 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,
+ TypeVariableSeq! unifiableVariables,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables,
+ IDictionary<TypeVariable!, Type!>! 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<TypeVariable!, Type!>! subst) {
+ return this;
+ }
+
+ //----------- Hashcodes ----------------------------------
+
+ [Pure]
+ public override int GetHashCode(TypeVariableSeq! boundVariables)
+ {
+ return this.Bits.GetHashCode();
+ }
+
+ //----------- Resolution ----------------------------------
+
+ public override Type! ResolveType(ResolutionContext! rc) {
+ // nothing to resolve
+ return this;
+ }
+
+ // determine the free variables in a type, in the order in which the variables occur
+ public override TypeVariableSeq! FreeVariables {
+ get {
+ return new TypeVariableSeq (); // bitvector-type are closed
+ }
+ }
+
+ public override List<TypeProxy!>! FreeProxies { get {
+ return new List<TypeProxy!> ();
+ } }
+
+ //----------- Getters/Issers ----------------------------------
+
+ public override bool IsBv { get { return true; } }
+ public override int BvBits { get {
+ return Bits;
+ } }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ 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 TypeSeq! Arguments;
+
+ public UnresolvedTypeIdentifier(IToken! token, string! name) {
+ this(token, name, new TypeSeq ());
+ }
+
+ public UnresolvedTypeIdentifier(IToken! token, string! name, TypeSeq! arguments)
+ : base(token)
+ {
+ 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<TypeVariable!, TypeVariable!>! varMap) {
+ TypeSeq! newArgs = new TypeSeq ();
+ foreach(Type! t in Arguments)
+ newArgs.Add(t.Clone(varMap));
+ return new UnresolvedTypeIdentifier(tok, Name, newArgs);
+ }
+
+ public override Type! CloneUnresolved() {
+ TypeSeq! newArgs = new TypeSeq ();
+ foreach(Type! t in Arguments)
+ newArgs.Add(t.CloneUnresolved());
+ return new UnresolvedTypeIdentifier(tok, Name, newArgs);
+ }
+
+ //----------- Equality ----------------------------------
+
+ [Pure]
+ public override bool Equals(Type! that,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables) {
+ 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,
+ TypeVariableSeq! unifiableVariables,
+ IDictionary<TypeVariable!, Type!>! result) {
+ assert false; // UnresolvedTypeIdentifier.Unify should never be called
+ }
+
+#if OLD_UNIFICATION
+ public override void Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables,
+ IDictionary<TypeVariable!, Type!>! result) {
+ 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<TypeVariable!, Type!>! subst) {
+ assert false; // UnresolvedTypeIdentifier.Substitute should never be called
+ }
+
+ //----------- Hashcodes ----------------------------------
+
+ [Pure]
+ public override int GetHashCode(TypeVariableSeq! boundVariables) {
+ assert false; // UnresolvedTypeIdentifier.GetHashCode should never be called
+ }
+
+ //----------- Resolution ----------------------------------
+
+ public override Type! ResolveType(ResolutionContext! rc) {
+ // 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.Length > 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.Length > 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.Length != 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.Length != synDecl.TypeParameters.Length) {
+ rc.Error(this,
+ "type synonym received wrong number of arguments: {0}",
+ synDecl);
+ return this;
+ }
+ TypeSeq! resolvedArgs = ResolveArguments(rc);
+
+
+ return new TypeSynonymAnnotation(this.tok, synDecl, resolvedArgs);
+
+ }
+
+ // otherwise: this name is not declared anywhere
+ rc.Error(this, "undeclared type: {0}", Name);
+ return this;
+ }
+
+ private TypeSeq! ResolveArguments(ResolutionContext! rc) {
+ TypeSeq! resolvedArgs = new TypeSeq ();
+ foreach (Type! t in Arguments)
+ resolvedArgs.Add(t.ResolveType(rc));
+ return resolvedArgs;
+ }
+
+ public override TypeVariableSeq! FreeVariables {
+ get {
+ return new TypeVariableSeq ();
+ }
+ }
+
+ public override List<TypeProxy!>! FreeProxies { get {
+ return new List<TypeProxy!> ();
+ } }
+
+ //----------- Linearisation ----------------------------------
+
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
+ {
+ 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 { return this; } }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitUnresolvedTypeIdentifier(this);
+ }
+ }
+
+ //=====================================================================
+
+ public class TypeVariable : Type {
+ public readonly string! Name;
+
+ public TypeVariable(IToken! token, string! name)
+ : base(token)
+ {
+ 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<TypeVariable!, TypeVariable!>! varMap) {
+ // 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() {
+ return this;
+ }
+
+ //----------- Equality ----------------------------------
+
+ [Pure]
+ public override bool Equals(Type! that,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables) {
+ 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,
+ TypeVariableSeq! unifiableVariables,
+ // an idempotent substitution that describes the
+ // unification result up to a certain point
+ IDictionary<TypeVariable!, Type!>! 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.Has(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.Has(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<TypeVariable!, Type!>! oldSolution,
+ // the type that "this" is instantiated with
+ Type! newSubst)
+ requires !oldSolution.ContainsKey(this); {
+
+ Dictionary<TypeVariable!, Type!>! newMapping = new Dictionary<TypeVariable!, Type!> ();
+ // apply the old (idempotent) substitution to the new instantiation
+ Type! substSubst = newSubst.Substitute(oldSolution);
+ // occurs check
+ if (substSubst.FreeVariables.Has(this))
+ return false;
+ newMapping.Add(this, substSubst);
+
+ // apply the new substitution to the old ones to ensure idempotence
+ List<TypeVariable!>! keys = new List<TypeVariable!> ();
+ keys.AddRange(oldSolution.Keys);
+ foreach (TypeVariable! var in keys)
+ oldSolution[var] = oldSolution[var].Substitute(newMapping);
+ oldSolution.Add(this, substSubst);
+
+ assert IsIdempotent(oldSolution);
+ return true;
+ }
+
+#if OLD_UNIFICATION
+ public override void Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables,
+ IDictionary<TypeVariable!, Type!>! result) {
+ 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
+ TypeVariableSeq! thatFreeVars = that.FreeVariables;
+ if (exists{TypeVariable! var in thatBoundVariables; 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<TypeVariable!, Type!>! subst) {
+ Type res;
+ if (subst.TryGetValue(this, out res)) {
+ assert res != null;
+ return res;
+ } else {
+ return this;
+ }
+ }
+
+ //----------- Hashcodes ----------------------------------
+
+ [Pure]
+ public override int GetHashCode(TypeVariableSeq! boundVariables) {
+ int thisIndex = boundVariables.LastIndexOf(this);
+ if (thisIndex == -1)
+ return GetBaseHashCode();
+ return thisIndex * 27473671;
+ }
+
+ //----------- Linearisation ----------------------------------
+
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
+ {
+ // never put parentheses around variables
+ stream.SetToken(this);
+ stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(this.Name));
+ }
+
+ //----------- Resolution ----------------------------------
+
+ public override Type! ResolveType(ResolutionContext! rc) {
+ // nothing to resolve
+ return this;
+ }
+
+ public override TypeVariableSeq! FreeVariables {
+ get { return new TypeVariableSeq(this); }
+ }
+
+ public override List<TypeProxy!>! FreeProxies { get {
+ return new List<TypeProxy!> ();
+ } }
+
+ //----------- Getters/Issers ----------------------------------
+
+ public override bool IsVariable { get { return true; } }
+ public override TypeVariable! AsVariable { get { return this; } }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitTypeVariable(this);
+ }
+ }
+
+ //=====================================================================
+
+ public class TypeProxy : Type {
+ static int proxies = 0;
+ protected readonly string! Name;
+
+ public TypeProxy(IToken! token, string! givenName)
+ {
+ this(token, givenName, "proxy");
+ }
+
+ protected TypeProxy(IToken! token, string! givenName, string! kind)
+ {
+ Name = givenName + "$" + kind + "#" + proxies;
+ proxies++;
+ base(token);
+ }
+
+ 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;
+ assert proxyFor != null;
+ }
+ return proxyFor;
+ }
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Everything)]
+ public static Type! FollowProxy(Type! t)
+ ensures result is TypeProxy ==> ((TypeProxy)result).proxyFor == null;
+ {
+ if (t is TypeProxy) {
+ Type p = ((TypeProxy)t).ProxyFor;
+ if (p != null) {
+ return p;
+ }
+ }
+ return t;
+ }
+
+ protected void DefineProxy(Type! ty)
+ 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<TypeVariable!, TypeVariable!>! varMap) {
+ 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<n>$proxy<m>
+ }
+ }
+
+ public override Type! CloneUnresolved() {
+ return new TypeProxy(this.tok, this.Name); // the clone will have a name that ends with $proxy<n>$proxy<m>
+ }
+
+ //----------- Equality ----------------------------------
+
+ [Pure]
+ public override bool Equals(Type! that,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables) {
+ 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) {
+ that = FollowProxy(that.Expanded);
+ return that.FreeProxies.Contains(this) &&
+ (that.IsCtor || that.IsMap && this != that && this.ProxyFor != that);
+ }
+
+ public override bool Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ IDictionary<TypeVariable!, Type!>! result) {
+ 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<TypeVariable!, Type!>! subst) {
+ Type p = ProxyFor;
+ if (p != null) {
+ return p.Substitute(subst);
+ } else {
+ return this;
+ }
+ }
+
+ //----------- Hashcodes ----------------------------------
+
+ [Pure]
+ public override int GetHashCode(TypeVariableSeq! boundVariables) {
+ Type p = ProxyFor;
+ if (p != null) {
+ return p.GetHashCode(boundVariables);
+ } else {
+ return GetBaseHashCode();
+ }
+ }
+
+ //----------- Linearisation ----------------------------------
+
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
+ {
+ 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) {
+ Type p = ProxyFor;
+ if (p != null) {
+ return p.ResolveType(rc);
+ } else {
+ return this;
+ }
+ }
+
+ public override TypeVariableSeq! FreeVariables {
+ get {
+ Type p = ProxyFor;
+ if (p != null) {
+ return p.FreeVariables;
+ } else {
+ return new TypeVariableSeq();
+ }
+ }
+ }
+
+ public override List<TypeProxy!>! FreeProxies { get {
+ Type p = ProxyFor;
+ if (p != null) {
+ return p.FreeProxies;
+ } else {
+ List<TypeProxy!>! res = new List<TypeProxy!> ();
+ 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 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 {
+ Type p = ProxyFor;
+ assume p != null;
+ return p.AsVariable;
+ } }
+
+ public override bool IsCtor { get {
+ Type p = ProxyFor;
+ return p != null && p.IsCtor;
+ } }
+ public override CtorType! AsCtor { get {
+ Type p = ProxyFor;
+ assume p != null;
+ return p.AsCtor;
+ } }
+ public override bool IsMap { get {
+ Type p = ProxyFor;
+ return p != null && p.IsMap;
+ } }
+ public override MapType! AsMap { get {
+ Type p = ProxyFor;
+ assume p != null;
+ return p.AsMap;
+ } }
+ public override int MapArity { get {
+ Type p = ProxyFor;
+ assume p != null;
+ return p.MapArity;
+ } }
+ public override bool IsUnresolved { get {
+ Type p = ProxyFor;
+ return p != null && p.IsUnresolved;
+ } }
+ public override UnresolvedTypeIdentifier! AsUnresolved { get {
+ Type p = ProxyFor;
+ 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;
+ assume p != null;
+ return p.BvBits;
+ } }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitTypeProxy(this);
+ }
+ }
+
+ public abstract class ConstrainedProxy : TypeProxy {
+ protected ConstrainedProxy(IToken! token, string! givenName, string! kind) {
+ base(token, givenName, kind);
+ }
+ }
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ public class BvTypeProxy : ConstrainedProxy {
+ public int MinBits;
+ List<BvTypeConstraint!> constraints;
+ class BvTypeConstraint {
+ public Type! T0;
+ public Type! T1;
+ public BvTypeConstraint(Type! t0, Type! t1)
+ requires t0.IsBv && t1.IsBv;
+ {
+ T0 = t0;
+ T1 = t1;
+ }
+ }
+
+ public BvTypeProxy(IToken! token, string! name, int minBits)
+ {
+ base(token, name, "bv" + minBits + "proxy");
+ this.MinBits = minBits;
+ }
+
+ /// <summary>
+ /// Requires that any further constraints to be placed on t0 and t1 go via the object to
+ /// be constructed.
+ /// </summary>
+ public BvTypeProxy(IToken! token, string! name, Type! t0, Type! t1)
+ requires t0.IsBv && t1.IsBv;
+ {
+ base(token, name, "bvproxy");
+ t0 = FollowProxy(t0);
+ t1 = FollowProxy(t1);
+ this.MinBits = MinBitsFor(t0) + MinBitsFor(t1);
+ List<BvTypeConstraint!> list = new List<BvTypeConstraint!>();
+ list.Add(new BvTypeConstraint(t0, t1));
+ this.constraints = list;
+ }
+
+ /// <summary>
+ /// Construct a BvTypeProxy like p, but with minBits.
+ /// </summary>
+ private BvTypeProxy(BvTypeProxy! p, int minBits)
+ {
+ base(p.tok, p.Name, "");
+ this.MinBits = minBits;
+ this.constraints = p.constraints;
+ }
+
+ private BvTypeProxy(IToken! token, string! name, int minBits, List<BvTypeConstraint!> constraints) {
+ base(token, name, "");
+ this.MinBits = minBits;
+ this.constraints = constraints;
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Everything)]
+ private static int MinBitsFor(Type! t)
+ requires t.IsBv;
+ ensures 0 <= result;
+ {
+ if (t is BvType) {
+ return t.BvBits;
+ } else {
+ return ((BvTypeProxy)t).MinBits;
+ }
+ }
+
+ //----------- Cloning ----------------------------------
+
+ public override Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
+ 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<n>$bvproxy<m>
+ }
+ }
+
+ public override Type! CloneUnresolved() {
+ return new BvTypeProxy(this.tok, this.Name, this.MinBits, this.constraints); // the clone will have a name that ends with $bvproxy<n>$bvproxy<m>
+ }
+
+ //----------- Unification of types -----------
+
+ public override bool Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ IDictionary<TypeVariable!, Type!>! 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.Has(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);
+ 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<BvTypeConstraint!> list = new List<BvTypeConstraint!>();
+ if (this.constraints != null) { list.AddRange(this.constraints); }
+ if (bt.constraints != null) { list.AddRange(bt.constraints); }
+ BvTypeProxy np = new BvTypeProxy(this.tok, this.Name, 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)
+ requires t.IsBv && 0 <= to && MinBitsFor(t) <= to;
+ ensures 0 <= result && result <= to;
+ {
+ t = FollowProxy(t);
+ if (t is BvType) {
+ return to - t.BvBits;
+ } else {
+ BvTypeProxy p = (BvTypeProxy)t;
+ 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<TypeVariable!, Type!>! subst) {
+ 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)
+ assert forall{BvTypeConstraint! c in constraints;
+ forall{TypeVariable! var in subst.Keys;
+ !c.T0.FreeVariables.Has(var) && !c.T1.FreeVariables.Has(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)
+ {
+ 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<Constraint>! constraints = new List<Constraint> ();
+
+ // 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 TypeSeq! Arguments;
+ public readonly Type! Result;
+
+ public Constraint(TypeSeq! arguments, Type! result) {
+ Arguments = arguments;
+ Result = result;
+ }
+
+ public Constraint Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
+ TypeSeq! args = new TypeSeq ();
+ foreach (Type! t in Arguments)
+ args.Add(t.Clone(varMap));
+ Type! res = Result.Clone(varMap);
+ return new Constraint(args, res);
+ }
+
+ public bool Unify(MapType! that,
+ TypeVariableSeq! unifiableVariables,
+ IDictionary<TypeVariable!, Type!>! result)
+ requires Arguments.Length == that.Arguments.Length; {
+ Dictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!>();
+ foreach (TypeVariable! tv in that.TypeParameters) {
+ TypeProxy proxy = new TypeProxy(Token.NoToken, tv.Name);
+ subst.Add(tv, proxy);
+ }
+
+ bool good = true;
+ for (int i = 0; i < that.Arguments.Length; 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)
+ requires 0 <= arity; {
+ base(token, name, "mapproxy");
+ this.Arity = arity;
+ }
+
+ private void AddConstraint(Constraint c)
+ requires c.Arguments.Length == Arity; {
+
+ Type f = ProxyFor;
+ MapType mf = f as MapType;
+ if (mf != null) {
+ bool success = c.Unify(mf, new TypeVariableSeq(), new Dictionary<TypeVariable!, Type!> ());
+ assert success;
+ return;
+ }
+
+ MapTypeProxy mpf = f as MapTypeProxy;
+ if (mpf != null) {
+ mpf.AddConstraint(c);
+ return;
+ }
+
+ assert f == null; // no other types should occur as specialisations of this proxy
+
+ constraints.Add(c);
+ }
+
+ public Type CheckArgumentTypes(ExprSeq! actualArgs,
+ out TypeParamInstantiation! tpInstantiation,
+ IToken! typeCheckingSubject,
+ string! opName,
+ TypecheckingContext! tc)
+ {
+ 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);
+
+ 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
+ TypeSeq! arguments = new TypeSeq ();
+ foreach (Expr! e in actualArgs)
+ arguments.Add(e.Type);
+ Type! result = new TypeProxy (tok, "result");
+ AddConstraint(new Constraint (arguments, result));
+
+ TypeSeq! argumentsResult = new TypeSeq ();
+ foreach (Expr! e in actualArgs)
+ argumentsResult.Add(e.Type);
+ argumentsResult.Add(result);
+
+ tpInstantiation = new MapTypeProxyParamInstantiation(this, argumentsResult);
+ return result;
+ }
+
+ //----------- Cloning ----------------------------------
+
+ public override Type! Clone(IDictionary<TypeVariable!, TypeVariable!>! varMap) {
+ 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<n>$mapproxy<m> (hopefully)
+ }
+ }
+
+ //----------- Linearisation ----------------------------------
+
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
+ {
+ 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,
+ TypeVariableSeq! unifiableVariables,
+ IDictionary<TypeVariable!, Type!>! 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.Has(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.Length == 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<TypeVariable!, Type!>! subst) {
+ 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)
+ assert forall{Constraint c in constraints;
+ forall{TypeVariable! var in subst.Keys;
+ forall{Type! t in c.Arguments; !t.FreeVariables.Has(var)} &&
+ !c.Result.FreeVariables.Has(var)}};
+ }
+ return base.Substitute(subst);
+ }
+
+ //----------- Getters/Issers ----------------------------------
+
+ public override bool IsMap { get { return true; } }
+ public override MapType! AsMap { get {
+ Type p = ProxyFor;
+ if (p != null) {
+ return p.AsMap;
+ } else {
+ assert false; // what to do now?
+ }
+ } }
+ public override int MapArity { get {
+ return Arity;
+ } }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ 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 TypeSeq! Arguments;
+ // is set during resolution and determines whether the right number of arguments is given
+ public readonly TypeSynonymDecl! Decl;
+
+ public TypeSynonymAnnotation(IToken! token, TypeSynonymDecl! decl, TypeSeq! arguments)
+ : base(token)
+ requires arguments.Length == decl.TypeParameters.Length;
+ {
+ this.Decl = decl;
+ this.Arguments = arguments;
+
+ // build a substitution that can be applied to the definition of
+ // the type synonym
+ IDictionary<TypeVariable!, Type!>! subst =
+ new Dictionary<TypeVariable!, Type!> ();
+ for (int i = 0; i < arguments.Length; ++i)
+ subst.Add(decl.TypeParameters[i], arguments[i]);
+
+ ExpandedType = decl.Body.Substitute(subst);
+ }
+
+ private TypeSynonymAnnotation(IToken! token, TypeSynonymDecl! decl, TypeSeq! arguments,
+ Type! expandedType)
+ : base(token) {
+ 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<TypeVariable!, TypeVariable!>! varMap) {
+ TypeSeq! newArgs = new TypeSeq ();
+ foreach(Type! t in Arguments)
+ newArgs.Add(t.Clone(varMap));
+ Type! newExpandedType = ExpandedType.Clone(varMap);
+ return new TypeSynonymAnnotation(tok, Decl, newArgs, newExpandedType);
+ }
+
+ public override Type! CloneUnresolved() {
+ TypeSeq! newArgs = new TypeSeq ();
+ foreach(Type! t in Arguments)
+ newArgs.Add(t.CloneUnresolved());
+ return new TypeSynonymAnnotation(tok, Decl, newArgs);
+ }
+
+ //----------- Equality ----------------------------------
+
+ [Pure]
+ public override bool Equals(Type! that,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables) {
+ return ExpandedType.Equals(that, thisBoundVariables, thatBoundVariables);
+ }
+
+ // used to skip leading type annotations
+ internal override Type! Expanded { get {
+ return ExpandedType.Expanded;
+ } }
+
+ //----------- Unification of types -----------
+
+ public override bool Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ IDictionary<TypeVariable!, Type!>! result) {
+ return ExpandedType.Unify(that, unifiableVariables, result);
+ }
+
+#if OLD_UNIFICATION
+ public override void Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables,
+ IDictionary<TypeVariable!, Type!>! result) {
+ ExpandedType.Unify(that, unifiableVariables,
+ thisBoundVariables, thatBoundVariables, result);
+ }
+#endif
+
+ //----------- Substitution of free variables with types not containing bound variables -----------------
+
+ public override Type! Substitute(IDictionary<TypeVariable!, Type!>! subst) {
+ if (subst.Count == 0)
+ return this;
+ TypeSeq newArgs = new TypeSeq ();
+ foreach (Type! t in Arguments)
+ newArgs.Add(t.Substitute(subst));
+ Type! newExpandedType = ExpandedType.Substitute(subst);
+ return new TypeSynonymAnnotation(tok, Decl, newArgs, newExpandedType);
+ }
+
+ //----------- Hashcodes ----------------------------------
+
+ [Pure]
+ public override int GetHashCode(TypeVariableSeq! boundVariables) {
+ return ExpandedType.GetHashCode(boundVariables);
+ }
+
+ //----------- Linearisation ----------------------------------
+
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
+ {
+ stream.SetToken(this);
+ CtorType.EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength);
+ }
+
+ //----------- Resolution ----------------------------------
+
+ public override Type! ResolveType(ResolutionContext! rc) {
+ TypeSeq resolvedArgs = new TypeSeq ();
+ foreach (Type! t in Arguments)
+ resolvedArgs.Add(t.ResolveType(rc));
+ return new TypeSynonymAnnotation(tok, Decl, resolvedArgs);
+ }
+
+ public override TypeVariableSeq! FreeVariables { get {
+ return ExpandedType.FreeVariables;
+ } }
+
+ public override List<TypeProxy!>! FreeProxies { get {
+ return ExpandedType.FreeProxies;
+ } }
+
+ //----------- Getters/Issers ----------------------------------
+
+ public override bool IsBasic { get { return ExpandedType.IsBasic; } }
+ public override bool IsInt { get { return ExpandedType.IsInt; } }
+ public override bool IsBool { get { return ExpandedType.IsBool; } }
+
+ public override bool IsVariable { get { return ExpandedType.IsVariable; } }
+ public override TypeVariable! AsVariable { get { return ExpandedType.AsVariable; } }
+ public override bool IsCtor { get { return ExpandedType.IsCtor; } }
+ public override CtorType! AsCtor { get { return ExpandedType.AsCtor; } }
+ public override bool IsMap { get { return ExpandedType.IsMap; } }
+ public override MapType! AsMap { get { return ExpandedType.AsMap; } }
+ public override bool IsUnresolved { get { return ExpandedType.IsUnresolved; } }
+ public override UnresolvedTypeIdentifier! AsUnresolved { get {
+ 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)
+ {
+ return visitor.VisitTypeSynonymAnnotation(this);
+ }
+ }
+
+ //=====================================================================
+
+ public class CtorType : Type {
+ public readonly TypeSeq! Arguments;
+ // is set during resolution and determines whether the right number of arguments is given
+ public readonly TypeCtorDecl! Decl;
+
+ public CtorType(IToken! token, TypeCtorDecl! decl, TypeSeq! arguments)
+ : base(token)
+ requires arguments.Length == decl.Arity;
+ {
+ this.Decl = decl;
+ 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<TypeVariable!, TypeVariable!>! varMap) {
+ TypeSeq! newArgs = new TypeSeq ();
+ foreach(Type! t in Arguments)
+ newArgs.Add(t.Clone(varMap));
+ return new CtorType(tok, Decl, newArgs);
+ }
+
+ public override Type! CloneUnresolved() {
+ TypeSeq! newArgs = new TypeSeq ();
+ foreach(Type! t in Arguments)
+ 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.Length == 0)
+ return true;
+ return base.Equals(thatType);
+ }
+
+ [Pure]
+ public override bool Equals(Type! that,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! 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.Length; ++i) {
+ if (!Arguments[i].Equals(thatCtorType.Arguments[i],
+ thisBoundVariables, thatBoundVariables))
+ return false;
+ }
+ return true;
+ }
+
+ //----------- Unification of types -----------
+
+ public override bool Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ IDictionary<TypeVariable!, Type!>! 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.Length; ++i)
+ good &= Arguments[i].Unify(thatCtorType.Arguments[i], unifiableVariables, result);
+ return good;
+ }
+ }
+
+#if OLD_UNIFICATION
+ public override void Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables,
+ IDictionary<TypeVariable!, Type!>! 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<TypeVariable!, Type!>! subst) {
+ if (subst.Count == 0)
+ return this;
+ TypeSeq newArgs = new TypeSeq ();
+ foreach (Type! t in Arguments)
+ newArgs.Add(t.Substitute(subst));
+ return new CtorType(tok, Decl, newArgs);
+ }
+
+ //----------- Hashcodes ----------------------------------
+
+ [Pure]
+ public override int GetHashCode(TypeVariableSeq! boundVariables) {
+ int res = 1637643879 * Decl.GetHashCode();
+ foreach (Type! t in Arguments)
+ res = res * 3 + t.GetHashCode(boundVariables);
+ return res;
+ }
+
+ //----------- Linearisation ----------------------------------
+
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
+ {
+ stream.SetToken(this);
+ EmitCtorType(this.Decl.Name, Arguments, stream, contextBindingStrength);
+ }
+
+ internal static void EmitCtorType(string! name, TypeSeq! args, TokenTextWriter! stream, int contextBindingStrength) {
+ int opBindingStrength = args.Length > 0 ? 0 : 2;
+ if (opBindingStrength < contextBindingStrength)
+ stream.Write("(");
+
+ stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(name));
+ int i = args.Length;
+ foreach (Type! t in args) {
+ 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) {
+ TypeSeq resolvedArgs = new TypeSeq ();
+ foreach (Type! t in Arguments)
+ resolvedArgs.Add(t.ResolveType(rc));
+ return new CtorType(tok, Decl, resolvedArgs);
+ }
+
+ public override TypeVariableSeq! FreeVariables {
+ get {
+ TypeVariableSeq! res = new TypeVariableSeq ();
+ foreach (Type! t in Arguments)
+ res.AppendWithoutDups(t.FreeVariables);
+ return res;
+ }
+ }
+
+ public override List<TypeProxy!>! FreeProxies { get {
+ List<TypeProxy!>! res = new List<TypeProxy!> ();
+ foreach (Type! t in Arguments)
+ 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)
+ {
+ 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 TypeVariableSeq! TypeParameters;
+ public readonly TypeSeq! Arguments;
+ public Type! Result;
+
+ public MapType(IToken! token, TypeVariableSeq! typeParameters, TypeSeq! arguments, Type! result)
+ : base(token)
+ {
+ 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<TypeVariable!, TypeVariable!>! varMap) {
+ IDictionary<TypeVariable!, TypeVariable!>! newVarMap =
+ new Dictionary<TypeVariable!, TypeVariable!>();
+ foreach (KeyValuePair<TypeVariable!, TypeVariable!> p in varMap) {
+ if (!TypeParameters.Has(p.Key))
+ newVarMap.Add(p);
+ }
+
+ TypeVariableSeq! newTypeParams = new TypeVariableSeq ();
+ foreach (TypeVariable! var in TypeParameters) {
+ TypeVariable! newVar = new TypeVariable (var.tok, var.Name);
+ newVarMap.Add(var, newVar);
+ newTypeParams.Add(newVar);
+ }
+
+ TypeSeq! newArgs = new TypeSeq ();
+ foreach(Type! t in Arguments)
+ newArgs.Add(t.Clone(newVarMap));
+ Type! newResult = Result.Clone(newVarMap);
+
+ return new MapType (this.tok, newTypeParams, newArgs, newResult);
+ }
+
+ public override Type! CloneUnresolved() {
+ TypeVariableSeq! newTypeParams = new TypeVariableSeq ();
+ foreach (TypeVariable! var in TypeParameters) {
+ TypeVariable! newVar = new TypeVariable (var.tok, var.Name);
+ newTypeParams.Add(newVar);
+ }
+
+ TypeSeq! newArgs = new TypeSeq ();
+ foreach(Type! t in Arguments)
+ newArgs.Add(t.CloneUnresolved());
+ Type! newResult = Result.CloneUnresolved();
+
+ return new MapType (this.tok, newTypeParams, newArgs, newResult);
+ }
+
+ //----------- Equality ----------------------------------
+
+ [Pure]
+ public override bool Equals(Type! that,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables) {
+ that = TypeProxy.FollowProxy(that.Expanded);
+ MapType thatMapType = that as MapType;
+ if (thatMapType == null ||
+ this.TypeParameters.Length != thatMapType.TypeParameters.Length ||
+ this.Arguments.Length != thatMapType.Arguments.Length)
+ return false;
+
+ foreach (TypeVariable! var in this.TypeParameters)
+ thisBoundVariables.Add(var);
+ foreach (TypeVariable! var in thatMapType.TypeParameters)
+ thatBoundVariables.Add(var);
+
+ try {
+
+ for (int i = 0; i < Arguments.Length; ++i) {
+ if (!Arguments[i].Equals(thatMapType.Arguments[i],
+ thisBoundVariables, thatBoundVariables))
+ return false;
+ }
+ if (!this.Result.Equals(thatMapType.Result,
+ thisBoundVariables, thatBoundVariables))
+ return false;
+
+ } finally {
+ // make sure that the bound variables are removed again
+ for (int i = 0; i < this.TypeParameters.Length; ++i) {
+ thisBoundVariables.Remove();
+ thatBoundVariables.Remove();
+ }
+ }
+
+ return true;
+ }
+
+ //----------- Unification of types -----------
+
+ public override bool Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ IDictionary<TypeVariable!, Type!>! 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.Length != thatMapType.TypeParameters.Length ||
+ this.Arguments.Length != thatMapType.Arguments.Length)
+ return false;
+
+ // treat the bound variables of the two map types as equal...
+ Dictionary<TypeVariable!, Type!>! subst0 = new Dictionary<TypeVariable!, Type!>();
+ Dictionary<TypeVariable!, Type!>! subst1 = new Dictionary<TypeVariable!, Type!>();
+ TypeVariableSeq freshies = new TypeVariableSeq();
+ for (int i = 0; i < this.TypeParameters.Length; 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.Length; 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.Length != 0) {
+ // This is done by looking for occurrences of the fresh variables in the
+ // non-substituted types ...
+ TypeVariableSeq freeVars = this.FreeVariables;
+ foreach (TypeVariable fr in freshies)
+ if (freeVars.Has(fr)) { return false; } // fresh variable escaped
+ freeVars = thatMapType.FreeVariables;
+ foreach (TypeVariable fr in freshies)
+ if (freeVars.Has(fr)) { return false; } // fresh variable escaped
+
+ // ... and in the resulting unifier of type variables
+ foreach (KeyValuePair<TypeVariable!, Type!> pair in result) {
+ freeVars = pair.Value.FreeVariables;
+ foreach (TypeVariable fr in freshies)
+ if (freeVars.Has(fr)) { return false; } // fresh variable escaped
+ }
+ }
+
+ return good;
+ }
+
+#if OLD_UNIFICATION
+ public override void Unify(Type! that,
+ TypeVariableSeq! unifiableVariables,
+ TypeVariableSeq! thisBoundVariables,
+ TypeVariableSeq! thatBoundVariables,
+ IDictionary<TypeVariable!, Type!>! 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)
+ thisBoundVariables.Add(var);
+ foreach (TypeVariable! var in thatMapType.TypeParameters)
+ 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<TypeVariable!, Type!>! subst) {
+ // PR: could be written more efficiently
+ return exists{TypeVariable! var in TypeParameters;
+ subst.ContainsKey(var) ||
+ exists{Type! t in subst.Values; t.FreeVariables.Has(var)}};
+ }
+
+ public override Type! Substitute(IDictionary<TypeVariable!, Type!>! subst) {
+ 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();
+ assert newType.Equals(this) && !newType.collisionsPossible(subst);
+ return newType.Substitute(subst);
+ }
+
+ TypeSeq newArgs = new TypeSeq ();
+ foreach (Type! t in Arguments)
+ newArgs.Add(t.Substitute(subst));
+ Type! newResult = Result.Substitute(subst);
+
+ return new MapType(tok, TypeParameters, newArgs, newResult);
+ }
+
+ //----------- Hashcodes ----------------------------------
+
+ [Pure]
+ public override int GetHashCode(TypeVariableSeq! boundVariables) {
+ int res = 7643761 * TypeParameters.Length + 65121 * Arguments.Length;
+
+ foreach (TypeVariable! var in this.TypeParameters)
+ boundVariables.Add(var);
+
+ foreach (Type! t in Arguments)
+ res = res * 5 + t.GetHashCode(boundVariables);
+ res = res * 7 + Result.GetHashCode(boundVariables);
+
+ for (int i = 0; i < this.TypeParameters.Length; ++i)
+ boundVariables.Remove();
+
+ return res;
+ }
+
+ //----------- Linearisation ----------------------------------
+
+ public override void Emit(TokenTextWriter! stream, int contextBindingStrength)
+ {
+ 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) {
+ int previousState = rc.TypeBinderState;
+ try {
+ foreach (TypeVariable! v in TypeParameters) {
+ rc.AddTypeBinder(v);
+ }
+
+ TypeSeq resolvedArgs = new TypeSeq ();
+ foreach (Type! ty in Arguments) {
+ resolvedArgs.Add(ty.ResolveType(rc));
+ }
+
+ Type resolvedResult = Result.ResolveType(rc);
+
+ CheckBoundVariableOccurrences(TypeParameters,
+ resolvedArgs, new TypeSeq(resolvedResult),
+ this.tok, "map arguments",
+ rc);
+
+ // sort the type parameters so that they are bound in the order of occurrence
+ TypeVariableSeq! sortedTypeParams = SortTypeParams(TypeParameters, resolvedArgs, resolvedResult);
+ return new MapType(tok, sortedTypeParams, resolvedArgs, resolvedResult);
+ } finally {
+ rc.TypeBinderState = previousState;
+ }
+ }
+
+ public override TypeVariableSeq! FreeVariables {
+ get {
+ TypeVariableSeq! res = FreeVariablesIn(Arguments);
+ res.AppendWithoutDups(Result.FreeVariables);
+ foreach (TypeVariable! v in TypeParameters)
+ res.Remove(v);
+ return res;
+ }
+ }
+
+ public override List<TypeProxy!>! FreeProxies { get {
+ List<TypeProxy!>! res = new List<TypeProxy!> ();
+ foreach (Type! t in Arguments)
+ 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.Length;
+ } }
+
+ //------------ 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(ExprSeq! actualArgs,
+ out TypeParamInstantiation! tpInstantiation,
+ IToken! typeCheckingSubject,
+ string! opName,
+ TypecheckingContext! tc) {
+ List<Type!>! actualTypeParams;
+ TypeSeq actualResult =
+ Type.CheckArgumentTypes(TypeParameters, out actualTypeParams, Arguments, actualArgs,
+ new TypeSeq (Result), null, typeCheckingSubject, opName, tc);
+ if (actualResult == null) {
+ tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
+ return null;
+ } else {
+ assert actualResult.Length == 1;
+ tpInstantiation = SimpleTypeParamInstantiation.From(TypeParameters, actualTypeParams);
+ return actualResult[0];
+ }
+ }
+
+ public override Absy! StdDispatch(StandardVisitor! visitor)
+ {
+ return visitor.VisitMapType(this);
+ }
+ }
+
+ //---------------------------------------------------------------------
+
+ public enum SimpleType { Int, 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.
+ public interface TypeParamInstantiation {
+ // return what formal type parameters there are
+ List<TypeVariable!>! FormalTypeParams { get; }
+ // given a formal type parameter, return the actual instantiation
+ Type! this[TypeVariable! var] { get; }
+ }
+
+ public class SimpleTypeParamInstantiation : TypeParamInstantiation {
+ private readonly List<TypeVariable!>! TypeParams;
+ private readonly IDictionary<TypeVariable!, Type!>! Instantiations;
+
+ public SimpleTypeParamInstantiation(List<TypeVariable!>! typeParams,
+ IDictionary<TypeVariable!, Type!>! instantiations) {
+ this.TypeParams = typeParams;
+ this.Instantiations = instantiations;
+ }
+
+ public static TypeParamInstantiation!
+ From(TypeVariableSeq! typeParams, List<Type!>! actualTypeParams)
+ requires typeParams.Length == actualTypeParams.Count; {
+ if (typeParams.Length == 0)
+ return EMPTY;
+
+ List<TypeVariable!>! typeParamList = new List<TypeVariable!> ();
+ IDictionary<TypeVariable!, Type!>! dict = new Dictionary<TypeVariable!, Type!> ();
+ for (int i = 0; i < typeParams.Length; ++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<TypeVariable!> (),
+ new Dictionary<TypeVariable!, Type!> ());
+
+ // return what formal type parameters there are
+ public List<TypeVariable!>! FormalTypeParams { get {
+ 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 TypeSeq! 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<TypeVariable!, Type!> Instantiations = null;
+
+ public MapTypeProxyParamInstantiation(MapTypeProxy! proxy,
+ TypeSeq! argumentsResult) {
+ this.Proxy = proxy;
+ this.ArgumentsResult = argumentsResult;
+ }
+
+ // return what formal type parameters there are
+ public List<TypeVariable!>! 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<TypeVariable!> ();
+ 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;
+ assert realType != null;
+ TypeSeq! formalArgs = new TypeSeq ();
+ foreach (Type! t in realType.Arguments)
+ formalArgs.Add(t);
+ formalArgs.Add(realType.Result);
+ Instantiations =
+ Type.InferTypeParameters(realType.TypeParameters, formalArgs, ArgumentsResult);
+ }
+ return Instantiations[var];
+ } }
+ }
+
+}
|