||| Abstract syntax for terms.
module Obs.Term

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

%default total

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

public export
data Term : Nat -> Type where
  Var    : WithBounds String -> Fin n -> Term n
  -- Sorts
  Sort   : Bounds -> Sort -> Term n
  -- Dependent Product
  Pi     : Bounds -> String -> Term n -> Term (S n) -> Term n
  Lambda : Bounds -> String -> Term (S n) -> Term n
  App    : Term n -> Term n -> Term n
  -- Dependent Sums
  Sigma  : Bounds -> String -> Term n -> Term (S n) -> Term n
  Pair   : Bounds -> Term n -> Term n -> Term n
  Fst    : Bounds -> Term n -> Term n
  Snd    : Bounds -> Term n -> Term n
  -- True
  Top    : Bounds -> Term n
  Point  : Bounds -> Term n
  -- False
  Bottom : Bounds -> Term n
  Absurd : Bounds -> Term n -> Term n -> Term n
  -- Equality
  Equal  : Bounds -> Term n -> Term n -> Term n
  Refl   : Bounds -> Term n -> Term n
  Transp : Bounds -> Term n -> Term n -> Term n -> Term n -> Term n -> Term n
  Cast   : Bounds -> Term n -> Term n -> Term n -> Term n
  CastId : Bounds -> Term n -> Term n

public export
record Definition (n : Nat) where
  constructor MkDefinition
  bounds : Bounds -- of the name
  name   : String
  ty     : Term n
  tm     : Term n

public export
data Block : Nat -> Type where
  Nil  : Block 0
  (:<) : Block n -> Definition n -> Block (S n)

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

export
fullBounds : Term n -> WithBounds (Term n)
fullBounds tm@(Var var i) = map (\_ => tm) var
fullBounds tm@(Sort x s) = MkBounded tm False x
fullBounds tm@(Pi x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
fullBounds tm@(Lambda x var t) = mergeBounds (fullBounds t) (MkBounded tm False x)
fullBounds tm@(App t u) = map (\_ => tm) (mergeBounds (fullBounds t) (fullBounds u))
fullBounds tm@(Sigma x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
fullBounds tm@(Pair x t u) = mergeBounds (mergeBounds (fullBounds t) (fullBounds u)) (MkBounded tm False x)
fullBounds tm@(Fst x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
fullBounds tm@(Snd x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
fullBounds tm@(Top x) = MkBounded tm False x
fullBounds tm@(Point x) = MkBounded tm False x
fullBounds tm@(Bottom x) = MkBounded tm False x
fullBounds tm@(Absurd x a t) = mergeBounds (mergeBounds (fullBounds a) (fullBounds t)) (MkBounded tm False x)
fullBounds tm@(Equal x t u) = mergeBounds (mergeBounds (fullBounds t) (fullBounds u)) (MkBounded tm False x)
fullBounds tm@(Refl x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
fullBounds tm@(Transp x t b u t' e) = mergeBounds (mergeBounds (mergeBounds (fullBounds t) (fullBounds b)) (mergeBounds (fullBounds u) (fullBounds t'))) (mergeBounds (fullBounds e) (MkBounded tm False x))
fullBounds tm@(Cast x b e t) = mergeBounds (mergeBounds (fullBounds b) (fullBounds e)) (mergeBounds (fullBounds t) (MkBounded tm False x))
fullBounds tm@(CastId x t) = mergeBounds (fullBounds t) (MkBounded tm False x)

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

export
Pretty (Term n) where
  prettyPrec d (Var var _) = pretty var.val
  prettyPrec d (Sort _ s) = prettyPrec d s
  prettyPrec d (Pi _ var a b) =
    parenthesise (d > Open) $
    group $
    parens (pretty var <++> colon <+> softline <+> prettyPrec Open a) <++>
    pretty "->" <+> softline <+>
    prettyPrec Open b
  prettyPrec d (Lambda _ var t) =
    parenthesise (d > Open) $
    group $
    backslash <+> pretty var <++>
    pretty "=>" <+> softline <+>
    prettyPrec Open t
  prettyPrec d (App t u) =
    parenthesise (d >= App) $
    group $
    fillSep [prettyPrec Open t, prettyPrec App u]
  prettyPrec d (Sigma _ var a b) =
    parenthesise (d >= App) $
    group $
    parens (pretty var <++> colon <+> softline <+> prettyPrec Open a) <++>
    pretty "**" <+> softline <+>
    prettyPrec Open b
  prettyPrec d (Pair _ t u) =
    angles $
    group $
    neutral <++> prettyPrec Open t <+> comma <+> softline <+> prettyPrec Open u <++> neutral
  prettyPrec d (Fst _ t) =
    parenthesise (d >= App) $
    group $
    fillSep [pretty "fst", prettyPrec App t]
  prettyPrec d (Snd _ t) =
    parenthesise (d >= App) $
    group $
    fillSep [pretty "snd", prettyPrec App t]
  prettyPrec d (Top _) = pretty "()"
  prettyPrec d (Point _) = pretty "tt"
  prettyPrec d (Bottom _) = pretty "Void"
  prettyPrec d (Absurd _ a t) =
    parenthesise (d > Open) $
    group $
    fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
  prettyPrec d (Equal _ t u) =
    parenthesise (d >= Equal) $
    group $
    prettyPrec Equal t <++> pretty "~" <+> softline <+> prettyPrec Equal u
  prettyPrec d (Refl _ t) =
    parenthesise (d >= App) $
    group $
    fillSep [pretty "refl", prettyPrec App t]
  prettyPrec d (Transp _ t b u t' e) =
    parenthesise (d >= App) $
    group $
    fillSep $
    [ pretty "transp"
    , prettyPrec App t
    , prettyPrec App b
    , prettyPrec App u
    , prettyPrec App t'
    , prettyPrec App e
    ]
  prettyPrec d (Cast _ b e t) =
    parenthesise (d >= App) $
    group $
    fillSep [pretty "cast", prettyPrec App b, prettyPrec App e, prettyPrec App t]
  prettyPrec d (CastId _ t) =
    parenthesise (d >= App) $
    group $
    fillSep [pretty "castRefl", prettyPrec App t]

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

export
Pretty (Block n) where
  pretty []           = neutral
  pretty ([] :< def)  = pretty def
  pretty (blk :< def) = pretty blk <+> hardline <+> hardline <+> pretty def