η for pairs #28
|
|
@ -3,6 +3,7 @@ load "misc.quox"
|
|||
namespace eta {
|
||||
|
||||
def0 Π : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) → B x
|
||||
def0 Σ : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) × B x
|
||||
|
||||
def0 function : (A : ★) → (B : A → Type) → (P : Π A B → ★) → (f : Π A B) →
|
||||
P (λ x ⇒ f x) → P f =
|
||||
|
|
@ -12,6 +13,10 @@ def0 box : (A : ★) → (P : [ω.A] → ★) → (e : [ω.A]) →
|
|||
P [case1 e return A of {[x] ⇒ x}] → P e =
|
||||
λ A P e p ⇒ p
|
||||
|
||||
def0 pair : (A : ★) → (B : A → ★) → (P : Σ A B → ★) → (e : Σ A B) →
|
||||
P (fst e, snd e) → P e =
|
||||
λ A B P e p ⇒ p
|
||||
|
||||
-- not exactly η, but kinda related
|
||||
def0 from-false : (A : ★) → (P : (False → A) → ★) → (f : False → A) →
|
||||
P (λ x ⇒ void A x) → P f =
|
||||
|
|
|
|||
|
|
@ -2,18 +2,21 @@ namespace pair {
|
|||
|
||||
def0 Σ : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) × B x;
|
||||
|
||||
{-
|
||||
-- now builtins
|
||||
def fst : 0.(A : ★) → 0.(B : A → ★) → ω.(Σ A B) → A =
|
||||
λ A B p ⇒ caseω p return A of { (x, _) ⇒ x };
|
||||
|
||||
def snd : 0.(A : ★) → 0.(B : A → ★) → ω.(p : Σ A B) → B (fst A B p) =
|
||||
λ A B p ⇒ caseω p return p' ⇒ B (fst A B p') of { (_, y) ⇒ y };
|
||||
-}
|
||||
|
||||
def uncurry :
|
||||
0.(A : ★) → 0.(B : A → ★) → 0.(C : (x : A) → (B x) → ★) →
|
||||
(f : (x : A) → (y : B x) → C x y) →
|
||||
(p : Σ A B) → C (fst A B p) (snd A B p) =
|
||||
(p : Σ A B) → C (fst p) (snd p) =
|
||||
λ A B C f p ⇒
|
||||
case p return p' ⇒ C (fst A B p') (snd A B p') of { (x, y) ⇒ f x y };
|
||||
case p return p' ⇒ C (fst p') (snd p') of { (x, y) ⇒ f x y };
|
||||
|
||||
def uncurry' :
|
||||
0.(A B C : ★) → (A → B → C) → (A × B) → C =
|
||||
|
|
@ -30,22 +33,22 @@ def curry' :
|
|||
|
||||
def0 fst-snd :
|
||||
(A : ★) → (B : A → ★) →
|
||||
(p : Σ A B) → p ≡ (fst A B p, snd A B p) : Σ A B =
|
||||
(p : Σ A B) → p ≡ (fst p, snd p) : Σ A B =
|
||||
λ A B p ⇒
|
||||
case p
|
||||
return p' ⇒ p' ≡ (fst A B p', snd A B p') : Σ A B
|
||||
return p' ⇒ p' ≡ (fst p', snd p') : Σ A B
|
||||
of { (x, y) ⇒ δ 𝑖 ⇒ (x, y) };
|
||||
|
||||
def0 fst-eq :
|
||||
(A : ★) → (B : A → ★) →
|
||||
(p q : Σ A B) → p ≡ q : Σ A B → fst A B p ≡ fst A B q : A =
|
||||
λ A B p q eq ⇒ δ 𝑖 ⇒ fst A B (eq @𝑖);
|
||||
(p q : Σ A B) → p ≡ q : Σ A B → fst p ≡ fst q : A =
|
||||
λ A B p q eq ⇒ δ 𝑖 ⇒ fst (eq @𝑖);
|
||||
|
||||
def0 snd-eq :
|
||||
(A : ★) → (B : A → ★) →
|
||||
(p q : Σ A B) → (eq : p ≡ q : Σ A B) →
|
||||
Eq (𝑖 ⇒ B (fst-eq A B p q eq @𝑖)) (snd A B p) (snd A B q) =
|
||||
λ A B p q eq ⇒ δ 𝑖 ⇒ snd A B (eq @𝑖);
|
||||
Eq (𝑖 ⇒ B (fst-eq A B p q eq @𝑖)) (snd p) (snd q) =
|
||||
λ A B p q eq ⇒ δ 𝑖 ⇒ snd (eq @𝑖);
|
||||
|
||||
def map :
|
||||
0.(A A' : ★) →
|
||||
|
|
@ -61,5 +64,5 @@ def map' : 0.(A A' B B' : ★) → (A → A') → (B → B') → (A × B) → A'
|
|||
}
|
||||
|
||||
def0 Σ = pair.Σ;
|
||||
def fst = pair.fst;
|
||||
def snd = pair.snd;
|
||||
-- def fst = pair.fst;
|
||||
-- def snd = pair.snd;
|
||||
|
|
|
|||
|
|
@ -23,9 +23,9 @@ die : Doc Opts -> IO a
|
|||
die err = do putDoc err; exitFailure
|
||||
|
||||
private
|
||||
prettySig : {opts : _} -> Name -> Definition -> Eff Pretty (Doc opts)
|
||||
prettySig : Name -> Definition -> Eff Pretty (Doc Opts)
|
||||
prettySig name def = do
|
||||
qty <- prettyQty def.qty.fst
|
||||
qty <- prettyQty def.qty.qty
|
||||
name <- prettyFree name
|
||||
type <- prettyTerm [<] [<] def.type
|
||||
hangDSingle (hsep [hcat [qty, !dotD, name], !colonD]) type
|
||||
|
|
|
|||
|
|
@ -0,0 +1,64 @@
|
|||
module Control.Monad.ST.Extra
|
||||
|
||||
import public Control.Monad.ST
|
||||
import Data.IORef
|
||||
import Control.MonadRec
|
||||
|
||||
%default total
|
||||
|
||||
export %inline
|
||||
MonadRec (ST s) where
|
||||
tailRecM seed (Access rec) st f = MkST $ do
|
||||
let MkST io = f seed st
|
||||
case !io of
|
||||
Done res => pure res
|
||||
Cont seed2 prf vst =>
|
||||
let MkST io = tailRecM seed2 (rec seed2 prf) vst f in io
|
||||
|
||||
|
||||
public export
|
||||
interface HasST (0 m : Type -> Type -> Type) where
|
||||
liftST : ST s a -> m s a
|
||||
|
||||
export %inline HasST ST where liftST = id
|
||||
|
||||
|
||||
public export
|
||||
record STErr e s a where
|
||||
constructor STE
|
||||
fromSTErr : ST s (Either e a)
|
||||
|
||||
export
|
||||
Functor (STErr e s) where
|
||||
map f (STE e) = STE $ map f <$> e
|
||||
|
||||
export
|
||||
Applicative (STErr e s) where
|
||||
pure x = STE $ pure $ pure x
|
||||
STE f <*> STE x = STE [|f <*> x|]
|
||||
|
||||
export
|
||||
Monad (STErr e s) where
|
||||
STE m >>= k = STE $ do
|
||||
case !m of
|
||||
Left err => pure $ Left err
|
||||
Right x => fromSTErr $ k x
|
||||
|
||||
export
|
||||
MonadRec (STErr e s) where
|
||||
tailRecM s (Access r) x k = STE $ do
|
||||
let STE m = k s x
|
||||
case !m of
|
||||
Left err => pure $ Left err
|
||||
Right (Cont s' p y) => fromSTErr $ tailRecM s' (r s' p) y k
|
||||
Right (Done y) => pure $ Right y
|
||||
|
||||
export
|
||||
runSTErr : (forall s. STErr e s a) -> Either e a
|
||||
runSTErr ste = runST $ fromSTErr ste
|
||||
|
||||
export %inline HasST (STErr e) where liftST = STE . map Right
|
||||
|
||||
export
|
||||
stLeft : e -> STErr e s a
|
||||
stLeft e = STE $ pure $ Left e
|
||||
|
|
@ -65,7 +65,7 @@ parameters {d, n : Nat}
|
|||
|
||||
public export %inline
|
||||
isZero : Definition -> Bool
|
||||
isZero g = g.qty.fst == Zero
|
||||
isZero g = g.qty == GZero
|
||||
|
||||
|
||||
public export
|
||||
|
|
|
|||
|
|
@ -49,6 +49,8 @@ parameters (k : Universe)
|
|||
doDisplace (App fun arg loc) = App (doDisplace fun) (doDisplace arg) loc
|
||||
doDisplace (CasePair qty pair ret body loc) =
|
||||
CasePair qty (doDisplace pair) (doDisplaceS ret) (doDisplaceS body) loc
|
||||
doDisplace (Fst pair loc) = Fst (doDisplace pair) loc
|
||||
doDisplace (Snd pair loc) = Snd (doDisplace pair) loc
|
||||
doDisplace (CaseEnum qty tag ret arms loc) =
|
||||
CaseEnum qty (doDisplace tag) (doDisplaceS ret)
|
||||
(assert_total $ map doDisplace arms) loc
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@ module Quox.EffExtra
|
|||
|
||||
import public Control.Eff
|
||||
|
||||
import Quox.ST
|
||||
import Control.Monad.ST.Extra
|
||||
import Data.IORef
|
||||
|
||||
|
||||
|
|
@ -43,8 +43,8 @@ handleStateIORef r (Put s) = writeIORef r s
|
|||
|
||||
export
|
||||
handleStateSTRef : HasST m => STRef s st -> StateL lbl st a -> m s a
|
||||
handleStateSTRef r Get = readRef r
|
||||
handleStateSTRef r (Put s) = writeRef r s
|
||||
handleStateSTRef r Get = liftST $ readSTRef r
|
||||
handleStateSTRef r (Put s) = liftST $ writeSTRef r s
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -70,22 +70,22 @@ sameTyCon (E {}) _ = False
|
|||
||| * `[π.A]` is empty if `A` is.
|
||||
||| * that's it.
|
||||
public export covering
|
||||
isEmpty : {n : Nat} -> Definitions -> EqContext n -> Term 0 n ->
|
||||
isEmpty : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
|
||||
Eff EqualInner Bool
|
||||
isEmpty defs ctx ty0 = do
|
||||
Element ty0 nc <- whnf defs ctx ty0.loc ty0
|
||||
isEmpty defs ctx sg ty0 = do
|
||||
Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
|
||||
case ty0 of
|
||||
TYPE {} => pure False
|
||||
Pi {arg, res, _} => pure False
|
||||
Sig {fst, snd, _} =>
|
||||
isEmpty defs ctx fst `orM`
|
||||
isEmpty defs (extendTy0 snd.name fst ctx) snd.term
|
||||
isEmpty defs ctx sg fst `orM`
|
||||
isEmpty defs (extendTy0 snd.name fst ctx) sg snd.term
|
||||
Enum {cases, _} =>
|
||||
pure $ null cases
|
||||
Eq {} => pure False
|
||||
Nat {} => pure False
|
||||
BOX {ty, _} => isEmpty defs ctx ty
|
||||
E (Ann {tm, _}) => isEmpty defs ctx tm
|
||||
BOX {ty, _} => isEmpty defs ctx sg ty
|
||||
E (Ann {tm, _}) => isEmpty defs ctx sg tm
|
||||
E _ => pure False
|
||||
Lam {} => pure False
|
||||
Pair {} => pure False
|
||||
|
|
@ -106,24 +106,24 @@ isEmpty defs ctx ty0 = do
|
|||
||| * an enum type is a subsingleton if it has zero or one tags.
|
||||
||| * a box type is a subsingleton if its content is
|
||||
public export covering
|
||||
isSubSing : {n : Nat} -> Definitions -> EqContext n -> Term 0 n ->
|
||||
isSubSing : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
|
||||
Eff EqualInner Bool
|
||||
isSubSing defs ctx ty0 = do
|
||||
Element ty0 nc <- whnf defs ctx ty0.loc ty0
|
||||
isSubSing defs ctx sg ty0 = do
|
||||
Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
|
||||
case ty0 of
|
||||
TYPE {} => pure False
|
||||
Pi {arg, res, _} =>
|
||||
isEmpty defs ctx arg `orM`
|
||||
isSubSing defs (extendTy0 res.name arg ctx) res.term
|
||||
isEmpty defs ctx sg arg `orM`
|
||||
isSubSing defs (extendTy0 res.name arg ctx) sg res.term
|
||||
Sig {fst, snd, _} =>
|
||||
isSubSing defs ctx fst `andM`
|
||||
isSubSing defs (extendTy0 snd.name fst ctx) snd.term
|
||||
isSubSing defs ctx sg fst `andM`
|
||||
isSubSing defs (extendTy0 snd.name fst ctx) sg snd.term
|
||||
Enum {cases, _} =>
|
||||
pure $ length (SortedSet.toList cases) <= 1
|
||||
Eq {} => pure True
|
||||
Nat {} => pure False
|
||||
BOX {ty, _} => isSubSing defs ctx ty
|
||||
E (Ann {tm, _}) => isSubSing defs ctx tm
|
||||
BOX {ty, _} => isSubSing defs ctx sg ty
|
||||
E (Ann {tm, _}) => isSubSing defs ctx sg tm
|
||||
E _ => pure False
|
||||
Lam {} => pure False
|
||||
Pair {} => pure False
|
||||
|
|
@ -155,7 +155,7 @@ namespace Term
|
|||
|||
|
||||
||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
|
||||
export covering %inline
|
||||
compare0 : Definitions -> EqContext n -> (ty, s, t : Term 0 n) ->
|
||||
compare0 : Definitions -> EqContext n -> SQty -> (ty, s, t : Term 0 n) ->
|
||||
Eff EqualInner ()
|
||||
|
||||
namespace Elim
|
||||
|
|
@ -164,7 +164,7 @@ namespace Elim
|
|||
||| ⚠ **assumes that they have both been typechecked, and have
|
||||
||| equal types.** ⚠
|
||||
export covering %inline
|
||||
compare0 : Definitions -> EqContext n -> (e, f : Elim 0 n) ->
|
||||
compare0 : Definitions -> EqContext n -> SQty -> (e, f : Elim 0 n) ->
|
||||
Eff EqualInner (Term 0 n)
|
||||
|
||||
||| compares two types, using the current variance `mode` for universes.
|
||||
|
|
@ -176,14 +176,14 @@ compareType : Definitions -> EqContext n -> (s, t : Term 0 n) ->
|
|||
|
||||
namespace Term
|
||||
private covering
|
||||
compare0' : (defs : Definitions) -> EqContext n ->
|
||||
compare0' : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
|
||||
(ty, s, t : Term 0 n) ->
|
||||
(0 _ : NotRedex defs ty) => (0 _ : So (isTyConE ty)) =>
|
||||
(0 _ : NotRedex defs s) => (0 _ : NotRedex defs t) =>
|
||||
(0 _ : NotRedex defs SZero ty) => (0 _ : So (isTyConE ty)) =>
|
||||
(0 _ : NotRedex defs sg s) => (0 _ : NotRedex defs sg t) =>
|
||||
Eff EqualInner ()
|
||||
compare0' defs ctx (TYPE {}) s t = compareType defs ctx s t
|
||||
compare0' defs ctx sg (TYPE {}) s t = compareType defs ctx s t
|
||||
|
||||
compare0' defs ctx ty@(Pi {qty, arg, res, _}) s t = local_ Equal $
|
||||
compare0' defs ctx sg ty@(Pi {qty, arg, res, _}) s t = local_ Equal $
|
||||
-- Γ ⊢ A empty
|
||||
-- -------------------------------------------
|
||||
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
|
||||
|
|
@ -193,7 +193,7 @@ namespace Term
|
|||
-- -------------------------------------------
|
||||
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
|
||||
(Lam b1 {}, Lam b2 {}) =>
|
||||
compare0 defs ctx' res.term b1.term b2.term
|
||||
compare0 defs ctx' sg res.term b1.term b2.term
|
||||
|
||||
-- Γ, x : A ⊢ s = e x : B
|
||||
-- -----------------------------------
|
||||
|
|
@ -201,14 +201,14 @@ namespace Term
|
|||
(E e, Lam b {}) => eta s.loc e b
|
||||
(Lam b {}, E e) => eta s.loc e b
|
||||
|
||||
(E e, E f) => ignore $ Elim.compare0 defs ctx e f
|
||||
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
|
||||
|
||||
(Lam {}, t) => wrongType t.loc ctx ty t
|
||||
(E _, t) => wrongType t.loc ctx ty t
|
||||
(s, _) => wrongType s.loc ctx ty s
|
||||
where
|
||||
isEmpty' : Term 0 n -> Eff EqualInner Bool
|
||||
isEmpty' t = let Val n = ctx.termLen in isEmpty defs ctx arg
|
||||
isEmpty' t = let Val n = ctx.termLen in isEmpty defs ctx sg arg
|
||||
|
||||
ctx' : EqContext (S n)
|
||||
ctx' = extendTy qty res.name arg ctx
|
||||
|
|
@ -218,9 +218,9 @@ namespace Term
|
|||
|
||||
eta : Loc -> Elim 0 n -> ScopeTerm 0 n -> Eff EqualInner ()
|
||||
eta loc e (S _ (N _)) = clashT loc ctx ty s t
|
||||
eta _ e (S _ (Y b)) = compare0 defs ctx' res.term (toLamBody e) b
|
||||
eta _ e (S _ (Y b)) = compare0 defs ctx' sg res.term (toLamBody e) b
|
||||
|
||||
compare0' defs ctx ty@(Sig {fst, snd, _}) s t = local_ Equal $
|
||||
compare0' defs ctx sg ty@(Sig {fst, snd, _}) s t = local_ Equal $
|
||||
case (s, t) of
|
||||
-- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x}
|
||||
-- --------------------------------------------
|
||||
|
|
@ -228,19 +228,27 @@ namespace Term
|
|||
--
|
||||
-- [todo] η for π ≥ 0 maybe
|
||||
(Pair sFst sSnd {}, Pair tFst tSnd {}) => do
|
||||
compare0 defs ctx fst sFst tFst
|
||||
compare0 defs ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
|
||||
compare0 defs ctx sg fst sFst tFst
|
||||
compare0 defs ctx sg (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
|
||||
|
||||
(E e, E f) => ignore $ Elim.compare0 defs ctx e f
|
||||
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
|
||||
|
||||
(Pair {}, E _) => clashT s.loc ctx ty s t
|
||||
(E _, Pair {}) => clashT s.loc ctx ty s t
|
||||
(E e, Pair fst snd _) => eta s.loc e fst snd
|
||||
(Pair fst snd _, E f) => eta s.loc f fst snd
|
||||
|
||||
(Pair {}, t) => wrongType t.loc ctx ty t
|
||||
(E _, t) => wrongType t.loc ctx ty t
|
||||
(s, _) => wrongType s.loc ctx ty s
|
||||
where
|
||||
eta : Loc -> Elim 0 n -> Term 0 n -> Term 0 n -> Eff EqualInner ()
|
||||
eta loc e s t =
|
||||
case sg of
|
||||
SZero => do
|
||||
compare0 defs ctx sg fst (E $ Fst e e.loc) s
|
||||
compare0 defs ctx sg (sub1 snd (Ann s fst s.loc)) (E $ Snd e e.loc) t
|
||||
SOne => clashT loc ctx ty s t
|
||||
|
||||
compare0' defs ctx ty@(Enum {}) s t = local_ Equal $
|
||||
compare0' defs ctx sg ty@(Enum {}) s t = local_ Equal $
|
||||
case (s, t) of
|
||||
-- --------------------
|
||||
-- Γ ⊢ `t = `t : {ts}
|
||||
|
|
@ -248,7 +256,7 @@ namespace Term
|
|||
-- t ∈ ts is in the typechecker, not here, ofc
|
||||
(Tag t1 {}, Tag t2 {}) =>
|
||||
unless (t1 == t2) $ clashT s.loc ctx ty s t
|
||||
(E e, E f) => ignore $ Elim.compare0 defs ctx e f
|
||||
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
|
||||
|
||||
(Tag {}, E _) => clashT s.loc ctx ty s t
|
||||
(E _, Tag {}) => clashT s.loc ctx ty s t
|
||||
|
|
@ -257,14 +265,14 @@ namespace Term
|
|||
(E _, t) => wrongType t.loc ctx ty t
|
||||
(s, _) => wrongType s.loc ctx ty s
|
||||
|
||||
compare0' _ _ (Eq {}) _ _ =
|
||||
compare0' _ _ _ (Eq {}) _ _ =
|
||||
-- ✨ uip ✨
|
||||
--
|
||||
-- ----------------------------
|
||||
-- Γ ⊢ e = f : Eq [i ⇒ A] s t
|
||||
pure ()
|
||||
|
||||
compare0' defs ctx nat@(Nat {}) s t = local_ Equal $
|
||||
compare0' defs ctx sg nat@(Nat {}) s t = local_ Equal $
|
||||
case (s, t) of
|
||||
-- ---------------
|
||||
-- Γ ⊢ 0 = 0 : ℕ
|
||||
|
|
@ -273,9 +281,9 @@ namespace Term
|
|||
-- Γ ⊢ s = t : ℕ
|
||||
-- -------------------------
|
||||
-- Γ ⊢ succ s = succ t : ℕ
|
||||
(Succ s' {}, Succ t' {}) => compare0 defs ctx nat s' t'
|
||||
(Succ s' {}, Succ t' {}) => compare0 defs ctx sg nat s' t'
|
||||
|
||||
(E e, E f) => ignore $ Elim.compare0 defs ctx e f
|
||||
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
|
||||
|
||||
(Zero {}, Succ {}) => clashT s.loc ctx nat s t
|
||||
(Zero {}, E _) => clashT s.loc ctx nat s t
|
||||
|
|
@ -289,12 +297,12 @@ namespace Term
|
|||
(E _, t) => wrongType t.loc ctx nat t
|
||||
(s, _) => wrongType s.loc ctx nat s
|
||||
|
||||
compare0' defs ctx bty@(BOX q ty {}) s t = local_ Equal $
|
||||
compare0' defs ctx sg bty@(BOX q ty {}) s t = local_ Equal $
|
||||
case (s, t) of
|
||||
-- Γ ⊢ s = t : A
|
||||
-- -----------------------
|
||||
-- Γ ⊢ [s] = [t] : [π.A]
|
||||
(Box s _, Box t _) => compare0 defs ctx ty s t
|
||||
(Box s _, Box t _) => compare0 defs ctx sg ty s t
|
||||
|
||||
-- Γ ⊢ s = (case1 e return A of {[x] ⇒ x}) ⇐ A
|
||||
-- -----------------------------------------------
|
||||
|
|
@ -302,7 +310,7 @@ namespace Term
|
|||
(Box s loc, E f) => eta s f
|
||||
(E e, Box t loc) => eta t e
|
||||
|
||||
(E e, E f) => ignore $ Elim.compare0 defs ctx e f
|
||||
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
|
||||
|
||||
(Box {}, _) => wrongType t.loc ctx bty t
|
||||
(E _, _) => wrongType t.loc ctx bty t
|
||||
|
|
@ -312,20 +320,20 @@ namespace Term
|
|||
eta s e = do
|
||||
nm <- mnb "inner" e.loc
|
||||
let e = CaseBox One e (SN ty) (SY [< nm] (BVT 0 nm.loc)) e.loc
|
||||
compare0 defs ctx ty s (E e)
|
||||
compare0 defs ctx sg ty s (E e)
|
||||
|
||||
compare0' defs ctx ty@(E _) s t = do
|
||||
compare0' defs ctx sg ty@(E _) s t = do
|
||||
-- a neutral type can only be inhabited by neutral values
|
||||
-- e.g. an abstract value in an abstract type, bound variables, …
|
||||
let E e = s | _ => wrongType s.loc ctx ty s
|
||||
E f = t | _ => wrongType t.loc ctx ty t
|
||||
ignore $ Elim.compare0 defs ctx e f
|
||||
ignore $ Elim.compare0 defs ctx sg e f
|
||||
|
||||
|
||||
private covering
|
||||
compareType' : (defs : Definitions) -> EqContext n -> (s, t : Term 0 n) ->
|
||||
(0 _ : NotRedex defs s) => (0 _ : So (isTyConE s)) =>
|
||||
(0 _ : NotRedex defs t) => (0 _ : So (isTyConE t)) =>
|
||||
(0 _ : NotRedex defs SZero s) => (0 _ : So (isTyConE s)) =>
|
||||
(0 _ : NotRedex defs SZero t) => (0 _ : So (isTyConE t)) =>
|
||||
(0 _ : So (sameTyCon s t)) =>
|
||||
Eff EqualInner ()
|
||||
-- equality is the same as subtyping, except with the
|
||||
|
|
@ -363,8 +371,8 @@ compareType' defs ctx (Eq {ty = sTy, l = sl, r = sr, _})
|
|||
compareType defs (extendDim sTy.name One ctx) sTy.one tTy.one
|
||||
ty <- bigger sTy tTy
|
||||
local_ Equal $ do
|
||||
Term.compare0 defs ctx ty.zero sl tl
|
||||
Term.compare0 defs ctx ty.one sr tr
|
||||
Term.compare0 defs ctx SZero ty.zero sl tl
|
||||
Term.compare0 defs ctx SZero ty.one sr tr
|
||||
|
||||
compareType' defs ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do
|
||||
-- ------------------
|
||||
|
|
@ -386,7 +394,7 @@ compareType' defs ctx (BOX pi a loc) (BOX rh b {}) = do
|
|||
compareType' defs ctx (E e) (E f) = do
|
||||
-- no fanciness needed here cos anything other than a neutral
|
||||
-- has been inlined by whnf
|
||||
ignore $ Elim.compare0 defs ctx e f
|
||||
ignore $ Elim.compare0 defs ctx SZero e f
|
||||
|
||||
|
||||
private
|
||||
|
|
@ -411,12 +419,12 @@ namespace Elim
|
|||
EqualElim = InnerErrEff :: EqualInner
|
||||
|
||||
private covering
|
||||
computeElimTypeE : (defs : Definitions) -> EqContext n ->
|
||||
(e : Elim 0 n) -> (0 ne : NotRedex defs e) =>
|
||||
computeElimTypeE : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
|
||||
(e : Elim 0 n) -> (0 ne : NotRedex defs sg e) =>
|
||||
Eff EqualElim (Term 0 n)
|
||||
computeElimTypeE defs ectx e =
|
||||
computeElimTypeE defs ectx sg e =
|
||||
let Val n = ectx.termLen in
|
||||
lift $ computeElimType defs (toWhnfContext ectx) e
|
||||
lift $ computeElimType defs (toWhnfContext ectx) sg e
|
||||
|
||||
private
|
||||
putError : Has InnerErrEff fs => Error -> Eff fs ()
|
||||
|
|
@ -427,12 +435,12 @@ namespace Elim
|
|||
try act = lift $ catch putError $ lift act {fs' = EqualElim}
|
||||
|
||||
private covering %inline
|
||||
clashE : (defs : Definitions) -> EqContext n ->
|
||||
(e, f : Elim 0 n) -> (0 nf : NotRedex defs f) =>
|
||||
clashE : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
|
||||
(e, f : Elim 0 n) -> (0 nf : NotRedex defs sg f) =>
|
||||
Eff EqualElim (Term 0 n)
|
||||
clashE defs ctx e f = do
|
||||
clashE defs ctx sg e f = do
|
||||
putError $ ClashE e.loc ctx !mode e f
|
||||
computeElimTypeE defs ctx f
|
||||
computeElimTypeE defs ctx sg f
|
||||
|
||||
|
||||
||| compare two type-case branches, which came from the arms of the given
|
||||
|
|
@ -454,24 +462,24 @@ namespace Elim
|
|||
(b1, b2 : TypeCaseArmBody k 0 n) ->
|
||||
Eff EqualElim ()
|
||||
compareArm_ defs ctx KTYPE ret u b1 b2 =
|
||||
try $ Term.compare0 defs ctx ret b1.term b2.term
|
||||
try $ Term.compare0 defs ctx SZero ret b1.term b2.term
|
||||
|
||||
compareArm_ defs ctx KPi ret u b1 b2 = do
|
||||
let [< a, b] = b1.names
|
||||
ctx = extendTyN0
|
||||
[< (a, TYPE u a.loc),
|
||||
(b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
|
||||
try $ Term.compare0 defs ctx (weakT 2 ret) b1.term b2.term
|
||||
try $ Term.compare0 defs ctx SZero (weakT 2 ret) b1.term b2.term
|
||||
|
||||
compareArm_ defs ctx KSig ret u b1 b2 = do
|
||||
let [< a, b] = b1.names
|
||||
ctx = extendTyN0
|
||||
[< (a, TYPE u a.loc),
|
||||
(b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
|
||||
try $ Term.compare0 defs ctx (weakT 2 ret) b1.term b2.term
|
||||
try $ Term.compare0 defs ctx SZero (weakT 2 ret) b1.term b2.term
|
||||
|
||||
compareArm_ defs ctx KEnum ret u b1 b2 =
|
||||
try $ Term.compare0 defs ctx ret b1.term b2.term
|
||||
try $ Term.compare0 defs ctx SZero ret b1.term b2.term
|
||||
|
||||
compareArm_ defs ctx KEq ret u b1 b2 = do
|
||||
let [< a0, a1, a, l, r] = b1.names
|
||||
|
|
@ -481,45 +489,45 @@ namespace Elim
|
|||
(a, Eq0 (TYPE u a.loc) (BVT 1 a0.loc) (BVT 0 a1.loc) a.loc),
|
||||
(l, BVT 2 a0.loc),
|
||||
(r, BVT 2 a1.loc)] ctx
|
||||
try $ Term.compare0 defs ctx (weakT 5 ret) b1.term b2.term
|
||||
try $ Term.compare0 defs ctx SZero (weakT 5 ret) b1.term b2.term
|
||||
|
||||
compareArm_ defs ctx KNat ret u b1 b2 =
|
||||
try $ Term.compare0 defs ctx ret b1.term b2.term
|
||||
try $ Term.compare0 defs ctx SZero ret b1.term b2.term
|
||||
|
||||
compareArm_ defs ctx KBOX ret u b1 b2 = do
|
||||
let ctx = extendTy0 b1.name (TYPE u b1.name.loc) ctx
|
||||
try $ Term.compare0 defs ctx (weakT 1 ret) b1.term b1.term
|
||||
try $ Term.compare0 defs ctx SZero (weakT 1 ret) b1.term b1.term
|
||||
|
||||
|
||||
private covering
|
||||
compare0Inner : Definitions -> EqContext n -> (e, f : Elim 0 n) ->
|
||||
Eff EqualElim (Term 0 n)
|
||||
compare0Inner : Definitions -> EqContext n -> (sg : SQty) ->
|
||||
(e, f : Elim 0 n) -> Eff EqualElim (Term 0 n)
|
||||
|
||||
private covering
|
||||
compare0Inner' : (defs : Definitions) -> EqContext n ->
|
||||
compare0Inner' : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
|
||||
(e, f : Elim 0 n) ->
|
||||
(0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
|
||||
(0 ne : NotRedex defs sg e) -> (0 nf : NotRedex defs sg f) ->
|
||||
Eff EqualElim (Term 0 n)
|
||||
|
||||
compare0Inner' defs ctx e@(F {}) f _ _ = do
|
||||
if e == f then computeElimTypeE defs ctx f
|
||||
else clashE defs ctx e f
|
||||
compare0Inner' defs ctx sg e@(F {}) f _ _ = do
|
||||
if e == f then computeElimTypeE defs ctx sg f
|
||||
else clashE defs ctx sg e f
|
||||
|
||||
compare0Inner' defs ctx e@(B {}) f _ _ = do
|
||||
if e == f then computeElimTypeE defs ctx f
|
||||
else clashE defs ctx e f
|
||||
compare0Inner' defs ctx sg e@(B {}) f _ _ = do
|
||||
if e == f then computeElimTypeE defs ctx sg f
|
||||
else clashE defs ctx sg e f
|
||||
|
||||
-- Ψ | Γ ⊢ e = f ⇒ π.(x : A) → B
|
||||
-- Ψ | Γ ⊢ s = t ⇐ A
|
||||
-- -------------------------------
|
||||
-- Ψ | Γ ⊢ e s = f t ⇒ B[s∷A/x]
|
||||
compare0Inner' defs ctx (App e s eloc) (App f t floc) ne nf = do
|
||||
ety <- compare0Inner defs ctx e f
|
||||
(_, arg, res) <- expectPi defs ctx eloc ety
|
||||
try $ Term.compare0 defs ctx arg s t
|
||||
compare0Inner' defs ctx sg (App e s eloc) (App f t floc) ne nf = do
|
||||
ety <- compare0Inner defs ctx sg e f
|
||||
(_, arg, res) <- expectPi defs ctx sg eloc ety
|
||||
try $ Term.compare0 defs ctx sg arg s t
|
||||
pure $ sub1 res $ Ann s arg s.loc
|
||||
compare0Inner' defs ctx e'@(App {}) f' ne nf =
|
||||
clashE defs ctx e' f'
|
||||
compare0Inner' defs ctx sg e'@(App {}) f' ne nf =
|
||||
clashE defs ctx sg e' f'
|
||||
|
||||
-- Ψ | Γ ⊢ e = f ⇒ (x : A) × B
|
||||
-- Ψ | Γ, 0.p : (x : A) × B ⊢ Q = R
|
||||
|
|
@ -527,22 +535,43 @@ namespace Elim
|
|||
-- -----------------------------------------------------------
|
||||
-- Ψ | Γ ⊢ caseπ e return Q of { (x, y) ⇒ s }
|
||||
-- = caseπ f return R of { (x, y) ⇒ t } ⇒ Q[e/p]
|
||||
compare0Inner' defs ctx (CasePair epi e eret ebody eloc)
|
||||
(CasePair fpi f fret fbody floc) ne nf =
|
||||
compare0Inner' defs ctx sg (CasePair epi e eret ebody eloc)
|
||||
(CasePair fpi f fret fbody floc) ne nf =
|
||||
local_ Equal $ do
|
||||
ety <- compare0Inner defs ctx e f
|
||||
(fst, snd) <- expectSig defs ctx eloc ety
|
||||
ety <- compare0Inner defs ctx sg e f
|
||||
(fst, snd) <- expectSig defs ctx sg eloc ety
|
||||
let [< x, y] = ebody.names
|
||||
try $ do
|
||||
compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
|
||||
Term.compare0 defs
|
||||
(extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
|
||||
(extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx) sg
|
||||
(substCasePairRet ebody.names ety eret)
|
||||
ebody.term fbody.term
|
||||
expectEqualQ e.loc epi fpi
|
||||
pure $ sub1 eret e
|
||||
compare0Inner' defs ctx e'@(CasePair {}) f' ne nf =
|
||||
clashE defs ctx e' f'
|
||||
compare0Inner' defs ctx sg e'@(CasePair {}) f' ne nf =
|
||||
clashE defs ctx sg e' f'
|
||||
|
||||
-- Ψ | Γ ⊢ e = f ⇒ (x : A) × B
|
||||
-- ------------------------------
|
||||
-- Ψ | Γ ⊢ fst e = fst f ⇒ A
|
||||
compare0Inner' defs ctx sg (Fst e eloc) (Fst f floc) ne nf =
|
||||
local_ Equal $ do
|
||||
ety <- compare0Inner defs ctx sg e f
|
||||
fst <$> expectSig defs ctx sg eloc ety
|
||||
compare0Inner' defs ctx sg e@(Fst {}) f _ _ =
|
||||
clashE defs ctx sg e f
|
||||
|
||||
-- Ψ | Γ ⊢ e = f ⇒ (x : A) × B
|
||||
-- ------------------------------------
|
||||
-- Ψ | Γ ⊢ snd e = snd f ⇒ B[fst e/x]
|
||||
compare0Inner' defs ctx sg (Snd e eloc) (Snd f floc) ne nf =
|
||||
local_ Equal $ do
|
||||
ety <- compare0Inner defs ctx sg e f
|
||||
(_, tsnd) <- expectSig defs ctx sg eloc ety
|
||||
pure $ sub1 tsnd (Fst e eloc)
|
||||
compare0Inner' defs ctx sg e@(Snd {}) f _ _ =
|
||||
clashE defs ctx sg e f
|
||||
|
||||
-- Ψ | Γ ⊢ e = f ⇒ {𝐚s}
|
||||
-- Ψ | Γ, x : {𝐚s} ⊢ Q = R
|
||||
|
|
@ -550,20 +579,20 @@ namespace Elim
|
|||
-- --------------------------------------------------
|
||||
-- Ψ | Γ ⊢ caseπ e return Q of { '𝐚ᵢ ⇒ sᵢ }
|
||||
-- = caseπ f return R of { '𝐚ᵢ ⇒ tᵢ } ⇒ Q[e/x]
|
||||
compare0Inner' defs ctx (CaseEnum epi e eret earms eloc)
|
||||
(CaseEnum fpi f fret farms floc) ne nf =
|
||||
compare0Inner' defs ctx sg (CaseEnum epi e eret earms eloc)
|
||||
(CaseEnum fpi f fret farms floc) ne nf =
|
||||
local_ Equal $ do
|
||||
ety <- compare0Inner defs ctx e f
|
||||
ety <- compare0Inner defs ctx sg e f
|
||||
try $
|
||||
compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
|
||||
for_ (SortedMap.toList earms) $ \(t, l) => do
|
||||
let Just r = lookup t farms
|
||||
| Nothing => putError $ TagNotIn floc t (fromList $ keys farms)
|
||||
let t' = Ann (Tag t l.loc) ety l.loc
|
||||
try $ Term.compare0 defs ctx (sub1 eret t') l r
|
||||
try $ Term.compare0 defs ctx sg (sub1 eret t') l r
|
||||
try $ expectEqualQ eloc epi fpi
|
||||
pure $ sub1 eret e
|
||||
compare0Inner' defs ctx e@(CaseEnum {}) f _ _ = clashE defs ctx e f
|
||||
compare0Inner' defs ctx sg e@(CaseEnum {}) f _ _ = clashE defs ctx sg e f
|
||||
|
||||
-- Ψ | Γ ⊢ e = f ⇒ ℕ
|
||||
-- Ψ | Γ, x : ℕ ⊢ Q = R
|
||||
|
|
@ -573,23 +602,23 @@ namespace Elim
|
|||
-- Ψ | Γ ⊢ caseπ e return Q of { 0 ⇒ s₀; x, π.y ⇒ s₁ }
|
||||
-- = caseπ f return R of { 0 ⇒ t₀; x, π.y ⇒ t₁ }
|
||||
-- ⇒ Q[e/x]
|
||||
compare0Inner' defs ctx (CaseNat epi epi' e eret ezer esuc eloc)
|
||||
(CaseNat fpi fpi' f fret fzer fsuc floc) ne nf =
|
||||
compare0Inner' defs ctx sg (CaseNat epi epi' e eret ezer esuc eloc)
|
||||
(CaseNat fpi fpi' f fret fzer fsuc floc) ne nf =
|
||||
local_ Equal $ do
|
||||
ety <- compare0Inner defs ctx e f
|
||||
ety <- compare0Inner defs ctx sg e f
|
||||
let [< p, ih] = esuc.names
|
||||
try $ do
|
||||
compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
|
||||
Term.compare0 defs ctx
|
||||
Term.compare0 defs ctx sg
|
||||
(sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc))
|
||||
ezer fzer
|
||||
Term.compare0 defs
|
||||
(extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx)
|
||||
(extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx) sg
|
||||
(substCaseSuccRet esuc.names eret) esuc.term fsuc.term
|
||||
expectEqualQ e.loc epi fpi
|
||||
expectEqualQ e.loc epi' fpi'
|
||||
pure $ sub1 eret e
|
||||
compare0Inner' defs ctx e@(CaseNat {}) f _ _ = clashE defs ctx e f
|
||||
compare0Inner' defs ctx sg e@(CaseNat {}) f _ _ = clashE defs ctx sg e f
|
||||
|
||||
-- Ψ | Γ ⊢ e = f ⇒ [ρ. A]
|
||||
-- Ψ | Γ, x : [ρ. A] ⊢ Q = R
|
||||
|
|
@ -597,32 +626,34 @@ namespace Elim
|
|||
-- --------------------------------------------------
|
||||
-- Ψ | Γ ⊢ caseπ e return Q of { [x] ⇒ s }
|
||||
-- = caseπ f return R of { [x] ⇒ t } ⇒ Q[e/x]
|
||||
compare0Inner' defs ctx (CaseBox epi e eret ebody eloc)
|
||||
(CaseBox fpi f fret fbody floc) ne nf =
|
||||
compare0Inner' defs ctx sg (CaseBox epi e eret ebody eloc)
|
||||
(CaseBox fpi f fret fbody floc) ne nf =
|
||||
local_ Equal $ do
|
||||
ety <- compare0Inner defs ctx e f
|
||||
(q, ty) <- expectBOX defs ctx eloc ety
|
||||
ety <- compare0Inner defs ctx sg e f
|
||||
(q, ty) <- expectBOX defs ctx sg eloc ety
|
||||
try $ do
|
||||
compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
|
||||
Term.compare0 defs (extendTy (epi * q) ebody.name ty ctx)
|
||||
Term.compare0 defs (extendTy (epi * q) ebody.name ty ctx) sg
|
||||
(substCaseBoxRet ebody.name ety eret)
|
||||
ebody.term fbody.term
|
||||
expectEqualQ eloc epi fpi
|
||||
pure $ sub1 eret e
|
||||
compare0Inner' defs ctx e@(CaseBox {}) f _ _ = clashE defs ctx e f
|
||||
compare0Inner' defs ctx sg e@(CaseBox {}) f _ _ = clashE defs ctx sg e f
|
||||
|
||||
-- (no neutral dim apps in a closed dctx)
|
||||
compare0Inner' _ _ (DApp _ (K {}) _) _ ne _ = void $ absurd $ noOr2 $ noOr2 ne
|
||||
compare0Inner' _ _ _ (DApp _ (K {}) _) _ nf = void $ absurd $ noOr2 $ noOr2 nf
|
||||
compare0Inner' _ _ _ (DApp _ (K {}) _) _ ne _ =
|
||||
void $ absurd $ noOr2 $ noOr2 ne
|
||||
compare0Inner' _ _ _ _ (DApp _ (K {}) _) _ nf =
|
||||
void $ absurd $ noOr2 $ noOr2 nf
|
||||
|
||||
-- Ψ | Γ ⊢ s <: t : B
|
||||
-- --------------------------------
|
||||
-- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
|
||||
--
|
||||
-- and similar for :> and A
|
||||
compare0Inner' defs ctx (Ann s a _) (Ann t b _) _ _ = do
|
||||
compare0Inner' defs ctx sg (Ann s a _) (Ann t b _) _ _ = do
|
||||
ty <- bigger a b
|
||||
try $ Term.compare0 defs ctx ty s t
|
||||
try $ Term.compare0 defs ctx sg ty s t
|
||||
pure ty
|
||||
|
||||
-- Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
|
||||
|
|
@ -631,82 +662,86 @@ namespace Elim
|
|||
-- -----------------------------------------------------------
|
||||
-- Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s
|
||||
-- <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖›
|
||||
compare0Inner' defs ctx (Coe ty1 p1 q1 val1 _)
|
||||
(Coe ty2 p2 q2 val2 _) ne nf = do
|
||||
compare0Inner' defs ctx sg (Coe ty1 p1 q1 val1 _)
|
||||
(Coe ty2 p2 q2 val2 _) ne nf = do
|
||||
let ty1p = dsub1 ty1 p1; ty2p = dsub1 ty2 p2
|
||||
ty1q = dsub1 ty1 q1; ty2q = dsub1 ty2 q2
|
||||
(ty_p, ty_q) <- bigger (ty1p, ty1q) (ty2p, ty2q)
|
||||
try $ do
|
||||
compareType defs ctx ty1p ty2p
|
||||
compareType defs ctx ty1q ty2q
|
||||
Term.compare0 defs ctx ty_p val1 val2
|
||||
Term.compare0 defs ctx sg ty_p val1 val2
|
||||
pure $ ty_q
|
||||
compare0Inner' defs ctx e@(Coe {}) f _ _ = clashE defs ctx e f
|
||||
compare0Inner' defs ctx sg e@(Coe {}) f _ _ = clashE defs ctx sg e f
|
||||
|
||||
-- (no neutral compositions in a closed dctx)
|
||||
compare0Inner' _ _ (Comp {r = K e _, _}) _ ne _ = void $ absurd $ noOr2 ne
|
||||
compare0Inner' _ _ (Comp {r = B i _, _}) _ _ _ = absurd i
|
||||
compare0Inner' _ _ _ (Comp {r = K _ _, _}) _ nf = void $ absurd $ noOr2 nf
|
||||
compare0Inner' _ _ _ (Comp {r = K {}, _}) _ ne _ = void $ absurd $ noOr2 ne
|
||||
compare0Inner' _ _ _ (Comp {r = B i _, _}) _ _ _ = absurd i
|
||||
compare0Inner' _ _ _ _ (Comp {r = K {}, _}) _ nf = void $ absurd $ noOr2 nf
|
||||
|
||||
-- (type case equality purely structural)
|
||||
compare0Inner' defs ctx (TypeCase ty1 ret1 arms1 def1 eloc)
|
||||
(TypeCase ty2 ret2 arms2 def2 floc) ne _ =
|
||||
local_ Equal $ do
|
||||
ety <- compare0Inner defs ctx ty1 ty2
|
||||
u <- expectTYPE defs ctx eloc ety
|
||||
try $ do
|
||||
compareType defs ctx ret1 ret2
|
||||
compareType defs ctx def1 def2
|
||||
for_ allKinds $ \k =>
|
||||
compareArm defs ctx k ret1 u
|
||||
(lookupPrecise k arms1) (lookupPrecise k arms2) def1
|
||||
pure ret1
|
||||
compare0Inner' defs ctx e@(TypeCase {}) f _ _ = clashE defs ctx e f
|
||||
compare0Inner' defs ctx sg (TypeCase ty1 ret1 arms1 def1 eloc)
|
||||
(TypeCase ty2 ret2 arms2 def2 floc) ne _ =
|
||||
case sg `decEq` SZero of
|
||||
Yes Refl => local_ Equal $ do
|
||||
ety <- compare0Inner defs ctx SZero ty1 ty2
|
||||
u <- expectTYPE defs ctx SZero eloc ety
|
||||
try $ do
|
||||
compareType defs ctx ret1 ret2
|
||||
compareType defs ctx def1 def2
|
||||
for_ allKinds $ \k =>
|
||||
compareArm defs ctx k ret1 u
|
||||
(lookupPrecise k arms1) (lookupPrecise k arms2) def1
|
||||
pure ret1
|
||||
No _ => do
|
||||
putError $ ClashQ eloc sg.qty Zero
|
||||
computeElimTypeE defs ctx sg $ TypeCase ty1 ret1 arms1 def1 eloc
|
||||
compare0Inner' defs ctx sg e@(TypeCase {}) f _ _ = clashE defs ctx sg e f
|
||||
|
||||
-- Ψ | Γ ⊢ s <: f ⇐ A
|
||||
-- --------------------------
|
||||
-- Ψ | Γ ⊢ (s ∷ A) <: f ⇒ A
|
||||
--
|
||||
-- and vice versa
|
||||
compare0Inner' defs ctx (Ann s a _) f _ _ = do
|
||||
try $ Term.compare0 defs ctx a s (E f)
|
||||
compare0Inner' defs ctx sg (Ann s a _) f _ _ = do
|
||||
try $ Term.compare0 defs ctx sg a s (E f)
|
||||
pure a
|
||||
compare0Inner' defs ctx e (Ann t b _) _ _ = do
|
||||
try $ Term.compare0 defs ctx b (E e) t
|
||||
compare0Inner' defs ctx sg e (Ann t b _) _ _ = do
|
||||
try $ Term.compare0 defs ctx sg b (E e) t
|
||||
pure b
|
||||
compare0Inner' defs ctx e@(Ann {}) f _ _ =
|
||||
clashE defs ctx e f
|
||||
compare0Inner' defs ctx sg e@(Ann {}) f _ _ =
|
||||
clashE defs ctx sg e f
|
||||
|
||||
compare0Inner defs ctx e f = do
|
||||
compare0Inner defs ctx sg e f = do
|
||||
let Val n = ctx.termLen
|
||||
Element e ne <- whnf defs ctx e.loc e
|
||||
Element f nf <- whnf defs ctx f.loc f
|
||||
ty <- compare0Inner' defs ctx e f ne nf
|
||||
if !(lift $ isSubSing defs ctx ty)
|
||||
Element e ne <- whnf defs ctx sg e.loc e
|
||||
Element f nf <- whnf defs ctx sg f.loc f
|
||||
ty <- compare0Inner' defs ctx sg e f ne nf
|
||||
if !(lift $ isSubSing defs ctx sg ty) && isJust !(getAt InnerErr)
|
||||
then putAt InnerErr Nothing
|
||||
else modifyAt InnerErr $ map $ WhileComparingE ctx !mode e f
|
||||
else modifyAt InnerErr $ map $ WhileComparingE ctx !mode sg e f
|
||||
pure ty
|
||||
|
||||
|
||||
namespace Term
|
||||
compare0 defs ctx ty s t =
|
||||
wrapErr (WhileComparingT ctx !mode ty s t) $ do
|
||||
compare0 defs ctx sg ty s t =
|
||||
wrapErr (WhileComparingT ctx !mode sg ty s t) $ do
|
||||
let Val n = ctx.termLen
|
||||
Element ty' _ <- whnf defs ctx ty.loc ty
|
||||
Element s' _ <- whnf defs ctx s.loc s
|
||||
Element t' _ <- whnf defs ctx t.loc t
|
||||
Element ty' _ <- whnf defs ctx SZero ty.loc ty
|
||||
Element s' _ <- whnf defs ctx sg s.loc s
|
||||
Element t' _ <- whnf defs ctx sg t.loc t
|
||||
tty <- ensureTyCon ty.loc ctx ty'
|
||||
compare0' defs ctx ty' s' t'
|
||||
compare0' defs ctx sg ty' s' t'
|
||||
|
||||
namespace Elim
|
||||
compare0 defs ctx e f = do
|
||||
(ty, err) <- runStateAt InnerErr Nothing $ compare0Inner defs ctx e f
|
||||
compare0 defs ctx sg e f = do
|
||||
(ty, err) <- runStateAt InnerErr Nothing $ compare0Inner defs ctx sg e f
|
||||
maybe (pure ty) throw err
|
||||
|
||||
compareType defs ctx s t = do
|
||||
let Val n = ctx.termLen
|
||||
Element s' _ <- whnf defs ctx s.loc s
|
||||
Element t' _ <- whnf defs ctx t.loc t
|
||||
Element s' _ <- whnf defs ctx SZero s.loc s
|
||||
Element t' _ <- whnf defs ctx SZero t.loc t
|
||||
ts <- ensureTyCon s.loc ctx s'
|
||||
tt <- ensureTyCon t.loc ctx t'
|
||||
st <- either pure (const $ clashTy s.loc ctx s' t') $
|
||||
|
|
@ -744,9 +779,9 @@ parameters (loc : Loc) (ctx : TyContext d n)
|
|||
|
||||
namespace Term
|
||||
export covering
|
||||
compare : (ty, s, t : Term d n) -> Eff Equal ()
|
||||
compare ty s t = runCompare (fdvAll [ty, s, t]) $ \defs, ectx, th =>
|
||||
compare0 defs ectx (ty // th) (s // th) (t // th)
|
||||
compare : SQty -> (ty, s, t : Term d n) -> Eff Equal ()
|
||||
compare sg ty s t = runCompare (fdvAll [ty, s, t]) $ \defs, ectx, th =>
|
||||
compare0 defs ectx sg (ty // th) (s // th) (t // th)
|
||||
|
||||
export covering
|
||||
compareType : (s, t : Term d n) -> Eff Equal ()
|
||||
|
|
@ -757,13 +792,13 @@ parameters (loc : Loc) (ctx : TyContext d n)
|
|||
||| you don't have to pass the type in but the arguments must still be
|
||||
||| of the same type!!
|
||||
export covering
|
||||
compare : (e, f : Elim d n) -> Eff Equal ()
|
||||
compare e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th =>
|
||||
ignore $ compare0 defs ectx (e // th) (f // th)
|
||||
compare : SQty -> (e, f : Elim d n) -> Eff Equal ()
|
||||
compare sg e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th =>
|
||||
ignore $ compare0 defs ectx sg (e // th) (f // th)
|
||||
|
||||
namespace Term
|
||||
export covering %inline
|
||||
equal, sub, super : (ty, s, t : Term d n) -> Eff Equal ()
|
||||
equal, sub, super : SQty -> (ty, s, t : Term d n) -> Eff Equal ()
|
||||
equal = compare Equal
|
||||
sub = compare Sub
|
||||
super = compare Super
|
||||
|
|
@ -776,7 +811,7 @@ parameters (loc : Loc) (ctx : TyContext d n)
|
|||
|
||||
namespace Elim
|
||||
export covering %inline
|
||||
equal, sub, super : (e, f : Elim d n) -> Eff Equal ()
|
||||
equal, sub, super : SQty -> (e, f : Elim d n) -> Eff Equal ()
|
||||
equal = compare Equal
|
||||
sub = compare Sub
|
||||
super = compare Super
|
||||
|
|
|
|||
|
|
@ -84,19 +84,19 @@ toSet (FV vs) =
|
|||
|
||||
|
||||
public export
|
||||
interface HasFreeVars (0 term : Nat -> Type) where
|
||||
interface HasFreeVars (0 tm : Nat -> Type) where
|
||||
constructor HFV
|
||||
fv : {n : Nat} -> term n -> FreeVars n
|
||||
fv : {n : Nat} -> tm n -> FreeVars n
|
||||
|
||||
public export
|
||||
interface HasFreeDVars (0 term : TermLike) where
|
||||
interface HasFreeDVars (0 tm : TermLike) where
|
||||
constructor HFDV
|
||||
fdv : {d, n : Nat} -> term d n -> FreeVars d
|
||||
fdv : {d, n : Nat} -> tm d n -> FreeVars d
|
||||
|
||||
export
|
||||
Fdv : (0 term : TermLike) -> {n : Nat} ->
|
||||
HasFreeDVars term => HasFreeVars (\d => term d n)
|
||||
Fdv term @{HFDV fdv} = HFV fdv
|
||||
Fdv : (0 tm : TermLike) -> {n : Nat} ->
|
||||
HasFreeDVars tm => HasFreeVars (\d => tm d n)
|
||||
Fdv tm @{HFDV fdv} = HFV fdv
|
||||
|
||||
|
||||
export
|
||||
|
|
@ -119,26 +119,26 @@ HasFreeVars Dim where
|
|||
|
||||
|
||||
export
|
||||
{s : Nat} -> HasFreeVars term => HasFreeVars (Scoped s term) where
|
||||
{s : Nat} -> HasFreeVars tm => HasFreeVars (Scoped s tm) where
|
||||
fv (S _ (Y body)) = FV $ drop s (fv body).vars
|
||||
fv (S _ (N body)) = fv body
|
||||
|
||||
export
|
||||
implementation [DScope]
|
||||
{s : Nat} -> HasFreeDVars term =>
|
||||
HasFreeDVars (\d, n => Scoped s (\d' => term d' n) d)
|
||||
{s : Nat} -> HasFreeDVars tm =>
|
||||
HasFreeDVars (\d, n => Scoped s (\d' => tm d' n) d)
|
||||
where
|
||||
fdv (S _ (Y body)) = FV $ drop s (fdv body).vars
|
||||
fdv (S _ (N body)) = fdv body
|
||||
|
||||
export
|
||||
fvD : {0 term : TermLike} -> {n : Nat} -> (forall d. HasFreeVars (term d)) =>
|
||||
Scoped s (\d => term d n) d -> FreeVars n
|
||||
fvD : {0 tm : TermLike} -> {n : Nat} -> (forall d. HasFreeVars (tm d)) =>
|
||||
Scoped s (\d => tm d n) d -> FreeVars n
|
||||
fvD (S _ (Y body)) = fv body
|
||||
fvD (S _ (N body)) = fv body
|
||||
|
||||
export
|
||||
fdvT : HasFreeDVars term => {s, d, n : Nat} -> Scoped s (term d) n -> FreeVars d
|
||||
fdvT : HasFreeDVars tm => {s, d, n : Nat} -> Scoped s (tm d) n -> FreeVars d
|
||||
fdvT (S _ (Y body)) = fdv body
|
||||
fdvT (S _ (N body)) = fdv body
|
||||
|
||||
|
|
@ -149,8 +149,8 @@ guardM b x = if b then x else neutral
|
|||
|
||||
export
|
||||
implementation
|
||||
(HasFreeVars term, HasFreeVars env) =>
|
||||
HasFreeVars (WithSubst term env)
|
||||
(HasFreeVars tm, HasFreeVars env) =>
|
||||
HasFreeVars (WithSubst tm env)
|
||||
where
|
||||
fv (Sub term subst) =
|
||||
let Val from = getFrom subst in
|
||||
|
|
@ -158,8 +158,8 @@ where
|
|||
|
||||
export
|
||||
implementation [WithSubst]
|
||||
((forall d. HasFreeVars (term d)), HasFreeDVars term, HasFreeDVars env) =>
|
||||
HasFreeDVars (\d => WithSubst (term d) (env d))
|
||||
((forall d. HasFreeVars (tm d)), HasFreeDVars tm, HasFreeDVars env) =>
|
||||
HasFreeDVars (\d => WithSubst (tm d) (env d))
|
||||
where
|
||||
fdv (Sub term subst) =
|
||||
let Val from = getFrom subst in
|
||||
|
|
@ -196,6 +196,8 @@ HasFreeVars (Elim d) where
|
|||
fv (B i _) = only i
|
||||
fv (App {fun, arg, _}) = fv fun <+> fv arg
|
||||
fv (CasePair {pair, ret, body, _}) = fv pair <+> fv ret <+> fv body
|
||||
fv (Fst pair _) = fv pair
|
||||
fv (Snd pair _) = fv pair
|
||||
fv (CaseEnum {tag, ret, arms, _}) =
|
||||
fv tag <+> fv ret <+> foldMap fv (values arms)
|
||||
fv (CaseNat {nat, ret, zero, succ, _}) =
|
||||
|
|
@ -225,8 +227,8 @@ expandDSubst (t ::: th) = expandDSubst th :< t
|
|||
|
||||
|
||||
private
|
||||
fdvSubst' : {d1, d2, n : Nat} -> HasFreeDVars term =>
|
||||
term d1 n -> DSubst d1 d2 -> FreeVars d2
|
||||
fdvSubst' : {d1, d2, n : Nat} -> HasFreeDVars tm =>
|
||||
tm d1 n -> DSubst d1 d2 -> FreeVars d2
|
||||
fdvSubst' t th =
|
||||
fold $ zipWith maybeOnly (fdv t).vars (expandDSubst th)
|
||||
where
|
||||
|
|
@ -235,8 +237,8 @@ where
|
|||
maybeOnly _ _ = none
|
||||
|
||||
private
|
||||
fdvSubst : {d, n : Nat} -> HasFreeDVars term =>
|
||||
WithSubst (\d => term d n) Dim d -> FreeVars d
|
||||
fdvSubst : {d, n : Nat} -> HasFreeDVars tm =>
|
||||
WithSubst (\d => tm d n) Dim d -> FreeVars d
|
||||
fdvSubst (Sub t th) = let Val from = getFrom th in fdvSubst' t th
|
||||
|
||||
|
||||
|
|
@ -269,6 +271,8 @@ HasFreeDVars Elim where
|
|||
fdv (B {}) = none
|
||||
fdv (App {fun, arg, _}) = fdv fun <+> fdv arg
|
||||
fdv (CasePair {pair, ret, body, _}) = fdv pair <+> fdvT ret <+> fdvT body
|
||||
fdv (Fst pair _) = fdv pair
|
||||
fdv (Snd pair _) = fdv pair
|
||||
fdv (CaseEnum {tag, ret, arms, _}) =
|
||||
fdv tag <+> fdvT ret <+> foldMap fdv (values arms)
|
||||
fdv (CaseNat {nat, ret, zero, succ, _}) =
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ import Data.List
|
|||
import Data.Maybe
|
||||
import Data.SnocVect
|
||||
import Quox.EffExtra
|
||||
import Quox.ST
|
||||
import Control.Monad.ST.Extra
|
||||
|
||||
import System.File
|
||||
import System.Path
|
||||
|
|
@ -141,6 +141,12 @@ mutual
|
|||
<*> fromPTermTScope ds ns [< x, y] body
|
||||
<*> pure loc
|
||||
|
||||
Fst pair loc =>
|
||||
map E $ Fst <$> fromPTermElim ds ns pair <*> pure loc
|
||||
|
||||
Snd pair loc =>
|
||||
map E $ Snd <$> fromPTermElim ds ns pair <*> pure loc
|
||||
|
||||
Case pi tag (r, ret) (CaseEnum arms _) loc =>
|
||||
map E $ CaseEnum (fromPQty pi)
|
||||
<$> fromPTermElim ds ns tag
|
||||
|
|
@ -267,9 +273,9 @@ fromPTerm = fromPTermWith [<] [<]
|
|||
|
||||
export
|
||||
globalPQty : Has (Except Error) fs => (q : Qty) -> Loc -> Eff fs GQty
|
||||
globalPQty pi loc = case choose $ isGlobal pi of
|
||||
Left y => pure $ Element pi y
|
||||
Right _ => throw $ QtyNotGlobal loc pi
|
||||
globalPQty pi loc = case toGlobal pi of
|
||||
Just g => pure g
|
||||
Nothing => throw $ QtyNotGlobal loc pi
|
||||
|
||||
export
|
||||
fromPBaseNameNS : Has (StateL NS Mods) fs => PBaseName -> Eff fs Name
|
||||
|
|
@ -340,14 +346,14 @@ fromParserPure : NameSuf -> Definitions ->
|
|||
Eff FromParserPure a ->
|
||||
Either Error (a, NameSuf, Definitions)
|
||||
fromParserPure suf defs act = runSTErr $ do
|
||||
suf <- newRef suf
|
||||
defs <- newRef defs
|
||||
suf <- liftST $ newSTRef suf
|
||||
defs <- liftST $ newSTRef defs
|
||||
res <- runEff act $ with Union.(::)
|
||||
[handleExcept (\e => stLeft e),
|
||||
handleStateSTRef defs,
|
||||
handleStateSTRef !(newRef [<]),
|
||||
handleStateSTRef !(liftST $ newSTRef [<]),
|
||||
handleStateSTRef suf]
|
||||
pure (res, !(readRef suf), !(readRef defs))
|
||||
pure (res, !(liftST $ readSTRef suf), !(liftST $ readSTRef defs))
|
||||
|
||||
|
||||
export covering
|
||||
|
|
|
|||
|
|
@ -203,6 +203,7 @@ reserved =
|
|||
Word "caseω" `Or` Word "case#",
|
||||
Word1 "return",
|
||||
Word1 "of",
|
||||
Word1 "fst", Word1 "snd",
|
||||
Word1 "_",
|
||||
Word1 "Eq",
|
||||
Word "λ" `Or` Word "fun",
|
||||
|
|
|
|||
|
|
@ -372,10 +372,23 @@ eqTerm : FileName -> Grammar True PTerm
|
|||
eqTerm fname = withLoc fname $
|
||||
resC "Eq" *> mustWork [|Eq (typeLine fname) (termArg fname) (termArg fname)|]
|
||||
|
||||
export
|
||||
resAppTerm : FileName -> (word : String) -> (0 _ : IsReserved word) =>
|
||||
(PTerm -> Loc -> PTerm) -> Grammar True PTerm
|
||||
resAppTerm fname word f = withLoc fname $
|
||||
resC word *> mustWork [|f (termArg fname)|]
|
||||
|
||||
export
|
||||
succTerm : FileName -> Grammar True PTerm
|
||||
succTerm fname = withLoc fname $
|
||||
resC "succ" *> mustWork [|Succ (termArg fname)|]
|
||||
succTerm fname = resAppTerm fname "succ" Succ
|
||||
|
||||
export
|
||||
fstTerm : FileName -> Grammar True PTerm
|
||||
fstTerm fname = resAppTerm fname "fst" Fst
|
||||
|
||||
export
|
||||
sndTerm : FileName -> Grammar True PTerm
|
||||
sndTerm fname = resAppTerm fname "snd" Snd
|
||||
|
||||
||| a dimension argument with an `@` prefix, or
|
||||
||| a term argument with no prefix
|
||||
|
|
@ -403,6 +416,8 @@ appTerm fname =
|
|||
<|> splitUniverseTerm fname
|
||||
<|> eqTerm fname
|
||||
<|> succTerm fname
|
||||
<|> fstTerm fname
|
||||
<|> sndTerm fname
|
||||
<|> normalAppTerm fname
|
||||
|
||||
export
|
||||
|
|
|
|||
|
|
@ -73,6 +73,7 @@ namespace PTerm
|
|||
| Sig PatVar PTerm PTerm Loc
|
||||
| Pair PTerm PTerm Loc
|
||||
| Case PQty PTerm (PatVar, PTerm) PCaseBody Loc
|
||||
| Fst PTerm Loc | Snd PTerm Loc
|
||||
|
||||
| Enum (List TagVal) Loc
|
||||
| Tag TagVal Loc
|
||||
|
|
@ -113,6 +114,8 @@ Located PTerm where
|
|||
(App _ _ loc).loc = loc
|
||||
(Sig _ _ _ loc).loc = loc
|
||||
(Pair _ _ loc).loc = loc
|
||||
(Fst _ loc).loc = loc
|
||||
(Snd _ loc).loc = loc
|
||||
(Case _ _ _ _ loc).loc = loc
|
||||
(Enum _ loc).loc = loc
|
||||
(Tag _ loc).loc = loc
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ module Quox.Pretty
|
|||
import Quox.Loc
|
||||
import Quox.Name
|
||||
|
||||
import Quox.ST
|
||||
import Control.Monad.ST.Extra
|
||||
import public Text.PrettyPrint.Bernardy
|
||||
import public Text.PrettyPrint.Bernardy.Core.Decorate
|
||||
import public Quox.EffExtra
|
||||
|
|
@ -68,7 +68,7 @@ runPrettyWith : PPrec -> Flavor -> (HL -> Highlight) -> Nat ->
|
|||
runPrettyWith prec flavor highlight indent act =
|
||||
runST $ do
|
||||
runEff act $ with Union.(::)
|
||||
[handleStateSTRef !(newRef prec),
|
||||
[handleStateSTRef !(newSTRef prec),
|
||||
handleReaderConst flavor,
|
||||
handleReaderConst highlight,
|
||||
handleReaderConst indent]
|
||||
|
|
@ -234,7 +234,7 @@ prettyDBind = hl DVar . prettyBind'
|
|||
export %inline
|
||||
typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
|
||||
eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
|
||||
ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD :
|
||||
ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD :
|
||||
{opts : LayoutOpts} -> Eff Pretty (Doc opts)
|
||||
typeD = hl Syntax . text =<< ifUnicode "★" "Type"
|
||||
arrowD = hl Delim . text =<< ifUnicode "→" "->"
|
||||
|
|
@ -261,6 +261,8 @@ compD = hl Syntax $ text "comp"
|
|||
undD = hl Syntax $ text "_"
|
||||
cstD = hl Syntax $ text "="
|
||||
pipeD = hl Syntax $ text "|"
|
||||
fstD = hl Syntax $ text "fst"
|
||||
sndD = hl Syntax $ text "snd"
|
||||
|
||||
|
||||
export
|
||||
|
|
|
|||
106
lib/Quox/ST.idr
106
lib/Quox/ST.idr
|
|
@ -1,106 +0,0 @@
|
|||
module Quox.ST
|
||||
|
||||
import Data.IORef
|
||||
import Control.MonadRec
|
||||
|
||||
|
||||
export
|
||||
Tag : Type
|
||||
Tag = () -- shhh don't tell anyone
|
||||
|
||||
export
|
||||
record ST (s : Tag) a where
|
||||
constructor MkST
|
||||
action : IO a
|
||||
%name ST st
|
||||
|
||||
export
|
||||
runST : (forall s. ST s a) -> a
|
||||
runST st = unsafePerformIO (st {s = ()}).action
|
||||
|
||||
export %inline Functor (ST s) where map f st = MkST $ map f st.action
|
||||
|
||||
export %inline
|
||||
Applicative (ST s) where
|
||||
pure = MkST . pure
|
||||
f <*> x = MkST $ f.action <*> x.action
|
||||
|
||||
export %inline Monad (ST s) where m >>= k = MkST $ m.action >>= action . k
|
||||
|
||||
export %inline
|
||||
MonadRec (ST s) where
|
||||
tailRecM s (Access r) x k = MkST $ do
|
||||
let MkST yy = k s x
|
||||
case !yy of
|
||||
Done y => pure y
|
||||
Cont s2 p y => let MkST z = tailRecM s2 (r s2 p) y k in z
|
||||
|
||||
|
||||
public export
|
||||
interface HasST (0 m : Tag -> Type -> Type) where
|
||||
liftST : ST s a -> m s a
|
||||
|
||||
export %inline HasST ST where liftST = id
|
||||
|
||||
export
|
||||
record STRef (s : Tag) a where
|
||||
constructor MkSTRef
|
||||
ref : IORef a
|
||||
%name STRef r
|
||||
|
||||
export %inline
|
||||
newRef : HasST m => a -> m s (STRef s a)
|
||||
newRef x = liftST $ MkST $ MkSTRef <$> newIORef x
|
||||
|
||||
export %inline
|
||||
readRef : HasST m => STRef s a -> m s a
|
||||
readRef r = liftST $ MkST $ readIORef r.ref
|
||||
|
||||
export %inline
|
||||
writeRef : HasST m => STRef s a -> a -> m s ()
|
||||
writeRef r x = liftST $ MkST $ writeIORef r.ref x
|
||||
|
||||
export %inline
|
||||
modifyRef : HasST m => STRef s a -> (a -> a) -> m s ()
|
||||
modifyRef r f = liftST $ MkST $ modifyIORef r.ref f
|
||||
|
||||
|
||||
public export
|
||||
record STErr e (s : Tag) a where
|
||||
constructor STE
|
||||
fromSTErr : ST s (Either e a)
|
||||
|
||||
export
|
||||
Functor (STErr e s) where
|
||||
map f (STE e) = STE $ map f <$> e
|
||||
|
||||
export
|
||||
Applicative (STErr e s) where
|
||||
pure x = STE $ pure $ pure x
|
||||
STE f <*> STE x = STE [|f <*> x|]
|
||||
|
||||
export
|
||||
Monad (STErr e s) where
|
||||
STE m >>= k = STE $ do
|
||||
case !m of
|
||||
Left err => pure $ Left err
|
||||
Right x => fromSTErr $ k x
|
||||
|
||||
export
|
||||
MonadRec (STErr e s) where
|
||||
tailRecM s (Access r) x k = STE $ do
|
||||
let STE m = k s x
|
||||
case !m of
|
||||
Left err => pure $ Left err
|
||||
Right (Cont s' p y) => fromSTErr $ tailRecM s' (r s' p) y k
|
||||
Right (Done y) => pure $ Right y
|
||||
|
||||
export
|
||||
runSTErr : (forall s. STErr e s a) -> Either e a
|
||||
runSTErr ste = runST $ fromSTErr ste
|
||||
|
||||
export %inline HasST (STErr e) where liftST = STE . map Right
|
||||
|
||||
export
|
||||
stLeft : e -> STErr e s a
|
||||
stLeft e = STE $ pure $ Left e
|
||||
|
|
@ -78,26 +78,16 @@ lub p q = if p == q then p else Any
|
|||
||| to maintain subject reduction, only 0 or 1 can occur
|
||||
||| for the subject of a typing judgment. see @qtt, §2.3 for more detail
|
||||
public export
|
||||
isSubj : Qty -> Bool
|
||||
isSubj Zero = True
|
||||
isSubj One = True
|
||||
isSubj Any = False
|
||||
|
||||
public export
|
||||
SQty : Type
|
||||
SQty = Subset Qty $ So . isSubj
|
||||
|
||||
public export %inline
|
||||
szero, sone : SQty
|
||||
szero = Element Zero Oh
|
||||
sone = Element One Oh
|
||||
data SQty = SZero | SOne
|
||||
%runElab derive "SQty" [Eq, Ord, Show]
|
||||
%name Qty.SQty sg
|
||||
|
||||
||| "σ ⨴ π"
|
||||
|||
|
||||
||| σ ⨭ π is 0 if either of σ or π are, otherwise it is σ.
|
||||
||| σ ⨴ π is 0 if either of σ or π are, otherwise it is σ.
|
||||
public export
|
||||
subjMult : SQty -> Qty -> SQty
|
||||
subjMult _ Zero = szero
|
||||
subjMult _ Zero = SZero
|
||||
subjMult sg _ = sg
|
||||
|
||||
|
||||
|
|
@ -105,23 +95,59 @@ subjMult sg _ = sg
|
|||
||| quantity of 1, so the only distinction is whether it is present
|
||||
||| at runtime at all or not
|
||||
public export
|
||||
isGlobal : Qty -> Bool
|
||||
isGlobal Zero = True
|
||||
isGlobal One = False
|
||||
isGlobal Any = True
|
||||
data GQty = GZero | GAny
|
||||
%runElab derive "GQty" [Eq, Ord, Show]
|
||||
%name GQty rh
|
||||
|
||||
public export
|
||||
GQty : Type
|
||||
GQty = Subset Qty $ So . isGlobal
|
||||
|
||||
public export
|
||||
gzero, gany : GQty
|
||||
gzero = Element Zero Oh
|
||||
gany = Element Any Oh
|
||||
toGlobal : Qty -> Maybe GQty
|
||||
toGlobal Zero = Just GZero
|
||||
toGlobal Any = Just GAny
|
||||
toGlobal One = Nothing
|
||||
|
||||
||| when checking a definition, a 0 definition is checked at 0,
|
||||
||| but an ω definition is checked at 1 since ω isn't a subject quantity
|
||||
public export %inline
|
||||
globalToSubj : GQty -> SQty
|
||||
globalToSubj (Element Zero _) = szero
|
||||
globalToSubj (Element Any _) = sone
|
||||
globalToSubj GZero = SZero
|
||||
globalToSubj GAny = SOne
|
||||
|
||||
|
||||
public export
|
||||
DecEq Qty where
|
||||
decEq Zero Zero = Yes Refl
|
||||
decEq Zero One = No $ \case _ impossible
|
||||
decEq Zero Any = No $ \case _ impossible
|
||||
decEq One Zero = No $ \case _ impossible
|
||||
decEq One One = Yes Refl
|
||||
decEq One Any = No $ \case _ impossible
|
||||
decEq Any Zero = No $ \case _ impossible
|
||||
decEq Any One = No $ \case _ impossible
|
||||
decEq Any Any = Yes Refl
|
||||
|
||||
public export
|
||||
DecEq SQty where
|
||||
decEq SZero SZero = Yes Refl
|
||||
decEq SZero SOne = No $ \case _ impossible
|
||||
decEq SOne SZero = No $ \case _ impossible
|
||||
decEq SOne SOne = Yes Refl
|
||||
|
||||
public export
|
||||
DecEq GQty where
|
||||
decEq GZero GZero = Yes Refl
|
||||
decEq GZero GAny = No $ \case _ impossible
|
||||
decEq GAny GZero = No $ \case _ impossible
|
||||
decEq GAny GAny = Yes Refl
|
||||
|
||||
|
||||
namespace SQty
|
||||
public export %inline
|
||||
(.qty) : SQty -> Qty
|
||||
(SZero).qty = Zero
|
||||
(SOne).qty = One
|
||||
|
||||
namespace GQty
|
||||
public export %inline
|
||||
(.qty) : GQty -> Qty
|
||||
(GZero).qty = Zero
|
||||
(GAny).qty = Any
|
||||
|
|
|
|||
|
|
@ -155,6 +155,12 @@ mutual
|
|||
(loc : Loc) ->
|
||||
Elim d n
|
||||
|
||||
||| first element of a pair. only works in non-linear contexts.
|
||||
Fst : (pair : Elim d n) -> (loc : Loc) -> Elim d n
|
||||
|
||||
||| second element of a pair. only works in non-linear contexts.
|
||||
Snd : (pair : Elim d n) -> (loc : Loc) -> Elim d n
|
||||
|
||||
||| enum matching
|
||||
CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
|
||||
(ret : ScopeTerm d n) ->
|
||||
|
|
@ -369,6 +375,8 @@ Located (Elim d n) where
|
|||
(B _ loc).loc = loc
|
||||
(App _ _ loc).loc = loc
|
||||
(CasePair _ _ _ _ loc).loc = loc
|
||||
(Fst _ loc).loc = loc
|
||||
(Snd _ loc).loc = loc
|
||||
(CaseEnum _ _ _ _ loc).loc = loc
|
||||
(CaseNat _ _ _ _ _ _ loc).loc = loc
|
||||
(CaseBox _ _ _ _ loc).loc = loc
|
||||
|
|
@ -417,6 +425,8 @@ Relocatable (Elim d n) where
|
|||
setLoc loc (App fun arg _) = App fun arg loc
|
||||
setLoc loc (CasePair qty pair ret body _) =
|
||||
CasePair qty pair ret body loc
|
||||
setLoc loc (Fst pair _) = Fst pair loc
|
||||
setLoc loc (Snd pair _) = Fst pair loc
|
||||
setLoc loc (CaseEnum qty tag ret arms _) =
|
||||
CaseEnum qty tag ret arms loc
|
||||
setLoc loc (CaseNat qty qtyIH nat ret zero succ _) =
|
||||
|
|
|
|||
|
|
@ -493,6 +493,16 @@ prettyElim dnames tnames (CasePair qty pair ret body _) = do
|
|||
prettyCase dnames tnames qty pair ret
|
||||
[MkCaseArm pat [<] [< x, y] body.term]
|
||||
|
||||
prettyElim dnames tnames (Fst pair _) =
|
||||
parensIfM App =<< do
|
||||
pair <- prettyTArg dnames tnames (E pair)
|
||||
prettyAppD !fstD [pair]
|
||||
|
||||
prettyElim dnames tnames (Snd pair _) =
|
||||
parensIfM App =<< do
|
||||
pair <- prettyTArg dnames tnames (E pair)
|
||||
prettyAppD !sndD [pair]
|
||||
|
||||
prettyElim dnames tnames (CaseEnum qty tag ret arms _) = do
|
||||
arms <- for (SortedMap.toList arms) $ \(tag, body) =>
|
||||
pure $ MkCaseArm !(prettyTag tag) [<] [<] body
|
||||
|
|
|
|||
|
|
@ -299,6 +299,10 @@ mutual
|
|||
nclo $ App (f // th // ph) (s // th // ph) loc
|
||||
pushSubstsWith th ph (CasePair pi p r b loc) =
|
||||
nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
|
||||
pushSubstsWith th ph (Fst pair loc) =
|
||||
nclo $ Fst (pair // th // ph) loc
|
||||
pushSubstsWith th ph (Snd pair loc) =
|
||||
nclo $ Snd (pair // th // ph) loc
|
||||
pushSubstsWith th ph (CaseEnum pi t r arms loc) =
|
||||
nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
|
||||
(map (\b => b // th // ph) arms) loc
|
||||
|
|
|
|||
|
|
@ -87,6 +87,10 @@ mutual
|
|||
<*> tightenS p ret
|
||||
<*> tightenS p body
|
||||
<*> pure loc
|
||||
tightenE' p (Fst pair loc) =
|
||||
Fst <$> tightenE p pair <*> pure loc
|
||||
tightenE' p (Snd pair loc) =
|
||||
Snd <$> tightenE p pair <*> pure loc
|
||||
tightenE' p (CaseEnum qty tag ret arms loc) =
|
||||
CaseEnum qty <$> tightenE p tag
|
||||
<*> tightenS p ret
|
||||
|
|
@ -202,6 +206,10 @@ mutual
|
|||
<*> dtightenS p ret
|
||||
<*> dtightenS p body
|
||||
<*> pure loc
|
||||
dtightenE' p (Fst pair loc) =
|
||||
Fst <$> dtightenE p pair <*> pure loc
|
||||
dtightenE' p (Snd pair loc) =
|
||||
Snd <$> dtightenE p pair <*> pure loc
|
||||
dtightenE' p (CaseEnum qty tag ret arms loc) =
|
||||
CaseEnum qty <$> dtightenE p tag
|
||||
<*> dtightenS p ret
|
||||
|
|
|
|||
|
|
@ -88,7 +88,7 @@ mutual
|
|||
||| `check0 ctx subj ty` checks a term (as `check`) in a zero context.
|
||||
export covering %inline
|
||||
check0 : TyContext d n -> Term d n -> Term d n -> Eff TC ()
|
||||
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
|
||||
|
||||
||| `check`, assuming the dimension context is consistent
|
||||
|
|
@ -96,7 +96,7 @@ mutual
|
|||
checkC : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n ->
|
||||
Eff TC (CheckResult' n)
|
||||
checkC ctx sg subj ty =
|
||||
wrapErr (WhileChecking ctx sg.fst subj ty) $
|
||||
wrapErr (WhileChecking ctx sg subj ty) $
|
||||
checkCNoWrap ctx sg subj ty
|
||||
|
||||
export covering %inline
|
||||
|
|
@ -142,7 +142,7 @@ mutual
|
|||
inferC : (ctx : TyContext d n) -> SQty -> Elim d n ->
|
||||
Eff TC (InferResult' d n)
|
||||
inferC ctx sg subj =
|
||||
wrapErr (WhileInferring ctx sg.fst subj) $
|
||||
wrapErr (WhileInferring ctx sg subj) $
|
||||
let Element subj nc = pushSubsts subj in
|
||||
infer' ctx sg subj
|
||||
|
||||
|
|
@ -152,8 +152,8 @@ mutual
|
|||
(subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
|
||||
Eff TC (CheckResult' n)
|
||||
toCheckType ctx sg t ty = do
|
||||
u <- expectTYPE !(askAt DEFS) ctx ty.loc ty
|
||||
expectEqualQ t.loc Zero sg.fst
|
||||
u <- expectTYPE !(askAt DEFS) ctx sg ty.loc ty
|
||||
expectEqualQ t.loc Zero sg.qty
|
||||
checkTypeNoWrap ctx t (Just u)
|
||||
pure $ zeroFor ctx
|
||||
|
||||
|
|
@ -167,10 +167,10 @@ mutual
|
|||
check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (Lam body loc) ty = do
|
||||
(qty, arg, res) <- expectPi !(askAt DEFS) ctx ty.loc ty
|
||||
(qty, arg, res) <- expectPi !(askAt DEFS) ctx SZero ty.loc ty
|
||||
-- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
|
||||
-- with ρ ≤ σπ
|
||||
let qty' = sg.fst * qty
|
||||
let qty' = sg.qty * qty
|
||||
qout <- checkC (extendTy qty' body.name arg ctx) sg body.term res.term
|
||||
-- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
|
||||
popQ loc qty' qout
|
||||
|
|
@ -178,7 +178,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 !(askAt DEFS) ctx ty.loc ty
|
||||
(tfst, tsnd) <- expectSig !(askAt DEFS) ctx SZero ty.loc ty
|
||||
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
|
||||
qfst <- checkC ctx sg fst tfst
|
||||
let tsnd = sub1 tsnd (Ann fst tfst fst.loc)
|
||||
|
|
@ -190,7 +190,7 @@ mutual
|
|||
check' ctx sg t@(Enum {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (Tag t loc) ty = do
|
||||
tags <- expectEnum !(askAt DEFS) ctx ty.loc ty
|
||||
tags <- expectEnum !(askAt DEFS) ctx SZero ty.loc ty
|
||||
-- if t ∈ ts
|
||||
unless (t `elem` tags) $ throw $ TagNotIn loc t tags
|
||||
-- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
|
||||
|
|
@ -199,33 +199,35 @@ mutual
|
|||
check' ctx sg t@(Eq {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (DLam body loc) ty = do
|
||||
(ty, l, r) <- expectEq !(askAt DEFS) ctx ty.loc ty
|
||||
(ty, l, r) <- expectEq !(askAt DEFS) ctx SZero ty.loc ty
|
||||
let ctx' = extendDim body.name ctx
|
||||
ty = ty.term
|
||||
body = body.term
|
||||
-- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ
|
||||
qout <- checkC ctx' sg body ty
|
||||
-- if Ψ, i, i = 0 | Γ ⊢ t = l : A
|
||||
lift $ equal loc (eqDim (B VZ loc) (K Zero loc) ctx') ty body (dweakT 1 l)
|
||||
let ctx0 = eqDim (B VZ loc) (K Zero loc) ctx'
|
||||
lift $ equal loc ctx0 sg ty body $ dweakT 1 l
|
||||
-- if Ψ, i, i = 1 | Γ ⊢ t = r : A
|
||||
lift $ equal loc (eqDim (B VZ loc) (K One loc) ctx') ty body (dweakT 1 r)
|
||||
let ctx1 = eqDim (B VZ loc) (K One loc) ctx'
|
||||
lift $ equal loc ctx1 sg ty body $ dweakT 1 r
|
||||
-- then Ψ | Γ ⊢ σ · (δ i ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
|
||||
pure qout
|
||||
|
||||
check' ctx sg t@(Nat {}) ty = toCheckType ctx sg t ty
|
||||
|
||||
check' ctx sg (Zero {}) ty = do
|
||||
expectNat !(askAt DEFS) ctx ty.loc ty
|
||||
expectNat !(askAt DEFS) ctx SZero ty.loc ty
|
||||
pure $ zeroFor ctx
|
||||
|
||||
check' ctx sg (Succ n {}) ty = do
|
||||
expectNat !(askAt DEFS) ctx ty.loc ty
|
||||
expectNat !(askAt DEFS) ctx SZero 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 !(askAt DEFS) ctx ty.loc ty
|
||||
(q, ty) <- expectBOX !(askAt DEFS) ctx SZero ty.loc ty
|
||||
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
|
||||
valout <- checkC ctx sg val ty
|
||||
-- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
|
||||
|
|
@ -299,11 +301,11 @@ mutual
|
|||
|
||||
checkType' ctx (E e) u = do
|
||||
-- if Ψ | Γ ⊢₀ E ⇒ Type ℓ
|
||||
infres <- inferC ctx szero e
|
||||
infres <- inferC ctx SZero e
|
||||
-- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
|
||||
case u of
|
||||
Just u => lift $ subtype e.loc ctx infres.type (TYPE u noLoc)
|
||||
Nothing => ignore $ expectTYPE !(askAt DEFS) ctx e.loc infres.type
|
||||
Nothing => ignore $ expectTYPE !(askAt DEFS) ctx SZero e.loc infres.type
|
||||
-- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
|
||||
|
||||
|
||||
|
|
@ -324,7 +326,7 @@ mutual
|
|||
-- if π·x : A {≔ s} in global context
|
||||
g <- lookupFree x loc !(askAt DEFS)
|
||||
-- if σ ≤ π
|
||||
expectCompatQ loc sg.fst g.qty.fst
|
||||
expectCompatQ loc sg.qty g.qty.qty
|
||||
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
|
||||
let Val d = ctx.dimLen; Val n = ctx.termLen
|
||||
pure $ InfRes {type = g.typeAt u, qout = zeroFor ctx}
|
||||
|
|
@ -332,7 +334,7 @@ mutual
|
|||
infer' ctx sg (B i _) =
|
||||
-- if x : A ∈ Γ
|
||||
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ (𝟎, σ·x, 𝟎)
|
||||
pure $ lookupBound sg.fst i ctx.tctx
|
||||
pure $ lookupBound sg.qty i ctx.tctx
|
||||
where
|
||||
lookupBound : forall n. Qty -> Var n -> TContext d n -> InferResult' d n
|
||||
lookupBound pi VZ (ctx :< type) =
|
||||
|
|
@ -344,7 +346,7 @@ mutual
|
|||
infer' ctx sg (App fun arg loc) = do
|
||||
-- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
|
||||
funres <- inferC ctx sg fun
|
||||
(qty, argty, res) <- expectPi !(askAt DEFS) ctx fun.loc funres.type
|
||||
(qty, argty, res) <- expectPi !(askAt DEFS) ctx SZero fun.loc funres.type
|
||||
-- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
|
||||
argout <- checkC ctx (subjMult sg qty) arg argty
|
||||
-- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + πΣ₂
|
||||
|
|
@ -361,12 +363,12 @@ 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 !(askAt DEFS) ctx pair.loc pairres.type
|
||||
(tfst, tsnd) <- expectSig !(askAt DEFS) ctx SZero pair.loc pairres.type
|
||||
-- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
|
||||
-- ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
|
||||
-- with ρ₁, ρ₂ ≤ πσ
|
||||
let [< x, y] = body.names
|
||||
pisg = pi * sg.fst
|
||||
pisg = pi * sg.qty
|
||||
bodyctx = extendTyN [< (pisg, x, tfst), (pisg, y, tsnd.term)] ctx
|
||||
bodyty = substCasePairRet body.names pairres.type ret
|
||||
bodyout <- checkC bodyctx sg body.term bodyty >>=
|
||||
|
|
@ -377,10 +379,30 @@ mutual
|
|||
qout = pi * pairres.qout + bodyout
|
||||
}
|
||||
|
||||
infer' ctx sg (Fst pair loc) = do
|
||||
-- if Ψ | Γ ⊢ σ · e ⇒ (x : A) × B ⊳ Σ
|
||||
pairres <- inferC ctx sg pair
|
||||
(tfst, _) <- expectSig !(askAt DEFS) ctx SZero pair.loc pairres.type
|
||||
-- then Ψ | Γ ⊢ σ · fst e ⇒ A ⊳ ωΣ
|
||||
pure $ InfRes {
|
||||
type = tfst,
|
||||
qout = Any * pairres.qout
|
||||
}
|
||||
|
||||
infer' ctx sg (Snd pair loc) = do
|
||||
-- if Ψ | Γ ⊢ σ · e ⇒ (x : A) × B ⊳ Σ
|
||||
pairres <- inferC ctx sg pair
|
||||
(_, tsnd) <- expectSig !(askAt DEFS) ctx SZero pair.loc pairres.type
|
||||
-- then Ψ | Γ ⊢ σ · snd e ⇒ B[fst e/x] ⊳ ωΣ
|
||||
pure $ InfRes {
|
||||
type = sub1 tsnd (Fst pair loc),
|
||||
qout = Any * pairres.qout
|
||||
}
|
||||
|
||||
infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do
|
||||
-- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
|
||||
tres <- inferC ctx sg t
|
||||
ttags <- expectEnum !(askAt DEFS) ctx t.loc tres.type
|
||||
ttags <- expectEnum !(askAt DEFS) ctx SZero 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
|
||||
|
|
@ -404,7 +426,7 @@ mutual
|
|||
-- if Ψ | Γ ⊢ σ · n ⇒ ℕ ⊳ Σn
|
||||
nres <- inferC ctx sg n
|
||||
let nat = nres.type
|
||||
expectNat !(askAt DEFS) ctx n.loc nat
|
||||
expectNat !(askAt DEFS) ctx SZero n.loc nat
|
||||
-- if Ψ | Γ, n : ℕ ⊢₀ A ⇐ Type
|
||||
checkTypeC (extendTy Zero ret.name nat ctx) ret.term Nothing
|
||||
-- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
|
||||
|
|
@ -412,11 +434,11 @@ mutual
|
|||
-- if Ψ | Γ, n : ℕ, ih : A ⊢ σ · suc ⇐ A[succ p ∷ ℕ/n] ⊳ Σs, ρ₁.p, ρ₂.ih
|
||||
-- with ρ₂ ≤ π'σ, (ρ₁ + ρ₂) ≤ πσ
|
||||
let [< p, ih] = suc.names
|
||||
pisg = pi * sg.fst
|
||||
pisg = pi * sg.qty
|
||||
sucCtx = extendTyN [< (pisg, p, Nat p.loc), (pi', ih, ret.term)] ctx
|
||||
sucType = substCaseSuccRet suc.names ret
|
||||
sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
|
||||
expectCompatQ loc qih (pi' * sg.fst)
|
||||
expectCompatQ loc qih (pi' * sg.qty)
|
||||
-- [fixme] better error here
|
||||
expectCompatQ loc (qp + qih) pisg
|
||||
-- then Ψ | Γ ⊢ caseπ ⋯ ⇒ A[n] ⊳ πΣn + Σz + ωΣs
|
||||
|
|
@ -428,12 +450,12 @@ mutual
|
|||
infer' ctx sg (CaseBox pi box ret body loc) = do
|
||||
-- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
|
||||
boxres <- inferC ctx sg box
|
||||
(q, ty) <- expectBOX !(askAt DEFS) ctx box.loc boxres.type
|
||||
(q, ty) <- expectBOX !(askAt DEFS) ctx SZero 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
|
||||
-- with ς ≤ ρπσ
|
||||
let qpisg = q * pi * sg.fst
|
||||
let qpisg = q * pi * sg.qty
|
||||
bodyCtx = extendTy qpisg body.name ty ctx
|
||||
bodyType = substCaseBoxRet body.name ty ret
|
||||
bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ loc qpisg
|
||||
|
|
@ -446,7 +468,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 !(askAt DEFS) ctx fun.loc type
|
||||
ty <- fst <$> expectEq !(askAt DEFS) ctx SZero fun.loc type
|
||||
-- then Ψ | Γ ⊢ σ · f p ⇒ A‹p/𝑖› ⊳ Σ
|
||||
pure $ InfRes {type = dsub1 ty dim, qout}
|
||||
|
||||
|
|
@ -462,19 +484,20 @@ mutual
|
|||
ctx0 = extendDim j0 $ eqDim r (K Zero j0.loc) ctx
|
||||
val0 = getTerm val0
|
||||
qout0 <- check ctx0 sg val0 ty'
|
||||
lift $ equal loc (eqDim (B VZ p.loc) p' ctx0) ty' val0 val'
|
||||
lift $ equal loc (eqDim (B VZ p.loc) p' ctx0) sg ty' val0 val'
|
||||
let ctx1 = extendDim j1 $ eqDim r (K One j1.loc) ctx
|
||||
val1 = getTerm val1
|
||||
qout1 <- check ctx1 sg val1 ty'
|
||||
lift $ equal loc (eqDim (B VZ p.loc) p' ctx1) ty' val1 val'
|
||||
lift $ equal loc (eqDim (B VZ p.loc) p' ctx1) sg ty' val1 val'
|
||||
let qouts = qout :: catMaybes [toMaybe qout0, toMaybe qout1]
|
||||
pure $ InfRes {type = ty, qout = lubs ctx qouts}
|
||||
|
||||
infer' ctx sg (TypeCase ty ret arms def loc) = do
|
||||
-- if σ = 0
|
||||
expectEqualQ loc Zero sg.fst
|
||||
expectEqualQ loc Zero sg.qty
|
||||
-- if Ψ, Γ ⊢₀ e ⇒ Type u
|
||||
u <- expectTYPE !(askAt DEFS) ctx ty.loc . type =<< inferC ctx szero ty
|
||||
u <- inferC ctx SZero ty >>=
|
||||
expectTYPE !(askAt DEFS) ctx SZero ty.loc . type
|
||||
-- if Ψ, Γ ⊢₀ C ⇐ Type (non-dependent return type)
|
||||
checkTypeC ctx ret Nothing
|
||||
-- if Ψ, Γ' ⊢₀ A ⇐ C for each rhs A
|
||||
|
|
|
|||
|
|
@ -67,13 +67,13 @@ substCaseBoxRet x dty retty =
|
|||
|
||||
parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
|
||||
namespace TyContext
|
||||
parameters (ctx : TyContext d n) (loc : Loc)
|
||||
parameters (ctx : TyContext d n) (sg : SQty) (loc : Loc)
|
||||
export covering
|
||||
whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
|
||||
tm d n -> Eff fs (NonRedex tm d n defs)
|
||||
tm d n -> Eff fs (NonRedex tm d n defs sg)
|
||||
whnf tm = do
|
||||
let Val n = ctx.termLen; Val d = ctx.dimLen
|
||||
res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) tm
|
||||
res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
|
||||
rethrow res
|
||||
|
||||
private covering %macro
|
||||
|
|
@ -113,13 +113,13 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
|
|||
|
||||
|
||||
namespace EqContext
|
||||
parameters (ctx : EqContext n) (loc : Loc)
|
||||
parameters (ctx : EqContext n) (sg : SQty) (loc : Loc)
|
||||
export covering
|
||||
whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
|
||||
tm 0 n -> Eff fs (NonRedex tm 0 n defs)
|
||||
tm 0 n -> Eff fs (NonRedex tm 0 n defs sg)
|
||||
whnf tm = do
|
||||
let Val n = ctx.termLen
|
||||
res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) tm
|
||||
res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
|
||||
rethrow res
|
||||
|
||||
private covering %macro
|
||||
|
|
|
|||
|
|
@ -87,7 +87,7 @@ data Error
|
|||
|
||||
-- extra context
|
||||
| WhileChecking
|
||||
(TyContext d n) Qty
|
||||
(TyContext d n) SQty
|
||||
(Term d n) -- term
|
||||
(Term d n) -- type
|
||||
Error
|
||||
|
|
@ -97,16 +97,16 @@ data Error
|
|||
(Maybe Universe)
|
||||
Error
|
||||
| WhileInferring
|
||||
(TyContext d n) Qty
|
||||
(TyContext d n) SQty
|
||||
(Elim d n)
|
||||
Error
|
||||
| WhileComparingT
|
||||
(EqContext n) EqMode
|
||||
(EqContext n) EqMode SQty
|
||||
(Term 0 n) -- type
|
||||
(Term 0 n) (Term 0 n) -- lhs/rhs
|
||||
Error
|
||||
| WhileComparingE
|
||||
(EqContext n) EqMode
|
||||
(EqContext n) EqMode SQty
|
||||
(Elim 0 n) (Elim 0 n)
|
||||
Error
|
||||
%name Error err
|
||||
|
|
@ -119,31 +119,31 @@ ErrorEff = Except Error
|
|||
|
||||
export
|
||||
Located Error where
|
||||
(ExpectedTYPE loc _ _).loc = loc
|
||||
(ExpectedPi loc _ _).loc = loc
|
||||
(ExpectedSig loc _ _).loc = loc
|
||||
(ExpectedEnum loc _ _).loc = loc
|
||||
(ExpectedEq loc _ _).loc = loc
|
||||
(ExpectedNat loc _ _).loc = loc
|
||||
(ExpectedBOX loc _ _).loc = loc
|
||||
(BadUniverse loc _ _).loc = loc
|
||||
(TagNotIn loc _ _).loc = loc
|
||||
(BadCaseEnum loc _ _).loc = loc
|
||||
(BadQtys loc _ _ _).loc = loc
|
||||
(ClashT loc _ _ _ _ _).loc = loc
|
||||
(ClashTy loc _ _ _ _).loc = loc
|
||||
(ClashE loc _ _ _ _).loc = loc
|
||||
(ClashU loc _ _ _).loc = loc
|
||||
(ClashQ loc _ _).loc = loc
|
||||
(NotInScope loc _).loc = loc
|
||||
(NotType loc _ _).loc = loc
|
||||
(WrongType loc _ _ _).loc = loc
|
||||
(MissingEnumArm loc _ _).loc = loc
|
||||
(WhileChecking _ _ _ _ err).loc = err.loc
|
||||
(WhileCheckingTy _ _ _ err).loc = err.loc
|
||||
(WhileInferring _ _ _ err).loc = err.loc
|
||||
(WhileComparingT _ _ _ _ _ err).loc = err.loc
|
||||
(WhileComparingE _ _ _ _ err).loc = err.loc
|
||||
(ExpectedTYPE loc _ _).loc = loc
|
||||
(ExpectedPi loc _ _).loc = loc
|
||||
(ExpectedSig loc _ _).loc = loc
|
||||
(ExpectedEnum loc _ _).loc = loc
|
||||
(ExpectedEq loc _ _).loc = loc
|
||||
(ExpectedNat loc _ _).loc = loc
|
||||
(ExpectedBOX loc _ _).loc = loc
|
||||
(BadUniverse loc _ _).loc = loc
|
||||
(TagNotIn loc _ _).loc = loc
|
||||
(BadCaseEnum loc _ _).loc = loc
|
||||
(BadQtys loc _ _ _).loc = loc
|
||||
(ClashT loc _ _ _ _ _).loc = loc
|
||||
(ClashTy loc _ _ _ _).loc = loc
|
||||
(ClashE loc _ _ _ _).loc = loc
|
||||
(ClashU loc _ _ _).loc = loc
|
||||
(ClashQ loc _ _).loc = loc
|
||||
(NotInScope loc _).loc = loc
|
||||
(NotType loc _ _).loc = loc
|
||||
(WrongType loc _ _ _).loc = loc
|
||||
(MissingEnumArm loc _ _).loc = loc
|
||||
(WhileChecking _ _ _ _ err).loc = err.loc
|
||||
(WhileCheckingTy _ _ _ err).loc = err.loc
|
||||
(WhileInferring _ _ _ err).loc = err.loc
|
||||
(WhileComparingT _ _ _ _ _ _ err).loc = err.loc
|
||||
(WhileComparingE _ _ _ _ _ err).loc = err.loc
|
||||
|
||||
|
||||
||| separates out all the error context layers
|
||||
|
|
@ -156,10 +156,10 @@ explodeContext (WhileCheckingTy ctx s k err) =
|
|||
mapFst (WhileCheckingTy ctx s k ::) $ explodeContext err
|
||||
explodeContext (WhileInferring ctx x e err) =
|
||||
mapFst (WhileInferring ctx x e ::) $ explodeContext err
|
||||
explodeContext (WhileComparingT ctx x s t r err) =
|
||||
mapFst (WhileComparingT ctx x s t r ::) $ explodeContext err
|
||||
explodeContext (WhileComparingE ctx x e f err) =
|
||||
mapFst (WhileComparingE ctx x e f ::) $ explodeContext err
|
||||
explodeContext (WhileComparingT ctx x sg s t r err) =
|
||||
mapFst (WhileComparingT ctx x sg s t r ::) $ explodeContext err
|
||||
explodeContext (WhileComparingE ctx x sg e f err) =
|
||||
mapFst (WhileComparingE ctx x sg e f ::) $ explodeContext err
|
||||
explodeContext err = ([], err)
|
||||
|
||||
||| leaves the outermost context layer, and the innermost (up to) n, and removes
|
||||
|
|
@ -342,12 +342,12 @@ prettyErrorNoLoc showContext = \case
|
|||
sep [hsep ["the tag", !(prettyTag tag), "is not contained in"],
|
||||
!(prettyTerm [<] [<] $ Enum (fromList tags) noLoc)]
|
||||
|
||||
WhileChecking ctx pi s a err =>
|
||||
WhileChecking ctx sg s a err =>
|
||||
[|vappendBlank
|
||||
(inTContext ctx . sep =<< sequence
|
||||
[hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames s),
|
||||
hangDSingle "has type" !(prettyTerm ctx.dnames ctx.tnames a),
|
||||
hangDSingle "with quantity" !(prettyQty pi)])
|
||||
hangDSingle "with quantity" !(prettyQty sg.qty)])
|
||||
(prettyErrorNoLoc showContext err)|]
|
||||
|
||||
WhileCheckingTy ctx a k err =>
|
||||
|
|
@ -357,29 +357,31 @@ prettyErrorNoLoc showContext = \case
|
|||
pure $ text $ isTypeInUniverse k])
|
||||
(prettyErrorNoLoc showContext err)|]
|
||||
|
||||
WhileInferring ctx pi e err =>
|
||||
WhileInferring ctx sg e err =>
|
||||
[|vappendBlank
|
||||
(inTContext ctx . sep =<< sequence
|
||||
[hangDSingle "while inferring the type of"
|
||||
!(prettyElim ctx.dnames ctx.tnames e),
|
||||
hangDSingle "with quantity" !(prettyQty pi)])
|
||||
hangDSingle "with quantity" !(prettyQty sg.qty)])
|
||||
(prettyErrorNoLoc showContext err)|]
|
||||
|
||||
WhileComparingT ctx mode a s t err =>
|
||||
WhileComparingT ctx mode sg a s t err =>
|
||||
[|vappendBlank
|
||||
(inEContext ctx . sep =<< sequence
|
||||
[hangDSingle "while checking that" !(prettyTerm [<] ctx.tnames s),
|
||||
hangDSingle (text "is \{prettyMode mode}")
|
||||
!(prettyTerm [<] ctx.tnames t),
|
||||
hangDSingle "at type" !(prettyTerm [<] ctx.tnames a)])
|
||||
hangDSingle "at type" !(prettyTerm [<] ctx.tnames a),
|
||||
hangDSingle "with quantity" !(prettyQty sg.qty)])
|
||||
(prettyErrorNoLoc showContext err)|]
|
||||
|
||||
WhileComparingE ctx mode e f err =>
|
||||
WhileComparingE ctx mode sg e f err =>
|
||||
[|vappendBlank
|
||||
(inEContext ctx . sep =<< sequence
|
||||
[hangDSingle "while checking that" !(prettyElim [<] ctx.tnames e),
|
||||
hangDSingle (text "is \{prettyMode mode}")
|
||||
!(prettyElim [<] ctx.tnames f)])
|
||||
!(prettyElim [<] ctx.tnames f),
|
||||
hangDSingle "with quantity" !(prettyQty sg.qty)])
|
||||
(prettyErrorNoLoc showContext err)|]
|
||||
|
||||
where
|
||||
|
|
|
|||
|
|
@ -23,12 +23,12 @@ where
|
|||
|
||||
parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
||||
{auto _ : CanWhnf Elim Interface.isRedexE}
|
||||
{d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
|
||||
{d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
|
||||
||| reduce a function application `App (Coe ty p q val) s loc`
|
||||
export covering
|
||||
piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
|
||||
(val, s : Term d n) -> Loc ->
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
|
||||
piCoe sty@(S [< i] ty) p q val s loc = do
|
||||
-- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
|
||||
-- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
|
||||
|
|
@ -36,23 +36,23 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
--
|
||||
-- type-case is used to expose A,B if the type is neutral
|
||||
let ctx1 = extendDim i ctx
|
||||
Element ty tynf <- whnf defs ctx1 $ getTerm ty
|
||||
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
|
||||
(arg, res) <- tycasePi defs ctx1 ty
|
||||
let s0 = CoeT i arg q p s s.loc
|
||||
body = E $ App (Ann val (ty // one p) val.loc) (E s0) loc
|
||||
s1 = CoeT i (arg // (BV 0 i.loc ::: shift 2)) (weakD 1 q) (BV 0 i.loc)
|
||||
(s // shift 1) s.loc
|
||||
whnf defs ctx $ CoeT i (sub1 res s1) p q body loc
|
||||
whnf defs ctx sg $ CoeT i (sub1 res s1) p q body loc
|
||||
|
||||
||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body loc`
|
||||
export covering
|
||||
sigCoe : (qty : Qty) ->
|
||||
(ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
|
||||
(ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc ->
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
|
||||
sigCoe qty sty@(S [< i] ty) p q val ret body loc = do
|
||||
-- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
|
||||
-- ⇝
|
||||
-- ⇝
|
||||
-- caseπ s ∷ ((x : A) × B)‹p/i› return z ⇒ C
|
||||
-- of { (a, b) ⇒
|
||||
-- e[(coe [i ⇒ A] @p @q a)/a,
|
||||
|
|
@ -60,7 +60,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
--
|
||||
-- type-case is used to expose A,B if the type is neutral
|
||||
let ctx1 = extendDim i ctx
|
||||
Element ty tynf <- whnf defs ctx1 $ getTerm ty
|
||||
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
|
||||
(tfst, tsnd) <- tycaseSig defs ctx1 ty
|
||||
let [< x, y] = body.names
|
||||
a' = CoeT i (weakT 2 tfst) p q (BVT 1 noLoc) x.loc
|
||||
|
|
@ -68,41 +68,81 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
(CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2))
|
||||
(weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2)
|
||||
b' = CoeT i tsnd' p q (BVT 0 noLoc) y.loc
|
||||
whnf defs ctx $ CasePair qty (Ann val (ty // one p) val.loc) ret
|
||||
whnf defs ctx sg $ CasePair qty (Ann val (ty // one p) val.loc) ret
|
||||
(ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc
|
||||
|
||||
||| reduce a pair projection `Fst (Coe ty p q val) loc`
|
||||
export covering
|
||||
fstCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
|
||||
Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
|
||||
fstCoe sty@(S [< i] ty) p q val loc = do
|
||||
-- fst (coe (𝑖 ⇒ (x : A) × B) @p @q s)
|
||||
-- ⇝
|
||||
-- coe (𝑖 ⇒ A) @p @q (fst (s ∷ (x : A‹p/𝑖›) × B‹p/𝑖›))
|
||||
--
|
||||
-- type-case is used to expose A,B if the type is neutral
|
||||
let ctx1 = extendDim i ctx
|
||||
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
|
||||
(tfst, _) <- tycaseSig defs ctx1 ty
|
||||
whnf defs ctx sg $
|
||||
Coe (ST [< i] tfst) p q
|
||||
(E (Fst (Ann val (ty // one p) val.loc) val.loc)) loc
|
||||
|
||||
||| reduce a pair projection `Snd (Coe ty p q val) loc`
|
||||
export covering
|
||||
sndCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
|
||||
Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
|
||||
sndCoe sty@(S [< i] ty) p q val loc = do
|
||||
-- snd (coe (𝑖 ⇒ (x : A) × B) @p @q s)
|
||||
-- ⇝
|
||||
-- coe (𝑖 ⇒ B[coe (𝑗 ⇒ A‹𝑗/𝑖›) @p @𝑖 (fst (s ∷ (x : A) × B))/x]) @p @q
|
||||
-- (snd (s ∷ (x : A‹p/𝑖›) × B‹p/𝑖›))
|
||||
--
|
||||
-- type-case is used to expose A,B if the type is neutral
|
||||
let ctx1 = extendDim i ctx
|
||||
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
|
||||
(tfst, tsnd) <- tycaseSig defs ctx1 ty
|
||||
whnf defs ctx sg $
|
||||
Coe (ST [< i] $ sub1 tsnd $
|
||||
Coe (ST [< !(fresh i)] $ tfst // (BV 0 i.loc ::: shift 2))
|
||||
(weakD 1 p) (BV 0 loc)
|
||||
(E (Fst (Ann (dweakT 1 val) ty val.loc) val.loc)) loc)
|
||||
p q
|
||||
(E (Snd (Ann val (ty // one p) val.loc) val.loc))
|
||||
loc
|
||||
|
||||
||| reduce a dimension application `DApp (Coe ty p q val) r loc`
|
||||
export covering
|
||||
eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
|
||||
(r : Dim d) -> Loc ->
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
|
||||
eqCoe sty@(S [< j] ty) p q val r loc = do
|
||||
-- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
|
||||
-- ⇝
|
||||
-- ⇝
|
||||
-- comp [j ⇒ A‹r/i›] @p @q (eq ∷ (Eq [i ⇒ A] L R)‹p/j›)
|
||||
-- @r { 0 j ⇒ L; 1 j ⇒ R }
|
||||
let ctx1 = extendDim j ctx
|
||||
Element ty tynf <- whnf defs ctx1 $ getTerm ty
|
||||
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
|
||||
(a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
|
||||
let a' = dsub1 a (weakD 1 r)
|
||||
val' = E $ DApp (Ann val (ty // one p) val.loc) r loc
|
||||
whnf defs ctx $ CompH j a' p q val' r j s j t loc
|
||||
whnf defs ctx sg $ CompH j a' p q val' r j s j t loc
|
||||
|
||||
||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body`
|
||||
export covering
|
||||
boxCoe : (qty : Qty) ->
|
||||
(ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
|
||||
(ret : ScopeTerm d n) -> (body : ScopeTerm d n) -> Loc ->
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
|
||||
boxCoe qty sty@(S [< i] ty) p q val ret body loc = do
|
||||
-- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
|
||||
-- ⇝
|
||||
-- ⇝
|
||||
-- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
|
||||
let ctx1 = extendDim i ctx
|
||||
Element ty tynf <- whnf defs ctx1 $ getTerm ty
|
||||
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
|
||||
ta <- tycaseBOX defs ctx1 ty
|
||||
let a' = CoeT i (weakT 1 ta) p q (BVT 0 noLoc) body.name.loc
|
||||
whnf defs ctx $ CaseBox qty (Ann val (ty // one p) val.loc) ret
|
||||
whnf defs ctx sg $ CaseBox qty (Ann val (ty // one p) val.loc) ret
|
||||
(ST body.names $ body.term // (a' ::: shift 1)) loc
|
||||
|
||||
|
||||
|
|
@ -110,13 +150,13 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
export covering
|
||||
pushCoe : BindName ->
|
||||
(ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc ->
|
||||
(0 pc : So (canPushCoe ty s)) =>
|
||||
Eff Whnf (NonRedex Elim d n defs)
|
||||
(0 pc : So (canPushCoe sg ty s)) =>
|
||||
Eff Whnf (NonRedex Elim d n defs sg)
|
||||
pushCoe i ty p q s loc =
|
||||
case ty of
|
||||
-- (coe ★ᵢ @_ @_ s) ⇝ (s ∷ ★ᵢ)
|
||||
TYPE l tyLoc =>
|
||||
whnf defs ctx $ Ann s (TYPE l tyLoc) loc
|
||||
whnf defs ctx sg $ Ann s (TYPE l tyLoc) loc
|
||||
|
||||
-- η expand it so that whnf for App can deal with it
|
||||
--
|
||||
|
|
@ -125,7 +165,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
-- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) ∷ (π.(x : A) → B)‹q/𝑖›
|
||||
Pi {} =>
|
||||
let inner = Coe (SY [< i] ty) p q s loc in
|
||||
whnf defs ctx $
|
||||
whnf defs ctx sg $
|
||||
Ann (LamY !(mnb "y" loc)
|
||||
(E $ App (weakE 1 inner) (BVT 0 loc) loc) loc)
|
||||
(ty // one q) loc
|
||||
|
|
@ -147,12 +187,12 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
(tfst // (BV 0 loc ::: shift 2))
|
||||
(weakD 1 p) (BV 0 loc) (dweakT 1 s) fst.loc
|
||||
snd' = CoeT i (sub1 tsnd fstInSnd) p q snd snd.loc
|
||||
whnf defs ctx $
|
||||
whnf defs ctx sg $
|
||||
Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc
|
||||
|
||||
-- (coe {𝐚̄} @_ @_ s) ⇝ (s ∷ {𝐚̄})
|
||||
Enum cases tyLoc =>
|
||||
whnf defs ctx $ Ann s (Enum cases tyLoc) loc
|
||||
whnf defs ctx sg $ Ann s (Enum cases tyLoc) loc
|
||||
|
||||
-- η expand, same as for Π
|
||||
--
|
||||
|
|
@ -161,14 +201,14 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
-- (δ 𝑘 ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @𝑘) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›
|
||||
Eq {} =>
|
||||
let inner = Coe (SY [< i] ty) p q s loc in
|
||||
whnf defs ctx $
|
||||
whnf defs ctx sg $
|
||||
Ann (DLamY !(mnb "k" loc)
|
||||
(E $ DApp (dweakE 1 inner) (BV 0 loc) loc) loc)
|
||||
(ty // one q) loc
|
||||
|
||||
-- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ)
|
||||
Nat tyLoc =>
|
||||
whnf defs ctx $ Ann s (Nat tyLoc) loc
|
||||
whnf defs ctx sg $ Ann s (Nat tyLoc) loc
|
||||
|
||||
-- η expand
|
||||
--
|
||||
|
|
@ -185,4 +225,4 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
loc
|
||||
}
|
||||
in
|
||||
whnf defs ctx $ Ann (Box (E inner) loc) (ty // one q) loc
|
||||
whnf defs ctx sg $ Ann (Box (E inner) loc) (ty // one q) loc
|
||||
|
|
|
|||
|
|
@ -14,8 +14,8 @@ export covering
|
|||
computeElimType : CanWhnf Term Interface.isRedexT =>
|
||||
CanWhnf Elim Interface.isRedexE =>
|
||||
{d, n : Nat} ->
|
||||
(defs : Definitions) -> WhnfContext d n ->
|
||||
(e : Elim d n) -> (0 ne : No (isRedexE defs e)) =>
|
||||
(defs : Definitions) -> WhnfContext d n -> (pi : SQty) ->
|
||||
(e : Elim d n) -> (0 ne : No (isRedexE defs pi e)) =>
|
||||
Eff Whnf (Term d n)
|
||||
|
||||
|
||||
|
|
@ -24,11 +24,11 @@ export covering
|
|||
computeWhnfElimType0 : CanWhnf Term Interface.isRedexT =>
|
||||
CanWhnf Elim Interface.isRedexE =>
|
||||
{d, n : Nat} ->
|
||||
(defs : Definitions) -> WhnfContext d n ->
|
||||
(e : Elim d n) -> (0 ne : No (isRedexE defs e)) =>
|
||||
(defs : Definitions) -> WhnfContext d n -> (pi : SQty) ->
|
||||
(e : Elim d n) -> (0 ne : No (isRedexE defs pi e)) =>
|
||||
Eff Whnf (Term d n)
|
||||
|
||||
computeElimType defs ctx e {ne} =
|
||||
computeElimType defs ctx pi e {ne} =
|
||||
case e of
|
||||
F x u loc => do
|
||||
let Just def = lookup x defs
|
||||
|
|
@ -39,13 +39,23 @@ computeElimType defs ctx e {ne} =
|
|||
pure $ ctx.tctx !! i
|
||||
|
||||
App f s loc =>
|
||||
case !(computeWhnfElimType0 defs ctx f {ne = noOr1 ne}) of
|
||||
case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of
|
||||
Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
|
||||
t => throw $ ExpectedPi loc ctx.names t
|
||||
ty => throw $ ExpectedPi loc ctx.names ty
|
||||
|
||||
CasePair {pair, ret, _} =>
|
||||
pure $ sub1 ret pair
|
||||
|
||||
Fst pair loc =>
|
||||
case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of
|
||||
Sig {fst, _} => pure fst
|
||||
ty => throw $ ExpectedSig loc ctx.names ty
|
||||
|
||||
Snd pair loc =>
|
||||
case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of
|
||||
Sig {snd, _} => pure $ sub1 snd $ Fst pair loc
|
||||
ty => throw $ ExpectedSig loc ctx.names ty
|
||||
|
||||
CaseEnum {tag, ret, _} =>
|
||||
pure $ sub1 ret tag
|
||||
|
||||
|
|
@ -56,7 +66,7 @@ computeElimType defs ctx e {ne} =
|
|||
pure $ sub1 ret box
|
||||
|
||||
DApp {fun = f, arg = p, loc} =>
|
||||
case !(computeWhnfElimType0 defs ctx f {ne = noOr1 ne}) of
|
||||
case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of
|
||||
Eq {ty, _} => pure $ dsub1 ty p
|
||||
t => throw $ ExpectedEq loc ctx.names t
|
||||
|
||||
|
|
@ -72,5 +82,5 @@ computeElimType defs ctx e {ne} =
|
|||
TypeCase {ret, _} =>
|
||||
pure ret
|
||||
|
||||
computeWhnfElimType0 defs ctx e =
|
||||
computeElimType defs ctx e >>= whnf0 defs ctx
|
||||
computeWhnfElimType0 defs ctx pi e =
|
||||
computeElimType defs ctx pi e >>= whnf0 defs ctx pi
|
||||
|
|
|
|||
|
|
@ -18,14 +18,14 @@ Whnf = [NameGen, Except Error]
|
|||
|
||||
public export
|
||||
0 RedexTest : TermLike -> Type
|
||||
RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool
|
||||
RedexTest tm = {d, n : Nat} -> Definitions -> SQty -> tm d n -> Bool
|
||||
|
||||
public export
|
||||
interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
|
||||
where
|
||||
whnf : {d, n : Nat} -> (defs : Definitions) ->
|
||||
(ctx : WhnfContext d n) ->
|
||||
tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs))
|
||||
(ctx : WhnfContext d n) -> (q : SQty) ->
|
||||
tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs q))
|
||||
-- having isRedex be part of the class header, and needing to be explicitly
|
||||
-- quantified on every use since idris can't infer its type, is a little ugly.
|
||||
-- but none of the alternatives i've thought of so far work. e.g. in some
|
||||
|
|
@ -33,23 +33,24 @@ where
|
|||
|
||||
public export %inline
|
||||
whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
|
||||
(defs : Definitions) -> WhnfContext d n -> tm d n -> Eff Whnf (tm d n)
|
||||
whnf0 defs ctx t = fst <$> whnf defs ctx t
|
||||
Definitions -> WhnfContext d n -> SQty -> tm d n -> Eff Whnf (tm d n)
|
||||
whnf0 defs ctx q t = fst <$> whnf defs ctx q t
|
||||
|
||||
public export
|
||||
0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
|
||||
Definitions -> Pred (tm d n)
|
||||
IsRedex defs = So . isRedex defs
|
||||
NotRedex defs = No . isRedex defs
|
||||
Definitions -> SQty -> Pred (tm d n)
|
||||
IsRedex defs q = So . isRedex defs q
|
||||
NotRedex defs q = No . isRedex defs q
|
||||
|
||||
public export
|
||||
0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
|
||||
CanWhnf tm isRedex => (d, n : Nat) -> (defs : Definitions) -> Type
|
||||
NonRedex tm d n defs = Subset (tm d n) (NotRedex defs)
|
||||
CanWhnf tm isRedex => (d, n : Nat) ->
|
||||
(defs : Definitions) -> SQty -> Type
|
||||
NonRedex tm d n defs q = Subset (tm d n) (NotRedex defs q)
|
||||
|
||||
public export %inline
|
||||
nred : {0 isRedex : RedexTest tm} -> (0 _ : CanWhnf tm isRedex) =>
|
||||
(t : tm d n) -> (0 nr : NotRedex defs t) => NonRedex tm d n defs
|
||||
(t : tm d n) -> (0 nr : NotRedex defs q t) => NonRedex tm d n defs q
|
||||
nred t = Element t nr
|
||||
|
||||
|
||||
|
|
@ -153,25 +154,25 @@ isK _ = False
|
|||
||| - `ty` has η
|
||||
||| - `val` is a constructor form
|
||||
public export %inline
|
||||
canPushCoe : (ty, val : Term {}) -> Bool
|
||||
canPushCoe (TYPE {}) _ = True
|
||||
canPushCoe (Pi {}) _ = True
|
||||
canPushCoe (Lam {}) _ = False
|
||||
canPushCoe (Sig {}) (Pair {}) = True
|
||||
canPushCoe (Sig {}) _ = False
|
||||
canPushCoe (Pair {}) _ = False
|
||||
canPushCoe (Enum {}) _ = True
|
||||
canPushCoe (Tag {}) _ = False
|
||||
canPushCoe (Eq {}) _ = True
|
||||
canPushCoe (DLam {}) _ = False
|
||||
canPushCoe (Nat {}) _ = True
|
||||
canPushCoe (Zero {}) _ = False
|
||||
canPushCoe (Succ {}) _ = False
|
||||
canPushCoe (BOX {}) _ = True
|
||||
canPushCoe (Box {}) _ = False
|
||||
canPushCoe (E {}) _ = False
|
||||
canPushCoe (CloT {}) _ = False
|
||||
canPushCoe (DCloT {}) _ = False
|
||||
canPushCoe : SQty -> (ty, val : Term {}) -> Bool
|
||||
canPushCoe sg (TYPE {}) _ = True
|
||||
canPushCoe sg (Pi {}) _ = True
|
||||
canPushCoe sg (Lam {}) _ = False
|
||||
canPushCoe sg (Sig {}) (Pair {}) = True
|
||||
canPushCoe sg (Sig {}) _ = False
|
||||
canPushCoe sg (Pair {}) _ = False
|
||||
canPushCoe sg (Enum {}) _ = True
|
||||
canPushCoe sg (Tag {}) _ = False
|
||||
canPushCoe sg (Eq {}) _ = True
|
||||
canPushCoe sg (DLam {}) _ = False
|
||||
canPushCoe sg (Nat {}) _ = True
|
||||
canPushCoe sg (Zero {}) _ = False
|
||||
canPushCoe sg (Succ {}) _ = False
|
||||
canPushCoe sg (BOX {}) _ = True
|
||||
canPushCoe sg (Box {}) _ = False
|
||||
canPushCoe sg (E {}) _ = False
|
||||
canPushCoe sg (CloT {}) _ = False
|
||||
canPushCoe sg (DCloT {}) _ = False
|
||||
|
||||
|
||||
mutual
|
||||
|
|
@ -193,32 +194,36 @@ mutual
|
|||
||| 7. a closure
|
||||
public export
|
||||
isRedexE : RedexTest Elim
|
||||
isRedexE defs (F {x, u, _}) {d, n} =
|
||||
isRedexE defs sg (F {x, u, _}) {d, n} =
|
||||
isJust $ lookupElim x u defs {d, n}
|
||||
isRedexE _ (B {}) = False
|
||||
isRedexE defs (App {fun, _}) =
|
||||
isRedexE defs fun || isLamHead fun
|
||||
isRedexE defs (CasePair {pair, _}) =
|
||||
isRedexE defs pair || isPairHead pair
|
||||
isRedexE defs (CaseEnum {tag, _}) =
|
||||
isRedexE defs tag || isTagHead tag
|
||||
isRedexE defs (CaseNat {nat, _}) =
|
||||
isRedexE defs nat || isNatHead nat
|
||||
isRedexE defs (CaseBox {box, _}) =
|
||||
isRedexE defs box || isBoxHead box
|
||||
isRedexE defs (DApp {fun, arg, _}) =
|
||||
isRedexE defs fun || isDLamHead fun || isK arg
|
||||
isRedexE defs (Ann {tm, ty, _}) =
|
||||
isE tm || isRedexT defs tm || isRedexT defs ty
|
||||
isRedexE defs (Coe {ty = S _ (N _), _}) = True
|
||||
isRedexE defs (Coe {ty = S _ (Y ty), p, q, val, _}) =
|
||||
isRedexT defs ty || canPushCoe ty val || isYes (p `decEqv` q)
|
||||
isRedexE defs (Comp {ty, p, q, r, _}) =
|
||||
isRedexE _ sg (B {}) = False
|
||||
isRedexE defs sg (App {fun, _}) =
|
||||
isRedexE defs sg fun || isLamHead fun
|
||||
isRedexE defs sg (CasePair {pair, _}) =
|
||||
isRedexE defs sg pair || isPairHead pair || isYes (sg `decEq` SZero)
|
||||
isRedexE defs sg (Fst pair _) =
|
||||
isRedexE defs sg pair || isPairHead pair
|
||||
isRedexE defs sg (Snd pair _) =
|
||||
isRedexE defs sg pair || isPairHead pair
|
||||
isRedexE defs sg (CaseEnum {tag, _}) =
|
||||
isRedexE defs sg tag || isTagHead tag
|
||||
isRedexE defs sg (CaseNat {nat, _}) =
|
||||
isRedexE defs sg nat || isNatHead nat
|
||||
isRedexE defs sg (CaseBox {box, _}) =
|
||||
isRedexE defs sg box || isBoxHead box
|
||||
isRedexE defs sg (DApp {fun, arg, _}) =
|
||||
isRedexE defs sg fun || isDLamHead fun || isK arg
|
||||
isRedexE defs sg (Ann {tm, ty, _}) =
|
||||
isE tm || isRedexT defs sg tm || isRedexT defs SZero ty
|
||||
isRedexE defs sg (Coe {ty = S _ (N _), _}) = True
|
||||
isRedexE defs sg (Coe {ty = S _ (Y ty), p, q, val, _}) =
|
||||
isRedexT defs SZero ty || canPushCoe sg ty val || isYes (p `decEqv` q)
|
||||
isRedexE defs sg (Comp {ty, p, q, r, _}) =
|
||||
isYes (p `decEqv` q) || isK r
|
||||
isRedexE defs (TypeCase {ty, ret, _}) =
|
||||
isRedexE defs ty || isRedexT defs ret || isAnnTyCon ty
|
||||
isRedexE _ (CloE {}) = True
|
||||
isRedexE _ (DCloE {}) = True
|
||||
isRedexE defs sg (TypeCase {ty, ret, _}) =
|
||||
isRedexE defs sg ty || isRedexT defs sg ret || isAnnTyCon ty
|
||||
isRedexE _ _ (CloE {}) = True
|
||||
isRedexE _ _ (DCloE {}) = True
|
||||
|
||||
||| a reducible term
|
||||
|||
|
||||
|
|
@ -228,7 +233,7 @@ mutual
|
|||
||| 3. a closure
|
||||
public export
|
||||
isRedexT : RedexTest Term
|
||||
isRedexT _ (CloT {}) = True
|
||||
isRedexT _ (DCloT {}) = True
|
||||
isRedexT defs (E {e, _}) = isAnn e || isRedexE defs e
|
||||
isRedexT _ _ = False
|
||||
isRedexT _ _ (CloT {}) = True
|
||||
isRedexT _ _ (DCloT {}) = True
|
||||
isRedexT defs sg (E {e, _}) = isAnn e || isRedexE defs sg e
|
||||
isRedexT _ _ _ = False
|
||||
|
|
|
|||
|
|
@ -16,53 +16,88 @@ export covering CanWhnf Elim Interface.isRedexE
|
|||
|
||||
covering
|
||||
CanWhnf Elim Interface.isRedexE where
|
||||
whnf defs ctx (F x u loc) with (lookupElim x u defs) proof eq
|
||||
_ | Just y = whnf defs ctx $ setLoc loc y
|
||||
whnf defs ctx sg (F x u loc) with (lookupElim x u defs) proof eq
|
||||
_ | Just y = whnf defs ctx sg $ setLoc loc y
|
||||
_ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
|
||||
|
||||
whnf _ _ (B i loc) = pure $ nred $ B i loc
|
||||
whnf _ _ _ (B i loc) = pure $ nred $ B i loc
|
||||
|
||||
-- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
|
||||
whnf defs ctx (App f s appLoc) = do
|
||||
Element f fnf <- whnf defs ctx f
|
||||
whnf defs ctx sg (App f s appLoc) = do
|
||||
Element f fnf <- whnf defs ctx sg f
|
||||
case nchoose $ isLamHead f of
|
||||
Left _ => case f of
|
||||
Ann (Lam {body, _}) (Pi {arg, res, _}) floc =>
|
||||
let s = Ann s arg s.loc in
|
||||
whnf defs ctx $ Ann (sub1 body s) (sub1 res s) appLoc
|
||||
Coe ty p q val _ => piCoe defs ctx ty p q val s appLoc
|
||||
whnf defs ctx sg $ Ann (sub1 body s) (sub1 res s) appLoc
|
||||
Coe ty p q val _ => piCoe defs ctx sg ty p q val s appLoc
|
||||
Right nlh => pure $ Element (App f s appLoc) $ fnf `orNo` nlh
|
||||
|
||||
-- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝
|
||||
-- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p]
|
||||
whnf defs ctx (CasePair pi pair ret body caseLoc) = do
|
||||
Element pair pairnf <- whnf defs ctx pair
|
||||
--
|
||||
-- 0 · case e return p ⇒ C of { (a, b) ⇒ u } ⇝
|
||||
-- u[fst e/a, snd e/b] ∷ C[e/p]
|
||||
whnf defs ctx sg (CasePair pi pair ret body caseLoc) = do
|
||||
Element pair pairnf <- whnf defs ctx sg pair
|
||||
case nchoose $ isPairHead pair of
|
||||
Left _ => case pair of
|
||||
Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc =>
|
||||
let fst = Ann fst tfst fst.loc
|
||||
snd = Ann snd (sub1 tsnd fst) snd.loc
|
||||
in
|
||||
whnf defs ctx $ Ann (subN body [< fst, snd]) (sub1 ret pair) caseLoc
|
||||
whnf defs ctx sg $ Ann (subN body [< fst, snd]) (sub1 ret pair) caseLoc
|
||||
Coe ty p q val _ => do
|
||||
sigCoe defs ctx pi ty p q val ret body caseLoc
|
||||
sigCoe defs ctx sg pi ty p q val ret body caseLoc
|
||||
Right np =>
|
||||
pure $ Element (CasePair pi pair ret body caseLoc) $ pairnf `orNo` np
|
||||
case sg `decEq` SZero of
|
||||
Yes Refl =>
|
||||
whnf defs ctx SZero $
|
||||
Ann (subN body [< Fst pair caseLoc, Snd pair caseLoc])
|
||||
(sub1 ret pair)
|
||||
caseLoc
|
||||
No n0 =>
|
||||
pure $ Element (CasePair pi pair ret body caseLoc)
|
||||
(pairnf `orNo` np `orNo` notYesNo n0)
|
||||
|
||||
-- fst ((s, t) ∷ (x : A) × B) ⇝ s ∷ A
|
||||
whnf defs ctx sg (Fst pair fstLoc) = do
|
||||
Element pair pairnf <- whnf defs ctx sg pair
|
||||
case nchoose $ isPairHead pair of
|
||||
Left _ => case pair of
|
||||
Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc =>
|
||||
whnf defs ctx sg $ Ann fst tfst pairLoc
|
||||
Coe ty p q val _ => do
|
||||
fstCoe defs ctx sg ty p q val fstLoc
|
||||
Right np =>
|
||||
pure $ Element (Fst pair fstLoc) (pairnf `orNo` np)
|
||||
|
||||
-- snd ((s, t) ∷ (x : A) × B) ⇝ t ∷ B[(s ∷ A)/x]
|
||||
whnf defs ctx sg (Snd pair sndLoc) = do
|
||||
Element pair pairnf <- whnf defs ctx sg pair
|
||||
case nchoose $ isPairHead pair of
|
||||
Left _ => case pair of
|
||||
Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc =>
|
||||
whnf defs ctx sg $ Ann snd (sub1 tsnd (Ann fst tfst fst.loc)) sndLoc
|
||||
Coe ty p q val _ => do
|
||||
sndCoe defs ctx sg ty p q val sndLoc
|
||||
Right np =>
|
||||
pure $ Element (Snd pair sndLoc) (pairnf `orNo` np)
|
||||
|
||||
-- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
|
||||
-- u ∷ C['a∷{a,…}/p]
|
||||
whnf defs ctx (CaseEnum pi tag ret arms caseLoc) = do
|
||||
Element tag tagnf <- whnf defs ctx tag
|
||||
whnf defs ctx sg (CaseEnum pi tag ret arms caseLoc) = do
|
||||
Element tag tagnf <- whnf defs ctx sg tag
|
||||
case nchoose $ isTagHead tag of
|
||||
Left _ => case tag of
|
||||
Ann (Tag t _) (Enum ts _) _ =>
|
||||
let ty = sub1 ret tag in
|
||||
case lookup t arms of
|
||||
Just arm => whnf defs ctx $ Ann arm ty arm.loc
|
||||
Just arm => whnf defs ctx sg $ Ann arm ty arm.loc
|
||||
Nothing => throw $ MissingEnumArm caseLoc t (keys arms)
|
||||
Coe ty p q val _ =>
|
||||
-- there is nowhere an equality can be hiding inside an enum type
|
||||
whnf defs ctx $
|
||||
whnf defs ctx sg $
|
||||
CaseEnum pi (Ann val (dsub1 ty q) val.loc) ret arms caseLoc
|
||||
Right nt =>
|
||||
pure $ Element (CaseEnum pi tag ret arms caseLoc) $ tagnf `orNo` nt
|
||||
|
|
@ -72,37 +107,37 @@ CanWhnf Elim Interface.isRedexE where
|
|||
--
|
||||
-- case succ n ∷ ℕ return p ⇒ C of { succ n', π.ih ⇒ u; … } ⇝
|
||||
-- u[n∷ℕ/n', (case n ∷ ℕ ⋯)/ih] ∷ C[succ n ∷ ℕ/p]
|
||||
whnf defs ctx (CaseNat pi piIH nat ret zer suc caseLoc) = do
|
||||
Element nat natnf <- whnf defs ctx nat
|
||||
whnf defs ctx sg (CaseNat pi piIH nat ret zer suc caseLoc) = do
|
||||
Element nat natnf <- whnf defs ctx sg nat
|
||||
case nchoose $ isNatHead nat of
|
||||
Left _ =>
|
||||
let ty = sub1 ret nat in
|
||||
case nat of
|
||||
Ann (Zero _) (Nat _) _ =>
|
||||
whnf defs ctx $ Ann zer ty zer.loc
|
||||
whnf defs ctx sg $ Ann zer ty zer.loc
|
||||
Ann (Succ n succLoc) (Nat natLoc) _ =>
|
||||
let nn = Ann n (Nat natLoc) succLoc
|
||||
tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc]
|
||||
in
|
||||
whnf defs ctx $ Ann tm ty caseLoc
|
||||
whnf defs ctx sg $ Ann tm ty caseLoc
|
||||
Coe ty p q val _ =>
|
||||
-- same deal as Enum
|
||||
whnf defs ctx $
|
||||
whnf defs ctx sg $
|
||||
CaseNat pi piIH (Ann val (dsub1 ty q) val.loc) ret zer suc caseLoc
|
||||
Right nn => pure $
|
||||
Element (CaseNat pi piIH nat ret zer suc caseLoc) (natnf `orNo` nn)
|
||||
|
||||
-- case [t] ∷ [π.A] return p ⇒ C of { [x] ⇒ u } ⇝
|
||||
-- u[t∷A/x] ∷ C[[t] ∷ [π.A]/p]
|
||||
whnf defs ctx (CaseBox pi box ret body caseLoc) = do
|
||||
Element box boxnf <- whnf defs ctx box
|
||||
whnf defs ctx sg (CaseBox pi box ret body caseLoc) = do
|
||||
Element box boxnf <- whnf defs ctx sg box
|
||||
case nchoose $ isBoxHead box of
|
||||
Left _ => case box of
|
||||
Ann (Box val boxLoc) (BOX q bty tyLoc) _ =>
|
||||
let ty = sub1 ret box in
|
||||
whnf defs ctx $ Ann (sub1 body (Ann val bty val.loc)) ty caseLoc
|
||||
whnf defs ctx sg $ Ann (sub1 body (Ann val bty val.loc)) ty caseLoc
|
||||
Coe ty p q val _ =>
|
||||
boxCoe defs ctx pi ty p q val ret body caseLoc
|
||||
boxCoe defs ctx sg pi ty p q val ret body caseLoc
|
||||
Right nb =>
|
||||
pure $ Element (CaseBox pi box ret body caseLoc) (boxnf `orNo` nb)
|
||||
|
||||
|
|
@ -110,35 +145,35 @@ CanWhnf Elim Interface.isRedexE where
|
|||
-- e : Eq (𝑗 ⇒ A) t u ⊢ e @1 ⇝ u ∷ A‹1/𝑗›
|
||||
--
|
||||
-- ((δ 𝑖 ⇒ s) ∷ Eq (𝑗 ⇒ A) t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
|
||||
whnf defs ctx (DApp f p appLoc) = do
|
||||
Element f fnf <- whnf defs ctx f
|
||||
whnf defs ctx sg (DApp f p appLoc) = do
|
||||
Element f fnf <- whnf defs ctx sg f
|
||||
case nchoose $ isDLamHead f of
|
||||
Left _ => case f of
|
||||
Ann (DLam {body, _}) (Eq {ty, l, r, _}) _ =>
|
||||
whnf defs ctx $
|
||||
whnf defs ctx sg $
|
||||
Ann (endsOr (setLoc appLoc l) (setLoc appLoc r) (dsub1 body p) p)
|
||||
(dsub1 ty p) appLoc
|
||||
Coe ty p' q' val _ =>
|
||||
eqCoe defs ctx ty p' q' val p appLoc
|
||||
eqCoe defs ctx sg ty p' q' val p appLoc
|
||||
Right ndlh => case p of
|
||||
K e _ => do
|
||||
Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx f
|
||||
Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx sg f
|
||||
| ty => throw $ ExpectedEq ty.loc ctx.names ty
|
||||
whnf defs ctx $
|
||||
whnf defs ctx sg $
|
||||
ends (Ann (setLoc appLoc l) ty.zero appLoc)
|
||||
(Ann (setLoc appLoc r) ty.one appLoc) e
|
||||
B {} => pure $ Element (DApp f p appLoc) (fnf `orNo` ndlh `orNo` Ah)
|
||||
|
||||
-- e ∷ A ⇝ e
|
||||
whnf defs ctx (Ann s a annLoc) = do
|
||||
Element s snf <- whnf defs ctx s
|
||||
whnf defs ctx sg (Ann s a annLoc) = do
|
||||
Element s snf <- whnf defs ctx sg s
|
||||
case nchoose $ isE s of
|
||||
Left _ => let E e = s in pure $ Element e $ noOr2 snf
|
||||
Right ne => do
|
||||
Element a anf <- whnf defs ctx a
|
||||
Element a anf <- whnf defs ctx SZero a
|
||||
pure $ Element (Ann s a annLoc) (ne `orNo` snf `orNo` anf)
|
||||
|
||||
whnf defs ctx (Coe sty p q val coeLoc) =
|
||||
whnf defs ctx sg (Coe sty p q val coeLoc) =
|
||||
-- 𝑖 ∉ fv(A)
|
||||
-- -------------------------------
|
||||
-- coe (𝑖 ⇒ A) @p @q s ⇝ s ∷ A
|
||||
|
|
@ -148,63 +183,71 @@ CanWhnf Elim Interface.isRedexE where
|
|||
([< i], Left ty) =>
|
||||
case p `decEqv` q of
|
||||
-- coe (𝑖 ⇒ A) @p @p s ⇝ (s ∷ A‹p/𝑖›)
|
||||
Yes _ => whnf defs ctx $ Ann val (dsub1 sty p) coeLoc
|
||||
Yes _ => whnf defs ctx sg $ Ann val (dsub1 sty p) coeLoc
|
||||
No npq => do
|
||||
Element ty tynf <- whnf defs (extendDim i ctx) ty
|
||||
case nchoose $ canPushCoe ty val of
|
||||
Left pc => pushCoe defs ctx i ty p q val coeLoc
|
||||
Element ty tynf <- whnf defs (extendDim i ctx) SZero ty
|
||||
case nchoose $ canPushCoe sg ty val of
|
||||
Left pc => pushCoe defs ctx sg i ty p q val coeLoc
|
||||
Right npc => pure $ Element (Coe (SY [< i] ty) p q val coeLoc)
|
||||
(tynf `orNo` npc `orNo` notYesNo npq)
|
||||
(_, Right ty) =>
|
||||
whnf defs ctx $ Ann val ty coeLoc
|
||||
whnf defs ctx sg $ Ann val ty coeLoc
|
||||
|
||||
whnf defs ctx (Comp ty p q val r zero one compLoc) =
|
||||
whnf defs ctx sg (Comp ty p q val r zero one compLoc) =
|
||||
case p `decEqv` q of
|
||||
-- comp [A] @p @p s @r { ⋯ } ⇝ s ∷ A
|
||||
Yes y => whnf defs ctx $ Ann val ty compLoc
|
||||
Yes y => whnf defs ctx sg $ Ann val ty compLoc
|
||||
No npq => case r of
|
||||
-- comp [A] @p @q s @0 { 0 𝑗 ⇒ t₀; ⋯ } ⇝ t₀‹q/𝑗› ∷ A
|
||||
K Zero _ => whnf defs ctx $ Ann (dsub1 zero q) ty compLoc
|
||||
K Zero _ => whnf defs ctx sg $ Ann (dsub1 zero q) ty compLoc
|
||||
-- comp [A] @p @q s @1 { 1 𝑗 ⇒ t₁; ⋯ } ⇝ t₁‹q/𝑗› ∷ A
|
||||
K One _ => whnf defs ctx $ Ann (dsub1 one q) ty compLoc
|
||||
K One _ => whnf defs ctx sg $ Ann (dsub1 one q) ty compLoc
|
||||
B {} => pure $ Element (Comp ty p q val r zero one compLoc)
|
||||
(notYesNo npq `orNo` Ah)
|
||||
|
||||
whnf defs ctx (TypeCase ty ret arms def tcLoc) = do
|
||||
Element ty tynf <- whnf defs ctx ty
|
||||
Element ret retnf <- whnf defs ctx ret
|
||||
case nchoose $ isAnnTyCon ty of
|
||||
Left y => let Ann ty (TYPE u _) _ = ty in
|
||||
reduceTypeCase defs ctx ty u ret arms def tcLoc
|
||||
Right nt => pure $ Element (TypeCase ty ret arms def tcLoc)
|
||||
(tynf `orNo` retnf `orNo` nt)
|
||||
whnf defs ctx sg (TypeCase ty ret arms def tcLoc) =
|
||||
case sg `decEq` SZero of
|
||||
Yes Refl => do
|
||||
Element ty tynf <- whnf defs ctx SZero ty
|
||||
Element ret retnf <- whnf defs ctx SZero ret
|
||||
case nchoose $ isAnnTyCon ty of
|
||||
Left y => let Ann ty (TYPE u _) _ = ty in
|
||||
reduceTypeCase defs ctx ty u ret arms def tcLoc
|
||||
Right nt => pure $ Element (TypeCase ty ret arms def tcLoc)
|
||||
(tynf `orNo` retnf `orNo` nt)
|
||||
No _ =>
|
||||
throw $ ClashQ tcLoc sg.qty Zero
|
||||
|
||||
whnf defs ctx (CloE (Sub el th)) = whnf defs ctx $ pushSubstsWith' id th el
|
||||
whnf defs ctx (DCloE (Sub el th)) = whnf defs ctx $ pushSubstsWith' th id el
|
||||
whnf defs ctx sg (CloE (Sub el th)) =
|
||||
whnf defs ctx sg $ pushSubstsWith' id th el
|
||||
whnf defs ctx sg (DCloE (Sub el th)) =
|
||||
whnf defs ctx sg $ pushSubstsWith' th id el
|
||||
|
||||
covering
|
||||
CanWhnf Term Interface.isRedexT where
|
||||
whnf _ _ t@(TYPE {}) = pure $ nred t
|
||||
whnf _ _ t@(Pi {}) = pure $ nred t
|
||||
whnf _ _ t@(Lam {}) = pure $ nred t
|
||||
whnf _ _ t@(Sig {}) = pure $ nred t
|
||||
whnf _ _ t@(Pair {}) = pure $ nred t
|
||||
whnf _ _ t@(Enum {}) = pure $ nred t
|
||||
whnf _ _ t@(Tag {}) = pure $ nred t
|
||||
whnf _ _ t@(Eq {}) = pure $ nred t
|
||||
whnf _ _ t@(DLam {}) = pure $ nred t
|
||||
whnf _ _ t@(Nat {}) = pure $ nred t
|
||||
whnf _ _ t@(Zero {}) = pure $ nred t
|
||||
whnf _ _ t@(Succ {}) = pure $ nred t
|
||||
whnf _ _ t@(BOX {}) = pure $ nred t
|
||||
whnf _ _ t@(Box {}) = pure $ nred t
|
||||
whnf _ _ _ t@(TYPE {}) = pure $ nred t
|
||||
whnf _ _ _ t@(Pi {}) = pure $ nred t
|
||||
whnf _ _ _ t@(Lam {}) = pure $ nred t
|
||||
whnf _ _ _ t@(Sig {}) = pure $ nred t
|
||||
whnf _ _ _ t@(Pair {}) = pure $ nred t
|
||||
whnf _ _ _ t@(Enum {}) = pure $ nred t
|
||||
whnf _ _ _ t@(Tag {}) = pure $ nred t
|
||||
whnf _ _ _ t@(Eq {}) = pure $ nred t
|
||||
whnf _ _ _ t@(DLam {}) = pure $ nred t
|
||||
whnf _ _ _ t@(Nat {}) = pure $ nred t
|
||||
whnf _ _ _ t@(Zero {}) = pure $ nred t
|
||||
whnf _ _ _ t@(Succ {}) = pure $ nred t
|
||||
whnf _ _ _ t@(BOX {}) = pure $ nred t
|
||||
whnf _ _ _ t@(Box {}) = pure $ nred t
|
||||
|
||||
-- s ∷ A ⇝ s (in term context)
|
||||
whnf defs ctx (E e) = do
|
||||
Element e enf <- whnf defs ctx e
|
||||
whnf defs ctx sg (E e) = do
|
||||
Element e enf <- whnf defs ctx sg e
|
||||
case nchoose $ isAnn e of
|
||||
Left _ => let Ann {tm, _} = e in pure $ Element tm $ noOr1 $ noOr2 enf
|
||||
Right na => pure $ Element (E e) $ na `orNo` enf
|
||||
|
||||
whnf defs ctx (CloT (Sub tm th)) = whnf defs ctx $ pushSubstsWith' id th tm
|
||||
whnf defs ctx (DCloT (Sub tm th)) = whnf defs ctx $ pushSubstsWith' th id tm
|
||||
whnf defs ctx sg (CloT (Sub tm th)) =
|
||||
whnf defs ctx sg $ pushSubstsWith' id th tm
|
||||
whnf defs ctx sg (DCloT (Sub tm th)) =
|
||||
whnf defs ctx sg $ pushSubstsWith' th id tm
|
||||
|
|
|
|||
|
|
@ -35,11 +35,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
||| for an elim returns a pair of type-cases that will reduce to that;
|
||||
||| for other intro forms error
|
||||
export covering
|
||||
tycasePi : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
|
||||
tycasePi : (t : Term d n) -> (0 tnf : No (isRedexT defs SZero t)) =>
|
||||
Eff Whnf (Term d n, ScopeTerm d n)
|
||||
tycasePi (Pi {arg, res, _}) = pure (arg, res)
|
||||
tycasePi (E e) {tnf} = do
|
||||
ty <- computeElimType defs ctx e {ne = noOr2 tnf}
|
||||
ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
|
||||
let loc = e.loc
|
||||
narg = mnb "Arg" loc; nret = mnb "Ret" loc
|
||||
arg = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc
|
||||
|
|
@ -53,11 +53,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
||| for an elim returns a pair of type-cases that will reduce to that;
|
||||
||| for other intro forms error
|
||||
export covering
|
||||
tycaseSig : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
|
||||
tycaseSig : (t : Term d n) -> (0 tnf : No (isRedexT defs SZero t)) =>
|
||||
Eff Whnf (Term d n, ScopeTerm d n)
|
||||
tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
|
||||
tycaseSig (E e) {tnf} = do
|
||||
ty <- computeElimType defs ctx e {ne = noOr2 tnf}
|
||||
ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
|
||||
let loc = e.loc
|
||||
nfst = mnb "Fst" loc; nsnd = mnb "Snd" loc
|
||||
fst = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc
|
||||
|
|
@ -71,11 +71,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
||| for an elim returns a type-case that will reduce to that;
|
||||
||| for other intro forms error
|
||||
export covering
|
||||
tycaseBOX : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
|
||||
tycaseBOX : (t : Term d n) -> (0 tnf : No (isRedexT defs SZero t)) =>
|
||||
Eff Whnf (Term d n)
|
||||
tycaseBOX (BOX {ty, _}) = pure ty
|
||||
tycaseBOX (E e) {tnf} = do
|
||||
ty <- computeElimType defs ctx e {ne = noOr2 tnf}
|
||||
ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
|
||||
pure $ E $ typeCase1Y e ty KBOX [< !(mnb "Ty" e.loc)] (BVT 0 e.loc) e.loc
|
||||
tycaseBOX t = throw $ ExpectedBOX t.loc ctx.names t
|
||||
|
||||
|
|
@ -83,11 +83,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
||| for an elim returns five type-cases that will reduce to that;
|
||||
||| for other intro forms error
|
||||
export covering
|
||||
tycaseEq : (t : Term d n) -> (0 tnf : No (isRedexT defs t)) =>
|
||||
tycaseEq : (t : Term d n) -> (0 tnf : No (isRedexT defs SZero t)) =>
|
||||
Eff Whnf (Term d n, Term d n, DScopeTerm d n, Term d n, Term d n)
|
||||
tycaseEq (Eq {ty, l, r, _}) = pure (ty.zero, ty.one, ty, l, r)
|
||||
tycaseEq (E e) {tnf} = do
|
||||
ty <- computeElimType defs ctx e {ne = noOr2 tnf}
|
||||
ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
|
||||
let loc = e.loc
|
||||
names = traverse' (\x => mnb x loc) [< "A0", "A1", "A", "L", "R"]
|
||||
a0 = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc
|
||||
|
|
@ -108,11 +108,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
reduceTypeCase : (ty : Term d n) -> (u : Universe) -> (ret : Term d n) ->
|
||||
(arms : TypeCaseArms d n) -> (def : Term d n) ->
|
||||
(0 _ : So (isTyCon ty)) => Loc ->
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs SZero))
|
||||
reduceTypeCase ty u ret arms def loc = case ty of
|
||||
-- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
|
||||
TYPE {} =>
|
||||
whnf defs ctx $ Ann (tycaseRhsDef0 def KTYPE arms) ret loc
|
||||
whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KTYPE arms) ret loc
|
||||
|
||||
-- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
|
||||
-- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
|
||||
|
|
@ -121,7 +121,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
res' = Ann (Lam res res.loc)
|
||||
(Arr Zero arg (TYPE u noLoc) arg.loc) res.loc
|
||||
in
|
||||
whnf defs ctx $
|
||||
whnf defs ctx SZero $
|
||||
Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc
|
||||
|
||||
-- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
|
||||
|
|
@ -131,12 +131,12 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
snd' = Ann (Lam snd snd.loc)
|
||||
(Arr Zero fst (TYPE u noLoc) fst.loc) snd.loc
|
||||
in
|
||||
whnf defs ctx $
|
||||
whnf defs ctx SZero $
|
||||
Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc
|
||||
|
||||
-- (type-case {⋯} ∷ _ return Q of { {} ⇒ s; ⋯ }) ⇝ s ∷ Q
|
||||
Enum {} =>
|
||||
whnf defs ctx $ Ann (tycaseRhsDef0 def KEnum arms) ret loc
|
||||
whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KEnum arms) ret loc
|
||||
|
||||
-- (type-case Eq [i ⇒ A] L R ∷ ★ᵢ return Q
|
||||
-- of { Eq a₀ a₁ a l r ⇒ s; ⋯ }) ⇝
|
||||
|
|
@ -145,7 +145,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
-- (L ∷ A‹0/i›)/l, (R ∷ A‹1/i›)/r] ∷ Q
|
||||
Eq {ty = a, l, r, loc = eqLoc, _} =>
|
||||
let a0 = a.zero; a1 = a.one in
|
||||
whnf defs ctx $ Ann
|
||||
whnf defs ctx SZero $ Ann
|
||||
(subN (tycaseRhsDef def KEq arms)
|
||||
[< Ann a0 (TYPE u noLoc) a.loc, Ann a1 (TYPE u noLoc) a.loc,
|
||||
Ann (DLam a a.loc) (Eq0 (TYPE u noLoc) a0 a1 a.loc) a.loc,
|
||||
|
|
@ -154,10 +154,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
|
||||
-- (type-case ℕ ∷ _ return Q of { ℕ ⇒ s; ⋯ }) ⇝ s ∷ Q
|
||||
Nat {} =>
|
||||
whnf defs ctx $ Ann (tycaseRhsDef0 def KNat arms) ret loc
|
||||
whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KNat arms) ret loc
|
||||
|
||||
-- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
|
||||
BOX {ty = a, loc = boxLoc, _} =>
|
||||
whnf defs ctx $ Ann
|
||||
whnf defs ctx SZero $ Ann
|
||||
(sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u noLoc) a.loc))
|
||||
ret loc
|
||||
|
|
|
|||
|
|
@ -9,12 +9,12 @@ depends = base, contrib, elab-util, sop, snocvect, eff, prettier
|
|||
|
||||
modules =
|
||||
Text.PrettyPrint.Bernardy.Core.Decorate,
|
||||
Control.Monad.ST.Extra,
|
||||
Quox.BoolExtra,
|
||||
Quox.CharExtra,
|
||||
Quox.NatExtra,
|
||||
Quox.EffExtra,
|
||||
Quox.Decidable,
|
||||
Quox.ST,
|
||||
Quox.No,
|
||||
Quox.Loc,
|
||||
Quox.OPE,
|
||||
|
|
|
|||
|
|
@ -12,15 +12,15 @@ import AstExtra
|
|||
|
||||
defGlobals : Definitions
|
||||
defGlobals = fromList
|
||||
[("A", ^mkPostulate gzero (^TYPE 0)),
|
||||
("B", ^mkPostulate gzero (^TYPE 0)),
|
||||
("a", ^mkPostulate gany (^FT "A" 0)),
|
||||
("a'", ^mkPostulate gany (^FT "A" 0)),
|
||||
("b", ^mkPostulate gany (^FT "B" 0)),
|
||||
("f", ^mkPostulate gany (^Arr One (^FT "A" 0) (^FT "A" 0))),
|
||||
("id", ^mkDef gany (^Arr One (^FT "A" 0) (^FT "A" 0)) (^LamY "x" (^BVT 0))),
|
||||
("eq-AB", ^mkPostulate gzero (^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0))),
|
||||
("two", ^mkDef gany (^Nat) (^Succ (^Succ (^Zero))))]
|
||||
[("A", ^mkPostulate GZero (^TYPE 0)),
|
||||
("B", ^mkPostulate GZero (^TYPE 0)),
|
||||
("a", ^mkPostulate GAny (^FT "A" 0)),
|
||||
("a'", ^mkPostulate GAny (^FT "A" 0)),
|
||||
("b", ^mkPostulate GAny (^FT "B" 0)),
|
||||
("f", ^mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "A" 0))),
|
||||
("id", ^mkDef GAny (^Arr One (^FT "A" 0) (^FT "A" 0)) (^LamY "x" (^BVT 0))),
|
||||
("eq-AB", ^mkPostulate GZero (^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0))),
|
||||
("two", ^mkDef GAny (^Nat) (^Succ (^Succ (^Zero))))]
|
||||
|
||||
parameters (label : String) (act : Eff Equal ())
|
||||
{default defGlobals globals : Definitions}
|
||||
|
|
@ -32,15 +32,17 @@ parameters (label : String) (act : Eff Equal ())
|
|||
|
||||
|
||||
parameters (ctx : TyContext d n)
|
||||
subT, equalT : Term d n -> Term d n -> Term d n -> Eff TC ()
|
||||
subT ty s t = lift $ Term.sub noLoc ctx ty s t
|
||||
equalT ty s t = lift $ Term.equal noLoc ctx ty s t
|
||||
subT, equalT : {default SOne sg : SQty} ->
|
||||
Term d n -> Term d n -> Term d n -> Eff TC ()
|
||||
subT ty s t {sg} = lift $ Term.sub noLoc ctx sg ty s t
|
||||
equalT ty s t {sg} = lift $ Term.equal noLoc ctx sg ty s t
|
||||
equalTy : Term d n -> Term d n -> Eff TC ()
|
||||
equalTy s t = lift $ Term.equalType noLoc ctx s t
|
||||
|
||||
subE, equalE : Elim d n -> Elim d n -> Eff TC ()
|
||||
subE e f = lift $ Elim.sub noLoc ctx e f
|
||||
equalE e f = lift $ Elim.equal noLoc ctx e f
|
||||
subE, equalE : {default SOne sg : SQty} ->
|
||||
Elim d n -> Elim d n -> Eff TC ()
|
||||
subE e f {sg} = lift $ Elim.sub noLoc ctx sg e f
|
||||
equalE e f {sg} = lift $ Elim.equal noLoc ctx sg e f
|
||||
|
||||
|
||||
export
|
||||
|
|
@ -154,7 +156,7 @@ tests = "equality & subtyping" :- [
|
|||
let tm = ^Eq0 (^TYPE 1) (^TYPE 0) (^TYPE 0) in
|
||||
equalT empty (^TYPE 2) tm tm,
|
||||
testEq "A ≔ ★₁ ⊢ (★₀ ≡ ★₀ : ★₁) = (★₀ ≡ ★₀ : A)"
|
||||
{globals = fromList [("A", ^mkDef gzero (^TYPE 2) (^TYPE 1))]} $
|
||||
{globals = fromList [("A", ^mkDef GZero (^TYPE 2) (^TYPE 1))]} $
|
||||
equalT empty (^TYPE 2)
|
||||
(^Eq0 (^TYPE 1) (^TYPE 0) (^TYPE 0))
|
||||
(^Eq0 (^FT "A" 0) (^TYPE 0) (^TYPE 0)),
|
||||
|
|
@ -174,7 +176,7 @@ tests = "equality & subtyping" :- [
|
|||
|
||||
testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ∥ ⊢ p = q (free)"
|
||||
{globals =
|
||||
let def = ^mkPostulate gzero
|
||||
let def = ^mkPostulate GZero
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))
|
||||
in defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $
|
||||
equalE empty (^F "p" 0) (^F "q" 0),
|
||||
|
|
@ -193,32 +195,32 @@ tests = "equality & subtyping" :- [
|
|||
|
||||
testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : EE ⊢ x = y"
|
||||
{globals = defGlobals `mergeLeft` fromList
|
||||
[("E", ^mkDef gzero (^TYPE 0)
|
||||
[("E", ^mkDef GZero (^TYPE 0)
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
|
||||
("EE", ^mkDef gzero (^TYPE 0) (^FT "E" 0))]} $
|
||||
("EE", ^mkDef GZero (^TYPE 0) (^FT "E" 0))]} $
|
||||
equalE
|
||||
(extendTyN [< (Any, "x", ^FT "EE" 0), (Any, "y", ^FT "EE" 0)] empty)
|
||||
(^BV 0) (^BV 1),
|
||||
|
||||
testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : E ⊢ x = y"
|
||||
{globals = defGlobals `mergeLeft` fromList
|
||||
[("E", ^mkDef gzero (^TYPE 0)
|
||||
[("E", ^mkDef GZero (^TYPE 0)
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
|
||||
("EE", ^mkDef gzero (^TYPE 0) (^FT "E" 0))]} $
|
||||
("EE", ^mkDef GZero (^TYPE 0) (^FT "E" 0))]} $
|
||||
equalE
|
||||
(extendTyN [< (Any, "x", ^FT "EE" 0), (Any, "y", ^FT "E" 0)] empty)
|
||||
(^BV 0) (^BV 1),
|
||||
|
||||
testEq "E ≔ a ≡ a' : A ∥ x : E, y : E ⊢ x = y"
|
||||
{globals = defGlobals `mergeLeft` fromList
|
||||
[("E", ^mkDef gzero (^TYPE 0)
|
||||
[("E", ^mkDef GZero (^TYPE 0)
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)))]} $
|
||||
equalE (extendTyN [< (Any, "x", ^FT "E" 0), (Any, "y", ^FT "E" 0)] empty)
|
||||
(^BV 0) (^BV 1),
|
||||
|
||||
testEq "E ≔ a ≡ a' : A ∥ x : (E×E), y : (E×E) ⊢ x = y"
|
||||
{globals = defGlobals `mergeLeft` fromList
|
||||
[("E", ^mkDef gzero (^TYPE 0)
|
||||
[("E", ^mkDef GZero (^TYPE 0)
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)))]} $
|
||||
let ty : forall n. Term 0 n := ^Sig (^FT "E" 0) (SN $ ^FT "E" 0) in
|
||||
equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
|
||||
|
|
@ -226,9 +228,9 @@ tests = "equality & subtyping" :- [
|
|||
|
||||
testEq "E ≔ a ≡ a' : A, W ≔ E × E ∥ x : W, y : E×E ⊢ x = y"
|
||||
{globals = defGlobals `mergeLeft` fromList
|
||||
[("E", ^mkDef gzero (^TYPE 0)
|
||||
[("E", ^mkDef GZero (^TYPE 0)
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
|
||||
("W", ^mkDef gzero (^TYPE 0) (^And (^FT "E" 0) (^FT "E" 0)))]} $
|
||||
("W", ^mkDef GZero (^TYPE 0) (^And (^FT "E" 0) (^FT "E" 0)))]} $
|
||||
equalE
|
||||
(extendTyN [< (Any, "x", ^FT "W" 0),
|
||||
(Any, "y", ^And (^FT "E" 0) (^FT "E" 0))] empty)
|
||||
|
|
@ -278,11 +280,11 @@ tests = "equality & subtyping" :- [
|
|||
|
||||
"free var" :-
|
||||
let au_bu = fromList
|
||||
[("A", ^mkDef gany (^TYPE 1) (^TYPE 0)),
|
||||
("B", ^mkDef gany (^TYPE 1) (^TYPE 0))]
|
||||
[("A", ^mkDef GAny (^TYPE 1) (^TYPE 0)),
|
||||
("B", ^mkDef GAny (^TYPE 1) (^TYPE 0))]
|
||||
au_ba = fromList
|
||||
[("A", ^mkDef gany (^TYPE 1) (^TYPE 0)),
|
||||
("B", ^mkDef gany (^TYPE 1) (^FT "A" 0))]
|
||||
[("A", ^mkDef GAny (^TYPE 1) (^TYPE 0)),
|
||||
("B", ^mkDef GAny (^TYPE 1) (^FT "A" 0))]
|
||||
in [
|
||||
testEq "A = A" $
|
||||
equalE empty (^F "A" 0) (^F "A" 0),
|
||||
|
|
@ -303,13 +305,13 @@ tests = "equality & subtyping" :- [
|
|||
testNeq "A ≮: B" $
|
||||
subE empty (^F "A" 0) (^F "B" 0),
|
||||
testEq "A : ★₃ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
|
||||
{globals = fromList [("A", ^mkDef gany (^TYPE 3) (^TYPE 0)),
|
||||
("B", ^mkDef gany (^TYPE 3) (^TYPE 2))]} $
|
||||
{globals = fromList [("A", ^mkDef GAny (^TYPE 3) (^TYPE 0)),
|
||||
("B", ^mkDef GAny (^TYPE 3) (^TYPE 2))]} $
|
||||
subE empty (^F "A" 0) (^F "B" 0),
|
||||
note "(A and B in different universes)",
|
||||
testEq "A : ★₁ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
|
||||
{globals = fromList [("A", ^mkDef gany (^TYPE 1) (^TYPE 0)),
|
||||
("B", ^mkDef gany (^TYPE 3) (^TYPE 2))]} $
|
||||
{globals = fromList [("A", ^mkDef GAny (^TYPE 1) (^TYPE 0)),
|
||||
("B", ^mkDef GAny (^TYPE 3) (^TYPE 2))]} $
|
||||
subE empty (^F "A" 0) (^F "B" 0),
|
||||
testEq "0=1 ⊢ A <: B" $
|
||||
subE empty01 (^F "A" 0) (^F "B" 0)
|
||||
|
|
|
|||
|
|
@ -38,17 +38,21 @@ testFreeVars lbl tm dims terms =
|
|||
Right ()
|
||||
|
||||
private
|
||||
prettyWith : (a -> Eff Pretty (Doc (Opts 80))) -> a -> String
|
||||
Doc80 : Type
|
||||
Doc80 = Doc $ Opts 80
|
||||
|
||||
private
|
||||
prettyWith : (a -> Eff Pretty Doc80) -> a -> String
|
||||
prettyWith f = trim . render _ . runPretty . f
|
||||
|
||||
parameters {d, n : Nat} (ds : BContext d) (ts : BContext n)
|
||||
private
|
||||
withContext : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
|
||||
withContext {opts} doc =
|
||||
withContext : Doc80 -> Eff Pretty Doc80
|
||||
withContext doc =
|
||||
if null ds && null ts then pure $ hsep ["⊢", doc]
|
||||
else pure $ sep [hsep [!(ctx1 ds), "|", !(ctx1 ts), "⊢"], doc]
|
||||
where
|
||||
ctx1 : forall k. BContext k -> Eff Pretty (Doc opts)
|
||||
ctx1 : forall k. BContext k -> Eff Pretty Doc80
|
||||
ctx1 [<] = pure "·"
|
||||
ctx1 ctx = fillSeparateTight !commaD . toList' <$>
|
||||
traverse' (pure . prettyBind') ctx
|
||||
|
|
|
|||
|
|
@ -85,7 +85,7 @@ tests = "PTerm → Term" :- [
|
|||
],
|
||||
|
||||
"terms" :-
|
||||
let defs = fromList [("f", mkDef gany (Nat noLoc) (Zero noLoc) noLoc)]
|
||||
let defs = fromList [("f", mkDef GAny (Nat noLoc) (Zero noLoc) noLoc)]
|
||||
-- doesn't have to be well typed yet, just well scoped
|
||||
fromPTerm = runFromParser {defs} .
|
||||
fromPTermWith [< "𝑖", "𝑗"] [< "A", "x", "y", "z"]
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@ module Tests.Reduce
|
|||
|
||||
import Quox.Syntax as Lib
|
||||
import Quox.Equal
|
||||
import Quox.ST
|
||||
import Control.Monad.ST.Extra
|
||||
import TypingImpls
|
||||
import AstExtra
|
||||
import TAP
|
||||
|
|
@ -14,15 +14,17 @@ import Control.Eff
|
|||
|
||||
runWhnf : Eff Whnf a -> Either Error a
|
||||
runWhnf act = runSTErr $ do
|
||||
runEff act [handleStateSTRef !(newRef 0), handleExcept (\e => stLeft e)]
|
||||
runEff act [handleStateSTRef !(liftST $ newSTRef 0),
|
||||
handleExcept (\e => stLeft e)]
|
||||
|
||||
parameters {0 isRedex : RedexTest tm} {auto _ : CanWhnf tm isRedex} {d, n : Nat}
|
||||
{auto _ : (Eq (tm d n), Show (tm d n))}
|
||||
{default empty defs : Definitions}
|
||||
{default SOne sg : SQty}
|
||||
private
|
||||
testWhnf : String -> WhnfContext d n -> tm d n -> tm d n -> Test
|
||||
testWhnf label ctx from to = test "\{label} (whnf)" $ do
|
||||
result <- mapFst toInfo $ runWhnf $ whnf0 defs ctx from
|
||||
result <- mapFst toInfo $ runWhnf $ whnf0 defs ctx sg from
|
||||
unless (result == to) $ Left [("exp", show to), ("got", show result)]
|
||||
|
||||
private
|
||||
|
|
@ -71,10 +73,10 @@ tests = "whnf" :- [
|
|||
|
||||
"definitions" :- [
|
||||
testWhnf "a (transparent)" empty
|
||||
{defs = fromList [("a", ^mkDef gzero (^TYPE 1) (^TYPE 0))]}
|
||||
{defs = fromList [("a", ^mkDef GZero (^TYPE 1) (^TYPE 0))]}
|
||||
(^F "a" 0) (^Ann (^TYPE 0) (^TYPE 1)),
|
||||
testNoStep "a (opaque)" empty
|
||||
{defs = fromList [("a", ^mkPostulate gzero (^TYPE 1))]}
|
||||
{defs = fromList [("a", ^mkPostulate GZero (^TYPE 1))]}
|
||||
(^F "a" 0)
|
||||
],
|
||||
|
||||
|
|
|
|||
|
|
@ -87,28 +87,28 @@ apps = foldl (\f, s => ^App f s)
|
|||
|
||||
defGlobals : Definitions
|
||||
defGlobals = fromList
|
||||
[("A", ^mkPostulate gzero (^TYPE 0)),
|
||||
("B", ^mkPostulate gzero (^TYPE 0)),
|
||||
("C", ^mkPostulate gzero (^TYPE 1)),
|
||||
("D", ^mkPostulate gzero (^TYPE 1)),
|
||||
("P", ^mkPostulate gzero (^Arr Any (^FT "A" 0) (^TYPE 0))),
|
||||
("a", ^mkPostulate gany (^FT "A" 0)),
|
||||
("a'", ^mkPostulate gany (^FT "A" 0)),
|
||||
("b", ^mkPostulate gany (^FT "B" 0)),
|
||||
("c", ^mkPostulate gany (^FT "C" 0)),
|
||||
("d", ^mkPostulate gany (^FT "D" 0)),
|
||||
("f", ^mkPostulate gany (^Arr One (^FT "A" 0) (^FT "A" 0))),
|
||||
("fω", ^mkPostulate gany (^Arr Any (^FT "A" 0) (^FT "A" 0))),
|
||||
("g", ^mkPostulate gany (^Arr One (^FT "A" 0) (^FT "B" 0))),
|
||||
("f2", ^mkPostulate gany
|
||||
[("A", ^mkPostulate GZero (^TYPE 0)),
|
||||
("B", ^mkPostulate GZero (^TYPE 0)),
|
||||
("C", ^mkPostulate GZero (^TYPE 1)),
|
||||
("D", ^mkPostulate GZero (^TYPE 1)),
|
||||
("P", ^mkPostulate GZero (^Arr Any (^FT "A" 0) (^TYPE 0))),
|
||||
("a", ^mkPostulate GAny (^FT "A" 0)),
|
||||
("a'", ^mkPostulate GAny (^FT "A" 0)),
|
||||
("b", ^mkPostulate GAny (^FT "B" 0)),
|
||||
("c", ^mkPostulate GAny (^FT "C" 0)),
|
||||
("d", ^mkPostulate GAny (^FT "D" 0)),
|
||||
("f", ^mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "A" 0))),
|
||||
("fω", ^mkPostulate GAny (^Arr Any (^FT "A" 0) (^FT "A" 0))),
|
||||
("g", ^mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "B" 0))),
|
||||
("f2", ^mkPostulate GAny
|
||||
(^Arr One (^FT "A" 0) (^Arr One (^FT "A" 0) (^FT "B" 0)))),
|
||||
("p", ^mkPostulate gany
|
||||
("p", ^mkPostulate GAny
|
||||
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))),
|
||||
("q", ^mkPostulate gany
|
||||
("q", ^mkPostulate GAny
|
||||
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))),
|
||||
("refl", ^mkDef gany reflTy reflDef),
|
||||
("fst", ^mkDef gany fstTy fstDef),
|
||||
("snd", ^mkDef gany sndTy sndDef)]
|
||||
("refl", ^mkDef GAny reflTy reflDef),
|
||||
("fst", ^mkDef GAny fstTy fstDef),
|
||||
("snd", ^mkDef GAny sndTy sndDef)]
|
||||
|
||||
parameters (label : String) (act : Lazy (Eff Test ()))
|
||||
{default defGlobals globals : Definitions}
|
||||
|
|
@ -168,7 +168,7 @@ tests = "typechecker" :- [
|
|||
testTC "0 · ★₀ ⇐ ★₁ # by checkType" $
|
||||
checkType_ empty (^TYPE 0) (Just 1),
|
||||
testTC "0 · ★₀ ⇐ ★₁ # by check" $
|
||||
check_ empty szero (^TYPE 0) (^TYPE 1),
|
||||
check_ empty SZero (^TYPE 0) (^TYPE 1),
|
||||
testTC "0 · ★₀ ⇐ ★₂" $
|
||||
checkType_ empty (^TYPE 0) (Just 2),
|
||||
testTC "0 · ★₀ ⇐ ★_" $
|
||||
|
|
@ -180,241 +180,241 @@ tests = "typechecker" :- [
|
|||
testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $
|
||||
checkType_ empty01 (^TYPE 1) (Just 0),
|
||||
testTCFail "1 · ★₀ ⇍ ★₁ # by check" $
|
||||
check_ empty sone (^TYPE 0) (^TYPE 1)
|
||||
check_ empty SOne (^TYPE 0) (^TYPE 1)
|
||||
],
|
||||
|
||||
"function types" :- [
|
||||
note "A, B : ★₀; C, D : ★₁; P : 0.A → ★₀",
|
||||
testTC "0 · 1.A → B ⇐ ★₀" $
|
||||
check_ empty szero (^Arr One (^FT "A" 0) (^FT "B" 0)) (^TYPE 0),
|
||||
check_ empty SZero (^Arr One (^FT "A" 0) (^FT "B" 0)) (^TYPE 0),
|
||||
note "subtyping",
|
||||
testTC "0 · 1.A → B ⇐ ★₁" $
|
||||
check_ empty szero (^Arr One (^FT "A" 0) (^FT "B" 0)) (^TYPE 1),
|
||||
check_ empty SZero (^Arr One (^FT "A" 0) (^FT "B" 0)) (^TYPE 1),
|
||||
testTC "0 · 1.C → D ⇐ ★₁" $
|
||||
check_ empty szero (^Arr One (^FT "C" 0) (^FT "D" 0)) (^TYPE 1),
|
||||
check_ empty SZero (^Arr One (^FT "C" 0) (^FT "D" 0)) (^TYPE 1),
|
||||
testTCFail "0 · 1.C → D ⇍ ★₀" $
|
||||
check_ empty szero (^Arr One (^FT "C" 0) (^FT "D" 0)) (^TYPE 0),
|
||||
check_ empty SZero (^Arr One (^FT "C" 0) (^FT "D" 0)) (^TYPE 0),
|
||||
testTC "0 · 1.(x : A) → P x ⇐ ★₀" $
|
||||
check_ empty szero
|
||||
check_ empty SZero
|
||||
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
|
||||
(^TYPE 0),
|
||||
testTCFail "0 · 1.A → P ⇍ ★₀" $
|
||||
check_ empty szero (^Arr One (^FT "A" 0) (^FT "P" 0)) (^TYPE 0),
|
||||
check_ empty SZero (^Arr One (^FT "A" 0) (^FT "P" 0)) (^TYPE 0),
|
||||
testTC "0=1 ⊢ 0 · 1.A → P ⇐ ★₀" $
|
||||
check_ empty01 szero (^Arr One (^FT "A" 0) (^FT "P" 0)) (^TYPE 0)
|
||||
check_ empty01 SZero (^Arr One (^FT "A" 0) (^FT "P" 0)) (^TYPE 0)
|
||||
],
|
||||
|
||||
"pair types" :- [
|
||||
testTC "0 · A × A ⇐ ★₀" $
|
||||
check_ empty szero (^And (^FT "A" 0) (^FT "A" 0)) (^TYPE 0),
|
||||
check_ empty SZero (^And (^FT "A" 0) (^FT "A" 0)) (^TYPE 0),
|
||||
testTCFail "0 · A × P ⇍ ★₀" $
|
||||
check_ empty szero (^And (^FT "A" 0) (^FT "P" 0)) (^TYPE 0),
|
||||
check_ empty SZero (^And (^FT "A" 0) (^FT "P" 0)) (^TYPE 0),
|
||||
testTC "0 · (x : A) × P x ⇐ ★₀" $
|
||||
check_ empty szero
|
||||
check_ empty SZero
|
||||
(^SigY "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
|
||||
(^TYPE 0),
|
||||
testTC "0 · (x : A) × P x ⇐ ★₁" $
|
||||
check_ empty szero
|
||||
check_ empty SZero
|
||||
(^SigY "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
|
||||
(^TYPE 1),
|
||||
testTC "0 · (A : ★₀) × A ⇐ ★₁" $
|
||||
check_ empty szero
|
||||
check_ empty SZero
|
||||
(^SigY "A" (^TYPE 0) (^BVT 0))
|
||||
(^TYPE 1),
|
||||
testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $
|
||||
check_ empty szero
|
||||
check_ empty SZero
|
||||
(^SigY "A" (^TYPE 0) (^BVT 0))
|
||||
(^TYPE 0),
|
||||
testTCFail "1 · A × A ⇍ ★₀" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^And (^FT "A" 0) (^FT "A" 0))
|
||||
(^TYPE 0)
|
||||
],
|
||||
|
||||
"enum types" :- [
|
||||
testTC "0 · {} ⇐ ★₀" $ check_ empty szero (^enum []) (^TYPE 0),
|
||||
testTC "0 · {} ⇐ ★₃" $ check_ empty szero (^enum []) (^TYPE 3),
|
||||
testTC "0 · {} ⇐ ★₀" $ check_ empty SZero (^enum []) (^TYPE 0),
|
||||
testTC "0 · {} ⇐ ★₃" $ check_ empty SZero (^enum []) (^TYPE 3),
|
||||
testTC "0 · {a,b,c} ⇐ ★₀" $
|
||||
check_ empty szero (^enum ["a", "b", "c"]) (^TYPE 0),
|
||||
check_ empty SZero (^enum ["a", "b", "c"]) (^TYPE 0),
|
||||
testTC "0 · {a,b,c} ⇐ ★₃" $
|
||||
check_ empty szero (^enum ["a", "b", "c"]) (^TYPE 3),
|
||||
testTCFail "1 · {} ⇍ ★₀" $ check_ empty sone (^enum []) (^TYPE 0),
|
||||
testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ empty01 sone (^enum []) (^TYPE 0)
|
||||
check_ empty SZero (^enum ["a", "b", "c"]) (^TYPE 3),
|
||||
testTCFail "1 · {} ⇍ ★₀" $ check_ empty SOne (^enum []) (^TYPE 0),
|
||||
testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ empty01 SOne (^enum []) (^TYPE 0)
|
||||
],
|
||||
|
||||
"free vars" :- [
|
||||
note "A : ★₀",
|
||||
testTC "0 · A ⇒ ★₀" $
|
||||
inferAs empty szero (^F "A" 0) (^TYPE 0),
|
||||
inferAs empty SZero (^F "A" 0) (^TYPE 0),
|
||||
testTC "0 · [A] ⇐ ★₀" $
|
||||
check_ empty szero (^FT "A" 0) (^TYPE 0),
|
||||
check_ empty SZero (^FT "A" 0) (^TYPE 0),
|
||||
note "subtyping",
|
||||
testTC "0 · [A] ⇐ ★₁" $
|
||||
check_ empty szero (^FT "A" 0) (^TYPE 1),
|
||||
check_ empty SZero (^FT "A" 0) (^TYPE 1),
|
||||
note "(fail) runtime-relevant type",
|
||||
testTCFail "1 · A ⇏ ★₀" $
|
||||
infer_ empty sone (^F "A" 0),
|
||||
infer_ empty SOne (^F "A" 0),
|
||||
testTC "1 . f ⇒ 1.A → A" $
|
||||
inferAs empty sone (^F "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)),
|
||||
inferAs empty SOne (^F "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 . f ⇐ 1.A → A" $
|
||||
check_ empty sone (^FT "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)),
|
||||
check_ empty SOne (^FT "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)),
|
||||
testTCFail "1 . f ⇍ 0.A → A" $
|
||||
check_ empty sone (^FT "f" 0) (^Arr Zero (^FT "A" 0) (^FT "A" 0)),
|
||||
check_ empty SOne (^FT "f" 0) (^Arr Zero (^FT "A" 0) (^FT "A" 0)),
|
||||
testTCFail "1 . f ⇍ ω.A → A" $
|
||||
check_ empty sone (^FT "f" 0) (^Arr Any (^FT "A" 0) (^FT "A" 0)),
|
||||
check_ empty SOne (^FT "f" 0) (^Arr Any (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 . (λ x ⇒ f x) ⇐ 1.A → A" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
|
||||
(^Arr One (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 . (λ x ⇒ f x) ⇐ ω.A → A" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
|
||||
(^Arr Any (^FT "A" 0) (^FT "A" 0)),
|
||||
testTCFail "1 . (λ x ⇒ f x) ⇍ 0.A → A" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
|
||||
(^Arr Zero (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 . fω ⇒ ω.A → A" $
|
||||
inferAs empty sone (^F "fω" 0) (^Arr Any (^FT "A" 0) (^FT "A" 0)),
|
||||
inferAs empty SOne (^F "fω" 0) (^Arr Any (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 . (λ x ⇒ fω x) ⇐ ω.A → A" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^LamY "x" (E $ ^App (^F "fω" 0) (^BVT 0)))
|
||||
(^Arr Any (^FT "A" 0) (^FT "A" 0)),
|
||||
testTCFail "1 . (λ x ⇒ fω x) ⇍ 0.A → A" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^LamY "x" (E $ ^App (^F "fω" 0) (^BVT 0)))
|
||||
(^Arr Zero (^FT "A" 0) (^FT "A" 0)),
|
||||
testTCFail "1 . (λ x ⇒ fω x) ⇍ 1.A → A" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^LamY "x" (E $ ^App (^F "fω" 0) (^BVT 0)))
|
||||
(^Arr One (^FT "A" 0) (^FT "A" 0)),
|
||||
note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ δ _ ⇒ x)",
|
||||
testTC "1 · refl ⇒ ⋯" $ inferAs empty sone (^F "refl" 0) reflTy,
|
||||
testTC "1 · [refl] ⇐ ⋯" $ check_ empty sone (^FT "refl" 0) reflTy
|
||||
testTC "1 · refl ⇒ ⋯" $ inferAs empty SOne (^F "refl" 0) reflTy,
|
||||
testTC "1 · [refl] ⇐ ⋯" $ check_ empty SOne (^FT "refl" 0) reflTy
|
||||
],
|
||||
|
||||
"bound vars" :- [
|
||||
testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
|
||||
inferAsQ (ctx [< ("x", ^FT "A" 0)]) sone
|
||||
inferAsQ (ctx [< ("x", ^FT "A" 0)]) SOne
|
||||
(^BV 0) (^FT "A" 0) [< One],
|
||||
testTC "x : A ⊢ 1 · x ⇐ A ⊳ 1·x" $
|
||||
checkQ (ctx [< ("x", ^FT "A" 0)]) sone (^BVT 0) (^FT "A" 0) [< One],
|
||||
checkQ (ctx [< ("x", ^FT "A" 0)]) SOne (^BVT 0) (^FT "A" 0) [< One],
|
||||
note "f2 : 1.A → 1.A → B",
|
||||
testTC "x : A ⊢ 1 · f2 x x ⇒ B ⊳ ω·x" $
|
||||
inferAsQ (ctx [< ("x", ^FT "A" 0)]) sone
|
||||
inferAsQ (ctx [< ("x", ^FT "A" 0)]) SOne
|
||||
(^App (^App (^F "f2" 0) (^BVT 0)) (^BVT 0)) (^FT "B" 0) [< Any]
|
||||
],
|
||||
|
||||
"lambda" :- [
|
||||
note "linear & unrestricted identity",
|
||||
testTC "1 · (λ x ⇒ x) ⇐ A → A" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^LamY "x" (^BVT 0))
|
||||
(^Arr One (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 · (λ x ⇒ x) ⇐ ω.A → A" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^LamY "x" (^BVT 0))
|
||||
(^Arr Any (^FT "A" 0) (^FT "A" 0)),
|
||||
note "(fail) zero binding used relevantly",
|
||||
testTCFail "1 · (λ x ⇒ x) ⇍ 0.A → A" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^LamY "x" (^BVT 0))
|
||||
(^Arr Zero (^FT "A" 0) (^FT "A" 0)),
|
||||
note "(but ok in overall erased context)",
|
||||
testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $
|
||||
check_ empty szero
|
||||
check_ empty SZero
|
||||
(^LamY "x" (^BVT 0))
|
||||
(^Arr Zero (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯ # (type of refl)" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^LamY "A" (^LamY "x"
|
||||
(E $ ^App (^App (^F "refl" 0) (^BVT 1)) (^BVT 0))))
|
||||
reflTy,
|
||||
testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $
|
||||
check_ empty sone reflDef reflTy
|
||||
check_ empty SOne reflDef reflTy
|
||||
],
|
||||
|
||||
"pairs" :- [
|
||||
testTC "1 · (a, a) ⇐ A × A" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^Pair (^FT "a" 0) (^FT "a" 0)) (^And (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $
|
||||
checkQ (ctx [< ("x", ^FT "A" 0)]) sone
|
||||
checkQ (ctx [< ("x", ^FT "A" 0)]) SOne
|
||||
(^Pair (^BVT 0) (^BVT 0)) (^And (^FT "A" 0) (^FT "A" 0)) [< Any],
|
||||
testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^Pair (^FT "a" 0) (^DLamN (^FT "a" 0)))
|
||||
(^SigY "x" (^FT "A" 0) (^Eq0 (^FT "A" 0) (^BVT 0) (^FT "a" 0)))
|
||||
],
|
||||
|
||||
"unpairing" :- [
|
||||
testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) sone
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) SOne
|
||||
(^CasePair One (^BV 0) (SN $ ^FT "B" 0)
|
||||
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0)))
|
||||
(^FT "B" 0) [< One],
|
||||
testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) sone
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) SOne
|
||||
(^CasePair Any (^BV 0) (SN $ ^FT "B" 0)
|
||||
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0)))
|
||||
(^FT "B" 0) [< Any],
|
||||
testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) szero
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) SZero
|
||||
(^CasePair Any (^BV 0) (SN $ ^FT "B" 0)
|
||||
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0)))
|
||||
(^FT "B" 0) [< Zero],
|
||||
testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $
|
||||
infer_ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) sone
|
||||
infer_ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) SOne
|
||||
(^CasePair Zero (^BV 0) (SN $ ^FT "B" 0)
|
||||
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0))),
|
||||
testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r) ⇒ l) ⇒ A ⊳ ω·x" $
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) sone
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) SOne
|
||||
(^CasePair Any (^BV 0) (SN $ ^FT "A" 0)
|
||||
(SY [< "l", "r"] $ ^BVT 1))
|
||||
(^FT "A" 0) [< Any],
|
||||
testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) szero
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) SZero
|
||||
(^CasePair One (^BV 0) (SN $ ^FT "A" 0)
|
||||
(SY [< "l", "r"] $ ^BVT 1))
|
||||
(^FT "A" 0) [< Zero],
|
||||
testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $
|
||||
infer_ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) sone
|
||||
infer_ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) SOne
|
||||
(^CasePair One (^BV 0) (SN $ ^FT "A" 0)
|
||||
(SY [< "l", "r"] $ ^BVT 1)),
|
||||
note "fst : 0.(A : ★₀) → 0.(B : ω.A → ★₀) → ω.((x : A) × B x) → A",
|
||||
note " ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)",
|
||||
testTC "0 · ‹type of fst› ⇐ ★₁" $
|
||||
check_ empty szero fstTy (^TYPE 1),
|
||||
check_ empty SZero fstTy (^TYPE 1),
|
||||
testTC "1 · ‹def of fst› ⇐ ‹type of fst›" $
|
||||
check_ empty sone fstDef fstTy,
|
||||
check_ empty SOne fstDef fstTy,
|
||||
note "snd : 0.(A : ★₀) → 0.(B : A ↠ ★₀) → ω.(p : (x : A) × B x) → B (fst A B p)",
|
||||
note " ≔ (λ A B p ⇒ caseω p return p ⇒ B (fst A B p) of (x, y) ⇒ y)",
|
||||
testTC "0 · ‹type of snd› ⇐ ★₁" $
|
||||
check_ empty szero sndTy (^TYPE 1),
|
||||
check_ empty SZero sndTy (^TYPE 1),
|
||||
testTC "1 · ‹def of snd› ⇐ ‹type of snd›" $
|
||||
check_ empty sone sndDef sndTy,
|
||||
check_ empty SOne sndDef sndTy,
|
||||
testTC "0 · snd A P ⇒ ω.(p : (x : A) × P x) → P (fst A P p)" $
|
||||
inferAs empty szero
|
||||
inferAs empty SZero
|
||||
(^App (^App (^F "snd" 0) (^FT "A" 0)) (^FT "P" 0))
|
||||
(^PiY Any "p" (^SigY "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
|
||||
(E $ ^App (^F "P" 0)
|
||||
(E $ apps (^F "fst" 0) [^FT "A" 0, ^FT "P" 0, ^BVT 0]))),
|
||||
testTC "1 · fst A (λ _ ⇒ B) (a, b) ⇒ A" $
|
||||
inferAs empty sone
|
||||
inferAs empty SOne
|
||||
(apps (^F "fst" 0)
|
||||
[^FT "A" 0, ^LamN (^FT "B" 0), ^Pair (^FT "a" 0) (^FT "b" 0)])
|
||||
(^FT "A" 0),
|
||||
testTC "1 · fst¹ A (λ _ ⇒ B) (a, b) ⇒ A" $
|
||||
inferAs empty sone
|
||||
inferAs empty SOne
|
||||
(apps (^F "fst" 1)
|
||||
[^FT "A" 0, ^LamN (^FT "B" 0), ^Pair (^FT "a" 0) (^FT "b" 0)])
|
||||
(^FT "A" 0),
|
||||
testTCFail "1 · fst ★⁰ (λ _ ⇒ ★⁰) (A, B) ⇏" $
|
||||
infer_ empty sone
|
||||
infer_ empty SOne
|
||||
(apps (^F "fst" 0)
|
||||
[^TYPE 0, ^LamN (^TYPE 0), ^Pair (^FT "A" 0) (^FT "B" 0)]),
|
||||
testTC "0 · fst¹ ★⁰ (λ _ ⇒ ★⁰) (A, B) ⇒ ★⁰" $
|
||||
inferAs empty szero
|
||||
inferAs empty SZero
|
||||
(apps (^F "fst" 1)
|
||||
[^TYPE 0, ^LamN (^TYPE 0), ^Pair (^FT "A" 0) (^FT "B" 0)])
|
||||
(^TYPE 0)
|
||||
|
|
@ -422,23 +422,23 @@ tests = "typechecker" :- [
|
|||
|
||||
"enums" :- [
|
||||
testTC "1 · 'a ⇐ {a}" $
|
||||
check_ empty sone (^Tag "a") (^enum ["a"]),
|
||||
check_ empty SOne (^Tag "a") (^enum ["a"]),
|
||||
testTC "1 · 'a ⇐ {a, b, c}" $
|
||||
check_ empty sone (^Tag "a") (^enum ["a", "b", "c"]),
|
||||
check_ empty SOne (^Tag "a") (^enum ["a", "b", "c"]),
|
||||
testTCFail "1 · 'a ⇍ {b, c}" $
|
||||
check_ empty sone (^Tag "a") (^enum ["b", "c"]),
|
||||
check_ empty SOne (^Tag "a") (^enum ["b", "c"]),
|
||||
testTC "0=1 ⊢ 1 · 'a ⇐ {b, c}" $
|
||||
check_ empty01 sone (^Tag "a") (^enum ["b", "c"])
|
||||
check_ empty01 SOne (^Tag "a") (^enum ["b", "c"])
|
||||
],
|
||||
|
||||
"enum matching" :- [
|
||||
testTC "ω.x : {tt} ⊢ 1 · case1 x return {tt} of { 'tt ⇒ 'tt } ⇒ {tt}" $
|
||||
inferAs (ctx [< ("x", ^enum ["tt"])]) sone
|
||||
inferAs (ctx [< ("x", ^enum ["tt"])]) SOne
|
||||
(^CaseEnum One (^BV 0) (SN (^enum ["tt"]))
|
||||
(singleton "tt" (^Tag "tt")))
|
||||
(^enum ["tt"]),
|
||||
testTCFail "ω.x : {tt} ⊢ 1 · case1 x return {tt} of { 'ff ⇒ 'tt } ⇏" $
|
||||
infer_ (ctx [< ("x", ^enum ["tt"])]) sone
|
||||
infer_ (ctx [< ("x", ^enum ["tt"])]) SOne
|
||||
(^CaseEnum One (^BV 0) (SN (^enum ["tt"]))
|
||||
(singleton "ff" (^Tag "tt")))
|
||||
],
|
||||
|
|
@ -447,44 +447,44 @@ tests = "typechecker" :- [
|
|||
testTC "0 · ℕ ≡ ℕ : ★₀ ⇐ Type" $
|
||||
checkType_ empty (^Eq0 (^TYPE 0) nat nat) Nothing,
|
||||
testTC "0 · ℕ ≡ ℕ : ★₀ ⇐ ★₁" $
|
||||
check_ empty szero (^Eq0 (^TYPE 0) nat nat) (^TYPE 1),
|
||||
check_ empty SZero (^Eq0 (^TYPE 0) nat nat) (^TYPE 1),
|
||||
testTCFail "1 · ℕ ≡ ℕ : ★₀ ⇍ ★₁" $
|
||||
check_ empty sone (^Eq0 (^TYPE 0) nat nat) (^TYPE 1),
|
||||
check_ empty SOne (^Eq0 (^TYPE 0) nat nat) (^TYPE 1),
|
||||
testTC "0 · ℕ ≡ ℕ : ★₀ ⇐ ★₂" $
|
||||
check_ empty szero (^Eq0 (^TYPE 0) nat nat) (^TYPE 2),
|
||||
check_ empty SZero (^Eq0 (^TYPE 0) nat nat) (^TYPE 2),
|
||||
testTC "0 · ℕ ≡ ℕ : ★₁ ⇐ ★₂" $
|
||||
check_ empty szero (^Eq0 (^TYPE 1) nat nat) (^TYPE 2),
|
||||
check_ empty SZero (^Eq0 (^TYPE 1) nat nat) (^TYPE 2),
|
||||
testTCFail "0 · ℕ ≡ ℕ : ★₁ ⇍ ★₁" $
|
||||
check_ empty szero (^Eq0 (^TYPE 1) nat nat) (^TYPE 1),
|
||||
check_ empty SZero (^Eq0 (^TYPE 1) nat nat) (^TYPE 1),
|
||||
testTCFail "0 ≡ 'beep : {beep} ⇍ Type" $
|
||||
checkType_ empty
|
||||
(^Eq0 (^enum ["beep"]) (^Zero) (^Tag "beep"))
|
||||
Nothing,
|
||||
testTC "ab : A ≡ B : ★₀, x : A, y : B ⊢ 0 · Eq [i ⇒ ab i] x y ⇐ ★₀" $
|
||||
check_ (ctx [< ("ab", ^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0)),
|
||||
("x", ^FT "A" 0), ("y", ^FT "B" 0)]) szero
|
||||
("x", ^FT "A" 0), ("y", ^FT "B" 0)]) SZero
|
||||
(^EqY "i" (E $ ^DApp (^BV 2) (^BV 0)) (^BVT 1) (^BVT 0))
|
||||
(^TYPE 0),
|
||||
testTCFail "ab : A ≡ B : ★₀, x : A, y : B ⊢ Eq [i ⇒ ab i] y x ⇍ Type" $
|
||||
check_ (ctx [< ("ab", ^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0)),
|
||||
("x", ^FT "A" 0), ("y", ^FT "B" 0)]) szero
|
||||
("x", ^FT "A" 0), ("y", ^FT "B" 0)]) SZero
|
||||
(^EqY "i" (E $ ^DApp (^BV 2) (^BV 0)) (^BVT 0) (^BVT 1))
|
||||
(^TYPE 0)
|
||||
],
|
||||
|
||||
"equalities" :- [
|
||||
testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $
|
||||
check_ empty sone (^DLamN (^FT "a" 0))
|
||||
check_ empty SOne (^DLamN (^FT "a" 0))
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0)),
|
||||
testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q # uip" $
|
||||
check_ empty szero
|
||||
check_ empty SZero
|
||||
(^LamY "p" (^LamY "q" (^DLamN (^BVT 1))))
|
||||
(^PiY Any "p" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
|
||||
(^PiY Any "q" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
|
||||
(^Eq0 (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
|
||||
(^BVT 1) (^BVT 0)))),
|
||||
testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q # uip(2)" $
|
||||
check_ empty szero
|
||||
check_ empty SZero
|
||||
(^LamY "p" (^LamY "q" (^DLamN (^BVT 0))))
|
||||
(^PiY Any "p" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
|
||||
(^PiY Any "q" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
|
||||
|
|
@ -493,15 +493,15 @@ tests = "typechecker" :- [
|
|||
],
|
||||
|
||||
"natural numbers" :- [
|
||||
testTC "0 · ℕ ⇐ ★₀" $ check_ empty szero nat (^TYPE 0),
|
||||
testTC "0 · ℕ ⇐ ★₇" $ check_ empty szero nat (^TYPE 7),
|
||||
testTCFail "1 · ℕ ⇍ ★₀" $ check_ empty sone nat (^TYPE 0),
|
||||
testTC "1 · zero ⇐ ℕ" $ check_ empty sone (^Zero) nat,
|
||||
testTCFail "1 · zero ⇍ ℕ×ℕ" $ check_ empty sone (^Zero) (^And nat nat),
|
||||
testTC "0 · ℕ ⇐ ★₀" $ check_ empty SZero nat (^TYPE 0),
|
||||
testTC "0 · ℕ ⇐ ★₇" $ check_ empty SZero nat (^TYPE 7),
|
||||
testTCFail "1 · ℕ ⇍ ★₀" $ check_ empty SOne nat (^TYPE 0),
|
||||
testTC "1 · zero ⇐ ℕ" $ check_ empty SOne (^Zero) nat,
|
||||
testTCFail "1 · zero ⇍ ℕ×ℕ" $ check_ empty SOne (^Zero) (^And nat nat),
|
||||
testTC "ω·n : ℕ ⊢ 1 · succ n ⇐ ℕ" $
|
||||
check_ (ctx [< ("n", nat)]) sone (^Succ (^BVT 0)) nat,
|
||||
check_ (ctx [< ("n", nat)]) SOne (^Succ (^BVT 0)) nat,
|
||||
testTC "1 · λ n ⇒ succ n ⇐ 1.ℕ → ℕ" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^LamY "n" (^Succ (^BVT 0)))
|
||||
(^Arr One nat nat)
|
||||
],
|
||||
|
|
@ -510,7 +510,7 @@ tests = "typechecker" :- [
|
|||
note "1 · λ n ⇒ case1 n return ℕ of { zero ⇒ 0; succ n ⇒ n }",
|
||||
note " ⇐ 1.ℕ → ℕ",
|
||||
testTC "pred" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^LamY "n" (E $
|
||||
^CaseNat One Zero (^BV 0) (SN nat)
|
||||
(^Zero) (SY [< "n", ^BN Unused] $ ^BVT 1)))
|
||||
|
|
@ -518,7 +518,7 @@ tests = "typechecker" :- [
|
|||
note "1 · λ m n ⇒ case1 m return ℕ of { zero ⇒ n; succ _, 1.p ⇒ succ p }",
|
||||
note " ⇐ 1.ℕ → 1.ℕ → 1.ℕ",
|
||||
testTC "plus" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
(^LamY "m" (^LamY "n" (E $
|
||||
^CaseNat One One (^BV 1) (SN nat)
|
||||
(^BVT 0)
|
||||
|
|
@ -528,11 +528,11 @@ tests = "typechecker" :- [
|
|||
|
||||
"box types" :- [
|
||||
testTC "0 · [0.ℕ] ⇐ ★₀" $
|
||||
check_ empty szero (^BOX Zero nat) (^TYPE 0),
|
||||
check_ empty SZero (^BOX Zero nat) (^TYPE 0),
|
||||
testTC "0 · [0.★₀] ⇐ ★₁" $
|
||||
check_ empty szero (^BOX Zero (^TYPE 0)) (^TYPE 1),
|
||||
check_ empty SZero (^BOX Zero (^TYPE 0)) (^TYPE 1),
|
||||
testTCFail "0 · [0.★₀] ⇍ ★₀" $
|
||||
check_ empty szero (^BOX Zero (^TYPE 0)) (^TYPE 0)
|
||||
check_ empty SZero (^BOX Zero (^TYPE 0)) (^TYPE 0)
|
||||
],
|
||||
|
||||
todo "box values",
|
||||
|
|
@ -540,7 +540,7 @@ tests = "typechecker" :- [
|
|||
|
||||
"type-case" :- [
|
||||
testTC "0 · type-case ℕ ∷ ★₀ return ★₀ of { _ ⇒ ℕ } ⇒ ★₀" $
|
||||
inferAs empty szero
|
||||
inferAs empty SZero
|
||||
(^TypeCase (^Ann nat (^TYPE 0)) (^TYPE 0) empty nat)
|
||||
(^TYPE 0)
|
||||
],
|
||||
|
|
@ -555,7 +555,7 @@ tests = "typechecker" :- [
|
|||
note "1 · λ x y xy ⇒ δ i ⇒ p (xy i)",
|
||||
note " ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
|
||||
testTC "cong" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
([< "x", "y", "xy"] :\\ [< "i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
|
||||
(PiY Zero "x" (FT "A") $
|
||||
PiY Zero "y" (FT "A") $
|
||||
|
|
@ -568,7 +568,7 @@ tests = "typechecker" :- [
|
|||
note "1 · λ eq ⇒ δ i ⇒ λ x ⇒ eq x i",
|
||||
note " ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
|
||||
testTC "funext" $
|
||||
check_ empty sone
|
||||
check_ empty SOne
|
||||
([< "eq"] :\\ [< "i"] :\\% [< "x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
|
||||
(PiY One "eq"
|
||||
(PiY One "x" (FT "A")
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ import public Quox.Typing
|
|||
import public Quox.Pretty
|
||||
import Quox.Equal
|
||||
import Quox.Typechecker
|
||||
import Quox.ST
|
||||
import Control.Monad.ST.Extra
|
||||
import PrettyExtra
|
||||
|
||||
import Derive.Prelude
|
||||
|
|
@ -25,7 +25,7 @@ runEqual defs act = runSTErr $ do
|
|||
runEff act
|
||||
[handleExcept (\e => stLeft e),
|
||||
handleReaderConst defs,
|
||||
handleStateSTRef !(newRef 0)]
|
||||
handleStateSTRef !(liftST $ newSTRef 0)]
|
||||
|
||||
export
|
||||
runTC : Definitions -> Eff TC a -> Either Error a
|
||||
|
|
|
|||
Loading…
Reference in New Issue