rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

multiple semi-sep binds in a let

Browse source
This commit is contained in:
rhiannon morris 2023-12-04 23:27:59 +01:00
parent 415a823dec
commit e48f03a61c
2 changed files with 41 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
lib/Quox/Parser/Parser.idr
View file

@ -585,22 +585,32 @@ where
foldr (\(q, x, s), t => Pi q x s t loc) cod $ toDoms (toQty q) doms
letIntro : FileName -> Grammar True PQty
export
letIntro : FileName -> Grammar True (Maybe PQty)
letIntro fname =
withLoc fname (PQ Zero <$ res "let0")
<|> withLoc fname (PQ One <$ res "let1")
<|> withLoc fname (PQ Any <$ res "letω")
<|> do resC "let"
qty fname <* needRes "." <|> defLoc fname (PQ One)
withLoc fname (Just . PQ Zero <$ res "let0")
<|> withLoc fname (Just . PQ One <$ res "let1")
<|> withLoc fname (Just . PQ Any <$ res "letω")
<|> Nothing <$ resC "let"
export
letBinder : FileName -> Maybe PQty -> Grammar True (PQty, PatVar, PTerm)
letBinder fname mq = do
qty <- the (Grammar False PQty) $ case mq of
Just q => pure q
Nothing => qty fname <* mustWork (resC ".") <|> defLoc fname (PQ One)
x <- patVar fname; mustWork (resC "=")
rhs <- term fname
pure $ (qty, x, rhs)
export
letTerm : FileName -> Grammar True PTerm
letTerm fname = withLoc fname $ do
qty <- letIntro fname
x <- patVar fname <* mustWork (resC "=")
rhs <- assert_total term fname <* mustWork (resC "in")
body <- assert_total term fname
pure $ Let (qty, x, rhs) body
qty <- letIntro fname
binds <- sepEndBy1 (res ";") $ assert_total letBinder fname qty
mustWork $ resC "in"
body <- assert_total term fname
pure $ \loc => foldr (\b, s => Let b s loc) body binds
-- term : FileName -> Grammar True PTerm
term fname = lamTerm fname

21
tests/Tests/Parser.idr
View file

@ -414,12 +414,16 @@ tests = "parser" :- [
"let" :- [
parseMatch term "let x = y in z"
`(Let (PQ One _, PV "x" {}, V "y" {}) (V "z" {}) _),
parseMatch term "let x = y; in z"
`(Let (PQ One _, PV "x" {}, V "y" {}) (V "z" {}) _),
parseMatch term "let0 x = y in z"
`(Let (PQ Zero _, PV "x" {}, V "y" {}) (V "z" {}) _),
parseMatch term "let1 x = y in z"
`(Let (PQ One _, PV "x" {}, V "y" {}) (V "z" {}) _),
parseMatch term "letω x = y in z"
`(Let (PQ Any _, PV "x" {}, V "y" {}) (V "z" {}) _),
parseMatch term "let ω.x = y in z"
`(Let (PQ Any _, PV "x" {}, V "y" {}) (V "z" {}) _),
parseMatch term "let x = y1 y2 in z1 z2"
`(Let (PQ One _, PV "x" {},
(App (V "y1" {}) (V "y2" {}) _))
@ -427,12 +431,27 @@ tests = "parser" :- [
parseMatch term "let x = a in let y = b in z"
`(Let (PQ One _, PV "x" {}, V "a" {})
(Let (PQ One _, PV "y" {}, V "b" {}) (V "z" {}) _) _),
parseMatch term "let x = a; y = b in z"
`(Let (PQ One _, PV "x" {}, V "a" {})
(Let (PQ One _, PV "y" {}, V "b" {}) (V "z" {}) _) _),
parseMatch term "letω x = a; y = b in z"
`(Let (PQ Any _, PV "x" {}, V "a" {})
(Let (PQ Any _, PV "y" {}, V "b" {}) (V "z" {}) _) _),
parseMatch term "letω x = a; y = b; in z"
`(Let (PQ Any _, PV "x" {}, V "a" {})
(Let (PQ Any _, PV "y" {}, V "b" {}) (V "z" {}) _) _),
parseMatch term "let ω.x = a; 1.y = b in z"
`(Let (PQ Any _, PV "x" {}, V "a" {})
(Let (PQ One _, PV "y" {}, V "b" {}) (V "z" {}) _) _),
parseMatch term "let x = y in z ∷ Z"
`(Let (PQ One _, PV "x" {}, V "y" {})
(Ann (V "z" {}) (V "Z" {}) _) _),
parseMatch term "let x = y in z₁ ≡ z₂ : Z"
`(Let (PQ One _, PV "x" {}, V "y" {})
(Eq (Unused _, V "Z" {}) (V "z₁" {}) (V "z₂" {}) _) _)
(Eq (Unused _, V "Z" {}) (V "z₁" {}) (V "z₂" {}) _) _),
parseFails term "let1 1.x = y in z",
parseFails term "let x = y",
parseFails term "let x in z"
],
"definitions" :-