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
|
#include "builtins/builtins.h"
namespace empathy::builtins
{
UniGen UnifyTDecl( const Term& lhs, const Term& rhs, UnificationContext& c )
{
auto tdecl = FromValue< TDecl >( *ValueFromIRExpr( lhs ) );
assert( tdecl );
// Both of the expressions are side by side in the same input expresion, which
// means their hole names share the same namespace. So pretend that both the LHS and RHS
// namespaces are the same for their unification, but restore it after.
auto savedRHSNamespaceIndex = c.RHSNamespaceIndex();
c.setRHSNamespaceIndex( c.LHSNamespaceIndex() );
for( auto&& [u,c] : Unify( tdecl->type(), tdecl->value(), c ) )
{
auto localC = c;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
co_yield Unify( u, rhs, localC );
}
}
void SetupTDeclUnification( Env& e )
{
auto tDeclPat = ValueToIRExpr( Value( GetValueType< TDecl >(), TVEC( ANYTERM( _ ), ANYTERM( _ ) ) ) );
e.unificationRuleSet()->addHalfUnificationRule( tDeclPat,
[]( const Term& lhs, UnificationContext& c ) -> UniGen
{
auto tdecl = FromValue< TDecl >( *ValueFromIRExpr( lhs ) );
assert( tdecl );
// Both of the expressions are side by side in the same input expression, which
// means their hole names share the same namespace. So pretend that both the LHS and RHS
// namespaces are the same for their unification, but restore it after.
auto savedRHSNamespaceIndex = c.RHSNamespaceIndex();
c.setRHSNamespaceIndex( c.LHSNamespaceIndex() );
for( auto&& [u,c] : Unify( tdecl->type(), tdecl->value(), c ) )
{
co_yield { u, localC };
}
} );
e.unificationRuleSet()->addSymRule( tDeclPat, ANYTERM( _ ), UnifyTDecl );
e.unificationRuleSet()->addSymRule( tDeclPat, UnifyTDecl );
}
}
|
>
>
>
>
>
|
|
>
>
>
>
|
|
|
|
|
|
|
|
>
>
>
>
>
>
>
|
>
>
>
|
>
|
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|
|
>
>
|
>
|
>
>
>
>
>
>
>
>
>
>
>
|
<
|
|
>
>
|
|
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
|
#include "builtins/builtins.h"
namespace empathy::builtins
{
Term BuildArgPatternFromTDecl( const TDecl& td )
{
return ValueToIRExpr( ValuePattern( MkHole( "_"_sid ), td.type(), MkHole( "_"_sid ) ) );
}
UniGen UnifyTDecl( const Term& lhs, const Term& rhs, UnificationContext& c )
{
auto tdecl = FromValue< TDecl >( *ValueFromIRExpr( lhs ) );
assert( tdecl );
auto tdeclHole = MkHole( tdecl->name() );
auto pat = ValueToIRExpr( Value( tdecl->type(), MkHole( "_"_sid ) ) );
for( auto&& [s,c] : Unify( pat, rhs, c ) )
{
// 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 savedRHSNamespaceIndex = c.RHSNamespaceIndex();
c.setRHSNamespaceIndex( c.LHSNamespaceIndex() );
for( auto&& [s,c] : Unify( s, tdeclHole, c ) )
{
auto localC = c;
localC.setRHSNamespaceIndex( savedRHSNamespaceIndex );
co_yield { s, localC };
}
c.setRHSNamespaceIndex( savedRHSNamespaceIndex );
}
}
void SetupTDeclUnification( Env& e )
{
auto tDeclPat = ValueToIRExpr( Value( GetValueType< TDecl >(), TVEC( ANYTERM( _ ), ANYTERM( _ ) ) ) );
e.unificationRuleSet()->addHalfUnificationRule( tDeclPat,
[]( const Term& lhs, UnificationContext& c ) -> UniGen
{
auto tdecl = FromValue< TDecl >( *ValueFromIRExpr( lhs ) );
assert( tdecl );
co_yield HalfUnify( tdecl->type(), c );
} );
e.unificationRuleSet()->addSymRule( tDeclPat, ANYTERM( _ ), UnifyTDecl );
e.unificationRuleSet()->addSymRule( tDeclPat, UnifyTDecl );
// tfunc tdecl param / tfunc arg
auto tFuncTypePat = ValueToIRExpr( Value( TypeType(), TVEC( TSID( texpr ), TSID( tfunc ),
ANYTERM( _ ), ANYTERM( _ ) ) ) );
auto tDeclTFuncPat = ValueToIRExpr( Value( GetValueType< TDecl >(), TVEC( tFuncTypePat, ANYTERM( _ ) ) ) );
e.unificationRuleSet()->addAsymRule(
tDeclTFuncPat,
ValueToIRExpr( ValuePattern(
TSID( constant ),
move( tFuncTypePat ),
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 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 );
} );
}
}
|