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

mtl ⇒ eff

Browse source
This commit is contained in:
rhiannon morris 2023-03-31 19:23:30 +02:00
parent 8a9b4c23dd
commit 36609713ac
8 changed files with 382 additions and 226 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
lib/Quox/Definition.idr
View file

@ -3,7 +3,7 @@ module Quox.Definition
import public Quox.No import public Quox.No
import public Quox.Syntax import public Quox.Syntax
import public Data.SortedMap import public Data.SortedMap
import public Control.Monad.Reader import Control.Eff
import Decidable.Decidable import Decidable.Decidable
@ -79,13 +79,12 @@ Definitions q = Definitions' q IsGlobal
public export public export
0 HasDefs' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type 0 DefsReader' : (q : Type) -> (q -> Type) -> Type -> Type
HasDefs' q isGlobal = MonadReader (Definitions' q isGlobal) DefsReader' q isGlobal = Reader (Definitions' q isGlobal)
public export public export
0 HasDefs : (q : Type) -> IsQty q => (Type -> Type) -> Type 0 DefsReader : (q : Type) -> IsQty q => Type -> Type
HasDefs q = HasDefs' q IsGlobal DefsReader q = DefsReader' q IsGlobal
public export %inline public export %inline
lookupElim : forall isGlobal. {d, n : Nat} -> lookupElim : forall isGlobal. {d, n : Nat} ->

102
lib/Quox/EffExtra.idr Normal file
View file

@ -0,0 +1,102 @@
module Quox.EffExtra
import public Control.Eff
import Data.IORef
export
localAt : (0 lbl : tag) -> Has (StateL lbl s) fs =>
(s -> s) -> Eff fs a -> Eff fs a
localAt lbl f act = do
old <- getAt lbl
modifyAt lbl f *> act <* putAt lbl old
export %inline
localAt_ : (0 lbl : tag) -> Has (StateL lbl s) fs =>
s -> Eff fs a -> Eff fs a
localAt_ lbl x = localAt lbl $ const x
export %inline
local : Has (State s) fs => (s -> s) -> Eff fs a -> Eff fs a
local = localAt ()
export %inline
local_ : Has (State s) fs => s -> Eff fs a -> Eff fs a
local_ = localAt_ ()
export
hasDrop : (0 neq : Not (a = b)) ->
(ha : Has a fs) => (hb : Has b fs) =>
Has a (drop fs hb)
hasDrop neq {ha = Z} {hb = Z} = void $ neq Refl
hasDrop neq {ha = S ha} {hb = Z} = ha
hasDrop neq {ha = Z} {hb = S hb} = Z
hasDrop neq {ha = S ha} {hb = S hb} = S $ hasDrop neq {ha, hb}
private
0 ioNotState : Not (IO = StateL _ _)
ioNotState Refl impossible
export
runStateIORefAt : (0 lbl : tag) -> (Has IO fs, Has (StateL lbl s) fs) =>
IORef s -> Eff fs a -> Eff (fs - StateL lbl s) a
runStateIORefAt lbl ref act = do
let hh : Has IO (fs - StateL lbl s) := hasDrop ioNotState
(val, st) <- runStateAt lbl !(readIORef ref) act
writeIORef ref st $> val
export %inline
runStateIORef : (Has IO fs, Has (State s) fs) =>
IORef s -> Eff fs a -> Eff (fs - State s) a
runStateIORef = runStateIORefAt ()
export %inline
evalStateAt : (0 lbl : tag) -> Has (StateL lbl s) fs =>
s -> Eff fs a -> Eff (fs - StateL lbl s) a
evalStateAt lbl s act = map fst $ runStateAt lbl s act
export %inline
evalState : Has (State s) fs => s -> Eff fs a -> Eff (fs - State s) a
evalState = evalStateAt ()
public export
data Length : List a -> Type where
Z : Length []
S : Length xs -> Length (x :: xs)
export
subsetWith : Length xs => (forall z. Has z xs -> Has z ys) ->
Subset xs ys
subsetWith @{Z} f = []
subsetWith @{S len} f = f Z :: subsetWith (f . S)
export
subsetSelf : Length xs => Subset xs xs
subsetSelf = subsetWith id
export
subsetTail : Length xs => Subset xs (x :: xs)
subsetTail = subsetWith S
-- [fixme] allow the error to be anywhere in the effect list
export
wrapErrAt : Length fs => (0 lbl : tag) -> (e -> e) ->
Eff (ExceptL lbl e :: fs) a -> Eff (ExceptL lbl e :: fs) a
wrapErrAt lbl f act =
rethrowAt lbl . mapFst f =<< lift @{subsetTail} (runExceptAt lbl act)
export %inline
wrapErr : Length fs => (e -> e) ->
Eff (Except e :: fs) a -> Eff (Except e :: fs) a
wrapErr = wrapErrAt ()
export %inline
runIO : (MonadRec io, HasIO io) => Eff [IO] a -> io a
runIO act = runEff act [liftIO]

136
lib/Quox/Equal.idr
View file

@ -2,49 +2,46 @@ module Quox.Equal
import Quox.BoolExtra import Quox.BoolExtra
import public Quox.Typing import public Quox.Typing
import public Control.Monad.Either
import public Control.Monad.Reader
import Data.Maybe import Data.Maybe
import Quox.EffExtra
%default total %default total
public export public export
record CmpContext where 0 EqModeState : Type -> Type
constructor MkCmpContext EqModeState = State EqMode
mode : EqMode
public export public export
0 HasCmpContext : (Type -> Type) -> Type 0 EqualEff : Type -> List (Type -> Type)
HasCmpContext = MonadReader CmpContext EqualEff q = [ErrorEff q, EqModeState]
public export public export
0 CanEqual : (q : Type) -> (Type -> Type) -> Type 0 EqualE : Type -> Type -> Type
CanEqual q m = (HasErr q m, HasCmpContext m) EqualE q = Eff $ EqualEff q
export %inline
mode : Has EqModeState fs => Eff fs EqMode
mode = get
private %inline
mode : HasCmpContext m => m EqMode
mode = asks mode
parameters {auto _ : CanEqual q m} (ctx : EqContext q n) parameters (ctx : EqContext q n)
private %inline private %inline
clashT : Term q 0 n -> Term q 0 n -> Term q 0 n -> m a clashT : Term q 0 n -> Term q 0 n -> Term q 0 n -> EqualE q a
clashT ty s t = throwError $ ClashT ctx !mode ty s t clashT ty s t = throw $ ClashT ctx !mode ty s t
private %inline private %inline
clashTy : Term q 0 n -> Term q 0 n -> m a clashTy : Term q 0 n -> Term q 0 n -> EqualE q a
clashTy s t = throwError $ ClashTy ctx !mode s t clashTy s t = throw $ ClashTy ctx !mode s t
private %inline private %inline
clashE : Elim q 0 n -> Elim q 0 n -> m a clashE : Elim q 0 n -> Elim q 0 n -> EqualE q a
clashE e f = throwError $ ClashE ctx !mode e f clashE e f = throw $ ClashE ctx !mode e f
private %inline private %inline
wrongType : Term q 0 n -> Term q 0 n -> m a wrongType : Term q 0 n -> Term q 0 n -> EqualE q a
wrongType ty s = throwError $ WrongType ctx ty s wrongType ty s = throw $ WrongType ctx ty s
||| true if a term is syntactically a type, or is neutral. ||| true if a term is syntactically a type, or is neutral.
@ -105,10 +102,11 @@ parameters (defs : Definitions' q g)
||| boundary separation. ||| boundary separation.
||| * an enum type is a subsingleton if it has zero or one tags. ||| * an enum type is a subsingleton if it has zero or one tags.
public export covering public export covering
isSubSing : HasErr q m => {n : Nat} -> Term q 0 n -> m Bool isSubSing : Has (ErrorEff q) fs =>
isSubSing ty = do {n : Nat} -> Term q 0 n -> Eff fs Bool
Element ty nc <- whnfT defs ty isSubSing ty0 = do
case ty of Element ty0 nc <- whnfT defs ty0
case ty0 of
TYPE _ => pure False TYPE _ => pure False
Pi {res, _} => isSubSing res.term Pi {res, _} => isSubSing res.term
Lam {} => pure False Lam {} => pure False
@ -128,13 +126,14 @@ parameters (defs : Definitions' q g)
export export
ensureTyCon : HasErr q m => ensureTyCon : Has (ErrorEff q) fs =>
(ctx : EqContext q n) -> (t : Term q 0 n) -> m (So (isTyCon t)) (ctx : EqContext q n) -> (t : Term q 0 n) ->
Eff fs (So (isTyCon t))
ensureTyCon ctx t = case nchoose $ isTyCon t of ensureTyCon ctx t = case nchoose $ isTyCon t of
Left y => pure y Left y => pure y
Right n => throwError $ NotType (toTyContext ctx) (t // shift0 ctx.dimLen) Right n => throw $ NotType (toTyContext ctx) (t // shift0 ctx.dimLen)
parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)} parameters (defs : Definitions' q _) {auto _ : IsQty q}
mutual mutual
namespace Term namespace Term
||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to ||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to
@ -142,7 +141,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
||| |||
||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠ ||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
export covering %inline export covering %inline
compare0 : EqContext q n -> (ty, s, t : Term q 0 n) -> m () compare0 : EqContext q n -> (ty, s, t : Term q 0 n) -> EqualE q ()
compare0 ctx ty s t = compare0 ctx ty s t =
wrapErr (WhileComparingT ctx !mode ty s t) $ do wrapErr (WhileComparingT ctx !mode ty s t) $ do
let Val n = ctx.termLen let Val n = ctx.termLen
@ -163,10 +162,10 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
(ty, s, t : Term q 0 n) -> (ty, s, t : Term q 0 n) ->
(0 nty : NotRedex defs ty) => (0 tty : So (isTyCon ty)) => (0 nty : NotRedex defs ty) => (0 tty : So (isTyCon ty)) =>
(0 ns : NotRedex defs s) => (0 nt : NotRedex defs t) => (0 ns : NotRedex defs s) => (0 nt : NotRedex defs t) =>
m () EqualE q ()
compare0' ctx (TYPE _) s t = compareType ctx s t compare0' ctx (TYPE _) s t = compareType ctx s t
compare0' ctx ty@(Pi {qty, arg, res}) s t {n} = local {mode := Equal} $ compare0' ctx ty@(Pi {qty, arg, res}) s t {n} = local_ Equal $
case (s, t) of case (s, t) of
-- Γ, x : A ⊢ s = t : B -- Γ, x : A ⊢ s = t : B
-- ------------------------------------------- -- -------------------------------------------
@ -188,11 +187,11 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
ctx' : EqContext q (S n) ctx' : EqContext q (S n)
ctx' = extendTy qty res.name arg ctx ctx' = extendTy qty res.name arg ctx
eta : Elim q 0 n -> ScopeTerm q 0 n -> m () eta : Elim q 0 n -> ScopeTerm q 0 n -> EqualE q ()
eta e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b eta e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
eta e (S _ (N _)) = clashT ctx ty s t eta e (S _ (N _)) = clashT ctx ty s t
compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $ compare0' ctx ty@(Sig {fst, snd, _}) s t = local_ Equal $
case (s, t) of case (s, t) of
-- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x} -- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x}
-- -------------------------------------------- -- --------------------------------------------
@ -212,7 +211,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
(E _, t) => wrongType ctx ty t (E _, t) => wrongType ctx ty t
(s, _) => wrongType ctx ty s (s, _) => wrongType ctx ty s
compare0' ctx ty@(Enum tags) s t = local {mode := Equal} $ compare0' ctx ty@(Enum tags) s t = local_ Equal $
case (s, t) of case (s, t) of
-- -------------------- -- --------------------
-- Γ ⊢ `t = `t : {ts} -- Γ ⊢ `t = `t : {ts}
@ -234,7 +233,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
-- Γ ⊢ e = f : Eq [i ⇒ A] s t -- Γ ⊢ e = f : Eq [i ⇒ A] s t
pure () pure ()
compare0' ctx Nat s t = local {mode := Equal} $ compare0' ctx Nat s t = local_ Equal $
case (s, t) of case (s, t) of
-- --------------- -- ---------------
-- Γ ⊢ 0 = 0 : ℕ -- Γ ⊢ 0 = 0 : ℕ
@ -259,7 +258,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
(E _, t) => wrongType ctx Nat t (E _, t) => wrongType ctx Nat t
(s, _) => wrongType ctx Nat s (s, _) => wrongType ctx Nat s
compare0' ctx ty@(BOX q ty') s t = local {mode := Equal} $ compare0' ctx ty@(BOX q ty') s t = local_ Equal $
case (s, t) of case (s, t) of
-- Γ ⊢ s = t : A -- Γ ⊢ s = t : A
-- ----------------------- -- -----------------------
@ -282,7 +281,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
||| compares two types, using the current variance `mode` for universes. ||| compares two types, using the current variance `mode` for universes.
||| fails if they are not types, even if they would happen to be equal. ||| fails if they are not types, even if they would happen to be equal.
export covering %inline export covering %inline
compareType : EqContext q n -> (s, t : Term q 0 n) -> m () compareType : EqContext q n -> (s, t : Term q 0 n) -> EqualE q ()
compareType ctx s t = do compareType ctx s t = do
let Val n = ctx.termLen let Val n = ctx.termLen
Element s ns <- whnfT defs s Element s ns <- whnfT defs s
@ -298,7 +297,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
(0 ns : NotRedex defs s) => (0 ts : So (isTyCon s)) => (0 ns : NotRedex defs s) => (0 ts : So (isTyCon s)) =>
(0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) => (0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) =>
(0 st : So (sameTyCon s t)) => (0 st : So (sameTyCon s t)) =>
m () EqualE q ()
-- equality is the same as subtyping, except with the -- equality is the same as subtyping, except with the
-- "≤" in the TYPE rule being replaced with "=" -- "≤" in the TYPE rule being replaced with "="
compareType' ctx (TYPE k) (TYPE l) = compareType' ctx (TYPE k) (TYPE l) =
@ -313,7 +312,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
-- ---------------------------------------- -- ----------------------------------------
-- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂ -- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
expectEqualQ sQty tQty expectEqualQ sQty tQty
local {mode $= flip} $ compareType ctx sArg tArg -- contra local flip $ compareType ctx sArg tArg -- contra
compareType (extendTy zero sRes.name sArg ctx) sRes.term tRes.term compareType (extendTy zero sRes.name sArg ctx) sRes.term tRes.term
compareType' ctx (Sig {fst = sFst, snd = sSnd, _}) compareType' ctx (Sig {fst = sFst, snd = sSnd, _})
@ -332,7 +331,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
-- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂ -- Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
compareType (extendDim sTy.name One ctx) sTy.one tTy.one compareType (extendDim sTy.name One ctx) sTy.one tTy.one
local {mode := Equal} $ do local_ Equal $ do
Term.compare0 ctx sTy.zero sl tl Term.compare0 ctx sTy.zero sl tl
Term.compare0 ctx sTy.one sr tr Term.compare0 ctx sTy.one sr tr
@ -364,7 +363,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
private covering private covering
computeElimType : EqContext q n -> (e : Elim q 0 n) -> computeElimType : EqContext q n -> (e : Elim q 0 n) ->
(0 ne : NotRedex defs e) -> (0 ne : NotRedex defs e) ->
m (Term q 0 n) EqualE q (Term q 0 n)
computeElimType ctx (F x) _ = do computeElimType ctx (F x) _ = do
defs <- lookupFree' defs x defs <- lookupFree' defs x
pure $ injectT ctx defs.type pure $ injectT ctx defs.type
@ -384,7 +383,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
private covering private covering
replaceEnd : EqContext q n -> replaceEnd : EqContext q n ->
(e : Elim q 0 n) -> DimConst -> (0 ne : NotRedex defs e) -> (e : Elim q 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
m (Elim q 0 n) EqualE q (Elim q 0 n)
replaceEnd ctx e p ne = do replaceEnd ctx e p ne = do
(ty, l, r) <- expectEqE defs ctx !(computeElimType ctx e ne) (ty, l, r) <- expectEqE defs ctx !(computeElimType ctx e ne)
pure $ ends l r p :# dsub1 ty (K p) pure $ ends l r p :# dsub1 ty (K p)
@ -398,7 +397,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
||| ⚠ **assumes that they have both been typechecked, and have ||| ⚠ **assumes that they have both been typechecked, and have
||| equal types.** ⚠ ||| equal types.** ⚠
export covering %inline export covering %inline
compare0 : EqContext q n -> (e, f : Elim q 0 n) -> m () compare0 : EqContext q n -> (e, f : Elim q 0 n) -> EqualE q ()
compare0 ctx e f = compare0 ctx e f =
wrapErr (WhileComparingE ctx !mode e f) $ do wrapErr (WhileComparingE ctx !mode e f) $ do
let Val n = ctx.termLen let Val n = ctx.termLen
@ -412,7 +411,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
compare0' : EqContext q n -> compare0' : EqContext q n ->
(e, f : Elim q 0 n) -> (e, f : Elim q 0 n) ->
(0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) -> (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
m () EqualE q ()
-- replace applied equalities with the appropriate end first -- replace applied equalities with the appropriate end first
-- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A‹𝟎/i› -- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A‹𝟎/i›
-- --
@ -429,7 +428,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
compare0' ctx e@(B _) f _ _ = clashE ctx e f compare0' ctx e@(B _) f _ _ = clashE ctx e f
compare0' ctx (e :@ s) (f :@ t) ne nf = compare0' ctx (e :@ s) (f :@ t) ne nf =
local {mode := Equal} $ do local_ Equal $ do
compare0 ctx e f compare0 ctx e f
(_, arg, _) <- expectPiE defs ctx !(computeElimType ctx e (noOr1 ne)) (_, arg, _) <- expectPiE defs ctx !(computeElimType ctx e (noOr1 ne))
Term.compare0 ctx arg s t Term.compare0 ctx arg s t
@ -437,7 +436,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
compare0' ctx (CasePair epi e eret ebody) compare0' ctx (CasePair epi e eret ebody)
(CasePair fpi f fret fbody) ne nf = (CasePair fpi f fret fbody) ne nf =
local {mode := Equal} $ do local_ Equal $ do
compare0 ctx e f compare0 ctx e f
ety <- computeElimType ctx e (noOr1 ne) ety <- computeElimType ctx e (noOr1 ne)
compareType (extendTy zero eret.name ety ctx) eret.term fret.term compareType (extendTy zero eret.name ety ctx) eret.term fret.term
@ -451,7 +450,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
compare0' ctx (CaseEnum epi e eret earms) compare0' ctx (CaseEnum epi e eret earms)
(CaseEnum fpi f fret farms) ne nf = (CaseEnum fpi f fret farms) ne nf =
local {mode := Equal} $ do local_ Equal $ do
compare0 ctx e f compare0 ctx e f
ety <- computeElimType ctx e (noOr1 ne) ety <- computeElimType ctx e (noOr1 ne)
compareType (extendTy zero eret.name ety ctx) eret.term fret.term compareType (extendTy zero eret.name ety ctx) eret.term fret.term
@ -460,15 +459,15 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
!(lookupArm t earms) !(lookupArm t farms) !(lookupArm t earms) !(lookupArm t farms)
expectEqualQ epi fpi expectEqualQ epi fpi
where where
lookupArm : TagVal -> CaseEnumArms q d n -> m (Term q d n) lookupArm : TagVal -> CaseEnumArms q d n -> EqualE q (Term q d n)
lookupArm t arms = case lookup t arms of lookupArm t arms = case lookup t arms of
Just arm => pure arm Just arm => pure arm
Nothing => throwError $ TagNotIn t (fromList $ keys arms) Nothing => throw $ TagNotIn t (fromList $ keys arms)
compare0' ctx e@(CaseEnum {}) f _ _ = clashE ctx e f compare0' ctx e@(CaseEnum {}) f _ _ = clashE ctx e f
compare0' ctx (CaseNat epi epi' e eret ezer esuc) compare0' ctx (CaseNat epi epi' e eret ezer esuc)
(CaseNat fpi fpi' f fret fzer fsuc) ne nf = (CaseNat fpi fpi' f fret fzer fsuc) ne nf =
local {mode := Equal} $ do local_ Equal $ do
compare0 ctx e f compare0 ctx e f
ety <- computeElimType ctx e (noOr1 ne) ety <- computeElimType ctx e (noOr1 ne)
compareType (extendTy zero eret.name ety ctx) eret.term fret.term compareType (extendTy zero eret.name ety ctx) eret.term fret.term
@ -483,7 +482,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
compare0' ctx (CaseBox epi e eret ebody) compare0' ctx (CaseBox epi e eret ebody)
(CaseBox fpi f fret fbody) ne nf = (CaseBox fpi f fret fbody) ne nf =
local {mode := Equal} $ do local_ Equal $ do
compare0 ctx e f compare0 ctx e f
ety <- computeElimType ctx e (noOr1 ne) ety <- computeElimType ctx e (noOr1 ne)
compareType (extendTy zero eret.name ety ctx) eret.term fret.term compareType (extendTy zero eret.name ety ctx) eret.term fret.term
@ -497,15 +496,16 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
compare0' ctx (s :# a) (t :# b) _ _ = compare0' ctx (s :# a) (t :# b) _ _ =
Term.compare0 ctx !(bigger a b) s t Term.compare0 ctx !(bigger a b) s t
where where
bigger : forall a. a -> a -> m a bigger : forall a. a -> a -> EqualE q a
bigger l r = asks mode <&> \case Super => l; _ => r bigger l r = mode <&> \case Super => l; _ => r
compare0' ctx (s :# a) f _ _ = Term.compare0 ctx a s (E f) compare0' ctx (s :# a) f _ _ = Term.compare0 ctx a s (E f)
compare0' ctx e (t :# b) _ _ = Term.compare0 ctx b (E e) t compare0' ctx e (t :# b) _ _ = Term.compare0 ctx b (E e) t
compare0' ctx e@(_ :# _) f _ _ = clashE ctx e f compare0' ctx e@(_ :# _) f _ _ = clashE ctx e f
parameters {auto _ : (HasDefs' q _ m, HasErr q m, IsQty q)} parameters {auto _ : (Has (DefsReader' q _) fs, Has (ErrorEff q) fs)}
{auto _ : IsQty q}
(ctx : TyContext q d n) (ctx : TyContext q d n)
-- [todo] only split on the dvars that are actually used anywhere in -- [todo] only split on the dvars that are actually used anywhere in
-- the calls to `splits` -- the calls to `splits`
@ -513,51 +513,51 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, IsQty q)}
parameters (mode : EqMode) parameters (mode : EqMode)
namespace Term namespace Term
export covering export covering
compare : (ty, s, t : Term q d n) -> m () compare : (ty, s, t : Term q d n) -> Eff fs ()
compare ty s t = do compare ty s t = do
defs <- ask defs <- ask
runReaderT {m} (MkCmpContext {mode}) $ map fst $ runState @{Z} mode $
for_ (splits ctx.dctx) $ \th => for_ (splits ctx.dctx) $ \th =>
let ectx = makeEqContext ctx th in let ectx = makeEqContext ctx th in
compare0 defs ectx (ty // th) (s // th) (t // th) lift $ compare0 defs ectx (ty // th) (s // th) (t // th)
export covering export covering
compareType : (s, t : Term q d n) -> m () compareType : (s, t : Term q d n) -> Eff fs ()
compareType s t = do compareType s t = do
defs <- ask defs <- ask
runReaderT {m} (MkCmpContext {mode}) $ map fst $ runState @{Z} mode $
for_ (splits ctx.dctx) $ \th => for_ (splits ctx.dctx) $ \th =>
let ectx = makeEqContext ctx th in let ectx = makeEqContext ctx th in
compareType defs ectx (s // th) (t // th) lift $ compareType defs ectx (s // th) (t // th)
namespace Elim namespace Elim
||| you don't have to pass the type in but the arguments must still be ||| you don't have to pass the type in but the arguments must still be
||| of the same type!! ||| of the same type!!
export covering %inline export covering %inline
compare : (e, f : Elim q d n) -> m () compare : (e, f : Elim q d n) -> Eff fs ()
compare e f = do compare e f = do
defs <- ask defs <- ask
runReaderT {m} (MkCmpContext {mode}) $ map fst $ runState @{Z} mode $
for_ (splits ctx.dctx) $ \th => for_ (splits ctx.dctx) $ \th =>
let ectx = makeEqContext ctx th in let ectx = makeEqContext ctx th in
compare0 defs ectx (e // th) (f // th) lift $ compare0 defs ectx (e // th) (f // th)
namespace Term namespace Term
export covering %inline export covering %inline
equal, sub, super : (ty, s, t : Term q d n) -> m () equal, sub, super : (ty, s, t : Term q d n) -> Eff fs ()
equal = compare Equal equal = compare Equal
sub = compare Sub sub = compare Sub
super = compare Super super = compare Super
export covering %inline export covering %inline
equalType, subtype, supertype : (s, t : Term q d n) -> m () equalType, subtype, supertype : (s, t : Term q d n) -> Eff fs ()
equalType = compareType Equal equalType = compareType Equal
subtype = compareType Sub subtype = compareType Sub
supertype = compareType Super supertype = compareType Super
namespace Elim namespace Elim
export covering %inline export covering %inline
equal, sub, super : (e, f : Elim q d n) -> m () equal, sub, super : (e, f : Elim q d n) -> Eff fs ()
equal = compare Equal equal = compare Equal
sub = compare Sub sub = compare Sub
super = compare Super super = compare Super

189
lib/Quox/Parser/FromParser.idr
View file

@ -7,15 +7,27 @@ import Quox.Typechecker
import Data.List import Data.List
import Data.SnocVect import Data.SnocVect
import public Control.Monad.Either import Quox.EffExtra
import public Control.Monad.State
import public Control.Monad.Reader
import System.File import System.File
import System.Path import System.Path
import Data.IORef
%hide Context.(<$>)
%hide Context.(<*>) %default total
%hide Typing.Error
%hide Lexer.Error
%hide Parser.Error
public export
0 Def : Type
Def = Definition Three
public export
0 NDef : Type
NDef = (Name, Def)
public export public export
0 Defs : Type 0 Defs : Type
@ -33,30 +45,26 @@ data FromParserError =
| ParseError Parser.Error | ParseError Parser.Error
public export public export
0 CanError : (Type -> Type) -> Type 0 IncludePath : Type
CanError = MonadError FromParserError IncludePath = List String
public export public export
0 HasDefsRW : (Type -> Type) -> Type 0 SeenFiles : Type
HasDefsRW = MonadState Defs SeenFiles = SortedSet String
public export
0 HasNamespace : (Type -> Type) -> Type
HasNamespace = MonadReader Mods
public export public export
0 LoadFile : (Type -> Type) -> Type data StateTag = DEFS | NS | SEEN
LoadFile m =
(HasIO m, MonadReader (List String) m, MonadState (SortedSet String) m)
-- reader for include paths, state for seen files
public export public export
0 FromParser : (Type -> Type) -> Type 0 FromParserEff : List (Type -> Type)
FromParser m = FromParserEff =
(CanError m, HasDefsRW m, HasNamespace m, LoadFile m) [Except Error, StateL DEFS Defs, StateL NS Mods,
Reader IncludePath, StateL SEEN SeenFiles, IO]
public export
0 FromParser : Type -> Type
FromParser = Eff FromParserEff
parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a) parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
@ -70,24 +78,24 @@ parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
fromName x = if null x.mods then fromBaseName x.base else f x fromName x = if null x.mods then fromBaseName x.base else f x
export export
fromPDimWith : CanError m => fromPDimWith : Has (Except Error) fs =>
Context' BName d -> PDim -> m (Dim d) Context' BName d -> PDim -> Eff fs (Dim d)
fromPDimWith ds (K e) = pure $ K e fromPDimWith ds (K e) = pure $ K e
fromPDimWith ds (V i) = fromPDimWith ds (V i) =
fromBaseName (pure . B) (const $ throwError $ DimNotInScope i) ds i fromBaseName (pure . B) (const $ throw $ DimNotInScope i) ds i
private private
avoidDim : CanError m => Context' BName d -> PName -> m (Term q d n) avoidDim : Has (Except Error) fs =>
Context' BName d -> PName -> Eff fs (Term q d n)
avoidDim ds x = avoidDim ds x =
fromName (const $ throwError $ DimNameInTerm x.base) fromName (const $ throw $ DimNameInTerm x.base) (pure . FT . fromPName) ds x
(pure . FT . fromPName) ds x
mutual mutual
export export
fromPTermWith : CanError m => fromPTermWith : Has (Except Error) fs =>
Context' BName d -> Context' BName n -> Context' BName d -> Context' BName n ->
PTerm -> m (Term Three d n) PTerm -> Eff fs (Term Three d n)
fromPTermWith ds ns t0 = case t0 of fromPTermWith ds ns t0 = case t0 of
TYPE k => TYPE k =>
pure $ TYPE $ k pure $ TYPE $ k
@ -136,7 +144,7 @@ mutual
if length strs == length (SortedSet.toList set) then if length strs == length (SortedSet.toList set) then
pure $ Enum set pure $ Enum set
else else
throwError $ DuplicatesInEnum strs throw $ DuplicatesInEnum strs
Tag str => pure $ Tag str Tag str => pure $ Tag str
@ -168,27 +176,27 @@ mutual
map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a
private private
fromPTermEnumArms : CanError m => fromPTermEnumArms : Has (Except Error) fs =>
Context' BName d -> Context' BName n -> Context' BName d -> Context' BName n ->
List (TagVal, PTerm) -> m (CaseEnumArms Three d n) List (TagVal, PTerm) -> Eff fs (CaseEnumArms Three d n)
fromPTermEnumArms ds ns = fromPTermEnumArms ds ns =
map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns) map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns)
private private
fromPTermElim : CanError m => fromPTermElim : Has (Except Error) fs =>
Context' BName d -> Context' BName n -> Context' BName d -> Context' BName n ->
PTerm -> m (Elim Three d n) PTerm -> Eff fs (Elim Three d n)
fromPTermElim ds ns e = fromPTermElim ds ns e =
case !(fromPTermWith ds ns e) of case !(fromPTermWith ds ns e) of
E e => pure e E e => pure e
_ => throwError $ AnnotationNeeded e _ => throw $ AnnotationNeeded e
-- [todo] use SN if the var is named but still unused -- [todo] use SN if the var is named but still unused
private private
fromPTermTScope : {s : Nat} -> CanError m => fromPTermTScope : {s : Nat} -> Has (Except Error) fs =>
Context' BName d -> Context' BName n -> Context' BName d -> Context' BName n ->
SnocVect s BName -> SnocVect s BName ->
PTerm -> m (ScopeTermN s Three d n) PTerm -> Eff fs (ScopeTermN s Three d n)
fromPTermTScope ds ns xs t = fromPTermTScope ds ns xs t =
if all isNothing xs then if all isNothing xs then
SN <$> fromPTermWith ds ns t SN <$> fromPTermWith ds ns t
@ -197,10 +205,10 @@ mutual
<$> fromPTermWith ds (ns ++ xs) t <$> fromPTermWith ds (ns ++ xs) t
private private
fromPTermDScope : {s : Nat} -> CanError m => fromPTermDScope : {s : Nat} -> Has (Except Error) fs =>
Context' BName d -> Context' BName n -> Context' BName d -> Context' BName n ->
SnocVect s BName -> SnocVect s BName ->
PTerm -> m (DScopeTermN s Three d n) PTerm -> Eff fs (DScopeTermN s Three d n)
fromPTermDScope ds ns xs t = fromPTermDScope ds ns xs t =
if all isNothing xs then if all isNothing xs then
SN <$> fromPTermWith ds ns t SN <$> fromPTermWith ds ns t
@ -210,29 +218,32 @@ mutual
export %inline export %inline
fromPTerm : CanError m => PTerm -> m (Term Three 0 0) fromPTerm : Has (Except Error) fs => PTerm -> Eff fs (Term Three 0 0)
fromPTerm = fromPTermWith [<] [<] fromPTerm = fromPTermWith [<] [<]
export export
globalPQty : CanError m => (q : PQty) -> m (IsGlobal q) globalPQty : Has (Except Error) fs =>
(q : PQty) -> Eff fs (IsGlobal q)
globalPQty pi = case isGlobal pi of globalPQty pi = case isGlobal pi of
Yes y => pure y Yes y => pure y
No n => throwError $ QtyNotGlobal pi No n => throw $ QtyNotGlobal pi
export export
fromPNameNS : HasNamespace m => PName -> m Name fromPNameNS : Has (StateL NS Mods) fs => PName -> Eff fs Name
fromPNameNS name = asks $ \ns => addMods ns $ fromPName name fromPNameNS name = pure $ addMods !(getAt NS) $ fromPName name
private private
injTC : (CanError m, HasDefsRW m) => (forall m'. CanTC Three m' => m' a) -> m a injTC : (Has (StateL DEFS Defs) fs, Has (Except Error) fs) =>
injTC act = TC Three a -> Eff fs a
either (throwError . TypeError) pure $ injTC act = rethrow $ mapFst TypeError $ runTC !(getAt DEFS) act
runReaderT {m = Either _} !get act
export export covering
fromPDef : (CanError m, HasDefsRW m, HasNamespace m) => PDefinition -> m () fromPDef : (Has (StateL DEFS Defs) fs,
Has (StateL NS Mods) fs,
Has (Except Error) fs) =>
PDefinition -> Eff fs NDef
fromPDef (MkPDef qty pname ptype pterm) = do fromPDef (MkPDef qty pname ptype pterm) = do
name <- fromPNameNS pname name <- fromPNameNS pname
qtyGlobal <- globalPQty qty qtyGlobal <- globalPQty qty
@ -243,39 +254,73 @@ fromPDef (MkPDef qty pname ptype pterm) = do
Just type => do Just type => do
injTC $ checkTypeC empty type Nothing injTC $ checkTypeC empty type Nothing
injTC $ ignore $ checkC empty sqty term type injTC $ ignore $ checkC empty sqty term type
modify $ insert name $ mkDef qty type term let def = mkDef qty type term
modifyAt DEFS $ insert name def
pure (name, def)
Nothing => do Nothing => do
let E elim = term | _ => throwError $ AnnotationNeeded pterm let E elim = term | _ => throw $ AnnotationNeeded pterm
res <- injTC $ inferC empty sqty elim res <- injTC $ inferC empty sqty elim
modify $ insert name $ mkDef qty res.type term let def = mkDef qty res.type term
modifyAt DEFS $ insert name def
pure (name, def)
export export covering
fromPDecl : FromParser m => PDecl -> m () fromPDecl : (Has (StateL DEFS Defs) fs,
fromPDecl (PDef def) = fromPDef def Has (StateL NS Mods) fs,
Has (Except Error) fs) =>
PDecl -> Eff fs (List NDef)
fromPDecl (PDef def) = singleton <$> fromPDef def
fromPDecl (PNs ns) = fromPDecl (PNs ns) =
local (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls localAt NS (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls
export export covering
loadFile : (LoadFile m, CanError m) => String -> m (Maybe String) loadFile : (Has IO fs,
Has (StateL SEEN SeenFiles) fs,
Has (Reader IncludePath) fs,
Has (Except Error) fs) =>
String -> Eff fs (Maybe String)
loadFile file = loadFile file =
if contains file !get then if contains file !(getAt SEEN) then
pure Nothing pure Nothing
else do else do
Just file <- firstExists (map (</> file) !ask) Just file <- firstExists (map (</> file) !ask)
| Nothing => throwError $ LoadError file FileNotFound | Nothing => throw $ LoadError file FileNotFound
case !(readFile file) of case !(readFile file) of
Right res => pure $ Just res Right res => modifyAt SEEN (insert file) $> Just res
Left err => throwError $ LoadError file err Left err => throw $ LoadError file err
parameters {auto _ : (Has IO fs,
Has (StateL SEEN SeenFiles) fs,
Has (Reader IncludePath) fs,
Has (Except Error) fs,
Has (StateL DEFS Defs) fs,
Has (StateL NS Mods) fs)}
mutual
export covering
loadProcessFile : String -> Eff fs (List NDef)
loadProcessFile file =
case !(loadFile file) of
Just inp => do
tl <- either (throw . ParseError) pure $ lexParseInput inp
concat <$> traverse fromPTopLevel tl
Nothing => pure []
||| populates the `defs` field of the state
export covering
fromPTopLevel : PTopLevel -> Eff fs (List NDef)
fromPTopLevel (PD decl) = fromPDecl decl
fromPTopLevel (PLoad file) = loadProcessFile file
||| populates the `defs` field of the state
export export
fromPTopLevel : FromParser m => PTopLevel -> m () fromParserIO : (MonadRec io, HasIO io) =>
fromPTopLevel (PD decl) = fromPDecl decl IncludePath -> IORef SeenFiles -> IORef Defs ->
fromPTopLevel (PLoad file) = FromParser a -> io (Either Error a)
case !(loadFile file) of fromParserIO inc seen defs act =
Just inp => do runIO $
tl <- either (throwError . ParseError) pure $ lexParseInput inp runExcept $
traverse_ fromPTopLevel tl evalStateAt NS [<] $
Nothing => pure () runStateIORefAt SEEN seen $
runStateIORefAt DEFS defs $
runReader inc act

72
lib/Quox/Typechecker.idr
View file

@ -6,27 +6,33 @@ import public Quox.Equal
import Data.List import Data.List
import Data.SnocVect import Data.SnocVect
import Data.List1 import Data.List1
import Quox.EffExtra
%default total %default total
public export public export
0 CanTC' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type 0 TCEff : (q : Type) -> IsQty q => List (Type -> Type)
CanTC' q isGlobal m = (HasErr q m, MonadReader (Definitions' q isGlobal) m) TCEff q = [ErrorEff q, DefsReader q]
public export public export
0 CanTC : (q : Type) -> IsQty q => (Type -> Type) -> Type 0 TC : (q : Type) -> IsQty q => Type -> Type
CanTC q = CanTC' q IsGlobal TC q = Eff $ TCEff q
export
runTC : (0 _ : IsQty q) => Definitions q -> TC q a -> Either (Error q) a
runTC defs = extract . runExcept . runReader defs
export export
popQs : HasErr q m => IsQty q => popQs : IsQty q => Has (ErrorEff q) fs =>
QOutput q s -> QOutput q (s + n) -> m (QOutput q n) QOutput q s -> QOutput q (s + n) -> Eff fs (QOutput q n)
popQs [<] qout = pure qout popQs [<] qout = pure qout
popQs (pis :< pi) (qout :< rh) = do expectCompatQ rh pi; popQs pis qout popQs (pis :< pi) (qout :< rh) = do expectCompatQ rh pi; popQs pis qout
export %inline export %inline
popQ : HasErr q m => IsQty q => q -> QOutput q (S n) -> m (QOutput q n) popQ : IsQty q => Has (ErrorEff q) fs =>
q -> QOutput q (S n) -> Eff fs (QOutput q n)
popQ pi = popQs [< pi] popQ pi = popQs [< pi]
export export
@ -42,7 +48,7 @@ lubs ctx [] = Just $ zeroFor ctx
lubs ctx (x :: xs) = lubs1 $ x ::: xs lubs ctx (x :: xs) = lubs1 $ x ::: xs
parameters {auto _ : IsQty q} {auto _ : CanTC q m} parameters {auto _ : IsQty q}
mutual mutual
||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ" ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
||| |||
@ -54,21 +60,21 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
||| doing any further work. ||| doing any further work.
export covering %inline export covering %inline
check : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n -> check : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n ->
m (CheckResult ctx.dctx q n) TC q (CheckResult ctx.dctx q n)
check ctx sg subj ty = ifConsistent ctx.dctx $ checkC ctx sg subj ty check ctx sg subj ty = ifConsistent ctx.dctx $ checkC ctx sg subj ty
||| "Ψ | Γ ⊢₀ s ⇐ A" ||| "Ψ | Γ ⊢₀ s ⇐ A"
||| |||
||| `check0 ctx subj ty` checks a term (as `check`) in a zero context. ||| `check0 ctx subj ty` checks a term (as `check`) in a zero context.
export covering %inline export covering %inline
check0 : TyContext q d n -> Term q d n -> Term q d n -> m () check0 : TyContext q d n -> Term q d n -> Term q d n -> TC q ()
check0 ctx tm ty = ignore $ check ctx szero tm ty check0 ctx tm ty = ignore $ check ctx szero tm ty
-- the output will always be 𝟎 because the subject quantity is 0 -- the output will always be 𝟎 because the subject quantity is 0
||| `check`, assuming the dimension context is consistent ||| `check`, assuming the dimension context is consistent
export covering %inline export covering %inline
checkC : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n -> checkC : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n ->
m (CheckResult' q n) TC q (CheckResult' q n)
checkC ctx sg subj ty = checkC ctx sg subj ty =
wrapErr (WhileChecking ctx sg.fst subj ty) $ wrapErr (WhileChecking ctx sg.fst subj ty) $
let Element subj nc = pushSubsts subj in let Element subj nc = pushSubsts subj in
@ -79,16 +85,16 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
||| `checkType ctx subj ty` checks a type (in a zero context). sometimes the ||| `checkType ctx subj ty` checks a type (in a zero context). sometimes the
||| universe doesn't matter, only that a term is _a_ type, so it is optional. ||| universe doesn't matter, only that a term is _a_ type, so it is optional.
export covering %inline export covering %inline
checkType : TyContext q d n -> Term q d n -> Maybe Universe -> m () checkType : TyContext q d n -> Term q d n -> Maybe Universe -> TC q ()
checkType ctx subj l = ignore $ ifConsistent ctx.dctx $ checkTypeC ctx subj l checkType ctx subj l = ignore $ ifConsistent ctx.dctx $ checkTypeC ctx subj l
export covering %inline export covering %inline
checkTypeC : TyContext q d n -> Term q d n -> Maybe Universe -> m () checkTypeC : TyContext q d n -> Term q d n -> Maybe Universe -> TC q ()
checkTypeC ctx subj l = checkTypeC ctx subj l =
wrapErr (WhileCheckingTy ctx subj l) $ checkTypeNoWrap ctx subj l wrapErr (WhileCheckingTy ctx subj l) $ checkTypeNoWrap ctx subj l
export covering %inline export covering %inline
checkTypeNoWrap : TyContext q d n -> Term q d n -> Maybe Universe -> m () checkTypeNoWrap : TyContext q d n -> Term q d n -> Maybe Universe -> TC q ()
checkTypeNoWrap ctx subj l = checkTypeNoWrap ctx subj l =
let Element subj nc = pushSubsts subj in let Element subj nc = pushSubsts subj in
checkType' ctx subj l checkType' ctx subj l
@ -102,13 +108,13 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
||| doing any further work. ||| doing any further work.
export covering %inline export covering %inline
infer : (ctx : TyContext q d n) -> SQty q -> Elim q d n -> infer : (ctx : TyContext q d n) -> SQty q -> Elim q d n ->
m (InferResult ctx.dctx q d n) TC q (InferResult ctx.dctx q d n)
infer ctx sg subj = ifConsistent ctx.dctx $ inferC ctx sg subj infer ctx sg subj = ifConsistent ctx.dctx $ inferC ctx sg subj
||| `infer`, assuming the dimension context is consistent ||| `infer`, assuming the dimension context is consistent
export covering %inline export covering %inline
inferC : (ctx : TyContext q d n) -> SQty q -> Elim q d n -> inferC : (ctx : TyContext q d n) -> SQty q -> Elim q d n ->
m (InferResult' q d n) TC q (InferResult' q d n)
inferC ctx sg subj = inferC ctx sg subj =
wrapErr (WhileInferring ctx sg.fst subj) $ wrapErr (WhileInferring ctx sg.fst subj) $
let Element subj nc = pushSubsts subj in let Element subj nc = pushSubsts subj in
@ -118,7 +124,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
private covering private covering
toCheckType : TyContext q d n -> SQty q -> toCheckType : TyContext q d n -> SQty q ->
(subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n -> (subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n ->
m (CheckResult' q n) TC q (CheckResult' q n)
toCheckType ctx sg t ty = do toCheckType ctx sg t ty = do
u <- expectTYPE !ask ctx ty u <- expectTYPE !ask ctx ty
expectEqualQ zero sg.fst expectEqualQ zero sg.fst
@ -128,7 +134,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
private covering private covering
check' : TyContext q d n -> SQty q -> check' : TyContext q d n -> SQty q ->
(subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n -> (subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n ->
m (CheckResult' q n) TC q (CheckResult' q n)
check' ctx sg t@(TYPE _) ty = toCheckType ctx sg t ty check' ctx sg t@(TYPE _) ty = toCheckType ctx sg t ty
@ -160,7 +166,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
check' ctx sg (Tag t) ty = do check' ctx sg (Tag t) ty = do
tags <- expectEnum !ask ctx ty tags <- expectEnum !ask ctx ty
-- if t ∈ ts -- if t ∈ ts
unless (t `elem` tags) $ throwError $ TagNotIn t tags unless (t `elem` tags) $ throw $ TagNotIn t tags
-- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎 -- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
pure $ zeroFor ctx pure $ zeroFor ctx
@ -207,12 +213,12 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
private covering private covering
checkType' : TyContext q d n -> checkType' : TyContext q d n ->
(subj : Term q d n) -> (0 nc : NotClo subj) => (subj : Term q d n) -> (0 nc : NotClo subj) =>
Maybe Universe -> m () Maybe Universe -> TC q ()
checkType' ctx (TYPE k) u = do checkType' ctx (TYPE k) u = do
-- if 𝓀 < ℓ then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type ℓ -- if 𝓀 < ℓ then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type ℓ
case u of case u of
Just l => unless (k < l) $ throwError $ BadUniverse k l Just l => unless (k < l) $ throw $ BadUniverse k l
Nothing => pure () Nothing => pure ()
checkType' ctx (Pi qty arg res) u = do checkType' ctx (Pi qty arg res) u = do
@ -225,7 +231,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
checkType' ctx t@(Lam {}) u = checkType' ctx t@(Lam {}) u =
throwError $ NotType ctx t throw $ NotType ctx t
checkType' ctx (Sig fst snd) u = do checkType' ctx (Sig fst snd) u = do
-- if Ψ | Γ ⊢₀ A ⇐ Type ℓ -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
@ -237,13 +243,13 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
checkType' ctx t@(Pair {}) u = checkType' ctx t@(Pair {}) u =
throwError $ NotType ctx t throw $ NotType ctx t
checkType' ctx (Enum _) u = pure () checkType' ctx (Enum _) u = pure ()
-- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ -- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ
checkType' ctx t@(Tag {}) u = checkType' ctx t@(Tag {}) u =
throwError $ NotType ctx t throw $ NotType ctx t
checkType' ctx (Eq t l r) u = do checkType' ctx (Eq t l r) u = do
-- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ -- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ
@ -257,14 +263,14 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ -- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ
checkType' ctx t@(DLam {}) u = checkType' ctx t@(DLam {}) u =
throwError $ NotType ctx t throw $ NotType ctx t
checkType' ctx Nat u = pure () checkType' ctx Nat u = pure ()
checkType' ctx Zero u = throwError $ NotType ctx Zero checkType' ctx Zero u = throw $ NotType ctx Zero
checkType' ctx t@(Succ _) u = throwError $ NotType ctx t checkType' ctx t@(Succ _) u = throw $ NotType ctx t
checkType' ctx (BOX q ty) u = checkType ctx ty u checkType' ctx (BOX q ty) u = checkType ctx ty u
checkType' ctx t@(Box _) u = throwError $ NotType ctx t checkType' ctx t@(Box _) u = throw $ NotType ctx t
checkType' ctx (E e) u = do checkType' ctx (E e) u = do
-- if Ψ | Γ ⊢₀ E ⇒ Type ℓ -- if Ψ | Γ ⊢₀ E ⇒ Type ℓ
@ -279,7 +285,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
private covering private covering
infer' : TyContext q d n -> SQty q -> infer' : TyContext q d n -> SQty q ->
(subj : Elim q d n) -> (0 nc : NotClo subj) => (subj : Elim q d n) -> (0 nc : NotClo subj) =>
m (InferResult' q d n) TC q (InferResult' q d n)
infer' ctx sg (F x) = do infer' ctx sg (F x) = do
-- if π·x : A {≔ s} in global context -- if π·x : A {≔ s} in global context
@ -289,7 +295,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎 -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
pure $ InfRes {type = injectT ctx g.type, qout = zeroFor ctx} pure $ InfRes {type = injectT ctx g.type, qout = zeroFor ctx}
where where
lookupFree : Name -> m (Definition q) lookupFree : Name -> TC q (Definition q)
lookupFree x = lookupFree' !ask x lookupFree x = lookupFree' !ask x
infer' ctx sg (B i) = infer' ctx sg (B i) =
@ -352,11 +358,11 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- with Σ₂ = lubs Σᵢ -- with Σ₂ = lubs Σᵢ
let arms = SortedMap.toList arms let arms = SortedMap.toList arms
let armTags = SortedSet.fromList $ map fst arms let armTags = SortedSet.fromList $ map fst arms
unless (ttags == armTags) $ throwError $ BadCaseEnum ttags armTags unless (ttags == armTags) $ throw $ BadCaseEnum ttags armTags
armres <- for arms $ \(a, s) => armres <- for arms $ \(a, s) =>
checkC ctx sg s (sub1 ret (Tag a :# tres.type)) checkC ctx sg s (sub1 ret (Tag a :# tres.type))
let Just armout = lubs ctx armres let Just armout = lubs ctx armres
| _ => throwError $ BadCaseQtys ctx $ | _ => throw $ BadCaseQtys ctx $
zipWith (\qs, (t, rhs) => (qs, Tag t)) armres arms zipWith (\qs, (t, rhs) => (qs, Tag t)) armres arms
pure $ InfRes { pure $ InfRes {
type = sub1 ret t, type = sub1 ret t,
@ -381,7 +387,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
sucType = substCaseNatRet ret sucType = substCaseNatRet ret
sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
let Just armout = lubs ctx [zerout, sucout] let Just armout = lubs ctx [zerout, sucout]
| _ => throwError $ BadCaseQtys ctx $ | _ => throw $ BadCaseQtys ctx $
[(zerout, Zero), (sucout, Succ $ FT $ unq p)] [(zerout, Zero), (sucout, Succ $ FT $ unq p)]
expectCompatQ qih (pi' * sg.fst) expectCompatQ qih (pi' * sg.fst)
-- [fixme] better error here -- [fixme] better error here

71
lib/Quox/Typing.idr
View file

@ -8,6 +8,8 @@ import public Quox.Syntax
import public Quox.Definition import public Quox.Definition
import public Quox.Reduce import public Quox.Reduce
import Control.Eff
%default total %default total
@ -31,11 +33,12 @@ InferResult eqs q d n = IfConsistent eqs $ InferResult' q d n
export export
lookupFree' : HasErr q m => Definitions' q g -> Name -> m (Definition' q g) lookupFree' : Has (ErrorEff q) fs =>
Definitions' q g -> Name -> Eff fs (Definition' q g)
lookupFree' defs x = lookupFree' defs x =
case lookup x defs of case lookup x defs of
Just d => pure d Just d => pure d
Nothing => throwError $ NotInScope x Nothing => throw $ NotInScope x
public export public export
@ -53,98 +56,100 @@ substCaseBoxRet : Term q d n -> ScopeTerm q d n -> Term q d (S n)
substCaseBoxRet dty retty = substCaseBoxRet dty retty =
retty.term // (Box (BVT 0) :# weakT dty ::: shift 1) retty.term // (Box (BVT 0) :# weakT dty ::: shift 1)
parameters {auto _ : HasErr q m} (defs : Definitions' q _)
parameters (defs : Definitions' q _) {auto _ : Has (ErrorEff q) fs}
export covering %inline export covering %inline
whnfT : {0 isRedex : RedexTest tm} -> Whnf tm isRedex WhnfError => whnfT : {0 isRedex : RedexTest tm} -> Whnf tm isRedex WhnfError =>
{d, n : Nat} -> tm q d n -> m (NonRedex tm q d n defs) {d, n : Nat} -> tm q d n -> Eff fs (NonRedex tm q d n defs)
whnfT = either (throwError . WhnfError) pure . whnf defs whnfT = either (throw . WhnfError) pure . whnf defs
parameters {d2, n : Nat} (ctx : Lazy (TyContext q d1 n)) parameters {d2, n : Nat} (ctx : Lazy (TyContext q d1 n))
(th : Lazy (DSubst d2 d1)) (th : Lazy (DSubst d2 d1))
export covering %inline export covering %inline
expectTYPE_ : Term q d2 n -> m Universe expectTYPE_ : Term q d2 n -> Eff fs Universe
expectTYPE_ s = case fst !(whnfT s) of expectTYPE_ s = case fst !(whnfT s) of
TYPE l => pure l TYPE l => pure l
_ => throwError $ ExpectedTYPE ctx (s // th) _ => throw $ ExpectedTYPE ctx (s // th)
export covering %inline export covering %inline
expectPi_ : Term q d2 n -> m (q, Term q d2 n, ScopeTerm q d2 n) expectPi_ : Term q d2 n -> Eff fs (q, Term q d2 n, ScopeTerm q d2 n)
expectPi_ s = case fst !(whnfT s) of expectPi_ s = case fst !(whnfT s) of
Pi {qty, arg, res, _} => pure (qty, arg, res) Pi {qty, arg, res, _} => pure (qty, arg, res)
_ => throwError $ ExpectedPi ctx (s // th) _ => throw $ ExpectedPi ctx (s // th)
export covering %inline export covering %inline
expectSig_ : Term q d2 n -> m (Term q d2 n, ScopeTerm q d2 n) expectSig_ : Term q d2 n -> Eff fs (Term q d2 n, ScopeTerm q d2 n)
expectSig_ s = case fst !(whnfT s) of expectSig_ s = case fst !(whnfT s) of
Sig {fst, snd, _} => pure (fst, snd) Sig {fst, snd, _} => pure (fst, snd)
_ => throwError $ ExpectedSig ctx (s // th) _ => throw $ ExpectedSig ctx (s // th)
export covering %inline export covering %inline
expectEnum_ : Term q d2 n -> m (SortedSet TagVal) expectEnum_ : Term q d2 n -> Eff fs (SortedSet TagVal)
expectEnum_ s = case fst !(whnfT s) of expectEnum_ s = case fst !(whnfT s) of
Enum tags => pure tags Enum tags => pure tags
_ => throwError $ ExpectedEnum ctx (s // th) _ => throw $ ExpectedEnum ctx (s // th)
export covering %inline export covering %inline
expectEq_ : Term q d2 n -> m (DScopeTerm q d2 n, Term q d2 n, Term q d2 n) expectEq_ : Term q d2 n ->
Eff fs (DScopeTerm q d2 n, Term q d2 n, Term q d2 n)
expectEq_ s = case fst !(whnfT s) of expectEq_ s = case fst !(whnfT s) of
Eq {ty, l, r, _} => pure (ty, l, r) Eq {ty, l, r, _} => pure (ty, l, r)
_ => throwError $ ExpectedEq ctx (s // th) _ => throw $ ExpectedEq ctx (s // th)
export covering %inline export covering %inline
expectNat_ : Term q d2 n -> m () expectNat_ : Term q d2 n -> Eff fs ()
expectNat_ s = case fst !(whnfT s) of expectNat_ s = case fst !(whnfT s) of
Nat => pure () Nat => pure ()
_ => throwError $ ExpectedNat ctx (s // th) _ => throw $ ExpectedNat ctx (s // th)
export covering %inline export covering %inline
expectBOX_ : Term q d2 n -> m (q, Term q d2 n) expectBOX_ : Term q d2 n -> Eff fs (q, Term q d2 n)
expectBOX_ s = case fst !(whnfT s) of expectBOX_ s = case fst !(whnfT s) of
BOX q a => pure (q, a) BOX q a => pure (q, a)
_ => throwError $ ExpectedBOX ctx (s // th) _ => throw $ ExpectedBOX ctx (s // th)
-- [fixme] refactor this stuff -- [fixme] refactor this stuff
parameters (ctx : TyContext q d n) parameters (ctx : TyContext q d n)
export covering %inline export covering %inline
expectTYPE : Term q d n -> m Universe expectTYPE : Term q d n -> Eff fs Universe
expectTYPE = expectTYPE =
let Val d = ctx.dimLen; Val n = ctx.termLen in let Val d = ctx.dimLen; Val n = ctx.termLen in
expectTYPE_ ctx id expectTYPE_ ctx id
export covering %inline export covering %inline
expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n) expectPi : Term q d n -> Eff fs (q, Term q d n, ScopeTerm q d n)
expectPi = expectPi =
let Val d = ctx.dimLen; Val n = ctx.termLen in let Val d = ctx.dimLen; Val n = ctx.termLen in
expectPi_ ctx id expectPi_ ctx id
export covering %inline export covering %inline
expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n) expectSig : Term q d n -> Eff fs (Term q d n, ScopeTerm q d n)
expectSig = expectSig =
let Val d = ctx.dimLen; Val n = ctx.termLen in let Val d = ctx.dimLen; Val n = ctx.termLen in
expectSig_ ctx id expectSig_ ctx id
export covering %inline export covering %inline
expectEnum : Term q d n -> m (SortedSet TagVal) expectEnum : Term q d n -> Eff fs (SortedSet TagVal)
expectEnum = expectEnum =
let Val d = ctx.dimLen; Val n = ctx.termLen in let Val d = ctx.dimLen; Val n = ctx.termLen in
expectEnum_ ctx id expectEnum_ ctx id
export covering %inline export covering %inline
expectEq : Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n) expectEq : Term q d n -> Eff fs (DScopeTerm q d n, Term q d n, Term q d n)
expectEq = expectEq =
let Val d = ctx.dimLen; Val n = ctx.termLen in let Val d = ctx.dimLen; Val n = ctx.termLen in
expectEq_ ctx id expectEq_ ctx id
export covering %inline export covering %inline
expectNat : Term q d n -> m () expectNat : Term q d n -> Eff fs ()
expectNat = expectNat =
let Val d = ctx.dimLen; Val n = ctx.termLen in let Val d = ctx.dimLen; Val n = ctx.termLen in
expectNat_ ctx id expectNat_ ctx id
export covering %inline export covering %inline
expectBOX : Term q d n -> m (q, Term q d n) expectBOX : Term q d n -> Eff fs (q, Term q d n)
expectBOX = expectBOX =
let Val d = ctx.dimLen; Val n = ctx.termLen in let Val d = ctx.dimLen; Val n = ctx.termLen in
expectBOX_ ctx id expectBOX_ ctx id
@ -152,43 +157,43 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _)
parameters (ctx : EqContext q n) parameters (ctx : EqContext q n)
export covering %inline export covering %inline
expectTYPEE : Term q 0 n -> m Universe expectTYPEE : Term q 0 n -> Eff fs Universe
expectTYPEE t = expectTYPEE t =
let Val n = ctx.termLen in let Val n = ctx.termLen in
expectTYPE_ (toTyContext ctx) (shift0 ctx.dimLen) t expectTYPE_ (toTyContext ctx) (shift0 ctx.dimLen) t
export covering %inline export covering %inline
expectPiE : Term q 0 n -> m (q, Term q 0 n, ScopeTerm q 0 n) expectPiE : Term q 0 n -> Eff fs (q, Term q 0 n, ScopeTerm q 0 n)
expectPiE t = expectPiE t =
let Val n = ctx.termLen in let Val n = ctx.termLen in
expectPi_ (toTyContext ctx) (shift0 ctx.dimLen) t expectPi_ (toTyContext ctx) (shift0 ctx.dimLen) t
export covering %inline export covering %inline
expectSigE : Term q 0 n -> m (Term q 0 n, ScopeTerm q 0 n) expectSigE : Term q 0 n -> Eff fs (Term q 0 n, ScopeTerm q 0 n)
expectSigE t = expectSigE t =
let Val n = ctx.termLen in let Val n = ctx.termLen in
expectSig_ (toTyContext ctx) (shift0 ctx.dimLen) t expectSig_ (toTyContext ctx) (shift0 ctx.dimLen) t
export covering %inline export covering %inline
expectEnumE : Term q 0 n -> m (SortedSet TagVal) expectEnumE : Term q 0 n -> Eff fs (SortedSet TagVal)
expectEnumE t = expectEnumE t =
let Val n = ctx.termLen in let Val n = ctx.termLen in
expectEnum_ (toTyContext ctx) (shift0 ctx.dimLen) t expectEnum_ (toTyContext ctx) (shift0 ctx.dimLen) t
export covering %inline export covering %inline
expectEqE : Term q 0 n -> m (DScopeTerm q 0 n, Term q 0 n, Term q 0 n) expectEqE : Term q 0 n -> Eff fs (DScopeTerm q 0 n, Term q 0 n, Term q 0 n)
expectEqE t = expectEqE t =
let Val n = ctx.termLen in let Val n = ctx.termLen in
expectEq_ (toTyContext ctx) (shift0 ctx.dimLen) t expectEq_ (toTyContext ctx) (shift0 ctx.dimLen) t
export covering %inline export covering %inline
expectNatE : Term q 0 n -> m () expectNatE : Term q 0 n -> Eff fs ()
expectNatE t = expectNatE t =
let Val n = ctx.termLen in let Val n = ctx.termLen in
expectNat_ (toTyContext ctx) (shift0 ctx.dimLen) t expectNat_ (toTyContext ctx) (shift0 ctx.dimLen) t
export covering %inline export covering %inline
expectBOXE : Term q 0 n -> m (q, Term q 0 n) expectBOXE : Term q 0 n -> Eff fs (q, Term q 0 n)
expectBOXE t = expectBOXE t =
let Val n = ctx.termLen in let Val n = ctx.termLen in
expectBOX_ (toTyContext ctx) (shift0 ctx.dimLen) t expectBOX_ (toTyContext ctx) (shift0 ctx.dimLen) t

24
lib/Quox/Typing/Error.idr
View file

@ -7,7 +7,7 @@ import Quox.Typing.EqMode
import Quox.Pretty import Quox.Pretty
import Data.List import Data.List
import public Control.Monad.Either import Control.Eff
public export public export
@ -64,8 +64,8 @@ data Error q
%name Error err %name Error err
public export public export
0 HasErr : Type -> (Type -> Type) -> Type ErrorEff : Type -> Type -> Type
HasErr q = MonadError (Error q) ErrorEff q = Except $ Error q
||| whether the error is surrounded in some context ||| whether the error is surrounded in some context
@ -119,24 +119,22 @@ where
takeEnd n = reverse . take n . reverse takeEnd n = reverse . take n . reverse
export %inline private
wrapErr : MonadError e m => (e -> e) -> m a -> m a expect : Has (Except e) fs =>
wrapErr f act = catchError act $ throwError . f (a -> a -> e) -> (a -> a -> Bool) -> a -> a -> Eff fs ()
expect err cmp x y = unless (x `cmp` y) $ throw $ err x y
expect : MonadError e m => (a -> a -> e) -> (a -> a -> Bool) -> a -> a -> m () parameters {auto _ : Has (Except $ Error q) fs}
expect err cmp x y = unless (x `cmp` y) $ throwError $ err x y
parameters {auto _ : HasErr q m}
export %inline export %inline
expectEqualQ : Eq q => q -> q -> m () expectEqualQ : Eq q => q -> q -> Eff fs ()
expectEqualQ = expect ClashQ (==) expectEqualQ = expect ClashQ (==)
export %inline export %inline
expectCompatQ : IsQty q => q -> q -> m () expectCompatQ : IsQty q => q -> q -> Eff fs ()
expectCompatQ = expect ClashQ $ \pi, rh => isYes $ pi `compat` rh expectCompatQ = expect ClashQ $ \pi, rh => isYes $ pi `compat` rh
export %inline export %inline
expectModeU : EqMode -> Universe -> Universe -> m () expectModeU : EqMode -> Universe -> Universe -> Eff fs ()
expectModeU mode = expect (ClashU mode) $ ucmp mode expectModeU mode = expect (ClashU mode) $ ucmp mode

3
lib/quox-lib.ipkg
View file

@ -5,11 +5,12 @@ authors = "rhiannon morris"
sourceloc = "https://git.rhiannon.website/rhi/quox" sourceloc = "https://git.rhiannon.website/rhi/quox"
license = "acsl" license = "acsl"
depends = base, contrib, elab-util, snocvect depends = base, contrib, elab-util, snocvect, eff
modules = modules =
Quox.BoolExtra, Quox.BoolExtra,
Quox.CharExtra, Quox.CharExtra,
Quox.EffExtra,
Quox.Decidable, Quox.Decidable,
Quox.No, Quox.No,
Quox.Pretty, Quox.Pretty,