From edce137539765639c3cc914e4e2c5dcf5d6b19d1 Mon Sep 17 00:00:00 2001 From: MichalMoskal Date: Wed, 18 Aug 2010 20:43:32 +0000 Subject: Chase type synonyms in arguments/results of map types when generating name (with tE:m). --- Source/VCExpr/SimplifyLikeLineariser.cs | 50 ++++++++++++++++++++++++--------- 1 file changed, 36 insertions(+), 14 deletions(-) (limited to 'Source') diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs index 01fd37c9..1ee61bfc 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.cs +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -242,22 +242,45 @@ Contract.Ensures(Contract.Result() != null); } } - private static string TypeToStringHelper(Type t){ -Contract.Requires(t != null); -Contract.Ensures(Contract.Result() != null); - System.IO.StringWriter buffer = new System.IO.StringWriter(); - using (TokenTextWriter stream = new TokenTextWriter("", buffer, false)) { - t.Emit(stream); + private static void TypeToStringHelper(Type t, StringBuilder sb) + { + Contract.Requires(t != null); + Contract.Ensures(Contract.Result() != null); + + TypeSynonymAnnotation syn = t as TypeSynonymAnnotation; + if (syn != null) { + TypeToStringHelper(syn.ExpandedType, sb); } - return buffer.ToString(); + else { + if (t.IsMap) { + MapType m = t.AsMap; + sb.Append('['); + for (int i = 0; i < m.MapArity; ++i) { + if (i != 0) sb.Append(','); + TypeToStringHelper(m.Arguments[i], sb); + } + sb.Append(']'); + TypeToStringHelper(m.Result, sb); + } + else if (t.IsBool || t.IsInt || t.IsBv) { + sb.Append(TypeToString(t)); + } + else { + System.IO.StringWriter buffer = new System.IO.StringWriter(); + using (TokenTextWriter stream = new TokenTextWriter("", buffer, false)) { + t.Emit(stream); + } + sb.Append(buffer.ToString()); + } + } + } + + public static string TypeToString(Type t) { Contract.Requires(t != null); Contract.Ensures(Contract.Result() != null); - TypeSynonymAnnotation syn = t as TypeSynonymAnnotation; - if (syn != null) - return TypeToString(syn.ExpandedType); if (t.IsBool) return "$bool"; @@ -265,11 +288,10 @@ Contract.Ensures(Contract.Result() != null); return "$int"; else if (t.IsBv) return "$bv" + t.BvBits; - else if (t.IsMap) - return TypeToStringHelper(t); else { - // at this point, only the types U, T, and bitvector types should be left - return TypeToStringHelper(t); + StringBuilder sb = new StringBuilder(); + TypeToStringHelper(t, sb); + return sb.ToString(); } } -- cgit v1.2.3