pair stuff

lib/Quox/Context.idr

@@ -86,6 +86,7 @@ getWith : (forall from, to. tm from -> Shift from to -> tm to) ->
 getWith shft = getShiftWith shft SZ
 
 infixl 8 !!
+public export %inline
 (!!) : CanShift tm => Context tm len -> Var len -> tm len
 (!!) = getWith (//)
 
@@ -156,6 +157,10 @@ export %inline
 ftel <*> xtel = runIdentity $ (pure .) <$> ftel `app` xtel
 -- ...but can't write pure without `from,to` being ω, so no idiom brackets ☹
 
+export %inline
+(<$) : (forall n. tm1 n) -> Telescope tm2 from to -> Telescope tm1 from to
+x <$ tel = const x <$> tel
+
 export
 teleLte' : Telescope tm from to -> from `LTE'` to
 teleLte' [<]        = LTERefl

lib/Quox/Equal.idr

@@ -41,21 +41,6 @@ private %inline
 clashE : CanEqual q m => Elim q d n -> Elim q d n -> m a
 clashE e f = throwError $ ClashE !mode e f
 
-export %inline
-compareU' : HasEnv m => Universe -> Universe -> m Bool
-compareU' i j = pure $
-  case !mode of Equal => i == j; Sub => i <= j
-
-export %inline
-compareU : CanEqual q m => Universe -> Universe -> m ()
-compareU k l = unless !(compareU' k l) $
-  throwError $ ClashU !mode k l
-
-export %inline
-compareD : HasErr q m => Dim d -> Dim d -> m ()
-compareD p q = unless (p == q) $
-  throwError $ ClashD p q
-
 
 parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
   mutual
@@ -66,11 +51,11 @@ parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
                   (0 _ : NotRedex defs s) -> (0 _ : NotRedex defs t) ->
                   m ()
 
-      compareN' (TYPE k) (TYPE l) _ _ = compareU k l
+      compareN' (TYPE k) (TYPE l) _ _ = expectModeU !mode k l
       compareN' s@(TYPE _) t _ _ = clashT s t
 
       compareN' (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
-        unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
+        expectEqualQ qty1 qty2
         compare0 arg2 arg1 -- reversed for contravariant domain
         compare0 res1 res2
       compareN' s@(Pi {}) t _ _ = clashT s t
@@ -80,6 +65,17 @@ parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
         local {mode := Equal} $ compare0 body1 body2
       compareN' s@(Lam {}) t _ _ = clashT s t
 
+      compareN' (Sig _ fst1 snd1) (Sig _ fst2 snd2) _ _ = do
+        compare0 fst1 fst2
+        compare0 snd1 snd2
+      compareN' s@(Sig {}) t _ _ = clashT s t
+
+      compareN' (Pair fst1 snd1) (Pair fst2 snd2) _ _ =
+        local {mode := Equal} $ do
+          compare0 fst1 fst2
+          compare0 snd1 snd2
+      compareN' s@(Pair {}) t _ _ = clashT s t
+
       compareN' (Eq _ ty1 l1 r1) (Eq _ ty2 l2 r2) _ _ = do
         compare0 ty1 ty2
         local {mode := Equal} $ do
@@ -88,7 +84,8 @@ parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
       compareN' s@(Eq {}) t _ _ = clashT s t
 
       compareN' (DLam _ body1) (DLam _ body2) _ _ =
-        compare0 body1 body2
+        local {mode := Equal} $ do
+          compare0 body1 body2
       compareN' s@(DLam {}) t _ _ = clashT s t
 
       compareN' (E e) (E f) ne nf = compareN' e f (noOr2 ne) (noOr2 nf)
@@ -117,11 +114,20 @@ parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
           compare0 arg1 arg2
       compareN' e@(_ :@ _) f _ _ = clashE e f
 
+      compareN' (CasePair pi1 pair1 _ ret1 _ _ body1)
+                (CasePair pi2 pair2 _ ret2 _ _ body2) _ _ =
+        local {mode := Equal} $ do
+          expectEqualQ pi1 pi2
+          compare0 pair1 pair2
+          compare0 ret1  ret2
+          compare0 body1 body2
+      compareN' e@(CasePair {}) f _ _ = clashE e f
+
       -- retain the mode unlike above because dimensions can't do
       -- anything that would mess up variance
       compareN' (fun1 :% dim1) (fun2 :% dim2) _ _ = do
         compare0 fun1 fun2
-        compareD dim1 dim2
+        expectEqualD dim1 dim2
       compareN' e@(_ :% _) f _ _ = clashE e f
 
       -- using the same mode for the type allows, e.g.

lib/Quox/Pretty.idr

@@ -80,6 +80,11 @@ export %inline
 bracks : Doc HL -> Doc HL
 bracks = delims "[" "]"
 
+||| includes spaces inside the braces
+export %inline
+braces : Doc HL -> Doc HL
+braces doc = hl Delim "{" <++> doc <++> hl Delim "}"
+
 export %inline
 parensIf : Bool -> Doc HL -> Doc HL
 parensIf True  = parens

lib/Quox/Syntax/Dim.idr

@@ -19,10 +19,11 @@ data DimConst = Zero | One
 
 %runElab derive "DimConst" [Generic, Meta, Eq, Ord, DecEq, Show]
 
+||| `ends l r e` returns `l` if `e` is `Zero`, or `r` if it is `One`.
 public export
-pick : a -> a -> DimConst -> a
+ends : a -> a -> DimConst -> a
-pick x y Zero = x
+ends l r Zero = l
-pick x y One  = y
+ends l r One  = r
 
 
 public export
@@ -55,6 +56,16 @@ PrettyHL (Dim n) where
   prettyM (B i) = prettyVar DVar DVarErr (!ask).dnames i
 
 
+||| `endsOr l r x e` returns:
+||| - `l` if `p` is `K Zero`;
+||| - `r` if `p` is `K One`;
+||| - `x` otherwise.
+public export
+endsOr : a -> a -> Lazy a -> Dim n -> a
+endsOr l r x (K e) = ends l r e
+endsOr l r x (B _) = x
+
+
 public export %inline
 toConst : Dim 0 -> DimConst
 toConst (K e) = e

lib/Quox/Syntax/Qty.idr

@@ -13,10 +13,15 @@ commas []      = []
 commas [x]     = [x]
 commas (x::xs) = (x <+> hl Delim ",") :: commas xs
 
+private %inline
+blobD : Pretty.HasEnv m => m (Doc HL)
+blobD = hlF Delim $ ifUnicode "·" "@"
+
 export %inline
 prettyQtyBinds : Pretty.HasEnv m => PrettyHL q => List q -> m (Doc HL)
-prettyQtyBinds =
+prettyQtyBinds [] = pure ""
-  map ((hl Delim "@" <++>) . align . sep . commas) . traverse pretty0M
+prettyQtyBinds qtys =
+  pure $ !blobD <++> align (sep $ commas !(traverse pretty0M qtys))
 
 
 public export

lib/Quox/Syntax/Subst.idr

@@ -7,6 +7,7 @@ import Quox.Pretty
 
 import Data.Nat
 import Data.List
+import Data.Vect
 
 %default total
 
@@ -101,9 +102,14 @@ drop1 (Shift by) = Shift $ ssDown by
 drop1 (t ::: th) = th
 
 
+public export
+fromVect : Vect s (f n) -> Subst f (s + n) n
+fromVect []        = id
+fromVect (x :: xs) = x ::: fromVect xs
+
 public export %inline
 one : f n -> Subst f (S n) n
-one x = x ::: id
+one x = fromVect [x]
 
 
 ||| `prettySubst pr names bnd op cl th` pretty-prints the substitution `th`,

lib/Quox/Syntax/Term/Base.idr

@@ -52,6 +52,12 @@ mutual
     ||| function term
     Lam : (x : Name) -> (body : ScopeTerm q d n) -> Term q d n
 
+    ||| pair type
+    Sig : (x : Name) -> (fst : Term q d n) -> (snd : ScopeTerm q d n) ->
+          Term q d n
+    ||| pair value
+    Pair : (fst, snd : Term q d n) -> Term q d n
+
     ||| equality type
     Eq : (i : Name) -> (ty : DScopeTerm q d n) -> (l, r : Term q d n) ->
          Term q d n
@@ -79,6 +85,15 @@ mutual
     ||| term application
     (:@) : (fun : Elim q d n) -> (arg : Term q d n) -> Elim q d n
 
+    ||| pair destruction
+    |||
+    ||| `CasePair 𝜋 𝑒 𝑟 𝐴 𝑥 𝑦 𝑡` is
+    ||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟 ⇒ 𝐴 𝐨𝐟 { (𝑥, 𝑦) ⇒ 𝑡 }`
+    CasePair : (qty : q) -> (pair : Elim q d n) ->
+               (r : Name) -> (ret  : ScopeTerm q d n) ->
+               (x, y : Name) -> (body : ScopeTermN 2 q d n) ->
+               Elim q d n
+
     ||| dim application
     (:%) : (fun : Elim q d n) -> (arg : Dim d) -> Elim q d n
 

lib/Quox/Syntax/Term/Pretty.idr

@@ -11,18 +11,25 @@ import Data.Vect
 
 
 private %inline
-arrowD, lamD, eqndD, dlamD, annD : Pretty.HasEnv m => m (Doc HL)
+arrowD, timesD, darrowD, lamD, eqndD, dlamD, annD :
-arrowD = hlF Syntax $ ifUnicode "→"  "->"
+  Pretty.HasEnv m => m (Doc HL)
-lamD   = hlF Syntax $ ifUnicode "λ"  "fun"
+arrowD  = hlF Syntax $ ifUnicode "→"  "->"
-eqndD  = hlF Syntax $ ifUnicode "≡"  "=="
+timesD  = hlF Syntax $ ifUnicode "×"  "**"
-dlamD  = hlF Syntax $ ifUnicode "λᴰ" "dfun"
+darrowD = hlF Syntax $ ifUnicode "⇒"  "=>"
-annD   = hlF Syntax $ ifUnicode "∷"  "::"
+lamD    = hlF Syntax $ ifUnicode "λ"  "fun"
+eqndD   = hlF Syntax $ ifUnicode "≡"  "=="
+dlamD   = hlF Syntax $ ifUnicode "λᴰ" "dfun"
+annD    = hlF Syntax $ ifUnicode "∷"  "::"
 
 private %inline
-typeD, eqD, colonD : Doc HL
+typeD, eqD, colonD, commaD, caseD, returnD, ofD : Doc HL
-typeD  = hl Syntax "Type"
+typeD   = hl Syntax "Type"
-eqD    = hl Syntax "Eq"
+eqD     = hl Syntax "Eq"
-colonD = hl Syntax ":"
+colonD  = hl Syntax ":"
+commaD  = hl Syntax ","
+caseD   = hl Syntax "case"
+ofD     = hl Syntax "of"
+returnD = hl Syntax "return"
 
 mutual
   export covering
@@ -30,12 +37,15 @@ mutual
     prettyM (TYPE l) =
       parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
     prettyM (Pi qty x s t) =
-      parensIfM Outer $ hang 2 $
+      prettyBindType [qty] x s !arrowD t
-        !(prettyBinder [qty] x s) <++> !arrowD
-          <//> !(under T x $ prettyM t)
     prettyM (Lam x t) =
       let GotLams {names, body, _} = getLams' [x] t.term Refl in
       prettyLams T (toList names) body
+    prettyM (Sig x s t) =
+      prettyBindType [] x s !timesD t
+    prettyM (Pair s t) =
+      let GotPairs {init, last, _} = getPairs t in
+      prettyTuple $ s :: init ++ [last]
     prettyM (Eq _ (DUnused ty) l r) =
       parensIfM Eq !(withPrec InEq $ pure $
         sep [!(prettyM l) <++> !eqndD, !(prettyM r) <++> colonD, !(prettyM ty)])
@@ -43,7 +53,7 @@ mutual
       parensIfM App $
         eqD <++>
         sep [bracks !(withPrec Outer $ pure $ hang 2 $
-               sep [hl DVar !(prettyM i) <++> !arrowD,
+               sep [hl DVar !(prettyM i) <++> !darrowD,
                     !(under D i $ prettyM ty)]),
              !(withPrec Arg $ prettyM l),
              !(withPrec Arg $ prettyM r)]
@@ -67,6 +77,10 @@ mutual
     prettyM (e :@ s) =
       let GotArgs {fun, args, _} = getArgs' e [s] in
       prettyApps fun args
+    prettyM (CasePair pi p r ret x y body) = do
+      pat <- (parens . separate commaD . map (hl TVar)) <$>
+             traverse prettyM [x, y]
+      prettyCase pi p r ret [([x, y], pat, body)]
     prettyM (e :% d) =
       let GotDArgs {fun, args, _} = getDArgs' e [d] in
       prettyApps fun args
@@ -90,6 +104,15 @@ mutual
                  TSubst q d from to -> m (Doc HL)
   prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
 
+  export covering
+  prettyBindType : Pretty.HasEnv m => PrettyHL q =>
+                   List q -> Name -> Term q d n -> Doc HL ->
+                   ScopeTerm q d n -> m (Doc HL)
+  prettyBindType qtys x s arr t =
+      parensIfM Outer $ hang 2 $
+        !(prettyBinder qtys x s) <++> arr
+          <//> !(under T x $ prettyM t)
+
   export covering
   prettyBinder : Pretty.HasEnv m => PrettyHL q =>
                  List q -> Name -> Term q d n -> m (Doc HL)
@@ -104,7 +127,7 @@ mutual
                BinderSort -> List Name -> Term q _ _ -> m (Doc HL)
   prettyLams sort names body = do
     lam    <- case sort of T => lamD; D => dlamD
-    header <- sequence $ [hl TVar <$> prettyM x | x <- names] ++ [arrowD]
+    header <- sequence $ [hl TVar <$> prettyM x | x <- names] ++ [darrowD]
     body   <- unders sort names $ prettyM body
     parensIfM Outer $ sep (lam :: header) <//> body
 
@@ -114,3 +137,30 @@ mutual
   prettyApps fun args =
     parensIfM App =<< withPrec Arg
       [|prettyM fun <//> (align . sep <$> traverse prettyM args)|]
+
+  export covering
+  prettyTuple : Pretty.HasEnv m => PrettyHL a => List a -> m (Doc HL)
+  prettyTuple = map (parens . align . separate commaD) . traverse prettyM
+
+  export covering
+  prettyArm : Pretty.HasEnv m => PrettyHL a =>
+              (List Name, Doc HL, a) -> m (Doc HL)
+  prettyArm (xs, pat, body) =
+    pure $ hang 2 $ sep
+      [hsep [pat, !darrowD],
+       !(withPrec Outer $ unders T xs $ prettyM body)]
+
+  export covering
+  prettyArms : Pretty.HasEnv m => PrettyHL a =>
+               List (List Name, Doc HL, a) -> m (Doc HL)
+  prettyArms = map (braces . align . sep) . traverse prettyArm
+
+  export covering
+  prettyCase : Pretty.HasEnv m =>
+               PrettyHL q => PrettyHL a => PrettyHL b => PrettyHL c =>
+               q -> a -> Name -> b -> List (List Name, Doc HL, c) -> m (Doc HL)
+  prettyCase pi elim r ret arms =
+    pure $ align $ sep $
+      [hsep [caseD,   !(prettyM elim), !(prettyQtyBinds [pi])],
+       hsep [returnD, !(prettyM r), !darrowD, !(under T r $ prettyM ret)],
+       hsep [ofD,     !(prettyArms arms)]]

lib/Quox/Syntax/Term/Reduce.idr

@@ -3,6 +3,7 @@ module Quox.Syntax.Term.Reduce
 import Quox.No
 import Quox.Syntax.Term.Base
 import Quox.Syntax.Term.Subst
+import Data.Vect
 import Data.Maybe
 
 %default total
@@ -66,6 +67,10 @@ mutual
       ncloT $ Pi qty x (subs a th ph) (subs body th ph)
     pushSubstsWith th ph (Lam x body) =
       ncloT $ Lam x $ subs body th ph
+    pushSubstsWith th ph (Sig x a b) =
+      ncloT $ Sig x (subs a th ph) (subs b th ph)
+    pushSubstsWith th ph (Pair s t) =
+      ncloT $ Pair (subs s th ph) (subs t th ph)
     pushSubstsWith th ph (Eq i ty l r) =
       ncloT $ Eq i (subs ty th ph) (subs l th ph) (subs r th ph)
     pushSubstsWith th ph (DLam i body) =
@@ -96,6 +101,8 @@ mutual
         Right no  => Element res no
     pushSubstsWith th ph (f :@ s) =
       ncloE $ subs f th ph :@ subs s th ph
+    pushSubstsWith th ph (CasePair pi p x r y z b) =
+      ncloE $ CasePair pi (subs p th ph) x (subs r th ph) y z (subs b th ph)
     pushSubstsWith th ph (f :% d) =
       ncloE $ subs f th ph :% (d // th)
     pushSubstsWith th ph (s :# a) =
@@ -141,6 +148,11 @@ isDLamHead : Elim {} -> Bool
 isDLamHead (DLam {} :# Eq {}) = True
 isDLamHead _                  = False
 
+public export %inline
+isPairHead : Elim {} -> Bool
+isPairHead (Pair {} :# Sig {}) = True
+isPairHead _                   = False
+
 public export %inline
 isE : Term {} -> Bool
 isE (E _) = True
@@ -156,13 +168,14 @@ parameters (g : Lookup q d n)
     namespace Elim
       public export
       isRedex : Elim q d n -> Bool
-      isRedex (F x)      = isJust $ g x
+      isRedex (F x)                = isJust $ g x
-      isRedex (B _)      = False
+      isRedex (B _)                = False
-      isRedex (f :@ _)   = isRedex f || isLamHead f
+      isRedex (f :@ _)             = isRedex f || isLamHead f
-      isRedex (f :% _)   = isRedex f || isDLamHead f
+      isRedex (CasePair {pair, _}) = isRedex pair || isPairHead pair
-      isRedex (t :# a)   = isE t || isRedex t || isRedex a
+      isRedex (f :% _)             = isRedex f || isDLamHead f
-      isRedex (CloE  {}) = True
+      isRedex (t :# a)             = isE t || isRedex t || isRedex a
-      isRedex (DCloE {}) = True
+      isRedex (CloE  {})           = True
+      isRedex (DCloE {})           = True
 
     namespace Term
       public export
@@ -211,24 +224,36 @@ parameters (g : Lookup q d n)
             whnf $ sub1 body s :# sub1 res s
           Right nlh => Element (f :@ s) $ fnf `orNo` nlh
 
+      whnf (CasePair pi pair r ret x y body) =
+        let Element pair pairnf = whnf pair in
+        case nchoose $ isPairHead pair of
+          Left _ =>
+            let Pair {fst, snd} :# Sig {fst = tfst, snd = tsnd, _} = pair
+                fst = fst :# tfst
+                snd = snd :# sub1 tsnd fst
+            in
+            whnf $ subN body [fst, snd] :# sub1 ret pair
+          Right np =>
+            Element (CasePair pi pair r ret x y body) $ pairnf `orNo` np
+
       whnf (f :% p) =
         let Element f fnf = whnf f in
         case nchoose $ isDLamHead f of
           Left _ =>
             let DLam {body, _} :# Eq {ty, l, r, _} = f
-                body = case p of K e => pick l r e; _ => dsub1 body p
+                body = endsOr l r (dsub1 body p) p
             in
             whnf $ body :# dsub1 ty p
           Right ndlh =>
             Element (f :% p) $ fnf `orNo` ndlh
 
       whnf (s :# a) =
-        let Element s snf = whnf s
+        let Element s snf = whnf s in
-            Element a anf = whnf a
-        in
         case nchoose $ isE s of
           Left  _  => let E e = s in Element e $ noOr2 snf
-          Right ne => Element (s :# a) $ ne `orNo` snf `orNo` anf
+          Right ne =>
+            let Element a anf = whnf a in
+            Element (s :# a) $ ne `orNo` snf `orNo` anf
 
       whnf (CloE  el th) = whnf $ pushSubstsWith' id th el
       whnf (DCloE el th) = whnf $ pushSubstsWith' th id el
@@ -236,11 +261,13 @@ parameters (g : Lookup q d n)
     namespace Term
       export covering
       whnf : Term q d n -> NonRedexTerm q d n g
-      whnf (TYPE l)           = Element (TYPE l)           Ah
+      whnf t@(TYPE {}) = Element t Ah
-      whnf (Pi qty x arg res) = Element (Pi qty x arg res) Ah
+      whnf t@(Pi   {}) = Element t Ah
-      whnf (Lam x body)       = Element (Lam x body)       Ah
+      whnf t@(Lam  {}) = Element t Ah
-      whnf (Eq i ty l r)      = Element (Eq i ty l r)      Ah
+      whnf t@(Sig  {}) = Element t Ah
-      whnf (DLam i body)      = Element (DLam i body)      Ah
+      whnf t@(Pair {}) = Element t Ah
+      whnf t@(Eq   {}) = Element t Ah
+      whnf t@(DLam {}) = Element t Ah
 
       whnf (E e) =
         let Element e enf = whnf e in

lib/Quox/Syntax/Term/Split.idr

@@ -29,6 +29,16 @@ public export
 NotDLam = No . isDLam
 
 
+public export %inline
+isPair : Term {} -> Bool
+isPair (Pair {}) = True
+isPair _         = False
+
+public export
+0 NotPair : Pred $ Term {}
+NotPair = No . isPair
+
+
 public export %inline
 isApp : Elim {} -> Bool
 isApp (_ :@ _) = True
@@ -159,8 +169,8 @@ record GetDLams q d n where
 
 export
 getDLams' : forall lams, rest.
-           Vect lams Name -> Term q rest n -> (0 eq : lams + d = rest) ->
+            Vect lams Name -> Term q rest n -> (0 eq : lams + d = rest) ->
-           GetDLams q d n
+            GetDLams q d n
 getDLams' is s Refl = case nchoose $ isDLam s of
   Left  y => let DLam i body = s in
              getDLams' (i :: is) (assert_smaller s body.term) Refl
@@ -169,3 +179,19 @@ getDLams' is s Refl = case nchoose $ isDLam s of
 export %inline
 getDLams : Term q d n -> GetDLams q d n
 getDLams s = getDLams' [] s Refl
+
+
+public export
+record GetPairs q d n where
+  constructor GotPairs
+  init : List $ Term q d n
+  last : Term q d n
+  notPair : NotPair last
+
+export
+getPairs : Term q d n -> GetPairs q d n
+getPairs t = case nchoose $ isPair t of
+  Left y =>
+    let Pair s t = t; GotPairs ts t np = getPairs t in
+    GotPairs (s :: ts) t np
+  Right n => GotPairs [] t n

lib/Quox/Syntax/Term/Subst.idr

@@ -1,6 +1,7 @@
 module Quox.Syntax.Term.Subst
 
 import Quox.Syntax.Term.Base
+import Data.Vect
 
 %default total
 
@@ -195,15 +196,25 @@ namespace DScopeTermN
   (DUsed   body).term = body
   (DUnused body).term = body /// shift s
 
+
+export %inline
+subN : ScopeTermN s q d n -> Vect s (Elim q d n) -> Term q d n
+subN (TUsed   body) es = body // fromVect es
+subN (TUnused body) _  = body
+
 export %inline
 sub1 : ScopeTerm q d n -> Elim q d n -> Term q d n
-sub1 (TUsed   body) e = body // one e
+sub1 t e = subN t [e]
-sub1 (TUnused body) e = body
+
+export %inline
+dsubN : DScopeTermN s q d n -> Vect s (Dim d) -> Term q d n
+dsubN (DUsed   body) ps = body /// fromVect ps
+dsubN (DUnused body) _  = body
 
 export %inline
 dsub1 : DScopeTerm q d n -> Dim d -> Term q d n
-dsub1 (DUsed   body) p = body /// one p
+dsub1 t p = dsubN t [p]
-dsub1 (DUnused body) p = body
+
 
 public export %inline
 (.zero) : DScopeTerm q d n -> Term q d n

lib/Quox/Typechecker.idr

@@ -5,6 +5,7 @@ import public Quox.Typing
 import public Quox.Equal
 import public Control.Monad.Either
 import Decidable.Decidable
+import Data.SnocVect
 
 %default total
 
@@ -33,6 +34,14 @@ expectPi ty =
     Element (Pi qty _ arg res) _ => pure (qty, arg, res)
     _ => throwError $ ExpectedPi ty
 
+private covering %inline
+expectSig : CanTC' q _ m => Term q d n ->
+            m (Term q d n, ScopeTerm q d n)
+expectSig ty =
+  case whnf !ask ty of
+    Element (Sig _ arg res) _ => pure (arg, res)
+    _ => throwError $ ExpectedSig ty
+
 private covering %inline
 expectEq : CanTC' q _ m => Term q d n ->
            m (DScopeTerm q d n, Term q d n, Term q d n)
@@ -41,16 +50,17 @@ expectEq ty =
     Element (Eq _ ty l r) _ => pure (ty, l, r)
     _ => throwError $ ExpectedEq ty
 
-private %inline
-expectEqualQ : HasErr q m => Eq q =>
-               (expect, actual : q) -> m ()
-expectEqualQ pi rh =
-  unless (pi == rh) $ throwError $ ClashQ pi rh
 
+private
+popQs : HasErr q m => IsQty q =>
+        SnocVect s q -> QOutput q (s + n) -> m (QOutput q n)
+popQs [<]         qctx         = pure qctx
+popQs (pis :< pi) (qctx :< rh) = do expectCompatQ rh pi; popQs pis qctx
 
 private %inline
-popQ : HasErr q m => Eq q => q -> QOutput q (S n) -> m (QOutput q n)
+popQ : HasErr q m => IsQty q => q -> QOutput q (S n) -> m (QOutput q n)
-popQ pi (qctx :< rh) = expectEqualQ pi rh $> qctx
+popQ pi = popQs [< pi]
+
 
 
 private %inline
@@ -64,8 +74,8 @@ weakI = {type $= weakT, qout $= (:< zero)}
 
 private
 lookupBound : IsQty q => q -> Var n -> TyContext q d n -> InferResult q d n
-lookupBound pi VZ ctx@(MkTyContext {tctx = _ :< ty, _}) =
+lookupBound pi VZ (MkTyContext {tctx = tctx :< ty, _}) =
-  InfRes {type = weakT ty, qout = zeroFor (tail ctx) :< pi}
+  InfRes {type = weakT ty, qout = (zero <$ tctx) :< pi}
 lookupBound pi (VS i) ctx =
   weakI $ lookupBound pi i (tail ctx)
 
@@ -105,6 +115,11 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     let Element subj nc = pushSubsts subj in
     check' ctx sg subj nc ty
 
+  ||| `check0 ctx subj ty` checks a term in a zero context.
+  export covering %inline
+  check0 : TyContext q d n -> Term q d n -> Term q d n -> m (CheckResult q n)
+  check0 ctx = check (zeroed ctx) szero
+
   ||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`,
   ||| and returns its type and the bound variables it used.
   export covering %inline
@@ -120,47 +135,85 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
            m (CheckResult q n)
 
   check' ctx sg (TYPE l) _ ty = do
+    -- if ℓ < ℓ' then Ψ | Γ ⊢ Type ℓ · 0 ⇐ Type ℓ' ⊳ 𝟎
     l' <- expectTYPE ty
     expectEqualQ zero sg.fst
     unless (l < l') $ throwError $ BadUniverse l l'
     pure $ zeroFor ctx
 
-  check' ctx sg (Pi qty x arg res) _ ty = do
+  check' ctx sg (Pi qty _ arg res) _ ty = do
     l <- expectTYPE ty
     expectEqualQ zero sg.fst
-    ignore $ check ctx szero arg (TYPE l)
+    -- if Ψ | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎
+    ignore $ check0 ctx arg (TYPE l)
+    -- if Ψ | Γ, x · 0 : A ⊢ B · 0 ⇐ Type ℓ ⊳ 𝟎
     case res of
-      TUsed   res => ignore $ check (extendTy arg zero ctx) szero res (TYPE l)
+      TUsed   res => ignore $ check0 (extendTy arg zero ctx) res (TYPE l)
-      TUnused res => ignore $ check ctx szero res (TYPE l)
+      TUnused res => ignore $ check0 ctx res (TYPE l)
+    -- then Ψ | Γ ⊢ (x : A) → B · 0 ⇐ Type ℓ ⊳ 𝟎
     pure $ zeroFor ctx
 
-  check' ctx sg (Lam x body) _ ty = do
+  check' ctx sg (Lam _ body) _ ty = do
     (qty, arg, res) <- expectPi ty
+    -- if Ψ | Γ, x · πσ : A ⊢ t · σ ⇐ B ⊳ Σ, x · σπ
     qout <- check (extendTy arg (sg.fst * qty) ctx) sg body.term res.term
-    popQ qty qout
+    -- then Ψ | Γ ⊢ λx. t · σ ⇐ (x · π : A) → B ⊳ Σ
+    popQ (sg.fst * qty) qout
+
+  check' ctx sg (Sig _ fst snd) _ ty = do
+    l <- expectTYPE ty
+    expectEqualQ zero sg.fst
+    -- if Ψ | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎
+    ignore $ check0 ctx fst (TYPE l)
+    -- if Ψ | Γ, x · 0 : A ⊢ B · 0 ⇐ Type ℓ ⊳ 𝟎
+    case snd of
+      TUsed   snd => ignore $ check0 (extendTy fst zero ctx) snd (TYPE l)
+      TUnused snd => ignore $ check0 ctx snd (TYPE l)
+    -- then Ψ | Γ ⊢ (x : A) × B · 0 ⇐ Type ℓ ⊳ 𝟎
+    pure $ zeroFor ctx
+
+  check' ctx sg (Pair fst snd) _ ty = do
+    (tfst, tsnd) <- expectSig ty
+    -- if Ψ | Γ ⊢ s · σ ⇐ A ⊳ Σ₁
+    qfst <- check ctx sg fst tfst
+    let tsnd = sub1 tsnd (fst :# tfst)
+    -- if Ψ | Γ ⊢ t · σ ⇐ B[s] ⊳ Σ₂
+    qsnd <- check ctx sg snd tsnd
+    -- then Ψ | Γ ⊢ (s, t) · σ ⇐ (x : A) × B ⊳ Σ₁ + Σ₂
+    pure $ qfst + qsnd
 
   check' ctx sg (Eq i t l r) _ ty = do
     u <- expectTYPE ty
     expectEqualQ zero sg.fst
+    -- if Ψ, i | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎
     case t of
-      DUsed   t => ignore $ check (extendDim ctx) sg t (TYPE u)
+      DUsed   t => ignore $ check0 (extendDim ctx) t (TYPE u)
-      DUnused t => ignore $ check ctx sg t (TYPE u)
+      DUnused t => ignore $ check0 ctx t (TYPE u)
-    ignore $ check ctx sg t.zero l
+    -- if Ψ | Γ ⊢ l · 0 ⇐ A‹0› ⊳ 𝟎
-    ignore $ check ctx sg t.one  r
+    ignore $ check0 ctx t.zero l
+    -- if Ψ | Γ ⊢ r · 0 ⇐ A‹1› ⊳ 𝟎
+    ignore $ check0 ctx t.one  r
+    -- then Ψ | Γ ⊢ Eq [i ⇒ A] l r ⇐ Type ℓ ⊳ 𝟎
     pure $ zeroFor ctx
 
   check' ctx sg (DLam i body) _ ty = do
     (ty, l, r) <- expectEq ty
+    -- if Ψ, i | Γ ⊢ t · σ ⇐ A ⊳ Σ
     qout <- check (extendDim ctx) sg body.term ty.term
     let eqs = makeDimEq ctx.dctx
+    -- if Ψ ⊢ t‹0› = l
     equal !ask eqs body.zero l
+    -- if Ψ ⊢ t‹1› = r
     equal !ask eqs body.one  r
+    -- then Ψ | Γ ⊢ (λᴰi ⇒ t) · σ ⇐ Eq [i ⇒ A] l r ⊳ Σ
     pure qout
 
   check' ctx sg (E e) _ ty = do
+    -- if Ψ | Γ ⊢ e · σ ⇒ A' ⊳ Σ
     infres <- infer ctx sg e
-    ignore $ check ctx szero ty (TYPE UAny)
+    -- if Ψ ⊢ A' <: A
     sub !ask (makeDimEq ctx.dctx) infres.type ty
+    -- then Ψ | Γ ⊢ e · σ ⇐ A ⊳ Σ
     pure infres.qout
 
   export covering
@@ -169,28 +222,63 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
            m (InferResult q d n)
 
   infer' ctx sg (F x) _ = do
+    -- if x · π : A {≔ s} in global context
     g <- lookupFree x
-    when (isYes $ isZero g) $ expectEqualQ sg.fst zero
+    -- if σ ≤ π
+    expectCompatQ sg.fst g.qty
+    -- then Ψ | Γ ⊢ x ⇒ A ⊳ 𝟎
     pure $ InfRes {type = g.type.get, qout = zeroFor ctx}
 
   infer' ctx sg (B i) _ =
+    -- if x : A ∈ Γ
+    -- then Ψ | Γ ⊢ x · σ ⇒ A ⊳ (𝟎, σ · x, 𝟎)
     pure $ lookupBound sg.fst i ctx
 
   infer' ctx sg (fun :@ arg) _ = do
+    -- if Ψ | Γ ⊢ f · σ ⇒ (x · π : A) → B ⊳ Σ₁
     funres <- infer ctx sg fun
     (qty, argty, res) <- expectPi funres.type
+    -- if Ψ | Γ ⊢ s · σ∧π ⇐ A ⊳ Σ₂
+    --   (0∧π = σ∧0 = 0; σ∧π = σ otherwise)
     argout <- check ctx (subjMult sg qty) arg argty
+    -- then Ψ | Γ ⊢ f s · σ ⇒ B[s] ⊳ Σ₁ + Σ₂
     pure $ InfRes {
       type = sub1 res $ arg :# argty,
       qout = funres.qout + argout
     }
 
+  infer' ctx sg (CasePair pi pair _ ret _ _ body) _ = do
+    -- if 1 ≤ π
+    expectCompatQ one pi
+    -- if Ψ | Γ ⊢ pair · 1 ⇒ (x : A) × B ⊳ Σ₁
+    pairres <- infer ctx sone pair
+    ignore $ check0 (extendTy pairres.type zero ctx) ret.term (TYPE UAny)
+    (tfst, tsnd) <- expectSig pairres.type
+    -- if Ψ | Γ, x · π : A, y · π : B ⊢ σ body ⇐ ret[(x, y)]
+    --      ⊳ Σ₂, x · π₁, y · π₂
+    -- if π₁, π₂ ≤ π
+    let bodyctx = extendTyN [< (tfst, pi), (tsnd.term, pi)] ctx
+        retarg  = Pair (BVT 0) (BVT 1) :# (pairres.type // fromNat 2)
+        bodyty  = ret.term // (retarg ::: shift 2)
+    bodyout <- check bodyctx sg body.term bodyty >>= popQs [< pi, pi]
+    -- then Ψ | Γ ⊢ σ case ⋯ ⇒ ret[pair] ⊳ πΣ₁ + Σ₂
+    pure $ InfRes {
+      type = sub1 ret pair,
+      qout = pi * pairres.qout + bodyout
+    }
+
+
   infer' ctx sg (fun :% dim) _ = do
+    -- if Ψ | Γ ⊢ f · σ ⇒ Eq [i ⇒ A] l r ⊳ Σ
     InfRes {type, qout} <- infer ctx sg fun
     (ty, _, _) <- expectEq type
+    -- then Ψ | Γ ⊢ f p · σ ⇒ A‹p› ⊳ Σ
     pure $ InfRes {type = dsub1 ty dim, qout}
 
   infer' ctx sg (term :# type) _ = do
-    ignore $ check ctx szero type (TYPE UAny)
+    -- if Ψ | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎
+    ignore $ check0 ctx type (TYPE UAny)
+    -- if Ψ | Γ ⊢ s · σ ⇐ A ⊳ Σ
     qout <- check ctx sg term type
+    -- then Ψ | Γ ⊢ (s ∷ A) · σ ⇒ A ⊳ Σ
     pure $ InfRes {type, qout}

lib/Quox/Typing.idr

@@ -52,11 +52,20 @@ namespace TContext
   pushD : TContext q d n -> TContext q (S d) n
   pushD tel = map (/// shift 1) tel
 
+  export
+  zeroed : IsQty q => TyContext q d n -> TyContext q d n
+  zeroed = {qctx $= map (const zero)}
+
 
 namespace TyContext
+  export
+  extendTyN : Telescope (\n => (Term q d n, q)) from to ->
+              TyContext q d from -> TyContext q d to
+  extendTyN ss = {tctx $= (. map fst ss), qctx $= (. map snd ss)}
+
   export
   extendTy : Term q d n -> q -> TyContext q d n -> TyContext q d (S n)
-  extendTy s rho = {tctx $= (:< s), qctx $= (:< rho)}
+  extendTy s rho = extendTyN [< (s, rho)]
 
   export
   extendDim : TyContext q d n -> TyContext q (S d) n
@@ -83,7 +92,7 @@ namespace QOutput
 
     export
     zeroFor : TyContext q _ n -> QOutput q n
-    zeroFor ctx = const zero <$> ctx.qctx
+    zeroFor ctx = zero <$ ctx.tctx
 
 
 public export
@@ -106,6 +115,7 @@ public export
 data Error q
 = ExpectedTYPE (Term q d n)
 | ExpectedPi   (Term q d n)
+| ExpectedSig  (Term q d n)
 | ExpectedEq   (Term q d n)
 | BadUniverse  Universe Universe
 
@@ -118,3 +128,30 @@ data Error q
 public export
 0 HasErr : Type -> (Type -> Type) -> Type
 HasErr q = MonadError (Error q)
+
+export %inline
+ucmp : EqMode -> Universe -> Universe -> Bool
+ucmp Sub   = (<=)
+ucmp Equal = (==)
+
+
+parameters {auto _ : HasErr q m}
+  export %inline
+  expect : Eq a => (a -> a -> Error q) -> (a -> a -> Bool) -> a -> a -> m ()
+  expect err cmp x y = unless (x `cmp` y) $ throwError $ err x y
+
+  export %inline
+  expectEqualQ : Eq q => q -> q -> m ()
+  expectEqualQ = expect ClashQ (==)
+
+  export %inline
+  expectCompatQ : IsQty q => q -> q -> m ()
+  expectCompatQ = expect ClashQ $ \pi, rh => isYes $ pi `compat` rh
+
+  export %inline
+  expectModeU : EqMode -> Universe -> Universe -> m ()
+  expectModeU mode = expect (ClashU mode) $ ucmp mode
+
+  export %inline
+  expectEqualD : Dim d -> Dim d -> m ()
+  expectEqualD = expect ClashD (==)

tests/TermImpls.idr

@@ -5,20 +5,18 @@ import public Quox.Pretty
 
 
 private
-eqShift : Shift from1 to -> Shift from2 to -> Maybe (from1 = from2)
+eqShiftLen : Shift from1 to -> Shift from2 to -> Maybe (from1 = from2)
-eqShift SZ      SZ      = Just Refl
+eqShiftLen SZ      SZ      = Just Refl
-eqShift (SS by) (SS bz) = eqShift by bz
+eqShiftLen (SS by) (SS bz) = eqShiftLen by bz
-eqShift SZ      (SS by) = Nothing
+eqShiftLen _       _       = Nothing
-eqShift (SS by) SZ      = Nothing
 
 private
-eqSubst : Subst tm1 from1 to -> Subst tm2 from2 to -> Maybe (from1 = from2)
+eqSubstLen : Subst tm1 from1 to -> Subst tm2 from2 to -> Maybe (from1 = from2)
-eqSubst (Shift by) (Shift bz) = eqShift by bz
+eqSubstLen (Shift by) (Shift bz) = eqShiftLen by bz
-eqSubst (_ ::: th) (_ ::: ph) = cong S <$> eqSubst th ph
+eqSubstLen (_ ::: th) (_ ::: ph) = cong S <$> eqSubstLen th ph
-eqSubst (Shift _)  (_ ::: _)  = Nothing
+eqSubstLen _          _          = Nothing
-eqSubst (_ ::: _)  (Shift _)  = Nothing
+  -- maybe from1 = from2 in the last case, but this is for
-  -- maybe from1 = from2 in the last two cases, but this is for
+  -- (==), and the substs aren't equal, so who cares
-  -- (==), and they're not equal, so who cares
 
 mutual
   export covering
@@ -33,6 +31,12 @@ mutual
     Lam _ body1 == Lam _ body2 = body1 == body2
     Lam {} == _ = False
 
+    Sig _ fst1 snd1 == Sig _ fst2 snd2 = fst1 == fst2 && snd1 == snd2
+    Sig {} == _ = False
+
+    Pair fst1 snd1 == Pair fst2 snd2 = fst1 == fst2 && snd1 == snd2
+    Pair {} == _ = False
+
     Eq _ ty1 l1 r1 == Eq _ ty2 l2 r2 =
       ty1 == ty2 && l1 == l2 && r1 == r2
     Eq {} == _ = False
@@ -44,13 +48,13 @@ mutual
     E _ == _ = False
 
     CloT tm1 th1 == CloT tm2 th2 =
-      case eqSubst th1 th2 of
+      case eqSubstLen th1 th2 of
            Just Refl => tm1 == tm2 && th1 == th2
            Nothing   => False
     CloT {} == _ = False
 
     DCloT tm1 th1 == DCloT tm2 th2 =
-      case eqSubst th1 th2 of
+      case eqSubstLen th1 th2 of
            Just Refl => tm1 == tm2 && th1 == th2
            Nothing   => False
     DCloT {} == _ = False
@@ -66,33 +70,37 @@ mutual
     (fun1 :@ arg1) == (fun2 :@ arg2) = fun1 == fun2 && arg1 == arg2
     (_ :@ _) == _ = False
 
-    (tm1 :# ty1) == (tm2 :# ty2) = tm1 == tm2 && ty1 == ty2
+    CasePair q1 p1 _ r1 _ _ b1 == CasePair q2 p2 _ r2 _ _ b2 =
-    (_ :# _) == _ = False
+      q1 == q2 && p1 == p2 && r1 == r2 && b1 == b2
+    CasePair {} == _ = False
 
     (fun1 :% dim1) == (fun2 :% dim2) = fun1 == fun2 && dim1 == dim2
     (_ :% _) == _ = False
 
+    (tm1 :# ty1) == (tm2 :# ty2) = tm1 == tm2 && ty1 == ty2
+    (_ :# _) == _ = False
+
     CloE el1 th1 == CloE el2 th2 =
-      case eqSubst th1 th2 of
+      case eqSubstLen th1 th2 of
            Just Refl => el1 == el2 && th1 == th2
            Nothing   => False
     CloE {} == _ = False
 
     DCloE el1 th1 == DCloE el2 th2 =
-      case eqSubst th1 th2 of
+      case eqSubstLen th1 th2 of
            Just Refl => el1 == el2 && th1 == th2
            Nothing   => False
     DCloE {} == _ = False
 
   export covering
-  Eq q => Eq (ScopeTerm q d n) where
+  Eq q => Eq (ScopeTermN s q d n) where
     TUsed   s == TUsed   t = s == t
     TUnused s == TUnused t = s == t
     TUsed   _ == TUnused _ = False
     TUnused _ == TUsed   _ = False
 
   export covering
-  Eq q => Eq (DScopeTerm q d n) where
+  Eq q => Eq (DScopeTermN s q d n) where
     DUsed   s == DUsed   t = s == t
     DUnused s == DUnused t = s == t
     DUsed   _ == DUnused _ = False

tests/Tests/Equal.idr

@@ -16,6 +16,9 @@ ToInfo (Error Three) where
   toInfo (ExpectedPi t) =
     [("type", "ExpectedPi"),
      ("got", prettyStr True t)]
+  toInfo (ExpectedSig t) =
+    [("type", "ExpectedSig"),
+     ("got", prettyStr True t)]
   toInfo (ExpectedEq t) =
     [("type", "ExpectedEq"),
      ("got", prettyStr True t)]
@@ -139,16 +142,6 @@ tests = "equality & subtyping" :- [
       subT tm1 tm2
   ],
 
-  "eq type" :- [
-    testEq "(★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : ★₁)" $
-      let tm = Eq0 (TYPE 1) (TYPE 0) (TYPE 0) in
-      equalT tm tm,
-    testEq "A ≔ ★₁ ⊢ (★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : A)"
-        {globals = fromList [("A", mkDef zero (TYPE 2) (TYPE 1))]} $
-      equalT (Eq0 (TYPE 1) (TYPE 0) (TYPE 0))
-             (Eq0 (FT "A") (TYPE 0) (TYPE 0))
-  ],
-
   "lambda" :- [
     testEq "λ x ⇒ [x] ≡ λ x ⇒ [x]" $
       equalT (Lam "x" $ TUsed $ BVT 0) (Lam "x" $ TUsed $ BVT 0),
@@ -170,6 +163,18 @@ tests = "equality & subtyping" :- [
              (FT "f")
   ],
 
+  "eq type" :- [
+    testEq "(★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : ★₁)" $
+      let tm = Eq0 (TYPE 1) (TYPE 0) (TYPE 0) in
+      equalT tm tm,
+    testEq "A ≔ ★₁ ⊢ (★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : A)"
+        {globals = fromList [("A", mkDef zero (TYPE 2) (TYPE 1))]} $
+      equalT (Eq0 (TYPE 1) (TYPE 0) (TYPE 0))
+             (Eq0 (FT "A") (TYPE 0) (TYPE 0))
+  ],
+
+  todo "dim lambda",
+
   "term closure" :- [
     note "𝑖, 𝑗 for bound variables pointing outside of the current expr",
     testEq "[𝑖]{} ≡ [𝑖]" $
@@ -266,6 +271,21 @@ tests = "equality & subtyping" :- [
       equalE (F "f" :@ FT "x") (F "x")
   ],
 
+  "dim application" :-
+  let refl : Term q d n -> Term q d n -> Elim q d n
+      refl a x = (DLam "_" $ DUnused x) :# (Eq0 a x x)
+  in
+  [
+    note #""refl [A] x" is an abbreviation for "(λᴰi ⇒ x) ∷ (x ≡ x : A)""#,
+    testEq "refl [A] x ≡ refl [A] x" $
+      equalE (refl (FT "A") (FT "x")) (refl (FT "A") (FT "x")),
+    testEq "p : (a ≡ b : A), q : (a ≡ b : A) ⊢ p ≡ q"
+           {globals =
+              let def = mkAbstract Zero $ Eq0 (FT "A") (FT "a") (FT "b") in
+              fromList [("p", def), ("q", def)]} $
+      equalE (F "p") (F "q")
+  ],
+
   todo "annotation",
 
   todo "elim closure",

tests/quox-tests.ipkg

@@ -4,3 +4,7 @@ depends = base, contrib, elab-util, sop, snocvect, quox-lib, tap
 
 executable = quox-tests
 main = Tests
+modules =
+  TermImpls,
+  Tests.Reduce,
+  Tests.Equal