quox/lib/Quox/Syntax/Term/Base.idr
2022-05-25 16:03:23 +02:00

110 lines
3 KiB
Idris

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