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

import Obs.Universe

import Text.Bounded
import Text.PrettyPrint.Prettyprinter

%default total

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

public export
data Syntax : Type where
  Var : String -> Syntax
  -- Universes
  Universe : Universe -> 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
  -- Booleans
  Bool : Syntax
  True : Syntax
  False : Syntax
  If : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
  -- True
  Top : Syntax
  Point : Syntax
  -- False
  Bottom : Syntax
  Absurd : 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 -> 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 (Universe s) = prettyPrec d s
prettyPrec d (Pi var a b) =
  parenthesise (d > Open) $
  group $
  parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++>
  pretty "->" <+> line <+>
  align (prettyPrecBounds Open b)
prettyPrec d (Lambda var t) =
  parenthesise (d > Open) $
  group $
  backslash <+> pretty var.val <++>
  pretty "=>" <+> line <+>
  align (prettyPrecBounds Open t)
prettyPrec d (App t u) =
  parenthesise (d >= App) $
  group $
  vsep [prettyPrecBounds Open t, prettyPrecBounds App u]
prettyPrec d (Sigma var a b) =
  parenthesise (d >= App) $
  group $
  parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++>
  pretty "**" <+> line <+>
  align (prettyPrecBounds Open b)
prettyPrec d (Pair t u) =
  angles $
  group $
  neutral <++> prettyPrecBounds Open t <+> comma <+> line <+> prettyPrecBounds Open u <++> neutral
prettyPrec d (Fst t) =
  parenthesise (d >= App) $
  group $
  vsep [pretty "fst", prettyPrecBounds App t]
prettyPrec d (Snd t) =
  parenthesise (d >= App) $
  group $
  vsep [pretty "snd", prettyPrecBounds App t]
prettyPrec d Bool = pretty "Bool"
prettyPrec d True = pretty "True"
prettyPrec d False = pretty "False"
prettyPrec d (If var a t f g) =
  parenthesise (d >= App) $
  group $
  vsep $
  [ pretty "if"
  , parens $
    group $
    backslash <+> pretty var.val <++>
    pretty "=>" <+> line <+>
    align (prettyPrecBounds Open a)
  , prettyPrecBounds App t
  , prettyPrecBounds App f
  , prettyPrecBounds App g
  ]
prettyPrec d Top = pretty "()"
prettyPrec d Point = pretty "tt"
prettyPrec d Bottom = pretty "Void"
prettyPrec d (Absurd t) =
  parenthesise (d >= App) $
  group $
  vsep [pretty "absurd", prettyPrecBounds App t]
prettyPrec d (Equal t u) =
  parenthesise (d >= Equal) $
  group $
  prettyPrecBounds Equal t <++> pretty "~" <+> line <+> prettyPrecBounds Equal u
prettyPrec d (Refl t) =
  parenthesise (d >= App) $
  group $
  vsep [pretty "refl", prettyPrecBounds App t]
prettyPrec d (Transp a t u t' e) =
  parenthesise (d >= App) $
  group $
  vsep $
  [ pretty "transp"
  , prettyPrecBounds App a
  , prettyPrecBounds App t
  , prettyPrecBounds App u
  , prettyPrecBounds App t'
  , prettyPrecBounds App e
  ]
prettyPrec d (Cast a b e t) =
  parenthesise (d >= App) $
  group $
  vsep $
  [ pretty "cast"
  , prettyPrecBounds App a
  , prettyPrecBounds App b
  , prettyPrecBounds App e
  , prettyPrecBounds App t
  ]
prettyPrec d (CastId t) =
  parenthesise (d >= App) $
  group $
  vsep [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