replace '≔' and '·' with '=' and (only) '.'

lib/Quox/Parser/Lexer.idr

@@ -183,7 +183,7 @@ reserved =
    Sym "×" `Or` Sym "**",
    Sym "≡" `Or` Sym "==",
    Sym "∷" `Or` Sym "::",
-   Sym "·" `Or` Punc '.',
+   Punc1 '.',
    Word1 "case",
    Word1 "case1",
    Word "caseω" `Or` Word "case#",
@@ -198,7 +198,7 @@ reserved =
    Word1 "def",
    Word1 "def0",
    Word "defω" `Or` Word "def#",
-   Sym "≔" `Or` Sym ":=",
+   Sym1 "=",
    Word1 "load",
    Word1 "namespace"]
 

lib/Quox/Parser/Parser.idr

@@ -120,7 +120,7 @@ qty = zeroOne Zero One
 
 private covering
 qtys : Grammar False (List PQty)
-qtys = option [] [|toList $ some qty <* res "·"|]
+qtys = option [] [|toList $ some qty <* res "."|]
 
 export
 dimConst : Grammar True DimConst
@@ -177,7 +177,7 @@ private covering
 caseIntro : Grammar True PQty
 caseIntro = resC "case1" $> One
         <|> resC "caseω" $> Any
-        <|> resC "case" *> qty <* resC "·"
+        <|> resC "case" *> qty <* resC "."
 
 private
 optNameBinder : Grammar False BName
@@ -272,12 +272,12 @@ export covering
 defIntro : Grammar True PQty
 defIntro = Zero <$ resC "def0"
        <|> Any  <$ resC "defω"
-       <|> resC "def" *> option Any (qty <* resC "·")
+       <|> resC "def" *> option Any (qty <* resC ".")
 
 export covering
 definition : Grammar True PDefinition
 definition =
-  [|MkPDef defIntro name (optional (resC ":" *> term)) (resC "≔" *> term)|]
+  [|MkPDef defIntro name (optional (resC ":" *> term)) (resC "=" *> term)|]
 
 export
 load : Grammar True String

lib/Quox/Syntax/Qty.idr

@@ -15,16 +15,15 @@ commas [x]     = [x]
 commas (x::xs) = (x <+> hl Delim ",") :: commas xs
 
 private %inline
-blobD : Pretty.HasEnv m => m (Doc HL)
+dotD : Doc HL
-blobD = hlF Delim $ ifUnicode "·" "%"
+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 $
-  hang 2 $ sep [aseparate comma !(traverse pretty0M qtys) <++> !blobD,
+  hcat [hseparate comma !(traverse pretty0M qtys), dotD, align !(pretty0M x)]
-                !(pretty0M x)]
 
 
 public export

tests/Tests/Lexer.idr

@@ -91,10 +91,10 @@ tests = "lexer" :- [
 
     lexes "+a" [Name "+", Name "a"],
 
-    lexes "x." [Name "x", Reserved "·"],
+    lexes "x." [Name "x", Reserved "."],
-    lexes "&." [Name "&", Reserved "·"],
+    lexes "&." [Name "&", Reserved "."],
-    lexes ".x" [Reserved "·", Name "x"],
+    lexes ".x" [Reserved ".", Name "x"],
-    lexes "a.b.c." [Name $ MakePName [< "a", "b"] "c", Reserved "·"],
+    lexes "a.b.c." [Name $ MakePName [< "a", "b"] "c", Reserved "."],
 
     lexes "case" [Reserved "case"],
     lexes "caseω" [Reserved "caseω"],
@@ -108,7 +108,12 @@ tests = "lexer" :- [
     lexes "a_" [Name "a_"],
 
     lexes "a'" [Name "a'"],
-    lexes "+'" [Name "+'"]
+    lexes "+'" [Name "+'"],
+
+    lexes "0.x" [Nat 0, Reserved ".", Name "x"],
+    lexes "1.x" [Nat 1, Reserved ".", Name "x"],
+    lexes "ω.x" [Reserved "ω", Reserved ".", Name "x"],
+    lexes "#.x" [Reserved "ω", Reserved ".", Name "x"]
   ],
 
   "syntax characters" :- [

tests/Tests/Parser.idr

@@ -142,21 +142,21 @@ 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" $
       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" $
       Pi Any (Just "x") (V "A") (V "B" :@ V "x"),
     parseFails term "(x : A) → B x",
-    parseFails term "(1 ω·x : A) → B x",
+    parseFails term "(1 ω.x : A) → B x",
     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"
   ],
 
   "lambdas" :- [
@@ -179,7 +179,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)" $
@@ -225,7 +225,7 @@ tests = "parser" :- [
            (CasePair (Just "l", Just "r")
                      (V "add" :@ V "l" :@ V "r")),
     parsesAs term
-      "case 1 · f s return x ⇒ A x of { (l, r) ⇒ add l r }" $
+      "case 1 . f s return x ⇒ A x of { (l, r) ⇒ add l r }" $
       Case One (V "f" :@ V "s")
            (Just "x", V "A" :@ V "x")
            (CasePair (Just "l", Just "r")
@@ -242,33 +242,33 @@ 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}" $
+    parsesAs definition "def0 A : ★₀ = {a, b, c}" $
       MkPDef Zero "A" (Just $ TYPE 0) (Enum ["a", "b", "c"])
   ],
 
   "top level" :- [
-    parsesAs input "def0 A : ★₀ ≔ {}; def0 B : ★₁ ≔ A;" $
+    parsesAs input "def0 A : ★₀ = {}; def0 B : ★₁ = A;" $
       [PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []),
        PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")],
-    parsesAs input "def0 A : ★₀ ≔ {} def0 B : ★₁ ≔ A" $
+    parsesAs input "def0 A : ★₀ = {} def0 B : ★₁ = A" $
       [PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []),
        PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")],
-    parsesAs input "def0 A : ★₀ ≔ {};;; def0 B : ★₁ ≔ A" $
+    parsesAs input "def0 A : ★₀ = {};;; def0 B : ★₁ = A" $
       [PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []),
        PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")],
     parsesAs input "" [] {label = "[empty input]"},

tests/Tests/PrettyTerm.idr

@@ -88,17 +88,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"
   ],
 
@@ -124,8 +124,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" :- [