diff options
Diffstat (limited to 'src/CC/Term/Parse.idr')
| -rw-r--r-- | src/CC/Term/Parse.idr | 155 |
1 files changed, 132 insertions, 23 deletions
diff --git a/src/CC/Term/Parse.idr b/src/CC/Term/Parse.idr index 3615956..5c8956a 100644 --- a/src/CC/Term/Parse.idr +++ b/src/CC/Term/Parse.idr @@ -4,40 +4,65 @@ import CC.Name import CC.Term import CC.Term.Raw +import Data.Bool import Data.List import Text.Lexer import Text.Parser +%hide Text.Parser.match + +-- Utilities ------------------------------------------------------------------- + +expandBindList : Functor f => (f (Maybe Name), RawTerm) -> f RawBinding +expandBindList (xs, t) = map (`Of` t) xs + -- Tokens ---------------------------------------------------------------------- data CCTokenKind = TIgnore + -- Variables | TIdent - -- Keywords + -- Let Syntax | TLet - -- Symbols + | TDef + | TSemi + -- Universes + | TSet + -- Abstraction + | TThinArrow | TLambda - | TPOpen - | TPClose | TComma | TFatArrow - | TDef - | TSemi + -- Symbols + | TUnderscore + | TColon + | TPOpen + | TPClose %name CCTokenKind k Eq CCTokenKind where TIgnore == TIgnore = True + TIdent == TIdent = True + TLet == TLet = True + TDef == TDef = True + TSemi == TSemi = True + + TSet == TSet = True + + TThinArrow == TThinArrow = True TLambda == TLambda = True - TPOpen == TPOpen = True - TPClose == TPClose = True TComma == TComma = True TFatArrow == TFatArrow = True - TDef == TDef = True - TSemi == TSemi = True + + TUnderscore == TUnderscore = True + TColon == TColon = True + TPOpen == TPOpen = True + TPClose == TPClose = True + _ == _ = False TokenKind CCTokenKind where @@ -45,15 +70,45 @@ TokenKind CCTokenKind where TokType _ = () tokValue TIgnore s = () + tokValue TIdent s = s + tokValue TLet s = () + tokValue TDef s = () + tokValue TSemi s = () + + tokValue TSet s = () + + tokValue TThinArrow s = () tokValue TLambda s = () - tokValue TPOpen s = () - tokValue TPClose s = () tokValue TComma s = () tokValue TFatArrow s = () - tokValue TDef s = () - tokValue TSemi s = () + + tokValue TUnderscore s = () + tokValue TColon s = () + tokValue TPOpen s = () + tokValue TPClose s = () + +Interpolation CCTokenKind where + interpolate TIgnore = "whitespace" + + interpolate TIdent = "identifier" + + interpolate TLet = #""let""# + interpolate TDef = #""=""# + interpolate TSemi = #"";""# + + interpolate TSet = #""Set""# + + interpolate TThinArrow = #""->""# + interpolate TLambda = #""\""# + interpolate TComma = #"",""# + interpolate TFatArrow = #""=>""# + + interpolate TUnderscore = #""_""# + interpolate TColon = #"":""# + interpolate TPOpen = #""(""# + interpolate TPClose = #"")""# export CCToken : Type @@ -68,47 +123,92 @@ identifier : Lexer identifier = alpha <+> many alphaNum keywords : List (String, CCTokenKind) -keywords = [("let", TLet)] +keywords = [("let", TLet), ("Set", TSet)] tokenMap : TokenMap CCToken tokenMap = + -- Ignored toTokenMap (map (, TIgnore) ignored) ++ + -- Identifiers [(identifier, \s => case lookup s keywords of Just kind => Tok kind s Nothing => Tok TIdent s) ] ++ toTokenMap [ + -- Abstraction + (exact "->", TThinArrow), (exact "\\", TLambda), (exact "\x03BB", TLambda), - (exact "(", TPOpen), - (exact ")", TPClose), (exact ",", TComma), (exact "=>", TFatArrow), + -- Symbols + (exact "_", TUnderscore), + (exact ":", TColon), + (exact "(", TPOpen), + (exact ")", TPClose), + -- Let syntax (has to be after fat arrow) (exact "=", TDef), (exact ";", TSemi) ] -- Parser ---------------------------------------------------------------------- +match : (kind : CCTokenKind) -> Grammar state CCToken True (TokType kind) +match k = terminal "expected \{k}" $ + \t => if t.kind == k then Just $ tokValue k t.text else Nothing + %tcinline parens : {b : Bool} -> Grammar state CCToken b ty -> Grammar state CCToken True ty -parens p = match TPOpen >> commit >> p >>= (\t => match TPClose *> commit *> pure t) +parens p = match TPOpen >> p >>= (\t => match TPClose *> pure t) parseIdent : Grammar state CCToken True Name parseIdent = MkName <$> (bounds $ match TIdent) +parseBinder : Grammar state CCToken True (Maybe Name) +parseBinder = either Just (const Nothing) <$> (parseIdent <||> match TUnderscore) + +%tcinline +withBounds : Grammar state CCToken True RawTerm -> Grammar state CCToken True RawTerm +withBounds p = Bounded <$> bounds p + +parseBindList : Grammar state CCToken True (List1 (Maybe Name)) +parseBindList = sepBy1 (match TComma) parseBinder + +parseAnnot : (commit : Bool) -> Grammar state CCToken True RawTerm +parseMaybeAnnot : (commit : Bool) -> Grammar state CCToken False (Maybe RawTerm) +parseAnnotArgs : (commit : Bool) -> Grammar state CCToken True (List1 (Maybe Name), RawTerm) +parseOptArrow : (commit : Bool) -> Grammar state CCToken False (Maybe RawTerm) + parseTerm : Grammar state CCToken True RawTerm +parsePi : Grammar state CCToken True RawTerm parseLambda : Grammar state CCToken True RawTerm parseLet : Grammar state CCToken True RawTerm +parseChain : Grammar state CCToken True RawTerm parseSpine : Grammar state CCToken True RawTerm parseAtom : Grammar state CCToken True RawTerm -parseTerm = parseLambda <|> parseLet <|> parseSpine +parseAnnot False = match TColon >> parseTerm +parseAnnot True = match TColon >> commit >> parseTerm + +parseMaybeAnnot b = Just <$> parseAnnot b <|> pure Nothing + +parseAnnotArgs b = [| MkPair parseBindList (parseAnnot b) |] + +parseOptArrow False = Just <$> (match TThinArrow >> parseTerm) <|> pure Nothing +parseOptArrow True = Just <$> (match TThinArrow >> commit >> parseTerm) <|> pure Nothing + +parseTerm = withBounds (parsePi <|> parseLambda <|> parseLet <|> parseChain) + +parsePi = do + dom <- parens (parseAnnotArgs False) + match TThinArrow + cod <- parseTerm + pure $ foldr1By Pi (flip Pi cod) $ expandBindList dom parseLambda = do match TLambda commit - names <- sepBy1 (match TComma >> commit) parseIdent + names <- parseBindList commit match TFatArrow commit @@ -120,19 +220,28 @@ parseLet = do commit n <- parseIdent commit + ty <- parseMaybeAnnot True match TDef commit t <- parseTerm match TSemi commit u <- parseTerm - pure $ Let n t u + pure $ Let n ty t u + +parseChain = do + spine <- parseSpine + maybeCod <- parseOptArrow True + pure $ case maybeCod of + Just cod => Pi (Nothing `Of` spine) cod + Nothing => spine parseSpine = foldl1 App <$> some parseAtom parseAtom = - (Var <$> parseIdent <* commit) <|> - (parens parseTerm) + withBounds (Var <$> parseIdent <* commit) <|> + withBounds (Set <$ match TSet <* commit) <|> + parens parseTerm parseSrc : Grammar state CCToken True RawTerm parseSrc = parseTerm <* eof |