quox/lib/Quox/Parser/Parser.idr
2023-03-18 02:46:41 +01:00

330 lines
8 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Quox.Parser.Parser
import public Quox.Parser.Lexer
import public Quox.Parser.Syntax
import Data.Fin
import Data.Vect
import public Text.Parser
%default total
public export
0 Grammar : Bool -> Type -> Type
Grammar = Core.Grammar () Token
%hide Core.Grammar
export
res : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
res str = terminal "expecting \"\{str}\"" $
\x => guard $ x == Reserved str
export
resC : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
resC str = do res str; commit
parameters {default True commit : Bool}
private
maybeCommit : Grammar False ()
maybeCommit = when commit Core.commit
export
betweenR : {c : Bool} -> (op, cl : String) ->
(0 _ : IsReserved op) => (0 _ : IsReserved cl) =>
Grammar c a -> Grammar True a
betweenR o c p = res o *> maybeCommit *> p <* res c <* maybeCommit
export
parens, bracks, braces : {c : Bool} -> Grammar c a -> Grammar True a
parens = betweenR "(" ")"
bracks = betweenR "[" "]"
braces = betweenR "{" "}"
export
commaSep : {c : Bool} -> Grammar c a -> Grammar False (List a)
commaSep = sepEndBy (res ",")
-- don't commit because of the possible terminating ","
export
semiSep : {c : Bool} -> Grammar c a -> Grammar False (List a)
semiSep = sepEndBy (res ";")
export
commaSep1 : {c : Bool} -> Grammar c a -> Grammar c (List1 a)
commaSep1 = sepEndBy1 (res ",")
export
darr : Grammar True ()
darr = resC ""
export
name : Grammar True PName
name = terminal "expecting name" $
\case Name i => Just i; _ => Nothing
export
mods : Grammar True Mods
mods = name <&> \n => n.mods :< n.base
export
baseName : Grammar True String
baseName = terminal "expecting unqualified name" $
\case Name i => guard (null i.mods) $> i.base
_ => Nothing
export
nat : Grammar True Nat
nat = terminal "expecting natural number" $
\case Nat n => pure n; _ => Nothing
export
string : Grammar True String
string = terminal "expecting string literal" $
\case Str s => pure s; _ => Nothing
export
tag : Grammar True String
tag = terminal "expecting tag constructor" $
\case Tag t => pure t; _ => Nothing
export
bareTag : Grammar True String
bareTag = string <|> [|toDotsP name|]
export
universe : Grammar True PUniverse
universe = terminal "expecting type universe" $
\case TYPE u => Just u; _ => Nothing
export
bname : Grammar True BName
bname = Nothing <$ res "_"
<|> [|Just baseName|]
export
zeroOne : (zero, one : a) -> Grammar True a
zeroOne zero one = terminal "expecting zero or one" $
\case Nat 0 => Just zero; Nat 1 => Just one; _ => Nothing
export covering
qty : Grammar True PQty
qty = zeroOne Zero One
<|> Any <$ res "ω"
<|> parens qty
private covering
qtys : Grammar False (List PQty)
qtys = option [] [|toList $ some qty <* res "."|]
export
dimConst : Grammar True DimConst
dimConst = zeroOne Zero One
export covering
dim : Grammar True PDim
dim = [|V baseName|]
<|> [|K dimConst|]
<|> parens dim
private
0 PBinderHead : Nat -> Type
PBinderHead n = (Vect n PQty, BName, PTerm)
private
toVect : List a -> (n ** Vect n a)
toVect [] = (_ ** [])
toVect (x :: xs) = (_ ** x :: snd (toVect xs))
private
0 MakeBinder : Nat -> Type
MakeBinder n = (String, PBinderHead n -> PTerm -> PTerm)
private
makePi : MakeBinder 1
makePi = ("", \([pi], x, s) => Pi pi x s)
private
makeSig : MakeBinder 0
makeSig = ("×", \([], x, s) => Sig x s)
private
makeBinder : {m, n : Nat} -> MakeBinder m -> PBinderHead n -> PTerm ->
Grammar False PTerm
makeBinder (str, f) h t =
case decEq m n of
Yes Refl => pure $ f h t
No _ =>
let q = if m == 1 then "quantity" else "quantities" in
fatalError "'\{str}' expects \{show m} \{q}, got \{show n}"
private
binderInfix : Grammar True (n ** MakeBinder n)
binderInfix = res "" $> (1 ** makePi)
<|> res "×" $> (0 ** makeSig)
private
lamIntro : Grammar True (BName -> PTerm -> PTerm)
lamIntro = Lam <$ resC "λ"
<|> DLam <$ resC "δ"
private covering
caseIntro : Grammar True PQty
caseIntro = resC "case1" $> One
<|> resC "caseω" $> Any
<|> resC "case" *> qty <* resC "."
private
optNameBinder : Grammar False BName
optNameBinder = [|join $ optional $ bname <* darr|]
mutual
export covering
term : Grammar True PTerm
term = lamTerm
<|> caseTerm
<|> bindTerm
<|> [|annotate infixEqTerm (optional $ resC "" *> term)|]
where
annotate : PTerm -> Maybe PTerm -> PTerm
annotate s a = maybe s (s :#) a
private covering
lamTerm : Grammar True PTerm
lamTerm = flip . foldr <$> lamIntro <*> some bname <* darr <*> term
private covering
caseTerm : Grammar True PTerm
caseTerm =
[|Case caseIntro term
(resC "return" *> optBinderTerm)
(resC "of" *> braces caseBody)|]
private covering
caseBody : Grammar False PCaseBody
caseBody = [|CasePair (pairPat <* darr) (term <* optSemi)|]
<|> [|CaseEnum $ semiSep [|MkPair tag (darr *> term)|]|]
where
optSemi = ignore $ optional $ res ";"
pairPat = parens [|MkPair bname (resC "," *> bname)|]
private covering
bindTerm : Grammar True PTerm
bindTerm = do
bnd <- binderHead
inf <- binderInfix
body <- term
makeBinder (snd inf) (snd bnd) body
private covering
infixEqTerm : Grammar True PTerm
infixEqTerm = do
l <- infixTimesTerm
rty <- optional [|MkPair (resC "" *> term) (resC ":" *> infixTimesTerm)|]
pure $ maybe l (\rty => Eq (Nothing, snd rty) l (fst rty)) rty
private covering
infixTimesTerm : Grammar True PTerm
infixTimesTerm = foldr1 (Sig Nothing) <$> sepBy1 (resC "×") appTerm
private covering
appTerm : Grammar True PTerm
appTerm = resC "" *> [|TYPE nat|]
<|> resC "Eq" *> [|Eq (bracks optBinderTerm) aTerm aTerm|]
<|> [|apply aTerm (many appArg)|]
where
data PArg = TermArg PTerm | DimArg PDim
appArg : Grammar True PArg
appArg = [|DimArg $ resC "@" *> dim|]
<|> [|TermArg aTerm|]
apply : PTerm -> List PArg -> PTerm
apply = foldl apply1 where
apply1 : PTerm -> PArg -> PTerm
apply1 f (TermArg x) = f :@ x
apply1 f (DimArg p) = f :% p
private covering
aTerm : Grammar True PTerm
aTerm = [|Enum $ braces $ commaSep bareTag|]
<|> [|TYPE universe|]
<|> [|V name|]
<|> [|Tag tag|]
<|> foldr1 Pair <$> parens (commaSep1 term)
private covering
binderHead : Grammar True (n ** PBinderHead n)
binderHead = parens {commit = False} $ do
qs <- [|toVect qtys|]
name <- bname
resC ":"
ty <- term
pure (qs.fst ** (qs.snd, name, ty))
private covering
optBinderTerm : Grammar True (BName, PTerm)
optBinderTerm = [|MkPair optNameBinder term|]
export covering
defIntro : Grammar True PQty
defIntro = Zero <$ resC "def0"
<|> Any <$ resC "defω"
<|> resC "def" *> option Any (qty <* resC ".")
export covering
definition : Grammar True PDefinition
definition =
[|MkPDef defIntro name (optional (resC ":" *> term)) (resC "=" *> term)|]
export
load : Grammar True String
load = resC "load" *> string
mutual
export covering
namespace_ : Grammar True PNamespace
namespace_ =
[|MkPNamespace (resC "namespace" *> mods) (braces $ many decl)|]
export covering
decl : Grammar True PDecl
decl = [|PDef definition|]
<|> [|PNs namespace_|]
export covering
topLevel : Grammar True PTopLevel
topLevel = [|PLoad load|]
<|> [|PD decl|]
export covering
input : Grammar False (List PTopLevel)
input = skipSemis *> many (topLevel <* skipSemis)
where skipSemis = ignore $ many $ resC ";"
public export
data Error =
LexError Lexer.Error
| ParseError (List1 (ParsingError Token))
%hide Lexer.Error
export
lexParseWith : {c : Bool} -> Grammar c a -> String -> Either Error a
lexParseWith grm input = do
toks <- mapFst LexError $ lex input
bimap ParseError fst $ parse (grm <* eof) toks
export covering %inline
lexParseInput : String -> Either Error (List PTopLevel)
lexParseInput = lexParseWith input
export covering %inline
lexParseTerm : String -> Either Error PTerm
lexParseTerm = lexParseWith term