Index: zechecking/Constraints.hs =================================================================== --- /sizechecking/Constraints.hs (revision 17) +++ (revision ) @@ -1,440 +1,0 @@ --- --- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking --- - -{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, - IncoherentInstances, RankNTypes, ScopedTypeVariables, - FlexibleContexts,UndecidableInstances, DeriveDataTypeable, - ImpredicativeTypes #-} -module Constraints where - -import Lambda -import qualified Data.List as List -import qualified Data.Set as Set -import qualified Data.Map as Map -import qualified Data.Ord as Ord -import qualified Data.SBV as SBV -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 -asType a _ = a - -data D = D { var::Int, cond::[Condition] } - -data TypeKind = V | L TypeKind | F TypeKind TypeKind | U - deriving Show - - -class TS a where - tk :: a -> TypeKind -instance (TS a, TS b) => TS (a -> b) where - tk _ = F (tk (undefined :: a)) (tk (undefined :: b)) -instance TS a => TS [a] where - tk _ = L (tk (undefined :: a)) -instance TS a where - tk _ = V -instance TS Int where - tk _ = U - -appall :: Int -> [L] -> L -appall var = foldl App (Var var) - -data Condition = Condition [Constraint] L L - -instance Show Condition where - showsPrec _ (Condition d a b) = shows d . showString "|- " . shows a . showString " = " . shows b - showList [] = showString "" - showList [x] = shows x - showList (x:xs) = shows x . showString "\n" . shows xs - -data Constraint = Zero L | LTC L L | GEC L L - deriving Eq - -instance Show Constraint where - showList [] = id - showList [s] = shows s . showChar ' ' - showList (x:xs) = shows x . showString ", " . shows xs - showsPrec _ (Zero s) = shows s . showString " = 0" - showsPrec _ (LTC s1 s2) = shows s1 . showString " < " . shows s2 - showsPrec _ (GEC s1 s2) = shows s1 . showString " >= " . shows s2 - -normalize :: L -> L -normalize l = delzero $ foldl (\a b -> Op a '-' b) (foldl (\a b -> Op a '+' b) (f1 $ List.sortBy (Ord.comparing snd) a) c) d - where - (a,b,c,d) = norm l - f1 ((0,l):xs) = f1 xs - f1 ((1,l):xs) = Op (f1 xs) '+' (Var l) - f1 ((-1,l):xs) = Op (f1 xs) '-' (Var l) - f1 [] = Num b - - delzero (Op (Num 0) '+' b) = b - delzero (Op a c b) = Op (delzero a) c b - delzero l = l - -gnormalize :: L -> (L, Int) -gnormalize l = case (c,d) of - ([], []) -> case nonzero of - [] -> (Num 0, b) - _ -> (expr, b) - (_, _) -> error $ "Expression in condition" ++ show c - where - nonzero = List.sortBy (Ord.comparing snd) $ filter ((/=0).fst) a - proc (1, l) = Var l - proc (-1, l) = Op (Num (-1)) '*' (Var l) - t :: L -> (Int, Int) -> L - t l (1, var) = Op l '+' (Var var) - t l (-1, var) = Op l '-' (Var var) - expr = foldl t (proc $ head nonzero) (tail nonzero) - - (a,b,c,d) = norm l - -normalizec :: Constraint -> Constraint -normalizec (Zero l) = Zero $ normalize l -normalizec (LTC a b) = LTC (normalize a) (normalize b) -normalizec (GEC a b) = GEC (normalize a) (normalize b) ---normalizec (LTC a b) = LTC x (Num (-y)) --- where (x,y) = gnormalize $ Op a '-' b ---normalizec (GEC a b) = GEC x (Num (-y)) --- where (x,y) = gnormalize $ Op a '-' b - -normalizecs :: [Constraint] -> [Constraint] -normalizecs = normalizecs' . Prelude.map normalizec - where - normalizecs' [] = [] - normalizecs' (x:xs) = x:normalizecs' (filter (/=x) xs) - -{- - - Takes an extended lambda expression and - -} -norm :: L -> ([(Int, Int)], Int, [L], [L]) -norm (App a b) = ([], 0, [App (normalize a) (normalize b)], []) -norm (List a b) = ([], 0, [List (normalize a) (normalize b)], []) -norm (AAbs a b e) = ([], 0, [AAbs a b (normalize e)], []) -norm (Shift a b c) = ([], 0, [Shift (normalize a) (normalize b) (normalize c)], []) -norm (Unsized) = ([], 0, [Unsized], []) -norm (Bottom) = ([], 0, [Bottom], []) -norm (Abs i l) = ([], 0, [Abs i $ normalize l], []) -norm (Var i) = ([(1, i)], 0, [], []) -norm (Num i) = ([], i, [], []) -norm q@(Op a c b) = case c of - '+' -> (a1++b1, a2+b2, a3++b3, a4++b4) - '-' -> (sub a1 b1, a2-b2, a3++b4, a4++b3) - '*' -> case a of - (Num cnt) -> (map (mul cnt) b1, cnt*b2, map (Op (Num cnt) '*') b3, map (Op (Num cnt) '*') b4) - _ -> ([], 0, [q], []) - _ -> ([], 0, [q], []) - where - mul c (x,var) = (c*x, var) - (a1, a2, a3, a4) = norm a - (b1, b2, b3, b4) = norm b - sub l1 ((c,i):xs) = sub (sub' l1 c i) xs - where - sub' [] c i = [(-c, i)] - sub' ((cc,ii):xs) c i = if i==ii then (cc-c,i):xs else (cc,ii):sub' xs c i - sub l1 [] = l1 - -tnorm = Op (Num 1) '+' (Op (Var 0) '-' (Num 1)) - -checkCond :: Supply Int -> [Condition] -> IO [Condition] -checkCond v l = do - ll <- mapM (checkCond1 v) l - return $ concat ll - - where --- checkCond1 v p@(Condition d a b) | a==b = do --- return [] - checkCond1 v z@(Condition d (List a b) (List p q)) = do --- i <- freshtypevar v - let (v1,v2,v3) = split3 v - let i = supplyValue v1 - let b' = rall $ App b (Var i) - let q' = rall $ App q (Var i) - l1 <- checkCond1 v2 (Condition ((Var i `GEC` Num 0):d) a p) - l2 <- checkCond1 v3 (Condition ((Var i `GEC` Num 0):(Var i `LTC` a):(Var i `LTC` p):d) b' q') - return $ l1++l2 - checkCond1 v z@(Condition d (App (Shift e f g) h) x) = do - let (v1,v2,v3) = split3 v - let e' = rall $ App e h - let g' = rall $ App g $ Op h '-' f - l1 <- checkCond1 v1 (Condition ((h `LTC` f):d) e' x) - l2 <- checkCond1 v2 (Condition ((h `GEC` f):d) g' x) --- putStrLn $ " -> " ++ show l1 --- putStrLn $ " -> " ++ show l2 - return $ l1 ++ l2 - checkCond1 v z@(Condition d (App (Var a) x) (App (Var b) y)) | a==b = - checkCond1 v (Condition d x y) - checkCond1 v p@(Condition d x z@(App (Shift e f g) h)) = - checkCond1 v (Condition d z x) - checkCond1 v z@(Condition d a b) = return [Condition dd (normalize a) (normalize b)] - where - dd = normalizecs d - -subst ndl hst (App a b) = App (subst ndl hst a) (subst ndl hst b) -subst ndl hst (List a b) = List (subst ndl hst a) (subst ndl hst b) -subst ndl hst (AAbs a b e) = AAbs a b (subst ndl hst e) -subst ndl hst (Shift a b c) = Shift (subst ndl hst a) (subst ndl hst b) (subst ndl hst c) -subst ndl hst (Unsized) = Unsized -subst ndl hst (Bottom) = Bottom -subst ndl hst q@(Abs i l) = if ndl==i then q else Abs i $ subst ndl hst l -subst ndl hst q@(Var i) = if ndl==i then hst else q -subst ndl hst (Num i) = Num i -subst ndl hst (Op a c b) = Op (subst ndl hst a) c (subst ndl hst b) - -substc ndl hst (Zero l) = Zero $ subst ndl hst l -substc ndl hst (LTC a b) = LTC (subst ndl hst a) (subst ndl hst b) -substc ndl hst (GEC a b) = GEC (subst ndl hst a) (subst ndl hst b) - -reorder cs = if any check cs - then Just (map r cs) - else Nothing - where - check (Zero _) = False - check (LTC a (Num 0)) = False - check (GEC a (Num 0)) = False - check _ = True - r (LTC a b) = LTC (normalize (Op a '-' b)) (Num 0) - r (GEC a b) = GEC (normalize (Op a '-' b)) (Num 0) - r l = l - -solve :: [Condition] -> Supply Int -> IO [Condition] -solve l supply = do - ll <- forM (zip l $ split supply) (\(c,s) -> do - putStrLn $ "\nSOLVING " ++ show c - solve1 s c - ) - return $ concat ll - where - - searchzero (Zero (Var a):xs) = Just (a,xs) - searchzero (x:xs) = do - (a,l) <- searchzero xs - return (a,x:l) - searchzero [] = Nothing - - - searcheq (q@(GEC (Var var) exp):xs) prev = case findeq (List.reverse prev ++ xs) [] of - Nothing -> searcheq xs (q:prev) - l -> l - where - expinc = normalize $ Op exp '+' $ Num 1 - findeq [] _ = Nothing - findeq (LTC (Var var2) exp2:xs) prev2 | var==var2 && exp2==expinc = Just (var, exp, List.reverse prev2 ++ xs) - findeq (x:xs) prev2 = findeq xs (x:prev2) - - searcheq (x:xs) prev = searcheq xs (x:prev) - searcheq [] _ = Nothing - - checkConds [] = False - checkConds (LTC a b : xs) | GEC a b `elem` xs = True - checkConds (GEC a b : xs) | LTC a b `elem` xs = True - checkConds (LTC a (Num b) : xs) | b<=0 && elem (Zero a) xs = True - checkConds (GEC a (Num b) : xs) | b>0 && elem (Zero a) xs = True - checkConds (_:xs) = checkConds xs - - checkConds2 (LTC (Num a) (Num b):xs) | a>=b = Nothing - checkConds2 (LTC (Num a) (Num b):xs) | a=b = checkConds2 xs - checkConds2 (x:xs) = do { y <- checkConds2 xs; return (x:y) } - checkConds2 [] = Just [] - --- applyList a b d supp = do --- let (s1,s2,s3) = split3 supp --- let t = fresh (L V) s1 --- let dd = (Condition d (rall $ App a t) (rall $ App b t)) --- putStrLn $ "Applying a fresh variable: "++(show t) ++"\n"++(show dd) --- x <- checkCond s2 [dd] >>= mapM (solve1 s3) --- return $ concat x - - solve1 supp c@(Condition d a b) = case checkConds2 d of - Nothing -> do - putStrLn "Contradiction in preconditions" - return [] - Just d' -> solve1' supp $ Condition d a b - - solve1' supp c@(Condition d a b) --- | 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 - | 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 --- let (s1, s2) = split2 supp --- let t = fresh (tk a) s1 --- let dd= (Condition d (rall $ App a t) (rall $ App b t)) --- putStrLn $ "Applying a fresh variable: "++(show t) ++"\n"++(show dd) --- solve1 s2 dd --- | AAbs _ _ _ <- a, Abs _ _ <- b = applyList a b d supp --- | 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 - | otherwise = do - putStrLn "Tying to call solver" - let x = compiletosolver a b d - y <- SBV.prove x - print y - case y of - (SBV.ThmResult (SBV.Unsatisfiable _)) -> return [] - 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 -fvc (GEC a b) = fv a `Set.union` fv b - -compiletosolver :: L -> L -> [Constraint] -> SBV.Symbolic SBV.SBool -compiletosolver a b d = do - 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 -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." - Index: zechecking/Examples.hs =================================================================== --- /sizechecking/Examples.hs (revision 17) +++ (revision ) @@ -1,279 +1,0 @@ --- --- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking --- - -{-# LANGUAGE ScopedTypeVariables, ExistentialQuantification, Rank2Types #-} -module Examples where - -import Lambda -import SizedExp -import Constraints() -import Prelude ( ($), (+), (-), Int, (==), (*), (<), (>), (<=), (>=), (/=) ) -import qualified Prelude as P -import qualified Control.Monad as M -import qualified Data.List as List - -head :: (SizedExp se ) => Size se ([l] -> l) -head = bind headc body - where - body l = match l true P.const - -tail :: (SizedExp se ) => Size se ([l] -> [l]) -tail = bind tailc body - where body l = match l true (\_ xs -> xs) - -cons :: (SizedExp se) => Size se (x -> [x] -> [x]) -cons = bind conss true - -t3 :: (SizedExp se) => Size se ( (a -> a) -> a -> a ) -t3 = bind t3s body - where body f x = f `app` (f `app` (f `app` x)) - -nil :: (SizedExp se) => Size se [x] -nil = bind nils true - -map :: (SizedExp se) => Size se ( (a->b) -> [a] -> [b] ) -map = bind smap body - where body f l = match l nil - ( \x xs -> cons `app` (f `app` x) `app` (map `app` f `app` xs )) - -heads :: (SizedExp se) => Size se ( [[a]] -> [a] ) -heads = bind sheads $ \l -> map `app` head `app` l - -tails :: (SizedExp se) => Size se ( [[a]] -> [[a]] ) -tails = bind stails $ \l -> map `app` tail `app` l - -append :: (SizedExp se) => Size se ([a] -> [a] -> [a]) -append = bind appends body - where body l1 l2 = match l1 l2 - (\x xs -> cons `app` x `app` (append `app` xs `app` l2)) - -t27 :: (SizedExp se) => Size se ((a -> a) -> a -> a) -t27 = bind (App t3s t3s) $ t3 `app` t3 - -t27_ :: (SizedExp se) => Size se ((a -> a) -> a -> a) -t27_ = bind (App t3s t3s) $ - \f -> t3 `app` t3 `app` f - -t27__ :: (SizedExp se) => Size se ((a -> a) -> a -> a) -t27__ = bind (App t3s t3s) $ \f x -> - t3 `app` t3 `app` f `app` x - -pam :: (SizedExp se) => Size se ([a -> b] -> a -> [b]) -pam = bind (AAbs 1 2 $ Abs 3 $ List (Var 1) (Abs 4 $ App (App (Var 2) (Var 4)) (Var 3))) $ \fl x -> match fl nil - (\f fs -> cons `app` (f `app` x) `app` (pam `app` fs `app` x)) - -reverse :: (SizedExp se) => Size se([a] -> [a]) -reverse = bind reverses $ \l -> match l - nil - ( - \x xs -> append `app` (reverse `app` xs) `app` (cons `app` x `app` nil) - ) - -addone :: (SizedExp se) => Size se ([P.Int] -> [P.Int]) -addone = bind addones $ \l -> cons `app` 1 `app` l - -add3 :: (SizedExp se) => Size se ([P.Int] -> [P.Int]) -add3 = bind (AAbs 0 1 $ List (Op (Var 0) '+' (Num 3)) (Var 1)) $ - \l -> t3 `app` addone `app` l - -add3_ :: (SizedExp se) => Size se ([P.Int] -> [P.Int]) -add3_ = bind (AAbs 0 1 $ List (Op (Var 0) '+' (Num 3)) (Var 1)) $ - t3 `app` addone - -t9_ :: (SizedExp se) => Size se ((a -> a) -> a -> a) -t9_ = bind ( Abs 0 $ App t3s (App t3s (Var 0))) $ - \f -> t3 `app` (t3 `app` f) - -t9 :: (SizedExp se) => Size se ((a -> a) -> a -> a) -t9 = bind ( Abs 0 $ App t3s (App t3s (Var 0))) $ - \f x -> t3 `app` (t3 `app` f) `app` x - -add27s :: L -add27s = AAbs 0 1 $ List (Op (Var 0) '+' (Num 27)) (Abs 2 Unsized) -add27 :: (SizedExp se) => Size se ([P.Int] -> [P.Int]) -add27 = bind add27s $ \x -> t27 `app` addone `app` x - - -zipWiths :: L -zipWiths = let q = App (Var 4) $ Op (Op (Var 5) '+' (Var 3)) '-' (Var 1) in - (Abs 0 $ AAbs 1 2 $ AAbs 3 4 $ List (Var 1) (Abs 5 $ App (App (Var 0) (App (Var 2) (Var 5))) q )) -zipWith :: (SizedExp se) => Size se ((a2 -> a1 -> a) -> [a2] -> [a1] -> [a]) -zipWith = bind zipWiths $ \f l1 l2 -> - match l1 - nil - ( - \x xs -> match l2 - true - ( - \y ys -> cons `app` (f `app` x `app` y) `app` (zipWith `app` f `app` xs `app` ys) - ) - ) -appAll :: (SizedExp se) => Size se ( [a -> b] -> a -> [b] ) -appAll = bind (AAbs 0 1 $ Abs 2 $ List (Var 0) (Abs 3 $ Var 1 `App` Var 3 `App` Var 2 ) ) $ \fl x -> match fl - nil - ( - \f fs -> cons `app` (f `app` x) `app` (appAll `app` fs `app` x) - ) - -conspack :: (SizedExp se) => Size se (P.Int -> [P.Int] -> [P.Int]) -conspack = bind (Abs 0 $ AAbs 1 2 $ List (Op (Var 1) '+' (Num 1)) (Abs 3 Unsized)) $ \x l -> - match l (cons `app` x `app` l) - (\hd tl -> iff (x == hd) ( - cons `app` x `app` l - ) ( - cons `app` hd `app` (conspack `app` x `app` tl) - ) - ) - -cprod :: (SizedExp se) => Size se ([P.Int] -> [P.Int] -> [[P.Int]]) -cprod = known (AAbs 0 1 $ AAbs 2 3 $ List (Op (Var 0) '*' (Var 2)) $ Abs 4 $ List (Num 2) $ Abs 5 Unsized) - -sqdiff :: SizedExp se => Size se ([Int] -> [Int] -> [[Int]]) -sqdiff = bind (let sq l = Op l '*' l in AAbs 0 1 $ AAbs 2 3 $ List (sq $ Op (Var 0) '-' (Var 2)) $ Abs 4 $ List (Num 2) $ Abs 5 Unsized) $ - \l1 l2 -> match l1 (cprod `app` l2 `app` l2) - (\_ tl1 -> match l2 (cprod `app` l1 `app` l1) - (\_ tl2 -> sqdiff `app` tl1 `app` tl2)) - -replace :: SizedExp se => Size se (Int -> [Int] -> [Int]) -replace = bind (Abs 0 $ AAbs 1 2 $ List (Var 1) (Abs 3 Unsized)) $ - \x l -> match l nil (\hd tl -> cons `app` (x+hd) `app` tl) - -scalarProd :: (SizedExp se0) => Size se0 ([Int] -> [Int] -> [Int]) -scalarProd = bind (AAbs 0 1 $ AAbs 2 3 $ List (Num 1) (Abs 4 Unsized)) $ - \l1 l2 -> match l1 ( - match l2 ( cons `app` 0 `app` nil ) - (\_ _ -> true) - ) ( \hd1 tl1 -> - match l2 true - ( \hd2 tl2 -> replace `app` (hd1 * hd2) `app` (scalarProd `app` tl1 `app` tl2) ) - ) - -mlist :: SizedExp se => Size se (a -> [a -> x] -> [x]) -mlist = bind (Abs 0 $ AAbs 1 2 $ List (Var 1) (Abs 3 $ Var 2 `App` Var 3 `App` Var 0)) - $ \x l -> match l nil (\f fs -> cons `app` (f `app` x) `app` (mlist `app` x `app` fs)) - -strange :: (SizedExp se) => Size se ([Int] -> [Int]) -strange = bind (AAbs 0 1 $ List (Num 2) (Abs 2 Unsized)) $ \l1 -> - let b = match l1 nil (\x1 l2 -> match l2 nil (\x2 l3 -> cons `app` x2 `app` (cons `app` x1 `app` nil))) - in match b (cons `app` 0 `app` (cons `app` 0 `app` nil)) (\x xs -> b) - - -take4 :: SizedExp se => Size se (([a] -> [a]) -> [[a]]) -take4 = bind (Abs 0 $ List (Num 1) (Abs 2 (Var 0 `App` (Var 0 `App` List (Num 0) (Abs 1 Bottom))))) $ - \f ->cons `app` (f `app` (f `app` nil) ) `app` nil - - -merge :: SizedExp se => Size se ([Int] -> [Int] -> [Int]) -merge = bind (AAbs 0 1 $ AAbs 2 3 $ List (Op (Var 0) '+' (Var 2)) (Abs 4 Unsized))$ - \l1 l2 -> match l1 l2 ( - \x xs -> match l2 l1 ( - \y ys -> iff (x>y) (cons `app` x `app` (merge `app` xs `app` l2)) - (cons `app` y `app` (merge `app` l1 `app` ys)) - ) - ) - -split1 :: SizedExp se => Size se ([Int] -> [Int]) -split1 = bind (AAbs 0 1 $ List (Op (Op (Var 0) '+' (Num 1))'/' (Num 2)) (Abs 2 Unsized)) $ - \z -> match z nil (\y ys -> cons `app` y `app` (split2 `app` ys)) - -split2 :: SizedExp se => Size se ([Int] -> [Int]) -split2 = bind (AAbs 0 1 $ List (Op (Var 0) '/' (Num 2)) (Abs 2 Unsized)) $ - \z -> match z nil (\y ys -> split1 `app` ys) - -ms = AAbs 0 1 $ List (Var 0) (Abs 4 Unsized) -mergesort :: SizedExp se => Size se ([Int] -> [Int]) -mergesort = bind ms $ - \l -> match l nil (\x xs -> - merge `app` (mergesort `app` (split1 `app` l)) `app` (mergesort `app` (split2 `app` l)) - ) - -last :: SizedExp se => Size se ([a] -> a) -last = bind (AAbs 0 1 $ App (Var 1) (Num 0)) $ - \l -> match l true (\x xs -> match xs x (\_ _ -> last `app` xs)) - -charm :: SizedExp se => Size se (([a] -> [a]) -> a) -charm = bind (Abs 0 $ App (AAbs 2 3 $ App (Var 3) (Num 0)) (App (Var 0) (List (Num 0) $ Abs 1 Bottom))) $ - \ f -> last `app` (f `app` nil) - -fix :: SizedExp se => Size se ((a -> a) -> a) -fix = bind (Abs 2 $ App yComb (Var 2)) $ - \f -> f `app` (fix `app` f) - -transpose :: SizedExp se => Size se ([[a]] -> [[a]]) -transpose = bind transposec $ \l -> match l true $ - \l1 xss -> match l1 true $ - \x xs -> cons `app` (cons `app` x `app` (heads `app` xss)) - `app` (transpose `app` (cons `app` xs `app` (tails `app` xss))) -transposec = AAbs 18 5 $ List len fun - where - len = AAbs 19 6 (Var 19) `App` (Var 5 `App` Num 0) - fun = Abs 8 $ List (Var 18) (Abs 9 $ AAbs 19 6 (Var 6 `App` Var 8) `App` (Var 5 `App` Var 9)) - -comps = Abs 2 $ Abs 3 $ Abs 4 $ App (Var 2) (App (Var 3) (Var 4)) -comp :: (SizedExp se) => Size se ( (b->c) -> (a->b) -> a->c ) -comp = bind comps $ \f g x -> f `app` (g `app` x) - -test1s = Abs 2 $ AAbs 19 6 $ Var 2 `App` List (Var 19) (Var 6) -test1 :: (SizedExp se) => Size se (([a] -> [b]) -> [a] -> [b]) -test1 = bind test1s $ \f l -> match (f `app` l) nil (\x xs -> f `app` l) - - -test2s = Abs 2 $ AAbs 18 5 $ appends `App` (Var 2 `App` List (Var 18) (Var 5)) `App` - (appends `App` (Var 2 `App` List (Var 18) (Var 5)) `App` List (Var 18) (Var 5)) -test2 :: (SizedExp se) => Size se (([a] -> [a]) -> [a] -> [a]) -test2 = bind test2s $ \f l -> append `app` (f `app` l) `app` (append `app` (f `app` l) `app` l) - -data TestCase = forall a . TestCase P.String (forall se. SizedExp se => Size se a) - -tests :: [TestCase] -tests = [ - TestCase "append" append - , TestCase "reverse" reverse - , TestCase "heads" heads - , TestCase "map" map - , TestCase "pam" pam - , TestCase "head" head - , TestCase "tail" tail - , TestCase "t3" t3 - , TestCase "t9" t9 --- , TestCase "t9_" t9_ -- too few arguments in definition --- , TestCase "t27" t27 --- , TestCase "t27_" t27_ - , TestCase "t27__" t27__ - , TestCase "addone" addone - , TestCase "add3" add3 --- , TestCase "add3_" add3_ -- too few arguments in definition - , TestCase "add27" add27 - , TestCase "zipWith" zipWith - , TestCase "appAll" appAll - , TestCase "conspack" conspack - , TestCase "scalarProd" scalarProd - , TestCase "sqdiff" sqdiff - , TestCase "mlist" mlist - , TestCase "strange" strange - , TestCase "take4" take4 - , TestCase "charm" charm - , TestCase "comp" comp - , TestCase "merge" merge - , TestCase "split1" split1 - , TestCase "split2" split2 - , TestCase "mergesort" mergesort - ] - -runTests = do - failed <- M.forM tests $ \(TestCase name test) -> do - P.print " +++++++++++++++++++++++++++++++" - P.print $ " + Proving " P.++ name - P.print " +++++++++++++++++++++++++++++++" - - s <- prove test - M.return [name | P.not s] - - let f = P.concat failed - if List.null f then - P.putStrLn "All ok." - else do - P.putStr "\n\nFailed test cases: " - P.putStrLn $ List.intercalate ", " f - Index: zechecking/LICENSE =================================================================== --- /sizechecking/LICENSE (revision 17) +++ (revision ) @@ -1,30 +1,0 @@ -Copyright (c) 2012, Attila Gobi - -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - - * Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. - - * Redistributions in binary form must reproduce the above - copyright notice, this list of conditions and the following - disclaimer in the documentation and/or other materials provided - with the distribution. - - * Neither the name of Attila Gobi nor the names of other - contributors may be used to endorse or promote products derived - from this software without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT -OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, -SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT -LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, -DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY -THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. Index: zechecking/Lambda.hs =================================================================== --- /sizechecking/Lambda.hs (revision 17) +++ (revision ) @@ -1,238 +1,0 @@ --- --- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking --- - -module Lambda where - -{- - Ez a cikkben megadott lambda kalkulus egy implementacioja + redukcio + peldak. - - Hasznalat: lasd Lambda_proof.hs - - -} -import Data.List -import qualified Data.Set as Set -import Data.Char - -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, Ord) - -showVar x = if x>28 - then showVar (x `div` 29) . showChar (chr $ ord 'a' + (x `mod` 29)) - else showChar $ chr $ ord 'a' + x - -getPrec :: Char -> (Int,Int,Int) -getPrec '+' = (4,4,5) -getPrec '-' = (4,4,5) -getPrec '*' = (5,5,6) -getPrec '/' = (5,5,6) -getPrec c = error $ "Unknown operator "++[c] - -instance Show L where - showsPrec p (Abs s l) = showParen (p>0) $ showChar 'λ' . showVar s . showChar '.' . shows l - showsPrec p (AAbs f s l) = showParen (p>0) $ showChar 'Λ' . showVar f . showChar ',' . showVar s . showChar '.' . shows l - showsPrec p (App m n) = showParen (p>6) $ showsPrec 6 m . showChar ' ' . showsPrec 7 n - showsPrec _ (Var s) = showVar s - showsPrec _ (Num i) = shows i - showsPrec p (Op m op n) = showParen (p>prec) $ showsPrec lprec m . showChar op . showsPrec rprec n - where (prec,lprec,rprec)=getPrec op - showsPrec p (List s f) = showParen (p>0) $ showString "List " . showsPrec 9 s . showChar ' ' . showsPrec 9 f - showsPrec p (Shift e1 s e2) = showParen (p>0) $ showString "Shift " .showsPrec 2 e1 . - showChar ' ' . showsPrec 2 s . showChar ' ' . showsPrec 2 e2 - showsPrec _ Bottom = showChar '┮' - showsPrec _ Unsized = showChar 'U' - -t3s = Abs 1 $ Abs 0 $ App t (App t (App t x)) - where t = Var 1 - x = Var 0 - -subs (App x z) var exp = App (subs x var exp) (subs z var exp) -subs (List s f) var exp = List (subs s var exp) (subs f var exp) -subs (Shift e1 e2 e3) var exp = Shift (subs e1 var exp) (subs e2 var exp) (subs e3 var exp) -subs (Op x c z) var exp = Op (subs x var exp) c (subs z var exp) -subs e@(Var v) var exp | v==var = exp - | otherwise = e -subs x@(Abs v e) var exp | v==var = x - | otherwise = Abs v (subs e var exp) -subs x@(AAbs s f e) var exp | s==var||f==var = x - | otherwise = AAbs s f (subs e var exp) -subs x@(Num _) _ _ = x -subs x@Bottom _ _ = x -subs x@Unsized _ _ = x - - -alpha (App x z) from to = App (alpha x from to) (alpha z from to) -alpha (List x z) from to = List (alpha x from to) (alpha z from to) -alpha (Op x c z) from to = Op (alpha x from to) c (alpha z from to) -alpha (Shift x y z) from to = Shift (alpha x from to) (alpha y from to) (alpha z from to) -alpha e@(Var _) _ _ = e -alpha e@(Num _) _ _ = e -alpha e@Bottom _ _ = e -alpha e@Unsized _ _ = e -alpha (Abs v e) from to | v==from = Abs to (alpha' e from to) - | otherwise = Abs v (alpha e from to) -alpha (AAbs v1 v2 e) from to | v1==from = AAbs to v2 (alpha' e from to) - | v2==from = AAbs v1 to (alpha' e from to) - | otherwise = AAbs v1 v2 (alpha e from to) - -alpha' (App x z) from to = App (alpha' x from to) (alpha' z from to) -alpha' (List x z) from to = List (alpha' x from to) (alpha' z from to) -alpha' (Op x c z) from to = Op (alpha' x from to) c (alpha' z from to) -alpha' (Shift x y z) from to = Shift (alpha' x from to) (alpha' y from to) (alpha' z from to) -alpha' e@(Var v) from to | v==from = Var to - | otherwise = e -alpha' (Abs v e) from to | v==from = Abs to (alpha' e from to) - | otherwise = Abs v (alpha' e from to) -alpha' (AAbs v1 v2 e) from to | v1==from = AAbs to v2 (alpha' e from to) - | v2==from = AAbs v1 to (alpha' e from to) - | otherwise = AAbs v1 v2 (alpha' e from to) -alpha' x@(Num _) _ _ = x -alpha' x@Bottom _ _ = x -alpha' x@Unsized _ _ = x - -fv (Var x) = Set.singleton x -fv (App x y) = fv x `Set.union` fv y -fv (Op x _ y) = fv x `Set.union` fv y -fv (Abs v e) = v `Set.delete` fv e -fv (AAbs x y e) = x `Set.delete` ( y `Set.delete` fv e) -fv (List s e) = fv s `Set.union` fv e -fv (Num _) = Set.empty -fv (Shift e1 e2 e3) = fv e1 `Set.union` fv e2 `Set.union` fv e3 -fv Unsized = Set.empty -fv Bottom = Set.empty - -bv (Var _) = Set.empty -bv (App x y) = bv x `Set.union` bv y -bv (Op x _ y) = bv x `Set.union` bv y -bv (List x y) = bv x `Set.union` bv y -bv (Abs v e) = v `Set.insert` bv e -bv (AAbs v1 v2 e) = v1 `Set.insert` (v2 `Set.insert` bv e) -bv (Shift e1 e2 e3) = bv e1 `Set.union` bv e2 `Set.union` bv e3 -bv (Num _) = Set.empty -bv Unsized = Set.empty -bv Bottom = Set.empty - -maxv (Var x) = x -maxv (Num _) = 0 -maxv Unsized = 0 -maxv Bottom = 0 -maxv (App x y) = maxv x `max` maxv y -maxv (Op x _ y) = maxv x `max` maxv y -maxv (Shift x y z) = maxv x `max` maxv y `max` maxv z -maxv (List x y) = maxv x `max` maxv y -maxv (Abs v e) = v `max` maxv e -maxv (AAbs v1 v2 e) = v1 `max` v2 `max` maxv e - -rsubs oexp var exp = subs renamed var exp - where - dvar = fv exp `Set.intersection` bv oexp - m = maxv exp `max` maxv oexp - renames = zip (Set.toList dvar) [m+1..] - renamed = foldr rename oexp renames - rename (from,to) _ = alpha oexp from to - - -reduce (App (Abs var exp) z) = return $ rsubs exp var z -reduce (App (AAbs s f exp) (List s' f')) = return $ rsubs (App (Abs f exp) f') s s' -reduce (App e f) = case reduce e of - Just e' -> return $ App e' f - _ -> reduce f >>= \f' -> return $ App e f' -reduce (Abs v e) = reduce e >>= \e' -> return $ Abs v e' -reduce (Var _) = Nothing -reduce (Num _) = Nothing -reduce (List e f) = case reduce e of - Just e' -> return $ List e' f - _ -> reduce f >>= \f' -> return $ List e f' -reduce (AAbs v1 v2 e) = reduce e >>= \e' -> return $ AAbs v1 v2 e' -reduce Unsized = Nothing -reduce Bottom = Nothing -reduce (Shift e1 e2 e3) = case reduce e1 of - Just e' -> return $ Shift e' e2 e3 - _ -> case reduce e2 of - Just e' -> return $ Shift e1 e' e3 - _ -> reduce e3 >>= \e' -> return $ Shift e1 e2 e' -reduce (Op m c n) = case c of - '+' | (Num i, Num j) <- (m,n) -> return $ Num $ i+j - '-' | (Num i, Num j) <- (m,n) -> return $ Num $ i-j - '*' | (Num i, Num j) <- (m,n) -> return $ Num $ i*j - '+' | (Num 0) <- m -> reduce n - '+' | (Num 0) <- n -> reduce m - '*' | (Num 0) <- m -> return $ Num 0 - '*' | (Num 0) <- n -> return $ Num 0 - '*' | (Num 1) <- m -> reduce n - '*' | (Num 1) <- n -> reduce m - '-' | (Num 0) <- n -> reduce m - _ -> case reduce m of - Just m' -> return $ Op m' c n - _ -> reduce n >>= \n' -> return $ Op m c n' - -r :: Maybe L -> Maybe L -r x = x >>= reduce - -it f x = it' f (Just x) - where - it' _ Nothing = [] - it' f (Just x) = x:it' f (f x) - -rchain :: L -> [L] -rchain = it reduce - -pchain = putStrLn . intercalate "\n-> " . map show . rchain - -lplus = Abs m $ Abs n $ Abs f $ Abs x $ App (App (Var m) (Var f)) $ App (App (Var n) (Var f)) (Var x) - where [m,n,f,x] = [0..3] -lzero = Abs f $ Abs x $ Var x - where [f,x] = [0,1] -lsucc = Abs n $ Abs f $ Abs x $ App (Var f) $ App (App (Var n) (Var f)) (Var x) - where [n,f,x] = [0..2] -lone = last $ it reduce $ App lsucc lzero -ltwo = last $ it reduce $ App lsucc lone - -lpred = Abs n $ Abs f $ Abs x $ App (App (App (Var n) u1) (Abs u $ Var x)) (Abs u $ Var u) - where - u1 = Abs g $ Abs h $ App (Var h) $ App (Var g) (Var f) - [n,f,x,g,h,u] = [0..5] - -lsub = Abs m $ Abs n $ App (App (Var n) lpred) (Var m) - where (m,n) = (0,1) - -ltrue = Abs 0 $ Abs 1 $ Var 0 -lfalse = Abs 0 $ Abs 1 $ Var 1 - -liszero = Abs n $ App (App (Var n) (Abs x lfalse)) ltrue - where (n,x) = (0,1) - -land = Abs 0 $ Abs 1 $ App (App (Var 0) (Var 1)) (Var 1) -lleq = Abs 0 $ Abs 1 $ App liszero $ App (App lsub (Var 0)) (Var 1) -leq = Abs 0 $ Abs 1 $ App (App land l1) l2 - where - l1 = App (App lleq (Var 0)) (Var 1) - l2 = App (App lleq (Var 1)) (Var 0) - -test = Abs 0 $ Abs 1 $ App (App leq xpy) ypx -xpy = App (App lplus (Var 0)) (Var 1) -ypx = App (App lplus (Var 1)) (Var 0) - -smap = Abs 5 $ AAbs 18 6 $ List (Var 18) (Abs 8$ App (Var 5) (App (Var 6) (Var 8))) -conss = Abs 23 $ AAbs 19 5 $ List (Op (Num 1) '+' (Var 19)) $ Shift (Var 5) (Var 19) (Abs 8 $ Var 23) -addones = AAbs 19 5 $ List (Op (Num 1) '+' (Var 19)) (Abs 8 Unsized) -nils = List (Num 0) (Abs 8 Bottom) -lz n = List (Num n) (Abs 8 Unsized) -srep n x = List (Num n) (Abs 8 x) -dupfst = AAbs 19 5 $ List (Op (Num 1) '+' (Var 19)) $ Shift (Var 5) (Op (Var 19) '-' (Num 1)) - $ Abs 8 $ App (Var 5) (Op (Var 19) '-' (Num 1)) -yComb = Abs 18 $ App (Abs 22 $ App (Var 18) (App (Var 22) (Var 22))) (Abs 22 $ App (Var 18) (App (Var 22) (Var 22))) --- Λs,g.List s (λi.(λx.Λt,f.List (1+t) (Shift f (t-1) x)) U (g i)) -reverses = AAbs 18 5 $ List (Var 18) (Abs 8 $ App (Var 5) $ Op (Op (Var 18) '-' (Num 1)) '-' (Var 8) ) -reverse' l = case l of - [] -> [] - (x:xs) -> x:reverse' xs -appends = AAbs 18 5 $ AAbs 19 6 $ List (Op (Var 18) '+' (Var 19)) $ Shift (Var 6) (Var 19) (Var 5) - -headc = AAbs 18 5 $ App (Var 5) (Op (Var 18) '-' (Num 1)) -tailc = AAbs 18 5 $ List (Op (Var 18) '-' (Num 1)) (Var 5) -rall = last . it reduce - -sheads = rall $ App smap headc -stails = rall $ App smap tailc Index: zechecking/README.html =================================================================== --- /sizechecking/README.html (revision 17) +++ (revision ) @@ -1,89 +1,0 @@ - - - - - - - - - -

Prerequisites

-

You need at least version 2011.4.0.0 of the Haskell platform, an installed Z3 and the packages sbv and value-supply. If you have a working Haskell platform installed you can install value-supply by typing

-
cabal install value-supply sbv
-

Source files

-
-
Examples.hs
-
Some examples -
-
SizedExp.hs
-
Embedded language to prove size expressions -
-
Lambda.hs
-
Size expressions -
-
Constraints.hs
-
Constraint solver -
-
-

Using the examples

-
$ ghci Examples.hs
-GHCi, version 7.0.4: http://www.haskell.org/ghc/  :? for help
-Loading package ghc-prim ... linking ... done.
-Loading package integer-gmp ... linking ... done.
-Loading package base ... linking ... done.
-Loading package ffi-1.0 ... linking ... done.
-[1 of 4] Compiling Lambda           ( Lambda.hs, interpreted )
-[2 of 4] Compiling Constraints      ( Constraints.hs, interpreted )
-[3 of 4] Compiling SizedExp         ( SizedExp.hs, interpreted )
-[4 of 4] Compiling Main             ( Examples.hs, interpreted )
-Ok, modules loaded: Lambda, SizedExp, Constraints, Main.
-*Main>
-

Type "runTests" to run all test cases or type "prove map" to prove the function named map.

-

Under Windows

-

It is not perfect, and you will see a box after every special character, but at least it works.

- -

Introduction to Haskell syntax

-

Haskell syntax is very much like Clean, however there are some expressions you cannot find in Clean.

-

Backtick

-

Every haskell function can be used as infix operator. For example the following two expressions are the same.

-
func a b
-a `func` b
-

Dollar

-

Dollar sign is just explicit application (but with different precedence), so it can be used as a backward pipe operator. The following expressions are the same.

-
func (a b)
-func $ a b
-

The Embedded Language

-

As an example the function map is examined.

-
1 smap  = Abs 5 $ AAbs 18 6 $ List (Var 18) (Abs 8$ App (Var 5) (App (Var 6) (Var 8)))
-2 map :: (SizedExp se)  => Size se ( (a->b) -> [a] -> [b] )
-3 map = bind smap body
-4     where body f l = match l (nil)
-5             ( \x xs ->  cons `app` (f `app` x) `app` (map `app` f `app` xs ))
-

Here line 3 tells us map is a top-level binding, where the body of the function is defined in line 4--5 and its size expression is in line 1. Unfortunately the size expression language has not yet been embedded, so it is a bit difficult to read. Type smap in the GHC console to get a pretty printed form.

-
*Main> smap
-λf.Λs,g.List s (λi.f (g i))
-

The type of the function tells us the underlying type, ie. (a->b) -> [a] -> [b].

-

The body of map corresponds to the following expression

-
match l of
-   nil       -> nil
-   cons x xs -> cons (f x) (map f xs)
-

In the embedded language bind, match and app are supercombinators.

-
-
bind sexp exp
-

combines a size and an expression and creates a top-level binding

-
-
match list nilexp consexp
-

embedding of the match operator of our language to haskell

-
-
app exp1 exp2
-

embedding of the function application of our language to haskell

-
-
-

There is also a function called true to denote that we do not want to prove that branch.

- - Index: zechecking/README.txt =================================================================== --- /sizechecking/README.txt (revision 17) +++ (revision ) @@ -1,133 +1,0 @@ -Prerequisites -------------- - -You need at least version 2011.4.0.0 of the Haskell platform, an installed -[Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/) -and the packages `sbv` and `value-supply`. If you have a working Haskell platform installed you can -install value-supply by typing - - cabal install value-supply sbv - - -Source files ------------- - -Examples.hs - ~ Some examples -SizedExp.hs - ~ Embedded language to prove size expressions -Lambda.hs - ~ Size expressions -Constraints.hs - ~ Constraint solver - -Using the examples ------------------- - -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -$ ghci Examples.hs -GHCi, version 7.0.4: http://www.haskell.org/ghc/ :? for help -Loading package ghc-prim ... linking ... done. -Loading package integer-gmp ... linking ... done. -Loading package base ... linking ... done. -Loading package ffi-1.0 ... linking ... done. -[1 of 4] Compiling Lambda ( Lambda.hs, interpreted ) -[2 of 4] Compiling Constraints ( Constraints.hs, interpreted ) -[3 of 4] Compiling SizedExp ( SizedExp.hs, interpreted ) -[4 of 4] Compiling Main ( Examples.hs, interpreted ) -Ok, modules loaded: Lambda, SizedExp, Constraints, Main. -*Main> -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Type "`runTests`" to run all test cases or type "`prove map`" to prove the -function named map. - -Under Windows -------------- -It is not perfect, and you will see a box after every special character, but at -least it works. - - - Open a console by running the program `cmd` - - Issue the command `chcp 65001` - - In the console cd to the trunk directory - - Now, you can run `ghci Examples.hs` - - -Introduction to Haskell syntax ------------------------------- - -Haskell syntax is very much like Clean, however there are some expressions you -cannot find in Clean. - -### Backtick ### - -Every haskell function can be used as infix operator. For example the -following two expressions are the same. - -~~~~~~~~~~~ -func a b -a `func` b -~~~~~~~~~~~ - -### Dollar ### - -Dollar sign is just explicit application (but with different precedence), so it -can be used as a backward pipe operator. The following expressions are the -same. - -~~~~~~~~~~~~~~ -func (a b) -func $ a b -~~~~~~~~~~~~~~ - - -The Embedded Language ---------------------- - -As an example the function `map` is examined. - -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -1 smap = Abs 5 $ AAbs 18 6 $ List (Var 18) (Abs 8$ App (Var 5) (App (Var 6) (Var 8))) -2 map :: (SizedExp se) => Size se ( (a->b) -> [a] -> [b] ) -3 map = bind smap body -4 where body f l = match l (nil) -5 ( \x xs -> cons `app` (f `app` x) `app` (map `app` f `app` xs )) -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Here line 3 tells us map is a top-level binding, where the body of the function is -defined in line 4--5 and its size expression is in line 1. Unfortunately the -size expression language has not yet been embedded, so it is a bit difficult to -read. Type `smap` in the GHC console to get a pretty printed form. - -~~~~~~~~~~~~~~~~~ -*Main> smap -λf.Λs,g.List s (λi.f (g i)) -~~~~~~~~~~~~~~~~~ - -The type of the function tells us the underlying type, ie. `(a->b) -> [a] -> [b]`. - -The body of map corresponds to the following expression - -~~~~~~~~~~~~~~~~~~~~~~~ -match l of - nil -> nil - cons x xs -> cons (f x) (map f xs) -~~~~~~~~~~~~~~~~~~~~~~~ - - -In the embedded language `bind`, `match` and `app` are supercombinators. - -`bind sexp exp` - - : combines a size and an expression and creates a top-level binding - -`match list nilexp consexp` - - : embedding of the match operator of our language to haskell - -`app exp1 exp2` - - : embedding of the function application of our language to haskell - -There is also a function called `true` to denote that we do not want to prove that -branch. Index: zechecking/Setup.hs =================================================================== --- /sizechecking/Setup.hs (revision 17) +++ (revision ) @@ -1,6 +1,0 @@ --- --- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking --- - -import Distribution.Simple -main = defaultMain Index: zechecking/SizedExp.hs =================================================================== --- /sizechecking/SizedExp.hs (revision 17) +++ (revision ) @@ -1,174 +1,0 @@ -{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, - IncoherentInstances, RankNTypes, ScopedTypeVariables, - FlexibleContexts,UndecidableInstances #-} --- --- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking --- - -module SizedExp where - -import Lambda as L -import Constraints -import Data.Supply -import Control.Arrow -import Control.Monad - -class TS b => (Unify se a b) where - unify :: (forall a b c. (TS c, Unify se a b) => c -> (Size se c -> a) -> (Size se (c -> b), d)) -> - (b -> Size se b -> (Size se b, d)) -> - a -> (Size se b, d) - -instance (SizedExp se, Unify se a b, se~se1, c1~c2, TS c2) => Unify se (Size se1 c1->a) (c2->b) where - unify f g = f undefined - -instance (SizedExp se, se~se1, c1~c2, TS c2) => Unify se (Size se1 c1) c2 where - unify f g = g undefined - -class SizedExp (se :: * -> *) where - data Size se :: * -> * - true :: Size se x - known :: L -> Size se x - match :: Size se [l] -> Size se r -> (Size se l -> Size se [l] -> Size se r) -> Size se r - bind :: (Unify se a b) => L.L -> a -> Size se b - app :: Size se (a->b) -> Size se a -> Size se b - iff :: Bool -> Size se a -> Size se a -> Size se a - num :: Integer -> Size se Int - -instance Show (Size se a) where - show (==) = error "no show on Size!" -instance Eq (Size se a) where - (==) = undefined -instance (SizedExp se) => Num (Size se Int) where - fromInteger = num - x + y = num 0 - x * y = num 0 - abs = undefined - signum = undefined -instance (SizedExp se) => Ord(Size se Int) where - -{- - - Implementation of constraints - -} -sizeof :: Size Q a -> IO [SExp] -sizeof (QSynt s) = s -sizeof (QProvable l _) = return [([], l)] - -fresh :: TypeKind -> Supply Int -> L -fresh sig var = fresh' sig [] var - where - fresh' U _ _ = Unsized - fresh' V l var = appall (supplyValue var) l - fresh' (F _ b) l var = Abs i $ fresh' b (Var i:l) v2 - where - (v1,v2) = split2 var - i = supplyValue v1 - fresh' (L a) l var = List (appall i l) (Abs j $ fresh' a (Var j:l) v3) - where - (v1,v2,v3) = split3 var - i = supplyValue v1 - j = supplyValue v2 - - -freshvars2 :: (TS b, Unify Q (Size Q a) a) => Supply Int -> b -> Size Q a -> (Size Q a, L -> L) -freshvars2 supply q exp = (exp , id) - -freshvars :: (TS c, Unify Q a b) => Supply Int -> c -> (Size Q c -> a) -> (Size Q (c -> b), L -> L) -freshvars supply q = freshvars' (unify (freshvars s1) (freshvars2 s2)) - where - (s1, s2, s3) = split3 supply - freshvars' :: (Unify Q a b) => (a -> (Size Q b, L -> L)) -> (Size Q c -> a) -> (Size Q (c -> b), L -> L) - freshvars' u exp = (QSynt $ sizeof x, \l -> f $ App l fv) - where - (x, f) = u $ exp $ QSynt $ do - return [([], fv)] - fv = fresh (tk q) s3 - -addConstraint :: Constraint -> [SExp] -> [SExp] -addConstraint nc = map (first ((:) nc)) - -concatMapM :: (a -> IO [b]) -> [a] -> IO [b] -concatMapM f l = liftM concat $ mapM f l - -type SExp = ([Constraint], L) -newtype Q a = Q { unQ :: () } -instance SizedExp Q where - data Size Q a = QSynt (IO [SExp]) | QProvable L (Supply Int -> IO [Condition]) - known l = QSynt $return [([], l)] - true = QSynt $ return [] - match l nil cons = let - match1 (cond, ltype) = do - x <- sizeof l - let lt = rall$ App (AAbs 18 5 $ Var 18) ltype - nils <- sizeof nil - let nilc = foldr addConstraint nils $ Zero lt:cond - let tx = rall $ App (AAbs 18 5 $ App (Var 5) (Op (Var 18) '-' (Num 1))) ltype - let txs = rall $App (AAbs 18 5 $ List (Op (Var 18) '-' (Num 1)) (Var 5)) ltype - conss <- sizeof $ cons (QSynt$return [([], tx)]) (QSynt$return [([], txs)]) - let consc = foldr addConstraint conss $ lt `GEC` Num 1:cond - return $ nilc ++ consc - in QSynt $ sizeof l >>= concatMapM match1 - - iff _ l1 l2 = QSynt $ do - ll1 <- sizeof l1 - ll2 <- sizeof l2 - return $ ll1 ++ ll2 - - app l1 l2 = QSynt $ do - ll1 <- sizeof l1 - ll2 <- sizeof l2 - return [ (c1 ++ c2, App e1 e2) | (c1,e1) <- ll1, (c2,e2) <- ll2] - - bind l exp = z $ \supply -> let (s1,s2) = split2 supply in unify (freshvars s1) (freshvars2 s2) exp - where - z :: (Supply Int -> (Size Q c, L -> L)) -> Size Q c - z x = QProvable l $ \supply -> let - (sexp, f) = x supply - ll = rall $ f l - rr (Zero a) = Zero $ rall a - rr (GEC a b) = rall a `GEC` rall b - rr (LTC a b) = rall a `LTC` rall b - in do - l3 <- sizeof sexp - return $ map (\(c,l2) -> Condition (map rr c) ll (rall l2)) l3 - - num n = QSynt $return [([], Unsized)] - -instance Num (Size Q Int) where - (+) = undefined - (*) = undefined - abs = undefined - signum = undefined - fromInteger = num - -conditions :: Size Q b -> IO () -conditions (QProvable l x) = do - (s1,s2,s3) <- liftM split3 $ newSupply 30 (+1) - c <- x s1 - print c - -prove :: Size Q b -> IO Bool -prove (QProvable l x) = do - (s1,s2,s3) <- liftM split3 $ newSupply 30 (+1) - c <- x s1 - putStrLn "" - putStrLn "------------" - putStrLn "Conditions: " - print c - putStrLn "" - putStrLn "------------" - putStrLn "Equations: " - x <- checkCond s2 c - print x - putStrLn "" - putStrLn "------------" - putStrLn "Solving: " - y <- solve x s3 - putStrLn "" - if null y then do - putStrLn "QED" - return True - else do - putStrLn "------------" - putStrLn "Cannot prove: " - print y - return False Index: zechecking/Test.hs =================================================================== --- /sizechecking/Test.hs (revision 17) +++ (revision ) @@ -1,7 +1,0 @@ --- --- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking --- - -module Main where -import Examples (runTests) -main=runTests Index: zechecking/sizechecking.cabal =================================================================== --- /sizechecking/sizechecking.cabal (revision 17) +++ (revision ) @@ -1,58 +1,0 @@ --- Initial sizechecking.cabal generated by cabal init. For further --- documentation, see http://haskell.org/cabal/users-guide/ - --- The name of the package. -name: sizechecking - --- The package version. See the Haskell package versioning policy (PVP) --- for standards guiding when and how versions should be incremented. --- http://www.haskell.org/haskellwiki/Package_versioning_policy --- PVP summary: +-+------- breaking API changes --- | | +----- non-breaking API additions --- | | | +--- code changes with no API change -version: 0.1.0.0 - --- A short (one-line) description of the package. --- synopsis: - --- A longer description of the package. --- description: - --- URL for the project homepage or repository. -homepage: kp.elte.hu/sizechecking - --- The license under which the package is released. -license: BSD3 - --- The file containing the license text. -license-file: LICENSE - --- The package author(s). -author: Attila Gobi - --- An email address to which users can send suggestions, bug reports, and --- patches. -maintainer: gobi@elte.hu - --- A copyright notice. --- copyright: - -category: Testing - -build-type: Simple - --- Constraint on the version of Cabal needed to build this package. -cabal-version: >=1.8 - - -library - -- Modules exported by the library. - exposed-modules: Constraints, SizedExp, Examples, Lambda - extensions: PatternGuards - - -- Modules included in this library but not exported. - -- other-modules: - - -- Other library packages from which modules are imported. - build-depends: base ==4.6.*, containers ==0.5.*, sbv, value-supply - Index: /sizechecking/trunk/Constraints.hs =================================================================== --- /sizechecking/trunk/Constraints.hs (revision 18) +++ /sizechecking/trunk/Constraints.hs (revision 18) @@ -0,0 +1,440 @@ +-- +-- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking +-- + +{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, + IncoherentInstances, RankNTypes, ScopedTypeVariables, + FlexibleContexts,UndecidableInstances, DeriveDataTypeable, + ImpredicativeTypes #-} +module Constraints where + +import Lambda +import qualified Data.List as List +import qualified Data.Set as Set +import qualified Data.Map as Map +import qualified Data.Ord as Ord +import qualified Data.SBV as SBV +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 +asType a _ = a + +data D = D { var::Int, cond::[Condition] } + +data TypeKind = V | L TypeKind | F TypeKind TypeKind | U + deriving Show + + +class TS a where + tk :: a -> TypeKind +instance (TS a, TS b) => TS (a -> b) where + tk _ = F (tk (undefined :: a)) (tk (undefined :: b)) +instance TS a => TS [a] where + tk _ = L (tk (undefined :: a)) +instance TS a where + tk _ = V +instance TS Int where + tk _ = U + +appall :: Int -> [L] -> L +appall var = foldl App (Var var) + +data Condition = Condition [Constraint] L L + +instance Show Condition where + showsPrec _ (Condition d a b) = shows d . showString "|- " . shows a . showString " = " . shows b + showList [] = showString "" + showList [x] = shows x + showList (x:xs) = shows x . showString "\n" . shows xs + +data Constraint = Zero L | LTC L L | GEC L L + deriving Eq + +instance Show Constraint where + showList [] = id + showList [s] = shows s . showChar ' ' + showList (x:xs) = shows x . showString ", " . shows xs + showsPrec _ (Zero s) = shows s . showString " = 0" + showsPrec _ (LTC s1 s2) = shows s1 . showString " < " . shows s2 + showsPrec _ (GEC s1 s2) = shows s1 . showString " >= " . shows s2 + +normalize :: L -> L +normalize l = delzero $ foldl (\a b -> Op a '-' b) (foldl (\a b -> Op a '+' b) (f1 $ List.sortBy (Ord.comparing snd) a) c) d + where + (a,b,c,d) = norm l + f1 ((0,l):xs) = f1 xs + f1 ((1,l):xs) = Op (f1 xs) '+' (Var l) + f1 ((-1,l):xs) = Op (f1 xs) '-' (Var l) + f1 [] = Num b + + delzero (Op (Num 0) '+' b) = b + delzero (Op a c b) = Op (delzero a) c b + delzero l = l + +gnormalize :: L -> (L, Int) +gnormalize l = case (c,d) of + ([], []) -> case nonzero of + [] -> (Num 0, b) + _ -> (expr, b) + (_, _) -> error $ "Expression in condition" ++ show c + where + nonzero = List.sortBy (Ord.comparing snd) $ filter ((/=0).fst) a + proc (1, l) = Var l + proc (-1, l) = Op (Num (-1)) '*' (Var l) + t :: L -> (Int, Int) -> L + t l (1, var) = Op l '+' (Var var) + t l (-1, var) = Op l '-' (Var var) + expr = foldl t (proc $ head nonzero) (tail nonzero) + + (a,b,c,d) = norm l + +normalizec :: Constraint -> Constraint +normalizec (Zero l) = Zero $ normalize l +normalizec (LTC a b) = LTC (normalize a) (normalize b) +normalizec (GEC a b) = GEC (normalize a) (normalize b) +--normalizec (LTC a b) = LTC x (Num (-y)) +-- where (x,y) = gnormalize $ Op a '-' b +--normalizec (GEC a b) = GEC x (Num (-y)) +-- where (x,y) = gnormalize $ Op a '-' b + +normalizecs :: [Constraint] -> [Constraint] +normalizecs = normalizecs' . Prelude.map normalizec + where + normalizecs' [] = [] + normalizecs' (x:xs) = x:normalizecs' (filter (/=x) xs) + +{- + - Takes an extended lambda expression and + -} +norm :: L -> ([(Int, Int)], Int, [L], [L]) +norm (App a b) = ([], 0, [App (normalize a) (normalize b)], []) +norm (List a b) = ([], 0, [List (normalize a) (normalize b)], []) +norm (AAbs a b e) = ([], 0, [AAbs a b (normalize e)], []) +norm (Shift a b c) = ([], 0, [Shift (normalize a) (normalize b) (normalize c)], []) +norm (Unsized) = ([], 0, [Unsized], []) +norm (Bottom) = ([], 0, [Bottom], []) +norm (Abs i l) = ([], 0, [Abs i $ normalize l], []) +norm (Var i) = ([(1, i)], 0, [], []) +norm (Num i) = ([], i, [], []) +norm q@(Op a c b) = case c of + '+' -> (a1++b1, a2+b2, a3++b3, a4++b4) + '-' -> (sub a1 b1, a2-b2, a3++b4, a4++b3) + '*' -> case a of + (Num cnt) -> (map (mul cnt) b1, cnt*b2, map (Op (Num cnt) '*') b3, map (Op (Num cnt) '*') b4) + _ -> ([], 0, [q], []) + _ -> ([], 0, [q], []) + where + mul c (x,var) = (c*x, var) + (a1, a2, a3, a4) = norm a + (b1, b2, b3, b4) = norm b + sub l1 ((c,i):xs) = sub (sub' l1 c i) xs + where + sub' [] c i = [(-c, i)] + sub' ((cc,ii):xs) c i = if i==ii then (cc-c,i):xs else (cc,ii):sub' xs c i + sub l1 [] = l1 + +tnorm = Op (Num 1) '+' (Op (Var 0) '-' (Num 1)) + +checkCond :: Supply Int -> [Condition] -> IO [Condition] +checkCond v l = do + ll <- mapM (checkCond1 v) l + return $ concat ll + + where +-- checkCond1 v p@(Condition d a b) | a==b = do +-- return [] + checkCond1 v z@(Condition d (List a b) (List p q)) = do +-- i <- freshtypevar v + let (v1,v2,v3) = split3 v + let i = supplyValue v1 + let b' = rall $ App b (Var i) + let q' = rall $ App q (Var i) + l1 <- checkCond1 v2 (Condition ((Var i `GEC` Num 0):d) a p) + l2 <- checkCond1 v3 (Condition ((Var i `GEC` Num 0):(Var i `LTC` a):(Var i `LTC` p):d) b' q') + return $ l1++l2 + checkCond1 v z@(Condition d (App (Shift e f g) h) x) = do + let (v1,v2,v3) = split3 v + let e' = rall $ App e h + let g' = rall $ App g $ Op h '-' f + l1 <- checkCond1 v1 (Condition ((h `LTC` f):d) e' x) + l2 <- checkCond1 v2 (Condition ((h `GEC` f):d) g' x) +-- putStrLn $ " -> " ++ show l1 +-- putStrLn $ " -> " ++ show l2 + return $ l1 ++ l2 + checkCond1 v z@(Condition d (App (Var a) x) (App (Var b) y)) | a==b = + checkCond1 v (Condition d x y) + checkCond1 v p@(Condition d x z@(App (Shift e f g) h)) = + checkCond1 v (Condition d z x) + checkCond1 v z@(Condition d a b) = return [Condition dd (normalize a) (normalize b)] + where + dd = normalizecs d + +subst ndl hst (App a b) = App (subst ndl hst a) (subst ndl hst b) +subst ndl hst (List a b) = List (subst ndl hst a) (subst ndl hst b) +subst ndl hst (AAbs a b e) = AAbs a b (subst ndl hst e) +subst ndl hst (Shift a b c) = Shift (subst ndl hst a) (subst ndl hst b) (subst ndl hst c) +subst ndl hst (Unsized) = Unsized +subst ndl hst (Bottom) = Bottom +subst ndl hst q@(Abs i l) = if ndl==i then q else Abs i $ subst ndl hst l +subst ndl hst q@(Var i) = if ndl==i then hst else q +subst ndl hst (Num i) = Num i +subst ndl hst (Op a c b) = Op (subst ndl hst a) c (subst ndl hst b) + +substc ndl hst (Zero l) = Zero $ subst ndl hst l +substc ndl hst (LTC a b) = LTC (subst ndl hst a) (subst ndl hst b) +substc ndl hst (GEC a b) = GEC (subst ndl hst a) (subst ndl hst b) + +reorder cs = if any check cs + then Just (map r cs) + else Nothing + where + check (Zero _) = False + check (LTC a (Num 0)) = False + check (GEC a (Num 0)) = False + check _ = True + r (LTC a b) = LTC (normalize (Op a '-' b)) (Num 0) + r (GEC a b) = GEC (normalize (Op a '-' b)) (Num 0) + r l = l + +solve :: [Condition] -> Supply Int -> IO [Condition] +solve l supply = do + ll <- forM (zip l $ split supply) (\(c,s) -> do + putStrLn $ "\nSOLVING " ++ show c + solve1 s c + ) + return $ concat ll + where + + searchzero (Zero (Var a):xs) = Just (a,xs) + searchzero (x:xs) = do + (a,l) <- searchzero xs + return (a,x:l) + searchzero [] = Nothing + + + searcheq (q@(GEC (Var var) exp):xs) prev = case findeq (List.reverse prev ++ xs) [] of + Nothing -> searcheq xs (q:prev) + l -> l + where + expinc = normalize $ Op exp '+' $ Num 1 + findeq [] _ = Nothing + findeq (LTC (Var var2) exp2:xs) prev2 | var==var2 && exp2==expinc = Just (var, exp, List.reverse prev2 ++ xs) + findeq (x:xs) prev2 = findeq xs (x:prev2) + + searcheq (x:xs) prev = searcheq xs (x:prev) + searcheq [] _ = Nothing + + checkConds [] = False + checkConds (LTC a b : xs) | GEC a b `elem` xs = True + checkConds (GEC a b : xs) | LTC a b `elem` xs = True + checkConds (LTC a (Num b) : xs) | b<=0 && elem (Zero a) xs = True + checkConds (GEC a (Num b) : xs) | b>0 && elem (Zero a) xs = True + checkConds (_:xs) = checkConds xs + + checkConds2 (LTC (Num a) (Num b):xs) | a>=b = Nothing + checkConds2 (LTC (Num a) (Num b):xs) | a=b = checkConds2 xs + checkConds2 (x:xs) = do { y <- checkConds2 xs; return (x:y) } + checkConds2 [] = Just [] + +-- applyList a b d supp = do +-- let (s1,s2,s3) = split3 supp +-- let t = fresh (L V) s1 +-- let dd = (Condition d (rall $ App a t) (rall $ App b t)) +-- putStrLn $ "Applying a fresh variable: "++(show t) ++"\n"++(show dd) +-- x <- checkCond s2 [dd] >>= mapM (solve1 s3) +-- return $ concat x + + solve1 supp c@(Condition d a b) = case checkConds2 d of + Nothing -> do + putStrLn "Contradiction in preconditions" + return [] + Just d' -> solve1' supp $ Condition d a b + + solve1' supp c@(Condition d a b) +-- | 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 + | 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 +-- let (s1, s2) = split2 supp +-- let t = fresh (tk a) s1 +-- let dd= (Condition d (rall $ App a t) (rall $ App b t)) +-- putStrLn $ "Applying a fresh variable: "++(show t) ++"\n"++(show dd) +-- solve1 s2 dd +-- | AAbs _ _ _ <- a, Abs _ _ <- b = applyList a b d supp +-- | 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 + | otherwise = do + putStrLn "Tying to call solver" + let x = compiletosolver a b d + y <- SBV.prove x + print y + case y of + (SBV.ThmResult (SBV.Unsatisfiable _)) -> return [] + 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 +fvc (GEC a b) = fv a `Set.union` fv b + +compiletosolver :: L -> L -> [Constraint] -> SBV.Symbolic SBV.SBool +compiletosolver a b d = do + 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 +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." + Index: /sizechecking/trunk/Examples.hs =================================================================== --- /sizechecking/trunk/Examples.hs (revision 18) +++ /sizechecking/trunk/Examples.hs (revision 18) @@ -0,0 +1,279 @@ +-- +-- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking +-- + +{-# LANGUAGE ScopedTypeVariables, ExistentialQuantification, Rank2Types #-} +module Examples where + +import Lambda +import SizedExp +import Constraints() +import Prelude ( ($), (+), (-), Int, (==), (*), (<), (>), (<=), (>=), (/=) ) +import qualified Prelude as P +import qualified Control.Monad as M +import qualified Data.List as List + +head :: (SizedExp se ) => Size se ([l] -> l) +head = bind headc body + where + body l = match l true P.const + +tail :: (SizedExp se ) => Size se ([l] -> [l]) +tail = bind tailc body + where body l = match l true (\_ xs -> xs) + +cons :: (SizedExp se) => Size se (x -> [x] -> [x]) +cons = bind conss true + +t3 :: (SizedExp se) => Size se ( (a -> a) -> a -> a ) +t3 = bind t3s body + where body f x = f `app` (f `app` (f `app` x)) + +nil :: (SizedExp se) => Size se [x] +nil = bind nils true + +map :: (SizedExp se) => Size se ( (a->b) -> [a] -> [b] ) +map = bind smap body + where body f l = match l nil + ( \x xs -> cons `app` (f `app` x) `app` (map `app` f `app` xs )) + +heads :: (SizedExp se) => Size se ( [[a]] -> [a] ) +heads = bind sheads $ \l -> map `app` head `app` l + +tails :: (SizedExp se) => Size se ( [[a]] -> [[a]] ) +tails = bind stails $ \l -> map `app` tail `app` l + +append :: (SizedExp se) => Size se ([a] -> [a] -> [a]) +append = bind appends body + where body l1 l2 = match l1 l2 + (\x xs -> cons `app` x `app` (append `app` xs `app` l2)) + +t27 :: (SizedExp se) => Size se ((a -> a) -> a -> a) +t27 = bind (App t3s t3s) $ t3 `app` t3 + +t27_ :: (SizedExp se) => Size se ((a -> a) -> a -> a) +t27_ = bind (App t3s t3s) $ + \f -> t3 `app` t3 `app` f + +t27__ :: (SizedExp se) => Size se ((a -> a) -> a -> a) +t27__ = bind (App t3s t3s) $ \f x -> + t3 `app` t3 `app` f `app` x + +pam :: (SizedExp se) => Size se ([a -> b] -> a -> [b]) +pam = bind (AAbs 1 2 $ Abs 3 $ List (Var 1) (Abs 4 $ App (App (Var 2) (Var 4)) (Var 3))) $ \fl x -> match fl nil + (\f fs -> cons `app` (f `app` x) `app` (pam `app` fs `app` x)) + +reverse :: (SizedExp se) => Size se([a] -> [a]) +reverse = bind reverses $ \l -> match l + nil + ( + \x xs -> append `app` (reverse `app` xs) `app` (cons `app` x `app` nil) + ) + +addone :: (SizedExp se) => Size se ([P.Int] -> [P.Int]) +addone = bind addones $ \l -> cons `app` 1 `app` l + +add3 :: (SizedExp se) => Size se ([P.Int] -> [P.Int]) +add3 = bind (AAbs 0 1 $ List (Op (Var 0) '+' (Num 3)) (Var 1)) $ + \l -> t3 `app` addone `app` l + +add3_ :: (SizedExp se) => Size se ([P.Int] -> [P.Int]) +add3_ = bind (AAbs 0 1 $ List (Op (Var 0) '+' (Num 3)) (Var 1)) $ + t3 `app` addone + +t9_ :: (SizedExp se) => Size se ((a -> a) -> a -> a) +t9_ = bind ( Abs 0 $ App t3s (App t3s (Var 0))) $ + \f -> t3 `app` (t3 `app` f) + +t9 :: (SizedExp se) => Size se ((a -> a) -> a -> a) +t9 = bind ( Abs 0 $ App t3s (App t3s (Var 0))) $ + \f x -> t3 `app` (t3 `app` f) `app` x + +add27s :: L +add27s = AAbs 0 1 $ List (Op (Var 0) '+' (Num 27)) (Abs 2 Unsized) +add27 :: (SizedExp se) => Size se ([P.Int] -> [P.Int]) +add27 = bind add27s $ \x -> t27 `app` addone `app` x + + +zipWiths :: L +zipWiths = let q = App (Var 4) $ Op (Op (Var 5) '+' (Var 3)) '-' (Var 1) in + (Abs 0 $ AAbs 1 2 $ AAbs 3 4 $ List (Var 1) (Abs 5 $ App (App (Var 0) (App (Var 2) (Var 5))) q )) +zipWith :: (SizedExp se) => Size se ((a2 -> a1 -> a) -> [a2] -> [a1] -> [a]) +zipWith = bind zipWiths $ \f l1 l2 -> + match l1 + nil + ( + \x xs -> match l2 + true + ( + \y ys -> cons `app` (f `app` x `app` y) `app` (zipWith `app` f `app` xs `app` ys) + ) + ) +appAll :: (SizedExp se) => Size se ( [a -> b] -> a -> [b] ) +appAll = bind (AAbs 0 1 $ Abs 2 $ List (Var 0) (Abs 3 $ Var 1 `App` Var 3 `App` Var 2 ) ) $ \fl x -> match fl + nil + ( + \f fs -> cons `app` (f `app` x) `app` (appAll `app` fs `app` x) + ) + +conspack :: (SizedExp se) => Size se (P.Int -> [P.Int] -> [P.Int]) +conspack = bind (Abs 0 $ AAbs 1 2 $ List (Op (Var 1) '+' (Num 1)) (Abs 3 Unsized)) $ \x l -> + match l (cons `app` x `app` l) + (\hd tl -> iff (x == hd) ( + cons `app` x `app` l + ) ( + cons `app` hd `app` (conspack `app` x `app` tl) + ) + ) + +cprod :: (SizedExp se) => Size se ([P.Int] -> [P.Int] -> [[P.Int]]) +cprod = known (AAbs 0 1 $ AAbs 2 3 $ List (Op (Var 0) '*' (Var 2)) $ Abs 4 $ List (Num 2) $ Abs 5 Unsized) + +sqdiff :: SizedExp se => Size se ([Int] -> [Int] -> [[Int]]) +sqdiff = bind (let sq l = Op l '*' l in AAbs 0 1 $ AAbs 2 3 $ List (sq $ Op (Var 0) '-' (Var 2)) $ Abs 4 $ List (Num 2) $ Abs 5 Unsized) $ + \l1 l2 -> match l1 (cprod `app` l2 `app` l2) + (\_ tl1 -> match l2 (cprod `app` l1 `app` l1) + (\_ tl2 -> sqdiff `app` tl1 `app` tl2)) + +replace :: SizedExp se => Size se (Int -> [Int] -> [Int]) +replace = bind (Abs 0 $ AAbs 1 2 $ List (Var 1) (Abs 3 Unsized)) $ + \x l -> match l nil (\hd tl -> cons `app` (x+hd) `app` tl) + +scalarProd :: (SizedExp se0) => Size se0 ([Int] -> [Int] -> [Int]) +scalarProd = bind (AAbs 0 1 $ AAbs 2 3 $ List (Num 1) (Abs 4 Unsized)) $ + \l1 l2 -> match l1 ( + match l2 ( cons `app` 0 `app` nil ) + (\_ _ -> true) + ) ( \hd1 tl1 -> + match l2 true + ( \hd2 tl2 -> replace `app` (hd1 * hd2) `app` (scalarProd `app` tl1 `app` tl2) ) + ) + +mlist :: SizedExp se => Size se (a -> [a -> x] -> [x]) +mlist = bind (Abs 0 $ AAbs 1 2 $ List (Var 1) (Abs 3 $ Var 2 `App` Var 3 `App` Var 0)) + $ \x l -> match l nil (\f fs -> cons `app` (f `app` x) `app` (mlist `app` x `app` fs)) + +strange :: (SizedExp se) => Size se ([Int] -> [Int]) +strange = bind (AAbs 0 1 $ List (Num 2) (Abs 2 Unsized)) $ \l1 -> + let b = match l1 nil (\x1 l2 -> match l2 nil (\x2 l3 -> cons `app` x2 `app` (cons `app` x1 `app` nil))) + in match b (cons `app` 0 `app` (cons `app` 0 `app` nil)) (\x xs -> b) + + +take4 :: SizedExp se => Size se (([a] -> [a]) -> [[a]]) +take4 = bind (Abs 0 $ List (Num 1) (Abs 2 (Var 0 `App` (Var 0 `App` List (Num 0) (Abs 1 Bottom))))) $ + \f ->cons `app` (f `app` (f `app` nil) ) `app` nil + + +merge :: SizedExp se => Size se ([Int] -> [Int] -> [Int]) +merge = bind (AAbs 0 1 $ AAbs 2 3 $ List (Op (Var 0) '+' (Var 2)) (Abs 4 Unsized))$ + \l1 l2 -> match l1 l2 ( + \x xs -> match l2 l1 ( + \y ys -> iff (x>y) (cons `app` x `app` (merge `app` xs `app` l2)) + (cons `app` y `app` (merge `app` l1 `app` ys)) + ) + ) + +split1 :: SizedExp se => Size se ([Int] -> [Int]) +split1 = bind (AAbs 0 1 $ List (Op (Op (Var 0) '+' (Num 1))'/' (Num 2)) (Abs 2 Unsized)) $ + \z -> match z nil (\y ys -> cons `app` y `app` (split2 `app` ys)) + +split2 :: SizedExp se => Size se ([Int] -> [Int]) +split2 = bind (AAbs 0 1 $ List (Op (Var 0) '/' (Num 2)) (Abs 2 Unsized)) $ + \z -> match z nil (\y ys -> split1 `app` ys) + +ms = AAbs 0 1 $ List (Var 0) (Abs 4 Unsized) +mergesort :: SizedExp se => Size se ([Int] -> [Int]) +mergesort = bind ms $ + \l -> match l nil (\x xs -> + merge `app` (mergesort `app` (split1 `app` l)) `app` (mergesort `app` (split2 `app` l)) + ) + +last :: SizedExp se => Size se ([a] -> a) +last = bind (AAbs 0 1 $ App (Var 1) (Num 0)) $ + \l -> match l true (\x xs -> match xs x (\_ _ -> last `app` xs)) + +charm :: SizedExp se => Size se (([a] -> [a]) -> a) +charm = bind (Abs 0 $ App (AAbs 2 3 $ App (Var 3) (Num 0)) (App (Var 0) (List (Num 0) $ Abs 1 Bottom))) $ + \ f -> last `app` (f `app` nil) + +fix :: SizedExp se => Size se ((a -> a) -> a) +fix = bind (Abs 2 $ App yComb (Var 2)) $ + \f -> f `app` (fix `app` f) + +transpose :: SizedExp se => Size se ([[a]] -> [[a]]) +transpose = bind transposec $ \l -> match l true $ + \l1 xss -> match l1 true $ + \x xs -> cons `app` (cons `app` x `app` (heads `app` xss)) + `app` (transpose `app` (cons `app` xs `app` (tails `app` xss))) +transposec = AAbs 18 5 $ List len fun + where + len = AAbs 19 6 (Var 19) `App` (Var 5 `App` Num 0) + fun = Abs 8 $ List (Var 18) (Abs 9 $ AAbs 19 6 (Var 6 `App` Var 8) `App` (Var 5 `App` Var 9)) + +comps = Abs 2 $ Abs 3 $ Abs 4 $ App (Var 2) (App (Var 3) (Var 4)) +comp :: (SizedExp se) => Size se ( (b->c) -> (a->b) -> a->c ) +comp = bind comps $ \f g x -> f `app` (g `app` x) + +test1s = Abs 2 $ AAbs 19 6 $ Var 2 `App` List (Var 19) (Var 6) +test1 :: (SizedExp se) => Size se (([a] -> [b]) -> [a] -> [b]) +test1 = bind test1s $ \f l -> match (f `app` l) nil (\x xs -> f `app` l) + + +test2s = Abs 2 $ AAbs 18 5 $ appends `App` (Var 2 `App` List (Var 18) (Var 5)) `App` + (appends `App` (Var 2 `App` List (Var 18) (Var 5)) `App` List (Var 18) (Var 5)) +test2 :: (SizedExp se) => Size se (([a] -> [a]) -> [a] -> [a]) +test2 = bind test2s $ \f l -> append `app` (f `app` l) `app` (append `app` (f `app` l) `app` l) + +data TestCase = forall a . TestCase P.String (forall se. SizedExp se => Size se a) + +tests :: [TestCase] +tests = [ + TestCase "append" append + , TestCase "reverse" reverse + , TestCase "heads" heads + , TestCase "map" map + , TestCase "pam" pam + , TestCase "head" head + , TestCase "tail" tail + , TestCase "t3" t3 + , TestCase "t9" t9 +-- , TestCase "t9_" t9_ -- too few arguments in definition +-- , TestCase "t27" t27 +-- , TestCase "t27_" t27_ + , TestCase "t27__" t27__ + , TestCase "addone" addone + , TestCase "add3" add3 +-- , TestCase "add3_" add3_ -- too few arguments in definition + , TestCase "add27" add27 + , TestCase "zipWith" zipWith + , TestCase "appAll" appAll + , TestCase "conspack" conspack + , TestCase "scalarProd" scalarProd + , TestCase "sqdiff" sqdiff + , TestCase "mlist" mlist + , TestCase "strange" strange + , TestCase "take4" take4 + , TestCase "charm" charm + , TestCase "comp" comp + , TestCase "merge" merge + , TestCase "split1" split1 + , TestCase "split2" split2 + , TestCase "mergesort" mergesort + ] + +runTests = do + failed <- M.forM tests $ \(TestCase name test) -> do + P.print " +++++++++++++++++++++++++++++++" + P.print $ " + Proving " P.++ name + P.print " +++++++++++++++++++++++++++++++" + + s <- prove test + M.return [name | P.not s] + + let f = P.concat failed + if List.null f then + P.putStrLn "All ok." + else do + P.putStr "\n\nFailed test cases: " + P.putStrLn $ List.intercalate ", " f + Index: /sizechecking/trunk/LICENSE =================================================================== --- /sizechecking/trunk/LICENSE (revision 18) +++ /sizechecking/trunk/LICENSE (revision 18) @@ -0,0 +1,30 @@ +Copyright (c) 2012, Attila Gobi + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Attila Gobi nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. Index: /sizechecking/trunk/Lambda.hs =================================================================== --- /sizechecking/trunk/Lambda.hs (revision 18) +++ /sizechecking/trunk/Lambda.hs (revision 18) @@ -0,0 +1,238 @@ +-- +-- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking +-- + +module Lambda where + +{- + Ez a cikkben megadott lambda kalkulus egy implementacioja + redukcio + peldak. + + Hasznalat: lasd Lambda_proof.hs + + -} +import Data.List +import qualified Data.Set as Set +import Data.Char + +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, Ord) + +showVar x = if x>28 + then showVar (x `div` 29) . showChar (chr $ ord 'a' + (x `mod` 29)) + else showChar $ chr $ ord 'a' + x + +getPrec :: Char -> (Int,Int,Int) +getPrec '+' = (4,4,5) +getPrec '-' = (4,4,5) +getPrec '*' = (5,5,6) +getPrec '/' = (5,5,6) +getPrec c = error $ "Unknown operator "++[c] + +instance Show L where + showsPrec p (Abs s l) = showParen (p>0) $ showChar 'λ' . showVar s . showChar '.' . shows l + showsPrec p (AAbs f s l) = showParen (p>0) $ showChar 'Λ' . showVar f . showChar ',' . showVar s . showChar '.' . shows l + showsPrec p (App m n) = showParen (p>6) $ showsPrec 6 m . showChar ' ' . showsPrec 7 n + showsPrec _ (Var s) = showVar s + showsPrec _ (Num i) = shows i + showsPrec p (Op m op n) = showParen (p>prec) $ showsPrec lprec m . showChar op . showsPrec rprec n + where (prec,lprec,rprec)=getPrec op + showsPrec p (List s f) = showParen (p>0) $ showString "List " . showsPrec 9 s . showChar ' ' . showsPrec 9 f + showsPrec p (Shift e1 s e2) = showParen (p>0) $ showString "Shift " .showsPrec 2 e1 . + showChar ' ' . showsPrec 2 s . showChar ' ' . showsPrec 2 e2 + showsPrec _ Bottom = showChar '┮' + showsPrec _ Unsized = showChar 'U' + +t3s = Abs 1 $ Abs 0 $ App t (App t (App t x)) + where t = Var 1 + x = Var 0 + +subs (App x z) var exp = App (subs x var exp) (subs z var exp) +subs (List s f) var exp = List (subs s var exp) (subs f var exp) +subs (Shift e1 e2 e3) var exp = Shift (subs e1 var exp) (subs e2 var exp) (subs e3 var exp) +subs (Op x c z) var exp = Op (subs x var exp) c (subs z var exp) +subs e@(Var v) var exp | v==var = exp + | otherwise = e +subs x@(Abs v e) var exp | v==var = x + | otherwise = Abs v (subs e var exp) +subs x@(AAbs s f e) var exp | s==var||f==var = x + | otherwise = AAbs s f (subs e var exp) +subs x@(Num _) _ _ = x +subs x@Bottom _ _ = x +subs x@Unsized _ _ = x + + +alpha (App x z) from to = App (alpha x from to) (alpha z from to) +alpha (List x z) from to = List (alpha x from to) (alpha z from to) +alpha (Op x c z) from to = Op (alpha x from to) c (alpha z from to) +alpha (Shift x y z) from to = Shift (alpha x from to) (alpha y from to) (alpha z from to) +alpha e@(Var _) _ _ = e +alpha e@(Num _) _ _ = e +alpha e@Bottom _ _ = e +alpha e@Unsized _ _ = e +alpha (Abs v e) from to | v==from = Abs to (alpha' e from to) + | otherwise = Abs v (alpha e from to) +alpha (AAbs v1 v2 e) from to | v1==from = AAbs to v2 (alpha' e from to) + | v2==from = AAbs v1 to (alpha' e from to) + | otherwise = AAbs v1 v2 (alpha e from to) + +alpha' (App x z) from to = App (alpha' x from to) (alpha' z from to) +alpha' (List x z) from to = List (alpha' x from to) (alpha' z from to) +alpha' (Op x c z) from to = Op (alpha' x from to) c (alpha' z from to) +alpha' (Shift x y z) from to = Shift (alpha' x from to) (alpha' y from to) (alpha' z from to) +alpha' e@(Var v) from to | v==from = Var to + | otherwise = e +alpha' (Abs v e) from to | v==from = Abs to (alpha' e from to) + | otherwise = Abs v (alpha' e from to) +alpha' (AAbs v1 v2 e) from to | v1==from = AAbs to v2 (alpha' e from to) + | v2==from = AAbs v1 to (alpha' e from to) + | otherwise = AAbs v1 v2 (alpha' e from to) +alpha' x@(Num _) _ _ = x +alpha' x@Bottom _ _ = x +alpha' x@Unsized _ _ = x + +fv (Var x) = Set.singleton x +fv (App x y) = fv x `Set.union` fv y +fv (Op x _ y) = fv x `Set.union` fv y +fv (Abs v e) = v `Set.delete` fv e +fv (AAbs x y e) = x `Set.delete` ( y `Set.delete` fv e) +fv (List s e) = fv s `Set.union` fv e +fv (Num _) = Set.empty +fv (Shift e1 e2 e3) = fv e1 `Set.union` fv e2 `Set.union` fv e3 +fv Unsized = Set.empty +fv Bottom = Set.empty + +bv (Var _) = Set.empty +bv (App x y) = bv x `Set.union` bv y +bv (Op x _ y) = bv x `Set.union` bv y +bv (List x y) = bv x `Set.union` bv y +bv (Abs v e) = v `Set.insert` bv e +bv (AAbs v1 v2 e) = v1 `Set.insert` (v2 `Set.insert` bv e) +bv (Shift e1 e2 e3) = bv e1 `Set.union` bv e2 `Set.union` bv e3 +bv (Num _) = Set.empty +bv Unsized = Set.empty +bv Bottom = Set.empty + +maxv (Var x) = x +maxv (Num _) = 0 +maxv Unsized = 0 +maxv Bottom = 0 +maxv (App x y) = maxv x `max` maxv y +maxv (Op x _ y) = maxv x `max` maxv y +maxv (Shift x y z) = maxv x `max` maxv y `max` maxv z +maxv (List x y) = maxv x `max` maxv y +maxv (Abs v e) = v `max` maxv e +maxv (AAbs v1 v2 e) = v1 `max` v2 `max` maxv e + +rsubs oexp var exp = subs renamed var exp + where + dvar = fv exp `Set.intersection` bv oexp + m = maxv exp `max` maxv oexp + renames = zip (Set.toList dvar) [m+1..] + renamed = foldr rename oexp renames + rename (from,to) _ = alpha oexp from to + + +reduce (App (Abs var exp) z) = return $ rsubs exp var z +reduce (App (AAbs s f exp) (List s' f')) = return $ rsubs (App (Abs f exp) f') s s' +reduce (App e f) = case reduce e of + Just e' -> return $ App e' f + _ -> reduce f >>= \f' -> return $ App e f' +reduce (Abs v e) = reduce e >>= \e' -> return $ Abs v e' +reduce (Var _) = Nothing +reduce (Num _) = Nothing +reduce (List e f) = case reduce e of + Just e' -> return $ List e' f + _ -> reduce f >>= \f' -> return $ List e f' +reduce (AAbs v1 v2 e) = reduce e >>= \e' -> return $ AAbs v1 v2 e' +reduce Unsized = Nothing +reduce Bottom = Nothing +reduce (Shift e1 e2 e3) = case reduce e1 of + Just e' -> return $ Shift e' e2 e3 + _ -> case reduce e2 of + Just e' -> return $ Shift e1 e' e3 + _ -> reduce e3 >>= \e' -> return $ Shift e1 e2 e' +reduce (Op m c n) = case c of + '+' | (Num i, Num j) <- (m,n) -> return $ Num $ i+j + '-' | (Num i, Num j) <- (m,n) -> return $ Num $ i-j + '*' | (Num i, Num j) <- (m,n) -> return $ Num $ i*j + '+' | (Num 0) <- m -> reduce n + '+' | (Num 0) <- n -> reduce m + '*' | (Num 0) <- m -> return $ Num 0 + '*' | (Num 0) <- n -> return $ Num 0 + '*' | (Num 1) <- m -> reduce n + '*' | (Num 1) <- n -> reduce m + '-' | (Num 0) <- n -> reduce m + _ -> case reduce m of + Just m' -> return $ Op m' c n + _ -> reduce n >>= \n' -> return $ Op m c n' + +r :: Maybe L -> Maybe L +r x = x >>= reduce + +it f x = it' f (Just x) + where + it' _ Nothing = [] + it' f (Just x) = x:it' f (f x) + +rchain :: L -> [L] +rchain = it reduce + +pchain = putStrLn . intercalate "\n-> " . map show . rchain + +lplus = Abs m $ Abs n $ Abs f $ Abs x $ App (App (Var m) (Var f)) $ App (App (Var n) (Var f)) (Var x) + where [m,n,f,x] = [0..3] +lzero = Abs f $ Abs x $ Var x + where [f,x] = [0,1] +lsucc = Abs n $ Abs f $ Abs x $ App (Var f) $ App (App (Var n) (Var f)) (Var x) + where [n,f,x] = [0..2] +lone = last $ it reduce $ App lsucc lzero +ltwo = last $ it reduce $ App lsucc lone + +lpred = Abs n $ Abs f $ Abs x $ App (App (App (Var n) u1) (Abs u $ Var x)) (Abs u $ Var u) + where + u1 = Abs g $ Abs h $ App (Var h) $ App (Var g) (Var f) + [n,f,x,g,h,u] = [0..5] + +lsub = Abs m $ Abs n $ App (App (Var n) lpred) (Var m) + where (m,n) = (0,1) + +ltrue = Abs 0 $ Abs 1 $ Var 0 +lfalse = Abs 0 $ Abs 1 $ Var 1 + +liszero = Abs n $ App (App (Var n) (Abs x lfalse)) ltrue + where (n,x) = (0,1) + +land = Abs 0 $ Abs 1 $ App (App (Var 0) (Var 1)) (Var 1) +lleq = Abs 0 $ Abs 1 $ App liszero $ App (App lsub (Var 0)) (Var 1) +leq = Abs 0 $ Abs 1 $ App (App land l1) l2 + where + l1 = App (App lleq (Var 0)) (Var 1) + l2 = App (App lleq (Var 1)) (Var 0) + +test = Abs 0 $ Abs 1 $ App (App leq xpy) ypx +xpy = App (App lplus (Var 0)) (Var 1) +ypx = App (App lplus (Var 1)) (Var 0) + +smap = Abs 5 $ AAbs 18 6 $ List (Var 18) (Abs 8$ App (Var 5) (App (Var 6) (Var 8))) +conss = Abs 23 $ AAbs 19 5 $ List (Op (Num 1) '+' (Var 19)) $ Shift (Var 5) (Var 19) (Abs 8 $ Var 23) +addones = AAbs 19 5 $ List (Op (Num 1) '+' (Var 19)) (Abs 8 Unsized) +nils = List (Num 0) (Abs 8 Bottom) +lz n = List (Num n) (Abs 8 Unsized) +srep n x = List (Num n) (Abs 8 x) +dupfst = AAbs 19 5 $ List (Op (Num 1) '+' (Var 19)) $ Shift (Var 5) (Op (Var 19) '-' (Num 1)) + $ Abs 8 $ App (Var 5) (Op (Var 19) '-' (Num 1)) +yComb = Abs 18 $ App (Abs 22 $ App (Var 18) (App (Var 22) (Var 22))) (Abs 22 $ App (Var 18) (App (Var 22) (Var 22))) +-- Λs,g.List s (λi.(λx.Λt,f.List (1+t) (Shift f (t-1) x)) U (g i)) +reverses = AAbs 18 5 $ List (Var 18) (Abs 8 $ App (Var 5) $ Op (Op (Var 18) '-' (Num 1)) '-' (Var 8) ) +reverse' l = case l of + [] -> [] + (x:xs) -> x:reverse' xs +appends = AAbs 18 5 $ AAbs 19 6 $ List (Op (Var 18) '+' (Var 19)) $ Shift (Var 6) (Var 19) (Var 5) + +headc = AAbs 18 5 $ App (Var 5) (Op (Var 18) '-' (Num 1)) +tailc = AAbs 18 5 $ List (Op (Var 18) '-' (Num 1)) (Var 5) +rall = last . it reduce + +sheads = rall $ App smap headc +stails = rall $ App smap tailc Index: /sizechecking/trunk/README.html =================================================================== --- /sizechecking/trunk/README.html (revision 18) +++ /sizechecking/trunk/README.html (revision 18) @@ -0,0 +1,89 @@ + + + + + + + + + +

Prerequisites

+

You need at least version 2011.4.0.0 of the Haskell platform, an installed Z3 and the packages sbv and value-supply. If you have a working Haskell platform installed you can install value-supply by typing

+
cabal install value-supply sbv
+

Source files

+
+
Examples.hs
+
Some examples +
+
SizedExp.hs
+
Embedded language to prove size expressions +
+
Lambda.hs
+
Size expressions +
+
Constraints.hs
+
Constraint solver +
+
+

Using the examples

+
$ ghci Examples.hs
+GHCi, version 7.0.4: http://www.haskell.org/ghc/  :? for help
+Loading package ghc-prim ... linking ... done.
+Loading package integer-gmp ... linking ... done.
+Loading package base ... linking ... done.
+Loading package ffi-1.0 ... linking ... done.
+[1 of 4] Compiling Lambda           ( Lambda.hs, interpreted )
+[2 of 4] Compiling Constraints      ( Constraints.hs, interpreted )
+[3 of 4] Compiling SizedExp         ( SizedExp.hs, interpreted )
+[4 of 4] Compiling Main             ( Examples.hs, interpreted )
+Ok, modules loaded: Lambda, SizedExp, Constraints, Main.
+*Main>
+

Type "runTests" to run all test cases or type "prove map" to prove the function named map.

+

Under Windows

+

It is not perfect, and you will see a box after every special character, but at least it works.

+ +

Introduction to Haskell syntax

+

Haskell syntax is very much like Clean, however there are some expressions you cannot find in Clean.

+

Backtick

+

Every haskell function can be used as infix operator. For example the following two expressions are the same.

+
func a b
+a `func` b
+

Dollar

+

Dollar sign is just explicit application (but with different precedence), so it can be used as a backward pipe operator. The following expressions are the same.

+
func (a b)
+func $ a b
+

The Embedded Language

+

As an example the function map is examined.

+
1 smap  = Abs 5 $ AAbs 18 6 $ List (Var 18) (Abs 8$ App (Var 5) (App (Var 6) (Var 8)))
+2 map :: (SizedExp se)  => Size se ( (a->b) -> [a] -> [b] )
+3 map = bind smap body
+4     where body f l = match l (nil)
+5             ( \x xs ->  cons `app` (f `app` x) `app` (map `app` f `app` xs ))
+

Here line 3 tells us map is a top-level binding, where the body of the function is defined in line 4--5 and its size expression is in line 1. Unfortunately the size expression language has not yet been embedded, so it is a bit difficult to read. Type smap in the GHC console to get a pretty printed form.

+
*Main> smap
+λf.Λs,g.List s (λi.f (g i))
+

The type of the function tells us the underlying type, ie. (a->b) -> [a] -> [b].

+

The body of map corresponds to the following expression

+
match l of
+   nil       -> nil
+   cons x xs -> cons (f x) (map f xs)
+

In the embedded language bind, match and app are supercombinators.

+
+
bind sexp exp
+

combines a size and an expression and creates a top-level binding

+
+
match list nilexp consexp
+

embedding of the match operator of our language to haskell

+
+
app exp1 exp2
+

embedding of the function application of our language to haskell

+
+
+

There is also a function called true to denote that we do not want to prove that branch.

+ + Index: /sizechecking/trunk/README.txt =================================================================== --- /sizechecking/trunk/README.txt (revision 18) +++ /sizechecking/trunk/README.txt (revision 18) @@ -0,0 +1,133 @@ +Prerequisites +------------- + +You need at least version 2011.4.0.0 of the Haskell platform, an installed +[Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/) +and the packages `sbv` and `value-supply`. If you have a working Haskell platform installed you can +install value-supply by typing + + cabal install value-supply sbv + + +Source files +------------ + +Examples.hs + ~ Some examples +SizedExp.hs + ~ Embedded language to prove size expressions +Lambda.hs + ~ Size expressions +Constraints.hs + ~ Constraint solver + +Using the examples +------------------ + +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +$ ghci Examples.hs +GHCi, version 7.0.4: http://www.haskell.org/ghc/ :? for help +Loading package ghc-prim ... linking ... done. +Loading package integer-gmp ... linking ... done. +Loading package base ... linking ... done. +Loading package ffi-1.0 ... linking ... done. +[1 of 4] Compiling Lambda ( Lambda.hs, interpreted ) +[2 of 4] Compiling Constraints ( Constraints.hs, interpreted ) +[3 of 4] Compiling SizedExp ( SizedExp.hs, interpreted ) +[4 of 4] Compiling Main ( Examples.hs, interpreted ) +Ok, modules loaded: Lambda, SizedExp, Constraints, Main. +*Main> +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Type "`runTests`" to run all test cases or type "`prove map`" to prove the +function named map. + +Under Windows +------------- +It is not perfect, and you will see a box after every special character, but at +least it works. + + - Open a console by running the program `cmd` + - Issue the command `chcp 65001` + - In the console cd to the trunk directory + - Now, you can run `ghci Examples.hs` + + +Introduction to Haskell syntax +------------------------------ + +Haskell syntax is very much like Clean, however there are some expressions you +cannot find in Clean. + +### Backtick ### + +Every haskell function can be used as infix operator. For example the +following two expressions are the same. + +~~~~~~~~~~~ +func a b +a `func` b +~~~~~~~~~~~ + +### Dollar ### + +Dollar sign is just explicit application (but with different precedence), so it +can be used as a backward pipe operator. The following expressions are the +same. + +~~~~~~~~~~~~~~ +func (a b) +func $ a b +~~~~~~~~~~~~~~ + + +The Embedded Language +--------------------- + +As an example the function `map` is examined. + +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +1 smap = Abs 5 $ AAbs 18 6 $ List (Var 18) (Abs 8$ App (Var 5) (App (Var 6) (Var 8))) +2 map :: (SizedExp se) => Size se ( (a->b) -> [a] -> [b] ) +3 map = bind smap body +4 where body f l = match l (nil) +5 ( \x xs -> cons `app` (f `app` x) `app` (map `app` f `app` xs )) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Here line 3 tells us map is a top-level binding, where the body of the function is +defined in line 4--5 and its size expression is in line 1. Unfortunately the +size expression language has not yet been embedded, so it is a bit difficult to +read. Type `smap` in the GHC console to get a pretty printed form. + +~~~~~~~~~~~~~~~~~ +*Main> smap +λf.Λs,g.List s (λi.f (g i)) +~~~~~~~~~~~~~~~~~ + +The type of the function tells us the underlying type, ie. `(a->b) -> [a] -> [b]`. + +The body of map corresponds to the following expression + +~~~~~~~~~~~~~~~~~~~~~~~ +match l of + nil -> nil + cons x xs -> cons (f x) (map f xs) +~~~~~~~~~~~~~~~~~~~~~~~ + + +In the embedded language `bind`, `match` and `app` are supercombinators. + +`bind sexp exp` + + : combines a size and an expression and creates a top-level binding + +`match list nilexp consexp` + + : embedding of the match operator of our language to haskell + +`app exp1 exp2` + + : embedding of the function application of our language to haskell + +There is also a function called `true` to denote that we do not want to prove that +branch. Index: /sizechecking/trunk/Setup.hs =================================================================== --- /sizechecking/trunk/Setup.hs (revision 18) +++ /sizechecking/trunk/Setup.hs (revision 18) @@ -0,0 +1,6 @@ +-- +-- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking +-- + +import Distribution.Simple +main = defaultMain Index: /sizechecking/trunk/SizedExp.hs =================================================================== --- /sizechecking/trunk/SizedExp.hs (revision 18) +++ /sizechecking/trunk/SizedExp.hs (revision 18) @@ -0,0 +1,174 @@ +{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, + IncoherentInstances, RankNTypes, ScopedTypeVariables, + FlexibleContexts,UndecidableInstances #-} +-- +-- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking +-- + +module SizedExp where + +import Lambda as L +import Constraints +import Data.Supply +import Control.Arrow +import Control.Monad + +class TS b => (Unify se a b) where + unify :: (forall a b c. (TS c, Unify se a b) => c -> (Size se c -> a) -> (Size se (c -> b), d)) -> + (b -> Size se b -> (Size se b, d)) -> + a -> (Size se b, d) + +instance (SizedExp se, Unify se a b, se~se1, c1~c2, TS c2) => Unify se (Size se1 c1->a) (c2->b) where + unify f g = f undefined + +instance (SizedExp se, se~se1, c1~c2, TS c2) => Unify se (Size se1 c1) c2 where + unify f g = g undefined + +class SizedExp (se :: * -> *) where + data Size se :: * -> * + true :: Size se x + known :: L -> Size se x + match :: Size se [l] -> Size se r -> (Size se l -> Size se [l] -> Size se r) -> Size se r + bind :: (Unify se a b) => L.L -> a -> Size se b + app :: Size se (a->b) -> Size se a -> Size se b + iff :: Bool -> Size se a -> Size se a -> Size se a + num :: Integer -> Size se Int + +instance Show (Size se a) where + show (==) = error "no show on Size!" +instance Eq (Size se a) where + (==) = undefined +instance (SizedExp se) => Num (Size se Int) where + fromInteger = num + x + y = num 0 + x * y = num 0 + abs = undefined + signum = undefined +instance (SizedExp se) => Ord(Size se Int) where + +{- + - Implementation of constraints + -} +sizeof :: Size Q a -> IO [SExp] +sizeof (QSynt s) = s +sizeof (QProvable l _) = return [([], l)] + +fresh :: TypeKind -> Supply Int -> L +fresh sig var = fresh' sig [] var + where + fresh' U _ _ = Unsized + fresh' V l var = appall (supplyValue var) l + fresh' (F _ b) l var = Abs i $ fresh' b (Var i:l) v2 + where + (v1,v2) = split2 var + i = supplyValue v1 + fresh' (L a) l var = List (appall i l) (Abs j $ fresh' a (Var j:l) v3) + where + (v1,v2,v3) = split3 var + i = supplyValue v1 + j = supplyValue v2 + + +freshvars2 :: (TS b, Unify Q (Size Q a) a) => Supply Int -> b -> Size Q a -> (Size Q a, L -> L) +freshvars2 supply q exp = (exp , id) + +freshvars :: (TS c, Unify Q a b) => Supply Int -> c -> (Size Q c -> a) -> (Size Q (c -> b), L -> L) +freshvars supply q = freshvars' (unify (freshvars s1) (freshvars2 s2)) + where + (s1, s2, s3) = split3 supply + freshvars' :: (Unify Q a b) => (a -> (Size Q b, L -> L)) -> (Size Q c -> a) -> (Size Q (c -> b), L -> L) + freshvars' u exp = (QSynt $ sizeof x, \l -> f $ App l fv) + where + (x, f) = u $ exp $ QSynt $ do + return [([], fv)] + fv = fresh (tk q) s3 + +addConstraint :: Constraint -> [SExp] -> [SExp] +addConstraint nc = map (first ((:) nc)) + +concatMapM :: (a -> IO [b]) -> [a] -> IO [b] +concatMapM f l = liftM concat $ mapM f l + +type SExp = ([Constraint], L) +newtype Q a = Q { unQ :: () } +instance SizedExp Q where + data Size Q a = QSynt (IO [SExp]) | QProvable L (Supply Int -> IO [Condition]) + known l = QSynt $return [([], l)] + true = QSynt $ return [] + match l nil cons = let + match1 (cond, ltype) = do + x <- sizeof l + let lt = rall$ App (AAbs 18 5 $ Var 18) ltype + nils <- sizeof nil + let nilc = foldr addConstraint nils $ Zero lt:cond + let tx = rall $ App (AAbs 18 5 $ App (Var 5) (Op (Var 18) '-' (Num 1))) ltype + let txs = rall $App (AAbs 18 5 $ List (Op (Var 18) '-' (Num 1)) (Var 5)) ltype + conss <- sizeof $ cons (QSynt$return [([], tx)]) (QSynt$return [([], txs)]) + let consc = foldr addConstraint conss $ lt `GEC` Num 1:cond + return $ nilc ++ consc + in QSynt $ sizeof l >>= concatMapM match1 + + iff _ l1 l2 = QSynt $ do + ll1 <- sizeof l1 + ll2 <- sizeof l2 + return $ ll1 ++ ll2 + + app l1 l2 = QSynt $ do + ll1 <- sizeof l1 + ll2 <- sizeof l2 + return [ (c1 ++ c2, App e1 e2) | (c1,e1) <- ll1, (c2,e2) <- ll2] + + bind l exp = z $ \supply -> let (s1,s2) = split2 supply in unify (freshvars s1) (freshvars2 s2) exp + where + z :: (Supply Int -> (Size Q c, L -> L)) -> Size Q c + z x = QProvable l $ \supply -> let + (sexp, f) = x supply + ll = rall $ f l + rr (Zero a) = Zero $ rall a + rr (GEC a b) = rall a `GEC` rall b + rr (LTC a b) = rall a `LTC` rall b + in do + l3 <- sizeof sexp + return $ map (\(c,l2) -> Condition (map rr c) ll (rall l2)) l3 + + num n = QSynt $return [([], Unsized)] + +instance Num (Size Q Int) where + (+) = undefined + (*) = undefined + abs = undefined + signum = undefined + fromInteger = num + +conditions :: Size Q b -> IO () +conditions (QProvable l x) = do + (s1,s2,s3) <- liftM split3 $ newSupply 30 (+1) + c <- x s1 + print c + +prove :: Size Q b -> IO Bool +prove (QProvable l x) = do + (s1,s2,s3) <- liftM split3 $ newSupply 30 (+1) + c <- x s1 + putStrLn "" + putStrLn "------------" + putStrLn "Conditions: " + print c + putStrLn "" + putStrLn "------------" + putStrLn "Equations: " + x <- checkCond s2 c + print x + putStrLn "" + putStrLn "------------" + putStrLn "Solving: " + y <- solve x s3 + putStrLn "" + if null y then do + putStrLn "QED" + return True + else do + putStrLn "------------" + putStrLn "Cannot prove: " + print y + return False Index: /sizechecking/trunk/Test.hs =================================================================== --- /sizechecking/trunk/Test.hs (revision 18) +++ /sizechecking/trunk/Test.hs (revision 18) @@ -0,0 +1,7 @@ +-- +-- Copyright (C) 2012 Attila Gobi - http://kp.elte.hu/sizechecking +-- + +module Main where +import Examples (runTests) +main=runTests Index: /sizechecking/trunk/sizechecking.cabal =================================================================== --- /sizechecking/trunk/sizechecking.cabal (revision 18) +++ /sizechecking/trunk/sizechecking.cabal (revision 18) @@ -0,0 +1,59 @@ +-- Initial sizechecking.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +-- The name of the package. +name: sizechecking + +-- The package version. See the Haskell package versioning policy (PVP) +-- for standards guiding when and how versions should be incremented. +-- http://www.haskell.org/haskellwiki/Package_versioning_policy +-- PVP summary: +-+------- breaking API changes +-- | | +----- non-breaking API additions +-- | | | +--- code changes with no API change +version: 0.1.0.0 + +-- A short (one-line) description of the package. +-- synopsis: + +-- A longer description of the package. +-- description: + +-- URL for the project homepage or repository. +homepage: kp.elte.hu/sizechecking + +-- The license under which the package is released. +license: BSD3 + +-- The file containing the license text. +license-file: LICENSE + +-- The package author(s). +author: Attila Gobi + +-- An email address to which users can send suggestions, bug reports, and +-- patches. +maintainer: gobi@elte.hu + +-- A copyright notice. +-- copyright: + +category: Testing + +build-type: Simple + +-- Constraint on the version of Cabal needed to build this package. +cabal-version: >=1.8 + + +library + -- Modules exported by the library. + exposed-modules: Constraints, SizedExp, Examples, Lambda + extensions: PatternGuards + + -- Modules included in this library but not exported. + -- other-modules: + + -- Other library packages from which modules are imported. + build-depends: base ==4.6.*, containers ==0.5.*, sbv, value-supply, + transformers +