From 38260d3838fe9dd1148656dc83851b0ae3b64e7e Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 8 Apr 2022 03:47:11 +0200
Subject: [PATCH] producing a proof in TC is not worth it

---
 src/Quox/Context.idr     |   2 +-
 src/Quox/Typechecker.idr | 168 ---------------------------------
 src/Quox/Typing.idr      | 199 +--------------------------------------
 3 files changed, 3 insertions(+), 366 deletions(-)
 delete mode 100644 src/Quox/Typechecker.idr

diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index ca2891f..7689de2 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -159,7 +159,7 @@ namespace Nat
     LTESuccR : m `LTE'` n -> m `LTE'` S n
   %builtin Natural LTE'
 
-  export
+  export %hint
   lteZero' : {n : Nat} -> 0 `LTE'` n
   lteZero' {n = 0}   = LTERefl
   lteZero' {n = S n} = LTESuccR lteZero'
diff --git a/src/Quox/Typechecker.idr b/src/Quox/Typechecker.idr
deleted file mode 100644
index ec73f8f..0000000
--- a/src/Quox/Typechecker.idr
+++ /dev/null
@@ -1,168 +0,0 @@
-module Quox.Typechecker
-
-import public Quox.Syntax
-import public Quox.Typing
-import Quox.Error
-
-import Data.Nat
-import Data.SortedMap
-import Control.Monad.Reader
-import Control.Monad.State
-import Syntax.WithProof
-
-%default total
-
-
-public export
-data Error : Type where
-  ExpectedType : (subj, ty : Term d n) -> Error
-  UniverseInconsistency : (lo, hi : Universe) -> Error
-  GlobalNotInScope : Name -> Error
-
-public export
-record CheckResult
-  {0 d, n : Nat}
-  (0 ctx : WfContext d n)
-  (0 subj, ty : Term d n)
-where
-  constructor MkCheckResult
-  tmout, tyout : QOutput n
-  hasType : HasTypeT {ctx = ctx.ctx, subj, ty, tmout, tyout}
-
-
-public export
-record InferResult
-  {0 d, n : Nat}
-  (0 ctx : WfContext d n)
-  (0 subj : Elim d n)
-where
-  constructor MkInferResult
-  tmout, tyout : QOutput n
-  ty : Term d n
-  hasType : HasTypeE {ctx = ctx.ctx, subj, ty, tmout, tyout}
-
-
-public export
-zeroCtx : Globals -> TyContext 0 0
-zeroCtx globals = MkTyContext {globals, dctx = DNil, tctx = [<], qctx = [<]}
-
-public export
-zeroWfCtx : Globals -> WfContext 0 0
-zeroWfCtx globals = MkWfContext (zeroCtx globals) NIL
-
-public export
-Check0 : (globals : Globals) -> (subj, ty : Term 0 0) -> Type
-Check0 globals subj ty =
-  HasTypeT {ctx = zeroCtx globals, subj, ty, tmout = [<], tyout = [<]}
-
-public export
-record Infer0 (globals : Globals) (subj : Elim 0 0) where
-  constructor MkInfer0
-  ty : Term 0 0
-  hasType : HasTypeE {ctx = zeroCtx globals, subj, ty, tmout = [<], tyout = [<]}
-
-
-export
-0 isTypeZeroTyout : HasTypeT {ty = TYPE _, tyout, _} -> IsZero tyout
-isTypeZeroTyout (TYPE  {zty, _}) = zty
-isTypeZeroTyout (Pi    {zty, _}) = zty
-isTypeZeroTyout (PushT {})   = ?isTypeZeroTyout_PushT
-
-
-parameters {auto _ : MonadThrow Error m} mutual
-  private
-  checkUniverse : (lo, hi : Universe) -> m (lo `LT` hi)
-  checkUniverse lo hi with (lo `isLT` hi)
-    _ | Yes lt = pure lt
-    _ | No  _  = throw $ UniverseInconsistency {lo, hi}
-
-  private
-  expectType : (subj, ty : Term d n) ->
-               m (l : Universe ** ty = TYPE l)
-  expectType _    (TYPE l) = pure (l ** Refl)
-  expectType subj ty       = throw $ ExpectedType {subj, ty}
-
-  private
-  checkType : (ctx : WfContext d n) ->
-              (l : Universe) -> (ty : Term d n) ->
-              m (CheckResult ctx (TYPE l) ty)
-  checkType (MkWfContext {ctx, wf}) l ty = do
-    (l' ** eq) <- expectType (TYPE l) ty; let Refl = eq
-    lt <- checkUniverse l l'
-    let Element _ zprf = zero ctx.qctx
-    pure $ MkCheckResult {hasType = TYPE {wf, lt, ztm = zprf, zty = zprf}, _}
-
-  private
-  checkPi : (ctx : WfContext d n) ->
-            (qtm, qty : Qty) ->
-            (x : Name) ->
-            (arg : Term d n) ->
-            (res : Term d (S n)) ->
-            (ty  : Term d n) ->
-            m (CheckResult ctx (Pi qtm qty x arg res) ty)
-  checkPi (MkWfContext {ctx, wf}) qtm qty x arg res ty = do
-    let whole = Pi qtm qty x arg res
-    (l' ** eq) <- expectType whole ty; let Refl = eq
-    ?checkPi_rhs
-
-
-  private
-  inferFree : (ctx : WfContext {}) -> (x : Name) -> m (InferResult ctx (F x))
-  inferFree (MkWfContext {ctx, wf}) x =
-    case @@ lookup x ctx.globals of
-      (Just g ** eq) =>
-        let Element _ zprf = zero ctx.tctx
-            hasType = F {wf, g, eq, ztm = zprf, zty = zprf}
-        in
-        pure $ MkInferResult {hasType, _}
-      _ => throw $ GlobalNotInScope x
-
-  private
-  inferBound : (ctx : WfContext _ n) -> (i : Var n) -> m (InferResult ctx (B i))
-  inferBound (MkWfContext {ctx, wf}) i =
-    pure $ MkInferResult {hasType = B {wf, look = lookup ctx i, eq = Refl}, _}
-
-  private
-  inferAnn : (ctx : WfContext d n) -> (tm, ty : Term d n) ->
-             m (InferResult ctx (tm :# ty))
-  inferAnn ctx tm ty = do
-    ignore $ check ctx ty (TYPE UAny)
-    MkCheckResult {hasType, _} <- check ctx tm ty
-    pure $ MkInferResult {hasType = Ann hasType, _}
-
-
-  export
-  check : (ctx : WfContext d n) -> (subj, ty : Term d n) ->
-          m (CheckResult ctx subj ty)
-  check ctx subj ty = case subj of
-    TYPE l               => checkType ctx l ty
-    Pi qtm qty x arg res => checkPi ctx qtm qty x arg res ty
-    Lam x body           => ?check_rhs_3
-    E e                  => ?check_rhs_4
-    CloT  s th           => ?check_rhs_5
-    DCloT s th           => ?check_rhs_6
-
-  export
-  infer : (ctx : WfContext d n) -> (subj : Elim d n) ->
-          m (InferResult ctx subj)
-  infer ctx subj = case subj of
-    F x        => inferFree ctx x
-    B i        => inferBound ctx i
-    fun :@ arg => ?infer_rhs_3
-    tm :# ty   => inferAnn ctx tm ty
-    CloE  e th => ?infer_rhs_5
-    DCloE e th => ?infer_rhs_6
-
-
-parameters {auto _ : MonadThrow Error m} (globals : Globals)
-  public export
-  check0 : (subj, ty : Term 0 0) -> m (Check0 globals subj ty)
-  check0 subj ty = pure $
-    case !(check (zeroWfCtx globals) subj ty) of
-      MkCheckResult [<] [<] prf => prf
-
-  public export
-  infer0 : (subj : Elim 0 0) -> (ty : Term 0 0) -> m (Infer0 globals subj)
-  infer0 subj ty = pure $
-    case !(infer (zeroWfCtx globals) subj) of
-      MkInferResult [<] [<] ty prf => MkInfer0 ty prf
diff --git a/src/Quox/Typing.idr b/src/Quox/Typing.idr
index 8feb6e6..f3e1406 100644
--- a/src/Quox/Typing.idr
+++ b/src/Quox/Typing.idr
@@ -71,7 +71,6 @@ namespace TyContext
   eqDim p q = {dctx $= DEq p q}
 
 
-
 namespace QOutput
   export
   (+) : QOutput n -> QOutput n -> QOutput n
@@ -81,200 +80,6 @@ namespace QOutput
   (*) : Qty -> QOutput n -> QOutput n
   (*) pi = map (pi *)
 
-
-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)
-
-
-namespace Universe
-  public export
-  data LT : Universe -> Universe -> Type where
-    Fin : k `LT` l -> U k `LT` U l
-    Any : U _ `LT` UAny
-
-  export
-  Uninhabited (UAny `LT` j) where
-    uninhabited _ impossible
-
-  export
-  isLT : (i, j : Universe) -> Dec (i `LT` j)
-  isLT (U i) (U j) with (i `isLT` j)
-    _ | Yes prf   = Yes $ Fin prf
-    _ | No contra = No  $ \(Fin prf) => contra prf
-  isLT (U _) UAny = Yes Any
-  isLT UAny  _    = No uninhabited
-
-
-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 qctx : QContext n)
-    (0 i : Var n)
-  where
-    constructor MkLookup
-    tmout, tyout : QOutput n
-    type : Term d from
-    by   : Shift from n
-    0 only : IsOnly tmout i
-    0 look : IsLookup tctx i type by
-
-  public export
-  lookup' : (tctx : TContext d n) -> (qctx : QContext n) ->
-            (i : Var n) -> Lookup' tctx qctx i
-  lookup' tctx@(_ :< _) (_ :< tyout) VZ =
-    MkLookup {only = (only tctx VZ).snd, look = Here,
-              tyout = tyout :< Zero, _}
-  lookup' (tctx :< _) (qctx :< _) (VS i) =
-    let inner = lookup' tctx qctx i in
-    MkLookup {only = There inner.only, look = There inner.look,
-              tyout = inner.tyout :< Zero, _}
-
-
-  public export %inline
-  Lookup : TyContext d n -> Var n -> Type
-  Lookup ctx i = Lookup' ctx.tctx ctx.qctx i
-
-  public export %inline
-  lookup : (ctx : TyContext d n) -> (i : Var n) -> Lookup ctx i
-  lookup ctx = lookup' ctx.tctx ctx.qctx
-
-
-
-mutual
-  public export
-  data HasTypeT :
-      {0 d, n : Nat} ->
-      (ctx  : TyContext d n) ->
-      (subj : Term d n) ->
-      (ty   : Term d n) ->
-      (tmout, tyout : QOutput n) ->
-      Type
-    where
-      TYPE :
-        (0 wf : IsWf ctx) ->
-        (lt : k `LT` l) ->
-        (0 ztm : IsZero tmout) -> (0 zty : IsZero tyout) ->
-        HasTypeT {ctx, subj = TYPE k, ty = TYPE l, tmout, tyout}
-      Pi :
-        (tyA : HasTypeT {ctx, subj = a, ty = TYPE l, tmout = tmoutA, tyout}) ->
-        (tyB : HasTypeT {ctx = extendTy a tmoutA ctx, subj = b, ty = TYPE l,
-                         tmout = tmoutB :< qty, tyout = tyout :< Zero}) ->
-        (0 zty : IsZero tyout) ->
-        HasTypeT {ctx, subj = Pi qtm qty x a b, ty = TYPE l,
-                  tmout = tmoutA + tmoutB, tyout}
-      PushT :
-        (0 eq : ty' = pushSubstsT' ty) ->
-        (j : HasTypeT {ctx, subj, ty = ty', tmout, tyout}) ->
-        HasTypeT {ctx, subj, ty, tmout, tyout}
-
-  public export
-  data HasTypeE :
-      {0 d, n : Nat} ->
-      (ctx  : TyContext d n) ->
-      (subj : Elim d n) ->
-      (ty   : Term d n) ->
-      (tmout, tyout : QOutput n) ->
-      Type
-    where
-      F :
-        (0 wf : IsWf ctx) ->
-        (g : Global) ->
-        (0 eq : lookup x ctx.globals = Just g) ->
-        (0 ztm : IsZero tmout) -> (0 zty : IsZero tyout) ->
-        HasTypeE {ctx, subj = F x, ty = g.type, tmout, tyout}
-      B :
-        {0 ctx : TyContext d n} ->
-        (0 wf : IsWf ctx) ->
-        (look : Lookup ctx i) ->
-        (0 eq : ty = look.type // look.by) ->
-        HasTypeE {ctx, subj = B i, ty, tmout = look.tmout, tyout = look.tyout}
-      Ann :
-        HasTypeT {ctx, subj = tm,       ty, tmout, tyout} ->
-        HasTypeE {ctx, subj = tm :# ty, ty, tmout, tyout}
-      PushE :
-        (0 eq : ty' = pushSubstsT' ty) ->
-        HasTypeE {ctx, subj, ty = ty', tmout, tyout} ->
-        HasTypeE {ctx, subj, ty, tmout, tyout}
-
-  public export
-  data IsWf' :
-      (globals : Globals) ->
-      (dctx : DContext d) ->
-      (tctx : TContext d n) ->
-      (qctx : QContext n) -> Type
-    where
-      NIL  : IsWf' globals dctx [<] [<]
-      BIND :
-        IsWf' {globals, dctx, tctx, qctx} ->
-        HasTypeT {ctx = MkTyContext {globals, dctx, tctx, qctx},
-                  subj, ty = TYPE l, tmout, tyout} ->
-        IsWf' {globals, dctx, tctx = tctx :< subj, qctx = qctx :< tmout}
-
-  public export %inline
-  IsWf : TyContext d n -> Type
-  IsWf (MkTyContext {globals, dctx, tctx, qctx}) =
-    IsWf' {globals, dctx, tctx, qctx}
-
-public export
-record WfContext (d, n : Nat) where
-  constructor MkWfContext
-  ctx  : TyContext d n
-  0 wf : IsWf ctx
-
-
-public export
-record TypeTerm {0 d, n : Nat} (ctx : TyContext d n) where
-  constructor MkTypeTerm
-  term : Term d n
-  univ : Universe
-  tmout, tyout : QOutput n
-  isType : HasTypeT {ctx, subj = term, ty = TYPE univ, tmout, tyout}
+  zero : {n : Nat} -> QOutput n
+  zero = pure Zero