diff options
Diffstat (limited to 'src/Obs/Parser.idr')
| -rw-r--r-- | src/Obs/Parser.idr | 185 |
1 files changed, 96 insertions, 89 deletions
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr index 68591ee..b00f5a8 100644 --- a/src/Obs/Parser.idr +++ b/src/Obs/Parser.idr @@ -29,11 +29,6 @@ data ObsTokenKind | OTTrue | OTFalse | OTIf - | OTContainer - | OTTag - | OTPosition - | OTNext - | OTSem | OTPoint | OTVoid | OTAbsurd @@ -43,7 +38,6 @@ data ObsTokenKind | OTCastRefl -- Special symbols | OTUnit - | OTTriangle -- Grouping symbols | OTPOpen | OTPClose @@ -59,7 +53,6 @@ data ObsTokenKind | OTTilde | OTEqual | OTColon - | OTPipe Eq ObsTokenKind where OTNewlines == OTNewlines = True @@ -74,11 +67,6 @@ Eq ObsTokenKind where OTTrue == OTTrue = True OTFalse == OTFalse = True OTIf == OTIf = 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 @@ -87,7 +75,6 @@ Eq ObsTokenKind where OTCast == OTCast = True OTCastRefl == OTCastRefl = True OTUnit == OTUnit = True - OTTriangle == OTTriangle = True OTPOpen == OTPOpen = True OTPClose == OTPClose = True OTAOpen == OTAOpen = True @@ -101,9 +88,43 @@ Eq ObsTokenKind where OTTilde == OTTilde = True OTEqual == OTEqual = True OTColon == OTColon = True - OTPipe == OTPipe = True _ == _ = False +Show ObsTokenKind where + show OTNewlines = "\\n" + show OTSpaces = " " + show OTIdent = "ident" + show OTProp = "Prop" + show OTSet = "Set" + show OTNat = "nat" + show OTFst = "fst" + show OTSnd = "snd" + show OTBool = "Bool" + show OTTrue = "True" + show OTFalse = "False" + show OTIf = "if" + show OTPoint = "tt" + show OTVoid = "Void" + show OTAbsurd = "absurd" + show OTRefl = "refl" + show OTTransp = "transp" + show OTCast = "cast" + show OTCastRefl = "castRefl" + show OTUnit = "()" + show OTPOpen = "(" + show OTPClose = ")" + show OTAOpen = "<" + show OTAClose = ">" + show OTBackslash = "\\" + show OTSlash = "/" + show OTThinArrow = "->" + show OTFatArrow = "=>" + show OTProduct = "**" + show OTComma = "," + show OTTilde = "~" + show OTEqual = "=" + show OTColon = ":" + TokenKind ObsTokenKind where TokType OTIdent = String TokType OTNat = Nat @@ -121,11 +142,6 @@ TokenKind ObsTokenKind where tokValue OTTrue s = () tokValue OTFalse s = () tokValue OTIf 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 = () @@ -134,7 +150,6 @@ TokenKind ObsTokenKind where tokValue OTCast s = () tokValue OTCastRefl s = () tokValue OTUnit s = () - tokValue OTTriangle s = () tokValue OTPOpen s = () tokValue OTPClose s = () tokValue OTAOpen s = () @@ -148,7 +163,6 @@ TokenKind ObsTokenKind where tokValue OTTilde s = () tokValue OTEqual s = () tokValue OTColon s = () - tokValue OTPipe s = () ObsToken : Type ObsToken = Token ObsTokenKind @@ -166,11 +180,6 @@ Show ObsToken where show (Tok OTTrue s) = "True" show (Tok OTFalse s) = "False" show (Tok OTIf s) = "if" - 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" @@ -179,7 +188,6 @@ 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) = "<" @@ -193,7 +201,6 @@ 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 @@ -208,11 +215,6 @@ keywords = , ("True", OTTrue) , ("False", OTFalse) , ("if", OTIf) - , ("Container", OTContainer) - , ("tag", OTTag) - , ("position", OTPosition) - , ("next", OTNext) - , ("sem", OTSem) , ("tt", OTPoint) , ("Void", OTVoid) , ("absurd", OTAbsurd) @@ -243,7 +245,6 @@ obsTokenMap = toTokenMap [(newlines, OTNewlines), (spaces, OTSpaces)] ++ , (exact "~", OTTilde) , (exact "=", OTEqual) , (exact ":", OTColon) - , (exact "|", OTPipe) ] op : Type -> Type -> Nat -> Type @@ -264,66 +265,77 @@ termForms = , (OTUnit, Top) ] -headForms : List (ObsTokenKind, (n ** (Vect (S n) (WithBounds Syntax) -> Syntax))) +headForms : List (ObsTokenKind, (n ** op (WithBounds Syntax) Syntax (S n))) headForms = - [ (OTFst, (0 ** uncurry 1 First)) - , (OTSnd, (0 ** uncurry 1 Second)) - , (OTAbsurd, (0 ** uncurry 1 Absurd)) - , (OTRefl, (0 ** uncurry 1 Refl)) - , (OTTransp, (4 ** (uncurry 5 Transp))) - , (OTCast, (3 ** uncurry 4 Cast)) - , (OTCastRefl, (0 ** uncurry 1 CastId)) + [ (OTFst, (0 ** First)) + , (OTSnd, (0 ** Second)) + , (OTAbsurd, (0 ** Absurd)) + , (OTRefl, (0 ** Refl)) + , (OTTransp, (4 ** Transp)) + , (OTCast, (3 ** Cast)) + , (OTCastRefl, (0 ** CastId)) ] -headLambdaForms : List (ObsTokenKind, (n ** ((WithBounds String, WithBounds Syntax) -> Vect n (WithBounds Syntax) -> Syntax))) -headLambdaForms = - [ (OTIf, (3 ** (uncurry 3 . uncurry If))) - ] +headLambdaForms : List (ObsTokenKind, (n ** (LambdaForm -> op (WithBounds Syntax) Syntax n))) +headLambdaForms = [(OTIf, (3 ** If))] -declForms : List (ObsTokenKind, (WithBounds String -> op (WithBounds Syntax) Syntax 2)) -declForms = [(OTThinArrow, Pi), (OTProduct, Sigma)] +declForms : List (ObsTokenKind, (n ** op DeclForm (WithBounds Syntax -> Syntax) (S n))) +declForms = + [ (OTThinArrow, (0 ** Pi)) + , (OTProduct, (0 ** Sigma)) + ] count : (n : _) -> Grammar state tok True a -> Grammar state tok (isSucc n) (Vect n a) count 0 p = pure [] count (S n) p = [| p :: count n p |] +match' : (tok : ObsTokenKind) -> Grammar state ObsToken True (TokType tok) +match' tok = do + pos <- position + token <- peek + let True = token.kind == tok + | False => failLoc pos "expected \{show tok}" + match tok + ident : Grammar state ObsToken True (WithBounds String) -ident = bounds $ match OTIdent +ident = bounds $ match' OTIdent whitespace : Grammar state ObsToken True () -whitespace = map (\_ => ()) $ some (optional (match OTNewlines) *> match OTSpaces) +whitespace = map (\_ => ()) $ some (optional (match' OTNewlines) *> match' OTSpaces) parens : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True a -parens p = match OTPOpen *> optional whitespace *> p <* optional whitespace <* match OTPClose +parens p = match' OTPOpen *> optional whitespace *> p <* optional whitespace <* match' OTPClose var : Grammar state ObsToken True (WithBounds Syntax) var = map (map Var) ident noArgUniverse : Grammar state ObsToken True (WithBounds Universe) noArgUniverse = bounds $ - map (const Prop) (match OTProp <* commit) <|> - map (const (Set 0)) (match OTSet <* commit) + map (const Prop) (match' OTProp <* commit) <|> + map (const (Set 0)) (match' OTSet <* commit) universe : Grammar state ObsToken True (WithBounds Universe) universe = bounds $ - map (const Prop) (match OTProp <* commit) <|> - map Set (match OTSet *> commit *> option 0 (match OTNat <* commit)) + map (const Prop) (match' OTProp <* commit) <|> + map Set (match' OTSet *> commit *> option 0 (match' OTNat <* commit)) -decl : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (WithBounds String, a) -decl p = [| MkPair (ident <* whitespace <* match OTColon <* whitespace) p |] +decl : Lazy (Grammar state ObsToken True (WithBounds Syntax)) -> + Grammar state ObsToken True DeclForm +decl p = [| MkDecl (ident <* whitespace <* match' OTColon <* whitespace) p |] pair : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (a, a) pair p = - match OTAOpen *> commit *> + match' OTAOpen *> commit *> [| MkPair - (optional whitespace *> p <* optional whitespace <* match OTComma <* commit) + (optional whitespace *> p <* optional whitespace <* match' OTComma <* commit) (optional whitespace *> p <* optional whitespace) |] - <* match OTAClose <* commit + <* match' OTAClose <* commit -lambda : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (WithBounds String, a) +lambda : Lazy (Grammar state ObsToken True (WithBounds Syntax)) -> + Grammar state ObsToken True LambdaForm lambda p = - match OTBackslash *> commit *> - [| MkPair (ident <* whitespace <* match OTFatArrow <* whitespace) p |] + match' OTBackslash *> commit *> + [| MkLambda (ident <* whitespace <* match' OTFatArrow <* whitespace) p |] partial noUniversesTerm : Grammar state ObsToken True (WithBounds Syntax) @@ -334,8 +346,6 @@ 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) @@ -344,7 +354,7 @@ noUniversesTerm = parens exp <|> var <|> bounds (map (uncurry Pair) (pair exp)) <|> - bounds (choiceMap (\(k, s) => map (const s) (match k)) termForms) + bounds (choiceMap (\(k, s) => map (const s) (match' k)) termForms) term = noUniversesTerm <|> map (map Universe) noArgUniverse @@ -353,54 +363,52 @@ head = map (map Universe) universe <|> bounds (choiceMap - (\(hd, (n ** f)) => match hd *> commit *> - [| f (whitespace *> parens (lambda exp)) (count n (whitespace *> term))|]) + (\(hd, (n ** f)) => + match' hd *> commit *> whitespace *> + pure (uncurry n . f) <*> parens (lambda exp) <*> count n (whitespace *> term)) headLambdaForms) <|> bounds (choiceMap - (\(hd, (n ** f)) => match hd *> commit *> [| f (count (S n) (whitespace *> term)) |]) + (\(hd, (n ** f)) => match' hd *> commit *> + pure (uncurry (S n) f) <*> count (S n) (whitespace *> term)) headForms) spine = map (uncurry $ foldl (\t, u => joinBounds (map (\_ => map (\_ => App t u) u) t))) $ [| MkPair head (many (whitespace *> term)) |] -container = spine - equals = map (\(t, u) => maybe t (\u => joinBounds (map (\_ => map (\_ => Equal t u) u) t)) u) $ - [| MkPair container (optional (whitespace *> match OTTilde *> commit *> whitespace *> container)) |] + [| MkPair spine (optional (whitespace *> match' OTTilde *> commit *> whitespace *> spine)) |] exp = equals <|> - bounds (map (uncurry Lambda) $ lambda exp) <|> + bounds (map Lambda $ lambda exp) <|> bounds - (map (\((var, a), (b, f)) => f var a b) $ - [| MkPair - (parens (decl exp) <* whitespace) - (choiceMap - (\(op, f) => match op *> commit *> whitespace *> [| MkPair exp (pure f) |]) - declForms) - |]) + (choiceMap + (\(sep, (n ** f)) => + pure (uncurry (S n) f) <*> + count (S n) (parens (decl exp) <* whitespace <* match' sep <* commit <* whitespace) <*> + exp) + declForms) partial def : Grammar state ObsToken True (WithBounds String, WithBounds Syntax) -def = [| MkPair (ident <* whitespace <* match OTEqual <* whitespace) exp |] +def = [| MkPair (ident <* whitespace <* match' OTEqual <* whitespace) exp |] partial fullDef : Grammar state ObsToken True Definition fullDef = seq - [| MkPair (decl exp <* commit) (optional whitespace *> match OTNewlines *> def <* commit) |] - (\((name, ty), (name', tm)) => + [| MkPair (decl exp <* commit) (optional whitespace *> match' OTNewlines *> def <* commit) |] + (\((MkDecl name ty), (name', tm)) => if name.val == name'.val then pure (MkDefinition {name = name, ty, tm}) - else fatalLoc name.bounds "name mismatch for declaration and definition") + else fatalLoc name.bounds "name mismatch' for declaration and definition") partial file : Grammar state ObsToken False (List Definition) file = - optional (whitespace *> match OTNewlines) *> - sepEndBy (optional whitespace *> match OTNewlines) (fullDef <* commit) - -- <* eof + optional (whitespace *> match' OTNewlines) *> + sepEndBy (optional whitespace *> match' OTNewlines) (fullDef <* commit) whitespaceIrrelevant : WithBounds ObsToken -> WithBounds ObsToken whitespaceIrrelevant a = case (a.val.kind) of @@ -413,7 +421,6 @@ 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 - (OTAOpen, OTPipe) => map (\_ => (Tok OTTriangle "<|")) (mergeBounds a b) :: mergeToks rest _ => a :: mergeToks tail mergeToks toks = toks @@ -425,7 +432,7 @@ castErr (Right x) = pure x castErr (Left errs) = do for_ {b = ()} errs (\(Error msg bounds) => - inBounds $ map error $ maybe (irrelevantBounds msg) (MkBounded msg True) bounds) + inBounds $ map error $ maybe (irrelevantBounds msg) (MkBounded msg False) bounds) abort partial |