1+ use crate :: UnknownError ;
12use crate :: Mexpr ;
23
34#[ derive( Debug , Clone , Copy , PartialEq ) ]
@@ -14,6 +15,7 @@ pub enum IntSize {
1415 I8 = 8 ,
1516}
1617
18+ #[ derive( Debug , Clone , PartialEq ) ]
1719pub enum SimpleType {
1820 Top ,
1921 Bottom ,
@@ -80,10 +82,18 @@ impl SimpleType {
8082 }
8183}
8284
85+ #[ derive( Debug , Clone , PartialEq ) ]
8386pub enum Type {
84- //
87+ Simple ( SimpleType ) ,
88+ Array ( Box < Type > , Box < Type > ) ,
89+ String ( Box < Type > ) ,
90+ Liquid ( Box < Type > , Vec < Predicate > ) ,
91+
8592}
8693
94+ #[ derive( Debug , Clone , PartialEq ) ]
95+ pub enum Predicate { }
96+
8797fn is_cmp_expr ( head : & str ) -> bool {
8898 [ "lt" , "le" , "eq" , "ge" , "gt" ] . contains ( & head)
8999}
@@ -137,7 +147,7 @@ impl Refiner {
137147 name : "arr" . to_owned ( ) ,
138148 body : vec ! [ ty, body[ 0 ] . clone( ) ]
139149 } ;
140-
150+
141151 * expr = val
142152 } ,
143153 Mexpr :: Apply { name, body } if name == "size" => {
@@ -172,6 +182,28 @@ pub struct Meeter { }
172182
173183impl Meeter {
174184 pub fn resolve ( & mut self , expr : & mut Mexpr ) {
175- todo ! ( )
185+ match expr {
186+ Mexpr :: Apply { name, body } if name == "and" => {
187+ let mut meet = body[ 0 ] . clone ( ) ;
188+ for e in body {
189+ meet = self . meet ( & meet, e)
190+ }
191+
192+ * expr = meet
193+ } ,
194+ _ => todo ! ( )
195+ }
196+ }
197+
198+ fn meet ( & mut self , left : & Mexpr , right : & Mexpr ) -> Mexpr {
199+ match ( left, right) {
200+ ( e, Mexpr :: Name ( n) ) | ( Mexpr :: Name ( n) , e) if n == "_" => {
201+ e. clone ( )
202+ } ,
203+ ( _, Mexpr :: Name ( n) ) | ( Mexpr :: Name ( n) , _) if n == "bottom" => {
204+ SimpleType :: Bottom . to_expr ( )
205+ } ,
206+ _ => todo ! ( )
207+ }
176208 }
177209}
0 commit comments