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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-15 19:02:37 -07:00
parent b77ff79133
commit ef636f6ec5
251 changed files with 72336 additions and 62604 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

108
stage0/src/Init/Core.lean generated
View file

@ -96,10 +96,10 @@ An element of `α ⊕ β` is either of the form `.inl a` where `a : α`,
or `.inr b` where `b : β`.
-/
inductive Sum (α : Type u) (β : Type v) where
| /-- Left injection into the sum type `α ⊕ β`. If `a : α` then `.inl a : α ⊕ β`. -/
inl (val : α) : Sum α β
| /-- Right injection into the sum type `α ⊕ β`. If `b : β` then `.inr b : α ⊕ β`. -/
inr (val : β) : Sum α β
/-- Left injection into the sum type `α ⊕ β`. If `a : α` then `.inl a : α ⊕ β`. -/
| inl (val : α) : Sum α β
/-- Right injection into the sum type `α ⊕ β`. If `b : β` then `.inr b : α ⊕ β`. -/
| inr (val : β) : Sum α β
@[inheritDoc] infixr:30 " ⊕ " => Sum
@ -115,10 +115,10 @@ because the equation `max 1 u v = ?u + 1` has no solution in level arithmetic.
`PSum` is usually only used in automation that constructs sums of arbitrary types.
-/
inductive PSum (α : Sort u) (β : Sort v) where
| /-- Left injection into the sum type `α ⊕' β`. If `a : α` then `.inl a : α ⊕' β`. -/
inl (val : α) : PSum α β
| /-- Right injection into the sum type `α ⊕' β`. If `b : β` then `.inr b : α ⊕' β`. -/
inr (val : β) : PSum α β
/-- Left injection into the sum type `α ⊕' β`. If `a : α` then `.inl a : α ⊕' β`. -/
| inl (val : α) : PSum α β
/-- Right injection into the sum type `α ⊕' β`. If `b : β` then `.inr b : α ⊕' β`. -/
| inr (val : β) : PSum α β
@[inheritDoc] infixr:30 " ⊕' " => PSum
@ -190,9 +190,9 @@ example (h : ∃ x : Nat, x = x) : True :=
```
-/
inductive Exists {α : Sort u} (p : α → Prop) : Prop where
| /-- Existential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`. -/
intro (w : α) (h : p w) : Exists p
/-- Existential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`. -/
| intro (w : α) (h : p w) : Exists p
/--
Auxiliary type used to compile `for x in xs` notation.
@ -206,12 +206,12 @@ representing the body of a for loop. It can be:
`.done` is produced by calls to `break` or `return` in the loop,
-/
inductive ForInStep (α : Type u) where
| /-- `.done a` means that we should early-exit the loop.
`.done` is produced by calls to `break` or `return` in the loop. -/
done : α → ForInStep α
| /-- `.yield a` means that we should continue the loop.
`.yield` is produced by `continue` and reaching the bottom of the loop body. -/
yield : α → ForInStep α
/-- `.done a` means that we should early-exit the loop.
`.done` is produced by calls to `break` or `return` in the loop. -/
| done : α → ForInStep α
/-- `.yield a` means that we should continue the loop.
`.yield` is produced by `continue` and reaching the bottom of the loop body. -/
| yield : α → ForInStep α
deriving Inhabited
/--
@ -276,16 +276,16 @@ block can exit:
All cases return a value `s : σ` which bundles all the mutable variables of the do-block.
-/
inductive DoResultPRBC (α β σ : Type u) where
| /-- `pure (a : α) s` means that the block exited normally with return value `a` -/
pure : α → σ → DoResultPRBC α β σ
| /-- `return (b : β) s` means that the block exited via a `return b` early-exit command -/
return : β → σ → DoResultPRBC α β σ
| /-- `break s` means that `break` was called, meaning that we should exit
from the containing loop -/
break : σ → DoResultPRBC α β σ
| /-- `continue s` means that `continue` was called, meaning that we should continue
to the next iteration of the containing loop -/
continue : σ → DoResultPRBC α β σ
/-- `pure (a : α) s` means that the block exited normally with return value `a` -/
| pure : α → σ → DoResultPRBC α β σ
/-- `return (b : β) s` means that the block exited via a `return b` early-exit command -/
| return : β → σ → DoResultPRBC α β σ
/-- `break s` means that `break` was called, meaning that we should exit
from the containing loop -/
| break : σ → DoResultPRBC α β σ
/-- `continue s` means that `continue` was called, meaning that we should continue
to the next iteration of the containing loop -/
| continue : σ → DoResultPRBC α β σ
/--
Auxiliary type used to compile `do` notation. It is the same as
@ -293,10 +293,10 @@ Auxiliary type used to compile `do` notation. It is the same as
because we are not in a loop context.
-/
inductive DoResultPR (α β σ : Type u) where
| /-- `pure (a : α) s` means that the block exited normally with return value `a` -/
pure : α → σ → DoResultPR α β σ
| /-- `return (b : β) s` means that the block exited via a `return b` early-exit command -/
return : β → σ → DoResultPR α β σ
/-- `pure (a : α) s` means that the block exited normally with return value `a` -/
| pure : α → σ → DoResultPR α β σ
/-- `return (b : β) s` means that the block exited via a `return b` early-exit command -/
| return : β → σ → DoResultPR α β σ
/--
Auxiliary type used to compile `do` notation. It is an optimization of
@ -304,12 +304,12 @@ Auxiliary type used to compile `do` notation. It is an optimization of
used when neither `pure` nor `return` are possible exit paths.
-/
inductive DoResultBC (σ : Type u) where
| /-- `break s` means that `break` was called, meaning that we should exit
from the containing loop -/
break : σ → DoResultBC σ
| /-- `continue s` means that `continue` was called, meaning that we should continue
to the next iteration of the containing loop -/
continue : σ → DoResultBC σ
/-- `break s` means that `break` was called, meaning that we should exit
from the containing loop -/
| break : σ → DoResultBC σ
/-- `continue s` means that `continue` was called, meaning that we should continue
to the next iteration of the containing loop -/
| continue : σ → DoResultBC σ
/--
Auxiliary type used to compile `do` notation. It is an optimization of
@ -317,18 +317,18 @@ either `DoResultPRBC α PEmpty σ` or `DoResultPRBC PEmpty α σ` to remove the
impossible case, used when either `pure` or `return` is never used.
-/
inductive DoResultSBC (α σ : Type u) where
| /-- This encodes either `pure (a : α)` or `return (a : α)`:
* `pure (a : α) s` means that the block exited normally with return value `a`
* `return (b : β) s` means that the block exited via a `return b` early-exit command
/-- This encodes either `pure (a : α)` or `return (a : α)`:
* `pure (a : α) s` means that the block exited normally with return value `a`
* `return (b : β) s` means that the block exited via a `return b` early-exit command
The one that is actually encoded depends on the context of use. -/
pureReturn : α → σ → DoResultSBC α σ
| /-- `break s` means that `break` was called, meaning that we should exit
from the containing loop -/
break : σ → DoResultSBC α σ
| /-- `continue s` means that `continue` was called, meaning that we should continue
to the next iteration of the containing loop -/
continue : σ → DoResultSBC α σ
The one that is actually encoded depends on the context of use. -/
| pureReturn : α → σ → DoResultSBC α σ
/-- `break s` means that `break` was called, meaning that we should exit
from the containing loop -/
| break : σ → DoResultSBC α σ
/-- `continue s` means that `continue` was called, meaning that we should continue
to the next iteration of the containing loop -/
| continue : σ → DoResultSBC α σ
/-- `HasEquiv α` is the typeclass which supports the notation `x ≈ y` where `x y : α`.-/
class HasEquiv (α : Sort u) where
@ -450,8 +450,8 @@ This is the universe-polymorphic version of `PNonScalar`; it is preferred to use
`NonScalar` instead where applicable.
-/
inductive PNonScalar : Type u where
| /-- You should not use this function -/
mk (v : Nat) : PNonScalar
/-- You should not use this function -/
| mk (v : Nat) : PNonScalar
@[simp] theorem Nat.add_zero (n : Nat) : n + 0 = n := rfl
@ -932,10 +932,10 @@ transitive and contains `r`. `r⁺ a z` if and only if there exists a sequence
`a r b r ... r z` of length at least 1 connecting `a` to `z`.
-/
inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop where
| /-- If `r a b` then `r⁺ a b`. This is the base case of the transitive closure. -/
base : ∀ a b, r a b → TC r a b
| /-- The transitive closure is transitive. -/
trans : ∀ a b c, TC r a b → TC r b c → TC r a c
/-- If `r a b` then `r⁺ a b`. This is the base case of the transitive closure. -/
| base : ∀ a b, r a b → TC r a b
/-- The transitive closure is transitive. -/
| trans : ∀ a b c, TC r a b → TC r b c → TC r a c
/-! # Subtype -/

46
stage0/src/Init/Data/Format/Basic.lean generated
View file

@ -36,32 +36,32 @@ open Format in
The pretty-printing algorithm is based on Wadler's paper
[_A Prettier Printer_](https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf). -/
inductive Format where
| /-- The empty format. -/
nil : Format
| /-- A position where a newline may be inserted
/-- The empty format. -/
| nil : Format
/-- A position where a newline may be inserted
if the current group does not fit within the allotted column width. -/
line : Format
| /-- A node containing a plain string. -/
text : String → Format
| /-- `nest n f` tells the formatter that `f` is nested inside something with length `n`
so that it is pretty-printed with the correct indentation on a line break.
For example, we can define a formatter for list `l : List Format` as:
| line : Format
/-- A node containing a plain string. -/
| text : String → Format
/-- `nest n f` tells the formatter that `f` is nested inside something with length `n`
so that it is pretty-printed with the correct indentation on a line break.
For example, we can define a formatter for list `l : List Format` as:
```
let f := join <| l.intersperse <| ", " ++ Format.line
group (nest 1 <| "[" ++ f ++ "]")
```
```
let f := join <| l.intersperse <| ", " ++ Format.line
group (nest 1 <| "[" ++ f ++ "]")
```
This will be written all on one line, but if the text is too large,
the formatter will put in linebreaks after the commas and indent later lines by 1.
-/
nest (indent : Int) : Format → Format
| /-- Concatenation of two Formats. -/
append : Format → Format → Format
| /-- Creates a new flattening group for the given inner format. -/
group : Format → (behavior : FlattenBehavior := FlattenBehavior.allOrNone) → Format
| /-- Used for associating auxiliary information (e.g. `Expr`s) with `Format` objects. -/
tag : Nat → Format → Format
This will be written all on one line, but if the text is too large,
the formatter will put in linebreaks after the commas and indent later lines by 1.
-/
| nest (indent : Int) : Format → Format
/-- Concatenation of two Formats. -/
| append : Format → Format → Format
/-- Creates a new flattening group for the given inner format. -/
| group : Format → (behavior : FlattenBehavior := FlattenBehavior.allOrNone) → Format
/-- Used for associating auxiliary information (e.g. `Expr`s) with `Format` objects. -/
| tag : Nat → Format → Format
deriving Inhabited
namespace Format

19
stage0/src/Init/Data/List/Control.lean generated
View file

@ -40,10 +40,12 @@ Finally, we rarely use `mapM` with something that is not a `Monad`.
Users that want to use `mapM` with `Applicative` should use `mapA` instead.
-/
@[specialize]
def mapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
| [] => pure []
| a::as => return (← f a) :: (← mapM f as)
@[inline]
def mapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) (as : List α) : m (List β) :=
let rec @[specialize] loop
| [], bs => pure bs.reverse
| a :: as, bs => do loop as ((← f a)::bs)
loop as []
@[specialize]
def mapA {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
@ -95,12 +97,9 @@ protected def foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w
let s' ← f s a
List.foldlM f s' as
@[specialize]
def foldrM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (f : α → s → m s) → (init : s) → List α → m s
| _, s, [] => pure s
| f, s, a :: as => do
let s' ← foldrM f s as
f a s'
@[inline]
def foldrM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : α → s → m s) (init : s) (l : List α) : m s :=
l.reverse.foldlM (fun s a => f a s) init
@[specialize]
def firstM {m : Type u → Type v} [Monad m] [Alternative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m β

6
stage0/src/Init/Data/Nat/Linear.lean generated
View file

@ -588,9 +588,9 @@ theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul
cases c; rename_i eq lhs rhs
have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp; apply Nat.succ_ne_zero
have : ¬ (k == 0) → (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))
have : ¬ ((k + 1 == 0) = true) := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
have : (1 == 0) = false := rfl
have : (1 == 1) = true := rfl
have : ¬ ((k + 1 == 0) = true) := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
have : (1 == (0 : Nat)) = false := rfl
have : (1 == (1 : Nat)) = true := rfl
by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
<;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply propext <;> apply Iff.intro <;> intro h
· exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h

22
stage0/src/Init/Meta.lean generated
View file

@ -901,22 +901,22 @@ end Syntax
namespace TSyntax
def getNat (s : NumLit) : Nat :=
s.raw.isNatLit?.get!
s.raw.isNatLit?.getD 0
def getId (s : Ident) : Name :=
s.raw.getId
def getScientific (s : ScientificLit) : Nat × Bool × Nat :=
s.raw.isScientificLit?.get!
s.raw.isScientificLit?.getD (0, false, 0)
def getString (s : StrLit) : String :=
s.raw.isStrLit?.get!
s.raw.isStrLit?.getD ""
def getChar (s : CharLit) : Char :=
s.raw.isCharLit?.get!
s.raw.isCharLit?.getD default
def getName (s : NameLit) : Name :=
s.raw.isNameLit?.get!
s.raw.isNameLit?.getD .anonymous
namespace Compat
@ -1187,12 +1187,12 @@ inductive TransparencyMode where
deriving Inhabited, BEq, Repr
inductive EtaStructMode where
| /-- Enable eta for structure and classes. -/
all
| /-- Enable eta only for structures that are not classes. -/
notClasses
| /-- Disable eta for structures and classes. -/
none
/-- Enable eta for structure and classes. -/
| all
/-- Enable eta only for structures that are not classes. -/
| notClasses
/-- Disable eta for structures and classes. -/
| none
deriving Inhabited, BEq, Repr
namespace DSimp

338
stage0/src/Init/Prelude.lean generated
View file

@ -107,8 +107,8 @@ This is the universe-polymorphic version of `Unit`; it is preferred to use
For more information about universe levels: [Types as objects](https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects)
-/
inductive PUnit : Sort u where
| /-- `PUnit.unit : PUnit` is the canonical element of the unit type. -/
unit : PUnit
/-- `PUnit.unit : PUnit` is the canonical element of the unit type. -/
| unit : PUnit
/--
The unit type, the canonical type with one element, named `unit` or `()`.
@ -177,9 +177,9 @@ In other words, `True` is simply true, and has a canonical proof, `True.intro`
For more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
-/
inductive True : Prop where
| /-- `True` is true, and `True.intro` (or more commonly, `trivial`)
is the proof. -/
intro : True
/-- `True` is true, and `True.intro` (or more commonly, `trivial`)
is the proof. -/
| intro : True
/--
`False` is the empty proposition. Thus, it has no introduction rules.
@ -264,9 +264,9 @@ The triangle in the second presentation is a macro built on top of `Eq.subst` an
For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
-/
inductive Eq : α → α → Prop where
| /-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the
equality type. See also `rfl`, which is usually used instead. -/
refl (a : α) : Eq a a
/-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the
equality type. See also `rfl`, which is usually used instead. -/
| refl (a : α) : Eq a a
/-- Non-dependent recursor for the equality type. -/
@[simp] abbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=
@ -444,8 +444,8 @@ and `f x` and `g y` are well typed it does not follow that `HEq (f x) (g y)`.
the same type then `a = b` and `HEq a b` ae equivalent.
-/
inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
| /-- Reflexivity of heterogeneous equality. -/
refl (a : α) : HEq a a
/-- Reflexivity of heterogeneous equality. -/
| refl (a : α) : HEq a a
/-- A version of `HEq.refl` with an implicit argument. -/
@[matchPattern] protected def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
@ -516,10 +516,10 @@ and you can use `match` or `cases` to destruct an `Or` assumption into the
two cases.
-/
inductive Or (a b : Prop) : Prop where
| /-- `Or.inl` is "left injection" into an `Or`. If `h : a` then `Or.inl h : a ∨ b`. -/
inl (h : a) : Or a b
| /-- `Or.inr` is "right injection" into an `Or`. If `h : b` then `Or.inr h : a ∨ b`. -/
inr (h : b) : Or a b
/-- `Or.inl` is "left injection" into an `Or`. If `h : a` then `Or.inl h : a ∨ b`. -/
| inl (h : a) : Or a b
/-- `Or.inr` is "right injection" into an `Or`. If `h : b` then `Or.inr h : a ∨ b`. -/
| inr (h : b) : Or a b
/-- Alias for `Or.inl`. -/
theorem Or.intro_left (b : Prop) (h : a) : Or a b :=
@ -546,10 +546,10 @@ code generator, while `Bool` corresponds to the type called `bool` or `boolean`
in most programming languages.
-/
inductive Bool : Type where
| /-- The boolean value `false`, not to be confused with the proposition `False`. -/
false : Bool
| /-- The boolean value `true`, not to be confused with the proposition `True`. -/
true : Bool
/-- The boolean value `false`, not to be confused with the proposition `False`. -/
| false : Bool
/-- The boolean value `true`, not to be confused with the proposition `True`. -/
| true : Bool
export Bool (false true)
@ -664,8 +664,8 @@ Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
-/
class inductive Nonempty (α : Sort u) : Prop where
| /-- If `val : α`, then `α` is nonempty. -/
intro (val : α) : Nonempty α
/-- If `val : α`, then `α` is nonempty. -/
| intro (val : α) : Nonempty α
/--
**The axiom of choice**. `Nonempty α` is a proof that `α` has an element,
@ -788,10 +788,10 @@ If a proposition `p` is `Decidable`, then `(by decide : p)` will prove it by
evaluating the decidability instance to `isTrue h` and returning `h`.
-/
class inductive Decidable (p : Prop) where
| /-- Prove that `p` is decidable by supplying a proof of `¬p` -/
isFalse (h : Not p) : Decidable p
| /-- Prove that `p` is decidable by supplying a proof of `p` -/
isTrue (h : p) : Decidable p
/-- Prove that `p` is decidable by supplying a proof of `¬p` -/
| isFalse (h : Not p) : Decidable p
/-- Prove that `p` is decidable by supplying a proof of `p` -/
| isTrue (h : p) : Decidable p
/--
Convert a decidable proposition into a boolean value.
@ -1012,12 +1012,12 @@ This type is special-cased by both the kernel and the compiler:
library (usually [GMP](https://gmplib.org/)).
-/
inductive Nat where
| /-- `Nat.zero`, normally written `0 : Nat`, is the smallest natural number.
This is one of the two constructors of `Nat`. -/
zero : Nat
| /-- The successor function on natural numbers, `succ n = n + 1`.
This is one of the two constructors of `Nat`. -/
succ (n : Nat) : Nat
/-- `Nat.zero`, normally written `0 : Nat`, is the smallest natural number.
This is one of the two constructors of `Nat`. -/
| zero : Nat
/-- The successor function on natural numbers, `succ n = n + 1`.
This is one of the two constructors of `Nat`. -/
| succ (n : Nat) : Nat
instance : Inhabited Nat where
default := Nat.zero
@ -1517,10 +1517,10 @@ An inductive definition of the less-equal relation on natural numbers,
characterized as the least relation `≤` such that `n ≤ n` and `n ≤ m → n ≤ m + 1`.
-/
protected inductive Nat.le (n : Nat) : Nat → Prop
| /-- Less-equal is reflexive: `n ≤ n` -/
refl : Nat.le n n
| /-- If `n ≤ m`, then `n ≤ m + 1`. -/
step {m} : Nat.le n m → Nat.le n (succ m)
/-- Less-equal is reflexive: `n ≤ n` -/
| refl : Nat.le n n
/-- If `n ≤ m`, then `n ≤ m + 1`. -/
| step {m} : Nat.le n m → Nat.le n (succ m)
instance : LE Nat where
le := Nat.le
@ -2097,10 +2097,10 @@ def map (f : α → β) (x : Option α) : Option β :=
```
-/
inductive Option (α : Type u) where
| /-- No value. -/
none : Option α
| /-- Some value of type `α`. -/
some (val : α) : Option α
/-- No value. -/
| none : Option α
/-- Some value of type `α`. -/
| some (val : α) : Option α
attribute [unbox] Option
@ -2140,11 +2140,11 @@ It is implemented as a linked list.
performance because it can do destructive updates.
-/
inductive List (α : Type u) where
| /-- `[]` is the empty list. -/
nil : List α
| /-- If `a : α` and `l : List α`, then `cons a l`, or `a :: l`, is the
list whose first element is `a` and with `l` as the rest of the list. -/
cons (head : α) (tail : List α) : List α
/-- `[]` is the empty list. -/
| nil : List α
/-- If `a : α` and `l : List α`, then `cons a l`, or `a :: l`, is the
list whose first element is `a` and with `l` as the rest of the list. -/
| cons (head : α) (tail : List α) : List α
instance {α} : Inhabited (List α) where
default := List.nil
@ -2610,7 +2610,7 @@ class SeqLeft (f : Type u → Type v) : Type (max (u+1) v) where
`Unit → f β` function. -/
seqLeft : {α β : Type u} → f α → (Unit → f β) → f α
/-- The typeclass which supplies the `<*` "seqRight" function. See `Applicative`. -/
/-- The typeclass which supplies the `*>` "seqRight" function. See `Applicative`. -/
class SeqRight (f : Type u → Type v) : Type (max (u+1) v) where
/-- If `x : F α` and `y : F β`, then `x *> y` evaluates `x`, then `y`,
and returns the result of `y`.
@ -2746,10 +2746,10 @@ value of type `α`. The error type is listed first because
operation returns the first encountered `error`.
-/
inductive Except (ε : Type u) (α : Type v) where
| /-- A failure value of type `ε` -/
error : ε → Except ε α
| /-- A success value of type `α` -/
ok : α → Except ε α
/-- A failure value of type `ε` -/
| error : ε → Except ε α
/-- A success value of type `α` -/
| ok : α → Except ε α
attribute [unbox] Except
@ -3070,10 +3070,10 @@ namespace EStateM
combined inductive yields a more efficient data representation.
-/
inductive Result (ε σ α : Type u) where
| /-- A success value of type `α`, and a new state `σ`. -/
ok : α → σ → Result ε σ α
| /-- A failure value of type `ε`, and a new state `σ`. -/
error : ε → σ → Result ε σ α
/-- A success value of type `α`, and a new state `σ`. -/
| ok : α → σ → Result ε σ α
/-- A failure value of type `ε`, and a new state `σ`. -/
| error : ε → σ → Result ε σ α
variable {ε σ α : Type u}
@ -3276,23 +3276,23 @@ corresponds to a Lean declaration in scope.
If the name is not in scope, Lean will report an error.
-/
inductive Name where
| /-- The "anonymous" name. -/
anonymous : Name
| /--
A string name. The name `Lean.Meta.run` is represented at
```lean
.str (.str (.str .anonymous "Lean") "Meta") "run"
```
-/
str (pre : Name) (str : String)
| /--
A numerical name. This kind of name is used, for example, to create hierarchical names for
free variables and metavariables. The identifier `_uniq.231` is represented as
```lean
.num (.str .anonymous "_uniq") 231
```
-/
num (pre : Name) (i : Nat)
/-- The "anonymous" name. -/
| anonymous : Name
/--
A string name. The name `Lean.Meta.run` is represented at
```lean
.str (.str (.str .anonymous "Lean") "Meta") "run"
```
-/
| str (pre : Name) (str : String)
/--
A numerical name. This kind of name is used, for example, to create hierarchical names for
free variables and metavariables. The identifier `_uniq.231` is represented as
```lean
.num (.str .anonymous "_uniq") 231
```
-/
| num (pre : Name) (i : Nat)
with
/-- A hash function for names, which is stored inside the name itself as a
computed field. -/
@ -3361,22 +3361,20 @@ end Name
/-- Source information of tokens. -/
inductive SourceInfo where
| /--
Token from original input with whitespace and position information.
`leading` will be inferred after parsing by `Syntax.updateLeading`. During parsing,
it is not at all clear what the preceding token was, especially with backtracking.
-/
original (leading : Substring) (pos : String.Pos) (trailing : Substring) (endPos : String.Pos)
| /--
Synthesized syntax (e.g. from a quotation) annotated with a span from the original source.
In the delaborator, we "misuse" this constructor to store synthetic positions identifying
subterms.
-/
synthetic (pos : String.Pos) (endPos : String.Pos)
| /--
Synthesized token without position information.
-/
protected none
/--
Token from original input with whitespace and position information.
`leading` will be inferred after parsing by `Syntax.updateLeading`. During parsing,
it is not at all clear what the preceding token was, especially with backtracking.
-/
| original (leading : Substring) (pos : String.Pos) (trailing : Substring) (endPos : String.Pos)
/--
Synthesized syntax (e.g. from a quotation) annotated with a span from the original source.
In the delaborator, we "misuse" this constructor to store synthetic positions identifying
subterms.
-/
| synthetic (pos : String.Pos) (endPos : String.Pos)
/-- Synthesized token without position information. -/
| protected none
instance : Inhabited SourceInfo := ⟨SourceInfo.none⟩
@ -3411,50 +3409,50 @@ Note: We do not statically know whether a syntax expects a namespace or term nam
so a `Syntax.ident` may contain both preresolution kinds.
-/
inductive Syntax.Preresolved where
| /-- A potential namespace reference -/
namespace (ns : Name)
| /-- A potential global constant or section variable reference, with additional field accesses -/
decl (n : Name) (fields : List String)
/-- A potential namespace reference -/
| namespace (ns : Name)
/-- A potential global constant or section variable reference, with additional field accesses -/
| decl (n : Name) (fields : List String)
/--
Syntax objects used by the parser, macro expander, delaborator, etc.
-/
inductive Syntax where
| /-- A `missing` syntax corresponds to a portion of the syntax tree that is
missing because of a parse error. The indexing operator on Syntax also
returns `missing` for indexing out of bounds. -/
missing : Syntax
| /-- Node in the syntax tree.
/-- A `missing` syntax corresponds to a portion of the syntax tree that is
missing because of a parse error. The indexing operator on Syntax also
returns `missing` for indexing out of bounds. -/
| missing : Syntax
/-- Node in the syntax tree.
The `info` field is used by the delaborator to store the position of the
subexpression corresponding to this node. The parser sets the `info` field
to `none`.
The parser sets the `info` field to `none`, with position retrieval continuing recursively.
Nodes created by quotatons use the result from `SourceInfo.fromRef` so that they are marked
as synthetic even when the leading/trailing token is not.
The delaborator uses the `info` field to store the position of the subexpression
corresponding to this node.
The `info` field is used by the delaborator to store the position of the
subexpression corresponding to this node. The parser sets the `info` field
to `none`.
The parser sets the `info` field to `none`, with position retrieval continuing recursively.
Nodes created by quotatons use the result from `SourceInfo.fromRef` so that they are marked
as synthetic even when the leading/trailing token is not.
The delaborator uses the `info` field to store the position of the subexpression
corresponding to this node.
(Remark: the `node` constructor did not have an `info` field in previous
versions. This caused a bug in the interactive widgets, where the popup for
`a + b` was the same as for `a`. The delaborator used to associate
subexpressions with pretty-printed syntax by setting the (string) position
of the first atom/identifier to the (expression) position of the
subexpression. For example, both `a` and `a + b` have the same first
identifier, and so their infos got mixed up.) -/
node (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
| /-- An `atom` corresponds to a keyword or piece of literal unquoted syntax.
These correspond to quoted strings inside `syntax` declarations.
For example, in `(x + y)`, `"("`, `"+"` and `")"` are `atom`
and `x` and `y` are `ident`. -/
atom (info : SourceInfo) (val : String) : Syntax
| /-- An `ident` corresponds to an identifier as parsed by the `ident` or
`rawIdent` parsers.
* `rawVal` is the literal substring from the input file
* `val` is the parsed identifier (with hygiene)
* `preresolved` is the list of possible declarations this could refer to
-/
ident (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List Syntax.Preresolved) : Syntax
(Remark: the `node` constructor did not have an `info` field in previous
versions. This caused a bug in the interactive widgets, where the popup for
`a + b` was the same as for `a`. The delaborator used to associate
subexpressions with pretty-printed syntax by setting the (string) position
of the first atom/identifier to the (expression) position of the
subexpression. For example, both `a` and `a + b` have the same first
identifier, and so their infos got mixed up.) -/
| node (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
/-- An `atom` corresponds to a keyword or piece of literal unquoted syntax.
These correspond to quoted strings inside `syntax` declarations.
For example, in `(x + y)`, `"("`, `"+"` and `")"` are `atom`
and `x` and `y` are `ident`. -/
| atom (info : SourceInfo) (val : String) : Syntax
/-- An `ident` corresponds to an identifier as parsed by the `ident` or
`rawIdent` parsers.
* `rawVal` is the literal substring from the input file
* `val` is the parsed identifier (with hygiene)
* `preresolved` is the list of possible declarations this could refer to
-/
| ident (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List Syntax.Preresolved) : Syntax
/-- `SyntaxNodeKinds` is a set of `SyntaxNodeKind` (implemented as a list). -/
def SyntaxNodeKinds := List SyntaxNodeKind
@ -3739,48 +3737,48 @@ A `ParserDescr` is a grammar for parsers. This is used by the `syntax` command
to produce parsers without having to `import Lean`.
-/
inductive ParserDescr where
| /-- A (named) nullary parser, like `ppSpace` -/
const (name : Name)
| /-- A (named) unary parser, like `group(p)` -/
unary (name : Name) (p : ParserDescr)
| /-- A (named) binary parser, like `orelse` or `andthen`
(written as `p1 <|> p2` and `p1 p2` respectively in `syntax`) -/
binary (name : Name) (p₁ p₂ : ParserDescr)
| /-- Parses using `p`, then pops the stack to create a new node with kind `kind`.
The precedence `prec` is used to determine whether the parser should apply given
the current precedence level. -/
node (kind : SyntaxNodeKind) (prec : Nat) (p : ParserDescr)
| /-- Like `node` but for trailing parsers (which start with a nonterminal).
Assumes the lhs is already on the stack, and parses using `p`, then pops the
stack including the lhs to create a new node with kind `kind`.
The precedence `prec` and `lhsPrec` are used to determine whether the parser
should apply. -/
trailingNode (kind : SyntaxNodeKind) (prec lhsPrec : Nat) (p : ParserDescr)
| /-- A literal symbol parser: parses `val` as a literal.
This parser does not work on identifiers, so `symbol` arguments are declared
as "keywords" and cannot be used as identifiers anywhere in the file. -/
symbol (val : String)
| /-- Like `symbol`, but without reserving `val` as a keyword.
If `includeIdent` is true then `ident` will be reinterpreted as `atom` if it matches. -/
nonReservedSymbol (val : String) (includeIdent : Bool)
| /-- Parses using the category parser `catName` with right binding power
(i.e. precedence) `rbp`. -/
cat (catName : Name) (rbp : Nat)
| /-- Parses using another parser `declName`, which can be either
a `Parser` or `ParserDescr`. -/
parser (declName : Name)
| /-- Like `node`, but also declares that the body can be matched using an antiquotation
with name `name`. For example, `def $id:declId := 1` uses an antiquotation with
name `declId` in the place where a `declId` is expected. -/
nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : ParserDescr)
| /-- A `sepBy(p, sep)` parses 0 or more occurrences of `p` separated by `sep`.
`psep` is usually the same as `symbol sep`, but it can be overridden.
`sep` is only used in the antiquot syntax: `$x;*` would match if `sep` is `";"`.
`allowTrailingSep` is true if e.g. `a, b,` is also allowed to match. -/
sepBy (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false)
| /-- `sepBy1` is just like `sepBy`, except it takes 1 or more instead of
0 or more occurrences of `p`. -/
sepBy1 (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false)
/-- A (named) nullary parser, like `ppSpace` -/
| const (name : Name)
/-- A (named) unary parser, like `group(p)` -/
| unary (name : Name) (p : ParserDescr)
/-- A (named) binary parser, like `orelse` or `andthen`
(written as `p1 <|> p2` and `p1 p2` respectively in `syntax`) -/
| binary (name : Name) (p₁ p₂ : ParserDescr)
/-- Parses using `p`, then pops the stack to create a new node with kind `kind`.
The precedence `prec` is used to determine whether the parser should apply given
the current precedence level. -/
| node (kind : SyntaxNodeKind) (prec : Nat) (p : ParserDescr)
/-- Like `node` but for trailing parsers (which start with a nonterminal).
Assumes the lhs is already on the stack, and parses using `p`, then pops the
stack including the lhs to create a new node with kind `kind`.
The precedence `prec` and `lhsPrec` are used to determine whether the parser
should apply. -/
| trailingNode (kind : SyntaxNodeKind) (prec lhsPrec : Nat) (p : ParserDescr)
/-- A literal symbol parser: parses `val` as a literal.
This parser does not work on identifiers, so `symbol` arguments are declared
as "keywords" and cannot be used as identifiers anywhere in the file. -/
| symbol (val : String)
/-- Like `symbol`, but without reserving `val` as a keyword.
If `includeIdent` is true then `ident` will be reinterpreted as `atom` if it matches. -/
| nonReservedSymbol (val : String) (includeIdent : Bool)
/-- Parses using the category parser `catName` with right binding power
(i.e. precedence) `rbp`. -/
| cat (catName : Name) (rbp : Nat)
/-- Parses using another parser `declName`, which can be either
a `Parser` or `ParserDescr`. -/
| parser (declName : Name)
/-- Like `node`, but also declares that the body can be matched using an antiquotation
with name `name`. For example, `def $id:declId := 1` uses an antiquotation with
name `declId` in the place where a `declId` is expected. -/
| nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : ParserDescr)
/-- A `sepBy(p, sep)` parses 0 or more occurrences of `p` separated by `sep`.
`psep` is usually the same as `symbol sep`, but it can be overridden.
`sep` is only used in the antiquot syntax: `$x;*` would match if `sep` is `";"`.
`allowTrailingSep` is true if e.g. `a, b,` is also allowed to match. -/
| sepBy (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false)
/-- `sepBy1` is just like `sepBy`, except it takes 1 or more instead of
0 or more occurrences of `p`. -/
| sepBy1 (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false)
instance : Inhabited ParserDescr where
default := ParserDescr.symbol ""
@ -4092,12 +4090,12 @@ structure Context where
/-- An exception in the `MacroM` monad. -/
inductive Exception where
| /-- A general error, given a message and a span (expressed as a `Syntax`). -/
error : Syntax → String → Exception
| /-- An unsupported syntax exception. We keep this separate because it is
used for control flow: if one macro does not support a syntax then we try
the next one. -/
unsupportedSyntax : Exception
/-- A general error, given a message and a span (expressed as a `Syntax`). -/
| error : Syntax → String → Exception
/-- An unsupported syntax exception. We keep this separate because it is
used for control flow: if one macro does not support a syntax then we try
the next one. -/
| unsupportedSyntax : Exception
/-- The mutable state for the `MacroM` monad. -/
structure State where

3
stage0/src/Lean/Attributes.lean generated
View file

@ -3,9 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Syntax
import Lean.CoreM
import Lean.ResolveName
import Lean.MonadEnv
namespace Lean

96
stage0/src/Lean/Compiler/IR/Basic.lean generated
View file

@ -191,36 +191,36 @@ def CtorInfo.isScalar (info : CtorInfo) : Bool :=
!info.isRef
inductive Expr where
| /-- We use `ctor` mainly for constructing Lean object/tobject values `lean_ctor_object` in the runtime.
This instruction is also used to creat `struct` and `union` return values.
For `union`, only `i.cidx` is relevant. For `struct`, `i` is irrelevant. -/
ctor (i : CtorInfo) (ys : Array Arg)
/-- We use `ctor` mainly for constructing Lean object/tobject values `lean_ctor_object` in the runtime.
This instruction is also used to creat `struct` and `union` return values.
For `union`, only `i.cidx` is relevant. For `struct`, `i` is irrelevant. -/
| ctor (i : CtorInfo) (ys : Array Arg)
| reset (n : Nat) (x : VarId)
| /-- `reuse x in ctor_i ys` instruction in the paper. -/
reuse (x : VarId) (i : CtorInfo) (updtHeader : Bool) (ys : Array Arg)
| /-- Extract the `tobject` value at Position `sizeof(void*)*i` from `x`.
We also use `proj` for extracting fields from `struct` return values, and casting `union` return values. -/
proj (i : Nat) (x : VarId)
| /-- Extract the `Usize` value at Position `sizeof(void*)*i` from `x`. -/
uproj (i : Nat) (x : VarId)
| /-- Extract the scalar value at Position `sizeof(void*)*n + offset` from `x`. -/
sproj (n : Nat) (offset : Nat) (x : VarId)
| /-- Full application. -/
fap (c : FunId) (ys : Array Arg)
| /-- Partial application that creates a `pap` value (aka closure in our nonstandard terminology). -/
pap (c : FunId) (ys : Array Arg)
| /-- Application. `x` must be a `pap` value. -/
ap (x : VarId) (ys : Array Arg)
| /-- Given `x : ty` where `ty` is a scalar type, this operation returns a value of Type `tobject`.
For small scalar values, the Result is a tagged pointer, and no memory allocation is performed. -/
box (ty : IRType) (x : VarId)
| /-- Given `x : [t]object`, obtain the scalar value. -/
unbox (x : VarId)
/-- `reuse x in ctor_i ys` instruction in the paper. -/
| reuse (x : VarId) (i : CtorInfo) (updtHeader : Bool) (ys : Array Arg)
/-- Extract the `tobject` value at Position `sizeof(void*)*i` from `x`.
We also use `proj` for extracting fields from `struct` return values, and casting `union` return values. -/
| proj (i : Nat) (x : VarId)
/-- Extract the `Usize` value at Position `sizeof(void*)*i` from `x`. -/
| uproj (i : Nat) (x : VarId)
/-- Extract the scalar value at Position `sizeof(void*)*n + offset` from `x`. -/
| sproj (n : Nat) (offset : Nat) (x : VarId)
/-- Full application. -/
| fap (c : FunId) (ys : Array Arg)
/-- Partial application that creates a `pap` value (aka closure in our nonstandard terminology). -/
| pap (c : FunId) (ys : Array Arg)
/-- Application. `x` must be a `pap` value. -/
| ap (x : VarId) (ys : Array Arg)
/-- Given `x : ty` where `ty` is a scalar type, this operation returns a value of Type `tobject`.
For small scalar values, the Result is a tagged pointer, and no memory allocation is performed. -/
| box (ty : IRType) (x : VarId)
/-- Given `x : [t]object`, obtain the scalar value. -/
| unbox (x : VarId)
| lit (v : LitVal)
| /-- Return `1 : uint8` Iff `RC(x) > 1` -/
isShared (x : VarId)
| /-- Return `1 : uint8` Iff `x : tobject` is a tagged pointer (storing a scalar value). -/
isTaggedPtr (x : VarId)
/-- Return `1 : uint8` Iff `RC(x) > 1` -/
| isShared (x : VarId)
/-- Return `1 : uint8` Iff `x : tobject` is a tagged pointer (storing a scalar value). -/
| isTaggedPtr (x : VarId)
@[export lean_ir_mk_ctor_expr] def mkCtorExpr (n : Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (ys : Array Arg) : Expr :=
Expr.ctor ⟨n, cidx, size, usize, ssize⟩ ys
@ -247,31 +247,31 @@ inductive AltCore (FnBody : Type) : Type where
| default (b : FnBody) : AltCore FnBody
inductive FnBody where
| /-- `let x : ty := e; b` -/
vdecl (x : VarId) (ty : IRType) (e : Expr) (b : FnBody)
| /-- Join point Declaration `block_j (xs) := e; b` -/
jdecl (j : JoinPointId) (xs : Array Param) (v : FnBody) (b : FnBody)
| /-- Store `y` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1.
This operation is not part of λPure is only used during optimization. -/
set (x : VarId) (i : Nat) (y : Arg) (b : FnBody)
/-- `let x : ty := e; b` -/
| vdecl (x : VarId) (ty : IRType) (e : Expr) (b : FnBody)
/-- Join point Declaration `block_j (xs) := e; b` -/
| jdecl (j : JoinPointId) (xs : Array Param) (v : FnBody) (b : FnBody)
/-- Store `y` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1.
This operation is not part of λPure is only used during optimization. -/
| set (x : VarId) (i : Nat) (y : Arg) (b : FnBody)
| setTag (x : VarId) (cidx : Nat) (b : FnBody)
| /-- Store `y : Usize` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. -/
uset (x : VarId) (i : Nat) (y : VarId) (b : FnBody)
| /-- Store `y : ty` at Position `sizeof(void*)*i + offset` in `x`. `x` must be a Constructor object and `RC(x)` must be 1.
`ty` must not be `object`, `tobject`, `irrelevant` nor `Usize`. -/
sset (x : VarId) (i : Nat) (offset : Nat) (y : VarId) (ty : IRType) (b : FnBody)
| /-- RC increment for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not.
If `persistent == true` then `x` is statically known to be a persistent object. -/
inc (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody)
| /-- RC decrement for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not.
If `persistent == true` then `x` is statically known to be a persistent object. -/
dec (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody)
/-- Store `y : Usize` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. -/
| uset (x : VarId) (i : Nat) (y : VarId) (b : FnBody)
/-- Store `y : ty` at Position `sizeof(void*)*i + offset` in `x`. `x` must be a Constructor object and `RC(x)` must be 1.
`ty` must not be `object`, `tobject`, `irrelevant` nor `Usize`. -/
| sset (x : VarId) (i : Nat) (offset : Nat) (y : VarId) (ty : IRType) (b : FnBody)
/-- RC increment for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not.
If `persistent == true` then `x` is statically known to be a persistent object. -/
| inc (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody)
/-- RC decrement for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not.
If `persistent == true` then `x` is statically known to be a persistent object. -/
| dec (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody)
| del (x : VarId) (b : FnBody)
| mdata (d : MData) (b : FnBody)
| case (tid : Name) (x : VarId) (xType : IRType) (cs : Array (AltCore FnBody))
| ret (x : Arg)
| /-- Jump to join point `j` -/
jmp (j : JoinPointId) (ys : Array Arg)
/-- Jump to join point `j` -/
| jmp (j : JoinPointId) (ys : Array Arg)
| unreachable
instance : Inhabited FnBody := ⟨FnBody.unreachable⟩

2
stage0/src/Lean/Compiler/InitAttr.lean generated
View file

@ -3,8 +3,6 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Environment
import Lean.Attributes
import Lean.Elab.InfoTree.Main
namespace Lean

11
stage0/src/Lean/Compiler/LCNF/Basic.lean generated
View file

@ -296,6 +296,17 @@ where
| .jmp .. => inc
| .return .. | unreach .. => return ()
partial def Code.forM [Monad m] (c : Code) (f : Code → m Unit) : m Unit :=
go c
where
go (c : Code) : m Unit := do
f c
match c with
| .let _ k => go k
| .fun decl k | .jp decl k => go decl.value; go k
| .cases c => c.alts.forM fun alt => go alt.getCode
| .unreach .. | .return .. | .jmp .. => return ()
/--
Declaration being processed by the Lean to Lean compiler passes.
-/

26
stage0/src/Lean/Compiler/LCNF/Bind.lean generated
View file

@ -66,20 +66,28 @@ where
else
return ps
def FunDeclCore.etaExpand (decl : FunDecl) : CompilerM FunDecl := do
let typeArity := getArrowArity decl.type
let valueArity := decl.getArity
def etaExpandCore? (type : Expr) (params : Array Param) (value : Code) : CompilerM (Option (Array Param × Code)) := do
let typeArity := getArrowArity type
let valueArity := params.size
if typeArity <= valueArity then
-- It can be < because of the "any" type
return decl
return none
else
let valueType ← instantiateForall decl.type decl.params
let valueType ← instantiateForall type params
let psNew ← mkNewParams valueType
let params := decl.params ++ psNew
let params := params ++ psNew
let xs := psNew.map fun p => Expr.fvar p.fvarId
let value ← decl.value.bind fun fvarId => do
let value ← value.bind fun fvarId => do
let auxDecl ← mkAuxLetDecl (mkAppN (.fvar fvarId) xs)
return .let auxDecl (.return auxDecl.fvarId)
decl.update decl.type params value
return (params, value)
end Lean.Compiler.LCNF
def FunDeclCore.etaExpand (decl : FunDecl) : CompilerM FunDecl := do
let some (params, value) ← etaExpandCore? decl.type decl.params decl.value | return decl
decl.update decl.type params value
def Decl.etaExpand (decl : Decl) : CompilerM Decl := do
let some (params, value) ← etaExpandCore? decl.type decl.params decl.value | return decl
return { decl with params, value }
end Lean.Compiler.LCNF

16
stage0/src/Lean/Compiler/LCNF/CSE.lean generated
View file

@ -32,9 +32,13 @@ instance : MonadFVarSubst M where
let map := (← get).map
try x finally modify fun s => { s with map }
def replaceFVar (fvarId fvarId' : FVarId) : M Unit := do
eraseFVar fvarId
modify fun s => { s with subst := s.subst.insert fvarId (.fvar fvarId') }
def replaceLet (decl : LetDecl) (fvarId : FVarId) : M Unit := do
eraseLetDecl decl
modify fun s => { s with subst := s.subst.insert decl.fvarId (.fvar fvarId) }
def replaceFun (decl : FunDecl) (fvarId : FVarId) : M Unit := do
eraseFunDecl decl
modify fun s => { s with subst := s.subst.insert decl.fvarId (.fvar fvarId) }
partial def _root_.Lean.Compiler.LCNF.Code.cse (code : Code) : CompilerM Code :=
go code |>.run' {}
@ -51,8 +55,8 @@ where
let decl ← normLetDecl decl
-- We only apply CSE to pure code
match (← get).map.find? decl.value with
| some fvarId' =>
replaceFVar decl.fvarId fvarId'
| some fvarId =>
replaceLet decl fvarId
go k
| none =>
addEntry decl.value decl.fvarId
@ -62,7 +66,7 @@ where
let value := decl.toExpr
match (← get).map.find? value with
| some fvarId' =>
replaceFVar decl.fvarId fvarId'
replaceFun decl fvarId'
go k
| none =>
addEntry value decl.fvarId

39
stage0/src/Lean/Compiler/LCNF/Check.lean generated
View file

@ -29,8 +29,7 @@ abbrev CheckM := ReaderT Context $ StateRefT State InferTypeM
def checkFVar (fvarId : FVarId) : CheckM Unit :=
unless (← read).vars.contains fvarId do
let localDecl ← getLocalDecl fvarId
throwError "invalid out of scope free variable {localDecl.userName}"
throwError "invalid out of scope free variable {← getBinderName fvarId}"
def checkAppArgs (f : Expr) (args : Array Expr) : CheckM Unit := do
let mut fType ← inferType f
@ -92,11 +91,8 @@ def checkJpInScope (jp : FVarId) : CheckM Unit := do
throwError "invalid jump to out of scope join point `{mkFVar jp}`"
def checkParam (param : Param) : CheckM Unit := do
let localDecl ← getLocalDecl param.fvarId
unless localDecl.userName == param.binderName do
throwError "LCNF parameter mismatch at `{param.binderName}`, binder name in local context `{localDecl.userName}`"
unless localDecl.type == param.type do
throwError "LCNF parameter mismatch at `{param.binderName}`, type in local context{indentExpr localDecl.type}\nexpected{indentExpr param.type}"
unless param == (← getParam param.fvarId) do
throwError "LCNF parameter mismatch at `{param.binderName}`, does not value in local context"
def checkParams (params : Array Param) : CheckM Unit :=
params.forM checkParam
@ -106,13 +102,8 @@ def checkLetDecl (letDecl : LetDecl) : CheckM Unit := do
let valueType ← inferType letDecl.value
unless compatibleTypes letDecl.type valueType do
throwError "type mismatch at `{letDecl.binderName}`, value has type{indentExpr valueType}\nbut is expected to have type{indentExpr letDecl.type}"
let localDecl ← getLocalDecl letDecl.fvarId
unless localDecl.userName == letDecl.binderName do
throwError "LCNF let declaration mismatch at `{letDecl.binderName}`, binder name in local context `{localDecl.userName}`"
unless localDecl.type == letDecl.type do
throwError "LCNF let declaration mismatch at `{letDecl.binderName}`, type in local context{indentExpr localDecl.type}\nexpected{indentExpr letDecl.type}"
unless localDecl.value == letDecl.value do
throwError "LCNF let declaration mismatch at `{letDecl.binderName}`, value in local context{indentExpr localDecl.value}\nexpected{indentExpr letDecl.value}"
unless letDecl == (← getLetDecl letDecl.fvarId) do
throwError "LCNF let declaration mismatch at `{letDecl.binderName}`, does not match value in local context"
def addFVarId (fvarId : FVarId) : CheckM Unit := do
if (← get).all.contains fvarId then
@ -143,11 +134,11 @@ partial def checkFunDeclCore (declName : Name) (type : Expr) (params : Array Par
partial def checkFunDecl (funDecl : FunDecl) : CheckM Unit := do
checkFunDeclCore funDecl.binderName funDecl.type funDecl.params funDecl.value
let localDecl ← getLocalDecl funDecl.fvarId
unless localDecl.userName == funDecl.binderName do
throwError "LCNF local function declaration mismatch at `{funDecl.binderName}`, binder name in local context `{localDecl.userName}`"
unless localDecl.type == funDecl.type do
throwError "LCNF local function declaration mismatch at `{funDecl.binderName}`, type in local context{indentExpr localDecl.type}\nexpected{indentExpr funDecl.type}"
let decl ← getFunDecl funDecl.fvarId
unless decl.binderName == funDecl.binderName do
throwError "LCNF local function declaration mismatch at `{funDecl.binderName}`, binder name in local context `{decl.binderName}`"
unless decl.type == funDecl.type do
throwError "LCNF local function declaration mismatch at `{funDecl.binderName}`, type in local context{indentExpr decl.type}\nexpected{indentExpr funDecl.type}"
unless (← getFunDecl funDecl.fvarId) == funDecl do
throwError "LCNF local function declaration mismatch at `{funDecl.binderName}`, declaration in local context does match"
@ -155,7 +146,7 @@ partial def checkCases (c : Cases) : CheckM Expr := do
let mut ctorNames : NameSet := {}
let mut hasDefault := false
checkFVar c.discr
let discrType ← inferFVarType c.discr
let discrType ← LCNF.getType c.discr
unless discrType.isAnyType do
let .const declName _ := discrType.headBeta.getAppFn | throwError "unexpected LCNF discriminant type {discrType}"
unless c.typeName == declName do
@ -213,9 +204,13 @@ Check whether every local declaration in the local context is used in one of giv
-/
partial def checkDeadLocalDecls (decls : Array Decl) : CompilerM Unit := do
let (_, s) := visitDecls decls |>.run {}
(← get).lctx.localDecls.forM fun fvarId decl =>
let usesFVar (binderName : Name) (fvarId : FVarId) :=
unless s.contains fvarId do
throwError "LCNF local context contains unused local variable declaration `{decl.userName}`"
throwError "LCNF local context contains unused local variable declaration `{binderName}`"
let lctx := (← get).lctx
lctx.params.forM fun fvarId decl => usesFVar decl.binderName fvarId
lctx.letDecls.forM fun fvarId decl => usesFVar decl.binderName fvarId
lctx.funDecls.forM fun fvarId decl => usesFVar decl.binderName fvarId
where
visitFVar (fvarId : FVarId) : StateM FVarIdHashSet Unit :=
modify (·.insert fvarId)

83
stage0/src/Lean/Compiler/LCNF/CompilerM.lean generated
View file

@ -31,13 +31,45 @@ instance : AddMessageContext CompilerM where
let opts ← getOptions
return MessageData.withContext { env, lctx, opts, mctx := {} } msgData
def getLocalDecl (fvarId : FVarId) : CompilerM LocalDecl := do
let some decl := (← get).lctx.localDecls.find? fvarId | throwError "unknown free variable {fvarId.name}"
return decl
def getType (fvarId : FVarId) : CompilerM Expr := do
let lctx := (← get).lctx
if let some decl := lctx.letDecls.find? fvarId then
return decl.type
else if let some decl := lctx.params.find? fvarId then
return decl.type
else if let some decl := lctx.funDecls.find? fvarId then
return decl.type
else
throwError "unknown free variable {fvarId.name}"
def getBinderName (fvarId : FVarId) : CompilerM Name := do
let lctx := (← get).lctx
if let some decl := lctx.letDecls.find? fvarId then
return decl.binderName
else if let some decl := lctx.params.find? fvarId then
return decl.binderName
else if let some decl := lctx.funDecls.find? fvarId then
return decl.binderName
else
throwError "unknown free variable {fvarId.name}"
def findParam? (fvarId : FVarId) : CompilerM (Option Param) :=
return (← get).lctx.params.find? fvarId
def findLetDecl? (fvarId : FVarId) : CompilerM (Option LetDecl) :=
return (← get).lctx.letDecls.find? fvarId
def findFunDecl? (fvarId : FVarId) : CompilerM (Option FunDecl) :=
return (← get).lctx.funDecls.find? fvarId
def getParam (fvarId : FVarId) : CompilerM Param := do
let some param ← findParam? fvarId | throwError "unknown parameter {fvarId.name}"
return param
def getLetDecl (fvarId : FVarId) : CompilerM LetDecl := do
let some decl ← findLetDecl? fvarId | throwError "unknown let-declaration {fvarId.name}"
return decl
def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
let some decl ← findFunDecl? fvarId | throwError "unknown local function {fvarId.name}"
return decl
@ -45,14 +77,25 @@ def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
@[inline] def modifyLCtx (f : LCtx → LCtx) : CompilerM Unit := do
modify fun s => { s with lctx := f s.lctx }
def eraseFVar (fvarId : FVarId) (recursive := true) : CompilerM Unit := do
modifyLCtx fun lctx => lctx.erase fvarId recursive
def eraseLetDecl (decl : LetDecl) : CompilerM Unit := do
modifyLCtx fun lctx => lctx.eraseLetDecl decl
def eraseFVarsAt (code : Code) : CompilerM Unit := do
modifyLCtx fun lctx => lctx.eraseFVarsAt code
def eraseFunDecl (decl : FunDecl) (recursive := true) : CompilerM Unit := do
modifyLCtx fun lctx => lctx.eraseFunDecl decl recursive
def eraseCode (code : Code) : CompilerM Unit := do
modifyLCtx fun lctx => lctx.eraseCode code
def eraseParam (param : Param) : CompilerM Unit :=
modifyLCtx fun lctx => lctx.eraseParam param
def eraseParams (params : Array Param) : CompilerM Unit :=
params.forM (eraseFVar ·.fvarId)
modifyLCtx fun lctx => lctx.eraseParams params
def eraseCodeDecl (decl : CodeDecl) : CompilerM Unit := do
match decl with
| .let decl => eraseLetDecl decl
| .jp decl | .fun decl => eraseFunDecl decl
/--
A free variable substitution.
@ -132,8 +175,9 @@ private def mkNewFVarId (fvarId : FVarId) : M FVarId := do
private def addParam (p : Param) : M Param := do
let type ← normExpr p.type
let fvarId ← mkNewFVarId p.fvarId
modifyLCtx fun lctx => lctx.addLocalDecl fvarId p.binderName type
return { p with fvarId, type }
let p := { p with fvarId, type }
modifyLCtx fun lctx => lctx.addParam p
return p
mutual
@ -154,9 +198,10 @@ partial def internalizeCode (code : Code) : M Code := do
let type ← normExpr decl.type
let value ← normExpr decl.value
let fvarId ← mkNewFVarId decl.fvarId
modifyLCtx fun lctx => lctx.addLetDecl fvarId binderName type value
let decl := { decl with binderName, fvarId, type, value }
modifyLCtx fun lctx => lctx.addLetDecl decl
let k ← internalizeCode k
return .let { decl with binderName, fvarId, type, value } k
return .let decl k
| .fun decl k =>
return .fun (← internalizeFunDecl decl) (← internalizeCode k)
| .jp decl k =>
@ -198,13 +243,15 @@ Helper functions for creating LCNF local declarations.
def mkParam (binderName : Name) (type : Expr) (borrow : Bool) : CompilerM Param := do
let fvarId ← mkFreshFVarId
modifyLCtx fun lctx => lctx.addLocalDecl fvarId binderName type
return { fvarId, binderName, type, borrow }
let param := { fvarId, binderName, type, borrow }
modifyLCtx fun lctx => lctx.addParam param
return param
def mkLetDecl (binderName : Name) (type : Expr) (value : Expr) : CompilerM LetDecl := do
let fvarId ← mkFreshFVarId
modifyLCtx fun lctx => lctx.addLetDecl fvarId binderName type value
return { fvarId, binderName, type, value }
let decl := { fvarId, binderName, type, value }
modifyLCtx fun lctx => lctx.addLetDecl decl
return decl
def mkFunDecl (binderName : Name) (type : Expr) (params : Array Param) (value : Code) : CompilerM FunDecl := do
let fvarId ← mkFreshFVarId
@ -217,7 +264,7 @@ private unsafe def updateParamImp (p : Param) (type : Expr) : CompilerM Param :=
return p
else
let p := { p with type }
modifyLCtx fun lctx => lctx.addLocalDecl p.fvarId p.binderName p.type
modifyLCtx fun lctx => lctx.addParam p
return p
@[implementedBy updateParamImp] opaque Param.update (p : Param) (type : Expr) : CompilerM Param
@ -227,7 +274,7 @@ private unsafe def updateLetDeclImp (decl : LetDecl) (type : Expr) (value : Expr
return decl
else
let decl := { decl with type, value }
modifyLCtx fun lctx => lctx.addLetDecl decl.fvarId decl.binderName decl.type decl.value
modifyLCtx fun lctx => lctx.addLetDecl decl
return decl
@[implementedBy updateLetDeclImp] opaque LetDecl.update (decl : LetDecl) (type : Expr) (value : Expr) : CompilerM LetDecl

6
stage0/src/Lean/Compiler/LCNF/ElimDead.lean generated
View file

@ -51,7 +51,7 @@ partial def elimDead (code : Code) : M Code := do
collectExprM decl.value
return code.updateCont! k
else
eraseFVar decl.fvarId
eraseLetDecl decl
return k
| .fun decl k | .jp decl k =>
let k ← elimDead k
@ -59,7 +59,7 @@ partial def elimDead (code : Code) : M Code := do
let decl ← visitFunDecl decl
return code.updateFun! decl k
else
eraseFVar decl.fvarId
eraseFunDecl decl
return k
| .cases c =>
let alts ← c.alts.mapMonoM fun alt => return alt.updateCode (← elimDead alt.getCode)
@ -79,4 +79,4 @@ def Code.elimDead (code : Code) : CompilerM Code :=
def Decl.elimDead (decl : Decl) : CompilerM Decl := do
return { decl with value := (← decl.value.elimDead) }
end Lean.Compiler.LCNF
end Lean.Compiler.LCNF

26
stage0/src/Lean/Compiler/LCNF/InferType.lean generated
View file

@ -21,16 +21,22 @@ created during type inference.
-/
abbrev InferTypeM := ReaderT LocalContext CompilerM
def getLocalDecl (fvarId : FVarId) : InferTypeM LocalDecl := do
def getBinderName (fvarId : FVarId) : InferTypeM Name := do
match (← read).find? fvarId with
| some localDecl => return localDecl
| none => LCNF.getLocalDecl fvarId
| some localDecl => return localDecl.userName
| none => LCNF.getBinderName fvarId
def getType (fvarId : FVarId) : InferTypeM Expr := do
match (← read).find? fvarId with
| some localDecl => return localDecl.type
| none => LCNF.getType fvarId
def mkForallFVars (xs : Array Expr) (type : Expr) : InferTypeM Expr :=
let b := type.abstract xs
xs.size.foldRevM (init := b) fun i b => do
let x := xs[i]!
let .cdecl _ _ n ty _ ← getLocalDecl x.fvarId! | unreachable!
let n ← InferType.getBinderName x.fvarId!
let ty ← InferType.getType x.fvarId!
let ty := ty.abstractRange i xs;
return .forallE n ty b .default
@ -43,9 +49,6 @@ def mkForallParams (params : Array Param) (type : Expr) : InferTypeM Expr :=
withReader (fun lctx => lctx.mkLocalDecl fvarId binderName type binderInfo) do
k (.fvar fvarId)
def inferFVarType (fvarId : FVarId) : InferTypeM Expr :=
return (← getLocalDecl fvarId).type
def inferConstType (declName : Name) (us : List Level) : CoreM Expr :=
if declName == ``lcAny || declName == ``lcErased then
return anyTypeExpr
@ -60,7 +63,7 @@ mutual
| .proj n i s => inferProjType n i s
| .app .. => inferAppType e
| .mvar .. => throwError "unexpected metavariable {e}"
| .fvar fvarId => inferFVarType fvarId
| .fvar fvarId => InferType.getType fvarId
| .bvar .. => throwError "unexpected bound variable {e}"
| .mdata _ e => inferType e
| .lit v => return v.type
@ -181,7 +184,7 @@ def mkLcCast (e : Expr) (expectedType : Expr) : CompilerM Expr := do
def Code.inferType (code : Code) : CompilerM Expr := do
match code with
| .let _ k | .fun _ k | .jp _ k => k.inferType
| .return fvarId => return (← getLocalDecl fvarId).type
| .return fvarId => getType fvarId
| .jmp fvarId args => InferType.inferAppTypeCore (.fvar fvarId) args |>.run {}
| .unreach type => return type
| .cases c => return c.resultType
@ -208,9 +211,8 @@ def mkAuxFunDecl (params : Array Param) (code : Code) (prefixName := `_f) : Comp
def mkAuxJpDecl (params : Array Param) (code : Code) (prefixName := `_jp) : CompilerM FunDecl := do
mkAuxFunDecl params code prefixName
def mkAuxJpDecl' (fvarId : FVarId) (code : Code) (prefixName := `_jp) : CompilerM FunDecl := do
let localDecl ← getLocalDecl fvarId
let params := #[{ fvarId, binderName := localDecl.userName, type := localDecl.type, borrow := false }]
def mkAuxJpDecl' (param : Param) (code : Code) (prefixName := `_jp) : CompilerM FunDecl := do
let params := #[param]
mkAuxFunDecl params code prefixName
def instantiateForall (type : Expr) (params : Array Param) : CoreM Expr :=

11
stage0/src/Lean/Compiler/LCNF/JoinPoints.lean generated
View file

@ -146,7 +146,7 @@ def test (b : Bool) (x y : Nat) : Nat :=
let x := Nat.mul y y
myjp x
cases b (f x) (g y)
```
```
`f` and `g` can be detected as a join point right away, however
`myjp` can only ever be detected as a join point after we have established
this. This is because otherwise the calls to `myjp` in `f` and `g` would
@ -172,7 +172,7 @@ where
else
eraseCandidate fvarId
| _, _, _ =>
removeCandidatesContainedIn decl.value
removeCandidatesContainedIn decl.value
go k
| .fun decl k => do
withReader (fun _ => some decl.fvarId) do
@ -207,9 +207,8 @@ where
match k, decl.value, decl.value.getAppFn with
| .return valId, .app .., (.fvar fvarId) =>
if valId == decl.fvarId then
let localDecl := (← get).lctx.localDecls.find! fvarId
if (← read).contains localDecl.fvarId then
modifyLCtx (.eraseLocal decl.fvarId)
if (← read).contains fvarId then
eraseLetDecl decl
return .jmp fvarId decl.value.getAppArgs
else
return code
@ -244,7 +243,7 @@ their definitions and call sites with `jp`/`jmp`.
def Decl.findJoinPoints (decl : Decl) : CompilerM Decl := do
let findResult ← JoinPointFinder.find decl
trace[Compiler.findJoinPoints] s!"Found: {findResult.candidates.size} jp candidates"
JoinPointFinder.replace decl findResult
JoinPointFinder.replace decl findResult
def findJoinPoints : Pass :=
.mkPerDeclaration `findJoinPoints Decl.findJoinPoints .base

80
stage0/src/Lean/Compiler/LCNF/LCtx.lean generated
View file

@ -12,68 +12,62 @@ namespace Lean.Compiler.LCNF
LCNF local context.
-/
structure LCtx where
localDecls : Std.HashMap FVarId LocalDecl := {}
params : Std.HashMap FVarId Param := {}
letDecls : Std.HashMap FVarId LetDecl := {}
funDecls : Std.HashMap FVarId FunDecl := {}
deriving Inhabited
def LCtx.addLocalDecl (lctx : LCtx) (fvarId : FVarId) (binderName : Name) (type : Expr) : LCtx :=
{ lctx with
localDecls := lctx.localDecls.insert fvarId (.cdecl 0 fvarId binderName type .default) }
def LCtx.addParam (lctx : LCtx) (param : Param) : LCtx :=
{ lctx with params := lctx.params.insert param.fvarId param }
def LCtx.addLetDecl (lctx : LCtx) (fvarId : FVarId) (binderName : Name) (type : Expr) (value : Expr) : LCtx :=
{ lctx with
localDecls := lctx.localDecls.insert fvarId (.ldecl 0 fvarId binderName type value true) }
def LCtx.addLetDecl (lctx : LCtx) (letDecl : LetDecl) : LCtx :=
{ lctx with letDecls := lctx.letDecls.insert letDecl.fvarId letDecl }
def LCtx.addFunDecl (lctx : LCtx) (funDecl : FunDecl) : LCtx :=
match lctx with
| { localDecls, funDecls } => -- TODO: this is a workaround for #316
{ localDecls := localDecls.insert funDecl.fvarId (.cdecl 0 funDecl.fvarId funDecl.binderName funDecl.type .default)
funDecls := funDecls.insert funDecl.fvarId funDecl }
{ lctx with funDecls := lctx.funDecls.insert funDecl.fvarId funDecl }
def LCtx.eraseLocal (fvarId : FVarId) : LCtx → LCtx
| { localDecls, funDecls } =>
let localDecls := localDecls.erase fvarId
{ localDecls, funDecls }
def LCtx.eraseParam (lctx : LCtx) (param : Param) : LCtx :=
{ lctx with params := lctx.params.erase param.fvarId }
partial def LCtx.erase (fvarId : FVarId) (lctx : LCtx) (recursive := true) : LCtx :=
match lctx with
| { localDecls, funDecls } =>
let localDecls := localDecls.erase fvarId
match funDecls.find? fvarId with
| none => { localDecls, funDecls }
| some funDecl =>
let funDecls := funDecls.erase fvarId
if recursive then
go funDecl.value <| goParams funDecl.params { localDecls, funDecls }
else
{ localDecls, funDecls }
where
goParams (params : Array Param) (lctx : LCtx) : LCtx :=
params.foldl (init := lctx) fun lctx p => lctx.erase p.fvarId
def LCtx.eraseParams (lctx : LCtx) (ps : Array Param) : LCtx :=
{ lctx with params := ps.foldl (init := lctx.params) fun params p => params.erase p.fvarId }
goAlts (alts : Array Alt) (lctx : LCtx) : LCtx :=
def LCtx.eraseLetDecl (lctx : LCtx) (decl : LetDecl) : LCtx :=
{ lctx with letDecls := lctx.letDecls.erase decl.fvarId }
mutual
partial def LCtx.eraseFunDecl (lctx : LCtx) (decl : FunDecl) (recursive := true) : LCtx :=
let lctx := { lctx with funDecls := lctx.funDecls.erase decl.fvarId }
if recursive then
eraseCode decl.value <| eraseParams lctx decl.params
else
lctx
partial def LCtx.eraseAlts (alts : Array Alt) (lctx : LCtx) : LCtx :=
alts.foldl (init := lctx) fun lctx alt =>
match alt with
| .default k => go k lctx
| .alt _ ps k => go k <| goParams ps lctx
| .default k => eraseCode k lctx
| .alt _ ps k => eraseCode k <| eraseParams lctx ps
go (code : Code) (lctx : LCtx) : LCtx :=
partial def LCtx.eraseCode (code : Code) (lctx : LCtx) : LCtx :=
match code with
| .let decl k => go k <| lctx.eraseLocal decl.fvarId
| .jp decl k | .fun decl k => go k <| lctx.erase decl.fvarId
| .cases c => goAlts c.alts lctx
| .let decl k => eraseCode k <| lctx.eraseLetDecl decl
| .jp decl k | .fun decl k => eraseCode k <| eraseFunDecl lctx decl
| .cases c => eraseAlts c.alts lctx
| _ => lctx
def LCtx.eraseFVarsAt (c : Code) (lctx : LCtx) : LCtx :=
LCtx.erase.go c lctx
end
/--
Convert a LCNF local context into a regular Lean local context.
-/
def LCtx.toLocalContext (lctx : LCtx) : LocalContext := Id.run do
let mut result := {}
for (_, localDecl) in lctx.localDecls.toArray do
result := result.addDecl localDecl
for (_, param) in lctx.params.toArray do
result := result.addDecl (.cdecl 0 param.fvarId param.binderName param.type .default)
for (_, decl) in lctx.letDecls.toArray do
result := result.addDecl (.ldecl 0 decl.fvarId decl.binderName decl.type decl.value true)
for (_, decl) in lctx.funDecls.toArray do
result := result.addDecl (.cdecl 0 decl.fvarId decl.binderName decl.type .default)
return result
end Lean.Compiler.LCNF
end Lean.Compiler.LCNF

14
stage0/src/Lean/Compiler/LCNF/PassManager.lean generated
View file

@ -15,13 +15,13 @@ namespace Lean.Compiler.LCNF
The pipeline phase a certain `Pass` is supposed to happen in.
-/
inductive Phase where
| /-- Here we still carry most of the original type information, most
of the dependent portion is already (partially) erased though. -/
base
| /-- In this phase polymorphism has been eliminated. -/
mono
| /-- In this phase impure stuff such as RC or efficient BaseIO transformations happen. -/
impure
/-- Here we still carry most of the original type information, most
of the dependent portion is already (partially) erased though. -/
| base
/-- In this phase polymorphism has been eliminated. -/
| mono
/-- In this phase impure stuff such as RC or efficient BaseIO transformations happen. -/
| impure
deriving Inhabited
/--

8
stage0/src/Lean/Compiler/LCNF/PrettyPrinter.lean generated
View file

@ -29,9 +29,11 @@ private def prefixJoin (pre : Format) (as : Array α) (f : α → M Format) : M
result := f!"{result}{pre}{← f a}"
return result
def ppFVar (fvarId : FVarId) : M Format := do
let localDecl ← getLocalDecl fvarId
return format localDecl.userName
def ppFVar (fvarId : FVarId) : M Format :=
try
return format (← getBinderName fvarId)
catch _ =>
return format fvarId.name
def ppExpr (e : Expr) : M Format := do
Meta.ppExpr e |>.run' { lctx := (← read) }

2
stage0/src/Lean/Compiler/LCNF/ReduceJpArity.lean generated
View file

@ -33,7 +33,7 @@ partial def reduce (code : Code) : ReduceM Code := do
mask := mask.push true
paramsNew := paramsNew.push param
else
eraseFVar param.fvarId
eraseParam param
mask := mask.push false
mask := mask.reverse
paramsNew := paramsNew.reverse

72
stage0/src/Lean/Compiler/LCNF/Simp.lean generated
View file

@ -50,19 +50,19 @@ a big problem in practice because we run the simplifier multiple times, and this
is recomputed from scratch at the beginning of each simplification step.
-/
inductive FunDeclInfo where
| /--
Local function is applied once, and must be inlined.
-/
once
| /--
Local function is applied many times, and will only be inlined
if it is small.
-/
many
| /--
Function must be inlined.
-/
mustInline
/--
Local function is applied once, and must be inlined.
-/
| once
/--
Local function is applied many times, and will only be inlined
if it is small.
-/
| many
/--
Function must be inlined.
-/
| mustInline
deriving Repr, Inhabited
/--
@ -78,8 +78,8 @@ structure FunDeclInfoMap where
def FunDeclInfoMap.format (s : FunDeclInfoMap) : CompilerM Format := do
let mut result := Format.nil
for (fvarId, info) in s.map.toList do
let localDecl ← getLocalDecl fvarId
result := result ++ "\n" ++ f!"{localDecl.userName} ↦ {repr info}"
let binderName ← getBinderName fvarId
result := result ++ "\n" ++ f!"{binderName} ↦ {repr info}"
return result
/--
@ -110,8 +110,8 @@ partial def findFunDecl? (e : Expr) : CompilerM (Option FunDecl) := do
| .fvar fvarId =>
if let some decl ← LCNF.findFunDecl? fvarId then
return some decl
else if let .ldecl (value := v) .. ← getLocalDecl fvarId then
findFunDecl? v
else if let some decl ← findLetDecl? fvarId then
findFunDecl? decl.value
else
return none
| .mdata _ e => findFunDecl? e
@ -120,8 +120,8 @@ partial def findFunDecl? (e : Expr) : CompilerM (Option FunDecl) := do
partial def findExpr (e : Expr) (skipMData := true) : CompilerM Expr := do
match e with
| .fvar fvarId =>
let .ldecl (value := v) .. ← getLocalDecl fvarId | return e
findExpr v
let some decl ← findLetDecl? fvarId | return e
findExpr decl.value
| .mdata _ e' => if skipMData then findExpr e' else return e
| _ => return e
@ -592,7 +592,7 @@ where
| .fun decl => markUsedFunDecl decl; go (i-1) (.fun decl code)
| .jp decl => markUsedFunDecl decl; go (i-1) (.jp decl code)
else
eraseFVar decl.fvarId
eraseCodeDecl decl
go (i-1) code
else
return code
@ -601,7 +601,7 @@ where
Erase all free variables occurring in `decls` from the local context.
-/
def eraseCodeDecls (decls : Array CodeDecl) : SimpM Unit := do
decls.forM fun decl => eraseFVar decl.fvarId
decls.forM fun decl => eraseCodeDecl decl
/--
Auxiliary function for projecting "type class dictionary access".
@ -785,7 +785,7 @@ private def addDefault (alts : Array Alt) : SimpM (Array Alt) := do
let .alt _ ps k := alt | unreachable!
eraseParams ps
unless first do
eraseFVarsAt k
eraseCode k
first := false
else
altsNew := altsNew.push alt
@ -831,11 +831,19 @@ def simpValue? (e : Expr) : SimpM (Option Expr) :=
simpProj? e <|> simpAppApp? e <|> applyImplementedBy? e
/--
Erase the given free variable from the local context,
Erase the given let-declaration from the local context,
and set the `simplified` flag to true.
-/
def eraseLocalDecl (fvarId : FVarId) : SimpM Unit := do
eraseFVar fvarId
def eraseLetDecl (decl : LetDecl) : SimpM Unit := do
LCNF.eraseLetDecl decl
markSimplified
/--
Erase the given local function declaration from the local context,
and set the `simplified` flag to true.
-/
def eraseFunDecl (decl : FunDecl) : SimpM Unit := do
LCNF.eraseFunDecl decl
markSimplified
/--
@ -858,7 +866,7 @@ def etaPolyApp? (letDecl : LetDecl) : OptionT SimpM FunDecl := do
let auxDecl ← mkAuxLetDecl value
let funDecl ← mkAuxFunDecl params (.let auxDecl (.return auxDecl.fvarId))
addSubst letDecl.fvarId (.fvar funDecl.fvarId)
eraseLocalDecl letDecl.fvarId
eraseLetDecl letDecl
return funDecl
mutual
@ -879,7 +887,7 @@ partial def simpCasesOnCtor? (cases : Cases) : SimpM (Option Code) := do
let discrExpr ← findCtor (.fvar discr)
let some (ctorVal, ctorArgs) := discrExpr.constructorApp? (← getEnv) (useRaw := true) | return none
let (alt, cases) := cases.extractAlt! ctorVal.name
eraseFVarsAt (.cases cases)
eraseCode (.cases cases)
markSimplified
match alt with
| .default k => simp k
@ -917,14 +925,14 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
else if decl.value.isFVar then
/- Eliminate `let _x_i := _x_j;` -/
addSubst decl.fvarId decl.value
eraseLocalDecl decl.fvarId
eraseLetDecl decl
simp k
else if let some code ← inlineApp? decl k then
eraseFVar decl.fvarId
eraseLetDecl decl
simp code
else if let some (decls, fvarId) ← inlineProjInst? decl.value then
addSubst decl.fvarId (.fvar fvarId)
eraseLocalDecl decl.fvarId
eraseLetDecl decl
let k ← simp k
attachCodeDecls decls k
else
@ -934,7 +942,7 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
return code.updateLet! decl k
else
/- Dead variable elimination -/
eraseLocalDecl decl.fvarId
eraseLetDecl decl
return k
| .fun decl k | .jp decl k =>
let mut decl := decl
@ -964,7 +972,7 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
return code.updateFun! decl k
else
/- Dead function elimination -/
eraseLocalDecl decl.fvarId
eraseFunDecl decl
return k
| .return fvarId =>
let fvarId ← normFVar fvarId

50
stage0/src/Lean/Compiler/LCNF/SpecInfo.lean generated
View file

@ -13,31 +13,31 @@ namespace Lean.Compiler.LCNF
Each parameter is associated with a `SpecParamInfo`. This information is used by `LCNF/Specialize.lean`.
-/
inductive SpecParamInfo where
| /--
A parameter that is an type class instance (or an arrow that produces a type class instance),
and is fixed in recursive declarations. By default, Lean always specializes this kind of argument.
-/
fixedInst
| /--
A parameter that is a function and is fixed in recursive declarations. If the user tags a declaration
with `@[specialize]` without specifying which arguments should be specialized, Lean will specialize
`.fixedHO` arguments in addition to `.fixedInst`.
-/
fixedHO
| /--
Computationally irrelevant parameters that are fixed in recursive declarations.
-/
fixedNeutral
| /--
An argument that has been specified in the `@[specialize]` attribute. Lean specializes it even if it is
not fixed in recursive declarations. Non-termination can happen, and Lean interrupts it with an error message
based on the stack depth.
-/
user
| /--
Parameter is not going to be specialized.
-/
other
/--
A parameter that is an type class instance (or an arrow that produces a type class instance),
and is fixed in recursive declarations. By default, Lean always specializes this kind of argument.
-/
| fixedInst
/--
A parameter that is a function and is fixed in recursive declarations. If the user tags a declaration
with `@[specialize]` without specifying which arguments should be specialized, Lean will specialize
`.fixedHO` arguments in addition to `.fixedInst`.
-/
| fixedHO
/--
Computationally irrelevant parameters that are fixed in recursive declarations.
-/
| fixedNeutral
/--
An argument that has been specified in the `@[specialize]` attribute. Lean specializes it even if it is
not fixed in recursive declarations. Non-termination can happen, and Lean interrupts it with an error message
based on the stack depth.
-/
| user
/--
Parameter is not going to be specialized.
-/
| other
deriving Inhabited, Repr
instance : ToMessageData SpecParamInfo where

1
stage0/src/Lean/Compiler/LCNF/Stage1.lean generated
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.CoreM
import Lean.MonadEnv
import Lean.Compiler.LCNF.Basic
namespace Lean.Compiler.LCNF

7
stage0/src/Lean/Compiler/LCNF/Testing.lean generated
View file

@ -233,5 +233,12 @@ Assert that the pass under test produces `Decl`s that do not contain
def assertDoesNotContainConstAfter (constName : Name) (msg : String) : TestInstaller :=
assertForEachDeclAfterEachOccurence (fun _ decl => !decl.value.containsConst constName) msg
def assertNoFun : TestInstaller :=
assertAfter do
for decl in (← getDecls) do
decl.value.forM fun
| .fun .. => throwError "declaration `{decl.name}` contains a local function declaration"
| _ => return ()
end Testing
end Lean.Compiler.LCNF

12
stage0/src/Lean/Compiler/LCNF/ToDecl.lean generated
View file

@ -100,10 +100,12 @@ def toDecl (declName : Name) : CompilerM Decl := do
-- let value ← applyCasesOnImplementedBy value
return (type, value)
let value ← toLCNF value
if let .fun decl (.return _) := value then
eraseFVar decl.fvarId (recursive := false)
return { name := declName, params := decl.params, type, value := decl.value, levelParams := info.levelParams }
let decl ← if let .fun decl (.return _) := value then
eraseFunDecl decl (recursive := false)
pure { name := declName, params := decl.params, type, value := decl.value, levelParams := info.levelParams : Decl }
else
return { name := declName, params := #[], type, value, levelParams := info.levelParams }
pure { name := declName, params := #[], type, value, levelParams := info.levelParams }
/- `toLCNF` may eta-reduce simple declarations. -/
decl.etaExpand
end Lean.Compiler.LCNF
end Lean.Compiler.LCNF

24
stage0/src/Lean/Compiler/LCNF/ToExpr.lean generated
View file

@ -30,9 +30,9 @@ where
| .lam n d b bi => .lam n (go o d) (go (o+1) b) bi
| .letE n t v b nd => .letE n (go o t) (go o v) (go (o+1) b) nd
abbrev M := ReaderT Nat $ StateM LevelMap
abbrev ToExprM := ReaderT Nat $ StateM LevelMap
private abbrev mkLambdaM (params : Array Param) (e : Expr) : M Expr :=
private abbrev mkLambdaM (params : Array Param) (e : Expr) : ToExprM Expr :=
return go (← read) (← get) params.size e
where
go (offset : Nat) (m : LevelMap) (i : Nat) (e : Expr) : Expr :=
@ -43,30 +43,30 @@ where
else
e
@[inline] private def _root_.Lean.FVarId.toExprM (fvarId : FVarId) : M Expr :=
@[inline] private def _root_.Lean.FVarId.toExprM (fvarId : FVarId) : ToExprM Expr :=
return fvarId.toExpr (← read) (← get)
@[inline] private def _root_.Lean.Expr.abstractM (e : Expr) : M Expr :=
@[inline] private def _root_.Lean.Expr.abstractM (e : Expr) : ToExprM Expr :=
return e.abstract' (← read) (← get)
@[inline] def withFVar (fvarId : FVarId) (k : M α) : M α := do
@[inline] def withFVar (fvarId : FVarId) (k : ToExprM α) : ToExprM α := do
let offset ← read
modify fun s => s.insert fvarId offset
withReader (·+1) k
@[inline] partial def withParams (params : Array Param) (k : M α) : M α :=
@[inline] partial def withParams (params : Array Param) (k : ToExprM α) : ToExprM α :=
go 0
where
@[specialize] go (i : Nat) : M α := do
@[specialize] go (i : Nat) : ToExprM α := do
if h : i < params.size then
withFVar params[i].fvarId (go (i+1))
else
k
@[inline] def run (x : M α) (offset : Nat := 0) (levelMap : LevelMap := {}) : α :=
@[inline] def run (x : ToExprM α) (offset : Nat := 0) (levelMap : LevelMap := {}) : α :=
x |>.run offset |>.run' levelMap
@[inline] def run' (x : M α) (xs : Array FVarId) : α :=
@[inline] def run' (x : ToExprM α) (xs : Array FVarId) : α :=
let map := xs.foldl (init := {}) fun map x => map.insert x map.size
run x xs.size map
@ -75,10 +75,10 @@ end ToExpr
open ToExpr
mutual
partial def FunDeclCore.toExprM (decl : FunDecl) : M Expr :=
partial def FunDeclCore.toExprM (decl : FunDecl) : ToExprM Expr :=
withParams decl.params do mkLambdaM decl.params (← decl.value.toExprM)
partial def Code.toExprM (code : Code) : M Expr := do
partial def Code.toExprM (code : Code) : ToExprM Expr := do
match code with
| .let decl k =>
let type ← decl.type.abstractM
@ -109,4 +109,4 @@ def FunDeclCore.toExpr (decl : FunDecl) (xs : Array FVarId := #[]) : Expr :=
def Decl.toExpr (decl : Decl) : Expr :=
run do withParams decl.params do mkLambdaM decl.params (← decl.value.toExprM)
end Lean.Compiler.LCNF
end Lean.Compiler.LCNF

37
stage0/src/Lean/Compiler/LCNF/ToLCNF.lean generated
View file

@ -33,8 +33,8 @@ inductive Element where
| jp (decl : FunDecl)
| fun (decl : FunDecl)
| let (decl : LetDecl)
| cases (fvarId : FVarId) (cases : Cases)
| unreach (fvarId : FVarId)
| cases (p : Param) (cases : Cases)
| unreach (p : Param)
deriving Inhabited
/--
@ -70,7 +70,7 @@ where
findFun? (f : FVarId) : CompilerM (Option FunDecl) := do
if let some funDecl ← findFunDecl? f then
return funDecl
else if let .ldecl (value := .fvar f') .. ← getLocalDecl f then
else if let some { value := .fvar f', .. } ← findLetDecl? f then
findFun? f'
else
return none
@ -89,11 +89,11 @@ where
-/
if decl.fvarId == fvarId && decl.value.isApp && decl.value.getAppFn.isFVar then
let f := decl.value.getAppFn.fvarId!
let localDecl ← getLocalDecl f
if localDecl.userName.getPrefix == `_alt then
let binderName ← getBinderName f
if binderName.getPrefix == `_alt then
if let some funDecl ← findFun? f then
let args := decl.value.getAppArgs
eraseFVar decl.fvarId
eraseLetDecl decl
if let some altJp := (← get).find? f then
/- We already have an auxiliary join point for `f`, then, we just use it. -/
return .jmp altJp.fvarId args
@ -164,23 +164,24 @@ where
| .let decl => go seq (i - 1) (.let decl c)
| .unreach _ =>
let type ← c.inferType
eraseFVarsAt c
eraseCode c
seq[:i].forM fun
| .let decl | .jp decl | .fun decl => eraseFVar decl.fvarId
| .cases _ cs => eraseFVarsAt (.cases cs)
| .unreach fvarId => eraseFVar fvarId
| .let decl => eraseLetDecl decl
| .jp decl | .fun decl => eraseFunDecl decl
| .cases _ cs => eraseCode (.cases cs)
| .unreach auxParam => eraseParam auxParam
return .unreach type
| .cases fvarId cases =>
if let .return fvarId' := c then
if fvarId == fvarId' then
eraseFVar fvarId
| .cases auxParam cases =>
if let .return fvarId := c then
if auxParam.fvarId == fvarId then
eraseParam auxParam
go seq (i - 1) (.cases cases)
else
-- `cases` is dead code
go seq (i - 1) c
else
/- Create a join point for `c` and jump to it from `cases` -/
let jpDecl ← mkAuxJpDecl' fvarId c
let jpDecl ← mkAuxJpDecl' auxParam c
go seq (i - 1) (← bindCases jpDecl cases)
else
return c
@ -212,7 +213,7 @@ def pushElement (elem : Element) : M Unit := do
def mkUnreachable (type : Expr) : M Expr := do
let p ← mkAuxParam type
pushElement (.unreach p.fvarId)
pushElement (.unreach p)
return .fvar p.fvarId
def mkAuxLetDecl (e : Expr) (prefixName := `_x) : M Expr := do
@ -470,7 +471,7 @@ where
alts := alts.push alt
let cases : Cases := { typeName, discr := discr.fvarId!, resultType, alts }
let auxDecl ← mkAuxParam resultType
pushElement (.cases auxDecl.fvarId cases)
pushElement (.cases auxDecl cases)
let result := .fvar auxDecl.fvarId
if args.size == casesInfo.arity then
return result
@ -648,4 +649,4 @@ end ToLCNF
export ToLCNF (toLCNF)
end Lean.Compiler.LCNF
end Lean.Compiler.LCNF

1
stage0/src/Lean/Compiler/LCNF/Util.lean generated
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.CoreM
import Lean.MonadEnv
import Lean.Util.Recognizers
namespace Lean.Compiler.LCNF

5
stage0/src/Lean/CoreM.lean generated
View file

@ -6,12 +6,7 @@ Authors: Leonardo de Moura
import Lean.Util.RecDepth
import Lean.Util.Trace
import Lean.Log
import Lean.Data.Options
import Lean.Environment
import Lean.Exception
import Lean.InternalExceptionId
import Lean.Eval
import Lean.MonadEnv
import Lean.ResolveName
import Lean.Elab.InfoTree.Types

1
stage0/src/Lean/Data.lean generated
View file

@ -14,6 +14,7 @@ import Lean.Data.LBool
import Lean.Data.LOption
import Lean.Data.Lsp
import Lean.Data.Name
import Lean.Data.NameMap
import Lean.Data.Occurrences
import Lean.Data.OpenDecl
import Lean.Data.Options

62
stage0/src/Lean/Data/JsonRpc.lean generated
View file

@ -37,32 +37,32 @@ instance : ToString RequestID where
[JSON-RPC](https://www.jsonrpc.org/specification#error_object) and
[LSP](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#errorCodes). -/
inductive ErrorCode where
| /-- Invalid JSON was received by the server. An error occurred on the server while parsing the JSON text.-/
parseError
| /-- The JSON sent is not a valid Request object. -/
invalidRequest
| /-- The method does not exist / is not available. -/
methodNotFound
| /-- Invalid method parameter(s). -/
invalidParams
| /-- Internal JSON-RPC error. -/
internalError
| /-- Error code indicating that a server received a notification or
request before the server has received the `initialize` request. -/
serverNotInitialized
/-- Invalid JSON was received by the server. An error occurred on the server while parsing the JSON text.-/
| parseError
/-- The JSON sent is not a valid Request object. -/
| invalidRequest
/-- The method does not exist / is not available. -/
| methodNotFound
/-- Invalid method parameter(s). -/
| invalidParams
/-- Internal JSON-RPC error. -/
| internalError
/-- Error code indicating that a server received a notification or
request before the server has received the `initialize` request. -/
| serverNotInitialized
| unknownErrorCode
-- LSP-specific codes below.
| /-- The server detected that the content of a document got
modified outside normal conditions. A server should
NOT send this error code if it detects a content change
in it unprocessed messages. The result even computed
on an older state might still be useful for the client.
/-- The server detected that the content of a document got
modified outside normal conditions. A server should
NOT send this error code if it detects a content change
in it unprocessed messages. The result even computed
on an older state might still be useful for the client.
If a client decides that a result is not of any use anymore
the client should cancel the request. -/
contentModified
| /-- The client has canceled a request and a server as detected the cancel. -/
requestCancelled
If a client decides that a result is not of any use anymore
the client should cancel the request. -/
| contentModified
/-- The client has canceled a request and a server as detected the cancel. -/
| requestCancelled
-- Lean-specific codes below.
| rpcNeedsReconnect
| workerExited
@ -104,14 +104,14 @@ Uses separate constructors for notifications and errors because client and serve
behavior is expected to be wildly different for both.
-/
inductive Message where
| /-- A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request. -/
request (id : RequestID) (method : String) (params? : Option Structured)
| /-- A notification message. A processed notification message must not send a response back. They work like events. -/
notification (method : String) (params? : Option Structured)
| /-- A Response Message sent as a result of a request. -/
response (id : RequestID) (result : Json)
| /-- A non-successful response. -/
responseError (id : RequestID) (code : ErrorCode) (message : String) (data? : Option Json)
/-- A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request. -/
| request (id : RequestID) (method : String) (params? : Option Structured)
/-- A notification message. A processed notification message must not send a response back. They work like events. -/
| notification (method : String) (params? : Option Structured)
/-- A Response Message sent as a result of a request. -/
| response (id : RequestID) (result : Json)
/-- A non-successful response. -/
| responseError (id : RequestID) (code : ErrorCode) (message : String) (data? : Option Json)
def Batch := Array Message

75
stage0/src/Lean/Data/Name.lean generated
View file

@ -3,10 +3,6 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
import Lean.Data.HashSet
import Lean.Data.RBMap
import Lean.Data.RBTree
import Lean.Data.SSet
namespace Lean
instance : Coe String Name := ⟨Name.mkSimple⟩
@ -133,77 +129,6 @@ def isNum : Name → Bool
| _ => false
end Name
open Std (RBMap RBTree mkRBMap mkRBTree)
def NameMap (α : Type) := Std.RBMap Name α Name.quickCmp
@[inline] def mkNameMap (α : Type) : NameMap α := Std.mkRBMap Name α Name.quickCmp
namespace NameMap
variable {α : Type}
instance (α : Type) : EmptyCollection (NameMap α) := ⟨mkNameMap α⟩
instance (α : Type) : Inhabited (NameMap α) where
default := {}
def insert (m : NameMap α) (n : Name) (a : α) := Std.RBMap.insert m n a
def contains (m : NameMap α) (n : Name) : Bool := Std.RBMap.contains m n
@[inline] def find? (m : NameMap α) (n : Name) : Option α := Std.RBMap.find? m n
instance : ForIn m (NameMap α) (Name × α) :=
inferInstanceAs (ForIn _ (Std.RBMap ..) ..)
end NameMap
def NameSet := RBTree Name Name.quickCmp
namespace NameSet
def empty : NameSet := mkRBTree Name Name.quickCmp
instance : EmptyCollection NameSet := ⟨empty⟩
instance : Inhabited NameSet := ⟨empty⟩
def insert (s : NameSet) (n : Name) : NameSet := Std.RBTree.insert s n
def contains (s : NameSet) (n : Name) : Bool := Std.RBMap.contains s n
instance : ForIn m NameSet Name :=
inferInstanceAs (ForIn _ (Std.RBTree ..) ..)
end NameSet
def NameSSet := SSet Name
namespace NameSSet
abbrev empty : NameSSet := SSet.empty
instance : EmptyCollection NameSSet := ⟨empty⟩
instance : Inhabited NameSSet := ⟨empty⟩
abbrev insert (s : NameSSet) (n : Name) : NameSSet := SSet.insert s n
abbrev contains (s : NameSSet) (n : Name) : Bool := SSet.contains s n
end NameSSet
def NameHashSet := Std.HashSet Name
namespace NameHashSet
@[inline] def empty : NameHashSet := Std.HashSet.empty
instance : EmptyCollection NameHashSet := ⟨empty⟩
instance : Inhabited NameHashSet := ⟨{}⟩
def insert (s : NameHashSet) (n : Name) := Std.HashSet.insert s n
def contains (s : NameHashSet) (n : Name) : Bool := Std.HashSet.contains s n
end NameHashSet
def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool :=
v₁.name.isPrefixOf v₂.name &&
v₁.scopes == v₂.scopes &&
v₁.mainModule == v₂.mainModule &&
v₁.imported == v₂.imported
def MacroScopesView.isSuffixOf (v₁ v₂ : MacroScopesView) : Bool :=
v₁.name.isSuffixOf v₂.name &&
v₁.scopes == v₂.scopes &&
v₁.mainModule == v₂.mainModule &&
v₁.imported == v₂.imported
end Lean
open Lean

85
stage0/src/Lean/Data/NameMap.lean generated Normal file
View file

@ -0,0 +1,85 @@
/-
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
import Lean.Data.HashSet
import Lean.Data.RBMap
import Lean.Data.RBTree
import Lean.Data.SSet
import Lean.Data.Name
namespace Lean
instance : Coe String Name := ⟨Name.mkSimple⟩
open Std (RBMap RBTree mkRBMap mkRBTree)
def NameMap (α : Type) := Std.RBMap Name α Name.quickCmp
@[inline] def mkNameMap (α : Type) : NameMap α := Std.mkRBMap Name α Name.quickCmp
namespace NameMap
variable {α : Type}
instance (α : Type) : EmptyCollection (NameMap α) := ⟨mkNameMap α⟩
instance (α : Type) : Inhabited (NameMap α) where
default := {}
def insert (m : NameMap α) (n : Name) (a : α) := Std.RBMap.insert m n a
def contains (m : NameMap α) (n : Name) : Bool := Std.RBMap.contains m n
@[inline] def find? (m : NameMap α) (n : Name) : Option α := Std.RBMap.find? m n
instance : ForIn m (NameMap α) (Name × α) :=
inferInstanceAs (ForIn _ (Std.RBMap ..) ..)
end NameMap
def NameSet := RBTree Name Name.quickCmp
namespace NameSet
def empty : NameSet := mkRBTree Name Name.quickCmp
instance : EmptyCollection NameSet := ⟨empty⟩
instance : Inhabited NameSet := ⟨empty⟩
def insert (s : NameSet) (n : Name) : NameSet := Std.RBTree.insert s n
def contains (s : NameSet) (n : Name) : Bool := Std.RBMap.contains s n
instance : ForIn m NameSet Name :=
inferInstanceAs (ForIn _ (Std.RBTree ..) ..)
end NameSet
def NameSSet := SSet Name
namespace NameSSet
abbrev empty : NameSSet := SSet.empty
instance : EmptyCollection NameSSet := ⟨empty⟩
instance : Inhabited NameSSet := ⟨empty⟩
abbrev insert (s : NameSSet) (n : Name) : NameSSet := SSet.insert s n
abbrev contains (s : NameSSet) (n : Name) : Bool := SSet.contains s n
end NameSSet
def NameHashSet := Std.HashSet Name
namespace NameHashSet
@[inline] def empty : NameHashSet := Std.HashSet.empty
instance : EmptyCollection NameHashSet := ⟨empty⟩
instance : Inhabited NameHashSet := ⟨{}⟩
def insert (s : NameHashSet) (n : Name) := Std.HashSet.insert s n
def contains (s : NameHashSet) (n : Name) : Bool := Std.HashSet.contains s n
end NameHashSet
def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool :=
v₁.name.isPrefixOf v₂.name &&
v₁.scopes == v₂.scopes &&
v₁.mainModule == v₂.mainModule &&
v₁.imported == v₂.imported
def MacroScopesView.isSuffixOf (v₁ v₂ : MacroScopesView) : Bool :=
v₁.name.isSuffixOf v₂.name &&
v₁.scopes == v₂.scopes &&
v₁.mainModule == v₂.mainModule &&
v₁.imported == v₂.imported
end Lean

5
stage0/src/Lean/Data/Options.lean generated
View file

@ -5,6 +5,7 @@ Authors: Sebastian Ullrich and Leonardo de Moura
-/
import Lean.ImportingFlag
import Lean.Data.KVMap
import Lean.Data.NameMap
namespace Lean
@ -51,7 +52,7 @@ def getOptionDecl (name : Name) : IO OptionDecl := do
let (some decl) ← pure (decls.find? name) | throw $ IO.userError s!"unknown option '{name}'"
pure decl
def getOptionDefaulValue (name : Name) : IO DataValue := do
def getOptionDefaultValue (name : Name) : IO DataValue := do
let decl ← getOptionDecl name
pure decl.defValue
@ -63,7 +64,7 @@ def setOptionFromString (opts : Options) (entry : String) : IO Options := do
let ps := (entry.splitOn "=").map String.trim
let [key, val] ← pure ps | throw $ IO.userError "invalid configuration option entry, it must be of the form '<key> = <value>'"
let key := Name.mkSimple key
let defValue ← getOptionDefaulValue key
let defValue ← getOptionDefaultValue key
match defValue with
| DataValue.ofString _ => pure $ opts.setString key val
| DataValue.ofBool _ =>

3
stage0/src/Lean/DocString.lean generated
View file

@ -95,7 +95,6 @@ def getDocStringText [Monad m] [MonadError m] [MonadRef m] (stx : TSyntax `Lean.
def TSyntax.getDocString (stx : TSyntax `Lean.Parser.Command.docComment) : String :=
match stx.raw[1] with
| Syntax.atom _ val => val.extract 0 (val.endPos - ⟨2⟩)
| Syntax.missing => ""
| _ => panic! s!"unexpected doc string\n{stx.raw[1]}"
| _ => ""
end Lean

3
stage0/src/Lean/Elab/Attributes.lean generated
View file

@ -3,9 +3,6 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Parser.Attr
import Lean.Attributes
import Lean.MonadEnv
import Lean.Elab.Util
namespace Lean.Elab

1
stage0/src/Lean/Elab/Binders.lean generated
View file

@ -3,7 +3,6 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Parser.Term
import Lean.Elab.Quotation.Precheck
import Lean.Elab.Term
import Lean.Elab.BindersUtil

5
stage0/src/Lean/Elab/BuiltinCommand.lean generated
View file

@ -3,12 +3,13 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Elab.DeclarationRange
import Lean.DocString
import Lean.Util.CollectLevelParams
import Lean.Meta.Reduce
import Lean.Elab.DeclarationRange
import Lean.Elab.Eval
import Lean.Elab.Command
import Lean.Elab.Open
import Lean.Elab.SetOption
namespace Lean.Elab.Command

6
stage0/src/Lean/Elab/BuiltinNotation.lean generated
View file

@ -3,11 +3,9 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Init.Data.ToString
import Lean.Compiler.BorrowedAnnotation
import Lean.Meta.KAbstract
import Lean.Meta.Transform
import Lean.Elab.App
import Lean.Meta.MatchUtil
import Lean.Elab.SyntheticMVars
namespace Lean.Elab.Term
@ -38,6 +36,8 @@ open Meta
(fun ival _ => do
match ival.ctors with
| [ctor] =>
if isPrivateNameFromImportedModule (← getEnv) ctor then
throwError "invalid ⟨...⟩ notation, constructor for `{ival.name}` is marked as private"
let cinfo ← getConstInfoCtor ctor
let numExplicitFields ← forallTelescopeReducing cinfo.type fun xs _ => do
let mut n := 0

3
stage0/src/Lean/Elab/BuiltinTerm.lean generated
View file

@ -3,7 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Elab.Term
import Lean.Elab.Open
import Lean.Elab.SetOption
import Lean.Elab.Eval
namespace Lean.Elab.Term

9
stage0/src/Lean/Elab/Command.lean generated
View file

@ -3,17 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Log
import Lean.Parser.Command
import Lean.ResolveName
import Lean.Meta.Reduce
import Lean.Elab.Term
import Lean.Elab.Tactic.Cache
import Lean.Elab.Binders
import Lean.Elab.SyntheticMVars
import Lean.Elab.DeclModifiers
import Lean.Elab.InfoTree
import Lean.Elab.SetOption
namespace Lean.Elab.Command

4
stage0/src/Lean/Elab/DeclModifiers.lean generated
View file

@ -3,12 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Modifiers
import Lean.DocString
import Lean.Structure
import Lean.Elab.Attributes
import Lean.Elab.Exception
import Lean.Elab.DeclUtil
namespace Lean.Elab

7
stage0/src/Lean/Elab/DefView.lean generated
View file

@ -3,15 +3,10 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Parser.Command
import Lean.Util.CollectLevelParams
import Lean.Util.FoldConsts
import Lean.Meta.ForEachExpr
import Lean.Meta.CollectFVars
import Lean.Elab.Command
import Lean.Elab.SyntheticMVars
import Lean.Elab.Binders
import Lean.Elab.DeclUtil
namespace Lean.Elab
inductive DefKind where

53
stage0/src/Lean/Elab/Deriving/Basic.lean generated
View file

@ -4,11 +4,62 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Wojciech Nawrocki
-/
import Lean.Elab.Command
import Lean.Elab.MutualDef
namespace Lean.Elab
open Command
namespace Term
open Meta
/-- Result for `mkInst?` -/
structure MkInstResult where
instVal : Expr
instType : Expr
outParams : Array Expr := #[]
/--
Construct an instance for `className out₁ ... outₙ type`.
The method support classes with a prefix of `outParam`s (e.g. `MonadReader`). -/
private partial def mkInst? (className : Name) (type : Expr) : MetaM (Option MkInstResult) := do
let rec go? (instType instTypeType : Expr) (outParams : Array Expr) : MetaM (Option MkInstResult) := do
let instTypeType ← whnfD instTypeType
unless instTypeType.isForall do
return none
let d := instTypeType.bindingDomain!
if d.isOutParam then
let mvar ← mkFreshExprMVar d
go? (mkApp instType mvar) (instTypeType.bindingBody!.instantiate1 mvar) (outParams.push mvar)
else
unless (← isDefEqGuarded (← inferType type) d) do
return none
let instType ← instantiateMVars (mkApp instType type)
let instVal ← synthInstance instType
return some { instVal, instType, outParams }
let instType ← mkConstWithFreshMVarLevels className
go? instType (← inferType instType) #[]
def processDefDeriving (className : Name) (declName : Name) : TermElabM Bool := do
try
let ConstantInfo.defnInfo info ← getConstInfo declName | return false
let some result ← mkInst? className info.value | return false
let instTypeNew := mkApp result.instType.appFn! (Lean.mkConst declName (info.levelParams.map mkLevelParam))
Meta.check instTypeNew
let instName ← liftMacroM <| mkUnusedBaseName (declName.appendBefore "inst" |>.appendAfter className.getString!)
addAndCompile <| Declaration.defnDecl {
name := instName
levelParams := info.levelParams
type := (← instantiateMVars instTypeNew)
value := (← instantiateMVars result.instVal)
hints := info.hints
safety := info.safety
}
addInstance instName AttributeKind.global (eval_prio default)
return true
catch _ =>
return false
end Term
def DerivingHandler := (typeNames : Array Name) → (args? : Option (TSyntax ``Parser.Term.structInst)) → CommandElabM Bool
def DerivingHandlerNoArgs := (typeNames : Array Name) → CommandElabM Bool

8
stage0/src/Lean/Elab/Deriving/Repr.lean generated
View file

@ -26,21 +26,19 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term :
let target := mkIdent header.targetNames[0]!
forallTelescopeReducing ctorVal.type fun xs _ => do
let mut fields ← `(Format.nil)
let mut first := true
if xs.size != numParams + fieldNames.size then
throwError "'deriving Repr' failed, unexpected number of fields in structure"
for i in [:fieldNames.size] do
let fieldName := fieldNames[i]!
let fieldNameLit := Syntax.mkStrLit (toString fieldName)
let x := xs[numParams + i]!
if first then
first := false
else
if i > numParams then
fields ← `($fields ++ "," ++ Format.line)
if (← isType x <||> isProof x) then
fields ← `($fields ++ $fieldNameLit ++ " := " ++ "_")
else
fields ← `($fields ++ $fieldNameLit ++ " := " ++ repr ($target.$(mkIdent fieldName):ident))
let indent := Syntax.mkNumLit <| toString ((toString fieldName |>.length) + " := ".length)
fields ← `($fields ++ $fieldNameLit ++ " := " ++ (Format.group (Format.nest $indent (repr ($target.$(mkIdent fieldName):ident)))))
`(Format.bracket "{ " $fields:term " }")
def mkBodyForInduct (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do

8
stage0/src/Lean/Elab/Do.lean generated
View file

@ -187,15 +187,15 @@ structure Alt (σ : Type) where
inductive Code where
| decl (xs : Array Var) (doElem : Syntax) (k : Code)
| reassign (xs : Array Var) (doElem : Syntax) (k : Code)
| /-- The Boolean value in `params` indicates whether we should use `(x : typeof! x)` when generating term Syntax or not -/
joinpoint (name : Name) (params : Array (Var × Bool)) (body : Code) (k : Code)
/-- The Boolean value in `params` indicates whether we should use `(x : typeof! x)` when generating term Syntax or not -/
| joinpoint (name : Name) (params : Array (Var × Bool)) (body : Code) (k : Code)
| seq (action : Syntax) (k : Code)
| action (action : Syntax)
| break (ref : Syntax)
| continue (ref : Syntax)
| return (ref : Syntax) (val : Syntax)
| /-- Recall that an if-then-else may declare a variable using `optIdent` for the branches `thenBranch` and `elseBranch`. We store the variable name at `var?`. -/
ite (ref : Syntax) (h? : Option Var) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code)
/-- Recall that an if-then-else may declare a variable using `optIdent` for the branches `thenBranch` and `elseBranch`. We store the variable name at `var?`. -/
| ite (ref : Syntax) (h? : Option Var) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code)
| match (ref : Syntax) (gen : Syntax) (discrs : Syntax) (optMotive : Syntax) (alts : Array (Alt Code))
| jmp (ref : Syntax) (jpName : Name) (args : Array Syntax)
deriving Inhabited

56
stage0/src/Lean/Elab/Extra.lean generated
View file

@ -128,18 +128,18 @@ there is no coercion `Matrix Real 5 4` from `Matrix Real 4 8` and vice-versa, bu
-/
private inductive Tree where
| /--
Leaf of the tree.
We store the `infoTrees` generated when elaborating `val`. These trees become
subtrees of the infotree nodes generated for `op` nodes.
-/
term (ref : Syntax) (infoTrees : Std.PersistentArray InfoTree) (val : Expr)
| /--
`ref` is the original syntax that expanded into `binop%`.
`macroName` is the `macro_rule` that produce the expansion. We store this information
here to make sure "go to definition" behaves similarly to notation defined without using `binop%` helper elaborator.
-/
op (ref : Syntax) (macroName : Name) (lazy : Bool) (f : Expr) (lhs rhs : Tree)
/--
Leaf of the tree.
We store the `infoTrees` generated when elaborating `val`. These trees become
subtrees of the infotree nodes generated for `op` nodes.
-/
| term (ref : Syntax) (infoTrees : Std.PersistentArray InfoTree) (val : Expr)
/--
`ref` is the original syntax that expanded into `binop%`.
`macroName` is the `macro_rule` that produce the expansion. We store this information
here to make sure "go to definition" behaves similarly to notation defined without using `binop%` helper elaborator.
-/
| op (ref : Syntax) (macroName : Name) (lazy : Bool) (f : Expr) (lhs rhs : Tree)
private partial def toTree (s : Syntax) : TermElabM Tree := do
/-
@ -381,7 +381,37 @@ def elabBinOpLazy : TermElab := elabBinOp
-/
def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
match (← resolveId? stx[1]) with
| some f => withSynthesize (mayPostpone := true) do
| some f => withSynthesizeLight do
/-
We used to use `withSynthesize (mayPostpone := true)` here instead of `withSynthesizeLight` here.
Recall that `withSynthesizeLight` is equivalent to `withSynthesize (mayPostpone := true) (synthesizeDefault := false)`.
It seems too much to apply default instances at binary relations. For example, we cannot elaborate
```
def as : List Int := [-1, 2, 0, -3, 4]
#eval as.map fun a => ite (a ≥ 0) [a] []
```
The problem is that when elaborating `a ≥ 0` we don't know yet that `a` is an `Int`.
Then, by applying default instances, we apply the default instance to `0` that forces it to become an `Int`,
and Lean infers that `a` has type `Nat`.
Then, later we get a type error because `as` is `List Int` instead of `List Nat`.
This behavior is quite counterintuitive since if we avoid this elaborator by writing
```
def as : List Int := [-1, 2, 0, -3, 4]
#eval as.map fun a => ite (GE.ge a 0) [a] []
```
everything works.
However, there is a drawback of using `withSynthesizeLight` instead of `withSynthesize (mayPostpone := true)`.
The following cannot be elaborated
```
have : (0 == 1) = false := rfl
```
We get a type error at `rfl`. `0 == 1` only reduces to `false` after we have applied the default instances that force
the numeral to be `Nat`. We claim this is defensible behavior because the same happens if we do not use this elaborator.
```
have : (BEq.beq 0 1) = false := rfl
```
We can improve this failure in the future by applying default instances before reporting a type mismatch.
-/
let lhs ← withRef stx[2] <| toTree stx[2]
let rhs ← withRef stx[3] <| toTree stx[3]
let tree := Tree.op (lazy := false) stx .anonymous f lhs rhs

2
stage0/src/Lean/Elab/Inductive.lean generated
View file

@ -787,7 +787,7 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
for view in views do
Term.addTermInfo' view.ref[1] (← mkConstWithLevelParams view.declName) (isBinder := true)
for ctor in view.ctors do
Term.addTermInfo' ctor.ref[2] (← mkConstWithLevelParams ctor.declName) (isBinder := true)
Term.addTermInfo' ctor.ref[3] (← mkConstWithLevelParams ctor.declName) (isBinder := true)
-- We need to invoke `applyAttributes` because `class` is implemented as an attribute.
Term.applyAttributesAt view.declName view.modifiers.attrs .afterTypeChecking

5
stage0/src/Lean/Elab/InfoTree/Main.lean generated
View file

@ -4,12 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Data.Position
import Lean.Message
import Lean.Data.Json
import Lean.Meta.Basic
import Lean.Meta.PPGoal
import Lean.Elab.InfoTree.Types
namespace Lean.Elab

12
stage0/src/Lean/Elab/InfoTree/Types.lean generated
View file

@ -150,12 +150,12 @@ inductive Info where
`hole`s which are filled in later in the same way that unassigned metavariables are.
-/
inductive InfoTree where
| /-- The context object is created by `liftTermElabM` at `Command.lean` -/
context (i : ContextInfo) (t : InfoTree)
| /-- The children contain information for nested term elaboration and tactic evaluation -/
node (i : Info) (children : Std.PersistentArray InfoTree)
| /-- The elaborator creates holes (aka metavariables) for tactics and postponed terms -/
hole (mvarId : MVarId)
/-- The context object is created by `liftTermElabM` at `Command.lean` -/
| context (i : ContextInfo) (t : InfoTree)
/-- The children contain information for nested term elaboration and tactic evaluation -/
| node (i : Info) (children : Std.PersistentArray InfoTree)
/-- The elaborator creates holes (aka metavariables) for tactics and postponed terms -/
| hole (mvarId : MVarId)
deriving Inhabited
/-- This structure is the state that is being used to build an InfoTree object.

9
stage0/src/Lean/Elab/Match.lean generated
View file

@ -3,17 +3,14 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Util.CollectFVars
import Lean.Parser.Term
import Lean.Meta.Match.MatchPatternAttr
import Lean.Meta.Match.Match
import Lean.Meta.GeneralizeVars
import Lean.Meta.ForEachExpr
import Lean.Elab.SyntheticMVars
import Lean.Elab.Arg
import Lean.Elab.PatternVar
import Lean.Elab.AuxDiscr
import Lean.Elab.BindersUtil
import Lean.Elab.PatternVar
import Lean.Elab.Quotation.Precheck
import Lean.Elab.SyntheticMVars
namespace Lean.Elab.Term
open Meta

50
stage0/src/Lean/Elab/MutualDef.lean generated
View file

@ -11,7 +11,8 @@ import Lean.PrettyPrinter.Delaborator.Options
import Lean.Elab.Command
import Lean.Elab.Match
import Lean.Elab.DefView
import Lean.Elab.PreDefinition
import Lean.Elab.Deriving.Basic
import Lean.Elab.PreDefinition.Main
import Lean.Elab.DeclarationRange
namespace Lean.Elab
@ -719,53 +720,6 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
let newHeaders ← (process).run' 1
newHeaders.mapM fun header => return { header with type := (← instantiateMVars header.type) }
/-- Result for `mkInst?` -/
structure MkInstResult where
instVal : Expr
instType : Expr
outParams : Array Expr := #[]
/--
Construct an instance for `className out₁ ... outₙ type`.
The method support classes with a prefix of `outParam`s (e.g. `MonadReader`). -/
private partial def mkInst? (className : Name) (type : Expr) : MetaM (Option MkInstResult) := do
let rec go? (instType instTypeType : Expr) (outParams : Array Expr) : MetaM (Option MkInstResult) := do
let instTypeType ← whnfD instTypeType
unless instTypeType.isForall do
return none
let d := instTypeType.bindingDomain!
if d.isOutParam then
let mvar ← mkFreshExprMVar d
go? (mkApp instType mvar) (instTypeType.bindingBody!.instantiate1 mvar) (outParams.push mvar)
else
unless (← isDefEqGuarded (← inferType type) d) do
return none
let instType ← instantiateMVars (mkApp instType type)
let instVal ← synthInstance instType
return some { instVal, instType, outParams }
let instType ← mkConstWithFreshMVarLevels className
go? instType (← inferType instType) #[]
def processDefDeriving (className : Name) (declName : Name) : TermElabM Bool := do
try
let ConstantInfo.defnInfo info ← getConstInfo declName | return false
let some result ← mkInst? className info.value | return false
let instTypeNew := mkApp result.instType.appFn! (Lean.mkConst declName (info.levelParams.map mkLevelParam))
Meta.check instTypeNew
let instName ← liftMacroM <| mkUnusedBaseName (declName.appendBefore "inst" |>.appendAfter className.getString!)
addAndCompile <| Declaration.defnDecl {
name := instName
levelParams := info.levelParams
type := (← instantiateMVars instTypeNew)
value := (← instantiateMVars result.instVal)
hints := info.hints
safety := info.safety
}
addInstance instName AttributeKind.global (eval_prio default)
return true
catch _ =>
return false
/-- Remove auxiliary match discriminant let-declarations. -/
def eraseAuxDiscr (e : Expr) : CoreM Expr := do
Core.transform e fun e => do

4
stage0/src/Lean/Elab/PreDefinition/Basic.lean generated
View file

@ -3,11 +3,9 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Util.SCC
import Lean.Compiler.NoncomputableAttr
import Lean.Util.CollectLevelParams
import Lean.Meta.AbstractNestedProofs
import Lean.Meta.Transform
import Lean.Elab.Term
import Lean.Elab.RecAppSyntax
import Lean.Elab.DefView

4
stage0/src/Lean/Elab/PreDefinition/Main.lean generated
View file

@ -3,10 +3,12 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Util.SCC
import Lean.Elab.PreDefinition.Basic
import Lean.Elab.PreDefinition.Structural
import Lean.Elab.PreDefinition.WF
import Lean.Elab.PreDefinition.WF.Main
import Lean.Elab.PreDefinition.MkInhabitant
namespace Lean.Elab
open Meta
open Term

1
stage0/src/Lean/Elab/PreDefinition/WF/PackDomain.lean generated
View file

@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Tactic.Cases
import Lean.Elab.PreDefinition.Basic
namespace Lean.Elab.WF

1
stage0/src/Lean/Elab/PreDefinition/WF/PackMutual.lean generated
View file

@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Tactic.Cases
import Lean.Elab.PreDefinition.Basic
namespace Lean.Elab.WF

2
stage0/src/Lean/Elab/PreDefinition/WF/Rel.lean generated
View file

@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Tactic.Apply
import Lean.Meta.Tactic.Cases
import Lean.Meta.Tactic.Rename
import Lean.Meta.Tactic.Intro
import Lean.Elab.SyntheticMVars
import Lean.Elab.PreDefinition.Basic
import Lean.Elab.PreDefinition.WF.TerminationHint

52
stage0/src/Lean/Elab/Quotation.lean generated
View file

@ -10,7 +10,7 @@ import Lean.ResolveName
import Lean.Elab.Term
import Lean.Elab.Quotation.Util
import Lean.Elab.Quotation.Precheck
import Lean.Parser.Term
import Lean.Parser.Syntax
namespace Lean.Elab.Term.Quotation
open Lean.Parser.Term
@ -190,7 +190,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
def addNamedQuotInfo (stx : Syntax) (k : SyntaxNodeKind) : TermElabM SyntaxNodeKind := do
if stx.getNumArgs == 3 && stx[0].isAtom then
let s := stx[0].getAtomVal!
let s := stx[0].getAtomVal
if s.length > 3 then
if let (some l, some r) := (stx[0].getPos? true, stx[0].getTailPos? true) then
-- HACK: The atom is the string "`(foo|", so chop off the edges.
@ -276,35 +276,35 @@ private abbrev Alt := List Term × Term
alternative. This datatype describes what kind of check this involves, which helps other patterns decide if
they are covered by the same check and don't have to be checked again (see also `MatchResult`). -/
inductive HeadCheck where
| /-- match step that always succeeds: _, x, `($x), ... -/
unconditional
| /-- match step based on kind and, optionally, arity of discriminant
If `arity` is given, that number of new discriminants is introduced. `covered` patterns should then introduce the
same number of new patterns.
We actually check the arity at run time only in the case of `null` nodes since it should otherwise by implied by
the node kind.
without arity: `($x:k)
with arity: any quotation without an antiquotation head pattern -/
shape (k : List SyntaxNodeKind) (arity : Option Nat)
| /-- Match step that succeeds on `null` nodes of arity at least `numPrefix + numSuffix`, introducing discriminants
for the first `numPrefix` children, one `null` node for those in between, and for the `numSuffix` last children.
example: `([$x, $xs,*, $y]) is `slice 2 2` -/
slice (numPrefix numSuffix : Nat)
| /-- other, complicated match step that will probably only cover identical patterns
example: antiquotation splices `($[...]*) -/
other (pat : Syntax)
/-- match step that always succeeds: _, x, `($x), ... -/
| unconditional
/-- match step based on kind and, optionally, arity of discriminant
If `arity` is given, that number of new discriminants is introduced. `covered` patterns should then introduce the
same number of new patterns.
We actually check the arity at run time only in the case of `null` nodes since it should otherwise by implied by
the node kind.
without arity: `($x:k)
with arity: any quotation without an antiquotation head pattern -/
| shape (k : List SyntaxNodeKind) (arity : Option Nat)
/-- Match step that succeeds on `null` nodes of arity at least `numPrefix + numSuffix`, introducing discriminants
for the first `numPrefix` children, one `null` node for those in between, and for the `numSuffix` last children.
example: `([$x, $xs,*, $y]) is `slice 2 2` -/
| slice (numPrefix numSuffix : Nat)
/-- other, complicated match step that will probably only cover identical patterns
example: antiquotation splices `($[...]*) -/
| other (pat : Syntax)
open HeadCheck
/-- Describe whether a pattern is covered by a head check (induced by the pattern itself or a different pattern). -/
inductive MatchResult where
| /-- Pattern agrees with head check, remove and transform remaining alternative.
If `exhaustive` is `false`, *also* include unchanged alternative in the "no" branch. -/
covered (f : Alt → TermElabM Alt) (exhaustive : Bool)
| /-- Pattern disagrees with head check, include in "no" branch only -/
uncovered
| /-- Pattern is not quite sure yet; include unchanged in both branches -/
undecided
/-- Pattern agrees with head check, remove and transform remaining alternative.
If `exhaustive` is `false`, *also* include unchanged alternative in the "no" branch. -/
| covered (f : Alt → TermElabM Alt) (exhaustive : Bool)
/-- Pattern disagrees with head check, include in "no" branch only -/
| uncovered
/-- Pattern is not quite sure yet; include unchanged in both branches -/
| undecided
open MatchResult

6
stage0/src/Lean/Elab/StructInst.lean generated
View file

@ -248,8 +248,8 @@ def Field.isSimple {σ} : Field σ → Bool
| _ => false
inductive Struct where
| /-- Remark: the field `params` is use for default value propagation. It is initially empty, and then set at `elabStruct`. -/
mk (ref : Syntax) (structName : Name) (params : Array (Name × Expr)) (fields : List (Field Struct)) (source : Source)
/-- Remark: the field `params` is use for default value propagation. It is initially empty, and then set at `elabStruct`. -/
| mk (ref : Syntax) (structName : Name) (params : Array (Name × Expr)) (fields : List (Field Struct)) (source : Source)
deriving Inhabited
abbrev Fields := List (Field Struct)
@ -598,6 +598,8 @@ structure ElabStructResult where
private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : TermElabM ElabStructResult := withRef s.ref do
let env ← getEnv
let ctorVal := getStructureCtor env s.structName
if isPrivateNameFromImportedModule env ctorVal.name then
throwError "invalid \{...} notation, constructor for `{s.structName}` is marked as private"
-- We store the parameters at the resulting `Struct`. We use this information during default value propagation.
let { ctorFn, ctorFnType, params, .. } ← mkCtorHeader ctorVal expectedType?
let (e, _, fields, instMVars) ← s.fields.foldlM (init := (ctorFn, ctorFnType, [], #[])) fun (e, type, fields, instMVars) field => do

3
stage0/src/Lean/Elab/SyntheticMVars.lean generated
View file

@ -3,8 +3,9 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Meta.Tactic.Util
import Lean.Util.ForEachExpr
import Lean.Elab.Term
import Lean.Util.OccursCheck
import Lean.Elab.Tactic.Basic
namespace Lean.Elab.Term

13
stage0/src/Lean/Elab/Tactic/Basic.lean generated
View file

@ -3,18 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Util.CollectMVars
import Lean.Parser.Command
import Lean.Meta.PPGoal
import Lean.Meta.Tactic.Assumption
import Lean.Meta.Tactic.Contradiction
import Lean.Meta.Tactic.Intro
import Lean.Meta.Tactic.Clear
import Lean.Meta.Tactic.Revert
import Lean.Meta.Tactic.Subst
import Lean.Elab.Util
import Lean.Elab.Term
import Lean.Elab.Binders
namespace Lean.Elab
open Meta
@ -294,7 +283,7 @@ def adaptExpander (exp : Syntax → TacticM Syntax) : Tactic := fun stx => do
def appendGoals (mvarIds : List MVarId) : TacticM Unit :=
modify fun s => { s with goals := s.goals ++ mvarIds }
/-- Discard the first goal and replace it by the given list of goals,
/-- Discard the first goal and replace it by the given list of goals,
keeping the other goals. -/
def replaceMainGoal (mvarIds : List MVarId) : TacticM Unit := do
let (_ :: mvarIds') ← getGoals | throwNoGoalsToBeSolved

5
stage0/src/Lean/Elab/Tactic/BuiltinTactic.lean generated
View file

@ -3,7 +3,12 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Tactic.Assumption
import Lean.Meta.Tactic.Contradiction
import Lean.Meta.Tactic.Refl
import Lean.Elab.Binders
import Lean.Elab.Open
import Lean.Elab.SetOption
import Lean.Elab.Tactic.Basic
import Lean.Elab.Tactic.ElabTerm

3
stage0/src/Lean/Elab/Tactic/ElabTerm.lean generated
View file

@ -3,10 +3,9 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.CollectMVars
import Lean.Meta.Tactic.Apply
import Lean.Meta.Tactic.Constructor
import Lean.Meta.Tactic.Assert
import Lean.Meta.Tactic.Clear
import Lean.Meta.Tactic.Rename
import Lean.Elab.Tactic.Basic
import Lean.Elab.SyntheticMVars

10
stage0/src/Lean/Elab/Tactic/Location.lean generated
View file

@ -10,11 +10,11 @@ namespace Lean.Elab.Tactic
/-- Denotes a set of locations where a tactic should be applied for the main goal. See also `withLocation`. -/
inductive Location where
| /-- Apply the tactic everywhere. -/
wildcard
| /-- `hypotheses` are hypothesis names in the main goal that the tactic should be applied to.
If `type` is true, then the tactic should also be applied to the target type. -/
targets (hypotheses : Array Syntax) (type : Bool)
/-- Apply the tactic everywhere. -/
| wildcard
/-- `hypotheses` are hypothesis names in the main goal that the tactic should be applied to.
If `type` is true, then the tactic should also be applied to the target type. -/
| targets (hypotheses : Array Syntax) (type : Bool)
/-
Recall that

3
stage0/src/Lean/Elab/Tactic/Rewrite.lean generated
View file

@ -5,10 +5,9 @@ Authors: Leonardo de Moura
-/
import Lean.Meta.Tactic.Rewrite
import Lean.Meta.Tactic.Replace
import Lean.Elab.Tactic.Basic
import Lean.Elab.Tactic.ElabTerm
import Lean.Elab.Tactic.Location
import Lean.Elab.Tactic.Config
namespace Lean.Elab.Tactic
open Meta

54
stage0/src/Lean/Elab/Term.lean generated
View file

@ -3,25 +3,13 @@ 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
-/
import Lean.ResolveName
import Lean.Log
import Lean.Deprecated
import Lean.Util.Sorry
import Lean.Util.ReplaceExpr
import Lean.Structure
import Lean.Meta.AppBuilder
import Lean.Meta.CollectMVars
import Lean.Meta.Coe
import Lean.Hygiene
import Lean.Util.RecDepth
import Lean.Elab.Config
import Lean.Elab.Level
import Lean.Elab.Attributes
import Lean.Elab.AutoBound
import Lean.Elab.InfoTree
import Lean.Elab.Open
import Lean.Elab.SetOption
import Lean.Elab.DeclModifiers
namespace Lean.Elab
@ -39,18 +27,18 @@ structure SavedContext where
/-- We use synthetic metavariables as placeholders for pending elaboration steps. -/
inductive SyntheticMVarKind where
| /-- Use typeclass resolution to synthesize value for metavariable. -/
typeClass
| /--
Similar to `typeClass`, but error messages are different.
if `f?` is `some f`, we produce an application type mismatch error message.
Otherwise, if `header?` is `some header`, we generate the error `(header ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)`
Otherwise, we generate the error `("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` -/
coe (header? : Option String) (eNew : Expr) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr)
| /-- Use tactic to synthesize value for metavariable. -/
tactic (tacticCode : Syntax) (ctx : SavedContext)
| /-- Metavariable represents a hole whose elaboration has been postponed. -/
postponed (ctx : SavedContext)
/-- Use typeclass resolution to synthesize value for metavariable. -/
| typeClass
/--
Similar to `typeClass`, but error messages are different.
if `f?` is `some f`, we produce an application type mismatch error message.
Otherwise, if `header?` is `some header`, we generate the error `(header ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)`
Otherwise, we generate the error `("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` -/
| coe (header? : Option String) (eNew : Expr) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr)
/-- Use tactic to synthesize value for metavariable. -/
| tactic (tacticCode : Syntax) (ctx : SavedContext)
/-- Metavariable represents a hole whose elaboration has been postponed. -/
| postponed (ctx : SavedContext)
deriving Inhabited
instance : ToString SyntheticMVarKind where
@ -70,12 +58,12 @@ structure SyntheticMVarDecl where
We have three different kinds of error context.
-/
inductive MVarErrorKind where
| /-- Metavariable for implicit arguments. `ctx` is the parent application. -/
implicitArg (ctx : Expr)
| /-- Metavariable for explicit holes provided by the user (e.g., `_` and `?m`) -/
hole
| /-- "Custom", `msgData` stores the additional error messages. -/
custom (msgData : MessageData)
/-- Metavariable for implicit arguments. `ctx` is the parent application. -/
| implicitArg (ctx : Expr)
/-- Metavariable for explicit holes provided by the user (e.g., `_` and `?m`) -/
| hole
/-- "Custom", `msgData` stores the additional error messages. -/
| custom (msgData : MessageData)
deriving Inhabited
instance : ToString MVarErrorKind where
@ -378,9 +366,9 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl
-/
inductive LVal where
| fieldIdx (ref : Syntax) (i : Nat)
| /-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierachical/composite name.
`ref` is the syntax object representing the field. `targetStx` is the target object being accessed. -/
fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (targetStx : Syntax)
/-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierachical/composite name.
`ref` is the syntax object representing the field. `targetStx` is the target object being accessed. -/
| fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (targetStx : Syntax)
def LVal.getRef : LVal → Syntax
| .fieldIdx ref _ => ref

9
stage0/src/Lean/Elab/Util.lean generated
View file

@ -3,16 +3,9 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Util.Trace
import Lean.Parser.Syntax
import Lean.Parser.Extension
import Lean.Parser.Command
import Lean.KeyedDeclsAttribute
import Lean.Elab.Exception
import Lean.Elab.InfoTree
import Lean.DocString
import Lean.DeclarationRange
import Lean.Compiler.InitAttr
import Lean.Log
namespace Lean

14
stage0/src/Lean/Exception.lean generated
View file

@ -12,13 +12,13 @@ namespace Lean
/-- Exception type used in most Lean monads -/
inductive Exception where
| /-- Error messages that are displayed to users. `ref` is used to provide position information. -/
error (ref : Syntax) (msg : MessageData)
| /--
Internal exceptions that are not meant to be seen by users.
Examples: "pospone elaboration", "stuck at universe constraint", etc
-/
internal (id : InternalExceptionId) (extra : KVMap := {})
/-- Error messages that are displayed to users. `ref` is used to provide position information. -/
| error (ref : Syntax) (msg : MessageData)
/--
Internal exceptions that are not meant to be seen by users.
Examples: "pospone elaboration", "stuck at universe constraint", etc
-/
| internal (id : InternalExceptionId) (extra : KVMap := {})
/-- Convert exception into a structured message. -/
def Exception.toMessageData : Exception → MessageData

302
stage0/src/Lean/Expr.lean generated
View file

@ -10,10 +10,10 @@ namespace Lean
/-- Literal values for `Expr`. -/
inductive Literal where
| /-- Natural number literal -/
natVal (val : Nat)
| /-- String literal -/
strVal (val : String)
/-- Natural number literal -/
| natVal (val : Nat)
/-- String literal -/
| strVal (val : String)
deriving Inhabited, BEq, Repr
protected def Literal.hash : Literal → UInt64
@ -63,27 +63,27 @@ def bar ⦃x : Nat⦄ : Nat := x
See also the Lean manual: https://leanprover.github.io/lean4/doc/expressions.html#implicit-arguments
-/
inductive BinderInfo where
| /-- Default binder annotation, e.g. `(x : α)` -/
default
| /-- Implicit binder annotation, e.g., `{x : α}` -/
implicit
| /-- Strict implict binder annotation, e.g., `{{ x : α }}` -/
strictImplicit
| /-- Local instance binder annotataion, e.g., `[Decidable α]` -/
instImplicit
| /--
Auxiliary declarations used by Lean when elaborating recursive declarations.
When defining a function such as
```
def f : Nat → Nat
| 0 => 1
| x+1 => (x+1)*f x
```
Lean adds a local declaration `f : Nat → Nat` to the local context (`LocalContext`)
with `BinderInfo` set to `auxDecl`.
This local declaration is later removed by the termination checker.
-/
auxDecl
/-- Default binder annotation, e.g. `(x : α)` -/
| default
/-- Implicit binder annotation, e.g., `{x : α}` -/
| implicit
/-- Strict implict binder annotation, e.g., `{{ x : α }}` -/
| strictImplicit
/-- Local instance binder annotataion, e.g., `[Decidable α]` -/
| instImplicit
/--
Auxiliary declarations used by Lean when elaborating recursive declarations.
When defining a function such as
```
def f : Nat → Nat
| 0 => 1
| x+1 => (x+1)*f x
```
Lean adds a local declaration `f : Nat → Nat` to the local context (`LocalContext`)
with `BinderInfo` set to `auxDecl`.
This local declaration is later removed by the termination checker.
-/
| auxDecl
deriving Inhabited, BEq, Repr
def BinderInfo.hash : BinderInfo → UInt64
@ -298,134 +298,134 @@ contain metavariables.
Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use. -/
inductive Expr where
| /--
Bound variables. The natural number is the "de Bruijn" index
for the bound variable. See https://en.wikipedia.org/wiki/De_Bruijn_index for additional information.
Example, the expression `fun x : Nat => forall y : Nat, x = y`
```lean
.lam `x (.const `Nat [])
(.forall `y (.const `Nat [])
(.app (.app (.app (.const `Eq [.succ .zero])
(.const `Nat [])) (.bvar 1))
(.bvar 0))
.default)
.default
```
-/
bvar (deBruijnIndex : Nat)
| /--
Free variable. Lean uses the locally nameless approach.
See https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf for additional details.
When "visiting" the body of a binding expression (`lam`, `forallE`, or `letE`), bound variables
are converted into free variables using a unique identifier, and their user-facing name, type,
value (for `LetE`), and binder annotation are stored in the `LocalContext`.
-/
fvar (fvarId : FVarId)
| /--
Metavariables are used to represent "holes" in expressions, and goals in the
tactic framework. Metavariable declarations are stored in the `MetavarContext`.
Metavariables are used during elaboration, and are not allowed in the kernel,
or in the code generator.
-/
mvar (mvarId : MVarId)
| /--
`Type u`, `Sort u`, `Prop`. -
- `Prop` is represented as `.sort .zero`,
- `Sort u` as ``.sort (.param `u)``, and
- `Type u` as ``.sort (.succ (.param `u))``
-/
sort (u : Level)
| /--
A (universe polymorphic) constant. For example,
`@Eq.{1}` is represented as ``.const `Eq [.succ .zero]``, and
`@Array.map.{0, 0}` is represented as ``.cons `Array.map [.zero, .zero]``.
-/
const (declName : Name) (us : List Level)
| /--
Function application. `Nat.succ Nat.zero` is represented as
```
.app (.const `Nat.succ []) (.const .zero [])
```
-/
app (fn : Expr) (arg : Expr)
| /--
Lambda abstraction (aka anonymous functions).
- `fun x : Nat => x` is represented as
```
.lam `x (.const `Nat []) (.bvar 0) .default
```
-/
lam (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo)
| /--
A dependent arrow (aka forall-expression). It is also used to represent non-dependent arrows.
Examples:
- `forall x : Prop, x ∧ x` is represented as
```
.forallE `x
(.sort .zero)
(.app (.app (.const `And []) (.bvar 0)) (.bvar 0))
.default
```
- `Nat → Bool` as
```
.forallE `a (.const `Nat []) (.const `Bool []) .default
```
-/
forallE (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo)
| /--
Let-expressions. The field `nonDep` is not currently used, but will be used in the future
by the code generator (and possibly `simp`) to track whether a let-expression is non-dependent
or not.
/--
Bound variables. The natural number is the "de Bruijn" index
for the bound variable. See https://en.wikipedia.org/wiki/De_Bruijn_index for additional information.
Example, the expression `fun x : Nat => forall y : Nat, x = y`
```lean
.lam `x (.const `Nat [])
(.forall `y (.const `Nat [])
(.app (.app (.app (.const `Eq [.succ .zero])
(.const `Nat [])) (.bvar 1))
(.bvar 0))
.default)
.default
```
-/
| bvar (deBruijnIndex : Nat)
/--
Free variable. Lean uses the locally nameless approach.
See https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf for additional details.
When "visiting" the body of a binding expression (`lam`, `forallE`, or `letE`), bound variables
are converted into free variables using a unique identifier, and their user-facing name, type,
value (for `LetE`), and binder annotation are stored in the `LocalContext`.
-/
| fvar (fvarId : FVarId)
/--
Metavariables are used to represent "holes" in expressions, and goals in the
tactic framework. Metavariable declarations are stored in the `MetavarContext`.
Metavariables are used during elaboration, and are not allowed in the kernel,
or in the code generator.
-/
| mvar (mvarId : MVarId)
/--
`Type u`, `Sort u`, `Prop`. -
- `Prop` is represented as `.sort .zero`,
- `Sort u` as ``.sort (.param `u)``, and
- `Type u` as ``.sort (.succ (.param `u))``
-/
| sort (u : Level)
/--
A (universe polymorphic) constant. For example,
`@Eq.{1}` is represented as ``.const `Eq [.succ .zero]``, and
`@Array.map.{0, 0}` is represented as ``.cons `Array.map [.zero, .zero]``.
-/
| const (declName : Name) (us : List Level)
/--
Function application. `Nat.succ Nat.zero` is represented as
```
.app (.const `Nat.succ []) (.const .zero [])
```
-/
| app (fn : Expr) (arg : Expr)
/--
Lambda abstraction (aka anonymous functions).
- `fun x : Nat => x` is represented as
```
.lam `x (.const `Nat []) (.bvar 0) .default
```
-/
| lam (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo)
/--
A dependent arrow (aka forall-expression). It is also used to represent non-dependent arrows.
Examples:
- `forall x : Prop, x ∧ x` is represented as
```
.forallE `x
(.sort .zero)
(.app (.app (.const `And []) (.bvar 0)) (.bvar 0))
.default
```
- `Nat → Bool` as
```
.forallE `a (.const `Nat []) (.const `Bool []) .default
```
-/
| forallE (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo)
/--
Let-expressions. The field `nonDep` is not currently used, but will be used in the future
by the code generator (and possibly `simp`) to track whether a let-expression is non-dependent
or not.
**IMPORTANT**: This flag is for "local" use only. That is, a module should not "trust" its value for any purpose.
In the intended use-case, the compiler will set this flag, and be responsible for maintaining it.
Other modules may not preserve its value while applying transformations.
**IMPORTANT**: This flag is for "local" use only. That is, a module should not "trust" its value for any purpose.
In the intended use-case, the compiler will set this flag, and be responsible for maintaining it.
Other modules may not preserve its value while applying transformations.
Given an environment, metavariable context, and local context, we say a let-expression
`let x : t := v; e` is non-dependent when it is equivalent to `(fun x : t => e) v`.
Here is an example of a dependent let-expression
`let n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b` is type correct, but
`(fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2` is not.
The let-expression `let x : Nat := 2; Nat.succ x` is represented as
```
.letE `x (.const `Nat []) (.lit (.natVal 2)) (.bvar 0) true
```
-/
letE (declName : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool)
| /--
Natural number and string literal values. They are not really needed, but provide a more
compact representation in memory for these two kinds of literals, and are used to implement
efficient reduction in the elaborator and kernel.
The "raw" natural number `2` can be represented as `.lit (.natVal 2)`. Note that, it is
definitionally equal to
```
.app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
```
-/
lit : Literal → Expr
| /--
Metadata (aka annotations). We use annotations to provide hints to the pretty-printer,
store references to `Syntax` nodes, position information, and save information for
elaboration procedures (e.g., we use the `inaccessible` annotation during elaboration to
mark `Expr`s that correspond to inaccessible patterns).
Note that `.mdata data e` is definitionally equal to `e`.
-/
mdata (data : MData) (expr : Expr)
| /--
Projection-expressions. They are redundant, but are used to create more compact
terms, speedup reduction, and implement eta for structures.
The type of `struct` must be an structure-like inductive type. That is, it has only one
constructor, is not recursive, and it is not an inductive predicate. The kernel and elaborators
check whether the `typeName` matches the type of `struct`, and whether the (zero-based) index
is valid (i.e., it is smaller than the numbef of constructor fields).
When exporting Lean developments to other systems, `proj` can be replaced with `typeName`.`rec`
applications.
Example, given `a : Nat x Bool`, `a.1` is represented as
```
.proj `Prod 0 a
```
-/
proj (typeName : Name) (idx : Nat) (struct : Expr)
Given an environment, metavariable context, and local context, we say a let-expression
`let x : t := v; e` is non-dependent when it is equivalent to `(fun x : t => e) v`.
Here is an example of a dependent let-expression
`let n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b` is type correct, but
`(fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2` is not.
The let-expression `let x : Nat := 2; Nat.succ x` is represented as
```
.letE `x (.const `Nat []) (.lit (.natVal 2)) (.bvar 0) true
```
-/
| letE (declName : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool)
/--
Natural number and string literal values. They are not really needed, but provide a more
compact representation in memory for these two kinds of literals, and are used to implement
efficient reduction in the elaborator and kernel.
The "raw" natural number `2` can be represented as `.lit (.natVal 2)`. Note that, it is
definitionally equal to
```
.app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
```
-/
| lit : Literal → Expr
/--
Metadata (aka annotations). We use annotations to provide hints to the pretty-printer,
store references to `Syntax` nodes, position information, and save information for
elaboration procedures (e.g., we use the `inaccessible` annotation during elaboration to
mark `Expr`s that correspond to inaccessible patterns).
Note that `.mdata data e` is definitionally equal to `e`.
-/
| mdata (data : MData) (expr : Expr)
/--
Projection-expressions. They are redundant, but are used to create more compact
terms, speedup reduction, and implement eta for structures.
The type of `struct` must be an structure-like inductive type. That is, it has only one
constructor, is not recursive, and it is not an inductive predicate. The kernel and elaborators
check whether the `typeName` matches the type of `struct`, and whether the (zero-based) index
is valid (i.e., it is smaller than the numbef of constructor fields).
When exporting Lean developments to other systems, `proj` can be replaced with `typeName`.`rec`
applications.
Example, given `a : Nat x Bool`, `a.1` is represented as
```
.proj `Prod 0 a
```
-/
| proj (typeName : Name) (idx : Nat) (struct : Expr)
with
@[computedField, extern c inline "lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*))"]
data : @& Expr → Data

2
stage0/src/Lean/KeyedDeclsAttribute.lean generated
View file

@ -3,9 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Attributes
import Lean.Compiler.InitAttr
import Lean.ToExpr
import Lean.ScopedEnvExtension
import Lean.Compiler.IR.CompilerM

6
stage0/src/Lean/Linter/MissingDocs.lean generated
View file

@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Lean.Meta.Tactic.Simp.SimpTheorems
import Lean.Elab.SetOption
import Lean.Linter.Util
namespace Lean.Linter
@ -182,8 +184,8 @@ def checkNotation : SimpleHandler := fun stx => do
@[builtinMissingDocsHandler «mixfix»]
def checkMixfix : SimpleHandler := fun stx => do
if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
if stx[5].isNone then lint stx[3] stx[3][0].getAtomVal!
else lintNamed stx[5][0][3] stx[3][0].getAtomVal!
if stx[5].isNone then lint stx[3] stx[3][0].getAtomVal
else lintNamed stx[5][0][3] stx[3][0].getAtomVal
@[builtinMissingDocsHandler «syntax»]
def checkSyntax : SimpleHandler := fun stx => do

4
stage0/src/Lean/Linter/UnusedVariables.lean generated
View file

@ -1,9 +1,5 @@
import Lean.Elab.Command
import Lean.Linter.Util
import Lean.Elab.InfoTree
import Lean.Server.InfoUtils
import Lean.Server.References
import Lean.Data.HashMap
namespace Lean.Linter
open Lean.Elab.Command Lean.Server Std

1
stage0/src/Lean/Message.lean generated
View file

@ -7,7 +7,6 @@ Message Type used by the Lean frontend
-/
import Lean.Data.Position
import Lean.Data.OpenDecl
import Lean.Syntax
import Lean.MetavarContext
import Lean.Environment
import Lean.Util.PPExt

7
stage0/src/Lean/Meta/Basic.lean generated
View file

@ -7,17 +7,10 @@ import Lean.Data.LOption
import Lean.Environment
import Lean.Class
import Lean.ReducibilityAttrs
import Lean.Util.Trace
import Lean.Util.RecDepth
import Lean.Util.PPExt
import Lean.Util.ReplaceExpr
import Lean.Util.OccursCheck
import Lean.Util.MonadBacktrack
import Lean.Compiler.InlineAttrs
import Lean.Meta.TransparencyMode
import Lean.Meta.DiscrTreeTypes
import Lean.Eval
import Lean.CoreM
/-!
This module provides four (mutually dependent) goodies that are needed for building the elaborator and tactic frameworks.

44
stage0/src/Lean/Meta/CongrTheorems.lean generated
View file

@ -8,28 +8,28 @@ import Lean.Meta.AppBuilder
namespace Lean.Meta
inductive CongrArgKind where
| /-- It is a parameter for the congruence theorem, the parameter occurs in the left and right hand sides. -/
fixed
| /--
It is not a parameter for the congruence theorem, the theorem was specialized for this parameter.
This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it. -/
fixedNoParam
| /--
The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : a_i = b_i`.
`a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their equality. -/
eq
| /--
The congr-simp theorems contains only one parameter for this kind of argument, and congr theorems contains two.
They correspond to arguments that are subsingletons/propositions. -/
cast
| /--
The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : HEq a_i b_i`.
`a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their heterogeneous equality. -/
heq
| /--
For congr-simp theorems only. Indicates a decidable instance argument.
The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...] -/
subsingletonInst
/-- It is a parameter for the congruence theorem, the parameter occurs in the left and right hand sides. -/
| fixed
/--
It is not a parameter for the congruence theorem, the theorem was specialized for this parameter.
This only happens if the parameter is a subsingleton/proposition, and other parameters depend on it. -/
| fixedNoParam
/--
The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : a_i = b_i`.
`a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their equality. -/
| eq
/--
The congr-simp theorems contains only one parameter for this kind of argument, and congr theorems contains two.
They correspond to arguments that are subsingletons/propositions. -/
| cast
/--
The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : HEq a_i b_i`.
`a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their heterogeneous equality. -/
| heq
/--
For congr-simp theorems only. Indicates a decidable instance argument.
The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...] -/
| subsingletonInst
deriving Inhabited
structure CongrTheorem where

5
stage0/src/Lean/Meta/DiscrTree.lean generated
View file

@ -3,11 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Basic
import Lean.Meta.FunInfo
import Lean.Meta.InferType
import Lean.Meta.WHNF
import Lean.Meta.Match.MatcherInfo
import Lean.Meta.DiscrTreeTypes
namespace Lean.Meta.DiscrTree
/-!

74
stage0/src/Lean/Meta/ExprDefEq.lean generated
View file

@ -3,15 +3,9 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.ProjFns
import Lean.Structure
import Lean.Meta.WHNF
import Lean.Meta.InferType
import Lean.Meta.FunInfo
import Lean.Meta.Check
import Lean.Meta.Offset
import Lean.Meta.ForEachExpr
import Lean.Meta.UnificationHint
import Lean.Util.OccursCheck
namespace Lean.Meta
@ -143,39 +137,39 @@ private def trySynthPending (e : Expr) : MetaM Bool := do
Result type for `isDefEqArgsFirstPass`.
-/
inductive DefEqArgsFirstPassResult where
| /--
Failed to establish that explicit arguments are def-eq.
Remark: higher output parameters, and parameters that depend on them
are postponed.
-/
failed
| /--
Succeeded. The array `postponedImplicit` contains the position
of the implicit arguments for which def-eq has been postponed.
`postponedHO` contains the higher order output parameters, and parameters
that depend on them. They should be processed after the implict ones.
`postponedHO` is used to handle applications involving functions that
contain higher order output parameters. Example:
```lean
getElem :
{cont : Type u_1} → {idx : Type u_2} → {elem : Type u_3} →
{dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] →
(xs : cont) → (i : idx) → (h : dom xs i) → elem
```
The argumengs `dom` and `h` must be processed after all implicit arguments
otherwise higher-order unification problems are generated. See issue #1299,
when trying to solve
```
getElem ?a ?i ?h =?= getElem a i (Fin.val_lt_of_le i ...)
```
we have to solve the constraint
```
?dom a i.val =?= LT.lt i.val (Array.size a)
```
by solving after the instance has been synthesized, we reduce this constraint to
a simple check.
-/
ok (postponedImplicit : Array Nat) (postponedHO : Array Nat)
/--
Failed to establish that explicit arguments are def-eq.
Remark: higher output parameters, and parameters that depend on them
are postponed.
-/
| failed
/--
Succeeded. The array `postponedImplicit` contains the position
of the implicit arguments for which def-eq has been postponed.
`postponedHO` contains the higher order output parameters, and parameters
that depend on them. They should be processed after the implict ones.
`postponedHO` is used to handle applications involving functions that
contain higher order output parameters. Example:
```lean
getElem :
{cont : Type u_1} → {idx : Type u_2} → {elem : Type u_3} →
{dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] →
(xs : cont) → (i : idx) → (h : dom xs i) → elem
```
The argumengs `dom` and `h` must be processed after all implicit arguments
otherwise higher-order unification problems are generated. See issue #1299,
when trying to solve
```
getElem ?a ?i ?h =?= getElem a i (Fin.val_lt_of_le i ...)
```
we have to solve the constraint
```
?dom a i.val =?= LT.lt i.val (Array.size a)
```
by solving after the instance has been synthesized, we reduce this constraint to
a simple check.
-/
| ok (postponedImplicit : Array Nat) (postponedHO : Array Nat)
/--
First pass for `isDefEqArgs`. We unify explicit arguments, *and* easy cases

3
stage0/src/Lean/Meta/IndPredBelow.lean generated
View file

@ -5,10 +5,7 @@ Authors: Dany Fabian
-/
import Lean.Meta.Constructions
import Lean.Meta.Transform
import Lean.Meta.Tactic
import Lean.Meta.Match.Match
import Lean.Meta.Reduce
namespace Lean.Meta.IndPredBelow
open Match

6
stage0/src/Lean/Meta/Match/Match.lean generated
View file

@ -3,18 +3,12 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Util.CollectLevelParams
import Lean.Util.CollectFVars
import Lean.Util.Recognizers
import Lean.Compiler.ExternAttr
import Lean.Meta.Check
import Lean.Meta.Closure
import Lean.Meta.Tactic.Cases
import Lean.Meta.Tactic.Contradiction
import Lean.Meta.GeneralizeTelescope
import Lean.Meta.Match.Basic
import Lean.Meta.Match.MVarRenaming
import Lean.Meta.Match.CaseValues
namespace Lean.Meta.Match

1
stage0/src/Lean/Meta/PPGoal.lean generated
View file

@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
import Lean.Meta.InferType
import Lean.Meta.MatchUtil
namespace Lean.Meta

3
stage0/src/Lean/Meta/Tactic/AC/Main.lean generated
View file

@ -3,10 +3,9 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Dany Fabian
-/
import Init.Data.AC
import Lean.Meta.AppBuilder
import Lean.Meta.Tactic.Refl
import Lean.Elab.Tactic.Basic
import Lean.Meta.Tactic.Simp.Main
import Lean.Elab.Tactic.Rewrite
namespace Lean.Meta.AC

2
stage0/src/Lean/Meta/Tactic/Assert.lean generated
View file

@ -3,10 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Tactic.Util
import Lean.Meta.Tactic.FVarSubst
import Lean.Meta.Tactic.Intro
import Lean.Meta.Tactic.Revert
namespace Lean.Meta

1
stage0/src/Lean/Meta/Tactic/Congr.lean generated
View file

@ -6,6 +6,7 @@ Authors: Leonardo de Moura
import Lean.Meta.CongrTheorems
import Lean.Meta.Tactic.Assert
import Lean.Meta.Tactic.Apply
import Lean.Meta.Tactic.Clear
import Lean.Meta.Tactic.Refl
import Lean.Meta.Tactic.Assumption

4
stage0/src/Lean/Meta/Tactic/Simp/Main.lean generated
View file

@ -4,12 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Transform
import Lean.Meta.CongrTheorems
import Lean.Meta.Tactic.Replace
import Lean.Meta.Tactic.Util
import Lean.Meta.Tactic.Clear
import Lean.Meta.Tactic.UnifyEq
import Lean.Meta.Tactic.Simp.Types
import Lean.Meta.Tactic.Simp.Rewrite
namespace Lean.Meta

18
stage0/src/Lean/Meta/Transform.lean generated
View file

@ -8,15 +8,15 @@ import Lean.Meta.Basic
namespace Lean
inductive TransformStep where
| /-- Return expression without visiting any subexpressions. -/
done (e : Expr)
| /-- Visit expression (which should be different from current expression) instead. -/
visit (e : Expr)
| /--
Continue transformation with the given expression (defaults to current expression).
For `pre`, this means visiting the children of the expression.
For `post`, this is equivalent to returning `done`. -/
continue (e? : Option Expr := none)
/-- Return expression without visiting any subexpressions. -/
| done (e : Expr)
/-- Visit expression (which should be different from current expression) instead. -/
| visit (e : Expr)
/--
Continue transformation with the given expression (defaults to current expression).
For `pre`, this means visiting the children of the expression.
For `post`, this is equivalent to returning `done`. -/
| continue (e? : Option Expr := none)
namespace Core

4
stage0/src/Lean/Meta/WHNF.lean generated
View file

@ -3,12 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.ToExpr
import Lean.AuxRecursor
import Lean.ProjFns
import Lean.Structure
import Lean.Util.Recognizers
import Lean.Meta.Basic
import Lean.Meta.GetConst
import Lean.Meta.FunInfo
import Lean.Meta.Match.MatcherInfo

1
stage0/src/Lean/MonadEnv.lean generated
View file

@ -7,7 +7,6 @@ import Lean.Environment
import Lean.Exception
import Lean.Declaration
import Lean.Log
import Lean.Util.FindExpr
import Lean.AuxRecursor
import Lean.Compiler.Old

30
stage0/src/Lean/Parser/Basic.lean generated
View file

@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Data.Trie
import Lean.Data.Position
import Lean.Syntax
import Lean.Environment
import Lean.Message
/-!
@ -1582,20 +1580,20 @@ instance : Inhabited PrattParsingTables := ⟨{}⟩
function).
-/
inductive LeadingIdentBehavior where
| /-- `LeadingIdentBehavior.default`: if the leading token
is an identifier, then `prattParser` just executes the parsers
associated with the auxiliary token "ident". -/
default
| /-- `LeadingIdentBehavior.symbol`: if the leading token is
an identifier `<foo>`, and there are parsers `P` associated with
the toek `<foo>`, then it executes `P`. Otherwise, it executes
only the parsers associated with the auxiliary token "ident". -/
symbol
| /-- `LeadingIdentBehavior.both`: if the leading token
an identifier `<foo>`, the it executes the parsers associated
with token `<foo>` and parsers associated with the auxiliary
token "ident". -/
both
/-- `LeadingIdentBehavior.default`: if the leading token
is an identifier, then `prattParser` just executes the parsers
associated with the auxiliary token "ident". -/
| default
/-- `LeadingIdentBehavior.symbol`: if the leading token is
an identifier `<foo>`, and there are parsers `P` associated with
the toek `<foo>`, then it executes `P`. Otherwise, it executes
only the parsers associated with the auxiliary token "ident". -/
| symbol
/-- `LeadingIdentBehavior.both`: if the leading token
an identifier `<foo>`, the it executes the parsers associated
with token `<foo>` and parsers associated with the auxiliary
token "ident". -/
| both
deriving Inhabited, BEq, Repr
/--

7
stage0/src/Lean/Parser/Extension.lean generated
View file

@ -3,13 +3,10 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.ResolveName
import Lean.ScopedEnvExtension
import Lean.Parser.Basic
import Lean.Parser.StrInterpolation
import Lean.KeyedDeclsAttribute
import Lean.Compiler.InitAttr
import Lean.ScopedEnvExtension
import Lean.DocString
import Lean.DeclarationRange
/-! Extensible parsing via attributes -/

1
stage0/src/Lean/Parser/Syntax.lean generated
View file

@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Parser.Command
import Lean.Parser.Tactic
namespace Lean
namespace Parser

4
stage0/src/Lean/ParserCompiler.lean generated
View file

@ -3,10 +3,8 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
import Lean.Util.ReplaceExpr
import Lean.Meta.Basic
import Lean.Meta.ReduceEval
import Lean.Meta.WHNF
import Lean.KeyedDeclsAttribute
import Lean.ParserCompiler.Attribute
import Lean.Parser.Extension

1
stage0/src/Lean/PrettyPrinter/Basic.lean generated
View file

@ -3,7 +3,6 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
import Lean.InternalExceptionId
import Lean.KeyedDeclsAttribute
namespace Lean

5
stage0/src/Lean/PrettyPrinter/Delaborator/Basic.lean generated
View file

@ -3,11 +3,6 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
import Lean.KeyedDeclsAttribute
import Lean.ProjFns
import Lean.Syntax
import Lean.Meta.Transform
import Lean.Meta.Match.Match
import Lean.Elab.Term
import Lean.Elab.AuxDiscr
import Lean.PrettyPrinter.Delaborator.Options

27
stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean generated
View file

@ -550,9 +550,29 @@ def delabLam : Delab :=
| `(fun $binderGroups* => $stxBody) => `(fun $group $binderGroups* => $stxBody)
| _ => `(fun $group => $stxBody)
/--
Similar to `delabBinders`, but tracking whether `forallE` is dependent or not.
See issue #1571
-/
private partial def delabForallBinders (delabGroup : Array Syntax → Bool → Syntax → Delab) (curNames : Array Syntax := #[]) (curDep := false) : Delab := do
let dep := !(← getExpr).isArrow
if !curNames.isEmpty && dep != curDep then
-- don't group
delabGroup curNames curDep (← delab)
else
let curDep := dep
if ← shouldGroupWithNext then
-- group with nested binder => recurse immediately
withBindingBodyUnusedName fun stxN => delabForallBinders delabGroup (curNames.push stxN) curDep
else
-- don't group => delab body and prepend current binder group
let (stx, stxN) ← withBindingBodyUnusedName fun stxN => return (← delab, stxN)
delabGroup (curNames.push stxN) curDep stx
@[builtinDelab forallE]
def delabForall : Delab :=
delabBinders fun curNames stxBody => do
def delabForall : Delab := do
delabForallBinders fun curNames dependent stxBody => do
let e ← getExpr
let prop ← try isProp e catch _ => pure false
let stxT ← withBindingDomain delab
@ -562,9 +582,6 @@ def delabForall : Delab :=
-- here `curNames.size == 1`
| BinderInfo.instImplicit => `(bracketedBinderF|[$curNames.back : $stxT])
| _ =>
-- heuristic: use non-dependent arrows only if possible for whole group to avoid
-- noisy mix like `(α : Type) → Type → (γ : Type) → ...`.
let dependent := curNames.any fun n => hasIdent n.getId stxBody
-- NOTE: non-dependent arrows are available only for the default binder info
if dependent then
if prop && !(← getPPOption getPPPiBinderTypes) then

1
stage0/src/Lean/PrettyPrinter/Formatter.lean generated
View file

@ -5,6 +5,7 @@ Authors: Sebastian Ullrich
-/
import Lean.CoreM
import Lean.Parser.Extension
import Lean.Parser.StrInterpolation
import Lean.KeyedDeclsAttribute
import Lean.ParserCompiler.Attribute
import Lean.PrettyPrinter.Basic

3
stage0/src/Lean/PrettyPrinter/Parenthesizer.lean generated
View file

@ -3,9 +3,8 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
import Lean.CoreM
import Lean.KeyedDeclsAttribute
import Lean.Parser.Extension
import Lean.Parser.StrInterpolation
import Lean.ParserCompiler.Attribute
import Lean.PrettyPrinter.Basic

1
stage0/src/Lean/Server/FileWorker.lean generated
View file

@ -23,7 +23,6 @@ import Lean.Server.References
import Lean.Server.FileWorker.Utils
import Lean.Server.FileWorker.RequestHandling
import Lean.Server.FileWorker.WidgetRequests
import Lean.Server.Rpc.Basic
import Lean.Widget.InteractiveDiagnostic

1
stage0/src/Lean/Server/References.lean generated
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joscha Mennicken
-/
import Lean.Data.Lsp.Internal
import Lean.Server.Utils
/-! # Representing collected and deduplicated definitions and usages -/

8
stage0/src/Lean/Server/Utils.lean generated
View file

@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wojciech Nawrocki, Marc Huisinga
-/
import Lean.Data.Position
import Lean.Data.Lsp
import Lean.Data.Lsp.Communication
import Lean.Data.Lsp.Diagnostics
import Lean.Data.Lsp.Extra
import Lean.Data.Lsp.TextSync
import Lean.Server.InfoUtils
import Init.System.FilePath
import Lean.Parser.Basic
namespace IO

Some files were not shown because too many files have changed in this diff Show more