Compare commits

...

4 Commits

9 changed files with 199 additions and 96 deletions

View File

@ -15,7 +15,7 @@ import Control.Monad.Identity
infixl 5 :<
||| a sequence of bindings under an existing context. each successive element
||| has one more bound variable, which correspond to all previous elements
||| as well as the global context.
||| as well as the surrounding context.
public export
data Telescope : (tm : Nat -> Type) -> (from, to : Nat) -> Type where
Lin : Telescope tm from from
@ -26,7 +26,7 @@ public export
Telescope' : (a : Type) -> (from, to : Nat) -> Type
Telescope' a = Telescope (\_ => a)
||| a global context is actually just a telescope over no existing bindings
||| a top level context is actually just a telescope over no existing bindings
public export
Context : (tm : Nat -> Type) -> (len : Nat) -> Type
Context tm len = Telescope tm 0 len

52
lib/Quox/Definition.idr Normal file
View File

@ -0,0 +1,52 @@
module Quox.Definition
import public Quox.Syntax
import public Data.SortedMap
import public Control.Monad.State
public export
record AnyTerm where
constructor T
def : forall d, n. Term d n
public export
record Definition where
constructor MkDef'
qty : Qty
0 qtyGlobal : IsGlobal qty
type : AnyTerm
term : Maybe AnyTerm
public export %inline
MkDef : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
(type, term : forall d, n. Term d n) -> Definition
MkDef {qty, type, term} =
MkDef' {qty, qtyGlobal = %search, type = T type, term = Just (T term)}
public export %inline
MkAbstract : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
(type : forall d, n. Term d n) -> Definition
MkAbstract {qty, type} =
MkDef' {qty, qtyGlobal = %search, type = T type, term = Nothing}
public export %inline
(.type0) : Definition -> Term 0 0
g.type0 = g.type.def
public export %inline
(.term0) : Definition -> Maybe (Term 0 0)
g.term0 = map (\t => t.def) g.term
public export %inline
(.qtyP) : Definition -> Subset Qty IsGlobal
g.qtyP = Element g.qty g.qtyGlobal
public export %inline
isZero : Definition -> Bool
isZero g = g.qty == Zero
public export
Definitions : Type
Definitions = SortedMap Name Definition

View File

@ -1,52 +1,72 @@
module Quox.Equal
import public Quox.Syntax
import Control.Monad.Either
import Generics.Derive
import public Quox.Definition
import public Quox.Typing
import public Control.Monad.Either
import public Control.Monad.Reader
import Data.Maybe
%default total
%language ElabReflection
public export
data Mode = Equal | Sub
%runElab derive "Mode" [Generic, Meta, Eq, Ord, DecEq, Show]
public export
data Error
= ClashT Mode (Term d n) (Term d n)
| ClashU Mode Universe Universe
| ClashQ Qty Qty
private %inline
ClashE : Mode -> Elim d n -> Elim d n -> Error
ClashE : EqMode -> Elim d n -> Elim d n -> Error
ClashE mode = ClashT mode `on` E
parameters {auto _ : MonadError Error m}
public export
CanEq : (Type -> Type) -> Type
CanEq m = (MonadError Error m, MonadReader Definitions m)
parameters {auto _ : CanEq m}
private %inline
clashT : Mode -> Term d n -> Term d n -> m a
clashT : EqMode -> Term d n -> Term d n -> m a
clashT mode = throwError .: ClashT mode
private %inline
clashE : Mode -> Elim d n -> Elim d n -> m a
clashE : EqMode -> Elim d n -> Elim d n -> m a
clashE mode = throwError .: ClashE mode
private %inline
defE : Name -> m (Maybe (Elim d n))
defE x = asks $ \defs => do
g <- lookup x defs
pure $ (!g.term).def :# g.type.def
private %inline
defT : Name -> m (Maybe (Term d n))
defT x = map E <$> defE x
export %inline
compareU' : EqMode -> Universe -> Universe -> Bool
compareU' = \case Equal => (==); Sub => (<=)
export %inline
compareU : EqMode -> Universe -> Universe -> m ()
compareU mode k l = unless (compareU' mode k l) $
throwError $ ClashU mode k l
mutual
private covering
compareTN' : Mode ->
compareTN' : EqMode ->
(s, t : Term 0 n) ->
(0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
compareTN' mode (TYPE k) (TYPE l) _ _ =
case mode of
Equal => unless (k == l) $ throwError $ ClashU Equal k l
Sub => unless (k <= l) $ throwError $ ClashU Sub k l
compareTN' mode (E e) (E f) ps pt = compareE0 mode e f
-- if either term is a def, try to unfold it
compareTN' mode s@(E (F x)) t ps pt = do
Just s' <- defT x | Nothing => clashT mode s t
compareT0 mode s' t
compareTN' mode s t@(E (F y)) ps pt = do
Just t' <- defT y | Nothing => clashT mode s t
compareT0 mode s t'
compareTN' mode s@(E _) t _ _ = clashT mode s t
compareTN' mode (TYPE k) (TYPE l) _ _ = compareU mode k l
compareTN' mode s@(TYPE _) t _ _ = clashT mode s t
compareTN' mode (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
-- [todo] this should probably always be ==, right..?
unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
compareT0 mode arg2 arg1 -- reversed for contravariant Sub
compareT0 mode arg2 arg1 -- reversed for contravariant domain
compareTS0 mode res1 res2
compareTN' mode s@(Pi {}) t _ _ = clashT mode s t
@ -55,20 +75,25 @@ parameters {auto _ : MonadError Error m}
compareTS0 Equal body1 body2
compareTN' mode s@(Lam {}) t _ _ = clashT mode s t
compareTN' mode (E e) (E f) ps pt = compareE0 mode e f
compareTN' mode s@(E _) t _ _ = clashT mode s t
compareTN' _ (CloT {}) _ ps _ = void $ ps IsCloT
compareTN' _ (DCloT {}) _ ps _ = void $ ps IsDCloT
private covering
compareEN' : Mode ->
compareEN' : EqMode ->
(e, f : Elim 0 n) ->
(0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
compareEN' mode e@(F x) f@(F y) _ _ =
unless (x == y) $ clashE mode e f
compareEN' mode e@(F _) f _ _ = clashE mode e f
if x == y then pure () else
case (!(defE x), !(defE y)) of
(Nothing, Nothing) => clashE mode e f
(s', t') => compareE0 mode (fromMaybe e s') (fromMaybe f t')
compareEN' mode e@(F x) f _ _ = do
Just e' <- defE x | Nothing => clashE mode e f
compareE0 mode e' f
compareEN' mode e f@(F y) _ _ = do
Just f' <- defE y | Nothing => clashE mode e f
compareE0 mode e f'
compareEN' mode e@(B i) f@(B j) _ _ =
unless (i == j) $ clashE mode e f
@ -92,35 +117,35 @@ parameters {auto _ : MonadError Error m}
private covering %inline
compareTN : Mode -> NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
compareTN : EqMode -> NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
compareTN mode s t = compareTN' mode s.fst t.fst s.snd t.snd
private covering %inline
compareEN : Mode -> NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
compareEN : EqMode -> NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
compareEN mode e f = compareEN' mode e.fst f.fst e.snd f.snd
export covering %inline
compareT : Mode -> DimEq d -> Term d n -> Term d n -> m ()
compareT : EqMode -> DimEq d -> Term d n -> Term d n -> m ()
compareT mode eqs s t =
for_ (splits eqs) $ \th => compareT0 mode (s /// th) (t /// th)
export covering %inline
compareE : Mode -> DimEq d -> Elim d n -> Elim d n -> m ()
compareE : EqMode -> DimEq d -> Elim d n -> Elim d n -> m ()
compareE mode eqs e f =
for_ (splits eqs) $ \th => compareE0 mode (e /// th) (f /// th)
export covering %inline
compareT0 : Mode -> Term 0 n -> Term 0 n -> m ()
compareT0 : EqMode -> Term 0 n -> Term 0 n -> m ()
compareT0 mode s t = compareTN mode (whnfT s) (whnfT t)
export covering %inline
compareE0 : Mode -> Elim 0 n -> Elim 0 n -> m ()
compareE0 : EqMode -> Elim 0 n -> Elim 0 n -> m ()
compareE0 mode e f = compareEN mode (whnfE e) (whnfE f)
export covering %inline
compareTS0 : Mode -> ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
compareTS0 : EqMode -> ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
compareTS0 mode (TUnused body1) (TUnused body2) =
compareT0 mode body1 body2
compareTS0 mode body1 body2 =

View File

@ -74,7 +74,11 @@ data IsSubj : Qty -> Type where
SZero : IsSubj Zero
SOne : IsSubj One
export Uninhabited (IsSubj Any) where uninhabited _ impossible
public export
data IsGlobal : Qty -> Type where
GZero : IsGlobal Zero
GAny : IsGlobal Any
export Uninhabited (IsGlobal One) where uninhabited _ impossible

View File

@ -40,7 +40,7 @@ mutual
sep [!lamD, hl TVar !(prettyM x), !arrowD]
<//> !(under T x $ prettyM t)
prettyM (E e) =
prettyM e
pure $ hl Delim "[" <+> !(prettyM e) <+> hl Delim "]"
prettyM (CloT s th) =
parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM s) </> prettyTSubst th|]

View File

@ -2,9 +2,9 @@ module Quox.Typechecker
import public Quox.Syntax
import public Quox.Typing
import Control.Monad.Either
import public Quox.Equal
import public Control.Monad.Either
%hide Equal.Error
%default total
@ -27,7 +27,7 @@ private %inline
expectEqualQ : MonadError Error m =>
(expect, actual : Qty) -> m ()
expectEqualQ pi rh =
unless (pi == rh) $ throwError $ EqualError $ ClashQ pi rh
unless (pi == rh) $ throwError $ ClashQ pi rh
private %inline
@ -40,12 +40,6 @@ tail : TyContext d (S n) -> TyContext d n
tail = {tctx $= tail, qctx $= tail}
private %inline
globalSubjQty : Global -> Qty
globalSubjQty (MkGlobal {qty = Zero, _}) = Zero
globalSubjQty (MkGlobal {qty = Any, _}) = One
private %inline
weakI : InferResult d n -> InferResult d (S n)
weakI = {type $= weakT, qout $= (:< zero)}
@ -66,30 +60,35 @@ subjMult sg qty =
else Element One %search
mutual
public export
CanTC : (Type -> Type) -> Type
CanTC m = (MonadError Error m, MonadReader Definitions m)
parameters {auto _ : CanTC m}
mutual
-- [todo] it seems like the options here for dealing with substitutions are
-- to either push them or parametrise the whole typechecker over ambient
-- substitutions. both of them seem like the same amount of work for the
-- computer but pushing is less work for the me
export covering %inline
check : MonadError Error m => {d, n : Nat} ->
(ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
check : {d, n : Nat} ->
(ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
(subj : Term d n) -> (ty : Term d n) ->
m (CheckResult n)
check ctx sg subj ty = check' ctx sg (pushSubstsT subj) ty
export covering %inline
infer : MonadError Error m => {d, n : Nat} ->
(ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
infer : {d, n : Nat} ->
(ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
(subj : Elim d n) ->
m (InferResult d n)
infer ctx sg subj = infer' ctx sg (pushSubstsE subj)
export covering
check' : MonadError Error m => {d, n : Nat} ->
(ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
check' : {d, n : Nat} ->
(ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
(subj : NotCloTerm d n) -> (ty : Term d n) ->
m (CheckResult n)
@ -99,7 +98,6 @@ mutual
unless (l < l') $ throwError $ BadUniverse l l'
pure zero
-- [todo] factor this stuff out
check' ctx sg (Element (Pi qty x arg res) _) ty = do
l <- expectTYPE ty
expectEqualQ zero sg
@ -119,21 +117,19 @@ mutual
check' ctx sg (Element (E e) _) ty = do
infres <- infer ctx sg e
ignore $ check ctx zero ty (TYPE UAny)
either (throwError . EqualError) pure $ infres.type `subT` ty
subT infres.type ty
pure infres.qout
export covering
infer' : MonadError Error m => {d, n : Nat} ->
(ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
infer' : {d, n : Nat} ->
(ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
(subj : NotCloElim d n) ->
m (InferResult d n)
infer' ctx sg (Element (F x) _) =
case lookup x ctx.globals of
Just g => do
expectEqualQ (globalSubjQty g) sg
pure $ InfRes {type = g.type, qout = zero}
Nothing => throwError $ NotInScope x
infer' ctx sg (Element (F x) _) = do
Just g <- asks $ lookup x | Nothing => throwError $ NotInScope x
when (isZero g) $ expectEqualQ sg Zero
pure $ InfRes {type = g.type.def, qout = zero}
infer' ctx sg (Element (B i) _) =
pure $ lookupBound sg i ctx

View File

@ -2,12 +2,17 @@ module Quox.Typing
import public Quox.Syntax
import public Quox.Context
import public Quox.Equal
import public Quox.Definition
import Data.Nat
import public Data.SortedMap
import Control.Monad.Reader
import Control.Monad.State
import Generics.Derive
%hide TT.Name
%default total
%language ElabReflection
%default total
@ -31,22 +36,9 @@ QOutput : Nat -> Type
QOutput = QContext
public export
record Global where
constructor MkGlobal
qty : Qty
0 qtyGlobal : IsGlobal qty
type, term : forall d, n. Term d n
public export
Globals : Type
Globals = SortedMap Name Global
public export
record TyContext (d, n : Nat) where
constructor MkTyContext
globals : Globals
dctx : DContext d
tctx : TContext d n
qctx : QContext n
@ -99,11 +91,18 @@ record InferResult d n where
qout : QOutput n
public export
data EqMode = Equal | Sub
%runElab derive "EqMode" [Generic, Meta, Eq, Ord, DecEq, Show]
public export
data Error
= NotInScope Name
| ExpectedTYPE (Term d n)
= ExpectedTYPE (Term d n)
| ExpectedPi (Term d n)
| BadUniverse Universe Universe
| EqualError (Equal.Error)
%hide Equal.Error
| ClashT EqMode (Term d n) (Term d n)
| ClashU EqMode Universe Universe
| ClashQ Qty Qty
| NotInScope Name

View File

@ -26,6 +26,7 @@ modules =
Quox.Syntax.Term.Subst,
Quox.Syntax.Universe,
Quox.Syntax.Var,
Quox.Definition,
Quox.Token,
Quox.Lexer,
Quox.Parser,

View File

@ -5,30 +5,45 @@ import Quox.Pretty
import TAP
export
ToInfo Equal.Error where
ToInfo Error where
toInfo (NotInScope x) =
[("type", "NotInScope"),
("name", show x)]
toInfo (ExpectedTYPE t) =
[("type", "ExpectedTYPE"),
("got", prettyStr True t)]
toInfo (ExpectedPi t) =
[("type", "ExpectedPi"),
("got", prettyStr True t)]
toInfo (BadUniverse k l) =
[("type", "BadUniverse"),
("low", show k),
("high", show l)]
toInfo (ClashT mode s t) =
[("clash", "term"),
[("type", "ClashT"),
("mode", show mode),
("left", prettyStr True s),
("right", prettyStr True t)]
toInfo (ClashU mode k l) =
[("clash", "universe"),
[("type", "ClashU"),
("mode", show mode),
("left", prettyStr True k),
("right", prettyStr True l)]
toInfo (ClashQ pi rh) =
[("clash", "quantity"),
[("type", "ClashQ"),
("left", prettyStr True pi),
("right", prettyStr True rh)]
M = Either Equal.Error
M = ReaderT Definitions (Either Error)
testEq : String -> Lazy (M ()) -> Test
testEq = test
parameters (label : String) (act : Lazy (M ()))
{default empty globals : Definitions}
testEq : Test
testEq = test label $ runReaderT globals act
testNeq : String -> Lazy (M ()) -> Test
testNeq label = testThrows label $ const True
testNeq : Test
testNeq = testThrows label (const True) $ runReaderT globals act
subT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
@ -144,11 +159,22 @@ tests = "equality & subtyping" :- [
todo "term d-closure",
"free var" :- [
"free var" :-
let au_bu = fromList
[("A", MkDef Any (TYPE (U 1)) (TYPE (U 0))),
("B", MkDef Any (TYPE (U 1)) (TYPE (U 0)))]
au_ba = fromList
[("A", MkDef Any (TYPE (U 1)) (TYPE (U 0))),
("B", MkDef Any (TYPE (U 1)) (FT "A"))]
in [
testEq "A ≡ A" $
equalE (F "A") (F "A"),
testNeq "A ≢ B" $
equalE (F "A") (F "B"),
testEq "A ≔ ★₀, B ≔ ★₀ ⊢ A ≡ B" {globals = au_bu} $
equalE (F "A") (F "B"),
testEq "A ≔ ★₀, B ≔ A ⊢ A ≡ B" {globals = au_ba} $
equalE (F "A") (F "B"),
testEq "A <: A" $
subE (F "A") (F "A"),
testNeq "A ≮: B" $