producing a proof in TC is not worth it
This commit is contained in:
parent
ce9d55becc
commit
38260d3838
3 changed files with 3 additions and 366 deletions
|
|
@ -159,7 +159,7 @@ namespace Nat
|
||||||
LTESuccR : m `LTE'` n -> m `LTE'` S n
|
LTESuccR : m `LTE'` n -> m `LTE'` S n
|
||||||
%builtin Natural LTE'
|
%builtin Natural LTE'
|
||||||
|
|
||||||
export
|
export %hint
|
||||||
lteZero' : {n : Nat} -> 0 `LTE'` n
|
lteZero' : {n : Nat} -> 0 `LTE'` n
|
||||||
lteZero' {n = 0} = LTERefl
|
lteZero' {n = 0} = LTERefl
|
||||||
lteZero' {n = S n} = LTESuccR lteZero'
|
lteZero' {n = S n} = LTESuccR lteZero'
|
||||||
|
|
|
||||||
|
|
@ -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
|
|
||||||
|
|
@ -71,7 +71,6 @@ namespace TyContext
|
||||||
eqDim p q = {dctx $= DEq p q}
|
eqDim p q = {dctx $= DEq p q}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
namespace QOutput
|
namespace QOutput
|
||||||
export
|
export
|
||||||
(+) : QOutput n -> QOutput n -> QOutput n
|
(+) : QOutput n -> QOutput n -> QOutput n
|
||||||
|
|
@ -81,200 +80,6 @@ namespace QOutput
|
||||||
(*) : Qty -> QOutput n -> QOutput n
|
(*) : Qty -> QOutput n -> QOutput n
|
||||||
(*) pi = map (pi *)
|
(*) pi = map (pi *)
|
||||||
|
|
||||||
|
|
||||||
namespace Zero
|
|
||||||
public export
|
|
||||||
data IsZero : QOutput n -> Type where
|
|
||||||
LinZ : IsZero [<]
|
|
||||||
SnocZ : IsZero qctx -> IsZero (qctx :< Zero)
|
|
||||||
|
|
||||||
export
|
export
|
||||||
isZeroIrrel : {qctx : _} -> (0 _ : IsZero qctx) -> IsZero qctx
|
zero : {n : Nat} -> QOutput n
|
||||||
isZeroIrrel {qctx = [<]} LinZ = LinZ
|
zero = pure Zero
|
||||||
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}
|
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue