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

use NContext/SnocVect for scope name lists etc

Browse source
This commit is contained in:
rhiannon morris 2023-03-16 18:18:49 +01:00
parent 32f38238ef
commit 6dc7177be5
12 changed files with 165 additions and 134 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
lib/Quox/Context.idr
View file

@ -7,6 +7,7 @@ import Quox.Name
import Data.DPair import Data.DPair
import Data.Nat import Data.Nat
import Data.SnocList import Data.SnocList
import Data.SnocVect
import Data.Vect import Data.Vect
import Control.Monad.Identity import Control.Monad.Identity
@ -68,6 +69,21 @@ export %inline
toList' : Telescope' a _ _ -> List a toList' : Telescope' a _ _ -> List a
toList' = map snd . toList toList' = map snd . toList
export
fromSnocVect : SnocVect n a -> Context' a n
fromSnocVect [<] = [<]
fromSnocVect (sx :< x) = fromSnocVect sx :< x
public export
tabulate : ((n : Nat) -> tm n) -> (n : Nat) -> Context tm n
tabulate f 0 = [<]
tabulate f (S k) = tabulate f k :< f k
public export
replicate : (n : Nat) -> a -> Context' a n
replicate n x = tabulate (const x) n
public export public export
(.) : Telescope tm from mid -> Telescope tm mid to -> Telescope tm from to (.) : Telescope tm from mid -> Telescope tm mid to -> Telescope tm from to
@ -81,6 +97,10 @@ export
rewrite plusSuccRightSucc n to in rewrite plusSuccRightSucc n to in
(tel :< x) <>< xs (tel :< x) <>< xs
export
(++) : Telescope' a from to -> SnocVect n a -> Telescope' a from (n + to)
tel ++ [<] = tel
tel ++ (sx :< x) = (tel ++ sx) :< x
public export public export
getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) -> getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) ->
@ -236,6 +256,12 @@ foldLazy : Monoid a => Telescope' (Lazy a) from to -> a
foldLazy = foldMap force foldLazy = foldMap force
export %inline
all, any : (forall n. tm n -> Bool) -> Telescope tm from to -> Bool
all p = foldMap @{All} p
any p = foldMap @{Any} p
export %inline export %inline
(forall n. Eq (tm n)) => Eq (Telescope tm from to) where (forall n. Eq (tm n)) => Eq (Telescope tm from to) where
(==) = foldLazy @{All} .: zipWithLazy (==) (==) = foldLazy @{All} .: zipWithLazy (==)

2
lib/Quox/Equal.idr
View file

@ -368,7 +368,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
ety <- computeElimType ctx e (noOr1 ne) ety <- computeElimType ctx e (noOr1 ne)
compareType (extendTy zero eret.name ety ctx) eret.term fret.term compareType (extendTy zero eret.name ety ctx) eret.term fret.term
(fst, snd) <- expectSigE defs ctx ety (fst, snd) <- expectSigE defs ctx ety
let [x, y] = ebody.names let [< x, y] = ebody.names
Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx) Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
(substCasePairRet ety eret) (substCasePairRet ety eret)
ebody.term fbody.term ebody.term fbody.term

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

@ -4,8 +4,9 @@ module Quox.Parser.FromParser
import Quox.Parser.Syntax import Quox.Parser.Syntax
import Quox.Parser.Parser import Quox.Parser.Parser
import Quox.Typechecker import Quox.Typechecker
import Data.List
import Data.List
import Data.SnocVect
import public Control.Monad.Either import public Control.Monad.Either
import public Control.Monad.State import public Control.Monad.State
import public Control.Monad.Reader import public Control.Monad.Reader
@ -91,16 +92,16 @@ mutual
Pi pi x s t => Pi pi x s t =>
Pi pi <$> fromPTermWith ds ns s Pi pi <$> fromPTermWith ds ns s
<*> fromPTermTScope ds ns [x] t <*> fromPTermTScope ds ns [< x] t
Lam x s => Lam x s =>
Lam <$> fromPTermTScope ds ns [x] s Lam <$> fromPTermTScope ds ns [< x] s
s :@ t => s :@ t =>
map E $ (:@) <$> fromPTermElim ds ns s <*> fromPTermWith ds ns t map E $ (:@) <$> fromPTermElim ds ns s <*> fromPTermWith ds ns t
Sig x s t => Sig x s t =>
Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [x] t Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [< x] t
Pair s t => Pair s t =>
Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t
@ -108,13 +109,13 @@ mutual
Case pi pair (r, ret) (CasePair (x, y) body) => Case pi pair (r, ret) (CasePair (x, y) body) =>
map E $ Base.CasePair pi map E $ Base.CasePair pi
<$> fromPTermElim ds ns pair <$> fromPTermElim ds ns pair
<*> fromPTermTScope ds ns [r] ret <*> fromPTermTScope ds ns [< r] ret
<*> fromPTermTScope ds ns [x, y] body <*> fromPTermTScope ds ns [< x, y] body
Case pi tag (r, ret) (CaseEnum arms) => Case pi tag (r, ret) (CaseEnum arms) =>
map E $ Base.CaseEnum pi map E $ Base.CaseEnum pi
<$> fromPTermElim ds ns tag <$> fromPTermElim ds ns tag
<*> fromPTermTScope ds ns [r] ret <*> fromPTermTScope ds ns [< r] ret
<*> assert_total fromPTermEnumArms ds ns arms <*> assert_total fromPTermEnumArms ds ns arms
Enum strs => Enum strs =>
@ -127,12 +128,12 @@ mutual
Tag str => pure $ Tag str Tag str => pure $ Tag str
Eq (i, ty) s t => Eq (i, ty) s t =>
Eq <$> fromPTermDScope ds ns [i] ty Eq <$> fromPTermDScope ds ns [< i] ty
<*> fromPTermWith ds ns s <*> fromPTermWith ds ns s
<*> fromPTermWith ds ns t <*> fromPTermWith ds ns t
DLam i s => DLam i s =>
DLam <$> fromPTermDScope ds ns [i] s DLam <$> fromPTermDScope ds ns [< i] s
s :% p => s :% p =>
map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p
@ -163,24 +164,26 @@ mutual
private private
fromPTermTScope : {s : Nat} -> CanError m => fromPTermTScope : {s : Nat} -> CanError m =>
Context' BName d -> Context' BName n -> Context' BName d -> Context' BName n ->
Vect s BName -> SnocVect s BName ->
PTerm -> m (ScopeTermN s Three d n) PTerm -> m (ScopeTermN s Three d n)
fromPTermTScope ds ns xs t = fromPTermTScope ds ns xs t =
if all isNothing xs then if all isNothing xs then
SN <$> fromPTermWith ds ns t SN <$> fromPTermWith ds ns t
else else
SY (map (maybe Unused UN) xs) <$> fromPTermWith ds (ns <>< xs) t SY (fromSnocVect $ map (maybe Unused UN) xs)
<$> fromPTermWith ds (ns ++ xs) t
private private
fromPTermDScope : {s : Nat} -> CanError m => fromPTermDScope : {s : Nat} -> CanError m =>
Context' BName d -> Context' BName n -> Context' BName d -> Context' BName n ->
Vect s BName -> SnocVect s BName ->
PTerm -> m (DScopeTermN s Three d n) PTerm -> m (DScopeTermN s Three d n)
fromPTermDScope ds ns xs t = fromPTermDScope ds ns xs t =
if all isNothing xs then if all isNothing xs then
SN <$> fromPTermWith ds ns t SN <$> fromPTermWith ds ns t
else else
SY (map (maybe Unused UN) xs) <$> fromPTermWith (ds <>< xs) ns t SY (fromSnocVect $ map (maybe Unused UN) xs)
<$> fromPTermWith (ds ++ xs) ns t
export %inline export %inline

14
lib/Quox/Parser/Syntax.idr
View file

@ -121,14 +121,14 @@ mutual
toPTermWith' ds ns s = case s of toPTermWith' ds ns s = case s of
TYPE l => TYPE l =>
TYPE l TYPE l
Pi qty arg (S [x] res) => Pi qty arg (S [< x] res) =>
Pi qty (Just $ show x) Pi qty (Just $ show x)
(toPTermWith ds ns arg) (toPTermWith ds ns arg)
(toPTermWith ds (ns :< baseStr x) res.term) (toPTermWith ds (ns :< baseStr x) res.term)
Lam (S [x] body) => Lam (S [< x] body) =>
Lam (Just $ show x) $ Lam (Just $ show x) $
toPTermWith ds (ns :< baseStr x) body.term toPTermWith ds (ns :< baseStr x) body.term
Sig fst (S [x] snd) => Sig fst (S [< x] snd) =>
Sig (Just $ show x) Sig (Just $ show x)
(toPTermWith ds ns fst) (toPTermWith ds ns fst)
(toPTermWith ds (ns :< baseStr x) snd.term) (toPTermWith ds (ns :< baseStr x) snd.term)
@ -138,10 +138,10 @@ mutual
Enum $ SortedSet.toList cases Enum $ SortedSet.toList cases
Tag tag => Tag tag =>
Tag tag Tag tag
Eq (S [i] ty) l r => Eq (S [< i] ty) l r =>
Eq (Just $ show i, toPTermWith (ds :< baseStr i) ns ty.term) Eq (Just $ show i, toPTermWith (ds :< baseStr i) ns ty.term)
(toPTermWith ds ns l) (toPTermWith ds ns r) (toPTermWith ds ns l) (toPTermWith ds ns r)
DLam (S [i] body) => DLam (S [< i] body) =>
DLam (Just $ show i) $ toPTermWith (ds :< baseStr i) ns body.term DLam (Just $ show i) $ toPTermWith (ds :< baseStr i) ns body.term
E e => E e =>
toPTermWith ds ns e toPTermWith ds ns e
@ -165,12 +165,12 @@ mutual
V $ MakePName [<] $ ns !!! i V $ MakePName [<] $ ns !!! i
fun :@ arg => fun :@ arg =>
toPTermWith ds ns fun :@ toPTermWith ds ns arg toPTermWith ds ns fun :@ toPTermWith ds ns arg
CasePair qty pair (S [r] ret) (S [x, y] body) => CasePair qty pair (S [< r] ret) (S [< x, y] body) =>
Case qty (toPTermWith ds ns pair) Case qty (toPTermWith ds ns pair)
(Just $ show r, toPTermWith ds (ns :< baseStr r) ret.term) (Just $ show r, toPTermWith ds (ns :< baseStr r) ret.term)
(CasePair (Just $ show x, Just $ show y) $ (CasePair (Just $ show x, Just $ show y) $
toPTermWith ds (ns :< baseStr x :< baseStr y) body.term) toPTermWith ds (ns :< baseStr x :< baseStr y) body.term)
CaseEnum qty tag (S [r] ret) arms => CaseEnum qty tag (S [< r] ret) arms =>
Case qty (toPTermWith ds ns tag) Case qty (toPTermWith ds ns tag)
(Just $ show r, toPTermWith ds (ns :< baseStr r) ret.term) (Just $ show r, toPTermWith ds (ns :< baseStr r) ret.term)
(CaseEnum $ mapSnd (toPTermWith ds ns) <$> SortedMap.toList arms) (CaseEnum $ mapSnd (toPTermWith ds ns) <$> SortedMap.toList arms)

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

@ -6,6 +6,7 @@ import public Quox.Syntax.Subst
import public Quox.Syntax.Qty import public Quox.Syntax.Qty
import public Quox.Syntax.Dim import public Quox.Syntax.Dim
import public Quox.Name import public Quox.Name
import public Quox.Context
-- import public Quox.OPE -- import public Quox.OPE
import Quox.Pretty import Quox.Pretty
@ -16,7 +17,6 @@ import Data.Maybe
import Data.Nat import Data.Nat
import public Data.So import public Data.So
import Data.String import Data.String
import Data.Vect
import public Data.SortedMap import public Data.SortedMap
import public Data.SortedSet import public Data.SortedSet
@ -132,7 +132,7 @@ mutual
public export public export
record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where
constructor S constructor S
names : Vect s BaseName names : NContext s
body : ScopedBody s f n body : ScopedBody s f n
public export public export
@ -158,16 +158,16 @@ mutual
||| scope which ignores all its binders ||| scope which ignores all its binders
public export %inline public export %inline
SN : {s : Nat} -> f n -> Scoped s f n SN : {s : Nat} -> f n -> Scoped s f n
SN = S (replicate s "_") . N SN = S (replicate s Unused) . N
||| scope which uses its binders ||| scope which uses its binders
public export %inline public export %inline
SY : Vect s BaseName -> f (s + n) -> Scoped s f n SY : NContext s -> f (s + n) -> Scoped s f n
SY ns = S ns . Y SY ns = S ns . Y
public export %inline public export %inline
name : Scoped 1 f n -> BaseName name : Scoped 1 f n -> BaseName
name (S [x] _) = x name (S [< x] _) = x
public export %inline public export %inline
(.name) : Scoped 1 f n -> BaseName (.name) : Scoped 1 f n -> BaseName
@ -177,7 +177,7 @@ s.name = name s
public export %inline public export %inline
Pi_ : (qty : q) -> (x : BaseName) -> Pi_ : (qty : q) -> (x : BaseName) ->
(arg : Term q d n) -> (res : Term q d (S n)) -> Term q d n (arg : Term q d n) -> (res : Term q d (S n)) -> Term q d n
Pi_ {qty, x, arg, res} = Pi {qty, arg, res = S [x] $ Y res} Pi_ {qty, x, arg, res} = Pi {qty, arg, res = S [< x] $ Y res}
||| non dependent function type ||| non dependent function type
public export %inline public export %inline
@ -188,7 +188,7 @@ Arr {qty, arg, res} = Pi {qty, arg, res = SN res}
public export %inline public export %inline
Sig_ : (x : BaseName) -> (fst : Term q d n) -> Sig_ : (x : BaseName) -> (fst : Term q d n) ->
(snd : Term q d (S n)) -> Term q d n (snd : Term q d (S n)) -> Term q d n
Sig_ {x, fst, snd} = Sig {fst, snd = S [x] $ Y snd} Sig_ {x, fst, snd} = Sig {fst, snd = S [< x] $ Y snd}
||| non dependent pair type ||| non dependent pair type
public export %inline public export %inline
@ -199,7 +199,7 @@ And {fst, snd} = Sig {fst, snd = SN snd}
public export %inline public export %inline
Eq_ : (i : BaseName) -> (ty : Term q (S d) n) -> Eq_ : (i : BaseName) -> (ty : Term q (S d) n) ->
(l, r : Term q d n) -> Term q d n (l, r : Term q d n) -> Term q d n
Eq_ {i, ty, l, r} = Eq {ty = S [i] $ Y ty, l, r} Eq_ {i, ty, l, r} = Eq {ty = S [< i] $ Y ty, l, r}
||| non dependent equality type ||| non dependent equality type
public export %inline public export %inline

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

@ -73,12 +73,13 @@ prettyArm sort xs pat body = do
export export
prettyLams : PrettyHL a => Pretty.HasEnv m => prettyLams : PrettyHL a => Pretty.HasEnv m =>
Maybe (Doc HL) -> BinderSort -> List BaseName -> a -> m (Doc HL) Maybe (Doc HL) -> BinderSort -> SnocList BaseName -> a ->
m (Doc HL)
prettyLams lam sort names body = do prettyLams lam sort names body = do
let var = case sort of T => TVar; D => DVar let var = case sort of T => TVar; D => DVar
header <- sequence $ [hlF var $ prettyM x | x <- names] header <- sequence $ [hlF var $ prettyM x | x <- toList names]
let header = sep $ maybe header (:: header) lam let header = sep $ maybe header (:: header) lam
parensIfM Outer =<< prettyArm sort (cast names) header body parensIfM Outer =<< prettyArm sort names header body
export export
prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m => prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m =>
@ -110,7 +111,7 @@ prettyCase : PrettyHL a => PrettyHL b => PrettyHL c => PrettyHL q =>
m (Doc HL) m (Doc HL)
prettyCase pi elim r ret arms = do prettyCase pi elim r ret arms = do
elim <- prettyQtyBinds [pi] elim elim <- prettyQtyBinds [pi] elim
ret <- prettyLams Nothing T [r] ret ret <- prettyLams Nothing T [< r] ret
arms <- prettyArms arms arms <- prettyArms arms
pure $ asep [caseD <++> elim, returnD <++> ret, ofD <++> arms] pure $ asep [caseD <++> elim, returnD <++> ret, ofD <++> arms]
@ -127,12 +128,12 @@ parameters (showSubsts : Bool)
where where
prettyM (TYPE l) = prettyM (TYPE l) =
parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l) parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
prettyM (Pi qty s (S [x] t)) = prettyM (Pi qty s (S [< x] t)) =
prettyBindType [qty] x s !arrowD t.term prettyBindType [qty] x s !arrowD t.term
prettyM (Lam (S x t)) = prettyM (Lam (S x t)) =
let GotLams {names, body, _} = getLams' x t.term Refl in let GotLams {names, body, _} = getLams' x t.term Refl in
prettyLams (Just !lamD) T (toList names) body prettyLams (Just !lamD) T (toSnocList' names) body
prettyM (Sig s (S [x] t)) = prettyM (Sig s (S [< x] t)) =
prettyBindType {q} [] x s !timesD t.term prettyBindType {q} [] x s !timesD t.term
prettyM (Pair s t) = prettyM (Pair s t) =
let GotPairs {init, last, _} = getPairs' [< s] t in let GotPairs {init, last, _} = getPairs' [< s] t in
@ -147,14 +148,14 @@ parameters (showSubsts : Bool)
r <- withPrec InEq $ prettyM r r <- withPrec InEq $ prettyM r
ty <- withPrec InEq $ prettyM ty ty <- withPrec InEq $ prettyM ty
parensIfM Eq $ asep [l <++> !eqndD, r <++> colonD, ty] parensIfM Eq $ asep [l <++> !eqndD, r <++> colonD, ty]
prettyM (Eq (S [i] (Y ty)) l r) = do prettyM (Eq (S [< i] (Y ty)) l r) = do
ty <- bracks <$> withPrec Outer (prettyLams Nothing D [i] ty) ty <- bracks <$> withPrec Outer (prettyLams Nothing D [< i] ty)
l <- withPrec Arg $ prettyM l l <- withPrec Arg $ prettyM l
r <- withPrec Arg $ prettyM r r <- withPrec Arg $ prettyM r
parensIfM App $ eqD <++> asep [ty, l, r] parensIfM App $ eqD <++> asep [ty, l, r]
prettyM (DLam (S i t)) = prettyM (DLam (S i t)) =
let GotDLams {names, body, _} = getDLams' i t.term Refl in let GotDLams {names, body, _} = getDLams' i t.term Refl in
prettyLams (Just !dlamD) D (toList names) body prettyLams (Just !dlamD) D (toSnocList' names) body
prettyM (E e) = prettyM e prettyM (E e) = prettyM e
prettyM (CloT s th) = prettyM (CloT s th) =
if showSubsts then if showSubsts then
@ -179,10 +180,10 @@ parameters (showSubsts : Bool)
prettyM (e :@ s) = prettyM (e :@ s) =
let GotArgs {fun, args, _} = getArgs' e [s] in let GotArgs {fun, args, _} = getArgs' e [s] in
prettyApps Nothing fun args prettyApps Nothing fun args
prettyM (CasePair pi p (S [r] ret) (S [x, y] body)) = do prettyM (CasePair pi p (S [< r] ret) (S [< x, y] body)) = do
pat <- parens . separate commaD <$> traverse (hlF TVar . prettyM) [x, y] pat <- parens . separate commaD <$> traverse (hlF TVar . prettyM) [x, y]
prettyCase pi p r ret.term [([< x, y], pat, body.term)] prettyCase pi p r ret.term [([< x, y], pat, body.term)]
prettyM (CaseEnum pi t (S [r] ret) arms) = prettyM (CaseEnum pi t (S [< r] ret) arms) =
prettyCase pi t r ret.term prettyCase pi t r ret.term
[([<], prettyTag t, b) | (t, b) <- SortedMap.toList arms] [([<], prettyTag t, b) | (t, b) <- SortedMap.toList arms]
prettyM (e :% d) = prettyM (e :% d) =

43
lib/Quox/Syntax/Term/Split.idr
View file

@ -2,6 +2,7 @@ module Quox.Syntax.Term.Split
import Quox.Syntax.Term.Base import Quox.Syntax.Term.Base
import Quox.Syntax.Term.Subst import Quox.Syntax.Term.Subst
import Quox.Context
import public Quox.No import public Quox.No
import public Data.Vect import public Data.Vect
@ -130,25 +131,23 @@ getDArgs e = getDArgs' e []
infixr 1 :\\ infixr 1 :\\
public export public export
absN : Vect m BaseName -> Term q d (m + n) -> Term q d n absN : NContext m -> Term q d (m + n) -> Term q d n
absN {m = 0} [] s = s absN [<] s = s
absN {m = S m} (x :: xs) s = absN (xs :< x) s = absN xs $ Lam $ SY [< x] s
Lam $ S [x] $ Y $ absN xs $ rewrite sym $ plusSuccRightSucc m n in s
public export %inline public export %inline
(:\\) : Vect m BaseName -> Term q d (m + n) -> Term q d n (:\\) : NContext m -> Term q d (m + n) -> Term q d n
(:\\) = absN (:\\) = absN
infixr 1 :\\% infixr 1 :\\%
public export public export
dabsN : Vect m BaseName -> Term q (m + d) n -> Term q d n dabsN : NContext m -> Term q (m + d) n -> Term q d n
dabsN {m = 0} [] s = s dabsN [<] s = s
dabsN {m = S m} (x :: xs) s = dabsN (xs :< x) s = dabsN xs $ DLam $ SY [< x] s
DLam $ S [x] $ Y $ dabsN xs $ rewrite sym $ plusSuccRightSucc m d in s
public export %inline public export %inline
(:\\%) : Vect m BaseName -> Term q (m + d) n -> Term q d n (:\\%) : NContext m -> Term q (m + d) n -> Term q d n
(:\\%) = dabsN (:\\%) = dabsN
@ -156,7 +155,7 @@ public export
record GetLams q d n where record GetLams q d n where
constructor GotLams constructor GotLams
{0 lams, rest : Nat} {0 lams, rest : Nat}
names : Vect lams BaseName names : NContext lams
body : Term q d rest body : Term q d rest
0 eq : lams + n = rest 0 eq : lams + n = rest
0 notLam : NotLam body 0 notLam : NotLam body
@ -164,7 +163,7 @@ record GetLams q d n where
mutual mutual
export %inline export %inline
getLams' : forall lams, rest. getLams' : forall lams, rest.
Vect lams BaseName -> Term q d rest -> (0 eq : lams + n = rest) -> NContext lams -> Term q d rest -> (0 eq : lams + n = rest) ->
GetLams q d n GetLams q d n
getLams' xs s0 eq = getLams' xs s0 eq =
let Element s nc = pushSubsts s0 in let Element s nc = pushSubsts s0 in
@ -172,25 +171,25 @@ mutual
private private
getLamsNc : forall lams, rest. getLamsNc : forall lams, rest.
Vect lams BaseName -> NContext lams ->
(t : Term q d rest) -> (0 nc : NotClo t) => (t : Term q d rest) -> (0 nc : NotClo t) =>
(0 eq : lams + n = rest) -> (0 eq : lams + n = rest) ->
GetLams q d n GetLams q d n
getLamsNc xs s Refl = case nchoose $ isLam s of getLamsNc xs s Refl = case nchoose $ isLam s of
Left y => let Lam (S [x] body) = s in Left y => let Lam (S [< x] body) = s in
getLams' (x :: xs) (assert_smaller s body.term) Refl getLams' (xs :< x) (assert_smaller s body.term) Refl
Right n => GotLams xs s Refl n Right n => GotLams xs s Refl n
export %inline export %inline
getLams : Term q d n -> GetLams q d n getLams : Term q d n -> GetLams q d n
getLams s = getLams' [] s Refl getLams s = getLams' [<] s Refl
public export public export
record GetDLams q d n where record GetDLams q d n where
constructor GotDLams constructor GotDLams
{0 lams, rest : Nat} {0 lams, rest : Nat}
names : Vect lams BaseName names : NContext lams
body : Term q rest n body : Term q rest n
0 eq : lams + d = rest 0 eq : lams + d = rest
0 notDLam : NotDLam body 0 notDLam : NotDLam body
@ -198,7 +197,7 @@ record GetDLams q d n where
mutual mutual
export %inline export %inline
getDLams' : forall lams, rest. getDLams' : forall lams, rest.
Vect lams BaseName -> Term q rest n -> (0 eq : lams + d = rest) -> NContext lams -> Term q rest n -> (0 eq : lams + d = rest) ->
GetDLams q d n GetDLams q d n
getDLams' xs s0 eq = getDLams' xs s0 eq =
let Element s nc = pushSubsts s0 in let Element s nc = pushSubsts s0 in
@ -206,18 +205,18 @@ mutual
private private
getDLamsNc : forall lams, rest. getDLamsNc : forall lams, rest.
Vect lams BaseName -> NContext lams ->
(t : Term q rest n) -> (0 nc : NotClo t) => (t : Term q rest n) -> (0 nc : NotClo t) =>
(0 eq : lams + d = rest) -> (0 eq : lams + d = rest) ->
GetDLams q d n GetDLams q d n
getDLamsNc is s Refl = case nchoose $ isDLam s of getDLamsNc is s Refl = case nchoose $ isDLam s of
Left y => let DLam (S [i] body) = s in Left y => let DLam (S [< i] body) = s in
getDLams' (i :: is) (assert_smaller s body.term) Refl getDLams' (is :< i) (assert_smaller s body.term) Refl
Right n => GotDLams is s Refl n Right n => GotDLams is s Refl n
export %inline export %inline
getDLams : Term q d n -> GetDLams q d n getDLams : Term q d n -> GetDLams q d n
getDLams s = getDLams' [] s Refl getDLams s = getDLams' [<] s Refl
public export public export

2
lib/Quox/Typechecker.idr
View file

@ -290,7 +290,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐ -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
-- ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y -- ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
-- with ρ₁, ρ₂ ≤ πσ -- with ρ₁, ρ₂ ≤ πσ
let [x, y] = body.names let [< x, y] = body.names
pisg = pi * sg.fst pisg = pi * sg.fst
bodyctx = extendTyN [< (pisg, x, tfst), (pisg, y, tsnd.term)] ctx bodyctx = extendTyN [< (pisg, x, tfst), (pisg, y, tsnd.term)] ctx
bodyty = substCasePairRet pairres.type ret bodyty = substCasePairRet pairres.type ret

58
tests/Tests/Equal.idr
View file

@ -16,7 +16,7 @@ defGlobals = fromList
("a'", mkPostulate Any $ FT "A"), ("a'", mkPostulate Any $ FT "A"),
("b", mkPostulate Any $ FT "B"), ("b", mkPostulate Any $ FT "B"),
("f", mkPostulate Any $ Arr One (FT "A") (FT "A")), ("f", mkPostulate Any $ Arr One (FT "A") (FT "A")),
("id", mkDef Any (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0)), ("id", mkDef Any (Arr One (FT "A") (FT "A")) ([< "x"] :\\ BVT 0)),
("eq-AB", mkPostulate Zero $ Eq0 (TYPE 0) (FT "A") (FT "B"))] ("eq-AB", mkPostulate Zero $ Eq0 (TYPE 0) (FT "A") (FT "B"))]
parameters (label : String) (act : Lazy (M ())) parameters (label : String) (act : Lazy (M ()))
@ -126,31 +126,31 @@ tests = "equality & subtyping" :- [
"lambda" :- [ "lambda" :- [
testEq "λ x ⇒ [x] = λ x ⇒ [x]" $ testEq "λ x ⇒ [x] = λ x ⇒ [x]" $
equalT empty (Arr One (FT "A") (FT "A")) equalT empty (Arr One (FT "A") (FT "A"))
(["x"] :\\ BVT 0) ([< "x"] :\\ BVT 0)
(["x"] :\\ BVT 0), ([< "x"] :\\ BVT 0),
testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $ testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $
subT empty (Arr One (FT "A") (FT "A")) subT empty (Arr One (FT "A") (FT "A"))
(["x"] :\\ BVT 0) ([< "x"] :\\ BVT 0)
(["x"] :\\ BVT 0), ([< "x"] :\\ BVT 0),
testEq "λ x ⇒ [x] = λ y ⇒ [y]" $ testEq "λ x ⇒ [x] = λ y ⇒ [y]" $
equalT empty (Arr One (FT "A") (FT "A")) equalT empty (Arr One (FT "A") (FT "A"))
(["x"] :\\ BVT 0) ([< "x"] :\\ BVT 0)
(["y"] :\\ BVT 0), ([< "y"] :\\ BVT 0),
testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $ testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $
equalT empty (Arr One (FT "A") (FT "A")) equalT empty (Arr One (FT "A") (FT "A"))
(["x"] :\\ BVT 0) ([< "x"] :\\ BVT 0)
(["y"] :\\ BVT 0), ([< "y"] :\\ BVT 0),
testNeq "λ x y ⇒ [x] ≠ λ x y ⇒ [y]" $ testNeq "λ x y ⇒ [x] ≠ λ x y ⇒ [y]" $
equalT empty (Arr One (FT "A") $ Arr One (FT "A") (FT "A")) equalT empty (Arr One (FT "A") $ Arr One (FT "A") (FT "A"))
(["x", "y"] :\\ BVT 1) ([< "x", "y"] :\\ BVT 1)
(["x", "y"] :\\ BVT 0), ([< "x", "y"] :\\ BVT 0),
testEq "λ x ⇒ [a] = λ x ⇒ [a] (Y vs N)" $ testEq "λ x ⇒ [a] = λ x ⇒ [a] (Y vs N)" $
equalT empty (Arr Zero (FT "B") (FT "A")) equalT empty (Arr Zero (FT "B") (FT "A"))
(Lam $ SY ["x"] $ FT "a") (Lam $ SY [< "x"] $ FT "a")
(Lam $ SN $ FT "a"), (Lam $ SN $ FT "a"),
testEq "λ x ⇒ [f [x]] = [f] (η)" $ testEq "λ x ⇒ [f [x]] = [f] (η)" $
equalT empty (Arr One (FT "A") (FT "A")) equalT empty (Arr One (FT "A") (FT "A"))
(["x"] :\\ E (F "f" :@ BVT 0)) ([< "x"] :\\ E (F "f" :@ BVT 0))
(FT "f") (FT "f")
], ],
@ -168,7 +168,7 @@ tests = "equality & subtyping" :- [
"equalities and uip" :- "equalities and uip" :-
let refl : Term q d n -> Term q d n -> Elim q d n let refl : Term q d n -> Term q d n -> Elim q d n
refl a x = (DLam $ S ["_"] $ N x) :# (Eq0 a x x) refl a x = (DLam $ S [< "_"] $ N x) :# (Eq0 a x x)
in in
[ [
note #""refl [A] x" is an abbreviation for "(δ i ⇒ x) ∷ (x ≡ x : A)""#, note #""refl [A] x" is an abbreviation for "(δ i ⇒ x) ∷ (x ≡ x : A)""#,
@ -217,7 +217,7 @@ tests = "equality & subtyping" :- [
{globals = defGlobals `mergeLeft` fromList {globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $ [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
let ty : forall n. Term Three 0 n := let ty : forall n. Term Three 0 n :=
Sig (FT "E") $ S ["_"] $ N $ FT "E" in Sig (FT "E") $ S [< "_"] $ N $ FT "E" in
equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty) equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
(BV 0) (BV 1), (BV 0) (BV 1),
@ -250,12 +250,12 @@ tests = "equality & subtyping" :- [
(FT "b"), (FT "b"),
testEq "(λy ⇒ [#1]){a} = λy ⇒ [a] : B ⇾ A (N)" $ testEq "(λy ⇒ [#1]){a} = λy ⇒ [a] : B ⇾ A (N)" $
equalT empty (Arr Zero (FT "B") (FT "A")) equalT empty (Arr Zero (FT "B") (FT "A"))
(CloT (Lam $ S ["y"] $ N $ BVT 0) (F "a" ::: id)) (CloT (Lam $ S [< "y"] $ N $ BVT 0) (F "a" ::: id))
(Lam $ S ["y"] $ N $ FT "a"), (Lam $ S [< "y"] $ N $ FT "a"),
testEq "(λy ⇒ [#1]){a} = λy ⇒ [a] : B ⇾ A (Y)" $ testEq "(λy ⇒ [#1]){a} = λy ⇒ [a] : B ⇾ A (Y)" $
equalT empty (Arr Zero (FT "B") (FT "A")) equalT empty (Arr Zero (FT "B") (FT "A"))
(CloT (["y"] :\\ BVT 1) (F "a" ::: id)) (CloT ([< "y"] :\\ BVT 1) (F "a" ::: id))
(["y"] :\\ FT "a") ([< "y"] :\\ FT "a")
], ],
"term d-closure" :- [ "term d-closure" :- [
@ -267,8 +267,8 @@ tests = "equality & subtyping" :- [
equalTD 1 equalTD 1
(extendDim "𝑗" empty) (extendDim "𝑗" empty)
(Eq0 (FT "A") (FT "a") (FT "a")) (Eq0 (FT "A") (FT "a") (FT "a"))
(DCloT (["i"] :\\% FT "a") (K Zero ::: id)) (DCloT ([< "i"] :\\% FT "a") (K Zero ::: id))
(["i"] :\\% FT "a"), ([< "i"] :\\% FT "a"),
note "it is hard to think of well-typed terms with big dctxs" note "it is hard to think of well-typed terms with big dctxs"
], ],
@ -334,20 +334,20 @@ tests = "equality & subtyping" :- [
subE empty (F "f" :@ FT "a") (F "f" :@ FT "a"), subE empty (F "f" :@ FT "a") (F "f" :@ FT "a"),
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = ([a ∷ A] ∷ A) (β)" $ testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = ([a ∷ A] ∷ A) (β)" $
equalE empty equalE empty
(((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a") ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
(E (FT "a" :# FT "A") :# FT "A"), (E (FT "a" :# FT "A") :# FT "A"),
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = a (βυ)" $ testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = a (βυ)" $
equalE empty equalE empty
(((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a") ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
(F "a"), (F "a"),
testEq "(λ g ⇒ [g [a]] ∷ ⋯)) [f] = (λ y ⇒ [f [y]] ∷ ⋯) [a] (β↘↙)" $ testEq "(λ g ⇒ [g [a]] ∷ ⋯)) [f] = (λ y ⇒ [f [y]] ∷ ⋯) [a] (β↘↙)" $
let a = FT "A"; a2a = (Arr One a a) in let a = FT "A"; a2a = (Arr One a a) in
equalE empty equalE empty
(((["g"] :\\ E (BV 0 :@ FT "a")) :# Arr One a2a a) :@ FT "f") ((([< "g"] :\\ E (BV 0 :@ FT "a")) :# Arr One a2a a) :@ FT "f")
(((["y"] :\\ E (F "f" :@ BVT 0)) :# a2a) :@ FT "a"), ((([< "y"] :\\ E (F "f" :@ BVT 0)) :# a2a) :@ FT "a"),
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $ testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $
subE empty subE empty
(((["x"] :\\ BVT 0) :# (Arr One (FT "A") (FT "A"))) :@ FT "a") ((([< "x"] :\\ BVT 0) :# (Arr One (FT "A") (FT "A"))) :@ FT "a")
(F "a"), (F "a"),
note "id : A ⊸ A ≔ λ x ⇒ [x]", note "id : A ⊸ A ≔ λ x ⇒ [x]",
testEq "id [a] = a" $ equalE empty (F "id" :@ FT "a") (F "a"), testEq "id [a] = a" $ equalE empty (F "id" :@ FT "a") (F "a"),
@ -407,13 +407,13 @@ tests = "equality & subtyping" :- [
"annotation" :- [ "annotation" :- [
testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = [f] ∷ A ⊸ A" $ testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = [f] ∷ A ⊸ A" $
equalE empty equalE empty
((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A")) (([< "x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
(FT "f" :# Arr One (FT "A") (FT "A")), (FT "f" :# Arr One (FT "A") (FT "A")),
testEq "[f] ∷ A ⊸ A = f" $ testEq "[f] ∷ A ⊸ A = f" $
equalE empty (FT "f" :# Arr One (FT "A") (FT "A")) (F "f"), equalE empty (FT "f" :# Arr One (FT "A") (FT "A")) (F "f"),
testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = f" $ testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = f" $
equalE empty equalE empty
((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A")) (([< "x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
(F "f") (F "f")
], ],

12
tests/Tests/FromPTerm.idr
View file

@ -83,12 +83,14 @@ tests = "PTerm → Term" :- [
parsesAs term fromPTerm' "x" $ BVT 2, parsesAs term fromPTerm' "x" $ BVT 2,
parseFails term fromPTerm' "𝑖", parseFails term fromPTerm' "𝑖",
parsesAs term fromPTerm' "f" $ FT "f", parsesAs term fromPTerm' "f" $ FT "f",
parsesAs term fromPTerm' "λ w ⇒ w" $ ["w"] :\\ BVT 0, parsesAs term fromPTerm' "λ w ⇒ w" $ [< "w"] :\\ BVT 0,
parsesAs term fromPTerm' "λ w ⇒ x" $ ["w"] :\\ BVT 3, parsesAs term fromPTerm' "λ w ⇒ x" $ [< "w"] :\\ BVT 3,
parsesAs term fromPTerm' "λ x ⇒ x" $ ["x"] :\\ BVT 0, parsesAs term fromPTerm' "λ x ⇒ x" $ [< "x"] :\\ BVT 0,
parsesAs term fromPTerm' "λ a b ⇒ f a b" $ parsesAs term fromPTerm' "λ a b ⇒ f a b" $
["a", "b"] :\\ E (F "f" :@@ [BVT 1, BVT 0]), [< "a", "b"] :\\ E (F "f" :@@ [BVT 1, BVT 0]),
parsesAs term fromPTerm' "f @𝑖" $ parsesAs term fromPTerm' "f @𝑖" $
E $ F "f" :% BV 1 E $ F "f" :% BV 1
] ],
todo "everything else"
] ]

22
tests/Tests/Reduce.idr
View file

@ -29,9 +29,9 @@ tests = "whnf" :- [
testNoStep "[A] ⊸ [B]" $ testNoStep "[A] ⊸ [B]" $
Arr One (FT "A") (FT "B"), Arr One (FT "A") (FT "B"),
testNoStep "(x: [A]) ⊸ [B [x]]" $ testNoStep "(x: [A]) ⊸ [B [x]]" $
Pi One (FT "A") (S ["x"] $ Y $ E $ F "B" :@ BVT 0), Pi One (FT "A") (S [< "x"] $ Y $ E $ F "B" :@ BVT 0),
testNoStep "λx. [x]" $ testNoStep "λx. [x]" $
Lam $ S ["x"] $ Y $ BVT 0, Lam $ S [< "x"] $ Y $ BVT 0,
testNoStep "[f [a]]" $ testNoStep "[f [a]]" $
E $ F "f" :@ FT "a" E $ F "f" :@ FT "a"
], ],
@ -51,7 +51,7 @@ tests = "whnf" :- [
(E (TYPE 1 :# TYPE 3)) (E (TYPE 1 :# TYPE 3))
(TYPE 1), (TYPE 1),
testWhnf "(λx. [x] ∷ [A] ⊸ [A]) [a]" testWhnf "(λx. [x] ∷ [A] ⊸ [A]) [a]"
(((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a") ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
(F "a") (F "a")
], ],
@ -87,28 +87,28 @@ tests = "whnf" :- [
"term closure" :- [ "term closure" :- [
testWhnf "(λy. x){a/x}" testWhnf "(λy. x){a/x}"
(CloT (Lam $ S ["y"] $ N $ BVT 0) (F "a" ::: id)) (CloT (Lam $ S [< "y"] $ N $ BVT 0) (F "a" ::: id))
(Lam $ S ["y"] $ N $ FT "a"), (Lam $ S [< "y"] $ N $ FT "a"),
testWhnf "(λy. y){a/x}" testWhnf "(λy. y){a/x}"
(CloT (["y"] :\\ BVT 0) (F "a" ::: id)) (CloT ([< "y"] :\\ BVT 0) (F "a" ::: id))
(["y"] :\\ BVT 0) ([< "y"] :\\ BVT 0)
], ],
"looking inside […]" :- [ "looking inside […]" :- [
testWhnf "[(λx. x ∷ A ⊸ A) [a]]" testWhnf "[(λx. x ∷ A ⊸ A) [a]]"
(E $ ((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a") (E $ (([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
(FT "a") (FT "a")
], ],
"nested redex" :- [ "nested redex" :- [
note "whnf only looks at top level redexes", note "whnf only looks at top level redexes",
testNoStep "λy. [(λx. [x] ∷ [A] ⊸ [A]) [y]]" $ testNoStep "λy. [(λx. [x] ∷ [A] ⊸ [A]) [y]]" $
["y"] :\\ E (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0), [< "y"] :\\ E ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0),
testNoStep "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" $ testNoStep "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" $
F "a" :@ F "a" :@
E (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a"), E ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a"),
testNoStep "λx. [y [x]]{x/x,a/y}" {n = 1} $ testNoStep "λx. [y [x]]{x/x,a/y}" {n = 1} $
["x"] :\\ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id), [< "x"] :\\ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id),
testNoStep "f ([y [x]]{x/x,a/y})" {n = 1} $ testNoStep "f ([y [x]]{x/x,a/y})" {n = 1} $
F "f" :@ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id) F "f" :@ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id)
] ]

50
tests/Tests/Typechecker.idr
View file

@ -41,7 +41,7 @@ reflTy =
Eq0 (BVT 1) (BVT 0) (BVT 0) Eq0 (BVT 1) (BVT 0) (BVT 0)
reflDef : IsQty q => Term q d n reflDef : IsQty q => Term q d n
reflDef = ["A","x"] :\\ ["i"] :\\% BVT 0 reflDef = [< "A","x"] :\\ [< "i"] :\\% BVT 0
fstTy : Term Three d n fstTy : Term Three d n
@ -52,8 +52,8 @@ fstTy =
fstDef : Term Three d n fstDef : Term Three d n
fstDef = fstDef =
(["A","B","p"] :\\ ([< "A","B","p"] :\\
E (CasePair Any (BV 0) (SN $ BVT 2) (SY ["x","y"] $ BVT 1))) E (CasePair Any (BV 0) (SN $ BVT 2) (SY [< "x","y"] $ BVT 1)))
sndTy : Term Three d n sndTy : Term Three d n
sndTy = sndTy =
@ -64,10 +64,10 @@ sndTy =
sndDef : Term Three d n sndDef : Term Three d n
sndDef = sndDef =
(["A","B","p"] :\\ ([< "A","B","p"] :\\
E (CasePair Any (BV 0) E (CasePair Any (BV 0)
(SY ["p"] $ E $ BV 2 :@ E (F "fst" :@@ [BVT 3, BVT 2, BVT 0])) (SY [< "p"] $ E $ BV 2 :@ E (F "fst" :@@ [BVT 3, BVT 2, BVT 0]))
(SY ["x","y"] $ BVT 0))) (SY [< "x","y"] $ BVT 0)))
defGlobals : Definitions Three defGlobals : Definitions Three
@ -270,18 +270,18 @@ tests = "typechecker" :- [
"lambda" :- [ "lambda" :- [
note "linear & unrestricted identity", note "linear & unrestricted identity",
testTC "1 · (λ x ⇒ x) ⇐ A ⊸ A" $ testTC "1 · (λ x ⇒ x) ⇐ A ⊸ A" $
check_ empty sone (["x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")), check_ empty sone ([< "x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")),
testTC "1 · (λ x ⇒ x) ⇐ A → A" $ testTC "1 · (λ x ⇒ x) ⇐ A → A" $
check_ empty sone (["x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")), check_ empty sone ([< "x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")),
note "(fail) zero binding used relevantly", note "(fail) zero binding used relevantly",
testTCFail "1 · (λ x ⇒ x) ⇍ A ⇾ A" $ testTCFail "1 · (λ x ⇒ x) ⇍ A ⇾ A" $
check_ empty sone (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")), check_ empty sone ([< "x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
note "(but ok in overall erased context)", note "(but ok in overall erased context)",
testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $ testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $
check_ empty szero (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")), check_ empty szero ([< "x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯ # (type of refl)" $ testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯ # (type of refl)" $
check_ empty sone check_ empty sone
(["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0])) ([< "A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0]))
reflTy, reflTy,
testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $ testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $
check_ empty sone reflDef reflTy check_ empty sone reflDef reflTy
@ -295,7 +295,7 @@ tests = "typechecker" :- [
(Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any], (Pair (BVT 0) (BVT 0)) (FT "A" `And` FT "A") [< Any],
testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $ testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
check_ empty sone check_ empty sone
(Pair (FT "a") (["i"] :\\% FT "a")) (Pair (FT "a") ([< "i"] :\\% FT "a"))
(Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a")) (Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a"))
], ],
@ -303,36 +303,36 @@ tests = "typechecker" :- [
testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $ testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $
inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) sone inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) sone
(CasePair One (BV 0) (SN $ FT "B") (CasePair One (BV 0) (SN $ FT "B")
(SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
(FT "B") [< One], (FT "B") [< One],
testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $ testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $
inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) sone inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) sone
(CasePair Any (BV 0) (SN $ FT "B") (CasePair Any (BV 0) (SN $ FT "B")
(SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
(FT "B") [< Any], (FT "B") [< Any],
testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $ testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $
inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) szero inferAsQ (ctx [< ("x", FT "A" `And` FT "A")]) szero
(CasePair Any (BV 0) (SN $ FT "B") (CasePair Any (BV 0) (SN $ FT "B")
(SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])) (SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0]))
(FT "B") [< Zero], (FT "B") [< Zero],
testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $ testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $
infer_ (ctx [< ("x", FT "A" `And` FT "A")]) sone infer_ (ctx [< ("x", FT "A" `And` FT "A")]) sone
(CasePair Zero (BV 0) (SN $ FT "B") (CasePair Zero (BV 0) (SN $ FT "B")
(SY ["l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])), (SY [< "l", "r"] $ E $ F "f2" :@@ [BVT 1, BVT 0])),
testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r) ⇒ l) ⇒ A ⊳ ω·x" $ testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r) ⇒ l) ⇒ A ⊳ ω·x" $
inferAsQ (ctx [< ("x", FT "A" `And` FT "B")]) sone inferAsQ (ctx [< ("x", FT "A" `And` FT "B")]) sone
(CasePair Any (BV 0) (SN $ FT "A") (CasePair Any (BV 0) (SN $ FT "A")
(SY ["l", "r"] $ BVT 1)) (SY [< "l", "r"] $ BVT 1))
(FT "A") [< Any], (FT "A") [< Any],
testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $ testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $
inferAsQ (ctx [< ("x", FT "A" `And` FT "B")]) szero inferAsQ (ctx [< ("x", FT "A" `And` FT "B")]) szero
(CasePair One (BV 0) (SN $ FT "A") (CasePair One (BV 0) (SN $ FT "A")
(SY ["l", "r"] $ BVT 1)) (SY [< "l", "r"] $ BVT 1))
(FT "A") [< Zero], (FT "A") [< Zero],
testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $ testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $
infer_ (ctx [< ("x", FT "A" `And` FT "B")]) sone infer_ (ctx [< ("x", FT "A" `And` FT "B")]) sone
(CasePair One (BV 0) (SN $ FT "A") (CasePair One (BV 0) (SN $ FT "A")
(SY ["l", "r"] $ BVT 1)), (SY [< "l", "r"] $ BVT 1)),
note "fst : (0·A : ★₁) → (0·B : A ↠ ★₁) → ((x : A) × B x) ↠ A", note "fst : (0·A : ★₁) → (0·B : A ↠ ★₁) → ((x : A) × B x) ↠ A",
note " ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)", note " ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)",
testTC "0 · ‹type of fst› ⇐ ★₂" $ testTC "0 · ‹type of fst› ⇐ ★₂" $
@ -347,9 +347,9 @@ tests = "typechecker" :- [
check_ empty sone sndDef sndTy, check_ empty sone sndDef sndTy,
testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $ testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $
inferAs empty szero inferAs empty szero
(F "snd" :@@ [TYPE 0, ["x"] :\\ BVT 0]) (F "snd" :@@ [TYPE 0, [< "x"] :\\ BVT 0])
(Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $ (Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $
(E $ F "fst" :@@ [TYPE 0, ["x"] :\\ BVT 0, BVT 0])) (E $ F "fst" :@@ [TYPE 0, [< "x"] :\\ BVT 0, BVT 0]))
], ],
"enums" :- [ "enums" :- [
@ -369,13 +369,13 @@ tests = "typechecker" :- [
(Eq0 (FT "A") (FT "a") (FT "a")), (Eq0 (FT "A") (FT "a") (FT "a")),
testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ empty szero check_ empty szero
(["p","q"] :\\ ["i"] :\\% BVT 1) ([< "p","q"] :\\ [< "i"] :\\% BVT 1)
(Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)), Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)),
testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $ testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ empty szero check_ empty szero
(["p","q"] :\\ ["i"] :\\% BVT 0) ([< "p","q"] :\\ [< "i"] :\\% BVT 0)
(Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)) Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0))
@ -388,7 +388,7 @@ tests = "typechecker" :- [
note " ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)", note " ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
testTC "cong" $ testTC "cong" $
check_ empty sone check_ empty sone
(["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0))) ([< "x", "y", "xy"] :\\ [< "i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
(Pi_ Zero "x" (FT "A") $ (Pi_ Zero "x" (FT "A") $
Pi_ Zero "y" (FT "A") $ Pi_ Zero "y" (FT "A") $
Pi_ One "xy" (Eq0 (FT "A") (BVT 1) (BVT 0)) $ Pi_ One "xy" (Eq0 (FT "A") (BVT 1) (BVT 0)) $
@ -401,7 +401,7 @@ tests = "typechecker" :- [
note " ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q", note " ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
testTC "funext" $ testTC "funext" $
check_ empty sone check_ empty sone
(["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0)) ([< "eq"] :\\ [< "i"] :\\% [< "x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
(Pi_ One "eq" (Pi_ One "eq"
(Pi_ One "x" (FT "A") (Pi_ One "x" (FT "A")
(Eq0 (E $ F "P" :@ BVT 0) (Eq0 (E $ F "P" :@ BVT 0)