3
3
4
4
use std:: sync:: Arc ;
5
5
6
+ use formality_core:: { Downcast , DowncastTo , Upcast , UpcastFrom } ;
6
7
// Default language for our crate
7
8
use formality_core:: { language:: HasKind , term} ;
8
9
use ptt:: grammar:: { Binder , BoundVar , ExistentialVar , UniversalVar , Variable } ;
@@ -24,12 +25,16 @@ formality_core::declare_language! {
24
25
#[ derive( Copy ) ]
25
26
pub enum Kind {
26
27
Ty ,
28
+ Perm ,
27
29
}
28
30
29
31
#[ term]
30
32
pub enum Parameter {
31
33
#[ cast]
32
34
Ty ( Ty ) ,
35
+
36
+ #[ cast]
37
+ Perm ( Perm ) ,
33
38
}
34
39
35
40
#[ term]
@@ -40,24 +45,48 @@ pub enum Ty {
40
45
#[ cast]
41
46
Id ( Id ) ,
42
47
48
+ #[ grammar( $v0 $v1) ]
49
+ Apply ( Perm , Arc < Ty > ) ,
50
+
43
51
#[ grammar( $v0 :: $v1) ]
44
52
Assoc ( Arc < Ty > , Id ) ,
45
53
}
46
54
55
+ #[ term]
56
+ pub enum Perm {
57
+ #[ variable( Kind :: Perm ) ]
58
+ Variable ( Variable ) ,
59
+ }
60
+
47
61
formality_core:: id!( Id ) ;
48
62
49
- formality_core:: cast_impl!( ( BoundVar ) <: ( Variable ) <: ( Ty ) ) ;
50
- formality_core:: cast_impl!( ( ExistentialVar ) <: ( Variable ) <: ( Ty ) ) ;
51
- formality_core:: cast_impl!( ( UniversalVar ) <: ( Variable ) <: ( Ty ) ) ;
52
- formality_core:: cast_impl!( ( Variable ) <: ( Ty ) <: ( Parameter ) ) ;
53
- formality_core:: cast_impl!( ( BoundVar ) <: ( Ty ) <: ( Parameter ) ) ;
54
- formality_core:: cast_impl!( ( ExistentialVar ) <: ( Ty ) <: ( Parameter ) ) ;
55
- formality_core:: cast_impl!( ( UniversalVar ) <: ( Ty ) <: ( Parameter ) ) ;
63
+ formality_core:: cast_impl!( ( BoundVar ) <: ( Variable ) <: ( Parameter ) ) ;
64
+ formality_core:: cast_impl!( ( ExistentialVar ) <: ( Variable ) <: ( Parameter ) ) ;
65
+ formality_core:: cast_impl!( ( UniversalVar ) <: ( Variable ) <: ( Parameter ) ) ;
66
+
67
+ impl UpcastFrom < Variable > for Parameter {
68
+ fn upcast_from ( term : Variable ) -> Self {
69
+ match term. kind ( ) {
70
+ Kind :: Ty => Ty :: Variable ( term) . upcast ( ) ,
71
+ Kind :: Perm => Perm :: Variable ( term) . upcast ( ) ,
72
+ }
73
+ }
74
+ }
75
+
76
+ impl DowncastTo < Variable > for Parameter {
77
+ fn downcast_to ( & self ) -> Option < Variable > {
78
+ match self {
79
+ Parameter :: Ty ( ty) => ty. downcast ( ) ,
80
+ Parameter :: Perm ( perm) => perm. downcast ( ) ,
81
+ }
82
+ }
83
+ }
56
84
57
85
impl HasKind < FormalityLang > for Parameter {
58
86
fn kind ( & self ) -> formality_core:: language:: CoreKind < FormalityLang > {
59
87
match self {
60
88
Parameter :: Ty ( _) => Kind :: Ty ,
89
+ Parameter :: Perm ( _) => Kind :: Perm ,
61
90
}
62
91
}
63
92
}
@@ -112,3 +141,50 @@ fn parse_assoc() {
112
141
"# ] ]
113
142
. assert_debug_eq ( & value) ;
114
143
}
144
+
145
+ /// Test for the case where the ambiguity occurs after some
146
+ /// reductions. In this case, we parse P (the variable) as a Perm
147
+ /// and then integrate that into the type, but we could also parse
148
+ /// P as a type itself.
149
+ #[ test]
150
+ #[ should_panic] // FIXME
151
+ fn parse_apply ( ) {
152
+ let value: Binder < Ty > = ptt:: term ( "<perm P> P i32" ) ;
153
+ expect_test:: expect![ [ r#"
154
+ Binder {
155
+ kinds: [
156
+ Ty,
157
+ ],
158
+ term: Assoc(
159
+ Id(
160
+ i32,
161
+ ),
162
+ T,
163
+ ),
164
+ }
165
+ "# ] ]
166
+ . assert_debug_eq ( & value) ;
167
+ }
168
+
169
+ /// Test for the case where the ambiguity occurs after some
170
+ /// reductions. In this case, we parse P (the variable) as a Perm
171
+ /// and then integrate that into the type, but we could also parse
172
+ /// P as a type itself.
173
+ #[ test]
174
+ #[ should_panic] // FIXME
175
+ fn parse_parameter ( ) {
176
+ let value: Binder < Parameter > = ptt:: term ( "<perm P> P" ) ;
177
+ expect_test:: expect![ [ r#"
178
+ Binder {
179
+ kinds: [
180
+ Perm,
181
+ ],
182
+ term: Perm(
183
+ Variable(
184
+ ^perm0_0,
185
+ ),
186
+ ),
187
+ }
188
+ "# ] ]
189
+ . assert_debug_eq ( & value) ;
190
+ }
0 commit comments