feat: dynamic quotations for categories
This commit is contained in:
Gabriel Ebner
Leonardo de Moura
parent
0e7afae1da
commit
fb4d90a58b
35 changed files with 170 additions and 160 deletions
|
|
@ -176,7 +176,8 @@ The modifier `local` specifies the scope of the macro.
|
|||
/-- The `have_eq lhs rhs` tactic (tries to) prove that `lhs = rhs`,
|
||||
and then replaces `lhs` with `rhs`. -/
|
||||
local macro "have_eq " lhs:term:max rhs:term:max : tactic =>
|
||||
`((have h : $lhs = $rhs :=
|
||||
`(tactic|
|
||||
(have h : $lhs = $rhs :=
|
||||
-- TODO: replace with linarith
|
||||
by simp_arith at *; apply Nat.le_antisymm <;> assumption
|
||||
try subst $lhs))
|
||||
|
|
@ -191,7 +192,7 @@ useful if `e` is the condition of an `if`-statement.
|
|||
-/
|
||||
/-- `by_cases' e` is a shorthand form `by_cases e <;> simp[*]` -/
|
||||
local macro "by_cases' " e:term : tactic =>
|
||||
`(by_cases $e <;> simp [*])
|
||||
`(tactic| by_cases $e <;> simp [*])
|
||||
|
||||
|
||||
/-!
|
||||
|
|
|
|||
|
|
@ -169,13 +169,13 @@ syntax (name := paren) "(" convSeq ")" : conv
|
|||
|
||||
/-- `rfl` closes one conv goal "trivially", by using reflexivity
|
||||
(that is, no rewriting). -/
|
||||
macro "rfl" : conv => `(tactic => rfl)
|
||||
macro "rfl" : conv => `(conv| tactic => rfl)
|
||||
|
||||
/-- `done` succeeds iff there are no goals remaining. -/
|
||||
macro "done" : conv => `(tactic' => done)
|
||||
macro "done" : conv => `(conv| tactic' => done)
|
||||
|
||||
/-- `trace_state` prints the current goal state. -/
|
||||
macro "trace_state" : conv => `(tactic' => trace_state)
|
||||
macro "trace_state" : conv => `(conv| tactic' => trace_state)
|
||||
|
||||
/-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
|
||||
macro (name := allGoals) tk:"all_goals " s:convSeq : conv =>
|
||||
|
|
@ -225,7 +225,7 @@ resulting in `t'`, which becomes the new target subgoal. -/
|
|||
syntax (name := convConvSeq) "conv" " => " convSeq : conv
|
||||
|
||||
/-- `· conv` focuses on the main conv goal and tries to solve it using `s`. -/
|
||||
macro dot:("·" <|> ".") s:convSeq : conv => `({%$dot ($s) })
|
||||
macro dot:("·" <|> ".") s:convSeq : conv => `(conv| {%$dot ($s) })
|
||||
|
||||
|
||||
/-- `fail_if_success t` fails if the tactic `t` succeeds. -/
|
||||
|
|
@ -234,12 +234,12 @@ macro (name := failIfSuccess) tk:"fail_if_success " s:convSeq : conv =>
|
|||
|
||||
/-- `rw [rules]` applies the given list of rewrite rules to the target.
|
||||
See the `rw` tactic for more information. -/
|
||||
macro "rw" c:(config)? s:rwRuleSeq : conv => `(rewrite $[$c]? $s)
|
||||
macro "rw" c:(config)? s:rwRuleSeq : conv => `(conv| rewrite $[$c]? $s)
|
||||
|
||||
/-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`.
|
||||
This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
|
||||
which only unfolds `@[reducible]` definitions). -/
|
||||
macro "erw" s:rwRuleSeq : conv => `(rw (config := { transparency := .default }) $s)
|
||||
macro "erw" s:rwRuleSeq : conv => `(conv| rw (config := { transparency := .default }) $s)
|
||||
|
||||
/-- `args` traverses into all arguments. Synonym for `congr`. -/
|
||||
macro "args" : conv => `(congr)
|
||||
|
|
@ -270,13 +270,13 @@ macro_rules
|
|||
There are no restrictions on `thm`, but strange results may occur if `thm`
|
||||
cannot be reasonably interpreted as proving one equality from a list of others. -/
|
||||
-- TODO: error if non-conv subgoals?
|
||||
macro "apply " e:term : conv => `(tactic => apply $e)
|
||||
macro "apply " e:term : conv => `(conv| tactic => apply $e)
|
||||
|
||||
/-- `first | conv | ...` runs each `conv` until one succeeds, or else fails. -/
|
||||
syntax (name := first) "first " withPosition((colGe "|" convSeq)+) : conv
|
||||
|
||||
/-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
|
||||
macro "try " t:convSeq : conv => `(first | $t | skip)
|
||||
macro "try " t:convSeq : conv => `(conv| first | $t | skip)
|
||||
|
||||
macro:1 x:conv tk:" <;> " y:conv:0 : conv =>
|
||||
`(conv| tactic' => (conv' => $x:conv) <;>%$tk (conv' => $y:conv))
|
||||
|
|
|
|||
|
|
@ -51,7 +51,7 @@ termination_by aux j _ => as.size - j
|
|||
`sizeOf arr[i] < sizeOf arr`, which is useful for well founded recursions
|
||||
over a nested inductive like `inductive T | mk : Array T → T`. -/
|
||||
macro "array_get_dec" : tactic =>
|
||||
`(first
|
||||
`(tactic| first
|
||||
| apply sizeOf_get
|
||||
| apply Nat.lt_trans (sizeOf_get ..); simp_arith)
|
||||
|
||||
|
|
|
|||
|
|
@ -125,7 +125,7 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a <
|
|||
`sizeOf a < sizeOf as` when `a ∈ as`, which is useful for well founded recursions
|
||||
over a nested inductive like `inductive T | mk : List T → T`. -/
|
||||
macro "sizeOf_list_dec" : tactic =>
|
||||
`(first
|
||||
`(tactic| first
|
||||
| apply sizeOf_lt_of_mem; assumption; done
|
||||
| apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
|
||||
case' h => assumption
|
||||
|
|
|
|||
|
|
@ -1283,7 +1283,7 @@ namespace Parser.Tactic
|
|||
This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
|
||||
which only unfolds `@[reducible]` definitions). -/
|
||||
macro "erw " s:rwRuleSeq loc:(location)? : tactic =>
|
||||
`(rw (config := { transparency := .default }) $s $(loc)?)
|
||||
`(tactic| rw (config := { transparency := .default }) $s $(loc)?)
|
||||
|
||||
syntax simpAllKind := atomic("(" &"all") " := " &"true" ")"
|
||||
syntax dsimpKind := atomic("(" &"dsimp") " := " &"true" ")"
|
||||
|
|
|
|||
|
|
@ -236,7 +236,7 @@ and push it to the front `n` times. If `n` is omitted, it defaults to `1`.
|
|||
syntax (name := rotateRight) "rotate_right" (num)? : tactic
|
||||
|
||||
/-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
|
||||
macro "try " t:tacticSeq : tactic => `(first | $t | skip)
|
||||
macro "try " t:tacticSeq : tactic => `(tactic| first | $t | skip)
|
||||
|
||||
/--
|
||||
`tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal,
|
||||
|
|
@ -464,7 +464,7 @@ syntax (name := unfold) "unfold " (colGt ident)+ (location)? : tactic
|
|||
Auxiliary macro for lifting have/suffices/let/...
|
||||
It makes sure the "continuation" `?_` is the main goal after refining.
|
||||
-/
|
||||
macro "refine_lift " e:term : tactic => `(focus (refine no_implicit_lambda% $e; rotate_right))
|
||||
macro "refine_lift " e:term : tactic => `(tactic| focus (refine no_implicit_lambda% $e; rotate_right))
|
||||
|
||||
/--
|
||||
`have h : t := e` adds the hypothesis `h : t` to the current goal if `e` a term
|
||||
|
|
@ -476,7 +476,7 @@ of type `t`.
|
|||
For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
|
||||
hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
|
||||
-/
|
||||
macro "have " d:haveDecl : tactic => `(refine_lift have $d:haveDecl; ?_)
|
||||
macro "have " d:haveDecl : tactic => `(tactic| refine_lift have $d:haveDecl; ?_)
|
||||
|
||||
/--
|
||||
Given a main goal `ctx ⊢ t`, `suffices h : t' from e` replaces the main goal with `ctx ⊢ t'`,
|
||||
|
|
@ -485,7 +485,7 @@ Given a main goal `ctx ⊢ t`, `suffices h : t' from e` replaces the main goal w
|
|||
The variant `suffices h : t' by tac` is a shorthand for `suffices h : t' from by tac`.
|
||||
If `h :` is omitted, the name `this` is used.
|
||||
-/
|
||||
macro "suffices " d:sufficesDecl : tactic => `(refine_lift suffices $d; ?_)
|
||||
macro "suffices " d:sufficesDecl : tactic => `(tactic| refine_lift suffices $d; ?_)
|
||||
/--
|
||||
`let h : t := e` adds the hypothesis `h : t := e` to the current goal if `e` a term of type `t`.
|
||||
If `t` is omitted, it will be inferred.
|
||||
|
|
@ -494,12 +494,12 @@ and it is convenient for types that have only applicable constructor.
|
|||
Example: given `h : p ∧ q ∧ r`, `let ⟨h₁, h₂, h₃⟩ := h` produces the hypotheses
|
||||
`h₁ : p`, `h₂ : q`, and `h₃ : r`.
|
||||
-/
|
||||
macro "let " d:letDecl : tactic => `(refine_lift let $d:letDecl; ?_)
|
||||
macro "let " d:letDecl : tactic => `(tactic| refine_lift let $d:letDecl; ?_)
|
||||
/--
|
||||
`show t` finds the first goal whose target unifies with `t`. It makes that the main goal,
|
||||
performs the unification, and replaces the target with the unified version of `t`.
|
||||
-/
|
||||
macro "show " e:term : tactic => `(refine_lift show $e from ?_) -- TODO: fix, see comment
|
||||
macro "show " e:term : tactic => `(tactic| refine_lift show $e from ?_) -- TODO: fix, see comment
|
||||
/-- `let rec f : t := e` adds a recursive definition `f` to the current goal.
|
||||
The syntax is the same as term-mode `let rec`. -/
|
||||
syntax (name := letrec) withPosition(atomic("let " &"rec ") letRecDecls) : tactic
|
||||
|
|
@ -507,13 +507,13 @@ macro_rules
|
|||
| `(tactic| let rec $d) => `(tactic| refine_lift let rec $d; ?_)
|
||||
|
||||
/-- Similar to `refine_lift`, but using `refine'` -/
|
||||
macro "refine_lift' " e:term : tactic => `(focus (refine' no_implicit_lambda% $e; rotate_right))
|
||||
macro "refine_lift' " e:term : tactic => `(tactic| focus (refine' no_implicit_lambda% $e; rotate_right))
|
||||
/-- Similar to `have`, but using `refine'` -/
|
||||
macro "have' " d:haveDecl : tactic => `(refine_lift' have $d:haveDecl; ?_)
|
||||
macro "have' " d:haveDecl : tactic => `(tactic| refine_lift' have $d:haveDecl; ?_)
|
||||
/-- Similar to `have`, but using `refine'` -/
|
||||
macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x : _ := $p)
|
||||
macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x : _ := $p)
|
||||
/-- Similar to `let`, but using `refine'` -/
|
||||
macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_)
|
||||
macro "let' " d:letDecl : tactic => `(tactic| refine_lift' let $d:letDecl; ?_)
|
||||
|
||||
/--
|
||||
The left hand side of an induction arm, `| foo a b c` or `| @foo a b c`
|
||||
|
|
@ -678,7 +678,7 @@ example : ∀ x : Nat, x = x := by unhygienic
|
|||
exact Eq.refl x -- refer to x
|
||||
```
|
||||
-/
|
||||
macro "unhygienic " t:tacticSeq : tactic => `(set_option tactic.hygienic false in $t)
|
||||
macro "unhygienic " t:tacticSeq : tactic => `(tactic| set_option tactic.hygienic false in $t)
|
||||
|
||||
/-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/
|
||||
syntax (name := fail) "fail " (str)? : tactic
|
||||
|
|
@ -812,7 +812,7 @@ to prove any side conditions that arise when constructing the term
|
|||
users are encouraged to extend `get_elem_tactic_trivial` instead of this tactic.
|
||||
-/
|
||||
macro "get_elem_tactic" : tactic =>
|
||||
`(first
|
||||
`(tactic| first
|
||||
| get_elem_tactic_trivial
|
||||
| fail "failed to prove index is valid, possible solutions:
|
||||
- Use `have`-expressions to prove the index is valid
|
||||
|
|
|
|||
|
|
@ -32,7 +32,8 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt; assu
|
|||
lexicographic order lemmas and using `ts` to solve the base case. If it fails,
|
||||
it prints a message to help the user diagnose an ill-founded recursive definition. -/
|
||||
macro "decreasing_with " ts:tacticSeq : tactic =>
|
||||
`((simp_wf
|
||||
`(tactic|
|
||||
(simp_wf
|
||||
repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
|
||||
repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
|
||||
first
|
||||
|
|
@ -49,4 +50,4 @@ on the recursive definition, and it can also be globally extended by adding
|
|||
more definitions for `decreasing_tactic` (or `decreasing_trivial`,
|
||||
which this tactic calls). -/
|
||||
macro "decreasing_tactic" : tactic =>
|
||||
`(decreasing_with first | decreasing_trivial | subst_vars; decreasing_trivial)
|
||||
`(tactic| decreasing_with first | decreasing_trivial | subst_vars; decreasing_trivial)
|
||||
|
|
|
|||
|
|
@ -247,7 +247,7 @@ def elabBinder (binder : Syntax) (x : Expr → TermElabM α) : TermElabM α :=
|
|||
/-- If `binder` is a `_` or an identifier, return a `bracketedBinder` using `type` otherwise throw an exception. -/
|
||||
def expandSimpleBinderWithType (type : Term) (binder : Syntax) : MacroM Syntax :=
|
||||
if binder.isOfKind ``hole || binder.isIdent then
|
||||
`(bracketedBinder| ($binder : $type))
|
||||
`(bracketedBinderF| ($binder : $type))
|
||||
else
|
||||
Macro.throwErrorAt type "unexpected type ascription"
|
||||
|
||||
|
|
|
|||
|
|
@ -138,9 +138,11 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
|
|||
modifyScope fun scope => { scope with openDecls := openDecls }
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
open Lean.Parser.Term
|
||||
|
||||
private def typelessBinder? : Syntax → Option (Array (TSyntax [`ident, `Lean.Parser.Term.hole]) × Bool)
|
||||
| `(bracketedBinder|($ids*)) => some <| (ids, true)
|
||||
| `(bracketedBinder|{$ids*}) => some <| (ids, false)
|
||||
| `(bracketedBinderF|($ids*)) => some (ids, true)
|
||||
| `(bracketedBinderF|{$ids*}) => some (ids, false)
|
||||
| _ => none
|
||||
|
||||
/-- If `id` is an identifier, return true if `ids` contains `id`. -/
|
||||
|
|
@ -167,15 +169,15 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
|
|||
let mut modifiedVarDecls := false
|
||||
for varDecl in varDecls do
|
||||
let (ids, ty?, explicit') ← match varDecl with
|
||||
| `(bracketedBinder|($ids* $[: $ty?]? $(annot?)?)) =>
|
||||
| `(bracketedBinderF|($ids* $[: $ty?]? $(annot?)?)) =>
|
||||
if annot?.isSome then
|
||||
for binderId in binderIds do
|
||||
if containsId ids binderId then
|
||||
throwErrorAt binderId "cannot update binder annotation of variables with default values/tactics"
|
||||
pure (ids, ty?, true)
|
||||
| `(bracketedBinder|{$ids* $[: $ty?]?}) =>
|
||||
| `(bracketedBinderF|{$ids* $[: $ty?]?}) =>
|
||||
pure (ids, ty?, false)
|
||||
| `(bracketedBinder|[$id : $_]) =>
|
||||
| `(bracketedBinderF|[$id : $_]) =>
|
||||
for binderId in binderIds do
|
||||
if binderId.raw.isIdent && binderId.raw.getId == id.getId then
|
||||
throwErrorAt binderId "cannot change the binder annotation of the previously declared local instance `{id.getId}`"
|
||||
|
|
@ -194,9 +196,9 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
|
|||
else
|
||||
let mkBinder (id : TSyntax [`ident, ``Parser.Term.hole]) (explicit : Bool) : CommandElabM (TSyntax ``Parser.Term.bracketedBinder) :=
|
||||
if explicit then
|
||||
`(bracketedBinder| ($id $[: $ty?]?))
|
||||
`(bracketedBinderF| ($id $[: $ty?]?))
|
||||
else
|
||||
`(bracketedBinder| {$id $[: $ty?]?})
|
||||
`(bracketedBinderF| {$id $[: $ty?]?})
|
||||
for id in ids do
|
||||
if let some idx := binderIds.findIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then
|
||||
binderIds := binderIds.eraseIdx idx
|
||||
|
|
@ -209,9 +211,9 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
|
|||
if binderIds.size != binderIdsIniSize then
|
||||
binderIds.mapM fun binderId =>
|
||||
if explicit then
|
||||
`(bracketedBinder| ($binderId))
|
||||
`(bracketedBinderF| ($binderId))
|
||||
else
|
||||
`(bracketedBinder| {$binderId})
|
||||
`(bracketedBinderF| {$binderId})
|
||||
else
|
||||
return #[binder]
|
||||
|
||||
|
|
|
|||
|
|
@ -339,12 +339,13 @@ private def mkMetaContext : Meta.Context := {
|
|||
config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true }
|
||||
}
|
||||
|
||||
open Lean.Parser.Term in
|
||||
/-- Return identifier names in the given bracketed binder. -/
|
||||
def getBracketedBinderIds : Syntax → Array Name
|
||||
| `(bracketedBinder|($ids* $[: $ty?]? $(_annot?)?)) => ids.map Syntax.getId
|
||||
| `(bracketedBinder|{$ids* $[: $ty?]?}) => ids.map Syntax.getId
|
||||
| `(bracketedBinder|[$id : $_]) => #[id.getId]
|
||||
| `(bracketedBinder|[$_]) => #[Name.anonymous]
|
||||
| `(bracketedBinderF|($ids* $[: $ty?]? $(_annot?)?)) => ids.map Syntax.getId
|
||||
| `(bracketedBinderF|{$ids* $[: $ty?]?}) => ids.map Syntax.getId
|
||||
| `(bracketedBinderF|[$id : $_]) => #[id.getId]
|
||||
| `(bracketedBinderF|[$_]) => #[Name.anonymous]
|
||||
| _ => #[]
|
||||
|
||||
private def mkTermContext (ctx : Context) (s : State) : Term.Context := Id.run do
|
||||
|
|
|
|||
|
|
@ -6,8 +6,7 @@ Authors: Leonardo de Moura
|
|||
import Lean.Elab.Deriving.Basic
|
||||
|
||||
namespace Lean.Elab
|
||||
open Command
|
||||
open Meta
|
||||
open Command Meta Parser Term
|
||||
|
||||
private abbrev IndexSet := RBTree Nat compare
|
||||
private abbrev LocalInst2Index := FVarIdMap Nat
|
||||
|
|
@ -66,10 +65,10 @@ where
|
|||
for i in [:indVal.numParams + indVal.numIndices] do
|
||||
let arg := mkIdent (← mkFreshUserName `a)
|
||||
indArgs := indArgs.push arg
|
||||
let binder ← `(bracketedBinder| { $arg:ident })
|
||||
let binder ← `(bracketedBinderF| { $arg:ident })
|
||||
binders := binders.push binder
|
||||
if assumingParamIdxs.contains i then
|
||||
let binder ← `(bracketedBinder| [Inhabited $arg:ident ])
|
||||
let binder ← `(bracketedBinderF| [Inhabited $arg:ident ])
|
||||
binders := binders.push binder
|
||||
let type ← `(Inhabited (@$(mkIdent inductiveTypeName):ident $indArgs:ident*))
|
||||
let mut ctorArgs := #[]
|
||||
|
|
|
|||
|
|
@ -16,7 +16,7 @@ open Std
|
|||
def mkReprHeader (indVal : InductiveVal) : TermElabM Header := do
|
||||
let header ← mkHeader `Repr 1 indVal
|
||||
return { header with
|
||||
binders := header.binders.push (← `(bracketedBinder| (prec : Nat)))
|
||||
binders := header.binders.push (← `(bracketedBinderF| (prec : Nat)))
|
||||
}
|
||||
|
||||
def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term := do
|
||||
|
|
|
|||
|
|
@ -45,22 +45,23 @@ where
|
|||
return ⟨mkNullNode #[mkAntiquotSuffixSpliceNode kind (← mkAntiquotNode stx id) suffix]⟩
|
||||
mkAntiquotNode : TSyntax `stx → Term → CommandElabM Term
|
||||
| `(stx| $id:ident$[:$_]?), term => do
|
||||
let kind ← match (← Elab.Term.resolveParserName id) with
|
||||
| [(`Lean.Parser.ident, _)] => pure identKind
|
||||
| [(`Lean.Parser.Term.ident, _)] => pure identKind
|
||||
| [(`Lean.Parser.strLit, _)] => pure strLitKind
|
||||
-- a syntax abbrev, assume kind == decl name
|
||||
| [(c, _)] => pure c
|
||||
| cs@(_ :: _ :: _) => throwError "ambiguous parser declaration {cs.map (·.1)}"
|
||||
| [] =>
|
||||
match (← liftTermElabM do Elab.Term.elabParserName? id) with
|
||||
| some (.parser n _) =>
|
||||
let kind := match n with
|
||||
| ``Parser.ident => identKind
|
||||
| ``Parser.Term.ident => identKind
|
||||
| ``Parser.strLit => strLitKind
|
||||
| _ => n -- assume kind == decl name
|
||||
return ⟨Syntax.mkAntiquotNode kind term⟩
|
||||
| some (.category cat) =>
|
||||
return ⟨Syntax.mkAntiquotNode cat term (isPseudoKind := true)⟩
|
||||
| none =>
|
||||
let id := id.getId.eraseMacroScopes
|
||||
if Parser.isParserCategory (← getEnv) id then
|
||||
return ⟨Syntax.mkAntiquotNode id term (isPseudoKind := true)⟩
|
||||
else if (← Parser.isParserAlias id) then
|
||||
pure <| (← Parser.getSyntaxKindOfParserAlias? id).getD Name.anonymous
|
||||
if (← Parser.isParserAlias id) then
|
||||
let kind := (← Parser.getSyntaxKindOfParserAlias? id).getD Name.anonymous
|
||||
return ⟨Syntax.mkAntiquotNode kind term⟩
|
||||
else
|
||||
throwError "unknown parser declaration/category/alias '{id}'"
|
||||
pure ⟨Syntax.mkAntiquotNode kind term⟩
|
||||
| stx, term => do
|
||||
-- can't match against `` `(stx| ($stxs*)) `` as `*` is interpreted as the `stx` operator
|
||||
if stx.raw.isOfKind ``Parser.Syntax.paren then
|
||||
|
|
|
|||
|
|
@ -10,6 +10,7 @@ import Lean.ResolveName
|
|||
import Lean.Elab.Term
|
||||
import Lean.Elab.Quotation.Util
|
||||
import Lean.Elab.Quotation.Precheck
|
||||
import Lean.Elab.Syntax
|
||||
import Lean.Parser.Syntax
|
||||
|
||||
namespace Lean.Elab.Term.Quotation
|
||||
|
|
@ -218,30 +219,20 @@ def getQuotKind (stx : Syntax) : TermElabM SyntaxNodeKind := do
|
|||
match stx.getKind with
|
||||
| ``Parser.Command.quot => addNamedQuotInfo stx `command
|
||||
| ``Parser.Term.quot => addNamedQuotInfo stx `term
|
||||
| ``Parser.Level.quot => addNamedQuotInfo stx `level
|
||||
| ``Parser.Tactic.quot => addNamedQuotInfo stx `tactic
|
||||
| ``Parser.Tactic.quotSeq => addNamedQuotInfo stx `tactic.seq
|
||||
| ``Parser.Term.stx.quot => addNamedQuotInfo stx `stx
|
||||
| ``Parser.Term.prec.quot => addNamedQuotInfo stx `prec
|
||||
| ``Parser.Term.attr.quot => addNamedQuotInfo stx `attr
|
||||
| ``Parser.Term.prio.quot => addNamedQuotInfo stx `prio
|
||||
| ``Parser.Term.doElem.quot => addNamedQuotInfo stx `doElem
|
||||
| .str kind "quot" => addNamedQuotInfo stx kind
|
||||
| ``dynamicQuot =>
|
||||
match (← resolveGlobalConstWithInfos stx[1]) with
|
||||
| [parser] => pure parser
|
||||
| _ => throwError "unknown parser {stx[1]}"
|
||||
| ``dynamicQuot => match ← elabParserName stx[1] with
|
||||
| .parser n _ => return n
|
||||
| .category c => return c
|
||||
| k => throwError "unexpected quotation kind {k}"
|
||||
|
||||
def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do
|
||||
let stx := if stx.getNumArgs == 1 then stx[0] else stx
|
||||
def mkSyntaxQuotation (stx : Syntax) (kind : Name) : TermElabM Syntax := do
|
||||
/- Syntax quotations are monadic values depending on the current macro scope. For efficiency, we bind
|
||||
the macro scope once for each quotation, then build the syntax tree in a completely pure computation
|
||||
depending on this binding. Note that regular function calls do not introduce a new macro scope (i.e.
|
||||
we preserve referential transparency), so we can refer to this same `scp` inside `quoteSyntax` by
|
||||
including it literally in a syntax quotation. -/
|
||||
let kind ← getQuotKind stx
|
||||
let stx ← quoteSyntax stx.getQuotContent
|
||||
`(Bind.bind MonadRef.mkInfoFromRefPos (fun info =>
|
||||
Bind.bind getCurrMacroScope (fun scp =>
|
||||
Bind.bind getMainModule (fun mainModule => Pure.pure (@TSyntax.mk $(quote kind) $stx)))))
|
||||
|
|
@ -261,23 +252,18 @@ def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do
|
|||
implementation is "self-stabilizing". It was in fact originally compiled
|
||||
by an unhygienic prototype implementation. -/
|
||||
|
||||
def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do
|
||||
let stx := if stx.getNumArgs == 1 then stx[0] else stx
|
||||
let kind ← getQuotKind stx
|
||||
let stx ← quoteSyntax stx.getQuotContent
|
||||
mkSyntaxQuotation stx kind
|
||||
|
||||
macro "elab_stx_quot" kind:ident : command =>
|
||||
`(@[builtinTermElab $kind:ident] def elabQuot : TermElab := adaptExpander stxQuot.expand)
|
||||
|
||||
--
|
||||
|
||||
elab_stx_quot Parser.Level.quot
|
||||
elab_stx_quot Parser.Term.quot
|
||||
elab_stx_quot Parser.Term.funBinder.quot
|
||||
elab_stx_quot Parser.Term.bracketedBinder.quot
|
||||
elab_stx_quot Parser.Term.matchDiscr.quot
|
||||
elab_stx_quot Parser.Tactic.quot
|
||||
elab_stx_quot Parser.Tactic.quotSeq
|
||||
elab_stx_quot Parser.Term.stx.quot
|
||||
elab_stx_quot Parser.Term.prec.quot
|
||||
elab_stx_quot Parser.Term.attr.quot
|
||||
elab_stx_quot Parser.Term.prio.quot
|
||||
elab_stx_quot Parser.Term.doElem.quot
|
||||
elab_stx_quot Parser.Term.dynamicQuot
|
||||
elab_stx_quot Parser.Command.quot
|
||||
|
||||
|
|
|
|||
|
|
@ -79,26 +79,21 @@ def checkLeftRec (stx : Syntax) : ToParserDescrM Bool := do
|
|||
markAsTrailingParser (prec?.getD 0)
|
||||
return true
|
||||
|
||||
/-- Resolve the given parser name and return a list of candidates.
|
||||
Each candidate is a pair `(resolvedParserName, isDescr)`.
|
||||
`isDescr == true` if the type of `resolvedParserName` is a `ParserDescr`. -/
|
||||
def resolveParserName [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] (parserName : Syntax) : m (List (Name × Bool)) := do
|
||||
try
|
||||
let candidates ← resolveGlobalConstWithInfos parserName
|
||||
/- Convert `candidates` in a list of pairs `(c, isDescr)`, where `c` is the parser name,
|
||||
and `isDescr` is true iff `c` has type `Lean.ParserDescr` or `Lean.TrailingParser` -/
|
||||
let env ← getEnv
|
||||
return candidates.filterMap fun c =>
|
||||
match env.find? c with
|
||||
| none => none
|
||||
| some info =>
|
||||
match info.type with
|
||||
| Expr.const ``Lean.Parser.TrailingParser _ => (c, false)
|
||||
| Expr.const ``Lean.Parser.Parser _ => (c, false)
|
||||
| Expr.const ``Lean.ParserDescr _ => (c, true)
|
||||
| Expr.const ``Lean.TrailingParserDescr _ => (c, true)
|
||||
| _ => none
|
||||
catch _ => return []
|
||||
def elabParserName? (stx : Syntax.Ident) : TermElabM (Option Parser.ParserName) := do
|
||||
match ← Parser.resolveParserName stx with
|
||||
| [n@(.category cat)] =>
|
||||
addCategoryInfo stx cat
|
||||
return n
|
||||
| [n@(.parser parser _)] =>
|
||||
addTermInfo' stx (Lean.mkConst parser)
|
||||
return n
|
||||
| _::_::_ => throwErrorAt stx "ambiguous parser {stx}"
|
||||
| [] => return none
|
||||
|
||||
def elabParserName (stx : Syntax.Ident) : TermElabM Parser.ParserName := do
|
||||
match ← elabParserName? stx with
|
||||
| some n => return n
|
||||
| none => throwErrorAt stx "unknown parser {stx}"
|
||||
|
||||
open TSyntax.Compat in
|
||||
/--
|
||||
|
|
@ -161,7 +156,6 @@ where
|
|||
throwErrorAt stx "invalid atomic left recursive syntax"
|
||||
let prec? ← liftMacroM <| expandOptPrecedence stx[1]
|
||||
let prec := prec?.getD 0
|
||||
addCategoryInfo stx catName
|
||||
return (← `(ParserDescr.cat $(quote catName) $(quote prec)), 1)
|
||||
|
||||
processAlias (id : Syntax) (args : Array Syntax) := do
|
||||
|
|
@ -185,23 +179,22 @@ where
|
|||
return (stx, stackSz)
|
||||
|
||||
processNullaryOrCat (stx : Syntax) := do
|
||||
match (← resolveParserName stx[0]) with
|
||||
| [(c, true)] =>
|
||||
match (← elabParserName? stx[0]) with
|
||||
| some (.parser c (isDescr := true)) =>
|
||||
ensureNoPrec stx
|
||||
-- `syntax _ :=` at least enforces this
|
||||
let stackSz := 1
|
||||
return (mkIdentFrom stx c, stackSz)
|
||||
| [(c, false)] =>
|
||||
| some (.parser c (isDescr := false)) =>
|
||||
ensureNoPrec stx
|
||||
-- as usual, we assume that people using `Parser` know what they are doing
|
||||
let stackSz := 1
|
||||
return (← `(ParserDescr.parser $(quote c)), stackSz)
|
||||
| cs@(_ :: _ :: _) => throwError "ambiguous parser declaration {cs.map (·.1)}"
|
||||
| [] =>
|
||||
| some (.category _) =>
|
||||
processParserCategory stx
|
||||
| none =>
|
||||
let id := stx[0].getId.eraseMacroScopes
|
||||
if Parser.isParserCategory (← getEnv) id then
|
||||
processParserCategory stx
|
||||
else if (← Parser.isParserAlias id) then
|
||||
if (← Parser.isParserAlias id) then
|
||||
ensureNoPrec stx
|
||||
processAlias stx[0] #[]
|
||||
else
|
||||
|
|
|
|||
|
|
@ -140,8 +140,6 @@ The second `notFollowedBy` prevents this problem.
|
|||
|
||||
@[builtinTermParser] def «do» := leading_parser:argPrec ppAllowUngrouped >> "do " >> doSeq
|
||||
|
||||
@[builtinTermParser] def doElem.quot : Parser := leading_parser "`(doElem|" >> incQuotDepth doElemParser >> ")"
|
||||
|
||||
/- macros for using `unless`, `for`, `try`, `return` as terms. They expand into `do unless ...`, `do for ...`, `do try ...`, and `do return ...` -/
|
||||
/-- `unless e do s` is a nicer way to write `if !e do s`. -/
|
||||
@[builtinTermParser] def termUnless := leading_parser "unless " >> withForbidden "do" termParser >> "do " >> doSeq
|
||||
|
|
|
|||
|
|
@ -633,17 +633,56 @@ def withOpenDeclFn (p : ParserFn) : ParserFn := fun c s =>
|
|||
fn := withOpenDeclFn p.fn
|
||||
}
|
||||
|
||||
def ParserContext.resolveName (ctx : ParserContext) (id : Name) : List (Name × List String) :=
|
||||
ResolveName.resolveGlobalName ctx.env ctx.currNamespace ctx.openDecls id
|
||||
inductive ParserName
|
||||
| category (cat : Name)
|
||||
| parser (decl : Name) (isDescr : Bool)
|
||||
-- TODO(gabriel): add parser aliases (this is blocked on doing IO in parsers)
|
||||
deriving Repr
|
||||
|
||||
/-- Resolve the given parser name and return a list of candidates. -/
|
||||
def resolveParserNameCore (env : Environment) (currNamespace : Name)
|
||||
(openDecls : List OpenDecl) (ident : Ident) : List ParserName := Id.run do
|
||||
let ⟨.ident (val := val) (preresolved := pre) ..⟩ := ident | return []
|
||||
|
||||
let rec isParser (name : Name) : Option Bool :=
|
||||
(env.find? name).bind fun ci =>
|
||||
match ci.type with
|
||||
| .const ``Parser _ | .const ``TrailingParser _ => some false
|
||||
| .const ``ParserDescr _ | .const ``TrailingParserDescr _ => some true
|
||||
| _ => none
|
||||
|
||||
for pre in pre do
|
||||
if let .decl n [] := pre then
|
||||
if let some isDescr := isParser n then
|
||||
return [.parser n isDescr]
|
||||
|
||||
let erased := val.eraseMacroScopes
|
||||
|
||||
if isParserCategory env erased then
|
||||
return [.category erased]
|
||||
|
||||
ResolveName.resolveGlobalName env currNamespace openDecls val |>.filterMap fun
|
||||
| (name, []) => (isParser name).map fun isDescr => .parser name isDescr
|
||||
| _ => none
|
||||
|
||||
/-- Resolve the given parser name and return a list of candidates. -/
|
||||
def ParserContext.resolveParserName (ctx : ParserContext) (id : Ident) : List ParserName :=
|
||||
Parser.resolveParserNameCore ctx.env ctx.currNamespace ctx.openDecls id
|
||||
|
||||
/-- Resolve the given parser name and return a list of candidates. -/
|
||||
def resolveParserName (id : Ident) : CoreM (List ParserName) :=
|
||||
return resolveParserNameCore (← getEnv) (← getCurrNamespace) (← getOpenDecls) id
|
||||
|
||||
def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s => Id.run do
|
||||
let stack := s.stxStack
|
||||
if stack.size < offset + 1 then
|
||||
return s.mkUnexpectedError ("failed to determine parser using syntax stack, stack is too small")
|
||||
let Syntax.ident (val := parserName) .. := stack.get! (stack.size - offset - 1)
|
||||
let parserName@(.ident ..) := stack.get! (stack.size - offset - 1)
|
||||
| s.mkUnexpectedError ("failed to determine parser using syntax stack, the specified element on the stack is not an identifier")
|
||||
match ctx.resolveName parserName with
|
||||
| [(parserName, [])] =>
|
||||
match ctx.resolveParserName ⟨parserName⟩ with
|
||||
| [.category cat] =>
|
||||
categoryParserFn cat ctx s
|
||||
| [.parser parserName _] =>
|
||||
let iniSz := s.stackSize
|
||||
let mut ctx' := ctx
|
||||
if !internal.parseQuotWithCurrentStage.get ctx'.options then
|
||||
|
|
@ -656,7 +695,7 @@ def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s => Id.run do
|
|||
else
|
||||
s
|
||||
| _::_::_ => s.mkUnexpectedError s!"ambiguous parser name {parserName}"
|
||||
| _ => s.mkUnexpectedError s!"unknown parser {parserName}"
|
||||
| [] => s.mkUnexpectedError s!"unknown parser {parserName}"
|
||||
|
||||
def parserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
|
||||
{ fn := fun c s => parserOfStackFn offset { c with prec := prec } s }
|
||||
|
|
|
|||
|
|
@ -39,14 +39,6 @@ namespace Syntax
|
|||
|
||||
end Syntax
|
||||
|
||||
namespace Term
|
||||
|
||||
@[builtinTermParser] def stx.quot : Parser := leading_parser "`(stx|" >> incQuotDepth syntaxParser >> ")"
|
||||
@[builtinTermParser] def prec.quot : Parser := leading_parser "`(prec|" >> incQuotDepth precedenceParser >> ")"
|
||||
@[builtinTermParser] def prio.quot : Parser := leading_parser "`(prio|" >> incQuotDepth priorityParser >> ")"
|
||||
|
||||
end Term
|
||||
|
||||
namespace Command
|
||||
|
||||
def namedName := leading_parser (atomic ("(" >> nonReservedSymbol "name") >> " := " >> ident >> ")")
|
||||
|
|
@ -75,11 +67,8 @@ def catBehaviorSymbol := leading_parser nonReservedSymbol "symbol"
|
|||
def catBehavior := optional ("(" >> nonReservedSymbol "behavior" >> " := " >> (catBehaviorBoth <|> catBehaviorSymbol) >> ")")
|
||||
@[builtinCommandParser] def syntaxCat := leading_parser optional docComment >> "declare_syntax_cat " >> ident >> catBehavior
|
||||
def macroArg := leading_parser optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> syntaxParser argPrec
|
||||
def macroRhs (quotP : Parser) : Parser := leading_parser "`(" >> incQuotDepth quotP >> ")" <|> withPosition termParser
|
||||
def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >> macroRhs Tactic.seq1
|
||||
def macroTailCommand : Parser := atomic (" : " >> identEq "command") >> darrow >> macroRhs (many1Unbox commandParser)
|
||||
def macroTailDefault : Parser := atomic (" : " >> ident) >> darrow >> macroRhs (categoryParserOfStack 2)
|
||||
def macroTail := leading_parser macroTailTactic <|> macroTailCommand <|> macroTailDefault
|
||||
def macroRhs : Parser := leading_parser withPosition termParser
|
||||
def macroTail := leading_parser atomic (" : " >> ident) >> darrow >> macroRhs
|
||||
@[builtinCommandParser] def «macro» := leading_parser suppressInsideQuot (optional docComment >> optional Term.«attributes» >> Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 macroArg >> macroTail)
|
||||
|
||||
@[builtinCommandParser] def «elab_rules» := leading_parser suppressInsideQuot (optional docComment >> optional Term.«attributes» >> Term.attrKind >> "elab_rules" >> optKind >> optional (" : " >> ident) >> optional (" <= " >> ident) >> Term.matchAlts)
|
||||
|
|
|
|||
|
|
@ -448,12 +448,8 @@ See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lea
|
|||
-/
|
||||
@[builtinTermParser] def subst := trailing_parser:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
|
||||
|
||||
-- NOTE: Doesn't call `categoryParser` directly in contrast to most other "static" quotations, so call `evalInsideQuot` explicitly
|
||||
@[builtinTermParser] def funBinder.quot : Parser := leading_parser "`(funBinder|" >> incQuotDepth (evalInsideQuot ``funBinder funBinder) >> ")"
|
||||
def bracketedBinderF := bracketedBinder -- no default arg
|
||||
@[builtinTermParser] def bracketedBinder.quot : Parser := leading_parser "`(bracketedBinder|" >> incQuotDepth (evalInsideQuot ``bracketedBinderF bracketedBinder) >> ")"
|
||||
@[builtinTermParser] def matchDiscr.quot : Parser := leading_parser "`(matchDiscr|" >> incQuotDepth (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
|
||||
@[builtinTermParser] def attr.quot : Parser := leading_parser "`(attr|" >> incQuotDepth attrParser >> ")"
|
||||
instance : Coe (TSyntax ``bracketedBinderF) (TSyntax ``bracketedBinder) where coe s := ⟨s⟩
|
||||
|
||||
/--
|
||||
`panic! msg` formally evaluates to `@Inhabited.default α` if the expected type
|
||||
|
|
@ -491,8 +487,6 @@ end Term
|
|||
@[builtinTermParser default+1] def Tactic.quot : Parser := leading_parser "`(tactic|" >> incQuotDepth tacticParser >> ")"
|
||||
@[builtinTermParser] def Tactic.quotSeq : Parser := leading_parser "`(tactic|" >> incQuotDepth Tactic.seq1 >> ")"
|
||||
|
||||
@[builtinTermParser] def Level.quot : Parser := leading_parser "`(level|" >> incQuotDepth levelParser >> ")"
|
||||
|
||||
open Term in
|
||||
builtin_initialize
|
||||
register_parser_alias letDecl
|
||||
|
|
|
|||
|
|
@ -72,7 +72,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
|
|||
-- create the constructor
|
||||
let fieldStxs ← argVars.mapM fun arg => do
|
||||
let name := (← getFVarLocalDecl arg).userName
|
||||
`(bracketedBinder| ($(mkIdent name) : Json))
|
||||
`(bracketedBinderF| ($(mkIdent name) : Json))
|
||||
let pktCtor ← `(Parser.Command.ctor|
|
||||
| $ctorId:ident $[$fieldStxs]* : RpcEncodablePacket)
|
||||
|
||||
|
|
@ -124,7 +124,7 @@ private def deriveInstance (declNames : Array Name) : CommandElabM Bool := do
|
|||
elabCommand <| ← liftTermElabM do
|
||||
forallTelescopeReducing indVal.type fun params _ => do
|
||||
let encInstBinders ← (← params.filterM (isType ·)).mapM fun p => do
|
||||
`(bracketedBinder| [RpcEncodable $(mkIdent (← getFVarLocalDecl p).userName):ident])
|
||||
`(bracketedBinderF| [RpcEncodable $(mkIdent (← getFVarLocalDecl p).userName):ident])
|
||||
if isStructure (← getEnv) typeName then
|
||||
deriveStructureInstance indVal params encInstBinders
|
||||
else
|
||||
|
|
|
|||
2
src/lake
2
src/lake
|
|
@ -1 +1 @@
|
|||
Subproject commit 8d98d5616bacc49700f63c78c30cefd00e040686
|
||||
Subproject commit b843041aa4589ee093a67794967421e347f33482
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
import Lean
|
||||
open Lean Elab Tactic
|
||||
|
||||
macro "obviously1" : tactic => `(exact sorryAx _)
|
||||
macro "obviously1" : tactic => `(tactic| exact sorryAx _)
|
||||
|
||||
theorem result1 : False := by obviously1
|
||||
|
||||
|
|
|
|||
|
|
@ -114,3 +114,7 @@ syntax "foo" term : term
|
|||
| `(a) => pure "0"
|
||||
| `(b) => pure "1"
|
||||
| _ => pure "2"
|
||||
|
||||
declare_syntax_cat mycat
|
||||
syntax "mystx" : mycat
|
||||
#eval run `(mycat| mystx)
|
||||
|
|
|
|||
|
|
@ -55,3 +55,4 @@ StxQuot.lean:108:22-108:23: error: unknown identifier 'y' at quotation precheck;
|
|||
"(Term.fun\n \"fun\"\n (Term.basicFun\n [`x._@.UnhygienicMain._hyg.1 `y._@.UnhygienicMain._hyg.1]\n []\n \"=>\"\n (Term.app `x._@.UnhygienicMain._hyg.1 [`y._@.UnhygienicMain._hyg.1])))"
|
||||
"(Term.fun\n \"fun\"\n (Term.basicFun\n [(Term.anonymousCtor \"⟨\" [`x._@.UnhygienicMain._hyg.1 \",\" `y._@.UnhygienicMain._hyg.1] \"⟩\")]\n []\n \"=>\"\n `x._@.UnhygienicMain._hyg.1))"
|
||||
"1"
|
||||
"(mycatMystx \"mystx\")"
|
||||
|
|
|
|||
|
|
@ -16,7 +16,7 @@ example (n : Nat) : True := by
|
|||
|
||||
|
||||
/-- My tactic -/
|
||||
macro "mytac" o:"only"? e:term : tactic => `(exact $e)
|
||||
macro "mytac" o:"only"? e:term : tactic => `(tactic| exact $e)
|
||||
|
||||
example : True := by
|
||||
mytac only True.intro
|
||||
|
|
|
|||
|
|
@ -39,7 +39,7 @@ theorem Weekday.nextOfPrevious'' (d : Weekday) : previous (next d) = d ∧ next
|
|||
apply And.intro <;> cases d <;> rfl
|
||||
|
||||
open Lean.Parser.Tactic in
|
||||
macro "rwd " x:term : tactic => `(rw [$x:term]; done)
|
||||
macro "rwd " x:term : tactic => `(tactic| rw [$x:term]; done)
|
||||
|
||||
theorem ex (a b c : α) (h₁ : a = b) (h₂ : a = c) : b = a ∧ c = a := by
|
||||
apply And.intro <;> first | rwd h₁ | rwd h₂
|
||||
|
|
|
|||
|
|
@ -57,7 +57,7 @@ return ()
|
|||
|
||||
#eval gTest
|
||||
|
||||
macro "ret!" x:term : doElem => `(return $x)
|
||||
macro "ret!" x:term : doElem => `(doElem| return $x)
|
||||
|
||||
def f1 (x : Nat) : Nat := Id.run <| do
|
||||
let mut x := x
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ def f : Nat → Bool → Nat
|
|||
| x+2, true => f x true
|
||||
| x+2, b => f x (not b)
|
||||
|
||||
macro "urfl" : tactic => `(set_option smartUnfolding false in rfl)
|
||||
macro "urfl" : tactic => `(tactic| set_option smartUnfolding false in rfl)
|
||||
|
||||
|
||||
theorem f_main_eq : f x b = f.match_1 (fun _ _ => Nat) x b (fun _ => 1) (fun _ => 2) (fun _ => 3) (fun _ => 4) (fun x => f x true) (fun x b => f x (not b)) := by
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ example (P : Prop) : ∀ {p : P}, P := by
|
|||
example (P : Prop) : ∀ {p : P}, P := by
|
||||
exact no_implicit_lambda% id
|
||||
|
||||
macro "exact'" x:term : tactic => `(exact no_implicit_lambda% $x)
|
||||
macro "exact'" x:term : tactic => `(tactic| exact no_implicit_lambda% $x)
|
||||
|
||||
example (P : Prop) : ∀ {p : P}, P := by
|
||||
exact' id
|
||||
|
|
|
|||
|
|
@ -2,6 +2,6 @@ macro x:ident noWs "(" ys:term,* ")" : term => `($x $ys*)
|
|||
|
||||
#check id(1)
|
||||
|
||||
macro "foo" &"only" : tactic => `(trivial)
|
||||
macro "foo" &"only" : tactic => `(tactic| trivial)
|
||||
|
||||
example : True := by foo only
|
||||
|
|
|
|||
|
|
@ -278,9 +278,10 @@ elab t1:tactic " ⟨|⟩ " t2:tactic : tactic =>
|
|||
|
||||
elab "fail" m:term : tactic => throwError m
|
||||
|
||||
macro "out" : tactic => `(apply escape_north ⟨|⟩ apply escape_south ⟨|⟩
|
||||
apply escape_east ⟨|⟩ apply escape_west ⟨|⟩
|
||||
fail "not currently at maze boundary")
|
||||
macro "out" : tactic => `(tactic|
|
||||
apply escape_north ⟨|⟩ apply escape_south ⟨|⟩
|
||||
apply escape_east ⟨|⟩ apply escape_west ⟨|⟩
|
||||
fail "not currently at maze boundary")
|
||||
|
||||
def maze1 := ┌───┐
|
||||
│▓▓▓│
|
||||
|
|
|
|||
|
|
@ -63,7 +63,7 @@ by {
|
|||
assumption
|
||||
}
|
||||
|
||||
macro "intro3" : tactic => `(intro; intro; intro)
|
||||
macro "intro3" : tactic => `(tactic| intro; intro; intro)
|
||||
macro "check2" x:term : command => `(#check $x #check $x)
|
||||
macro "foo" x:term "," y:term : term => `($x + $y + $x)
|
||||
|
||||
|
|
@ -228,7 +228,7 @@ by {
|
|||
exact h1
|
||||
}
|
||||
|
||||
macro "blabla" : tactic => `(assumption)
|
||||
macro "blabla" : tactic => `(tactic| assumption)
|
||||
|
||||
-- Tactic head symbols do not become reserved words
|
||||
def blabla := 100
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
open Lean.Parser.Tactic in
|
||||
macro "rw0" s:rwRuleSeq : tactic =>
|
||||
`(rw (config := { offsetCnstrs := false }) $s:rwRuleSeq)
|
||||
`(tactic| rw (config := { offsetCnstrs := false }) $s:rwRuleSeq)
|
||||
|
||||
example (m n : Nat) : Nat.ble (n+1) (n+0) = false := by
|
||||
rw0 [Nat.add_zero]
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
import Lean
|
||||
|
||||
macro "t" t:interpolatedStr(term) : doElem =>
|
||||
`(Macro.trace[Meta.debug] $t)
|
||||
`(doElem| Macro.trace[Meta.debug] $t)
|
||||
|
||||
macro "tstcmd" : command => do
|
||||
t "hello"
|
||||
|
|
@ -13,7 +13,7 @@ tstcmd
|
|||
open Lean Meta
|
||||
|
||||
macro "r" r:interpolatedStr(term) : doElem =>
|
||||
`(trace[Meta.debug] $r)
|
||||
`(doElem| trace[Meta.debug] $r)
|
||||
|
||||
set_option trace.Meta.debug true in
|
||||
#eval show MetaM _ from do r "world"
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ example : f x = id (x + 2) := by
|
|||
simp
|
||||
simp [my_simp]
|
||||
|
||||
macro "my_simp" : tactic => `(simp [my_simp])
|
||||
macro "my_simp" : tactic => `(tactic| simp [my_simp])
|
||||
|
||||
example : f x = id (x + 2) := by
|
||||
my_simp
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue