refactor #[attribute] stuff

lib/Quox/Parser/FromParser.idr

@@ -311,8 +311,8 @@ fromPTerm = fromPTermWith [<] [<]
 
 
 export
-globalPQty : Has (Except Error) fs => (q : Qty) -> Loc -> Eff fs GQty
+globalPQty : Has (Except Error) fs => PQty -> Eff fs GQty
-globalPQty pi loc = case toGlobal pi of
+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 ->
+fromPDef : PDefinition -> Eff FromParserPure NDefinition
-           Eff FromParserPure NDefinition
+fromPDef def = do
-fromPDef (MkPDef qty pname pbody defLoc) scheme isMain = do
+  name <- fromPBaseNameNS def.name
-  name <- fromPBaseNameNS pname
   when !(getsAt DEFS $ isJust . lookup name) $ do
-    throw $ AlreadyExists defLoc name
+    throw $ AlreadyExists def.loc name
-  gqty <- globalPQty qty.val qty.loc
+  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
+export covering
-hasFail : List PDeclMod -> HasFail
+expectFail : Loc -> Eff FromParserPure a -> Eff FromParserPure Error
-hasFail []               = NoFail
+expectFail loc act =
-hasFail (PFail str :: _) = maybe AnyFail FailWith str
+  case fromParserPure !(getAt GEN) !(getAt DEFS) act of
-hasFail (_ :: rest)      = hasFail rest
+    Left  err => pure err
+    Right _   => throw $ ExpectedFail loc
 
-export
+export covering
-getScheme : List PDeclMod -> Maybe String
+maybeFail : Monoid a =>
-getScheme []                        = Nothing
+            PFail -> Loc -> Eff FromParserPure a -> Eff FromParserPure a
-getScheme (PCompileScheme str :: _) = Just str
+maybeFail PSucceed         _   act = act
-getScheme (_ :: rest)               = getScheme rest
+maybeFail PFailAny         loc act = expectFail loc act $> neutral
-
+maybeFail (PFailMatch str) loc act = do
-export
+    err <- expectFail loc act
-isMain : List PDeclMod -> Bool
+    let msg = runPretty $ prettyError False err {opts = Opts 10_000} -- w/e
-isMain []           = False
+    if str `isInfixOf` renderInfinite msg
-isMain (PMain :: _) = True
+       then pure neutral
-isMain (_ :: rest)  = isMain rest
+       else throw $ WrongFail str err loc
 
 export covering
 fromPDecl : PDecl -> Eff FromParserPure (List NDefinition)
-
+fromPDecl (PDef def) =
-export covering
+  maybeFail def.fail def.loc $ singleton <$> fromPDef def
-fromPDeclBody : PDeclBody -> Maybe String -> Bool -> Loc ->
+fromPDecl (PNs  ns)  =
-                Eff FromParserPure (List NDefinition)
+  maybeFail ns.fail ns.loc $
-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
   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)

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
+attr : FileName -> Grammar True PAttr
-pragma p = resC "#[" *> p <* mustWork (resC "]")
+attr fname = withLoc fname $ do
+  resC "#["
+  name <- baseName
+  args <- many $ termArg fname
+  mustWork $ resC "]"
+  pure $ PA name args
 
 export
-declMod : Grammar True PDeclMod
+findDups : List PAttr -> List String
-declMod = pragma $
+findDups attrs =
-      exactName "fail" *> [|PFail $ optional strLit|]
+  SortedSet.toList $ snd $ foldl check (empty, empty) attrs
-  <|> exactName "compile-scheme" *> [|PCompileScheme strLit|]
+where
-  <|> exactName "main" $> PMain
+  Seen = SortedSet String; Dups = SortedSet String
-  <|> do other <- qname
+  check : (Seen, Dups) -> PAttr -> (Seen, Dups)
-         fatalError "unknown declaration flag \{show other}" {c = False}
+  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 : FileName -> List PAttr -> Grammar True PDefinition
-postulate fname = withLoc fname $ Core.do
+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 : FileName -> List PAttr -> Grammar True PDefinition
-concrete fname = withLoc fname $ do
+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 : FileName -> List PAttr -> Grammar True PDefinition
-definition fname = try (postulate fname) <|> concrete fname
+definition fname attrs =
+  try (postulate fname attrs) <|> concrete fname attrs
 
 export
-namespace_ : FileName -> Grammar True PNamespace
+nsname : Grammar True Mods
-namespace_ fname = withLoc fname $ do
+nsname = do ns <- qname; pure $ ns.mods :< ns.base
-  ns    <- resC "namespace" *> qname; needRes "{"
+
-  decls <- nsInner; optRes ";"
+
-  pure $ MkPNamespace (ns.mods :< ns.base) decls
+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 : FileName -> List PAttr -> Grammar True PDecl
-declBody fname = [|PDef $ definition fname|] <|> [|PNs $ namespace_ fname|]
+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

lib/Quox/Parser/Syntax.idr

@@ -159,57 +159,50 @@ 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
+  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
+  data PDecl =
-    constructor MkPDecl
-    mods : List PDeclMod
-    decl : PDeclBody
-    loc_ : Loc
-
-  public export
-  data PDeclBody =
       PDef PDefinition
     | PNs  PNamespace
-  %name PDeclBody decl
+  %name PDecl decl
-%runElab deriveMutual ["PNamespace", "PDecl", "PDeclBody"]
+%runElab deriveMutual ["PNamespace", "PDecl"] [Eq, Ord, Show, PrettyVal]
-                      [Eq, Ord, Show, PrettyVal]
 
 export Located PNamespace where ns.loc = ns.loc_
 
-export Located PDecl where decl.loc = decl.loc_
-
 export
-Located PDeclBody where
+Located PDecl where
-  (PDef  def).loc  = def.loc
+  (PDef d).loc  = d.loc
   (PNs  ns).loc = ns.loc
 
 public export
@@ -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

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 []
+      `([PD $ PDef $ MkPDef (PQ Zero _) "A"
-          (PDef $ MkPDef (PQ Zero _) "A"
+            (PConcrete (Just $ TYPE 0 _) (Enum [] _)) PSucceed False Nothing _,
-            (PConcrete (Just $ TYPE 0 _) (Enum [] _)) _) _,
+         PD $ PDef $ MkPDef (PQ Zero _) "B"
-         PD $ MkPDecl []
+            (PConcrete (Just $ TYPE 1 _) (V "A" {})) PSucceed False Nothing _]),
-          (PDef $ MkPDef (PQ Zero _) "B"
-            (PConcrete (Just $ TYPE 1 _) (V "A" {})) _) _]),
     parseMatch input "def0 A : ★⁰ = {} def0 B : ★¹ = A" $
-      `([PD $ MkPDecl []
+      `([PD $ PDef $ MkPDef (PQ Zero _) "A"
-          (PDef $ MkPDef (PQ Zero _) "A"
+            (PConcrete (Just $ TYPE 0 _) (Enum [] _)) PSucceed False Nothing _,
-            (PConcrete (Just $ TYPE 0 _) (Enum [] _)) _) _,
+         PD $ PDef $ MkPDef (PQ Zero _) "B"
-         PD $ MkPDecl []
+            (PConcrete (Just $ TYPE 1 _) (V "A" {})) PSucceed False Nothing _]),
-          (PDef $ MkPDef (PQ Zero _) "B"
-            (PConcrete (Just $ TYPE 1 _) (V "A" {})) _) _]),
     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 []
+      `([PD $ PNs $ MkPNamespace [< "a", "b", "c"] [] PSucceed _]),
-          (PNs $ MkPNamespace [< "a", "b", "c"] [] _) _]),
     parseMatch input "namespace a {namespace b {}}"
-      `([PD (MkPDecl []
+      `([PD (PNs $ MkPNamespace [< "a"]
-          (PNs $ MkPNamespace [< "a"]
+            [PNs $ MkPNamespace [< "b"] [] PSucceed _] PSucceed _)]),
-            [MkPDecl [] (PNs $ MkPNamespace [< "b"] [] _) _] _) _)]),
     parseMatch input "namespace a {def x = 't ∷ {t}}"
-      `([PD (MkPDecl []
+      `([PD (PNs $ MkPNamespace [< "a"]
-          (PNs $ MkPNamespace [< "a"]
+            [PDef $ MkPDef (PQ Any _) "x"
-            [MkPDecl []
+              (PConcrete Nothing (Ann (Tag "t" _) (Enum ["t"] _) _))
-              (PDef $ MkPDef (PQ Any _) "x"
+              PSucceed False Nothing _]
-                (PConcrete Nothing
+            PSucceed _)]),
-                           (Ann (Tag "t" _) (Enum ["t"] _) _)) _) _] _) _)]),
     parseMatch input "namespace a {def x : {t} = 't} def y = a.x"
-      `([PD (MkPDecl []
+      `([PD (PNs $ MkPNamespace [< "a"]
-          (PNs $ MkPNamespace [< "a"]
+            [PDef $ MkPDef (PQ Any _) "x"
-            [MkPDecl []
+              (PConcrete (Just (Enum ["t"] _)) (Tag "t" _))
-              (PDef $ MkPDef (PQ Any _) "x"
+              PSucceed False Nothing _]
-                (PConcrete (Just (Enum ["t"] _))
+            PSucceed _),
-                           (Tag "t" _)) _) _] _) _),
+         PD (PDef $ MkPDef (PQ Any _) "y"
-         PD (MkPDecl []
+          (PConcrete Nothing (V (MakePName [< "a"] "x") Nothing _))
-          (PDef $ MkPDef (PQ Any _) "y"
+          PSucceed False Nothing _)]),
-            (PConcrete Nothing (V (MakePName [< "a"] "x") Nothing _)) _) _)]),
     parseMatch input #" load "a.quox"; def b = a.b "#
       `([PLoad "a.quox" _,
-         PD (MkPDecl []
+         PD (PDef $ MkPDef (PQ Any _) "b"
-           (PDef $ MkPDef (PQ Any _) "b"
+          (PConcrete Nothing (V (MakePName [< "a"] "b") Nothing _))
-              (PConcrete Nothing (V (MakePName [< "a"] "b") Nothing _)) _) _)])
+          PSucceed False Nothing _)])
   ]
 ]