@@ -7,9 +7,8 @@ use ast::{FnBody, StatementKind};
77use liquid_rust_core:: {
88 ast:: { self , ContDef , FnDef , Rvalue , Statement } ,
99 names:: * ,
10- ty:: { self , pred, subst:: Subst , BaseTy , ContTy , Heap , Pred , Ty , TyCtxt , TyKind , TyS } ,
10+ ty:: { self , pred, subst:: Subst , BaseTy , ContTy , Pred , Ty , TyCtxt } ,
1111} ;
12- use pred:: Place ;
1312
1413use crate :: env:: Env ;
1514
@@ -316,34 +315,3 @@ impl<'a> RefineChecker<'a> {
316315 self . errors . push ( err) ;
317316 }
318317}
319-
320- pub fn subtyping ( tcx : & TyCtxt , heap1 : & Heap , ty1 : & TyS , heap2 : & Heap , ty2 : & TyS ) -> Constraint {
321- match ( ty1. kind ( ) , ty2. kind ( ) ) {
322- ( TyKind :: Tuple ( tup1) , TyKind :: Tuple ( tup2) ) if tup1. len ( ) == tup2. len ( ) => tup1
323- . iter ( )
324- . zip ( tup2. types ( ) )
325- . rev ( )
326- . fold ( Constraint :: True , |c, ( ( f, ty1) , ty2) | {
327- Constraint :: Conj ( vec ! [
328- subtyping( tcx, heap1, ty1, heap2, ty2) ,
329- Constraint :: from_binding( * f, ty1. clone( ) , c) ,
330- ] )
331- } ) ,
332- // TODO check regions
333- ( TyKind :: Ref ( bk1, _, l1) , TyKind :: Ref ( bk2, _, l2) ) if bk1 >= bk2 => {
334- let ty1 = & tcx. selfify ( & heap1[ l1] , Place :: from ( * l1) ) ;
335- let ty2 = & heap2[ l2] ;
336- subtyping ( tcx, heap1, ty1, heap2, ty2)
337- }
338- ( TyKind :: OwnRef ( l1) , TyKind :: OwnRef ( l2) ) => {
339- let ty1 = & tcx. selfify ( & heap1[ l1] , Place :: from ( * l1) ) ;
340- let ty2 = & heap2[ l2] ;
341- subtyping ( tcx, heap1, ty1, heap2, ty2)
342- }
343- ( TyKind :: Refine ( bty1, refine1) , TyKind :: Refine ( bty2, refine2) ) if bty1 == bty2 => {
344- Constraint :: from_subtype ( * bty1, refine1, refine2)
345- }
346- ( _, TyKind :: Uninit ( n) ) if ty1. size ( ) == * n => Constraint :: True ,
347- _ => bug ! ( "{} {}" , ty1, ty2) ,
348- }
349- }
0 commit comments