||| 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    : Bounds -> Fin n -> Term n
  -- Sorts
  Sort   : Bounds -> Sort -> Term n
  -- True
  Top    : Bounds -> Term n
  Point  : Bounds -> Term n
  -- False
  Bottom : Bounds -> Term n
  Absurd : Bounds -> Term n -> Term n -> Term n

public export
record Definition (n : Nat) where
  constructor MkDefinition
  bounds : Bounds -- of the name
  name   : String
  ty     : Term n
  tm     : Term n

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

-- Operations ------------------------------------------------------------------

export
fullBounds : Term n -> WithBounds (Term n)
fullBounds tm@(Var x i)      = MkBounded tm False x
fullBounds tm@(Sort x s)     = MkBounded tm False x
fullBounds tm@(Top x)        = MkBounded tm False x
fullBounds tm@(Point x)      = MkBounded tm False x
fullBounds tm@(Bottom x)     = MkBounded tm False x
fullBounds tm@(Absurd x a t) = mergeBounds (mergeBounds (fullBounds a) (fullBounds t)) (MkBounded tm False x)

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

export
Pretty (Term n) where
  prettyPrec d (Var x i) = pretty "$\{show i}"
  prettyPrec d (Sort x s) = prettyPrec d s
  prettyPrec d (Top x) = pretty "()"
  prettyPrec d (Point x) = pretty "_"
  prettyPrec d (Bottom x) = pretty "Void"
  prettyPrec d (Absurd x a t) =
    parenthesise (d > Open) $
    group $
    fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]

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

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