-
Notifications
You must be signed in to change notification settings - Fork 350
/
ToExpr.lean
193 lines (162 loc) · 6.19 KB
/
ToExpr.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
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Expr
import Init.Data.BitVec.Basic
universe u
namespace Lean
/--
We use the `ToExpr` type class to convert values of type `α` into
expressions that denote these values in Lean.
Example:
```
toExpr true = .const ``Bool.true []
```
-/
class ToExpr (α : Type u) where
/-- Convert a value `a : α` into an expression that denotes `a` -/
toExpr : α → Expr
/-- Expression representing the type `α` -/
toTypeExpr : Expr
export ToExpr (toExpr toTypeExpr)
instance : ToExpr Nat where
toExpr := mkNatLit
toTypeExpr := mkConst ``Nat
instance : ToExpr Int where
toTypeExpr := .const ``Int []
toExpr i := if 0 ≤ i then
mkNat i.toNat
else
mkApp3 (.const ``Neg.neg [0]) (.const ``Int []) (.const ``Int.instNegInt [])
(mkNat (-i).toNat)
where
mkNat (n : Nat) : Expr :=
let r := mkRawNatLit n
mkApp3 (.const ``OfNat.ofNat [0]) (.const ``Int []) r
(.app (.const ``instOfNat []) r)
instance : ToExpr (Fin n) where
toTypeExpr := .app (mkConst ``Fin) (toExpr n)
toExpr a :=
let r := mkRawNatLit a.val
mkApp3 (.const ``OfNat.ofNat [0]) (.app (mkConst ``Fin) (toExpr n)) r
(mkApp2 (.const ``Fin.instOfNat []) (mkNatLit (n-1)) r)
instance : ToExpr (BitVec n) where
toTypeExpr := .app (mkConst ``BitVec) (toExpr n)
-- Remark: We use ``BitVec.ofNat to represent bitvector literals
toExpr a := mkApp2 (.const ``BitVec.ofNat []) (toExpr n) (toExpr a.toNat)
instance : ToExpr UInt8 where
toTypeExpr := mkConst ``UInt8
toExpr a :=
let r := mkRawNatLit a.val
mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt8) r
(.app (.const ``UInt8.instOfNat []) r)
instance : ToExpr UInt16 where
toTypeExpr := mkConst ``UInt16
toExpr a :=
let r := mkRawNatLit a.val
mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt16) r
(.app (.const ``UInt16.instOfNat []) r)
instance : ToExpr UInt32 where
toTypeExpr := mkConst ``UInt32
toExpr a :=
let r := mkRawNatLit a.val
mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt32) r
(.app (.const ``UInt32.instOfNat []) r)
instance : ToExpr UInt64 where
toTypeExpr := mkConst ``UInt64
toExpr a :=
let r := mkRawNatLit a.val
mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt64) r
(.app (.const ``UInt64.instOfNat []) r)
instance : ToExpr USize where
toTypeExpr := mkConst ``USize
toExpr a :=
let r := mkRawNatLit a.val
mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``USize) r
(.app (.const ``USize.instOfNat []) r)
instance : ToExpr Bool where
toExpr := fun b => if b then mkConst ``Bool.true else mkConst ``Bool.false
toTypeExpr := mkConst ``Bool
instance : ToExpr Char where
toExpr := fun c => mkApp (mkConst ``Char.ofNat) (mkRawNatLit c.toNat)
toTypeExpr := mkConst ``Char
instance : ToExpr String where
toExpr := mkStrLit
toTypeExpr := mkConst ``String
instance : ToExpr Unit where
toExpr := fun _ => mkConst `Unit.unit
toTypeExpr := mkConst ``Unit
instance : ToExpr System.FilePath where
toExpr p := mkApp (mkConst ``System.FilePath.mk) (toExpr p.toString)
toTypeExpr := mkConst ``System.FilePath
private def Name.toExprAux (n : Name) : Expr :=
if isSimple n 0 then
mkStr n 0 #[]
else
go n
where
isSimple (n : Name) (sz : Nat) : Bool :=
match n with
| .anonymous => 0 < sz && sz <= 8
| .str p _ => isSimple p (sz+1)
| _ => false
mkStr (n : Name) (sz : Nat) (args : Array Expr) : Expr :=
match n with
| .anonymous => mkAppN (mkConst (.str ``Lean.Name ("mkStr" ++ toString sz))) args.reverse
| .str p s => mkStr p (sz+1) (args.push (toExpr s))
| _ => unreachable!
go : Name → Expr
| .anonymous => mkConst ``Lean.Name.anonymous
| .str p s ..=> mkApp2 (mkConst ``Lean.Name.str) (go p) (toExpr s)
| .num p n ..=> mkApp2 (mkConst ``Lean.Name.num) (go p) (toExpr n)
instance : ToExpr Name where
toExpr := Name.toExprAux
toTypeExpr := mkConst ``Name
instance [ToExpr α] : ToExpr (Option α) :=
let type := toTypeExpr α
{ toExpr := fun o => match o with
| none => mkApp (mkConst ``Option.none [levelZero]) type
| some a => mkApp2 (mkConst ``Option.some [levelZero]) type (toExpr a),
toTypeExpr := mkApp (mkConst ``Option [levelZero]) type }
private def List.toExprAux [ToExpr α] (nilFn : Expr) (consFn : Expr) : List α → Expr
| [] => nilFn
| a::as => mkApp2 consFn (toExpr a) (toExprAux nilFn consFn as)
instance [ToExpr α] : ToExpr (List α) :=
let type := toTypeExpr α
let nil := mkApp (mkConst ``List.nil [levelZero]) type
let cons := mkApp (mkConst ``List.cons [levelZero]) type
{ toExpr := List.toExprAux nil cons,
toTypeExpr := mkApp (mkConst ``List [levelZero]) type }
instance [ToExpr α] : ToExpr (Array α) :=
let type := toTypeExpr α
{ toExpr := fun as => mkApp2 (mkConst ``List.toArray [levelZero]) type (toExpr as.toList),
toTypeExpr := mkApp (mkConst ``Array [levelZero]) type }
instance [ToExpr α] [ToExpr β] : ToExpr (α × β) :=
let αType := toTypeExpr α
let βType := toTypeExpr β
{ toExpr := fun ⟨a, b⟩ => mkApp4 (mkConst ``Prod.mk [levelZero, levelZero]) αType βType (toExpr a) (toExpr b),
toTypeExpr := mkApp2 (mkConst ``Prod [levelZero, levelZero]) αType βType }
instance : ToExpr Literal where
toTypeExpr := mkConst ``Literal
toExpr l := match l with
| .natVal _ => mkApp (mkConst ``Literal.natVal) (.lit l)
| .strVal _ => mkApp (mkConst ``Literal.strVal) (.lit l)
instance : ToExpr FVarId where
toTypeExpr := mkConst ``FVarId
toExpr fvarId := mkApp (mkConst ``FVarId.mk) (toExpr fvarId.name)
instance : ToExpr Syntax.Preresolved where
toTypeExpr := .const ``Syntax.Preresolved []
toExpr
| .namespace ns => mkApp (.const ``Syntax.Preresolved.namespace []) (toExpr ns)
| .decl a ls => mkApp2 (.const ``Syntax.Preresolved.decl []) (toExpr a) (toExpr ls)
def Expr.toCtorIfLit : Expr → Expr
| .lit (.natVal v) =>
if v == 0 then mkConst ``Nat.zero
else mkApp (mkConst ``Nat.succ) (mkRawNatLit (v-1))
| .lit (.strVal v) =>
mkApp (mkConst ``String.mk) (toExpr v.toList)
| e => e
end Lean