{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :  Disco.AST.Surface
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Abstract syntax trees representing the surface syntax of the Disco
-- language.
module Disco.AST.Surface (
  -- * Modules
  Module (..),
  emptyModule,
  TopLevel (..),

  -- ** Documentation
  Docs,
  DocThing (..),
  Property,

  -- ** Declarations
  TypeDecl (..),
  TermDefn (..),
  TypeDefn (..),
  Decl (..),
  partitionDecls,
  prettyTyDecl,

  -- * Terms
  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 (..),

  -- ** Telescopes
  Telescope (..),
  foldTelescope,
  mapTelescope,
  toTelescope,
  fromTelescope,

  -- ** Expressions
  Side (..),
  Link,
  pattern TLink,
  Binding,

  -- ** Lists
  Qual,
  pattern QBind,
  pattern QGuard,
  Container (..),
  Ellipsis (..),

  -- ** Case expressions and patterns
  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)

-- | The extension descriptor for Surface specific AST types.
data UD

-- | A module contains all the information from one disco source file.
data Module = Module
  { Module -> Set Ext
modExts :: Set Ext
  -- ^ Enabled extensions
  , Module -> [String]
modImports :: [String]
  -- ^ Module imports
  , Module -> [Decl]
modDecls :: [Decl]
  -- ^ Declarations
  , Module -> [(Name (Term_ UD), Docs)]
modDocs :: [(Name Term, Docs)]
  -- ^ Documentation
  , Module -> [Term_ UD]
modTerms :: [Term]
  -- ^ Top-level (bare) terms
  }

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 = []
    }

-- | A @TopLevel@ is either documentation (a 'DocThing') or a
--   declaration ('Decl').
data TopLevel = TLDoc DocThing | TLDecl Decl | TLExpr Term

deriving instance ForallTerm Show UD => Show TopLevel

-- | Convenient synonym for a list of 'DocThing's.
type Docs = [DocThing]

-- | An item of documentation.
data DocThing
  = -- | A documentation string, i.e. a block
    --   of @||| text@ items
    DocString [String]
  | -- | An example/doctest/property of the
    --   form @!!! forall (x1:ty1) ... . property@
    DocProperty Property

deriving instance ForallTerm Show UD => Show DocThing

-- | A property is a universally quantified term of the form
--   @forall v1 : T1, v2 : T2. term@.
type Property = Property_ UD

-- | A type declaration, @name : type@.
data TypeDecl = TypeDecl (Name Term) PolyType

-- | A group of definition clauses of the form @name pat1 .. patn = term@. The
--   patterns bind variables in the term. For example, @f n (x,y) =
--   n*x + y@.
data TermDefn = TermDefn (Name Term) [Bind [Pattern] Term]

-- | A user-defined type (potentially recursive).
--
--   @type T arg1 arg2 ... = body
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)

-- | A declaration is either a type declaration, a term definition, or
--   a type definition.
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 [] = ([], [], [])

------------------------------------------------------------
-- Pretty-printing top-level declarations

-- prettyModule :: Module -> Doc
-- prettyModule = foldr ($+$) empty . map pretty

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

-- | Pretty-print a single clause in a definition.
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)

-- | Pretty-print a type declaration.
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]

------------------------------------------------------------
-- Terms
------------------------------------------------------------
type Term = Term_ UD

-- In the surface language, abstractions bind variables using a
-- (nonempty) list of patterns. Each pattern might contain any
-- number of variables, and might have type annotations on some
-- of its components.
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 = () -- TWild

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

-- Since we parse patterns by first parsing a term and then ensuring
-- it is a valid pattern, we have to include wildcards in the syntax
-- of terms, although they will be rejected at a later phase.
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_ ()

-- (?) TAscr uses a PolyType, but without higher rank types
-- I think we can't possibly need that here.
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
  #-}

------------------------------------------------------------
-- Pretty-printing for surface-syntax terms
--
-- The instances in this section are used to pretty-print surface
-- syntax, for example, when printing the source code definition of a
-- term (e.g. via the :doc REPL command).

-- | Pretty-print a term with guaranteed parentheses.
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 t@TContainer{} = setPA initPA $ "" <+> prettyTerm 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
"∃"

    -- special case for fully applied unary operators
    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
    -- special case for fully applied binary operators
    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)
          ]
    -- Always pretty-print function applications with parentheses
    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
"_"

-- | Print appropriate delimiters for a container literal.
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

-- | Pretty-print a single branch in a case expression.
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

-- | Pretty-print the guards in a single branch of a case expression.
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

-- | Pretty-print a binding, i.e. a pairing of a name (with optional
--   type annotation) and term.
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]

-- | Pretty-print the qualifiers in a comprehension.
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

-- | Pretty-print a single qualifier in a comprehension.
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

-- | Pretty-print a pattern with guaranteed parentheses.
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

-- We could probably alternatively write a function to turn a pattern
-- back into a term, and pretty-print that instead of the below.
-- Unsure whether it would be worth it.

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)