"1.(x: A) → B" instead of "(1.x: A) → B"

also "1.A → B"

lib/Quox/Parser/Parser.idr

@@ -151,31 +151,6 @@ toVect : List a -> (n ** Vect n a)
 toVect []        = (_ ** [])
 toVect (x :: xs) = (_ ** x :: snd (toVect xs))
 
-private
-0 MakeBinder : Nat -> Type
-MakeBinder n = (String, PBinderHead n -> PTerm -> PTerm)
-
-private
-makePi : MakeBinder 1
-makePi = ("→", \([pi], x, s) => Pi pi x s)
-
-private
-makeSig : MakeBinder 0
-makeSig = ("×", \([], x, s) => Sig x s)
-
-private
-makeBinder : (m ** PBinderHead m) -> (n ** MakeBinder n) -> PTerm ->
-             Grammar False PTerm
-makeBinder (m ** h) (n ** (str, f)) t =
-  case decEq m n of
-    Yes Refl => pure $ f h t
-    No  _    =>
-      let q = if m == 1 then "quantity" else "quantities" in
-      fatalError "'\{str}' expects \{show m} \{q}, got \{show n}"
-
-private
-binderInfix : Grammar True (n ** MakeBinder n)
-binderInfix = symbols [((1 ** makePi), "→"), ((0 ** makeSig), "×")]
 
 private
 lamIntro : Grammar True (BName -> PTerm -> PTerm)
@@ -217,7 +192,21 @@ mutual
 
   private covering
   bindTerm : Grammar True PTerm
-  bindTerm = join [|makeBinder binderHead binderInfix term|]
+  bindTerm = pi <|> sigma
+  where
+    binderHead = parens {commit = False} [|MkPair bname (resC ":" *> term)|]
+
+    pi, sigma : Grammar True PTerm
+    pi = [|makePi (qty <* res ".") domain (resC "→" *> term)|]
+    where
+      makePi : Three -> (BName, PTerm) -> PTerm -> PTerm
+      makePi q (x, s) t = Pi q x s t
+      domain = binderHead <|> [|(Nothing,) aTerm|]
+
+    sigma = [|makeSigma binderHead (resC "×" *> annTerm)|]
+    where
+      makeSigma : (BName, PTerm) -> PTerm -> PTerm
+      makeSigma (x, s) t = Sig x s t
 
   private covering
   annTerm : Grammar True PTerm
@@ -260,14 +249,6 @@ mutual
       <|> [|Tag tag|]
       <|> foldr1 Pair <$> parens (commaSep1 term)
 
-  private covering
-  binderHead : Grammar True (n ** PBinderHead n)
-  binderHead = parens {commit = False} $ do
-    qs   <- [|toVect qtys|]
-    name <- bname
-    ty   <- resC ":" *> term
-    pure (qs.fst ** (qs.snd, name, ty))
-
   private covering
   optBinderTerm : Grammar True (BName, PTerm)
   optBinderTerm = [|MkPair optNameBinder term|]

lib/Quox/Syntax/Qty.idr

@@ -8,24 +8,6 @@ import Data.DPair
 %default total
 
 
-private
-commas : List (Doc HL) -> List (Doc HL)
-commas []      = []
-commas [x]     = [x]
-commas (x::xs) = (x <+> hl Delim ",") :: commas xs
-
-private %inline
-dotD : Doc HL
-dotD = hl Delim "."
-
-export %inline
-prettyQtyBinds : Pretty.HasEnv m => PrettyHL q => PrettyHL a =>
-                 List q -> a -> m (Doc HL)
-prettyQtyBinds []   x = pretty0M x
-prettyQtyBinds qtys x = pure $
-  hcat [hseparate comma !(traverse pretty0M qtys), dotD, align !(pretty0M x)]
-
-
 public export
 interface Eq q => IsQty q where
   zero, one : q
@@ -57,6 +39,9 @@ interface Eq q => IsQty q where
   isGlobal : Dec1 IsGlobal
   zeroIsGlobal : forall pi. IsZero pi -> IsGlobal zero
 
+  ||| prints in a form that can be a suffix of "case"
+  prettySuffix : Pretty.HasEnv m => q -> m (Doc HL)
+
 public export
 0 SQty : (q : Type) -> IsQty q => Type
 SQty q = Subset q IsSubj

lib/Quox/Syntax/Qty/Three.idr

@@ -120,6 +120,8 @@ IsQty Three where
   isGlobal     = isGlobal3
   zeroIsGlobal = \Refl => GZero
 
+  prettySuffix = pretty0M
+
 
 export Uninhabited (IsGlobal3 One) where uninhabited _ impossible
 

lib/Quox/Syntax/Term/Pretty.idr

@@ -24,13 +24,14 @@ dlamD   = hlF Syntax $ ifUnicode "δ" "dfun"
 annD    = hlF Syntax $ ifUnicode "∷" "::"
 
 private %inline
-eqD, colonD, commaD, caseD, returnD, ofD : Doc HL
+eqD, colonD, commaD, caseD, returnD, ofD, dotD : Doc HL
 eqD     = hl Syntax "Eq"
 colonD  = hl Syntax ":"
 commaD  = hl Syntax ","
 caseD   = hl Syntax "case"
 ofD     = hl Syntax "of"
 returnD = hl Syntax "return"
+dotD    = hl Delim "."
 
 
 export
@@ -47,22 +48,39 @@ export
 prettyUniverse : Universe -> Doc HL
 prettyUniverse = hl Syntax . pretty
 
+
+public export
+data WithQty q a = MkWithQty q a
+
 export
-prettyBind : PrettyHL a => PrettyHL q => Pretty.HasEnv m =>
+PrettyHL q => PrettyHL a => PrettyHL (WithQty q a) where
-             List q -> BaseName -> a -> m (Doc HL)
+  prettyM (MkWithQty q x) = do
-prettyBind qtys x s = do
+    q <- pretty0M q
-  var <- prettyQtyBinds qtys $ TV x
+    x <- withPrec Arg $ prettyM x
-  s   <- withPrec Outer $ prettyM s
+    pure $ hcat [q, dotD, x]
-  pure $ var <++> colonD <%%> hang 2 s
+
+
+public export
+data Binder a = MkBinder BaseName a
+
+export
+PrettyHL a => PrettyHL (Binder a) where
+  prettyM (MkBinder x ty) = do
+    x  <- pretty0M $ TV x
+    ty <- align <$> pretty0M ty
+    pure $ parens $ sep [hsep [x, colonD], ty]
+
 
 export
 prettyBindType : PrettyHL a => PrettyHL b => PrettyHL q =>
                  Pretty.HasEnv m =>
-                 List q -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
+                 Maybe q -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
-prettyBindType qtys x s arr t = do
+prettyBindType q x s arr t = do
-  bind <- prettyBind qtys x s
+  bind <- case q of
-  t    <- withPrec AnnR $ under T x $ prettyM t
+    Nothing => pretty0M $ MkBinder x s
-  parensIfM AnnR $ hang 2 $ parens bind <++> arr <%%> t
+    Just q  => pretty0M $ MkWithQty q $ MkBinder x s
+  t <- withPrec AnnR $ under T x $ prettyM t
+  parensIfM AnnR $ hang 2 $ bind <++> arr <%%> t
 
 export
 prettyArm : PrettyHL a => Pretty.HasEnv m =>
@@ -105,15 +123,16 @@ prettyArms =
   map (braces . asep) . traverse (\(xs, l, r) => prettyArm T xs l r)
 
 export
-prettyCase : PrettyHL a => PrettyHL b => PrettyHL c => PrettyHL q =>
+prettyCase : PrettyHL a => PrettyHL b => PrettyHL c => IsQty q =>
              Pretty.HasEnv m =>
              q -> a -> BaseName -> b -> List (SnocList BaseName, Doc HL, c) ->
              m (Doc HL)
 prettyCase pi elim r ret arms = do
-  elim <- prettyQtyBinds [pi] elim
+  caseq <- (caseD <+>) <$> prettySuffix pi
-  ret  <- prettyLams Nothing T [< r] ret
+  elim  <- pretty0M elim
-  arms <- prettyArms arms
+  ret   <- prettyLams Nothing T [< r] ret
-  pure $ asep [caseD <++> elim, returnD <++> ret, ofD <++> arms]
+  arms  <- prettyArms arms
+  pure $ asep [caseq <++> elim, returnD <++> ret, ofD <++> arms]
 
 export
 escapeString : String -> String
@@ -142,12 +161,12 @@ prettyTagBare t = hl Tag $ quoteTag t
 parameters (showSubsts : Bool)
  mutual
   export covering
-  [TermSubst] PrettyHL q => PrettyHL (Term q d n) using TermSubst ElimSubst
+  [TermSubst] IsQty q => PrettyHL q => PrettyHL (Term q d n) using ElimSubst
   where
     prettyM (TYPE l) =
       parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
     prettyM (Pi qty s (S [< x] t)) =
-      prettyBindType [qty] x s !arrowD t.term
+      prettyBindType (Just qty) x s !arrowD t.term
     prettyM (Lam (S x t)) =
       let GotLams {names, body, _} = getLams' x t.term Refl in
       prettyLams (Just !lamD) T (toSnocList' names) body
@@ -156,7 +175,7 @@ parameters (showSubsts : Bool)
       t <- withPrec Times   $ prettyM t
       parensIfM Times $ asep [s <++> !timesD, t]
     prettyM (Sig s (S [< x] (Y t))) =
-      prettyBindType {q} [] x s !timesD t
+      prettyBindType {q} Nothing x s !timesD t
     prettyM (Pair s t) =
       let GotPairs {init, last, _} = getPairs' [< s] t in
       prettyTuple $ toList $ init :< last
@@ -193,7 +212,7 @@ parameters (showSubsts : Bool)
         prettyM $ pushSubstsWith' th id s
 
   export covering
-  [ElimSubst] PrettyHL q => PrettyHL (Elim q d n) using TermSubst ElimSubst
+  [ElimSubst] IsQty q => PrettyHL q => PrettyHL (Elim q d n) using TermSubst
   where
     prettyM (F x) =
       hl' Free <$> prettyM x
@@ -229,22 +248,22 @@ parameters (showSubsts : Bool)
         prettyM $ pushSubstsWith' th id e
 
   export covering
-  prettyTSubst : Pretty.HasEnv m => PrettyHL q =>
+  prettyTSubst : Pretty.HasEnv m => IsQty q => PrettyHL q =>
                  TSubst q d from to -> m (Doc HL)
   prettyTSubst s =
     prettySubstM (prettyM @{ElimSubst}) (!ask).tnames TVar "[" "]" s
 
 export covering %inline
-PrettyHL q => PrettyHL (Term q d n) where
+IsQty q => PrettyHL q => PrettyHL (Term q d n) where
   prettyM = prettyM @{TermSubst False}
 
 export covering %inline
-PrettyHL q => PrettyHL (Elim q d n) where
+IsQty q => PrettyHL q => PrettyHL (Elim q d n) where
   prettyM = prettyM @{ElimSubst False}
 
 
 export covering
-prettyTerm : PrettyHL q => (unicode : Bool) ->
+prettyTerm : IsQty q => PrettyHL q => (unicode : Bool) ->
              (dnames : NContext d) -> (tnames : NContext n) ->
              Term q d n -> Doc HL
 prettyTerm unicode dnames tnames term =

lib/Quox/Typing/Context.idr

@@ -150,14 +150,15 @@ namespace EqContext
     }
 
 
-parameters {auto _ : (Eq q, PrettyHL q)} (unicode : Bool)
+parameters {auto _ : (Eq q, PrettyHL q, IsQty q)} (unicode : Bool)
   export covering
   prettyTContext : QContext q n -> NContext n -> TContext q d n -> Doc HL
   prettyTContext qs ns ctx = separate comma $ toList $ go qs ns ctx where
     go : QContext q m -> NContext m -> TContext q d m -> SnocList (Doc HL)
     go [<]       [<]       [<] = [<]
     go (qs :< q) (xs :< x) (ctx :< t) =
-      go qs xs ctx :< runPretty unicode (prettyBind [q] x t)
+      let bind = MkWithQty q $ MkBinder x t in
+      go qs xs ctx :< runPretty unicode (pretty0M bind)
 
   private
   prettyDVars : NContext d -> Doc HL

lib/Quox/Typing/Error.idr

@@ -154,7 +154,7 @@ isTypeInUniverse : Maybe Universe -> Doc HL
 isTypeInUniverse Nothing  = "is a type"
 isTypeInUniverse (Just k) = "is a type in universe" <++> prettyUniverse k
 
-parameters {auto _ : (Eq q, PrettyHL q)} (unicode : Bool)
+parameters {auto _ : (Eq q, IsQty q, PrettyHL q)} (unicode : Bool)
   private
   termt : TyContext q d n -> Term q d n -> Doc HL
   termt ctx = hang 4 . prettyTerm unicode ctx.dnames ctx.tnames

tests/TermImpls.idr

@@ -104,9 +104,9 @@ mutual
     DCloE {} == _ = False
 
 export covering
-PrettyHL q => Show (Term q d n) where
+IsQty q => PrettyHL q => Show (Term q d n) where
   showPrec d t = showParens (d /= Open) $ prettyStr True t
 
 export covering
-PrettyHL q => Show (Elim q d n) where
+IsQty q => PrettyHL q => Show (Elim q d n) where
   showPrec d e = showParens (d /= Open) $ prettyStr True e

tests/Tests/Parser.idr

@@ -140,21 +140,25 @@ tests = "parser" :- [
   ],
 
   "binders" :- [
-    parsesAs term "(1.x : A) → B x" $
+    parsesAs term "1.(x : A) → B x" $
       Pi One (Just "x") (V "A") (V "B" :@ V "x"),
-    parsesAs term "(1.x : A) -> B x" $
+    parsesAs term "1.(x : A) -> B x" $
       Pi One (Just "x") (V "A") (V "B" :@ V "x"),
-    parsesAs term "(ω.x : A) → B x" $
+    parsesAs term "ω.(x : A) → B x" $
       Pi Any (Just "x") (V "A") (V "B" :@ V "x"),
-    parsesAs term "(#.x : A) -> B x" $
+    parsesAs term "#.(x : A) -> B x" $
       Pi Any (Just "x") (V "A") (V "B" :@ V "x"),
     parseFails term "(x : A) → B x",
-    parseFails term "(1 ω.x : A) → B x",
+    parsesAs term "1.A → B"
+      (Pi One Nothing (V "A") (V "B")),
+    parsesAs term "1.(List A) → List B"
+      (Pi One Nothing (V "List" :@ V "A") (V "List" :@ V "B")),
+    parseFails term "1.List A → List B",
     parsesAs term "(x : A) × B x" $
       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" $
@@ -185,7 +189,7 @@ tests = "parser" :- [
       Pair (Pair (V "x") (V "y")) (V "z"),
     parsesAs term "(f x, g @y)" $
       Pair (V "f" :@ V "x") (V "g" :% V "y"),
-    parsesAs term "((x : A) × B, (0.x : C) → D)" $
+    parsesAs term "((x : A) × B, 0.(x : C) → D)" $
       Pair (Sig (Just "x") (V "A") (V "B"))
            (Pi Zero (Just "x") (V "C") (V "D")),
     parsesAs term "(λ x ⇒ x, δ i ⇒ e @i)" $

tests/Tests/PrettyTerm.idr

@@ -93,17 +93,17 @@ tests = "pretty printing terms" :- [
     testPrettyT [<] [<] (Arr One (FT "A") (FT "B")) "A ⊸ B" "A -o B",
     testPrettyT [<] [<]
       (Pi_ One "x" (FT "A") (E $ F "B" :@ BVT 0))
-      "(1.x : A) → B x"
+      "1.(x : A) → B x"
-      "(1.x : A) -> B x",
+      "1.(x : A) -> B x",
     testPrettyT [<] [<]
       (Pi_ Zero "A" (TYPE 0) $ Arr Any (BVT 0) (BVT 0))
-      "(0.A : ★₀) → (ω._ : A) → A"
+      "0.(A : ★₀) → ω.(_ : A) → A"
-      "(0.A : Type0) -> (#._ : A) -> A",
+      "0.(A : Type0) -> #.(_ : A) -> A",
     todo #"print (and parse) the below as "(A ↠ A) ↠ A""#,
     testPrettyT [<] [<]
       (Arr Any (Arr Any (FT "A") (FT "A")) (FT "A"))
-      "(ω._ : (ω._ : A) → A) → A"
+      "ω.(_ : ω.(_ : A) → A) → A"
-      "(#._ : (#._ : A) -> A) -> A",
+      "#.(_ : #.(_ : A) -> A) -> A",
     todo "non-dependent, left and right nested"
   ],
 
@@ -128,8 +128,8 @@ tests = "pretty printing terms" :- [
     testPrettyT1 [<] [<] (Pair (Pair (FT "A") (FT "B")) (FT "C")) "((A, B), C)",
     testPrettyT [<] [<]
       (Pair ([< "x"] :\\ BVT 0) (Arr One (FT "B₁") (FT "B₂")))
-      "(λ x ⇒ x, (1._ : B₁) → B₂)"
+      "(λ x ⇒ x, 1.(_ : B₁) → B₂)"
-      "(fun x => x, (1._ : B₁) -> B₂)"
+      "(fun x => x, 1.(_ : B₁) -> B₂)"
   ],
 
   "enum types" :- [
@@ -152,20 +152,19 @@ tests = "pretty printing terms" :- [
   todo "equality types",
 
   "case" :- [
-    note "todo: print using case1 and caseω???",
     testPrettyE [<] [<]
       (CasePair One (F "a") (SN $ TYPE 1) (SN $ TYPE 0))
-      "case 1.a return _ ⇒ ★₁ of { (_, _) ⇒ ★₀ }"
+      "case1 a return _ ⇒ ★₁ of { (_, _) ⇒ ★₀ }"
-      "case 1.a return _ => Type1 of { (_, _) => Type0 }",
+      "case1 a return _ => Type1 of { (_, _) => Type0 }",
     testPrettyT [<] [<]
       ([< "u"] :\\
         E (CaseEnum One (F "u")
             (SY [< "x"] $ Eq0 (enum ["tt"]) (BVT 0) (Tag "tt"))
             (fromList [("tt", [< Unused] :\\% Tag "tt")])))
-      "λ u ⇒ case 1.u return x ⇒ x ≡ 'tt : {tt} of { 'tt ⇒ δ _ ⇒ 'tt }"
+      "λ u ⇒ case1 u return x ⇒ x ≡ 'tt : {tt} of { 'tt ⇒ δ _ ⇒ 'tt }"
       """
         fun u =>
-        case 1.u return x => x == 'tt : {tt} of { 'tt => dfun _ => 'tt }
+        case1 u return x => x == 'tt : {tt} of { 'tt => dfun _ => 'tt }
       """
   ],
 
@@ -181,11 +180,11 @@ tests = "pretty printing terms" :- [
       "(α :: a) :: A",
     testPrettyE [<] [<]
       (([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A"))
-      "(λ x ⇒ x) ∷ (1._ : A) → A"
+      "(λ x ⇒ x) ∷ 1.(_ : A) → A"
-      "(fun x => x) :: (1._ : A) -> A",
+      "(fun x => x) :: 1.(_ : A) -> A",
     testPrettyE [<] [<]
       (Arr One (FT "A") (FT "A") :# TYPE 7)
-      "((1._ : A) → A) ∷ ★₇"
+      "(1.(_ : A) → A) ∷ ★₇"
-      "((1._ : A) -> A) :: Type7"
+      "(1.(_ : A) -> A) :: Type7"
   ]
 ]

tests/TypingImpls.idr

@@ -14,15 +14,15 @@ import Derive.Prelude
 %runElab deriveIndexed "DimEq" [Show]
 
 export %hint
-showTyContext : (PrettyHL q, Show q) => Show (TyContext q d n)
+showTyContext : (IsQty q, PrettyHL q, Show q) => Show (TyContext q d n)
 showTyContext = deriveShow
 
 export %hint
-showEqContext : (PrettyHL q, Show q) => Show (EqContext q n)
+showEqContext : (IsQty q, PrettyHL q, Show q) => Show (EqContext q n)
 showEqContext = deriveShow
 
 export %hint
-showTypingError : (PrettyHL q, Show q) => Show (Error q)
+showTypingError : (IsQty q, PrettyHL q, Show q) => Show (Error q)
 showTypingError = deriveShow
 
 export
@@ -33,5 +33,5 @@ ToInfo WhnfError where
      ("list", show ts)]
 
 export
-(Eq q, PrettyHL q) => ToInfo (Error q) where
+(IsQty q, PrettyHL q) => ToInfo (Error q) where
   toInfo err = [("err", show $ prettyError True True err)]