module Quox.Syntax.Term.Base

import public Quox.Syntax.Var
import public Quox.Syntax.Shift
import public Quox.Syntax.Subst
import public Quox.Syntax.Universe
import public Quox.Syntax.Qty
import public Quox.Syntax.Dim
import public Quox.Name
-- import public Quox.OPE

import Quox.Pretty

import public Data.DPair
import Data.List
import Data.Maybe
import Data.Nat
import public Data.So
import Data.String
import Data.Vect

%default total


infixl 8 :#
infixl 9 :@
mutual
  public export
  TSubst : Nat -> Nat -> Nat -> Type
  TSubst d = Subst (\n => Elim d n)

  ||| first argument `d` is dimension scope size, second `n` is term scope size
  public export
  data Term : (d, n : Nat) -> Type where
    ||| type of types
    TYPE : (l : Universe) -> Term d n

    ||| function type
    Pi  : (qty : Qty) -> (x : Name) ->
          (arg : Term d n) -> (res : ScopeTerm d n) -> Term d n
    ||| function term
    Lam : (x : Name) -> (body : ScopeTerm d n) -> Term d n

    ||| elimination
    E : (e : Elim d n) -> Term d n

    ||| term closure/suspended substitution
    CloT  : (tm : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
    ||| dimension closure/suspended substitution
    DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n

  ||| first argument `d` is dimension scope size, second `n` is term scope size
  public export
  data Elim : (d, n : Nat) -> Type where
    ||| free variable
    F : (x : Name) -> Elim d n
    ||| bound variable
    B : (i : Var n) -> Elim d n

    ||| term application
    (:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n

    ||| type-annotated term
    (:#) : (tm, ty : Term d n) -> Elim d n

    ||| term closure/suspended substitution
    CloE  : (el : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
    ||| dimension closure/suspended substitution
    DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n

  ||| a scope with one more bound variable
  public export
  data ScopeTerm : (d, n : Nat) -> Type where
    ||| variable is used
    TUsed : (body : Term d (S n)) -> ScopeTerm d n
    ||| variable is unused
    TUnused : (body : Term d n) -> ScopeTerm d n

  ||| a scope with one more bound dimension variable
  public export
  data DScopeTerm : (d, n : Nat) -> Type where
    ||| variable is used
    DUsed : (body : Term (S d) n) -> DScopeTerm d n
    ||| variable is unused
    DUnused : (body : Term d n) -> DScopeTerm d n

%name Term s, t, r
%name Elim e, f
%name ScopeTerm body
%name DScopeTerm body

public export %inline
Arr : (qty : Qty) -> (arg, res : Term d n) -> Term d n
Arr {qty, arg, res} = Pi {qty, x = "_", arg, res = TUnused res}

||| same as `F` but as a term
public export %inline
FT : Name -> Term d n
FT = E . F

||| abbreviation for a bound variable like `BV 4` instead of
||| `B (VS (VS (VS (VS VZ))))`
public export %inline
BV : (i : Nat) -> (0 _ : LT i n) => Elim d n
BV i = B $ V i

||| same as `BV` but as a term
public export %inline
BVT : (i : Nat) -> (0 _ : LT i n) => Term d n
BVT i = E $ BV i