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