allow fst, snd, case to be application heads #35
|
@ -286,8 +286,66 @@ export
|
|||
universe1 : Grammar True Universe
|
||||
universe1 = universeTok <|> res "★" *> option 0 super
|
||||
|
||||
||| argument/atomic term: single-token terms, or those with delimiters e.g.
|
||||
||| `[t]`
|
||||
|
||||
public export
|
||||
PCaseArm : Type
|
||||
PCaseArm = (PCasePat, PTerm)
|
||||
|
||||
export
|
||||
caseArm : FileName -> Grammar True PCaseArm
|
||||
caseArm fname =
|
||||
[|(,) (casePat fname) (needRes "⇒" *> assert_total term fname)|]
|
||||
|
||||
export
|
||||
checkCaseArms : Loc -> List PCaseArm -> Grammar False PCaseBody
|
||||
checkCaseArms loc [] = pure $ CaseEnum [] loc
|
||||
checkCaseArms loc ((PPair x y _, rhs) :: rest) =
|
||||
if null rest then pure $ CasePair (x, y) rhs loc
|
||||
else fatalError "unexpected pattern after pair"
|
||||
checkCaseArms loc ((PTag tag _, rhs1) :: rest) = do
|
||||
let rest = for rest $ \case
|
||||
(PTag tag _, rhs) => Just (tag, rhs)
|
||||
_ => Nothing
|
||||
maybe (fatalError "expected all patterns to be tags")
|
||||
(\rest => pure $ CaseEnum ((tag, rhs1) :: rest) loc) rest
|
||||
checkCaseArms loc ((PZero _, rhs1) :: rest) = do
|
||||
let [(PSucc p q ih _, rhs2)] = rest
|
||||
| _ => fatalError "expected succ pattern after zero"
|
||||
pure $ CaseNat rhs1 (p, q, ih, rhs2) loc
|
||||
checkCaseArms loc ((PSucc p q ih _, rhs1) :: rest) = do
|
||||
let [(PZero _, rhs2)] = rest
|
||||
| _ => fatalError "expected zero pattern after succ"
|
||||
pure $ CaseNat rhs2 (p, q, ih, rhs1) loc
|
||||
checkCaseArms loc ((PBox x _, rhs) :: rest) =
|
||||
if null rest then pure $ CaseBox x rhs loc
|
||||
else fatalError "unexpected pattern after box"
|
||||
|
||||
export
|
||||
caseBody : FileName -> Grammar True PCaseBody
|
||||
caseBody fname = do
|
||||
body <- bounds $ delimSep "{" "}" ";" $ caseArm fname
|
||||
let loc = makeLoc fname body.bounds
|
||||
checkCaseArms loc body.val
|
||||
|
||||
export
|
||||
caseReturn : FileName -> Grammar True (PatVar, PTerm)
|
||||
caseReturn fname = do
|
||||
x <- patVar fname <* resC "⇒" <|> unused fname
|
||||
ret <- assert_total term fname
|
||||
pure (x, ret)
|
||||
|
||||
export
|
||||
caseTerm : FileName -> Grammar True PTerm
|
||||
caseTerm fname = withLoc fname $ do
|
||||
qty <- caseIntro fname; commit
|
||||
head <- mustWork $ assert_total term fname; needRes "return"
|
||||
ret <- mustWork $ caseReturn fname; needRes "of"
|
||||
body <- mustWork $ caseBody fname
|
||||
pure $ Case qty head ret body
|
||||
|
||||
|
||||
||| argument/atomic term: single-token terms, or those with delimiters
|
||||
||| e.g. `[t]`. includes `case` because the end delimiter is the `}`.
|
||||
export
|
||||
termArg : FileName -> Grammar True PTerm
|
||||
termArg fname = withLoc fname $
|
||||
|
@ -302,6 +360,7 @@ termArg fname = withLoc fname $
|
|||
<|> STRING <$ res "String"
|
||||
<|> [|Str strLit|]
|
||||
<|> [|V qname displacement|]
|
||||
<|> const <$> caseTerm fname
|
||||
<|> const <$> tupleTerm fname
|
||||
|
||||
export
|
||||
|
@ -381,11 +440,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 +471,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`.
|
||||
|
@ -521,65 +584,12 @@ where
|
|||
makePi q doms cod loc =
|
||||
foldr (\(q, x, s), t => Pi q x s t loc) cod $ toDoms (toQty q) doms
|
||||
|
||||
public export
|
||||
PCaseArm : Type
|
||||
PCaseArm = (PCasePat, PTerm)
|
||||
|
||||
|
||||
export
|
||||
caseArm : FileName -> Grammar True PCaseArm
|
||||
caseArm fname =
|
||||
[|(,) (casePat fname) (needRes "⇒" *> assert_total term fname)|]
|
||||
|
||||
export
|
||||
checkCaseArms : Loc -> List PCaseArm -> Grammar False PCaseBody
|
||||
checkCaseArms loc [] = pure $ CaseEnum [] loc
|
||||
checkCaseArms loc ((PPair x y _, rhs) :: rest) =
|
||||
if null rest then pure $ CasePair (x, y) rhs loc
|
||||
else fatalError "unexpected pattern after pair"
|
||||
checkCaseArms loc ((PTag tag _, rhs1) :: rest) = do
|
||||
let rest = for rest $ \case
|
||||
(PTag tag _, rhs) => Just (tag, rhs)
|
||||
_ => Nothing
|
||||
maybe (fatalError "expected all patterns to be tags")
|
||||
(\rest => pure $ CaseEnum ((tag, rhs1) :: rest) loc) rest
|
||||
checkCaseArms loc ((PZero _, rhs1) :: rest) = do
|
||||
let [(PSucc p q ih _, rhs2)] = rest
|
||||
| _ => fatalError "expected succ pattern after zero"
|
||||
pure $ CaseNat rhs1 (p, q, ih, rhs2) loc
|
||||
checkCaseArms loc ((PSucc p q ih _, rhs1) :: rest) = do
|
||||
let [(PZero _, rhs2)] = rest
|
||||
| _ => fatalError "expected zero pattern after succ"
|
||||
pure $ CaseNat rhs2 (p, q, ih, rhs1) loc
|
||||
checkCaseArms loc ((PBox x _, rhs) :: rest) =
|
||||
if null rest then pure $ CaseBox x rhs loc
|
||||
else fatalError "unexpected pattern after box"
|
||||
|
||||
export
|
||||
caseBody : FileName -> Grammar True PCaseBody
|
||||
caseBody fname = do
|
||||
body <- bounds $ delimSep "{" "}" ";" $ caseArm fname
|
||||
let loc = makeLoc fname body.bounds
|
||||
checkCaseArms loc body.val
|
||||
|
||||
export
|
||||
caseReturn : FileName -> Grammar True (PatVar, PTerm)
|
||||
caseReturn fname = do
|
||||
x <- patVar fname <* resC "⇒" <|> unused fname
|
||||
ret <- assert_total term fname
|
||||
pure (x, ret)
|
||||
|
||||
export
|
||||
caseTerm : FileName -> Grammar True PTerm
|
||||
caseTerm fname = withLoc fname $ do
|
||||
qty <- caseIntro fname; commit
|
||||
head <- mustWork $ assert_total term fname; needRes "return"
|
||||
ret <- mustWork $ caseReturn fname; needRes "of"
|
||||
body <- mustWork $ caseBody fname
|
||||
pure $ Case qty head ret body
|
||||
|
||||
-- term : FileName -> Grammar True PTerm
|
||||
term fname = lamTerm fname
|
||||
<|> caseTerm fname
|
||||
<|> piTerm fname
|
||||
<|> sigmaTerm fname
|
||||
|
||||
|
|
|
@ -138,7 +138,15 @@ tests = "parser" :- [
|
|||
parseMatch term "f @p"
|
||||
`(DApp (V "f" {}) (V "p" {}) _),
|
||||
parseMatch term "f x @p y"
|
||||
`(App (DApp (App (V "f" {}) (V "x" {}) _) (V "p" {}) _) (V "y" {}) _)
|
||||
`(App (DApp (App (V "f" {}) (V "x" {}) _) (V "p" {}) _) (V "y" {}) _),
|
||||
parseMatch term "fst e"
|
||||
`(Fst (V "e" {}) _),
|
||||
parseMatch term "snd e"
|
||||
`(Snd (V "e" {}) _),
|
||||
parseMatch term "(fst e) x"
|
||||
`(App (Fst (V "e" {}) _) (V "x" {}) _),
|
||||
parseMatch term "fst e x"
|
||||
`(App (Fst (V "e" {}) _) (V "x" {}) _)
|
||||
],
|
||||
|
||||
"annotations" :- [
|
||||
|
@ -392,7 +400,15 @@ tests = "parser" :- [
|
|||
`(Case (PQ Any _) (V "n" {}) (Unused _, NAT _)
|
||||
(CaseNat (Nat 0 _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
|
||||
parseFails term "caseω n return A of { zero ⇒ a }",
|
||||
parseFails term "caseω n return ℕ of { succ ⇒ 5 }"
|
||||
parseFails term "caseω n return ℕ of { succ ⇒ 5 }",
|
||||
parseMatch term
|
||||
"case1 f s return x ⇒ A x of { (l, r) ⇒ r l } x"
|
||||
`(App
|
||||
(Case (PQ One _) (App (V "f" {}) (V "s" {}) _)
|
||||
(PV "x" _, App (V "A" {}) (V "x" {}) _)
|
||||
(CasePair (PV "l" _, PV "r" _)
|
||||
(App (V "r" {}) (V "l" {}) _) _) _)
|
||||
(V "x" {}) _)
|
||||
],
|
||||
|
||||
"definitions" :-
|
||||
|
|
Loading…
Reference in New Issue