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

chore: control code size explosion

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-07 08:42:39 -07:00
parent 67d31f60c6
commit 87db970cfa
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Meta/Basic.lean
View file

@ -667,17 +667,23 @@ forallTelescopeReducingAuxAux isClassExpensive? false none k lctx #[] 0 type
def forallTelescope {α} (type : Expr) (k : Array Expr → Expr → n α) : n α :=
map2MetaM (fun _ k => forallTelescopeImp type k) k
@[noinline] private def forallTelescopeReducingImp {α} (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α :=
forallTelescopeReducingAux isClassExpensive? type none k
/--
Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,
it reduces `A` and continues bulding the telescope if it is a `forall`. -/
def forallTelescopeReducing {α} (type : Expr) (k : Array Expr → Expr → n α) : n α :=
map2MetaM (fun _ k => forallTelescopeReducingAux isClassExpensive? type none k) k
map2MetaM (fun _ k => forallTelescopeReducingImp type k) k
@[noinline] private def forallBoundedTelescopeImp {α} (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) : MetaM α :=
forallTelescopeReducingAux isClassExpensive? type maxFVars? k
/--
Similar to `forallTelescopeReducing`, stops constructing the telescope when
it reaches size `maxFVars`. -/
def forallBoundedTelescope {α} (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) : n α :=
map2MetaM (fun _ k => forallTelescopeReducingAux isClassExpensive? type maxFVars? k) k
map2MetaM (fun _ k => forallBoundedTelescopeImp type maxFVars? k) k
/-- Similar to `forallTelescopeAuxAux` but for lambda and let expressions. -/
private partial def lambdaTelescopeAux {α}