print non-dependent products (easy mode)

only if the AST uses SN, like with Eq

lib/Quox/Parser/Parser.idr

@@ -224,10 +224,14 @@ mutual
   private covering
   infixEqTerm : Grammar True PTerm
   infixEqTerm = do
-    l <- appTerm
-    rty <- optional [|MkPair (resC "≡" *> term) (resC ":" *> appTerm)|]
+    l <- infixTimesTerm
+    rty <- optional [|MkPair (resC "≡" *> term) (resC ":" *> infixTimesTerm)|]
     pure $ maybe l (\rty => Eq (Nothing, snd rty) l (fst rty)) rty
 
+  private covering
+  infixTimesTerm : Grammar True PTerm
+  infixTimesTerm = foldr1 (Sig Nothing) <$> sepBy1 (resC "×") appTerm
+
   private covering
   appTerm : Grammar True PTerm
   appTerm = resC "★"  *> [|TYPE nat|]

lib/Quox/Pretty.idr

@@ -42,10 +42,12 @@ data HL
 public export
 data PPrec
 = Outer
-| Ann  -- right of "∷"
+| AnnR    -- right of "∷"
 | AnnL    -- left  of "∷"
 | Eq      -- "_ ≡ _ : _"
 | InEq    -- arguments of ≡
+| Times   -- "_ × _"
+| InTimes -- arguments of ×
   -- ...
 | App  -- term/dimension application
 | SApp -- substitution application

lib/Quox/Syntax/Term/Pretty.idr

@@ -61,8 +61,8 @@ prettyBindType : PrettyHL a => PrettyHL b => PrettyHL q =>
                  List q -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
 prettyBindType qtys x s arr t = do
   bind <- prettyBind qtys x s
-  t    <- withPrec Outer $ under T x $ prettyM t
-  parensIfM Outer $ hang 2 $ parens bind <++> arr <%%> t
+  t    <- withPrec AnnR $ under T x $ prettyM t
+  parensIfM AnnR $ hang 2 $ parens bind <++> arr <%%> t
 
 export
 prettyArm : PrettyHL a => Pretty.HasEnv m =>
@@ -151,8 +151,12 @@ parameters (showSubsts : Bool)
     prettyM (Lam (S x t)) =
       let GotLams {names, body, _} = getLams' x t.term Refl in
       prettyLams (Just !lamD) T (toSnocList' names) body
-    prettyM (Sig s (S [< x] t)) =
-      prettyBindType {q} [] x s !timesD t.term
+    prettyM (Sig s (S _ (N t))) = do
+      s <- withPrec InTimes $ prettyM s
+      t <- withPrec Times   $ prettyM t
+      parensIfM Times $ asep [s <++> !timesD, t]
+    prettyM (Sig s (S [< x] (Y t))) =
+      prettyBindType {q} [] x s !timesD t
     prettyM (Pair s t) =
       let GotPairs {init, last, _} = getPairs' [< s] t in
       prettyTuple $ toList $ init :< last
@@ -209,8 +213,8 @@ parameters (showSubsts : Bool)
       prettyApps (Just "@") fun args
     prettyM (s :# a) = do
       s <- withPrec AnnL $ prettyM s
-      a <- withPrec Ann  $ prettyM a
-      parensIfM Ann $ hang 2 $ s <++> !annD <%%> a
+      a <- withPrec AnnR $ prettyM a
+      parensIfM AnnR $ hang 2 $ s <++> !annD <%%> a
     prettyM (CloE e th)  =
       if showSubsts then
         parensIfM SApp . hang 2 =<<

tests/Tests/Parser.idr

@@ -156,7 +156,15 @@ tests = "parser" :- [
       Sig (Just "x") (V "A") (V "B" :@ V "x"),
     parsesAs term "(x : A) ** B x" $
       Sig (Just "x") (V "A") (V "B" :@ V "x"),
-    parseFails term "(1.x : A) × B x"
+    parseFails term "(1.x : A) × B x",
+    parsesAs term "A × B" $
+      Sig Nothing (V "A") (V "B"),
+    parsesAs term "A ** B" $
+      Sig Nothing (V "A") (V "B"),
+    parsesAs term "A × B × C" $
+      Sig Nothing (V "A") (Sig Nothing (V "B") (V "C")),
+    parsesAs term "(A × B) × C" $
+      Sig Nothing (Sig Nothing (V "A") (V "B")) (V "C")
   ],
 
   "lambdas" :- [
@@ -205,6 +213,9 @@ tests = "parser" :- [
     parsesAs term "f x y ≡ g y z : A B C" $
       Eq (Nothing, V "A" :@ V "B" :@ V "C")
          (V "f" :@ V "x" :@ V "y") (V "g" :@ V "y" :@ V "z"),
+    parsesAs term "A × B ≡ A' × B' : ★₁" $
+      Eq (Nothing, TYPE 1)
+         (Sig Nothing (V "A") (V "B")) (Sig Nothing (V "A'") (V "B'")),
     parseFails term "Eq",
     parseFails term "Eq s t",
     parseFails term "s ≡ t",
@@ -242,19 +253,19 @@ tests = "parser" :- [
   ],
 
   "definitions" :- [
-    parsesAs definition "defω x : (_: {a}) × {b} = ('a, 'b)" $
+    parsesAs definition "defω x : {a} × {b} = ('a, 'b)" $
       MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
         (Pair (Tag "a") (Tag "b")),
-    parsesAs definition "defω x : (_: {a}) × {b} = ('a, 'b)" $
+    parsesAs definition "defω x : {a} × {b} = ('a, 'b)" $
       MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
         (Pair (Tag "a") (Tag "b")),
-    parsesAs definition "def# x : (_: {a}) ** {b} = ('a, 'b)" $
+    parsesAs definition "def# x : {a} ** {b} = ('a, 'b)" $
       MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
         (Pair (Tag "a") (Tag "b")),
-    parsesAs definition "def ω.x : (_: {a}) × {b} = ('a, 'b)" $
+    parsesAs definition "def ω.x : {a} × {b} = ('a, 'b)" $
       MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
         (Pair (Tag "a") (Tag "b")),
-    parsesAs definition "def x : (_: {a}) × {b} = ('a, 'b)" $
+    parsesAs definition "def x : {a} × {b} = ('a, 'b)" $
       MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
         (Pair (Tag "a") (Tag "b")),
     parsesAs definition "def0 A : ★₀ = {a, b, c}" $

tests/Tests/PrettyTerm.idr

@@ -108,7 +108,6 @@ tests = "pretty printing terms" :- [
   ],
 
   "pair types" :- [
-    skipWith "todo: non-dependent notation" $
     testPrettyT [<] [<] (FT "A" `And` FT "B") "A × B" "A ** B",
     testPrettyT [<] [<]
       (Sig_ "x" (FT "A") (E $ F "B" :@ BVT 0))