diff options
Diffstat (limited to 'src/Obs/Parser.idr')
| -rw-r--r-- | src/Obs/Parser.idr | 34 |
1 files changed, 29 insertions, 5 deletions
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr index 278ff0f..2dd7052 100644 --- a/src/Obs/Parser.idr +++ b/src/Obs/Parser.idr @@ -23,11 +23,17 @@ data ObsTokenKind = OTNewline | OTIgnore | OTIdent - | OTSet + -- Keywords | OTProp + | OTSet | OTNat + -- Special symbols + | OTUnit + | OTPoint + -- Grouping symbols | OTPOpen | OTPClose + -- Definition characters | OTEqual | OTColon @@ -35,9 +41,11 @@ Eq ObsTokenKind where OTNewline == OTNewline = True OTIgnore == OTIgnore = True OTIdent == OTIdent = True - OTSet == OTSet = True OTProp == OTProp = True + OTSet == OTSet = True OTNat == OTNat = True + OTUnit == OTUnit = True + OTPoint == OTPoint = True OTPOpen == OTPOpen = True OTPClose == OTPClose = True OTEqual == OTEqual = True @@ -52,9 +60,11 @@ TokenKind ObsTokenKind where tokValue OTNewline s = () tokValue OTIgnore s = () tokValue OTIdent s = s - tokValue OTSet s = () tokValue OTProp s = () + tokValue OTSet s = () tokValue OTNat s = stringToNatOrZ s + tokValue OTUnit s = () + tokValue OTPoint s = () tokValue OTPOpen s = () tokValue OTPClose s = () tokValue OTEqual s = () @@ -84,6 +94,7 @@ obsTokenMap = toTokenMap [(newline, OTNewline), (spaces, OTIgnore)] ++ Nothing => Tok OTIdent s) ] ++ toTokenMap [ (digits, OTNat) + , (exact "_", OTPoint) , (exact "(", OTPOpen) , (exact ")", OTPClose) , (exact "=", OTEqual) @@ -122,13 +133,19 @@ sort = do sort <- prop <|> set pure (Sort sort.bounds sort.val) +top : Grammar state ObsToken True Syntax +top = map (\v => Top v.bounds) $ bounds $ match OTUnit + +point : Grammar state ObsToken True Syntax +point = map (\v => Point v.bounds) $ bounds $ match OTPoint + partial exp : Grammar state ObsToken True Syntax partial term : Grammar state ObsToken True Syntax exp = term -term = var <|> sort <|> parens exp +term = var <|> sort <|> top <|> point <|> parens exp partial decl : Grammar state ObsToken True (WithBounds String, Syntax) @@ -152,13 +169,20 @@ partial file : Grammar state ObsToken False (List Definition) file = many (match OTNewline) *> sepEndBy (some (match OTNewline)) fullDef +postprocess : List (WithBounds ObsToken) -> List (WithBounds ObsToken) +postprocess [] = [] +postprocess [tok] = if ignored tok then [] else [tok] +postprocess (tok :: tail@(tok' :: toks)) = case (tok.val.kind, tok'.val.kind) of + (OTPOpen, OTPClose) => map (\_ => Tok OTUnit "()") (mergeBounds tok tok') :: postprocess toks + _ => if ignored tok then postprocess tail else tok :: postprocess tail + partial 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 + (defs, []) <- parse file $ postprocess toks | (_, (t :: _)) => report (Error "unparsed tokens" (Just t.bounds) ::: []) pure defs |