rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

remove old typecheck stuff

Browse source
This commit is contained in:
rhiannon morris 2021-12-23 15:53:40 +01:00
parent e833322ebe
commit c75332be44
1 changed files with 0 additions and 152 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

152
src/Quox/Typecheck.idr
View file

@ -1,152 +0,0 @@
module Quox.Typecheck
import Quox.Syntax
import Quox.Error
import Quox.Context
import Data.Nat
import Control.Monad.Reader
import Control.Monad.State
%default total
public export
DContext : Nat -> Type
DContext = Context Dim
public export
TContext : Nat -> Nat -> Type
TContext d = Context (Term d)
public export
QContext : Nat -> Type
QContext = Triangle' Qty
public export
QOutput : Nat -> Type
QOutput = Context' Qty
namespace TContext
export
pushD : TContext d n -> TContext (S d) n
pushD tel = map (/// shift 1) tel
namespace Zero
public export
data IsZero : QOutput n -> Type where
LinZ : IsZero [<]
SnocZ : IsZero qctx -> IsZero (qctx :< Zero)
export
isZeroIrrel : {qctx : _} -> (0 _ : IsZero qctx) -> IsZero qctx
isZeroIrrel {qctx = [<]} LinZ = LinZ
isZeroIrrel {qctx = _ :< _} (SnocZ x) = SnocZ $ isZeroIrrel x
export
zero : Context _ n -> Subset (QOutput n) IsZero
zero [<] = Element [<] LinZ
zero (ctx :< _) = let zeroN = zero ctx in
Element (zeroN.fst :< Zero) (SnocZ zeroN.snd)
namespace Only
public export
data IsOnly : QOutput n -> Var n -> Type where
Here : IsZero qctx -> IsOnly (qctx :< One) VZ
There : IsOnly qctx i -> IsOnly (qctx :< Zero) (VS i)
export
isOnlyIrrel : {qctx, i : _} -> (0 _ : IsOnly qctx i) -> IsOnly qctx i
isOnlyIrrel {i = VZ} (Here z) = Here $ isZeroIrrel z
isOnlyIrrel {i = (VS i)} (There o) = There $ isOnlyIrrel o
export
only : Context _ n -> (i : Var n) ->
Subset (QOutput n) (\qctx => IsOnly qctx i)
only (ctx :< _) VZ =
let zeroN = zero ctx in
Element (zeroN.fst :< One) (Here zeroN.snd)
only (ctx :< _) (VS i) =
let onlyN = only ctx i in
Element (onlyN.fst :< Zero) (There onlyN.snd)
public export
data LT : Universe -> Universe -> Type where
Fin : k `LT` l -> U k `LT` U l
Any : U _ `LT` UAny
namespace Lookup
public export
data IsLookup :
(tctx : TContext d n) ->
(i : Var n) ->
(ty : Term d from) ->
(by : Shift from n) -> Type
where
Here : IsLookup {tctx=(tctx :< ty), i=VZ, ty, by=(SS SZ)}
There : IsLookup {tctx, i, ty, by} ->
IsLookup {tctx=(tctx :< ty'), i=(VS i), ty, by=(SS by)}
public export
record Lookup {0 d, n : Nat} (0 tctx : TContext d n) (0 i : Var n) where
constructor MkLookup
qtys : QOutput n
type : Term d from
by : Shift from n
0 only : IsOnly qtys i
0 look : IsLookup tctx i type by
export
lookup : (ctx : TContext d n) -> (i : Var n) -> Lookup tctx i
lookup (ctx :< x) VZ =
?lookup_rhs_3
lookup (ctx :< x) (VS i) =
?lookup_rhs_4
mutual
public export
data HasTypeT :
(dctx : DContext d) ->
(tctx : TContext d n) ->
(qctx : QContext n) ->
(subj : Term d n) ->
(ty : Term d n) ->
(tmout, tyout : QOutput n) ->
Type
where
TYPE :
WfCtx {dctx, tctx, qctx} ->
k `LT` l ->
(0 _ : IsZero tmout) -> (0 _ : IsZero tyout) ->
HasTypeT {dctx, tctx, qctx, subj=(TYPE k), ty=(TYPE l), tmout, tyout}
public export
data HasTypeE :
(dctx : DContext d) ->
(tctx : TContext d n) ->
(qctx : QContext n) ->
(subj : Elim d n) ->
(ty : Term d n) ->
(tmout, tyout : QOutput n) ->
Type
where
public export
data WfCtx :
(dctx : DContext d) ->
(tctx : TContext d n) ->
(qctx : QContext n) ->
Type
where
NIL : WfCtx [<] [<] [<]
BIND :
WfCtx {dctx, tctx, qctx} ->
HasTypeT {dctx, tctx, qctx, subj=a, ty=(TYPE l), tmout, tyout} ->
WfCtx {dctx, tctx=(tctx :< a), qctx=(qctx :< tmout)}