module Language.Core.Core where
import Language.Core.Encoding
import Data.Generics
import Data.List (elemIndex)
import Data.Char
data Module
= Module AnMname [Tdef] [Vdefg]
deriving (Data, Typeable)
data Tdef
= Data (Qual Tcon) [Tbind] [Cdef]
| Newtype (Qual Tcon) (Qual Tcon) [Tbind] Ty
deriving (Data, Typeable)
data Cdef
= Constr (Qual Dcon) [Tbind] [Ty]
deriving (Data, Typeable)
data Vdefg
= Rec [Vdef]
| Nonrec Vdef
deriving (Data, Typeable)
newtype Vdef = Vdef (Qual Var,Ty,Exp)
deriving (Data, Typeable)
data Exp
= Var (Qual Var)
| Dcon (Qual Dcon)
| Lit Lit
| App Exp Exp
| Appt Exp Ty
| Lam Bind Exp
| Let Vdefg Exp
| Case Exp Vbind Ty [Alt]
| Cast Exp Ty
| Note String Exp
| External String Ty
deriving (Data, Typeable)
data Bind
= Vb Vbind
| Tb Tbind
deriving (Data, Typeable)
data Alt
= Acon (Qual Dcon) [Tbind] [Vbind] Exp
| Alit Lit Exp
| Adefault Exp
deriving (Data, Typeable)
type Vbind = (Var,Ty)
type Tbind = (Tvar,Kind)
data Ty
= Tvar Tvar
| Tcon (Qual Tcon)
| Tapp Ty Ty
| Tforall Tbind Ty
| TransCoercion Ty Ty
| SymCoercion Ty
| UnsafeCoercion Ty Ty
| InstCoercion Ty Ty
| LeftCoercion Ty
| RightCoercion Ty
deriving (Data, Typeable)
data Kind
= Klifted
| Kunlifted
| Kopen
| Karrow Kind Kind
| Keq Ty Ty
deriving (Data, Typeable)
data CoercionKind =
DefinedCoercion [Tbind] (Ty,Ty)
data KindOrCoercion = Kind Kind | Coercion CoercionKind
data Lit = Literal CoreLit Ty
deriving (Data, Typeable, Eq)
data CoreLit = Lint Integer
| Lrational Rational
| Lchar Char
| Lstring String
deriving (Data, Typeable, Eq)
type Mname = Maybe AnMname
newtype AnMname = M (Pname, [Id], Id)
deriving (Eq, Ord, Data, Typeable)
newtype Pname = P Id
deriving (Eq, Ord, Data, Typeable)
type Var = Id
type Tvar = Id
type Tcon = Id
type Dcon = Id
type Qual t = (Mname,t)
qual :: AnMname -> t -> Qual t
qual mn t = (Just mn, t)
unqual :: t -> Qual t
unqual = (,) Nothing
getModule :: Qual t -> Mname
getModule = fst
type Id = String
eqKind :: Kind -> Kind -> Bool
eqKind Klifted Klifted = True
eqKind Kunlifted Kunlifted = True
eqKind Kopen Kopen = True
eqKind (Karrow k1 k2) (Karrow l1 l2) = k1 `eqKind` l1
&& k2 `eqKind` l2
eqKind (Keq t1 t2) (Keq u1 u2) = t1 == u1
&& t2 == u2
eqKind _ _ = False
splitTyConApp_maybe :: Ty -> Maybe (Qual Tcon,[Ty])
splitTyConApp_maybe (Tvar _) = Nothing
splitTyConApp_maybe (Tcon t) = Just (t,[])
splitTyConApp_maybe (Tapp rator rand) =
case (splitTyConApp_maybe rator) of
Just (r,rs) -> Just (r,rs++[rand])
Nothing -> case rator of
Tcon tc -> Just (tc,[rand])
_ -> Nothing
splitTyConApp_maybe (Tforall _ _) = Nothing
splitTyConApp_maybe _ = Nothing
equalTy :: Ty -> Ty -> Bool
equalTy t1 t2 = eqTy [] [] t1 t2
where eqTy e1 e2 (Tvar v1) (Tvar v2) =
case (elemIndex v1 e1,elemIndex v2 e2) of
(Just i1, Just i2) -> i1 == i2
(Nothing, Nothing) -> v1 == v2
_ -> False
eqTy _ _ (Tcon c1) (Tcon c2) = c1 == c2
eqTy e1 e2 (Tapp t1a t1b) (Tapp t2a t2b) =
eqTy e1 e2 t1a t2a && eqTy e1 e2 t1b t2b
eqTy e1 e2 (Tforall (tv1,tk1) b1) (Tforall (tv2,tk2) b2) =
tk1 `eqKind` tk2 && eqTy (tv1:e1) (tv2:e2) b1 b2
eqTy _ _ _ _ = False
instance Eq Ty where (==) = equalTy
subKindOf :: Kind -> Kind -> Bool
_ `subKindOf` Kopen = True
(Karrow a1 r1) `subKindOf` (Karrow a2 r2) =
a2 `subKindOf` a1 && (r1 `subKindOf` r2)
k1 `subKindOf` k2 = k1 `eqKind` k2
baseKind :: Kind -> Bool
baseKind (Karrow _ _ ) = False
baseKind _ = True
isPrimVar (Just mn,_) = mn == primMname
isPrimVar _ = False
primMname = mkPrimMname "Prim"
errMname = mkBaseMname "Err"
mkBaseMname,mkPrimMname :: Id -> AnMname
mkBaseMname mn = M (basePkg, ghcPrefix, mn)
mkPrimMname mn = M (primPkg, ghcPrefix, mn)
basePkg = P "base"
mainPkg = P "main"
primPkg = P $ zEncodeString "ghc-prim"
ghcPrefix = ["GHC"]
mainPrefix = []
boolMname = mkPrimMname "Bool"
mainVar = qual mainMname "main"
wrapperMainVar = qual wrapperMainMname "main"
mainMname = M (mainPkg, mainPrefix, "Main")
wrapperMainMname = M (mainPkg, mainPrefix, "ZCMain")
wrapperMainAnMname = Just wrapperMainMname
dcTrue :: Dcon
dcTrue = "True"
dcFalse :: Dcon
dcFalse = "False"
tcArrow :: Qual Tcon
tcArrow = (Just primMname, "ZLzmzgZR")
tArrow :: Ty -> Ty -> Ty
tArrow t1 t2 = Tapp (Tapp (Tcon tcArrow) t1) t2
mkFunTy :: Ty -> Ty -> Ty
mkFunTy randTy resultTy =
Tapp (Tapp (Tcon tcArrow) randTy) resultTy
ktArrow :: Kind
ktArrow = Karrow Kopen (Karrow Kopen Klifted)
maxUtuple :: Int
maxUtuple = 100
tcUtuple :: Int -> Qual Tcon
tcUtuple n = (Just primMname,"Z"++ (show n) ++ "H")
ktUtuple :: Int -> Kind
ktUtuple n = foldr Karrow Kunlifted (replicate n Kopen)
tUtuple :: [Ty] -> Ty
tUtuple ts = foldl Tapp (Tcon (tcUtuple (length ts))) ts
isUtupleTy :: Ty -> Bool
isUtupleTy (Tapp t _) = isUtupleTy t
isUtupleTy (Tcon tc) =
case tc of
(Just pm, 'Z':rest) | pm == primMname && last rest == 'H' ->
let mid = take ((length rest) 1) rest in
all isDigit mid && (let num = read mid in
1 <= num && num <= maxUtuple)
_ -> False
isUtupleTy _ = False
dcUtuple :: Int -> Qual Dcon
dcUtuple n = (Just primMname,"Z" ++ (show n) ++ "H")
isUtupleDc :: Qual Dcon -> Bool
isUtupleDc dc = dc `elem` [dcUtuple n | n <- [1..maxUtuple]]
dcUtupleTy :: Int -> Ty
dcUtupleTy n =
foldr ( \tv t -> Tforall (tv,Kopen) t)
(foldr ( \tv t -> tArrow (Tvar tv) t)
(tUtuple (map Tvar tvs)) tvs)
tvs
where tvs = map ( \i -> ("a" ++ (show i))) [1..n]
utuple :: [Ty] -> [Exp] -> Exp
utuple ts es = foldl App (foldl Appt (Dcon (dcUtuple (length es))) ts) es
flattenBinds :: [Vdefg] -> [Vdef]
flattenBinds (Nonrec vd : binds) = vd : flattenBinds binds
flattenBinds (Rec prs1 : binds) = prs1 ++ flattenBinds binds
flattenBinds [] = []
unitMname :: AnMname
unitMname = mkPrimMname "Unit"