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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
// val-defs.h
// Syntax class definitions for compile-time values.
// A compile-time integer (may not have a specific concrete value)
ABSTRACT_SYNTAX_CLASS(IntVal, Val)
END_SYNTAX_CLASS()
// Trivial case of a value that is just a constant integer
SYNTAX_CLASS(ConstantIntVal, IntVal)
FIELD(IntegerLiteralValue, value)
RAW(
ConstantIntVal()
{}
ConstantIntVal(IntegerLiteralValue value)
: value(value)
{}
virtual bool EqualsVal(Val* val) override;
virtual String ToString() override;
virtual int GetHashCode() override;
)
END_SYNTAX_CLASS()
// The logical "value" of a rererence to a generic value parameter
SYNTAX_CLASS(GenericParamIntVal, IntVal)
DECL_FIELD(DeclRef<VarDeclBase>, declRef)
RAW(
GenericParamIntVal()
{}
GenericParamIntVal(DeclRef<VarDeclBase> declRef)
: declRef(declRef)
{}
virtual bool EqualsVal(Val* val) override;
virtual String ToString() override;
virtual int GetHashCode() override;
virtual RefPtr<Val> SubstituteImpl(SubstitutionSet subst, int* ioDiff) override;
)
END_SYNTAX_CLASS()
// A witness to the fact that some proposition is true, encoded
// at the level of the type system.
//
// Given a generic like:
//
// void example<L>(L light)
// where L : ILight
// { ... }
//
// a call to `example()` needs two things for us to be sure
// it is valid:
//
// 1. We need a type `X` to use as the argument for the
// parameter `L`. We might supply this explicitly, or
// via inference.
//
// 2. We need a *proof* that whatever `X` we chose conforms
// to the `ILight` interface.
//
// The easiest way to make such a proof is by construction,
// and a `Witness` represents such a constructive proof.
// Conceptually a proposition like `X : ILight` can be
// seen as a type, and witness prooving that proposition
// is a value of that type.
//
// We construct and store witnesses explicitly during
// semantic checking because they can help us with
// generating downstream code. By following the structure
// of a witness (the structure of a proof) we can, e.g.,
// navigate from the knowledge that `X : ILight` to
// the concrete declarations that provide the implementation
// of `ILight` for `X`.
//
ABSTRACT_SYNTAX_CLASS(Witness, Val)
END_SYNTAX_CLASS()
// A witness that one type is a subtype of another
// (where by "subtype" we include both inheritance
// relationships and type-conforms-to-interface relationships)
//
// TODO: we may need to tease those apart.
ABSTRACT_SYNTAX_CLASS(SubtypeWitness, Witness)
FIELD(RefPtr<Type>, sub)
FIELD(RefPtr<Type>, sup)
RAW(
virtual DeclRef<Decl> getLastStepDeclRef() = 0;
)
END_SYNTAX_CLASS()
SYNTAX_CLASS(TypeEqualityWitness, SubtypeWitness)
RAW(
virtual bool EqualsVal(Val* val) override;
virtual String ToString() override;
virtual int GetHashCode() override;
virtual RefPtr<Val> SubstituteImpl(SubstitutionSet subst, int * ioDiff) override;
virtual DeclRef<Decl> getLastStepDeclRef() override
{
return DeclRef<Decl>();
}
)
END_SYNTAX_CLASS()
// A witness that one type is a subtype of another
// because some in-scope declaration says so
SYNTAX_CLASS(DeclaredSubtypeWitness, SubtypeWitness)
FIELD(DeclRef<Decl>, declRef);
RAW(
virtual bool EqualsVal(Val* val) override;
virtual String ToString() override;
virtual int GetHashCode() override;
virtual RefPtr<Val> SubstituteImpl(SubstitutionSet subst, int * ioDiff) override;
virtual DeclRef<Decl> getLastStepDeclRef() override
{
return declRef;
}
)
END_SYNTAX_CLASS()
// A witness that `sub : sup` because `sub : mid` and `mid : sup`
SYNTAX_CLASS(TransitiveSubtypeWitness, SubtypeWitness)
// Witness that `sub : mid`
FIELD(RefPtr<SubtypeWitness>, subToMid);
// Witness that `mid : sup`
FIELD(RefPtr<SubtypeWitness>, midToSup);
RAW(
virtual bool EqualsVal(Val* val) override;
virtual String ToString() override;
virtual int GetHashCode() override;
virtual RefPtr<Val> SubstituteImpl(SubstitutionSet subst, int * ioDiff) override;
virtual DeclRef<Decl> getLastStepDeclRef() override
{
return midToSup->getLastStepDeclRef();
}
)
END_SYNTAX_CLASS()
// A value that is used as a proxy when we need to
// put an IR-level value into AST types
SYNTAX_CLASS(IRProxyVal, Val)
FIELD(IRUse, inst)
RAW(
virtual bool EqualsVal(Val* val) override;
virtual String ToString() override;
virtual int GetHashCode() override;
~IRProxyVal() override
{
inst.clear();
}
)
END_SYNTAX_CLASS()
|
