module Cryptol.TypeCheck.AST
( module Cryptol.TypeCheck.AST
, Name()
, TFun(..)
, Selector(..)
, Import(..)
, ImportSpec(..)
, ExportType(..)
, ExportSpec(..), isExportedBind, isExportedType
, Pragma(..)
, Fixity(..)
, PrimMap(..)
) where
import Cryptol.ModuleSystem.Name
import Cryptol.Prims.Syntax
import Cryptol.Parser.AST ( Selector(..),Pragma(..), ppSelector
, Import(..), ImportSpec(..), ExportType(..)
, ExportSpec(..), isExportedBind
, isExportedType, Fixity(..) )
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent)
import Cryptol.Utils.Panic(panic)
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Solver.InfNat
import GHC.Generics (Generic)
import Control.DeepSeq
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import Data.Set (Set)
data Module = Module { mName :: !ModName
, mExports :: ExportSpec Name
, mImports :: [Import]
, mTySyns :: Map Name TySyn
, mNewtypes :: Map Name Newtype
, mDecls :: [DeclGroup]
} deriving (Show, Generic, NFData)
data Kind = KType
| KNum
| KProp
| Kind :-> Kind
deriving (Eq, Show, Generic, NFData)
infixr 5 :->
data Schema = Forall { sVars :: [TParam], sProps :: [Prop], sType :: Type }
deriving (Eq, Show, Generic, NFData)
data TySyn = TySyn { tsName :: Name
, tsParams :: [TParam]
, tsConstraints :: [Prop]
, tsDef :: Type
}
deriving (Eq, Show, Generic, NFData)
data Newtype = Newtype { ntName :: Name
, ntParams :: [TParam]
, ntConstraints :: [Prop]
, ntFields :: [(Ident,Type)]
} deriving (Show, Generic, NFData)
data TParam = TParam { tpUnique :: !Int
, tpKind :: Kind
, tpName :: Maybe Name
}
deriving (Show, Generic, NFData)
instance Eq TParam where
x == y = tpUnique x == tpUnique y
instance Ord TParam where
compare x y = compare (tpUnique x) (tpUnique y)
tpVar :: TParam -> TVar
tpVar p = TVBound (tpUnique p) (tpKind p)
data Type = TCon TCon [Type]
| TVar TVar
| TUser Name [Type] Type
| TRec [(Ident,Type)]
deriving (Show, Eq, Ord, Generic, NFData)
type Prop = Type
type SType = Type
data TVar = TVFree !Int Kind (Set TVar) Doc
| TVBound !Int Kind
deriving (Show, Generic, NFData)
data TCon = TC TC | PC PC | TF TFun
deriving (Show, Eq, Ord, Generic, NFData)
data PC = PEqual
| PNeq
| PGeq
| PFin
| PHas Selector
| PArith
| PCmp
deriving (Show, Eq, Ord, Generic, NFData)
data TC = TCNum Integer
| TCInf
| TCBit
| TCSeq
| TCFun
| TCTuple Int
| TCNewtype UserTC
deriving (Show, Eq, Ord, Generic, NFData)
data UserTC = UserTC Name Kind
deriving (Show, Generic, NFData)
instance Eq UserTC where
UserTC x _ == UserTC y _ = x == y
instance Ord UserTC where
compare (UserTC x _) (UserTC y _) = compare x y
instance Eq TVar where
TVBound x _ == TVBound y _ = x == y
TVFree x _ _ _ == TVFree y _ _ _ = x == y
_ == _ = False
instance Ord TVar where
compare (TVFree x _ _ _) (TVFree y _ _ _) = compare x y
compare (TVFree _ _ _ _) _ = LT
compare _ (TVFree _ _ _ _) = GT
compare (TVBound x _) (TVBound y _) = compare x y
data Expr = EList [Expr] Type
| ETuple [Expr]
| ERec [(Ident,Expr)]
| ESel Expr Selector
| EIf Expr Expr Expr
| EComp Type Expr [[Match]]
| EVar Name
| ETAbs TParam Expr
| ETApp Expr Type
| EApp Expr Expr
| EAbs Name Type Expr
| EProofAbs Prop Expr
| EProofApp Expr
| ECast Expr Type
| EWhere Expr [DeclGroup]
deriving (Show, Generic, NFData)
data Match = From Name Type Expr
| Let Decl
deriving (Show, Generic, NFData)
data DeclGroup = Recursive [Decl]
| NonRecursive Decl
deriving (Show, Generic, NFData)
groupDecls :: DeclGroup -> [Decl]
groupDecls dg = case dg of
Recursive ds -> ds
NonRecursive d -> [d]
data Decl = Decl { dName :: !Name
, dSignature :: Schema
, dDefinition :: DeclDef
, dPragmas :: [Pragma]
, dInfix :: !Bool
, dFixity :: Maybe Fixity
, dDoc :: Maybe String
} deriving (Show, Generic, NFData)
data DeclDef = DPrim
| DExpr Expr
deriving (Show, Generic, NFData)
isFreeTV :: TVar -> Bool
isFreeTV (TVFree {}) = True
isFreeTV _ = False
isBoundTV :: TVar -> Bool
isBoundTV (TVBound {}) = True
isBoundTV _ = False
tIsNat' :: Type -> Maybe Nat'
tIsNat' ty =
case tNoUser ty of
TCon (TC (TCNum x)) [] -> Just (Nat x)
TCon (TC TCInf) [] -> Just Inf
_ -> Nothing
tIsNum :: Type -> Maybe Integer
tIsNum ty = do Nat x <- tIsNat' ty
return x
tIsInf :: Type -> Bool
tIsInf ty = tIsNat' ty == Just Inf
tIsVar :: Type -> Maybe TVar
tIsVar ty = case tNoUser ty of
TVar x -> Just x
_ -> Nothing
tIsFun :: Type -> Maybe (Type, Type)
tIsFun ty = case tNoUser ty of
TCon (TC TCFun) [a, b] -> Just (a, b)
_ -> Nothing
tIsSeq :: Type -> Maybe (Type, Type)
tIsSeq ty = case tNoUser ty of
TCon (TC TCSeq) [n, a] -> Just (n, a)
_ -> Nothing
tIsBit :: Type -> Bool
tIsBit ty = case tNoUser ty of
TCon (TC TCBit) [] -> True
_ -> False
tIsTuple :: Type -> Maybe [Type]
tIsTuple ty = case tNoUser ty of
TCon (TC (TCTuple _)) ts -> Just ts
_ -> Nothing
tIsBinFun :: TFun -> Type -> Maybe (Type,Type)
tIsBinFun f ty = case tNoUser ty of
TCon (TF g) [a,b] | f == g -> Just (a,b)
_ -> Nothing
tSplitFun :: TFun -> Type -> [Type]
tSplitFun f t0 = go t0 []
where go ty xs = case tIsBinFun f ty of
Just (a,b) -> go a (go b xs)
Nothing -> ty : xs
pIsFin :: Prop -> Maybe Type
pIsFin ty = case tNoUser ty of
TCon (PC PFin) [t1] -> Just t1
_ -> Nothing
pIsGeq :: Prop -> Maybe (Type,Type)
pIsGeq ty = case tNoUser ty of
TCon (PC PGeq) [t1,t2] -> Just (t1,t2)
_ -> Nothing
pIsEq :: Prop -> Maybe (Type,Type)
pIsEq ty = case tNoUser ty of
TCon (PC PEqual) [t1,t2] -> Just (t1,t2)
_ -> Nothing
pIsArith :: Prop -> Maybe Type
pIsArith ty = case tNoUser ty of
TCon (PC PArith) [t1] -> Just t1
_ -> Nothing
pIsCmp :: Prop -> Maybe Type
pIsCmp ty = case tNoUser ty of
TCon (PC PCmp) [t1] -> Just t1
_ -> Nothing
pIsNumeric :: Prop -> Bool
pIsNumeric (TCon (PC PEqual) _) = True
pIsNumeric (TCon (PC PNeq) _) = True
pIsNumeric (TCon (PC PGeq) _) = True
pIsNumeric (TCon (PC PFin) _) = True
pIsNumeric (TUser _ _ t) = pIsNumeric t
pIsNumeric _ = False
tNum :: Integral a => a -> Type
tNum n = TCon (TC (TCNum (fromIntegral n))) []
tZero :: Type
tZero = tNum (0 :: Int)
tOne :: Type
tOne = tNum (1 :: Int)
tTwo :: Type
tTwo = tNum (2 :: Int)
tInf :: Type
tInf = TCon (TC TCInf) []
tNat' :: Nat' -> Type
tNat' n' = case n' of
Inf -> tInf
Nat n -> tNum n
tBit :: Type
tBit = TCon (TC TCBit) []
tWord :: Type -> Type
tWord a = tSeq a tBit
tSeq :: Type -> Type -> Type
tSeq a b = TCon (TC TCSeq) [a,b]
tChar :: Type
tChar = tWord (tNum (8 :: Int))
tString :: Int -> Type
tString len = tSeq (tNum len) tChar
tRec :: [(Ident,Type)] -> Type
tRec = TRec
tTuple :: [Type] -> Type
tTuple ts = TCon (TC (TCTuple (length ts))) ts
infixr 5 `tFun`
tFun :: Type -> Type -> Type
tFun a b = TCon (TC TCFun) [a,b]
tNoUser :: Type -> Type
tNoUser t = case t of
TUser _ _ a -> tNoUser a
_ -> t
tWidth :: Type -> Type
tWidth t = TCon (TF TCWidth) [t]
tLenFromThen :: Type -> Type -> Type -> Type
tLenFromThen t1 t2 t3 = TCon (TF TCLenFromThen) [t1,t2,t3]
tLenFromThenTo :: Type -> Type -> Type -> Type
tLenFromThenTo t1 t2 t3 = TCon (TF TCLenFromThenTo) [t1,t2,t3]
tMax :: Type -> Type -> Type
tMax t1 t2 = TCon (TF TCMax) [t1,t2]
infix 4 =#=, >==
infixl 6 .+.
infixl 7 .*.
(=#=) :: Type -> Type -> Prop
x =#= y = TCon (PC PEqual) [x,y]
(=/=) :: Type -> Type -> Prop
x =/= y = TCon (PC PNeq) [x,y]
pArith :: Type -> Prop
pArith t = TCon (PC PArith) [t]
pCmp :: Type -> Prop
pCmp t = TCon (PC PCmp) [t]
(>==) :: Type -> Type -> Prop
x >== y = TCon (PC PGeq) [x,y]
pHas :: Selector -> Type -> Type -> Prop
pHas l ty fi = TCon (PC (PHas l)) [ty,fi]
pFin :: Type -> Prop
pFin ty = TCon (PC PFin) [ty]
(.*.) :: Type -> Type -> Type
x .*. y = TCon (TF TCMul) [x,y]
(.+.) :: Type -> Type -> Type
x .+. y = TCon (TF TCAdd) [x,y]
(.-.) :: Type -> Type -> Type
x .-. y = TCon (TF TCSub) [x,y]
(.^.) :: Type -> Type -> Type
x .^. y = TCon (TF TCExp) [x,y]
tDiv :: Type -> Type -> Type
tDiv x y = TCon (TF TCDiv) [x,y]
tMod :: Type -> Type -> Type
tMod x y = TCon (TF TCMod) [x,y]
tMin :: Type -> Type -> Type
tMin x y = TCon (TF TCMin) [x,y]
newtypeTyCon :: Newtype -> TCon
newtypeTyCon nt = TC $ TCNewtype $ UserTC (ntName nt) (kindOf nt)
newtypeConType :: Newtype -> Schema
newtypeConType nt =
Forall as (ntConstraints nt)
$ TRec (ntFields nt) `tFun` TCon (newtypeTyCon nt) (map (TVar . tpVar) as)
where
as = ntParams nt
ePrim :: PrimMap -> Ident -> Expr
ePrim pm n = EVar (lookupPrimDecl n pm)
eError :: PrimMap -> Type -> String -> Expr
eError prims t str =
EApp (ETApp (ETApp (ePrim prims (packIdent "error")) t)
(tNum (length str))) (eString prims str)
eString :: PrimMap -> String -> Expr
eString prims str = EList (map (eChar prims) str) tChar
eChar :: PrimMap -> Char -> Expr
eChar prims c = ETApp (ETApp (ePrim prims (packIdent "demote")) (tNum v)) (tNum w)
where v = fromEnum c
w = 8 :: Int
class HasKind t where
kindOf :: t -> Kind
instance HasKind TVar where
kindOf (TVFree _ k _ _) = k
kindOf (TVBound _ k) = k
instance HasKind TCon where
kindOf (TC tc) = kindOf tc
kindOf (PC pc) = kindOf pc
kindOf (TF tf) = kindOf tf
instance HasKind UserTC where
kindOf (UserTC _ k) = k
instance HasKind TC where
kindOf tcon =
case tcon of
TCNum _ -> KNum
TCInf -> KNum
TCBit -> KType
TCSeq -> KNum :-> KType :-> KType
TCFun -> KType :-> KType :-> KType
TCTuple n -> foldr (:->) KType (replicate n KType)
TCNewtype x -> kindOf x
instance HasKind PC where
kindOf pc =
case pc of
PEqual -> KNum :-> KNum :-> KProp
PNeq -> KNum :-> KNum :-> KProp
PGeq -> KNum :-> KNum :-> KProp
PFin -> KNum :-> KProp
PHas _ -> KType :-> KType :-> KProp
PArith -> KType :-> KProp
PCmp -> KType :-> KProp
instance HasKind TFun where
kindOf tfun =
case tfun of
TCWidth -> KNum :-> KNum
TCAdd -> KNum :-> KNum :-> KNum
TCSub -> KNum :-> KNum :-> KNum
TCMul -> KNum :-> KNum :-> KNum
TCDiv -> KNum :-> KNum :-> KNum
TCMod -> KNum :-> KNum :-> KNum
TCExp -> KNum :-> KNum :-> KNum
TCMin -> KNum :-> KNum :-> KNum
TCMax -> KNum :-> KNum :-> KNum
TCLenFromThen -> KNum :-> KNum :-> KNum :-> KNum
TCLenFromThenTo -> KNum :-> KNum :-> KNum :-> KNum
instance HasKind Type where
kindOf ty =
case ty of
TVar a -> kindOf a
TCon c ts -> quickApply (kindOf c) ts
TUser _ _ t -> kindOf t
TRec {} -> KType
instance HasKind TySyn where
kindOf (TySyn _ as _ t) = foldr (:->) (kindOf t) (map kindOf as)
instance HasKind Newtype where
kindOf nt = foldr (:->) KType (map kindOf (ntParams nt))
instance HasKind TParam where
kindOf p = tpKind p
quickApply :: Kind -> [a] -> Kind
quickApply k [] = k
quickApply (_ :-> k) (_ : ts) = quickApply k ts
quickApply k _ = panic "Cryptol.TypeCheck.AST.quickApply"
[ "Applying a non-function kind:", show k ]
instance PP Kind where
ppPrec p k = case k of
KType -> char '*'
KNum -> char '#'
KProp -> text "Prop"
l :-> r -> optParens (p >= 1) (sep [ppPrec 1 l, text "->", ppPrec 0 r])
instance PP (WithNames TVar) where
ppPrec _ (WithNames (TVBound x _) mp) =
case IntMap.lookup x mp of
Just a -> text a
Nothing -> text ("a`" ++ show x)
ppPrec _ (WithNames (TVFree x _ _ _) _) =
char '?' <> text (intToName x)
instance PP TVar where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP TParam where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP (WithNames TParam) where
ppPrec _ (WithNames p mp) = ppWithNames mp (tpVar p)
instance PP (WithNames Type) where
ppPrec prec ty0@(WithNames ty nmMap) =
case ty of
TVar a -> ppWithNames nmMap a
TRec fs -> braces $ fsep $ punctuate comma
[ pp l <+> text ":" <+> go 0 t | (l,t) <- fs ]
TUser c ts _ -> optParens (prec > 3) $ pp c <+> fsep (map (go 4) ts)
TCon (TC tc) ts ->
case (tc,ts) of
(TCNum n, []) -> integer n
(TCInf, []) -> text "inf"
(TCBit, []) -> text "Bit"
(TCSeq, [t1,TCon (TC TCBit) []]) -> brackets (go 0 t1)
(TCSeq, [t1,t2]) -> optParens (prec > 3)
$ brackets (go 0 t1) <> go 3 t2
(TCFun, [t1,t2]) -> optParens (prec > 1)
$ go 2 t1 <+> text "->" <+> go 1 t2
(TCTuple _, fs) -> parens $ fsep $ punctuate comma $ map (go 0) fs
(_, _) -> pp tc <+> fsep (map (go 4) ts)
TCon (PC pc) ts ->
case (pc,ts) of
(PEqual, [t1,t2]) -> go 0 t1 <+> text "==" <+> go 0 t2
(PNeq , [t1,t2]) -> go 0 t1 <+> text "/=" <+> go 0 t2
(PGeq, [t1,t2]) -> go 0 t1 <+> text ">=" <+> go 0 t2
(PFin, [t1]) -> text "fin" <+> (go 4 t1)
(PHas x, [t1,t2]) -> ppSelector x <+> text "of"
<+> go 0 t1 <+> text "is" <+> go 0 t2
(PArith, [t1]) -> pp pc <+> go 4 t1
(PCmp, [t1]) -> pp pc <+> go 4 t1
(_, _) -> pp pc <+> fsep (map (go 4) ts)
_ | Just tinf <- isTInfix ty0 -> optParens (prec > 2)
$ ppInfix 2 isTInfix tinf
TCon f ts -> optParens (prec > 3)
$ pp f <+> fsep (map (go 4) ts)
where
go p t = ppWithNamesPrec nmMap p t
isTInfix (WithNames (TCon (TF ieOp) [ieLeft',ieRight']) _) =
do let ieLeft = WithNames ieLeft' nmMap
ieRight = WithNames ieRight' nmMap
(ieAssoc,iePrec) <- Map.lookup ieOp tBinOpPrec
return Infix { .. }
isTInfix _ = Nothing
addTNames :: [TParam] -> NameMap -> NameMap
addTNames as ns = foldr (uncurry IntMap.insert) ns
$ named ++ zip unnamed avail
where avail = filter (`notElem` used) (nameList [])
named = [ (u,show (pp n))
| TParam { tpUnique = u, tpName = Just n } <- as ]
unnamed = [ u | TParam { tpUnique = u, tpName = Nothing } <- as ]
used = map snd named ++ IntMap.elems ns
ppNewtypeShort :: Newtype -> Doc
ppNewtypeShort nt =
text "newtype" <+> pp (ntName nt) <+> hsep (map (ppWithNamesPrec nm 9) ps)
where
ps = ntParams nt
nm = addTNames ps emptyNameMap
instance PP Schema where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP (WithNames Schema) where
ppPrec _ (WithNames s ns) = vars <+> props <+> ppWithNames ns1 (sType s)
where
vars = case sVars s of
[] -> empty
vs -> braces $ commaSep $ map (ppWithNames ns1) vs
props = case sProps s of
[] -> empty
ps -> parens (commaSep (map (ppWithNames ns1) ps)) <+> text "=>"
ns1 = addTNames (sVars s) ns
instance PP TySyn where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP (WithNames TySyn) where
ppPrec _ (WithNames (TySyn n ps _ ty) ns) =
text "type" <+> pp n <+> sep (map (ppWithNames ns1) ps) <+> char '='
<+> ppWithNames ns1 ty
where ns1 = addTNames ps ns
instance PP Type where
ppPrec n t = ppWithNamesPrec IntMap.empty n t
instance PP TCon where
ppPrec _ (TC tc) = pp tc
ppPrec _ (PC tc) = pp tc
ppPrec _ (TF tc) = pp tc
instance PP PC where
ppPrec _ x =
case x of
PEqual -> text "(==)"
PNeq -> text "(/=)"
PGeq -> text "(>=)"
PFin -> text "fin"
PHas sel -> parens (ppSelector sel)
PArith -> text "Arith"
PCmp -> text "Cmp"
instance PP TC where
ppPrec _ x =
case x of
TCNum n -> integer n
TCInf -> text "inf"
TCBit -> text "Bit"
TCSeq -> text "[]"
TCFun -> text "(->)"
TCTuple 0 -> text "()"
TCTuple 1 -> text "(one tuple?)"
TCTuple n -> parens $ hcat $ replicate (n1) comma
TCNewtype u -> pp u
instance PP UserTC where
ppPrec p (UserTC x _) = ppPrec p x
instance PP (WithNames Expr) where
ppPrec prec (WithNames expr nm) =
case expr of
EList [] t -> optParens (prec > 0)
$ text "[]" <+> colon <+> ppWP prec t
EList es _ -> brackets $ sep $ punctuate comma $ map ppW es
ETuple es -> parens $ sep $ punctuate comma $ map ppW es
ERec fs -> braces $ sep $ punctuate comma
[ pp f <+> text "=" <+> ppW e | (f,e) <- fs ]
ESel e sel -> ppWP 4 e <+> text "." <> pp sel
EIf e1 e2 e3 -> optParens (prec > 0)
$ sep [ text "if" <+> ppW e1
, text "then" <+> ppW e2
, text "else" <+> ppW e3 ]
EComp _ e mss -> let arm ms = text "|" <+> commaSep (map ppW ms)
in brackets $ ppW e <+> vcat (map arm mss)
EVar x -> ppPrefixName x
EAbs {} -> let (xs,e) = splitWhile splitAbs expr
in ppLam nm prec [] [] xs e
EProofAbs {} -> let (ps,e1) = splitWhile splitProofAbs expr
(xs,e2) = splitWhile splitAbs e1
in ppLam nm prec [] ps xs e2
ETAbs {} -> let (ts,e1) = splitWhile splitTAbs expr
(ps,e2) = splitWhile splitProofAbs e1
(xs,e3) = splitWhile splitAbs e2
in ppLam nm prec ts ps xs e3
EApp (EApp (EVar o) a) b
| isInfixIdent (nameIdent o) ->
ppPrec 3 a <+> ppInfixName o <+> ppPrec 3 b
| otherwise ->
ppPrefixName o <+> ppPrec 3 a <+> ppPrec 3 b
EApp e1 e2 -> optParens (prec > 3)
$ ppWP 3 e1 <+> ppWP 4 e2
EProofApp e -> optParens (prec > 3)
$ ppWP 3 e <+> text "<>"
ETApp e t -> optParens (prec > 3)
$ ppWP 3 e <+> ppWP 4 t
ECast e t -> optParens (prec > 0)
( ppWP 2 e <+> text ":" <+> ppW t )
EWhere e ds -> optParens (prec > 0)
( ppW e $$ text "where"
$$ nest 2 (vcat (map ppW ds))
$$ text "" )
where
ppW x = ppWithNames nm x
ppWP x = ppWithNamesPrec nm x
ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name,Type)] -> Expr -> Doc
ppLam nm prec [] [] [] e = ppWithNamesPrec nm prec e
ppLam nm prec ts ps xs e =
optParens (prec > 0) $
sep [ text "\\" <> tsD <+> psD <+> xsD <+> text "->"
, ppWithNames ns1 e
]
where
ns1 = addTNames ts nm
tsD = if null ts then empty else braces $ sep $ punctuate comma $ map ppT ts
psD = if null ps then empty else parens $ sep $ punctuate comma $ map ppP ps
xsD = if null xs then empty else sep $ map ppArg xs
ppT = ppWithNames ns1
ppP = ppWithNames ns1
ppArg (x,t) = parens (pp x <+> text ":" <+> ppWithNames ns1 t)
splitWhile :: (a -> Maybe (b,a)) -> a -> ([b],a)
splitWhile f e = case f e of
Nothing -> ([], e)
Just (x,e1) -> let (xs,e2) = splitWhile f e1
in (x:xs,e2)
splitAbs :: Expr -> Maybe ((Name,Type), Expr)
splitAbs (EAbs x t e) = Just ((x,t), e)
splitAbs _ = Nothing
splitTAbs :: Expr -> Maybe (TParam, Expr)
splitTAbs (ETAbs t e) = Just (t, e)
splitTAbs _ = Nothing
splitProofAbs :: Expr -> Maybe (Prop, Expr)
splitProofAbs (EProofAbs p e) = Just (p,e)
splitProofAbs _ = Nothing
instance PP Expr where
ppPrec n t = ppWithNamesPrec IntMap.empty n t
instance PP (WithNames Match) where
ppPrec _ (WithNames mat nm) =
case mat of
From x _ e -> pp x <+> text "<-" <+> ppWithNames nm e
Let d -> text "let" <+> ppWithNames nm d
instance PP Match where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP (WithNames DeclGroup) where
ppPrec _ (WithNames dg nm) =
case dg of
Recursive ds -> text "/* Recursive */"
$$ vcat (map (ppWithNames nm) ds)
$$ text ""
NonRecursive d -> text "/* Not recursive */"
$$ ppWithNames nm d
$$ text ""
instance PP DeclGroup where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP (WithNames Decl) where
ppPrec _ (WithNames Decl { .. } nm) =
pp dName <+> text ":" <+> ppWithNames nm dSignature $$
(if null dPragmas
then empty
else text "pragmas" <+> pp dName <+> sep (map pp dPragmas)
) $$
pp dName <+> text "=" <+> ppWithNames nm dDefinition
instance PP (WithNames DeclDef) where
ppPrec _ (WithNames DPrim _) = text "<primitive>"
ppPrec _ (WithNames (DExpr e) nm) = ppWithNames nm e
instance PP Decl where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP Module where
ppPrec = ppWithNamesPrec IntMap.empty
instance PP (WithNames Module) where
ppPrec _ (WithNames Module { .. } nm) =
text "module" <+> pp mName $$
vcat (map pp mImports) $$
vcat (map (ppWithNames nm) mDecls)