{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Disco.AST.Surface
(
Module(..), 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 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 Data.Void
import Disco.Effects.LFresh
import Polysemy hiding (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, Docs)]
modDocs :: [(Name Term, Docs)]
, Module -> [Term]
modTerms :: [Term]
}
deriving instance ForallTerm Show UD => Show Module
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
(Int -> TypeDefn -> ShowS)
-> (TypeDefn -> String) -> ([TypeDefn] -> ShowS) -> Show TypeDefn
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) = (([TypeDecl] -> Identity [TypeDecl])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> Identity ([TypeDecl], [TermDefn], [TypeDefn])
forall s t a b. Field1 s t a b => Lens s t a b
_1 (([TypeDecl] -> Identity [TypeDecl])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> Identity ([TypeDecl], [TermDefn], [TypeDefn]))
-> ([TypeDecl] -> [TypeDecl])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (TypeDecl
tyDeclTypeDecl -> [TypeDecl] -> [TypeDecl]
forall a. a -> [a] -> [a]
:)) ([Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
partitionDecls [Decl]
ds)
partitionDecls (DDefn TermDefn
def : [Decl]
ds) = (([TermDefn] -> Identity [TermDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> Identity ([TypeDecl], [TermDefn], [TypeDefn])
forall s t a b. Field2 s t a b => Lens s t a b
_2 (([TermDefn] -> Identity [TermDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> Identity ([TypeDecl], [TermDefn], [TypeDefn]))
-> ([TermDefn] -> [TermDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (TermDefn
defTermDefn -> [TermDefn] -> [TermDefn]
forall a. a -> [a] -> [a]
:)) ([Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
partitionDecls [Decl]
ds)
partitionDecls (DTyDef TypeDefn
def : [Decl]
ds) = (([TypeDefn] -> Identity [TypeDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> Identity ([TypeDecl], [TermDefn], [TypeDefn])
forall s t a b. Field3 s t a b => Lens s t a b
_3 (([TypeDefn] -> Identity [TypeDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> Identity ([TypeDecl], [TermDefn], [TypeDefn]))
-> ([TypeDefn] -> [TypeDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (TypeDefn
defTypeDefn -> [TypeDefn] -> [TypeDefn]
forall a. a -> [a] -> [a]
:)) ([Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
partitionDecls [Decl]
ds)
partitionDecls [] = ([], [], [])
instance Pretty Decl where
pretty :: Decl -> Sem r Doc
pretty = \case
DType (TypeDecl Name Term
x PolyType
ty) -> Name Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Term
x Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> PolyType -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty PolyType
ty
DTyDef (TypeDefn String
x [String]
args Type
body) ->
String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"type" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
x Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep ((String -> Sem r Doc) -> [String] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text [String]
args) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"=" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
body
DDefn (TermDefn Name Term
x [Bind [Pattern] Term]
bs) -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat ([Sem r Doc] -> Sem r Doc) -> [Sem r Doc] -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ (Bind [Pattern] Term -> Sem r Doc)
-> [Bind [Pattern] Term] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Name Term, Bind [Pattern] Term) -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty ((Name Term, Bind [Pattern] Term) -> Sem r Doc)
-> (Bind [Pattern] Term -> (Name Term, Bind [Pattern] Term))
-> Bind [Pattern] Term
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name Term
x,)) [Bind [Pattern] Term]
bs
instance Pretty (Name a, Bind [Pattern] Term) where
pretty :: (Name a, Bind [Pattern] Term) -> Sem r Doc
pretty (Name a
x, Bind [Pattern] Term
b) = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc)
-> ((([Pattern], Term) -> Sem r Doc) -> Sem r Doc)
-> (([Pattern], Term) -> Sem r Doc)
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind [Pattern] Term
-> (([Pattern], Term) -> Sem r Doc) -> Sem r Doc
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] Term
b ((([Pattern], Term) -> Sem r Doc) -> Sem r Doc)
-> (([Pattern], Term) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \([Pattern]
ps, Term
t) ->
Name a -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name a
x Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hcat ((Pattern -> Sem r Doc) -> [Pattern] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> Sem r Doc
forall (r :: EffectRow).
Members '[LFresh, Reader PA] r =>
Pattern -> Sem r Doc
prettyPatternP [Pattern]
ps) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"=" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t)
prettyTyDecl :: Members '[Reader PA, LFresh] r => Name t -> Type -> Sem r Doc
prettyTyDecl :: Name t -> Type -> Sem r Doc
prettyTyDecl Name t
x Type
ty = [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Name t -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name t
x, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":", Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
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 -> Term
$mTVar :: forall r. Term -> (Name Term -> r) -> (Void# -> r) -> r
TVar name = TVar_ () name
pattern TPrim :: Prim -> Term
pattern $bTPrim :: Prim -> Term
$mTPrim :: forall r. Term -> (Prim -> r) -> (Void# -> r) -> r
TPrim name = TPrim_ () name
pattern TUn :: UOp -> Term -> Term
pattern $bTUn :: UOp -> Term -> Term
$mTUn :: forall r. Term -> (UOp -> Term -> r) -> (Void# -> r) -> r
TUn uop term = TApp_ () (TPrim_ () (PrimUOp uop)) term
pattern TBin :: BOp -> Term -> Term -> Term
pattern $bTBin :: BOp -> Term -> Term -> Term
$mTBin :: forall r. Term -> (BOp -> Term -> Term -> r) -> (Void# -> 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) Term -> Term
$mTLet :: forall r.
Term -> (Bind (Telescope Binding) Term -> r) -> (Void# -> r) -> r
TLet bind = TLet_ () bind
pattern TParens :: Term -> Term
pattern $bTParens :: Term -> Term
$mTParens :: forall r. Term -> (Term -> r) -> (Void# -> r) -> r
TParens term = TParens_ () term
pattern TUnit :: Term
pattern $bTUnit :: Term
$mTUnit :: forall r. Term -> (Void# -> r) -> (Void# -> r) -> r
TUnit = TUnit_ ()
pattern TBool :: Bool -> Term
pattern $bTBool :: Bool -> Term
$mTBool :: forall r. Term -> (Bool -> r) -> (Void# -> r) -> r
TBool bool = TBool_ () bool
pattern TNat :: Integer -> Term
pattern $bTNat :: Integer -> Term
$mTNat :: forall r. Term -> (Integer -> r) -> (Void# -> r) -> r
TNat int = TNat_ () int
pattern TRat :: Rational -> Term
pattern $bTRat :: Rational -> Term
$mTRat :: forall r. Term -> (Rational -> r) -> (Void# -> r) -> r
TRat rat = TRat_ () rat
pattern TChar :: Char -> Term
pattern $bTChar :: Char -> Term
$mTChar :: forall r. Term -> (Char -> r) -> (Void# -> r) -> r
TChar c = TChar_ () c
pattern TString :: String -> Term
pattern $bTString :: String -> Term
$mTString :: forall r. Term -> (String -> r) -> (Void# -> r) -> r
TString s = TString_ () s
pattern TAbs :: Quantifier -> Bind [Pattern] Term -> Term
pattern $bTAbs :: Quantifier -> Bind [Pattern] Term -> Term
$mTAbs :: forall r.
Term
-> (Quantifier -> Bind [Pattern] Term -> r) -> (Void# -> r) -> r
TAbs q bind = TAbs_ q () bind
pattern TApp :: Term -> Term -> Term
pattern $bTApp :: Term -> Term -> Term
$mTApp :: forall r. Term -> (Term -> Term -> r) -> (Void# -> r) -> r
TApp term1 term2 = TApp_ () term1 term2
pattern TTup :: [Term] -> Term
pattern $bTTup :: [Term] -> Term
$mTTup :: forall r. Term -> ([Term] -> r) -> (Void# -> r) -> r
TTup termlist = TTup_ () termlist
pattern TCase :: [Branch] -> Term
pattern $bTCase :: [Branch] -> Term
$mTCase :: forall r. Term -> ([Branch] -> r) -> (Void# -> r) -> r
TCase branch = TCase_ () branch
pattern TChain :: Term -> [Link] -> Term
pattern $bTChain :: Term -> [Link] -> Term
$mTChain :: forall r. Term -> (Term -> [Link] -> r) -> (Void# -> r) -> r
TChain term linklist = TChain_ () term linklist
pattern TTyOp :: TyOp -> Type -> Term
pattern $bTTyOp :: TyOp -> Type -> Term
$mTTyOp :: forall r. Term -> (TyOp -> Type -> r) -> (Void# -> r) -> r
TTyOp tyop ty = TTyOp_ () tyop ty
pattern TContainer :: Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term
pattern $bTContainer :: Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term
$mTContainer :: forall r.
Term
-> (Container
-> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> r)
-> (Void# -> r)
-> r
TContainer c tl mets = TContainer_ () c tl mets
pattern TContainerComp :: Container -> Bind (Telescope Qual) Term -> Term
pattern $bTContainerComp :: Container -> Bind (Telescope Qual) Term -> Term
$mTContainerComp :: forall r.
Term
-> (Container -> Bind (Telescope Qual) Term -> r)
-> (Void# -> r)
-> r
TContainerComp c b = TContainerComp_ () c b
pattern TAscr :: Term -> PolyType -> Term
pattern $bTAscr :: Term -> PolyType -> Term
$mTAscr :: forall r. Term -> (Term -> PolyType -> r) -> (Void# -> r) -> r
TAscr term ty = TAscr_ () term ty
pattern TWild :: Term
pattern $bTWild :: Term
$mTWild :: forall r. Term -> (Void# -> r) -> (Void# -> 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] -> Maybe (Ellipsis Term) -> Term
$mTList :: forall r.
Term -> ([Term] -> Maybe (Ellipsis Term) -> r) -> (Void# -> r) -> r
TList ts e <- TContainer_ () ListContainer (map fst -> ts) e
where
TList [Term]
ts Maybe (Ellipsis Term)
e = X_TContainer UD
-> Container
-> [(Term, Maybe Term)]
-> Maybe (Ellipsis Term)
-> Term
forall e.
X_TContainer e
-> Container
-> [(Term_ e, Maybe (Term_ e))]
-> Maybe (Ellipsis (Term_ e))
-> Term_ e
TContainer_ () Container
ListContainer ((Term -> (Term, Maybe Term)) -> [Term] -> [(Term, Maybe Term)]
forall a b. (a -> b) -> [a] -> [b]
map (,Maybe Term
forall a. Maybe a
Nothing) [Term]
ts) Maybe (Ellipsis Term)
e
pattern TListComp :: Bind (Telescope Qual) Term -> Term
pattern $bTListComp :: Bind (Telescope Qual) Term -> Term
$mTListComp :: forall r.
Term -> (Bind (Telescope Qual) Term -> r) -> (Void# -> 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 -> Link
$mTLink :: forall r. Link -> (BOp -> Term -> r) -> (Void# -> 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 -> Embed Term -> Qual
$mQBind :: forall r.
Qual -> (Name Term -> Embed Term -> r) -> (Void# -> r) -> r
QBind namet embedt = QBind_ () namet embedt
pattern QGuard :: Embed Term -> Qual
pattern $bQGuard :: Embed Term -> Qual
$mQGuard :: forall r. Qual -> (Embed Term -> r) -> (Void# -> 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 -> Embed Term -> Binding
$mBinding :: forall r.
Binding
-> (Maybe (Embed PolyType) -> Name Term -> Embed Term -> r)
-> (Void# -> 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 -> Guard
$mGBool :: forall r. Guard -> (Embed Term -> r) -> (Void# -> r) -> r
GBool embedt = GBool_ () embedt
pattern GPat :: Embed Term -> Pattern -> Guard
pattern $bGPat :: Embed Term -> Pattern -> Guard
$mGPat :: forall r.
Guard -> (Embed Term -> Pattern -> r) -> (Void# -> r) -> r
GPat embedt pat = GPat_ () embedt pat
pattern GLet :: Binding -> Guard
pattern $bGLet :: Binding -> Guard
$mGLet :: forall r. Guard -> (Binding -> r) -> (Void# -> 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 -> Pattern
$mPVar :: forall r. Pattern -> (Name Term -> r) -> (Void# -> r) -> r
PVar name = PVar_ () name
pattern PWild :: Pattern
pattern $bPWild :: Pattern
$mPWild :: forall r. Pattern -> (Void# -> r) -> (Void# -> r) -> r
PWild = PWild_ ()
pattern PAscr :: Pattern -> Type -> Pattern
pattern $bPAscr :: Pattern -> Type -> Pattern
$mPAscr :: forall r. Pattern -> (Pattern -> Type -> r) -> (Void# -> r) -> r
PAscr p ty = PAscr_ () p ty
pattern PUnit :: Pattern
pattern $bPUnit :: Pattern
$mPUnit :: forall r. Pattern -> (Void# -> r) -> (Void# -> r) -> r
PUnit = PUnit_ ()
pattern PBool :: Bool -> Pattern
pattern $bPBool :: Bool -> Pattern
$mPBool :: forall r. Pattern -> (Bool -> r) -> (Void# -> r) -> r
PBool b = PBool_ () b
pattern PChar :: Char -> Pattern
pattern $bPChar :: Char -> Pattern
$mPChar :: forall r. Pattern -> (Char -> r) -> (Void# -> r) -> r
PChar c = PChar_ () c
pattern PString :: String -> Pattern
pattern $bPString :: String -> Pattern
$mPString :: forall r. Pattern -> (String -> r) -> (Void# -> r) -> r
PString s = PString_ () s
pattern PTup :: [Pattern] -> Pattern
pattern $bPTup :: [Pattern] -> Pattern
$mPTup :: forall r. Pattern -> ([Pattern] -> r) -> (Void# -> r) -> r
PTup lp = PTup_ () lp
pattern PInj :: Side -> Pattern -> Pattern
pattern $bPInj :: Side -> Pattern -> Pattern
$mPInj :: forall r. Pattern -> (Side -> Pattern -> r) -> (Void# -> r) -> r
PInj s p = PInj_ () s p
pattern PNat :: Integer -> Pattern
pattern $bPNat :: Integer -> Pattern
$mPNat :: forall r. Pattern -> (Integer -> r) -> (Void# -> r) -> r
PNat n = PNat_ () n
pattern PCons :: Pattern -> Pattern -> Pattern
pattern $bPCons :: Pattern -> Pattern -> Pattern
$mPCons :: forall r. Pattern -> (Pattern -> Pattern -> r) -> (Void# -> r) -> r
PCons p1 p2 = PCons_ () p1 p2
pattern PList :: [Pattern] -> Pattern
pattern $bPList :: [Pattern] -> Pattern
$mPList :: forall r. Pattern -> ([Pattern] -> r) -> (Void# -> r) -> r
PList lp = PList_ () lp
pattern PAdd :: Side -> Pattern -> Term -> Pattern
pattern $bPAdd :: Side -> Pattern -> Term -> Pattern
$mPAdd :: forall r.
Pattern -> (Side -> Pattern -> Term -> r) -> (Void# -> r) -> r
PAdd s p t = PAdd_ () s p t
pattern PMul :: Side -> Pattern -> Term -> Pattern
pattern $bPMul :: Side -> Pattern -> Term -> Pattern
$mPMul :: forall r.
Pattern -> (Side -> Pattern -> Term -> r) -> (Void# -> r) -> r
PMul s p t = PMul_ () s p t
pattern PSub :: Pattern -> Term -> Pattern
pattern $bPSub :: Pattern -> Term -> Pattern
$mPSub :: forall r. Pattern -> (Pattern -> Term -> r) -> (Void# -> r) -> r
PSub p t = PSub_ () p t
pattern PNeg :: Pattern -> Pattern
pattern $bPNeg :: Pattern -> Pattern
$mPNeg :: forall r. Pattern -> (Pattern -> r) -> (Void# -> r) -> r
PNeg p = PNeg_ () p
pattern PFrac :: Pattern -> Pattern -> Pattern
pattern $bPFrac :: Pattern -> Pattern -> Pattern
$mPFrac :: forall r. Pattern -> (Pattern -> Pattern -> r) -> (Void# -> r) -> r
PFrac p1 p2 = PFrac_ () p1 p2
{-# 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
prettyTermP :: Term -> Sem r Doc
prettyTermP t :: Term
t@TTup{} = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t
prettyTermP Term
t = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t
instance Pretty Term where
pretty :: Term -> Sem r Doc
pretty = \case
TVar Name Term
x -> Name Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Term
x
TPrim (PrimUOp UOp
uop) ->
case UOp -> Map UOp OpInfo -> Maybe OpInfo
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
_) -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
syn Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"~"
Just (OpInfo (UOpF UFixity
Post UOp
_) (String
syn:[String]
_) Int
_) -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"~" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
syn
Maybe OpInfo
_ -> String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"pretty @Term: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ UOp -> String
forall a. Show a => a -> String
show UOp
uop String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not in the uopMap!"
TPrim (PrimBOp BOp
bop) -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"~" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> BOp -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty BOp
bop Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"~"
TPrim Prim
p ->
case Prim -> Map Prim PrimInfo -> Maybe PrimInfo
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) -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
nm
Just (PrimInfo Prim
_ String
nm Bool
False) -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"$" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
nm
Maybe PrimInfo
Nothing -> String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"pretty @Term: Prim " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Prim -> String
forall a. Show a => a -> String
show Prim
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not in the primMap!"
TParens Term
t -> Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t
Term
TUnit -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"■"
(TBool Bool
b) -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text ((Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Bool -> String
forall a. Show a => a -> String
show Bool
b)
TChar Char
c -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Char -> String
forall a. Show a => a -> String
show Char
c)
TString String
cs -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
doubleQuotes (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
cs
TAbs Quantifier
q Bind [Pattern] Term
bnd -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Bind [Pattern] Term
-> (([Pattern], Term) -> Sem r Doc) -> Sem r Doc
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] Term
bnd ((([Pattern], Term) -> Sem r Doc) -> Sem r Doc)
-> (([Pattern], Term) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \([Pattern]
args, Term
body) ->
Quantifier -> Sem r Doc
forall (m :: * -> *). Applicative m => Quantifier -> m Doc
prettyQ Quantifier
q
Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep ([Sem r Doc] -> Sem r Doc) -> Sem r [Sem r Doc] -> Sem r Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Pattern -> Sem r Doc) -> [Pattern] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Pattern]
args))
Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"."
Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
body)
where
prettyQ :: Quantifier -> m Doc
prettyQ Quantifier
Lam = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"λ"
prettyQ Quantifier
All = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"∀"
prettyQ Quantifier
Ex = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"∃"
TApp (TPrim (PrimUOp UOp
uop)) Term
t ->
case UOp -> Map UOp OpInfo -> Maybe OpInfo
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
_) -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (UOp -> PA
ugetPA UOp
uop) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> UOp -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty UOp
uop
Just (OpInfo (UOpF UFixity
Pre UOp
_) [String]
_ Int
_) -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (UOp -> PA
ugetPA UOp
uop) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
UOp -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty UOp
uop Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t)
Maybe OpInfo
_ -> String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"pretty @Term: uopMap doesn't contain " String -> ShowS
forall a. [a] -> [a] -> [a]
++ UOp -> String
forall a. Show a => a -> String
show UOp
uop
TApp (TPrim (PrimBOp BOp
bop)) (TTup [Term
t1, Term
t2]) -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
bop) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
[Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep
[ Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t1)
, BOp -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty BOp
bop
, Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t2)
]
TApp Term
t1 Term
t2 -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t1) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Term -> Sem r Doc
forall (r :: EffectRow).
Members '[LFresh, Reader PA] r =>
Term -> Sem r Doc
prettyTermP Term
t2
TTup [Term]
ts -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ do
[Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Term -> Sem r Doc) -> [Term] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Term]
ts)
Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds)
TContainer Container
c [(Term, Maybe Term)]
ts Maybe (Ellipsis Term)
e -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ do
[Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") (((Term, Maybe Term) -> Sem r Doc)
-> [(Term, Maybe Term)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term, Maybe Term) -> Sem r Doc
forall (r :: EffectRow) t t.
(Member (Reader PA) r, Member LFresh r, Pretty t, Pretty t) =>
(t, Maybe t) -> Sem r Doc
prettyCount [(Term, Maybe Term)]
ts)
let pe :: [Sem r Doc]
pe = case Maybe (Ellipsis Term)
e of
Maybe (Ellipsis Term)
Nothing -> []
Just (Until Term
t) -> [String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"..", Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t]
Container -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Container -> Sem r Doc -> Sem r Doc
containerDelims Container
c ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep ([Sem r Doc]
ds [Sem r Doc] -> [Sem r Doc] -> [Sem r Doc]
forall a. [a] -> [a] -> [a]
++ [Sem r Doc]
pe))
where
prettyCount :: (t, Maybe t) -> Sem r Doc
prettyCount (t
t, Maybe t
Nothing) = t -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty t
t
prettyCount (t
t, Just t
n) = Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (t -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty t
t) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"#" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (t -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty t
n)
TContainerComp Container
c Bind (Telescope Qual) Term
bqst ->
Bind (Telescope Qual) Term
-> ((Telescope Qual, Term) -> Sem r Doc) -> Sem r Doc
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) Term
bqst (((Telescope Qual, Term) -> Sem r Doc) -> Sem r Doc)
-> ((Telescope Qual, Term) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \(Telescope Qual
qs,Term
t) ->
PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Container -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Container -> Sem r Doc -> Sem r Doc
containerDelims Container
c ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"|", Telescope Qual -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Telescope Qual
qs])
TNat Integer
n -> Integer -> Sem r Doc
forall (m :: * -> *). Applicative m => Integer -> m Doc
integer Integer
n
TChain Term
t [Link]
lks -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Eq) (Sem r Doc -> Sem r Doc)
-> ([Sem r Doc] -> Sem r Doc) -> [Sem r Doc] -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep ([Sem r Doc] -> Sem r Doc) -> [Sem r Doc] -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t)
Sem r Doc -> [Sem r Doc] -> [Sem r Doc]
forall a. a -> [a] -> [a]
: (Link -> [Sem r Doc]) -> [Link] -> [Sem r Doc]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Link -> [Sem r Doc]
forall (r :: EffectRow).
(Member (Reader PA) r, Member LFresh r) =>
Link -> [Sem r Doc]
prettyLink [Link]
lks
where
prettyLink :: Link -> [Sem r Doc]
prettyLink (TLink BOp
op Term
t2) =
[ BOp -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty BOp
op
, PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA (BOp -> PA
getPA BOp
op) (Sem r Doc -> Sem r Doc)
-> (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t2
]
TLet Bind (Telescope Binding) Term
bnd -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Bind (Telescope Binding) Term
-> ((Telescope Binding, Term) -> Sem r Doc) -> Sem r Doc
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) Term
bnd (((Telescope Binding, Term) -> Sem r Doc) -> Sem r Doc)
-> ((Telescope Binding, Term) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \(Telescope Binding
bs, Term
t2) -> do
[Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Binding -> Sem r Doc) -> [Binding] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Binding -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (Telescope Binding -> [Binding]
forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope Binding
bs))
[Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep
[ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"let"
, [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds
, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"in"
, Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t2
]
TCase [Branch]
b -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
(String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"{?" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> [Branch] -> Sem r Doc
forall (r :: EffectRow).
Members '[Reader PA, LFresh] r =>
[Branch] -> Sem r Doc
prettyBranches [Branch]
b) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"?}"
TAscr Term
t PolyType
ty -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
ascrPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (PolyType -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty PolyType
ty)
TRat Rational
r -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Rational -> String
prettyDecimal Rational
r)
TTyOp TyOp
op Type
ty -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
TyOp -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty TyOp
op Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty
Term
TWild -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"_"
containerDelims :: Member (Reader PA) r => Container -> (Sem r Doc -> Sem r Doc)
containerDelims :: Container -> Sem r Doc -> Sem r Doc
containerDelims Container
ListContainer = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
brackets
containerDelims Container
BagContainer = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc
bag
containerDelims Container
SetContainer = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
braces
prettyBranches :: Members '[Reader PA, LFresh] r => [Branch] -> Sem r Doc
prettyBranches :: [Branch] -> Sem r Doc
prettyBranches = \case
[] -> String -> Sem r Doc
forall a. HasCallStack => String -> a
error String
"Empty branches are disallowed."
Branch
b:[Branch]
bs ->
Branch -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Branch
b
Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
(Branch -> Sem r Doc -> Sem r Doc)
-> Sem r Doc -> [Branch] -> Sem r Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
($+$) (Sem r Doc -> Sem r Doc -> Sem r Doc)
-> (Branch -> Sem r Doc) -> Branch -> Sem r Doc -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"," Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+>) (Sem r Doc -> Sem r Doc)
-> (Branch -> Sem r Doc) -> Branch -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Branch -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty) Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
empty [Branch]
bs
instance Pretty Branch where
pretty :: Branch -> Sem r Doc
pretty Branch
br = Branch -> ((Telescope Guard, Term) -> Sem r Doc) -> Sem r Doc
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 (((Telescope Guard, Term) -> Sem r Doc) -> Sem r Doc)
-> ((Telescope Guard, Term) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \(Telescope Guard
gs,Term
t) ->
Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Telescope Guard -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Telescope Guard
gs
instance Pretty (Telescope Guard) where
pretty :: Telescope Guard -> Sem r Doc
pretty = \case
Telescope Guard
TelEmpty -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"otherwise"
Telescope Guard
gs -> (Guard -> Sem r Doc -> Sem r Doc)
-> Sem r Doc -> [Guard] -> Sem r Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Guard
g Sem r Doc
r -> Guard -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Guard
g Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
r) (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"") (Telescope Guard -> [Guard]
forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope Guard
gs)
instance Pretty Guard where
pretty :: Guard -> Sem r Doc
pretty = \case
GBool Embed Term
et -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"if" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed Embed Term
et)
GPat Embed Term
et Pattern
p -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"when" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed Embed Term
et) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"is" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p
GLet Binding
b -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"let" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Binding -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Binding
b
instance Pretty Binding where
pretty :: Binding -> Sem r Doc
pretty = \case
Binding Maybe (Embed PolyType)
Nothing Name Term
x (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t) ->
[Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Name Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Term
x, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"=", Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Embedded (Embed Term)
Term
t]
Binding (Just (Embed PolyType -> Embedded (Embed PolyType)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed PolyType)
ty)) Name Term
x (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t) ->
[Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Name Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Term
x, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":", PolyType -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Embedded (Embed PolyType)
PolyType
ty, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"=", Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Embedded (Embed Term)
Term
t]
instance Pretty (Telescope Qual) where
pretty :: Telescope Qual -> Sem r Doc
pretty (Telescope Qual -> [Qual]
forall b. Alpha b => Telescope b -> [b]
fromTelescope -> [Qual]
qs) = do
[Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Qual -> Sem r Doc) -> [Qual] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Qual -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Qual]
qs)
[Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds
instance Pretty Qual where
pretty :: Qual -> Sem r Doc
pretty = \case
QBind Name Term
x (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t) -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Name Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Term
x, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"in", Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Embedded (Embed Term)
Term
t]
QGuard (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t) -> Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Embedded (Embed Term)
Term
t
prettyPatternP :: Members '[LFresh, Reader PA] r => Pattern -> Sem r Doc
prettyPatternP :: Pattern -> Sem r Doc
prettyPatternP p :: Pattern
p@PTup{} = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p
prettyPatternP Pattern
p = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p
instance Pretty Pattern where
pretty :: Pattern -> Sem r Doc
pretty = \case
PVar Name Term
x -> Name Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Term
x
Pattern
PWild -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"_"
PAscr Pattern
p Type
ty -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
ascrPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty)
Pattern
PUnit -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"■"
PBool Bool
b -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Bool -> String
forall a. Show a => a -> String
show Bool
b
PChar Char
c -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Char -> String
forall a. Show a => a -> String
show Char
c)
PString String
s -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (ShowS
forall a. Show a => a -> String
show String
s)
PTup [Pattern]
ts -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ do
[Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Pattern -> Sem r Doc) -> [Pattern] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Pattern]
ts)
Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds)
PInj Side
s Pattern
p -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Side -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Side
s Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Pattern -> Sem r Doc
forall (r :: EffectRow).
Members '[LFresh, Reader PA] r =>
Pattern -> Sem r Doc
prettyPatternP Pattern
p
PNat Integer
n -> Integer -> Sem r Doc
forall (m :: * -> *). Applicative m => Integer -> m Doc
integer Integer
n
PCons Pattern
p1 Pattern
p2 -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Cons) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p1) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"::" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p2)
PList [Pattern]
ps -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ do
[Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Pattern -> Sem r Doc) -> [Pattern] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Pattern]
ps)
Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
brackets ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds)
PAdd Side
L Pattern
p Term
t -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Add) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"+" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t)
PAdd Side
R Pattern
p Term
t -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Add) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"+" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p)
PMul Side
L Pattern
p Term
t -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Mul) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"*" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t)
PMul Side
R Pattern
p Term
t -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Mul) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"*" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p)
PSub Pattern
p Term
t -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Sub) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"-" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t)
PNeg Pattern
p -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (UOp -> PA
ugetPA UOp
Neg) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"-" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p)
PFrac Pattern
p1 Pattern
p2 -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Div) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p1) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"/" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p2)