forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
/
TupleTypeDecl.cs
98 lines (85 loc) · 4.22 KB
/
TupleTypeDecl.cs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Linq;
using JetBrains.Annotations;
namespace Microsoft.Dafny;
public class TupleTypeDecl : IndDatatypeDecl {
public readonly List<bool> ArgumentGhostness;
public int Dims => ArgumentGhostness.Count;
public int NonGhostDims => ArgumentGhostness.Count(x => !x);
[CanBeNull] public TupleTypeDecl NonGhostTupleTypeDecl { get; }
/// <summary>
/// Construct a resolved built-in tuple type with "dim" arguments. "systemModule" is expected to be the _System module.
/// </summary>
public TupleTypeDecl(List<bool> argumentGhostness, ModuleDefinition systemModule, [CanBeNull] TupleTypeDecl nonGhostTupleTypeDecl, Attributes attributes)
: this(systemModule, CreateCovariantTypeParameters(argumentGhostness.Count), argumentGhostness, attributes) {
Contract.Requires(0 <= argumentGhostness.Count);
Contract.Requires(systemModule != null);
// Resolve the type parameters here
Contract.Assert(TypeArgs.Count == Dims);
for (var i = 0; i < Dims; i++) {
var tp = TypeArgs[i];
tp.Parent = this;
tp.PositionalIndex = i;
}
NonGhostTupleTypeDecl = nonGhostTupleTypeDecl;
}
private TupleTypeDecl(ModuleDefinition systemModule, List<TypeParameter> typeArgs, List<bool> argumentGhostness, Attributes attributes)
: base(RangeToken.NoToken, new Name(SystemModuleManager.TupleTypeName(argumentGhostness)), systemModule, typeArgs,
CreateConstructors(typeArgs, argumentGhostness),
new List<Type>(), new List<MemberDecl>(), attributes, false) {
Contract.Requires(systemModule != null);
Contract.Requires(typeArgs != null);
Contract.Assert(Ctors.Count == 1);
ArgumentGhostness = argumentGhostness;
foreach (var ctor in Ctors) {
ctor.EnclosingDatatype = this; // resolve here
GroundingCtor = ctor;
TypeParametersUsedInConstructionByGroundingCtor = new bool[typeArgs.Count];
for (int i = 0; i < typeArgs.Count; i++) {
TypeParametersUsedInConstructionByGroundingCtor[i] = !argumentGhostness[i];
}
}
this.EqualitySupport = argumentGhostness.Contains(true) ? ES.Never : ES.ConsultTypeArguments;
// Resolve parent type information - not currently possible for tuples to have any parent traits
ParentTypeInformation = new InheritanceInformationClass();
}
private static List<TypeParameter> CreateCovariantTypeParameters(int dims) {
Contract.Requires(0 <= dims);
var ts = new List<TypeParameter>();
for (int i = 0; i < dims; i++) {
var tp = new TypeParameter(RangeToken.NoToken, new Name("T" + i), TypeParameter.TPVarianceSyntax.Covariant_Strict);
tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
ts.Add(tp);
}
return ts;
}
/// <summary>
/// Creates the one and only constructor of the tuple type.
/// </summary>
private static List<DatatypeCtor> CreateConstructors(List<TypeParameter> typeArgs, List<bool> argumentGhostness) {
Contract.Requires(typeArgs != null);
var formals = new List<Formal>();
var nonGhostArgs = 0;
for (int i = 0; i < typeArgs.Count; i++) {
string compileName;
if (argumentGhostness[i]) {
// This name is irrelevant, since it won't be used in compilation. Give it a strange name
// that would alert us of any bug that nevertheless tries to access this name.
compileName = "this * ghost * arg * should * never * be * compiled * " + i.ToString();
} else {
compileName = nonGhostArgs.ToString();
nonGhostArgs++;
}
var tp = typeArgs[i];
var f = new Formal(Token.NoToken, i.ToString(), new UserDefinedType(Token.NoToken, tp), true, argumentGhostness[i], null, nameForCompilation: compileName);
formals.Add(f);
}
string ctorName = SystemModuleManager.TupleTypeCtorName(typeArgs.Count);
var ctor = new DatatypeCtor(RangeToken.NoToken, new Name(ctorName), false, formals, null);
return new List<DatatypeCtor>() { ctor };
}
public override string SanitizedName =>
sanitizedName ??= $"Tuple{SystemModuleManager.ArgumentGhostnessToString(ArgumentGhostness)}";
public override string GetCompileName(DafnyOptions options) => NonGhostTupleTypeDecl?.GetCompileName(options) ?? $"Tuple{NonGhostDims}";
}