add delimited continuations to bib

lib/Quox/Typechecker.idr

@@ -479,23 +479,34 @@ mutual
     pure $ InfRes {type = dsub1 ty dim, qout}
 
   infer' ctx sg (Coe ty p q val loc) = do
+    -- if Ψ, 𝑖 | Γ ⊢₀ A ⇐ Type _
     checkType (extendDim ty.name ctx) ty.term Nothing
+    -- if Ψ | Γ ⊢ σ · s ⇐ A‹p/𝑖› ⊳ Σ
     qout <- checkC ctx sg val $ dsub1 ty p
+    -- then Ψ | Γ ⊢ σ · coe (𝑖 ⇒ A) @p @q s ⇒ A‹q/𝑖› ⊳ Σ
     pure $ InfRes {type = dsub1 ty q, qout}
 
   infer' ctx sg (Comp ty p q val r (S [< j0] val0) (S [< j1] val1) loc) = do
+    -- if Ψ | Γ ⊢₀ A ⇐ Type _
     checkType ctx ty Nothing
+    -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
     qout <- checkC ctx sg val ty
+    -- if Ψ, 𝑗, 𝑖=0      | Γ ⊢ σ · t₀ ⇐ A ⊳ Σ₀
+    --    Ψ, 𝑗, 𝑖=0, 𝑗=p | Γ ⊢ t₀ = s ⇐ A
     let ty'  = dweakT 1 ty; val' = dweakT 1 val; p' = weakD 1 p
         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) sg ty' val0 val'
+    -- if Ψ, 𝑗, 𝑖=1      | Γ ⊢ σ · t₁ ⇐ A ⊳ Σ₁
+    --    Ψ, 𝑗, 𝑖=1, 𝑗=p | Γ ⊢ t₁ = s ⇐ A
     let ctx1 = extendDim j1 $ eqDim r (K One j1.loc) ctx
         val1  = getTerm val1
     qout1 <- check ctx1 sg val1 ty'
+    -- if Σ = Σ₀ = Σ₁
     lift $ equal loc (eqDim (B VZ p.loc) p' ctx1) sg ty' val1 val'
     let qouts  = qout :: catMaybes [toMaybe qout0, toMaybe qout1]
+    -- then Ψ | Γ ⊢ comp A @p @q s @r {0 𝑗 ⇒ t₀; 1 𝑗 ⇒ t₁} ⇒ A ⊳ Σ
     pure $ InfRes {type = ty, qout = lubs ctx qouts}
 
   infer' ctx sg (TypeCase ty ret arms def loc) = do

lib/Quox/Whnf/Coercion.idr

@@ -199,7 +199,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
             fstInSnd =
               CoeT !(fresh i)
                    (tfst // (BV 0 loc ::: shift 2))
-                   (weakD 1 p) (BV 0 loc) (dweakT 1 s) fst.loc
+                   (weakD 1 p) (BV 0 loc) (dweakT 1 fst) fst.loc
             snd' = CoeT i (sub1 tsnd fstInSnd) p q snd snd.loc
         whnf defs ctx sg $
           Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc

pack.toml

@@ -1,4 +1,4 @@
-collection = "nightly-240101"
+collection = "nightly-240326"
 
 [custom.all.tap]
 type = "git"

quox.bib

@@ -20,7 +20,7 @@
 @article{granule,
   author  = {Dominic Orchard and Vilem{-}Benjamin Liepelt and Harley Eades III},
   title   = {Quantitative program reasoning with graded modal types},
-  journal = {Proceedings of the ACM on Programming Languages},
+  journal = {Proceedings of the {ACM} on Programming Languages},
   volume  = {3},
   number  = {{ICFP}},
   pages   = {110:1--110:30},
@@ -198,7 +198,7 @@
   number = {POPL},
   url = {https://doi.org/10.1145/3498670},
   doi = {10.1145/3498670},
-  journal = {Proc. ACM Program. Lang.},
+  journal = {Proc. {ACM} Program. Lang.},
   month = {jan},
   articleno = {9},
   numpages = {31},
@@ -239,7 +239,7 @@
     for universe levels based on displacement algebras, for use in proof
     assistant implementations.
   },
-  journal = {Proc. ACM Program. Lang.},
+  journal = {Proc. {ACM} Program. Lang.},
   month = {jan},
   articleno = {57},
   numpages = {27},
@@ -362,9 +362,9 @@
   date         = {2019-07},
   doi          = {10.1145/3341711},
   issn         = {2475-1421},
-  journaltitle = {Proceedings of the ACM on Programming Languages},
+  journaltitle = {Proceedings of the {ACM} on Programming Languages},
   keywords     = {Modal types,dependent types,normalization by evaluation,type-checking},
-  number       = {ICFP},
+  number       = {{ICFP}},
   pages        = {107:1--107:29},
   title        = {Implementing a Modal Dependent Type Theory},
   volume       = {3},
@@ -389,7 +389,7 @@
 @article{defunc,
   author  = {Yulong Huang and Jeremy Yallop},
   title   = {Defunctionalization with Dependent Types},
-  journal = {Proceedings of the ACM on Programming Languages},
+  journal = {Proceedings of the {ACM} on Programming Languages},
   volume  = {7},
   number  = {{PLDI}},
   pages   = {516--538},
@@ -397,3 +397,18 @@
   url     = {https://doi.org/10.1145/3591241},
   doi     = {10.1145/3591241},
 }
+
+@inproceedings{delcont-callcc,
+  author       = {Martin Gasbichler and Michael Sperber},
+  editor       = {Mitchell Wand and Simon L. Peyton Jones},
+  title        = {Final shift for \texttt{call/cc}:
+                  direct implementation of shift and reset},
+  journaltitle = {Proceedings of the {ACM} on Programming Languages},
+  number       = {{ICFP}},
+  pages        = {271--282},
+  publisher    = {{ACM}},
+  year         = {2002},
+  % url          = {https://doi.org/10.1145/581478.581504},
+  url          = {https://www.cs.tufts.edu/~nr/cs257/archive/mike-sperber/shift-reset-direct.pdf},
+  doi          = {10.1145/581478.581504},
+}

tests/Tests/PrettyTerm.idr

@@ -215,6 +215,7 @@ tests = "pretty printing terms" :- [
       "type-case Nat :: Type 0 return Type 0 of { _ => Nat }"
   ],
 
+  skipWith "(todo: print user-written redundant annotations)" $
   "annotations" :- [
     testPrettyE [<] [<]
       (^Ann (^FT "a" 0) (^FT "A" 0))