golden-tests/tests/isprop-subsing/expected

@@ -0,0 +1,2 @@
+0.IsProp : 1.★ → ★
+0.feq : 1.(A : ★) → 1.(f : IsProp A) → 1.(g : IsProp A) → f ≡ g : IsProp A

golden-tests/tests/isprop-subsing/isprop-subsing.quox

@@ -0,0 +1,4 @@
+def0 IsProp : ★ → ★ = λ A ⇒ (x y : A) → x ≡ y : A
+
+def0 feq : (A : ★) → (f g : IsProp A) → f ≡ g : IsProp A =
+  λ A f g ⇒ δ _ ⇒ f

golden-tests/tests/isprop-subsing/run

@@ -0,0 +1,2 @@
+. ../lib.sh
+check "$1" isprop-subsing.quox

golden-tests/tests/useless-coe/coe.quox

@@ -0,0 +1,9 @@
+-- non-dependent coe should reduce to its body
+
+def five  : ℕ = 5
+def five? : ℕ = coe ℕ 5
+
+def eq : five ≡ five? : ℕ = δ _ ⇒ 5
+
+def subst1 : 0.(P : ℕ → ★) → P five  → P five? = λ P p ⇒ p
+def subst2 : 0.(P : ℕ → ★) → P five? → P five  = λ P p ⇒ p

golden-tests/tests/useless-coe/expected

@@ -0,0 +1,5 @@
+ω.five : ℕ
+ω.five? : ℕ
+ω.eq : five ≡ five? : ℕ
+ω.subst1 : 0.(P : 1.ℕ → ★) → 1.(P five) → P five?
+ω.subst2 : 0.(P : 1.ℕ → ★) → 1.(P five?) → P five

golden-tests/tests/useless-coe/run

@@ -0,0 +1,2 @@
+. ../lib.sh
+check "$1" coe.quox

lib/Quox/OPE.idr

@@ -1,76 +0,0 @@
-||| "order preserving embeddings", for recording a correspondence between
-||| a smaller scope and part of a larger one.
-module Quox.OPE
-
-import Quox.NatExtra
-import Data.Nat
-
-%default total
-
-
-public export
-data OPE : Nat -> Nat -> Type where
-  Id   : OPE n n
-  Drop : OPE m n -> OPE m     (S n)
-  Keep : OPE m n -> OPE (S m) (S n)
-%name OPE p, q
-
-public export %inline Injective Drop where injective Refl = Refl
-public export %inline Injective Keep where injective Refl = Refl
-
-public export
-opeZero : {n : Nat} -> OPE 0 n
-opeZero {n = 0}   = Id
-opeZero {n = S n} = Drop opeZero
-
-public export
-(.) : OPE m n -> OPE n p -> OPE m p
-p      . Id     = p
-Id     . q      = q
-p      . Drop q = Drop $ p . q
-Drop p . Keep q = Drop $ p . q
-Keep p . Keep q = Keep $ p . q
-
-public export
-toLTE : {m : Nat} -> OPE m n -> m `LTE` n
-toLTE Id       = reflexive
-toLTE (Drop p) = lteSuccRight $ toLTE p
-toLTE (Keep p) = LTESucc      $ toLTE p
-
-
-public export
-keepN : (n : Nat) -> OPE a b -> OPE (n + a) (n + b)
-keepN 0     p = p
-keepN (S n) p = Keep $ keepN n p
-
-public export
-dropInner' : LTE' m n -> OPE m n
-dropInner' LTERefl      = Id
-dropInner' (LTESuccR p) = Drop $ dropInner' $ force p
-
-public export
-dropInner : {n : Nat} -> LTE m n -> OPE m n
-dropInner = dropInner' . fromLte
-
-public export
-dropInnerN : (m : Nat) -> OPE n (m + n)
-dropInnerN 0     = Id
-dropInnerN (S m) = Drop $ dropInnerN m
-
-
-public export
-interface Tighten t where
-  tighten : OPE m n -> t n -> Maybe (t m)
-
-parameters {auto _ : Tighten t}
-  export %inline
-  tightenInner : {n : Nat} -> m `LTE` n -> t n -> Maybe (t m)
-  tightenInner = tighten . dropInner
-
-  export %inline
-  tightenN : (m : Nat) -> t (m + n) -> Maybe (t n)
-  tightenN m = tighten $ dropInnerN m
-
-  export %inline
-  tighten1 : t (S n) -> Maybe (t n)
-  tighten1 = tightenN 1

lib/Quox/Parser/FromParser.idr

@@ -297,7 +297,7 @@ mutual
     if all isUnused xs then
       SN <$> fromPTermWith ds ns t
     else
-      ST (fromSnocVect $ map fromPatVar xs) <$> fromPTermWith ds (ns ++ xs) t
+      SY (fromSnocVect $ map fromPatVar xs) <$> fromPTermWith ds (ns ++ xs) t
 
   private
   fromPTermDScope : {s : Nat} -> Context' PatVar d -> Context' PatVar n ->
@@ -307,7 +307,7 @@ mutual
     if all isUnused xs then
       SN {f = \d => Term d n} <$> fromPTermWith ds ns t
     else
-      DST (fromSnocVect $ map fromPatVar xs) <$> fromPTermWith (ds ++ xs) ns t
+      SY (fromSnocVect $ map fromPatVar xs) <$> fromPTermWith (ds ++ xs) ns t
 
 
 export %inline

lib/Quox/Syntax/Term.idr

@@ -3,4 +3,3 @@ module Quox.Syntax.Term
 import public Quox.Syntax.Term.Base
 import public Quox.Syntax.Term.Subst
 import public Quox.Syntax.Term.Pretty
-import public Quox.Syntax.Term.Tighten

lib/Quox/Syntax/Term/Base.idr

@@ -398,6 +398,12 @@ public export %inline
 DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
 DLamN {body, loc} = DLam {body = SN body, loc}
 
+||| more convenient Coe
+public export %inline
+CoeY : (i : BindName) -> (ty : Term (S d) n) ->
+       (p, q : Dim d) -> (val : Term d n) -> (loc : Loc) -> Elim d n
+CoeY {i, ty, p, q, val, loc} = Coe {ty = SY [< i] ty, p, q, val, loc}
+
 ||| non dependent equality type
 public export %inline
 Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n

lib/Quox/Syntax/Term/Subst.idr

@@ -354,3 +354,31 @@ PushSubsts Term Subst.isCloT where
     pushSubstsWith th (comp th ps ph) s
   pushSubstsWith th ph (DCloT (Sub s ps)) =
     pushSubstsWith (ps . th) ph s
+
+
+||| heterogeneous comp, in terms of Comp and Coe
+public export %inline
+CompH' : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
+         (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
+CompH' {ty, p, q, val, r, zero, one, loc} =
+  let ty' = SY ty.names $ ty.term // (B VZ ty.name.loc ::: shift 2) in
+  Comp {
+    ty = dsub1 ty q, p, q,
+    val = E $ Coe ty p q val val.loc, r,
+    zero = SY zero.names $ E $
+      Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc,
+    one = SY one.names $ E $
+      Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc,
+    loc
+  }
+
+||| heterogeneous comp, in terms of Comp and Coe
+public export %inline
+CompH : (i : BindName) -> (ty : Term (S d) n) ->
+        (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
+        (j0 : BindName) -> (zero : Term (S d) n) ->
+        (j1 : BindName) -> (one : Term (S d) n) ->
+        (loc : Loc) -> Elim d n
+CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} =
+  CompH' {ty = SY [< i] ty, p, q, val, r,
+          zero = SY [< j0] zero, one = SY [< j1] one, loc}

lib/Quox/Syntax/Term/Tighten.idr

@@ -1,376 +0,0 @@
-module Quox.Syntax.Term.Tighten
-
-import Quox.Syntax.Term.Base
-import Quox.Syntax.Term.Subst
-import public Quox.OPE
-import Quox.No
-
-%default total
-
-
-export
-Tighten Dim where
-  tighten p (K e loc) = pure $ K e loc
-  tighten p (B i loc) = B <$> tighten p i <*> pure loc
-
-export
-tightenScope : (forall m, n. OPE m n -> f n -> Maybe (f m)) ->
-               {s : Nat} -> OPE m n -> Scoped s f n -> Maybe (Scoped s f m)
-tightenScope f p (S names (Y body)) = SY names <$> f (keepN s p) body
-tightenScope f p (S names (N body)) = S names . N <$> f p body
-
-export
-tightenDScope : {0 f : Nat -> Nat -> Type} ->
-                (forall m, n, k. OPE m n -> f n k -> Maybe (f m k)) ->
-                OPE m n -> Scoped s (f n) k -> Maybe (Scoped s (f m) k)
-tightenDScope f p (S names (Y body)) = SY names <$> f p body
-tightenDScope f p (S names (N body)) = S names . N <$> f p body
-
-
-mutual
-  private
-  tightenT : OPE n1 n2 -> Term d n2 -> Maybe (Term d n1)
-  tightenT p s =
-    let Element s' _ = pushSubsts s in
-    tightenT' p $ assert_smaller s s'
-
-  private
-  tightenE : OPE n1 n2 -> Elim d n2 -> Maybe (Elim d n1)
-  tightenE p e =
-    let Element e' _ = pushSubsts e in
-    tightenE' p $ assert_smaller e e'
-
-  private
-  tightenT' : OPE n1 n2 -> (t : Term d n2) -> (0 nt : NotClo t) =>
-              Maybe (Term d n1)
-  tightenT' p (TYPE l loc) = pure $ TYPE l loc
-  tightenT' p (IOState loc) = pure $ IOState loc
-  tightenT' p (Pi qty arg res loc) =
-    Pi qty <$> tightenT p arg <*> tightenS p res <*> pure loc
-  tightenT' p (Lam body loc) =
-    Lam <$> tightenS p body <*> pure loc
-  tightenT' p (Sig fst snd loc) =
-    Sig <$> tightenT p fst <*> tightenS p snd <*> pure loc
-  tightenT' p (Pair fst snd loc) =
-    Pair <$> tightenT p fst <*> tightenT p snd <*> pure loc
-  tightenT' p (Enum cases loc) =
-    pure $ Enum cases loc
-  tightenT' p (Tag tag loc) =
-    pure $ Tag tag loc
-  tightenT' p (Eq ty l r loc) =
-    Eq <$> tightenDS p ty <*> tightenT p l <*> tightenT p r <*> pure loc
-  tightenT' p (DLam body loc) =
-    DLam <$> tightenDS p body <*> pure loc
-  tightenT' p (NAT loc) =
-    pure $ NAT loc
-  tightenT' p (Nat n loc) =
-    pure $ Nat n loc
-  tightenT' p (Succ s loc) =
-    Succ <$> tightenT p s <*> pure loc
-  tightenT' p (STRING loc) =
-    pure $ STRING loc
-  tightenT' p (Str s loc) =
-    pure $ Str s loc
-  tightenT' p (BOX qty ty loc) =
-    BOX qty <$> tightenT p ty <*> pure loc
-  tightenT' p (Box val loc) =
-    Box <$> tightenT p val <*> pure loc
-  tightenT' p (Let qty rhs body loc) =
-    Let qty <$> assert_total tightenE p rhs <*> tightenS p body <*> pure loc
-  tightenT' p (E e) =
-    E <$> assert_total tightenE p e
-
-  private
-  tightenE' : OPE n1 n2 -> (e : Elim d n2) -> (0 ne : NotClo e) =>
-              Maybe (Elim d n1)
-  tightenE' p (F x u loc) =
-    pure $ F x u loc
-  tightenE' p (B i loc) =
-    B <$> tighten p i <*> pure loc
-  tightenE' p (App fun arg loc) =
-    App <$> tightenE p fun <*> tightenT p arg <*> pure loc
-  tightenE' p (CasePair qty pair ret body loc) =
-    CasePair qty <$> tightenE p pair
-                 <*> 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
-                 <*> traverse (tightenT p) arms
-                 <*> pure loc
-  tightenE' p (CaseNat qty qtyIH nat ret zero succ loc) =
-    CaseNat qty qtyIH
-      <$> tightenE p nat
-      <*> tightenS p ret
-      <*> tightenT p zero
-      <*> tightenS p succ
-      <*> pure loc
-  tightenE' p (CaseBox qty box ret body loc) =
-    CaseBox qty <$> tightenE p box
-                <*> tightenS p ret
-                <*> tightenS p body
-                <*> pure loc
-  tightenE' p (DApp fun arg loc) =
-    DApp <$> tightenE p fun <*> pure arg <*> pure loc
-  tightenE' p (Ann tm ty loc) =
-    Ann <$> tightenT p tm <*> tightenT p ty <*> pure loc
-  tightenE' p (Coe ty q0 q1 val loc) =
-    Coe <$> tightenDS p ty
-        <*> pure q0 <*> pure q1
-        <*> tightenT p val
-        <*> pure loc
-  tightenE' p (Comp ty q0 q1 val r zero one loc) =
-    Comp <$> tightenT p ty
-         <*> pure q0 <*> pure q1
-         <*> tightenT p val
-         <*> pure r
-         <*> tightenDS p zero
-         <*> tightenDS p one
-         <*> pure loc
-  tightenE' p (TypeCase ty ret arms def loc) =
-    TypeCase <$> tightenE p ty
-             <*> tightenT p ret
-             <*> traverse (tightenS p) arms
-             <*> tightenT p def
-             <*> pure loc
-
-  export
-  tightenS : {s : Nat} -> OPE m n ->
-             ScopeTermN s f n -> Maybe (ScopeTermN s f m)
-  tightenS = assert_total $ tightenScope tightenT
-
-  export
-  tightenDS : OPE m n -> DScopeTermN s f n -> Maybe (DScopeTermN s f m)
-  tightenDS = assert_total $ tightenDScope tightenT {f = \n, d => Term d n}
-
-export Tighten (Elim d) where tighten p e = tightenE p e
-export Tighten (Term d) where tighten p t = tightenT p t
-
-
-mutual
-  export
-  dtightenT : OPE d1 d2 -> Term d2 n -> Maybe (Term d1 n)
-  dtightenT p s =
-    let Element s' _ = pushSubsts s in
-    dtightenT' p $ assert_smaller s s'
-
-  export
-  dtightenE : OPE d1 d2 -> Elim d2 n -> Maybe (Elim d1 n)
-  dtightenE p e =
-    let Element e' _ = pushSubsts e in
-    dtightenE' p $ assert_smaller e e'
-
-  private
-  dtightenT' : OPE d1 d2 -> (t : Term d2 n) -> (0 nt : NotClo t) =>
-               Maybe (Term d1 n)
-  dtightenT' p (TYPE l loc) =
-    pure $ TYPE l loc
-  dtightenT' p (IOState loc) =
-    pure $ IOState loc
-  dtightenT' p (Pi qty arg res loc) =
-    Pi qty <$> dtightenT p arg <*> dtightenS p res <*> pure loc
-  dtightenT' p (Lam body loc) =
-    Lam <$> dtightenS p body <*> pure loc
-  dtightenT' p (Sig fst snd loc) =
-    Sig <$> dtightenT p fst <*> dtightenS p snd <*> pure loc
-  dtightenT' p (Pair fst snd loc) =
-    Pair <$> dtightenT p fst <*> dtightenT p snd <*> pure loc
-  dtightenT' p (Enum cases loc) =
-    pure $ Enum cases loc
-  dtightenT' p (Tag tag loc) =
-    pure $ Tag tag loc
-  dtightenT' p (Eq ty l r loc) =
-    Eq <$> dtightenDS p ty <*> dtightenT p l <*> dtightenT p r <*> pure loc
-  dtightenT' p (DLam body loc) =
-    DLam <$> dtightenDS p body <*> pure loc
-  dtightenT' p (NAT loc) =
-    pure $ NAT loc
-  dtightenT' p (Nat n loc) =
-    pure $ Nat n loc
-  dtightenT' p (Succ s loc) =
-    Succ <$> dtightenT p s <*> pure loc
-  dtightenT' p (STRING loc) =
-    pure $ STRING loc
-  dtightenT' p (Str s loc) =
-    pure $ Str s loc
-  dtightenT' p (BOX qty ty loc) =
-    BOX qty <$> dtightenT p ty <*> pure loc
-  dtightenT' p (Box val loc) =
-    Box <$> dtightenT p val <*> pure loc
-  dtightenT' p (Let qty rhs body loc) =
-    Let qty <$> assert_total dtightenE p rhs <*> dtightenS p body <*> pure loc
-  dtightenT' p (E e) =
-    E <$> assert_total dtightenE p e
-
-  export
-  dtightenE' : OPE d1 d2 -> (e : Elim d2 n) -> (0 ne : NotClo e) =>
-               Maybe (Elim d1 n)
-  dtightenE' p (F x u loc) =
-    pure $ F x u loc
-  dtightenE' p (B i loc) =
-    pure $ B i loc
-  dtightenE' p (App fun arg loc) =
-    App <$> dtightenE p fun <*> dtightenT p arg <*> pure loc
-  dtightenE' p (CasePair qty pair ret body loc) =
-    CasePair qty <$> dtightenE p pair
-                 <*> 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
-                 <*> traverse (dtightenT p) arms
-                 <*> pure loc
-  dtightenE' p (CaseNat qty qtyIH nat ret zero succ loc) =
-    CaseNat qty qtyIH
-      <$> dtightenE p nat
-      <*> dtightenS p ret
-      <*> dtightenT p zero
-      <*> dtightenS p succ
-      <*> pure loc
-  dtightenE' p (CaseBox qty box ret body loc) =
-    CaseBox qty <$> dtightenE p box
-                <*> dtightenS p ret
-                <*> dtightenS p body
-                <*> pure loc
-  dtightenE' p (DApp fun arg loc) =
-    DApp <$> dtightenE p fun <*> tighten p arg <*> pure loc
-  dtightenE' p (Ann tm ty loc) =
-    Ann <$> dtightenT p tm <*> dtightenT p ty <*> pure loc
-  dtightenE' p (Coe ty q0 q1 val loc) =
-    [|Coe (dtightenDS p ty) (tighten p q0) (tighten p q1) (dtightenT p val)
-          (pure loc)|]
-  dtightenE' p (Comp ty q0 q1 val r zero one loc) =
-    [|Comp (dtightenT p ty) (tighten p q0) (tighten p q1)
-           (dtightenT p val) (tighten p r)
-           (dtightenDS p zero) (dtightenDS p one) (pure loc)|]
-  dtightenE' p (TypeCase ty ret arms def loc) =
-    [|TypeCase (dtightenE p ty) (dtightenT p ret)
-               (traverse (dtightenS p) arms) (dtightenT p def) (pure loc)|]
-
-  export
-  dtightenS : OPE d1 d2 -> ScopeTermN s d2 n -> Maybe (ScopeTermN s d1 n)
-  dtightenS = assert_total $ tightenDScope dtightenT {f = Term}
-
-  export
-  dtightenDS : {s : Nat} -> OPE d1 d2 ->
-               DScopeTermN s d2 n -> Maybe (DScopeTermN s d1 n)
-  dtightenDS = assert_total $ tightenScope dtightenT
-
-
-export Tighten (\d => Term d n) where tighten p t = dtightenT p t
-export Tighten (\d => Elim d n) where tighten p e = dtightenE p e
-
-
-parameters {auto _ : Tighten f} {s : Nat}
-  export
-  squeeze : Scoped s f n -> (BContext s, Either (f (s + n)) (f n))
-  squeeze (S ns (N t)) = (ns, Right t)
-  squeeze (S ns (Y t)) = (ns, maybe (Left t) Right $ tightenN s t)
-
-  export
-  squeeze' : Scoped s f n -> Scoped s f n
-  squeeze' t = let (ns, res) = squeeze t in S ns $ either Y N res
-
-parameters {0 f : Nat -> Nat -> Type}
-           {auto tt : Tighten (\d => f d n)} {s : Nat}
-  export
-  dsqueeze : Scoped s (\d => f d n) d ->
-             (BContext s, Either (f (s + d) n) (f d n))
-  dsqueeze = squeeze
-
-  export
-  dsqueeze' : Scoped s (\d => f d n) d -> Scoped s (\d => f d n) d
-  dsqueeze' = squeeze'
-
-
--- versions of SY, etc, that try to tighten and use SN automatically
-
-public export %inline
-ST : Tighten f => {s : Nat} -> BContext s -> f (s + n) -> Scoped s f n
-ST names body = squeeze' $ SY names body
-
-public export %inline
-DST : {s : Nat} -> BContext s -> Term (s + d) n -> DScopeTermN s d n
-DST names body = dsqueeze' {f = Term} $ SY names body
-
-public export %inline
-PiT : (qty : Qty) -> (x : BindName) ->
-      (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
-PiT {qty, x, arg, res, loc} = Pi {qty, arg, res = ST [< x] res, loc}
-
-public export %inline
-LamT : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
-LamT {x, body, loc} = Lam {body = ST [< x] body, loc}
-
-public export %inline
-SigT : (x : BindName) -> (fst : Term d n) ->
-       (snd : Term d (S n)) -> (loc : Loc) -> Term d n
-SigT {x, fst, snd, loc} = Sig {fst, snd = ST [< x] snd, loc}
-
-public export %inline
-EqT : (i : BindName) -> (ty : Term (S d) n) ->
-      (l, r : Term d n) -> (loc : Loc) -> Term d n
-EqT {i, ty, l, r, loc} = Eq {ty = DST [< i] ty, l, r, loc}
-
-public export %inline
-DLamT : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
-DLamT {i, body, loc} = DLam {body = DST [< i] body, loc}
-
-public export %inline
-CoeT : (i : BindName) -> (ty : Term (S d) n) ->
-       (p, q : Dim d) -> (val : Term d n) -> (loc : Loc) -> Elim d n
-CoeT {i, ty, p, q, val, loc} = Coe {ty = DST [< i] ty, p, q, val, loc}
-
-public export %inline
-typeCase1T : Elim d n -> Term d n ->
-             (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
-             (loc : Loc) ->
-             {default (NAT loc) def : Term d n} ->
-             Elim d n
-typeCase1T ty ret k ns body loc {def} =
-  typeCase ty ret [(k ** ST ns body)] def loc
-
-
-public export %inline
-CompH' : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
-         (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
-CompH' {ty, p, q, val, r, zero, one, loc} =
-  let ty' = DST ty.names $ ty.term // (B VZ ty.name.loc ::: shift 2) in
-  Comp {
-    ty = dsub1 ty q, p, q,
-    val = E $ Coe ty p q val val.loc, r,
-    zero = DST zero.names $ E $
-      Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc,
-    one = DST one.names $ E $
-      Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc,
-    loc
-  }
-
-||| heterogeneous composition, using Comp and Coe (and subst)
-|||
-||| comp [i ⇒ A] @p @q s @r { 0 j ⇒ t₀; 1 j ⇒ t₁ }
-||| ≔
-||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) @r {
-|||   0 j ⇒ coe [i ⇒ A] @j @q t₀;
-|||   1 j ⇒ coe [i ⇒ A] @j @q t₁
-||| }
-public export %inline
-CompH : (i : BindName) -> (ty : Term (S d) n) ->
-        (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
-        (j0 : BindName) -> (zero : Term (S d) n) ->
-        (j1 : BindName) -> (one : Term (S d) n) ->
-        (loc : Loc) ->
-        Elim d n
-CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} =
-  CompH' {ty = DST [< i] ty, p, q, val, r,
-          zero = DST [< j0] zero, one = DST [< j1] one, loc}

lib/Quox/Var.idr

@@ -2,7 +2,6 @@ module Quox.Var
 
 import public Quox.Loc
 import public Quox.Name
-import Quox.OPE
 
 import Data.Nat
 import Data.List
@@ -290,12 +289,3 @@ decEqFromBool i j =
 %transform "Var.decEq" varDecEq = decEqFromBool
 
 public export %inline DecEq (Var n) where decEq = varDecEq
-
-
-export
-Tighten Var where
-  tighten Id       i      = Just i
-  tighten (Drop p) VZ     = Nothing
-  tighten (Drop p) (VS i) = tighten p i
-  tighten (Keep p) VZ     = Just VZ
-  tighten (Keep p) (VS i) = VS <$> tighten p i

lib/Quox/Whnf/Coercion.idr

@@ -14,7 +14,7 @@ coeScoped : {s : Nat} -> DScopeTerm d n -> Dim d -> Dim d -> Loc ->
 coeScoped ty p q loc (S names (N body)) =
   S names $ N $ E $ Coe ty p q body loc
 coeScoped ty p q loc (S names (Y body)) =
-  ST names $ E $ Coe (weakDS s ty) p q body loc
+  SY names $ E $ Coe (weakDS s ty) p q body loc
 where
   weakDS : (by : Nat) -> DScopeTerm d n -> DScopeTerm d (by + n)
   weakDS by (S names (Y body)) = S names $ Y $ weakT by body
@@ -38,11 +38,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     let ctx1 = extendDim i ctx
     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
+    let s0   = CoeY 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)
+        s1   = CoeY i (arg // (BV 0 i.loc ::: shift 2)) (weakD 1 q) (BV 0 i.loc)
                     (s // shift 1) s.loc
-    whnf defs ctx sg $ CoeT i (sub1 res s1) p q body loc
+    whnf defs ctx sg $ CoeY i (sub1 res s1) p q body loc
 
   ||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body loc`
   export covering
@@ -63,13 +63,13 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     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 x.loc) x.loc
+        a' = CoeY i (weakT 2 tfst) p q (BVT 1 x.loc) x.loc
         tsnd' = tsnd.term //
-          (CoeT i (weakT 2 $ tfst // (B VZ tsnd.loc ::: shift 2))
+          (CoeY i (weakT 2 $ tfst // (B VZ tsnd.loc ::: shift 2))
             (weakD 1 p) (B VZ i.loc) (BVT 1 tsnd.loc) y.loc ::: shift 2)
-        b' = CoeT i tsnd' p q (BVT 0 y.loc) y.loc
+        b' = CoeY i tsnd' p q (BVT 0 y.loc) y.loc
     whnf defs ctx sg $ CasePair qty (Ann val (ty // one p) val.loc) ret
-      (ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc
+      (SY body.names $ body.term // (a' ::: b' ::: shift 2)) loc
 
   ||| reduce a pair projection `Fst (Coe ty p q val) loc`
   export covering
@@ -85,7 +85,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
     (tfst, _) <- tycaseSig defs ctx1 ty
     whnf defs ctx sg $
-      Coe (ST [< i] tfst) p q
+      Coe (SY [< 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`
@@ -103,8 +103,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     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 (SY [< i] $ sub1 tsnd $
-            Coe (ST [< !(fresh i)] $ tfst // (BV 0 i.loc ::: shift 2))
+            Coe (SY [< !(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
@@ -142,9 +142,9 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
     ta <- tycaseBOX defs ctx1 ty
     let xloc = body.name.loc
-    let a' = CoeT i (weakT 1 ta) p q (BVT 0 xloc) xloc
+    let a' = CoeY i (weakT 1 ta) p q (BVT 0 xloc) xloc
     whnf defs ctx sg $ CaseBox qty (Ann val (ty // one p) val.loc) ret
-      (ST body.names $ body.term // (a' ::: shift 1)) loc
+      (SY body.names $ body.term // (a' ::: shift 1)) loc
 
 
 -- new params block to call the above functions at different `n`
@@ -195,12 +195,12 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       --     ∷ ((x : A) × B)‹q/𝑖›
       Sig tfst tsnd tyLoc => do
         let Pair fst snd sLoc = s
-            fst' = CoeT i tfst p q fst fst.loc
+            fst' = CoeY i tfst p q fst fst.loc
             fstInSnd =
-              CoeT !(fresh i)
+              CoeY !(fresh i)
                    (tfst // (BV 0 loc ::: shift 2))
                    (weakD 1 p) (BV 0 loc) (dweakT 1 fst) fst.loc
-            snd' = CoeT i (sub1 tsnd fstInSnd) p q snd snd.loc
+            snd' = CoeY i (sub1 tsnd fstInSnd) p q snd snd.loc
         whnf defs ctx sg $
           Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc
 

lib/Quox/Whnf/Main.idr

@@ -206,25 +206,18 @@ CanWhnf Elim Interface.isRedexE where
         Element a anf <- whnf defs ctx SZero a
         pure $ Element (Ann s a annLoc) (ne `orNo` snf `orNo` anf)
 
-  whnfNoLog defs ctx sg (Coe sty p q val coeLoc) =
+  whnfNoLog defs ctx sg (Coe sty@(S [< i] ty) p q val coeLoc) =
-    --   𝑖 ∉ fv(A)
+    -- reduction if A‹0/𝑖› = A‹1/𝑖› lives in Equal
-    -- -------------------------------
+    case p `decEqv` q of
-    --   coe (𝑖 ⇒ A) @p @q s ⇝ s ∷ A
+      -- coe (𝑖 ⇒ A) @p @p s ⇝ (s ∷ A‹p/𝑖›)
-    --
+      Yes _   => whnf defs ctx sg $ Ann val (dsub1 sty p) coeLoc
-    -- [fixme] needs a real equality check between A‹0/𝑖› and A‹1/𝑖›
+      No  npq => do
-    case dsqueeze sty {f = Term} of
+        let ty = getTerm ty
-      ([< i], Left ty) =>
+        Element ty tynf <- whnf defs (extendDim i ctx) SZero ty
-        case p `decEqv` q of
+        case nchoose $ canPushCoe sg ty val of
-          -- coe (𝑖 ⇒ A) @p @p s ⇝ (s ∷ A‹p/𝑖›)
+          Left  pc  => pushCoe defs ctx sg i ty p q val coeLoc
-          Yes _   => whnf defs ctx sg $ Ann val (dsub1 sty p) coeLoc
+          Right npc => pure $ Element (Coe (SY [< i] ty) p q val coeLoc)
-          No  npq => do
+                                      (tynf `orNo` npc `orNo` notYesNo npq)
-            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 sg $ Ann val ty coeLoc
 
   whnfNoLog defs ctx sg (Comp ty p q val r zero one compLoc) =
     case p `decEqv` q of

lib/Quox/Whnf/TypeCase.idr

@@ -45,7 +45,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
         arg  = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc
         res' = typeCase1Y e (Arr Zero arg ty loc) KPi [< !narg, !nret]
                  (BVT 0 loc) loc
-        res  = ST [< !narg] $ E $ App (weakE 1 res') (BVT 0 loc) loc
+        res  = SY [< !narg] $ E $ App (weakE 1 res') (BVT 0 loc) loc
     pure (arg, res)
   tycasePi t = throw $ ExpectedPi t.loc ctx.names t
 
@@ -63,7 +63,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
         fst  = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc
         snd' = typeCase1Y e (Arr Zero fst ty loc) KSig [< !nfst, !nsnd]
                  (BVT 0 loc) loc
-        snd  = ST [< !nfst] $ E $ App (weakE 1 snd') (BVT 0 loc) loc
+        snd  = SY [< !nfst] $ E $ App (weakE 1 snd') (BVT 0 loc) loc
     pure (fst, snd)
   tycaseSig t = throw $ ExpectedSig t.loc ctx.names t
 
@@ -93,7 +93,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
         a0    = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc
         a1    = E $ typeCase1Y e ty KEq !names (BVT 3 loc) loc
         a'    = typeCase1Y e (Eq0 ty a0 a1 loc) KEq !names (BVT 2 loc) loc
-        a     = DST [< !(mnb "i" loc)] $ E $ DApp (dweakE 1 a') (B VZ loc) loc
+        a     = SY [< !(mnb "i" loc)] $ E $ DApp (dweakE 1 a') (B VZ loc) loc
         l     = E $ typeCase1Y e a0 KEq !names (BVT 1 loc) loc
         r     = E $ typeCase1Y e a1 KEq !names (BVT 0 loc) loc
     pure (a0, a1, a, l, r)

lib/quox-lib.ipkg

@@ -23,7 +23,6 @@ modules =
   Quox.Loc,
   Quox.Var,
   Quox.Scoped,
-  Quox.OPE,
   Quox.Pretty,
   Quox.Syntax,
   Quox.Syntax.Builtin,
@@ -35,7 +34,6 @@ modules =
   Quox.Syntax.Term,
   Quox.Syntax.Term.TyConKind,
   Quox.Syntax.Term.Base,
-  Quox.Syntax.Term.Tighten,
   Quox.Syntax.Term.Pretty,
   Quox.Syntax.Term.Subst,
   Quox.FreeVars,

quox.bib

@@ -221,6 +221,17 @@
   doi       = {10.4230/LIPIcs.FSCD.2019.31}
 }
 
+@article{xtt2,
+  author  = {Jonathan Sterling and Carlo Angiuli and Daniel Gratzer},
+  title   = {A Cubical Language for Bishop Sets},
+  journal = {Log. Methods Comput. Sci.},
+  volume  = {18},
+  number  = {1},
+  year    = {2022},
+  url     = {https://doi.org/10.46298/lmcs-18(1:43)2022},
+  doi     = {10.46298/LMCS-18(1:43)2022},
+}
+
 @unpublished{cubical-ott,
   author = {James Chapman and Fredrik Nordvall Forsberg and Conor {McBride}},
   title  = {The Box of Delights (Cubical Observational Type Theory)},
@@ -456,6 +467,24 @@
 
 % Misc type stuff {{{1
 
+% not open access. i cry
+@inproceedings{simple-quotient,
+  author       = {Martin Hofmann},
+  editor       = {Mariangiola Dezani{-}Ciancaglini and Gordon D. Plotkin},
+  title        = {A Simple Model for Quotient Types},
+  booktitle    = {Typed Lambda Calculi and Applications,
+                  Second International Conference on Typed Lambda Calculi and
+                  Applications, {TLCA} '95, Edinburgh, UK, April 10-12, 1995,
+                  Proceedings},
+  series       = {Lecture Notes in Computer Science},
+  volume       = {902},
+  pages        = {216--234},
+  publisher    = {Springer},
+  year         = {1995},
+  url          = {https://doi.org/10.1007/BFb0014055},
+  doi          = {10.1007/BFB0014055},
+}
+
 @inproceedings{local,
   author    = {Michael Vollmer and
                Chaitanya Koparkar and

stdlib/list.quox

@@ -144,6 +144,7 @@ def elimω2 : 0.(A B : ★) → 0.(P : (n : ℕ) → Vec n A → Vec n B → ★
         pc x y n xs ys (IH xs ys)
     }
 
+{-
 postulate elimP :
     ω.(π : NzQty) → ω.(ρₙ ρₗ : Qty) →
     0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
@@ -156,6 +157,7 @@ postulate elimP :
   =
   λ π ρₙ ρₗ A P ⇒ uhhhhhhhhhhhhhhhhhhh
 -}
+-}
 
 def elimω2-uneven :
     0.(A B : ★) → 0.(P : (m n : ℕ) → Vec m A → Vec n B → ★) →
@@ -238,6 +240,9 @@ def0 ZipWith = zip-with.Result
 def zip-with-het = zip-with.zip-with-het
 def zip-with-hetω = zip-with.zip-with-hetω
 
+def map : 0.(A B : ★) → ω.(A → B) → (n : ℕ) → Vec n A → Vec n B =
+  λ A B f ⇒ elim A (λ n _ ⇒ Vec n B) 'nil (λ x _ _ ys ⇒ (f x, ys))
+
 #[compile-scheme "(lambda% (n xs) xs)"]
 def up : 0.(A : ★) → (n : ℕ) → Vec n A → Vec¹ n A =
   λ A n ⇒

tests/Tests/FromPTerm.idr

@@ -16,11 +16,14 @@ import Derive.Prelude
 %hide TParser.Failure
 %hide TParser.ExpectedFail
 
+PError  = Parser.Error
+FPError = FromParser.Error
+
 public export
 data Failure =
-    ParseError Parser.Error
+    ParseError   PError
-  | FromParser FromParser.Error
+  | FromParser   FPError
-  | WrongResult String
+  | WrongResult  String
   | ExpectedFail String
 
 %runElab derive "FileError" [Show]
@@ -39,42 +42,33 @@ ToInfo Failure where
 
 parameters {c : Bool} {auto _ : Show b}
            (grm : FileName -> Grammar c a)
-           (fromP : a -> Either FromParser.Error b)
+           (fromP : a -> Either FPError b)
            (inp : String)
-  parameters {default (ltrim inp) label : String}
+  parsesWith : String -> (b -> Bool) -> Test
-    parsesWith : (b -> Bool) -> Test
+  parsesWith label p = test label $ do
-    parsesWith p = test label $ do
+    pres <- mapFst ParseError $ lexParseWith (grm "‹test›") inp
-      pres <- mapFst ParseError $ lexParseWith (grm "‹test›") inp
+    res  <- mapFst FromParser $ fromP pres
-      res  <- mapFst FromParser $ fromP pres
+    unless (p res) $ Left $ WrongResult $ show res
-      unless (p res) $ Left $ WrongResult $ show res
 
-    parses : Test
+  %macro
-    parses = parsesWith $ const True
+  parseMatch : {default (ltrim inp) label : String} -> TTImp -> Elab Test
+  parseMatch {label} pat =
+    parsesWith label <$> check `(\case ~(pat) => True; _ => False)
 
-    %macro
+  parseFails : {default "\{ltrim inp}  # fails" label : String} -> Test
-    parseMatch : TTImp -> Elab Test
+  parseFails {label} = test label $ do
-    parseMatch pat =
+    pres <- mapFst ParseError $ lexParseWith (grm "‹test›") inp
-      parsesWith <$> check `(\case ~(pat) => True; _ => False)
+    either (const $ Right ()) (Left . ExpectedFail . show) $ fromP pres
-
-    parsesAs : Eq b => b -> Test
-    parsesAs exp = parsesWith (== exp)
-
-  parameters {default "\{ltrim inp}  # fails" label : String}
-    parseFails : Test
-    parseFails = test label $ do
-      pres <- mapFst ParseError $ lexParseWith (grm "‹test›") inp
-      either (const $ Right ()) (Left . ExpectedFail . show) $ fromP pres
 
 
-runFromParser : {default empty defs : Definitions} ->
+runFromParser : Definitions -> Eff FromParserPure a -> Either FPError a
-                Eff FromParserPure a -> Either FromParser.Error a
+runFromParser defs = map val . fromParserPure [<] 0 defs initStack
-runFromParser = map val . fromParserPure [<] 0 defs initStack
 
 export
 tests : Test
 tests = "PTerm → Term" :- [
   "dimensions" :-
-  let fromPDim = runFromParser . fromPDimWith [< "𝑖", "𝑗"]
+  let fromPDim = runFromParser empty . fromPDimWith [< "𝑖", "𝑗"]
   in [
     note "dim ctx: [𝑖, 𝑗]",
     parseMatch dim fromPDim "𝑖" `(B (VS VZ) _),
@@ -87,7 +81,7 @@ tests = "PTerm → Term" :- [
   "terms" :-
   let defs = fromList [("f", mkDef GAny (^NAT) (^Zero))]
         -- doesn't have to be well typed yet, just well scoped
-      fromPTerm = runFromParser {defs} .
+      fromPTerm = runFromParser defs .
                   fromPTermWith [< "𝑖", "𝑗"] [< "A", "x", "y", "z"]
   in [
     note "dim ctx: [𝑖, 𝑗]; term ctx: [A, x, y, z]",
@@ -97,7 +91,7 @@ tests = "PTerm → Term" :- [
     parseMatch term fromPTerm "λ w ⇒ w"
       `(Lam (S _ $ Y $ E $ B VZ _) _),
     parseMatch term fromPTerm "λ w ⇒ x"
-      `(Lam (S _ $ N $ E $ B (VS $ VS VZ) _) _),
+      `(Lam (S _ $ Y $ E $ B (VS $ VS $ VS VZ) _) _),
     parseMatch term fromPTerm "λ x ⇒ x"
       `(Lam (S _ $ Y $ E $ B VZ _) _),
     parseMatch term fromPTerm "λ a b ⇒ f a b"