35 lines
797 B
Idris
35 lines
797 B
Idris
|
module Quox.Syntax.Term.TyConKind
|
||
|
|
|
||
|
|
import Decidable.Equality
|
||
|
|
import Derive.Prelude
|
||
|
|
import Generics.Derive
|
||
|
|
|
||
|
|
%language ElabReflection
|
||
|
|
%default total
|
||
|
|
|
||
|
|
|
||
|
|
public export
|
||
|
|
data TyConKind = KTYPE | KPi | KSig | KEnum | KEq | KNat | KBOX
|
||
|
|
%name TyConKind k
|
||
|
|
%runElab derive "TyConKind" [Eq.Eq, Ord.Ord, Show.Show, Generic, Meta, DecEq]
|
||
|
|
|
||
|
|
||| a list of all `TyConKind`s
|
||
|
|
public export %inline
|
||
|
|
allKinds : List TyConKind
|
||
|
|
allKinds = %runElab do
|
||
|
|
-- as a script so it stays up to date if there are more tycon kinds
|
||
|
|
cs <- getCons $ fst !(lookupName "TyConKind")
|
||
|
|
traverse (check . var) cs
|
||
|
|
|
||
|
|
|
||
|
|
||| in `type-case`, how many variables are bound in this branch
|
||
|
|
public export %inline
|
||
|
|
arity : TyConKind -> Nat
|
||
|
|
arity KTYPE = 0
|
||
|
|
arity KPi = 2
|
||
|
|
arity KSig = 2
|
||
|
|
arity KEnum = 0
|
||
|
|
arity KEq = 5
|
||
|
|
arity KNat = 0
|
||
|
|
arity KBOX = 1
|