||| Abstract syntax for terms.
module Obs.Term

import Data.Fin
import Obs.Sort
import Text.Bounded
import Text.PrettyPrint.Prettyprinter

%default total

-- Definition ------------------------------------------------------------------

public export
data Term : Nat -> Type where
  Var    : String -> Fin n -> Term n
  -- Sorts
  Sort   : Sort -> Term n
  -- Dependent Product
  Pi     : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
  Lambda : WithBounds String -> WithBounds (Term (S n)) -> Term n
  App    : WithBounds (Term n) -> WithBounds (Term n) -> Term n
  -- Dependent Sums
  Sigma  : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
  Pair   : WithBounds (Term n) -> WithBounds (Term n) -> Term n
  Fst    : WithBounds (Term n) -> Term n
  Snd    : WithBounds (Term n) -> Term n
  -- True
  Top    : Term n
  Point  : Term n
  -- False
  Bottom : Term n
  Absurd : WithBounds (Term n) -> WithBounds (Term n) -> Term n
  -- Equality
  Equal  : WithBounds (Term n) -> WithBounds (Term n) -> Term n
  Refl   : WithBounds (Term n) -> Term n
  Transp : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
  Cast   : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
  CastId : WithBounds (Term n) -> Term n

public export
record Definition (n : Nat) where
  constructor MkDefinition
  name   : WithBounds String
  ty     : WithBounds (Term n)
  tm     : WithBounds (Term n)

public export
data Block : Nat -> Type where
  Nil  : Block 0
  (:<) : Block n -> Definition n -> Block (S n)

-- Pretty Print ----------------------------------------------------------------

prettyPrec : Prec -> Term n -> Doc ann
prettyPrecBounds : Prec -> WithBounds (Term n) -> Doc ann

prettyPrec d (Var var _) = pretty var
prettyPrec d (Sort s) = prettyPrec d s
prettyPrec d (Pi var a b) =
  parenthesise (d > Open) $
  group $
  parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
  pretty "->" <+> softline <+>
  prettyPrecBounds Open b
prettyPrec d (Lambda var t) =
  parenthesise (d > Open) $
  group $
  backslash <+> pretty var.val <++>
  pretty "=>" <+> softline <+>
  prettyPrecBounds Open t
prettyPrec d (App t u) =
  parenthesise (d >= App) $
  group $
  fillSep [prettyPrecBounds Open t, prettyPrecBounds App u]
prettyPrec d (Sigma var a b) =
  parenthesise (d >= App) $
  group $
  parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
  pretty "**" <+> softline <+>
  prettyPrecBounds Open b
prettyPrec d (Pair t u) =
  angles $
  group $
  neutral <++> prettyPrecBounds Open t <+> comma <+> softline <+> prettyPrecBounds Open u <++> neutral
prettyPrec d (Fst t) =
  parenthesise (d >= App) $
  group $
  fillSep [pretty "fst", prettyPrecBounds App t]
prettyPrec d (Snd t) =
  parenthesise (d >= App) $
  group $
  fillSep [pretty "snd", prettyPrecBounds App t]
prettyPrec d Top = pretty "()"
prettyPrec d Point = pretty "tt"
prettyPrec d Bottom = pretty "Void"
prettyPrec d (Absurd a t) =
  parenthesise (d > Open) $
  group $
  fillSep [pretty "absurd", prettyPrecBounds App a, prettyPrecBounds App t]
prettyPrec d (Equal t u) =
  parenthesise (d >= Equal) $
  group $
  prettyPrecBounds Equal t <++> pretty "~" <+> softline <+> prettyPrecBounds Equal u
prettyPrec d (Refl t) =
  parenthesise (d >= App) $
  group $
  fillSep [pretty "refl", prettyPrecBounds App t]
prettyPrec d (Transp t b u t' e) =
  parenthesise (d >= App) $
  group $
  fillSep $
  [ pretty "transp"
  , prettyPrecBounds App t
  , prettyPrecBounds App b
  , prettyPrecBounds App u
  , prettyPrecBounds App t'
  , prettyPrecBounds App e
  ]
prettyPrec d (Cast b e t) =
  parenthesise (d >= App) $
  group $
  fillSep [pretty "cast", prettyPrecBounds App b, prettyPrecBounds App e, prettyPrecBounds App t]
prettyPrec d (CastId t) =
  parenthesise (d >= App) $
  group $
  fillSep [pretty "castRefl", prettyPrecBounds App t]

prettyPrecBounds d (MkBounded v _ _) = prettyPrec d v

export
Pretty (Term n) where
  prettyPrec = Term.prettyPrec

export
Pretty (Definition n) where
  pretty def = group $
    pretty def.name.val <++> colon <+> softline <+> pretty def.ty.val <+> hardline <+>
    pretty def.name.val <++> equals <+> softline <+> pretty def.tm.val

export
Pretty (Block n) where
  pretty []           = neutral
  pretty ([] :< def)  = pretty def
  pretty (blk :< def) = pretty blk <+> hardline <+> hardline <+> pretty def