||| Raw syntax for terms. This is before eliminating names.
module Obs.Syntax

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

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

public export
data Syntax : Type where
  Var  : Bounds -> String -> Syntax
  -- Sorts
  Sort : Bounds -> Sort -> Syntax

public export
record Definition where
  constructor MkDefinition
  bounds : Bounds -- of the name
  name   : String
  ty     : Syntax
  tm     : Syntax

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

fullBounds : Syntax -> Bounds
fullBounds (Var x str) = x
fullBounds (Sort x s)  = x

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

export
Pretty Syntax where
  prettyPrec d (Var x str) = pretty str
  prettyPrec d (Sort x s)  = prettyPrec d s

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