-
Notifications
You must be signed in to change notification settings - Fork 87
/
Expr.lean
125 lines (107 loc) · 3.72 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
/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Lean.Elab.Term
/-!
# Additional operations on Expr and related types
This file defines basic operations on the types expr, name, declaration, level, environment.
This file is mostly for non-tactics.
-/
namespace Lean.Expr
open Lean.Elab.Term in
/-- Converts an `Expr` into a `Syntax`, by creating a fresh metavariable
assigned to the expr and returning a named metavariable syntax `?a`. -/
def toSyntax (e : Expr) : TermElabM Syntax.Term := withFreshMacroScope do
let stx ← `(?a)
let mvar ← elabTermEnsuringType stx (← Meta.inferType e)
mvar.mvarId!.assign e
pure stx
/--
Returns the number of leading `∀` binders of an expression. Ignores metadata.
-/
def forallArity : Expr → Nat
| mdata _ b => forallArity b
| forallE _ _ body _ => 1 + forallArity body
| _ => 0
/--
Returns the number of leading `λ` binders of an expression. Ignores metadata.
-/
def lambdaArity : Expr → Nat
| mdata _ b => lambdaArity b
| lam _ _ b _ => 1 + lambdaArity b
| _ => 0
/-- Like `getAppNumArgs` but ignores metadata. -/
def getAppNumArgs' (e : Expr) : Nat :=
go e 0
where
/-- Auxiliary definition for `getAppNumArgs'`. -/
go : Expr → Nat → Nat
| mdata _ b, n => go b n
| app f _ , n => go f (n + 1)
| _ , n => n
/-- Like `withApp` but ignores metadata. -/
@[inline]
def withApp' (e : Expr) (k : Expr → Array Expr → α) : α :=
let dummy := mkSort levelZero
let nargs := e.getAppNumArgs'
go e (mkArray nargs dummy) (nargs - 1)
where
/-- Auxiliary definition for `withApp'`. -/
@[specialize]
go : Expr → Array Expr → Nat → α
| mdata _ b, as, i => go b as i
| app f a , as, i => go f (as.set! i a) (i-1)
| f , as, _ => k f as
/-- Like `getAppArgs` but ignores metadata. -/
@[inline]
def getAppArgs' (e : Expr) : Array Expr :=
e.withApp' λ _ as => as
/-- Like `traverseApp` but ignores metadata. -/
def traverseApp' {m} [Monad m]
(f : Expr → m Expr) (e : Expr) : m Expr :=
e.withApp' λ fn args => return mkAppN (← f fn) (← args.mapM f)
/-- Like `withAppRev` but ignores metadata. -/
@[inline]
def withAppRev' (e : Expr) (k : Expr → Array Expr → α) : α :=
go e (Array.mkEmpty e.getAppNumArgs')
where
/-- Auxiliary definition for `withAppRev'`. -/
@[specialize]
go : Expr → Array Expr → α
| mdata _ b, as => go b as
| app f a , as => go f (as.push a)
| f , as => k f as
/-- Like `getAppRevArgs` but ignores metadata. -/
@[inline]
def getAppRevArgs' (e : Expr) : Array Expr :=
e.withAppRev' λ _ as => as
/-- Like `getRevArgD` but ignores metadata. -/
def getRevArgD' : Expr → Nat → Expr → Expr
| mdata _ b, n , v => getRevArgD' b n v
| app _ a , 0 , _ => a
| app f _ , i+1, v => getRevArgD' f i v
| _ , _ , v => v
/-- Like `getArgD` but ignores metadata. -/
@[inline]
def getArgD' (e : Expr) (i : Nat) (v₀ : Expr) (n := e.getAppNumArgs') : Expr :=
getRevArgD' e (n - i - 1) v₀
/-- Like `isAppOf` but ignores metadata. -/
def isAppOf' (e : Expr) (n : Name) : Bool :=
match e.getAppFn' with
| const c .. => c == n
| _ => false
/-- Turns an expression that is a natural number literal into a natural number. -/
def natLit! : Expr → Nat
| lit (Literal.natVal v) => v
| _ => panic! "nat literal expected"
/-- Turns an expression that is a constructor of `Int` applied to a natural number literal
into an integer. -/
def intLit! (e : Expr) : Int :=
if e.isAppOfArity ``Int.ofNat 1 then
e.appArg!.natLit!
else if e.isAppOfArity ``Int.negOfNat 1 then
.negOfNat e.appArg!.natLit!
else
panic! "not a raw integer literal"