start of parser stuff

lib/quox-lib.ipkg

@@ -5,7 +5,7 @@ authors   = "rhiannon morris"
 sourceloc = "https://git.rhiannon.website/rhi/quox"
 license   = "acsl"
 
-depends = base, contrib, elab-util, sop
+depends = base, contrib, elab-util, sop, snocvect
 
 sourcedir = "src"
 modules =
@@ -28,6 +28,7 @@ modules =
   Quox.Syntax.Var,
   Quox.Token,
   Quox.Lexer,
+  Quox.Parser,
   Quox.Context,
   Quox.Equal,
   Quox.Name,

lib/src/Quox/Lexer.idr

@@ -119,10 +119,10 @@ tokens = choice [
 
 
 export
-lex : MonadError Error m => String -> m (List (WithBounds Token))
+lex : String -> Either Error (List BToken)
 lex str =
   let (res, (reason, line, col, str)) = lex tokens str in
   case reason of
-       EndInput => pure $ mapMaybe sequence res
+       EndInput => Right $ mapMaybe sequence res
        _        => let char = assert_total strIndex str 0 in
-                   throwError $ Err {reason, line, col, char}
+                   Left $ Err {reason, line, col, char}

lib/src/Quox/Parser.idr

@@ -0,0 +1,115 @@
+module Quox.Parser
+
+import Quox.Syntax
+import Quox.Token
+import Quox.Lexer
+
+import Data.SnocVect
+import Data.SnocList
+import Text.Parser
+
+%default total
+
+
+public export
+Vars : Nat -> Type
+Vars n = SnocVect n String
+
+public export
+Grammar : Bool -> Type -> Type
+Grammar = Core.Grammar () Token
+%hide Core.Grammar
+
+public export
+data Error
+= Lex (Lexer.Error)
+| Parse (List1 (ParsingError Token))
+| Leftover (List BToken)
+%hide Lexer.Error
+
+
+public export
+parseAll : {c : Bool} -> Grammar c a -> List BToken -> Either Error a
+parseAll grm input =
+  case parse grm input of
+       Right (x, [])   => Right x
+       Right (x, rest) => Left $ Leftover rest
+       Left  errs      => Left $ Parse errs
+
+public export
+lexParseAll : {c : Bool} -> Grammar c a -> String -> Either Error a
+lexParseAll grm = lex' >=> parseAll grm
+  where lex' : String -> Either Error (List BToken)
+        lex' = bimap Lex id . lex
+
+
+
+punc : Punc -> Grammar True ()
+punc p = terminal (show p) $ \case
+  P p' => if p == p' then Just () else Nothing
+  _    => Nothing
+
+between : Punc -> Punc -> Grammar True a -> Grammar True a
+between opener closer inner = punc opener *> inner <* punc closer
+
+parens, squares, braces : Grammar True a -> Grammar True a
+parens  = between LParen  RParen
+squares = between LSquare RSquare
+braces  = between LBrace  RBrace
+
+
+export
+number : Grammar True Nat
+number = terminal "number" $ \case
+  N Zero      => Just 0
+  N One       => Just 1
+  N (Other k) => Just k
+  _           => Nothing
+
+zero, one, omega : Grammar True ()
+zero  = terminal "0" $ \case N Zero  => Just (); _ => Nothing
+one   = terminal "1" $ \case N One   => Just (); _ => Nothing
+omega = terminal "ω" $ \case K Omega => Just (); _ => Nothing
+
+export
+quantity : Grammar True Qty
+quantity = Zero <$ zero <|> One <$ one <|> Any <$ omega
+
+
+find1 : Eq a => SnocVect k a -> a -> Maybe (Var k)
+find1 [<]       y = Nothing
+find1 (sx :< x) y = if x == y then Just VZ else VS <$> find1 sx y
+
+find : Vars k -> Name -> Maybe (Var k)
+find vs (MakeName [<] (UN y)) = find1 vs y
+find _  _                     = Nothing
+
+
+export
+bound : Vars k -> Grammar True (Var k)
+bound vs =
+  terminal "bound variable" $ \case Name x => find1 vs x; _ => Nothing
+
+export
+sname : Grammar True String
+sname = terminal "simple name" $ \case Name x => pure x; _ => Nothing
+
+export
+qname : Grammar True Name
+qname = do
+  parts <- sepBy1 (punc Dot) sname
+  pure $ MakeName {mods = cast $ init parts, base = UN $ last parts}
+
+export
+nameWith : Vars k -> Grammar True (Either (Var k) Name)
+nameWith vs = do
+  y <- qname
+  pure $ maybe (Right y) Left $ find vs y
+
+
+export
+dimension : Vars d -> Grammar True (Dim d)
+dimension vs =
+      K Zero <$  zero
+  <|> K One  <$  one
+  <|> B      <$> bound vs

lib/src/Quox/Token.idr

@@ -1,6 +1,7 @@
 module Quox.Token
 
 import Generics.Derive
+import Text.Lexer
 
 %default total
 %language ElabReflection
@@ -44,3 +45,8 @@ data Token
 | K Keyword
 
 %runElab derive "Token" [Generic, Meta, Eq, Ord, DecEq, Show]
+
+
+public export
+BToken : Type
+BToken = WithBounds Token