1 files changed, 176 insertions, 0 deletions
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
new file mode 100644
index 0000000..2802690
--- /dev/null
+++ b/src/Obs/Parser.idr
@@ -0,0 +1,176 @@
+module Obs.Parser
+
+import Data.String
+
+import Obs.Sort
+import Obs.Syntax
+
+import System
+import System.File
+
+import Text.Lexer
+import Text.Parser
+
+Error : Type -> Type -> Type
+Error tok = Either (List1 (ParsingError tok))
+
+report : List1 (ParsingError tok) -> Error tok a
+report = Left
+
+data ObsTokenKind
+  = OTNewline
+  | OTIgnore
+  | OTIdent
+  | OTSet
+  | OTProp
+  | OTNat
+  | OTPOpen
+  | OTPClose
+  | OTEqual
+  | OTColon
+
+Eq ObsTokenKind where
+  OTNewline == OTNewline = True
+  OTIgnore  == OTIgnore  = True
+  OTIdent   == OTIdent   = True
+  OTSet     == OTSet     = True
+  OTProp    == OTProp    = True
+  OTNat     == OTNat     = True
+  OTPOpen   == OTPOpen   = True
+  OTPClose  == OTPClose  = True
+  OTEqual   == OTEqual   = True
+  OTColon   == OTColon   = True
+  _         == _         = False
+
+TokenKind ObsTokenKind where
+  TokType OTIdent = String
+  TokType OTNat   = Nat
+  TokType _     = ()
+
+  tokValue OTNewline s = ()
+  tokValue OTIgnore  s = ()
+  tokValue OTIdent   s = s
+  tokValue OTSet     s = ()
+  tokValue OTProp    s = ()
+  tokValue OTNat     s = stringToNatOrZ s
+  tokValue OTPOpen   s = ()
+  tokValue OTPClose  s = ()
+  tokValue OTEqual   s = ()
+  tokValue OTColon   s = ()
+
+ObsToken : Type
+ObsToken = Token ObsTokenKind
+
+ignored : WithBounds ObsToken -> Bool
+ignored (MkBounded (Tok OTIgnore _) _ _) = True
+ignored _ = False
+
+identifier : Lexer
+identifier = alpha <+> many alphaNum
+
+keywords : List (String, ObsTokenKind)
+keywords =
+  [ ("Set", OTSet)
+  , ("Prop", OTProp)
+  ]
+
+obsTokenMap : TokenMap ObsToken
+obsTokenMap = toTokenMap [(newline, OTNewline), (spaces, OTIgnore)] ++
+  [ (identifier, \s =>
+        case lookup s keywords of
+          (Just kind) => Tok kind s
+          Nothing => Tok OTIdent s)
+  ] ++ toTokenMap
+  [ (digits, OTNat)
+  , (exact "(", OTPOpen)
+  , (exact ")", OTPClose)
+  , (exact "=", OTEqual)
+  , (exact ":", OTColon)
+  ]
+
+parens : {c : _} -> Grammar state ObsToken c a -> Grammar state ObsToken True a
+parens g =
+  match OTPOpen *>
+  many (match OTNewline) *>
+  g <*
+  many (match OTNewline) <*
+  match OTPClose
+
+ident : Grammar state ObsToken True (WithBounds String)
+ident = bounds $ match OTIdent
+
+var : Grammar state ObsToken True Syntax
+var = do
+  id <- ident
+  pure (Var id.bounds id.val)
+
+prop : Grammar state ObsToken True (WithBounds Sort)
+prop = do
+  p <- bounds $ match OTProp
+  pure (map (\_ => Prop) p)
+
+set : Grammar state ObsToken True (WithBounds Sort)
+set = do
+  s <- bounds $ match OTSet
+  i <- bounds $ option 0 (match OTNat)
+  pure (map Set $ mergeBounds s i)
+
+sort : Grammar state ObsToken True Syntax
+sort = do
+  sort <- prop <|> set
+  pure (Sort sort.bounds sort.val)
+
+exp  : Grammar state ObsToken True Syntax
+term : Grammar state ObsToken True Syntax
+
+exp = term
+term = var <|> sort <|> parens exp
+
+decl : Grammar state ObsToken True (WithBounds String, Syntax)
+decl = [| MkPair ident (match OTColon *> exp) |]
+
+def : Grammar state ObsToken True (WithBounds String, Syntax)
+def = [| MkPair ident (match OTEqual *> exp) |]
+
+fullDef : Grammar state ObsToken True Definition
+fullDef =
+  seq
+    [| MkPair decl (match OTNewline *> def) |]
+    (\((name, ty), (name', tm)) =>
+      if name.val == name'.val
+        then pure (MkDefinition {bounds = name.bounds, name = name.val, ty, tm})
+        else fatalLoc name.bounds "name mismatch for declaration and definition")
+
+file : Grammar state ObsToken False (List Definition)
+file = many (match OTNewline) *> sepEndBy (some (match OTNewline)) fullDef
+
+export
+parse : String -> Error ObsToken (List Definition)
+parse str = do
+  let (toks, _, _, "") = lex obsTokenMap str
+    | (_, l, c, rem) => report (Error "failed to lex input" (Just $ MkBounds { startLine = l, startCol = c, endLine = l, endCol = c }) ::: [])
+  (defs, []) <- parse file $ filter (not . ignored) toks
+    | (_, (t :: _)) => report (Error "unparsed tokens" (Just t.bounds) ::: [])
+  pure defs
+
+printErr : ParsingError tok -> IO ()
+printErr (Error str Nothing)  = putStrLn "error: \{str}"
+printErr (Error str (Just b)) = putStrLn
+  "error: \{show b.startLine}:\{show b.startCol}-\{show b.endLine}:\{show b.endCol}: \{str}"
+
+reportErrs : List (ParsingError tok) -> IO a
+reportErrs []          = exitFailure
+reportErrs (e :: errs) = do
+  () <- printErr e
+  reportErrs errs
+
+export
+parseFile : (fname : String) -> IO (List Definition)
+parseFile fname = do
+  Right str <- readFile fname
+    | Left err => do
+      () <- putStrLn "error: \{show err}"
+      exitFailure
+  let Right defs = parse str
+    | Left err => reportErrs (forget err)
+  pure defs