1040 lines
48 KiB
Text
1040 lines
48 KiB
Text
/-
|
||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Leonardo de Moura, Sebastian Ullrich, Mario Carneiro
|
||
-/
|
||
module
|
||
|
||
prelude
|
||
public import Lean.Parser.Term.Basic
|
||
public import Lean.Parser.Term.Doc
|
||
import Lean.DocString.Parser
|
||
public import Lean.DocString.Formatter
|
||
|
||
public section
|
||
|
||
namespace Lean
|
||
namespace Parser
|
||
|
||
namespace Command
|
||
|
||
open Lean.Parser in
|
||
def versoCommentBodyFn : ParserFn := fun c s =>
|
||
let startPos := s.pos
|
||
let s := finishCommentBlock (pushMissingOnError := true) 1 c s
|
||
if !s.hasError then
|
||
let iniSz := s.stackSize
|
||
let commentEndPos := s.pos
|
||
let endPos := c.prev (c.prev commentEndPos)
|
||
let endPos := if endPos ≤ c.inputString.rawEndPos then endPos else c.inputString.rawEndPos
|
||
let c' := c.setEndPos endPos (by unfold endPos; split <;> simp [*])
|
||
let s := Doc.Parser.document {} c' (s.setPos startPos)
|
||
let s :=
|
||
if !s.allErrors.isEmpty then
|
||
-- Docstring parsing must always succeed, or else later error messages are atrocious! Syntax
|
||
-- errors in the docs should not cause verso-docstring-expecting commands to be removed from
|
||
-- consideration. So, at this stage, we push an indication of the failure, and then later,
|
||
-- when adding docstrings, the failing case is re-parsed and the errors are reported then.
|
||
-- We don't just parse them later because then the syntax of the docs doesn't end up as part
|
||
-- of the syntax of the actual program.
|
||
let s := s.restore iniSz endPos
|
||
let leading := c.mkEmptySubstringAt startPos
|
||
let trailing := c.mkEmptySubstringAt endPos
|
||
let s :=
|
||
s.pushSyntax <|
|
||
.atom (.original leading startPos trailing endPos) (String.Pos.Raw.extract c.inputString startPos endPos)
|
||
let s := s.mkNode `Lean.Doc.Syntax.parseFailure iniSz
|
||
{s with recoveredErrors := #[]}
|
||
else s
|
||
rawFn (Doc.Parser.ignoreFn <| chFn '-' >> chFn '/') (trailingWs := true) c s
|
||
else s
|
||
|
||
public def versoCommentBody : Parser where
|
||
fn := fun c s => nodeFn `Lean.Parser.Command.versoCommentBody versoCommentBodyFn c s
|
||
|
||
|
||
@[combinator_parenthesizer versoCommentBody, expose]
|
||
public def versoCommentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
|
||
|
||
open PrettyPrinter Formatter in
|
||
open Syntax.MonadTraverser in
|
||
@[combinator_formatter versoCommentBody, expose]
|
||
public def versoCommentBody.formatter : PrettyPrinter.Formatter := do
|
||
visitArgs $ do
|
||
visitAtom `«-/»
|
||
goLeft
|
||
Lean.Doc.Parser.document.formatter
|
||
|
||
def commentBody : Parser :=
|
||
{ fn := rawFn (finishCommentBlock (pushMissingOnError := true) 1) (trailingWs := true) }
|
||
|
||
@[combinator_parenthesizer commentBody, expose]
|
||
def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
|
||
@[combinator_formatter commentBody, expose]
|
||
def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
|
||
|
||
/--
|
||
A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
|
||
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.
|
||
|
||
At parse time, `docComment` checks the value of the `doc.verso` option. If it is true, the contents
|
||
are parsed as Verso markup. If not, the contents are treated as plain text or Markdown. Use
|
||
`plainDocComment` to always treat the contents as plain text.
|
||
|
||
A plain text doc comment node contains a `/--` atom and then the remainder of the comment, `foo -/`
|
||
in this example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node.
|
||
A Verso comment node contains the `/--` atom, the document's syntax tree, and a closing `-/` atom.
|
||
-/
|
||
-- @[builtin_doc] -- FIXME: suppress the hover
|
||
@[run_builtin_parser_attribute_hooks]
|
||
def docComment := leading_parser
|
||
ppDedent $ "/--" >> ppSpace >> Doc.Parser.ifVerso versoCommentBody commentBody >> ppLine
|
||
|
||
@[inherit_doc docComment, run_builtin_parser_attribute_hooks]
|
||
def plainDocComment : Parser := Doc.Parser.withoutVersoSyntax docComment
|
||
|
||
end Command
|
||
|
||
def darrow : Parser := " => "
|
||
def semicolonOrLinebreak := ";" <|> checkLinebreakBefore >> pushNone
|
||
|
||
namespace Term
|
||
|
||
/-! # Built-in parsers -/
|
||
|
||
/-- `by tac` constructs a term of the expected type by running the tactic(s) `tac`. -/
|
||
@[builtin_term_parser] def byTactic := leading_parser:leadPrec
|
||
ppAllowUngrouped >> "by " >> Tactic.tacticSeqIndentGt
|
||
|
||
/-
|
||
This is the same as `byTactic`, but it uses a different syntax kind. This is
|
||
used by `show` and `suffices` instead of `byTactic` because these syntaxes don't
|
||
support arbitrary terms where `byTactic` is accepted. Mathport uses this to e.g.
|
||
safely find-replace `by exact $e` by `$e` in any context without causing
|
||
incorrect syntax when the full expression is `show $T by exact $e`. -/
|
||
def byTactic' := leading_parser
|
||
"by " >> Tactic.tacticSeqIndentGt
|
||
|
||
-- TODO: rename to e.g. `afterSemicolonOrLinebreak`
|
||
def optSemicolon (p : Parser) : Parser :=
|
||
ppDedent $ semicolonOrLinebreak >> ppLine >> p
|
||
|
||
-- `checkPrec` necessary for the pretty printer
|
||
@[builtin_term_parser] def ident :=
|
||
checkPrec maxPrec >> Parser.ident
|
||
@[builtin_term_parser] def num : Parser :=
|
||
checkPrec maxPrec >> numLit
|
||
@[builtin_term_parser] def scientific : Parser :=
|
||
checkPrec maxPrec >> scientificLit
|
||
@[builtin_term_parser] def str : Parser :=
|
||
checkPrec maxPrec >> strLit
|
||
@[builtin_term_parser] def char : Parser :=
|
||
checkPrec maxPrec >> charLit
|
||
/-- A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. -/
|
||
@[builtin_term_parser] def type := leading_parser
|
||
"Type" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
|
||
/-- A specific universe in Lean's infinite hierarchy of universes. -/
|
||
@[builtin_term_parser] def sort := leading_parser
|
||
"Sort" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
|
||
/-- The universe of propositions. `Prop ≡ Sort 0`.
|
||
|
||
Every proposition is propositionally equal to either `True` or `False`. -/
|
||
@[builtin_term_parser] def prop := leading_parser
|
||
"Prop"
|
||
|
||
|
||
/--
|
||
The `sorry` term is a temporary placeholder for a missing proof or value.
|
||
|
||
The syntax is intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton.
|
||
Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it,
|
||
but you can double check if a declaration depends on `sorry` by looking for `sorryAx` in the output
|
||
of the `#print axioms my_thm` command, the axiom used by the implementation of `sorry`.
|
||
|
||
"Go to definition" on `sorry` in the Infoview will go to the source position where it was introduced, if such information is available.
|
||
|
||
Each `sorry` is guaranteed to be unique, so for example the following fails:
|
||
```lean
|
||
example : (sorry : Nat) = sorry := rfl -- fails
|
||
```
|
||
|
||
See also the `sorry` tactic, which is short for `exact sorry`.
|
||
-/
|
||
@[builtin_term_parser] def «sorry» := leading_parser
|
||
"sorry"
|
||
-- Left parenthesis with hygiene info, for cdot function expansion.
|
||
def hygienicLParen : Parser := leading_parser (withAnonymousAntiquot := false)
|
||
"(" >> hygieneInfo
|
||
/--
|
||
A placeholder for an implicit lambda abstraction's variable. The lambda abstraction is scoped to the surrounding parentheses.
|
||
For example, `(· + ·)` is equivalent to `fun x y => x + y`. Tuple notation and type ascription notation also serve as scopes.
|
||
Note that `(· : ty)` expands to `((fun x => x) : ty)`, so `ty` should be a function type.
|
||
-/
|
||
@[builtin_term_parser] def cdot := leading_parser
|
||
unicodeSymbol "·" "." >> hygieneInfo
|
||
/--
|
||
Type ascription notation: `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
|
||
An empty type ascription `(e :)` elaborates `e` without the expected type.
|
||
This is occasionally useful when Lean's heuristics for filling arguments from the expected type
|
||
do not yield the right result.
|
||
-/
|
||
@[builtin_term_parser] def typeAscription := leading_parser
|
||
hygienicLParen >> (withoutPosition (withoutForbidden (termParser >> " :" >> optional (ppSpace >> termParser)))) >> ")"
|
||
|
||
/-- Tuple notation; `()` is short for `Unit.unit`, `(a, b, c)` for `Prod.mk a (Prod.mk b c)`, etc. -/
|
||
@[builtin_term_parser] def tuple := leading_parser
|
||
hygienicLParen >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true)))) >> ")"
|
||
|
||
recommended_spelling "mk" for "(a, b)" in [Prod.mk, tuple]
|
||
|
||
/--
|
||
Parentheses, used for grouping expressions (e.g., `a * (b + c)`).
|
||
Can also be used for creating simple functions when combined with `·`. Here are some examples:
|
||
- `(· + 1)` is shorthand for `fun x => x + 1`
|
||
- `(· + ·)` is shorthand for `fun x y => x + y`
|
||
- `(f · a b)` is shorthand for `fun x => f x a b`
|
||
- `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`
|
||
- also applies to other parentheses-like notations such as `(·, 1)` and `(· : Nat → Nat)`
|
||
-/
|
||
@[builtin_term_parser] def paren := leading_parser
|
||
hygienicLParen >> withoutPosition (withoutForbidden (ppDedentIfGrouped termParser)) >> ")"
|
||
/--
|
||
The *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the
|
||
expected type is an inductive type with a single constructor `c`.
|
||
If more terms are given than `c` has parameters, the remaining arguments
|
||
are turned into a new anonymous constructor application. For example,
|
||
`⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`.
|
||
-/
|
||
@[builtin_term_parser] def anonymousCtor := leading_parser
|
||
"⟨" >> withoutPosition (withoutForbidden (sepBy termParser ", " (allowTrailingSep := true))) >> "⟩"
|
||
def fromTerm := leading_parser
|
||
"from " >> termParser
|
||
def showRhs := fromTerm <|> byTactic'
|
||
/-- A `sufficesDecl` represents everything that comes after the `suffices` keyword:
|
||
an optional `x :`, then a term `ty`, then `from val` or `by tac`. -/
|
||
@[builtin_doc] def sufficesDecl := leading_parser
|
||
(atomic (group (binderIdent >> " : ")) <|> hygieneInfo) >> termParser >> ppSpace >> showRhs
|
||
@[builtin_term_parser] def «suffices» := leading_parser:leadPrec
|
||
withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser
|
||
@[builtin_term_parser] def «show» := leading_parser:leadPrec "show " >> termParser >> ppSpace >> showRhs
|
||
/--
|
||
`@x` disables automatic insertion of implicit parameters of the constant `x`.
|
||
`@e` for any term `e` also disables the insertion of implicit lambdas at this position.
|
||
-/
|
||
@[builtin_term_parser] def explicit := leading_parser
|
||
"@" >> termParser maxPrec
|
||
/--
|
||
`.(e)` marks an "inaccessible pattern", which does not influence evaluation of the pattern match, but may be necessary for type-checking.
|
||
In contrast to regular patterns, `e` may be an arbitrary term of the appropriate type.
|
||
-/
|
||
@[builtin_term_parser] def inaccessible := leading_parser
|
||
".(" >> withoutPosition termParser >> ")"
|
||
|
||
/-
|
||
It is feasible to support dependent arrows such as `{α} → α → α` without sacrificing the quality of the error messages for the longer case.
|
||
`{α} → α → α` would be short for `{α : Type} → α → α`
|
||
Here is the encoding:
|
||
```
|
||
def implicitShortBinder := node `Lean.Parser.Term.implicitBinder $ "{" >> many1 binderIdent >> pushNone >> "}"
|
||
def depArrowShortPrefix := try (implicitShortBinder >> unicodeSymbol " → " " -> ")
|
||
def depArrowLongPrefix := bracketedBinder true >> unicodeSymbol " → " " -> "
|
||
def depArrowPrefix := depArrowShortPrefix <|> depArrowLongPrefix
|
||
@[builtin_term_parser] def depArrow := leading_parser depArrowPrefix >> termParser
|
||
```
|
||
Note that no changes in the elaborator are needed.
|
||
We decided to not use it because terms such as `{α} → α → α` may look too cryptic.
|
||
Note that we did not add a `explicitShortBinder` parser since `(α) → α → α` is really cryptic as a short for `(α : Type) → α → α`.
|
||
-/
|
||
@[builtin_term_parser] def depArrow := leading_parser:25
|
||
bracketedBinder true >> unicodeSymbol " → " " -> " >> termParser
|
||
|
||
@[builtin_term_parser]
|
||
def «forall» := leading_parser:leadPrec
|
||
unicodeSymbol "∀" "forall" >>
|
||
many1 (ppSpace >> (binderIdent <|> bracketedBinder)) >>
|
||
optType >> ", " >> termParser
|
||
|
||
def matchAlt (rhsParser : Parser := termParser) : Parser :=
|
||
leading_parser (withAnonymousAntiquot := false)
|
||
"| " >> ppIndent (
|
||
sepBy1 (sepBy1 termParser ", ") " | " >> darrow >>
|
||
checkColGe "alternative right-hand-side to start in a column greater than or equal to the corresponding '|'" >>
|
||
rhsParser)
|
||
/--
|
||
Useful for syntax quotations. Note that generic patterns such as `` `(matchAltExpr| | ... => $rhs) `` should also
|
||
work with other `rhsParser`s (of arity 1). -/
|
||
def matchAltExpr := matchAlt
|
||
|
||
instance : Coe (TSyntax ``matchAltExpr) (TSyntax ``matchAlt) where
|
||
coe stx := ⟨stx.raw⟩
|
||
|
||
def matchAlts (rhsParser : Parser := termParser) : Parser :=
|
||
leading_parser withPosition $ many1Indent (ppLine >> matchAlt rhsParser)
|
||
|
||
/-- `matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as
|
||
`match h1 : e1, e2, h3 : e3 with ...`. -/
|
||
@[builtin_doc] def matchDiscr := leading_parser
|
||
optional (atomic (binderIdent >> " : ")) >> termParser
|
||
|
||
def trueVal := leading_parser nonReservedSymbol "true"
|
||
def falseVal := leading_parser nonReservedSymbol "false"
|
||
def generalizingParam := leading_parser
|
||
atomic ("(" >> nonReservedSymbol "generalizing") >> " := " >>
|
||
(trueVal <|> falseVal) >> ")" >> ppSpace
|
||
|
||
def motive := leading_parser
|
||
atomic ("(" >> nonReservedSymbol "motive" >> " := ") >>
|
||
withoutPosition termParser >> ")" >> ppSpace
|
||
|
||
/--
|
||
Pattern matching. `match e, ... with | p, ... => f | ...` matches each given
|
||
term `e` against each pattern `p` of a match alternative. When all patterns
|
||
of an alternative match, the `match` term evaluates to the value of the
|
||
corresponding right-hand side `f` with the pattern variables bound to the
|
||
respective matched values.
|
||
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
|
||
within `f`.
|
||
|
||
When not constructing a proof, `match` does not automatically substitute variables
|
||
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
|
||
enforce this.
|
||
|
||
Syntax quotations can also be used in a pattern match.
|
||
This matches a `Syntax` value against quotations, pattern variables, or `_`.
|
||
|
||
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
|
||
names only should be done explicitly.
|
||
|
||
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
|
||
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
|
||
should participate in matching.
|
||
For example, in
|
||
```lean
|
||
syntax "c" ("foo" <|> "bar") ...
|
||
```
|
||
`foo` and `bar` are indistinguishable during matching, but in
|
||
```lean
|
||
syntax foo := "foo"
|
||
syntax "c" (foo <|> "bar") ...
|
||
```
|
||
they are not.
|
||
-/
|
||
@[builtin_term_parser] def «match» := leading_parser:leadPrec
|
||
"match " >> optional generalizingParam >> optional motive >> sepBy1 matchDiscr ", " >>
|
||
" with" >> ppDedent matchAlts
|
||
/--
|
||
Empty match/ex falso. `nomatch e` is of arbitrary type `α : Sort u` if
|
||
Lean can show that an empty set of patterns is exhaustive given `e`'s type,
|
||
e.g. because it has no constructors.
|
||
-/
|
||
@[builtin_term_parser] def «nomatch» := leading_parser:leadPrec "nomatch " >> sepBy1 termParser ", "
|
||
|
||
@[builtin_term_parser] def «nofun» := leading_parser "nofun"
|
||
|
||
/--
|
||
Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
|
||
inherited. If `e` is itself a variable called `x`, it can be elided:
|
||
`fun y => { x := 1, y }`.
|
||
A *structure update* of an existing value can be given via `with`:
|
||
`{ point with x := 1 }`.
|
||
The structure type can be specified if not inferable:
|
||
`{ x := 1, y := 2 : Point }`.
|
||
-/
|
||
@[builtin_term_parser] def structInst := leading_parser
|
||
"{ " >> withoutPosition (optional (atomic (sepBy1 termParser ", " >> " with "))
|
||
>> structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
|
||
>> optEllipsis
|
||
>> optional (" : " >> termParser)) >> " }"
|
||
|
||
@[builtin_structInstFieldDecl_parser]
|
||
def structInstFieldDef := leading_parser
|
||
" := " >> optional "private" >> termParser
|
||
@[builtin_structInstFieldDecl_parser]
|
||
def structInstFieldEqns := leading_parser
|
||
optional "private" >> matchAlts
|
||
|
||
def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <|
|
||
atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
|
||
def funStrictImplicitBinder :=
|
||
atomic (lookahead (
|
||
strictImplicitLeftBracket >> many1 binderIdent >>
|
||
(symbol " : " <|> strictImplicitRightBracket))) >>
|
||
strictImplicitBinder
|
||
def funBinder : Parser :=
|
||
withAntiquot (mkAntiquot "funBinder" decl_name% (isPseudoKind := true)) <|
|
||
funStrictImplicitBinder <|> funImplicitBinder <|> instBinder <|> termParser maxPrec
|
||
-- NOTE: we disable anonymous antiquotations to ensure that `fun $b => ...`
|
||
-- remains a `term` antiquotation
|
||
def basicFun : Parser := leading_parser (withAnonymousAntiquot := false)
|
||
ppGroup (many1 (ppSpace >> funBinder) >> optType >> unicodeSymbol " ↦" " =>" (preserveForPP := true)) >> ppSpace >> termParser
|
||
@[builtin_term_parser] def «fun» := leading_parser:maxPrec
|
||
ppAllowUngrouped >> unicodeSymbol "λ" "fun" (preserveForPP := true) >> (basicFun <|> matchAlts)
|
||
|
||
def optExprPrecedence := optional (atomic ":" >> termParser maxPrec)
|
||
def withAnonymousAntiquot := leading_parser
|
||
atomic (" (" >> nonReservedSymbol "withAnonymousAntiquot" >> " := ") >>
|
||
(trueVal <|> falseVal) >> ")"
|
||
@[builtin_term_parser] def «leading_parser» := leading_parser:leadPrec
|
||
"leading_parser" >> optExprPrecedence >> optional withAnonymousAntiquot >> ppSpace >> termParser
|
||
@[builtin_term_parser] def «trailing_parser» := leading_parser:leadPrec
|
||
"trailing_parser" >> optExprPrecedence >> optExprPrecedence >> ppSpace >> termParser
|
||
|
||
/--
|
||
Indicates that an argument to a function marked `@[extern]` is borrowed.
|
||
|
||
Being borrowed only affects the ABI and runtime behavior of the function when compiled or interpreted. From the perspective of Lean's type system, this annotation has no effect. It similarly has no effect on functions not marked `@[extern]`.
|
||
|
||
When a function argument is borrowed, the function does not consume the value. This means that the function will not decrement the value's reference count or deallocate it, and the caller is responsible for doing so.
|
||
|
||
Please see https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=ffi-borrowing for a complete description.
|
||
-/
|
||
@[builtin_term_parser] def borrowed := leading_parser
|
||
"@& " >> termParser leadPrec
|
||
/-- A literal of type `Name`. -/
|
||
@[builtin_term_parser] def quotedName := leading_parser nameLit
|
||
/--
|
||
A resolved name literal. Evaluates to the full name of the given constant if
|
||
existent in the current context, or else fails.
|
||
-/
|
||
-- use `rawCh` because ``"`" >> ident`` overlaps with `nameLit`, with the latter being preferred by the tokenizer
|
||
-- note that we cannot use ```"``"``` as a new token either because it would break `precheckedQuot`
|
||
@[builtin_term_parser] def doubleQuotedName := leading_parser
|
||
"`" >> checkNoWsBefore >> rawCh '`' (trailingWs := false) >> ident
|
||
|
||
def letId := leading_parser (withAnonymousAntiquot := false)
|
||
(ppSpace >> binderIdent >> notFollowedBy (checkNoWsBefore "" >> "[")
|
||
"space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`")
|
||
<|> hygieneInfo
|
||
def letIdBinder :=
|
||
withAntiquot (mkAntiquot "letIdBinder" decl_name% (isPseudoKind := true)) <|
|
||
binderIdent <|> bracketedBinder
|
||
/- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/
|
||
def letIdLhs : Parser :=
|
||
letId >> many (ppSpace >> letIdBinder) >> optType
|
||
def letIdDecl := leading_parser (withAnonymousAntiquot := false)
|
||
atomic (letIdLhs >> " := ") >> termParser
|
||
/- Remark: `requireParens` forces the pattern to have parentheses, for trying before `letIdDecl`.
|
||
We need this because for `let (rfl) := h`, which would parse as `letIdDecl` due to `hygieneInfo`. -/
|
||
def letPatDecl (requireParens := false) := leading_parser (withAnonymousAntiquot := false)
|
||
atomic (ppSpace >> (if requireParens then lookahead "(" >> paren else termParser) >> pushNone >> optType >> " := ") >> termParser
|
||
/-
|
||
Remark: the following `(" := " <|> matchAlts)` is a hack we use
|
||
to produce a better error message at `letDecl`.
|
||
Consider this following example
|
||
```
|
||
def myFun (n : Nat) : IO Nat :=
|
||
let q ← (10 : Nat)
|
||
n + q
|
||
```
|
||
Without the hack, we get the error `expected '|'` at `←`. Reason: at `letDecl`,
|
||
we use the parser `(letIdDecl <|> letPatDecl <|> letEqnsDecl)`,
|
||
`letIdDecl` and `letEqnsDecl` have the same prefix `letIdLhs`, but `letIdDecl` uses `atomic`.
|
||
Note that the hack relies on the fact that the parser `":="` never succeeds
|
||
at `(" := " <|> matchAlts)`.
|
||
It is there just to make sure we produce the error `expected ':=' or '|'`
|
||
-/
|
||
def letEqnsDecl := leading_parser (withAnonymousAntiquot := false)
|
||
letIdLhs >> (" := " <|> matchAlts)
|
||
/-- `letDecl` matches the body of a let declaration `let f x1 x2 := e`,
|
||
`let pat := e` (where `pat` is an arbitrary term) or `let f | pat1 => e1 | pat2 => e2 ...`
|
||
(a pattern matching declaration), except for the `let` keyword itself.
|
||
`let rec` declarations are not handled here. -/
|
||
@[builtin_doc] def letDecl := leading_parser (withAnonymousAntiquot := false)
|
||
-- Remark: we disable anonymous antiquotations here to make sure
|
||
-- anonymous antiquotations (e.g., `$x`) are not `letDecl`
|
||
notFollowedBy (nonReservedSymbol "rec") "rec" >>
|
||
(letPatDecl true <|> letIdDecl <|> letPatDecl <|> letEqnsDecl)
|
||
/--
|
||
`+nondep` elaborates as a nondependent `let`, a `have` expression.
|
||
-/
|
||
@[builtin_doc] def letOptNondep := leading_parser
|
||
nonReservedSymbol "nondep"
|
||
/--
|
||
`+postponeValue` causes the body of the `let` to be elaborated before the value.
|
||
-/
|
||
@[builtin_doc] def letOptPostponeValue := leading_parser
|
||
nonReservedSymbol "postponeValue"
|
||
/--
|
||
`+usedOnly` causes unused `let`s bindings to be eliminated.
|
||
-/
|
||
@[builtin_doc] def letOptUsedOnly := leading_parser
|
||
nonReservedSymbol "usedOnly"
|
||
/--
|
||
`+zeta` immediately inlines the `let` value after elaboration (it zeta reduces the `let`).
|
||
-/
|
||
@[builtin_doc] def letOptZeta := leading_parser
|
||
nonReservedSymbol "zeta"
|
||
/--
|
||
`+generalize` directs `let`/`have` to generalize the value from the expected type before elaborating the body.
|
||
-/
|
||
@[builtin_doc] def letOptGeneralize := leading_parser
|
||
nonReservedSymbol "generalize"
|
||
def letOpts := leading_parser
|
||
letOptNondep <|> letOptPostponeValue <|> letOptUsedOnly <|> letOptZeta <|> letOptGeneralize
|
||
def letPosOpt := leading_parser (withAnonymousAntiquot := false)
|
||
" +" >> checkNoWsBefore >> letOpts
|
||
def letNegOpt := leading_parser (withAnonymousAntiquot := false)
|
||
" -" >> checkNoWsBefore >> letOpts
|
||
/--
|
||
`let (eq := h) x := v; ...` adds the equality `h : x = v` to the context while elaborating the body.
|
||
-/
|
||
@[builtin_doc] def letOptEq := leading_parser (withAnonymousAntiquot := false)
|
||
atomic (" (" >> nonReservedSymbol "eq" >> " := ") >> binderIdent >> ")"
|
||
def letConfigItem := letPosOpt <|> letNegOpt <|> letOptEq
|
||
/-- Configuration options for `let` tactics. -/
|
||
def letConfig := leading_parser (withAnonymousAntiquot := false)
|
||
many letConfigItem
|
||
/--
|
||
`let` is used to declare a local definition. Example:
|
||
```
|
||
let x := 1
|
||
let y := x + 1
|
||
x + y
|
||
```
|
||
Since functions are first class citizens in Lean, you can use `let` to declare
|
||
local functions too.
|
||
```
|
||
let double := fun x => 2*x
|
||
double (double 3)
|
||
```
|
||
For recursive definitions, you should use `let rec`.
|
||
You can also perform pattern matching using `let`. For example,
|
||
assume `p` has type `Nat × Nat`, then you can write
|
||
```
|
||
let (x, y) := p
|
||
x + y
|
||
```
|
||
|
||
The *anaphoric let* `let := v` defines a variable called `this`.
|
||
-/
|
||
@[builtin_term_parser] def «let» := leading_parser:leadPrec
|
||
withPosition ("let" >> letConfig >> letDecl) >> optSemicolon termParser
|
||
/--
|
||
`have` is used to declare local hypotheses and opaque local definitions.
|
||
|
||
It has the same syntax as `let`, and it is equivalent to `let +nondep`,
|
||
creating a *nondependent* let expression.
|
||
-/
|
||
@[builtin_term_parser] def «have» := leading_parser:leadPrec
|
||
withPosition ("have" >> letConfig >> letDecl) >> optSemicolon termParser
|
||
/--
|
||
`let_fun x := v; b` is deprecated syntax sugar for `have x := v; b`.
|
||
-/
|
||
@[builtin_term_parser] def «let_fun» := leading_parser:leadPrec
|
||
withPosition ((symbol "let_fun " <|> "let_λ ") >> letDecl) >> optSemicolon termParser
|
||
/--
|
||
`let_delayed x := v; b` is similar to `let x := v; b`, but `b` is elaborated before `v`.
|
||
-/
|
||
@[builtin_term_parser] def «let_delayed» := leading_parser:leadPrec
|
||
withPosition ("let_delayed " >> letDecl) >> optSemicolon termParser
|
||
/--
|
||
`let`-declaration that is only included in the elaborated term if variable is still there.
|
||
It is often used when building macros.
|
||
-/
|
||
@[builtin_term_parser] def «let_tmp» := leading_parser:leadPrec
|
||
withPosition ("let_tmp " >> letDecl) >> optSemicolon termParser
|
||
/-- `haveI` behaves like `have`, but inlines the value instead of producing a `have` term. -/
|
||
@[builtin_term_parser] def «haveI» := leading_parser
|
||
withPosition ("haveI " >> letConfig >> letDecl) >> optSemicolon termParser
|
||
/-- `letI` behaves like `let`, but inlines the value instead of producing a `let` term. -/
|
||
@[builtin_term_parser] def «letI» := leading_parser
|
||
withPosition ("letI " >> letConfig >> letDecl) >> optSemicolon termParser
|
||
|
||
def «scoped» := leading_parser "scoped "
|
||
def «local» := leading_parser "local "
|
||
/-- `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. -/
|
||
@[builtin_doc] def attrKind := leading_parser optional («scoped» <|> «local»)
|
||
def attrInstance := ppGroup $ leading_parser attrKind >> attrParser
|
||
|
||
def attributes := leading_parser
|
||
"@[" >> withoutPosition (sepBy1 attrInstance ", ") >> "] "
|
||
|
||
end Term
|
||
namespace Termination
|
||
|
||
/-
|
||
Termination suffix parsers, typically thought of as part of a command, but due to
|
||
letrec we need them here already.
|
||
-/
|
||
|
||
/--
|
||
Specify a termination measure for recursive functions.
|
||
```
|
||
termination_by a - b
|
||
```
|
||
indicates that termination of the currently defined recursive function follows
|
||
because the difference between the arguments `a` and `b` decreases.
|
||
|
||
If the function takes further argument after the colon, you can name them as follows:
|
||
```
|
||
def example (a : Nat) : Nat → Nat → Nat :=
|
||
termination_by b c => a - b
|
||
```
|
||
|
||
By default, a `termination_by` clause will cause the function to be constructed using well-founded
|
||
recursion. The syntax `termination_by structural a` (or `termination_by structural _ c => c`)
|
||
indicates the function is expected to be structural recursive on the argument. In this case
|
||
the body of the `termination_by` clause must be one of the function's parameters.
|
||
|
||
If omitted, a termination measure will be inferred. If written as `termination_by?`,
|
||
the inferred termination measure will be suggested.
|
||
|
||
-/
|
||
@[builtin_doc] def terminationBy := leading_parser
|
||
"termination_by " >>
|
||
optional (nonReservedSymbol "structural ") >>
|
||
optional (atomic (many (ppSpace >> Term.binderIdent) >> " => ")) >>
|
||
termParser
|
||
|
||
@[inherit_doc terminationBy, builtin_doc]
|
||
def terminationBy? := leading_parser
|
||
"termination_by?"
|
||
|
||
/--
|
||
Defines a possibly non-terminating function as a fixed-point in a suitable partial order.
|
||
|
||
Such a function is compiled as if it was marked `partial`, but its equations are provided as
|
||
theorems, so that it can be verified.
|
||
|
||
In general it accepts functions whose return type has a `Lean.Order.CCPO` instance and whose
|
||
definition is `Lean.Order.monotone` with regard to its recursive calls.
|
||
|
||
Common special cases are
|
||
|
||
* Functions whose type is inhabited a-priori (as with `partial`), and where all recursive
|
||
calls are in tail-call position.
|
||
* Monadic in certain “monotone chain-complete monads” (in particular, `Option`) composed using
|
||
the bind operator and other supported monadic combinators.
|
||
|
||
By default, the monotonicity proof is performed by the compositional `monotonicity` tactic. Using
|
||
the syntax `partial_fixpoint monotonicity by $tac` the proof can be done manually.
|
||
-/
|
||
@[builtin_doc] def partialFixpoint := leading_parser
|
||
withPosition (
|
||
"partial_fixpoint" >>
|
||
optional (checkColGt "indentation" >> nonReservedSymbol "monotonicity " >>
|
||
checkColGt "indented monotonicity proof" >> termParser))
|
||
|
||
/--
|
||
Defines a coinductive predicate using lattice theory, based on the Knaster-Tarski fixpoint theorem.
|
||
|
||
This feature constructs coinductive predicates by leveraging the lattice structure on `Prop`
|
||
and ensures correctness through monotonicity.
|
||
|
||
The coinductive predicate is defined as the greatest fixed point of a monotone function on `Prop`.
|
||
|
||
By default, monotonicity is verified automatically. However, users can provide custom proofs
|
||
of monotonicity if needed.
|
||
-/
|
||
def coinductiveFixpoint := leading_parser
|
||
withPosition (
|
||
"coinductive_fixpoint" >>
|
||
optional (checkColGt "indentation" >> nonReservedSymbol "monotonicity " >>
|
||
checkColGt "indented monotonicity proof" >> termParser))
|
||
|
||
/--
|
||
Defines an inductive predicate using lattice theory, based on the Knaster-Tarski fixpoint theorem.
|
||
|
||
This feature constructs inductive predicates by leveraging the lattice structure on `Prop`
|
||
and ensures correctness through monotonicity.
|
||
|
||
The inductive predicate is defined as the least fixed point of a monotone function on `Prop`.
|
||
|
||
By default, monotonicity is verified automatically. However, users can provide custom proofs
|
||
of monotonicity if needed.
|
||
-/
|
||
def inductiveFixpoint := leading_parser
|
||
withPosition (
|
||
"inductive_fixpoint" >>
|
||
optional (checkColGt "indentation" >> nonReservedSymbol "monotonicity " >>
|
||
checkColGt "indented monotonicity proof" >> termParser))
|
||
|
||
/--
|
||
Manually prove that the termination measure (as specified with `termination_by` or inferred)
|
||
decreases at each recursive call.
|
||
|
||
By default, the tactic `decreasing_tactic` is used.
|
||
|
||
Forces the use of well-founded recursion and is hence incompatible with
|
||
`termination_by structural`.
|
||
-/
|
||
@[builtin_doc] def decreasingBy := leading_parser
|
||
ppDedent ppLine >> "decreasing_by " >> Tactic.tacticSeqIndentGt
|
||
|
||
/--
|
||
Termination hints are `termination_by` and `decreasing_by`, in that order.
|
||
-/
|
||
@[builtin_doc] def suffix := leading_parser
|
||
optional (ppDedent ppLine >> (terminationBy? <|> terminationBy <|> partialFixpoint <|> coinductiveFixpoint <|> inductiveFixpoint)) >> optional decreasingBy
|
||
|
||
end Termination
|
||
namespace Term
|
||
|
||
/-- `letRecDecl` matches the body of a let-rec declaration: a doc comment, attributes, and then
|
||
a let declaration without the `let` keyword, such as `/-- foo -/ @[simp] bar := 1`. -/
|
||
@[builtin_doc] def letRecDecl := leading_parser
|
||
optional Command.docComment >> optional «attributes» >> letDecl >> Termination.suffix
|
||
/-- `letRecDecls` matches `letRecDecl,+`, a comma-separated list of let-rec declarations (see `letRecDecl`). -/
|
||
-- @[builtin_doc] -- FIXME: suppress the hover
|
||
def letRecDecls := leading_parser
|
||
sepBy1 letRecDecl ", "
|
||
@[builtin_term_parser]
|
||
def «letrec» := leading_parser:leadPrec
|
||
withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >>
|
||
optSemicolon termParser
|
||
|
||
/--
|
||
A named subsection of `where ... finally`. In the future, sections such as `decreasing_by` might become
|
||
syntactic sugar for an `where ... finally` subsection `| decreasing => ...`.
|
||
-/
|
||
def whereFinallySubsection := leading_parser
|
||
ppLine >> "| " >> ident >> darrow >> Tactic.tacticSeq
|
||
|
||
/--
|
||
The `finally` section trailing a `where` opens a tactic block to fill in `?hole`s in the definition body.
|
||
-/
|
||
@[builtin_doc] def whereFinally := leading_parser
|
||
ppDedent ppLine >> "finally " >> optional Tactic.tacticSeqIndentGt >> manyIndent whereFinallySubsection
|
||
|
||
@[run_builtin_parser_attribute_hooks]
|
||
def whereDecls := leading_parser
|
||
ppDedent ppLine >> "where" >> sepByIndent (ppGroup letRecDecl) "; " (allowTrailingSep := true) >> optional whereFinally
|
||
|
||
@[run_builtin_parser_attribute_hooks]
|
||
def matchAltsWhereDecls := leading_parser
|
||
matchAlts >> Termination.suffix >> optional whereDecls
|
||
|
||
@[builtin_term_parser] def noindex := leading_parser
|
||
"no_index " >> termParser maxPrec
|
||
|
||
/--
|
||
`unsafe t : α` is an expression constructor which allows using unsafe declarations inside the
|
||
body of `t : α`, by creating an auxiliary definition containing `t` and using `implementedBy` to
|
||
wrap it in a safe interface. It is required that `α` is nonempty for this to be sound,
|
||
but even beyond that, an `unsafe` block should be carefully inspected for memory safety because
|
||
the compiler is unable to guarantee the safety of the operation.
|
||
|
||
For example, the `evalExpr` function is unsafe, because the compiler cannot guarantee that when
|
||
you call ```evalExpr Foo ``Foo e``` that the type `Foo` corresponds to the name `Foo`, but in a
|
||
particular use case, we can ensure this, so `unsafe (evalExpr Foo ``Foo e)` is a correct usage.
|
||
-/
|
||
@[builtin_term_parser] def «unsafe» := leading_parser:leadPrec "unsafe " >> termParser
|
||
|
||
/-- `binrel% r a b` elaborates `r a b` as a binary relation using the type propagation protocol in `Lean.Elab.Extra`. -/
|
||
@[builtin_term_parser] def binrel := leading_parser
|
||
"binrel% " >> ident >> ppSpace >> termParser maxPrec >> ppSpace >> termParser maxPrec
|
||
/-- `binrel_no_prop% r a b` is similar to `binrel% r a b`, but it coerces `Prop` arguments into `Bool`. -/
|
||
@[builtin_term_parser] def binrel_no_prop := leading_parser
|
||
"binrel_no_prop% " >> ident >> ppSpace >> termParser maxPrec >> ppSpace >> termParser maxPrec
|
||
/-- `binop% f a b` elaborates `f a b` as a binary operation using the type propagation protocol in `Lean.Elab.Extra`. -/
|
||
@[builtin_term_parser] def binop := leading_parser
|
||
"binop% " >> ident >> ppSpace >> termParser maxPrec >> ppSpace >> termParser maxPrec
|
||
/-- `binop_lazy%` is similar to `binop% f a b`, but it wraps `b` as a function from `Unit`. -/
|
||
@[builtin_term_parser] def binop_lazy := leading_parser
|
||
"binop_lazy% " >> ident >> ppSpace >> termParser maxPrec >> ppSpace >> termParser maxPrec
|
||
/-- `leftact% f a b` elaborates `f a b` as a left action using the type propagation protocol in `Lean.Elab.Extra`.
|
||
In particular, it is like a unary operation with a fixed parameter `a`, where only the right argument `b` participates in the operator coercion elaborator. -/
|
||
@[builtin_term_parser] def leftact := leading_parser
|
||
"leftact% " >> ident >> ppSpace >> termParser maxPrec >> ppSpace >> termParser maxPrec
|
||
/-- `rightact% f a b` elaborates `f a b` as a right action using the type propagation protocol in `Lean.Elab.Extra`.
|
||
In particular, it is like a unary operation with a fixed parameter `b`, where only the left argument `a` participates in the operator coercion elaborator. -/
|
||
@[builtin_term_parser] def rightact := leading_parser
|
||
"rightact% " >> ident >> ppSpace >> termParser maxPrec >> ppSpace >> termParser maxPrec
|
||
/-- `unop% f a` elaborates `f a` as a unary operation using the type propagation protocol in `Lean.Elab.Extra`. -/
|
||
@[builtin_term_parser] def unop := leading_parser
|
||
"unop% " >> ident >> ppSpace >> termParser maxPrec
|
||
|
||
@[builtin_term_parser] def forInMacro := leading_parser
|
||
"for_in% " >> termParser maxPrec >> termParser maxPrec >> ppSpace >> termParser maxPrec
|
||
@[builtin_term_parser] def forInMacro' := leading_parser
|
||
"for_in'% " >> termParser maxPrec >> termParser maxPrec >> ppSpace >> termParser maxPrec
|
||
|
||
/-- A macro which evaluates to the name of the currently elaborating declaration. -/
|
||
@[builtin_term_parser] def declName := leading_parser "decl_name%"
|
||
|
||
/-- `private_decl% e` elaborates `e` in a private context and wraps the result in a helper `def`. -/
|
||
@[builtin_term_parser] def «privateDecl» :=
|
||
leading_parser "private_decl% " >> termParser maxPrec
|
||
|
||
/--
|
||
* `with_decl_name% id e` elaborates `e` in a context while changing the effective
|
||
declaration name to `id`.
|
||
* `with_decl_name% ?id e` does the same, but resolves `id` as a new definition name
|
||
(appending the current namespaces).
|
||
-/
|
||
@[builtin_term_parser] def withDeclName := leading_parser
|
||
"with_decl_name% " >> optional "?" >> ident >> ppSpace >> termParser
|
||
@[builtin_term_parser] def typeOf := leading_parser
|
||
"type_of% " >> termParser maxPrec
|
||
@[builtin_term_parser] def ensureTypeOf := leading_parser
|
||
"ensure_type_of% " >> termParser maxPrec >> strLit >> ppSpace >> termParser
|
||
@[builtin_term_parser] def ensureExpectedType := leading_parser
|
||
"ensure_expected_type% " >> strLit >> ppSpace >> termParser maxPrec
|
||
@[builtin_term_parser] def noImplicitLambda := leading_parser
|
||
"no_implicit_lambda% " >> termParser maxPrec
|
||
/--
|
||
`value_of% x` elaborates to the value of `x`, which can be a local or global definition.
|
||
-/
|
||
@[builtin_term_parser] def valueOf := leading_parser
|
||
"value_of% " >> ident
|
||
|
||
/--
|
||
`clear% x; e` elaborates `x` after clearing the free variable `x` from the local context.
|
||
If `x` cannot be cleared (due to dependencies), it will keep `x` without failing.
|
||
-/
|
||
@[builtin_term_parser] def clear := leading_parser
|
||
"clear% " >> ident >> semicolonOrLinebreak >> ppDedent ppLine >> termParser
|
||
|
||
@[builtin_term_parser] def letMVar := leading_parser
|
||
"let_mvar% " >> "?" >> ident >> " := " >> termParser >> "; " >> termParser
|
||
@[builtin_term_parser] def waitIfTypeMVar := leading_parser
|
||
"wait_if_type_mvar% " >> "?" >> ident >> "; " >> termParser
|
||
@[builtin_term_parser] def waitIfTypeContainsMVar := leading_parser
|
||
"wait_if_type_contains_mvar% " >> "?" >> ident >> "; " >> termParser
|
||
@[builtin_term_parser] def waitIfContainsMVar := leading_parser
|
||
"wait_if_contains_mvar% " >> "?" >> ident >> "; " >> termParser
|
||
|
||
@[builtin_term_parser] def defaultOrOfNonempty := leading_parser
|
||
"default_or_ofNonempty% " >> optional "unsafe"
|
||
|
||
/--
|
||
Helper parser for marking `match`-alternatives that should not trigger errors if unused.
|
||
We use them to implement `macro_rules` and `elab_rules`
|
||
-/
|
||
@[builtin_term_parser] def noErrorIfUnused := leading_parser
|
||
"no_error_if_unused% " >> termParser
|
||
|
||
def namedArgument := leading_parser (withAnonymousAntiquot := false)
|
||
atomic ("(" >> ident >> " := ") >> withoutPosition termParser >> ")"
|
||
/-- In a function application, `..` notation inserts zero or more `_` placeholders. -/
|
||
def ellipsis := leading_parser (withAnonymousAntiquot := false)
|
||
".." >> notFollowedBy (checkNoWsBefore >> ".") "`.` immediately after `..`"
|
||
def argument :=
|
||
checkWsBefore "expected space" >>
|
||
checkColGt "expected to be indented" >>
|
||
(namedArgument <|> ellipsis <|> termParser argPrec)
|
||
-- `app` precedence is `lead` (cannot be used as argument)
|
||
-- `lhs` precedence is `max` (i.e. does not accept `arg` precedence)
|
||
-- argument precedence is `arg` (i.e. does not accept `lead` precedence)
|
||
@[builtin_term_parser] def app := trailing_parser:leadPrec:maxPrec many1 argument
|
||
|
||
/--
|
||
The *extended field notation* `e.f` is roughly short for `T.f e` where `T` is the type of `e`.
|
||
More precisely,
|
||
* if `e` is of a function type, `e.f` is translated to `Function.f (p := e)`
|
||
where `p` is the first explicit parameter of function type
|
||
* if `e` is of a named type `T ...` and there is a declaration `T.f` (possibly from `export`),
|
||
`e.f` is translated to `T.f (p := e)` where `p` is the first explicit parameter of type `T ...`
|
||
* otherwise, if `e` is of a structure type,
|
||
the above is repeated for every base type of the structure.
|
||
|
||
The field index notation `e.i`, where `i` is a positive number,
|
||
is short for accessing the `i`-th field (1-indexed) of `e` if it is of a structure type. -/
|
||
@[builtin_term_parser] def proj := trailing_parser
|
||
checkNoWsBefore >> "." >> checkNoWsBefore >> (fieldIdx <|> rawIdent)
|
||
@[builtin_term_parser] def completion := trailing_parser
|
||
checkNoWsBefore >> "."
|
||
@[builtin_term_parser] def arrow := trailing_parser
|
||
checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser 25
|
||
|
||
/--
|
||
Syntax kind for syntax nodes representing the field of a projection in the `InfoTree`.
|
||
Specifically, the `InfoTree` node for a projection `s.f` contains a child `InfoTree` node
|
||
with syntax ``(Syntax.node .none identProjKind #[`f])``.
|
||
|
||
This is necessary because projection syntax cannot always be detected purely syntactically
|
||
(`s.f` may refer to either the identifier `s.f` or a projection `s.f` depending on
|
||
the available context).
|
||
-/
|
||
def identProjKind := `Lean.Parser.Term.identProj
|
||
|
||
def isIdent (stx : Syntax) : Bool :=
|
||
-- antiquotations should also be allowed where an identifier is expected
|
||
stx.isAntiquot || stx.isIdent
|
||
|
||
/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
|
||
@[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser
|
||
checkStackTop isIdent "expected preceding identifier" >>
|
||
checkNoWsBefore "no space before '.{'" >> ".{" >>
|
||
sepBy1 levelParser ", " >> "}"
|
||
/-- `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
|
||
If present, the identifier `h` is bound to a proof of `x = e`. -/
|
||
@[builtin_term_parser] def namedPattern : TrailingParser := trailing_parser
|
||
checkStackTop isIdent "expected preceding identifier" >>
|
||
checkNoWsBefore "no space before '@'" >> "@" >>
|
||
optional (atomic (ident >> ":")) >> termParser maxPrec
|
||
|
||
/--
|
||
`e |>.x` is a shorthand for `(e).x`.
|
||
It is especially useful for avoiding parentheses with repeated applications.
|
||
-/
|
||
@[builtin_term_parser] def pipeProj := trailing_parser:minPrec
|
||
" |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> many argument
|
||
@[builtin_term_parser] def pipeCompletion := trailing_parser:minPrec
|
||
" |>."
|
||
|
||
/--
|
||
`h ▸ e` is a macro built on top of `Eq.rec` and `Eq.symm` definitions.
|
||
Given `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`.
|
||
You can also view `h ▸ e` as a "type casting" operation
|
||
where you change the type of `e` by using `h`.
|
||
|
||
The macro tries both orientations of `h`. If the context provides an
|
||
expected type, it rewrites the expected type, else it rewrites the type of e`.
|
||
|
||
See the Chapter "Quantifiers and Equality" in the manual
|
||
"Theorem Proving in Lean" for additional information.
|
||
-/
|
||
@[builtin_term_parser] def subst := trailing_parser:75
|
||
" ▸ " >> sepBy1 (termParser 75) " ▸ "
|
||
|
||
def bracketedBinderF := bracketedBinder -- no default arg
|
||
instance : Coe (TSyntax ``bracketedBinderF) (TSyntax ``bracketedBinder) where coe s := ⟨s⟩
|
||
|
||
/--
|
||
`panic! msg` formally evaluates to `@Inhabited.default α` if the expected type
|
||
`α` implements `Inhabited`.
|
||
At runtime, `msg` and the file position are printed to stderr unless the C
|
||
function `lean_set_panic_messages(false)` has been executed before. If the C
|
||
function `lean_set_exit_on_panic(true)` has been executed before, the process is
|
||
then aborted.
|
||
-/
|
||
@[builtin_term_parser] def panic := leading_parser:leadPrec
|
||
"panic! " >> termParser
|
||
/-- A shorthand for `panic! "unreachable code has been reached"`. -/
|
||
@[builtin_term_parser] def unreachable := leading_parser:leadPrec
|
||
"unreachable!"
|
||
/--
|
||
`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an
|
||
interpolated string literal) to stderr. It should only be used for debugging.
|
||
-/
|
||
@[builtin_term_parser] def dbgTrace := leading_parser:leadPrec
|
||
withPosition ("dbg_trace" >> (interpolatedStr termParser <|> termParser)) >>
|
||
optSemicolon termParser
|
||
/-- `assert! cond` panics if `cond` evaluates to `false`. -/
|
||
@[builtin_term_parser] def assert := leading_parser:leadPrec
|
||
withPosition ("assert! " >> termParser) >> optSemicolon termParser
|
||
/--
|
||
`debug_assert! cond` panics if `cond` evaluates to `false` and the executing code has been built
|
||
with debug assertions enabled (see the `debugAssertions` option).
|
||
-/
|
||
@[builtin_term_parser] def debugAssert := leading_parser:leadPrec
|
||
withPosition ("debug_assert! " >> termParser) >> optSemicolon termParser
|
||
|
||
def macroArg := termParser maxPrec
|
||
def macroDollarArg := leading_parser "$" >> termParser 10
|
||
def macroLastArg := macroDollarArg <|> macroArg
|
||
|
||
/--
|
||
A state monad that uses an actual mutable reference cell (i.e. an `ST.Ref`).
|
||
|
||
This is syntax, rather than a function, to make it easier to use. Its elaborator synthesizes an
|
||
appropriate parameter for the underlying monad's `ST` effects, then passes it to `StateRefT'`.
|
||
-/
|
||
-- Macro for avoiding exponentially big terms when using `STWorld`
|
||
@[builtin_term_parser] def stateRefT := leading_parser
|
||
"StateRefT " >> macroArg >> ppSpace >> macroLastArg
|
||
|
||
@[builtin_term_parser] def dynamicQuot := withoutPosition <| leading_parser
|
||
"`(" >> ident >> "| " >> incQuotDepth (parserOfStack 1) >> ")"
|
||
|
||
@[builtin_term_parser] def dotIdent := leading_parser
|
||
"." >> checkNoWsBefore >> rawIdent
|
||
|
||
/--
|
||
Implementation of the `show_term` term elaborator.
|
||
-/
|
||
@[builtin_term_parser] def showTermElabImpl :=
|
||
leading_parser:leadPrec "show_term_elab " >> termParser
|
||
|
||
/-!
|
||
`match_expr` support.
|
||
-/
|
||
|
||
def matchExprPat := leading_parser optional (atomic (ident >> "@")) >> ident >> many binderIdent
|
||
def matchExprAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (matchExprPat >> " => " >> rhsParser)
|
||
def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (hole >> " => " >> rhsParser)
|
||
def matchExprAlts (rhsParser : Parser) :=
|
||
leading_parser withPosition $
|
||
many (ppLine >> checkColGe "irrelevant" >> notFollowedBy (symbol "| " >> " _ ") "irrelevant" >> matchExprAlt rhsParser)
|
||
>> (ppLine >> checkColGe "else-alternative for `match_expr`, i.e., `| _ => ...`" >> matchExprElseAlt rhsParser)
|
||
@[builtin_term_parser] def matchExpr := leading_parser:leadPrec
|
||
"match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser)
|
||
|
||
@[builtin_term_parser] def letExpr := leading_parser:leadPrec
|
||
withPosition ("let_expr " >> matchExprPat >> " := " >> termParser >> checkColGt >> " | " >> termParser) >> optSemicolon termParser
|
||
|
||
/--
|
||
Throws an error exception, tagging the associated message as a named error with the specified name
|
||
and validating that an associated error explanation exists. The message may be passed as an
|
||
interpolated string or a `MessageData` term. The result of `getRef` is used as position information.
|
||
-/
|
||
@[builtin_term_parser] def throwNamedErrorMacro := leading_parser
|
||
"throwNamedError " >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
|
||
|
||
/--
|
||
Throws an error exception, tagging the associated message as a named error with the specified name
|
||
and validating that an associated error explanation exists. The error name must be followed by a
|
||
`Syntax` at which the error is to be thrown. The message is the final argument and may be passed as
|
||
an interpolated string or a `MessageData` term.
|
||
-/
|
||
@[builtin_term_parser] def throwNamedErrorAtMacro := leading_parser
|
||
"throwNamedErrorAt " >> termParser maxPrec >> ppSpace >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
|
||
|
||
/--
|
||
Logs an error, tagging the message as a named error with the specified name and validating that an
|
||
associated error explanation exists. The message may be passed as an interpolated string or a
|
||
`MessageData` term. The result of `getRef` is used as position information.
|
||
-/
|
||
@[builtin_term_parser] def logNamedErrorMacro := leading_parser
|
||
"logNamedError " >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
|
||
|
||
/--
|
||
Logs an error, tagging the message as a named error with the specified name and validating that an
|
||
associated error explanation exists. The error name must be followed by a `Syntax` at which the
|
||
error is to be logged. The message is the final argument and may be passed as an interpolated string
|
||
or a `MessageData` term.
|
||
-/
|
||
@[builtin_term_parser] def logNamedErrorAtMacro := leading_parser
|
||
"logNamedErrorAt " >> termParser maxPrec >> ppSpace >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
|
||
|
||
/--
|
||
Logs a warning, tagging the message as a named diagnostic with the specified name and validating
|
||
that an associated error explanation exists. The message may be passed as an interpolated string or
|
||
a `MessageData` term. The result of `getRef` is used as position information.
|
||
-/
|
||
@[builtin_term_parser] def logNamedWarningMacro := leading_parser
|
||
"logNamedWarning " >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
|
||
|
||
/--
|
||
Logs a warning, tagging the message as a named diagnostic with the specified name and validating
|
||
that an associated error explanation exists. The error name must be followed by a `Syntax` at which
|
||
the warning is to be logged. The message is the final argument and may be passed as an interpolated
|
||
string or a `MessageData` term.
|
||
-/
|
||
@[builtin_term_parser] def logNamedWarningAtMacro := leading_parser
|
||
"logNamedWarningAt " >> termParser maxPrec >> ppSpace >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec)
|
||
|
||
end Term
|
||
|
||
@[builtin_term_parser default+1] def Tactic.quot : Parser := leading_parser
|
||
"`(tactic| " >> withoutPosition (incQuotDepth tacticParser) >> ")"
|
||
@[builtin_term_parser] def Tactic.quotSeq : Parser := leading_parser
|
||
"`(tactic| " >> withoutPosition (incQuotDepth Tactic.seq1) >> ")"
|
||
|
||
open Term in
|
||
builtin_initialize
|
||
register_parser_alias letDecl
|
||
register_parser_alias letConfig
|
||
register_parser_alias sufficesDecl
|
||
register_parser_alias letRecDecls
|
||
register_parser_alias hole
|
||
register_parser_alias syntheticHole
|
||
register_parser_alias matchDiscr
|
||
register_parser_alias bracketedBinder
|
||
register_parser_alias attrKind
|
||
register_parser_alias optSemicolon
|
||
register_parser_alias structInstFields
|
||
|
||
end Parser
|
||
end Lean
|