diff options
Diffstat (limited to 'src/Obs/Parser.idr')
| -rw-r--r-- | src/Obs/Parser.idr | 64 |
1 files changed, 62 insertions, 2 deletions
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr index acb1360..7ce31c4 100644 --- a/src/Obs/Parser.idr +++ b/src/Obs/Parser.idr @@ -29,6 +29,11 @@ data ObsTokenKind | OTLeft | OTRight | OTCase + | OTContainer + | OTTag + | OTPosition + | OTNext + | OTSem | OTPoint | OTVoid | OTAbsurd @@ -38,6 +43,7 @@ data ObsTokenKind | OTCastRefl -- Special symbols | OTUnit + | OTTriangle -- Grouping symbols | OTPOpen | OTPClose @@ -45,6 +51,7 @@ data ObsTokenKind | OTAClose -- Definition characters | OTBackslash + | OTSlash | OTThinArrow | OTFatArrow | OTProduct @@ -52,6 +59,7 @@ data ObsTokenKind | OTTilde | OTEqual | OTColon + | OTPipe Eq ObsTokenKind where OTNewlines == OTNewlines = True @@ -66,6 +74,11 @@ Eq ObsTokenKind where OTLeft == OTLeft = True OTRight == OTRight = True OTCase == OTCase = True + OTContainer == OTContainer = True + OTTag == OTTag = True + OTPosition == OTPosition = True + OTNext == OTNext = True + OTSem == OTSem = True OTPoint == OTPoint = True OTVoid == OTVoid = True OTAbsurd == OTAbsurd = True @@ -74,11 +87,13 @@ Eq ObsTokenKind where OTCast == OTCast = True OTCastRefl == OTCastRefl = True OTUnit == OTUnit = True + OTTriangle == OTTriangle = True OTPOpen == OTPOpen = True OTPClose == OTPClose = True OTAOpen == OTAOpen = True OTAClose == OTAClose = True OTBackslash == OTBackslash = True + OTSlash == OTSlash = True OTThinArrow == OTThinArrow = True OTFatArrow == OTFatArrow = True OTProduct == OTProduct = True @@ -86,6 +101,7 @@ Eq ObsTokenKind where OTTilde == OTTilde = True OTEqual == OTEqual = True OTColon == OTColon = True + OTPipe == OTPipe = True _ == _ = False TokenKind ObsTokenKind where @@ -105,6 +121,11 @@ TokenKind ObsTokenKind where tokValue OTLeft s = () tokValue OTRight s = () tokValue OTCase s = () + tokValue OTContainer s = () + tokValue OTTag s = () + tokValue OTPosition s = () + tokValue OTNext s = () + tokValue OTSem s = () tokValue OTPoint s = () tokValue OTVoid s = () tokValue OTAbsurd s = () @@ -113,11 +134,13 @@ TokenKind ObsTokenKind where tokValue OTCast s = () tokValue OTCastRefl s = () tokValue OTUnit s = () + tokValue OTTriangle s = () tokValue OTPOpen s = () tokValue OTPClose s = () tokValue OTAOpen s = () tokValue OTAClose s = () tokValue OTBackslash s = () + tokValue OTSlash s = () tokValue OTThinArrow s = () tokValue OTFatArrow s = () tokValue OTProduct s = () @@ -125,6 +148,7 @@ TokenKind ObsTokenKind where tokValue OTTilde s = () tokValue OTEqual s = () tokValue OTColon s = () + tokValue OTPipe s = () ObsToken : Type ObsToken = Token ObsTokenKind @@ -142,6 +166,11 @@ Show ObsToken where show (Tok OTLeft s) = "Left" show (Tok OTRight s) = "Right" show (Tok OTCase s) = "case" + show (Tok OTContainer s) = "Container" + show (Tok OTTag s) = "tag" + show (Tok OTPosition s) = "position" + show (Tok OTNext s) = "next" + show (Tok OTSem s) = "sem" show (Tok OTPoint s) = "tt" show (Tok OTVoid s) = "Void" show (Tok OTAbsurd s) = "absurd" @@ -150,11 +179,13 @@ Show ObsToken where show (Tok OTCast s) = "cast" show (Tok OTCastRefl s) = "castRefl" show (Tok OTUnit s) = "()" + show (Tok OTTriangle s) = "<|" show (Tok OTPOpen s) = "(" show (Tok OTPClose s) = ")" show (Tok OTAOpen s) = "<" show (Tok OTAClose s) = ">" show (Tok OTBackslash s) = "\\" + show (Tok OTSlash s) = "/" show (Tok OTThinArrow s) = "->" show (Tok OTFatArrow s) = "=>" show (Tok OTProduct s) = "**" @@ -162,6 +193,7 @@ Show ObsToken where show (Tok OTTilde s) = "~" show (Tok OTEqual s) = "=" show (Tok OTColon s) = ":" + show (Tok OTPipe s) = "|" identifier : Lexer identifier = alpha <+> many alphaNum @@ -176,6 +208,11 @@ keywords = , ("Left", OTLeft) , ("Right", OTRight) , ("case", OTCase) + , ("Container", OTContainer) + , ("tag", OTTag) + , ("position", OTPosition) + , ("next", OTNext) + , ("sem", OTSem) , ("tt", OTPoint) , ("Void", OTVoid) , ("absurd", OTAbsurd) @@ -200,11 +237,13 @@ obsTokenMap = toTokenMap [(newlines, OTNewlines), (spaces, OTSpaces)] ++ , (exact "=>", OTFatArrow) , (exact "->", OTThinArrow) , (exact "\\", OTBackslash) + , (exact "/", OTSlash) , (exact "**", OTProduct) , (exact ",", OTComma) , (exact "~", OTTilde) , (exact "=", OTEqual) , (exact ":", OTColon) + , (exact "|", OTPipe) ] op : Type -> Type -> Nat -> Type @@ -230,6 +269,11 @@ headForms = , (OTLeft, (0 ** uncurry 1 Left)) , (OTRight, (0 ** uncurry 1 Right)) , (OTCase, (4 ** uncurry 5 Case)) + , (OTContainer, (2 ** uncurry 3 Container)) + , (OTTag, (0 ** uncurry 1 Tag)) + , (OTPosition, (0 ** uncurry 1 Position)) + , (OTNext, (0 ** uncurry 1 Next)) + , (OTSem, (2 ** uncurry 3 Sem)) , (OTAbsurd, (1 ** uncurry 2 Absurd)) , (OTRefl, (0 ** uncurry 1 Refl)) , (OTTransp, (4 ** uncurry 5 Transp)) @@ -286,6 +330,8 @@ head : Grammar state ObsToken True (WithBounds Syntax) partial spine : Grammar state ObsToken True (WithBounds Syntax) partial +container : Grammar state ObsToken True (WithBounds Syntax) +partial equals : Grammar state ObsToken True (WithBounds Syntax) partial exp : Grammar state ObsToken True (WithBounds Syntax) @@ -309,8 +355,21 @@ head = spine = map (uncurry $ foldl (\t, u => joinBounds (map (\_ => map (\_ => App t u) u) t))) $ [| MkPair head (many (whitespace *> term)) |] +container = + map (\bounds@(MkBounded (t, u) _ _) => case u of + Nothing => t + Just (p, f) => map (\_ => MkContainer t p f) bounds) $ + bounds $ + [| MkPair spine + (optional + [| MkPair + (whitespace *> match OTTriangle *> commit *> whitespace *> spine) + (whitespace *> match OTSlash *> commit *> whitespace *> spine) + |]) + |] + equals = map (\(t, u) => maybe t (\u => joinBounds (map (\_ => map (\_ => Equal t u) u) t)) u) $ - [| MkPair spine (optional (whitespace *> match OTTilde *> commit *> whitespace *> spine)) |] + [| MkPair container (optional (whitespace *> match OTTilde *> commit *> whitespace *> container)) |] exp = equals <|> @@ -358,7 +417,8 @@ whitespaceIrrelevant a = case (a.val.kind) of mergeToks : List (WithBounds ObsToken) -> List (WithBounds ObsToken) mergeToks (a :: tail@(b :: rest)) = case (a.val.kind, b.val.kind) of (OTSpaces, OTNat) => mergeBounds a b :: mergeToks rest - (OTPOpen, OTPClose) => map (\_ => (Tok OTUnit "")) (mergeBounds a b) :: mergeToks rest + (OTPOpen, OTPClose) => map (\_ => (Tok OTUnit "()")) (mergeBounds a b) :: mergeToks rest + (OTAOpen, OTPipe) => map (\_ => (Tok OTTriangle "<|")) (mergeBounds a b) :: mergeToks rest _ => a :: mergeToks tail mergeToks toks = toks |