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

allow fst/snd to take multiple arguments

Browse source 
also succ though that won't be well typed
This commit is contained in:
rhiannon morris 2023-12-04 18:21:27 +01:00
parent e2ad18ff1f
commit 4291afd51b
2 changed files with 25 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -381,11 +381,24 @@ eqTerm : FileName -> Grammar True PTerm
eqTerm fname = withLoc fname $
resC "Eq" *> mustWork [|Eq (typeLine fname) (termArg fname) (termArg fname)|]
private
appArg : Loc -> PTerm -> Either PDim PTerm -> PTerm
appArg loc f (Left p) = DApp f p loc
appArg loc f (Right s) = App f s loc
||| a dimension argument with an `@` prefix, or
||| a term argument with no prefix
export
anyArg : FileName -> Grammar True (Either PDim PTerm)
anyArg fname = dimArg fname <||> termArg fname
export
resAppTerm : FileName -> (word : String) -> (0 _ : IsReserved word) =>
(PTerm -> Loc -> PTerm) -> Grammar True PTerm
resAppTerm fname word f = withLoc fname $
resC word *> mustWork [|f (termArg fname)|]
resAppTerm fname word f = withLoc fname $ do
head <- withLoc fname $ resC word *> mustWork [|f (termArg fname)|]
args <- many $ anyArg fname
pure $ \loc => foldl (appArg loc) head args
export
succTerm : FileName -> Grammar True PTerm
@ -399,21 +412,12 @@ export
sndTerm : FileName -> Grammar True PTerm
sndTerm fname = resAppTerm fname "snd" Snd
||| a dimension argument with an `@` prefix, or
||| a term argument with no prefix
export
anyArg : FileName -> Grammar True (Either PDim PTerm)
anyArg fname = dimArg fname <||> termArg fname
export
normalAppTerm : FileName -> Grammar True PTerm
normalAppTerm fname = withLoc fname $ do
head <- termArg fname
args <- many $ anyArg fname
pure $ \loc => foldl (ap loc) head args
where ap : Loc -> PTerm -> Either PDim PTerm -> PTerm
ap loc f (Left p) = DApp f p loc
ap loc f (Right s) = App f s loc
pure $ \loc => foldl (appArg loc) head args
||| application term `f x @y z`, or other terms that look like application
||| like `succ` or `coe`.