||| 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    : String -> Syntax
  -- Sorts
  Sort   : Sort -> Syntax
  -- Dependent Products
  Pi     : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
  Lambda : WithBounds String -> WithBounds Syntax -> Syntax
  App    : WithBounds Syntax -> WithBounds Syntax -> Syntax
  -- Dependent Sums
  Sigma  : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
  Pair   : WithBounds Syntax -> WithBounds Syntax -> Syntax
  Fst    : WithBounds Syntax -> Syntax
  Snd    : WithBounds Syntax -> Syntax
  -- True
  Top    : Syntax
  Point  : Syntax
  -- False
  Bottom : Syntax
  Absurd : WithBounds Syntax -> WithBounds Syntax -> Syntax
  -- Equality
  Equal  : WithBounds Syntax -> WithBounds Syntax -> Syntax
  Refl   : WithBounds Syntax -> Syntax
  Transp : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
  Cast   : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
  CastId : WithBounds Syntax -> Syntax

public export
record Definition where
  constructor MkDefinition
  name   : WithBounds String
  ty     : WithBounds Syntax
  tm     : WithBounds Syntax

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

prettyPrec : Prec -> Syntax -> Doc ann
prettyPrecBounds : Prec -> WithBounds Syntax -> 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 >= App) $
  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 val _ _) = prettyPrec d val

export
Pretty Syntax where
  prettyPrec = Syntax.prettyPrec

export
Pretty Definition 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