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 arms"]
+#[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