Changeset 15
- Timestamp:
- Nov 16, 2012, 4:26:26 PM (13 years ago)
- Files:
-
- 2 added
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
sizechecking/Constraints.hs
r14 r15 1 1 {-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, 2 2 IncoherentInstances, RankNTypes, ScopedTypeVariables, 3 FlexibleContexts,UndecidableInstances #-} 3 FlexibleContexts,UndecidableInstances, DeriveDataTypeable, 4 ImpredicativeTypes #-} 4 5 module Constraints where 5 6 … … 12 13 import Data.SBV ( (.==), (.<), (.>=)) 13 14 import Control.Monad 15 import Control.Monad.IO.Class 14 16 import Data.IORef() 15 17 import Data.Supply as S 18 import Data.Data 19 import Data.IORef 20 import Data.Dynamic 16 21 17 22 asType :: a -> a -> a … … 37 42 appall :: Int -> [L] -> L 38 43 appall var = foldl App (Var var) 39 40 44 41 45 data Condition = Condition [Constraint] L L … … 253 257 254 258 solve1' supp c@(Condition d a b) 255 | checkConds d = do256 putStrLn "Contradiction in preconditions"257 return []259 -- | checkConds d = do 260 -- putStrLn "Contradiction in preconditions" 261 -- return [] 258 262 | a==b = do 259 263 putStrLn "Equals" 260 264 return [] 261 | Just (var, nl) <- searchzero d = do262 let x = Condition (Prelude.map (normalizec.substc var (Num 0)) nl)263 (normalize$subst var (Num 0) a)264 (normalize$subst var (Num 0) b)265 266 putStrLn $ show (Var var) ++ " is zero:\n" ++ show x267 solve1 supp x268 | Just (var, exp, nl) <- searcheq d [] = do269 putStrLn $ "Found equation " ++ show (Var var) ++ " = " ++ show exp270 let x = Condition (Prelude.map (normalizec.substc var exp) nl )271 (normalize$subst var exp a)272 (normalize$subst var exp b)273 putStrLn $ "New equations:\n" ++ show x274 solve1 supp x265 -- | Just (var, nl) <- searchzero d = do 266 -- let x = Condition (Prelude.map (normalizec.substc var (Num 0)) nl) 267 -- (normalize$subst var (Num 0) a) 268 -- (normalize$subst var (Num 0) b) 269 -- 270 -- putStrLn $ show (Var var) ++ " is zero:\n" ++ show x 271 -- solve1 supp x 272 -- | Just (var, exp, nl) <- searcheq d [] = do 273 -- putStrLn $ "Found equation " ++ show (Var var) ++ " = " ++ show exp 274 -- let x = Condition (Prelude.map (normalizec.substc var exp) nl ) 275 -- (normalize$subst var exp a) 276 -- (normalize$subst var exp b) 277 -- putStrLn $ "New equations:\n" ++ show x 278 -- solve1 supp x 275 279 | App p q <- a, App r s <- b = do 276 280 putStrLn "Branching!" 277 281 nc <- checkCond supp [Condition d p r, Condition d q s] 278 282 solve nc supp 279 280 283 281 284 -- | Abs _ _ <- a, Abs _ _ <- b = do … … 288 291 -- | Abs _ _ <- a, AAbs _ _ _ <- b = applyList a b d supp 289 292 -- | AAbs _ _ _ <- a, AAbs _ _ _ <- b = applyList a b d supp 290 | Just dd <- reorder d = do 291 putStrLn $ "Reorder " ++ show dd 292 solve1 supp $ Condition dd a b 293 294 -- | Just dd <- reorder d = do 295 -- putStrLn $ "Reorder " ++ show dd 296 -- solve1 supp $ Condition dd a b 293 297 | otherwise = do 294 298 putStrLn "Tying to call solver" … … 300 304 otherwise -> return [c] 301 305 306 data LU = LU deriving (Eq, Ord, Data, Typeable) 307 instance SBV.SymWord LU 308 instance SBV.HasKind LU 309 302 310 fvc (Zero a) = fv a 303 311 fvc (LTC a b) = fv a `Set.union` fv b … … 306 314 compiletosolver :: L -> L -> [Constraint] -> SBV.Symbolic SBV.SBool 307 315 compiletosolver a b d = do 308 let fvs = Set.toList $ Set.unions $ fv a : fv b : map fvc d 309 (vars::[SBV.SInteger]) <- mapM (SBV.free . flip showVar "") fvs 310 let varmap = Map.fromList $ zip fvs vars 311 mapM_ (SBV.constrain . compilec varmap) d 312 return $ compilel varmap a .== compilel varmap b 313 314 compilec v (Zero a) = compilel v a .== (0::SBV.SInteger) 315 compilec v (LTC a b) = compilel v a .< compilel v b 316 compilec v (GEC a b) = compilel v a .>= compilel v b 317 318 compilel :: Map.Map Int SBV.SInteger -> L -> SBV.SInteger 319 compilel v (Op a c b) = case c of 316 varmap <- liftIO createVarPool 317 expmap <- liftIO createExpPool 318 supply <- liftIO $ newNumSupply 319 let (s1,s2,s3,s4) = split4 supply 320 cs <- mapM (\(s,x) -> compilec varmap expmap s x) $ zip (split s1) d 321 mapM_ (SBV.constrain) cs 322 lhs <- compilel varmap expmap s3 a 323 rhs <- compilel varmap expmap s4 b 324 return $ lhs .== rhs 325 326 data VarT = VarI | VarF VarT VarT 327 type VarPool = IORef (Map.Map Int Dynamic) 328 type ExpPool = IORef (Map.Map L SBV.SInteger) 329 330 createVarPool :: IO (VarPool) 331 createVarPool = newIORef $ Map.empty 332 createExpPool :: IO (ExpPool) 333 createExpPool = newIORef $ Map.empty 334 335 336 sbvTc :: TyCon 337 sbvTc = mkTyCon3 "Data" "SBV" "SBV" 338 339 instance (Typeable t) => Typeable (SBV.SBV t) where 340 typeOf x = mkTyConApp sbvTc [typeOf (get x)] 341 where 342 get :: SBV.SBV a -> a 343 get = undefined 344 345 346 getVarSymbol :: VarPool -> (SBV.Symbolic Dynamic) -> Int -> SBV.Symbolic Dynamic 347 getVarSymbol pool factory a = do 348 v <- liftIO $ readIORef pool 349 case Map.lookup a v of 350 Just q -> return $ q 351 Nothing -> do 352 dx <- factory 353 let newmap = Map.insert a dx v 354 liftIO $ writeIORef pool newmap 355 return dx 356 357 getExpSymbol :: ExpPool -> (SBV.Symbolic SBV.SInteger) -> L -> SBV.Symbolic SBV.SInteger 358 getExpSymbol pool factory a = do 359 v <- liftIO $ readIORef pool 360 case Map.lookup a v of 361 Just q -> return $ q 362 Nothing -> do 363 dx <- factory 364 let newmap = Map.insert a dx v 365 liftIO $ writeIORef pool newmap 366 return dx 367 368 369 compilec :: VarPool -> ExpPool -> Supply Int -> Constraint -> SBV.Symbolic (SBV.SBool) 370 compilec v e s (Zero a) = do 371 lhs <- compilel v e s a 372 return $ lhs .== (0::SBV.SInteger) 373 374 compilec v e s (LTC a b) = do 375 let (s1,s2) = split2 s 376 lhs <- compilel v e s1 a 377 rhs <- compilel v e s2 b 378 return $ lhs .< rhs 379 380 compilec v e s (GEC a b) = do 381 let (s1,s2) = split2 s 382 lhs <- compilel v e s1 a 383 rhs <- compilel v e s2 b 384 return $ lhs .>= rhs 385 386 class Typeable a => VarFactory a where 387 createDyn :: String -> a -> SBV.Symbolic Dynamic 388 createDyn a n = do 389 x <- createVar a n 390 return $ toDyn x 391 createVar :: String -> a -> SBV.Symbolic a 392 393 instance VarFactory SBV.SInteger where 394 createVar n _ = SBV.free n 395 396 compilel :: VarPool -> ExpPool -> Supply Int -> L -> SBV.Symbolic (SBV.SInteger) 397 compilel v e s (Op a c b) = do 398 let (s1, s2) = split2 s 399 al <- compilel v e s1 a 400 bl <- compilel v e s1 b 401 return $ case c of 320 402 '+' -> al + bl 321 403 '-' -> al - bl 322 404 '*' -> al * bl 323 405 '/' -> al `SBV.sDiv` bl 324 where 325 al = compilel v a 326 bl = compilel v b 327 compilel v (Var a) | Just x<-Map.lookup a v = x 328 compilel v (Num a) = SBV.literal $ fromIntegral a 329 compilel v a = error $ "Cannot compile " ++ show a 406 compilel v e s (Var a) = do 407 let itype = (undefined ::SBV.SInteger) 408 sym <- getVarSymbol v (createDyn (showVar a "") itype) a 409 let var = (fromDynamic sym) :: Maybe SBV.SInteger 410 case var of 411 Just x -> return x 412 Nothing -> do 413 error "Type Error" 414 compilel v e s (Num a) = return $ SBV.literal $ fromIntegral a 415 compilel v e s (Bottom) = SBV.free_ 416 compilel v e s l = do 417 sym <- getExpSymbol e (return $ SBV.uninterpret ("unint" ++ showVar (supplyValue s) "") ) l 418 return sym 419 --compilel v e x = error $ "Cannot compile "++ show x 420 421 gettype :: ((b -> t) -> t) -> a -> b -> a 422 gettype = error "???" 423 424 {- 425 compileapp :: (VarFactory b, SBV.Uninterpreted (b -> SBV.SInteger)) => VarPool -> L -> ((b -> t) -> t) -> SBV.Symbolic (SBV.SInteger) 426 compileapp v (Var a) f = do 427 let itype = (error :: SBV.SInteger) 428 sym <- getVarSymbol v (createDyn (showVar a "") (gettype f itype)) a 429 let var = (fromDynamic sym) :: Maybe SBV.SInteger 430 case var of 431 Just x -> return x 432 Nothing -> do 433 error "Type Error" 434 -} 435 compileapp v (App x y) t = error $ "Not yet implemented." 436 -
sizechecking/Lambda.hs
r12 r15 13 13 data L = Abs Int L | App L L | Var Int | Num Int | Op L Char L | List L L | AAbs Int Int L 14 14 | Shift L L L | Unsized | Bottom 15 deriving Eq15 deriving (Eq, Ord) 16 16 17 17 showVar x = if x>28 -
sizechecking_branches/L.hs
r10 r15 1 {-# Language GADTs, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables, TypeFamilies, NoMonomorphismRestriction, OverlappingInstances #-}1 {-# Language GADTs, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables, TypeFamilies, NoMonomorphismRestriction, OverlappingInstances, IncoherentInstances #-} 2 2 module L where 3 3 4 import qualified Data.SBV as SBV 4 5 import Data.Char(ord, chr) 5 6 import Control.Monad.State … … 13 14 type Arr repr a b = repr a -> repr b 14 15 15 class Lambda l where 16 class (Num (LInt l)) => Lambda l where 17 type LInt l :: * 16 18 labs :: (l a -> l b) -> l (Arr l a b) 17 19 app :: l (Arr l a b) -> l a -> l b 18 lit :: Int -> l Int19 op :: l Int -> OpName -> l Int -> l Int20 lit :: (LInt l) -> l (LInt l) 21 op :: l (LInt l) -> OpName -> l (LInt l) -> l (LInt l) 20 22 21 23 class SizeExp l where … … 27 29 unsized :: l () 28 30 29 instance Lambda l => Show (l a) where 30 showsPrec _ e = error "Error: no show" 31 32 instance Lambda l => Eq (l a) where 33 (==) _ _ = error "Error: no eq" 34 35 instance Lambda l => Num (l Int) where 31 instance (Lambda l, LInt l ~ a) => Num (l a) where 36 32 fromInteger = lit . fromIntegral 37 33 lhs + rhs = op lhs PLUS rhs … … 45 41 46 42 instance Lambda LPrint where 43 type LInt LPrint = Int 47 44 lit x = LPrint $ \_ -> return $ shows x 48 45 op m opc n = LPrint $ \p -> do … … 99 96 x = aabs (\s _ -> s) `app` list (lit 0) (labs $ \_ -> undef) 100 97 y = list 0 $ labs $ \_ -> undef 101 z = (labs $ \s -> s+1) `app` (lit 1+2)102 98 conss = labs $ \x -> aabs $ \ys yf -> list (ys + 1) $ shift yf ys (labs $ \_ -> x) 103 99 concats = aabs $ \xs xf -> (aabs $ \ys yf -> list (xs+ys) $ shift xf xs yf) … … 112 108 l12 = list (lit 1) (labs $ \_ -> list (lit 2) (labs $ \_ -> unsized)) 113 109 110 v = (labs $ \s -> s+1) `app` (lit 1+2) 111 w1 = (labs $ \s -> s+ lit 1) 112 w2 = (labs $ \s -> s+ lit 2) 113 q1 :: (Lambda l, a ~ LInt l, Num (l a)) => l (Arr l b (Arr l a a)) 114 q1 = (labs $ \q -> labs $ \s -> s + lit 1) 115 q2 :: (Lambda l, a ~ LInt l, Num (l a)) => l (Arr l a (Arr l a a)) 116 q2 = (labs $ \q -> labs $ \s -> s + q) 117 q3 = (labs $ \q -> labs $ \s -> q + s) 118 114 119 {- Evaluating -} 120 eval = unR 115 121 newtype R a = R { unR :: a } 116 122 instance Lambda R where 117 labs f = R $ f 123 type LInt R = Int 124 labs f = R $ f 118 125 app e1 e2 = (unR e1) e2 119 126 lit i = R i … … 136 143 shift a s c = R $ \i -> if (unR i)<(unR s) then unR a i else unR c i 137 144 138 -- Type level int to count arity 139 data Zero 140 data Succ a 141 142 data Exp a where 143 Lit :: Int -> Exp Zero 144 Op :: Exp Zero -> OpName -> Exp Zero -> Exp Zero 145 App :: Exp (Succ a) -> Exp Zero -> Exp a 146 Var :: Int -> Exp a 147 148 instance Show (Exp a) where 149 showsPrec _ (Lit a) = shows a 150 showsPrec p (Op lhs op rhs) = 151 let (prec, lprec, rprec, c) = getPrec op 152 in showParen (p>prec) $ showsPrec lprec lhs . showChar c . showsPrec rprec rhs 153 showsPrec p (App lhs rhs) = 154 showParen (p>6) $ showsPrec 6 lhs . showChar ' ' . showsPrec 7 rhs 155 showsPrec _ (Var i) = showVar i 156 157 type IntExp = Exp Zero 158 data Condition = Eq IntExp IntExp | Gt IntExp IntExp | Lt IntExp IntExp 159 type SExp a = ([Condition], IntExp) 160 newtype Compile a = Compile { unCompile :: SExp a } 161 162 --instance Lambda Compile where 163 -- labs :: (l a -> l b) -> l (a -> b) 164 -- labs f = Compile $ f 165 166 167 --{- Create a restricted deep embedding to work with the expression -} 168 --{- sized [a] to prove -} 169 -- 170 --class Restricted a where 171 -- kind :: a -> Int 172 -- 173 --instance Restricted Int where 174 -- kind _ = 0 175 -- 176 --instance Restricted a => Restricted (Int -> a) where 177 -- kind _ = succ $ kind $ (undefined :: a) 178 -- 179 --class Var l where 180 -- var :: Restricted a => Int -> l a 181 -- 182 --showVar2 x = showChar '_' . showVar x 183 -- 184 --newtype Count a = C { count :: Int } 185 --cnv :: Restricted a => Count a -> a 186 --cnv = undefined 187 -- 188 --ckind :: (Restricted a) => Count a -> Int 189 --ckind = kind . cnv 190 -- 191 --instance Var Count where 192 -- var _ = undefined 193 -- 194 --instance Var LPrint where 195 -- var x = LPrint $ \_ -> return $ showVar2 x 196 -- 197 --class MGS a where 198 -- mgs :: Supply Int -> a -> a 199 -- mgs = mgs' [] 200 -- mgs' :: [Int] -> Supply Int -> a -> a 201 -- 202 --instance MGS () where 203 -- mgs' _ _ _ = () 204 -- 205 --instance MGS a => MGS (RList a) where 206 -- mgs' bound supp _ = RList (listsize, undefined) 207 -- where 208 -- (s1, s2, s3) = split3 supp 209 -- listsize = mgs' bound supp (undefined :: a) 145 newtype E a = E { unE :: a } 146 instance Lambda E where 147 type LInt E = SBV.SInteger 148 labs f = E $ f 149 app e1 e2 = (unE e1) e2 150 lit = E 151 op e1 op e2 = let opm = case op of 152 PLUS -> (+) 153 MINUS -> (-) 154 MUL -> (*) 155 in E $ opm (unE e1) (unE e2) 156 157 class Sizeable' a where 158 getl' :: E (Arr E a b) -> SBV.Symbolic b 159 160 instance Sizeable' (SBV.SInteger) where 161 getl' f = do 162 x <- SBV.sInteger "x" 163 return $ unE $ (unE f) $ E x 164 165 {- 166 getEq f = SBV.proveWith (SBV.z3 {SBV.verbose=True}) $ do 167 x <- getl f 168 return $ x SBV..== x 169 -} 170 data ST = ST 171 172 class Instantiateable a r | a -> r where 173 instantiate :: a -> SBV.Symbolic r 174 175 instance Instantiateable SBV.SInteger SBV.SInteger where 176 instantiate _ = do 177 liftIO $ putStrLn " INT VARIABLE x" 178 SBV.sInteger "x" 179 180 instance Instantiateable a ST where 181 instantiate _ = do 182 liftIO $ putStrLn " ? VARIABLE x" 183 return $ undefined -- SBV.uninterpret "f" 184 185 class Sizeable a where 186 type Ret a :: * 187 getl :: a -> a -> SBV.Symbolic (Ret a, Ret a) 188 189 instance (Instantiateable a r, Sizeable b) => Sizeable (Arr E a b) where 190 type Ret (Arr E a b) = Ret b 191 getl f g = do 192 liftIO $ putStrLn " -> x" 193 x <- instantiate (undefined :: a) 194 let f' = unE $ f $ E x 195 let g' = unE $ g $ E x 196 getl f' g' 197 198 instance Sizeable (SBV.SInteger) where 199 type Ret SBV.SInteger = SBV.SInteger 200 getl f g = return (f,g) 201 202 getEq f g = SBV.proveWith (SBV.z3 {SBV.verbose=True}) $ do 203 (x,y) <- getl (unE f) (unE g) 204 return $ x SBV..== y -
sizechecking_branches/LL.hs
r10 r15 1 {-# Language GADTs, 2 FlexibleInstances, 3 FlexibleContexts, 4 ScopedTypeVariables, 5 TypeFamilies, 1 {-# Language GADTs, 2 FlexibleInstances, 3 FlexibleContexts, 4 ScopedTypeVariables, 5 TypeFamilies, 6 6 NoMonomorphismRestriction, 7 7 OverlappingInstances #-} 8 module LL where 8 9 9 10 import Data.Char … … 14 15 deriving Show 15 16 16 type family Arr (repr :: * -> *) (a :: *) (b :: *) :: *17 17 18 18 class Lambda l where 19 type Arr l (a :: *) (b :: *) :: * 19 20 labs :: (l a -> l b) -> l (Arr l a b) 20 21 app :: l (Arr l a b) -> l a -> l b … … 49 50 50 51 newtype LPrint a = LPrint { unPrint :: Int -> Int -> ShowS } 51 type instance Arr LPrint a b = a -> b52 52 53 53 instance Lambda LPrint where 54 type Arr LPrint a b = a -> b 54 55 lit x = LPrint $ \_ -> return $ shows x 55 56 op m opc n = LPrint $ \p -> do … … 75 76 {- Evaluating -} 76 77 newtype R a = R { unR :: a } 77 type instance Arr R a b = R a -> R b78 78 79 79 instance Lambda R where 80 type Arr R a b = R a -> R b 80 81 labs = R 81 82 app = unR … … 94 95 eval = unR 95 96 96 z = labs ( \s -> s + 1) `app` ( 1 + lit2)97 z = labs (\s -> s + lit 1) `app` (lit 1 + 2)
Note: See TracChangeset
for help on using the changeset viewer.