Index: sizechecking/branches/macs/LICENSE =================================================================== --- sizechecking/branches/macs/LICENSE (revision 25) +++ sizechecking/branches/macs/LICENSE (revision 25) @@ -0,0 +1,23 @@ +Copyright (c) 2014, 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: + +1. Redistributions of source code must retain the above copyright notice, this +list of conditions and the following disclaimer. + +2. 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. + +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 HOLDER 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/branches/macs/Lambda.hs =================================================================== --- sizechecking/branches/macs/Lambda.hs (revision 24) +++ sizechecking/branches/macs/Lambda.hs (revision 25) @@ -1,7 +1,10 @@ -{-# LANGUAGE FlexibleContexts,FlexibleInstances #-} +{-# LANGUAGE TypeFamilies #-} + module Lambda where import qualified Data.Supply as S import qualified Data.Char as C +import Control.Monad.IO.Class (MonadIO, liftIO) +import Data.IORef (newIORef, readIORef, writeIORef) {- @@ -9,6 +12,6 @@ -} class Lambda l where - lam :: (l a -> l b) -> l (a -> b) - app :: l (a -> b) -> l a -> l b + lam :: (l a -> l b) -> l (a -> b) + app :: l (a -> b) -> l a -> l b lit :: Int -> l Int @@ -54,2 +57,25 @@ printAst :: S a -> IO () printAst l = ast l >>= (\s -> putStrLn $ s "") + + +type family Sem (m :: * -> *) a :: * +type instance Sem m Int = Int +type instance Sem m (a -> b) = m (Sem m a) -> m (Sem m b) + +newtype R m a = R { unR :: m (Sem m a) } + +share :: (MonadIO m) => m a -> m (m a) +share f = do + mem <- liftIO $ newIORef (False, f) + return $ do + (evald, thunk) <- liftIO $ readIORef mem + if evald then thunk + else do + value <- thunk + liftIO $ writeIORef mem (True, return value) + return value + +instance (MonadIO m) => Lambda (R m) where + app x y = R $ unR x >>= ($ (unR y)) + lit = R . return + lam f = R . return $ (\x -> share x >>= unR . f . R) Index: sizechecking/branches/macs/Ops.hs =================================================================== --- sizechecking/branches/macs/Ops.hs (revision 24) +++ sizechecking/branches/macs/Ops.hs (revision 25) @@ -1,3 +1,3 @@ -{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleInstances, KindSignatures #-} module Ops where @@ -8,18 +8,20 @@ import Lambda +-- infix operatorok, ezek beagyazasa picit necces, lasd a type family kesobb class (Lambda l) => LOps l where - infixop :: String -> Int -> (a -> b -> c) -> l a -> l b -> l c + infixop :: String -> Int -> (a -> b -> c) -> l a -> l b -> l c infixopr :: String -> Int -> (a -> b -> c) -> l a -> l b -> l c infixopl :: String -> Int -> (a -> b -> c) -> l a -> l b -> l c - fun :: String -> a -> l a + fun :: String -> a -> l a - (+) :: l Int -> l Int -> l Int - (+) = infixopl "+" 6 (Prelude.+) +(+) :: (LOps l) => l Int -> l Int -> l Int +(+) = infixopl "+" 6 (Prelude.+) - (-) :: l Int -> l Int -> l Int - (-) = infixopl "-" 6 (Prelude.-) +(-) :: (LOps l) => l Int -> l Int -> l Int +(-) = infixopl "-" 6 (Prelude.-) - (*) :: l Int -> l Int -> l Int - (*) = infixopl "*" 7 (Prelude.*) +(*) :: (LOps l) => l Int -> l Int -> l Int +(*) = infixopl "*" 7 (Prelude.*) + Index: sizechecking/branches/macs/Size.hs =================================================================== --- sizechecking/branches/macs/Size.hs (revision 24) +++ sizechecking/branches/macs/Size.hs (revision 25) @@ -1,2 +1,6 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} + module Size where @@ -13,4 +17,5 @@ unsized :: l Unsized bottom :: l a + instance Size S where @@ -46,2 +51,3 @@ . showChar ' ' . unS e2 s3 2 + Index: sizechecking/branches/macs/Tests/ExpTest.hs =================================================================== --- sizechecking/branches/macs/Tests/ExpTest.hs (revision 25) +++ sizechecking/branches/macs/Tests/ExpTest.hs (revision 25) @@ -0,0 +1,51 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} + +module Tests.ExpTest where + +import Lambda +import Exp +import Prelude ( ($), Int, (==), return, sequence, (>>=), and, (.), IO, Bool, String, const ) +import qualified Control.Monad + +testNil :: Exp e => e [a] +testNil = nil + +testAddOne :: Exp e => e ([Int] -> [Int]) +testAddOne = lam $ \l -> cons (lit 1) l + +testHead :: Exp e => e ([a] -> a) +testHead = lam $ \l -> match l undefined const + +testTail :: Exp e => e ([a] -> [a]) +testTail = lam $ \l -> match l undefined $ \_ xs -> xs + +testConcat :: Exp e => e ([a] -> [a] -> [a]) +testConcat = lam $ \l1 -> lam $ \l2 -> match l1 l2 + $ \x xs -> cons x (testConcat `app` xs `app` l2) + +testDCons :: Exp e => e [Int] +testDCons = cons (lit 1) $ cons (lit 2) nil + +testD2Cons :: Exp e => e [[Int]] +testD2Cons = cons (cons (lit 1) nil) nil + +checkAST :: S a -> String -> IO Bool +checkAST exp repr = ast exp >>= (\t -> return $ t "" == repr ) + +tests :: [ IO Bool ] +tests = + [ return $ ([]::[Int]) == eval testNil + , checkAST testNil "[]" + , return $ [1::Int] == eval (testAddOne `app` nil) + , checkAST testAddOne "λa.1:a" + , return $ [2..6::Int] == eval testTail [1..6] + , return $ [1..6::Int] == eval testConcat [1,2,3] [4,5,6] + , return $ [1,2::Int] == eval testDCons + , checkAST testDCons "1:2:[]" + , return $ [[1::Int]] == eval testD2Cons + , checkAST testD2Cons "(1:[]):[]" + ] + + +runTests :: IO Bool +runTests = Control.Monad.liftM and $ sequence tests Index: sizechecking/branches/macs/Tests/LambdaTest.hs =================================================================== --- sizechecking/branches/macs/Tests/LambdaTest.hs (revision 25) +++ sizechecking/branches/macs/Tests/LambdaTest.hs (revision 25) @@ -0,0 +1,27 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} + +module Tests.LambdaTest where + +import Lambda +import Prelude ( ($), Int, (==), return, sequence, (>>=), and, (.), IO, Bool ) +import qualified Control.Monad + +test1 :: (Lambda l) => l Int +test1 = app (lam $ \_ -> lit 3) (lit 2) + +test1ast :: IO Bool +test1ast = do + t <- ast test1 + return $ t "" == "(λa.3) 2" + +test1eval :: IO Bool +test1eval = return $ eval test1 == 3 + +tests :: [IO Bool] +tests = [ + test1ast + , test1eval + ] + +runTests :: IO Bool +runTests = Control.Monad.liftM and $ sequence tests Index: sizechecking/branches/macs/Tests/Main.hs =================================================================== --- sizechecking/branches/macs/Tests/Main.hs (revision 25) +++ sizechecking/branches/macs/Tests/Main.hs (revision 25) @@ -0,0 +1,17 @@ +module Tests.Main where + +import qualified Tests.LambdaTest (tests) +import qualified Tests.OpsTest (tests) +import qualified Tests.SizeTest (tests) +import qualified Tests.ExpTest (tests) +import Control.Monad + +tests :: [IO Bool] +tests = Tests.LambdaTest.tests + ++ Tests.OpsTest.tests + ++ Tests.SizeTest.tests + ++ Tests.ExpTest.tests + +main :: IO () +main = liftM and ( sequence tests ) >>= print + Index: sizechecking/branches/macs/Tests/OpsTest.hs =================================================================== --- sizechecking/branches/macs/Tests/OpsTest.hs (revision 25) +++ sizechecking/branches/macs/Tests/OpsTest.hs (revision 25) @@ -0,0 +1,51 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} + +module Tests.OpsTest where + +import Ops +import Lambda +import Prelude ( ($), Int, (==), return, sequence, (>>=), and, (.), IO, Bool ) +import qualified Control.Monad + +test1 :: (LOps l) => l Int +test1 = app (lam $ \x -> lit 3 + x) (lit 2) + +test2 :: (LOps l) => l Int +test2 = app (lam $ \x -> lit 3 * x) (lit 2) + +test3 :: (LOps l) => l Int +test3 = app (lam $ \x -> lit 2 * x + lit 1) (lit 5 - lit 2) + + +test1ast :: IO Bool +test1ast = do + t <- ast test1 + return $ t "" == "(λa.3+a) 2" + +test1eval :: IO Bool +test1eval = return $ eval test1 == 5 + +test2ast :: IO Bool +test2ast = do + t <- ast test2 + return $ t "" == "(λa.3*a) 2" + +test2eval :: IO Bool +test2eval = return $ eval test2 == 6 + +test3ast :: IO Bool +test3ast = do + t <- ast test3 + return $ t "" == "(λa.2*a+1) (5-2)" + +test3eval :: IO Bool +test3eval = return $ eval test3 == 7 + +tests :: [IO Bool] +tests = [ + test1ast + , test1eval + ] + +runTests :: IO Bool +runTests = Control.Monad.liftM and $ sequence tests Index: sizechecking/branches/macs/Tests/SizeTest.hs =================================================================== --- sizechecking/branches/macs/Tests/SizeTest.hs (revision 25) +++ sizechecking/branches/macs/Tests/SizeTest.hs (revision 25) @@ -0,0 +1,40 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} + +module Tests.SizeTest where + +import Size +import Lambda +import Ops +import Prelude ( ($), Int, (==), return, sequence, (>>=), and, (.), IO, Bool, String, const ) +import qualified Control.Monad + +testEmpty1 :: (Size l) => l [Unsized] +testEmpty1 = list (lit 0) (lam $ const unsized) + +testNil :: (Size l) => l [a] +testNil = list (lit 0) (lam $ const bottom) + +testHead :: (Size l) => l ([a] -> a) +testHead = slam $ \s f -> f `app` (s - lit 1) + +testTail :: (Size l) => l ([a] -> [a]) +testTail = slam $ \s f -> list (s - lit 1) f + +testCons :: Size l => l (a -> [a] -> [a]) +testCons = lam $ \x -> slam $ \s f -> + list (s + lit 1) $ shift f s (lam $ const x) + +checkAst :: S a -> String -> IO Bool +checkAst exp repr = ast exp >>= (\t -> return $ t "" == repr) + +tests :: [IO Bool] +tests = [ + checkAst testEmpty1 "List 0 (λa.U)" + , checkAst testNil "List 0 (λa.┮)" + , checkAst testHead "Λa,b.b (a-1)" + , checkAst testTail "Λa,b.List (a-1) b" + , checkAst testCons "λa.Λb,c.List (b+1) (Shift c b (λd.a))" + ] + +runTests :: IO Bool +runTests = Control.Monad.liftM and $ sequence tests Index: sizechecking/branches/macs/sizechecking.cabal =================================================================== --- sizechecking/branches/macs/sizechecking.cabal (revision 25) +++ sizechecking/branches/macs/sizechecking.cabal (revision 25) @@ -0,0 +1,57 @@ +-- 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: Lambda + + -- Modules included in this library but not exported. + -- other-modules: + + -- Other library packages from which modules are imported. + build-depends: base ==4.*, containers ==0.5.*, sbv, value-supply, + transformers