diff options
| author |  MichalMoskal <unknown> | 2010-08-18 20:43:32 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2010-08-18 20:43:32 +0000 |
| commit | edce137539765639c3cc914e4e2c5dcf5d6b19d1 (patch) | |
| tree | 1553bb4c3aad1b1964b1a30ed95a5c31fc895e3e /Source | |
| parent | aa046e67454b6a0bb3288c8dbe95250186fe750d (diff) | |
Chase type synonyms in arguments/results of map types when generating name (with tE:m).
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/VCExpr/SimplifyLikeLineariser.cs | 50 |
1 files changed, 36 insertions, 14 deletions
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<string>() != null); }
}
- private static string TypeToStringHelper(Type t){
-Contract.Requires(t != null);
-Contract.Ensures(Contract.Result<string>() != null);
- System.IO.StringWriter buffer = new System.IO.StringWriter();
- using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
- t.Emit(stream);
+ private static void TypeToStringHelper(Type t, StringBuilder sb)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result<string>() != 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>", buffer, false)) {
+ t.Emit(stream);
+ }
+ sb.Append(buffer.ToString());
+ }
+ }
+
}
+
+
public static string TypeToString(Type t)
{
Contract.Requires(t != null);
Contract.Ensures(Contract.Result<string>() != 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<string>() != 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();
}
}
|