From 9d60f366cf7ac3727ec09ec0ee2daff394001413 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Fri, 12 Apr 2024 21:49:15 +0200 Subject: [PATCH] add #![log] pragma --- lib/Quox/Log.idr | 4 +- lib/Quox/Parser/FromParser.idr | 4 ++ lib/Quox/Parser/Lexer.idr | 2 +- lib/Quox/Parser/Parser.idr | 107 +++++++++++++++++++++++++-------- lib/Quox/Parser/Syntax.idr | 23 +++++-- lib/Quox/PrettyValExtra.idr | 10 +++ tests/Tests/Parser.idr | 48 ++++++++++++++- 7 files changed, 164 insertions(+), 34 deletions(-) diff --git a/lib/Quox/Log.idr b/lib/Quox/Log.idr index bfe5d26..6630bb6 100644 --- a/lib/Quox/Log.idr +++ b/lib/Quox/Log.idr @@ -2,6 +2,7 @@ module Quox.Log import Quox.Loc import Quox.Pretty +import Quox.PrettyValExtra import Data.So import Data.DPair @@ -90,7 +91,7 @@ record LogLevels where defLevel : LogLevel levels : LevelMap %name LogLevels lvls -%runElab derive "LogLevels" [Eq, Show] +%runElab derive "LogLevels" [Eq, Show, PrettyVal] public export LevelStack : Type @@ -142,6 +143,7 @@ data PushArg = SetDefault LogLevel | SetCat LogCategory LogLevel | SetAll LogLevel +%runElab derive "PushArg" [Eq, Ord, Show, PrettyVal] %name PushArg push export %inline diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr index 08a7210..ddf8671 100644 --- a/lib/Quox/Parser/FromParser.idr +++ b/lib/Quox/Parser/FromParser.idr @@ -398,6 +398,10 @@ fromPDecl (PDef def) = fromPDecl (PNs ns) = maybeFail ns.fail ns.loc $ localAt NS (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls +fromPDecl (PPrag prag) = + case prag of + PLogPush p _ => Log.push p $> [] + PLogPop _ => Log.pop $> [] mutual export covering diff --git a/lib/Quox/Parser/Lexer.idr b/lib/Quox/Parser/Lexer.idr index afd6df5..f4a4ee0 100644 --- a/lib/Quox/Parser/Lexer.idr +++ b/lib/Quox/Parser/Lexer.idr @@ -247,7 +247,7 @@ public export reserved : List Reserved reserved = [Punc1 "(", Punc1 ")", Punc1 "[", Punc1 "]", Punc1 "{", Punc1 "}", - Punc1 ",", Punc1 ";", Punc1 "#[", + Punc1 ",", Punc1 ";", Punc1 "#[", Punc1 "#![", Sym1 "@", Sym1 ":", Sym "⇒" `Or` Sym "=>", diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr index 44b5833..6035d57 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/lib/Quox/Parser/Parser.idr @@ -626,14 +626,19 @@ term fname = lamTerm fname export -attr : FileName -> Grammar True PAttr -attr fname = withLoc fname $ do - resC "#[" +attr' : FileName -> (o : String) -> (0 _ : IsReserved o) => + Grammar True PAttr +attr' fname o = withLoc fname $ do + resC o name <- baseName args <- many $ termArg fname mustWork $ resC "]" pure $ PA name args +export %inline +attr : FileName -> Grammar True PAttr +attr fname = attr' fname "#[" + export findDups : List PAttr -> List String findDups attrs = @@ -658,44 +663,48 @@ attrList fname = do noDups res $> res public export -data AttrMatch a = Matched a | NoMatch String | Malformed String String +data AttrMatch a = + Matched a + | NoMatch String (List String) + | Malformed String String export Functor AttrMatch where map f (Matched x) = Matched $ f x - map f (NoMatch s) = NoMatch s + map f (NoMatch s w) = NoMatch s w map f (Malformed a e) = Malformed a e export (<|>) : AttrMatch a -> AttrMatch a -> AttrMatch a Matched x <|> _ = Matched x -NoMatch _ <|> y = y +NoMatch {} <|> y = y Malformed a e <|> _ = Malformed a e export -isFail : PAttr -> AttrMatch PFail -isFail (PA "fail" [] _) = Matched PFailAny -isFail (PA "fail" [Str s _] _) = Matched $ PFailMatch s -isFail (PA "fail" _ _) = Malformed "fail" "be absent or a string literal" -isFail a = NoMatch a.name +isFail : PAttr -> List String -> AttrMatch PFail +isFail (PA "fail" [] _) _ = Matched PFailAny +isFail (PA "fail" [Str s _] _) _ = Matched $ PFailMatch s +isFail (PA "fail" _ _) _ = Malformed "fail" "be absent or a string literal" +isFail a w = NoMatch a.name w export -isMain : PAttr -> AttrMatch () -isMain (PA "main" [] _) = Matched () -isMain (PA "main" _ _) = Malformed "main" "have no arguments" -isMain a = NoMatch a.name +isMain : PAttr -> List String -> AttrMatch () +isMain (PA "main" [] _) _ = Matched () +isMain (PA "main" _ _) _ = Malformed "main" "have no arguments" +isMain a w = NoMatch a.name w export -isScheme : PAttr -> AttrMatch String -isScheme (PA "compile-scheme" [Str s _] _) = Matched s -isScheme (PA "compile-scheme" _ _) = +isScheme : PAttr -> List String -> AttrMatch String +isScheme (PA "compile-scheme" [Str s _] _) _ = Matched s +isScheme (PA "compile-scheme" _ _) _ = Malformed "compile-scheme" "be a string literal" -isScheme a = NoMatch a.name +isScheme a w = NoMatch a.name w export matchAttr : String -> AttrMatch a -> Either String a matchAttr _ (Matched x) = Right x -matchAttr d (NoMatch a) = Left "unrecognised \{d} attribute \{a}" +matchAttr d (NoMatch a w) = Left $ unlines + ["unrecognised \{d} attribute \{a}", "expected one of: \{show w}"] matchAttr _ (Malformed a s) = Left $ unlines ["invalid \{a} attribute", "(should \{s})"] @@ -710,10 +719,12 @@ where data PDefAttr = DefFail PFail | DefMain | DefScheme String isDefAttr : PAttr -> Either String PDefAttr - isDefAttr attr = matchAttr "definition" $ - DefFail <$> isFail attr - <|> DefMain <$ isMain attr - <|> DefScheme <$> isScheme attr + isDefAttr attr = + let defAttrs = ["fail", "main", "compile-scheme"] in + matchAttr "definition" $ + DefFail <$> isFail attr defAttrs + <|> DefMain <$ isMain attr defAttrs + <|> DefScheme <$> isScheme attr defAttrs addAttr : PDefinition -> PAttr -> Either String PDefinition addAttr def attr = @@ -730,7 +741,7 @@ mkPNamespace attrs name decls = do res <- foldlM addAttr start attrs pure $ \l => {loc_ := l} (the PNamespace res) where - isNsAttr = matchAttr "namespace" . isFail + isNsAttr a = matchAttr "namespace" $ isFail a ["fail"] addAttr : PNamespace -> PAttr -> Either String PNamespace addAttr ns attr = pure $ {fail := !(isNsAttr attr)} ns @@ -785,6 +796,48 @@ export nsname : Grammar True Mods nsname = do ns <- qname; pure $ ns.mods :< ns.base +export +pragma : FileName -> Grammar True PPragma +pragma fname = do + a <- attr' fname "#![" + either fatalError pure $ case a.name of + "log" => logArgs a.args a.loc + _ => Left $ + #"unrecognised pragma "\#{a.name}"\n"# ++ + #"known pragmas: ["log"]"# +where + levelOOB : Nat -> Either String a + levelOOB n = Left $ + "log level \{show n} out of bounds\n" ++ + "expected number in range 0–\{show maxLogLevel} inclusive" + + toLevel : Nat -> Either String LogLevel + toLevel lvl = maybe (levelOOB lvl) Right $ toLogLevel lvl + + unknownCat : String -> Either String a + unknownCat cat = Left $ + "unknown log category \{show cat}\n" ++ + "known categories: \{show $ ["all", "default"] ++ logCategories}" + + toCat : String -> Either String LogCategory + toCat cat = maybe (unknownCat cat) Right $ toLogCategory cat + + fromPair : PTerm -> Either String (String, Nat) + fromPair (Pair (V (MkPName [<] x) Nothing _) (Nat n _) _) = Right (x, n) + fromPair _ = Left "invalid argument to log pragma" + + logCatArg : (String, Nat) -> Either String Log.PushArg + logCatArg ("default", lvl) = [|SetDefault $ toLevel lvl|] + logCatArg ("all", lvl) = [|SetAll $ toLevel lvl|] + logCatArg (cat, lvl) = [|SetCat (toCat cat) (toLevel lvl)|] + + logArgs : List PTerm -> Loc -> Either String PPragma + logArgs [] _ = Left "missing arguments to log pragma" + logArgs [V "pop" Nothing _] loc = Right $ PLogPop loc + logArgs other loc = do + args <- traverse (logCatArg <=< fromPair) other + pure $ PLogPush args loc + export decl : FileName -> Grammar True PDecl @@ -806,7 +859,9 @@ declBody fname attrs = [|PDef $ definition fname attrs|] <|> [|PNs $ namespace_ fname attrs|] -- decl : FileName -> Grammar True PDecl -decl fname = attrList fname >>= declBody fname +decl fname = + (attrList fname >>= declBody fname) + <|> PPrag <$> pragma fname export load : FileName -> Grammar True PTopLevel diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr index 4011ac5..9c8609f 100644 --- a/lib/Quox/Parser/Syntax.idr +++ b/lib/Quox/Parser/Syntax.idr @@ -4,6 +4,7 @@ import public Quox.Loc import public Quox.Syntax import public Quox.Definition import Quox.PrettyValExtra +import public Quox.Log import Derive.Prelude %hide TT.Name @@ -184,6 +185,18 @@ record PDefinition where export Located PDefinition where def.loc = def.loc_ +public export +data PPragma = + PLogPush (List Log.PushArg) Loc + | PLogPop Loc +%name PPragma prag +%runElab derive "PPragma" [Eq, Ord, Show, PrettyVal] + +export +Located PPragma where + (PLogPush _ loc).loc = loc + (PLogPop loc).loc = loc + mutual public export record PNamespace where @@ -196,8 +209,9 @@ mutual public export data PDecl = - PDef PDefinition - | PNs PNamespace + PDef PDefinition + | PNs PNamespace + | PPrag PPragma %name PDecl decl %runElab deriveMutual ["PNamespace", "PDecl"] [Eq, Ord, Show, PrettyVal] @@ -205,8 +219,9 @@ export Located PNamespace where ns.loc = ns.loc_ export Located PDecl where - (PDef d).loc = d.loc - (PNs ns).loc = ns.loc + (PDef d).loc = d.loc + (PNs ns).loc = ns.loc + (PPrag prag).loc = prag.loc public export data PTopLevel = PD PDecl | PLoad String Loc diff --git a/lib/Quox/PrettyValExtra.idr b/lib/Quox/PrettyValExtra.idr index afd210e..8ef7366 100644 --- a/lib/Quox/PrettyValExtra.idr +++ b/lib/Quox/PrettyValExtra.idr @@ -1,5 +1,6 @@ module Quox.PrettyValExtra +import Data.DPair import Derive.Prelude import public Text.Show.Value import public Text.Show.PrettyVal @@ -8,3 +9,12 @@ import public Text.Show.PrettyVal.Derive %language ElabReflection %runElab derive "SnocList" [PrettyVal] + + +export %inline +PrettyVal a => PrettyVal (Subset a p) where + prettyVal (Element x _) = Con "Element" [prettyVal x, Con "_" []] + +export %inline +(forall x. PrettyVal (p x)) => PrettyVal (Exists p) where + prettyVal (Evidence _ p) = Con "Evidence" [Con "_" [], prettyVal p] diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index e4f6d88..7bbca5d 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -531,7 +531,51 @@ tests = "parser" :- [ parseMatch input #" load "a.quox"; def b = a.b "# `([PLoad "a.quox" _, PD (PDef $ MkPDef (PQ Any _) "b" - (PConcrete Nothing (V (MakePName [< "a"] "b") Nothing _)) - PSucceed False Nothing _)]) + (PConcrete Nothing (V (MkPName [< "a"] "b") Nothing _)) + PSucceed False Nothing _)]), + parseMatch input #" #[main] postulate hi : String "# + `([PD (PDef $ MkPDef (PQ Any _) "hi" + (PPostulate (STRING _)) + PSucceed True Nothing _)]), + parseMatch input #" #[compile-scheme "hi"] postulate hi : String "# + `([PD (PDef $ MkPDef (PQ Any _) "hi" + (PPostulate (STRING _)) + PSucceed False (Just "hi") _)]), + parseMatch input #" #[main] #[compile-scheme "hi"] postulate hi : String "# + `([PD (PDef $ MkPDef (PQ Any _) "hi" + (PPostulate (STRING _)) + PSucceed True (Just "hi") _)]), + parseMatch input #" #[fail] def hi = "hi!!!! uwu" "# + `([PD (PDef $ MkPDef (PQ Any _) "hi" + (PConcrete Nothing (Str "hi!!!! uwu" _)) + PFailAny False Nothing _)]), + parseMatch input #" #[fail "type"] def hi = "hi!!!! uwu" "# + `([PD (PDef $ MkPDef (PQ Any _) "hi" + (PConcrete Nothing (Str "hi!!!! uwu" _)) + (PFailMatch "type") False Nothing _)]), + parseMatch input #" #[fail] namespace ns { } "# + `([PD (PNs $ MkPNamespace [< "ns"] [] PFailAny _)]), + parseFails input #" #[fail 69] namespace ns { } "#, + parseFails input "#[main]", + parseFails input "#[main] namespace a { } ", + parseFails input #" #[not-an-attr] postulate hi : String "#, + parseFails input #" #[log pop] postulate hi : String "#, + parseMatch input #" #![log pop] "# + `([PD (PPrag (PLogPop _))]), + parseMatch input #" #![log (all, 5)] "# + `([PD (PPrag (PLogPush [SetAll (Element 5 _)] _))]), + parseMatch input #" #![log (default, 69)] "# + `([PD (PPrag (PLogPush [SetDefault (Element 69 _)] _))]), + parseMatch input #" #![log (whnf, 100)] "# + `([PD (PPrag (PLogPush [SetCat (Element "whnf" _) (Element 100 _)] _))]), + parseMatch input #" #![log (all, 5) (default, 69) (whnf, 100)] "# + `([PD (PPrag (PLogPush + [SetAll (Element 5 _), SetDefault (Element 69 _), + SetCat (Element "whnf" _) (Element 100 _)] _))]), + parseFails input #" #![log] "#, + parseFails input #" #![log (non-category, 5)] "#, + parseFails input #" #![log (whnf, 50000000)] "#, + parseFails input #" #![log [0.★⁵]] "#, + parseFails input #" #![main] "# ] ]