module Language.Glambda.Type (
Ty(..), readTyCon,
STy(..), SCtx(..), ITy(..),
emptyContext, refineTy, unrefineTy, eqSTy,
) where
import Language.Glambda.Util
import Text.PrettyPrint.ANSI.Leijen
data Ty
= Arr Ty Ty
| IntTy
| BoolTy
deriving Eq
infixr 1 `Arr`
readTyCon :: String -> Maybe Ty
readTyCon "Int" = Just IntTy
readTyCon "Bool" = Just BoolTy
readTyCon _ = Nothing
data STy :: * -> * where
SArr :: STy arg -> STy res -> STy (arg -> res)
SIntTy :: STy Int
SBoolTy :: STy Bool
infixr 1 `SArr`
class ITy ty where
sty :: STy ty
instance (ITy arg, ITy res) => ITy (arg -> res) where
sty = sty `SArr` sty
instance ITy Int where
sty = SIntTy
instance ITy Bool where
sty = SBoolTy
data SCtx :: [*] -> * where
SNil :: SCtx '[]
SCons :: STy h -> SCtx t -> SCtx (h ': t)
infixr 5 `SCons`
emptyContext :: SCtx '[]
emptyContext = SNil
refineTy :: Ty -> (forall ty. STy ty -> r) -> r
refineTy (ty1 `Arr` ty2) k
= refineTy ty1 $ \sty1 ->
refineTy ty2 $ \sty2 ->
k (sty1 `SArr` sty2)
refineTy IntTy k = k SIntTy
refineTy BoolTy k = k SBoolTy
unrefineTy :: STy ty -> Ty
unrefineTy (arg `SArr` res) = unrefineTy arg `Arr` unrefineTy res
unrefineTy SIntTy = IntTy
unrefineTy SBoolTy = BoolTy
eqSTy :: STy ty1 -> STy ty2 -> Maybe (ty1 :~: ty2)
eqSTy (s1 `SArr` t1) (s2 `SArr` t2)
| Just Refl <- s1 `eqSTy` s2
, Just Refl <- t1 `eqSTy` t2
= Just Refl
eqSTy SIntTy SIntTy = Just Refl
eqSTy SBoolTy SBoolTy = Just Refl
eqSTy _ _ = Nothing
instance Pretty Ty where
pretty = pretty_ty topPrec
instance Show Ty where
show = render . pretty
instance Pretty (STy ty) where
pretty = pretty . unrefineTy
arrowLeftPrec, arrowRightPrec, arrowPrec :: Prec
arrowLeftPrec = 5
arrowRightPrec = 4.9
arrowPrec = 5
pretty_ty :: Prec -> Ty -> Doc
pretty_ty prec (Arr arg res) = maybeParens (prec >= arrowPrec) $
hsep [ pretty_ty arrowLeftPrec arg
, text "->"
, pretty_ty arrowRightPrec res ]
pretty_ty _ IntTy = text "Int"
pretty_ty _ BoolTy = text "Bool"