diff options
Diffstat (limited to 'src/Obs/Parser.idr')
| -rw-r--r-- | src/Obs/Parser.idr | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr index 2802690..278ff0f 100644 --- a/src/Obs/Parser.idr +++ b/src/Obs/Parser.idr @@ -11,6 +11,8 @@ import System.File import Text.Lexer import Text.Parser +%default total + Error : Type -> Type -> Type Error tok = Either (List1 (ParsingError tok)) @@ -120,18 +122,23 @@ sort = do sort <- prop <|> set pure (Sort sort.bounds sort.val) +partial exp : Grammar state ObsToken True Syntax +partial term : Grammar state ObsToken True Syntax exp = term term = var <|> sort <|> parens exp +partial decl : Grammar state ObsToken True (WithBounds String, Syntax) decl = [| MkPair ident (match OTColon *> exp) |] +partial def : Grammar state ObsToken True (WithBounds String, Syntax) def = [| MkPair ident (match OTEqual *> exp) |] +partial fullDef : Grammar state ObsToken True Definition fullDef = seq @@ -141,9 +148,11 @@ fullDef = then pure (MkDefinition {bounds = name.bounds, name = name.val, ty, tm}) else fatalLoc name.bounds "name mismatch for declaration and definition") +partial file : Grammar state ObsToken False (List Definition) file = many (match OTNewline) *> sepEndBy (some (match OTNewline)) fullDef +partial export parse : String -> Error ObsToken (List Definition) parse str = do @@ -164,6 +173,7 @@ reportErrs (e :: errs) = do () <- printErr e reportErrs errs +partial export parseFile : (fname : String) -> IO (List Definition) parseFile fname = do |