source: sizechecking/L.hs @ 9

{-# Language GADTs, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables, TypeFamilies, NoMonomorphismRestriction #-}

import Data.Char(ord, chr)
import Control.Monad.State
--import Data.Supply

data OpName = PLUS | MINUS | MUL
data Bottom = Bottom
  deriving Show

{- Lambda calculus without free variables -}
type Arr repr a b = repr a -> repr b
--type family Arr (repr :: * -> *) (a :: *) (b :: *) :: *

class Lambda l where
    labs    :: (l a -> l b) -> l (Arr l a b)
    app     :: l (Arr l a b) -> l a -> l b
    lit     :: Int -> l Int
    op      :: l Int -> OpName -> l Int -> l Int

class SizeExp l where
    type List l :: * -> *
    list    :: l Int -> l (Arr l Int b) -> l (List l b)
    aabs    :: (l Int -> l (Arr l Int a) -> l b) -> l (Arr l (List l a) b)
    shift   :: l (Arr l Int a) -> l Int -> l (Arr l Int a) -> l (Arr l Int a)
    undef   :: l Bottom
    unsized :: l ()

instance Lambda l => Num (l Int) where
    fromInteger = lit . fromIntegral
    lhs + rhs   = op lhs PLUS rhs
    lhs - rhs   = op lhs MINUS rhs
    lhs * rhs   = op lhs MUL rhs
    abs = error "abs is not implemented"
    signum = error "signum is not implemented"

{- Printing -}
newtype LPrint a = LPrint { unPrint :: Int -> Int -> ShowS }

instance Lambda LPrint where
  lit x      = LPrint $ \_ -> return $ shows x
  op m opc n = LPrint $ \p -> do
    let (prec, lprec, rprec, c) = getPrec opc
    l1 <- (unPrint m lprec)
    l2 <- (unPrint n rprec)
    return $ showParen (p>prec) $  l1 . showChar c . l2
  app f v    = LPrint $ \p -> do
    l1 <- unPrint f 6
    l2 <- unPrint v 7
    return $ showParen (p>6) $ l1 . showChar ' ' . l2
  labs e      = LPrint $ \p v -> let
    var = LPrint $ \_ -> return $ showVar v
    l = unPrint (e var) 0 $ succ v
    in showParen (p>0) $ showChar 'λ' . showVar v . showChar '.' . l

instance SizeExp LPrint where
  type List LPrint = []
  aabs f   = LPrint $ \p v -> let 
    v2 = succ v
    var1 = LPrint $ \_ _ -> showVar v
    var2 = LPrint $ \_ _ -> showVar v2
    l = unPrint (f var1 var2) 0 (v+2)
    in showParen (p>0) $ showChar 'Λ' . showVar v . showChar ',' . showVar v2 . showChar '.' . l
  list s f = LPrint $ \p -> do
    l1 <- unPrint s 9
    l2 <- unPrint f 9
    return $ showParen (p>0) $ showString "List " . l1 . showChar ' ' . l2
  shift e1 s e2 = LPrint $ \p -> do
    l1 <- unPrint e1 2
    l2 <- unPrint s 2
    l3 <- unPrint e2 2
    return $ showParen (p>0) $ showString "Shift " . l1 .  showChar ' ' . l2 . showChar ' ' . l3
  undef = LPrint $ \_ -> return $ showChar '┮'
  unsized = LPrint $ \_ -> return $ showChar 'U'

view :: LPrint a -> LPrint a
view = id
instance Show (LPrint a) where
    showsPrec _ e = unPrint e 0 0

showVar x = if x>28 
    then showVar (x `div` 29) . showChar (chr $ ord 'a' + (x `mod` 29))
    else showChar $ chr $ ord 'a' + x

getPrec :: OpName -> (Int,Int,Int,Char)
getPrec PLUS = (4,4,5,'+')
getPrec MINUS = (4,4,5,'-')
getPrec MUL = (5,5,6,'*')

getVar :: State Int Int
getVar = do { x <- get; put (x+1); return x }

x = aabs (\s _ -> s) `app` list (lit 0) (labs $ \_ -> undef)
y = list 0 $ labs $ \_ -> undef
z = (labs $ \s -> s+1) `app` (lit 1+2)
conss = labs $ \x -> aabs $ \ys yf -> list (ys + 1) $ shift yf ys (labs $ \_ -> x)
concats = aabs $ \xs xf -> (aabs $ \ys yf -> list (xs+ys) $ shift xf xs yf)
maps = labs $ \x -> aabs $ \ys yf -> list ys ( x `app` yf )
l0 = list (lit 0) (labs $ \_ -> unsized)
l1 = list (lit 1) (labs $ \_ -> unsized)
l2 = list (lit 2) (labs $ \_ -> unsized)
l00 = list (lit 0) (labs $ \_ -> list (lit 0) (labs $ \_ -> unsized))
l10 = list (lit 1) (labs $ \_ -> list (lit 0) (labs $ \_ -> unsized))
l01 = list (lit 0) (labs $ \_ -> list (lit 1) (labs $ \_ -> unsized))
l11 = list (lit 1) (labs $ \_ -> list (lit 1) (labs $ \_ -> unsized))
l12 = list (lit 1) (labs $ \_ -> list (lit 2) (labs $ \_ -> unsized))

{- Evaluating -}
newtype R a = R { unR :: a }
instance Lambda R where
  labs f      = R $ f 
  app e1 e2   = (unR e1) e2
  lit i       = R i
  op e1 op e2 = let opm = case op of
                                  PLUS  -> (+)
                                  MINUS -> (-)
                                  MUL   -> (*)
                in R $ opm (unR e1) (unR e2)

newtype RList a = RList { unList :: (Int, Int -> a)  }
instance (Show a) => Show (RList a) where
  show (RList (s,f)) = show (map f [0..s-1])

instance SizeExp R where
  type List R = RList
  undef       = R $ Bottom
  unsized     = R $ ()
  list s f    = R $ RList (unR s, unR . (unR f) . R )
  aabs e = R $ ( \(RList (s,f)) -> (e (R s) (R (R . f . unR))) ) . unR
  shift a s c = R $ \i -> if (unR i)<(unR s) then unR a i else unR c i

-- Type level int to count arity
data Zero
data Succ a

data Exp a where
    Lit :: Int -> Exp Zero
    Op  :: Exp Zero -> OpName -> Exp Zero -> Exp Zero
    App :: Exp (Succ a) -> Exp Zero -> Exp a
    Var :: Int -> Exp a

instance Show (Exp a) where
    showsPrec _ (Lit a)         = shows a
    showsPrec p (Op lhs op rhs) =
        let (prec, lprec, rprec, c) = getPrec op
        in showParen (p>prec) $  showsPrec lprec lhs . showChar c . showsPrec rprec rhs
    showsPrec p (App lhs rhs)   =
        showParen (p>6) $ showsPrec 6 lhs . showChar ' ' . showsPrec 7 rhs
    showsPrec _ (Var i)         = showVar i

type IntExp = Exp Zero
data Condition = Eq IntExp IntExp | Gt IntExp IntExp | Lt IntExp IntExp
type SExp a = ([Condition], IntExp)
newtype Compile a = Compile { unCompile :: SExp a }

--instance Lambda Compile where
--  labs :: (l a -> l b) -> l (a -> b)
--    labs f = Compile $ f


--{- Create a restricted deep embedding to work with the expression -}
--{- sized [a] to prove -}
--
--class Restricted a where
--    kind :: a -> Int
--
--instance Restricted Int where
--    kind _ = 0
--
--instance Restricted a => Restricted (Int -> a) where
--    kind _ = succ $ kind $ (undefined :: a)
--
--class Var l where
--    var :: Restricted a => Int -> l a
--
--showVar2 x = showChar '_' . showVar x
--
--newtype Count a = C { count :: Int }
--cnv :: Restricted a => Count a -> a
--cnv = undefined
--
--ckind :: (Restricted a) => Count a -> Int
--ckind = kind . cnv
--
--instance Var Count where
--    var _ = undefined
--
--instance Var LPrint where
--    var x = LPrint $ \_ -> return $ showVar2 x
--
--class MGS a where
--  mgs :: Supply Int -> a -> a
--  mgs = mgs' []
--  mgs' :: [Int] -> Supply Int -> a -> a
--
--instance MGS () where
--  mgs' _ _ _ = ()
--
--instance MGS a => MGS (RList a) where
--  mgs' bound supp  _ = RList (listsize, undefined)
--    where
--    (s1, s2, s3) = split3 supp
--    listsize = mgs' bound supp (undefined :: a)