beginnings of typechecker, maybe

src/Quox/Typecheck.idr

@@ -0,0 +1,152 @@
+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)}