{-# 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(..), 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 Binding
       )
       where

import           Prelude                          hiding ((<>))

import           Control.Lens                     (_1, _2, _3, (%~))
import           Data.Char                        (toLower)
import qualified Data.Map                         as M
import           Data.Set                         (Set)
import           Data.Void

import           Disco.Effects.LFresh
import           Polysemy                         hiding (Embed)
import           Polysemy.Reader

import           Disco.AST.Generic
import           Disco.Extensions
import           Disco.Pretty
import           Disco.Syntax.Operators
import           Disco.Syntax.Prims
import           Disco.Types
import           Unbound.Generics.LocallyNameless hiding (LFresh (..), lunbind)

-- | 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

-- | 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
  = DocString   [String]    -- ^ A documentation string, i.e. a block
                            --   of @||| text@ items
  | DocProperty Property    -- ^ An example/doctest/property of the
                            --   form @!!! forall (x1:ty1) ... . 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
(Int -> TypeDefn -> ShowS)
-> (TypeDefn -> String) -> ([TypeDefn] -> ShowS) -> Show TypeDefn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeDefn] -> ShowS
$cshowList :: [TypeDefn] -> ShowS
show :: TypeDefn -> String
$cshow :: TypeDefn -> String
showsPrec :: Int -> TypeDefn -> ShowS
$cshowsPrec :: Int -> TypeDefn -> ShowS
Show

-- | 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
_1 (([TypeDecl] -> Identity [TypeDecl])
 -> ([TypeDecl], [TermDefn], [TypeDefn])
 -> Identity ([TypeDecl], [TermDefn], [TypeDefn]))
-> ([TypeDecl] -> [TypeDecl])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (TypeDecl
tyDeclTypeDecl -> [TypeDecl] -> [TypeDecl]
forall a. a -> [a] -> [a]
:)) ([Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
partitionDecls [Decl]
ds)
partitionDecls (DDefn  TermDefn
def    : [Decl]
ds) = (([TermDefn] -> Identity [TermDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> Identity ([TypeDecl], [TermDefn], [TypeDefn])
forall s t a b. Field2 s t a b => Lens s t a b
_2 (([TermDefn] -> Identity [TermDefn])
 -> ([TypeDecl], [TermDefn], [TypeDefn])
 -> Identity ([TypeDecl], [TermDefn], [TypeDefn]))
-> ([TermDefn] -> [TermDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (TermDefn
defTermDefn -> [TermDefn] -> [TermDefn]
forall a. a -> [a] -> [a]
:))    ([Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
partitionDecls [Decl]
ds)
partitionDecls (DTyDef TypeDefn
def    : [Decl]
ds) = (([TypeDefn] -> Identity [TypeDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> Identity ([TypeDecl], [TermDefn], [TypeDefn])
forall s t a b. Field3 s t a b => Lens s t a b
_3 (([TypeDefn] -> Identity [TypeDefn])
 -> ([TypeDecl], [TermDefn], [TypeDefn])
 -> Identity ([TypeDecl], [TermDefn], [TypeDefn]))
-> ([TypeDefn] -> [TypeDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
-> ([TypeDecl], [TermDefn], [TypeDefn])
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (TypeDefn
defTypeDefn -> [TypeDefn] -> [TypeDefn]
forall a. a -> [a] -> [a]
:))    ([Decl] -> ([TypeDecl], [TermDefn], [TypeDefn])
partitionDecls [Decl]
ds)
partitionDecls []                   = ([], [], [])

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

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

instance Pretty Decl where
  pretty :: Decl -> Sem r Doc
pretty = \case
    DType  (TypeDecl Name Term
x PolyType
ty) -> Name Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Term
x Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> PolyType -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty PolyType
ty
    DTyDef (TypeDefn String
x [String]
args Type
body) ->
      String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"type" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
x Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep ((String -> Sem r Doc) -> [String] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text [String]
args) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"=" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
body
    DDefn  (TermDefn Name Term
x [Bind [Pattern] Term]
bs) -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat ([Sem r Doc] -> Sem r Doc) -> [Sem r Doc] -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ (Bind [Pattern] Term -> Sem r Doc)
-> [Bind [Pattern] Term] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Name Term, Bind [Pattern] Term) -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty ((Name Term, Bind [Pattern] Term) -> Sem r Doc)
-> (Bind [Pattern] Term -> (Name Term, Bind [Pattern] Term))
-> Bind [Pattern] Term
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name Term
x,)) [Bind [Pattern] Term]
bs

-- | Pretty-print a single clause in a definition.
instance Pretty (Name a, Bind [Pattern] Term) where
  pretty :: (Name a, Bind [Pattern] Term) -> Sem r Doc
pretty (Name a
x, Bind [Pattern] Term
b) = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc)
-> ((([Pattern], Term) -> Sem r Doc) -> Sem r Doc)
-> (([Pattern], Term) -> Sem r Doc)
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind [Pattern] Term
-> (([Pattern], Term) -> Sem r Doc) -> Sem r Doc
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind [Pattern] Term
b ((([Pattern], Term) -> Sem r Doc) -> Sem r Doc)
-> (([Pattern], Term) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \([Pattern]
ps, Term
t) ->
    Name a -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name a
x Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hcat ((Pattern -> Sem r Doc) -> [Pattern] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> Sem r Doc
forall (r :: EffectRow).
Members '[LFresh, Reader PA] r =>
Pattern -> Sem r Doc
prettyPatternP [Pattern]
ps) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"=" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t)

-- | Pretty-print a type declaration.
prettyTyDecl :: Members '[Reader PA, LFresh] r => Name t -> Type -> Sem r Doc
prettyTyDecl :: Name t -> Type -> Sem r Doc
prettyTyDecl Name t
x Type
ty = [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Name t -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name t
x, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":", Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty]

------------------------------------------------------------
-- 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 -> Term
$mTVar :: forall r. Term -> (Name Term -> r) -> (Void# -> r) -> r
TVar name = TVar_ () name

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

pattern TAscr :: Term -> PolyType -> Term
pattern $bTAscr :: Term -> PolyType -> Term
$mTAscr :: forall r. Term -> (Term -> PolyType -> r) -> (Void# -> r) -> r
TAscr term ty = TAscr_ () term ty

-- 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
$mTWild :: forall r. Term -> (Void# -> r) -> (Void# -> r) -> r
TWild = XTerm_ ()

{-# COMPLETE TVar, TPrim, TLet, TParens, TUnit, TBool, TNat, TRat, TChar,
             TString, TAbs, TApp, TTup, TCase, TChain, TTyOp,
             TContainer, TContainerComp, TAscr, TWild #-}

pattern TList :: [Term] -> Maybe (Ellipsis Term) -> Term
pattern $bTList :: [Term] -> Maybe (Ellipsis Term) -> Term
$mTList :: forall r.
Term -> ([Term] -> Maybe (Ellipsis Term) -> r) -> (Void# -> r) -> r
TList ts e <- TContainer_ () ListContainer (map fst -> ts) e
  where
    TList [Term]
ts Maybe (Ellipsis Term)
e = X_TContainer UD
-> Container
-> [(Term, Maybe Term)]
-> Maybe (Ellipsis Term)
-> Term
forall e.
X_TContainer e
-> Container
-> [(Term_ e, Maybe (Term_ e))]
-> Maybe (Ellipsis (Term_ e))
-> Term_ e
TContainer_ () Container
ListContainer ((Term -> (Term, Maybe Term)) -> [Term] -> [(Term, Maybe Term)]
forall a b. (a -> b) -> [a] -> [b]
map (,Maybe Term
forall a. Maybe a
Nothing) [Term]
ts) Maybe (Ellipsis Term)
e

pattern TListComp :: Bind (Telescope Qual) Term -> Term
pattern $bTListComp :: Bind (Telescope Qual) Term -> Term
$mTListComp :: forall r.
Term -> (Bind (Telescope Qual) Term -> r) -> (Void# -> r) -> r
TListComp x = TContainerComp_ () ListContainer x

type Link = Link_ UD

type instance X_TLink UD = ()

pattern TLink :: BOp -> Term -> Link
pattern $bTLink :: BOp -> Term -> Link
$mTLink :: forall r. Link -> (BOp -> Term -> r) -> (Void# -> r) -> r
TLink bop term = TLink_ () bop term

{-# COMPLETE TLink #-}

type Qual = Qual_ UD

type instance X_QBind UD = ()
type instance X_QGuard UD = ()

pattern QBind :: Name Term -> Embed Term -> Qual
pattern $bQBind :: Name Term -> Embed Term -> Qual
$mQBind :: forall r.
Qual -> (Name Term -> Embed Term -> r) -> (Void# -> r) -> r
QBind namet embedt = QBind_ () namet embedt

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

{-# COMPLETE QBind, QGuard #-}

type Binding = Binding_ UD

pattern Binding :: Maybe (Embed PolyType) -> Name Term -> Embed Term -> Binding
pattern $bBinding :: Maybe (Embed PolyType) -> Name Term -> Embed Term -> Binding
$mBinding :: forall r.
Binding
-> (Maybe (Embed PolyType) -> Name Term -> Embed Term -> r)
-> (Void# -> r)
-> r
Binding m b n = Binding_ m b n

{-# COMPLETE Binding #-}

type Branch = Branch_ UD

type Guard = Guard_ UD

type instance X_GBool UD = ()
type instance X_GPat  UD = ()
type instance X_GLet  UD = ()

pattern GBool :: Embed Term -> Guard
pattern $bGBool :: Embed Term -> Guard
$mGBool :: forall r. Guard -> (Embed Term -> r) -> (Void# -> r) -> r
GBool embedt = GBool_ () embedt

pattern GPat :: Embed Term -> Pattern -> Guard
pattern $bGPat :: Embed Term -> Pattern -> Guard
$mGPat :: forall r.
Guard -> (Embed Term -> Pattern -> r) -> (Void# -> r) -> r
GPat embedt pat = GPat_ () embedt pat

pattern GLet :: Binding -> Guard
pattern $bGLet :: Binding -> Guard
$mGLet :: forall r. Guard -> (Binding -> r) -> (Void# -> r) -> r
GLet b = GLet_ () b

{-# COMPLETE GBool, GPat, GLet #-}

type Pattern = Pattern_ UD

type instance X_PVar UD    = ()
type instance X_PWild UD   = ()
type instance X_PAscr UD   = ()
type instance X_PUnit UD   = ()
type instance X_PBool UD   = ()
type instance X_PTup UD    = ()
type instance X_PInj UD    = ()
type instance X_PNat UD    = ()
type instance X_PChar UD   = ()
type instance X_PString UD = ()
type instance X_PCons UD   = ()
type instance X_PList UD   = ()
type instance X_PAdd UD    = ()
type instance X_PMul UD    = ()
type instance X_PSub UD    = ()
type instance X_PNeg UD    = ()
type instance X_PFrac UD   = ()
type instance X_Pattern UD = Void

pattern PVar :: Name Term -> Pattern
pattern $bPVar :: Name Term -> Pattern
$mPVar :: forall r. Pattern -> (Name Term -> r) -> (Void# -> r) -> r
PVar name = PVar_ () name

pattern PWild :: Pattern
pattern $bPWild :: Pattern
$mPWild :: forall r. Pattern -> (Void# -> r) -> (Void# -> r) -> r
PWild = PWild_ ()

 -- (?) 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 -> Type -> Pattern
$mPAscr :: forall r. Pattern -> (Pattern -> Type -> r) -> (Void# -> r) -> r
PAscr p ty = PAscr_ () p ty

pattern PUnit :: Pattern
pattern $bPUnit :: Pattern
$mPUnit :: forall r. Pattern -> (Void# -> r) -> (Void# -> r) -> r
PUnit = PUnit_ ()

pattern PBool :: Bool -> Pattern
pattern $bPBool :: Bool -> Pattern
$mPBool :: forall r. Pattern -> (Bool -> r) -> (Void# -> r) -> r
PBool  b = PBool_ () b

pattern PChar :: Char -> Pattern
pattern $bPChar :: Char -> Pattern
$mPChar :: forall r. Pattern -> (Char -> r) -> (Void# -> r) -> r
PChar c = PChar_ () c

pattern PString :: String -> Pattern
pattern $bPString :: String -> Pattern
$mPString :: forall r. Pattern -> (String -> r) -> (Void# -> r) -> r
PString s = PString_ () s

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

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

pattern PNat  :: Integer -> Pattern
pattern $bPNat :: Integer -> Pattern
$mPNat :: forall r. Pattern -> (Integer -> r) -> (Void# -> r) -> r
PNat n = PNat_ () n

pattern PCons :: Pattern -> Pattern -> Pattern
pattern $bPCons :: Pattern -> Pattern -> Pattern
$mPCons :: forall r. Pattern -> (Pattern -> Pattern -> r) -> (Void# -> r) -> r
PCons  p1 p2 = PCons_ () p1 p2

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

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

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

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

pattern PNeg :: Pattern -> Pattern
pattern $bPNeg :: Pattern -> Pattern
$mPNeg :: forall r. Pattern -> (Pattern -> r) -> (Void# -> r) -> r
PNeg p = PNeg_ () p

pattern PFrac :: Pattern -> Pattern -> Pattern
pattern $bPFrac :: Pattern -> Pattern -> Pattern
$mPFrac :: forall r. Pattern -> (Pattern -> Pattern -> r) -> (Void# -> r) -> r
PFrac p1 p2 = PFrac_ () p1 p2

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

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

instance Pretty Term where
  pretty :: Term -> Sem r Doc
pretty = \case
    TVar Name Term
x      -> Name Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Term
x
    TPrim (PrimUOp UOp
uop) ->
      case UOp -> Map UOp OpInfo -> Maybe OpInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup UOp
uop Map UOp OpInfo
uopMap of
        Just (OpInfo (UOpF UFixity
Pre UOp
_) (String
syn:[String]
_) Int
_)  -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
syn Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"~"
        Just (OpInfo (UOpF UFixity
Post UOp
_) (String
syn:[String]
_) Int
_) -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"~" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
syn
        Maybe OpInfo
_ -> String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"pretty @Term: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ UOp -> String
forall a. Show a => a -> String
show UOp
uop String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not in the uopMap!"
    TPrim (PrimBOp BOp
bop) -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"~" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> BOp -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty BOp
bop Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"~"
    TPrim Prim
p ->
      case Prim -> Map Prim PrimInfo -> Maybe PrimInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Prim
p Map Prim PrimInfo
primMap of
        Just (PrimInfo Prim
_ String
nm Bool
True)  -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
nm
        Just (PrimInfo Prim
_ String
nm Bool
False) -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"$" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
nm
        Maybe PrimInfo
Nothing -> String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"pretty @Term: Prim " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Prim -> String
forall a. Show a => a -> String
show Prim
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not in the primMap!"
    TParens Term
t   -> Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t
    Term
TUnit       -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"■"
    (TBool Bool
b)     -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text ((Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Bool -> String
forall a. Show a => a -> String
show Bool
b)
    TChar Char
c     -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Char -> String
forall a. Show a => a -> String
show Char
c)
    TString String
cs  -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
doubleQuotes (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
cs
    TAbs Quantifier
q Bind [Pattern] Term
bnd  -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      Bind [Pattern] Term
-> (([Pattern], Term) -> Sem r Doc) -> Sem r Doc
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind [Pattern] Term
bnd ((([Pattern], Term) -> Sem r Doc) -> Sem r Doc)
-> (([Pattern], Term) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \([Pattern]
args, Term
body) ->
      Quantifier -> Sem r Doc
forall (m :: * -> *). Applicative m => Quantifier -> m Doc
prettyQ Quantifier
q
        Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep ([Sem r Doc] -> Sem r Doc) -> Sem r [Sem r Doc] -> Sem r Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Pattern -> Sem r Doc) -> [Pattern] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Pattern]
args))
        Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"."
        Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
body)
      where
        prettyQ :: Quantifier -> m Doc
prettyQ Quantifier
Lam = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"λ"
        prettyQ Quantifier
All = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"∀"
        prettyQ Quantifier
Ex  = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"∃"

    -- 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 -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (UOp -> PA
ugetPA UOp
uop) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
          Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> UOp -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty UOp
uop
        Just (OpInfo (UOpF UFixity
Pre  UOp
_) [String]
_ Int
_) -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (UOp -> PA
ugetPA UOp
uop) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
          UOp -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty UOp
uop Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t)
        Maybe OpInfo
_ -> String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"pretty @Term: uopMap doesn't contain " String -> ShowS
forall a. [a] -> [a] -> [a]
++ UOp -> String
forall a. Show a => a -> String
show UOp
uop

    -- special case for fully applied binary operators
    TApp (TPrim (PrimBOp BOp
bop)) (TTup [Term
t1, Term
t2]) -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
bop) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep
      [ Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t1)
      , BOp -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty BOp
bop
      , Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t2)
      ]

    -- Always pretty-print function applications with parentheses
    TApp Term
t1 Term
t2  -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t1) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Term -> Sem r Doc
forall (r :: EffectRow).
Members '[LFresh, Reader PA] r =>
Term -> Sem r Doc
prettyTermP Term
t2

    TTup [Term]
ts     -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ do
      [Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Term -> Sem r Doc) -> [Term] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Term]
ts)
      Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds)
    TContainer Container
c [(Term, Maybe Term)]
ts Maybe (Ellipsis Term)
e  -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ do
      [Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") (((Term, Maybe Term) -> Sem r Doc)
-> [(Term, Maybe Term)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term, Maybe Term) -> Sem r Doc
forall (r :: EffectRow) t t.
(Member (Reader PA) r, Member LFresh r, Pretty t, Pretty t) =>
(t, Maybe t) -> Sem r Doc
prettyCount [(Term, Maybe Term)]
ts)
      let pe :: [Sem r Doc]
pe = case Maybe (Ellipsis Term)
e of
                 Maybe (Ellipsis Term)
Nothing        -> []
                 Just (Until Term
t) -> [String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"..", Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t]
      Container -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Container -> Sem r Doc -> Sem r Doc
containerDelims Container
c ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep ([Sem r Doc]
ds [Sem r Doc] -> [Sem r Doc] -> [Sem r Doc]
forall a. [a] -> [a] -> [a]
++ [Sem r Doc]
pe))
      where
        prettyCount :: (t, Maybe t) -> Sem r Doc
prettyCount (t
t, Maybe t
Nothing) = t -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty t
t
        prettyCount (t
t, Just t
n)  = Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (t -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty t
t) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"#" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (t -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty t
n)
    TContainerComp Container
c Bind (Telescope Qual) Term
bqst ->
      Bind (Telescope Qual) Term
-> ((Telescope Qual, Term) -> Sem r Doc) -> Sem r Doc
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind (Telescope Qual) Term
bqst (((Telescope Qual, Term) -> Sem r Doc) -> Sem r Doc)
-> ((Telescope Qual, Term) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \(Telescope Qual
qs,Term
t) ->
      PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Container -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Container -> Sem r Doc -> Sem r Doc
containerDelims Container
c ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"|", Telescope Qual -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Telescope Qual
qs])
    TNat Integer
n       -> Integer -> Sem r Doc
forall (m :: * -> *). Applicative m => Integer -> m Doc
integer Integer
n
    TChain Term
t [Link]
lks -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Eq) (Sem r Doc -> Sem r Doc)
-> ([Sem r Doc] -> Sem r Doc) -> [Sem r Doc] -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep ([Sem r Doc] -> Sem r Doc) -> [Sem r Doc] -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
        Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t)
        Sem r Doc -> [Sem r Doc] -> [Sem r Doc]
forall a. a -> [a] -> [a]
: (Link -> [Sem r Doc]) -> [Link] -> [Sem r Doc]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Link -> [Sem r Doc]
forall (r :: EffectRow).
(Member (Reader PA) r, Member LFresh r) =>
Link -> [Sem r Doc]
prettyLink [Link]
lks
      where
        prettyLink :: Link -> [Sem r Doc]
prettyLink (TLink BOp
op Term
t2) =
          [ BOp -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty BOp
op
          , PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA (BOp -> PA
getPA BOp
op) (Sem r Doc -> Sem r Doc)
-> (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t2
          ]
    TLet Bind (Telescope Binding) Term
bnd -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      Bind (Telescope Binding) Term
-> ((Telescope Binding, Term) -> Sem r Doc) -> Sem r Doc
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind (Telescope Binding) Term
bnd (((Telescope Binding, Term) -> Sem r Doc) -> Sem r Doc)
-> ((Telescope Binding, Term) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \(Telescope Binding
bs, Term
t2) -> do
        [Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Binding -> Sem r Doc) -> [Binding] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Binding -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (Telescope Binding -> [Binding]
forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope Binding
bs))
        [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep
          [ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"let"
          , [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds
          , String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"in"
          , Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t2
          ]

    TCase [Branch]
b    -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"{?" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> [Branch] -> Sem r Doc
forall (r :: EffectRow).
Members '[Reader PA, LFresh] r =>
[Branch] -> Sem r Doc
prettyBranches [Branch]
b) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"?}"
    TAscr Term
t PolyType
ty -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
ascrPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (PolyType -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty PolyType
ty)
    TRat  Rational
r    -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Rational -> String
prettyDecimal Rational
r)
    TTyOp TyOp
op Type
ty  -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      TyOp -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty TyOp
op Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty
    Term
TWild -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"_"

-- | Print appropriate delimiters for a container literal.
containerDelims :: Member (Reader PA) r => Container -> (Sem r Doc -> Sem r Doc)
containerDelims :: Container -> Sem r Doc -> Sem r Doc
containerDelims Container
ListContainer = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
brackets
containerDelims Container
BagContainer  = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc
bag
containerDelims Container
SetContainer  = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
braces

prettyBranches :: Members '[Reader PA, LFresh] r => [Branch] -> Sem r Doc
prettyBranches :: [Branch] -> Sem r Doc
prettyBranches = \case
  [] -> String -> Sem r Doc
forall a. HasCallStack => String -> a
error String
"Empty branches are disallowed."
  Branch
b:[Branch]
bs ->
    Branch -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Branch
b
    Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
    (Branch -> Sem r Doc -> Sem r Doc)
-> Sem r Doc -> [Branch] -> Sem r Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
($+$) (Sem r Doc -> Sem r Doc -> Sem r Doc)
-> (Branch -> Sem r Doc) -> Branch -> Sem r Doc -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"," Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+>) (Sem r Doc -> Sem r Doc)
-> (Branch -> Sem r Doc) -> Branch -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Branch -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty) Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
empty [Branch]
bs

-- | Pretty-print a single branch in a case expression.
instance Pretty Branch where
  pretty :: Branch -> Sem r Doc
pretty Branch
br = Branch -> ((Telescope Guard, Term) -> Sem r Doc) -> Sem r Doc
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Branch
br (((Telescope Guard, Term) -> Sem r Doc) -> Sem r Doc)
-> ((Telescope Guard, Term) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \(Telescope Guard
gs,Term
t) ->
    Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Telescope Guard -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Telescope Guard
gs

-- | Pretty-print the guards in a single branch of a case expression.
instance Pretty (Telescope Guard) where
  pretty :: Telescope Guard -> Sem r Doc
pretty = \case
    Telescope Guard
TelEmpty -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"otherwise"
    Telescope Guard
gs       -> (Guard -> Sem r Doc -> Sem r Doc)
-> Sem r Doc -> [Guard] -> Sem r Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Guard
g Sem r Doc
r -> Guard -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Guard
g Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
r) (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"") (Telescope Guard -> [Guard]
forall b. Alpha b => Telescope b -> [b]
fromTelescope Telescope Guard
gs)

instance Pretty Guard where
  pretty :: Guard -> Sem r Doc
pretty = \case
    GBool Embed Term
et  -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"if" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed Embed Term
et)
    GPat Embed Term
et Pattern
p -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"when" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed Embed Term
et) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"is" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p
    GLet Binding
b    -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"let" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Binding -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Binding
b

-- | Pretty-print a binding, i.e. a pairing of a name (with optional
--   type annotation) and term.
instance Pretty Binding where
  pretty :: Binding -> Sem r Doc
pretty = \case
    Binding Maybe (Embed PolyType)
Nothing Name Term
x (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t) ->
      [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Name Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Term
x, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"=", Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Embedded (Embed Term)
Term
t]
    Binding (Just (Embed PolyType -> Embedded (Embed PolyType)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed PolyType)
ty)) Name Term
x (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t) ->
      [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Name Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Term
x, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":", PolyType -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Embedded (Embed PolyType)
PolyType
ty, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"=", Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Embedded (Embed Term)
Term
t]

-- | Pretty-print the qualifiers in a comprehension.
instance Pretty (Telescope Qual) where
  pretty :: Telescope Qual -> Sem r Doc
pretty (Telescope Qual -> [Qual]
forall b. Alpha b => Telescope b -> [b]
fromTelescope -> [Qual]
qs) = do
    [Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Qual -> Sem r Doc) -> [Qual] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Qual -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Qual]
qs)
    [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds

-- | Pretty-print a single qualifier in a comprehension.
instance Pretty Qual where
  pretty :: Qual -> Sem r Doc
pretty = \case
    QBind Name Term
x (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t) -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Name Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Term
x, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"in", Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Embedded (Embed Term)
Term
t]
    QGuard (Embed Term -> Embedded (Embed Term)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed Term)
t)  -> Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Embedded (Embed Term)
Term
t

-- | Pretty-print a pattern with guaranteed parentheses.
prettyPatternP :: Members '[LFresh, Reader PA] r => Pattern -> Sem r Doc
prettyPatternP :: Pattern -> Sem r Doc
prettyPatternP p :: Pattern
p@PTup{} = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p
prettyPatternP Pattern
p        = PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p

-- 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 :: Pattern -> Sem r Doc
pretty = \case
    PVar Name Term
x      -> Name Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Term
x
    Pattern
PWild       -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"_"
    PAscr Pattern
p Type
ty  -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
ascrPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty)
    Pattern
PUnit       -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"■"
    PBool Bool
b     -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Bool -> String
forall a. Show a => a -> String
show Bool
b
    PChar Char
c     -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Char -> String
forall a. Show a => a -> String
show Char
c)
    PString String
s   -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (ShowS
forall a. Show a => a -> String
show String
s)
    PTup [Pattern]
ts     -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ do
      [Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Pattern -> Sem r Doc) -> [Pattern] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Pattern]
ts)
      Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds)
    PInj Side
s Pattern
p    -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      Side -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Side
s Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Pattern -> Sem r Doc
forall (r :: EffectRow).
Members '[LFresh, Reader PA] r =>
Pattern -> Sem r Doc
prettyPatternP Pattern
p
    PNat Integer
n      -> Integer -> Sem r Doc
forall (m :: * -> *). Applicative m => Integer -> m Doc
integer Integer
n
    PCons Pattern
p1 Pattern
p2 -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Cons) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p1) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"::" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p2)
    PList [Pattern]
ps    -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ do
      [Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Pattern -> Sem r Doc) -> [Pattern] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Pattern]
ps)
      Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
brackets ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds)
    PAdd Side
L Pattern
p Term
t  -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Add) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"+" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t)
    PAdd Side
R Pattern
p Term
t  -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Add) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"+" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p)
    PMul Side
L Pattern
p Term
t  -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Mul) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"*" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t)
    PMul Side
R Pattern
p Term
t  -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Mul) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"*" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p)
    PSub Pattern
p Term
t    -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Sub) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"-" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Term
t)
    PNeg Pattern
p      -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (UOp -> PA
ugetPA UOp
Neg) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"-" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p)
    PFrac Pattern
p1 Pattern
p2 -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Div) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
      Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p1) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"/" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Pattern -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Pattern
p2)