quox/lib/Quox/Typing.idr

201 lines
4.7 KiB
Idris
Raw Normal View History

2021-12-23 13:05:50 -05:00
module Quox.Typing
import public Quox.Syntax
import public Quox.Context
2022-08-22 04:17:08 -04:00
import public Quox.Definition
2021-12-23 13:05:50 -05:00
import Data.Nat
2022-04-23 18:21:30 -04:00
import public Data.SortedMap
2023-01-08 14:44:25 -05:00
import Control.Monad.Either
2021-12-23 13:05:50 -05:00
import Control.Monad.Reader
import Control.Monad.State
import Generics.Derive
%hide TT.Name
2023-02-02 08:58:36 -05:00
%hide SOP.from
%hide SOP.to
%default total
%language ElabReflection
2021-12-23 13:05:50 -05:00
%default total
2022-02-26 19:28:19 -05:00
2021-12-23 13:05:50 -05:00
public export
2023-01-08 14:44:25 -05:00
TContext : Type -> Nat -> Nat -> Type
TContext q d = Context (Term q d)
2021-12-23 13:05:50 -05:00
public export
2023-01-08 14:44:25 -05:00
QOutput : Type -> Nat -> Type
2023-02-14 15:14:47 -05:00
QOutput = Context'
2021-12-23 13:05:50 -05:00
public export
2023-01-08 14:44:25 -05:00
record TyContext q d n where
2021-12-23 13:05:50 -05:00
constructor MkTyContext
2023-02-14 15:29:04 -05:00
dctx : DimEq d
2023-01-08 14:44:25 -05:00
tctx : TContext q d n
2021-12-23 13:05:50 -05:00
%name TyContext ctx
namespace TContext
2023-02-14 15:14:47 -05:00
export %inline
2023-01-08 14:44:25 -05:00
pushD : TContext q d n -> TContext q (S d) n
2021-12-23 13:05:50 -05:00
pushD tel = map (/// shift 1) tel
namespace TyContext
public export %inline
empty : {d : Nat} -> TyContext q d 0
empty = MkTyContext {dctx = new, tctx = [<]}
2023-02-14 15:14:47 -05:00
export %inline
extendTyN : Telescope (Term q d) from to ->
2023-01-26 13:54:46 -05:00
TyContext q d from -> TyContext q d to
2023-02-14 15:14:47 -05:00
extendTyN ss = {tctx $= (. ss)}
2023-01-26 13:54:46 -05:00
2023-02-14 15:14:47 -05:00
export %inline
extendTy : Term q d n -> TyContext q d n -> TyContext q d (S n)
extendTy s = extendTyN [< s]
2021-12-23 13:05:50 -05:00
2023-02-14 15:14:47 -05:00
export %inline
2023-01-08 14:44:25 -05:00
extendDim : TyContext q d n -> TyContext q (S d) n
2023-02-14 15:29:04 -05:00
extendDim = {dctx $= (:<? Nothing), tctx $= pushD}
2021-12-23 13:05:50 -05:00
2023-02-14 15:14:47 -05:00
export %inline
2023-01-08 14:44:25 -05:00
eqDim : Dim d -> Dim d -> TyContext q d n -> TyContext q d n
2023-02-14 15:29:04 -05:00
eqDim p q = {dctx $= set p q}
2021-12-23 13:05:50 -05:00
namespace QOutput
2023-01-08 14:44:25 -05:00
parameters {auto _ : IsQty q}
2023-02-14 15:14:47 -05:00
export %inline
2023-01-08 14:44:25 -05:00
(+) : QOutput q n -> QOutput q n -> QOutput q n
(+) = zipWith (+)
2021-12-23 13:05:50 -05:00
2023-02-14 15:14:47 -05:00
export %inline
2023-01-08 14:44:25 -05:00
(*) : q -> QOutput q n -> QOutput q n
(*) pi = map (pi *)
2021-12-23 13:05:50 -05:00
2023-02-14 15:14:47 -05:00
export %inline
zeroFor : TyContext q _ n -> QOutput q n
2023-01-26 13:54:46 -05:00
zeroFor ctx = zero <$ ctx.tctx
2022-04-23 18:21:30 -04:00
public export
2023-01-08 14:44:25 -05:00
CheckResult : Type -> Nat -> Type
2022-04-27 15:58:09 -04:00
CheckResult = QOutput
2022-04-23 18:21:30 -04:00
public export
2023-01-08 14:44:25 -05:00
record InferResult q d n where
2022-04-23 18:21:30 -04:00
constructor InfRes
2023-01-08 14:44:25 -05:00
type : Term q d n
qout : QOutput q n
2022-04-23 18:21:30 -04:00
public export
2023-02-12 15:30:08 -05:00
data EqMode = Equal | Sub | Super
%runElab derive "EqMode" [Generic, Meta, Eq, Ord, DecEq, Show]
2022-04-23 18:21:30 -04:00
public export
2023-01-08 14:44:25 -05:00
data Error q
= ExpectedTYPE (Term q d n)
| ExpectedPi (Term q d n)
2023-01-26 13:54:46 -05:00
| ExpectedSig (Term q d n)
2023-01-20 20:34:28 -05:00
| ExpectedEq (Term q d n)
| BadUniverse Universe Universe
2023-02-10 15:40:44 -05:00
-- first arg of ClashT is the type
| ClashT EqMode (Term q d n) (Term q d n) (Term q d n)
| ClashE EqMode (Elim q d n) (Elim q d n)
2023-01-08 14:44:25 -05:00
| ClashU EqMode Universe Universe
| ClashQ q q
2023-01-20 20:34:28 -05:00
| ClashD (Dim d) (Dim d)
| NotInScope Name
2023-01-08 14:44:25 -05:00
2023-02-10 15:40:44 -05:00
| NotType (Term q d n)
| WrongType (Term q d n) (Term q d n) (Term q d n)
2023-01-08 14:44:25 -05:00
public export
0 HasErr : Type -> (Type -> Type) -> Type
HasErr q = MonadError (Error q)
2023-01-26 13:54:46 -05:00
export %inline
ucmp : EqMode -> Universe -> Universe -> Bool
ucmp Equal = (==)
2023-02-12 15:30:08 -05:00
ucmp Sub = (<=)
ucmp Super = (>=)
export %inline
flip : EqMode -> EqMode
flip Equal = Equal
flip Sub = Super
flip Super = Sub
2023-01-26 13:54:46 -05:00
parameters {auto _ : HasErr q m}
export %inline
expect : Eq a => (a -> a -> Error q) -> (a -> a -> Bool) -> a -> a -> m ()
expect err cmp x y = unless (x `cmp` y) $ throwError $ err x y
export %inline
expectEqualQ : Eq q => q -> q -> m ()
expectEqualQ = expect ClashQ (==)
export %inline
expectCompatQ : IsQty q => q -> q -> m ()
expectCompatQ = expect ClashQ $ \pi, rh => isYes $ pi `compat` rh
export %inline
expectModeU : EqMode -> Universe -> Universe -> m ()
expectModeU mode = expect (ClashU mode) $ ucmp mode
export %inline
expectEqualD : Dim d -> Dim d -> m ()
expectEqualD = expect ClashD (==)
2023-02-10 15:40:44 -05:00
export
lookupFree' : HasErr q m => Definitions' q g -> Name -> m (Definition' q g)
lookupFree' defs x =
case lookup x defs of
Just d => pure d
Nothing => throwError $ NotInScope x
2023-02-12 15:30:08 -05:00
public export
2023-02-10 15:40:44 -05:00
substCasePairRet : Term q d n -> ScopeTerm q d n -> Term q d (2 + n)
substCasePairRet dty retty =
let arg = Pair (BVT 0) (BVT 1) :# (dty // fromNat 2) in
retty.term // (arg ::: shift 2)
2023-02-11 12:15:50 -05:00
parameters {auto _ : HasErr q m} (defs : Definitions' q _)
export covering %inline
expectTYPE : Term q d n -> m Universe
expectTYPE s =
case fst $ whnfD defs s of
TYPE l => pure l
_ => throwError $ ExpectedTYPE s
export covering %inline
expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n)
expectPi s =
case fst $ whnfD defs s of
Pi {qty, arg, res, _} => pure (qty, arg, res)
_ => throwError $ ExpectedPi s
export covering %inline
expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n)
expectSig s =
case fst $ whnfD defs s of
Sig {fst, snd, _} => pure (fst, snd)
_ => throwError $ ExpectedSig s
export covering %inline
expectEq : Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n)
expectEq s =
case fst $ whnfD defs s of
Eq {ty, l, r, _} => pure (ty, l, r)
_ => throwError $ ExpectedEq s