Changeset 15


Ignore:
Timestamp:
Nov 16, 2012, 4:26:26 PM (13 years ago)
Author:
gobi
Message:

new solver

Files:
2 added
4 edited

Legend:

Unmodified
Added
Removed

  • sizechecking/Constraints.hs

    r14 r15  
    11{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, 
    22             IncoherentInstances, RankNTypes, ScopedTypeVariables, 
    3              FlexibleContexts,UndecidableInstances #-} 
     3             FlexibleContexts,UndecidableInstances, DeriveDataTypeable, 
     4             ImpredicativeTypes #-} 
    45module Constraints where 
    56 
    … …  
    1213import Data.SBV ( (.==), (.<), (.>=)) 
    1314import Control.Monad 
     15import Control.Monad.IO.Class 
    1416import Data.IORef() 
    1517import Data.Supply as S 
     18import Data.Data 
     19import Data.IORef 
     20import Data.Dynamic 
    1621 
    1722asType :: a -> a -> a 
    … …  
    3742appall :: Int -> [L] -> L 
    3843appall var = foldl App (Var var) 
    39  
    4044 
    4145data Condition = Condition [Constraint] L L 
    … …  
    253257 
    254258    solve1' supp c@(Condition d a b) 
    255         | checkConds d = do 
    256             putStrLn "Contradiction in preconditions" 
    257             return [] 
     259--        | checkConds d = do 
     260--            putStrLn "Contradiction in preconditions" 
     261--            return [] 
    258262        | a==b = do 
    259263            putStrLn "Equals" 
    260264            return [] 
    261         | Just (var, nl) <- searchzero d = do 
    262             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 x 
    267             solve1 supp x  
    268         | Just (var, exp, nl) <- searcheq d [] = do 
    269             putStrLn $ "Found equation " ++ show (Var var) ++ " = " ++ show exp 
    270             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 x 
    274             solve1 supp x  
     265--        | 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  
    275279        | App p q <- a, App r s <- b = do 
    276280            putStrLn "Branching!" 
    277281            nc <- checkCond supp [Condition d p r, Condition d q s]  
    278282            solve nc supp 
    279  
    280283 
    281284--        | Abs _ _ <- a, Abs _ _ <- b = do 
    … …  
    288291--        | Abs  _ _   <- a, AAbs _ _ _ <- b = applyList a b d supp 
    289292--        | 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 
    293297        | otherwise = do 
    294298            putStrLn "Tying to call solver" 
    … …  
    300304                otherwise -> return [c] 
    301305 
     306data LU = LU deriving (Eq, Ord, Data, Typeable) 
     307instance SBV.SymWord LU 
     308instance SBV.HasKind LU 
     309 
    302310fvc (Zero a)  = fv a 
    303311fvc (LTC a b) = fv a `Set.union` fv b 
    … …  
    306314compiletosolver :: L -> L -> [Constraint] -> SBV.Symbolic SBV.SBool 
    307315compiletosolver 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 
     326data VarT = VarI | VarF VarT VarT 
     327type VarPool = IORef (Map.Map Int Dynamic) 
     328type ExpPool = IORef (Map.Map L SBV.SInteger) 
     329 
     330createVarPool :: IO (VarPool) 
     331createVarPool = newIORef $ Map.empty 
     332createExpPool :: IO (ExpPool) 
     333createExpPool = newIORef $ Map.empty 
     334 
     335 
     336sbvTc :: TyCon 
     337sbvTc = mkTyCon3 "Data" "SBV" "SBV" 
     338 
     339instance (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 
     346getVarSymbol :: VarPool -> (SBV.Symbolic Dynamic) -> Int -> SBV.Symbolic Dynamic 
     347getVarSymbol 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 
     357getExpSymbol :: ExpPool -> (SBV.Symbolic SBV.SInteger) -> L -> SBV.Symbolic SBV.SInteger 
     358getExpSymbol 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 
     369compilec :: VarPool -> ExpPool -> Supply Int -> Constraint -> SBV.Symbolic (SBV.SBool) 
     370compilec v e s (Zero a)  = do 
     371  lhs <- compilel v e s a 
     372  return $ lhs .== (0::SBV.SInteger) 
     373 
     374compilec 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 
     380compilec 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 
     386class 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 
     393instance VarFactory SBV.SInteger where 
     394  createVar n _ = SBV.free n 
     395 
     396compilel :: VarPool -> ExpPool -> Supply Int -> L -> SBV.Symbolic (SBV.SInteger) 
     397compilel 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 
    320402    '+' -> al + bl 
    321403    '-' -> al - bl 
    322404    '*' -> al * bl 
    323405    '/' -> 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 
     406compilel 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" 
     414compilel v e s (Num a)   = return $ SBV.literal $ fromIntegral a 
     415compilel v e s (Bottom)  = SBV.free_ 
     416compilel 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 
     421gettype :: ((b -> t) -> t) -> a -> b -> a 
     422gettype = error "???" 
     423 
     424{- 
     425compileapp :: (VarFactory b, SBV.Uninterpreted (b -> SBV.SInteger)) => VarPool -> L -> ((b -> t) -> t) -> SBV.Symbolic (SBV.SInteger) 
     426compileapp 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-} 
     435compileapp v (App x y) t = error $ "Not yet implemented." 
     436 

  • sizechecking/Lambda.hs

    r12 r15  
    1313data L = Abs Int L | App L L | Var Int | Num Int | Op L Char L | List L L | AAbs Int Int L 
    1414    | Shift L L L | Unsized | Bottom  
    15     deriving Eq 
     15    deriving (Eq, Ord) 
    1616 
    1717showVar 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 #-} 
    22module L where 
    33 
     4import qualified Data.SBV as SBV 
    45import Data.Char(ord, chr) 
    56import Control.Monad.State 
    … …  
    1314type Arr repr a b = repr a -> repr b 
    1415 
    15 class Lambda l where 
     16class (Num (LInt l)) => Lambda l where 
     17    type LInt l :: * 
    1618    labs    :: (l a -> l b) -> l (Arr l a b) 
    1719    app     :: l (Arr l a b) -> l a -> l b 
    18     lit     :: Int -> l Int 
    19     op      :: l Int -> OpName -> l Int -> l Int 
     20    lit     :: (LInt l) -> l (LInt l) 
     21    op      :: l (LInt l) -> OpName -> l (LInt l) -> l (LInt l) 
    2022 
    2123class SizeExp l where 
    … …  
    2729    unsized :: l () 
    2830 
    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 
     31instance (Lambda l, LInt l ~ a) => Num (l a) where 
    3632    fromInteger = lit . fromIntegral 
    3733    lhs + rhs   = op lhs PLUS rhs 
    … …  
    4541 
    4642instance Lambda LPrint where 
     43  type LInt LPrint = Int 
    4744  lit x      = LPrint $ \_ -> return $ shows x 
    4845  op m opc n = LPrint $ \p -> do 
    … …  
    9996x = aabs (\s _ -> s) `app` list (lit 0) (labs $ \_ -> undef) 
    10097y = list 0 $ labs $ \_ -> undef 
    101 z = (labs $ \s -> s+1) `app` (lit 1+2) 
    10298conss = labs $ \x -> aabs $ \ys yf -> list (ys + 1) $ shift yf ys (labs $ \_ -> x) 
    10399concats = aabs $ \xs xf -> (aabs $ \ys yf -> list (xs+ys) $ shift xf xs yf) 
    … …  
    112108l12 = list (lit 1) (labs $ \_ -> list (lit 2) (labs $ \_ -> unsized)) 
    113109 
     110v = (labs $ \s -> s+1) `app` (lit 1+2) 
     111w1 = (labs $ \s -> s+ lit 1) 
     112w2 = (labs $ \s -> s+ lit 2) 
     113q1 :: (Lambda l, a ~ LInt l, Num (l a)) => l (Arr l b (Arr l a a)) 
     114q1 = (labs $ \q -> labs $ \s -> s + lit 1) 
     115q2 :: (Lambda l, a ~ LInt l, Num (l a)) => l (Arr l a (Arr l a a)) 
     116q2 = (labs $ \q -> labs $ \s -> s + q) 
     117q3 = (labs $ \q -> labs $ \s -> q + s) 
     118 
    114119{- Evaluating -} 
     120eval = unR 
    115121newtype R a = R { unR :: a } 
    116122instance Lambda R where 
    117   labs f      = R $ f  
     123  type LInt R = Int 
     124  labs f      = R $ f 
    118125  app e1 e2   = (unR e1) e2 
    119126  lit i       = R i 
    … …  
    136143  shift a s c = R $ \i -> if (unR i)<(unR s) then unR a i else unR c i 
    137144 
    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) 
     145newtype E a = E { unE :: a } 
     146instance 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 
     157class Sizeable' a where 
     158  getl' :: E (Arr E a b) -> SBV.Symbolic b 
     159 
     160instance Sizeable' (SBV.SInteger) where 
     161  getl' f = do 
     162    x <- SBV.sInteger "x" 
     163    return $ unE $ (unE f) $ E x 
     164 
     165{- 
     166getEq f = SBV.proveWith (SBV.z3 {SBV.verbose=True}) $ do 
     167  x <- getl f 
     168  return $ x SBV..== x 
     169-} 
     170data ST  = ST 
     171 
     172class Instantiateable a r | a -> r where 
     173  instantiate :: a -> SBV.Symbolic r 
     174 
     175instance Instantiateable SBV.SInteger SBV.SInteger where 
     176  instantiate _ = do 
     177    liftIO $ putStrLn " INT VARIABLE x" 
     178    SBV.sInteger "x" 
     179 
     180instance Instantiateable a ST where 
     181  instantiate _ = do 
     182    liftIO $ putStrLn " ? VARIABLE x" 
     183    return $ undefined -- SBV.uninterpret "f" 
     184 
     185class Sizeable a where 
     186  type Ret a :: * 
     187  getl :: a -> a -> SBV.Symbolic (Ret a, Ret a) 
     188 
     189instance (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 
     198instance Sizeable (SBV.SInteger) where 
     199  type Ret SBV.SInteger = SBV.SInteger 
     200  getl f g = return (f,g) 
     201 
     202getEq 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, 
    66        NoMonomorphismRestriction, 
    77        OverlappingInstances #-} 
     8module LL where 
    89 
    910import Data.Char 
    … …  
    1415  deriving Show 
    1516 
    16 type family Arr (repr :: * -> *) (a :: *) (b :: *) :: * 
    1717 
    1818class Lambda l where 
     19    type Arr l (a :: *) (b :: *) :: * 
    1920    labs    :: (l a -> l b) -> l (Arr l a b) 
    2021    app     :: l (Arr l a b) -> l a -> l b 
    … …  
    4950 
    5051newtype LPrint a = LPrint { unPrint :: Int -> Int -> ShowS } 
    51 type instance Arr LPrint a b = a -> b 
    5252 
    5353instance Lambda LPrint where 
     54  type Arr LPrint a b = a -> b 
    5455  lit x      = LPrint $ \_ -> return $ shows x 
    5556  op m opc n = LPrint $ \p -> do 
    … …  
    7576{- Evaluating -} 
    7677newtype R a = R { unR :: a } 
    77 type instance Arr R a b = R a -> R b 
    7878 
    7979instance Lambda R where 
     80  type Arr R a b = R a -> R b 
    8081  labs        = R 
    8182  app         = unR 
    … …  
    9495eval = unR 
    9596 
    96 z = labs ( \s -> s + 1) `app` ( 1 + lit 2) 
     97z = labs (\s -> s + lit 1) `app` (lit 1 + 2) 
Note: See TracChangeset for help on using the changeset viewer.