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

squash warnings

Browse source
This commit is contained in:
rhiannon morris 2023-06-23 18:32:05 +02:00
parent 6eccfeef52
commit fa09aaf228
9 changed files with 53 additions and 54 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
lib/Quox/Definition.idr
View file

@ -74,10 +74,6 @@ public export
DefsState : Type -> Type
DefsState = StateL DEFS Definitions
export
defs : Has DefsReader fs => Eff fs Definitions
defs = askAt DEFS
public export %inline
lookupElim : {d, n : Nat} -> Name -> Definitions -> Maybe (Elim d n)

2
lib/Quox/Equal.idr
View file

@ -637,7 +637,7 @@ parameters (loc : Loc) (ctx : TyContext d n)
private
runCompare : (Definitions -> EqContext n -> DSubst d 0 -> Equal_ ()) ->
Equal ()
runCompare act = fromEqual_ $ eachFace $ act !defs
runCompare act = fromEqual_ $ eachFace $ act !(askAt DEFS)
namespace Term
export covering

2
lib/Quox/Parser/FromParser/Error.idr
View file

@ -6,6 +6,8 @@ import System.File
import Quox.Pretty
%hide Text.PrettyPrint.Prettyprinter.Doc.infixr.(<++>)
public export
TypeError, LexError, ParseError : Type

16
lib/Quox/Syntax/Term/Pretty.idr
View file

@ -58,11 +58,12 @@ pbname (_, x, _) = x
private
record SplitPi d n where
constructor MkSplitPi
{0 inner : Nat}
binds : Telescope (PiBind d) n inner
cod : Term d inner
private
splitPi : Telescope (PiBind d) n inner -> Term d inner -> SplitPi d n
splitPi : Telescope (PiBind d) n n' -> Term d n' -> SplitPi d n
splitPi binds (Pi qty arg res _) =
splitPi (binds :< (qty, res.name, arg)) $
assert_smaller res $ pushSubsts' res.term
@ -87,7 +88,7 @@ prettyPiBind1 pi x dnames tnames s = hcat <$> sequence
private
prettyPiBinds : {opts : _} ->
BContext d -> BContext n ->
Telescope (PiBind d) n inner ->
Telescope (PiBind d) n n' ->
Eff Pretty (SnocList (Doc opts))
prettyPiBinds _ _ [<] = pure [<]
prettyPiBinds dnames tnames (binds :< (q, x, t)) =
@ -103,11 +104,12 @@ SigBind d n = (BindName, Term d n)
private
record SplitSig d n where
constructor MkSplitSig
{0 inner : Nat}
binds : Telescope (SigBind d) n inner
last : Term d inner
private
splitSig : Telescope (SigBind d) n inner -> Term d inner -> SplitSig d n
splitSig : Telescope (SigBind d) n n' -> Term d n' -> SplitSig d n
splitSig binds (Sig fst snd _) =
splitSig (binds :< (snd.name, fst)) $
assert_smaller snd $ pushSubsts' snd.term
@ -129,7 +131,7 @@ prettySigBind1 x dnames tnames s = hcat <$> sequence
private
prettySigBinds : {opts : _} ->
BContext d -> BContext n ->
Telescope (SigBind d) n inner ->
Telescope (SigBind d) n n' ->
Eff Pretty (SnocList (Doc opts))
prettySigBinds _ _ [<] = pure [<]
prettySigBinds dnames tnames (binds :< (x, t)) =
@ -163,6 +165,7 @@ NameChunks = SnocList (NameSort, SnocList BindName)
private
record SplitLams d n where
constructor MkSplitLams
{0 dinner, ninner : Nat}
dnames : BTelescope d dinner
tnames : BTelescope n ninner
chunks : NameChunks
@ -178,9 +181,9 @@ where
if s == s' then xss :< (s', xs :< y)
else xss :< (s', xs) :< (s, [< y])
go : BTelescope d dinner -> BTelescope n ninner ->
go : BTelescope d d' -> BTelescope n n' ->
SnocList (NameSort, SnocList BindName) ->
Term dinner ninner -> SplitLams d n
Term d' n' -> SplitLams d n
go dnames tnames chunks (Lam b _) =
go dnames (tnames :< b.name) (push T b.name chunks) $
assert_smaller b $ pushSubsts' b.term
@ -235,6 +238,7 @@ prettyDTApps dnames tnames f xs = do
private
record CaseArm opts d n where
constructor MkCaseArm
{0 dinner, ninner : Nat}
pat : Doc opts
dbinds : BTelescope d dinner -- 🍴
tbinds : BTelescope n ninner

31
lib/Quox/Syntax/Term/Subst.idr
View file

@ -10,7 +10,7 @@ import Data.SnocVect
namespace CanDSubst
public export
interface CanDSubst (0 tm : TermLike) where
(//) : tm dfrom n -> Lazy (DSubst dfrom dto) -> tm dto n
(//) : tm d1 n -> Lazy (DSubst d1 d2) -> tm d2 n
||| does the minimal reasonable work:
||| - deletes the closure around an atomic constant like `TYPE`
@ -25,7 +25,7 @@ CanDSubst Term where
s // th = DCloT $ Sub s th
private
subDArgs : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
subDArgs : Elim d1 n -> DSubst d1 d2 -> Elim d2 n
subDArgs (DApp f d loc) th = DApp (subDArgs f th) (d // th) loc
subDArgs e th = DCloE $ Sub e th
@ -47,16 +47,16 @@ CanDSubst Elim where
namespace DSubst.ScopeTermN
export %inline
(//) : ScopeTermN s dfrom n -> Lazy (DSubst dfrom dto) ->
ScopeTermN s dto n
(//) : ScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
ScopeTermN s d2 n
S ns (Y body) // th = S ns $ Y $ body // th
S ns (N body) // th = S ns $ N $ body // th
namespace DSubst.DScopeTermN
export %inline
(//) : {s : Nat} ->
DScopeTermN s dfrom n -> Lazy (DSubst dfrom dto) ->
DScopeTermN s dto n
DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
DScopeTermN s d2 n
S ns (Y body) // th = S ns $ Y $ body // pushN s th
S ns (N body) // th = S ns $ N $ body // th
@ -83,7 +83,7 @@ CanSubstSelf (Elim d) where
namespace CanTSubst
public export
interface CanTSubst (0 tm : TermLike) where
(//) : tm d from -> Lazy (TSubst d from to) -> tm d to
(//) : tm d n1 -> Lazy (TSubst d n1 n2) -> tm d n2
||| does the minimal reasonable work:
||| - deletes the closure around an atomic constant like `TYPE`
@ -103,16 +103,15 @@ CanTSubst Term where
namespace ScopeTermN
export %inline
(//) : {s : Nat} ->
ScopeTermN s d from -> Lazy (TSubst d from to) ->
ScopeTermN s d to
ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
ScopeTermN s d n2
S ns (Y body) // th = S ns $ Y $ body // pushN s th
S ns (N body) // th = S ns $ N $ body // th
namespace DScopeTermN
export %inline
(//) : {s : Nat} ->
DScopeTermN s d from -> Lazy (TSubst d from to) ->
DScopeTermN s d to
DScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> DScopeTermN s d n2
S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
S ns (N body) // th = S ns $ N $ body // th
@ -125,8 +124,7 @@ export %inline
export %inline
comp : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
TSubst dto from to
comp : DSubst d1 d2 -> TSubst d1 n1 mid -> TSubst d2 mid n2 -> TSubst d2 n1 n2
comp th ps ph = map (// th) ps . ph
@ -205,8 +203,8 @@ public export
CloTest tm = forall d, n. tm d n -> Bool
interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
pushSubstsWith : DSubst dfrom dto -> TSubst dto from to ->
tm dfrom from -> Subset (tm dto to) (No . isClo)
pushSubstsWith : DSubst d1 d2 -> TSubst d2 n1 n2 ->
tm d1 n1 -> Subset (tm d2 n2) (No . isClo)
public export
0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm d n)
@ -230,8 +228,7 @@ parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
pushSubsts s = pushSubstsWith id id s
export %inline
pushSubstsWith' : DSubst dfrom dto -> TSubst dto from to ->
tm dfrom from -> tm dto to
pushSubstsWith' : DSubst d1 d2 -> TSubst d2 n1 n2 -> tm d1 n1 -> tm d2 n2
pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
export %inline

10
lib/Quox/Syntax/Term/Tighten.idr
View file

@ -8,10 +8,10 @@ import public Quox.OPE
export
Tighten (Shift from) where
Tighten (Shift f) where
-- `OPE m n` is a spicy `m ≤ n`,
-- and `Shift from n` is a (different) spicy `from ≤ n`
-- so the value is `from ≤ m` (as a `Shift`), if that is the case
-- and `Shift f n` is a (different) spicy `f ≤ n`
-- so the value is `f ≤ m` (as a `Shift`), if that is the case
tighten _ SZ = Nothing
tighten Id by = Just by
tighten (Drop p) (SS by) = tighten p by
@ -26,12 +26,12 @@ Tighten Dim where
export
tightenSub : (forall m, n. OPE m n -> env n -> Maybe (env m)) ->
OPE to1 to2 -> Subst env from to2 -> Maybe (Subst env from to1)
OPE t1 t2 -> Subst env f t2 -> Maybe (Subst env f t1)
tightenSub f p (Shift by) = [|Shift $ tighten p by|]
tightenSub f p (t ::: th) = [|f p t !::: tightenSub f p th|]
export
Tighten env => Tighten (Subst env from) where
Tighten env => Tighten (Subst env f) where
tighten p th = tightenSub tighten p th

34
lib/Quox/Typechecker.idr
View file

@ -163,7 +163,7 @@ mutual
(subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
TC (CheckResult' n)
toCheckType ctx sg t ty = do
u <- expectTYPE !defs ctx ty.loc ty
u <- expectTYPE !(askAt DEFS) ctx ty.loc ty
expectEqualQ t.loc Zero sg.fst
checkTypeNoWrap ctx t (Just u)
pure $ zeroFor ctx
@ -178,7 +178,7 @@ mutual
check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
check' ctx sg (Lam body loc) ty = do
(qty, arg, res) <- expectPi !defs ctx ty.loc ty
(qty, arg, res) <- expectPi !(askAt DEFS) ctx ty.loc ty
-- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
-- with ρ ≤ σπ
let qty' = sg.fst * qty
@ -189,7 +189,7 @@ mutual
check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
check' ctx sg (Pair fst snd loc) ty = do
(tfst, tsnd) <- expectSig !defs ctx ty.loc ty
(tfst, tsnd) <- expectSig !(askAt DEFS) ctx ty.loc ty
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
qfst <- checkC ctx sg fst tfst
let tsnd = sub1 tsnd (Ann fst tfst fst.loc)
@ -201,7 +201,7 @@ mutual
check' ctx sg t@(Enum {}) ty = toCheckType ctx sg t ty
check' ctx sg (Tag t loc) ty = do
tags <- expectEnum !defs ctx ty.loc ty
tags <- expectEnum !(askAt DEFS) ctx ty.loc ty
-- if t ∈ ts
unless (t `elem` tags) $ throw $ TagNotIn loc t tags
-- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
@ -210,7 +210,7 @@ mutual
check' ctx sg t@(Eq {}) ty = toCheckType ctx sg t ty
check' ctx sg (DLam body loc) ty = do
(ty, l, r) <- expectEq !defs ctx ty.loc ty
(ty, l, r) <- expectEq !(askAt DEFS) ctx ty.loc ty
let ctx' = extendDim body.name ctx
ty = ty.term
body = body.term
@ -226,17 +226,17 @@ mutual
check' ctx sg t@(Nat {}) ty = toCheckType ctx sg t ty
check' ctx sg (Zero {}) ty = do
expectNat !defs ctx ty.loc ty
expectNat !(askAt DEFS) ctx ty.loc ty
pure $ zeroFor ctx
check' ctx sg (Succ n {}) ty = do
expectNat !defs ctx ty.loc ty
expectNat !(askAt DEFS) ctx ty.loc ty
checkC ctx sg n ty
check' ctx sg t@(BOX {}) ty = toCheckType ctx sg t ty
check' ctx sg (Box val loc) ty = do
(q, ty) <- expectBOX !defs ctx ty.loc ty
(q, ty) <- expectBOX !(askAt DEFS) ctx ty.loc ty
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
valout <- checkC ctx sg val ty
-- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
@ -314,7 +314,7 @@ mutual
-- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
case u of
Just u => lift $ subtype e.loc ctx infres.type (TYPE u noLoc)
Nothing => ignore $ expectTYPE !defs ctx e.loc infres.type
Nothing => ignore $ expectTYPE !(askAt DEFS) ctx e.loc infres.type
-- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
@ -333,7 +333,7 @@ mutual
infer' ctx sg (F x u loc) = do
-- if π·x : A {≔ s} in global context
g <- lookupFree x loc !defs
g <- lookupFree x loc !(askAt DEFS)
-- if σ ≤ π
expectCompatQ loc sg.fst g.qty.fst
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
@ -355,7 +355,7 @@ mutual
infer' ctx sg (App fun arg loc) = do
-- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
funres <- inferC ctx sg fun
(qty, argty, res) <- expectPi !defs ctx fun.loc funres.type
(qty, argty, res) <- expectPi !(askAt DEFS) ctx fun.loc funres.type
-- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
argout <- checkC ctx (subjMult sg qty) arg argty
-- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + πΣ₂
@ -372,7 +372,7 @@ mutual
pairres <- inferC ctx sg pair
-- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
checkTypeC (extendTy Zero ret.name pairres.type ctx) ret.term Nothing
(tfst, tsnd) <- expectSig !defs ctx pair.loc pairres.type
(tfst, tsnd) <- expectSig !(askAt DEFS) ctx pair.loc pairres.type
-- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
-- ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
-- with ρ₁, ρ₂ ≤ πσ
@ -391,7 +391,7 @@ mutual
infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do
-- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
tres <- inferC ctx sg t
ttags <- expectEnum !defs ctx t.loc tres.type
ttags <- expectEnum !(askAt DEFS) ctx t.loc tres.type
-- if 1 ≤ π, OR there is only zero or one option
unless (length (SortedSet.toList ttags) <= 1) $ expectCompatQ loc One pi
-- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
@ -415,7 +415,7 @@ mutual
-- if Ψ | Γ ⊢ σ · n ⇒ ℕ ⊳ Σn
nres <- inferC ctx sg n
let nat = nres.type
expectNat !defs ctx n.loc nat
expectNat !(askAt DEFS) ctx n.loc nat
-- if Ψ | Γ, n : ℕ ⊢₀ A ⇐ Type
checkTypeC (extendTy Zero ret.name nat ctx) ret.term Nothing
-- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
@ -439,7 +439,7 @@ mutual
infer' ctx sg (CaseBox pi box ret body loc) = do
-- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
boxres <- inferC ctx sg box
(q, ty) <- expectBOX !defs ctx box.loc boxres.type
(q, ty) <- expectBOX !(askAt DEFS) ctx box.loc boxres.type
-- if Ψ | Γ, x : [ρ.A] ⊢₀ R ⇐ Type
checkTypeC (extendTy Zero ret.name boxres.type ctx) ret.term Nothing
-- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
@ -457,7 +457,7 @@ mutual
infer' ctx sg (DApp fun dim loc) = do
-- if Ψ | Γ ⊢ σ · f ⇒ Eq [𝑖 ⇒ A] l r ⊳ Σ
InfRes {type, qout} <- inferC ctx sg fun
ty <- fst <$> expectEq !defs ctx fun.loc type
ty <- fst <$> expectEq !(askAt DEFS) ctx fun.loc type
-- then Ψ | Γ ⊢ σ · f p ⇒ A‹p/𝑖› ⊳ Σ
pure $ InfRes {type = dsub1 ty dim, qout}
@ -485,7 +485,7 @@ mutual
-- if σ = 0
expectEqualQ loc Zero sg.fst
-- if Ψ, Γ ⊢₀ e ⇒ Type u
u <- expectTYPE !defs ctx ty.loc . type =<< inferC ctx szero ty
u <- expectTYPE !(askAt DEFS) ctx ty.loc . type =<< inferC ctx szero ty
-- if Ψ, Γ ⊢₀ C ⇐ Type (non-dependent return type)
checkTypeC ctx ret Nothing
-- if Ψ, Γ' ⊢₀ A ⇐ C for each rhs A

6
lib/Quox/Typing/Context.idr
View file

@ -69,7 +69,7 @@ namespace TContext
zeroFor ctx = Zero <$ ctx
private
extendLen : Telescope a from to -> Singleton from -> Singleton to
extendLen : Telescope a n1 n2 -> Singleton n1 -> Singleton n2
extendLen [<] x = x
extendLen (tel :< _) x = [|S $ extendLen tel x|]
@ -89,7 +89,7 @@ namespace TyContext
null ctx = null ctx.dnames && null ctx.tnames
export %inline
extendTyN : CtxExtension d from to -> TyContext d from -> TyContext d to
extendTyN : CtxExtension d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyN xss (MkTyContext {termLen, dctx, dnames, tctx, tnames, qtys}) =
let (qs, xs, ss) = unzip3 xss in
MkTyContext {
@ -172,7 +172,7 @@ namespace EqContext
null ctx = null ctx.dnames && null ctx.tnames
export %inline
extendTyN : CtxExtension 0 from to -> EqContext from -> EqContext to
extendTyN : CtxExtension 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyN xss (MkEqContext {termLen, dassign, dnames, tctx, tnames, qtys}) =
let (qs, xs, ss) = unzip3 xss in
MkEqContext {

2
tests/Tests/Typechecker.idr
View file

@ -34,7 +34,7 @@ ToInfo Error' where
M = Eff [Except Error', DefsReader]
inj : TC a -> M a
inj act = rethrow $ mapFst TCError $ runTC !defs act
inj act = rethrow $ mapFst TCError $ runTC !(askAt DEFS) act
reflTy : Term d n