------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples of pretty printing
------------------------------------------------------------------------
{-# OPTIONS --sized-types #-}
module README.Text.Pretty where
open import Size
open import Data.Bool.Base
open import Data.List.Base as List
open import Data.List.NonEmpty as List⁺
open import Data.Nat.Base
open import Data.Product.Base using (_×_; uncurry; _,_)
open import Data.String.Base hiding (parens; _<+>_)
open import Data.Vec.Base as Vec
open import Function.Base
-- We import the pretty printer and pass 80 to say that we do not want to
-- have lines longer than 80 characters
open import Text.Pretty 80
open import Relation.Binary.PropositionalEquality
------------------------------------------------------------------------
-- A small declarative programming language
------------------------------------------------------------------------
-- We define a small programming language where definitions are
-- introduced by providing a non-empty list of equations with:
-- * the same number of patterns on the LHS
-- * a term on the RHS of each equation
-- A pattern is either a variable or a constructor applied to a
-- list of subpatterns
data Pattern (i : Size) : Set where
var : String → Pattern i
con : ∀ {j : Size< i} → String → List (Pattern j) → Pattern i
-- A term is either a (bound) variable, the application of a
-- named definition / constructor to a list of arguments or a
-- lambda abstraction
data Term (i : Size) : Set where
var : String → Term i
app : ∀ {j : Size< i} → String → List (Term j) → Term i
lam : ∀ {j : Size< i} → String → Term j → Term i
-- As explained before, a definitions is given by a list of equations
infix 1 _by_
record Def : Set where
constructor _by_
field name : String
{arity} : ℕ
equations : List⁺ (Vec (Pattern _) arity × (Term _))
------------------------------------------------------------------------
-- A pretty printer for this language
------------------------------------------------------------------------
-- First we print patterns. We only wrap a pattern in parentheses if it
-- is compound: i.e. if it is a constructor applied to a non-empty list
-- of subpatterns
-- Lists of patterns are printed separated by a single space.
prettyPattern : ∀ {i} → Pattern i → Doc
prettyPatterns : ∀ {i} → List (Pattern i) → Doc
prettyPattern (var v) = text v
prettyPattern (con c []) = text c
prettyPattern (con c ps) = parens $ text c <+> prettyPatterns ps
prettyPatterns = hsep ∘ List.map prettyPattern
-- Next we print terms. The Bool argument tells us whether we are on
-- the RHS of an application (in which case it is sensible to wrap
-- complex subterms in parentheses).
prettyTerm : ∀ {i} → Bool → Term i → Doc
prettyTerm l (var v) = text v
prettyTerm l (app f []) = text f
prettyTerm l (app f es) = if l then parens else id
$ text f <+> sep (List.map (prettyTerm true) es)
prettyTerm l (lam x b) = if l then parens else id
$ text "λ" <+> text x <> text "." <+> prettyTerm false b
-- We now have all the pieces to print definitions.
-- We print the equations below each other by using vcat.
--
-- The LHS is printed as follows: the name of the function followed by
-- the space-separated list of patterns (if any) and then an equal sign.
--
-- The RHS is printed as a term which is *not* on the RHS of an application.
--
-- Finally we can layout the definition in two different manners:
-- * either LHS followed by RHS
-- * or LHS followed and the RHS as a relative block (indented by 2 spaces)
-- on the next line
prettyDef : Def → Doc
prettyDef (fun by eqs) =
vcat $ List⁺.toList $ flip List⁺.map eqs $ uncurry $ λ ps e →
let lhs = text fun <+> (case ps of λ where
[] → text "="
_ → prettyPatterns (Vec.toList ps) <+> text "=")
rhs = prettyTerm false e
in lhs <+> rhs <|> lhs $$ (spaces 2 <> rhs)
-- The pretty printer is obtained by using the renderer.
pretty : Def → String
pretty = render ∘ prettyDef
------------------------------------------------------------------------
-- Some examples
------------------------------------------------------------------------
-- Our first example is the identity function defined as a λ-abstraction
`id : Def
`id = "id" by ([] , lam "x" (var "x")) ∷ []
_ : pretty `id ≡ "id = λ x. x"
_ = refl
-- If we were to assume that this definition also takes a level (a) and
-- a Set at that level (A) as arguments, we can have a slightly more complex
-- definition like so.
`explicitid : Def
`explicitid = "id" by (var "a" ∷ var "A" ∷ [] , lam "x" (var "x")) ∷ []
_ : pretty `explicitid ≡ "id a A = λ x. x"
_ = refl
-- A more complex example: boolFilter, a function that takes a boolean
-- predicate and a list as arguments and returns a list containing only
-- the values that satisfy the predicate.
-- We use nil and con for [] and _∷_ as our little toy language does not
-- support infix notations.
`filter : Def
`filter = "boolFilter"
by ( var "P?" ∷ con "nil" [] ∷ []
, app "nil" []
)
∷ ( var "P?" ∷ con "con" (var "x" ∷ var "xs" ∷ []) ∷ []
, let rec = app "filter" (var "P?" ∷ var "xs" ∷ []) in
app "if" (app "P?" (var "x" ∷ [])
∷ app "con" (var "x" ∷ rec ∷ [])
∷ rec
∷ [])
)
∷ []
_ : pretty `filter ≡
"boolFilter P? nil = nil
\ \boolFilter P? (con x xs) = if (P? x) (con x (filter P? xs)) (filter P? xs)"
_ = refl
-- We can once more revisit this example with its more complex counterpart:
-- boolFilter taking its level and set arguments explicitly (idem for the
-- list constructors nil and con).
-- This time laying out the second equation on a single line would produce a
-- string larger than 80 characters long. So the pretty printer decides to
-- make the RHS a relative block indented by 2 spaces.
`explicitfilter : Def
`explicitfilter = "boolFilter"
by ( var "a" ∷ var "A" ∷ var "P?" ∷ con "nil" [] ∷ []
, app "nil" (var "a" ∷ var "A" ∷ [])
)
∷ ( var "a" ∷ var "A" ∷ var "P?" ∷ con "con" (var "x" ∷ var "xs" ∷ []) ∷ []
, let rec = app "filter" (var "a" ∷ var "A" ∷ var "P?" ∷ var "xs" ∷ []) in
app "if" (app "P?" (var "x" ∷ [])
∷ app "con" (var "a" ∷ var "A" ∷ var "x" ∷ rec ∷ [])
∷ rec
∷ [])
)
∷ []
_ : pretty `explicitfilter
≡ "boolFilter a A P? nil = nil a A
\ \boolFilter a A P? (con x xs) =
\ \ if (P? x) (con a A x (filter a A P? xs)) (filter a A P? xs)"
_ = refl