{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Disco.AST.Surface (
Module (..),
emptyModule,
TopLevel (..),
Docs,
DocThing (..),
Property,
TypeDecl (..),
TermDefn (..),
TypeDefn (..),
Decl (..),
partitionDecls,
prettyTyDecl,
UD,
Term,
pattern TVar,
pattern TPrim,
pattern TUn,
pattern TBin,
pattern TLet,
pattern TParens,
pattern TUnit,
pattern TBool,
pattern TChar,
pattern TString,
pattern TNat,
pattern TRat,
pattern TAbs,
pattern TApp,
pattern TTup,
pattern TCase,
pattern TChain,
pattern TTyOp,
pattern TContainerComp,
pattern TContainer,
pattern TAscr,
pattern TWild,
pattern TList,
pattern TListComp,
Quantifier (..),
Telescope (..),
foldTelescope,
mapTelescope,
toTelescope,
fromTelescope,
Side (..),
Link,
pattern TLink,
Binding,
Qual,
pattern QBind,
pattern QGuard,
Container (..),
Ellipsis (..),
Branch,
Guard,
pattern GBool,
pattern GPat,
pattern GLet,
Pattern,
pattern PVar,
pattern PWild,
pattern PAscr,
pattern PUnit,
pattern PBool,
pattern PChar,
pattern PString,
pattern PTup,
pattern PInj,
pattern PNat,
pattern PCons,
pattern PList,
pattern PAdd,
pattern PMul,
pattern PSub,
pattern PNeg,
pattern PFrac,
pattern PNonlinear,
pattern Binding,
)
where
import Prelude hiding ((<>))
import Control.Lens ((%~), _1, _2, _3)
import Data.Char (toLower)
import qualified Data.Map as M
import Data.Set (Set)
import qualified Data.Set as S
import Data.Void
import Disco.Effects.LFresh
import Polysemy hiding (Embed, embed)
import Polysemy.Reader
import Disco.AST.Generic
import Disco.Extensions
import Disco.Pretty
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Types
import Unbound.Generics.LocallyNameless hiding (LFresh (..), lunbind)
data UD
data Module = Module
{ Module -> Set Ext
modExts :: Set Ext
, Module -> [String]
modImports :: [String]
, Module -> [Decl]
modDecls :: [Decl]
, Module -> [(Name (Term_ UD), Docs)]
modDocs :: [(Name Term, Docs)]
, Module -> [Term_ UD]
modTerms :: [Term]
}
deriving instance ForallTerm Show UD => Show Module
emptyModule :: Module
emptyModule :: Module
emptyModule =
Module
{ modExts :: Set Ext
modExts = forall a. Set a
S.empty
, modImports :: [String]
modImports = []
, modDecls :: [Decl]
modDecls = []
, modDocs :: [(Name (Term_ UD), Docs)]
modDocs = []
, modTerms :: [Term_ UD]
modTerms = []
}
data TopLevel = TLDoc DocThing | TLDecl Decl | TLExpr Term
deriving instance ForallTerm Show UD => Show TopLevel
type Docs = [DocThing]
data DocThing
=
DocString [String]
|
DocProperty Property
deriving instance ForallTerm Show UD => Show DocThing
type Property = Property_ UD
data TypeDecl = TypeDecl (Name Term) PolyType
data TermDefn = TermDefn (Name Term) [Bind [Pattern] Term]
data TypeDefn = TypeDefn String [String] Type
deriving (Int -> TypeDefn -> ShowS
[TypeDefn] -> ShowS
TypeDefn -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeDefn] -> ShowS
$cshowList :: [TypeDefn] -> ShowS
show :: TypeDefn -> String
$cshow :: TypeDefn -> String
showsPrec :: Int -> TypeDefn -> ShowS
$cshowsPrec :: Int -> TypeDefn -> ShowS
Show)
data Decl where
DType :: TypeDecl -> Decl
DDefn :: TermDefn -> Decl
DTyDef :: TypeDefn -> Decl
deriving instance ForallTerm Show UD => Show TypeDecl
deriving instance ForallTerm Show UD => Show TermDefn
deriving instance ForallTerm Show UD => Show Decl
partitionDecls :: [Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
partitionDecls :: [Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
partitionDecls (DType TypeDecl
tyDecl : [Decl]
ds) = (forall s t a b. Field1 s t a b => Lens s t a b
_1 forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (TypeDecl
tyDecl forall a. a -> [a] -> [a]
:)) ([Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
partitionDecls [Decl]
ds)
partitionDecls (DDefn TermDefn
def : [Decl]
ds) = (forall s t a b. Field2 s t a b => Lens s t a b
_2 forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (TermDefn
def forall a. a -> [a] -> [a]
:)) ([Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
partitionDecls [Decl]
ds)
partitionDecls (DTyDef TypeDefn
def : [Decl]
ds) = (forall s t a b. Field3 s t a b => Lens s t a b
_3 forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (TypeDefn
def forall a. a -> [a] -> [a]
:)) ([Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
partitionDecls [Decl]
ds)
partitionDecls [] = ([], [], [])
instance Pretty Decl where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Decl -> Sem r (Doc ann)
pretty = \case
DType (TypeDecl Name (Term_ UD)
x PolyType
ty) -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name (Term_ UD)
x forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
":" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty PolyType
ty
DTyDef (TypeDefn String
x [String]
args Type
body) ->
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"type" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
x forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text [String]
args) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"=" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
body
DDefn (TermDefn Name (Term_ UD)
x [Bind [Pattern_ UD] (Term_ UD)]
bs) -> forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name (Term_ UD)
x,)) [Bind [Pattern_ UD] (Term_ UD)]
bs
instance Pretty (Name a, Bind [Pattern] Term) where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
(Name a, Bind [Pattern_ UD] (Term_ UD)) -> Sem r (Doc ann)
pretty (Name a
x, Bind [Pattern_ UD] (Term_ UD)
b) = forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind [Pattern_ UD] (Term_ UD)
b forall a b. (a -> b) -> a -> b
$ \([Pattern_ UD]
ps, Term_ UD
t) ->
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name a
x forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hcat (forall a b. (a -> b) -> [a] -> [b]
map forall (r :: EffectRow) ann.
Members '[LFresh, Reader PA] r =>
Pattern_ UD -> Sem r (Doc ann)
prettyPatternP [Pattern_ UD]
ps) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"=" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t)
prettyTyDecl :: Members '[Reader PA, LFresh] r => Name t -> Type -> Sem r (Doc ann)
prettyTyDecl :: forall (r :: EffectRow) t ann.
Members '[Reader PA, LFresh] r =>
Name t -> Type -> Sem r (Doc ann)
prettyTyDecl Name t
x Type
ty = forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name t
x, forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
":", forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty]
type Term = Term_ UD
type instance X_Binder UD = [Pattern]
type instance X_TVar UD = ()
type instance X_TPrim UD = ()
type instance X_TLet UD = ()
type instance X_TParens UD = ()
type instance X_TUnit UD = ()
type instance X_TBool UD = ()
type instance X_TNat UD = ()
type instance X_TRat UD = ()
type instance X_TChar UD = ()
type instance X_TString UD = ()
type instance X_TAbs UD = ()
type instance X_TApp UD = ()
type instance X_TTup UD = ()
type instance X_TCase UD = ()
type instance X_TChain UD = ()
type instance X_TTyOp UD = ()
type instance X_TContainer UD = ()
type instance X_TContainerComp UD = ()
type instance X_TAscr UD = ()
type instance X_Term UD = ()
pattern TVar :: Name Term -> Term
pattern $bTVar :: Name (Term_ UD) -> Term_ UD
$mTVar :: forall {r}. Term_ UD -> (Name (Term_ UD) -> r) -> ((# #) -> r) -> r
TVar name = TVar_ () name
pattern TPrim :: Prim -> Term
pattern $bTPrim :: Prim -> Term_ UD
$mTPrim :: forall {r}. Term_ UD -> (Prim -> r) -> ((# #) -> r) -> r
TPrim name = TPrim_ () name
pattern TUn :: UOp -> Term -> Term
pattern $bTUn :: UOp -> Term_ UD -> Term_ UD
$mTUn :: forall {r}. Term_ UD -> (UOp -> Term_ UD -> r) -> ((# #) -> r) -> r
TUn uop term = TApp_ () (TPrim_ () (PrimUOp uop)) term
pattern TBin :: BOp -> Term -> Term -> Term
pattern $bTBin :: BOp -> Term_ UD -> Term_ UD -> Term_ UD
$mTBin :: forall {r}.
Term_ UD -> (BOp -> Term_ UD -> Term_ UD -> r) -> ((# #) -> r) -> r
TBin bop term1 term2 = TApp_ () (TPrim_ () (PrimBOp bop)) (TTup_ () [term1, term2])
pattern TLet :: Bind (Telescope Binding) Term -> Term
pattern $bTLet :: Bind (Telescope (Binding_ UD)) (Term_ UD) -> Term_ UD
$mTLet :: forall {r}.
Term_ UD
-> (Bind (Telescope (Binding_ UD)) (Term_ UD) -> r)
-> ((# #) -> r)
-> r
TLet bind = TLet_ () bind
pattern TParens :: Term -> Term
pattern $bTParens :: Term_ UD -> Term_ UD
$mTParens :: forall {r}. Term_ UD -> (Term_ UD -> r) -> ((# #) -> r) -> r
TParens term = TParens_ () term
pattern TUnit :: Term
pattern $bTUnit :: Term_ UD
$mTUnit :: forall {r}. Term_ UD -> ((# #) -> r) -> ((# #) -> r) -> r
TUnit = TUnit_ ()
pattern TBool :: Bool -> Term
pattern $bTBool :: Bool -> Term_ UD
$mTBool :: forall {r}. Term_ UD -> (Bool -> r) -> ((# #) -> r) -> r
TBool bool = TBool_ () bool
pattern TNat :: Integer -> Term
pattern $bTNat :: Integer -> Term_ UD
$mTNat :: forall {r}. Term_ UD -> (Integer -> r) -> ((# #) -> r) -> r
TNat int = TNat_ () int
pattern TRat :: Rational -> Term
pattern $bTRat :: Rational -> Term_ UD
$mTRat :: forall {r}. Term_ UD -> (Rational -> r) -> ((# #) -> r) -> r
TRat rat = TRat_ () rat
pattern TChar :: Char -> Term
pattern $bTChar :: Char -> Term_ UD
$mTChar :: forall {r}. Term_ UD -> (Char -> r) -> ((# #) -> r) -> r
TChar c = TChar_ () c
pattern TString :: String -> Term
pattern $bTString :: String -> Term_ UD
$mTString :: forall {r}. Term_ UD -> (String -> r) -> ((# #) -> r) -> r
TString s = TString_ () s
pattern TAbs :: Quantifier -> Bind [Pattern] Term -> Term
pattern $bTAbs :: Quantifier -> Bind [Pattern_ UD] (Term_ UD) -> Term_ UD
$mTAbs :: forall {r}.
Term_ UD
-> (Quantifier -> Bind [Pattern_ UD] (Term_ UD) -> r)
-> ((# #) -> r)
-> r
TAbs q bind = TAbs_ q () bind
pattern TApp :: Term -> Term -> Term
pattern $bTApp :: Term_ UD -> Term_ UD -> Term_ UD
$mTApp :: forall {r}.
Term_ UD -> (Term_ UD -> Term_ UD -> r) -> ((# #) -> r) -> r
TApp term1 term2 = TApp_ () term1 term2
pattern TTup :: [Term] -> Term
pattern $bTTup :: [Term_ UD] -> Term_ UD
$mTTup :: forall {r}. Term_ UD -> ([Term_ UD] -> r) -> ((# #) -> r) -> r
TTup termlist = TTup_ () termlist
pattern TCase :: [Branch] -> Term
pattern $bTCase :: [Branch] -> Term_ UD
$mTCase :: forall {r}. Term_ UD -> ([Branch] -> r) -> ((# #) -> r) -> r
TCase branch = TCase_ () branch
pattern TChain :: Term -> [Link] -> Term
pattern $bTChain :: Term_ UD -> [Link_ UD] -> Term_ UD
$mTChain :: forall {r}.
Term_ UD -> (Term_ UD -> [Link_ UD] -> r) -> ((# #) -> r) -> r
TChain term linklist = TChain_ () term linklist
pattern TTyOp :: TyOp -> Type -> Term
pattern $bTTyOp :: TyOp -> Type -> Term_ UD
$mTTyOp :: forall {r}. Term_ UD -> (TyOp -> Type -> r) -> ((# #) -> r) -> r
TTyOp tyop ty = TTyOp_ () tyop ty
pattern TContainer :: Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term
pattern $bTContainer :: Container
-> [(Term_ UD, Maybe (Term_ UD))]
-> Maybe (Ellipsis (Term_ UD))
-> Term_ UD
$mTContainer :: forall {r}.
Term_ UD
-> (Container
-> [(Term_ UD, Maybe (Term_ UD))]
-> Maybe (Ellipsis (Term_ UD))
-> r)
-> ((# #) -> r)
-> r
TContainer c tl mets = TContainer_ () c tl mets
pattern TContainerComp :: Container -> Bind (Telescope Qual) Term -> Term
pattern $bTContainerComp :: Container -> Bind (Telescope (Qual_ UD)) (Term_ UD) -> Term_ UD
$mTContainerComp :: forall {r}.
Term_ UD
-> (Container -> Bind (Telescope (Qual_ UD)) (Term_ UD) -> r)
-> ((# #) -> r)
-> r
TContainerComp c b = TContainerComp_ () c b
pattern TAscr :: Term -> PolyType -> Term
pattern $bTAscr :: Term_ UD -> PolyType -> Term_ UD
$mTAscr :: forall {r}.
Term_ UD -> (Term_ UD -> PolyType -> r) -> ((# #) -> r) -> r
TAscr term ty = TAscr_ () term ty
pattern TWild :: Term
pattern $bTWild :: Term_ UD
$mTWild :: forall {r}. Term_ UD -> ((# #) -> r) -> ((# #) -> r) -> r
TWild = XTerm_ ()
{-# COMPLETE
TVar
, TPrim
, TLet
, TParens
, TUnit
, TBool
, TNat
, TRat
, TChar
, TString
, TAbs
, TApp
, TTup
, TCase
, TChain
, TTyOp
, TContainer
, TContainerComp
, TAscr
, TWild
#-}
pattern TList :: [Term] -> Maybe (Ellipsis Term) -> Term
pattern $bTList :: [Term_ UD] -> Maybe (Ellipsis (Term_ UD)) -> Term_ UD
$mTList :: forall {r}.
Term_ UD
-> ([Term_ UD] -> Maybe (Ellipsis (Term_ UD)) -> r)
-> ((# #) -> r)
-> r
TList ts e <- TContainer_ () ListContainer (map fst -> ts) e
where
TList [Term_ UD]
ts Maybe (Ellipsis (Term_ UD))
e = forall e.
X_TContainer e
-> Container
-> [(Term_ e, Maybe (Term_ e))]
-> Maybe (Ellipsis (Term_ e))
-> Term_ e
TContainer_ () Container
ListContainer (forall a b. (a -> b) -> [a] -> [b]
map (,forall a. Maybe a
Nothing) [Term_ UD]
ts) Maybe (Ellipsis (Term_ UD))
e
pattern TListComp :: Bind (Telescope Qual) Term -> Term
pattern $bTListComp :: Bind (Telescope (Qual_ UD)) (Term_ UD) -> Term_ UD
$mTListComp :: forall {r}.
Term_ UD
-> (Bind (Telescope (Qual_ UD)) (Term_ UD) -> r)
-> ((# #) -> r)
-> r
TListComp x = TContainerComp_ () ListContainer x
type Link = Link_ UD
type instance X_TLink UD = ()
pattern TLink :: BOp -> Term -> Link
pattern $bTLink :: BOp -> Term_ UD -> Link_ UD
$mTLink :: forall {r}. Link_ UD -> (BOp -> Term_ UD -> r) -> ((# #) -> r) -> r
TLink bop term = TLink_ () bop term
{-# COMPLETE TLink #-}
type Qual = Qual_ UD
type instance X_QBind UD = ()
type instance X_QGuard UD = ()
pattern QBind :: Name Term -> Embed Term -> Qual
pattern $bQBind :: Name (Term_ UD) -> Embed (Term_ UD) -> Qual_ UD
$mQBind :: forall {r}.
Qual_ UD
-> (Name (Term_ UD) -> Embed (Term_ UD) -> r) -> ((# #) -> r) -> r
QBind namet embedt = QBind_ () namet embedt
pattern QGuard :: Embed Term -> Qual
pattern $bQGuard :: Embed (Term_ UD) -> Qual_ UD
$mQGuard :: forall {r}.
Qual_ UD -> (Embed (Term_ UD) -> r) -> ((# #) -> r) -> r
QGuard embedt = QGuard_ () embedt
{-# COMPLETE QBind, QGuard #-}
type Binding = Binding_ UD
pattern Binding :: Maybe (Embed PolyType) -> Name Term -> Embed Term -> Binding
pattern $bBinding :: Maybe (Embed PolyType)
-> Name (Term_ UD) -> Embed (Term_ UD) -> Binding_ UD
$mBinding :: forall {r}.
Binding_ UD
-> (Maybe (Embed PolyType)
-> Name (Term_ UD) -> Embed (Term_ UD) -> r)
-> ((# #) -> r)
-> r
Binding m b n = Binding_ m b n
{-# COMPLETE Binding #-}
type Branch = Branch_ UD
type Guard = Guard_ UD
type instance X_GBool UD = ()
type instance X_GPat UD = ()
type instance X_GLet UD = ()
pattern GBool :: Embed Term -> Guard
pattern $bGBool :: Embed (Term_ UD) -> Guard_ UD
$mGBool :: forall {r}.
Guard_ UD -> (Embed (Term_ UD) -> r) -> ((# #) -> r) -> r
GBool embedt = GBool_ () embedt
pattern GPat :: Embed Term -> Pattern -> Guard
pattern $bGPat :: Embed (Term_ UD) -> Pattern_ UD -> Guard_ UD
$mGPat :: forall {r}.
Guard_ UD
-> (Embed (Term_ UD) -> Pattern_ UD -> r) -> ((# #) -> r) -> r
GPat embedt pat = GPat_ () embedt pat
pattern GLet :: Binding -> Guard
pattern $bGLet :: Binding_ UD -> Guard_ UD
$mGLet :: forall {r}. Guard_ UD -> (Binding_ UD -> r) -> ((# #) -> r) -> r
GLet b = GLet_ () b
{-# COMPLETE GBool, GPat, GLet #-}
type Pattern = Pattern_ UD
type instance X_PVar UD = ()
type instance X_PWild UD = ()
type instance X_PAscr UD = ()
type instance X_PUnit UD = ()
type instance X_PBool UD = ()
type instance X_PTup UD = ()
type instance X_PInj UD = ()
type instance X_PNat UD = ()
type instance X_PChar UD = ()
type instance X_PString UD = ()
type instance X_PCons UD = ()
type instance X_PList UD = ()
type instance X_PAdd UD = ()
type instance X_PMul UD = ()
type instance X_PSub UD = ()
type instance X_PNeg UD = ()
type instance X_PFrac UD = ()
type instance X_Pattern UD = Void
pattern PVar :: Name Term -> Pattern
pattern $bPVar :: Name (Term_ UD) -> Pattern_ UD
$mPVar :: forall {r}.
Pattern_ UD -> (Name (Term_ UD) -> r) -> ((# #) -> r) -> r
PVar name = PVar_ () name
pattern PWild :: Pattern
pattern $bPWild :: Pattern_ UD
$mPWild :: forall {r}. Pattern_ UD -> ((# #) -> r) -> ((# #) -> r) -> r
PWild = PWild_ ()
pattern PAscr :: Pattern -> Type -> Pattern
pattern $bPAscr :: Pattern_ UD -> Type -> Pattern_ UD
$mPAscr :: forall {r}.
Pattern_ UD -> (Pattern_ UD -> Type -> r) -> ((# #) -> r) -> r
PAscr p ty = PAscr_ () p ty
pattern PUnit :: Pattern
pattern $bPUnit :: Pattern_ UD
$mPUnit :: forall {r}. Pattern_ UD -> ((# #) -> r) -> ((# #) -> r) -> r
PUnit = PUnit_ ()
pattern PBool :: Bool -> Pattern
pattern $bPBool :: Bool -> Pattern_ UD
$mPBool :: forall {r}. Pattern_ UD -> (Bool -> r) -> ((# #) -> r) -> r
PBool b = PBool_ () b
pattern PChar :: Char -> Pattern
pattern $bPChar :: Char -> Pattern_ UD
$mPChar :: forall {r}. Pattern_ UD -> (Char -> r) -> ((# #) -> r) -> r
PChar c = PChar_ () c
pattern PString :: String -> Pattern
pattern $bPString :: String -> Pattern_ UD
$mPString :: forall {r}. Pattern_ UD -> (String -> r) -> ((# #) -> r) -> r
PString s = PString_ () s
pattern PTup :: [Pattern] -> Pattern
pattern $bPTup :: [Pattern_ UD] -> Pattern_ UD
$mPTup :: forall {r}.
Pattern_ UD -> ([Pattern_ UD] -> r) -> ((# #) -> r) -> r
PTup lp = PTup_ () lp
pattern PInj :: Side -> Pattern -> Pattern
pattern $bPInj :: Side -> Pattern_ UD -> Pattern_ UD
$mPInj :: forall {r}.
Pattern_ UD -> (Side -> Pattern_ UD -> r) -> ((# #) -> r) -> r
PInj s p = PInj_ () s p
pattern PNat :: Integer -> Pattern
pattern $bPNat :: Integer -> Pattern_ UD
$mPNat :: forall {r}. Pattern_ UD -> (Integer -> r) -> ((# #) -> r) -> r
PNat n = PNat_ () n
pattern PCons :: Pattern -> Pattern -> Pattern
pattern $bPCons :: Pattern_ UD -> Pattern_ UD -> Pattern_ UD
$mPCons :: forall {r}.
Pattern_ UD
-> (Pattern_ UD -> Pattern_ UD -> r) -> ((# #) -> r) -> r
PCons p1 p2 = PCons_ () p1 p2
pattern PList :: [Pattern] -> Pattern
pattern $bPList :: [Pattern_ UD] -> Pattern_ UD
$mPList :: forall {r}.
Pattern_ UD -> ([Pattern_ UD] -> r) -> ((# #) -> r) -> r
PList lp = PList_ () lp
pattern PAdd :: Side -> Pattern -> Term -> Pattern
pattern $bPAdd :: Side -> Pattern_ UD -> Term_ UD -> Pattern_ UD
$mPAdd :: forall {r}.
Pattern_ UD
-> (Side -> Pattern_ UD -> Term_ UD -> r) -> ((# #) -> r) -> r
PAdd s p t = PAdd_ () s p t
pattern PMul :: Side -> Pattern -> Term -> Pattern
pattern $bPMul :: Side -> Pattern_ UD -> Term_ UD -> Pattern_ UD
$mPMul :: forall {r}.
Pattern_ UD
-> (Side -> Pattern_ UD -> Term_ UD -> r) -> ((# #) -> r) -> r
PMul s p t = PMul_ () s p t
pattern PSub :: Pattern -> Term -> Pattern
pattern $bPSub :: Pattern_ UD -> Term_ UD -> Pattern_ UD
$mPSub :: forall {r}.
Pattern_ UD -> (Pattern_ UD -> Term_ UD -> r) -> ((# #) -> r) -> r
PSub p t = PSub_ () p t
pattern PNeg :: Pattern -> Pattern
pattern $bPNeg :: Pattern_ UD -> Pattern_ UD
$mPNeg :: forall {r}. Pattern_ UD -> (Pattern_ UD -> r) -> ((# #) -> r) -> r
PNeg p = PNeg_ () p
pattern PFrac :: Pattern -> Pattern -> Pattern
pattern $bPFrac :: Pattern_ UD -> Pattern_ UD -> Pattern_ UD
$mPFrac :: forall {r}.
Pattern_ UD
-> (Pattern_ UD -> Pattern_ UD -> r) -> ((# #) -> r) -> r
PFrac p1 p2 = PFrac_ () p1 p2
pattern PNonlinear :: Pattern -> Name Term -> Pattern
pattern $bPNonlinear :: Pattern_ UD -> Name (Term_ UD) -> Pattern_ UD
$mPNonlinear :: forall {r}.
Pattern_ UD
-> (Pattern_ UD -> Name (Term_ UD) -> r) -> ((# #) -> r) -> r
PNonlinear p x <- PNonlinear_ (unembed -> p) x
where
PNonlinear Pattern_ UD
p Name (Term_ UD)
x = forall e. Embed (Pattern_ e) -> Name (Term_ e) -> Pattern_ e
PNonlinear_ (forall e. IsEmbed e => Embedded e -> e
embed Pattern_ UD
p) Name (Term_ UD)
x
{-# COMPLETE
PVar
, PWild
, PAscr
, PUnit
, PBool
, PTup
, PInj
, PNat
, PChar
, PString
, PCons
, PList
, PAdd
, PMul
, PSub
, PNeg
, PFrac
#-}
prettyTermP :: Members '[LFresh, Reader PA] r => Term -> Sem r (Doc ann)
prettyTermP :: forall (r :: EffectRow) ann.
Members '[LFresh, Reader PA] r =>
Term_ UD -> Sem r (Doc ann)
prettyTermP t :: Term_ UD
t@TTup {} = forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA forall a b. (a -> b) -> a -> b
$ forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t
prettyTermP Term_ UD
t = forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA forall a b. (a -> b) -> a -> b
$ forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t
instance Pretty Term where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term_ UD -> Sem r (Doc ann)
pretty = \case
TVar Name (Term_ UD)
x -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name (Term_ UD)
x
TPrim (PrimUOp UOp
uop) ->
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup UOp
uop Map UOp OpInfo
uopMap of
Just (OpInfo (UOpF UFixity
Pre UOp
_) (String
syn : [String]
_) Int
_) -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
syn forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"~"
Just (OpInfo (UOpF UFixity
Post UOp
_) (String
syn : [String]
_) Int
_) -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"~" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
syn
Maybe OpInfo
_ -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"pretty @Term: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UOp
uop forall a. [a] -> [a] -> [a]
++ String
" is not in the uopMap!"
TPrim (PrimBOp BOp
bop) -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"~" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty BOp
bop forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"~"
TPrim Prim
p ->
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Prim
p Map Prim PrimInfo
primMap of
Just (PrimInfo Prim
_ String
nm Bool
True) -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
nm
Just (PrimInfo Prim
_ String
nm Bool
False) -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"$" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
nm
Maybe PrimInfo
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"pretty @Term: Prim " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Prim
p forall a. [a] -> [a] -> [a]
++ String
" is not in the primMap!"
TParens Term_ UD
t -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t
Term_ UD
TUnit -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"■"
(TBool Bool
b) -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Bool
b)
TChar Char
c -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (forall a. Show a => a -> String
show Char
c)
TString String
cs -> forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
doubleQuotes forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
cs
TAbs Quantifier
q Bind [Pattern_ UD] (Term_ UD)
bnd -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind [Pattern_ UD] (Term_ UD)
bnd forall a b. (a -> b) -> a -> b
$ \([Pattern_ UD]
args, Term_ UD
body) ->
forall {m :: * -> *} {ann}.
Applicative m =>
Quantifier -> m (Doc ann)
prettyQ Quantifier
q
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> (forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Pattern_ UD]
args))
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"."
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
body)
where
prettyQ :: Quantifier -> m (Doc ann)
prettyQ Quantifier
Lam = forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"λ"
prettyQ Quantifier
All = forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"∀"
prettyQ Quantifier
Ex = forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"∃"
TApp (TPrim (PrimUOp UOp
uop)) Term_ UD
t ->
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup UOp
uop Map UOp OpInfo
uopMap of
Just (OpInfo (UOpF UFixity
Post UOp
_) [String]
_ Int
_) ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (UOp -> PA
ugetPA UOp
uop) forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty UOp
uop
Just (OpInfo (UOpF UFixity
Pre UOp
_) [String]
_ Int
_) ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (UOp -> PA
ugetPA UOp
uop) forall a b. (a -> b) -> a -> b
$
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty UOp
uop forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t)
Maybe OpInfo
_ -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"pretty @Term: uopMap doesn't contain " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UOp
uop
TApp (TPrim (PrimBOp BOp
bop)) (TTup [Term_ UD
t1, Term_ UD
t2]) ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
bop) forall a b. (a -> b) -> a -> b
$
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep
[ forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t1)
, forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty BOp
bop
, forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t2)
]
TApp Term_ UD
t1 Term_ UD
t2 ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t1) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (r :: EffectRow) ann.
Members '[LFresh, Reader PA] r =>
Term_ UD -> Sem r (Doc ann)
prettyTermP Term_ UD
t2
TTup [Term_ UD]
ts -> forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA forall a b. (a -> b) -> a -> b
$ do
[Sem r (Doc ann)]
ds <- forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Term_ UD]
ts)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
ds)
TContainer Container
c [(Term_ UD, Maybe (Term_ UD))]
ts Maybe (Ellipsis (Term_ UD))
e -> forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA forall a b. (a -> b) -> a -> b
$ do
[Sem r (Doc ann)]
ds <- forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") (forall a b. (a -> b) -> [a] -> [b]
map forall {r :: EffectRow} {t} {t} {ann}.
(Member (Reader PA) r, Member LFresh r, Pretty t, Pretty t) =>
(t, Maybe t) -> Sem r (Doc ann)
prettyCount [(Term_ UD, Maybe (Term_ UD))]
ts)
let pe :: [Sem r (Doc ann)]
pe = case Maybe (Ellipsis (Term_ UD))
e of
Maybe (Ellipsis (Term_ UD))
Nothing -> []
Just (Until Term_ UD
t) -> [forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"..", forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t]
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Container -> Sem r (Doc ann) -> Sem r (Doc ann)
containerDelims Container
c (forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep ([Sem r (Doc ann)]
ds forall a. [a] -> [a] -> [a]
++ [Sem r (Doc ann)]
pe))
where
prettyCount :: (t, Maybe t) -> Sem r (Doc ann)
prettyCount (t
t, Maybe t
Nothing) = forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty t
t
prettyCount (t
t, Just t
n) = forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty t
t) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"#" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty t
n)
TContainerComp Container
c Bind (Telescope (Qual_ UD)) (Term_ UD)
bqst ->
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind (Telescope (Qual_ UD)) (Term_ UD)
bqst forall a b. (a -> b) -> a -> b
$ \(Telescope (Qual_ UD)
qs, Term_ UD
t) ->
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Container -> Sem r (Doc ann) -> Sem r (Doc ann)
containerDelims Container
c (forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t, forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"|", forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Telescope (Qual_ UD)
qs])
TNat Integer
n -> forall (m :: * -> *) ann. Applicative m => Integer -> m (Doc ann)
integer Integer
n
TChain Term_ UD
t [Link_ UD]
lks ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Eq) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t)
forall a. a -> [a] -> [a]
: forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {r :: EffectRow} {ann}.
(Member (Reader PA) r, Member LFresh r) =>
Link_ UD -> [Sem r (Doc ann)]
prettyLink [Link_ UD]
lks
where
prettyLink :: Link_ UD -> [Sem r (Doc ann)]
prettyLink (TLink BOp
op Term_ UD
t2) =
[ forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty BOp
op
, forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA (BOp -> PA
getPA BOp
op) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt forall a b. (a -> b) -> a -> b
$ forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t2
]
TLet Bind (Telescope (Binding_ UD)) (Term_ UD)
bnd -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind (Telescope (Binding_ UD)) (Term_ UD)
bnd forall a b. (a -> b) -> a -> b
$ \(Telescope (Binding_ UD)
bs, Term_ UD
t2) -> do
[Sem r (Doc ann)]
ds <- forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty (forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope (Binding_ UD)
bs))
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep
[ forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"let"
, forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
ds
, forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"in"
, forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t2
]
TCase [Branch]
b ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA forall a b. (a -> b) -> a -> b
$
(forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"{?" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
[Branch] -> Sem r (Doc ann)
prettyBranches [Branch]
b) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"?}"
TAscr Term_ UD
t PolyType
ty ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
ascrPA forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
":" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty PolyType
ty)
TRat Rational
r -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Rational -> String
prettyDecimal Rational
r)
TTyOp TyOp
op Type
ty ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA forall a b. (a -> b) -> a -> b
$
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty TyOp
op forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty
Term_ UD
TWild -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"_"
containerDelims :: Member (Reader PA) r => Container -> (Sem r (Doc ann) -> Sem r (Doc ann))
containerDelims :: forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Container -> Sem r (Doc ann) -> Sem r (Doc ann)
containerDelims Container
ListContainer = forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
brackets
containerDelims Container
BagContainer = forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann)
bag
containerDelims Container
SetContainer = forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
braces
prettyBranches :: Members '[Reader PA, LFresh] r => [Branch] -> Sem r (Doc ann)
prettyBranches :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
[Branch] -> Sem r (Doc ann)
prettyBranches = \case
[] -> forall a. HasCallStack => String -> a
error String
"Empty branches are disallowed."
Branch
b : [Branch]
bs ->
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Branch
b
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
($+$) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"," forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty) forall (m :: * -> *) ann. Applicative m => m (Doc ann)
empty [Branch]
bs
instance Pretty Branch where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Branch -> Sem r (Doc ann)
pretty Branch
br = forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Branch
br forall a b. (a -> b) -> a -> b
$ \(Telescope (Guard_ UD)
gs, Term_ UD
t) ->
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Telescope (Guard_ UD)
gs
instance Pretty (Telescope Guard) where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Telescope (Guard_ UD) -> Sem r (Doc ann)
pretty = \case
Telescope (Guard_ UD)
TelEmpty -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"otherwise"
Telescope (Guard_ UD)
gs -> forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Guard_ UD
g Sem r (Doc ann)
r -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Guard_ UD
g forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
r) (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"") (forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope (Guard_ UD)
gs)
instance Pretty Guard where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Guard_ UD -> Sem r (Doc ann)
pretty = \case
GBool Embed (Term_ UD)
et -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"if" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty (forall e. IsEmbed e => e -> Embedded e
unembed Embed (Term_ UD)
et)
GPat Embed (Term_ UD)
et Pattern_ UD
p -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"when" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty (forall e. IsEmbed e => e -> Embedded e
unembed Embed (Term_ UD)
et) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"is" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p
GLet Binding_ UD
b -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"let" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Binding_ UD
b
instance Pretty Binding where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Binding_ UD -> Sem r (Doc ann)
pretty = \case
Binding Maybe (Embed PolyType)
Nothing Name (Term_ UD)
x (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed (Term_ UD))
t) ->
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name (Term_ UD)
x, forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"=", forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Embedded (Embed (Term_ UD))
t]
Binding (Just (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed PolyType)
ty)) Name (Term_ UD)
x (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed (Term_ UD))
t) ->
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name (Term_ UD)
x, forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
":", forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Embedded (Embed PolyType)
ty, forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"=", forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Embedded (Embed (Term_ UD))
t]
instance Pretty (Telescope Qual) where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Telescope (Qual_ UD) -> Sem r (Doc ann)
pretty (forall b. Alpha b => Telescope b -> [b]
fromTelescope -> [Qual_ UD]
qs) = do
[Sem r (Doc ann)]
ds <- forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Qual_ UD]
qs)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
ds
instance Pretty Qual where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Qual_ UD -> Sem r (Doc ann)
pretty = \case
QBind Name (Term_ UD)
x (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed (Term_ UD))
t) -> forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name (Term_ UD)
x, forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"in", forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Embedded (Embed (Term_ UD))
t]
QGuard (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed (Term_ UD))
t) -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Embedded (Embed (Term_ UD))
t
prettyPatternP :: Members '[LFresh, Reader PA] r => Pattern -> Sem r (Doc ann)
prettyPatternP :: forall (r :: EffectRow) ann.
Members '[LFresh, Reader PA] r =>
Pattern_ UD -> Sem r (Doc ann)
prettyPatternP p :: Pattern_ UD
p@PTup {} = forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA forall a b. (a -> b) -> a -> b
$ forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p
prettyPatternP Pattern_ UD
p = forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA forall a b. (a -> b) -> a -> b
$ forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p
instance Pretty Pattern where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
pretty = \case
PVar Name (Term_ UD)
x -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name (Term_ UD)
x
Pattern_ UD
PWild -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"_"
PAscr Pattern_ UD
p Type
ty ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
ascrPA forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
":" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty)
Pattern_ UD
PUnit -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"■"
PBool Bool
b -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Bool
b
PChar Char
c -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (forall a. Show a => a -> String
show Char
c)
PString String
s -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (forall a. Show a => a -> String
show String
s)
PTup [Pattern_ UD]
ts -> forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA forall a b. (a -> b) -> a -> b
$ do
[Sem r (Doc ann)]
ds <- forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Pattern_ UD]
ts)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
ds)
PInj Side
s Pattern_ UD
p ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA forall a b. (a -> b) -> a -> b
$
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Side
s forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (r :: EffectRow) ann.
Members '[LFresh, Reader PA] r =>
Pattern_ UD -> Sem r (Doc ann)
prettyPatternP Pattern_ UD
p
PNat Integer
n -> forall (m :: * -> *) ann. Applicative m => Integer -> m (Doc ann)
integer Integer
n
PCons Pattern_ UD
p1 Pattern_ UD
p2 ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Cons) forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p1) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"::" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p2)
PList [Pattern_ UD]
ps -> forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA forall a b. (a -> b) -> a -> b
$ do
[Sem r (Doc ann)]
ds <- forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Pattern_ UD]
ps)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
brackets (forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
ds)
PAdd Side
L Pattern_ UD
p Term_ UD
t ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Add) forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"+" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t)
PAdd Side
R Pattern_ UD
p Term_ UD
t ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Add) forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"+" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p)
PMul Side
L Pattern_ UD
p Term_ UD
t ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Mul) forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"*" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t)
PMul Side
R Pattern_ UD
p Term_ UD
t ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Mul) forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"*" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p)
PSub Pattern_ UD
p Term_ UD
t ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Sub) forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"-" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term_ UD
t)
PNeg Pattern_ UD
p ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (UOp -> PA
ugetPA UOp
Neg) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"-" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p)
PFrac Pattern_ UD
p1 Pattern_ UD
p2 ->
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Div) forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p1) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"/" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p2)