![(please configure the [header_logo] section in trac.ini)](/trac/tamop/chrome/site/your_project_logo.png){kind=logo}
Changeset 8
- Timestamp:
- Nov 13, 2012, 11:27:26 PM (13 years ago)
- File:
-
- 1 edited
-
sizechecking/L.hs (modified) (9 diffs)
Legend:
- Unmodified
- Added
- Removed
-
sizechecking/L.hs
r7 r8 3 3 import Data.Char(ord, chr) 4 4 import Control.Monad.State 5 import Data.Supply5 --import Data.Supply 6 6 7 7 data OpName = PLUS | MINUS | MUL … … 10 10 11 11 {- Lambda calculus without free variables -} 12 type Arr repr a b = repr a -> repr b 13 12 14 class Lambda l where 13 labs :: (l a -> l b) -> l ( a ->b)14 app :: l ( a ->b) -> l a -> l b15 labs :: (l a -> l b) -> l (Arr l a b) 16 app :: l (Arr l a b) -> l a -> l b 15 17 lit :: Int -> l Int 16 18 op :: l Int -> OpName -> l Int -> l Int … … 18 20 class SizeExp l where 19 21 type List l :: * -> * 20 list :: l Int -> l ( Int ->b) -> l (List l b)21 aabs :: (l Int -> l ( Int -> a) -> l b) -> l (List l a ->b)22 shift :: l ( Int -> a) -> l Int -> l (Int -> a) -> l (Int ->a)22 list :: l Int -> l (Arr l Int b) -> l (List l b) 23 aabs :: (l Int -> l (Arr l Int a) -> l b) -> l (Arr l (List l a) b) 24 shift :: l (Arr l Int a) -> l Int -> l (Arr l Int a) -> l (Arr l Int a) 23 25 undef :: l Bottom 24 26 unsized :: l () … … 33 35 34 36 {- Printing -} 35 newtype LPrint a = LPrint { unPrint :: Int -> State IntShowS }37 newtype LPrint a = LPrint { unPrint :: Int -> Int -> ShowS } 36 38 37 39 instance Lambda LPrint where 38 lit x = LPrint $ \ p-> return $ shows x40 lit x = LPrint $ \_ -> return $ shows x 39 41 op m opc n = LPrint $ \p -> do 40 42 let (prec, lprec, rprec, c) = getPrec opc … … 46 48 l2 <- unPrint v 7 47 49 return $ showParen (p>6) $ l1 . showChar ' ' . l2 48 labs e = LPrint $ \p -> do 49 v <- getVar 50 let var = LPrint $ \_ -> return $ showVar v 51 l <- unPrint (e var) 0 52 return $ showParen (p>0) $ showChar 'λ' . showVar v . showChar '.' . l 50 labs e = LPrint $ \p v -> let 51 var = LPrint $ \_ -> return $ showVar v 52 l = unPrint (e var) 0 $ succ v 53 in showParen (p>0) $ showChar 'λ' . showVar v . showChar '.' . l 53 54 54 55 instance SizeExp LPrint where 55 56 type List LPrint = [] 56 aabs f = LPrint $ \p -> do 57 v1 <- getVar 58 v2 <- getVar 59 let var1 = LPrint $ \_ -> return $ showVar v1 60 var2 = LPrint $ \_ -> return $ showVar v2 61 l <- unPrint (f var1 var2) 0 62 return $ showParen (p>0) $ showChar 'Î' . showVar v1 . showChar ',' . showVar v2 . showChar '.' . l 57 aabs f = LPrint $ \p v -> let 58 v2 = succ v 59 var1 = LPrint $ \_ _ -> showVar v 60 var2 = LPrint $ \_ _ -> showVar v2 61 l = unPrint (f var1 var2) 0 (v+2) 62 in showParen (p>0) $ showChar 'Î' . showVar v . showChar ',' . showVar v2 . showChar '.' . l 63 63 list s f = LPrint $ \p -> do 64 64 l1 <- unPrint s 9 … … 73 73 unsized = LPrint $ \_ -> return $ showChar 'U' 74 74 75 mprint x = putStrLn $ (fst $ runState (unPrint x 0) 0) "" 75 view :: LPrint a -> LPrint a 76 view = id 77 instance Show (LPrint a) where 78 showsPrec _ e = unPrint e 0 0 76 79 77 80 showVar x = if x>28 … … 105 108 newtype R a = R { unR :: a } 106 109 instance Lambda R where 107 labs f = R $ unR . f . R108 app e1 e2 = R $ (unR e1) (unR e2)110 labs f = R $ f 111 app e1 e2 = (unR e1) e2 109 112 lit i = R i 110 113 op e1 op e2 = let opm = case op of … … 115 118 116 119 newtype RList a = RList { unList :: (Int, Int -> a) } 117 instance (Show a) => Show (RList a) where118 show (RList (s,f)) = show (map f [0..s-1])120 --instance (Show a) => Show (RList a) where 121 -- show (RList (s,f)) = show (map f [0..s-1]) 119 122 120 123 instance SizeExp R where … … 122 125 undef = R $ Bottom 123 126 unsized = R $ () 124 list s f = R $ RList (unR s, unR f) 125 aabs e = R $ \(RList (s,f)) -> unR (e (R s) (R f)) 126 shift a s c = R $ \i -> if i<(unR s) then unR a i else unR c i 127 128 {- Create a restricted deep embedding to work with the expression -} 129 130 {- sized [a] to prove -} 131 data Nil 132 data Cons a 133 data SLInt a where 134 SLNil :: SLInt Nil 135 SLCons :: Int -> SLInt a -> SLInt (Cons a) 136 137 class MGS a where 138 mgs :: Supply Int -> a -> a 139 mgs = mgs' [] 140 mgs' :: [Int] -> Supply Int -> a -> a 141 142 143 instance MGS () where 144 mgs' _ _ _ = () 145 instance MGS a => MGS (RList a) where 146 mgs' bound supp _ = RList undefined 147 where 148 (s1, s2, s3) = split3 supp 149 listsize = mgs' bound supp (undefined :: a) 127 list s f = R $ RList (unR s, unR . (unR f) . R ) 128 --aabs :: Arr l Int (Arr l (Arr l Int a) b) -> l (Arr l (List l a) b) 129 -- aabs e = R $ \(RList (s,f)) -> unR (e (R s) (R f)) 130 -- shift a s c = R $ \i -> if i<(unR s) then unR a i else unR c i 131 132 -- Type level int to count arity 133 data Zero 134 data Succ a 135 136 data Exp a where 137 Lit :: Int -> Exp Zero 138 Op :: Exp Zero -> OpName -> Exp Zero -> Exp Zero 139 App :: Exp (Succ a) -> Exp Zero -> Exp a 140 Var :: Int -> Exp a 141 142 instance Show (Exp a) where 143 showsPrec _ (Lit a) = shows a 144 showsPrec p (Op lhs op rhs) = 145 let (prec, lprec, rprec, c) = getPrec op 146 in showParen (p>prec) $ showsPrec lprec lhs . showChar c . showsPrec rprec rhs 147 showsPrec p (App lhs rhs) = 148 showParen (p>6) $ showsPrec 6 lhs . showChar ' ' . showsPrec 7 rhs 149 showsPrec _ (Var i) = showVar i 150 151 type IntExp = Exp Zero 152 data Condition = Eq IntExp IntExp | Gt IntExp IntExp | Lt IntExp IntExp 153 type SExp = ([Condition], IntExp) 154 newtype Compile a = Compile { unCompile :: SExp } 155 156 --instance Lambda Compile where 157 -- labs :: (l a -> l b) -> l (a -> b) 158 -- labs f = Compile $ f 159 160 161 --{- Create a restricted deep embedding to work with the expression -} 162 --{- sized [a] to prove -} 163 -- 164 --class Restricted a where 165 -- kind :: a -> Int 166 -- 167 --instance Restricted Int where 168 -- kind _ = 0 169 -- 170 --instance Restricted a => Restricted (Int -> a) where 171 -- kind _ = succ $ kind $ (undefined :: a) 172 -- 173 --class Var l where 174 -- var :: Restricted a => Int -> l a 175 -- 176 --showVar2 x = showChar '_' . showVar x 177 -- 178 --newtype Count a = C { count :: Int } 179 --cnv :: Restricted a => Count a -> a 180 --cnv = undefined 181 -- 182 --ckind :: (Restricted a) => Count a -> Int 183 --ckind = kind . cnv 184 -- 185 --instance Var Count where 186 -- var _ = undefined 187 -- 188 --instance Var LPrint where 189 -- var x = LPrint $ \_ -> return $ showVar2 x 190 -- 191 --class MGS a where 192 -- mgs :: Supply Int -> a -> a 193 -- mgs = mgs' [] 194 -- mgs' :: [Int] -> Supply Int -> a -> a 195 -- 196 --instance MGS () where 197 -- mgs' _ _ _ = () 198 -- 199 --instance MGS a => MGS (RList a) where 200 -- mgs' bound supp _ = RList (listsize, undefined) 201 -- where 202 -- (s1, s2, s3) = split3 supp 203 -- listsize = mgs' bound supp (undefined :: a)
Note: See TracChangeset
for help on using the changeset viewer.
