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
|
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
|
-
+
-
+
-
-
+
+
-
-
+
+
-
+
-
+
-
+
|
#include "builtins/builtins.h"
namespace goose::builtins
{
Term BuildArgPatternFromTDecl( const Context& c, Term&& sig )
{
return ValueToEIR( ValuePattern( HOLE( "_"_sid ), move( sig ), HOLE( "_"_sid ) ) );
}
void SetupTDeclTypeChecking( Env& e )
{
auto tDeclPat = TDeclSigPattern( ANYTERM( _ ), ANYTERM( _ ) );
auto tDeclPat = TDeclSigPattern( ANYTERM( _ ), ANYTERM( _ ), ANYTERM( _ ) );
e.typeCheckingRuleSet()->addHalfUnificationRule( TCRINFOS, tDeclPat,
[]( const Term& lhs, TypeCheckingContext& c )
{
auto [name,sig] = DecomposeTDSig( lhs );
auto [name,rptDepth,sig] = DecomposeTDSig( lhs );
return HalfUnify( sig, c );
} );
e.typeCheckingRuleSet()->addTypeCheckingRule( TCRINFOS, tDeclPat, ANYTERM( _ ),
[]( const Term& lhs, const Term& rhs, TypeCheckingContext tcc ) -> TCGen
{
auto [name,typeSig] = DecomposeTDSig( lhs );
auto tdeclHole = HOLE( name );
auto [name,rptDepth,typeSig] = DecomposeTDSig( lhs );
auto tdeclHole = HOLE( name, ""_sid, rptDepth );
auto pat = ValueToEIR( Value( move( typeSig ), HOLE( "_"_sid ) ) );
for( auto&& [s,tcc] : TypeCheck( pat, rhs, tcc ) )
{
// We need to typecheck the result with a hole named after the decl. However, since both sides of
// this unification orignally appeared on the LHS, we need to setup RHS to alias the LHS namespace for this.
auto savedRHSSubContext = tcc.RHSSubContext();
tcc.RHSSubContext() = tcc.LHSSubContext();
for( auto&& [s,tcc] : TypeCheck( s, tdeclHole, tcc ) )
{
tcc.RHSSubContext() = savedRHSSubContext;
co_yield { s, tcc };
}
}
} );
e.typeCheckingRuleSet()->addUnificationRule( TCRINFOS, tDeclPat, ANYTERM( _ ),
[]( const Term& lhs, const Term& rhs, TypeCheckingContext tcc ) -> TCGen
{
auto [name,typeSig] = DecomposeTDSig( lhs );
auto tdeclHole = HOLE( name );
auto [name,rptDepth,typeSig] = DecomposeTDSig( lhs );
auto tdeclHole = HOLE( name, ""_sid, rptDepth );
auto pat = ValueToEIR( Value( move( typeSig ), HOLE( "_"_sid ) ) );
for( auto&& [s,tcc] : Unify( pat, rhs, tcc ) )
{
// We need to unify the result with a hole named after the decl. However, since both sides of
// this unification orignally appeared on the LHS, we need to setup RHS to alias the LHS namespace for this.
auto savedRHSSubContext = tcc.RHSSubContext();
tcc.RHSSubContext() = tcc.LHSSubContext();
for( auto&& [s,tcc] : Unify( s, tdeclHole, tcc ) )
{
tcc.RHSSubContext() = savedRHSSubContext;
co_yield { s, tcc };
}
}
} );
// tfunc tdecl param / tfunc arg
auto tDeclTFuncPat = TDeclSigPattern( ANYTERM( _ ), TFuncTypeSigPattern( ANYTERM( _ ), ANYTERM( _ ) ) );
auto tDeclTFuncPat = TDeclSigPattern( ANYTERM( _ ), ANYTERM( _ ), TFuncTypeSigPattern( ANYTERM( _ ), ANYTERM( _ ) ) );
e.typeCheckingRuleSet()->addTypeCheckingRule( TCRINFOS,
tDeclTFuncPat,
ValueToEIR( ValuePattern(
TSID( constant ),
TFuncTypePattern(),
ANYTERM( _ ) ) ),
[]( const Term& lhs, const Term& rhs, TypeCheckingContext tcc ) -> TCGen
{
auto [name,typeSig] = DecomposeTDSig( lhs );
auto [name,rptDepth,typeSig] = DecomposeTDSig( lhs );
auto [_,tfSig] = DecomposeTFTSig( typeSig );
auto callPat = BuildArgPatternFromTDecl( tcc.context(), move( typeSig ) );
auto tdeclHole = HOLE( name );
auto tdeclHole = HOLE( name, ""_sid, rptDepth );
auto rhsVal = *EIRToValue( rhs );
ConstrainedFunc cfunc( tfSig, GetTFuncInvocationRule(), rhsVal );
auto cFuncTerm = ValueToEIR( ToValue( move( cfunc ) ) );
// Create a new named hole namespace to isolate holes from the passed function from those in
|
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
|
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
|
-
+
-
+
|
ValueToEIR( ValuePattern(
TSID( constant ),
GetValueType< ptr< sema::OverloadSet > >(),
ANYTERM( _ ) ) ),
[]( const Term& lhs, const Term& rhs, TypeCheckingContext tcc ) -> TCGen
{
auto [name,typeSig] = DecomposeTDSig( lhs );
auto [name,rptDepth,typeSig] = DecomposeTDSig( lhs );
auto [_,tfSig] = DecomposeTFTSig( typeSig );
auto callPat = BuildArgPatternFromTDecl( tcc.context(), move( typeSig ) );
auto tdeclHole = HOLE( name );
auto tdeclHole = HOLE( name, ""_sid, rptDepth );
auto rhsVal = *EIRToValue( rhs );
ConstrainedFunc cfunc( tfSig, GetOverloadSetInvocationRule(), rhsVal );
auto cFuncTerm = ValueToEIR( ToValue( move( cfunc ) ) );
// Create a new named hole namespace to isolate holes from the passed function from those in
|