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

import Obs.Pretty
import Obs.Universe

import Text.Bounded

%default total

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

data Syntax : Type

public export
record DeclForm where
  constructor MkDecl
  var : WithBounds String
  type : WithBounds Syntax

public export
record LambdaForm where
  constructor MkLambda
  var : WithBounds String
  body : WithBounds Syntax

public export
data Syntax : Type where
  Var : (var : String) -> Syntax
  -- Universes
  Universe : (s : Universe) -> Syntax
  -- Dependent Products
  Pi : (domain : DeclForm) -> (codomain : WithBounds Syntax) -> Syntax
  Lambda : (body : LambdaForm) -> Syntax
  App : (fun, arg : WithBounds Syntax) -> Syntax
  -- Dependent Sums
  Sigma : (index : DeclForm) -> (element : WithBounds Syntax) -> Syntax
  Pair : (first, second : WithBounds Syntax) -> Syntax
  First : (arg : WithBounds Syntax) -> Syntax
  Second : (arg : WithBounds Syntax) -> Syntax
  -- Booleans
  Bool : Syntax
  True : Syntax
  False : Syntax
  If : (returnType : LambdaForm) -> (discriminant, true, false : WithBounds Syntax) -> Syntax
  -- True
  Top : Syntax
  Point : Syntax
  -- False
  Bottom : Syntax
  Absurd : (contradiction : WithBounds Syntax) -> Syntax
  -- Equality
  Equal : (left, right : WithBounds Syntax) -> Syntax
  Refl : (value : WithBounds Syntax) -> Syntax
  Transp : (indexedType, oldIndex, value, newIndex, equality : WithBounds Syntax) -> Syntax
  Cast : (oldType, newType, equality, value : WithBounds Syntax) -> Syntax
  CastId : (value : WithBounds Syntax) -> Syntax

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

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

prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann

prettyPrecDecl : DeclForm -> Doc ann
prettyPrecDecl (MkDecl var type) = prettyDecl (Just var.val) (prettyPrecBounds Open type)

prettyPrecLambda : Prec -> LambdaForm -> Doc ann
prettyPrecLambda d (MkLambda var body) = prettyLambda d var.val (prettyPrecBounds Open body)

prettyPrec : Prec -> Syntax -> Doc ann
prettyPrec d (Var {var}) = pretty var
prettyPrec d (Universe {s}) = prettyPrec d s
prettyPrec d (Pi {domain, codomain}) =
  prettyDeclForm d [prettyPrecDecl domain] "->" (prettyPrecBounds Open codomain)
prettyPrec d (Lambda {body}) = prettyPrecLambda d body
prettyPrec d (App {fun, arg}) = prettyApp d (prettyPrecBounds Open fun) [prettyPrecBounds App arg]
prettyPrec d (Sigma {index, element}) =
  prettyDeclForm d [prettyPrecDecl index] "**" (prettyPrecBounds Open element)
prettyPrec d (Pair {first, second}) =
  prettyPair (prettyPrecBounds Open first) (prettyPrecBounds Open second)
prettyPrec d (First {arg}) = prettyApp d (pretty "fst") [prettyPrecBounds App arg]
prettyPrec d (Second {arg}) = prettyApp d (pretty "snd") [prettyPrecBounds App arg]
prettyPrec d Bool = pretty "Bool"
prettyPrec d True = pretty "True"
prettyPrec d False = pretty "False"
prettyPrec d (If {returnType, discriminant, true, false}) =
  prettyApp d (pretty "if") $
  [ prettyPrecLambda App returnType
  , prettyPrecBounds App discriminant
  , prettyPrecBounds App true
  , prettyPrecBounds App false
  ]
prettyPrec d Top = pretty "()"
prettyPrec d Point = pretty "tt"
prettyPrec d Bottom = pretty "Void"
prettyPrec d (Absurd {contradiction}) =
  prettyApp d (pretty "absurd") [prettyPrecBounds App contradiction]
prettyPrec d (Equal {left, right}) =
  prettyEqual d (prettyPrecBounds Equal left) (prettyPrecBounds Equal right)
prettyPrec d (Refl {value}) = prettyApp d (pretty "refl") [prettyPrecBounds App value]
prettyPrec d (Transp {indexedType, oldIndex, value, newIndex, equality}) =
  prettyApp d (pretty "transp") $
  [ prettyPrecBounds App indexedType
  , prettyPrecBounds App oldIndex
  , prettyPrecBounds App value
  , prettyPrecBounds App newIndex
  , prettyPrecBounds App equality
  ]
prettyPrec d (Cast {oldType, newType, equality, value}) =
  prettyApp d (pretty "cast") $
  [ prettyPrecBounds App oldType
  , prettyPrecBounds App newType
  , prettyPrecBounds App equality
  , prettyPrecBounds App value
  ]
prettyPrec d (CastId {value}) = prettyApp d (pretty "castRefl") [prettyPrecBounds App value]

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