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:
Sebastian Ullrich 2022-08-20 20:48:02 +02:00
parent 5694dea36d
commit 6f0faa8000
35 changed files with 57415 additions and 36799 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -83,7 +83,7 @@ example : foo.default = (default, default) :=
rfl
```
-/
@[reducible] def inferInstance {α : Sort u} [i : α] : α := i
abbrev inferInstance {α : Sort u} [i : α] : α := i
set_option checkBinderAnnotations false in
/-- `inferInstanceAs α` synthesizes a value of any target type by typeclass
@ -97,7 +97,7 @@ does.) Example:
#check inferInstanceAs (Inhabited Nat) -- Inhabited Nat
```
-/
@[reducible] def inferInstanceAs (α : Sort u) [i : α] : α := i
abbrev inferInstanceAs (α : Sort u) [i : α] : α := i
set_option bootstrap.inductiveCheckResultingUniverse false in
/--
@ -3399,6 +3399,17 @@ abbrev SyntaxNodeKind := Name
/-! # Syntax AST -/
/--
Binding information resolved and stored at compile time of a syntax quotation.
Note: We do not statically know whether a syntax expects a namespace or term name,
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)
/--
Syntax objects used by the parser, macro expander, delaborator, etc.
-/

8
stage0/src/Lean/Compiler/CSE.lean generated
View file

@ -27,13 +27,13 @@ partial def visitCases (casesInfo : CasesInfo) (cases : Expr) : M Expr := do
partial def visitLambda (e : Expr) : M Expr :=
withNewScope do
let (as, e) ← Compiler.visitLambda e
let e ← mkLetUsingScope (← visitLet e)
let (as, e) ← Compiler.visitLambdaCore e
let e ← mkLetUsingScope (← visitLet e as)
mkLambda as e
partial def visitLet (e : Expr) : M Expr := do
partial def visitLet (e : Expr) (xs : Array Expr): M Expr := do
let saved ← get
try go e #[] finally set saved
try go e xs finally set saved
where
go (e : Expr) (xs : Array Expr) : M Expr := do
match e with

3
stage0/src/Lean/Compiler/Check.lean generated
View file

@ -14,6 +14,7 @@ Type checker for LCNF expressions
-/
structure Check.Config where
checkJpScope : Bool := true
terminalCasesOnly : Bool := true
structure Check.Context where
@ -69,7 +70,7 @@ where
checkBlock b (xs.push x)
| _ =>
if let some fvarId ← isJump? e then
unless (← read).jps.contains fvarId do
unless !cfg.checkJpScope || (← read).jps.contains fvarId do
/-
We cannot jump to join points defined out of the scope of a local function declaration.
For example, the following is an invalid LCNF.

84
stage0/src/Lean/Compiler/CompilerM.lean generated
View file

@ -21,6 +21,7 @@ structure CompilerM.State where
letFVars : Array Expr := #[]
/-- Next auxiliary variable suffix -/
nextIdx : Nat := 1
deriving Inhabited
abbrev CompilerM := StateRefT CompilerM.State CoreM
@ -56,6 +57,12 @@ def mkLetDecl (binderName : Name) (type : Expr) (value : Expr) (nonDep : Bool) :
modify fun s => { s with lctx := s.lctx.mkLetDecl fvarId binderName type value nonDep, letFVars := s.letFVars.push x }
return x
def mkFreshLetVarIdx : CompilerM Nat := do
modifyGet fun s => (s.nextIdx, { s with nextIdx := s.nextIdx +1 })
def mkAuxLetDeclName (prefixName := `_x) : CompilerM Name :=
return .num prefixName (← mkFreshLetVarIdx)
/--
Create a new auxiliary let declaration with value `e` The name of the
declaration is guaranteed to be unique.
@ -65,10 +72,7 @@ def mkAuxLetDecl (e : Expr) (prefixName := `_x) : CompilerM Expr := do
if e.isFVar then
return e
else
try
mkLetDecl (.num prefixName (← get).nextIdx) (← inferType e) e (nonDep := false)
finally
modify fun s => { s with nextIdx := s.nextIdx + 1 }
mkLetDecl (← mkAuxLetDeclName prefixName) (← inferType e) e (nonDep := false)
/--
Create an auxiliary let declaration with value `e`, that is a join point.
@ -97,7 +101,7 @@ let-declarations that are safe to unfold without producing code blowup, and join
Remark: user-facing names provided by users are preserved. We keep them as the prefix
of the new unique names.
-/
def ensureUniqueLetVarNames (e : Expr) : CoreM Expr :=
def ensureUniqueLetVarNamesCore (e : Expr) : StateRefT Nat CoreM Expr :=
let pre (e : Expr) : StateRefT Nat CoreM TransformStep := do
match e with
| .letE binderName type value body nonDep =>
@ -107,7 +111,34 @@ def ensureUniqueLetVarNames (e : Expr) : CoreM Expr :=
| _ => .num binderName idx
return .visit <| .letE binderName' type value body nonDep
| _ => return .visit e
Core.transform e pre |>.run' 1
Core.transform e pre
def ensureUniqueLetVarNames (e : Expr) : CompilerM Expr := do
let (e, nextIdx) ← ensureUniqueLetVarNamesCore e |>.run (← get).nextIdx
modify fun s => { s with nextIdx }
return e
/--
Move through all consecutive lambda abstractions at the top level of `e`.
Returning the body of the last one we find with **loose bound variables**.
Returns a tuple consisting of:
1. An `Array` of all the newly created free variables.
2. The body of the last lambda binder that was visited.
The caller is responsible for replacing the loose bound variables
with the newly created free variables.
See `visitLambda`.
-/
def visitLambdaCore (e : Expr) : CompilerM (Array Expr × Expr) :=
go e #[]
where
go (e : Expr) (fvars : Array Expr) := do
if let .lam binderName type body binderInfo := e then
let type := type.instantiateRev fvars
let fvar ← mkLocalDecl binderName type binderInfo
go body (fvars.push fvar)
else
return (fvars, e)
/--
Move through all consecutive lambda abstractions at the top level of `e`.
@ -117,16 +148,9 @@ Returns a tuple consisting of:
1. An `Array` of all the newly created free variables
2. The (fully instantiated) body of the last lambda binder that was visited
-/
def visitLambda (e : Expr) : CompilerM (Array Expr × Expr) :=
go e #[]
where
go (e : Expr) (fvars : Array Expr) := do
if let .lam binderName type body binderInfo := e then
let type := type.instantiateRev fvars
let fvar ← mkLocalDecl binderName type binderInfo
go body (fvars.push fvar)
else
return (fvars, e.instantiateRev fvars)
def visitLambda (e : Expr) : CompilerM (Array Expr × Expr) := do
let (fvars, e) ← visitLambdaCore e
return (fvars, e.instantiateRev fvars)
/--
Given an expression representing a `match` return a tuple consisting of:
@ -147,7 +171,7 @@ def visitMatch (cases : Expr) (casesInfo : CasesInfo) : CompilerM (Expr × Array
arms := arms.push (←visitLambda args[i]!).snd
return (motive, discrs, arms)
def withNewScopeImp (x : CompilerM α) : CompilerM α := do
@[inline] def withNewScopeImp (x : CompilerM α) : CompilerM α := do
let saved ← get
modify fun s => { s with letFVars := #[] }
try x
@ -155,7 +179,7 @@ def withNewScopeImp (x : CompilerM α) : CompilerM α := do
let saved := { saved with nextIdx := (← get).nextIdx }
set saved
def withNewScope [MonadFunctorT CompilerM m] (x : m α) : m α :=
@[inline] def withNewScope [MonadFunctorT CompilerM m] (x : m α) : m α :=
monadMap (m := CompilerM) withNewScopeImp x
/--
@ -175,10 +199,10 @@ class VisitLet (m : Type → Type) where
export VisitLet (visitLet)
def visitLetImp (e : Expr) (f : Name → Expr → CompilerM Expr) : CompilerM Expr :=
@[inline] def visitLetImp (e : Expr) (f : Name → Expr → CompilerM Expr) : CompilerM Expr :=
go e #[]
where
go (e : Expr) (fvars : Array Expr) : CompilerM Expr := do
@[specialize] go (e : Expr) (fvars : Array Expr) : CompilerM Expr := do
if let .letE binderName type value body nonDep := e then
let type := type.instantiateRev fvars
let value := value.instantiateRev fvars
@ -284,8 +308,8 @@ partial def attachJp (e : Expr) (jp : Expr) : CompilerM Expr := do
where
visitLambda (e : Expr) : ReaderT FVarIdSet CompilerM Expr := do
withNewScope do
let (as, e) ← Compiler.visitLambda e
let e ← mkLetUsingScope (← visitLet e #[])
let (as, e) ← Compiler.visitLambdaCore e
let e ← mkLetUsingScope (← visitLet e as)
mkLambda as e
visitCases (casesInfo : CasesInfo) (cases : Expr) : ReaderT FVarIdSet CompilerM Expr := do
@ -299,13 +323,19 @@ where
visitLet (e : Expr) (xs : Array Expr) : ReaderT FVarIdSet CompilerM Expr := do
match e with
| .letE binderName type value body nonDep =>
let mkDecl (type value : Expr) := do
let x ← mkLetDecl binderName type value nonDep
withReader (fun jps => if isJpBinderName binderName then jps.insert x.fvarId! else jps) do
visitLet body (xs.push x)
let type := type.instantiateRev xs
let mut value := value.instantiateRev xs
let value := value.instantiateRev xs
if isJpBinderName binderName then
value ← visitLambda value
let x ← mkLetDecl binderName type value nonDep
withReader (fun jps => if isJpBinderName binderName then jps.insert x.fvarId! else jps) do
visitLet body (xs.push x)
let value ← visitLambda value
-- Recall that the resulting type of join point may change after the attachment
let type ← inferType value
mkDecl type value
else
mkDecl type value
| _ =>
let e := e.instantiateRev xs
if let some fvarId ← isJump? e then

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

@ -166,7 +166,7 @@ Make sure all let-declarations have unique user-facing names.
See `Compiler.ensureUniqueLetVarNames`
-/
def Decl.ensureUniqueLetVarNames (decl : Decl) : CoreM Decl := do
return { decl with value := (← Compiler.ensureUniqueLetVarNames decl.value) }
return { decl with value := (← ensureUniqueLetVarNamesCore decl.value |>.run' 1) }
def Decl.getArity (decl : Decl) : Nat :=
getLambdaArity decl.value

5
stage0/src/Lean/Compiler/InferType.lean generated
View file

@ -69,11 +69,12 @@ mutual
match fType with
| .forallE _ _ b _ => fType := b
| _ =>
match fType.instantiateRevRange j i args |>.headBeta with
fType := fType.instantiateRevRange j i args |>.headBeta
match fType with
| .forallE _ _ b _ => j := i; fType := b
| _ =>
if fType.isAnyType then return anyTypeExpr
throwError "function expected{indentExpr f}"
throwError "function expected{indentExpr (mkAppN f args[:i])} : {fType}\nfunction type{indentExpr (← inferType f)}"
return fType.instantiateRevRange j args.size args |>.headBeta
partial def inferProjType (structName : Name) (idx : Nat) (s : Expr) : InferTypeM Expr := do

60
stage0/src/Lean/Compiler/JoinPoints.lean generated
View file

@ -74,14 +74,44 @@ end Visitors
namespace JoinPointFinder
abbrev M := StateRefT (Std.HashMap Name Nat) CompilerM
structure CandidateInfo where
arity : Nat
associated : Std.HashSet Name
deriving Inhabited
abbrev M := ReaderT (Option Name) StateRefT (Std.HashMap Name CandidateInfo) CompilerM
private def findCandidate? (name : Name) : M (Option CandidateInfo) := do
return (← get).find? name
private partial def eraseCandidate (name : Name) : M Unit := do
if let some info ← findCandidate? name then
modify (fun candidates => candidates.erase name)
info.associated.forM eraseCandidate
private partial def removeCandidatesContainedIn (e : Expr) : M Unit := do
let remover := fun fvarId => do
let some decl ← findDecl? fvarId | unreachable!
modify (fun jps? => jps?.erase decl.userName)
eraseCandidate decl.userName
forEachFVar e remover
private def addCandidate (name : Name) (arity : Nat) : M Unit := do
let cinfo := { arity, associated := .empty }
modify (fun cs => cs.insert name cinfo)
private def addDependency (src : Name) (target : Name) : M Unit := do
if let some targetInfo ← findCandidate? target then
modify (fun cs => cs.insert target { targetInfo with associated := targetInfo.associated.insert src })
else
eraseCandidate src
def declIsInScope (decl : LocalDecl) : CompilerM Bool := do
let fvars := (←getThe CompilerM.State).letFVars
fvars.anyM (fun fvar => do
let scopeDecl := (←findDecl? fvar.fvarId!).get!
return scopeDecl.userName == decl.userName
)
/--
Return a set of let declaration names inside of `e` that qualify as a join
point that is:
@ -92,25 +122,28 @@ Since declaration names are unique inside of LCNF the let bindings and
call sites can be uniquely identified by this.
-/
partial def findJoinPoints (e : Expr) : CompilerM (Array Name) := do
let (_, names) ← visitLambda goTailApp removeCandidatesContainedIn goLetValue e |>.run .empty
return names.toArray.map Prod.fst
let (_, state) ← visitLambda goTailApp removeCandidatesContainedIn goLetValue e |>.run none |>.run .empty
return state.toArray.map Prod.fst
where
goLetValue (userName : Name) (value : Expr) : M Expr := do
if let .lam .. := value then
withNewScope do
let (vars, body) ← Compiler.visitLambda value
modify (fun jps? => jps?.insert userName vars.size)
match value with
| .lam .. => withNewScope do
let (vars, body) ← Compiler.visitLambda value
addCandidate userName vars.size
withReader (fun _ => some userName) do
visitTails goTailApp removeCandidatesContainedIn goLetValue body
else
visitTails goTailApp removeCandidatesContainedIn goLetValue value
| _ => removeCandidatesContainedIn value
return value
goTailApp (fvarId : FVarId) (e : Expr) : M Unit := do
let some decl ← findDecl? fvarId | unreachable!
if let some jpArity := (←get).find? decl.userName then
if let some candidateInfo ← findCandidate? decl.userName then
let args := e.getAppNumArgs
if args != jpArity then
modify (fun jps? => jps?.erase decl.userName)
if args != candidateInfo.arity then
eraseCandidate decl.userName
else if let some upperCandidate ← read then
if !(←declIsInScope decl) then
addDependency decl.userName upperCandidate
end JoinPointFinder
@ -120,7 +153,6 @@ namespace JoinPointChecker
Throws an exception if `e` contains a join point.
-/
def containsNoJp (e : Expr) : CompilerM Unit := do
trace[Compiler.step] s!"Checking whether {e} contains jp"
let checker := fun fvarId => do
let some decl ← findDecl? fvarId | unreachable!
if decl.isJp then

33
stage0/src/Lean/Compiler/LCNF.lean generated
View file

@ -41,14 +41,16 @@ structure Context where
structure State where
/-- Local context containing the original Lean types (not LCNF ones). -/
lctx : LocalContext := {}
lctx : LocalContext := {}
/-- Local context containing Lean LCNF types. -/
lctx' : LocalContext := {}
letFVars : Array Expr := #[]
/-- Next auxiliary variable suffix -/
nextIdx : Nat := 1
/-- Cache from Lean regular expression to LCNF expression. -/
cache : PersistentExprMap Expr := {}
cache : Std.PHashMap (Expr × Bool) Expr := {}
/-- `toLCNFType` cache -/
typeCache : Std.PHashMap Expr Expr := {}
abbrev M := ReaderT Context $ StateRefT State CoreM
@ -67,13 +69,21 @@ def withNewRootScope (x : M α) : M α := do
try
withRoot true x
finally
let saved := { saved with nextIdx := (← get).nextIdx }
let saved := { saved with nextIdx := (← get).nextIdx, typeCache := (← get).typeCache }
set saved
def toLCNFType (type : Expr) : M Expr := do
match (← get).typeCache.find? type with
| some type' => return type'
| none =>
let type' ← liftMetaM <| Compiler.toLCNFType type
modify fun s => { s with typeCache := s.typeCache.insert type type' }
return type'
/-- Create a new local declaration using a Lean regular type. -/
def mkLocalDecl (binderName : Name) (type : Expr) (bi := BinderInfo.default) : M Expr := do
let fvarId ← mkFreshFVarId
let type' ← liftMetaM <| toLCNFType type
let type' ← toLCNFType type
modify fun s => { s with
lctx := s.lctx.mkLocalDecl fvarId binderName type bi
lctx' := s.lctx'.mkLocalDecl fvarId binderName type' bi
@ -170,7 +180,8 @@ partial def toLCNF (e : Expr) : CoreM Expr := do
return s.lctx'.mkLambda s.letFVars e
where
visitCore (e : Expr) : M Expr := withIncRecDepth do
if let some e := (← get).cache.find? e then
let key := (e, (← read).root)
if let some e := (← get).cache.find? key then
return e
let r ← match e with
| .app .. => visitApp e
@ -184,7 +195,7 @@ where
| .mvar .. => throwError "unexpected occurrence of metavariable in code generator{indentExpr e}"
| .bvar .. => unreachable!
| _ => pure e
modify fun s => { s with cache := s.cache.insert e r }
modify fun s => { s with cache := s.cache.insert key r }
return r
visit (e : Expr) : M Expr := withIncRecDepth do
@ -217,7 +228,7 @@ where
return mkConst ``lcErased
if (← liftMetaM <| Meta.isTypeFormerType type) then
/- Types and Type formers are not put into A-normal form -/
return (← liftMetaM <| toLCNFType e)
toLCNFType e
else
withRoot false <| visitCore e
@ -273,7 +284,7 @@ where
visitCases (casesInfo : CasesInfo) (e : Expr) : M Expr :=
etaIfUnderApplied e casesInfo.arity do
let mut args := e.getAppArgs
let mut resultType ← liftMetaM do toLCNFType (← Meta.inferType (mkAppN e.getAppFn args[:casesInfo.arity]))
let mut resultType ← toLCNFType (← liftMetaM do Meta.inferType (mkAppN e.getAppFn args[:casesInfo.arity]))
let mut discrTypes := #[]
for i in [:casesInfo.numParams] do
-- `cases` and `match` parameters are irrelevant at LCNF
@ -318,7 +329,7 @@ where
etaIfUnderApplied e arity do
let args := e.getAppArgs
let f := e.getAppFn
let recType ← liftMetaM do toLCNFType (← Meta.inferType (mkAppN f args[:arity]))
let recType ← toLCNFType (← liftMetaM do Meta.inferType (mkAppN f args[:arity]))
let minor := if e.isAppOf ``Eq.rec || e.isAppOf ``Eq.ndrec then args[3]! else args[5]!
let minor ← visit minor
let minorType ← inferType minor
@ -333,7 +344,7 @@ where
visitFalseRec (e : Expr) : M Expr :=
let arity := 2
etaIfUnderApplied e arity do
let type ← liftMetaM do toLCNFType (← Meta.inferType e)
let type ← toLCNFType (← liftMetaM do Meta.inferType e)
mkAuxLetDecl (← mkLcUnreachable type)
visitAndRec (e : Expr) : M Expr :=
@ -444,7 +455,7 @@ where
if (← liftMetaM <| Meta.isProp type <||> Meta.isTypeFormerType type) then
visitLet body (xs.push value)
else
let type' ← liftMetaM <| toLCNFType type
let type' ← toLCNFType type
let value' ← withRoot true <| visit value
let x ← mkLetDecl binderName type value type' value'
visitLet body (xs.push x)

33
stage0/src/Lean/Compiler/LCNFTypes.lean generated
View file

@ -93,18 +93,25 @@ partial def toLCNFType (type : Expr) : MetaM Expr := do
return b
else
return (Expr.lam n d (b.abstract #[x]) bi).eta
| .forallE n d b bi =>
withLocalDecl n bi d fun x => do
let borrowed := isMarkedBorrowed d
let mut d ← toLCNFType d
if borrowed then
d := markBorrowed d
let b ← toLCNFType (b.instantiate1 x)
return .forallE n d (b.abstract #[x]) bi
| .forallE .. => visitForall type #[]
| .app .. => type.withApp visitApp
| .fvar .. => visitApp type #[]
| _ => return anyTypeExpr
where
visitForall (e : Expr) (xs : Array Expr) : MetaM Expr := do
match e with
| .forallE n d b bi =>
let d := d.instantiateRev xs
withLocalDecl n bi d fun x => do
let borrowed := isMarkedBorrowed d
let mut d := (← toLCNFType d).abstract xs
if borrowed then
d := markBorrowed d
return .forallE n d (← visitForall b (xs.push x)) bi
| _ =>
let e ← toLCNFType (e.instantiateRev xs)
return e.abstract xs
visitApp (f : Expr) (args : Array Expr) := do
let fNew ← match f with
| .const declName us =>
@ -185,4 +192,14 @@ def isTypeFormerType (type : Expr) : Bool :=
| .forallE _ _ b _ => isTypeFormerType b
| _ => type.isAnyType
/--
`isClass? type` return `some ClsName` if the LCNF `type` is an instance of the class `ClsName`.
-/
def isClass? (type : Expr) : CoreM (Option Name) := do
let .const declName _ := type.getAppFn | return none
if isClass (← getEnv) declName then
return declName
else
return none
end Lean.Compiler

15
stage0/src/Lean/Compiler/Main.lean generated
View file

@ -8,6 +8,7 @@ import Lean.Compiler.TerminalCases
import Lean.Compiler.CSE
import Lean.Compiler.Stage1
import Lean.Compiler.Simp
import Lean.Compiler.PullLocalDecls
namespace Lean.Compiler
@ -53,12 +54,17 @@ def compileStage1Impl (declNames : Array Name) : CoreM (Array Decl) := do
checkpoint `init decls { terminalCasesOnly := false }
let decls ← decls.mapM (·.terminalCases)
checkpoint `terminalCases decls
let decls ← decls.mapM (·.simp)
checkpoint `simp decls
-- Remark: add simplification step here, `cse` is useful after simplification
decls.forM fun decl => do trace[Compiler.jp] "{decl.name}: {(← JoinPoints.JoinPointFinder.findJoinPoints decl.value |>.run' {})}"
let decls ← decls.mapM (·.pullInstances)
checkpoint `pullInstances decls
let decls ← decls.mapM (·.cse)
checkpoint `cse decls
let decls ← decls.mapM (·.simp)
checkpoint `simp decls
-- let decls ← decls.mapM (·.cse)
-- checkpoint `cse decls
saveStage1Decls decls
decls.forM fun decl => do trace[Compiler.stat] "{decl.name}: {← getLCNFSize decl.value}"
return decls
/--
@ -70,9 +76,12 @@ def compile (declNames : Array Name) : CoreM Unit := do profileitM Exception "co
builtin_initialize
registerTraceClass `Compiler
registerTraceClass `Compiler.stat
registerTraceClass `Compiler.init (inherited := true)
registerTraceClass `Compiler.terminalCases (inherited := true)
registerTraceClass `Compiler.simp (inherited := true)
registerTraceClass `Compiler.pullInstances (inherited := true)
registerTraceClass `Compiler.cse (inherited := true)
registerTraceClass `Compiler.jp
end Lean.Compiler

98
stage0/src/Lean/Compiler/PullLocalDecls.lean generated Normal file
View file

@ -0,0 +1,98 @@
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Compiler.CompilerM
import Lean.Compiler.Decl
namespace Lean.Compiler
namespace PullLocalDecls
structure Context where
isCandidateFn : LocalDecl → FVarIdSet → CompilerM Bool
structure State where
toPull : FVarIdSet := {}
abbrev PullM := ReaderT Context $ StateRefT State CompilerM
def dependsOn (e : Expr) (fvarIdSet : FVarIdSet) : Bool :=
Option.isSome <| e.find? fun e => e.isFVar && fvarIdSet.contains e.fvarId!
def mkLambda (xs : Array Expr) (letFVarsSavedSize : Nat) (e : Expr) : PullM Expr := do
let letFVars := (← getThe CompilerM.State).letFVars
let toPull := (← get).toPull
let mut xs := xs
let mut included : FVarIdSet := xs.foldl (init := {}) fun s x => s.insert x.fvarId!
let mut keep := #[] -- Variables to keep pulling
for i in [letFVarsSavedSize : letFVars.size] do
let y := letFVars[i]!
let some (.ldecl _ fvarId _ type value _) ← findDecl? y.fvarId! | unreachable!
if toPull.contains fvarId then
if !dependsOn value included && !dependsOn type included then
keep := keep.push y
continue
xs := xs.push y
included := included.insert fvarId
modifyThe CompilerM.State fun s => { s with letFVars := s.letFVars.shrink letFVarsSavedSize ++ keep }
-- Remark: we could remove all variables in `xs` from the local context
Compiler.mkLambda xs e
mutual
partial def visitLambda (e : Expr) (topLevel := false) : PullM Expr := do
let (as, e) ← Compiler.visitLambdaCore e
let letFVarsSavedSize := (← getThe CompilerM.State).letFVars.size
let e ← visitLet e as
if topLevel then
Compiler.mkLambda as (← mkLetUsingScope e)
else
mkLambda as letFVarsSavedSize e
partial def visitCases (casesInfo : CasesInfo) (cases : Expr) : PullM Expr := do
let mut args := cases.getAppArgs
for i in casesInfo.altsRange do
args ← args.modifyM i visitLambda
return mkAppN cases.getAppFn args
partial def visitLet (e : Expr) (xs : Array Expr := #[]) : PullM Expr := do
match e with
| .letE binderName type value body nonDep =>
let type := type.instantiateRev xs
let mut value := value.instantiateRev xs
if value.isLambda then
value ← visitLambda value
let x ← mkLetDecl binderName type value nonDep
let some localDecl ← findDecl? x.fvarId! | unreachable!
if (← (← read).isCandidateFn localDecl (← get).toPull) then
trace[Compiler.pullLocalDecls.candidate] "{x}"
modify fun s => { s with toPull := s.toPull.insert localDecl.fvarId }
visitLet body (xs.push x)
| e =>
let e := e.instantiateRev xs
if let some casesInfo ← isCasesApp? e then
visitCases casesInfo e
else
return e
end
end PullLocalDecls
def Decl.pullLocalDecls (decl : Decl) (isCandidateFn : LocalDecl → FVarIdSet → CompilerM Bool) : CoreM Decl :=
decl.mapValue fun value => PullLocalDecls.visitLambda value (topLevel := true) |>.run { isCandidateFn } |>.run' {}
def Decl.pullInstances (decl : Decl) : CoreM Decl :=
decl.pullLocalDecls fun localDecl candidates => do
if (← isClass? localDecl.type).isSome then
return true
else if let .proj _ _ (.fvar fvarId) := localDecl.value then
return candidates.contains fvarId
else
return false
builtin_initialize
registerTraceClass `Compiler.pullLocalDecls.candidate
end Lean.Compiler

544
stage0/src/Lean/Compiler/Simp.lean generated
View file

@ -27,146 +27,381 @@ partial def findExpr (e : Expr) (skipMData := true): CompilerM Expr := do
| .mdata _ e' => if skipMData then findExpr e' else return e
| _ => return e
inductive Occ where
| once
| many
deriving Repr, Inhabited
/--
Local function declaration statistics.
Remark: we use the `userName` as the key. Thus, `ensureUniqueLetVarNames`
must be used before collectin stastistics.
-/
structure InlineStats where
structure OccInfo where
/--
Mapping from local function name to the number of times it is used
in a declaration.
Mapping from local function name to occurrence information.
-/
numOccs : Std.HashMap Name Nat := {}
/--
Mapping from local function name to their LCNF size.
-/
size : Std.HashMap Name Nat := {}
map : Std.HashMap Name Occ := {}
deriving Inhabited
def InlineStats.format (s : InlineStats) : Format := Id.run do
def OccInfo.format (s : OccInfo) : Format := Id.run do
let mut result := Format.nil
for (k, n) in s.numOccs.toList do
let some size := s.size.find? k | pure ()
result := result ++ "\n" ++ f!"{k} ↦ {n}, {size}"
pure ()
for (k, n) in s.map.toList do
result := result ++ "\n" ++ f!"{k} ↦ {repr n}"
return result
def InlineStats.shouldInline (s : InlineStats) (k : Name) : Bool := Id.run do
let some numOccs := s.numOccs.find? k | return false
if numOccs == 1 then return true
let some sz := s.size.find? k | return false
return sz == 1
instance : ToFormat OccInfo where
format := OccInfo.format
instance : ToFormat InlineStats where
format := InlineStats.format
partial def collectInlineStats (e : Expr) : CoreM InlineStats := do
let ((_, s), _) ← goLambda e |>.run {} |>.run {}
return s
where
goLambda (e : Expr) : StateRefT InlineStats CompilerM Unit := do
withNewScope do
let (_, body) ← visitLambda e
go body
goValue (value : Expr) : StateRefT InlineStats CompilerM Unit := do
match value with
| .lam .. => goLambda value
| .app .. =>
match (← findLambda? value.getAppFn) with
| some localDecl =>
trace[Meta.debug] "found decl {localDecl.userName}"
if localDecl.value.isLambda then
let key := localDecl.userName
match (← get).numOccs.find? localDecl.userName with
| some numOccs => modify fun s => { s with numOccs := s.numOccs.insert key (numOccs + 1) }
| _ =>
let sz ← getLCNFSize localDecl.value
modify fun { numOccs, size } => { numOccs := numOccs.insert key 1, size := size.insert key sz }
| _ => pure ()
| _ => pure ()
go (e : Expr) : StateRefT InlineStats CompilerM Unit := do
match e with
| .letE .. =>
withNewScope do
let body ← visitLet e fun _ value => do goValue value; return value
go body
| e =>
if let some casesInfo ← isCasesApp? e then
let args := e.getAppArgs
for i in casesInfo.altsRange do
goLambda args[i]!
else
goValue e
def OccInfo.add (s : OccInfo) (key : Name) : OccInfo :=
match s with
| { map } =>
match map.find? key with
| some .once => { map := map.insert key .many }
| none => { map := map.insert key .once }
| _ => { map }
structure Config where
increaseFactor : Nat := 2
smallThreshold : Nat := 1
structure Context where
config : Config := {}
/--
Statistics for deciding whether to inline local function declarations.
-/
stats : InlineStats
/--
We only inline local declarations when `localInline` is `true`.
We set it to `false` when we are inlining a non local definition
that may have let-declarations whose names collide with the ones
stored at `stats`.
-/
localInline : Bool := true
structure State where
/--
(Approximate) occurence information for local function declarations.
-/
occInfo : OccInfo := {}
simplified : Bool := false
deriving Inhabited
abbrev SimpM := ReaderT Context $ StateRefT State CompilerM
/-- Ensure binder names are unique, and update occurrence information -/
partial def internalize (e : Expr) : SimpM Expr := do
visitLambda e
where
visitLambda (e : Expr) : SimpM Expr := do
withNewScope do
let (as, e) ← Compiler.visitLambdaCore e
let e ← mkLetUsingScope (← visitLet e as)
mkLambda as e
visitCases (casesInfo : CasesInfo) (cases : Expr) : SimpM Expr := do
let mut args := cases.getAppArgs
for i in casesInfo.altsRange do
args ← args.modifyM i visitLambda
return mkAppN cases.getAppFn args
visitValue (e : Expr) : SimpM Unit := do
if e.isApp then
match (← findLambda? e.getAppFn) with
| some localDecl =>
if localDecl.value.isLambda then
let key := localDecl.userName
modify fun s => { s with occInfo := s.occInfo.add key }
| _ => pure ()
visitLet (e : Expr) (xs : Array Expr) : SimpM Expr := do
match e with
| .letE binderName type value body nonDep =>
let idx ← mkFreshLetVarIdx
let binderName' := match binderName with
| .num p _ => .num p idx
| _ => .num binderName idx
let type := type.instantiateRev xs
let mut value := value.instantiateRev xs
if value.isLambda then
value ← visitLambda value
else
visitValue value
let x ← mkLetDecl binderName' type value nonDep
visitLet body (xs.push x)
| _ =>
let e := e.instantiateRev xs
if let some casesInfo ← isCasesApp? e then
visitCases casesInfo e
else
visitValue e
return e
def markSimplified : SimpM Unit :=
modify fun s => { s with simplified := true }
def shouldInline (localDecl : LocalDecl) : SimpM Bool :=
return (← read).localInline && (← read).stats.shouldInline localDecl.userName
def findCtor (e : Expr) : SimpM Expr := do
-- TODO: add support for mapping discriminants to constructors in branches
findExpr e
def inlineCandidate? (e : Expr) : SimpM (Option Nat) := do
/--
Try to simplify projections `.proj _ i s` where `s` is constructor.
-/
def simpProj? (e : Expr) : OptionT SimpM Expr := do
let .proj _ i s := e | failure
let s ← findCtor s
let some (ctorVal, args) := s.constructorApp? (← getEnv) | failure
markSimplified
return args[ctorVal.numParams + i]!
/--
Application over application.
```
let _x.i := f a
_x.i b
```
is simplified to `f a b`.
-/
def simpAppApp? (e : Expr) : OptionT SimpM Expr := do
guard e.isApp
let f := e.getAppFn
let arity ← match f with
| .const declName _ =>
unless hasInlineAttribute (← getEnv) declName do return none
-- TODO: check whether function is recursive or not.
-- We can skip the test and store function inline so far.
let some decl ← getStage1Decl? declName | return none
pure decl.getArity
| _ =>
match (← findLambda? f) with
| none => return none
| some localDecl =>
unless (← shouldInline localDecl) do return none
pure (getLambdaArity localDecl.value)
if e.getAppNumArgs < arity then return none
return e.getAppNumArgs - arity
guard f.isFVar
let f ← findExpr f
guard <| f.isApp || f.isConst
markSimplified
return mkAppN f e.getAppArgs
def shouldInlineLocal (localDecl : LocalDecl) : SimpM Bool := do
match (← get).occInfo.map.find? localDecl.userName with
| some .once => return true
| _ => lcnfSizeLe localDecl.value (← read).config.smallThreshold
structure InlineCandidateInfo where
isLocal : Bool
arity : Nat
/-- Value (lambda expression) of the function to be inlined. -/
value : Expr
def inlineCandidate? (e : Expr) : SimpM (Option InlineCandidateInfo) := do
let f := e.getAppFn
if let .const declName us ← findExpr f then
unless hasInlineAttribute (← getEnv) declName do return none
-- TODO: check whether function is recursive or not.
-- We can skip the test and store function inline so far.
let some decl ← getStage1Decl? declName | return none
let numArgs := e.getAppNumArgs
let arity := decl.getArity
if numArgs < arity then return none
/-
Recall that we use binder names to build `InlineStats`.
Thus, we use `ensureUniqueLetVarNames` to make sure there is no name collision.
-/
let value ← ensureUniqueLetVarNames (decl.value.instantiateLevelParams decl.levelParams us)
return some {
arity, value
isLocal := false
}
else if let some localDecl ← findLambda? f then
unless (← shouldInlineLocal localDecl) do return none
let numArgs := e.getAppNumArgs
let arity := getLambdaArity localDecl.value
if numArgs < arity then return none
let value ← ensureUniqueLetVarNames localDecl.value
return some {
arity, value
isLocal := true
}
else
return none
/--
If `e` if a free variable that expands to a valid LCNF terminal `let`-block expression `e'`,
return `e'`. -/
return `e'`.
-/
def expandTrivialExpr (e : Expr) : SimpM Expr := do
if e.isFVar then
let e' ← findExpr e
unless e'.isLambda do
if e != e' then markSimplified
return e'
if e != e' then
markSimplified
return e'
return e
mutual
/--
Given `value` of the form `let x_1 := v_1; ...; let x_n := v_n; e`,
return `let x_1; ...; let x_n := v_n; let y : type := e; body`.
partial def visitLambda (e : Expr) : SimpM Expr :=
This methods assumes `type` and `value` do not have loose bound variables.
Remark: `body` may have many loose bound variables, and the loose bound variables > 0
must be lifted by `n`.
-/
def mkFlatLet (y : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool := false) : Expr :=
go value 0
where
go (value : Expr) (i : Nat) : Expr :=
match value with
| .letE n t v b d => .letE n t v (go b (i+1)) d
| _ => .letE y type value (body.liftLooseBVars 1 i) nonDep
/--
Auxiliary function for projecting "type class dictionary access".
That is, we are trying to extract one of the type class instance elements.
Remark: We do not consider parent instances to be elements.
For example, suppose `e` is `_x_4.1`, and we have
```
_x_2 : Monad (ReaderT Bool (ExceptT String Id)) := @ReaderT.Monad Bool (ExceptT String Id) _x_1
_x_3 : Applicative (ReaderT Bool (ExceptT String Id)) := _x_2.1
_x_4 : Functor (ReaderT Bool (ExceptT String Id)) := _x_3.1
```
Then, we will expand `_x_4.1` since it corresponds to the `Functor` `map` element,
and its type is not a type class, but is of the form
```
{α β : Type u} → (α → β) → ...
```
In the example above, the compiler should not expand `_x_3.1` or `_x_2.1` because they are
type class applications: `Functor` and `Applicative` respectively.
By eagerly expanding them, we may produce inefficient and bloated code.
For example, we may be using `_x_3.1` to invoke a function that expects a `Functor` instance.
By expanding `_x_3.1` we will be just expanding the code that creates this instance.
-/
partial def inlineProjInst? (e : Expr) : OptionT SimpM Expr := do
let .proj _ _ s := e | failure
let sType ← inferType s
guard (← isClass? sType).isSome
let eType ← inferType e
guard (← isClass? eType).isNone
/-
We use `withNewScope` + `mkLetUsingScope` to filter the relevant let-declarations.
Recall that we are extracting only one of the type class elements.
-/
let value ← withNewScope do mkLetUsingScope (← visitProj e)
markSimplified
internalize value
where
visitProj (e : Expr) : OptionT SimpM Expr := do
let .proj _ i s := e | unreachable!
let s ← visit s
if let some (ctorVal, ctorArgs) := s.constructorApp? (← getEnv) then
return ctorArgs[ctorVal.numParams + i]!
else
failure
visit (e : Expr) : OptionT SimpM Expr := do
let e ← findExpr e
if e.isConstructorApp (← getEnv) then
return e
else if e.isProj then
/- We may have nested projections as we traverse parent classes. -/
visit (← visitProj e)
else
let .const declName us := e.getAppFn | failure
let some decl ← getStage1Decl? declName | failure
guard <| decl.getArity == e.getAppNumArgs
let value := decl.value.instantiateLevelParams decl.levelParams us
let value := value.beta e.getAppArgs
/-
Here, we just go inside of the let-declaration block without trying to simplify it.
Reason: a type class instannce may have many elements, and it does not make sense to simplify
all of them when we are extracting only one of them.
-/
let value ← Compiler.visitLet (m := SimpM) value fun _ value => return value
visit value
def betaReduce (e : Expr) (args : Array Expr) : SimpM Expr := do
-- TODO: add necessary casts
internalize (e.beta args)
/--
Try "cases on cases" simplification.
If `casesFn args` is of the form
```
casesOn _x.i
(... let _x.j₁ := ctorⱼ₁ ...; _jp.k _x.j₁)
...
(... let _x.jₙ := ctorⱼₙ ...; _jp.k _x.jₙ)
```
where `_jp.k` is a join point of the form
```
let _jp.k := fun y =>
casesOn y ...
```
Then, inline `_jp.k`. The idea is to force the `casesOn` application in the join point to
reduce after the inlining step.
Example: consider the following declarations
```
@[inline] def pred? (x : Nat) : Option Nat :=
match x with
| 0 => none
| x+1 => some x
def isZero (x : Nat) :=
match pred? x with
| some _ => false
| none => true
```
After inlining `pred?` in `isZero`, we have
```
let _jp.1 := fun y : Option Nat =>
casesOn y true (fun y => false)
casesOn x
(let _x.1 := none; _jp.1 _x.1)
(fun n => let _x.2 := some n; _jp.1 _x.2)
```
and this simplification is applicable, producing
```
casesOn x true (fun n => false)
```
-/
def simpCasesOnCases? (casesInfo : CasesInfo) (casesFn : Expr) (args : Array Expr) : OptionT SimpM Expr := do
let mut jpFirst? := none
for i in casesInfo.altsRange do
let alt := args[i]!
let jp ← isJpCtor? alt
if let some jpFirst := jpFirst? then
guard <| jp == jpFirst
else
let some localDecl ← findDecl? jp | failure
let .lam _ _ jpBody _ := localDecl.value | failure
guard (← isCasesApp? jpBody).isSome
jpFirst? := jp
let some jpFVarId := jpFirst? | failure
let some localDecl ← findDecl? jpFVarId | failure
let .lam _ _ jpBody _ := localDecl.value | failure
let mut args := args
for i in casesInfo.altsRange do
args := args.modify i (inlineJp · jpBody)
return mkAppN casesFn args
where
isJpCtor? (alt : Expr) : OptionT SimpM FVarId := do
match alt with
| .lam _ _ b _ => isJpCtor? b
| .letE _ _ v b _ => match b with
| .letE .. => isJpCtor? b
| .app (.fvar fvarId) (.bvar 0) =>
let some localDecl ← findDecl? fvarId | failure
guard localDecl.isJp
guard <| v.isConstructorApp (← getEnv)
return fvarId
| _ => failure
| _ => failure
inlineJp (alt : Expr) (jpBody : Expr) : Expr :=
match alt with
| .lam n d b bi => .lam n d (inlineJp b jpBody) bi
| .letE n t v b nd => .letE n t v (inlineJp b jpBody) nd
| _ => jpBody
mutual
/--
Simplify the given lambda expression.
If `checkEmptyTypes := true`, then return `fun a_i : t_i => lcUnreachable` if
`t_i` is the `Empty` type.
-/
partial def visitLambda (e : Expr) (checkEmptyTypes := false): SimpM Expr :=
withNewScope do
let (as, e) ← Compiler.visitLambda e
let e ← mkLetUsingScope (← visitLet e)
let (as, e) ← Compiler.visitLambdaCore e
if checkEmptyTypes then
for a in as do
if (← isEmptyType (← inferType a)) then
let e := e.instantiateRev as
let unreach ← mkLcUnreachable (← inferType e)
let r ← mkLambda as unreach
return r
let e ← mkLetUsingScope (← visitLet e as)
mkLambda as e
partial def visitCases (casesInfo : CasesInfo) (e : Expr) : SimpM Expr := do
let f := e.getAppFn
let mut args := e.getAppArgs
let major := args[casesInfo.discrsRange.stop - 1]!
let major ← findExpr major
@ -179,28 +414,12 @@ partial def visitCases (casesInfo : CasesInfo) (e : Expr) : SimpM Expr := do
assert! !alt.isLambda
markSimplified
visitLet alt
else if let some e ← simpCasesOnCases? casesInfo f args then
visitCases casesInfo e
else
for i in casesInfo.altsRange do
args ← args.modifyM i visitLambda
return mkAppN e.getAppFn args
partial def inlineApp (e : Expr) (jp? : Option Expr := none) : SimpM Expr := do
let f := e.getAppFn
trace[Compiler.simp.inline] "inlining {e}"
let value ← match f with
| .const declName us =>
let some decl ← getStage1Decl? declName | unreachable!
pure <| decl.value.instantiateLevelParams decl.levelParams us
| _ =>
let some localDecl ← findLambda? f | unreachable!
pure localDecl.value
let args := e.getAppArgs
let value := value.beta args
let value ← attachOptJp value jp?
assert! !value.isLambda
markSimplified
withReader (fun ctx => { ctx with localInline := !f.isConst }) do
visitLet value
args ← args.modifyM i (visitLambda · (checkEmptyTypes := true))
return mkAppN f args
/--
If `e` is an application that can be inlined, inline it.
@ -210,36 +429,46 @@ that need to instantiated with `xs`. That is, if `k? = some k`, then `k.instanti
is an expression without loose bound variables.
-/
partial def inlineApp? (e : Expr) (xs : Array Expr) (k? : Option Expr) : SimpM (Option Expr) := do
let some numExtraArgs ← inlineCandidate? e | return none
let some info ← inlineCandidate? e | return none
let args := e.getAppArgs
if k?.isNone && numExtraArgs == 0 then
-- Easy case, there is not continuation and `e` is not over applied
inlineApp e
let numArgs := args.size
trace[Compiler.simp.inline] "inlining {e}"
markSimplified
if k?.isNone && numArgs == info.arity then
/- Easy case, there is no continuation and `e` is not over applied -/
visitLet (← betaReduce info.value args)
else if (← onlyOneExitPoint info.value) then
/- If `info.value` has only one exit point, we don't need to create a new auxiliary join point -/
let mut value ← betaReduce info.value args[:info.arity]
if numArgs > info.arity then
let type ← inferType (mkAppN e.getAppFn args[:info.arity])
value := mkFlatLet (← mkAuxLetDeclName) type value (mkAppN (.bvar 0) args[info.arity:])
if let some k := k? then
let type ← inferType e
value := mkFlatLet (← mkAuxLetDeclName) type value k
visitLet value xs
else
/-
There is a continuation `k` or `e` is over applied.
If `e` is over applied, the extra arguments act as continuation.
If `e` is over applied, the extra arguments act as a continuation.
We create a new join point
```
let jp := fun y =>
let x := y <extra-arguments> -- if `e` is over applied
k
```
Recall that `visitLet` incorporates the current continuation
to the new join point `jp`.
-/
let toInline := mkAppN e.getAppFn args[:args.size - numExtraArgs]
/-
`toInline` is the application that is going to be inline
We create a new join point
```
let jp := fun y =>
let x := y <extra-arguments> -- if `e` is over applied
k
```
Recall that `visitLet` incorporates the current continuation
to the new join point `jp`.
-/
let jpDomain ← inferType toInline
let jpDomain ← inferType (mkAppN e.getAppFn args[:info.arity])
let binderName ← mkFreshUserName `_y
let jp ← withNewScope do
let y ← mkLocalDecl binderName jpDomain
let body ← if numExtraArgs == 0 then
let body ← if numArgs == info.arity then
visitLet k?.get! (xs.push y)
else
let x ← mkAuxLetDecl (mkAppN y args[args.size - numExtraArgs:])
let x ← mkAuxLetDecl (mkAppN y args[info.arity:])
if let some k := k? then
visitLet k (xs.push x)
else
@ -247,8 +476,13 @@ partial def inlineApp? (e : Expr) (xs : Array Expr) (k? : Option Expr) : SimpM (
let body ← mkLetUsingScope body
mkLambda #[y] body
let jp ← mkJpDeclIfNotSimple jp
/- Inline `toInline` and "go-to" `jp` with the result. -/
inlineApp toInline jp
let value ← betaReduce info.value args[:info.arity]
let value ← attachJp value jp
visitLet value
/-- Try to apply simple simplifications. -/
partial def simpValue? (e : Expr) : SimpM (Option Expr) :=
simpProj? e <|> simpAppApp? e <|> inlineProjInst? e
/--
Let-declaration basic block visitor. `e` may contain loose bound variables that
@ -260,6 +494,12 @@ partial def visitLet (e : Expr) (xs : Array Expr := #[]): SimpM Expr := do
let mut value := value.instantiateRev xs
if value.isLambda then
value ← visitLambda value
else if let some value' ← simpValue? value then
if value'.isLet then
let e := mkFlatLet binderName type value' body nonDep
let e ← visitLet e xs
return e
value := value'
if value.isFVar then
/- Eliminate `let _x_i := _x_j;` -/
markSimplified
@ -272,7 +512,9 @@ partial def visitLet (e : Expr) (xs : Array Expr := #[]): SimpM Expr := do
visitLet body (xs.push x)
| _ =>
let e := e.instantiateRev xs
if let some casesInfo ← isCasesApp? e then
if let some value ← simpValue? e then
visitLet value
else if let some casesInfo ← isCasesApp? e then
visitCases casesInfo e
else if let some e ← inlineApp? e #[] none then
return e
@ -282,18 +524,20 @@ end
end Simp
def Decl.simp? (decl : Decl) : CoreM (Option Decl) := do
let decl ← decl.ensureUniqueLetVarNames
let stats ← Simp.collectInlineStats decl.value
trace[Compiler.simp.inline.stats] "{decl.name}:{Format.nest 2 (format stats)}"
let (value, s) ← Simp.visitLambda decl.value |>.run { stats } |>.run { simplified := false } |>.run' {}
if s.simplified then
def Decl.simp? (decl : Decl) : Simp.SimpM (Option Decl) := do
let value ← Simp.internalize decl.value
trace[Compiler.simp.inline.occs] "{decl.name}:{Format.nest 2 (format (← get).occInfo)}"
trace[Compiler.simp.step] "{decl.name} :=\n{decl.value}"
let value ← Simp.visitLambda value
trace[Compiler.simp.step.new] "{decl.name} :=\n{value}"
trace[Compiler.simp.stat] "{decl.name}: {← getLCNFSize decl.value}"
if (← get).simplified then
return some { decl with value }
else
return none
partial def Decl.simp (decl : Decl) : CoreM Decl := do
if let some decl ← decl.simp? then
if let some decl ← decl.simp? |>.run {} |>.run' {} |>.run' {} then
-- TODO: bound number of steps?
decl.simp
else
@ -301,7 +545,9 @@ partial def Decl.simp (decl : Decl) : CoreM Decl := do
builtin_initialize
registerTraceClass `Compiler.simp.inline
registerTraceClass `Compiler.simp.stat
registerTraceClass `Compiler.simp.step
registerTraceClass `Compiler.simp.inline.stats
registerTraceClass `Compiler.simp.step.new
registerTraceClass `Compiler.simp.inline.occs
end Lean.Compiler
end Lean.Compiler

7
stage0/src/Lean/Compiler/Stage1.lean generated
View file

@ -36,7 +36,10 @@ def getStage1Decl? (declName : Name) : CoreM (Option Decl) := do
| some decl => return decl
| none =>
let info ← getConstInfo declName
let decls ← compileStage1 info.all.toArray
return decls.find? fun decl => declName == decl.name
if info.hasValue then
let decls ← compileStage1 info.all.toArray
return decls.find? fun decl => declName == decl.name
else
return none
end Lean.Compiler

4
stage0/src/Lean/Compiler/TerminalCases.lean generated
View file

@ -21,8 +21,8 @@ private partial def visitCases (casesInfo : CasesInfo) (cases : Expr) : Compiler
private partial def visitLambda (e : Expr) : CompilerM Expr :=
withNewScope do
let (as, e) ← Compiler.visitLambda e
let e ← mkLetUsingScope (← visitLet e #[])
let (as, e) ← Compiler.visitLambdaCore e
let e ← mkLetUsingScope (← visitLet e as)
mkLambda as e
private partial def visitLet (e : Expr) (fvars : Array Expr) : CompilerM Expr := do

53
stage0/src/Lean/Compiler/Util.lean generated
View file

@ -146,6 +146,30 @@ where
for i in casesInfo.altsRange do
go args[i]!
/--
Return `true` if `getLCNFSIze e ≤ n`
-/
partial def lcnfSizeLe (e : Expr) (n : Nat) : CoreM Bool := do
go e |>.run' 0
where
inc : StateRefT Nat CoreM Bool := do
modify (·+1)
return (← get) <= n
go (e : Expr) : StateRefT Nat CoreM Bool := do
match e with
| .lam _ _ b _ => go b
| .letE _ _ v b _ => inc <&&> go v <&&> go b
| _ =>
unless (← inc) do
return false
if let some casesInfo ← isCasesApp? e then
let args := e.getAppArgs
for i in casesInfo.altsRange do
unless (← go args[i]!) do
return false
return true
def getLambdaArity (e : Expr) :=
match e with
| .lam _ _ b _ => getLambdaArity b + 1
@ -175,4 +199,33 @@ def isJump? [Monad m] [MonadLCtx m] (e : Expr) : m (Option FVarId) := do
else
return none
/--
Return `true` if the LCNF expression has many exit points.
It assumes `cases` expressions only occur at the end of `let`-blocks.
That is, `terminalCases` has already been applied.
It also assumes that if contains a join point, then it has multiple
exit points. This is a reasonable assumption because the simplifier
inlines any join point that was used only once.
-/
def manyExitPoints (e : Expr) : CoreM Bool := do
match e with
| .lam _ _ b _ => manyExitPoints b
| .letE n _ _ b _ => pure (isJpBinderName n) <||> manyExitPoints b
| e => return (← isCasesApp? e).isSome
/--
Return `true` if the LCNF expression has only one exit point.
-/
def onlyOneExitPoint (e : Expr) : CoreM Bool := do
return !(← manyExitPoints e)
/--
Return `true` if `type` is an empty type.
Remark: this is an approximate test that only checks
whether `type == Empty`. It is good enough (and fast) for our purposes.
-/
def isEmptyType (type : Expr) : CoreM Bool :=
return type.isConstOf ``Empty
end Lean.Compiler

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

@ -99,6 +99,11 @@ def tryAddSyntaxNodeKindInfo (stx : Syntax) (k : SyntaxNodeKind) : TermElabM Uni
if (← getEnv).contains k then
addTermInfo' stx (← mkConstWithFreshMVarLevels k)
instance : Quote Syntax.Preresolved where
quote
| .namespace ns => Unhygienic.run ``(Syntax.Preresolved.namespace $(quote ns))
| .decl n fs => Unhygienic.run ``(Syntax.Preresolved.decl $(quote n) $(quote fs))
/-- Elaborate the content of a syntax quotation term -/
private partial def quoteSyntax : Syntax → TermElabM Term
| Syntax.ident _ rawVal val preresolved => do
@ -109,8 +114,9 @@ private partial def quoteSyntax : Syntax → TermElabM Term
let r ← resolveGlobalName val
-- extension of the paper algorithm: also store unique section variable names as top-level scopes
-- so they can be captured and used inside the section, but not outside
let r' := resolveSectionVariable (← read).sectionVars val
let preresolved := r ++ r' ++ preresolved
let r := r ++ resolveSectionVariable (← read).sectionVars val
let preresolved := r ++ preresolved
let preresolved := preresolved.map fun (n, fs) => Syntax.Preresolved.decl n fs
let val := quote val
-- `scp` is bound in stxQuot.expand
`(Syntax.ident info $(quote rawVal) (addMacroScope mainModule $val scp) $(quote preresolved))

37
stage0/src/Lean/Meta/InferType.lean generated
View file

@ -151,12 +151,6 @@ private def inferLambdaType (e : Expr) : MetaM Expr :=
let type ← inferType e
mkForallFVars xs type
@[inline] private def withLocalDecl' {α} (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α :=
savingCache do
let fvarId ← mkFreshFVarId
withReader (fun ctx => { ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi }) do
x (mkFVar fvarId)
def throwUnknownMVar {α} (mvarId : MVarId) : MetaM α :=
throwError "unknown metavariable '?{mvarId.name}'"
@ -377,16 +371,35 @@ def isType (e : Expr) : MetaM Bool := do
| .sort .. => return true
| _ => return false
@[inline] private def withLocalDecl' {α} (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α := do
let fvarId ← mkFreshFVarId
withReader (fun ctx => { ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi }) do
x (mkFVar fvarId)
def isTypeFormerTypeQuick : Expr → Bool
| .forallE _ _ b _ => isTypeFormerTypeQuick b
| .sort _ => true
| _ => false
/--
Return true iff `type` is `Sort _` or `As → Sort _`.
-/
partial def isTypeFormerType (type : Expr) : MetaM Bool := do
let type ← whnfD type
match type with
| .sort .. => return true
| .forallE n d b c =>
withLocalDecl' n c d fun fvar => isTypeFormerType (b.instantiate1 fvar)
| _ => return false
match isTypeFormerTypeQuick type with
| true => return true
| false => savingCache <| go type #[]
where
go (type : Expr) (xs : Array Expr) : MetaM Bool := do
match type with
| .sort .. => return true
| .forallE n d b c => withLocalDecl' n c (d.instantiateRev xs) fun x => go b (xs.push x)
| _ =>
let type ← whnfD (type.instantiateRev xs)
match type with
| .sort .. => return true
| .forallE .. => go type #[]
| _ => return false
/--
Return true iff `e : Sort _` or `e : (forall As, Sort _)`.

13
stage0/src/Std/Data/HashSet.lean generated
View file

@ -46,6 +46,12 @@ def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
@[inline] def fold {δ : Type w} (f : δ → α → δ) (d : δ) (m : HashSetImp α) : δ :=
foldBuckets m.buckets d f
@[inline] def forBucketsM {m : Type w → Type w} [Monad m] (data : HashSetBucket α) (f : α → m PUnit) : m PUnit :=
data.val.forM fun as=> as.forM f
@[inline] def forM {m : Type w → Type w} [Monad m] (f : α → m PUnit) (h : HashSetImp α) : m PUnit :=
forBucketsM h.buckets f
def find? [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
match m with
| ⟨_, buckets⟩ =>
@ -149,6 +155,13 @@ variable {α : Type u} {_ : BEq α} {_ : Hashable α}
match m with
| ⟨ m, _ ⟩ => m.fold f init
@[inline] def forM {m : Type w → Type w} [Monad m] (h : HashSet α) (f : α → m PUnit) : m PUnit :=
match h with
| ⟨h, _⟩ => h.forM f
instance : ForM m (HashSet α) α where
forM := HashSet.forM
@[inline] def size (m : HashSet α) : Nat :=
match m with
| ⟨ {size := sz, ..}, _ ⟩ => sz

681
stage0/stdlib/Lean/Compiler/CSE.c generated
View file

@ -16,30 +16,24 @@ extern "C" {
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
static lean_object* l_Lean_Compiler_CSE_State_map___default___closed__1;
lean_object* l_Lean_Compiler_mkLetUsingScope(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitLet(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitLet(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_CSE_State_map___default___closed__2;
lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_Decl_mapValue(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
LEAN_EXPORT lean_object* l_ReaderT_bind___at_Lean_Compiler_CSE_visitLambda___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_withNewScopeImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Compiler_ToLCNF_toLCNF_visitCore___spec__7(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_CSE_visitLet___closed__1;
extern lean_object* l_Lean_levelZero;
lean_object* lean_nat_add(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_CSE_visitLambda___closed__1;
lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Compiler_ToLCNF_toLCNFType___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
lean_object* l_StateRefT_x27_lift___rarg___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitLambda___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_CSE_visitCases___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_mkLetDecl(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ReaderT_bind___at_Lean_Compiler_CSE_visitLambda___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitCases(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_CSE_visitCases___closed__1;
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
@ -50,16 +44,16 @@ lean_object* l_Lean_Expr_sort___override(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_Decl_cse___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_Decl_cse___closed__1;
uint8_t l_Lean_Expr_isLambda(lean_object*);
lean_object* l_Std_PersistentHashMap_insert___at_Lean_Compiler_ToLCNF_toLCNF_visitCore___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_visitLambdaCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_CSE_State_map___default___closed__3;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
uint8_t l_Lean_Compiler_isJpBinderName(lean_object*);
lean_object* l_Lean_Compiler_mkLambda(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitLet_go___lambda__2(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_Decl_cse(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_visitLambda___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_instantiate_rev(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_insert___at_Lean_Compiler_ToLCNF_toLCNFType___spec__4(lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_array(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_State_map___default;
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitLet_go___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -67,7 +61,6 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitLet_go(lean_object*, lean_obje
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitLambda(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn(lean_object*);
lean_object* l_Lean_Compiler_isCasesApp_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_withNewScope___at_Lean_Compiler_CSE_visitLambda___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitLet_go___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_CSE_visitCases___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
@ -135,7 +128,7 @@ x_17 = lean_ctor_get(x_15, 1);
lean_inc(x_17);
lean_dec(x_15);
lean_inc(x_6);
x_18 = l_Std_PersistentHashMap_find_x3f___at_Lean_Compiler_ToLCNF_toLCNF_visitCore___spec__7(x_16, x_6);
x_18 = l_Std_PersistentHashMap_find_x3f___at_Lean_Compiler_ToLCNF_toLCNFType___spec__1(x_16, x_6);
if (lean_obj_tag(x_18) == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23;
@ -165,7 +158,7 @@ x_28 = lean_ctor_get(x_26, 1);
lean_inc(x_28);
lean_dec(x_26);
lean_inc(x_21);
x_29 = l_Std_PersistentHashMap_insert___at_Lean_Compiler_ToLCNF_toLCNF_visitCore___spec__1(x_27, x_6, x_21);
x_29 = l_Std_PersistentHashMap_insert___at_Lean_Compiler_ToLCNF_toLCNFType___spec__4(x_27, x_6, x_21);
x_30 = lean_st_ref_set(x_8, x_29, x_28);
x_31 = lean_ctor_get(x_30, 1);
lean_inc(x_31);
@ -573,218 +566,480 @@ return x_32;
}
}
}
LEAN_EXPORT lean_object* l_ReaderT_bind___at_Lean_Compiler_CSE_visitLambda___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8;
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_8 = lean_apply_5(x_1, x_3, x_4, x_5, x_6, x_7);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_8, 1);
lean_inc(x_10);
lean_dec(x_8);
x_11 = lean_apply_6(x_2, x_9, x_3, x_4, x_5, x_6, x_10);
return x_11;
}
else
{
uint8_t x_12;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_12 = !lean_is_exclusive(x_8);
if (x_12 == 0)
{
return x_8;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = lean_ctor_get(x_8, 0);
x_14 = lean_ctor_get(x_8, 1);
lean_inc(x_14);
lean_inc(x_13);
lean_dec(x_8);
x_15 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_15, 0, x_13);
lean_ctor_set(x_15, 1, x_14);
return x_15;
}
}
}
}
LEAN_EXPORT lean_object* l_ReaderT_bind___at_Lean_Compiler_CSE_visitLambda___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Compiler_CSE_visitLambda___spec__1___rarg), 7, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_withNewScope___at_Lean_Compiler_CSE_visitLambda___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8;
x_7 = lean_apply_1(x_1, x_2);
x_8 = l_Lean_Compiler_withNewScopeImp___rarg(x_7, x_3, x_4, x_5, x_6);
return x_8;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitLambda___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_1, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_1, 1);
lean_inc(x_8);
lean_dec(x_1);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_9 = l_Lean_Compiler_CSE_visitLet(x_8, x_2, x_3, x_4, x_5, x_6);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_12 = l_Lean_Compiler_mkLetUsingScope(x_10, x_3, x_4, x_5, x_11);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
x_14 = lean_ctor_get(x_12, 1);
lean_inc(x_14);
lean_dec(x_12);
x_15 = l_Lean_Compiler_mkLambda(x_7, x_13, x_3, x_4, x_5, x_14);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_7);
return x_15;
}
else
{
uint8_t x_16;
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_16 = !lean_is_exclusive(x_12);
if (x_16 == 0)
{
return x_12;
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_17 = lean_ctor_get(x_12, 0);
x_18 = lean_ctor_get(x_12, 1);
lean_inc(x_18);
lean_inc(x_17);
lean_dec(x_12);
x_19 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_18);
return x_19;
}
}
}
else
{
uint8_t x_20;
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_20 = !lean_is_exclusive(x_9);
if (x_20 == 0)
{
return x_9;
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_9, 0);
x_22 = lean_ctor_get(x_9, 1);
lean_inc(x_22);
lean_inc(x_21);
lean_dec(x_9);
x_23 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_23, 0, x_21);
lean_ctor_set(x_23, 1, x_22);
return x_23;
}
}
}
}
static lean_object* _init_l_Lean_Compiler_CSE_visitLambda___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Compiler_CSE_visitLambda___lambda__1), 6, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitLambda(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_7 = lean_alloc_closure((void*)(l_Lean_Compiler_visitLambda___boxed), 5, 1);
lean_closure_set(x_7, 0, x_1);
x_8 = lean_alloc_closure((void*)(l_StateRefT_x27_lift___rarg___boxed), 2, 1);
lean_closure_set(x_8, 0, x_7);
x_9 = l_Lean_Compiler_CSE_visitLambda___closed__1;
x_10 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Compiler_CSE_visitLambda___spec__1___rarg), 7, 2);
lean_closure_set(x_10, 0, x_8);
lean_closure_set(x_10, 1, x_9);
x_11 = l_Lean_Compiler_withNewScope___at_Lean_Compiler_CSE_visitLambda___spec__2(x_10, x_2, x_3, x_4, x_5, x_6);
return x_11;
}
}
static lean_object* _init_l_Lean_Compiler_CSE_visitLet___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitLet(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitLambda(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; uint8_t x_45;
x_7 = lean_st_ref_get(x_5, x_6);
x_8 = lean_ctor_get(x_7, 1);
lean_inc(x_8);
lean_dec(x_7);
x_9 = lean_st_ref_get(x_2, x_8);
x_9 = lean_st_ref_get(x_3, x_8);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = l_Lean_Compiler_CSE_visitLet___closed__1;
x_40 = lean_st_ref_get(x_5, x_11);
x_41 = lean_ctor_get(x_40, 1);
lean_inc(x_41);
lean_dec(x_40);
x_42 = lean_st_ref_take(x_3, x_41);
x_43 = lean_ctor_get(x_42, 0);
lean_inc(x_43);
x_44 = lean_ctor_get(x_42, 1);
lean_inc(x_44);
lean_dec(x_42);
x_45 = !lean_is_exclusive(x_43);
if (x_45 == 0)
{
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55;
x_46 = lean_ctor_get(x_43, 1);
lean_dec(x_46);
x_47 = l_Lean_Compiler_CSE_visitLambda___closed__1;
lean_ctor_set(x_43, 1, x_47);
x_48 = lean_st_ref_set(x_3, x_43, x_44);
x_49 = lean_ctor_get(x_48, 1);
lean_inc(x_49);
lean_dec(x_48);
x_50 = l_Lean_Compiler_visitLambdaCore(x_1, x_3, x_4, x_5, x_49);
x_51 = lean_ctor_get(x_50, 0);
lean_inc(x_51);
x_52 = lean_ctor_get(x_50, 1);
lean_inc(x_52);
lean_dec(x_50);
x_53 = lean_ctor_get(x_51, 0);
lean_inc(x_53);
x_54 = lean_ctor_get(x_51, 1);
lean_inc(x_54);
lean_dec(x_51);
lean_inc(x_5);
lean_inc(x_2);
x_13 = l_Lean_Compiler_CSE_visitLet_go(x_1, x_12, x_2, x_3, x_4, x_5, x_11);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_53);
x_55 = l_Lean_Compiler_CSE_visitLet(x_54, x_53, x_2, x_3, x_4, x_5, x_52);
if (lean_obj_tag(x_55) == 0)
{
lean_object* x_56; lean_object* x_57; lean_object* x_58;
x_56 = lean_ctor_get(x_55, 0);
lean_inc(x_56);
x_57 = lean_ctor_get(x_55, 1);
lean_inc(x_57);
lean_dec(x_55);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_58 = l_Lean_Compiler_mkLetUsingScope(x_56, x_3, x_4, x_5, x_57);
if (lean_obj_tag(x_58) == 0)
{
lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; uint8_t x_71;
x_59 = lean_ctor_get(x_58, 0);
lean_inc(x_59);
x_60 = lean_ctor_get(x_58, 1);
lean_inc(x_60);
lean_dec(x_58);
x_61 = l_Lean_Compiler_mkLambda(x_53, x_59, x_3, x_4, x_5, x_60);
lean_dec(x_4);
lean_dec(x_53);
x_62 = lean_ctor_get(x_61, 0);
lean_inc(x_62);
x_63 = lean_ctor_get(x_61, 1);
lean_inc(x_63);
lean_dec(x_61);
x_64 = lean_st_ref_get(x_5, x_63);
x_65 = lean_ctor_get(x_64, 1);
lean_inc(x_65);
lean_dec(x_64);
x_66 = lean_st_ref_get(x_3, x_65);
x_67 = lean_ctor_get(x_66, 0);
lean_inc(x_67);
x_68 = lean_ctor_get(x_66, 1);
lean_inc(x_68);
lean_dec(x_66);
x_69 = lean_ctor_get(x_10, 0);
lean_inc(x_69);
x_70 = lean_ctor_get(x_10, 1);
lean_inc(x_70);
lean_dec(x_10);
x_71 = !lean_is_exclusive(x_67);
if (x_71 == 0)
{
lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; uint8_t x_77;
x_72 = lean_ctor_get(x_67, 1);
lean_dec(x_72);
x_73 = lean_ctor_get(x_67, 0);
lean_dec(x_73);
lean_ctor_set(x_67, 1, x_70);
lean_ctor_set(x_67, 0, x_69);
x_74 = lean_st_ref_get(x_5, x_68);
lean_dec(x_5);
x_75 = lean_ctor_get(x_74, 1);
lean_inc(x_75);
lean_dec(x_74);
x_76 = lean_st_ref_set(x_3, x_67, x_75);
lean_dec(x_3);
x_77 = !lean_is_exclusive(x_76);
if (x_77 == 0)
{
lean_object* x_78;
x_78 = lean_ctor_get(x_76, 0);
lean_dec(x_78);
lean_ctor_set(x_76, 0, x_62);
return x_76;
}
else
{
lean_object* x_79; lean_object* x_80;
x_79 = lean_ctor_get(x_76, 1);
lean_inc(x_79);
lean_dec(x_76);
x_80 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_80, 0, x_62);
lean_ctor_set(x_80, 1, x_79);
return x_80;
}
}
else
{
lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88;
x_81 = lean_ctor_get(x_67, 2);
lean_inc(x_81);
lean_dec(x_67);
x_82 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_82, 0, x_69);
lean_ctor_set(x_82, 1, x_70);
lean_ctor_set(x_82, 2, x_81);
x_83 = lean_st_ref_get(x_5, x_68);
lean_dec(x_5);
x_84 = lean_ctor_get(x_83, 1);
lean_inc(x_84);
lean_dec(x_83);
x_85 = lean_st_ref_set(x_3, x_82, x_84);
lean_dec(x_3);
x_86 = lean_ctor_get(x_85, 1);
lean_inc(x_86);
if (lean_is_exclusive(x_85)) {
lean_ctor_release(x_85, 0);
lean_ctor_release(x_85, 1);
x_87 = x_85;
} else {
lean_dec_ref(x_85);
x_87 = lean_box(0);
}
if (lean_is_scalar(x_87)) {
x_88 = lean_alloc_ctor(0, 2, 0);
} else {
x_88 = x_87;
}
lean_ctor_set(x_88, 0, x_62);
lean_ctor_set(x_88, 1, x_86);
return x_88;
}
}
else
{
lean_object* x_89; lean_object* x_90;
lean_dec(x_53);
lean_dec(x_4);
x_89 = lean_ctor_get(x_58, 0);
lean_inc(x_89);
x_90 = lean_ctor_get(x_58, 1);
lean_inc(x_90);
lean_dec(x_58);
x_12 = x_89;
x_13 = x_90;
goto block_39;
}
}
else
{
lean_object* x_91; lean_object* x_92;
lean_dec(x_53);
lean_dec(x_4);
x_91 = lean_ctor_get(x_55, 0);
lean_inc(x_91);
x_92 = lean_ctor_get(x_55, 1);
lean_inc(x_92);
lean_dec(x_55);
x_12 = x_91;
x_13 = x_92;
goto block_39;
}
}
else
{
lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104;
x_93 = lean_ctor_get(x_43, 0);
x_94 = lean_ctor_get(x_43, 2);
lean_inc(x_94);
lean_inc(x_93);
lean_dec(x_43);
x_95 = l_Lean_Compiler_CSE_visitLambda___closed__1;
x_96 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_96, 0, x_93);
lean_ctor_set(x_96, 1, x_95);
lean_ctor_set(x_96, 2, x_94);
x_97 = lean_st_ref_set(x_3, x_96, x_44);
x_98 = lean_ctor_get(x_97, 1);
lean_inc(x_98);
lean_dec(x_97);
x_99 = l_Lean_Compiler_visitLambdaCore(x_1, x_3, x_4, x_5, x_98);
x_100 = lean_ctor_get(x_99, 0);
lean_inc(x_100);
x_101 = lean_ctor_get(x_99, 1);
lean_inc(x_101);
lean_dec(x_99);
x_102 = lean_ctor_get(x_100, 0);
lean_inc(x_102);
x_103 = lean_ctor_get(x_100, 1);
lean_inc(x_103);
lean_dec(x_100);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_102);
x_104 = l_Lean_Compiler_CSE_visitLet(x_103, x_102, x_2, x_3, x_4, x_5, x_101);
if (lean_obj_tag(x_104) == 0)
{
lean_object* x_105; lean_object* x_106; lean_object* x_107;
x_105 = lean_ctor_get(x_104, 0);
lean_inc(x_105);
x_106 = lean_ctor_get(x_104, 1);
lean_inc(x_106);
lean_dec(x_104);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_107 = l_Lean_Compiler_mkLetUsingScope(x_105, x_3, x_4, x_5, x_106);
if (lean_obj_tag(x_107) == 0)
{
lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128;
x_108 = lean_ctor_get(x_107, 0);
lean_inc(x_108);
x_109 = lean_ctor_get(x_107, 1);
lean_inc(x_109);
lean_dec(x_107);
x_110 = l_Lean_Compiler_mkLambda(x_102, x_108, x_3, x_4, x_5, x_109);
lean_dec(x_4);
lean_dec(x_102);
x_111 = lean_ctor_get(x_110, 0);
lean_inc(x_111);
x_112 = lean_ctor_get(x_110, 1);
lean_inc(x_112);
lean_dec(x_110);
x_113 = lean_st_ref_get(x_5, x_112);
x_114 = lean_ctor_get(x_113, 1);
lean_inc(x_114);
lean_dec(x_113);
x_115 = lean_st_ref_get(x_3, x_114);
x_116 = lean_ctor_get(x_115, 0);
lean_inc(x_116);
x_117 = lean_ctor_get(x_115, 1);
lean_inc(x_117);
lean_dec(x_115);
x_118 = lean_ctor_get(x_10, 0);
lean_inc(x_118);
x_119 = lean_ctor_get(x_10, 1);
lean_inc(x_119);
lean_dec(x_10);
x_120 = lean_ctor_get(x_116, 2);
lean_inc(x_120);
if (lean_is_exclusive(x_116)) {
lean_ctor_release(x_116, 0);
lean_ctor_release(x_116, 1);
lean_ctor_release(x_116, 2);
x_121 = x_116;
} else {
lean_dec_ref(x_116);
x_121 = lean_box(0);
}
if (lean_is_scalar(x_121)) {
x_122 = lean_alloc_ctor(0, 3, 0);
} else {
x_122 = x_121;
}
lean_ctor_set(x_122, 0, x_118);
lean_ctor_set(x_122, 1, x_119);
lean_ctor_set(x_122, 2, x_120);
x_123 = lean_st_ref_get(x_5, x_117);
lean_dec(x_5);
x_124 = lean_ctor_get(x_123, 1);
lean_inc(x_124);
lean_dec(x_123);
x_125 = lean_st_ref_set(x_3, x_122, x_124);
lean_dec(x_3);
x_126 = lean_ctor_get(x_125, 1);
lean_inc(x_126);
if (lean_is_exclusive(x_125)) {
lean_ctor_release(x_125, 0);
lean_ctor_release(x_125, 1);
x_127 = x_125;
} else {
lean_dec_ref(x_125);
x_127 = lean_box(0);
}
if (lean_is_scalar(x_127)) {
x_128 = lean_alloc_ctor(0, 2, 0);
} else {
x_128 = x_127;
}
lean_ctor_set(x_128, 0, x_111);
lean_ctor_set(x_128, 1, x_126);
return x_128;
}
else
{
lean_object* x_129; lean_object* x_130;
lean_dec(x_102);
lean_dec(x_4);
x_129 = lean_ctor_get(x_107, 0);
lean_inc(x_129);
x_130 = lean_ctor_get(x_107, 1);
lean_inc(x_130);
lean_dec(x_107);
x_12 = x_129;
x_13 = x_130;
goto block_39;
}
}
else
{
lean_object* x_131; lean_object* x_132;
lean_dec(x_102);
lean_dec(x_4);
x_131 = lean_ctor_get(x_104, 0);
lean_inc(x_131);
x_132 = lean_ctor_get(x_104, 1);
lean_inc(x_132);
lean_dec(x_104);
x_12 = x_131;
x_13 = x_132;
goto block_39;
}
}
block_39:
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21;
x_14 = lean_st_ref_get(x_5, x_13);
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
lean_dec(x_14);
x_16 = lean_st_ref_get(x_3, x_15);
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_ctor_get(x_16, 1);
lean_inc(x_18);
lean_dec(x_16);
x_19 = lean_ctor_get(x_10, 0);
lean_inc(x_19);
x_20 = lean_ctor_get(x_10, 1);
lean_inc(x_20);
lean_dec(x_10);
x_21 = !lean_is_exclusive(x_17);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27;
x_22 = lean_ctor_get(x_17, 1);
lean_dec(x_22);
x_23 = lean_ctor_get(x_17, 0);
lean_dec(x_23);
lean_ctor_set(x_17, 1, x_20);
lean_ctor_set(x_17, 0, x_19);
x_24 = lean_st_ref_get(x_5, x_18);
lean_dec(x_5);
x_25 = lean_ctor_get(x_24, 1);
lean_inc(x_25);
lean_dec(x_24);
x_26 = lean_st_ref_set(x_3, x_17, x_25);
lean_dec(x_3);
x_27 = !lean_is_exclusive(x_26);
if (x_27 == 0)
{
lean_object* x_28;
x_28 = lean_ctor_get(x_26, 0);
lean_dec(x_28);
lean_ctor_set_tag(x_26, 1);
lean_ctor_set(x_26, 0, x_12);
return x_26;
}
else
{
lean_object* x_29; lean_object* x_30;
x_29 = lean_ctor_get(x_26, 1);
lean_inc(x_29);
lean_dec(x_26);
x_30 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_30, 0, x_12);
lean_ctor_set(x_30, 1, x_29);
return x_30;
}
}
else
{
lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38;
x_31 = lean_ctor_get(x_17, 2);
lean_inc(x_31);
lean_dec(x_17);
x_32 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_32, 0, x_19);
lean_ctor_set(x_32, 1, x_20);
lean_ctor_set(x_32, 2, x_31);
x_33 = lean_st_ref_get(x_5, x_18);
lean_dec(x_5);
x_34 = lean_ctor_get(x_33, 1);
lean_inc(x_34);
lean_dec(x_33);
x_35 = lean_st_ref_set(x_3, x_32, x_34);
lean_dec(x_3);
x_36 = lean_ctor_get(x_35, 1);
lean_inc(x_36);
if (lean_is_exclusive(x_35)) {
lean_ctor_release(x_35, 0);
lean_ctor_release(x_35, 1);
x_37 = x_35;
} else {
lean_dec_ref(x_35);
x_37 = lean_box(0);
}
if (lean_is_scalar(x_37)) {
x_38 = lean_alloc_ctor(1, 2, 0);
} else {
x_38 = x_37;
lean_ctor_set_tag(x_38, 1);
}
lean_ctor_set(x_38, 0, x_12);
lean_ctor_set(x_38, 1, x_36);
return x_38;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_CSE_visitLet(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_8 = lean_st_ref_get(x_6, x_7);
x_9 = lean_ctor_get(x_8, 1);
lean_inc(x_9);
lean_dec(x_8);
x_10 = lean_st_ref_get(x_3, x_9);
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_10, 1);
lean_inc(x_12);
lean_dec(x_10);
lean_inc(x_6);
lean_inc(x_3);
x_13 = l_Lean_Compiler_CSE_visitLet_go(x_1, x_2, x_3, x_4, x_5, x_6, x_12);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19;
@ -793,13 +1048,13 @@ lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
lean_inc(x_15);
lean_dec(x_13);
x_16 = lean_st_ref_get(x_5, x_15);
lean_dec(x_5);
x_16 = lean_st_ref_get(x_6, x_15);
lean_dec(x_6);
x_17 = lean_ctor_get(x_16, 1);
lean_inc(x_17);
lean_dec(x_16);
x_18 = lean_st_ref_set(x_2, x_10, x_17);
lean_dec(x_2);
x_18 = lean_st_ref_set(x_3, x_11, x_17);
lean_dec(x_3);
x_19 = !lean_is_exclusive(x_18);
if (x_19 == 0)
{
@ -829,13 +1084,13 @@ lean_inc(x_23);
x_24 = lean_ctor_get(x_13, 1);
lean_inc(x_24);
lean_dec(x_13);
x_25 = lean_st_ref_get(x_5, x_24);
lean_dec(x_5);
x_25 = lean_st_ref_get(x_6, x_24);
lean_dec(x_6);
x_26 = lean_ctor_get(x_25, 1);
lean_inc(x_26);
lean_dec(x_25);
x_27 = lean_st_ref_set(x_2, x_10, x_26);
lean_dec(x_2);
x_27 = lean_st_ref_set(x_3, x_11, x_26);
lean_dec(x_3);
x_28 = !lean_is_exclusive(x_27);
if (x_28 == 0)
{
@ -1006,8 +1261,6 @@ l_Lean_Compiler_CSE_visitCases___closed__1 = _init_l_Lean_Compiler_CSE_visitCase
lean_mark_persistent(l_Lean_Compiler_CSE_visitCases___closed__1);
l_Lean_Compiler_CSE_visitLambda___closed__1 = _init_l_Lean_Compiler_CSE_visitLambda___closed__1();
lean_mark_persistent(l_Lean_Compiler_CSE_visitLambda___closed__1);
l_Lean_Compiler_CSE_visitLet___closed__1 = _init_l_Lean_Compiler_CSE_visitLet___closed__1();
lean_mark_persistent(l_Lean_Compiler_CSE_visitLet___closed__1);
l_Lean_Compiler_Decl_cse___closed__1 = _init_l_Lean_Compiler_Decl_cse___closed__1();
lean_mark_persistent(l_Lean_Compiler_Decl_cse___closed__1);
return lean_io_result_mk_ok(lean_box(0));

869
stage0/stdlib/Lean/Compiler/Check.c generated
View file

File diff suppressed because it is too large Load diff

3395
stage0/stdlib/Lean/Compiler/CompilerM.c generated
View file

File diff suppressed because it is too large Load diff

314
stage0/stdlib/Lean/Compiler/Decl.c generated
View file

@ -64,9 +64,10 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_toDecl___spec__1__
LEAN_EXPORT lean_object* l_Lean_Compiler_inlineMatchers___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_inlineMatchers___closed__21;
static lean_object* l_Lean_Compiler_inlineMatchers___closed__13;
lean_object* l_Lean_Compiler_check(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_check(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_inlineMatchers___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_ensureUniqueLetVarNamesCore___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ConstantInfo_levelParams(lean_object*);
static lean_object* l_Lean_Compiler_inlineMatchers___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_lambdaTelescope___at___private_Lean_Compiler_Decl_0__Lean_Compiler_normalizeAlt___spec__2(lean_object*);
@ -77,7 +78,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Compiler_Decl_0__Lean_Compiler_normali
LEAN_EXPORT lean_object* l_Lean_Meta_withLetDecl___at___private_Lean_Compiler_Decl_0__Lean_Compiler_normalizeAlt___spec__1(lean_object*);
static lean_object* l_Lean_Compiler_Decl_check___closed__2;
lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_Decl_check___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_toLCNFType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_Decl_check___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_Decl_check___closed__1;
@ -101,6 +101,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_macroInline(lean_object*, lean_object*,
LEAN_EXPORT lean_object* l_Lean_Meta_withLetDecl___at___private_Lean_Compiler_Decl_0__Lean_Compiler_normalizeAlt___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_macroInline___closed__1;
lean_object* l_Lean_Compiler_ensureUniqueLetVarNamesCore___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_instHashableExpr;
static lean_object* l_Lean_Compiler_inlineMatchers___closed__10;
lean_object* lean_format_pretty(lean_object*, lean_object*);
@ -128,7 +129,7 @@ lean_object* l_Lean_ConstantInfo_value_x3f(lean_object*);
lean_object* l_instBEqProd___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_inlineMatchers___closed__8;
static lean_object* l_Lean_Compiler_Decl_check___closed__8;
LEAN_EXPORT lean_object* l_Lean_Compiler_Decl_check(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_Decl_check(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_macroInline___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_macroInline___lambda__1___closed__1;
static lean_object* l_Lean_Compiler_inlineMatchers_inlineMatcher___closed__5;
@ -157,6 +158,7 @@ static lean_object* l_Lean_Compiler_inlineMatchers___closed__14;
static lean_object* l_Lean_Compiler_Decl_checkJoinPoints___closed__1;
lean_object* l_Array_ofSubarray___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_inlineMatchers_inlineMatcher___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__2;
lean_object* lean_is_unsafe_rec_name(lean_object*);
static lean_object* l_Lean_Compiler_toDecl___closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
@ -164,6 +166,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_Decl_getArity(lean_object*);
lean_object* l_panic___at_Lean_TSyntax_getNat___spec__1(lean_object*);
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_macroInline___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__1;
lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_MatcherInfo_arity(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_toDecl___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -176,7 +179,7 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_Decl_check___spec_
static lean_object* l_Lean_Compiler_inlineMatchers___closed__17;
lean_object* l_Lean_Expr_getAppFn(lean_object*);
lean_object* l_Lean_Meta_Match_MatcherInfo_numAlts(lean_object*);
lean_object* l_Lean_Compiler_ensureUniqueLetVarNames(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_transform___at_Lean_Compiler_ensureUniqueLetVarNamesCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_toDecl___closed__6;
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLetDeclImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3290,7 +3293,7 @@ x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_Decl_check(lean_object* x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
LEAN_EXPORT lean_object* l_Lean_Compiler_Decl_check(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
@ -3562,16 +3565,6 @@ lean_dec(x_2);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_Decl_check___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
uint8_t x_6; lean_object* x_7;
x_6 = lean_unbox(x_2);
lean_dec(x_2);
x_7 = l_Lean_Compiler_Decl_check(x_1, x_6, x_3, x_4, x_5);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_Decl_mapValue(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
@ -4065,6 +4058,22 @@ lean_dec(x_2);
return x_5;
}
}
static lean_object* _init_l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Compiler_ensureUniqueLetVarNamesCore___lambda__1___boxed), 5, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Compiler_ensureUniqueLetVarNamesCore___lambda__2___boxed), 5, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Compiler_Decl_ensureUniqueLetVarNames(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -4072,134 +4081,189 @@ uint8_t x_5;
x_5 = !lean_is_exclusive(x_1);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_6 = lean_ctor_get(x_1, 0);
x_7 = lean_ctor_get(x_1, 1);
x_8 = lean_ctor_get(x_1, 2);
x_9 = lean_ctor_get(x_1, 3);
x_10 = l_Lean_Compiler_ensureUniqueLetVarNames(x_9, x_2, x_3, x_4);
if (lean_obj_tag(x_10) == 0)
{
uint8_t x_11;
x_11 = !lean_is_exclusive(x_10);
if (x_11 == 0)
{
lean_object* x_12;
x_12 = lean_ctor_get(x_10, 0);
lean_ctor_set(x_1, 3, x_12);
lean_ctor_set(x_10, 0, x_1);
return x_10;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = lean_ctor_get(x_10, 0);
x_14 = lean_ctor_get(x_10, 1);
lean_inc(x_14);
lean_inc(x_13);
x_10 = lean_st_ref_get(x_3, x_4);
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
lean_ctor_set(x_1, 3, x_13);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_1);
lean_ctor_set(x_15, 1, x_14);
return x_15;
x_12 = lean_unsigned_to_nat(1u);
x_13 = lean_st_mk_ref(x_12, x_11);
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
lean_inc(x_15);
lean_dec(x_13);
x_16 = l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__1;
x_17 = l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__2;
lean_inc(x_3);
lean_inc(x_14);
x_18 = l_Lean_Core_transform___at_Lean_Compiler_ensureUniqueLetVarNamesCore___spec__1(x_9, x_16, x_17, x_14, x_2, x_3, x_15);
if (lean_obj_tag(x_18) == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_19 = lean_ctor_get(x_18, 0);
lean_inc(x_19);
x_20 = lean_ctor_get(x_18, 1);
lean_inc(x_20);
lean_dec(x_18);
x_21 = lean_st_ref_get(x_3, x_20);
lean_dec(x_3);
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_21);
x_23 = lean_st_ref_get(x_14, x_22);
lean_dec(x_14);
x_24 = !lean_is_exclusive(x_23);
if (x_24 == 0)
{
lean_object* x_25;
x_25 = lean_ctor_get(x_23, 0);
lean_dec(x_25);
lean_ctor_set(x_1, 3, x_19);
lean_ctor_set(x_23, 0, x_1);
return x_23;
}
else
{
lean_object* x_26; lean_object* x_27;
x_26 = lean_ctor_get(x_23, 1);
lean_inc(x_26);
lean_dec(x_23);
lean_ctor_set(x_1, 3, x_19);
x_27 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_27, 0, x_1);
lean_ctor_set(x_27, 1, x_26);
return x_27;
}
}
else
{
uint8_t x_16;
uint8_t x_28;
lean_dec(x_14);
lean_free_object(x_1);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
x_16 = !lean_is_exclusive(x_10);
if (x_16 == 0)
lean_dec(x_3);
x_28 = !lean_is_exclusive(x_18);
if (x_28 == 0)
{
return x_10;
return x_18;
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_17 = lean_ctor_get(x_10, 0);
x_18 = lean_ctor_get(x_10, 1);
lean_inc(x_18);
lean_inc(x_17);
lean_dec(x_10);
x_19 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_18);
return x_19;
}
}
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_20 = lean_ctor_get(x_1, 0);
x_21 = lean_ctor_get(x_1, 1);
x_22 = lean_ctor_get(x_1, 2);
x_23 = lean_ctor_get(x_1, 3);
lean_inc(x_23);
lean_inc(x_22);
lean_inc(x_21);
lean_inc(x_20);
lean_dec(x_1);
x_24 = l_Lean_Compiler_ensureUniqueLetVarNames(x_23, x_2, x_3, x_4);
if (lean_obj_tag(x_24) == 0)
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_25 = lean_ctor_get(x_24, 0);
lean_inc(x_25);
x_26 = lean_ctor_get(x_24, 1);
lean_inc(x_26);
if (lean_is_exclusive(x_24)) {
lean_ctor_release(x_24, 0);
lean_ctor_release(x_24, 1);
x_27 = x_24;
} else {
lean_dec_ref(x_24);
x_27 = lean_box(0);
}
x_28 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_28, 0, x_20);
lean_ctor_set(x_28, 1, x_21);
lean_ctor_set(x_28, 2, x_22);
lean_ctor_set(x_28, 3, x_25);
if (lean_is_scalar(x_27)) {
x_29 = lean_alloc_ctor(0, 2, 0);
} else {
x_29 = x_27;
}
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_26);
return x_29;
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
lean_dec(x_22);
lean_dec(x_21);
lean_dec(x_20);
x_30 = lean_ctor_get(x_24, 0);
lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_29 = lean_ctor_get(x_18, 0);
x_30 = lean_ctor_get(x_18, 1);
lean_inc(x_30);
x_31 = lean_ctor_get(x_24, 1);
lean_inc(x_31);
if (lean_is_exclusive(x_24)) {
lean_ctor_release(x_24, 0);
lean_ctor_release(x_24, 1);
x_32 = x_24;
} else {
lean_dec_ref(x_24);
x_32 = lean_box(0);
lean_inc(x_29);
lean_dec(x_18);
x_31 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_31, 0, x_29);
lean_ctor_set(x_31, 1, x_30);
return x_31;
}
if (lean_is_scalar(x_32)) {
x_33 = lean_alloc_ctor(1, 2, 0);
} else {
x_33 = x_32;
}
lean_ctor_set(x_33, 0, x_30);
lean_ctor_set(x_33, 1, x_31);
return x_33;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44;
x_32 = lean_ctor_get(x_1, 0);
x_33 = lean_ctor_get(x_1, 1);
x_34 = lean_ctor_get(x_1, 2);
x_35 = lean_ctor_get(x_1, 3);
lean_inc(x_35);
lean_inc(x_34);
lean_inc(x_33);
lean_inc(x_32);
lean_dec(x_1);
x_36 = lean_st_ref_get(x_3, x_4);
x_37 = lean_ctor_get(x_36, 1);
lean_inc(x_37);
lean_dec(x_36);
x_38 = lean_unsigned_to_nat(1u);
x_39 = lean_st_mk_ref(x_38, x_37);
x_40 = lean_ctor_get(x_39, 0);
lean_inc(x_40);
x_41 = lean_ctor_get(x_39, 1);
lean_inc(x_41);
lean_dec(x_39);
x_42 = l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__1;
x_43 = l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__2;
lean_inc(x_3);
lean_inc(x_40);
x_44 = l_Lean_Core_transform___at_Lean_Compiler_ensureUniqueLetVarNamesCore___spec__1(x_35, x_42, x_43, x_40, x_2, x_3, x_41);
if (lean_obj_tag(x_44) == 0)
{
lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53;
x_45 = lean_ctor_get(x_44, 0);
lean_inc(x_45);
x_46 = lean_ctor_get(x_44, 1);
lean_inc(x_46);
lean_dec(x_44);
x_47 = lean_st_ref_get(x_3, x_46);
lean_dec(x_3);
x_48 = lean_ctor_get(x_47, 1);
lean_inc(x_48);
lean_dec(x_47);
x_49 = lean_st_ref_get(x_40, x_48);
lean_dec(x_40);
x_50 = lean_ctor_get(x_49, 1);
lean_inc(x_50);
if (lean_is_exclusive(x_49)) {
lean_ctor_release(x_49, 0);
lean_ctor_release(x_49, 1);
x_51 = x_49;
} else {
lean_dec_ref(x_49);
x_51 = lean_box(0);
}
x_52 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_52, 0, x_32);
lean_ctor_set(x_52, 1, x_33);
lean_ctor_set(x_52, 2, x_34);
lean_ctor_set(x_52, 3, x_45);
if (lean_is_scalar(x_51)) {
x_53 = lean_alloc_ctor(0, 2, 0);
} else {
x_53 = x_51;
}
lean_ctor_set(x_53, 0, x_52);
lean_ctor_set(x_53, 1, x_50);
return x_53;
}
else
{
lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57;
lean_dec(x_40);
lean_dec(x_34);
lean_dec(x_33);
lean_dec(x_32);
lean_dec(x_3);
x_54 = lean_ctor_get(x_44, 0);
lean_inc(x_54);
x_55 = lean_ctor_get(x_44, 1);
lean_inc(x_55);
if (lean_is_exclusive(x_44)) {
lean_ctor_release(x_44, 0);
lean_ctor_release(x_44, 1);
x_56 = x_44;
} else {
lean_dec_ref(x_44);
x_56 = lean_box(0);
}
if (lean_is_scalar(x_56)) {
x_57 = lean_alloc_ctor(1, 2, 0);
} else {
x_57 = x_56;
}
lean_ctor_set(x_57, 0, x_54);
lean_ctor_set(x_57, 1, x_55);
return x_57;
}
}
}
@ -4377,6 +4441,10 @@ l_Lean_Compiler_Decl_toString___closed__1 = _init_l_Lean_Compiler_Decl_toString_
lean_mark_persistent(l_Lean_Compiler_Decl_toString___closed__1);
l_Lean_Compiler_Decl_toString___closed__2 = _init_l_Lean_Compiler_Decl_toString___closed__2();
lean_mark_persistent(l_Lean_Compiler_Decl_toString___closed__2);
l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__1 = _init_l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__1();
lean_mark_persistent(l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__1);
l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__2 = _init_l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__2();
lean_mark_persistent(l_Lean_Compiler_Decl_ensureUniqueLetVarNames___closed__2);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

215
stage0/stdlib/Lean/Compiler/InferType.c generated
View file

@ -27,9 +27,10 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_InferType_i
static lean_object* l_panic___at_Lean_Compiler_InferType_inferProjType___spec__3___closed__2;
lean_object* lean_array_uget(lean_object*, size_t);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__2;
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_InferType_inferProjType___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Level_succ___override(lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__6;
static lean_object* l_Lean_Compiler_InferType_getCasesResultingType_go___closed__4;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_InferType_inferForallType_go___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferProjType___spec__4___closed__3;
@ -48,6 +49,7 @@ static lean_object* l_Lean_Compiler_InferType_getCasesResultingType_go___closed_
lean_object* l_Lean_FVarId_throwUnknown___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_InferType_inferForallType_go___spec__4(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_InferType_getCasesResultingType_go___closed__2;
lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Compiler_InferType_withLocalDeclImp___spec__2(lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
@ -63,6 +65,7 @@ LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inf
uint8_t lean_usize_dec_lt(size_t, size_t);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferProjType___spec__4___closed__2;
extern lean_object* l_Lean_levelZero;
static lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__4;
static lean_object* l_Lean_getConstInfo___at_Lean_Compiler_InferType_inferProjType___spec__1___closed__4;
lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_InferType_inferForallType_go___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -89,7 +92,7 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_InferType_inferType___closed__4;
static lean_object* l_Lean_Compiler_InferType_instAddMessageContextInferTypeM___closed__5;
lean_object* l_Lean_Expr_headBeta(lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_InferType_inferForallType_go___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_InferType_instAddMessageContextInferTypeM___closed__3;
static lean_object* l_Lean_getConstInfo___at_Lean_Compiler_InferType_inferProjType___spec__1___closed__2;
@ -164,6 +167,7 @@ lean_object* l_Lean_Level_normalize(lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_InferType_inferForallType_go___spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_InferType_inferProjType___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_ofSubarray___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_InferType_inferLambdaType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isAnyType(lean_object*);
lean_object* l_Lean_throwError___rarg(lean_object*, lean_object*, lean_object*);
@ -190,6 +194,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_instMonadInferType___rarg(lean_object*,
lean_object* l_Lean_Expr_getAppFn(lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_InferType_inferForallType_go___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_instMonadInferType(lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__3;
lean_object* l_Lean_Compiler_isCasesApp_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_local_ctx_find(lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_mkForall(lean_object*, lean_object*, lean_object*);
@ -201,6 +206,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_InferType_inferLambdaType_go(lean_objec
LEAN_EXPORT lean_object* l_Lean_Compiler_mkLcCast___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferProjType___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_indentExpr(lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__5;
static lean_object* l_panic___at_Lean_Compiler_InferType_inferProjType___spec__3___closed__1;
LEAN_EXPORT lean_object* l_Lean_Compiler_InferType_inferFVarType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Compiler_InferType_getLevel_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -7265,37 +7271,137 @@ x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__3() {
_start:
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16;
x_10 = l_Lean_indentExpr(x_1);
x_11 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__2;
x_12 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set(x_12, 1, x_10);
x_13 = l_Lean_Compiler_InferType_getCasesResultingType_go___closed__4;
x_14 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_14, 0, x_12);
lean_ctor_set(x_14, 1, x_13);
x_15 = l_Lean_throwError___at_Lean_Compiler_InferType_inferAppType___spec__1(x_14, x_6, x_7, x_8, x_9);
x_16 = !lean_is_exclusive(x_15);
if (x_16 == 0)
lean_object* x_1;
x_1 = lean_mk_string_from_bytes(" : ", 3);
return x_1;
}
}
static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__4() {
_start:
{
return x_15;
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__3;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("\nfunction type", 14);
return x_1;
}
}
static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__5;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
lean_object* x_12;
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_1);
x_12 = l_Lean_Compiler_InferType_inferType(x_1, x_8, x_9, x_10, x_11);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
x_14 = lean_ctor_get(x_12, 1);
lean_inc(x_14);
lean_dec(x_12);
x_15 = lean_unsigned_to_nat(0u);
x_16 = l_Array_toSubarray___rarg(x_2, x_15, x_3);
x_17 = l_Array_ofSubarray___rarg(x_16);
x_18 = l_Lean_mkAppN(x_1, x_17);
x_19 = l_Lean_indentExpr(x_18);
x_20 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__2;
x_21 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
x_22 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__4;
x_23 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_23, 0, x_21);
lean_ctor_set(x_23, 1, x_22);
x_24 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_24, 0, x_4);
x_25 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
x_26 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__6;
x_27 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_27, 0, x_25);
lean_ctor_set(x_27, 1, x_26);
x_28 = l_Lean_indentExpr(x_13);
x_29 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
x_30 = l_Lean_Compiler_InferType_getCasesResultingType_go___closed__4;
x_31 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_31, 0, x_29);
lean_ctor_set(x_31, 1, x_30);
x_32 = l_Lean_throwError___at_Lean_Compiler_InferType_inferAppType___spec__1(x_31, x_8, x_9, x_10, x_14);
lean_dec(x_10);
lean_dec(x_9);
x_33 = !lean_is_exclusive(x_32);
if (x_33 == 0)
{
return x_32;
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_17 = lean_ctor_get(x_15, 0);
x_18 = lean_ctor_get(x_15, 1);
lean_inc(x_18);
lean_inc(x_17);
lean_dec(x_15);
x_19 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_18);
return x_19;
lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_34 = lean_ctor_get(x_32, 0);
x_35 = lean_ctor_get(x_32, 1);
lean_inc(x_35);
lean_inc(x_34);
lean_dec(x_32);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_34);
lean_ctor_set(x_36, 1, x_35);
return x_36;
}
}
else
{
uint8_t x_37;
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_37 = !lean_is_exclusive(x_12);
if (x_37 == 0)
{
return x_12;
}
else
{
lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_38 = lean_ctor_get(x_12, 0);
x_39 = lean_ctor_get(x_12, 1);
lean_inc(x_39);
lean_inc(x_38);
lean_dec(x_12);
x_40 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_40, 0, x_38);
lean_ctor_set(x_40, 1, x_39);
return x_40;
}
}
}
}
@ -7349,11 +7455,11 @@ else
{
lean_object* x_44; lean_object* x_45;
x_44 = lean_expr_instantiate_rev_range(x_38, x_37, x_5, x_2);
lean_dec(x_38);
x_45 = l_Lean_Expr_headBeta(x_44);
if (lean_obj_tag(x_45) == 7)
{
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50;
lean_dec(x_38);
lean_dec(x_37);
x_46 = lean_ctor_get(x_45, 2);
lean_inc(x_46);
@ -7377,17 +7483,19 @@ goto block_34;
else
{
uint8_t x_51;
lean_dec(x_45);
x_51 = l_Lean_Expr_isAnyType(x_38);
x_51 = l_Lean_Expr_isAnyType(x_45);
if (x_51 == 0)
{
lean_object* x_52; lean_object* x_53;
x_52 = lean_box(0);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_5);
lean_inc(x_2);
lean_inc(x_1);
x_53 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1(x_1, x_38, x_37, x_3, x_52, x_9, x_10, x_11, x_12);
x_53 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1(x_1, x_2, x_5, x_45, x_37, x_3, x_52, x_9, x_10, x_11, x_12);
lean_dec(x_37);
lean_dec(x_38);
x_18 = x_53;
goto block_34;
}
@ -7395,7 +7503,7 @@ else
{
lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58;
x_54 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_54, 0, x_38);
lean_ctor_set(x_54, 0, x_45);
lean_ctor_set(x_54, 1, x_37);
x_55 = l_Array_forInUnsafe_loop___at_Lean_Compiler_InferType_inferForallType_go___spec__1___closed__1;
x_56 = lean_alloc_ctor(0, 2, 0);
@ -7422,9 +7530,12 @@ if (lean_obj_tag(x_19) == 0)
{
uint8_t x_20;
lean_dec(x_17);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_20 = !lean_is_exclusive(x_18);
if (x_20 == 0)
@ -7475,9 +7586,12 @@ else
{
uint8_t x_30;
lean_dec(x_17);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_30 = !lean_is_exclusive(x_18);
if (x_30 == 0)
@ -7503,10 +7617,13 @@ return x_33;
else
{
lean_object* x_59;
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_59 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_59, 0, x_8);
@ -7517,10 +7634,13 @@ return x_59;
else
{
lean_object* x_60;
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_60 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_60, 0, x_8);
@ -7600,8 +7720,11 @@ lean_ctor_set(x_22, 1, x_10);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_21);
lean_ctor_set(x_23, 1, x_22);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_20);
lean_inc(x_16);
x_24 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2(x_9, x_16, x_21, x_20, x_10, x_20, x_14, x_23, x_2, x_3, x_4, x_19);
if (lean_obj_tag(x_24) == 0)
{
@ -8094,7 +8217,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferProjType___spec__4___closed__4;
x_2 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferProjType___spec__4___closed__5;
x_3 = lean_unsigned_to_nat(93u);
x_3 = lean_unsigned_to_nat(94u);
x_4 = lean_unsigned_to_nat(12u);
x_5 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferProjType___spec__4___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -9086,18 +9209,15 @@ lean_dec(x_3);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
lean_object* x_10;
x_10 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_object* x_12;
x_12 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_10;
return x_12;
}
}
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
@ -9105,11 +9225,8 @@ _start:
{
lean_object* x_13;
x_13 = l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_2);
return x_13;
}
}
@ -9542,6 +9659,14 @@ l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lam
lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__1);
l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__2 = _init_l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__2();
lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__2);
l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__3 = _init_l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__3();
lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__3);
l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__4 = _init_l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__4();
lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__4);
l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__5 = _init_l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__5();
lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__5);
l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__6 = _init_l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__6();
lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Compiler_InferType_inferAppType___spec__2___lambda__1___closed__6);
l_Lean_Compiler_InferType_inferAppType___closed__1 = _init_l_Lean_Compiler_InferType_inferAppType___closed__1();
lean_mark_persistent(l_Lean_Compiler_InferType_inferAppType___closed__1);
l_Lean_getConstInfo___at_Lean_Compiler_InferType_inferProjType___spec__1___closed__1 = _init_l_Lean_getConstInfo___at_Lean_Compiler_InferType_inferProjType___spec__1___closed__1();

41424
stage0/stdlib/Lean/Compiler/JoinPoints.c generated
View file

File diff suppressed because it is too large Load diff

6636
stage0/stdlib/Lean/Compiler/LCNF.c generated
View file

File diff suppressed because it is too large Load diff

1666
stage0/stdlib/Lean/Compiler/LCNFTypes.c generated
View file

File diff suppressed because it is too large Load diff

1992
stage0/stdlib/Lean/Compiler/Main.c generated
View file

File diff suppressed because it is too large Load diff

3131
stage0/stdlib/Lean/Compiler/PullLocalDecls.c generated Normal file
View file

File diff suppressed because it is too large Load diff

19396
stage0/stdlib/Lean/Compiler/Simp.c generated
View file

File diff suppressed because it is too large Load diff

738
stage0/stdlib/Lean/Compiler/Stage1.c generated
View file

@ -54,6 +54,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_compileStage1___boxed(lean_object*, lea
static size_t l_Std_PersistentHashMap_insertAux___at_Lean_Compiler_saveStage1Decls___spec__2___closed__1;
LEAN_EXPORT lean_object* l_Lean_Compiler_getStage1Decl_x3f___lambda__1(lean_object*);
lean_object* l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
uint8_t l_Lean_ConstantInfo_hasValue(lean_object*);
size_t lean_usize_shift_left(size_t, size_t);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_Compiler_getStage1Decl_x3f___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_Compiler_saveStage1Decls___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1207,342 +1208,505 @@ lean_inc(x_1);
x_14 = l_Lean_getConstInfo___at___private_Lean_Compiler_InlineAttrs_0__Lean_Compiler_isValidMacroInline___spec__1(x_1, x_2, x_3, x_8);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
x_17 = l_Lean_ConstantInfo_all(x_15);
lean_dec(x_15);
x_18 = l_List_redLength___rarg(x_17);
x_19 = lean_mk_empty_array_with_capacity(x_18);
lean_dec(x_18);
x_20 = l_List_toArrayAux___rarg(x_17, x_19);
x_21 = lean_compile_stage1(x_20, x_2, x_3, x_16);
if (lean_obj_tag(x_21) == 0)
uint8_t x_15;
x_15 = !lean_is_exclusive(x_14);
if (x_15 == 0)
{
uint8_t x_22;
x_22 = !lean_is_exclusive(x_21);
if (x_22 == 0)
lean_object* x_16; lean_object* x_17; uint8_t x_18;
x_16 = lean_ctor_get(x_14, 0);
x_17 = lean_ctor_get(x_14, 1);
x_18 = l_Lean_ConstantInfo_hasValue(x_16);
if (x_18 == 0)
{
lean_object* x_23; lean_object* x_24; size_t x_25; size_t x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_23 = lean_ctor_get(x_21, 0);
x_24 = lean_array_get_size(x_23);
x_25 = lean_usize_of_nat(x_24);
lean_dec(x_24);
x_26 = 0;
x_27 = l_Lean_Compiler_getStage1Decl_x3f___closed__1;
x_28 = l_Array_forInUnsafe_loop___at_Lean_Compiler_getStage1Decl_x3f___spec__4(x_1, x_27, x_23, x_25, x_26, x_27);
lean_dec(x_23);
lean_dec(x_1);
x_29 = lean_ctor_get(x_28, 0);
lean_inc(x_29);
lean_dec(x_28);
if (lean_obj_tag(x_29) == 0)
{
lean_object* x_30;
x_30 = l_Lean_Compiler_getStage1Decl_x3f___closed__3;
lean_ctor_set(x_21, 0, x_30);
return x_21;
}
else
{
lean_object* x_31;
x_31 = lean_ctor_get(x_29, 0);
lean_inc(x_31);
lean_dec(x_29);
lean_ctor_set(x_21, 0, x_31);
return x_21;
}
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; size_t x_35; size_t x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_32 = lean_ctor_get(x_21, 0);
x_33 = lean_ctor_get(x_21, 1);
lean_inc(x_33);
lean_inc(x_32);
lean_dec(x_21);
x_34 = lean_array_get_size(x_32);
x_35 = lean_usize_of_nat(x_34);
lean_dec(x_34);
x_36 = 0;
x_37 = l_Lean_Compiler_getStage1Decl_x3f___closed__1;
x_38 = l_Array_forInUnsafe_loop___at_Lean_Compiler_getStage1Decl_x3f___spec__4(x_1, x_37, x_32, x_35, x_36, x_37);
lean_dec(x_32);
lean_dec(x_1);
x_39 = lean_ctor_get(x_38, 0);
lean_inc(x_39);
lean_dec(x_38);
if (lean_obj_tag(x_39) == 0)
{
lean_object* x_40; lean_object* x_41;
x_40 = l_Lean_Compiler_getStage1Decl_x3f___closed__3;
x_41 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_41, 0, x_40);
lean_ctor_set(x_41, 1, x_33);
return x_41;
}
else
{
lean_object* x_42; lean_object* x_43;
x_42 = lean_ctor_get(x_39, 0);
lean_inc(x_42);
lean_dec(x_39);
x_43 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_43, 0, x_42);
lean_ctor_set(x_43, 1, x_33);
return x_43;
}
}
}
else
{
uint8_t x_44;
lean_dec(x_1);
x_44 = !lean_is_exclusive(x_21);
if (x_44 == 0)
{
return x_21;
}
else
{
lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_45 = lean_ctor_get(x_21, 0);
x_46 = lean_ctor_get(x_21, 1);
lean_inc(x_46);
lean_inc(x_45);
lean_dec(x_21);
x_47 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_47, 0, x_45);
lean_ctor_set(x_47, 1, x_46);
return x_47;
}
}
}
else
{
uint8_t x_48;
lean_object* x_19;
lean_dec(x_16);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_48 = !lean_is_exclusive(x_14);
if (x_48 == 0)
x_19 = lean_box(0);
lean_ctor_set(x_14, 0, x_19);
return x_14;
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
lean_free_object(x_14);
x_20 = l_Lean_ConstantInfo_all(x_16);
lean_dec(x_16);
x_21 = l_List_redLength___rarg(x_20);
x_22 = lean_mk_empty_array_with_capacity(x_21);
lean_dec(x_21);
x_23 = l_List_toArrayAux___rarg(x_20, x_22);
x_24 = lean_compile_stage1(x_23, x_2, x_3, x_17);
if (lean_obj_tag(x_24) == 0)
{
uint8_t x_25;
x_25 = !lean_is_exclusive(x_24);
if (x_25 == 0)
{
lean_object* x_26; lean_object* x_27; size_t x_28; size_t x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_26 = lean_ctor_get(x_24, 0);
x_27 = lean_array_get_size(x_26);
x_28 = lean_usize_of_nat(x_27);
lean_dec(x_27);
x_29 = 0;
x_30 = l_Lean_Compiler_getStage1Decl_x3f___closed__1;
x_31 = l_Array_forInUnsafe_loop___at_Lean_Compiler_getStage1Decl_x3f___spec__4(x_1, x_30, x_26, x_28, x_29, x_30);
lean_dec(x_26);
lean_dec(x_1);
x_32 = lean_ctor_get(x_31, 0);
lean_inc(x_32);
lean_dec(x_31);
if (lean_obj_tag(x_32) == 0)
{
lean_object* x_33;
x_33 = l_Lean_Compiler_getStage1Decl_x3f___closed__3;
lean_ctor_set(x_24, 0, x_33);
return x_24;
}
else
{
lean_object* x_34;
x_34 = lean_ctor_get(x_32, 0);
lean_inc(x_34);
lean_dec(x_32);
lean_ctor_set(x_24, 0, x_34);
return x_24;
}
}
else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; size_t x_38; size_t x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42;
x_35 = lean_ctor_get(x_24, 0);
x_36 = lean_ctor_get(x_24, 1);
lean_inc(x_36);
lean_inc(x_35);
lean_dec(x_24);
x_37 = lean_array_get_size(x_35);
x_38 = lean_usize_of_nat(x_37);
lean_dec(x_37);
x_39 = 0;
x_40 = l_Lean_Compiler_getStage1Decl_x3f___closed__1;
x_41 = l_Array_forInUnsafe_loop___at_Lean_Compiler_getStage1Decl_x3f___spec__4(x_1, x_40, x_35, x_38, x_39, x_40);
lean_dec(x_35);
lean_dec(x_1);
x_42 = lean_ctor_get(x_41, 0);
lean_inc(x_42);
lean_dec(x_41);
if (lean_obj_tag(x_42) == 0)
{
lean_object* x_43; lean_object* x_44;
x_43 = l_Lean_Compiler_getStage1Decl_x3f___closed__3;
x_44 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_44, 0, x_43);
lean_ctor_set(x_44, 1, x_36);
return x_44;
}
else
{
lean_object* x_45; lean_object* x_46;
x_45 = lean_ctor_get(x_42, 0);
lean_inc(x_45);
lean_dec(x_42);
x_46 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_46, 0, x_45);
lean_ctor_set(x_46, 1, x_36);
return x_46;
}
}
}
else
{
uint8_t x_47;
lean_dec(x_1);
x_47 = !lean_is_exclusive(x_24);
if (x_47 == 0)
{
return x_24;
}
else
{
lean_object* x_48; lean_object* x_49; lean_object* x_50;
x_48 = lean_ctor_get(x_24, 0);
x_49 = lean_ctor_get(x_24, 1);
lean_inc(x_49);
lean_inc(x_48);
lean_dec(x_24);
x_50 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_50, 0, x_48);
lean_ctor_set(x_50, 1, x_49);
return x_50;
}
}
}
}
else
{
lean_object* x_51; lean_object* x_52; uint8_t x_53;
x_51 = lean_ctor_get(x_14, 0);
x_52 = lean_ctor_get(x_14, 1);
lean_inc(x_52);
lean_inc(x_51);
lean_dec(x_14);
x_53 = l_Lean_ConstantInfo_hasValue(x_51);
if (x_53 == 0)
{
lean_object* x_54; lean_object* x_55;
lean_dec(x_51);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_54 = lean_box(0);
x_55 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_55, 0, x_54);
lean_ctor_set(x_55, 1, x_52);
return x_55;
}
else
{
lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60;
x_56 = l_Lean_ConstantInfo_all(x_51);
lean_dec(x_51);
x_57 = l_List_redLength___rarg(x_56);
x_58 = lean_mk_empty_array_with_capacity(x_57);
lean_dec(x_57);
x_59 = l_List_toArrayAux___rarg(x_56, x_58);
x_60 = lean_compile_stage1(x_59, x_2, x_3, x_52);
if (lean_obj_tag(x_60) == 0)
{
lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; size_t x_65; size_t x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69;
x_61 = lean_ctor_get(x_60, 0);
lean_inc(x_61);
x_62 = lean_ctor_get(x_60, 1);
lean_inc(x_62);
if (lean_is_exclusive(x_60)) {
lean_ctor_release(x_60, 0);
lean_ctor_release(x_60, 1);
x_63 = x_60;
} else {
lean_dec_ref(x_60);
x_63 = lean_box(0);
}
x_64 = lean_array_get_size(x_61);
x_65 = lean_usize_of_nat(x_64);
lean_dec(x_64);
x_66 = 0;
x_67 = l_Lean_Compiler_getStage1Decl_x3f___closed__1;
x_68 = l_Array_forInUnsafe_loop___at_Lean_Compiler_getStage1Decl_x3f___spec__4(x_1, x_67, x_61, x_65, x_66, x_67);
lean_dec(x_61);
lean_dec(x_1);
x_69 = lean_ctor_get(x_68, 0);
lean_inc(x_69);
lean_dec(x_68);
if (lean_obj_tag(x_69) == 0)
{
lean_object* x_70; lean_object* x_71;
x_70 = l_Lean_Compiler_getStage1Decl_x3f___closed__3;
if (lean_is_scalar(x_63)) {
x_71 = lean_alloc_ctor(0, 2, 0);
} else {
x_71 = x_63;
}
lean_ctor_set(x_71, 0, x_70);
lean_ctor_set(x_71, 1, x_62);
return x_71;
}
else
{
lean_object* x_72; lean_object* x_73;
x_72 = lean_ctor_get(x_69, 0);
lean_inc(x_72);
lean_dec(x_69);
if (lean_is_scalar(x_63)) {
x_73 = lean_alloc_ctor(0, 2, 0);
} else {
x_73 = x_63;
}
lean_ctor_set(x_73, 0, x_72);
lean_ctor_set(x_73, 1, x_62);
return x_73;
}
}
else
{
lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77;
lean_dec(x_1);
x_74 = lean_ctor_get(x_60, 0);
lean_inc(x_74);
x_75 = lean_ctor_get(x_60, 1);
lean_inc(x_75);
if (lean_is_exclusive(x_60)) {
lean_ctor_release(x_60, 0);
lean_ctor_release(x_60, 1);
x_76 = x_60;
} else {
lean_dec_ref(x_60);
x_76 = lean_box(0);
}
if (lean_is_scalar(x_76)) {
x_77 = lean_alloc_ctor(1, 2, 0);
} else {
x_77 = x_76;
}
lean_ctor_set(x_77, 0, x_74);
lean_ctor_set(x_77, 1, x_75);
return x_77;
}
}
}
}
else
{
uint8_t x_78;
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_78 = !lean_is_exclusive(x_14);
if (x_78 == 0)
{
return x_14;
}
else
{
lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_49 = lean_ctor_get(x_14, 0);
x_50 = lean_ctor_get(x_14, 1);
lean_inc(x_50);
lean_inc(x_49);
lean_object* x_79; lean_object* x_80; lean_object* x_81;
x_79 = lean_ctor_get(x_14, 0);
x_80 = lean_ctor_get(x_14, 1);
lean_inc(x_80);
lean_inc(x_79);
lean_dec(x_14);
x_51 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_51, 0, x_49);
lean_ctor_set(x_51, 1, x_50);
return x_51;
x_81 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_81, 0, x_79);
lean_ctor_set(x_81, 1, x_80);
return x_81;
}
}
}
else
{
uint8_t x_52;
uint8_t x_82;
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_52 = !lean_is_exclusive(x_13);
if (x_52 == 0)
x_82 = !lean_is_exclusive(x_13);
if (x_82 == 0)
{
lean_ctor_set(x_5, 0, x_13);
return x_5;
}
else
{
lean_object* x_53; lean_object* x_54;
x_53 = lean_ctor_get(x_13, 0);
lean_inc(x_53);
lean_object* x_83; lean_object* x_84;
x_83 = lean_ctor_get(x_13, 0);
lean_inc(x_83);
lean_dec(x_13);
x_54 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_5, 0, x_54);
x_84 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_84, 0, x_83);
lean_ctor_set(x_5, 0, x_84);
return x_5;
}
}
}
else
{
lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61;
x_55 = lean_ctor_get(x_5, 0);
x_56 = lean_ctor_get(x_5, 1);
lean_inc(x_56);
lean_inc(x_55);
lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91;
x_85 = lean_ctor_get(x_5, 0);
x_86 = lean_ctor_get(x_5, 1);
lean_inc(x_86);
lean_inc(x_85);
lean_dec(x_5);
x_57 = lean_ctor_get(x_55, 0);
lean_inc(x_57);
lean_dec(x_55);
x_58 = l_Lean_Compiler_instInhabitedStage1ExtState;
x_59 = l_Lean_Compiler_saveStage1Decls___closed__1;
x_60 = l_Lean_EnvExtensionInterfaceUnsafe_getState___rarg(x_58, x_59, x_57);
lean_dec(x_57);
lean_inc(x_1);
x_61 = l_Std_PersistentHashMap_find_x3f___at_Lean_Compiler_getStage1Decl_x3f___spec__1(x_60, x_1);
if (lean_obj_tag(x_61) == 0)
{
lean_object* x_62;
lean_inc(x_1);
x_62 = l_Lean_getConstInfo___at___private_Lean_Compiler_InlineAttrs_0__Lean_Compiler_isValidMacroInline___spec__1(x_1, x_2, x_3, x_56);
if (lean_obj_tag(x_62) == 0)
{
lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69;
x_63 = lean_ctor_get(x_62, 0);
lean_inc(x_63);
x_64 = lean_ctor_get(x_62, 1);
lean_inc(x_64);
lean_dec(x_62);
x_65 = l_Lean_ConstantInfo_all(x_63);
lean_dec(x_63);
x_66 = l_List_redLength___rarg(x_65);
x_67 = lean_mk_empty_array_with_capacity(x_66);
lean_dec(x_66);
x_68 = l_List_toArrayAux___rarg(x_65, x_67);
x_69 = lean_compile_stage1(x_68, x_2, x_3, x_64);
if (lean_obj_tag(x_69) == 0)
{
lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; size_t x_74; size_t x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78;
x_70 = lean_ctor_get(x_69, 0);
lean_inc(x_70);
x_71 = lean_ctor_get(x_69, 1);
lean_inc(x_71);
if (lean_is_exclusive(x_69)) {
lean_ctor_release(x_69, 0);
lean_ctor_release(x_69, 1);
x_72 = x_69;
} else {
lean_dec_ref(x_69);
x_72 = lean_box(0);
}
x_73 = lean_array_get_size(x_70);
x_74 = lean_usize_of_nat(x_73);
lean_dec(x_73);
x_75 = 0;
x_76 = l_Lean_Compiler_getStage1Decl_x3f___closed__1;
x_77 = l_Array_forInUnsafe_loop___at_Lean_Compiler_getStage1Decl_x3f___spec__4(x_1, x_76, x_70, x_74, x_75, x_76);
lean_dec(x_70);
lean_dec(x_1);
x_78 = lean_ctor_get(x_77, 0);
lean_inc(x_78);
lean_dec(x_77);
if (lean_obj_tag(x_78) == 0)
{
lean_object* x_79; lean_object* x_80;
x_79 = l_Lean_Compiler_getStage1Decl_x3f___closed__3;
if (lean_is_scalar(x_72)) {
x_80 = lean_alloc_ctor(0, 2, 0);
} else {
x_80 = x_72;
}
lean_ctor_set(x_80, 0, x_79);
lean_ctor_set(x_80, 1, x_71);
return x_80;
}
else
{
lean_object* x_81; lean_object* x_82;
x_81 = lean_ctor_get(x_78, 0);
lean_inc(x_81);
lean_dec(x_78);
if (lean_is_scalar(x_72)) {
x_82 = lean_alloc_ctor(0, 2, 0);
} else {
x_82 = x_72;
}
lean_ctor_set(x_82, 0, x_81);
lean_ctor_set(x_82, 1, x_71);
return x_82;
}
}
else
{
lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86;
lean_dec(x_1);
x_83 = lean_ctor_get(x_69, 0);
lean_inc(x_83);
x_84 = lean_ctor_get(x_69, 1);
lean_inc(x_84);
if (lean_is_exclusive(x_69)) {
lean_ctor_release(x_69, 0);
lean_ctor_release(x_69, 1);
x_85 = x_69;
} else {
lean_dec_ref(x_69);
x_85 = lean_box(0);
}
if (lean_is_scalar(x_85)) {
x_86 = lean_alloc_ctor(1, 2, 0);
} else {
x_86 = x_85;
}
lean_ctor_set(x_86, 0, x_83);
lean_ctor_set(x_86, 1, x_84);
return x_86;
}
}
else
{
lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90;
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_87 = lean_ctor_get(x_62, 0);
x_87 = lean_ctor_get(x_85, 0);
lean_inc(x_87);
x_88 = lean_ctor_get(x_62, 1);
lean_inc(x_88);
if (lean_is_exclusive(x_62)) {
lean_ctor_release(x_62, 0);
lean_ctor_release(x_62, 1);
x_89 = x_62;
lean_dec(x_85);
x_88 = l_Lean_Compiler_instInhabitedStage1ExtState;
x_89 = l_Lean_Compiler_saveStage1Decls___closed__1;
x_90 = l_Lean_EnvExtensionInterfaceUnsafe_getState___rarg(x_88, x_89, x_87);
lean_dec(x_87);
lean_inc(x_1);
x_91 = l_Std_PersistentHashMap_find_x3f___at_Lean_Compiler_getStage1Decl_x3f___spec__1(x_90, x_1);
if (lean_obj_tag(x_91) == 0)
{
lean_object* x_92;
lean_inc(x_1);
x_92 = l_Lean_getConstInfo___at___private_Lean_Compiler_InlineAttrs_0__Lean_Compiler_isValidMacroInline___spec__1(x_1, x_2, x_3, x_86);
if (lean_obj_tag(x_92) == 0)
{
lean_object* x_93; lean_object* x_94; lean_object* x_95; uint8_t x_96;
x_93 = lean_ctor_get(x_92, 0);
lean_inc(x_93);
x_94 = lean_ctor_get(x_92, 1);
lean_inc(x_94);
if (lean_is_exclusive(x_92)) {
lean_ctor_release(x_92, 0);
lean_ctor_release(x_92, 1);
x_95 = x_92;
} else {
lean_dec_ref(x_62);
x_89 = lean_box(0);
lean_dec_ref(x_92);
x_95 = lean_box(0);
}
if (lean_is_scalar(x_89)) {
x_90 = lean_alloc_ctor(1, 2, 0);
x_96 = l_Lean_ConstantInfo_hasValue(x_93);
if (x_96 == 0)
{
lean_object* x_97; lean_object* x_98;
lean_dec(x_93);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_97 = lean_box(0);
if (lean_is_scalar(x_95)) {
x_98 = lean_alloc_ctor(0, 2, 0);
} else {
x_90 = x_89;
x_98 = x_95;
}
lean_ctor_set(x_90, 0, x_87);
lean_ctor_set(x_90, 1, x_88);
return x_90;
lean_ctor_set(x_98, 0, x_97);
lean_ctor_set(x_98, 1, x_94);
return x_98;
}
else
{
lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103;
lean_dec(x_95);
x_99 = l_Lean_ConstantInfo_all(x_93);
lean_dec(x_93);
x_100 = l_List_redLength___rarg(x_99);
x_101 = lean_mk_empty_array_with_capacity(x_100);
lean_dec(x_100);
x_102 = l_List_toArrayAux___rarg(x_99, x_101);
x_103 = lean_compile_stage1(x_102, x_2, x_3, x_94);
if (lean_obj_tag(x_103) == 0)
{
lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; size_t x_108; size_t x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112;
x_104 = lean_ctor_get(x_103, 0);
lean_inc(x_104);
x_105 = lean_ctor_get(x_103, 1);
lean_inc(x_105);
if (lean_is_exclusive(x_103)) {
lean_ctor_release(x_103, 0);
lean_ctor_release(x_103, 1);
x_106 = x_103;
} else {
lean_dec_ref(x_103);
x_106 = lean_box(0);
}
x_107 = lean_array_get_size(x_104);
x_108 = lean_usize_of_nat(x_107);
lean_dec(x_107);
x_109 = 0;
x_110 = l_Lean_Compiler_getStage1Decl_x3f___closed__1;
x_111 = l_Array_forInUnsafe_loop___at_Lean_Compiler_getStage1Decl_x3f___spec__4(x_1, x_110, x_104, x_108, x_109, x_110);
lean_dec(x_104);
lean_dec(x_1);
x_112 = lean_ctor_get(x_111, 0);
lean_inc(x_112);
lean_dec(x_111);
if (lean_obj_tag(x_112) == 0)
{
lean_object* x_113; lean_object* x_114;
x_113 = l_Lean_Compiler_getStage1Decl_x3f___closed__3;
if (lean_is_scalar(x_106)) {
x_114 = lean_alloc_ctor(0, 2, 0);
} else {
x_114 = x_106;
}
lean_ctor_set(x_114, 0, x_113);
lean_ctor_set(x_114, 1, x_105);
return x_114;
}
else
{
lean_object* x_115; lean_object* x_116;
x_115 = lean_ctor_get(x_112, 0);
lean_inc(x_115);
lean_dec(x_112);
if (lean_is_scalar(x_106)) {
x_116 = lean_alloc_ctor(0, 2, 0);
} else {
x_116 = x_106;
}
lean_ctor_set(x_116, 0, x_115);
lean_ctor_set(x_116, 1, x_105);
return x_116;
}
}
else
{
lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94;
lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120;
lean_dec(x_1);
x_117 = lean_ctor_get(x_103, 0);
lean_inc(x_117);
x_118 = lean_ctor_get(x_103, 1);
lean_inc(x_118);
if (lean_is_exclusive(x_103)) {
lean_ctor_release(x_103, 0);
lean_ctor_release(x_103, 1);
x_119 = x_103;
} else {
lean_dec_ref(x_103);
x_119 = lean_box(0);
}
if (lean_is_scalar(x_119)) {
x_120 = lean_alloc_ctor(1, 2, 0);
} else {
x_120 = x_119;
}
lean_ctor_set(x_120, 0, x_117);
lean_ctor_set(x_120, 1, x_118);
return x_120;
}
}
}
else
{
lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124;
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_91 = lean_ctor_get(x_61, 0);
lean_inc(x_91);
if (lean_is_exclusive(x_61)) {
lean_ctor_release(x_61, 0);
x_92 = x_61;
x_121 = lean_ctor_get(x_92, 0);
lean_inc(x_121);
x_122 = lean_ctor_get(x_92, 1);
lean_inc(x_122);
if (lean_is_exclusive(x_92)) {
lean_ctor_release(x_92, 0);
lean_ctor_release(x_92, 1);
x_123 = x_92;
} else {
lean_dec_ref(x_61);
x_92 = lean_box(0);
lean_dec_ref(x_92);
x_123 = lean_box(0);
}
if (lean_is_scalar(x_92)) {
x_93 = lean_alloc_ctor(1, 1, 0);
if (lean_is_scalar(x_123)) {
x_124 = lean_alloc_ctor(1, 2, 0);
} else {
x_93 = x_92;
x_124 = x_123;
}
lean_ctor_set(x_93, 0, x_91);
x_94 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_94, 0, x_93);
lean_ctor_set(x_94, 1, x_56);
return x_94;
lean_ctor_set(x_124, 0, x_121);
lean_ctor_set(x_124, 1, x_122);
return x_124;
}
}
else
{
lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128;
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_125 = lean_ctor_get(x_91, 0);
lean_inc(x_125);
if (lean_is_exclusive(x_91)) {
lean_ctor_release(x_91, 0);
x_126 = x_91;
} else {
lean_dec_ref(x_91);
x_126 = lean_box(0);
}
if (lean_is_scalar(x_126)) {
x_127 = lean_alloc_ctor(1, 1, 0);
} else {
x_127 = x_126;
}
lean_ctor_set(x_127, 0, x_125);
x_128 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_128, 0, x_127);
lean_ctor_set(x_128, 1, x_86);
return x_128;
}
}
}

1250
stage0/stdlib/Lean/Compiler/TerminalCases.c generated
View file

File diff suppressed because it is too large Load diff

5666
stage0/stdlib/Lean/Compiler/Util.c generated
View file

File diff suppressed because it is too large Load diff

3994
stage0/stdlib/Lean/Elab/Quotation.c generated
View file

File diff suppressed because it is too large Load diff

1309
stage0/stdlib/Lean/Meta/InferType.c generated
View file

File diff suppressed because it is too large Load diff

514
stage0/stdlib/Std/Data/HashSet.c generated
View file

@ -24,14 +24,19 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_foldM___spec
uint8_t lean_usize_dec_eq(size_t, size_t);
static lean_object* l_Std_HashSet_empty___closed__1;
lean_object* lean_array_uget(lean_object*, size_t);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_foldM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_insert___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_foldBucketsM(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_forM___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_find_x3f(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_reinsertAux___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Std_HashSetImp_contains___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_replace___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_List_elem___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_foldM___spec__1___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_fold(lean_object*, lean_object*);
@ -44,13 +49,17 @@ lean_object* l_List_foldlM___rarg(lean_object*, lean_object*, lean_object*, lean
LEAN_EXPORT lean_object* l_Std_HashSetImp_contains___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldlM___at_Std_HashSet_fold___spec__1___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_mkHashSetImp___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_List_foldl___at_Std_HashSetImp_moveEntries___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_fold___spec__2___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_fold___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_foldM___spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldlM___at_Std_HashSetImp_fold___spec__1___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_size___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_forBucketsM___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_foldBuckets___spec__2(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_toList(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_foldM(lean_object*, lean_object*, lean_object*);
@ -58,6 +67,7 @@ LEAN_EXPORT lean_object* l_Std_HashSet_empty(lean_object*, lean_object*, lean_ob
size_t lean_uint64_to_usize(uint64_t);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_foldBuckets___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_foldM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_forM___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetBucket_update___rarg(lean_object*, size_t, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_erase(lean_object*);
@ -81,6 +91,7 @@ static lean_object* l_Std_mkHashSetImp___rarg___closed__2;
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_foldBucketsM___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT size_t l_Std_HashSetImp_mkIdx(lean_object*, lean_object*, size_t);
LEAN_EXPORT lean_object* l_Std_HashSet_instForMHashSet(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_toList___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_foldBucketsM___spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_isEmpty___rarg___boxed(lean_object*);
@ -92,6 +103,7 @@ LEAN_EXPORT lean_object* l_Std_HashSet_find_x3f___rarg(lean_object*, lean_object
size_t lean_usize_modn(size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_foldBucketsM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_toList___spec__2(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_foldM___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_toList___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_toArray(lean_object*, lean_object*, lean_object*);
@ -101,9 +113,11 @@ LEAN_EXPORT lean_object* l_List_foldl___at_Std_HashSetImp_moveEntries___spec__1_
LEAN_EXPORT lean_object* l_Std_HashSetImp_contains(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_foldM___spec__1___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_insert(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_foldM___spec__1___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
LEAN_EXPORT uint8_t l_Std_HashSet_isEmpty___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_toList___spec__2___rarg(lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_find_x3f___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_foldM(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_foldBucketsM___spec__1___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
@ -112,12 +126,15 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_toArray___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_fold___spec__2(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_toArray___rarg(lean_object*);
static lean_object* l_Std_HashSet_instForMHashSet___closed__1;
LEAN_EXPORT lean_object* l_List_foldlM___at_Std_HashSet_toList___spec__1___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldlM___at_Std_HashSet_fold___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_size(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_numBuckets___rarg___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_instForMHashSet___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_size___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_fold___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_forM(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_fold___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_numBuckets___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_mul(lean_object*, lean_object*);
@ -127,27 +144,35 @@ LEAN_EXPORT lean_object* l_Std_HashSetImp_foldBuckets(lean_object*, lean_object*
LEAN_EXPORT lean_object* l_Std_HashSet_instEmptyCollectionHashSet(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_expand___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldlM___at_Std_HashSet_toArray___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_forM(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_foldM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_moveEntries___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_array(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
lean_object* l_List_forM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_erase___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_mkHashSet___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_find_x3f(lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_reinsertAux(lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_find_x3f___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_forBucketsM(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldlM___at_Std_HashSet_toArray___spec__1___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_toArray___spec__2(lean_object*);
LEAN_EXPORT lean_object* l_List_foldlM___at_Std_HashSetImp_fold___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_foldBucketsM___spec__1___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_isEmpty___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldlM___at_Std_HashSetImp_foldBuckets___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_mkIdx___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_instInhabitedHashSet(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_foldBucketsM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_forM___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_List_foldlM___at_Std_HashSetImp_foldBuckets___spec__1___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_find_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_insert___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_foldM___spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_fold___spec__2___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_numBuckets(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetImp_foldBuckets___rarg(lean_object*, lean_object*, lean_object*);
@ -155,6 +180,7 @@ LEAN_EXPORT lean_object* l_Std_mkHashSet___boxed(lean_object*, lean_object*, lea
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_toList___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSet_isEmpty(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetBucket_update(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_toArray___spec__2___rarg(lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Std_HashSetBucket_update___rarg(lean_object* x_1, size_t x_2, lean_object* x_3, lean_object* x_4) {
@ -826,6 +852,305 @@ lean_dec(x_2);
return x_8;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg___lambda__1(size_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, size_t x_5, lean_object* x_6) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = 1;
x_8 = lean_usize_add(x_1, x_7);
x_9 = l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg(x_2, x_3, x_4, x_8, x_5, x_6);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, size_t x_4, size_t x_5, lean_object* x_6) {
_start:
{
uint8_t x_7;
x_7 = lean_usize_dec_eq(x_4, x_5);
if (x_7 == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
lean_dec(x_6);
x_8 = lean_ctor_get(x_1, 1);
lean_inc(x_8);
x_9 = lean_array_uget(x_3, x_4);
lean_inc(x_2);
lean_inc(x_1);
x_10 = l_List_forM___rarg(x_1, lean_box(0), x_9, x_2);
x_11 = lean_box_usize(x_4);
x_12 = lean_box_usize(x_5);
x_13 = lean_alloc_closure((void*)(l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg___lambda__1___boxed), 6, 5);
lean_closure_set(x_13, 0, x_11);
lean_closure_set(x_13, 1, x_1);
lean_closure_set(x_13, 2, x_2);
lean_closure_set(x_13, 3, x_3);
lean_closure_set(x_13, 4, x_12);
x_14 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_10, x_13);
return x_14;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
lean_dec(x_3);
lean_dec(x_2);
x_15 = lean_ctor_get(x_1, 0);
lean_inc(x_15);
lean_dec(x_1);
x_16 = lean_ctor_get(x_15, 1);
lean_inc(x_16);
lean_dec(x_15);
x_17 = lean_apply_2(x_16, lean_box(0), x_6);
return x_17;
}
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg___boxed), 6, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_HashSetImp_forBucketsM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; uint8_t x_6;
x_4 = lean_array_get_size(x_2);
x_5 = lean_unsigned_to_nat(0u);
x_6 = lean_nat_dec_lt(x_5, x_4);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_7 = lean_ctor_get(x_1, 0);
lean_inc(x_7);
lean_dec(x_1);
x_8 = lean_ctor_get(x_7, 1);
lean_inc(x_8);
lean_dec(x_7);
x_9 = lean_box(0);
x_10 = lean_apply_2(x_8, lean_box(0), x_9);
return x_10;
}
else
{
uint8_t x_11;
x_11 = lean_nat_dec_le(x_4, x_4);
if (x_11 == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_12 = lean_ctor_get(x_1, 0);
lean_inc(x_12);
lean_dec(x_1);
x_13 = lean_ctor_get(x_12, 1);
lean_inc(x_13);
lean_dec(x_12);
x_14 = lean_box(0);
x_15 = lean_apply_2(x_13, lean_box(0), x_14);
return x_15;
}
else
{
size_t x_16; size_t x_17; lean_object* x_18; lean_object* x_19;
x_16 = 0;
x_17 = lean_usize_of_nat(x_4);
lean_dec(x_4);
x_18 = lean_box(0);
x_19 = l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg(x_1, x_3, x_2, x_16, x_17, x_18);
return x_19;
}
}
}
}
LEAN_EXPORT lean_object* l_Std_HashSetImp_forBucketsM(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Std_HashSetImp_forBucketsM___rarg), 3, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_9 = l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg___lambda__1(x_7, x_2, x_3, x_4, x_8, x_6);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_9 = l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forBucketsM___spec__1___rarg(x_1, x_2, x_3, x_7, x_8, x_6);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg___lambda__1(size_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, size_t x_5, lean_object* x_6) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = 1;
x_8 = lean_usize_add(x_1, x_7);
x_9 = l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg(x_2, x_3, x_4, x_8, x_5, x_6);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, size_t x_4, size_t x_5, lean_object* x_6) {
_start:
{
uint8_t x_7;
x_7 = lean_usize_dec_eq(x_4, x_5);
if (x_7 == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
lean_dec(x_6);
x_8 = lean_ctor_get(x_1, 1);
lean_inc(x_8);
x_9 = lean_array_uget(x_3, x_4);
lean_inc(x_2);
lean_inc(x_1);
x_10 = l_List_forM___rarg(x_1, lean_box(0), x_9, x_2);
x_11 = lean_box_usize(x_4);
x_12 = lean_box_usize(x_5);
x_13 = lean_alloc_closure((void*)(l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg___lambda__1___boxed), 6, 5);
lean_closure_set(x_13, 0, x_11);
lean_closure_set(x_13, 1, x_1);
lean_closure_set(x_13, 2, x_2);
lean_closure_set(x_13, 3, x_3);
lean_closure_set(x_13, 4, x_12);
x_14 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_10, x_13);
return x_14;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
lean_dec(x_3);
lean_dec(x_2);
x_15 = lean_ctor_get(x_1, 0);
lean_inc(x_15);
lean_dec(x_1);
x_16 = lean_ctor_get(x_15, 1);
lean_inc(x_16);
lean_dec(x_15);
x_17 = lean_apply_2(x_16, lean_box(0), x_6);
return x_17;
}
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg___boxed), 6, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_HashSetImp_forM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = lean_array_get_size(x_4);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_nat_dec_lt(x_6, x_5);
if (x_7 == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
x_8 = lean_ctor_get(x_1, 0);
lean_inc(x_8);
lean_dec(x_1);
x_9 = lean_ctor_get(x_8, 1);
lean_inc(x_9);
lean_dec(x_8);
x_10 = lean_box(0);
x_11 = lean_apply_2(x_9, lean_box(0), x_10);
return x_11;
}
else
{
uint8_t x_12;
x_12 = lean_nat_dec_le(x_5, x_5);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
x_13 = lean_ctor_get(x_1, 0);
lean_inc(x_13);
lean_dec(x_1);
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = lean_box(0);
x_16 = lean_apply_2(x_14, lean_box(0), x_15);
return x_16;
}
else
{
size_t x_17; size_t x_18; lean_object* x_19; lean_object* x_20;
x_17 = 0;
x_18 = lean_usize_of_nat(x_5);
lean_dec(x_5);
x_19 = lean_box(0);
x_20 = l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg(x_1, x_2, x_4, x_17, x_18, x_19);
return x_20;
}
}
}
}
LEAN_EXPORT lean_object* l_Std_HashSetImp_forM(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Std_HashSetImp_forM___rarg), 3, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_9 = l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg___lambda__1(x_7, x_2, x_3, x_4, x_8, x_6);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_9 = l_Array_foldlMUnsafe_fold___at_Std_HashSetImp_forM___spec__1___rarg(x_1, x_2, x_3, x_7, x_8, x_6);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Std_HashSetImp_find_x3f___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -1711,6 +2036,193 @@ lean_dec(x_2);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg___lambda__1(size_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, size_t x_5, lean_object* x_6) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = 1;
x_8 = lean_usize_add(x_1, x_7);
x_9 = l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg(x_2, x_3, x_4, x_8, x_5, x_6);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, size_t x_4, size_t x_5, lean_object* x_6) {
_start:
{
uint8_t x_7;
x_7 = lean_usize_dec_eq(x_4, x_5);
if (x_7 == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
lean_dec(x_6);
x_8 = lean_ctor_get(x_1, 1);
lean_inc(x_8);
x_9 = lean_array_uget(x_3, x_4);
lean_inc(x_2);
lean_inc(x_1);
x_10 = l_List_forM___rarg(x_1, lean_box(0), x_9, x_2);
x_11 = lean_box_usize(x_4);
x_12 = lean_box_usize(x_5);
x_13 = lean_alloc_closure((void*)(l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg___lambda__1___boxed), 6, 5);
lean_closure_set(x_13, 0, x_11);
lean_closure_set(x_13, 1, x_1);
lean_closure_set(x_13, 2, x_2);
lean_closure_set(x_13, 3, x_3);
lean_closure_set(x_13, 4, x_12);
x_14 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_10, x_13);
return x_14;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
lean_dec(x_3);
lean_dec(x_2);
x_15 = lean_ctor_get(x_1, 0);
lean_inc(x_15);
lean_dec(x_1);
x_16 = lean_ctor_get(x_15, 1);
lean_inc(x_16);
lean_dec(x_15);
x_17 = lean_apply_2(x_16, lean_box(0), x_6);
return x_17;
}
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg___boxed), 6, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_HashSet_forM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = lean_array_get_size(x_4);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_nat_dec_lt(x_6, x_5);
if (x_7 == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_8 = lean_ctor_get(x_1, 0);
lean_inc(x_8);
lean_dec(x_1);
x_9 = lean_ctor_get(x_8, 1);
lean_inc(x_9);
lean_dec(x_8);
x_10 = lean_box(0);
x_11 = lean_apply_2(x_9, lean_box(0), x_10);
return x_11;
}
else
{
uint8_t x_12;
x_12 = lean_nat_dec_le(x_5, x_5);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_13 = lean_ctor_get(x_1, 0);
lean_inc(x_13);
lean_dec(x_1);
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = lean_box(0);
x_16 = lean_apply_2(x_14, lean_box(0), x_15);
return x_16;
}
else
{
size_t x_17; size_t x_18; lean_object* x_19; lean_object* x_20;
x_17 = 0;
x_18 = lean_usize_of_nat(x_5);
lean_dec(x_5);
x_19 = lean_box(0);
x_20 = l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg(x_1, x_3, x_4, x_17, x_18, x_19);
return x_20;
}
}
}
}
LEAN_EXPORT lean_object* l_Std_HashSet_forM(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_alloc_closure((void*)(l_Std_HashSet_forM___rarg), 3, 0);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_9 = l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg___lambda__1(x_7, x_2, x_3, x_4, x_8, x_6);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_9 = l_Array_foldlMUnsafe_fold___at_Std_HashSet_forM___spec__1___rarg(x_1, x_2, x_3, x_7, x_8, x_6);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Std_HashSet_forM___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Std_HashSet_forM(x_1, x_2, x_3, x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_5;
}
}
static lean_object* _init_l_Std_HashSet_instForMHashSet___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Std_HashSet_forM___rarg), 3, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Std_HashSet_instForMHashSet(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Std_HashSet_instForMHashSet___closed__1;
return x_5;
}
}
LEAN_EXPORT lean_object* l_Std_HashSet_instForMHashSet___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Std_HashSet_instForMHashSet(x_1, x_2, x_3, x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Std_HashSet_size___rarg(lean_object* x_1) {
_start:
{
@ -2127,6 +2639,8 @@ l_Std_mkHashSetImp___rarg___closed__2 = _init_l_Std_mkHashSetImp___rarg___closed
lean_mark_persistent(l_Std_mkHashSetImp___rarg___closed__2);
l_Std_HashSet_empty___closed__1 = _init_l_Std_HashSet_empty___closed__1();
lean_mark_persistent(l_Std_HashSet_empty___closed__1);
l_Std_HashSet_instForMHashSet___closed__1 = _init_l_Std_HashSet_instForMHashSet___closed__1();
lean_mark_persistent(l_Std_HashSet_instForMHashSet___closed__1);
l_Std_HashSet_toArray___rarg___closed__1 = _init_l_Std_HashSet_toArray___rarg___closed__1();
lean_mark_persistent(l_Std_HashSet_toArray___rarg___closed__1);
return lean_io_result_mk_ok(lean_box(0));