max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: adjust elaborator to new syntax

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-06 06:51:45 -07:00
parent fda85f6a71
commit 0447966b72
2 changed files with 24 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/Do.lean
View file

@ -447,9 +447,9 @@ pure {
private def getDoSeqElems (doSeq : Syntax) : List Syntax :=
if doSeq.getKind == `Lean.Parser.Term.doSeqBracketed then
(doSeq.getArg 1).getArgs.getSepElems.toList
(doSeq.getArg 1).getArgs.toList.map fun arg => arg.getArg 0
else if doSeq.getKind == `Lean.Parser.Term.doSeqIndent then
(doSeq.getArg 0).getArgs.getSepElems.toList
(doSeq.getArg 0).getArgs.toList.map fun arg => arg.getArg 0
else
[]
@ -526,7 +526,7 @@ else
throwError "unexpected kind of reassignment"
def toDoSeq (doElem : Syntax) : Syntax :=
mkNode `Lean.Parser.Term.doSeqIndent #[mkNullNode #[doElem, mkNullNode]]
mkNode `Lean.Parser.Term.doSeqIndent #[mkNullNode #[mkNullNode #[doElem, mkNullNode]]]
/-
Recall that the `doIf` syntax is of the form

49
tests/compiler/termparsertest1.lean.expected.out
View file

@ -275,39 +275,32 @@ do
(Term.do
"do"
(Term.doSeqIndent
[(Term.doLetArrow "let" (Term.doIdDecl `x [] "←" (Term.app `f [`a])))
[";"]
(Term.doLetArrow "let" (Term.doIdDecl `x [(Term.typeSpec ":" `Nat)] "←" (Term.app `f [`a])))
[";"]
(Term.doExpr (Term.app `g [`x]))
[";"]
(Term.doLet "let" (Term.letDecl (Term.letIdDecl `y [] [] ":=" (Term.app `g [`x]))))
[";"]
(Term.doLetArrow
"let"
(Term.doPatDecl (Term.paren "(" [`a [(Term.tupleTail "," [`b])]] ")") "<-" (Term.app `h [`x `y]) []))
[";"]
(Term.doLet
"let"
(Term.letDecl
(Term.letPatDecl
(Term.paren "(" [`a [(Term.tupleTail "," [`b])]] ")")
[]
[]
":="
(Term.paren "(" [`b [(Term.tupleTail "," [`a])]] ")"))))
[";"]
(Term.doExpr (Term.app `pure [(Term.paren "(" [(Term.add `a "+" `b) []] ")")]))
[]]))
[[(Term.doLetArrow "let" (Term.doIdDecl `x [] "←" (Term.app `f [`a]))) [";"]]
[(Term.doLetArrow "let" (Term.doIdDecl `x [(Term.typeSpec ":" `Nat)] "←" (Term.app `f [`a]))) [";"]]
[(Term.doExpr (Term.app `g [`x])) [";"]]
[(Term.doLet "let" (Term.letDecl (Term.letIdDecl `y [] [] ":=" (Term.app `g [`x])))) [";"]]
[(Term.doLetArrow
"let"
(Term.doPatDecl (Term.paren "(" [`a [(Term.tupleTail "," [`b])]] ")") "<-" (Term.app `h [`x `y]) []))
[";"]]
[(Term.doLet
"let"
(Term.letDecl
(Term.letPatDecl
(Term.paren "(" [`a [(Term.tupleTail "," [`b])]] ")")
[]
[]
":="
(Term.paren "(" [`b [(Term.tupleTail "," [`a])]] ")"))))
[";"]]
[(Term.doExpr (Term.app `pure [(Term.paren "(" [(Term.add `a "+" `b) []] ")")])) []]]))
do { let x ← f a; pure $ a + a }
(Term.do
"do"
(Term.doSeqBracketed
"{"
[(Term.doLetArrow "let" (Term.doIdDecl `x [] "←" (Term.app `f [`a])))
[";"]
(Term.doExpr (Term.dollar `pure "$" (Term.add `a "+" `a)))
[]]
[[(Term.doLetArrow "let" (Term.doIdDecl `x [] "←" (Term.app `f [`a]))) [";"]]
[(Term.doExpr (Term.dollar `pure "$" (Term.add `a "+" `a))) []]]
"}"))
let f : Nat → Nat → Nat
| 0, a => a + 10