109 lines
2.0 KiB
Idris
109 lines
2.0 KiB
Idris
module Quox.Typing
|
|
|
|
import public Quox.Syntax
|
|
import public Quox.Context
|
|
import public Quox.Definition
|
|
|
|
import Data.Nat
|
|
import public Data.SortedMap
|
|
import Control.Monad.Reader
|
|
import Control.Monad.State
|
|
import Generics.Derive
|
|
|
|
%hide TT.Name
|
|
%default total
|
|
%language ElabReflection
|
|
|
|
%default total
|
|
|
|
|
|
public export
|
|
data DContext : Nat -> Type where
|
|
DNil : DContext 0
|
|
DBind : DContext d -> DContext (S d)
|
|
DEq : Dim d -> Dim d -> DContext d -> DContext d
|
|
|
|
public export
|
|
TContext : Nat -> Nat -> Type
|
|
TContext d = Context (Term d)
|
|
|
|
public export
|
|
QContext : Nat -> Type
|
|
QContext = Context' Qty
|
|
|
|
public export
|
|
QOutput : Nat -> Type
|
|
QOutput = QContext
|
|
|
|
|
|
public export
|
|
record TyContext (d, n : Nat) where
|
|
constructor MkTyContext
|
|
dctx : DContext d
|
|
tctx : TContext d n
|
|
qctx : QContext n
|
|
|
|
%name TyContext ctx
|
|
|
|
|
|
namespace TContext
|
|
export
|
|
pushD : TContext d n -> TContext (S d) n
|
|
pushD tel = map (/// shift 1) tel
|
|
|
|
|
|
namespace TyContext
|
|
export
|
|
extendTy : Term d n -> Qty -> TyContext d n -> TyContext d (S n)
|
|
extendTy s rho = {tctx $= (:< s), qctx $= (:< rho)}
|
|
|
|
export
|
|
extendDim : TyContext d n -> TyContext (S d) n
|
|
extendDim = {dctx $= DBind, tctx $= pushD}
|
|
|
|
export
|
|
eqDim : Dim d -> Dim d -> TyContext d n -> TyContext d n
|
|
eqDim p q = {dctx $= DEq p q}
|
|
|
|
|
|
namespace QOutput
|
|
export
|
|
(+) : QOutput n -> QOutput n -> QOutput n
|
|
(+) = zipWith (+)
|
|
|
|
export
|
|
(*) : Qty -> QOutput n -> QOutput n
|
|
(*) pi = map (pi *)
|
|
|
|
export
|
|
zero : {n : Nat} -> QOutput n
|
|
zero = pure Zero
|
|
|
|
|
|
public export
|
|
CheckResult : Nat -> Type
|
|
CheckResult = QOutput
|
|
|
|
public export
|
|
record InferResult d n where
|
|
constructor InfRes
|
|
type : Term d n
|
|
qout : QOutput n
|
|
|
|
|
|
public export
|
|
data EqMode = Equal | Sub
|
|
%runElab derive "EqMode" [Generic, Meta, Eq, Ord, DecEq, Show]
|
|
|
|
|
|
public export
|
|
data Error
|
|
= ExpectedTYPE (Term d n)
|
|
| ExpectedPi (Term d n)
|
|
| BadUniverse Universe Universe
|
|
|
|
| ClashT EqMode (Term d n) (Term d n)
|
|
| ClashU EqMode Universe Universe
|
|
| ClashQ Qty Qty
|
|
| NotInScope Name
|