-
Notifications
You must be signed in to change notification settings - Fork 80
/
expr.lean
584 lines (480 loc) · 22.9 KB
/
expr.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.meta.level init.control.monad init.meta.rb_map
universes u v
open native
/-- Column and line position in a Lean source file. -/
structure pos :=
(line : nat)
(column : nat)
instance : decidable_eq pos
| ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ := if h₁ : l₁ = l₂ then
if h₂ : c₁ = c₂ then is_true (eq.rec_on h₁ (eq.rec_on h₂ rfl))
else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₂ h₂))
else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₁ h₁))
meta instance : has_to_format pos :=
⟨λ ⟨l, c⟩, "⟨" ++ l ++ ", " ++ c ++ "⟩"⟩
/-- Auxiliary annotation for binders (Lambda and Pi).
This information is only used for elaboration.
The difference between `{}` and `⦃⦄` is how implicit arguments are treated that are *not* followed by explicit arguments.
`{}` arguments are applied eagerly, while `⦃⦄` arguments are left partially applied:
```lean
def foo {x : ℕ} : ℕ := x
def bar ⦃x : ℕ⦄ : ℕ := x
#check foo -- foo : ℕ
#check bar -- bar : Π ⦃x : ℕ⦄, ℕ
```
-/
inductive binder_info
/- `(x : α)` -/
| default
/- `{x : α}` -/
| implicit
/- `⦃x:α⦄` -/
| strict_implicit
/- `[x : α]`. Should be inferred with typeclass resolution. -/
| inst_implicit
/- Auxiliary internal attribute used to mark local constants representing recursive functions
in recursive equations and `match` statements. -/
| aux_decl
instance : has_repr binder_info :=
⟨λ bi, match bi with
| binder_info.default := "default"
| binder_info.implicit := "implicit"
| binder_info.strict_implicit := "strict_implicit"
| binder_info.inst_implicit := "inst_implicit"
| binder_info.aux_decl := "aux_decl"
end⟩
/-- Macros are basically "promises" to build an expr by some C++ code, you can't build them in Lean.
You can unfold a macro and force it to evaluate.
They are used for
- `sorry`.
- Term placeholders (`_`) in `pexpr`s.
- Expression annotations. See `expr.is_annotation`.
- Meta-recursive calls. Eg:
```
meta def Y : (α → α) → α | f := f (Y f)
```
The `Y` that appears in `f (Y f)` is a macro.
- Builtin projections:
```
structure foo := (mynat : ℕ)
#print foo.mynat
-- @[reducible]
-- def foo.mynat : foo → ℕ :=
-- λ (c : foo), [foo.mynat c]
```
The thing in square brackets is a macro.
- Ephemeral structures inside certain specialised C++ implemented tactics.
-/
meta constant macro_def : Type
/-- An expression. eg ```(4+5)```.
The `elab` flag is indicates whether the `expr` has been elaborated and doesn't contain any placeholder macros.
For example the equality `x = x` is represented in `expr ff` as ``app (app (const `eq _) x) x`` while in `expr tt` it is represented as ``app (app (app (const `eq _) t) x) x`` (one more argument).
The VM replaces instances of this datatype with the C++ implementation. -/
meta inductive expr (elaborated : bool := tt)
/- A bound variable with a de-Bruijn index. -/
| var : nat → expr
/- A type universe: `Sort u` -/
| sort : level → expr
/- A global constant. These include definitions, constants and inductive type stuff present
in the environment as well as hard-coded definitions. -/
| const : name → list level → expr
/- [WARNING] Do not trust the types for `mvar` and `local_const`,
they are sometimes dummy values. Use `tactic.infer_type` instead. -/
/- An `mvar` is a 'hole' yet to be filled in by the elaborator or tactic state. -/
| mvar (unique : name) (pretty : name) (type : expr) : expr
/- A local constant. For example, if our tactic state was `h : P ⊢ Q`, `h` would be a local constant. -/
| local_const (unique : name) (pretty : name) (bi : binder_info) (type : expr) : expr
/- Function application. -/
| app : expr → expr → expr
/- Lambda abstraction. eg ```(λ a : α, x)`` -/
| lam (var_name : name) (bi : binder_info) (var_type : expr) (body : expr) : expr
/- Pi type constructor. eg ```(Π a : α, x)`` and ```(α → β)`` -/
| pi (var_name : name) (bi : binder_info) (var_type : expr) (body : expr) : expr
/- An explicit let binding. -/
| elet (var_name : name) (type : expr) (assignment : expr) (body : expr) : expr
/- A macro, see the docstring for `macro_def`.
The list of expressions are local constants and metavariables that the macro depends on.
-/
| macro : macro_def → list expr → expr
variable {elab : bool}
meta instance : inhabited expr := ⟨expr.sort level.zero⟩
/-- Get the name of the macro definition. -/
meta constant expr.macro_def_name (d : macro_def) : name
meta def expr.mk_var (n : nat) : expr := expr.var n
/-- Expressions can be annotated using an annotation macro during compilation.
For example, a `have x:X, from p, q` expression will be compiled to `(λ x:X,q)(p)`, but nested in an annotation macro with the name `"have"`.
These annotations have no real semantic meaning, but are useful for helping Lean's pretty printer. -/
meta constant expr.is_annotation : expr elab → option (name × expr elab)
/-- Remove all macro annotations from the given `expr`. -/
meta def expr.erase_annotations : expr elab → expr elab
| e :=
match e.is_annotation with
| some (_, a) := expr.erase_annotations a
| none := e
end
/-- Compares expressions, including binder names. -/
meta constant expr.has_decidable_eq : decidable_eq expr
attribute [instance] expr.has_decidable_eq
/-- Compares expressions while ignoring binder names. -/
meta constant expr.alpha_eqv : expr → expr → bool
notation a ` =ₐ `:50 b:50 := expr.alpha_eqv a b = bool.tt
protected meta constant expr.to_string : expr elab → string
meta instance : has_to_string (expr elab) := ⟨expr.to_string⟩
meta instance : has_to_format (expr elab) := ⟨λ e, e.to_string⟩
/-- Coercion for letting users write (f a) instead of (expr.app f a) -/
meta instance : has_coe_to_fun (expr elab) :=
{ F := λ e, expr elab → expr elab, coe := λ e, expr.app e }
/-- Each expression created by Lean carries a hash.
This is calculated upon creation of the expression.
Two structurally equal expressions will have the same hash. -/
meta constant expr.hash : expr → nat
/-- Compares expressions, ignoring binder names, and sorting by hash. -/
meta constant expr.lt : expr → expr → bool
/-- Compares expressions, ignoring binder names. -/
meta constant expr.lex_lt : expr → expr → bool
/-- `expr.fold e a f`: Traverses each subexpression of `e`. The `nat` passed to the folder `f` is the binder depth. -/
meta constant expr.fold {α : Type} : expr → α → (expr → nat → α → α) → α
/-- `expr.replace e f`
Traverse over an expr `e` with a function `f` which can decide to replace subexpressions or not.
For each subexpression `s` in the expression tree, `f s n` is called where `n` is how many binders are present above the given subexpression `s`.
If `f s n` returns `none`, the children of `s` will be traversed.
Otherwise if `some s'` is returned, `s'` will replace `s` and this subexpression will not be traversed further.
-/
meta constant expr.replace : expr → (expr → nat → option expr) → expr
/-- `abstract_local e n` replaces each instance of the local constant with unique (not pretty) name `n` in `e` with a de-Bruijn variable. -/
meta constant expr.abstract_local : expr → name → expr
/-- Multi version of `abstract_local`. Note that the given expression will only be traversed once, so this is not the same as `list.foldl expr.abstract_local`.-/
meta constant expr.abstract_locals : expr → list name → expr
/-- `abstract e x` Abstracts the expression `e` over the local constant `x`. -/
meta def expr.abstract : expr → expr → expr
| e (expr.local_const n m bi t) := e.abstract_local n
| e _ := e
/-- Expressions depend on `level`s, and these may depend on universe parameters which have names.
`instantiate_univ_params e [(n₁,l₁), ...]` will traverse `e` and replace any universe parameters with name `nᵢ` with the corresponding level `lᵢ`. -/
meta constant expr.instantiate_univ_params : expr → list (name × level) → expr
/-- `instantiate_nth_var n a b` takes the `n`th de-Bruijn variable in `a` and replaces each occurrence with `b`. -/
meta constant expr.instantiate_nth_var : nat → expr → expr → expr
/-- `instantiate_var a b` takes the 0th de-Bruijn variable in `a` and replaces each occurrence with `b`. -/
meta constant expr.instantiate_var : expr → expr → expr
/-- ``instantiate_vars `(#0 #1 #2) [x,y,z] = `(%%x %%y %%z)`` -/
meta constant expr.instantiate_vars : expr → list expr → expr
/-- Same as `instantiate_vars` except lifts and shifts the vars by the given amount.
``instantiate_vars_core `(#0 #1 #2 #3) 0 [x,y] = `(x y #0 #1)``
``instantiate_vars_core `(#0 #1 #2 #3) 1 [x,y] = `(#0 x y #1)``
``instantiate_vars_core `(#0 #1 #2 #3) 2 [x,y] = `(#0 #1 x y)``
-/
meta constant expr.instantiate_vars_core : expr → nat → list expr → expr
/-- Perform beta-reduction if the left expression is a lambda, or construct an application otherwise.
That is: ``expr.subst `(λ x, %%Y) Z = Y[x/Z]``, and
``expr.subst X Z = X.app Z`` otherwise -/
protected meta constant expr.subst : expr elab → expr elab → expr elab
/-- `get_free_var_range e` returns one plus the maximum de-Bruijn value in `e`. Eg `get_free_var_range `(#1 #0)` yields `2` -/
meta constant expr.get_free_var_range : expr → nat
/-- `has_var e` returns true iff e has free variables. -/
meta constant expr.has_var : expr → bool
/-- `has_var_idx e n` returns true iff `e` has a free variable with de-Bruijn index `n`. -/
meta constant expr.has_var_idx : expr → nat → bool
/-- `has_local e` returns true if `e` contains a local constant. -/
meta constant expr.has_local : expr → bool
/-- `has_meta_var e` returns true iff `e` contains a metavariable. -/
meta constant expr.has_meta_var : expr → bool
/-- `lower_vars e s d` lowers the free variables >= s in `e` by `d`. Note that this can cause variable clashes.
examples:
- ``lower_vars `(#2 #1 #0) 1 1 = `(#1 #0 #0)``
- ``lower_vars `(λ x, #2 #1 #0) 1 1 = `(λ x, #1 #1 #0 )``
-/
meta constant expr.lower_vars : expr → nat → nat → expr
/-- Lifts free variables. `lift_vars e s d` will lift all free variables with index `≥ s` in `e` by `d`. -/
meta constant expr.lift_vars : expr → nat → nat → expr
/-- Get the position of the given expression in the Lean source file, if anywhere. -/
protected meta constant expr.pos : expr elab → option pos
/-- `copy_pos_info src tgt` copies position information from `src` to `tgt`. -/
meta constant expr.copy_pos_info : expr → expr → expr
/-- Returns `some n` when the given expression is a constant with the name `..._cnstr.n`
```
is_internal_cnstr : expr → option unsigned
|(const (mk_numeral n (mk_string "_cnstr" _)) _) := some n
|_ := none
```
[NOTE] This is not used anywhere in core Lean.
-/
meta constant expr.is_internal_cnstr : expr → option unsigned
/-- There is a macro called a "nat_value_macro" holding a natural number which are used during compilation.
This function extracts that to a natural number. [NOTE] This is not used anywhere in Lean. -/
meta constant expr.get_nat_value : expr → option nat
/-- Get a list of all of the universe parameters that the given expression depends on. -/
meta constant expr.collect_univ_params : expr → list name
/-- `occurs e t` returns `tt` iff `e` occurs in `t` up to α-equivalence. Purely structural: no unification or definitional equality. -/
meta constant expr.occurs : expr → expr → bool
/-- Returns true if any of the names in the given `name_set` are present in the given `expr`. -/
meta constant expr.has_local_in : expr → name_set → bool
/-- Computes the number of sub-expressions (constant time). -/
meta constant expr.get_weight : expr → ℕ
/-- Computes the maximum depth of the expression (constant time). -/
meta constant expr.get_depth : expr → ℕ
/-- `mk_delayed_abstraction m ls` creates a delayed abstraction on the metavariable `m` with the unique names of the local constants `ls`.
If `m` is not a metavariable then this is equivalent to `abstract_locals`.
-/
meta constant expr.mk_delayed_abstraction : expr → list name → expr
/-- If the given expression is a delayed abstraction macro, return `some ls`
where `ls` is a list of unique names of locals that will be abstracted. -/
meta constant expr.get_delayed_abstraction_locals : expr → option (list name)
/-- (reflected a) is a special opaque container for a closed `expr` representing `a`.
It can only be obtained via type class inference, which will use the representation
of `a` in the calling context. Local constants in the representation are replaced
by nested inference of `reflected` instances.
The quotation expression `` `(a) `` (outside of patterns) is equivalent to `reflect a`
and thus can be used as an explicit way of inferring an instance of `reflected a`. -/
@[class] meta def reflected {α : Sort u} : α → Type :=
λ _, expr
@[inline] meta def reflected.to_expr {α : Sort u} {a : α} : reflected a → expr :=
id
@[inline] meta def reflected.subst {α : Sort v} {β : α → Sort u} {f : Π a : α, β a} {a : α} :
reflected f → reflected a → reflected (f a) :=
expr.subst
attribute [irreducible] reflected reflected.subst reflected.to_expr
@[instance] protected meta constant expr.reflect (e : expr elab) : reflected e
@[instance] protected meta constant string.reflect (s : string) : reflected s
@[inline] meta instance {α : Sort u} (a : α) : has_coe (reflected a) expr :=
⟨reflected.to_expr⟩
protected meta def reflect {α : Sort u} (a : α) [h : reflected a] : reflected a := h
meta instance {α} (a : α) : has_to_format (reflected a) :=
⟨λ h, to_fmt h.to_expr⟩
namespace expr
open decidable
meta def lt_prop (a b : expr) : Prop :=
expr.lt a b = tt
meta instance : decidable_rel expr.lt_prop :=
λ a b, bool.decidable_eq _ _
/-- Compares expressions, ignoring binder names, and sorting by hash. -/
meta instance : has_lt expr :=
⟨ expr.lt_prop ⟩
meta def mk_true : expr :=
const `true []
meta def mk_false : expr :=
const `false []
/-- Returns the sorry macro with the given type. -/
meta constant mk_sorry (type : expr) : expr
/-- Checks whether e is sorry, and returns its type. -/
meta constant is_sorry (e : expr) : option expr
/-- Replace each instance of the local constant with name `n` by the expression `s` in `e`. -/
meta def instantiate_local (n : name) (s : expr) (e : expr) : expr :=
instantiate_var (abstract_local e n) s
meta def instantiate_locals (s : list (name × expr)) (e : expr) : expr :=
instantiate_vars (abstract_locals e (list.reverse (list.map prod.fst s))) (list.map prod.snd s)
meta def is_var : expr → bool
| (var _) := tt
| _ := ff
meta def app_of_list : expr → list expr → expr
| f [] := f
| f (p::ps) := app_of_list (f p) ps
meta def is_app : expr → bool
| (app f a) := tt
| e := ff
meta def app_fn : expr → expr
| (app f a) := f
| a := a
meta def app_arg : expr → expr
| (app f a) := a
| a := a
meta def get_app_fn : expr elab → expr elab
| (app f a) := get_app_fn f
| a := a
meta def get_app_num_args : expr → nat
| (app f a) := get_app_num_args f + 1
| e := 0
meta def get_app_args_aux : list expr → expr → list expr
| r (app f a) := get_app_args_aux (a::r) f
| r e := r
meta def get_app_args : expr → list expr :=
get_app_args_aux []
meta def mk_app : expr → list expr → expr
| e [] := e
| e (x::xs) := mk_app (e x) xs
meta def mk_binding (ctor : name → binder_info → expr → expr → expr) (e : expr) : Π (l : expr), expr
| (local_const n pp_n bi ty) := ctor pp_n bi ty (e.abstract_local n)
| _ := e
/-- (bind_pi e l) abstracts and pi-binds the local `l` in `e` -/
meta def bind_pi := mk_binding pi
/-- (bind_lambda e l) abstracts and lambda-binds the local `l` in `e` -/
meta def bind_lambda := mk_binding lam
meta def ith_arg_aux : expr → nat → expr
| (app f a) 0 := a
| (app f a) (n+1) := ith_arg_aux f n
| e _ := e
meta def ith_arg (e : expr) (i : nat) : expr :=
ith_arg_aux e (get_app_num_args e - i - 1)
meta def const_name : expr elab → name
| (const n ls) := n
| e := name.anonymous
meta def is_constant : expr elab → bool
| (const n ls) := tt
| e := ff
meta def is_local_constant : expr → bool
| (local_const n m bi t) := tt
| e := ff
meta def local_uniq_name : expr → name
| (local_const n m bi t) := n
| e := name.anonymous
meta def local_pp_name : expr elab → name
| (local_const x n bi t) := n
| e := name.anonymous
meta def local_type : expr elab → expr elab
| (local_const _ _ _ t) := t
| e := e
meta def is_aux_decl : expr → bool
| (local_const _ _ binder_info.aux_decl _) := tt
| _ := ff
meta def is_constant_of : expr elab → name → bool
| (const n₁ ls) n₂ := n₁ = n₂
| e n := ff
meta def is_app_of (e : expr) (n : name) : bool :=
is_constant_of (get_app_fn e) n
/-- The same as `is_app_of` but must also have exactly `n` arguments. -/
meta def is_napp_of (e : expr) (c : name) (n : nat) : bool :=
is_app_of e c ∧ get_app_num_args e = n
meta def is_false : expr → bool
| `(false) := tt
| _ := ff
meta def is_not : expr → option expr
| `(not %%a) := some a
| `(%%a → false) := some a
| e := none
meta def is_and : expr → option (expr × expr)
| `(and %%α %%β) := some (α, β)
| _ := none
meta def is_or : expr → option (expr × expr)
| `(or %%α %%β) := some (α, β)
| _ := none
meta def is_iff : expr → option (expr × expr)
| `((%%a : Prop) ↔ %%b) := some (a, b)
| _ := none
meta def is_eq : expr → option (expr × expr)
| `((%%a : %%_) = %%b) := some (a, b)
| _ := none
meta def is_ne : expr → option (expr × expr)
| `((%%a : %%_) ≠ %%b) := some (a, b)
| _ := none
meta def is_bin_arith_app (e : expr) (op : name) : option (expr × expr) :=
if is_napp_of e op 4
then some (app_arg (app_fn e), app_arg e)
else none
meta def is_lt (e : expr) : option (expr × expr) :=
is_bin_arith_app e ``has_lt.lt
meta def is_gt (e : expr) : option (expr × expr) :=
is_bin_arith_app e ``gt
meta def is_le (e : expr) : option (expr × expr) :=
is_bin_arith_app e ``has_le.le
meta def is_ge (e : expr) : option (expr × expr) :=
is_bin_arith_app e ``ge
meta def is_heq : expr → option (expr × expr × expr × expr)
| `(@heq %%α %%a %%β %%b) := some (α, a, β, b)
| _ := none
meta def is_lambda : expr → bool
| (lam _ _ _ _) := tt
| e := ff
meta def is_pi : expr → bool
| (pi _ _ _ _) := tt
| e := ff
meta def is_arrow : expr → bool
| (pi _ _ _ b) := bnot (has_var b)
| e := ff
meta def is_let : expr → bool
| (elet _ _ _ _) := tt
| e := ff
/-- The name of the bound variable in a pi, lambda or let expression. -/
meta def binding_name : expr → name
| (pi n _ _ _) := n
| (lam n _ _ _) := n
| (elet n _ _ _) := n
| e := name.anonymous
/-- The binder info of a pi or lambda expression. -/
meta def binding_info : expr → binder_info
| (pi _ bi _ _) := bi
| (lam _ bi _ _) := bi
| e := binder_info.default
/-- The domain (type of bound variable) of a pi, lambda or let expression. -/
meta def binding_domain : expr → expr
| (pi _ _ d _) := d
| (lam _ _ d _) := d
| (elet _ d _ _) := d
| e := e
/-- The body of a pi, lambda or let expression.
This definition doesn't instantiate bound variables, and therefore produces a term that is open.
See note [open expressions] in mathlib. -/
meta def binding_body : expr → expr
| (pi _ _ _ b) := b
| (lam _ _ _ b) := b
| (elet _ _ _ b) := b
| e := e
/-- `nth_binding_body n e` iterates `binding_body` `n` times to an iterated pi expression `e`.
This definition doesn't instantiate bound variables, and therefore produces a term that is open.
See note [open expressions] in mathlib. -/
meta def nth_binding_body : ℕ → expr → expr
| (n + 1) (pi _ _ _ b) := nth_binding_body n b
| _ e := e
meta def is_macro : expr → bool
| (macro d a) := tt
| e := ff
meta def is_numeral : expr → bool
| `(@has_zero.zero %%α %%s) := tt
| `(@has_one.one %%α %%s) := tt
| `(@bit0 %%α %%s %%v) := is_numeral v
| `(@bit1 %%α %%s₁ %%s₂ %%v) := is_numeral v
| _ := ff
meta def pi_arity : expr → ℕ
| (pi _ _ _ b) := pi_arity b + 1
| _ := 0
meta def lam_arity : expr → ℕ
| (lam _ _ _ b) := lam_arity b + 1
| _ := 0
meta def imp (a b : expr) : expr :=
pi `_ binder_info.default a b
/-- `lambdas cs e` lambda binds `e` with each of the local constants in `cs`. -/
meta def lambdas : list expr → expr → expr
| (local_const uniq pp info t :: es) f :=
lam pp info t (abstract_local (lambdas es f) uniq)
| _ f := f
/-- Same as `expr.lambdas` but with `pi`. -/
meta def pis : list expr → expr → expr
| (local_const uniq pp info t :: es) f :=
pi pp info t (abstract_local (pis es f) uniq)
| _ f := f
meta def extract_opt_auto_param : expr → expr
| `(@opt_param %%t _) := extract_opt_auto_param t
| `(@auto_param %%t _) := extract_opt_auto_param t
| e := e
open format
private meta def p := λ xs, paren (format.join (list.intersperse " " xs))
meta def to_raw_fmt : expr elab → format
| (var n) := p ["var", to_fmt n]
| (sort l) := p ["sort", to_fmt l]
| (const n ls) := p ["const", to_fmt n, to_fmt ls]
| (mvar n m t) := p ["mvar", to_fmt n, to_fmt m, to_raw_fmt t]
| (local_const n m bi t) := p ["local_const", to_fmt n, to_fmt m, to_raw_fmt t]
| (app e f) := p ["app", to_raw_fmt e, to_raw_fmt f]
| (lam n bi e t) := p ["lam", to_fmt n, repr bi, to_raw_fmt e, to_raw_fmt t]
| (pi n bi e t) := p ["pi", to_fmt n, repr bi, to_raw_fmt e, to_raw_fmt t]
| (elet n g e f) := p ["elet", to_fmt n, to_raw_fmt g, to_raw_fmt e, to_raw_fmt f]
| (macro d args) := sbracket (format.join (list.intersperse " " ("macro" :: to_fmt (macro_def_name d) :: args.map to_raw_fmt)))
/-- Fold an accumulator `a` over each subexpression in the expression `e`.
The `nat` passed to `fn` is the number of binders above the subexpression. -/
meta def mfold {α : Type} {m : Type → Type} [monad m] (e : expr) (a : α) (fn : expr → nat → α → m α) : m α :=
fold e (return a) (λ e n a, a >>= fn e n)
end expr
/-- An dictionary from `data` to expressions. -/
@[reducible] meta def expr_map (data : Type) := rb_map expr data
namespace expr_map
export native.rb_map (hiding mk)
meta def mk (data : Type) : expr_map data := rb_map.mk expr data
end expr_map
meta def mk_expr_map {data : Type} : expr_map data :=
expr_map.mk data
@[reducible] meta def expr_set := rb_set expr
meta def mk_expr_set : expr_set := mk_rb_set