Changeset 15 for sizechecking

Timestamp:

Nov 16, 2012, 4:26:26 PM (13 years ago)

Author:

gobi

Message:

new solver

Location:

sizechecking

Files:

• Constraints.hs (modified) (7 diffs)
• Lambda.hs (modified) (1 diff)

sizechecking/Constraints.hs

@@ -1 +1 @@
 {-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,
              IncoherentInstances, RankNTypes, ScopedTypeVariables,
-             FlexibleContexts,UndecidableInstances #-}
+             FlexibleContexts,UndecidableInstances, DeriveDataTypeable,
+             ImpredicativeTypes #-}
 module Constraints where
 
@@ -12 +13 @@
 import Data.SBV ( (.==), (.<), (.>=))
 import Control.Monad
+import Control.Monad.IO.Class
 import Data.IORef()
 import Data.Supply as S
+import Data.Data
+import Data.IORef
+import Data.Dynamic
 
 asType :: a -> a -> a
@@ -37 +42 @@
 appall :: Int -> [L] -> L
 appall var = foldl App (Var var)
-
 
 data Condition = Condition [Constraint] L L
@@ -253 +257 @@
 
     solve1' supp c@(Condition d a b)
-        | checkConds d = do
-            putStrLn "Contradiction in preconditions"
-            return []
+--        | checkConds d = do
+--            putStrLn "Contradiction in preconditions"
+--            return []
         | a==b = do
             putStrLn "Equals"
             return []
-        | Just (var, nl) <- searchzero d = do
-            let x = Condition (Prelude.map (normalizec.substc var (Num 0)) nl)
-                        (normalize$subst var (Num 0) a)
-                        (normalize$subst var (Num 0) b)
-
-            putStrLn $ show (Var var) ++ " is zero:\n" ++ show x
-            solve1 supp x 
-        | Just (var, exp, nl) <- searcheq d [] = do
-            putStrLn $ "Found equation " ++ show (Var var) ++ " = " ++ show exp
-            let x = Condition (Prelude.map (normalizec.substc var exp) nl )
-                        (normalize$subst var exp a)
-                        (normalize$subst var exp b)
-            putStrLn $ "New equations:\n" ++ show x
-            solve1 supp x 
+--        | Just (var, nl) <- searchzero d = do
+--            let x = Condition (Prelude.map (normalizec.substc var (Num 0)) nl)
+--                        (normalize$subst var (Num 0) a)
+--                        (normalize$subst var (Num 0) b)
+--
+--            putStrLn $ show (Var var) ++ " is zero:\n" ++ show x
+--            solve1 supp x 
+--        | Just (var, exp, nl) <- searcheq d [] = do
+--            putStrLn $ "Found equation " ++ show (Var var) ++ " = " ++ show exp
+--            let x = Condition (Prelude.map (normalizec.substc var exp) nl )
+--                        (normalize$subst var exp a)
+--                        (normalize$subst var exp b)
+--            putStrLn $ "New equations:\n" ++ show x
+--            solve1 supp x 
         | App p q <- a, App r s <- b = do
             putStrLn "Branching!"
             nc <- checkCond supp [Condition d p r, Condition d q s] 
             solve nc supp
-
 
 --        | Abs _ _ <- a, Abs _ _ <- b = do
@@ -288 +291 @@
 --        | Abs  _ _   <- a, AAbs _ _ _ <- b = applyList a b d supp
 --        | AAbs _ _ _ <- a, AAbs _ _ _ <- b = applyList a b d supp
-        | Just dd <- reorder d = do
-            putStrLn $ "Reorder " ++ show dd
-            solve1 supp $ Condition dd a b
+
+--        | Just dd <- reorder d = do
+--            putStrLn $ "Reorder " ++ show dd
+--            solve1 supp $ Condition dd a b
         | otherwise = do
             putStrLn "Tying to call solver"
@@ -300 +304 @@
                 otherwise -> return [c]
 
+data LU = LU deriving (Eq, Ord, Data, Typeable)
+instance SBV.SymWord LU
+instance SBV.HasKind LU
+
 fvc (Zero a)  = fv a
 fvc (LTC a b) = fv a `Set.union` fv b
@@ -306 +314 @@
 compiletosolver :: L -> L -> [Constraint] -> SBV.Symbolic SBV.SBool
 compiletosolver a b d = do
-    let fvs = Set.toList $ Set.unions $ fv a : fv b : map fvc d
-    (vars::[SBV.SInteger]) <- mapM (SBV.free . flip showVar "") fvs
-    let varmap = Map.fromList $ zip fvs vars
-    mapM_ (SBV.constrain . compilec varmap) d
-    return $ compilel varmap a .== compilel varmap b
-
-compilec v (Zero a)  = compilel v a .== (0::SBV.SInteger)
-compilec v (LTC a b) = compilel v a .<  compilel v b
-compilec v (GEC a b) = compilel v a .>= compilel v b
-
-compilel :: Map.Map Int SBV.SInteger -> L -> SBV.SInteger
-compilel v (Op a c b) = case c of 
+    varmap <- liftIO createVarPool
+    expmap <- liftIO createExpPool
+    supply  <- liftIO $ newNumSupply
+    let (s1,s2,s3,s4) = split4 supply
+    cs <- mapM (\(s,x) -> compilec varmap expmap s x) $ zip (split s1) d
+    mapM_ (SBV.constrain) cs
+    lhs <- compilel varmap expmap s3 a
+    rhs <- compilel varmap expmap s4 b
+    return $ lhs .== rhs
+
+data VarT = VarI | VarF VarT VarT
+type VarPool = IORef (Map.Map Int Dynamic)
+type ExpPool = IORef (Map.Map L SBV.SInteger)
+
+createVarPool :: IO (VarPool)
+createVarPool = newIORef $ Map.empty
+createExpPool :: IO (ExpPool)
+createExpPool = newIORef $ Map.empty
+
+
+sbvTc :: TyCon
+sbvTc = mkTyCon3 "Data" "SBV" "SBV"
+
+instance (Typeable t) => Typeable (SBV.SBV t) where
+  typeOf x = mkTyConApp sbvTc [typeOf (get x)]
+    where
+      get :: SBV.SBV a -> a
+      get = undefined
+
+
+getVarSymbol :: VarPool -> (SBV.Symbolic Dynamic) -> Int -> SBV.Symbolic Dynamic
+getVarSymbol pool factory a = do
+  v <- liftIO $ readIORef pool
+  case Map.lookup a v of
+    Just q -> return $ q
+    Nothing -> do
+      dx <- factory
+      let newmap = Map.insert a dx v
+      liftIO $ writeIORef pool newmap
+      return dx
+
+getExpSymbol :: ExpPool -> (SBV.Symbolic SBV.SInteger) -> L -> SBV.Symbolic SBV.SInteger
+getExpSymbol pool factory a = do
+  v <- liftIO $ readIORef pool
+  case Map.lookup a v of
+    Just q -> return $ q
+    Nothing -> do
+      dx <- factory
+      let newmap = Map.insert a dx v
+      liftIO $ writeIORef pool newmap
+      return dx
+
+
+compilec :: VarPool -> ExpPool -> Supply Int -> Constraint -> SBV.Symbolic (SBV.SBool)
+compilec v e s (Zero a)  = do
+  lhs <- compilel v e s a
+  return $ lhs .== (0::SBV.SInteger)
+
+compilec v e s (LTC a b) = do
+  let (s1,s2) = split2 s 
+  lhs <- compilel v e s1 a
+  rhs <- compilel v e s2 b
+  return $ lhs .< rhs
+
+compilec v e s (GEC a b) = do
+  let (s1,s2) = split2 s 
+  lhs <- compilel v e s1 a
+  rhs <- compilel v e s2 b
+  return $ lhs .>= rhs
+
+class Typeable a => VarFactory a where
+  createDyn :: String -> a -> SBV.Symbolic Dynamic
+  createDyn a n = do
+    x <- createVar a n
+    return $ toDyn x
+  createVar :: String -> a -> SBV.Symbolic a
+
+instance VarFactory SBV.SInteger where
+  createVar n _ = SBV.free n
+
+compilel :: VarPool -> ExpPool -> Supply Int -> L -> SBV.Symbolic (SBV.SInteger)
+compilel v e s (Op a c b) = do
+  let (s1, s2) = split2 s
+  al <- compilel v e s1 a
+  bl <- compilel v e s1 b
+  return $ case c of
     '+' -> al + bl
     '-' -> al - bl
     '*' -> al * bl
     '/' -> al `SBV.sDiv` bl
-    where
-    al = compilel v a
-    bl = compilel v b
-compilel v (Var a) | Just x<-Map.lookup a v = x
-compilel v (Num a) = SBV.literal $ fromIntegral a
-compilel v a = error $ "Cannot compile " ++ show a
+compilel v e s (Var a)   = do
+  let itype = (undefined ::SBV.SInteger)
+  sym <- getVarSymbol v (createDyn (showVar a "") itype) a
+  let var = (fromDynamic sym) :: Maybe SBV.SInteger
+  case var of
+      Just x -> return x
+      Nothing -> do
+        error "Type Error"
+compilel v e s (Num a)   = return $ SBV.literal $ fromIntegral a
+compilel v e s (Bottom)  = SBV.free_
+compilel v e s l = do
+    sym <- getExpSymbol e (return $ SBV.uninterpret ("unint" ++ showVar (supplyValue s) "") ) l
+    return sym
+--compilel v e x         = error $  "Cannot compile "++ show x
+
+gettype :: ((b -> t) -> t) -> a -> b -> a
+gettype = error "???"
+
+{-
+compileapp :: (VarFactory b, SBV.Uninterpreted (b -> SBV.SInteger)) => VarPool -> L -> ((b -> t) -> t) -> SBV.Symbolic (SBV.SInteger)
+compileapp v (Var a) f = do
+  let itype = (error :: SBV.SInteger)
+  sym <- getVarSymbol v (createDyn (showVar a "") (gettype f itype)) a
+  let var = (fromDynamic sym) :: Maybe SBV.SInteger
+  case var of
+      Just x -> return x
+      Nothing -> do
+        error "Type Error"
+-}
+compileapp v (App x y) t = error $ "Not yet implemented."
+

sizechecking/Lambda.hs

@@ -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
     | Shift L L L | Unsized | Bottom 
-    deriving Eq
+    deriving (Eq, Ord)
 
 showVar x = if x>28