From d4cfbd4045917b1e5b4a9205e641cc436b9849fc Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 22 Sep 2023 01:29:23 +0200
Subject: [PATCH] add @[fail] modifier to declarations

- `@[fail] def foo = ...` succeeds if `foo` has some error.
- `@[fail "scope"] def foo = ...` succeeds if `foo` has some error
  containing the word "scope" somewhere
- `@[fail] namespace foo { }` works too and the error must be anywhere
  in the namespace
---
 lib/Quox/Parser/FromParser.idr                | 94 +++++++++++++------
 lib/Quox/Parser/FromParser/Error.idr          | 10 ++
 lib/Quox/Parser/Lexer.idr                     |  2 +-
 lib/Quox/Parser/Parser.idr                    | 21 ++++-
 lib/Quox/Parser/Syntax.idr                    | 31 ++++--
 .../PrettyPrint/Bernardy/Core/Decorate.idr    | 10 ++
 6 files changed, 127 insertions(+), 41 deletions(-)

diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 9c2fdcd..53411c7 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -3,6 +3,7 @@ module Quox.Parser.FromParser
 
 import public Quox.Parser.FromParser.Error as Quox.Parser.FromParser
 
+import Quox.Pretty
 import Quox.Parser.Syntax
 import Quox.Parser.Parser
 import public Quox.Parser.LoadFile
@@ -42,6 +43,35 @@ FromParserIO : List (Type -> Type)
 FromParserIO = LoadFile :: FromParserPure
 
 
+export
+fromParserPure : NameSuf -> Definitions ->
+                 Eff FromParserPure a ->
+                 Either Error (a, NameSuf, Definitions)
+fromParserPure suf defs act = runSTErr $ do
+  suf  <- liftST $ newSTRef suf
+  defs <- liftST $ newSTRef defs
+  res  <- runEff act $ with Union.(::)
+    [handleExcept (\e => stLeft e),
+     handleStateSTRef defs,
+     handleStateSTRef !(liftST $ newSTRef [<]),
+     handleStateSTRef suf]
+  pure (res, !(liftST $ readSTRef suf), !(liftST $ readSTRef defs))
+
+
+export covering
+fromParserIO : (MonadRec io, HasIO io) =>
+               IncludePath -> IORef SeenSet ->
+               IORef NameSuf -> IORef Definitions ->
+               Eff FromParserIO a -> io (Either Error a)
+fromParserIO inc seen suf defs act = liftIO $ fromIOErr $ do
+  runEff act $ with Union.(::)
+    [handleLoadFileIOE LoadError seen inc,
+     handleExcept (\e => ioLeft e),
+     handleStateIORef defs,
+     handleStateIORef !(newIORef [<]),
+     handleStateIORef suf]
+
+
 parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
            (xs : Context' PatVar n)
   private
@@ -318,12 +348,43 @@ fromPDef (MkPDef qty pname ptype pterm defLoc) = do
       res <- liftTC $ inferC empty sqty elim
       addDef name gqty res.type term defLoc
 
+
+public export
+data HasFail = NoFail | AnyFail | FailWith String
+
+export
+hasFail : List PDeclMod -> HasFail
+hasFail []                  = NoFail
+hasFail (PFail str _ :: _)  = maybe AnyFail FailWith str
+
 export covering
 fromPDecl : PDecl -> Eff FromParserPure (List NDefinition)
-fromPDecl (PDef def) = singleton <$> fromPDef def
-fromPDecl (PNs  ns)  =
+
+export covering
+fromPDeclBody : PDeclBody -> Eff FromParserPure (List NDefinition)
+fromPDeclBody (PDef def) = singleton <$> fromPDef def
+fromPDeclBody (PNs  ns)  =
   localAt NS (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls
 
+export covering
+expectFail : PDeclBody -> Eff FromParserPure Error
+expectFail body =
+  case fromParserPure !(getAt GEN) !(getAt DEFS) $ fromPDeclBody body of
+    Left  err => pure err
+    Right _   => throw $ ExpectedFail body.loc
+
+
+fromPDecl (MkPDecl mods decl loc) = case hasFail mods of
+  NoFail       => fromPDeclBody decl
+  AnyFail      => expectFail decl $> []
+  FailWith str => do
+    err <- expectFail decl
+    let msg = runPretty $ prettyError False err {opts = Opts 10_000} -- w/e
+    if str `isInfixOf` renderInfinite msg
+       then pure []
+       else throw $ WrongFail str err loc
+
+
 mutual
   export covering
   loadProcessFile : Loc -> String -> Eff FromParserIO (List NDefinition)
@@ -339,32 +400,3 @@ mutual
   fromPTopLevel : PTopLevel -> Eff FromParserIO (List NDefinition)
   fromPTopLevel (PD    decl)     = lift $ fromPDecl decl
   fromPTopLevel (PLoad file loc) = loadProcessFile loc file
-
-
-export
-fromParserPure : NameSuf -> Definitions ->
-                 Eff FromParserPure a ->
-                 Either Error (a, NameSuf, Definitions)
-fromParserPure suf defs act = runSTErr $ do
-  suf  <- liftST $ newSTRef suf
-  defs <- liftST $ newSTRef defs
-  res  <- runEff act $ with Union.(::)
-    [handleExcept (\e => stLeft e),
-     handleStateSTRef defs,
-     handleStateSTRef !(liftST $ newSTRef [<]),
-     handleStateSTRef suf]
-  pure (res, !(liftST $ readSTRef suf), !(liftST $ readSTRef defs))
-
-
-export covering
-fromParserIO : (MonadRec io, HasIO io) =>
-               IncludePath -> IORef SeenSet ->
-               IORef NameSuf -> IORef Definitions ->
-               Eff FromParserIO a -> io (Either Error a)
-fromParserIO inc seen suf defs act = liftIO $ fromIOErr $ do
-  runEff act $ with Union.(::)
-    [handleLoadFileIOE LoadError seen inc,
-     handleExcept (\e => ioLeft e),
-     handleStateIORef defs,
-     handleStateIORef !(newIORef [<]),
-     handleStateIORef suf]
diff --git a/lib/Quox/Parser/FromParser/Error.idr b/lib/Quox/Parser/FromParser/Error.idr
index f6c7e53..0803f1f 100644
--- a/lib/Quox/Parser/FromParser/Error.idr
+++ b/lib/Quox/Parser/FromParser/Error.idr
@@ -30,6 +30,8 @@ data Error =
   | DisplacedBoundVar Loc PName
   | WrapTypeError TypeError
   | LoadError Loc FilePath FileError
+  | ExpectedFail Loc
+  | WrongFail String Error Loc
   | WrapParseError String ParseError
 
 
@@ -106,5 +108,13 @@ parameters (showContext : Bool)
           "couldn't load file" <++> text file,
           text $ show err]
 
+  prettyError (ExpectedFail loc) = pure $
+    sep [!(prettyLoc loc), "expected error"]
+
+  prettyError (WrongFail str err loc) = pure $
+    sep [!(prettyLoc loc),
+         "wrong error, expected to match", !(hl Tag $ text "\"\{str}\""),
+         "but got", !(prettyError err)]
+
   prettyError (WrapParseError file err) =
     prettyParseError file err
diff --git a/lib/Quox/Parser/Lexer.idr b/lib/Quox/Parser/Lexer.idr
index d4359d4..a01b6b3 100644
--- a/lib/Quox/Parser/Lexer.idr
+++ b/lib/Quox/Parser/Lexer.idr
@@ -190,7 +190,7 @@ reserved : List Reserved
 reserved =
   [Punc1 '(', Punc1 ')', Punc1 '[', Punc1 ']', Punc1 '{', Punc1 '}',
    Punc1 ',', Punc1 ';',
-   Sym1 "@",
+   Sym1 "@[", Sym1 "@",
    Sym1 ":",
    Sym "⇒" `Or` Sym "=>",
    Sym "→" `Or` Sym "->",
diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
index ba90021..b57d54d 100644
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@@ -149,6 +149,12 @@ export
 qty : FileName -> Grammar True PQty
 qty fname = withLoc fname [|PQ qtyVal|]
 
+export
+exactName : String -> Grammar True ()
+exactName name = terminal "expected '\{name}'" $ \case
+  Name (MakePName [<] x) => guard $ x == name
+  _                      => Nothing
+
 
 ||| pattern var (unqualified name or _)
 export
@@ -576,6 +582,15 @@ term fname = lamTerm fname
          <|> sigmaTerm fname
 
 
+export
+pragma : Grammar True a -> Grammar True a
+pragma p = resC "@[" *> p <* mustWork (resC "]")
+
+export
+declMod : FileName -> Grammar True PDeclMod
+declMod fname = withLoc fname $ pragma $
+  exactName "fail" *> [|PFail $ optional strLit|]
+
 export
 decl : FileName -> Grammar True PDecl
 
@@ -610,7 +625,11 @@ where
   nsInner = [] <$ resC "}"
         <|> [|(assert_total decl fname <* commit) :: assert_total nsInner|]
 
-decl fname = [|PDef $ definition fname|] <|> [|PNs $ namespace_ fname|]
+export
+declBody : FileName -> Grammar True PDeclBody
+declBody fname = [|PDef $ definition fname|] <|> [|PNs $ namespace_ fname|]
+
+decl fname = withLoc fname [|MkPDecl (many $ declMod fname) (declBody fname)|]
 
 export
 load : FileName -> Grammar True PTopLevel
diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr
index b95e351..af92211 100644
--- a/lib/Quox/Parser/Syntax.idr
+++ b/lib/Quox/Parser/Syntax.idr
@@ -153,6 +153,12 @@ record PDefinition where
 
 export Located PDefinition where def.loc = def.loc_
 
+public export
+data PDeclMod =
+    PFail (Maybe String) Loc
+%name PDeclMod mod
+%runElab derive "PDeclMod" [Eq, Ord, Show]
+
 mutual
   public export
   record PNamespace where
@@ -163,18 +169,27 @@ mutual
   %name PNamespace ns
 
   public export
-  data PDecl =
-      PDef PDefinition
-    | PNs  PNamespace
-  %name PDecl decl
-%runElab deriveMutual ["PNamespace", "PDecl"] [Eq, Ord, Show]
+  record PDecl where
+    constructor MkPDecl
+    mods : List PDeclMod
+    decl : PDeclBody
+    loc_ : Loc
+
+  public export
+  data PDeclBody =
+      PDef  PDefinition
+    | PNs   PNamespace
+  %name PDeclBody decl
+%runElab deriveMutual ["PNamespace", "PDecl", "PDeclBody"] [Eq, Ord, Show]
 
 export Located PNamespace where ns.loc = ns.loc_
 
+export Located PDecl where decl.loc = decl.loc_
+
 export
-Located PDecl where
-  (PDef def).loc = def.loc
-  (PNs  ns).loc  = ns.loc
+Located PDeclBody where
+  (PDef  def).loc  = def.loc
+  (PNs   ns).loc   = ns.loc
 
 public export
 data PTopLevel = PD PDecl | PLoad String Loc
diff --git a/lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr b/lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr
index 9e276d6..c986889 100644
--- a/lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr
+++ b/lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr
@@ -5,6 +5,7 @@ module Text.PrettyPrint.Bernardy.Core.Decorate
 
 import public Text.PrettyPrint.Bernardy.Core
 import Data.DPair
+import Data.String
 
 
 public export
@@ -43,3 +44,12 @@ decorateLayout h l@(MkLayout content stats) =
 export
 decorate : {opts : _} -> Highlight -> Doc opts -> Doc opts
 decorate h doc = doc >>= \l => pure (decorateLayout h l)
+
+
+||| render a doc with no line breaks at all
+export
+renderInfinite : Doc opts -> String
+renderInfinite (MkDoc (MkLayout content _) _) = unwords content where
+  unwords : SnocList String -> String
+  unwords [<]       = ""
+  unwords (xs :< x) = foldMap (++ " ") xs ++ x