78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
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
|
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
|
auto tf = *FromValue< TFunc >( rhsVal );
auto constraintPat = BuildTFuncSignature( uc.context(), *tfuncType );
assert( constraintPat );
auto cfunc = make_shared< ConstrainedFunc >( *constraintPat, GetTFuncInvocationRule(), rhsVal );
auto cFuncTerm = ValueToIRExpr( ToValue( move( cfunc ) ) );
// Create a new named hole namespace to isolate holes from the passed function from those in
// the called function.
auto savedRHSNamespaceIndex = uc.RHSNamespaceIndex();
uc.setRHSNamespaceIndex( uc.newNamespaceIndex() );
auto oldValueRequired = uc.isValueResolutionRequired();
uc.setValueResolutionRequired( false );
for( auto&& [s, uc] : Unify( callPat, rhs, uc ) )
{
// Restore the namespace
auto localC = uc;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
localC.setValueResolutionRequired( oldValueRequired );
// 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.
localC.setRHSNamespaceIndex( localC.LHSNamespaceIndex() );
for( auto&& [s,c] : Unify( cFuncTerm, tdeclHole, localC ) )
{
auto localC = c;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
co_yield { s, localC };
}
}
uc.setRHSNamespaceIndex( savedRHSNamespaceIndex );
uc.setValueResolutionRequired( oldValueRequired );
} );
// tfunc tdecl param / overloadset arg
e.unificationRuleSet()->addAsymRule(
move( tDeclTFuncPat ),
ValueToIRExpr( ValuePattern(
TSID( constant ),
GetValueType< ptr< builtins::OverloadSet > >(),
ANYTERM( _ ) ) ),
[]( const Term& lhs, const Term& rhs, UnificationContext& uc ) -> UniGen
{
auto tdecl = FromValue< TDecl >( *ValueFromIRExpr( lhs ) );
assert( tdecl );
auto tfuncType = FromValue< TFuncType >( *ValueFromIRExpr( tdecl->type() ) );
assert( tfuncType );
auto callPat = BuildArgPatternFromTDecl( *tdecl );
auto tdeclHole = MkHole( tdecl->name() );
auto rhsVal = *ValueFromIRExpr( rhs );
auto os = *FromValue< ptr< OverloadSet > >( rhsVal );
auto constraintPat = BuildTFuncSignature( uc.context(), *tfuncType );
assert( constraintPat );
auto cfunc = make_shared< ConstrainedFunc >( *constraintPat, GetOverloadSetInvocationRule(), rhsVal );
auto cFuncTerm = ValueToIRExpr( ToValue( move( cfunc ) ) );
// Create a new named hole namespace to isolate holes from the passed function from those in
// the called function.
auto savedRHSNamespaceIndex = uc.RHSNamespaceIndex();
uc.setRHSNamespaceIndex( uc.newNamespaceIndex() );
auto oldValueRequired = uc.isValueResolutionRequired();
|