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

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

%default total

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

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

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

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

export
Pretty Syntax where
  prettyPrec d (Var x str) = pretty str
  prettyPrec d (Sort x s)  = prettyPrec d s
  prettyPrec d (Top x)     = pretty "()"
  prettyPrec d (Point x)   = pretty "_"

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