Skip to content

Commit 167c9c9

Browse files
hargoniXhargoniX
committed
fix: use general allocator for closures
1 parent 3a42ee0 commit 167c9c9

File tree

3 files changed

+260
-1
lines changed

3 files changed

+260
-1
lines changed

‎src/include/lean/lean.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -715,7 +715,7 @@ static inline lean_object ** lean_closure_arg_cptr(lean_object * o) { return lea
715715
static inline lean_obj_res lean_alloc_closure(void * fun, unsigned arity, unsigned num_fixed) {
716716
assert(arity > 0);
717717
assert(num_fixed < arity);
718-
lean_closure_object * o = (lean_closure_object*)lean_alloc_small_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed);
718+
lean_closure_object * o = (lean_closure_object*)lean_alloc_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed);
719719
lean_set_st_header((lean_object*)o, LeanClosure, 0);
720720
o->m_fun = fun;
721721
o->m_arity = arity;

‎tests/compiler/large_closure_bug.lean‎

Lines changed: 258 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,258 @@
1+
import Lean
2+
import Std
3+
4+
abbrev IteratedProd (ts : List Type) : Type :=
5+
ts.foldr Prod Unit
6+
7+
abbrev IteratedArrow (codomain : Type) (ts : List Type) : Type :=
8+
ts.foldr (· → ·) codomain
9+
10+
section IteratedProdInstances
11+
12+
macro "infer_instance_for_iterated_prod" : tactic =>
13+
`(tactic| repeat' (first | infer_instance | constructor ))
14+
15+
end IteratedProdInstances
16+
17+
section SingleField
18+
19+
variable (fieldDomain : List Type) (FieldCodomain : Type)
20+
21+
local macro "⌞" t1:ident t2:ident* "⌟" : term => `($t1 $(Lean.mkIdent `fieldDomain) $t2:ident*)
22+
local macro "⌞_" t1:ident t2:ident* "⌟" : term => `(⌞ $t1 $(Lean.mkIdent `FieldCodomain) $t2:ident* ⌟)
23+
24+
abbrev FieldUpdatePat : Type := IteratedProd (fieldDomain.map Option)
25+
26+
abbrev CanonicalField : Type := IteratedArrow FieldCodomain fieldDomain
27+
28+
abbrev FieldUpdateDescr := List (⌞ FieldUpdatePat ⌟ × ⌞_ CanonicalField ⌟)
29+
30+
class FieldRepresentation (FieldTypeConcrete : Type) where
31+
set : ⌞_ FieldUpdateDescr ⌟ → FieldTypeConcrete → FieldTypeConcrete
32+
33+
instance canonicalFieldRepresentation {fieldDomain : List Type} {FieldCodomain : Type} :
34+
(⌞_ FieldRepresentation ⌟) (⌞_ CanonicalField ⌟) where
35+
set favs fc := favs.foldr (init := fc) fun (_, v) _ => v
36+
37+
end SingleField
38+
39+
inductive NonDetT (m : Type u -> Type v) : (α : Type u) -> Type _ where
40+
| pure {α} (ret : α) : NonDetT m α
41+
| vis {α} {β} (x : m β) (f : β → NonDetT m α) : NonDetT m α
42+
43+
def NonDetT.bind (x : NonDetT m α) (f : α → NonDetT m β) : NonDetT m β :=
44+
match x with
45+
| pure ret => f ret
46+
| vis x f' => vis x fun y => bind (f' y) f
47+
48+
instance : Monad (NonDetT m) where
49+
pure := NonDetT.pure
50+
bind := NonDetT.bind
51+
52+
instance : MonadLift m (NonDetT m) where
53+
monadLift x := NonDetT.vis x pure
54+
55+
abbrev VeilM (σ α : Type) := NonDetT ((StateT σ (ExceptT Int Option))) α
56+
57+
inductive ExtractNonDet {m} : {α : Type u} -> NonDetT m α -> Type _ where
58+
| pure {α} : ∀ (x : α), ExtractNonDet (NonDetT.pure x)
59+
| vis {α} {β} (x : m β) (f : β → NonDetT m α) :
60+
(∀ y, ExtractNonDet (f y)) → ExtractNonDet (.vis x f)
61+
62+
set_option linter.unusedVariables false in
63+
def ExtractNonDet.bind :
64+
(_ : ExtractNonDet x) -> (_ : ∀ y, ExtractNonDet (f y)) -> ExtractNonDet (x >>= f)
65+
| .pure x, inst => by
66+
dsimp [Bind.bind, NonDetT.bind]; exact (inst x)
67+
| .vis x f inst, inst' => by
68+
dsimp [Bind.bind, NonDetT.bind]; constructor
69+
intro y; apply ExtractNonDet.bind <;> solve_by_elim
70+
71+
instance ExtractNonDet.pure' : ExtractNonDet (Pure.pure (f := NonDetT m) x) := by
72+
dsimp [Pure.pure, NonDetT.pure]; constructor
73+
74+
instance ExtractNonDet.liftM (x : m α) :
75+
ExtractNonDet (liftM (n := NonDetT m) x) := by
76+
dsimp [_root_.liftM, monadLift, MonadLift.monadLift]; constructor
77+
intro y; apply ExtractNonDet.pure'
78+
79+
macro "extract_step" : tactic =>
80+
`(tactic|
81+
first
82+
| apply ExtractNonDet.bind
83+
| apply ExtractNonDet.pure'
84+
| apply ExtractNonDet.liftM
85+
| split )
86+
87+
macro "extract_tactic" : tactic =>
88+
`(tactic| repeat' (intros; extract_step <;> try dsimp))
89+
90+
abbrev VeilExecM (ε σ α : Type) := σ → Option (Except ε (α × σ))
91+
92+
def NonDetT.extract {α : Type} : (s : VeilM σ α) → (ex : ExtractNonDet s) → VeilExecM Int σ α
93+
| .pure x, _ => fun s => (Option.some (Except.ok (x, s)))
94+
| .vis x f, .vis _ _ _ =>
95+
fun s =>
96+
match x s with
97+
| Option.some (Except.ok (y, s')) =>
98+
extract (f y) (by rename_i a ; exact a y) s'
99+
| Option.none => (Option.none)
100+
| Option.some (Except.error e) => (Option.some (Except.error e))
101+
102+
inductive State.Label : Type where
103+
| m_client_request
104+
| m_marked_client_request
105+
106+
def State.Label.toDomain (l : State.Label) : List Type :=
107+
State.Label.casesOn l [Bool] [Bool, Bool, Bool]
108+
109+
structure State (χ : State.Label → Type) where mk ::
110+
m_client_request : χ State.Label.m_client_request
111+
m_marked_client_request : χ State.Label.m_marked_client_request
112+
113+
def initializer.ext {χ : State.Label → Type}
114+
[χ_rep : (f : State.Label) →
115+
FieldRepresentation (State.Label.toDomain f) Bool (χ f)] : VeilM (State χ) Unit :=
116+
do
117+
let mut __veil_state := (← MonadState.get)
118+
let mut m_client_request_conc := __veil_state.m_client_request
119+
let mut m_marked_client_request_conc := __veil_state.m_marked_client_request
120+
121+
let __veil_bind_m_client_request :=
122+
(χ_rep _).set
123+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
124+
(fun _ => (false)))] m_client_request_conc
125+
m_client_request_conc ←
126+
MonadState.modifyGet
127+
(fun st =>
128+
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
129+
let __veil_bind_m_marked_client_request :=
130+
(χ_rep _).set
131+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
132+
(fun _ _ _ => (false)))] m_marked_client_request_conc
133+
m_marked_client_request_conc ←
134+
MonadState.modifyGet
135+
(fun st =>
136+
((__veil_bind_m_marked_client_request,
137+
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
138+
139+
-- NOTE: the following are just multiple copy & pastes of the do-elements above
140+
let __veil_bind_m_client_request :=
141+
(χ_rep _).set
142+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
143+
(fun _ => (false)))] m_client_request_conc
144+
m_client_request_conc ←
145+
MonadState.modifyGet
146+
(fun st =>
147+
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
148+
let __veil_bind_m_marked_client_request :=
149+
(χ_rep _).set
150+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
151+
(fun _ _ _ => (false)))] m_marked_client_request_conc
152+
m_marked_client_request_conc ←
153+
MonadState.modifyGet
154+
(fun st =>
155+
((__veil_bind_m_marked_client_request,
156+
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
157+
158+
let __veil_bind_m_client_request :=
159+
(χ_rep _).set
160+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
161+
(fun _ => (false)))] m_client_request_conc
162+
m_client_request_conc ←
163+
MonadState.modifyGet
164+
(fun st =>
165+
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
166+
let __veil_bind_m_marked_client_request :=
167+
(χ_rep _).set
168+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
169+
(fun _ _ _ => (false)))] m_marked_client_request_conc
170+
m_marked_client_request_conc ←
171+
MonadState.modifyGet
172+
(fun st =>
173+
((__veil_bind_m_marked_client_request,
174+
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
175+
176+
let __veil_bind_m_client_request :=
177+
(χ_rep _).set
178+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
179+
(fun _ => (false)))] m_client_request_conc
180+
m_client_request_conc ←
181+
MonadState.modifyGet
182+
(fun st =>
183+
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
184+
let __veil_bind_m_marked_client_request :=
185+
(χ_rep _).set
186+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
187+
(fun _ _ _ => (false)))] m_marked_client_request_conc
188+
m_marked_client_request_conc ←
189+
MonadState.modifyGet
190+
(fun st =>
191+
((__veil_bind_m_marked_client_request,
192+
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
193+
194+
let __veil_bind_m_client_request :=
195+
(χ_rep _).set
196+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
197+
(fun _ => (false)))] m_client_request_conc
198+
m_client_request_conc ←
199+
MonadState.modifyGet
200+
(fun st =>
201+
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
202+
let __veil_bind_m_marked_client_request :=
203+
(χ_rep _).set
204+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
205+
(fun _ _ _ => (false)))] m_marked_client_request_conc
206+
m_marked_client_request_conc ←
207+
MonadState.modifyGet
208+
(fun st =>
209+
((__veil_bind_m_marked_client_request,
210+
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
211+
212+
let __veil_bind_m_client_request :=
213+
(χ_rep _).set
214+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
215+
(fun _ => (false)))] m_client_request_conc
216+
m_client_request_conc ←
217+
MonadState.modifyGet
218+
(fun st =>
219+
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
220+
let __veil_bind_m_marked_client_request :=
221+
(χ_rep _).set
222+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
223+
(fun _ _ _ => (false)))] m_marked_client_request_conc
224+
m_marked_client_request_conc ←
225+
MonadState.modifyGet
226+
(fun st =>
227+
((__veil_bind_m_marked_client_request,
228+
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
229+
230+
let __veil_bind_m_client_request :=
231+
(χ_rep _).set
232+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_client_request)) (Option.none, ())),
233+
(fun _ => (false)))] m_client_request_conc
234+
m_client_request_conc ←
235+
MonadState.modifyGet
236+
(fun st =>
237+
((__veil_bind_m_client_request, { st with m_client_request := __veil_bind_m_client_request })))
238+
let __veil_bind_m_marked_client_request :=
239+
(χ_rep _).set
240+
[((@id (FieldUpdatePat (State.Label.toDomain State.Label.m_marked_client_request)) (Option.none, Option.none, Option.none, ())),
241+
(fun _ _ _ => (false)))] m_marked_client_request_conc
242+
m_marked_client_request_conc ←
243+
MonadState.modifyGet
244+
(fun st =>
245+
((__veil_bind_m_marked_client_request,
246+
{ st with m_marked_client_request := __veil_bind_m_marked_client_request })))
247+
248+
def initExec (χ : State.Label → Type) [χ_rep : ∀ f, FieldRepresentation (State.Label.toDomain f) Bool (χ f)]
249+
: VeilExecM Int (State χ) Unit :=
250+
NonDetT.extract (@initializer.ext χ χ_rep) (by (extract_tactic))
251+
252+
def res := initExec (fun f => CanonicalField ( (State.Label.toDomain) f) Bool) {
253+
m_client_request := fun _ => false,
254+
m_marked_client_request := fun _ _ _ => false
255+
}
256+
257+
def main : IO Unit :=
258+
IO.println s!"{[res].length}"

‎tests/compiler/large_closure_bug.lean.expected.out‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
1

0 commit comments

Comments
 (0)