mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 10:24:07 +00:00
feat: non exponential codegen for reset-reuse (#12665)
This PR ports the expand reset/reuse pass from IR to LCNF. In addition it prevents exponential code generation unlike the old one. This results in a ~15% decrease in binary size and slight speedups across the board. The change also removes the "is this reset actually used" syntactic approximation as the previous passes guarantee (at the moment) that all uses are in the continuation and will thus be caught by this.
This commit is contained in:
Henrik Böving
@@ -32,6 +32,89 @@ unsafe axiom lcAny : Type
|
||||
/-- Internal representation of `Void` in the compiler. -/
|
||||
unsafe axiom lcVoid : Type
|
||||
|
||||
set_option bootstrap.inductiveCheckResultingUniverse false in
|
||||
/--
|
||||
The canonical universe-polymorphic type with just one element.
|
||||
|
||||
It should be used in contexts that require a type to be universe polymorphic, thus disallowing
|
||||
`Unit`.
|
||||
-/
|
||||
inductive PUnit : Sort u where
|
||||
/-- The only element of the universe-polymorphic unit type. -/
|
||||
| unit : PUnit
|
||||
|
||||
/--
|
||||
The equality relation. It has one introduction rule, `Eq.refl`.
|
||||
We use `a = b` as notation for `Eq a b`.
|
||||
A fundamental property of equality is that it is an equivalence relation.
|
||||
```
|
||||
variable (α : Type) (a b c d : α)
|
||||
variable (hab : a = b) (hcb : c = b) (hcd : c = d)
|
||||
|
||||
example : a = d :=
|
||||
Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
|
||||
```
|
||||
Equality is much more than an equivalence relation, however. It has the important property that every assertion
|
||||
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
|
||||
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
|
||||
Example:
|
||||
```
|
||||
example (α : Type) (a b : α) (p : α → Prop)
|
||||
(h1 : a = b) (h2 : p a) : p b :=
|
||||
Eq.subst h1 h2
|
||||
|
||||
example (α : Type) (a b : α) (p : α → Prop)
|
||||
(h1 : a = b) (h2 : p a) : p b :=
|
||||
h1 ▸ h2
|
||||
```
|
||||
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
|
||||
For more information: [Equality](https://lean-lang.org/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
|
||||
|
||||
|
||||
/-- 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 :=
|
||||
h.rec m
|
||||
|
||||
/--
|
||||
Heterogeneous equality. `a ≍ b` asserts that `a` and `b` have the same
|
||||
type, and casting `a` across the equality yields `b`, and vice versa.
|
||||
|
||||
You should avoid using this type if you can. Heterogeneous equality does not
|
||||
have all the same properties as `Eq`, because the assumption that the types of
|
||||
`a` and `b` are equal is often too weak to prove theorems of interest. One
|
||||
public important non-theorem is the analogue of `congr`: If `f ≍ g` and `x ≍ y`
|
||||
and `f x` and `g y` are well typed it does not follow that `f x ≍ g y`.
|
||||
(This does follow if you have `f = g` instead.) However if `a` and `b` have
|
||||
the same type then `a = b` and `a ≍ b` are equivalent.
|
||||
-/
|
||||
inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
|
||||
/-- Reflexivity of heterogeneous equality. -/
|
||||
| refl (a : α) : HEq a a
|
||||
|
||||
/--
|
||||
The Boolean values, `true` and `false`.
|
||||
|
||||
Logically speaking, this is equivalent to `Prop` (the type of propositions). The distinction is
|
||||
public important for programming: both propositions and their proofs are erased in the code generator,
|
||||
while `Bool` corresponds to the Boolean type in most programming languages and carries precisely one
|
||||
bit of run-time information.
|
||||
-/
|
||||
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
|
||||
|
||||
export Bool (false true)
|
||||
|
||||
/-- Compute whether `x` is a tagged pointer or not. -/
|
||||
@[extern "lean_is_scalar"]
|
||||
unsafe axiom isScalarObj {α : Type u} (x : α) : Bool
|
||||
|
||||
/--
|
||||
The identity function. `id` takes an implicit argument `α : Sort u`
|
||||
@@ -115,16 +198,7 @@ does.) Example:
|
||||
-/
|
||||
abbrev inferInstanceAs (α : Sort u) [i : α] : α := i
|
||||
|
||||
set_option bootstrap.inductiveCheckResultingUniverse false in
|
||||
/--
|
||||
The canonical universe-polymorphic type with just one element.
|
||||
|
||||
It should be used in contexts that require a type to be universe polymorphic, thus disallowing
|
||||
`Unit`.
|
||||
-/
|
||||
inductive PUnit : Sort u where
|
||||
/-- The only element of the universe-polymorphic unit type. -/
|
||||
| unit : PUnit
|
||||
|
||||
/--
|
||||
The canonical type with one element. This element is written `()`.
|
||||
@@ -245,42 +319,6 @@ For more information: [Propositional Logic](https://lean-lang.org/theorem_provin
|
||||
@[macro_inline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : Not a) : b :=
|
||||
(h₂ h₁).rec
|
||||
|
||||
/--
|
||||
The equality relation. It has one introduction rule, `Eq.refl`.
|
||||
We use `a = b` as notation for `Eq a b`.
|
||||
A fundamental property of equality is that it is an equivalence relation.
|
||||
```
|
||||
variable (α : Type) (a b c d : α)
|
||||
variable (hab : a = b) (hcb : c = b) (hcd : c = d)
|
||||
|
||||
example : a = d :=
|
||||
Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
|
||||
```
|
||||
Equality is much more than an equivalence relation, however. It has the important property that every assertion
|
||||
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
|
||||
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
|
||||
Example:
|
||||
```
|
||||
example (α : Type) (a b : α) (p : α → Prop)
|
||||
(h1 : a = b) (h2 : p a) : p b :=
|
||||
Eq.subst h1 h2
|
||||
|
||||
example (α : Type) (a b : α) (p : α → Prop)
|
||||
(h1 : a = b) (h2 : p a) : p b :=
|
||||
h1 ▸ h2
|
||||
```
|
||||
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
|
||||
For more information: [Equality](https://lean-lang.org/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
|
||||
|
||||
/-- 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 :=
|
||||
h.rec m
|
||||
|
||||
/--
|
||||
`rfl : a = a` is the unique constructor of the equality type. This is the
|
||||
same as `Eq.refl` except that it takes `a` implicitly instead of explicitly.
|
||||
@@ -477,21 +515,6 @@ Unsafe auxiliary constant used by the compiler to erase `Quot.lift`.
|
||||
-/
|
||||
unsafe axiom Quot.lcInv {α : Sort u} {r : α → α → Prop} (q : Quot r) : α
|
||||
|
||||
/--
|
||||
Heterogeneous equality. `a ≍ b` asserts that `a` and `b` have the same
|
||||
type, and casting `a` across the equality yields `b`, and vice versa.
|
||||
|
||||
You should avoid using this type if you can. Heterogeneous equality does not
|
||||
have all the same properties as `Eq`, because the assumption that the types of
|
||||
`a` and `b` are equal is often too weak to prove theorems of interest. One
|
||||
public important non-theorem is the analogue of `congr`: If `f ≍ g` and `x ≍ y`
|
||||
and `f x` and `g y` are well typed it does not follow that `f x ≍ g y`.
|
||||
(This does follow if you have `f = g` instead.) However if `a` and `b` have
|
||||
the same type then `a = b` and `a ≍ b` are equivalent.
|
||||
-/
|
||||
inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
|
||||
/-- Reflexivity of heterogeneous equality. -/
|
||||
| refl (a : α) : HEq a a
|
||||
|
||||
/-- A version of `HEq.refl` with an implicit argument. -/
|
||||
@[match_pattern] protected def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
|
||||
@@ -599,23 +622,6 @@ theorem Or.resolve_left (h: Or a b) (na : Not a) : b := h.elim (absurd · na) i
|
||||
theorem Or.resolve_right (h: Or a b) (nb : Not b) : a := h.elim id (absurd · nb)
|
||||
theorem Or.neg_resolve_left (h : Or (Not a) b) (ha : a) : b := h.elim (absurd ha) id
|
||||
theorem Or.neg_resolve_right (h : Or a (Not b)) (nb : b) : a := h.elim id (absurd nb)
|
||||
|
||||
/--
|
||||
The Boolean values, `true` and `false`.
|
||||
|
||||
Logically speaking, this is equivalent to `Prop` (the type of propositions). The distinction is
|
||||
public important for programming: both propositions and their proofs are erased in the code generator,
|
||||
while `Bool` corresponds to the Boolean type in most programming languages and carries precisely one
|
||||
bit of run-time information.
|
||||
-/
|
||||
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
|
||||
|
||||
export Bool (false true)
|
||||
|
||||
/--
|
||||
All the elements of a type that satisfy a predicate.
|
||||
|
||||
|
||||
@@ -10,10 +10,8 @@ public import Lean.Compiler.IR.AddExtern
|
||||
public import Lean.Compiler.IR.Basic
|
||||
public import Lean.Compiler.IR.Format
|
||||
public import Lean.Compiler.IR.CompilerM
|
||||
public import Lean.Compiler.IR.PushProj
|
||||
public import Lean.Compiler.IR.NormIds
|
||||
public import Lean.Compiler.IR.Checker
|
||||
public import Lean.Compiler.IR.ExpandResetReuse
|
||||
public import Lean.Compiler.IR.UnboxResult
|
||||
public import Lean.Compiler.IR.EmitC
|
||||
public import Lean.Compiler.IR.Sorry
|
||||
@@ -21,7 +19,6 @@ public import Lean.Compiler.IR.ToIR
|
||||
public import Lean.Compiler.IR.ToIRType
|
||||
public import Lean.Compiler.IR.Meta
|
||||
public import Lean.Compiler.IR.SimpleGroundExpr
|
||||
public import Lean.Compiler.IR.ElimDeadVars
|
||||
|
||||
-- The following imports are not required by the compiler. They are here to ensure that there
|
||||
-- are no orphaned modules.
|
||||
@@ -36,11 +33,6 @@ def compile (decls : Array Decl) : CompilerM (Array Decl) := do
|
||||
logDecls `init decls
|
||||
checkDecls decls
|
||||
let mut decls := decls
|
||||
if Compiler.LCNF.compiler.reuse.get (← getOptions) then
|
||||
decls := decls.map Decl.expandResetReuse
|
||||
logDecls `expand_reset_reuse decls
|
||||
decls := decls.map Decl.pushProj
|
||||
logDecls `push_proj decls
|
||||
decls ← updateSorryDep decls
|
||||
logDecls `result decls
|
||||
checkDecls decls
|
||||
|
||||
@@ -1,72 +0,0 @@
|
||||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
module
|
||||
|
||||
prelude
|
||||
public import Lean.Compiler.IR.FreeVars
|
||||
|
||||
public section
|
||||
|
||||
namespace Lean.IR
|
||||
|
||||
/--
|
||||
This function implements a simple heuristic for let values that we know may be dropped because they
|
||||
are pure.
|
||||
-/
|
||||
private def safeToElim (e : Expr) : Bool :=
|
||||
match e with
|
||||
| .ctor .. | .reset .. | .reuse .. | .proj .. | .uproj .. | .sproj .. | .box .. | .unbox ..
|
||||
| .lit .. | .isShared .. | .pap .. => true
|
||||
-- 0-ary full applications are considered constants
|
||||
| .fap _ args => args.isEmpty
|
||||
| .ap .. => false
|
||||
|
||||
partial def reshapeWithoutDead (bs : Array FnBody) (term : FnBody) : FnBody :=
|
||||
let rec reshape (bs : Array FnBody) (b : FnBody) (used : IndexSet) :=
|
||||
if bs.isEmpty then b
|
||||
else
|
||||
let curr := bs.back!
|
||||
let bs := bs.pop
|
||||
let keep (_ : Unit) :=
|
||||
let used := curr.collectFreeIndices used
|
||||
let b := curr.setBody b
|
||||
reshape bs b used
|
||||
let keepIfUsedJp (vidx : Index) :=
|
||||
if used.contains vidx then
|
||||
keep ()
|
||||
else
|
||||
reshape bs b used
|
||||
let keepIfUsedLet (vidx : Index) (val : Expr) :=
|
||||
if used.contains vidx || !safeToElim val then
|
||||
keep ()
|
||||
else
|
||||
reshape bs b used
|
||||
match curr with
|
||||
| FnBody.vdecl x _ e _ => keepIfUsedLet x.idx e
|
||||
-- TODO: we should keep all struct/union projections because they are used to ensure struct/union values are fully consumed.
|
||||
| FnBody.jdecl j _ _ _ => keepIfUsedJp j.idx
|
||||
| _ => keep ()
|
||||
reshape bs term term.freeIndices
|
||||
|
||||
partial def FnBody.elimDead (b : FnBody) : FnBody :=
|
||||
let (bs, term) := b.flatten
|
||||
let bs := modifyJPs bs elimDead
|
||||
let term := match term with
|
||||
| FnBody.case tid x xType alts =>
|
||||
let alts := alts.map fun alt => alt.modifyBody elimDead
|
||||
FnBody.case tid x xType alts
|
||||
| other => other
|
||||
reshapeWithoutDead bs term
|
||||
|
||||
/-- Eliminate dead let-declarations and join points -/
|
||||
def Decl.elimDead (d : Decl) : Decl :=
|
||||
match d with
|
||||
| .fdecl (body := b) .. => d.updateBody! b.elimDead
|
||||
| other => other
|
||||
|
||||
builtin_initialize registerTraceClass `compiler.ir.elim_dead (inherited := true)
|
||||
|
||||
end Lean.IR
|
||||
@@ -470,7 +470,7 @@ def emitDec (x : VarId) (n : Nat) (checkRef : Bool) : M Unit := do
|
||||
emitLn ");"
|
||||
|
||||
def emitDel (x : VarId) : M Unit := do
|
||||
emit "lean_free_object("; emit x; emitLn ");"
|
||||
emit "lean_del_object("; emit x; emitLn ");"
|
||||
|
||||
def emitSetTag (x : VarId) (i : Nat) : M Unit := do
|
||||
emit "lean_ctor_set_tag("; emit x; emit ", "; emit i; emitLn ");"
|
||||
|
||||
@@ -1081,7 +1081,7 @@ def emitSSet (builder : LLVM.Builder llvmctx) (x : VarId) (n : Nat) (offset : Na
|
||||
def emitDel (builder : LLVM.Builder llvmctx) (x : VarId) : M llvmctx Unit := do
|
||||
let argtys := #[ ← LLVM.voidPtrType llvmctx]
|
||||
let retty ← LLVM.voidType llvmctx
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty "lean_free_object" argtys
|
||||
let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty "lean_del_object" argtys
|
||||
let xv ← emitLhsVal builder x
|
||||
let fnty ← LLVM.functionType retty argtys
|
||||
let _ ← LLVM.buildCall2 builder fnty fn #[xv]
|
||||
|
||||
@@ -1,288 +0,0 @@
|
||||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
module
|
||||
|
||||
prelude
|
||||
public import Lean.Compiler.IR.CompilerM
|
||||
public import Lean.Compiler.IR.NormIds
|
||||
public import Lean.Compiler.IR.FreeVars
|
||||
import Init.Omega
|
||||
|
||||
public section
|
||||
|
||||
namespace Lean.IR.ExpandResetReuse
|
||||
/-- Mapping from variable to projections -/
|
||||
abbrev ProjMap := Std.HashMap VarId Expr
|
||||
namespace CollectProjMap
|
||||
abbrev Collector := ProjMap → ProjMap
|
||||
@[inline] def collectVDecl (x : VarId) (v : Expr) : Collector := fun m =>
|
||||
match v with
|
||||
| .proj .. => m.insert x v
|
||||
| .sproj .. => m.insert x v
|
||||
| .uproj .. => m.insert x v
|
||||
| _ => m
|
||||
|
||||
partial def collectFnBody : FnBody → Collector
|
||||
| .vdecl x _ v b => collectVDecl x v ∘ collectFnBody b
|
||||
| .jdecl _ _ v b => collectFnBody v ∘ collectFnBody b
|
||||
| .case _ _ _ alts => fun s => alts.foldl (fun s alt => collectFnBody alt.body s) s
|
||||
| e => if e.isTerminal then id else collectFnBody e.body
|
||||
end CollectProjMap
|
||||
|
||||
/-- Create a mapping from variables to projections.
|
||||
This function assumes variable ids have been normalized -/
|
||||
def mkProjMap (d : Decl) : ProjMap :=
|
||||
match d with
|
||||
| .fdecl (body := b) .. => CollectProjMap.collectFnBody b {}
|
||||
| _ => {}
|
||||
|
||||
structure Context where
|
||||
projMap : ProjMap
|
||||
|
||||
/-- Return true iff `x` is consumed in all branches of the current block.
|
||||
Here consumption means the block contains a `dec x` or `reuse x ...`. -/
|
||||
partial def consumed (x : VarId) : FnBody → Bool
|
||||
| .vdecl _ _ v b =>
|
||||
match v with
|
||||
| Expr.reuse y _ _ _ => x == y || consumed x b
|
||||
| _ => consumed x b
|
||||
| .dec y _ _ _ b => x == y || consumed x b
|
||||
| .case _ _ _ alts => alts.all fun alt => consumed x alt.body
|
||||
| e => !e.isTerminal && consumed x e.body
|
||||
|
||||
abbrev Mask := Array (Option VarId)
|
||||
|
||||
/-- Auxiliary function for eraseProjIncFor -/
|
||||
partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask :=
|
||||
let done (_ : Unit) := (bs ++ keep.reverse, mask)
|
||||
let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b)
|
||||
if h : bs.size < 2 then done ()
|
||||
else
|
||||
let b := bs.back!
|
||||
match b with
|
||||
| .vdecl _ _ (.sproj _ _ _) _ => keepInstr b
|
||||
| .vdecl _ _ (.uproj _ _) _ => keepInstr b
|
||||
| .inc z n c p _ =>
|
||||
if n == 0 then done () else
|
||||
let b' := bs[bs.size - 2]
|
||||
match b' with
|
||||
| .vdecl w _ (.proj i x) _ =>
|
||||
if w == z && y == x then
|
||||
/- Found
|
||||
```
|
||||
let z := proj[i] y
|
||||
inc z n c
|
||||
```
|
||||
We keep `proj`, and `inc` when `n > 1`
|
||||
-/
|
||||
let bs := bs.pop.pop
|
||||
let mask := mask.set! i (some z)
|
||||
let keep := keep.push b'
|
||||
let keep := if n == 1 then keep else keep.push (FnBody.inc z (n-1) c p FnBody.nil)
|
||||
eraseProjIncForAux y bs mask keep
|
||||
else done ()
|
||||
| _ => done ()
|
||||
| _ => done ()
|
||||
|
||||
/-- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`.
|
||||
Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/
|
||||
def eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask :=
|
||||
eraseProjIncForAux y bs (.replicate n none) #[]
|
||||
|
||||
/-- Replace `reuse x ctor ...` with `ctor ...`, and remove `dec x` -/
|
||||
partial def reuseToCtor (x : VarId) : FnBody → FnBody
|
||||
| FnBody.dec y n c p b =>
|
||||
if x == y then b -- n must be 1 since `x := reset ...`
|
||||
else FnBody.dec y n c p (reuseToCtor x b)
|
||||
| FnBody.vdecl z t v b =>
|
||||
match v with
|
||||
| Expr.reuse y c _ xs =>
|
||||
if x == y then FnBody.vdecl z t (Expr.ctor c xs) b
|
||||
else FnBody.vdecl z t v (reuseToCtor x b)
|
||||
| _ =>
|
||||
FnBody.vdecl z t v (reuseToCtor x b)
|
||||
| FnBody.case tid y yType alts =>
|
||||
let alts := alts.map fun alt => alt.modifyBody (reuseToCtor x)
|
||||
FnBody.case tid y yType alts
|
||||
| e =>
|
||||
if e.isTerminal then
|
||||
e
|
||||
else
|
||||
let (instr, b) := e.split
|
||||
let b := reuseToCtor x b
|
||||
instr.setBody b
|
||||
|
||||
/--
|
||||
replace
|
||||
```
|
||||
x := reset y; b
|
||||
```
|
||||
with
|
||||
```
|
||||
inc z_1; ...; inc z_i; dec y; b'
|
||||
```
|
||||
where `z_i`'s are the variables in `mask`,
|
||||
and `b'` is `b` where we removed `dec x` and replaced `reuse x ctor_i ...` with `ctor_i ...`.
|
||||
-/
|
||||
def mkSlowPath (x y : VarId) (mask : Mask) (b : FnBody) : FnBody :=
|
||||
let b := reuseToCtor x b
|
||||
let b := FnBody.dec y 1 true false b
|
||||
mask.foldl (init := b) fun b m => match m with
|
||||
| some z => FnBody.inc z 1 true false b
|
||||
| none => b
|
||||
|
||||
abbrev M := ReaderT Context (StateM Nat)
|
||||
def mkFresh : M VarId :=
|
||||
modifyGet fun n => ({ idx := n }, n + 1)
|
||||
|
||||
def releaseUnreadFields (y : VarId) (mask : Mask) (b : FnBody) : M FnBody :=
|
||||
mask.size.foldM (init := b) fun i _ b =>
|
||||
match mask[i] with
|
||||
| some _ => pure b -- code took ownership of this field
|
||||
| none => do
|
||||
let fld ← mkFresh
|
||||
pure (FnBody.vdecl fld .tobject (Expr.proj i y) (FnBody.dec fld 1 true false b))
|
||||
|
||||
def setFields (y : VarId) (zs : Array Arg) (b : FnBody) : FnBody :=
|
||||
zs.size.fold (init := b) fun i _ b => FnBody.set y i zs[i] b
|
||||
|
||||
/-- Given `set x[i] := y`, return true iff `y := proj[i] x` -/
|
||||
def isSelfSet (ctx : Context) (x : VarId) (i : Nat) (y : Arg) : Bool :=
|
||||
match y with
|
||||
| .var y =>
|
||||
match ctx.projMap[y]? with
|
||||
| some (Expr.proj j w) => j == i && w == x
|
||||
| _ => false
|
||||
| .erased => false
|
||||
|
||||
/-- Given `uset x[i] := y`, return true iff `y := uproj[i] x` -/
|
||||
def isSelfUSet (ctx : Context) (x : VarId) (i : Nat) (y : VarId) : Bool :=
|
||||
match ctx.projMap[y]? with
|
||||
| some (Expr.uproj j w) => j == i && w == x
|
||||
| _ => false
|
||||
|
||||
/-- Given `sset x[n, i] := y`, return true iff `y := sproj[n, i] x` -/
|
||||
def isSelfSSet (ctx : Context) (x : VarId) (n : Nat) (i : Nat) (y : VarId) : Bool :=
|
||||
match ctx.projMap[y]? with
|
||||
| some (Expr.sproj m j w) => n == m && j == i && w == x
|
||||
| _ => false
|
||||
|
||||
/-- Remove unnecessary `set/uset/sset` operations -/
|
||||
partial def removeSelfSet (ctx : Context) : FnBody → FnBody
|
||||
| FnBody.set x i y b =>
|
||||
if isSelfSet ctx x i y then removeSelfSet ctx b
|
||||
else FnBody.set x i y (removeSelfSet ctx b)
|
||||
| FnBody.uset x i y b =>
|
||||
if isSelfUSet ctx x i y then removeSelfSet ctx b
|
||||
else FnBody.uset x i y (removeSelfSet ctx b)
|
||||
| FnBody.sset x n i y t b =>
|
||||
if isSelfSSet ctx x n i y then removeSelfSet ctx b
|
||||
else FnBody.sset x n i y t (removeSelfSet ctx b)
|
||||
| FnBody.case tid y yType alts =>
|
||||
let alts := alts.map fun alt => alt.modifyBody (removeSelfSet ctx)
|
||||
FnBody.case tid y yType alts
|
||||
| e =>
|
||||
if e.isTerminal then e
|
||||
else
|
||||
let (instr, b) := e.split
|
||||
let b := removeSelfSet ctx b
|
||||
instr.setBody b
|
||||
|
||||
partial def reuseToSet (ctx : Context) (x y : VarId) : FnBody → FnBody
|
||||
| FnBody.dec z n c p b =>
|
||||
if x == z then FnBody.del y b
|
||||
else FnBody.dec z n c p (reuseToSet ctx x y b)
|
||||
| FnBody.vdecl z t v b =>
|
||||
match v with
|
||||
| Expr.reuse w c u zs =>
|
||||
if x == w then
|
||||
let b := setFields y zs (b.replaceVar z y)
|
||||
let b := if u then FnBody.setTag y c.cidx b else b
|
||||
removeSelfSet ctx b
|
||||
else FnBody.vdecl z t v (reuseToSet ctx x y b)
|
||||
| _ => FnBody.vdecl z t v (reuseToSet ctx x y b)
|
||||
| FnBody.case tid z zType alts =>
|
||||
let alts := alts.map fun alt => alt.modifyBody (reuseToSet ctx x y)
|
||||
FnBody.case tid z zType alts
|
||||
| e =>
|
||||
if e.isTerminal then e
|
||||
else
|
||||
let (instr, b) := e.split
|
||||
let b := reuseToSet ctx x y b
|
||||
instr.setBody b
|
||||
|
||||
/--
|
||||
replace
|
||||
```
|
||||
x := reset y; b
|
||||
```
|
||||
with
|
||||
```
|
||||
let f_i_1 := proj[i_1] y;
|
||||
...
|
||||
let f_i_k := proj[i_k] y;
|
||||
b'
|
||||
```
|
||||
where `i_j`s are the field indexes
|
||||
that the code did not touch immediately before the reset.
|
||||
That is `mask[j] == none`.
|
||||
`b'` is `b` where `y` `dec x` is replaced with `del y`,
|
||||
and `z := reuse x ctor_i ws; F` is replaced with
|
||||
`set x i ws[i]` operations, and we replace `z` with `x` in `F`
|
||||
-/
|
||||
def mkFastPath (x y : VarId) (mask : Mask) (b : FnBody) : M FnBody := do
|
||||
let ctx ← read
|
||||
let b := reuseToSet ctx x y b
|
||||
releaseUnreadFields y mask b
|
||||
|
||||
-- Expand `bs; x := reset[n] y; b`
|
||||
partial def expand (mainFn : FnBody → Array FnBody → M FnBody)
|
||||
(bs : Array FnBody) (x : VarId) (n : Nat) (y : VarId) (b : FnBody) : M FnBody := do
|
||||
let (bs, mask) := eraseProjIncFor n y bs
|
||||
/- Remark: we may be duplicating variable/JP indices. That is, `bSlow` and `bFast` may
|
||||
have duplicate indices. We run `normalizeIds` to fix the ids after we have expand them. -/
|
||||
let bSlow := mkSlowPath x y mask b
|
||||
let bFast ← mkFastPath x y mask b
|
||||
/- We only optimize recursively the fast. -/
|
||||
let bFast ← mainFn bFast #[]
|
||||
let c ← mkFresh
|
||||
let b := FnBody.vdecl c IRType.uint8 (Expr.isShared y) (mkIf c bSlow bFast)
|
||||
return reshape bs b
|
||||
|
||||
partial def searchAndExpand : FnBody → Array FnBody → M FnBody
|
||||
| d@(FnBody.vdecl x _ (Expr.reset n y) b), bs =>
|
||||
if consumed x b then do
|
||||
expand searchAndExpand bs x n y b
|
||||
else
|
||||
searchAndExpand b (push bs d)
|
||||
| FnBody.jdecl j xs v b, bs => do
|
||||
let v ← searchAndExpand v #[]
|
||||
searchAndExpand b (push bs (FnBody.jdecl j xs v FnBody.nil))
|
||||
| FnBody.case tid x xType alts, bs => do
|
||||
let alts ← alts.mapM fun alt => alt.modifyBodyM fun b => searchAndExpand b #[]
|
||||
return reshape bs (FnBody.case tid x xType alts)
|
||||
| b, bs =>
|
||||
if b.isTerminal then return reshape bs b
|
||||
else searchAndExpand b.body (push bs b)
|
||||
|
||||
def main (d : Decl) : Decl :=
|
||||
match d with
|
||||
| .fdecl (body := b) .. =>
|
||||
let m := mkProjMap d
|
||||
let nextIdx := d.maxIndex + 1
|
||||
let bNew := (searchAndExpand b #[] { projMap := m }).run' nextIdx
|
||||
d.updateBody! bNew
|
||||
| d => d
|
||||
|
||||
end ExpandResetReuse
|
||||
|
||||
/-- (Try to) expand `reset` and `reuse` instructions. -/
|
||||
def Decl.expandResetReuse (d : Decl) : Decl :=
|
||||
(ExpandResetReuse.main d).normalizeIds
|
||||
|
||||
builtin_initialize registerTraceClass `compiler.ir.expand_reset_reuse (inherited := true)
|
||||
|
||||
end Lean.IR
|
||||
@@ -1,245 +0,0 @@
|
||||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
module
|
||||
|
||||
prelude
|
||||
public import Lean.Compiler.IR.Basic
|
||||
|
||||
public section
|
||||
|
||||
namespace Lean.IR
|
||||
|
||||
namespace MaxIndex
|
||||
/-! Compute the maximum index `M` used in a declaration.
|
||||
We `M` to initialize the fresh index generator used to create fresh
|
||||
variable and join point names.
|
||||
|
||||
Recall that we variable and join points share the same namespace in
|
||||
our implementation.
|
||||
-/
|
||||
|
||||
structure State where
|
||||
currentMax : Nat := 0
|
||||
|
||||
abbrev M := StateM State
|
||||
|
||||
private def visitIndex (x : Index) : M Unit := do
|
||||
modify fun s => { s with currentMax := s.currentMax.max x }
|
||||
|
||||
private def visitVar (x : VarId) : M Unit :=
|
||||
visitIndex x.idx
|
||||
|
||||
private def visitJP (j : JoinPointId) : M Unit :=
|
||||
visitIndex j.idx
|
||||
|
||||
private def visitArg (arg : Arg) : M Unit :=
|
||||
match arg with
|
||||
| .var x => visitVar x
|
||||
| .erased => pure ()
|
||||
|
||||
private def visitParam (p : Param) : M Unit :=
|
||||
visitVar p.x
|
||||
|
||||
private def visitExpr (e : Expr) : M Unit := do
|
||||
match e with
|
||||
| .proj _ x | .uproj _ x | .sproj _ _ x | .box _ x | .unbox x | .reset _ x | .isShared x =>
|
||||
visitVar x
|
||||
| .ctor _ ys | .fap _ ys | .pap _ ys =>
|
||||
ys.forM visitArg
|
||||
| .ap x ys | .reuse x _ _ ys =>
|
||||
visitVar x
|
||||
ys.forM visitArg
|
||||
| .lit _ => pure ()
|
||||
|
||||
partial def visitFnBody (fnBody : FnBody) : M Unit := do
|
||||
match fnBody with
|
||||
| .vdecl x _ v b =>
|
||||
visitVar x
|
||||
visitExpr v
|
||||
visitFnBody b
|
||||
| .jdecl j ys v b =>
|
||||
visitJP j
|
||||
visitFnBody v
|
||||
ys.forM visitParam
|
||||
visitFnBody b
|
||||
| .set x _ y b =>
|
||||
visitVar x
|
||||
visitArg y
|
||||
visitFnBody b
|
||||
| .uset x _ y b | .sset x _ _ y _ b =>
|
||||
visitVar x
|
||||
visitVar y
|
||||
visitFnBody b
|
||||
| .setTag x _ b | .inc x _ _ _ b | .dec x _ _ _ b | .del x b =>
|
||||
visitVar x
|
||||
visitFnBody b
|
||||
| .case _ x _ alts =>
|
||||
visitVar x
|
||||
alts.forM (visitFnBody ·.body)
|
||||
| .jmp j ys =>
|
||||
visitJP j
|
||||
ys.forM visitArg
|
||||
| .ret x =>
|
||||
visitArg x
|
||||
| .unreachable => pure ()
|
||||
|
||||
private def visitDecl (decl : Decl) : M Unit := do
|
||||
match decl with
|
||||
| .fdecl (xs := xs) (body := b) .. =>
|
||||
xs.forM visitParam
|
||||
visitFnBody b
|
||||
| .extern (xs := xs) .. =>
|
||||
xs.forM visitParam
|
||||
|
||||
end MaxIndex
|
||||
|
||||
def FnBody.maxIndex (b : FnBody) : Index := Id.run do
|
||||
let ⟨_, { currentMax }⟩ := MaxIndex.visitFnBody b |>.run {}
|
||||
return currentMax
|
||||
|
||||
def Decl.maxIndex (d : Decl) : Index := Id.run do
|
||||
let ⟨_, { currentMax }⟩ := MaxIndex.visitDecl d |>.run {}
|
||||
return currentMax
|
||||
|
||||
namespace FreeIndices
|
||||
/-! We say a variable (join point) index (aka name) is free in a function body
|
||||
if there isn't a `FnBody.vdecl` (`Fnbody.jdecl`) binding it. -/
|
||||
|
||||
structure State where
|
||||
freeIndices : IndexSet := {}
|
||||
|
||||
abbrev M := StateM State
|
||||
|
||||
private def visitIndex (x : Index) : M Unit := do
|
||||
modify fun s => { s with freeIndices := s.freeIndices.insert x }
|
||||
|
||||
private def visitVar (x : VarId) : M Unit :=
|
||||
visitIndex x.idx
|
||||
|
||||
private def visitJP (j : JoinPointId) : M Unit :=
|
||||
visitIndex j.idx
|
||||
|
||||
private def visitArg (arg : Arg) : M Unit :=
|
||||
match arg with
|
||||
| .var x => visitVar x
|
||||
| .erased => pure ()
|
||||
|
||||
private def visitParam (p : Param) : M Unit :=
|
||||
visitVar p.x
|
||||
|
||||
private def visitExpr (e : Expr) : M Unit := do
|
||||
match e with
|
||||
| .proj _ x | .uproj _ x | .sproj _ _ x | .box _ x | .unbox x | .reset _ x | .isShared x =>
|
||||
visitVar x
|
||||
| .ctor _ ys | .fap _ ys | .pap _ ys =>
|
||||
ys.forM visitArg
|
||||
| .ap x ys | .reuse x _ _ ys =>
|
||||
visitVar x
|
||||
ys.forM visitArg
|
||||
| .lit _ => pure ()
|
||||
|
||||
partial def visitFnBody (fnBody : FnBody) : M Unit := do
|
||||
match fnBody with
|
||||
| .vdecl x _ v b =>
|
||||
visitVar x
|
||||
visitExpr v
|
||||
visitFnBody b
|
||||
| .jdecl j ys v b =>
|
||||
visitJP j
|
||||
visitFnBody v
|
||||
ys.forM visitParam
|
||||
visitFnBody b
|
||||
| .set x _ y b =>
|
||||
visitVar x
|
||||
visitArg y
|
||||
visitFnBody b
|
||||
| .uset x _ y b | .sset x _ _ y _ b =>
|
||||
visitVar x
|
||||
visitVar y
|
||||
visitFnBody b
|
||||
| .setTag x _ b | .inc x _ _ _ b | .dec x _ _ _ b | .del x b =>
|
||||
visitVar x
|
||||
visitFnBody b
|
||||
| .case _ x _ alts =>
|
||||
visitVar x
|
||||
alts.forM (visitFnBody ·.body)
|
||||
| .jmp j ys =>
|
||||
visitJP j
|
||||
ys.forM visitArg
|
||||
| .ret x =>
|
||||
visitArg x
|
||||
| .unreachable => pure ()
|
||||
|
||||
private def visitDecl (decl : Decl) : M Unit := do
|
||||
match decl with
|
||||
| .fdecl (xs := xs) (body := b) .. =>
|
||||
xs.forM visitParam
|
||||
visitFnBody b
|
||||
| .extern (xs := xs) .. =>
|
||||
xs.forM visitParam
|
||||
|
||||
end FreeIndices
|
||||
|
||||
def FnBody.collectFreeIndices (b : FnBody) (init : IndexSet) : IndexSet := Id.run do
|
||||
let ⟨_, { freeIndices }⟩ := FreeIndices.visitFnBody b |>.run { freeIndices := init }
|
||||
return freeIndices
|
||||
|
||||
def FnBody.freeIndices (b : FnBody) : IndexSet :=
|
||||
b.collectFreeIndices {}
|
||||
|
||||
namespace HasIndex
|
||||
/-! In principle, we can check whether a function body `b` contains an index `i` using
|
||||
`b.freeIndices.contains i`, but it is more efficient to avoid the construction
|
||||
of the set of freeIndices and just search whether `i` occurs in `b` or not.
|
||||
-/
|
||||
def visitVar (w : Index) (x : VarId) : Bool := w == x.idx
|
||||
def visitJP (w : Index) (x : JoinPointId) : Bool := w == x.idx
|
||||
|
||||
def visitArg (w : Index) : Arg → Bool
|
||||
| .var x => visitVar w x
|
||||
| .erased => false
|
||||
|
||||
def visitArgs (w : Index) (xs : Array Arg) : Bool :=
|
||||
xs.any (visitArg w)
|
||||
|
||||
def visitParams (w : Index) (ps : Array Param) : Bool :=
|
||||
ps.any (fun p => w == p.x.idx)
|
||||
|
||||
def visitExpr (w : Index) : Expr → Bool
|
||||
| .proj _ x | .uproj _ x | .sproj _ _ x | .box _ x | .unbox x | .reset _ x | .isShared x =>
|
||||
visitVar w x
|
||||
| .ctor _ ys | .fap _ ys | .pap _ ys =>
|
||||
visitArgs w ys
|
||||
| .ap x ys | .reuse x _ _ ys =>
|
||||
visitVar w x || visitArgs w ys
|
||||
| .lit _ => false
|
||||
|
||||
partial def visitFnBody (w : Index) : FnBody → Bool
|
||||
| .vdecl _ _ v b =>
|
||||
visitExpr w v || visitFnBody w b
|
||||
| .jdecl _ _ v b =>
|
||||
visitFnBody w v || visitFnBody w b
|
||||
| FnBody.set x _ y b =>
|
||||
visitVar w x || visitArg w y || visitFnBody w b
|
||||
| .uset x _ y b | .sset x _ _ y _ b =>
|
||||
visitVar w x || visitVar w y || visitFnBody w b
|
||||
| .setTag x _ b | .inc x _ _ _ b | .dec x _ _ _ b | .del x b =>
|
||||
visitVar w x || visitFnBody w b
|
||||
| .case _ x _ alts =>
|
||||
visitVar w x || alts.any (fun alt => visitFnBody w alt.body)
|
||||
| .jmp j ys =>
|
||||
visitJP w j || visitArgs w ys
|
||||
| .ret x =>
|
||||
visitArg w x
|
||||
| .unreachable => false
|
||||
|
||||
end HasIndex
|
||||
|
||||
def Arg.hasFreeVar (arg : Arg) (x : VarId) : Bool := HasIndex.visitArg x.idx arg
|
||||
def Expr.hasFreeVar (e : Expr) (x : VarId) : Bool := HasIndex.visitExpr x.idx e
|
||||
def FnBody.hasFreeVar (b : FnBody) (x : VarId) : Bool := HasIndex.visitFnBody x.idx b
|
||||
|
||||
end Lean.IR
|
||||
@@ -1,62 +0,0 @@
|
||||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
module
|
||||
|
||||
prelude
|
||||
public import Lean.Compiler.IR.FreeVars
|
||||
public import Lean.Compiler.IR.NormIds
|
||||
|
||||
public section
|
||||
|
||||
namespace Lean.IR
|
||||
|
||||
partial def pushProjs (bs : Array FnBody) (alts : Array Alt) (altsF : Array IndexSet) (ctx : Array FnBody) (ctxF : IndexSet) : Array FnBody × Array Alt :=
|
||||
if bs.isEmpty then (ctx.reverse, alts)
|
||||
else
|
||||
let b := bs.back!
|
||||
let bs := bs.pop
|
||||
let done (_ : Unit) := (bs.push b ++ ctx.reverse, alts)
|
||||
let skip (_ : Unit) := pushProjs bs alts altsF (ctx.push b) (b.collectFreeIndices ctxF)
|
||||
let push (x : VarId) :=
|
||||
if !ctxF.contains x.idx then
|
||||
let alts := alts.mapIdx fun i alt => alt.modifyBody fun b' =>
|
||||
if altsF[i]!.contains x.idx then b.setBody b'
|
||||
else b'
|
||||
let altsF := altsF.map fun s => if s.contains x.idx then b.collectFreeIndices s else s
|
||||
pushProjs bs alts altsF ctx ctxF
|
||||
else
|
||||
skip ()
|
||||
match b with
|
||||
| FnBody.vdecl x _ v _ =>
|
||||
match v with
|
||||
| Expr.proj _ _ => push x
|
||||
| Expr.uproj _ _ => push x
|
||||
| Expr.sproj _ _ _ => push x
|
||||
| Expr.isShared _ => skip ()
|
||||
| _ => done ()
|
||||
| _ => done ()
|
||||
|
||||
partial def FnBody.pushProj (b : FnBody) : FnBody :=
|
||||
let (bs, term) := b.flatten
|
||||
let bs := modifyJPs bs pushProj
|
||||
match term with
|
||||
| .case tid x xType alts =>
|
||||
let altsF := alts.map fun alt => alt.body.freeIndices
|
||||
let (bs, alts) := pushProjs bs alts altsF #[] (mkIndexSet x.idx)
|
||||
let alts := alts.map fun alt => alt.modifyBody pushProj
|
||||
let term := FnBody.case tid x xType alts
|
||||
reshape bs term
|
||||
| _ => reshape bs term
|
||||
|
||||
/-- Push projections inside `case` branches. -/
|
||||
def Decl.pushProj (d : Decl) : Decl :=
|
||||
match d with
|
||||
| .fdecl (body := b) .. => d.updateBody! b.pushProj |>.normalizeIds
|
||||
| other => other
|
||||
|
||||
builtin_initialize registerTraceClass `compiler.ir.push_proj (inherited := true)
|
||||
|
||||
end Lean.IR
|
||||
369
src/Lean/Compiler/LCNF/ExpandResetReuse.lean
Normal file
369
src/Lean/Compiler/LCNF/ExpandResetReuse.lean
Normal file
@@ -0,0 +1,369 @@
|
||||
/-
|
||||
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Henrik Böving
|
||||
-/
|
||||
module
|
||||
|
||||
prelude
|
||||
public import Lean.Compiler.LCNF.PassManager
|
||||
import Init.While
|
||||
|
||||
/-!
|
||||
This pass expands pairs of reset-reuse instructions into explicit hot and cold paths. We do this on
|
||||
the LCNF level rather than letting the backend do it because we can apply domain specific
|
||||
optimizations at this point in time.
|
||||
|
||||
Whenever we encounter a `let token := reset nfields orig; k`, we create code of the shape (not
|
||||
showing reference counting instructions):
|
||||
```
|
||||
jp resetjp token isShared :=
|
||||
k
|
||||
cases isShared orig with
|
||||
| false -> jmp resetjp orig true
|
||||
| true -> jmp resetjp box(0) false
|
||||
```
|
||||
Then within the join point body `k` we turn `dec` instructions on `token` into `del` and expand
|
||||
`let final := reuse token arg; k'` into another join point:
|
||||
```
|
||||
jp reusejp final :=
|
||||
k'
|
||||
cases isShared with
|
||||
| false -> jmp reusejp token
|
||||
| true ->
|
||||
let x := alloc args
|
||||
jmp reusejp x
|
||||
```
|
||||
|
||||
In addition to this we perform optimizations specific to the hot path for both the `resetjp` and
|
||||
`reusejp`. For the former, we will frequently encounter the pattern:
|
||||
```
|
||||
let x_0 = proj[0] orig
|
||||
inc x_0
|
||||
...
|
||||
let x_i = proj[i] orig
|
||||
inc x_i
|
||||
let token := reset nfields orig
|
||||
```
|
||||
On the hot path we do not free `orig`, thus there is no need to increment the reference counts of
|
||||
the projections because the reference coming from `orig` will keep all of the projections alive
|
||||
naturally (a form of "dynamic derived borrows" if you wish). On the cold path the reference counts
|
||||
still have to happen though.
|
||||
|
||||
For `resetjp` we frequently encounter the pattern:
|
||||
```
|
||||
let final := reuse token args
|
||||
set final[0] := x0
|
||||
...
|
||||
set final[i] := xi
|
||||
```
|
||||
On the hot path we know that `token` and `orig` refer to the same value. Thus, if we can detect that
|
||||
one of the `xi` is of the shape `let xi := proj[i] orig`, we can omit the store on the hot path.
|
||||
Just like with `reusejp` on the cold path we have to perform all the stores.
|
||||
-/
|
||||
|
||||
namespace Lean.Compiler.LCNF
|
||||
|
||||
open ImpureType
|
||||
|
||||
abbrev Mask := Array (Option FVarId)
|
||||
|
||||
/--
|
||||
Try to erase `inc` instructions on projections of `targetId` occuring in the tail of `ds`.
|
||||
Return the updated `ds` and mask contianing the `FVarId`s whose `inc` was removed.
|
||||
-/
|
||||
partial def eraseProjIncFor (nFields : Nat) (targetId : FVarId) (ds : Array (CodeDecl .impure)) :
|
||||
CompilerM (Array (CodeDecl .impure) × Mask) := do
|
||||
let mut ds := ds
|
||||
let mut keep := #[]
|
||||
let mut mask := Array.replicate nFields none
|
||||
while ds.size ≥ 2 do
|
||||
let d := ds.back!
|
||||
match d with
|
||||
| .let { value := .sproj .., .. } | .let { value := .uproj .., .. } =>
|
||||
ds := ds.pop
|
||||
keep := keep.push d
|
||||
| .inc z n c p =>
|
||||
assert! n > 0 -- 0 incs should not be happening
|
||||
let d' := ds[ds.size - 2]!
|
||||
let .let { fvarId := w, value := .oproj i x _, .. } := d'
|
||||
| break
|
||||
if !(w == z && targetId == x) then
|
||||
break
|
||||
/-
|
||||
Found
|
||||
```
|
||||
let z := proj[i] targetId
|
||||
inc z n c
|
||||
```
|
||||
We keep `proj`, and `inc` when `n > 1`
|
||||
-/
|
||||
ds := ds.pop.pop
|
||||
mask := mask.set! i (some z)
|
||||
keep := keep.push d'
|
||||
keep := if n == 1 then keep else keep.push (.inc z (n - 1) c p)
|
||||
| _ => break
|
||||
|
||||
return (ds ++ keep.reverse, mask)
|
||||
|
||||
def mkIf (discr : FVarId) (discrType : Expr) (resultType : Expr) (t e : Code .impure) :
|
||||
CompilerM (Code .impure) := do
|
||||
return .cases <| .mk discrType.getAppFn.constName! resultType discr #[
|
||||
.ctorAlt { name := ``Bool.false, cidx := 0, size := 0, usize := 0, ssize := 0 } e,
|
||||
.ctorAlt { name := ``Bool.true, cidx := 1, size := 0, usize := 0, ssize := 0 } t,
|
||||
]
|
||||
|
||||
def remapSets (targetId : FVarId) (sets : Array (CodeDecl .impure)) :
|
||||
CompilerM (Array (CodeDecl .impure)) :=
|
||||
return sets.map fun
|
||||
| .oset fvarId i y => .oset targetId i y
|
||||
| .sset fvarId i offset y ty => .sset targetId i offset y ty
|
||||
| .uset fvarId i y => .uset targetId i y
|
||||
| _ => unreachable!
|
||||
|
||||
def isSelfOset (fvarId : FVarId) (i : Nat) (y : Arg .impure) : CompilerM Bool := do
|
||||
match y with
|
||||
| .fvar y =>
|
||||
let some value ← findLetValue? (pu := .impure) y | return false
|
||||
let .oproj i' fvarId' := value | return false
|
||||
return i == i' && fvarId == fvarId'
|
||||
| .erased => return false
|
||||
|
||||
def isSelfUset (fvarId : FVarId) (i : Nat) (y : FVarId) : CompilerM Bool := do
|
||||
let some value ← findLetValue? (pu := .impure) y | return false
|
||||
let .uproj i' fvarId' := value | return false
|
||||
return i == i' && fvarId == fvarId'
|
||||
|
||||
def isSelfSset (fvarId : FVarId) (i : Nat) (offset : Nat) (y : FVarId) :
|
||||
CompilerM Bool := do
|
||||
let some value ← findLetValue? (pu := .impure) y | return false
|
||||
let .sproj i' offset' fvarId' := value | return false
|
||||
return i == i' && offset == offset' && fvarId == fvarId'
|
||||
|
||||
/--
|
||||
Partition the set instructions in `sets` into a pair `(selfSets, necessarySets)` where `selfSets`
|
||||
contain instructions that perform a set with the same value projected from `selfId` and
|
||||
`necessarySets` all others.
|
||||
-/
|
||||
def partitionSelfSets (selfId : FVarId) (sets : Array (CodeDecl .impure)) :
|
||||
CompilerM (Array (CodeDecl .impure) × Array (CodeDecl .impure)) := do
|
||||
let mut necessarySets := #[]
|
||||
let mut selfSets := #[]
|
||||
for set in sets do
|
||||
let isSelfSet :=
|
||||
match set with
|
||||
| .oset _ i y => isSelfOset selfId i y
|
||||
| .uset _ i y => isSelfUset selfId i y
|
||||
| .sset _ i offset y _ => isSelfSset selfId i offset y
|
||||
| _ => unreachable!
|
||||
if ← isSelfSet then
|
||||
selfSets := selfSets.push set
|
||||
else
|
||||
necessarySets := necessarySets.push set
|
||||
|
||||
return (selfSets, necessarySets)
|
||||
|
||||
def collectSucceedingSets (target : FVarId) (k : Code .impure) :
|
||||
CompilerM (Array (CodeDecl .impure) × Code .impure) := do
|
||||
let mut sets := #[]
|
||||
let mut k := k
|
||||
while true do
|
||||
match k with
|
||||
| .oset (fvarId := fvarId) (k := k') .. | .sset (fvarId := fvarId) (k := k') ..
|
||||
| .uset (fvarId := fvarId) (k := k') .. =>
|
||||
if target != fvarId then
|
||||
break
|
||||
sets := sets.push k.toCodeDecl!
|
||||
k := k'
|
||||
| _ => break
|
||||
return (sets, k)
|
||||
|
||||
mutual
|
||||
|
||||
/--
|
||||
Expand the matching `reuse`/`dec` for the allocation in `origAllocId` whose `reset` token is in
|
||||
`resetTokenId`.
|
||||
-/
|
||||
partial def processResetCont (resetTokenId : FVarId) (code : Code .impure) (origAllocId : FVarId)
|
||||
(isSharedId : FVarId) (currentRetType : Expr) : CompilerM (Code .impure) := do
|
||||
match code with
|
||||
| .dec y n _ _ k =>
|
||||
if resetTokenId == y then
|
||||
assert! n == 1 -- n must be one since `resetToken := reset ...`
|
||||
return .del resetTokenId k
|
||||
else
|
||||
let k ← processResetCont resetTokenId k origAllocId isSharedId currentRetType
|
||||
return code.updateCont! k
|
||||
| .let decl k =>
|
||||
match decl.value with
|
||||
| .reuse y c u xs =>
|
||||
if resetTokenId != y then
|
||||
let k ← processResetCont resetTokenId k origAllocId isSharedId currentRetType
|
||||
return code.updateCont! k
|
||||
|
||||
let (succeedingSets, k) ← collectSucceedingSets decl.fvarId k
|
||||
let (selfSets, necessarySets) ← partitionSelfSets origAllocId succeedingSets
|
||||
let k := attachCodeDecls necessarySets k
|
||||
|
||||
let param := {
|
||||
fvarId := decl.fvarId,
|
||||
binderName := decl.binderName,
|
||||
type := decl.type,
|
||||
borrow := false
|
||||
}
|
||||
let contJp ← mkFunDecl (← mkFreshBinderName `reusejp) currentRetType #[param] k
|
||||
|
||||
let slowPath ← mkSlowPath decl c xs contJp.fvarId selfSets
|
||||
let fastPath ← mkFastPath resetTokenId c u xs contJp.fvarId origAllocId
|
||||
|
||||
eraseLetDecl decl
|
||||
|
||||
let reuse ← mkIf isSharedId uint8 currentRetType slowPath fastPath
|
||||
return .jp contJp reuse
|
||||
| _ =>
|
||||
let k ← processResetCont resetTokenId k origAllocId isSharedId currentRetType
|
||||
return code.updateCont! k
|
||||
| .cases cs =>
|
||||
return code.updateAlts! (← cs.alts.mapMonoM (·.mapCodeM (processResetCont resetTokenId · origAllocId isSharedId cs.resultType)))
|
||||
| .jp decl k =>
|
||||
let decl ← decl.updateValue (← processResetCont resetTokenId decl.value origAllocId isSharedId decl.type)
|
||||
let k ← processResetCont resetTokenId k origAllocId isSharedId currentRetType
|
||||
return code.updateFun! decl k
|
||||
| .uset (k := k) .. | .sset (k := k) .. | .inc (k := k) .. | .setTag (k := k) ..
|
||||
| .del (k := k) .. | .oset (k := k) .. =>
|
||||
let k ← processResetCont resetTokenId k origAllocId isSharedId currentRetType
|
||||
return code.updateCont! k
|
||||
| .jmp .. | .return .. | .unreach .. => return code
|
||||
where
|
||||
/--
|
||||
On the slow path we have to:
|
||||
1. Make a fresh alloation
|
||||
2. Apply all the self sets as the fresh allocation is of course not in sync with the original one.
|
||||
3. Pass the fresh allocation to the joinpoint.
|
||||
-/
|
||||
mkSlowPath (decl : LetDecl .impure) (info : CtorInfo) (args : Array (Arg .impure))
|
||||
(contJpId : FVarId) (selfSets : Array (CodeDecl .impure)) : CompilerM (Code .impure) := do
|
||||
let allocDecl ← mkLetDecl (← mkFreshBinderName `reuseFailAlloc) decl.type (.ctor info args)
|
||||
let mut code := .jmp contJpId #[.fvar allocDecl.fvarId]
|
||||
code := attachCodeDecls (← remapSets allocDecl.fvarId selfSets) code
|
||||
code := .let allocDecl code
|
||||
return code
|
||||
|
||||
/--
|
||||
On the fast path path we have to:
|
||||
1. Make all non-self object sets to "simulate" the allocation (the remaining necessary sets will
|
||||
be made in the continuation)
|
||||
2. Pass the reused allocation to the joinpoint.
|
||||
-/
|
||||
mkFastPath (resetTokenId : FVarId) (info : CtorInfo) (update : Bool) (args : Array (Arg .impure))
|
||||
(contJpId : FVarId) (origAllocId : FVarId) : CompilerM (Code .impure) := do
|
||||
let mut code := .jmp contJpId #[.fvar resetTokenId]
|
||||
for h : idx in 0...args.size do
|
||||
if !(← isSelfOset origAllocId idx args[idx]) then
|
||||
code := .oset resetTokenId idx args[idx] code
|
||||
if update then
|
||||
code := .setTag resetTokenId info.cidx code
|
||||
return code
|
||||
|
||||
/--
|
||||
Traverse `code` looking for reset-reuse pairs to expand while `ds` holds the instructions up to the
|
||||
last branching point.
|
||||
-/
|
||||
partial def Code.expandResetReuse (code : Code .impure) (ds : Array (CodeDecl .impure))
|
||||
(currentRetType : Expr) : CompilerM (Code .impure) := do
|
||||
let collectAndGo (code : Code .impure) (ds : Array (CodeDecl .impure)) (k : Code .impure) :=
|
||||
let d := code.toCodeDecl!
|
||||
k.expandResetReuse (ds.push d) currentRetType
|
||||
match code with
|
||||
| .let decl k =>
|
||||
match decl.value with
|
||||
| .reset nFields origAllocId => expand ds decl nFields origAllocId k
|
||||
| _ => collectAndGo code ds k
|
||||
| .jp decl k =>
|
||||
let value ← decl.value.expandResetReuse #[] decl.type
|
||||
let decl ← decl.updateValue value
|
||||
k.expandResetReuse (ds.push (.jp decl)) currentRetType
|
||||
| .cases cs =>
|
||||
let alts ← cs.alts.mapMonoM (·.mapCodeM (·.expandResetReuse #[] cs.resultType))
|
||||
let code := code.updateAlts! alts
|
||||
return attachCodeDecls ds code
|
||||
| .uset (k := k) .. | .sset (k := k) .. | .inc (k := k) .. | .setTag (k := k) ..
|
||||
| .dec (k := k) .. | .del (k := k) .. | .oset (k := k) .. =>
|
||||
collectAndGo code ds k
|
||||
| .jmp .. | .return .. | .unreach .. =>
|
||||
return attachCodeDecls ds code
|
||||
where
|
||||
/--
|
||||
Expand the reset in `decl` together with its matching `reuse`/`dec`s in its continuation `k`.
|
||||
-/
|
||||
expand (ds : Array (CodeDecl .impure)) (decl : LetDecl .impure) (nFields : Nat)
|
||||
(origAllocId : FVarId) (k : Code .impure) : CompilerM (Code .impure) := do
|
||||
let (ds, mask) ← eraseProjIncFor nFields origAllocId ds
|
||||
let isSharedParam ← mkParam (← mkFreshBinderName `isShared) uint8 false
|
||||
let k ← processResetCont decl.fvarId k origAllocId isSharedParam.fvarId currentRetType
|
||||
let k ← k.expandResetReuse #[] currentRetType
|
||||
let allocParam := {
|
||||
fvarId := decl.fvarId,
|
||||
binderName := decl.binderName,
|
||||
type := tobject,
|
||||
borrow := false
|
||||
}
|
||||
let resetJp ← mkFunDecl (← mkFreshBinderName `resetjp) currentRetType #[allocParam, isSharedParam] k
|
||||
let isSharedDecl ← mkLetDecl (← mkFreshBinderName `isSharedCheck) uint8 (.isShared origAllocId)
|
||||
let slowPath ← mkSlowPath origAllocId mask resetJp.fvarId isSharedDecl.fvarId
|
||||
let fastPath ← mkFastPath origAllocId mask resetJp.fvarId isSharedDecl.fvarId
|
||||
let mut reset ← mkIf isSharedDecl.fvarId uint8 currentRetType slowPath fastPath
|
||||
reset := .let isSharedDecl reset
|
||||
eraseLetDecl decl
|
||||
return attachCodeDecls ds (.jp resetJp reset)
|
||||
|
||||
/--
|
||||
On the slow path we cannot reuse the allocation, this means we have to:
|
||||
1. Increments all variables projected from `origAllocId` that have not been incremented yet by
|
||||
the shared prologue. On the fast path they are kept alive naturally by the original allocation
|
||||
but here that is not necessarily the case.
|
||||
2. Decrement the value being reset (the natural behavior of a failed reset)
|
||||
3. Pass box(0) as a reuse value into the continuation join point
|
||||
-/
|
||||
mkSlowPath (origAllocId : FVarId) (mask : Mask) (resetJpId : FVarId) (isSharedId : FVarId) :
|
||||
CompilerM (Code .impure) := do
|
||||
let mut code := .jmp resetJpId #[.erased, .fvar isSharedId]
|
||||
code := .dec origAllocId 1 true false code
|
||||
for fvarId? in mask do
|
||||
let some fvarId := fvarId? | continue
|
||||
code := .inc fvarId 1 true false code
|
||||
return code
|
||||
|
||||
/--
|
||||
On the fast path we can reuse the allocation, this means we have to:
|
||||
1. decrement all unread fields as their parent allocation would usually be dropped at this point
|
||||
and we want to be garbage free.
|
||||
2. Pass the original allocation as a reuse value into the continuation join point
|
||||
-/
|
||||
mkFastPath (origAllocId : FVarId) (mask : Mask) (resetJpId : FVarId) (isSharedId : FVarId) :
|
||||
CompilerM (Code .impure) := do
|
||||
let mut code := .jmp resetJpId #[.fvar origAllocId, .fvar isSharedId]
|
||||
for h : idx in 0...mask.size do
|
||||
if mask[idx].isSome then
|
||||
continue
|
||||
let fieldDecl ← mkLetDecl (← mkFreshBinderName `unused) tobject (.oproj idx origAllocId)
|
||||
code := .let fieldDecl (.dec fieldDecl.fvarId 1 true false code)
|
||||
return code
|
||||
|
||||
end
|
||||
|
||||
def Decl.expandResetReuse (decl : Decl .impure) : CompilerM (Decl .impure) := do
|
||||
if (← getConfig).resetReuse then
|
||||
let value ← decl.value.mapCodeM (·.expandResetReuse #[] decl.type)
|
||||
let decl := { decl with value }
|
||||
return decl
|
||||
else
|
||||
return decl
|
||||
|
||||
public def expandResetReuse : Pass :=
|
||||
Pass.mkPerDeclaration `expandResetReuse .impure Decl.expandResetReuse
|
||||
|
||||
builtin_initialize
|
||||
registerTraceClass `Compiler.expandResetReuse (inherited := true)
|
||||
|
||||
end Lean.Compiler.LCNF
|
||||
@@ -27,6 +27,7 @@ public import Lean.Compiler.LCNF.InferBorrow
|
||||
public import Lean.Compiler.LCNF.ExplicitBoxing
|
||||
public import Lean.Compiler.LCNF.ExplicitRC
|
||||
public import Lean.Compiler.LCNF.Toposort
|
||||
public import Lean.Compiler.LCNF.ExpandResetReuse
|
||||
|
||||
public section
|
||||
|
||||
@@ -154,6 +155,8 @@ def builtinPassManager : PassManager := {
|
||||
inferBorrow,
|
||||
explicitBoxing,
|
||||
explicitRc,
|
||||
expandResetReuse,
|
||||
pushProj (occurrence := 1),
|
||||
inferVisibility (phase := .impure),
|
||||
saveImpure, -- End of impure phase
|
||||
toposortPass,
|
||||
|
||||
@@ -309,7 +309,7 @@ typedef struct {
|
||||
void * m_data;
|
||||
} lean_external_object;
|
||||
|
||||
static inline LEAN_ALWAYS_INLINE bool lean_is_scalar(lean_object * o) { return ((size_t)(o) & 1) == 1; }
|
||||
static inline LEAN_ALWAYS_INLINE uint8_t lean_is_scalar(lean_object * o) { return ((size_t)(o) & 1) == 1; }
|
||||
static inline lean_object * lean_box(size_t n) { return (lean_object*)(((size_t)(n) << 1) | 1); }
|
||||
static inline size_t lean_unbox(lean_object * o) { return (size_t)(o) >> 1; }
|
||||
|
||||
@@ -441,6 +441,13 @@ static inline void lean_free_small_object(lean_object * o) {
|
||||
LEAN_EXPORT lean_object * lean_alloc_object(size_t sz);
|
||||
LEAN_EXPORT void lean_free_object(lean_object * o);
|
||||
|
||||
|
||||
static inline void lean_del_object(lean_object * o) {
|
||||
if (!lean_is_scalar(o)) {
|
||||
lean_free_object(o);
|
||||
}
|
||||
}
|
||||
|
||||
static inline uint8_t lean_ptr_tag(lean_object * o) {
|
||||
return o->m_tag;
|
||||
}
|
||||
|
||||
@@ -751,7 +751,7 @@ private:
|
||||
break;
|
||||
}
|
||||
case fn_body_kind::Del: // delete object of unique reference
|
||||
lean_free_object(var(fn_body_del_var(b)).m_obj);
|
||||
lean_del_object(var(fn_body_del_var(b)).m_obj);
|
||||
b = fn_body_del_cont(b);
|
||||
break;
|
||||
case fn_body_kind::Case: { // branch according to constructor tag
|
||||
|
||||
@@ -32,6 +32,89 @@ unsafe axiom lcAny : Type
|
||||
/-- Internal representation of `Void` in the compiler. -/
|
||||
unsafe axiom lcVoid : Type
|
||||
|
||||
set_option bootstrap.inductiveCheckResultingUniverse false in
|
||||
/--
|
||||
The canonical universe-polymorphic type with just one element.
|
||||
|
||||
It should be used in contexts that require a type to be universe polymorphic, thus disallowing
|
||||
`Unit`.
|
||||
-/
|
||||
inductive PUnit : Sort u where
|
||||
/-- The only element of the universe-polymorphic unit type. -/
|
||||
| unit : PUnit
|
||||
|
||||
/--
|
||||
The equality relation. It has one introduction rule, `Eq.refl`.
|
||||
We use `a = b` as notation for `Eq a b`.
|
||||
A fundamental property of equality is that it is an equivalence relation.
|
||||
```
|
||||
variable (α : Type) (a b c d : α)
|
||||
variable (hab : a = b) (hcb : c = b) (hcd : c = d)
|
||||
|
||||
example : a = d :=
|
||||
Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
|
||||
```
|
||||
Equality is much more than an equivalence relation, however. It has the important property that every assertion
|
||||
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
|
||||
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
|
||||
Example:
|
||||
```
|
||||
example (α : Type) (a b : α) (p : α → Prop)
|
||||
(h1 : a = b) (h2 : p a) : p b :=
|
||||
Eq.subst h1 h2
|
||||
|
||||
example (α : Type) (a b : α) (p : α → Prop)
|
||||
(h1 : a = b) (h2 : p a) : p b :=
|
||||
h1 ▸ h2
|
||||
```
|
||||
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
|
||||
For more information: [Equality](https://lean-lang.org/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
|
||||
|
||||
|
||||
/-- 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 :=
|
||||
h.rec m
|
||||
|
||||
/--
|
||||
Heterogeneous equality. `a ≍ b` asserts that `a` and `b` have the same
|
||||
type, and casting `a` across the equality yields `b`, and vice versa.
|
||||
|
||||
You should avoid using this type if you can. Heterogeneous equality does not
|
||||
have all the same properties as `Eq`, because the assumption that the types of
|
||||
`a` and `b` are equal is often too weak to prove theorems of interest. One
|
||||
public important non-theorem is the analogue of `congr`: If `f ≍ g` and `x ≍ y`
|
||||
and `f x` and `g y` are well typed it does not follow that `f x ≍ g y`.
|
||||
(This does follow if you have `f = g` instead.) However if `a` and `b` have
|
||||
the same type then `a = b` and `a ≍ b` are equivalent.
|
||||
-/
|
||||
inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
|
||||
/-- Reflexivity of heterogeneous equality. -/
|
||||
| refl (a : α) : HEq a a
|
||||
|
||||
/--
|
||||
The Boolean values, `true` and `false`.
|
||||
|
||||
Logically speaking, this is equivalent to `Prop` (the type of propositions). The distinction is
|
||||
public important for programming: both propositions and their proofs are erased in the code generator,
|
||||
while `Bool` corresponds to the Boolean type in most programming languages and carries precisely one
|
||||
bit of run-time information.
|
||||
-/
|
||||
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
|
||||
|
||||
export Bool (false true)
|
||||
|
||||
/-- Compute whether `x` is a tagged pointer or not. -/
|
||||
@[extern "lean_is_scalar"]
|
||||
unsafe axiom isScalarObj {α : Type u} (x : α) : Bool
|
||||
|
||||
/--
|
||||
The identity function. `id` takes an implicit argument `α : Sort u`
|
||||
@@ -115,16 +198,7 @@ does.) Example:
|
||||
-/
|
||||
abbrev inferInstanceAs (α : Sort u) [i : α] : α := i
|
||||
|
||||
set_option bootstrap.inductiveCheckResultingUniverse false in
|
||||
/--
|
||||
The canonical universe-polymorphic type with just one element.
|
||||
|
||||
It should be used in contexts that require a type to be universe polymorphic, thus disallowing
|
||||
`Unit`.
|
||||
-/
|
||||
inductive PUnit : Sort u where
|
||||
/-- The only element of the universe-polymorphic unit type. -/
|
||||
| unit : PUnit
|
||||
|
||||
/--
|
||||
The canonical type with one element. This element is written `()`.
|
||||
@@ -244,42 +318,6 @@ For more information: [Propositional Logic](https://lean-lang.org/theorem_provin
|
||||
-/
|
||||
@[macro_inline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : Not a) : b :=( h₂ h₁).rec
|
||||
|
||||
/--
|
||||
The equality relation. It has one introduction rule, `Eq.refl`.
|
||||
We use `a = b` as notation for `Eq a b`.
|
||||
A fundamental property of equality is that it is an equivalence relation.
|
||||
```
|
||||
variable (α : Type) (a b c d : α)
|
||||
variable (hab : a = b) (hcb : c = b) (hcd : c = d)
|
||||
|
||||
example : a = d :=
|
||||
Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
|
||||
```
|
||||
Equality is much more than an equivalence relation, however. It has the important property that every assertion
|
||||
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
|
||||
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
|
||||
Example:
|
||||
```
|
||||
example (α : Type) (a b : α) (p : α → Prop)
|
||||
(h1 : a = b) (h2 : p a) : p b :=
|
||||
Eq.subst h1 h2
|
||||
|
||||
example (α : Type) (a b : α) (p : α → Prop)
|
||||
(h1 : a = b) (h2 : p a) : p b :=
|
||||
h1 ▸ h2
|
||||
```
|
||||
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
|
||||
For more information: [Equality](https://lean-lang.org/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
|
||||
|
||||
/-- 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 :=
|
||||
h.rec m
|
||||
|
||||
/--
|
||||
`rfl : a = a` is the unique constructor of the equality type. This is the
|
||||
same as `Eq.refl` except that it takes `a` implicitly instead of explicitly.
|
||||
@@ -476,21 +514,6 @@ Unsafe auxiliary constant used by the compiler to erase `Quot.lift`.
|
||||
-/
|
||||
unsafe axiom Quot.lcInv {α : Sort u} {r : α → α → Prop} (q : Quot r) : α
|
||||
|
||||
/--
|
||||
Heterogeneous equality. `a ≍ b` asserts that `a` and `b` have the same
|
||||
type, and casting `a` across the equality yields `b`, and vice versa.
|
||||
|
||||
You should avoid using this type if you can. Heterogeneous equality does not
|
||||
have all the same properties as `Eq`, because the assumption that the types of
|
||||
`a` and `b` are equal is often too weak to prove theorems of interest. One
|
||||
public important non-theorem is the analogue of `congr`: If `f ≍ g` and `x ≍ y`
|
||||
and `f x` and `g y` are well typed it does not follow that `f x ≍ g y`.
|
||||
(This does follow if you have `f = g` instead.) However if `a` and `b` have
|
||||
the same type then `a = b` and `a ≍ b` are equivalent.
|
||||
-/
|
||||
inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
|
||||
/-- Reflexivity of heterogeneous equality. -/
|
||||
| refl (a : α) : HEq a a
|
||||
|
||||
/-- A version of `HEq.refl` with an implicit argument. -/
|
||||
@[match_pattern] protected def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
|
||||
@@ -598,23 +621,6 @@ theorem Or.resolve_left (h: Or a b) (na : Not a) : b := h.elim ( absurd · na)
|
||||
theorem Or.resolve_right (h: Or a b) (nb : Not b) : a := h.elim id ( absurd · nb)
|
||||
theorem Or.neg_resolve_left (h : Or ( Not a)b) (ha : a) : b := h.elim ( absurd ha)id
|
||||
theorem Or.neg_resolve_right (h : Or a ( Not b)) (nb : b) : a := h.elim id ( absurd nb)
|
||||
|
||||
/--
|
||||
The Boolean values, `true` and `false`.
|
||||
|
||||
Logically speaking, this is equivalent to `Prop` (the type of propositions). The distinction is
|
||||
public important for programming: both propositions and their proofs are erased in the code generator,
|
||||
while `Bool` corresponds to the Boolean type in most programming languages and carries precisely one
|
||||
bit of run-time information.
|
||||
-/
|
||||
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
|
||||
|
||||
export Bool (false true)
|
||||
|
||||
/--
|
||||
All the elements of a type that satisfy a predicate.
|
||||
|
||||
|
||||
@@ -11,6 +11,21 @@ trace: [Compiler.pushProj] size: 5
|
||||
| Option.some =>
|
||||
let val.2 : tobj := oproj[0] a;
|
||||
return val.2
|
||||
[Compiler.pushProj] size: 6
|
||||
def test1 @&a : tobj :=
|
||||
cases a : tobj
|
||||
| Option.none =>
|
||||
let _x.1 : tagged := 0;
|
||||
return _x.1
|
||||
| Option.some =>
|
||||
let val.2 : tobj := oproj[0] a;
|
||||
inc val.2;
|
||||
return val.2
|
||||
[Compiler.pushProj] size: 2
|
||||
def test1._boxed a : tobj :=
|
||||
let res : tobj := test1 a;
|
||||
dec a;
|
||||
return res
|
||||
-/
|
||||
#guard_msgs in
|
||||
set_option pp.letVarTypes true in
|
||||
@@ -37,6 +52,45 @@ trace: [Compiler.pushProj] size: 10
|
||||
let _x.3 : tobj := Nat.add val.1 val.2;
|
||||
let _x.4 : obj := ctor_1[Option.some] _x.3;
|
||||
return _x.4
|
||||
[Compiler.pushProj] size: 27
|
||||
def test2 @&a b : tobj :=
|
||||
cases a : tobj
|
||||
| Option.none =>
|
||||
dec b;
|
||||
return a
|
||||
| Option.some =>
|
||||
cases b : tobj
|
||||
| Option.none =>
|
||||
inc a;
|
||||
return a
|
||||
| Option.some =>
|
||||
let val.1 : tobj := oproj[0] a;
|
||||
let val.2 : tobj := oproj[0] b;
|
||||
jp resetjp.3 _x.4 isShared.5 : tobj :=
|
||||
let _x.6 : tobj := Nat.add val.1 val.2;
|
||||
dec val.2;
|
||||
jp reusejp.7 _x.8 : tobj :=
|
||||
return _x.8;
|
||||
cases isShared.5 : tobj
|
||||
| Bool.false =>
|
||||
oset _x.4 [0] := _x.6;
|
||||
goto reusejp.7 _x.4
|
||||
| Bool.true =>
|
||||
let reuseFailAlloc.9 : obj := ctor_1[Option.some] _x.6;
|
||||
goto reusejp.7 reuseFailAlloc.9;
|
||||
let isSharedCheck.10 : UInt8 := isShared b;
|
||||
cases isSharedCheck.10 : tobj
|
||||
| Bool.false =>
|
||||
goto resetjp.3 b isSharedCheck.10
|
||||
| Bool.true =>
|
||||
inc val.2;
|
||||
dec b;
|
||||
goto resetjp.3 ◾ isSharedCheck.10
|
||||
[Compiler.pushProj] size: 2
|
||||
def test2._boxed a b : tobj :=
|
||||
let res : tobj := test2 a b;
|
||||
dec a;
|
||||
return res
|
||||
-/
|
||||
#guard_msgs in
|
||||
set_option pp.letVarTypes true in
|
||||
@@ -69,6 +123,63 @@ trace: [Compiler.pushProj] size: 14
|
||||
let _x.7 : tobj := Nat.add val.5 val.6;
|
||||
let _x.8 : obj := ctor_1[Option.some] _x.7;
|
||||
return _x.8
|
||||
[Compiler.pushProj] size: 48
|
||||
def test3 a b : tobj :=
|
||||
cases a : tobj
|
||||
| Option.none =>
|
||||
dec b;
|
||||
return a
|
||||
| Option.some =>
|
||||
cases b : tobj
|
||||
| Option.none =>
|
||||
let val.1 : tobj := oproj[0] a;
|
||||
jp resetjp.2 _x.3 isShared.4 : tobj :=
|
||||
let _x.5 : tagged := 1;
|
||||
let _x.6 : tobj := Nat.add val.1 _x.5;
|
||||
dec val.1;
|
||||
jp reusejp.7 _x.8 : tobj :=
|
||||
return _x.8;
|
||||
cases isShared.4 : tobj
|
||||
| Bool.false =>
|
||||
oset _x.3 [0] := _x.6;
|
||||
goto reusejp.7 _x.3
|
||||
| Bool.true =>
|
||||
let reuseFailAlloc.9 : obj := ctor_1[Option.some] _x.6;
|
||||
goto reusejp.7 reuseFailAlloc.9;
|
||||
let isSharedCheck.10 : UInt8 := isShared a;
|
||||
cases isSharedCheck.10 : tobj
|
||||
| Bool.false =>
|
||||
goto resetjp.2 a isSharedCheck.10
|
||||
| Bool.true =>
|
||||
inc val.1;
|
||||
dec a;
|
||||
goto resetjp.2 ◾ isSharedCheck.10
|
||||
| Option.some =>
|
||||
let val.11 : tobj := oproj[0] a;
|
||||
inc val.11;
|
||||
dec a;
|
||||
let val.12 : tobj := oproj[0] b;
|
||||
jp resetjp.13 _x.14 isShared.15 : tobj :=
|
||||
let _x.16 : tobj := Nat.add val.11 val.12;
|
||||
dec val.12;
|
||||
dec val.11;
|
||||
jp reusejp.17 _x.18 : tobj :=
|
||||
return _x.18;
|
||||
cases isShared.15 : tobj
|
||||
| Bool.false =>
|
||||
oset _x.14 [0] := _x.16;
|
||||
goto reusejp.17 _x.14
|
||||
| Bool.true =>
|
||||
let reuseFailAlloc.19 : obj := ctor_1[Option.some] _x.16;
|
||||
goto reusejp.17 reuseFailAlloc.19;
|
||||
let isSharedCheck.20 : UInt8 := isShared b;
|
||||
cases isSharedCheck.20 : tobj
|
||||
| Bool.false =>
|
||||
goto resetjp.13 b isSharedCheck.20
|
||||
| Bool.true =>
|
||||
inc val.12;
|
||||
dec b;
|
||||
goto resetjp.13 ◾ isSharedCheck.20
|
||||
-/
|
||||
#guard_msgs in
|
||||
set_option pp.letVarTypes true in
|
||||
@@ -106,6 +217,75 @@ trace: [Compiler.pushProj] size: 18
|
||||
let _x.8 : tobj := Nat.add val.6 val.7;
|
||||
let _x.9 : obj := ctor_1[Option.some] _x.8;
|
||||
return _x.9
|
||||
[Compiler.pushProj] size: 54
|
||||
def test4 a b c : tobj :=
|
||||
cases a : tobj
|
||||
| Option.none =>
|
||||
dec b;
|
||||
return a
|
||||
| Option.some =>
|
||||
cases b : tobj
|
||||
| Option.none =>
|
||||
let val.1 : tobj := oproj[0] a;
|
||||
jp resetjp.2 _x.3 isShared.4 : tobj :=
|
||||
let _x.5 : tagged := 1;
|
||||
let _x.6 : tobj := Nat.add val.1 _x.5;
|
||||
dec val.1;
|
||||
jp reusejp.7 _x.8 : tobj :=
|
||||
return _x.8;
|
||||
cases isShared.4 : tobj
|
||||
| Bool.false =>
|
||||
oset _x.3 [0] := _x.6;
|
||||
goto reusejp.7 _x.3
|
||||
| Bool.true =>
|
||||
let reuseFailAlloc.9 : obj := ctor_1[Option.some] _x.6;
|
||||
goto reusejp.7 reuseFailAlloc.9;
|
||||
let isSharedCheck.10 : UInt8 := isShared a;
|
||||
cases isSharedCheck.10 : tobj
|
||||
| Bool.false =>
|
||||
goto resetjp.2 a isSharedCheck.10
|
||||
| Bool.true =>
|
||||
inc val.1;
|
||||
dec a;
|
||||
goto resetjp.2 ◾ isSharedCheck.10
|
||||
| Option.some =>
|
||||
cases c : tobj
|
||||
| Bool.false =>
|
||||
dec b;
|
||||
dec a;
|
||||
let _x.11 : tagged := ctor_0[Option.none];
|
||||
return _x.11
|
||||
| Bool.true =>
|
||||
let val.12 : tobj := oproj[0] a;
|
||||
inc val.12;
|
||||
dec a;
|
||||
let val.13 : tobj := oproj[0] b;
|
||||
jp resetjp.14 _x.15 isShared.16 : tobj :=
|
||||
let _x.17 : tobj := Nat.add val.12 val.13;
|
||||
dec val.13;
|
||||
dec val.12;
|
||||
jp reusejp.18 _x.19 : tobj :=
|
||||
return _x.19;
|
||||
cases isShared.16 : tobj
|
||||
| Bool.false =>
|
||||
oset _x.15 [0] := _x.17;
|
||||
goto reusejp.18 _x.15
|
||||
| Bool.true =>
|
||||
let reuseFailAlloc.20 : obj := ctor_1[Option.some] _x.17;
|
||||
goto reusejp.18 reuseFailAlloc.20;
|
||||
let isSharedCheck.21 : UInt8 := isShared b;
|
||||
cases isSharedCheck.21 : tobj
|
||||
| Bool.false =>
|
||||
goto resetjp.14 b isSharedCheck.21
|
||||
| Bool.true =>
|
||||
inc val.13;
|
||||
dec b;
|
||||
goto resetjp.14 ◾ isSharedCheck.21
|
||||
[Compiler.pushProj] size: 2
|
||||
def test4._boxed a b c : tobj :=
|
||||
let c.boxed : UInt8 := unbox c;
|
||||
let res : tobj := test4 a b c.boxed;
|
||||
return res
|
||||
-/
|
||||
#guard_msgs in
|
||||
set_option pp.letVarTypes true in
|
||||
|
||||
@@ -33,6 +33,21 @@ trace: [Compiler.saveMono] size: 5
|
||||
| Option.some =>
|
||||
let _x.2 := 0;
|
||||
return _x.2
|
||||
[Compiler.pushProj] size: 5
|
||||
def isNone @&x : UInt8 :=
|
||||
cases x : UInt8
|
||||
| Option.none =>
|
||||
let _x.1 := 1;
|
||||
return _x.1
|
||||
| Option.some =>
|
||||
let _x.2 := 0;
|
||||
return _x.2
|
||||
[Compiler.pushProj] size: 3
|
||||
def isNone._boxed x : tagged :=
|
||||
let res := isNone x;
|
||||
dec x;
|
||||
let r := box res;
|
||||
return r
|
||||
-/
|
||||
#guard_msgs in
|
||||
set_option trace.Compiler.saveMono true in
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
|
||||
set_option trace.compiler.ir.result true
|
||||
set_option trace.Compiler.saveMono true
|
||||
|
||||
def g (ys : List Nat) : IO Nat := do
|
||||
let x := 0
|
||||
|
||||
@@ -1,95 +1,46 @@
|
||||
[Compiler.IR] [result]
|
||||
def IO.print._at_.IO.println._at_.g.spec_0.spec_0 (x_1 : obj) (x_2 : void) : obj :=
|
||||
let x_3 : obj := IO.getStdout ◾;
|
||||
let x_4 : obj := proj[4] x_3;
|
||||
inc x_4;
|
||||
dec x_3;
|
||||
let x_5 : obj := app x_4 x_1 ◾;
|
||||
ret x_5
|
||||
def IO.print._at_.IO.println._at_.g.spec_0.spec_0._boxed (x_1 : obj) (x_2 : tagged) : obj :=
|
||||
let x_3 : obj := IO.print._at_.IO.println._at_.g.spec_0.spec_0 x_1 x_2;
|
||||
ret x_3
|
||||
[Compiler.IR] [result]
|
||||
def IO.println._at_.g.spec_0 (x_1 : tobj) (x_2 : void) : obj :=
|
||||
let x_3 : obj := Nat.reprFast x_1;
|
||||
let x_4 : u32 := 10;
|
||||
let x_5 : obj := String.push x_3 x_4;
|
||||
let x_6 : obj := IO.print._at_.IO.println._at_.g.spec_0.spec_0 x_5 ◾;
|
||||
ret x_6
|
||||
def IO.println._at_.g.spec_0._boxed (x_1 : tobj) (x_2 : tagged) : obj :=
|
||||
let x_3 : obj := IO.println._at_.g.spec_0 x_1 x_2;
|
||||
ret x_3
|
||||
[Compiler.IR] [result]
|
||||
def List.forM._at_.g.spec_1 (x_1 : tobj) (x_2 : tobj) (x_3 : void) : obj :=
|
||||
case x_1 : tobj of
|
||||
List.nil →
|
||||
let x_4 : tagged := ctor_0[PUnit.unit];
|
||||
let x_5 : obj := ctor_0[Prod.mk] x_4 x_2;
|
||||
let x_6 : obj := ctor_0[EST.Out.ok] x_5;
|
||||
ret x_6
|
||||
List.cons →
|
||||
let x_7 : tobj := proj[0] x_1;
|
||||
inc x_7;
|
||||
let x_8 : tobj := proj[1] x_1;
|
||||
inc x_8;
|
||||
dec x_1;
|
||||
let x_9 : obj := IO.println._at_.g.spec_0 x_7 ◾;
|
||||
case x_9 : obj of
|
||||
EST.Out.ok →
|
||||
dec x_9;
|
||||
let x_10 : obj := List.forM._at_.g.spec_1 x_8 x_2 ◾;
|
||||
ret x_10
|
||||
EST.Out.error →
|
||||
dec x_8;
|
||||
dec x_2;
|
||||
let x_11 : u8 := isShared x_9;
|
||||
case x_11 : u8 of
|
||||
Bool.false →
|
||||
ret x_9
|
||||
Bool.true →
|
||||
let x_12 : tobj := proj[0] x_9;
|
||||
inc x_12;
|
||||
dec x_9;
|
||||
let x_13 : obj := ctor_1[EST.Out.error] x_12;
|
||||
ret x_13
|
||||
def List.forM._at_.g.spec_1._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tagged) : obj :=
|
||||
let x_4 : obj := List.forM._at_.g.spec_1 x_1 x_2 x_3;
|
||||
ret x_4
|
||||
[Compiler.IR] [result]
|
||||
def g (x_1 : tobj) (x_2 : void) : obj :=
|
||||
let x_3 : tagged := 0;
|
||||
let x_4 : obj := List.forM._at_.g.spec_1 x_1 x_3 ◾;
|
||||
case x_4 : obj of
|
||||
EST.Out.ok →
|
||||
let x_5 : u8 := isShared x_4;
|
||||
case x_5 : u8 of
|
||||
Bool.false →
|
||||
let x_6 : tobj := proj[0] x_4;
|
||||
let x_7 : tobj := proj[1] x_6;
|
||||
inc x_7;
|
||||
dec x_6;
|
||||
set x_4[0] := x_7;
|
||||
ret x_4
|
||||
Bool.true →
|
||||
let x_8 : tobj := proj[0] x_4;
|
||||
inc x_8;
|
||||
dec x_4;
|
||||
let x_9 : tobj := proj[1] x_8;
|
||||
inc x_9;
|
||||
dec x_8;
|
||||
let x_10 : obj := ctor_0[EST.Out.ok] x_9;
|
||||
ret x_10
|
||||
EST.Out.error →
|
||||
let x_11 : u8 := isShared x_4;
|
||||
case x_11 : u8 of
|
||||
Bool.false →
|
||||
ret x_4
|
||||
Bool.true →
|
||||
let x_12 : tobj := proj[0] x_4;
|
||||
inc x_12;
|
||||
dec x_4;
|
||||
let x_13 : obj := ctor_1[EST.Out.error] x_12;
|
||||
ret x_13
|
||||
def g._boxed (x_1 : tobj) (x_2 : tagged) : obj :=
|
||||
let x_3 : obj := g x_1 x_2;
|
||||
ret x_3
|
||||
[Compiler.saveMono] size: 6
|
||||
def IO.print._at_.IO.println._at_.g.spec_0.spec_0 s a.1 : EST.Out IO.Error lcAny PUnit :=
|
||||
let _x.2 := IO.getStdout a.1;
|
||||
cases _x.2 : EST.Out IO.Error lcAny PUnit
|
||||
| ST.Out.mk val.3 state.4 =>
|
||||
cases val.3 : EST.Out IO.Error lcAny PUnit
|
||||
| IO.FS.Stream.mk flush read write getLine putStr isTty =>
|
||||
let _x.5 := putStr s state.4;
|
||||
return _x.5
|
||||
[Compiler.saveMono] size: 4
|
||||
def IO.println._at_.g.spec_0 s a.1 : EST.Out IO.Error lcAny PUnit :=
|
||||
let _x.2 := Nat.reprFast s;
|
||||
let _x.3 := 10;
|
||||
let _x.4 := String.push _x.2 _x.3;
|
||||
let _x.5 := IO.print._at_.IO.println._at_.g.spec_0.spec_0 _x.4 a.1;
|
||||
return _x.5
|
||||
[Compiler.saveMono] size: 12
|
||||
def List.forM._at_.g.spec_1 as _y.1 _y.2 : EST.Out IO.Error lcAny (Prod PUnit Nat) :=
|
||||
cases as : EST.Out IO.Error lcAny (Prod PUnit Nat)
|
||||
| List.nil =>
|
||||
let _x.3 := PUnit.unit;
|
||||
let _x.4 := Prod.mk ◾ ◾ _x.3 _y.1;
|
||||
let _x.5 := @EST.Out.ok ◾ ◾ ◾ _x.4 _y.2;
|
||||
return _x.5
|
||||
| List.cons head.6 tail.7 =>
|
||||
let _x.8 := IO.println._at_.g.spec_0 head.6 _y.2;
|
||||
cases _x.8 : EST.Out IO.Error lcAny (Prod PUnit Nat)
|
||||
| EST.Out.ok a.9 a.10 =>
|
||||
let _x.11 := List.forM._at_.g.spec_1 tail.7 _y.1 a.10;
|
||||
return _x.11
|
||||
| EST.Out.error a.12 a.13 =>
|
||||
let _x.14 := @EST.Out.error ◾ ◾ ◾ a.12 a.13;
|
||||
return _x.14
|
||||
[Compiler.saveMono] size: 9
|
||||
def g ys a.1 : EST.Out IO.Error lcAny Nat :=
|
||||
let x := 0;
|
||||
let _x.2 := List.forM._at_.g.spec_1 ys x a.1;
|
||||
cases _x.2 : EST.Out IO.Error lcAny Nat
|
||||
| EST.Out.ok a.3 a.4 =>
|
||||
cases a.3 : EST.Out IO.Error lcAny Nat
|
||||
| Prod.mk fst.5 snd.6 =>
|
||||
let _x.7 := @EST.Out.ok ◾ ◾ ◾ snd.6 a.4;
|
||||
return _x.7
|
||||
| EST.Out.error a.8 a.9 =>
|
||||
let _x.10 := @EST.Out.error ◾ ◾ ◾ a.8 a.9;
|
||||
return _x.10
|
||||
|
||||
Reference in New Issue
Block a user