From 50984aa1aaadbe12e0d68079ef277738f16de636 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 5 Nov 2023 20:49:02 +0100 Subject: [PATCH] refactor #[attribute] stuff --- lib/Quox/Parser/FromParser.idr | 90 +++++++------------ lib/Quox/Parser/Parser.idr | 159 +++++++++++++++++++++++++++------ lib/Quox/Parser/Syntax.idr | 65 +++++++------- tests/Tests/Parser.idr | 83 ++++++++--------- 4 files changed, 237 insertions(+), 160 deletions(-) diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr index 8b312e4..d96645c 100644 --- a/lib/Quox/Parser/FromParser.idr +++ b/lib/Quox/Parser/FromParser.idr @@ -311,8 +311,8 @@ fromPTerm = fromPTermWith [<] [<] export -globalPQty : Has (Except Error) fs => (q : Qty) -> Loc -> Eff fs GQty -globalPQty pi loc = case toGlobal pi of +globalPQty : Has (Except Error) fs => PQty -> Eff fs GQty +globalPQty (PQ pi loc) = case toGlobal pi of Just g => pure g Nothing => throw $ QtyNotGlobal loc pi @@ -336,15 +336,14 @@ addDef name def = do export covering -fromPDef : PDefinition -> Maybe String -> Bool -> - Eff FromParserPure NDefinition -fromPDef (MkPDef qty pname pbody defLoc) scheme isMain = do - name <- fromPBaseNameNS pname +fromPDef : PDefinition -> Eff FromParserPure NDefinition +fromPDef def = do + name <- fromPBaseNameNS def.name when !(getsAt DEFS $ isJust . lookup name) $ do - throw $ AlreadyExists defLoc name - gqty <- globalPQty qty.val qty.loc + throw $ AlreadyExists def.loc name + gqty <- globalPQty def.qty let sqty = globalToSubj gqty - case pbody of + case def.body of PConcrete ptype pterm => do type <- traverse fromPTerm ptype term <- fromPTerm pterm @@ -353,72 +352,47 @@ fromPDef (MkPDef qty pname pbody defLoc) scheme isMain = do ignore $ liftTC $ do checkTypeC empty type Nothing checkC empty sqty term type - addDef name $ mkDef gqty type term scheme isMain defLoc + addDef name $ mkDef gqty type term def.scheme def.main def.loc Nothing => do let E elim = term | _ => throw $ AnnotationNeeded term.loc empty term res <- liftTC $ inferC empty sqty elim - addDef name $ mkDef gqty res.type term scheme isMain defLoc + addDef name $ mkDef gqty res.type term def.scheme def.main def.loc PPostulate ptype => do type <- fromPTerm ptype - addDef name $ mkPostulate gqty type scheme isMain defLoc + addDef name $ mkPostulate gqty type def.scheme def.main def.loc public export data HasFail = NoFail | AnyFail | FailWith String -export -hasFail : List PDeclMod -> HasFail -hasFail [] = NoFail -hasFail (PFail str :: _) = maybe AnyFail FailWith str -hasFail (_ :: rest) = hasFail rest +export covering +expectFail : Loc -> Eff FromParserPure a -> Eff FromParserPure Error +expectFail loc act = + case fromParserPure !(getAt GEN) !(getAt DEFS) act of + Left err => pure err + Right _ => throw $ ExpectedFail loc -export -getScheme : List PDeclMod -> Maybe String -getScheme [] = Nothing -getScheme (PCompileScheme str :: _) = Just str -getScheme (_ :: rest) = getScheme rest - -export -isMain : List PDeclMod -> Bool -isMain [] = False -isMain (PMain :: _) = True -isMain (_ :: rest) = isMain rest +export covering +maybeFail : Monoid a => + PFail -> Loc -> Eff FromParserPure a -> Eff FromParserPure a +maybeFail PSucceed _ act = act +maybeFail PFailAny loc act = expectFail loc act $> neutral +maybeFail (PFailMatch str) loc act = do + err <- expectFail loc act + let msg = runPretty $ prettyError False err {opts = Opts 10_000} -- w/e + if str `isInfixOf` renderInfinite msg + then pure neutral + else throw $ WrongFail str err loc export covering fromPDecl : PDecl -> Eff FromParserPure (List NDefinition) - -export covering -fromPDeclBody : PDeclBody -> Maybe String -> Bool -> Loc -> - Eff FromParserPure (List NDefinition) -fromPDeclBody (PDef def) scheme isMain loc = - singleton <$> fromPDef def scheme isMain -fromPDeclBody (PNs ns) scheme isMain loc = do - when (isJust scheme) $ throw $ SchemeOnNamespace loc ns.name - when isMain $ throw $ MainOnNamespace loc ns.name +fromPDecl (PDef def) = + maybeFail def.fail def.loc $ singleton <$> fromPDef def +fromPDecl (PNs ns) = + maybeFail ns.fail ns.loc $ localAt NS (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls -export covering -expectFail : PDeclBody -> Loc -> Eff FromParserPure Error -expectFail body loc = - let res = fromParserPure !(getAt GEN) !(getAt DEFS) $ - fromPDeclBody body Nothing False loc in - case res of - Left err => pure err - Right _ => throw $ ExpectedFail body.loc - - -fromPDecl (MkPDecl mods decl loc) = case hasFail mods of - NoFail => fromPDeclBody decl (getScheme mods) (isMain mods) loc - AnyFail => expectFail decl loc $> [] - FailWith str => do - err <- expectFail decl loc - 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) diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr index 030c2ec..de94618 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/lib/Quox/Parser/Parser.idr @@ -577,7 +577,6 @@ caseTerm fname = withLoc fname $ do body <- mustWork $ caseBody fname pure $ Case qty head ret body --- export -- term : FileName -> Grammar True PTerm term fname = lamTerm fname <|> caseTerm fname @@ -586,20 +585,114 @@ term fname = lamTerm fname export -pragma : Grammar True a -> Grammar True a -pragma p = resC "#[" *> p <* mustWork (resC "]") +attr : FileName -> Grammar True PAttr +attr fname = withLoc fname $ do + resC "#[" + name <- baseName + args <- many $ termArg fname + mustWork $ resC "]" + pure $ PA name args export -declMod : Grammar True PDeclMod -declMod = pragma $ - exactName "fail" *> [|PFail $ optional strLit|] - <|> exactName "compile-scheme" *> [|PCompileScheme strLit|] - <|> exactName "main" $> PMain - <|> do other <- qname - fatalError "unknown declaration flag \{show other}" {c = False} +findDups : List PAttr -> List String +findDups attrs = + SortedSet.toList $ snd $ foldl check (empty, empty) attrs +where + Seen = SortedSet String; Dups = SortedSet String + check : (Seen, Dups) -> PAttr -> (Seen, Dups) + check (seen, dups) (PA a _ _) = + (insert a seen, if contains a seen then insert a dups else dups) export -decl : FileName -> Grammar True PDecl +noDups : List PAttr -> Grammar False () +noDups attrs = do + let dups = findDups attrs + when (not $ null dups) $ + fatalError "duplicate attribute names: \{joinBy "," dups}" + +export +attrList : FileName -> Grammar False (List PAttr) +attrList fname = do + res <- many $ attr fname + noDups res $> res + +public export +data AttrMatch a = Matched a | NoMatch String | Malformed String String + +export +Functor AttrMatch where + map f (Matched x) = Matched $ f x + map f (NoMatch s) = NoMatch s + map f (Malformed a e) = Malformed a e + +export +(<|>) : AttrMatch a -> AttrMatch a -> AttrMatch a +Matched x <|> _ = Matched x +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 + +export +isMain : PAttr -> AttrMatch () +isMain (PA "main" [] _) = Matched () +isMain (PA "main" _ _) = Malformed "main" "have no arguments" +isMain a = NoMatch a.name + +export +isScheme : PAttr -> 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 + +export +matchAttr : String -> AttrMatch a -> Either String a +matchAttr _ (Matched x) = Right x +matchAttr d (NoMatch a) = Left "unrecognised \{d} attribute \{a}" +matchAttr _ (Malformed a s) = Left $ unlines + ["invalid \{a} attribute", "(should \{s})"] + +export +mkPDef : List PAttr -> PQty -> PBaseName -> PBody -> + Either String (Loc -> PDefinition) +mkPDef attrs qty name body = do + let start = MkPDef qty name body PSucceed False Nothing noLoc + res <- foldlM addAttr start attrs + pure $ \l => {loc_ := l} (the PDefinition res) +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 + + addAttr : PDefinition -> PAttr -> Either String PDefinition + addAttr def attr = + case !(isDefAttr attr) of + DefFail f => pure $ {fail := f} def + DefMain => pure $ {main := True} def + DefScheme str => pure $ {scheme := Just str} def + +export +mkPNamespace : List PAttr -> Mods -> List PDecl -> + Either String (Loc -> PNamespace) +mkPNamespace attrs name decls = do + let start = MkPNamespace name decls PSucceed noLoc + res <- foldlM addAttr start attrs + pure $ \l => {loc_ := l} (the PNamespace res) +where + isNsAttr = matchAttr "namespace" . isFail + + addAttr : PNamespace -> PAttr -> Either String PNamespace + addAttr ns attr = pure $ {fail := !(isNsAttr attr)} ns ||| `def` alone means `defω`; same for `postulate` export @@ -624,43 +717,55 @@ postulateIntro : FileName -> Grammar True PQty postulateIntro = defIntro' "postulate" "postulate0" "postulateω" export -postulate : FileName -> Grammar True PDefinition -postulate fname = withLoc fname $ Core.do +postulate : FileName -> List PAttr -> Grammar True PDefinition +postulate fname attrs = withLoc fname $ do qty <- postulateIntro fname name <- baseName type <- resC ":" *> mustWork (term fname) - pure $ MkPDef qty name $ PPostulate type + optRes ";" + either fatalError pure $ mkPDef attrs qty name $ PPostulate type export -concrete : FileName -> Grammar True PDefinition -concrete fname = withLoc fname $ do +concrete : FileName -> List PAttr -> Grammar True PDefinition +concrete fname attrs = withLoc fname $ do qty <- defIntro fname name <- baseName type <- optional $ resC ":" *> mustWork (term fname) term <- needRes "=" *> mustWork (term fname) optRes ";" - pure $ MkPDef qty name $ PConcrete type term + either fatalError pure $ mkPDef attrs qty name $ PConcrete type term export -definition : FileName -> Grammar True PDefinition -definition fname = try (postulate fname) <|> concrete fname +definition : FileName -> List PAttr -> Grammar True PDefinition +definition fname attrs = + try (postulate fname attrs) <|> concrete fname attrs export -namespace_ : FileName -> Grammar True PNamespace -namespace_ fname = withLoc fname $ do - ns <- resC "namespace" *> qname; needRes "{" - decls <- nsInner; optRes ";" - pure $ MkPNamespace (ns.mods :< ns.base) decls +nsname : Grammar True Mods +nsname = do ns <- qname; pure $ ns.mods :< ns.base + + +export +decl : FileName -> Grammar True PDecl + +export +namespace_ : FileName -> List PAttr -> Grammar True PNamespace +namespace_ fname attrs = withLoc fname $ do + ns <- resC "namespace" *> nsname; needRes "{" + decls <- nsInner + either fatalError pure $ mkPNamespace attrs ns decls where nsInner : Grammar True (List PDecl) nsInner = [] <$ resC "}" <|> [|(assert_total decl fname <* commit) :: assert_total nsInner|] export -declBody : FileName -> Grammar True PDeclBody -declBody fname = [|PDef $ definition fname|] <|> [|PNs $ namespace_ fname|] +declBody : FileName -> List PAttr -> Grammar True PDecl +declBody fname attrs = + [|PDef $ definition fname attrs|] <|> [|PNs $ namespace_ fname attrs|] -decl fname = withLoc fname [|MkPDecl (many declMod) (declBody fname)|] +-- decl : FileName -> Grammar True PDecl +decl fname = attrList fname >>= declBody fname export load : FileName -> Grammar True PTopLevel diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr index 2b7e19c..3265fd2 100644 --- a/lib/Quox/Parser/Syntax.idr +++ b/lib/Quox/Parser/Syntax.idr @@ -159,58 +159,51 @@ data PBody = PConcrete (Maybe PTerm) PTerm | PPostulate PTerm %runElab derive "PBody" [Eq, Ord, Show, PrettyVal] +public export +data PFail = + PSucceed +| PFailAny +| PFailMatch String +%runElab derive "PFail" [Eq, Ord, Show, PrettyVal] + public export record PDefinition where constructor MkPDef - qty : PQty - name : PBaseName - body : PBody - loc_ : Loc + qty : PQty + name : PBaseName + body : PBody + fail : PFail + main : Bool + scheme : Maybe String + loc_ : Loc %name PDefinition def %runElab derive "PDefinition" [Eq, Ord, Show, PrettyVal] export Located PDefinition where def.loc = def.loc_ -public export -data PDeclMod = - PFail (Maybe String) - | PCompileScheme String - | PMain -%name PDeclMod mod -%runElab derive "PDeclMod" [Eq, Ord, Show, PrettyVal] - mutual public export record PNamespace where constructor MkPNamespace name : Mods decls : List PDecl + fail : PFail loc_ : Loc %name PNamespace ns public export - 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, PrettyVal] + data PDecl = + PDef PDefinition + | PNs PNamespace + %name PDecl decl +%runElab deriveMutual ["PNamespace", "PDecl"] [Eq, Ord, Show, PrettyVal] export Located PNamespace where ns.loc = ns.loc_ -export Located PDecl where decl.loc = decl.loc_ - export -Located PDeclBody where - (PDef def).loc = def.loc - (PNs ns).loc = ns.loc +Located PDecl where + (PDef d).loc = d.loc + (PNs ns).loc = ns.loc public export data PTopLevel = PD PDecl | PLoad String Loc @@ -223,6 +216,18 @@ Located PTopLevel where (PLoad _ loc).loc = loc +public export +record PAttr where + constructor PA + name : PBaseName + args : List PTerm + loc_ : Loc +%name PAttr attr +%runElab derive "PAttr" [Eq, Ord, Show, PrettyVal] + +export Located PAttr where attr.loc = attr.loc_ + + public export PFile : Type PFile = List PTopLevel diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index 299c905..4736e89 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -395,36 +395,37 @@ tests = "parser" :- [ parseFails term "caseω n return ℕ of { succ ⇒ 5 }" ], - "definitions" :- [ + "definitions" :- + let definition = flip definition [] in [ parseMatch definition "defω x : {a} × {b} = ('a, 'b);" `(MkPDef (PQ Any _) "x" (PConcrete (Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _)) - (Pair (Tag "a" _) (Tag "b" _) _)) _), + (Pair (Tag "a" _) (Tag "b" _) _)) _ _ _ _), parseMatch definition "def# x : {a} ** {b} = ('a, 'b)" `(MkPDef (PQ Any _) "x" (PConcrete (Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _)) - (Pair (Tag "a" _) (Tag "b" _) _)) _), + (Pair (Tag "a" _) (Tag "b" _) _)) _ _ _ _), parseMatch definition "def ω.x : {a} × {b} = ('a, 'b)" `(MkPDef (PQ Any _) "x" (PConcrete (Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _)) - (Pair (Tag "a" _) (Tag "b" _) _)) _), + (Pair (Tag "a" _) (Tag "b" _) _)) _ _ _ _), parseMatch definition "def x : {a} × {b} = ('a, 'b)" `(MkPDef (PQ Any _) "x" (PConcrete (Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _)) - (Pair (Tag "a" _) (Tag "b" _) _)) _), + (Pair (Tag "a" _) (Tag "b" _) _)) _ _ _ _), parseMatch definition "def0 A : ★⁰ = {a, b, c}" `(MkPDef (PQ Zero _) "A" - (PConcrete (Just $ TYPE 0 _) (Enum ["a", "b", "c"] _)) _), + (PConcrete (Just $ TYPE 0 _) (Enum ["a", "b", "c"] _)) _ _ _ _), parseMatch definition "postulate yeah : ℕ" - `(MkPDef (PQ Any _) "yeah" (PPostulate (NAT _)) _), + `(MkPDef (PQ Any _) "yeah" (PPostulate (NAT _)) _ _ _ _), parseMatch definition "postulateω yeah : ℕ" - `(MkPDef (PQ Any _) "yeah" (PPostulate (NAT _)) _), + `(MkPDef (PQ Any _) "yeah" (PPostulate (NAT _)) _ _ _ _), parseMatch definition "postulate0 FileHandle : ★" - `(MkPDef (PQ Zero _) "FileHandle" (PPostulate (TYPE 0 _)) _), + `(MkPDef (PQ Zero _) "FileHandle" (PPostulate (TYPE 0 _)) _ _ _ _), parseFails definition "postulate not-a-postulate : ℕ = 69", parseFails definition "postulate not-a-postulate = 69", parseFails definition "def not-a-def : ℕ" @@ -432,52 +433,44 @@ tests = "parser" :- [ "top level" :- [ parseMatch input "def0 A : ★⁰ = {}; def0 B : ★¹ = A;" - `([PD $ MkPDecl [] - (PDef $ MkPDef (PQ Zero _) "A" - (PConcrete (Just $ TYPE 0 _) (Enum [] _)) _) _, - PD $ MkPDecl [] - (PDef $ MkPDef (PQ Zero _) "B" - (PConcrete (Just $ TYPE 1 _) (V "A" {})) _) _]), + `([PD $ PDef $ MkPDef (PQ Zero _) "A" + (PConcrete (Just $ TYPE 0 _) (Enum [] _)) PSucceed False Nothing _, + PD $ PDef $ MkPDef (PQ Zero _) "B" + (PConcrete (Just $ TYPE 1 _) (V "A" {})) PSucceed False Nothing _]), parseMatch input "def0 A : ★⁰ = {} def0 B : ★¹ = A" $ - `([PD $ MkPDecl [] - (PDef $ MkPDef (PQ Zero _) "A" - (PConcrete (Just $ TYPE 0 _) (Enum [] _)) _) _, - PD $ MkPDecl [] - (PDef $ MkPDef (PQ Zero _) "B" - (PConcrete (Just $ TYPE 1 _) (V "A" {})) _) _]), + `([PD $ PDef $ MkPDef (PQ Zero _) "A" + (PConcrete (Just $ TYPE 0 _) (Enum [] _)) PSucceed False Nothing _, + PD $ PDef $ MkPDef (PQ Zero _) "B" + (PConcrete (Just $ TYPE 1 _) (V "A" {})) PSucceed False Nothing _]), note "empty input", parsesAs input "" [], parseFails input ";;;;;;;;;;;;;;;;;;;;;;;;;;", parseMatch input "namespace a {}" - `([PD $ MkPDecl [] (PNs $ MkPNamespace [< "a"] [] _) _]), + `([PD $ PNs $ MkPNamespace [< "a"] [] PSucceed _]), parseMatch input "namespace a.b.c {}" - `([PD $ MkPDecl [] - (PNs $ MkPNamespace [< "a", "b", "c"] [] _) _]), + `([PD $ PNs $ MkPNamespace [< "a", "b", "c"] [] PSucceed _]), parseMatch input "namespace a {namespace b {}}" - `([PD (MkPDecl [] - (PNs $ MkPNamespace [< "a"] - [MkPDecl [] (PNs $ MkPNamespace [< "b"] [] _) _] _) _)]), + `([PD (PNs $ MkPNamespace [< "a"] + [PNs $ MkPNamespace [< "b"] [] PSucceed _] PSucceed _)]), parseMatch input "namespace a {def x = 't ∷ {t}}" - `([PD (MkPDecl [] - (PNs $ MkPNamespace [< "a"] - [MkPDecl [] - (PDef $ MkPDef (PQ Any _) "x" - (PConcrete Nothing - (Ann (Tag "t" _) (Enum ["t"] _) _)) _) _] _) _)]), + `([PD (PNs $ MkPNamespace [< "a"] + [PDef $ MkPDef (PQ Any _) "x" + (PConcrete Nothing (Ann (Tag "t" _) (Enum ["t"] _) _)) + PSucceed False Nothing _] + PSucceed _)]), parseMatch input "namespace a {def x : {t} = 't} def y = a.x" - `([PD (MkPDecl [] - (PNs $ MkPNamespace [< "a"] - [MkPDecl [] - (PDef $ MkPDef (PQ Any _) "x" - (PConcrete (Just (Enum ["t"] _)) - (Tag "t" _)) _) _] _) _), - PD (MkPDecl [] - (PDef $ MkPDef (PQ Any _) "y" - (PConcrete Nothing (V (MakePName [< "a"] "x") Nothing _)) _) _)]), + `([PD (PNs $ MkPNamespace [< "a"] + [PDef $ MkPDef (PQ Any _) "x" + (PConcrete (Just (Enum ["t"] _)) (Tag "t" _)) + PSucceed False Nothing _] + PSucceed _), + PD (PDef $ MkPDef (PQ Any _) "y" + (PConcrete Nothing (V (MakePName [< "a"] "x") Nothing _)) + PSucceed False Nothing _)]), parseMatch input #" load "a.quox"; def b = a.b "# `([PLoad "a.quox" _, - PD (MkPDecl [] - (PDef $ MkPDef (PQ Any _) "b" - (PConcrete Nothing (V (MakePName [< "a"] "b") Nothing _)) _) _)]) + PD (PDef $ MkPDef (PQ Any _) "b" + (PConcrete Nothing (V (MakePName [< "a"] "b") Nothing _)) + PSucceed False Nothing _)]) ] ]