From ebf6aefb1d113062f83b45c9283831d09047f5e8 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sat, 18 Mar 2023 20:00:29 +0100 Subject: [PATCH] parser tweaks qtys and dims don't allow useless parens any more. everything else should be the same --- lib/Quox/Parser/Parser.idr | 98 +++++++++++++++++++------------------- tests/Tests/Parser.idr | 4 +- 2 files changed, 50 insertions(+), 52 deletions(-) diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr index f02fe56..4dbfb75 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/lib/Quox/Parser/Parser.idr @@ -18,8 +18,7 @@ Grammar = Core.Grammar () Token export res : (str : String) -> (0 _ : IsReserved str) => Grammar True () -res str = terminal "expecting \"\{str}\"" $ - \x => guard $ x == Reserved str +res str = terminal "expecting \"\{str}\"" $ guard . (== Reserved str) export resC : (str : String) -> (0 _ : IsReserved str) => Grammar True () @@ -107,30 +106,41 @@ 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 +dimConst : Grammar True DimConst +dimConst = terminal "expecting 0 or 1" $ + \case Nat 0 => Just Zero; Nat 1 => Just One; _ => Nothing - -export covering +export qty : Grammar True PQty -qty = zeroOne Zero One - <|> Any <$ res "ω" - <|> parens qty +qty = terminal "expecting quantity" $ + \case Nat 0 => Just Zero; Nat 1 => Just One; Reserved "ω" => Just Any + _ => Nothing + + +public export +AllReserved : List (a, String) -> Type +AllReserved = foldr (\x, ps => (IsReserved $ snd x, ps)) () + +export +symbols : (lst : List (a, String)) -> (0 _ : AllReserved lst) => + Grammar True a +symbols [] = fail "no symbols found" +symbols ((x, str) :: rest) = x <$ res str <|> symbols rest + +export +symbolsC : (lst : List (a, String)) -> (0 _ : AllReserved lst) => + Grammar True a +symbolsC lst = symbols lst <* commit + private covering qtys : Grammar False (List PQty) qtys = option [] [|toList $ some qty <* res "."|] -export -dimConst : Grammar True DimConst -dimConst = zeroOne Zero One -export covering +export dim : Grammar True PDim -dim = [|V baseName|] - <|> [|K dimConst|] - <|> parens dim +dim = [|V baseName|] <|> [|K dimConst|] private 0 PBinderHead : Nat -> Type @@ -154,9 +164,9 @@ makeSig : MakeBinder 0 makeSig = ("×", \([], x, s) => Sig x s) private -makeBinder : {m, n : Nat} -> MakeBinder m -> PBinderHead n -> PTerm -> +makeBinder : (m ** PBinderHead m) -> (n ** MakeBinder n) -> PTerm -> Grammar False PTerm -makeBinder (str, f) h t = +makeBinder (m ** h) (n ** (str, f)) t = case decEq m n of Yes Refl => pure $ f h t No _ => @@ -165,18 +175,15 @@ makeBinder (str, f) h t = private binderInfix : Grammar True (n ** MakeBinder n) -binderInfix = res "→" $> (1 ** makePi) - <|> res "×" $> (0 ** makeSig) +binderInfix = symbols [((1 ** makePi), "→"), ((0 ** makeSig), "×")] private lamIntro : Grammar True (BName -> PTerm -> PTerm) -lamIntro = Lam <$ resC "λ" - <|> DLam <$ resC "δ" +lamIntro = symbolsC [(Lam, "λ"), (DLam, "δ")] private covering caseIntro : Grammar True PQty -caseIntro = resC "case1" $> One - <|> resC "caseω" $> Any +caseIntro = symbols [(One, "case1"), (Any, "caseω")] <|> resC "case" *> qty <* resC "." private @@ -186,13 +193,7 @@ 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 + term = lamTerm <|> caseTerm <|> bindTerm <|> annTerm private covering lamTerm : Grammar True PTerm @@ -203,23 +204,25 @@ mutual caseTerm = [|Case caseIntro term (resC "return" *> optBinderTerm) - (resC "of" *> braces caseBody)|] + (resC "of" *> caseBody)|] private covering - caseBody : Grammar False PCaseBody - caseBody = [|CasePair (pairPat <* darr) (term <* optSemi)|] - <|> [|CaseEnum $ semiSep [|MkPair tag (darr *> term)|]|] + caseBody : Grammar True PCaseBody + caseBody = braces $ + [|CasePair (pairPat <* darr) (term <* optSemi)|] + <|> [|CaseEnum $ semiSep [|MkPair tag (darr *> term)|]|] where - optSemi = ignore $ optional $ res ";" + optSemi = 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 + bindTerm = join [|makeBinder binderHead binderInfix term|] + + private covering + annTerm : Grammar True PTerm + annTerm = [|annotate infixEqTerm (optional $ resC "∷" *> term)|] + where annotate s a = maybe s (s :#) a private covering infixEqTerm : Grammar True PTerm @@ -241,8 +244,7 @@ mutual data PArg = TermArg PTerm | DimArg PDim appArg : Grammar True PArg - appArg = [|DimArg $ resC "@" *> dim|] - <|> [|TermArg aTerm|] + appArg = [|DimArg $ resC "@" *> dim|] <|> [|TermArg aTerm|] apply : PTerm -> List PArg -> PTerm apply = foldl apply1 where @@ -261,10 +263,9 @@ mutual private covering binderHead : Grammar True (n ** PBinderHead n) binderHead = parens {commit = False} $ do - qs <- [|toVect qtys|] + qs <- [|toVect qtys|] name <- bname - resC ":" - ty <- term + ty <- resC ":" *> term pure (qs.fst ** (qs.snd, name, ty)) private covering @@ -274,8 +275,7 @@ mutual export covering defIntro : Grammar True PQty -defIntro = Zero <$ resC "def0" - <|> Any <$ resC "defω" +defIntro = symbols [(Zero, "def0"), (Any, "defω")] <|> resC "def" *> option Any (qty <* resC ".") export covering diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index fe9d8f0..a36b701 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -70,8 +70,7 @@ tests = "parser" :- [ "dimensions" :- [ parsesAs dim "0" (K Zero), parsesAs dim "1" (K One), - parsesAs dim "ι" (V "ι"), - parsesAs dim "(0)" (K Zero), + parsesAs dim "𝑖" (V "𝑖"), parseFails dim "M.x", parseFails dim "_" ], @@ -81,7 +80,6 @@ tests = "parser" :- [ parsesAs qty "1" One, parsesAs qty "ω" Any, parsesAs qty "#" Any, - parsesAs qty "(#)" Any, parseFails qty "anythingElse", parseFails qty "_" ],