change it to #[..] since # is also reserved

examples/fail.quox

@@ -1,10 +1,10 @@
-@[fail "but cases for"]
+#[fail "but cases for"]
 def missing-b : {a, b} → {a} =
   λ x ⇒ case x return {a} of { 'a ⇒ 'a }
 
-@[fail "duplicate tags"]
+#[fail "duplicate arms"]
 def repeat-enum-case : {a} → {a} =
   λ x ⇒ case x return {a} of { 'a ⇒ 'a; 'a ⇒ 'a }
 
-@[fail "duplicate tags"]
+#[fail "duplicate tags"]
 def repeat-enum-type : {a, a} = 'a

lib/Quox/Parser/Lexer.idr

@@ -134,9 +134,11 @@ namespace Reserved
   ||| description of a reserved symbol
   ||| @ Word a reserved word (must not be followed by letters, digits, etc)
   ||| @ Sym a reserved symbol (must not be followed by symbolic chars)
-  ||| @ Punc a character that doesn't show up in names (brackets, etc)
+  ||| @ Punc a character that doesn't show up in names (brackets, etc);
+  |||        also a sequence ending in one of those, like `#[`, since the
+  |||        difference relates to lookahead
   public export
-  data Reserved1 = Word String | Sym String | Punc Char
+  data Reserved1 = Word String | Sym String | Punc String
   %runElab derive "Reserved1" [Eq, Ord, Show]
 
   ||| description of a token that might have unicode & ascii-only aliases
@@ -145,17 +147,14 @@ namespace Reserved
   %runElab derive "Reserved" [Eq, Ord, Show]
 
   public export
-  Sym1, Word1 : String -> Reserved
-  Sym1 = Only . Sym
+  Sym1, Word1, Punc1 : String -> Reserved
+  Sym1  = Only . Sym
   Word1 = Only . Word
-
-  public export
-  Punc1 : Char -> Reserved
   Punc1 = Only . Punc
 
 public export
 resString1 : Reserved1 -> String
-resString1 (Punc x) = singleton x
+resString1 (Punc x) = x
 resString1 (Word w) = w
 resString1 (Sym  s) = s
 
@@ -171,8 +170,8 @@ resTokenizer1 : Reserved1 -> String -> Tokenizer TokenW
 resTokenizer1 r str =
   let res : String -> Token := const $ Reserved str in
   case r of Word w => match (exact w <+> reject idContEnd) res
-            Sym s  => match (exact s <+> reject symCont)   res
-            Punc x => match (is x)                         res
+            Sym  s => match (exact s <+> reject symCont)   res
+            Punc x => match (exact x)                      res
 
 ||| match a reserved token
 export
@@ -188,16 +187,16 @@ resTokenizer (r `Or` s) =
 public export
 reserved : List Reserved
 reserved =
-  [Punc1 '(', Punc1 ')', Punc1 '[', Punc1 ']', Punc1 '{', Punc1 '}',
-   Punc1 ',', Punc1 ';',
-   Sym1 "@[", Sym1 "@",
+  [Punc1 "(", Punc1 ")", Punc1 "[", Punc1 "]", Punc1 "{", Punc1 "}",
+   Punc1 ",", Punc1 ";", Punc1 "#[",
+   Sym1 "@",
    Sym1 ":",
    Sym "⇒" `Or` Sym "=>",
    Sym "→" `Or` Sym "->",
    Sym "×" `Or` Sym "**",
    Sym "≡" `Or` Sym "==",
    Sym "∷" `Or` Sym "::",
-   Punc1 '.',
+   Punc1 ".",
    Word1 "case",
    Word1 "case0", Word1 "case1",
    Word "caseω" `Or` Word "case#",

lib/Quox/Parser/Parser.idr

@@ -584,7 +584,7 @@ term fname = lamTerm fname
 
 export
 pragma : Grammar True a -> Grammar True a
-pragma p = resC "@[" *> p <* mustWork (resC "]")
+pragma p = resC "#[" *> p <* mustWork (resC "]")
 
 export
 declMod : FileName -> Grammar True PDeclMod

tests/Tests/Parser.idr

@@ -424,33 +424,46 @@ tests = "parser" :- [
 
   "top level" :- [
     parseMatch input "def0 A : ★⁰ = {}; def0 B : ★¹ = A;"
-      `([PD $ PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _,
-         PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _]),
+      `([PD $ MkPDecl []
+          (PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _) _,
+         PD $ MkPDecl []
+          (PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _) _]),
     parseMatch input "def0 A : ★⁰ = {} def0 B : ★¹ = A" $
-      `([PD $ PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _,
-         PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _]),
+      `([PD $ MkPDecl []
+          (PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _) _,
+         PD $ MkPDecl []
+          (PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _) _]),
     note "empty input",
     parsesAs input "" [],
     parseFails input ";;;;;;;;;;;;;;;;;;;;;;;;;;",
     parseMatch input "namespace a {}"
-      `([PD $ PNs $ MkPNamespace [< "a"] [] _]),
+      `([PD $ MkPDecl [] (PNs $ MkPNamespace [< "a"] [] _) _]),
     parseMatch input "namespace a.b.c {}"
-      `([PD $ PNs $ MkPNamespace [< "a", "b", "c"] [] _]),
+      `([PD $ MkPDecl []
+          (PNs $ MkPNamespace [< "a", "b", "c"] [] _) _]),
     parseMatch input "namespace a {namespace b {}}"
-      `([PD $ PNs $ MkPNamespace [< "a"] [PNs $ MkPNamespace [< "b"] [] _] _]),
+      `([PD (MkPDecl []
+          (PNs $ MkPNamespace [< "a"]
+            [MkPDecl [] (PNs $ MkPNamespace [< "b"] [] _) _] _) _)]),
     parseMatch input "namespace a {def x = 't ∷ {t}}"
-      `([PD $ PNs $ MkPNamespace [< "a"]
-          [PDef $ MkPDef (PQ Any _) "x" Nothing
-              (Ann (Tag "t" _) (Enum ["t"] _) _) _] _]),
+      `([PD (MkPDecl []
+          (PNs $ MkPNamespace [< "a"]
+            [MkPDecl []
+              (PDef $ MkPDef (PQ Any _) "x" Nothing
+                (Ann (Tag "t" _) (Enum ["t"] _) _) _) _] _) _)]),
     parseMatch input "namespace a {def x = 't ∷ {t}} def y = a.x"
-      `([PD $ PNs $ MkPNamespace [< "a"]
-          [PDef $ MkPDef (PQ Any _) "x" Nothing
-              (Ann (Tag "t" _) (Enum ["t"] _) _) _] _,
-         PD $ PDef $ MkPDef (PQ Any _) "y" Nothing
-            (V (MakePName [< "a"] "x") {}) _]),
+      `([PD (MkPDecl []
+          (PNs $ MkPNamespace [< "a"]
+            [MkPDecl []
+              (PDef $ MkPDef (PQ Any _) "x" Nothing
+                             (Ann (Tag "t" _) (Enum ["t"] _) _) _) _] _) _),
+         PD (MkPDecl []
+          (PDef $ MkPDef (PQ Any _) "y" Nothing
+                         (V (MakePName [< "a"] "x") Nothing _) _) _)]),
     parseMatch input #" load "a.quox"; def b = a.b "#
       `([PLoad "a.quox" _,
-         PD $ PDef $ MkPDef (PQ Any _) "b" Nothing
-            (V (MakePName [< "a"] "b") {}) _])
+         PD (MkPDecl []
+           (PDef $ MkPDef (PQ Any _) "b" Nothing
+                          (V (MakePName [< "a"] "b") Nothing _) _) _)])
   ]
 ]