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

-- |
-- Module      :  Disco.AST.Surface
-- Copyright   :  disco team and contributors
-- Maintainer  :  [email protected]
--
-- 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,

  -- ** Pretty printing
  prettyPatternP,
)
where

import Control.Lens ((%~), _1, _2, _3)
import Data.Char (toLower)
import Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NE
import qualified Data.Map as M
import Data.Set (Set)
import qualified Data.Set as S
import Data.Void
import Disco.AST.Generic
import Disco.Effects.LFresh
import Disco.Extensions
import Disco.Pretty
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Types
import Polysemy hiding (Embed, embed)
import Polysemy.Reader
import Unbound.Generics.LocallyNameless hiding (LFresh (..), lunbind)
import Prelude hiding ((<>))

-- | 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, Docs)]
modDocs :: [(Name Term, Docs)]
  -- ^ Documentation
  , Module -> [Term]
modTerms :: [Term]
  -- ^ Top-level (bare) terms
  }

deriving instance ForallTerm Show UD => Show Module

emptyModule :: Module
emptyModule :: Module
emptyModule =
  Module
    { modExts :: Set Ext
modExts = Set Ext
forall a. Set a
S.empty
    , modImports :: [String]
modImports = []
    , modDecls :: [Decl]
modDecls = []
    , modDocs :: [(Name Term, Docs)]
modDocs = []
    , modTerms :: [Term]
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) (NonEmpty (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
(Int -> TypeDefn -> ShowS)
-> (TypeDefn -> String) -> ([TypeDefn] -> ShowS) -> Show TypeDefn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TypeDefn -> ShowS
showsPrec :: Int -> TypeDefn -> ShowS
$cshow :: TypeDefn -> String
show :: TypeDefn -> String
$cshowList :: [TypeDefn] -> ShowS
showList :: [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) = (([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
Lens
  ([TypeDecl], [TermDefn], [TypeDefn])
  ([TypeDecl], [TermDefn], [TypeDefn])
  [TypeDecl]
  [TypeDecl]
_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
tyDecl TypeDecl -> [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
Lens
  ([TypeDecl], [TermDefn], [TypeDefn])
  ([TypeDecl], [TermDefn], [TypeDefn])
  [TermDefn]
  [TermDefn]
_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
def TermDefn -> [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
Lens
  ([TypeDecl], [TermDefn], [TypeDefn])
  ([TypeDecl], [TermDefn], [TypeDefn])
  [TypeDefn]
  [TypeDefn]
_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
def TypeDefn -> [TypeDefn] -> [TypeDefn]
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
x PolyType
ty) -> Name Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Term
x Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
":" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> PolyType -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
PolyType -> Sem r (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) ->
      String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"type" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
x Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep ((String -> Sem r (Doc ann)) -> [String] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text [String]
args) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"=" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (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
x NonEmpty (Bind [Pattern_ UD] Term)
bs) -> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat ([Sem r (Doc ann)] -> Sem r (Doc ann))
-> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ (Bind [Pattern_ UD] Term -> Sem r (Doc ann))
-> [Bind [Pattern_ UD] Term] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name Term, Bind [Pattern_ UD] Term) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
(Name Term, Bind [Pattern_ UD] Term) -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty ((Name Term, Bind [Pattern_ UD] Term) -> Sem r (Doc ann))
-> (Bind [Pattern_ UD] Term
    -> (Name Term, Bind [Pattern_ UD] Term))
-> Bind [Pattern_ UD] Term
-> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name Term
x,)) (NonEmpty (Bind [Pattern_ UD] Term) -> [Bind [Pattern_ UD] Term]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Bind [Pattern_ UD] Term)
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) -> Sem r (Doc ann)
pretty (Name a
x, Bind [Pattern_ UD] Term
b) = PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> ((([Pattern_ UD], Term) -> Sem r (Doc ann)) -> Sem r (Doc ann))
-> (([Pattern_ UD], Term) -> Sem r (Doc ann))
-> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind [Pattern_ UD] Term
-> (([Pattern_ UD], Term) -> Sem r (Doc ann)) -> Sem r (Doc ann)
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
b ((([Pattern_ UD], Term) -> Sem r (Doc ann)) -> Sem r (Doc ann))
-> (([Pattern_ UD], Term) -> Sem r (Doc ann)) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ \([Pattern_ UD]
ps, Term
t) ->
    Name a -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name a -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name a
x Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hcat ((Pattern_ UD -> Sem r (Doc ann))
-> [Pattern_ UD] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[LFresh, Reader PA] r =>
Pattern_ UD -> Sem r (Doc ann)
prettyPatternP [Pattern_ UD]
ps) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"=" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
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 = [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Name t -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name t -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name t
x, String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
":", Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
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 $mTVar :: forall {r}. Term -> (Name Term -> r) -> ((# #) -> r) -> r
$bTVar :: Name Term -> Term
TVar name = TVar_ () name

pattern TPrim :: Prim -> Term
pattern $mTPrim :: forall {r}. Term -> (Prim -> r) -> ((# #) -> r) -> r
$bTPrim :: Prim -> Term
TPrim name = TPrim_ () name

pattern TUn :: UOp -> Term -> Term
pattern $mTUn :: forall {r}. Term -> (UOp -> Term -> r) -> ((# #) -> r) -> r
$bTUn :: UOp -> Term -> Term
TUn uop term = TApp_ () (TPrim_ () (PrimUOp uop)) term

pattern TBin :: BOp -> Term -> Term -> Term
pattern $mTBin :: forall {r}. Term -> (BOp -> Term -> Term -> r) -> ((# #) -> r) -> r
$bTBin :: BOp -> Term -> Term -> Term
TBin bop term1 term2 = TApp_ () (TPrim_ () (PrimBOp bop)) (TTup_ () [term1, term2])

pattern TLet :: Bind (Telescope Binding) Term -> Term
pattern $mTLet :: forall {r}.
Term
-> (Bind (Telescope (Binding_ UD)) Term -> r) -> ((# #) -> r) -> r
$bTLet :: Bind (Telescope (Binding_ UD)) Term -> Term
TLet bind = TLet_ () bind

pattern TParens :: Term -> Term
pattern $mTParens :: forall {r}. Term -> (Term -> r) -> ((# #) -> r) -> r
$bTParens :: Term -> Term
TParens term = TParens_ () term

pattern TUnit :: Term
pattern $mTUnit :: forall {r}. Term -> ((# #) -> r) -> ((# #) -> r) -> r
$bTUnit :: Term
TUnit = TUnit_ ()

pattern TBool :: Bool -> Term
pattern $mTBool :: forall {r}. Term -> (Bool -> r) -> ((# #) -> r) -> r
$bTBool :: Bool -> Term
TBool bool = TBool_ () bool

pattern TNat :: Integer -> Term
pattern $mTNat :: forall {r}. Term -> (Integer -> r) -> ((# #) -> r) -> r
$bTNat :: Integer -> Term
TNat int = TNat_ () int

pattern TRat :: Rational -> Term
pattern $mTRat :: forall {r}. Term -> (Rational -> r) -> ((# #) -> r) -> r
$bTRat :: Rational -> Term
TRat rat = TRat_ () rat

pattern TChar :: Char -> Term
pattern $mTChar :: forall {r}. Term -> (Char -> r) -> ((# #) -> r) -> r
$bTChar :: Char -> Term
TChar c = TChar_ () c

pattern TString :: String -> Term
pattern $mTString :: forall {r}. Term -> (String -> r) -> ((# #) -> r) -> r
$bTString :: String -> Term
TString s = TString_ () s

pattern TAbs :: Quantifier -> Bind [Pattern] Term -> Term
pattern $mTAbs :: forall {r}.
Term
-> (Quantifier -> Bind [Pattern_ UD] Term -> r)
-> ((# #) -> r)
-> r
$bTAbs :: Quantifier -> Bind [Pattern_ UD] Term -> Term
TAbs q bind = TAbs_ q () bind

pattern TApp :: Term -> Term -> Term
pattern $mTApp :: forall {r}. Term -> (Term -> Term -> r) -> ((# #) -> r) -> r
$bTApp :: Term -> Term -> Term
TApp term1 term2 = TApp_ () term1 term2

pattern TTup :: [Term] -> Term
pattern $mTTup :: forall {r}. Term -> ([Term] -> r) -> ((# #) -> r) -> r
$bTTup :: [Term] -> Term
TTup termlist = TTup_ () termlist

pattern TCase :: [Branch] -> Term
pattern $mTCase :: forall {r}. Term -> ([Branch] -> r) -> ((# #) -> r) -> r
$bTCase :: [Branch] -> Term
TCase branch = TCase_ () branch

pattern TChain :: Term -> [Link] -> Term
pattern $mTChain :: forall {r}. Term -> (Term -> [Link_ UD] -> r) -> ((# #) -> r) -> r
$bTChain :: Term -> [Link_ UD] -> Term
TChain term linklist = TChain_ () term linklist

pattern TTyOp :: TyOp -> Type -> Term
pattern $mTTyOp :: forall {r}. Term -> (TyOp -> Type -> r) -> ((# #) -> r) -> r
$bTTyOp :: TyOp -> Type -> Term
TTyOp tyop ty = TTyOp_ () tyop ty

pattern TContainer :: Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term
pattern $mTContainer :: forall {r}.
Term
-> (Container
    -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> r)
-> ((# #) -> r)
-> r
$bTContainer :: Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term
TContainer c tl mets = TContainer_ () c tl mets

pattern TContainerComp :: Container -> Bind (Telescope Qual) Term -> Term
pattern $mTContainerComp :: forall {r}.
Term
-> (Container -> Bind (Telescope (Qual_ UD)) Term -> r)
-> ((# #) -> r)
-> r
$bTContainerComp :: Container -> Bind (Telescope (Qual_ UD)) Term -> Term
TContainerComp c b = TContainerComp_ () c b

pattern TAscr :: Term -> PolyType -> Term
pattern $mTAscr :: forall {r}. Term -> (Term -> PolyType -> r) -> ((# #) -> r) -> r
$bTAscr :: Term -> PolyType -> Term
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 $mTWild :: forall {r}. Term -> ((# #) -> r) -> ((# #) -> r) -> r
$bTWild :: Term
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 $mTList :: forall {r}.
Term -> ([Term] -> Maybe (Ellipsis Term) -> r) -> ((# #) -> r) -> r
$bTList :: [Term] -> Maybe (Ellipsis Term) -> Term
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 $mTListComp :: forall {r}.
Term
-> (Bind (Telescope (Qual_ UD)) Term -> r) -> ((# #) -> r) -> r
$bTListComp :: Bind (Telescope (Qual_ UD)) Term -> Term
TListComp x = TContainerComp_ () ListContainer x

type Link = Link_ UD

type instance X_TLink UD = ()

pattern TLink :: BOp -> Term -> Link
pattern $mTLink :: forall {r}. Link_ UD -> (BOp -> Term -> r) -> ((# #) -> r) -> r
$bTLink :: BOp -> Term -> Link_ UD
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 $mQBind :: forall {r}.
Qual_ UD -> (Name Term -> Embed Term -> r) -> ((# #) -> r) -> r
$bQBind :: Name Term -> Embed Term -> Qual_ UD
QBind namet embedt = QBind_ () namet embedt

pattern QGuard :: Embed Term -> Qual
pattern $mQGuard :: forall {r}. Qual_ UD -> (Embed Term -> r) -> ((# #) -> r) -> r
$bQGuard :: Embed Term -> Qual_ UD
QGuard embedt = QGuard_ () embedt

{-# COMPLETE QBind, QGuard #-}

type Binding = Binding_ UD

pattern Binding :: Maybe (Embed PolyType) -> Name Term -> Embed Term -> Binding
pattern $mBinding :: forall {r}.
Binding_ UD
-> (Maybe (Embed PolyType) -> Name Term -> Embed Term -> r)
-> ((# #) -> r)
-> r
$bBinding :: Maybe (Embed PolyType) -> Name Term -> Embed Term -> Binding_ UD
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 $mGBool :: forall {r}. Guard_ UD -> (Embed Term -> r) -> ((# #) -> r) -> r
$bGBool :: Embed Term -> Guard_ UD
GBool embedt = GBool_ () embedt

pattern GPat :: Embed Term -> Pattern -> Guard
pattern $mGPat :: forall {r}.
Guard_ UD -> (Embed Term -> Pattern_ UD -> r) -> ((# #) -> r) -> r
$bGPat :: Embed Term -> Pattern_ UD -> Guard_ UD
GPat embedt pat = GPat_ () embedt pat

pattern GLet :: Binding -> Guard
pattern $mGLet :: forall {r}. Guard_ UD -> (Binding_ UD -> r) -> ((# #) -> r) -> r
$bGLet :: Binding_ UD -> Guard_ UD
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 $mPVar :: forall {r}. Pattern_ UD -> (Name Term -> r) -> ((# #) -> r) -> r
$bPVar :: Name Term -> Pattern_ UD
PVar name = PVar_ () name

pattern PWild :: Pattern
pattern $mPWild :: forall {r}. Pattern_ UD -> ((# #) -> r) -> ((# #) -> r) -> r
$bPWild :: Pattern_ UD
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 $mPAscr :: forall {r}.
Pattern_ UD -> (Pattern_ UD -> Type -> r) -> ((# #) -> r) -> r
$bPAscr :: Pattern_ UD -> Type -> Pattern_ UD
PAscr p ty = PAscr_ () p ty

pattern PUnit :: Pattern
pattern $mPUnit :: forall {r}. Pattern_ UD -> ((# #) -> r) -> ((# #) -> r) -> r
$bPUnit :: Pattern_ UD
PUnit = PUnit_ ()

pattern PBool :: Bool -> Pattern
pattern $mPBool :: forall {r}. Pattern_ UD -> (Bool -> r) -> ((# #) -> r) -> r
$bPBool :: Bool -> Pattern_ UD
PBool b = PBool_ () b

pattern PChar :: Char -> Pattern
pattern $mPChar :: forall {r}. Pattern_ UD -> (Char -> r) -> ((# #) -> r) -> r
$bPChar :: Char -> Pattern_ UD
PChar c = PChar_ () c

pattern PString :: String -> Pattern
pattern $mPString :: forall {r}. Pattern_ UD -> (String -> r) -> ((# #) -> r) -> r
$bPString :: String -> Pattern_ UD
PString s = PString_ () s

pattern PTup :: [Pattern] -> Pattern
pattern $mPTup :: forall {r}.
Pattern_ UD -> ([Pattern_ UD] -> r) -> ((# #) -> r) -> r
$bPTup :: [Pattern_ UD] -> Pattern_ UD
PTup lp = PTup_ () lp

pattern PInj :: Side -> Pattern -> Pattern
pattern $mPInj :: forall {r}.
Pattern_ UD -> (Side -> Pattern_ UD -> r) -> ((# #) -> r) -> r
$bPInj :: Side -> Pattern_ UD -> Pattern_ UD
PInj s p = PInj_ () s p

pattern PNat :: Integer -> Pattern
pattern $mPNat :: forall {r}. Pattern_ UD -> (Integer -> r) -> ((# #) -> r) -> r
$bPNat :: Integer -> Pattern_ UD
PNat n = PNat_ () n

pattern PCons :: Pattern -> Pattern -> Pattern
pattern $mPCons :: forall {r}.
Pattern_ UD
-> (Pattern_ UD -> Pattern_ UD -> r) -> ((# #) -> r) -> r
$bPCons :: Pattern_ UD -> Pattern_ UD -> Pattern_ UD
PCons p1 p2 = PCons_ () p1 p2

pattern PList :: [Pattern] -> Pattern
pattern $mPList :: forall {r}.
Pattern_ UD -> ([Pattern_ UD] -> r) -> ((# #) -> r) -> r
$bPList :: [Pattern_ UD] -> Pattern_ UD
PList lp = PList_ () lp

pattern PAdd :: Side -> Pattern -> Term -> Pattern
pattern $mPAdd :: forall {r}.
Pattern_ UD
-> (Side -> Pattern_ UD -> Term -> r) -> ((# #) -> r) -> r
$bPAdd :: Side -> Pattern_ UD -> Term -> Pattern_ UD
PAdd s p t = PAdd_ () s p t

pattern PMul :: Side -> Pattern -> Term -> Pattern
pattern $mPMul :: forall {r}.
Pattern_ UD
-> (Side -> Pattern_ UD -> Term -> r) -> ((# #) -> r) -> r
$bPMul :: Side -> Pattern_ UD -> Term -> Pattern_ UD
PMul s p t = PMul_ () s p t

pattern PSub :: Pattern -> Term -> Pattern
pattern $mPSub :: forall {r}.
Pattern_ UD -> (Pattern_ UD -> Term -> r) -> ((# #) -> r) -> r
$bPSub :: Pattern_ UD -> Term -> Pattern_ UD
PSub p t = PSub_ () p t

pattern PNeg :: Pattern -> Pattern
pattern $mPNeg :: forall {r}. Pattern_ UD -> (Pattern_ UD -> r) -> ((# #) -> r) -> r
$bPNeg :: Pattern_ UD -> Pattern_ UD
PNeg p = PNeg_ () p

pattern PFrac :: Pattern -> Pattern -> Pattern
pattern $mPFrac :: forall {r}.
Pattern_ UD
-> (Pattern_ UD -> Pattern_ UD -> r) -> ((# #) -> r) -> r
$bPFrac :: Pattern_ UD -> Pattern_ UD -> Pattern_ UD
PFrac p1 p2 = PFrac_ () p1 p2

pattern PNonlinear :: Pattern -> Name Term -> Pattern
pattern $mPNonlinear :: forall {r}.
Pattern_ UD -> (Pattern_ UD -> Name Term -> r) -> ((# #) -> r) -> r
$bPNonlinear :: Pattern_ UD -> Name Term -> Pattern_ UD
PNonlinear p x <- PNonlinear_ (unembed -> p) x
  where
    PNonlinear Pattern_ UD
p Name Term
x = Embed (Pattern_ UD) -> Name Term -> Pattern_ UD
forall e. Embed (Pattern_ e) -> Name (Term_ e) -> Pattern_ e
PNonlinear_ (Embedded (Embed (Pattern_ UD)) -> Embed (Pattern_ UD)
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed (Pattern_ UD))
Pattern_ UD
p) Name Term
x

{-# COMPLETE
  PVar
  , PWild
  , PAscr
  , PUnit
  , PBool
  , PTup
  , PInj
  , PNat
  , PChar
  , PString
  , PCons
  , PList
  , PAdd
  , PMul
  , PSub
  , PNeg
  , PFrac
  , PNonlinear
  #-}

------------------------------------------------------------
-- 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 -> Sem r (Doc ann)
prettyTermP t :: Term
t@TTup {} = PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t
-- prettyTermP t@TContainer{} = setPA initPA $ "" <+> prettyTerm t
prettyTermP Term
t = PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t

instance Pretty Term where
  pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
pretty = \case
    TVar Name Term
x -> Name Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
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 ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
syn Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"~"
        Just (OpInfo (UOpF UFixity
Post UOp
_) (String
syn : [String]
_) Int
_) -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"~" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
syn
        Maybe OpInfo
_ -> String -> Sem r (Doc ann)
forall a. HasCallStack => String -> a
error (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
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 ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"~" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> BOp -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
BOp -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty BOp
bop Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
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 ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
nm
        Just (PrimInfo Prim
_ String
nm Bool
False) -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"$" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
nm
        Maybe PrimInfo
Nothing -> String -> Sem r (Doc ann)
forall a. HasCallStack => String -> a
error (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
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 ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t
    Term
TUnit -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"■"
    (TBool Bool
b) -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
1 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 ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Char -> String
forall a. Show a => a -> String
show Char
c)
    TString String
cs -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
doubleQuotes (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
cs
    TAbs Quantifier
q Bind [Pattern_ UD] Term
bnd -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
      Bind [Pattern_ UD] Term
-> (([Pattern_ UD], Term) -> Sem r (Doc ann)) -> Sem r (Doc ann)
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
bnd ((([Pattern_ UD], Term) -> Sem r (Doc ann)) -> Sem r (Doc ann))
-> (([Pattern_ UD], Term) -> Sem r (Doc ann)) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ \([Pattern_ UD]
args, Term
body) ->
        Quantifier -> Sem r (Doc ann)
forall {m :: * -> *} {ann}.
Applicative m =>
Quantifier -> m (Doc ann)
prettyQ Quantifier
q
          Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> ([Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep ([Sem r (Doc ann)] -> Sem r (Doc ann))
-> Sem r [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") ((Pattern_ UD -> Sem r (Doc ann))
-> [Pattern_ UD] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Pattern_ UD]
args))
          Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"."
          Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
body)
     where
      prettyQ :: Quantifier -> m (Doc ann)
prettyQ Quantifier
Lam = String -> m (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"λ"
      prettyQ Quantifier
All = String -> m (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"∀"
      prettyQ Quantifier
Ex = String -> m (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"∃"

    -- special case for fully applied unary operators
    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 ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (UOp -> PA
ugetPA UOp
uop) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
            Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> UOp -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
UOp -> Sem r (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
_) ->
          PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (UOp -> PA
ugetPA UOp
uop) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
            UOp -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
UOp -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty UOp
uop Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t)
        Maybe OpInfo
_ -> String -> Sem r (Doc ann)
forall a. HasCallStack => String -> a
error (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
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
    -- special case for fully applied binary operators
    TApp (TPrim (PrimBOp BOp
bop)) (TTup [Term
t1, Term
t2]) ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
bop) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep
          [ Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t1)
          , BOp -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
BOp -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty BOp
bop
          , Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t2)
          ]
    -- Always pretty-print function applications with parentheses
    TApp Term
t1 Term
t2 ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t1) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[LFresh, Reader PA] r =>
Term -> Sem r (Doc ann)
prettyTermP Term
t2
    TTup [Term]
ts -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ do
      [Sem r (Doc ann)]
ds <- Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") ((Term -> Sem r (Doc ann)) -> [Term] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Term]
ts)
      Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens ([Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
ds)
    TContainer Container
c [(Term, Maybe Term)]
ts Maybe (Ellipsis Term)
e -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ do
      [Sem r (Doc ann)]
ds <- Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") (((Term, Maybe Term) -> Sem r (Doc ann))
-> [(Term, Maybe Term)] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map (Term, Maybe Term) -> Sem r (Doc ann)
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, Maybe Term)]
ts)
      let pe :: [Sem r (Doc ann)]
pe = case Maybe (Ellipsis Term)
e of
            Maybe (Ellipsis Term)
Nothing -> []
            Just (Until Term
t) -> [String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"..", Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t]
      Container -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Container -> Sem r (Doc ann) -> Sem r (Doc ann)
containerDelims Container
c ([Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep ([Sem r (Doc ann)]
ds [Sem r (Doc ann)] -> [Sem r (Doc ann)] -> [Sem r (Doc ann)]
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) = t -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
t -> Sem r (Doc ann)
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) = Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (t -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
t -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty t
t) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"#" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (t -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
t -> Sem r (Doc ann)
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
bqst ->
      Bind (Telescope (Qual_ UD)) Term
-> ((Telescope (Qual_ UD), Term) -> Sem r (Doc ann))
-> Sem r (Doc ann)
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
bqst (((Telescope (Qual_ UD), Term) -> Sem r (Doc ann))
 -> Sem r (Doc ann))
-> ((Telescope (Qual_ UD), Term) -> Sem r (Doc ann))
-> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ \(Telescope (Qual_ UD)
qs, Term
t) ->
        PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Container -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Container -> Sem r (Doc ann) -> Sem r (Doc ann)
containerDelims Container
c ([Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t, String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"|", Telescope (Qual_ UD) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Telescope (Qual_ UD) -> Sem r (Doc ann)
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 -> Integer -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => Integer -> m (Doc ann)
integer Integer
n
    TChain Term
t [Link_ UD]
lks ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Eq) (Sem r (Doc ann) -> Sem r (Doc ann))
-> ([Sem r (Doc ann)] -> Sem r (Doc ann))
-> [Sem r (Doc ann)]
-> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep ([Sem r (Doc ann)] -> Sem r (Doc ann))
-> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t)
          Sem r (Doc ann) -> [Sem r (Doc ann)] -> [Sem r (Doc ann)]
forall a. a -> [a] -> [a]
: (Link_ UD -> [Sem r (Doc ann)]) -> [Link_ UD] -> [Sem r (Doc ann)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Link_ UD -> [Sem r (Doc ann)]
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
t2) =
        [ BOp -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
BOp -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty BOp
op
        , PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA (BOp -> PA
getPA BOp
op) (Sem r (Doc ann) -> Sem r (Doc ann))
-> (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann)
-> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t2
        ]
    TLet Bind (Telescope (Binding_ UD)) Term
bnd -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
      Bind (Telescope (Binding_ UD)) Term
-> ((Telescope (Binding_ UD), Term) -> Sem r (Doc ann))
-> Sem r (Doc ann)
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
bnd (((Telescope (Binding_ UD), Term) -> Sem r (Doc ann))
 -> Sem r (Doc ann))
-> ((Telescope (Binding_ UD), Term) -> Sem r (Doc ann))
-> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ \(Telescope (Binding_ UD)
bs, Term
t2) -> do
        [Sem r (Doc ann)]
ds <- Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") ((Binding_ UD -> Sem r (Doc ann))
-> [Binding_ UD] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map Binding_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Binding_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty (Telescope (Binding_ UD) -> [Binding_ UD]
forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope (Binding_ UD)
bs))
        [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep
          [ String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"let"
          , [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
ds
          , String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"in"
          , Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t2
          ]
    TCase [Branch]
b ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"{?" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> [Branch] -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
[Branch] -> Sem r (Doc ann)
prettyBranches [Branch]
b) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"?}"
    TAscr Term
t PolyType
ty ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
ascrPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
":" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (PolyType -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
PolyType -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty PolyType
ty)
    TRat Rational
r -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Rational -> String
prettyDecimal Rational
r)
    TTyOp TyOp
op Type
ty ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        TyOp -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
TyOp -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty TyOp
op Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty
    Term
TWild -> String -> Sem r (Doc ann)
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 = Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
brackets
containerDelims Container
BagContainer = Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann)
bag
containerDelims Container
SetContainer = Sem r (Doc ann) -> Sem r (Doc ann)
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
  [] -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
""
  Branch
b : [Branch]
bs ->
    Branch -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Branch -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Branch
b
      Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ (Branch -> Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> [Branch] -> Sem r (Doc ann)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
($+$) (Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann))
-> (Branch -> Sem r (Doc ann))
-> Branch
-> Sem r (Doc ann)
-> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"," Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+>) (Sem r (Doc ann) -> Sem r (Doc ann))
-> (Branch -> Sem r (Doc ann)) -> Branch -> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Branch -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Branch -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty) Sem r (Doc ann)
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 = Branch
-> ((Telescope (Guard_ UD), Term) -> Sem r (Doc ann))
-> Sem r (Doc ann)
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_ UD), Term) -> Sem r (Doc ann))
 -> Sem r (Doc ann))
-> ((Telescope (Guard_ UD), Term) -> Sem r (Doc ann))
-> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ \(Telescope (Guard_ UD)
gs, Term
t) ->
    Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Telescope (Guard_ UD) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Telescope (Guard_ UD) -> Sem r (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 -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"otherwise"
    Telescope (Guard_ UD)
gs -> (Guard_ UD -> Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> [Guard_ UD] -> Sem r (Doc ann)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Guard_ UD
g Sem r (Doc ann)
r -> Guard_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Guard_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Guard_ UD
g Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
r) (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"") (Telescope (Guard_ UD) -> [Guard_ UD]
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
et -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"if" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed Embed Term
et)
    GPat Embed Term
et Pattern_ UD
p -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"when" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed Embed Term
et) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"is" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (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 -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"let" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Binding_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Binding_ UD -> Sem r (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
x (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t) ->
      [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Name Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Term
x, String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"=", Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
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 ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Name Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Term
x, String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
":", PolyType -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
PolyType -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Embedded (Embed PolyType)
PolyType
ty, String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"=", Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Embedded (Embed Term)
Term
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 (Telescope (Qual_ UD) -> [Qual_ UD]
forall b. Alpha b => Telescope b -> [b]
fromTelescope -> [Qual_ UD]
qs) = do
    [Sem r (Doc ann)]
ds <- Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") ((Qual_ UD -> Sem r (Doc ann)) -> [Qual_ UD] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map Qual_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Qual_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Qual_ UD]
qs)
    [Sem r (Doc ann)] -> Sem r (Doc ann)
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
x (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t) -> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Name Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Term
x, String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"in", Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
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 ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Embedded (Embed Term)
Term
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 {} = PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
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 = PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
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
x -> Name Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Term
x
    Pattern_ UD
PWild -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"_"
    PAscr Pattern_ UD
p Type
ty ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
ascrPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
":" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty)
    Pattern_ UD
PUnit -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"■"
    PBool Bool
b -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
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 ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Char -> String
forall a. Show a => a -> String
show Char
c)
    PString String
s -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (ShowS
forall a. Show a => a -> String
show String
s)
    PTup [Pattern_ UD]
ts -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ do
      [Sem r (Doc ann)]
ds <- Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") ((Pattern_ UD -> Sem r (Doc ann))
-> [Pattern_ UD] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Pattern_ UD]
ts)
      Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens ([Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
ds)
    PInj Side
s Pattern_ UD
p ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        Side -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Side -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Side
s Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[LFresh, Reader PA] r =>
Pattern_ UD -> Sem r (Doc ann)
prettyPatternP Pattern_ UD
p
    PNat Integer
n -> Integer -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => Integer -> m (Doc ann)
integer Integer
n
    PCons Pattern_ UD
p1 Pattern_ UD
p2 ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Cons) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p1) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"::" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
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 -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ do
      [Sem r (Doc ann)]
ds <- Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") ((Pattern_ UD -> Sem r (Doc ann))
-> [Pattern_ UD] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Pattern_ UD]
ps)
      Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
brackets ([Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
ds)
    PAdd Side
L Pattern_ UD
p Term
t ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Add) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"+" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t)
    PAdd Side
R Pattern_ UD
p Term
t ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Add) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"+" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
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
t ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Mul) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"*" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t)
    PMul Side
R Pattern_ UD
p Term
t ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Mul) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"*" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
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
t ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Sub) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"-" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Term -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Term -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Term
t)
    PNeg Pattern_ UD
p ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (UOp -> PA
ugetPA UOp
Neg) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"-" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
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 ->
      PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Div) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
        Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p1) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
"/" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p2)
    PNonlinear Pattern_ UD
p Name Term
_ -> Pattern_ UD -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern_ UD -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Pattern_ UD
p