114 lines
3.2 KiB
Idris
114 lines
3.2 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 : Type -> Nat -> Nat -> Nat -> Type
|
|
TSubst q d = Subst (\n => Elim q d n)
|
|
|
|
||| first argument `d` is dimension scope size, second `n` is term scope size
|
|
public export
|
|
data Term : (q : Type) -> (d, n : Nat) -> Type where
|
|
||| type of types
|
|
TYPE : (l : Universe) -> Term q d n
|
|
|
|
||| function type
|
|
Pi : (qty : q) -> (x : Name) ->
|
|
(arg : Term q d n) -> (res : ScopeTerm q d n) -> Term q d n
|
|
||| function term
|
|
Lam : (x : Name) -> (body : ScopeTerm q d n) -> Term q d n
|
|
|
|
||| elimination
|
|
E : (e : Elim q d n) -> Term q d n
|
|
|
|
||| term closure/suspended substitution
|
|
CloT : (tm : Term q d from) -> (th : Lazy (TSubst q d from to)) ->
|
|
Term q d to
|
|
||| dimension closure/suspended substitution
|
|
DCloT : (tm : Term q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
|
|
Term q dto n
|
|
|
|
||| first argument `d` is dimension scope size, second `n` is term scope size
|
|
public export
|
|
data Elim : (q : Type) -> (d, n : Nat) -> Type where
|
|
||| free variable
|
|
F : (x : Name) -> Elim q d n
|
|
||| bound variable
|
|
B : (i : Var n) -> Elim q d n
|
|
|
|
||| term application
|
|
(:@) : (fun : Elim q d n) -> (arg : Term q d n) -> Elim q d n
|
|
|
|
||| type-annotated term
|
|
(:#) : (tm, ty : Term q d n) -> Elim q d n
|
|
|
|
||| term closure/suspended substitution
|
|
CloE : (el : Elim q d from) -> (th : Lazy (TSubst q d from to)) ->
|
|
Elim q d to
|
|
||| dimension closure/suspended substitution
|
|
DCloE : (el : Elim q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
|
|
Elim q dto n
|
|
|
|
||| a scope with one more bound variable
|
|
public export
|
|
data ScopeTerm : (q : Type) -> (d, n : Nat) -> Type where
|
|
||| variable is used
|
|
TUsed : (body : Term q d (S n)) -> ScopeTerm q d n
|
|
||| variable is unused
|
|
TUnused : (body : Term q d n) -> ScopeTerm q d n
|
|
|
|
||| a scope with one more bound dimension variable
|
|
public export
|
|
data DScopeTerm : (q : Type) -> (d, n : Nat) -> Type where
|
|
||| variable is used
|
|
DUsed : (body : Term q (S d) n) -> DScopeTerm q d n
|
|
||| variable is unused
|
|
DUnused : (body : Term q d n) -> DScopeTerm q d n
|
|
|
|
%name Term s, t, r
|
|
%name Elim e, f
|
|
%name ScopeTerm body
|
|
%name DScopeTerm body
|
|
|
|
public export %inline
|
|
Arr : (qty : q) -> (arg, res : Term q d n) -> Term q 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 q 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 q 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 q d n
|
|
BVT i = E $ BV i
|