Repository navigation
Expand file tree
/
Copy pathFrontend.lean
More file actions
110 lines (74 loc) · 3.63 KB
/
Copy pathFrontend.lean
File metadata and controls
110 lines (74 loc) · 3.63 KB
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
import Verified.Reflect.Command
namespace Verified.Examples.Frontend
@[inline] def offset (x k : UInt64) : UInt64 := x + k
abbrev shifted (x : UInt64) : UInt64 := offset x 3
def inlineScalar (x : UInt64) : UInt64 := shifted (offset x 5)
@[inline] def replace (xs : Array UInt64) (i v : UInt64) : Array UInt64 :=
xs.setIfInBounds i.toNat v
def inlineArray (xs : Array UInt64) (i v : UInt64) : Array UInt64 :=
replace (xs.push 7) i v
def inlineLoop (n : UInt64) : UInt64 :=
LeanExe.loop n 0 fun i total => offset total (shifted i)
def setDirect (xs : Array UInt64) (i v : UInt64) : Array UInt64 :=
xs.setIfInBounds i.toNat v
def insertDirect (xs : Array UInt64) (i v : UInt64) : Array UInt64 :=
xs.insertIdxIfInBounds i.toNat v
def eraseDirect (xs : Array UInt64) (i : UInt64) : Array UInt64 :=
xs.eraseIdxIfInBounds i.toNat
def insertChecked (xs : Array UInt64) (i v : UInt64) : Array UInt64 :=
xs.insertIdx! i.toNat v
def insertFresh (xs : Array UInt64) (i v : UInt64) : Array UInt64 :=
(xs.push 7).insertIdx! (i + 1).toNat v
def insertBorrowed (xs : Array UInt64) (i v : UInt64) : Array UInt64 × Array UInt64 :=
(xs.insertIdx! i.toNat v, xs)
def insertRead (xs : Array UInt64) (i v : UInt64) : Array UInt64 × UInt64 :=
let ys := xs.insertIdx! i.toNat v
(ys, xs.size.toUInt64)
def insertFloat (xs : Array Float) (i : UInt64) (v : Float) : Array Float :=
xs.insertIdx! i.toNat v
@[inline] def listed (x : UInt64) : UInt64 := x * 7
def listedCall (x : UInt64) : UInt64 := listed x + 1
def emptyWords : Array UInt64 := #[]
def emptyFloats : Array Float := #[]
structure Entry where
key : UInt64
price : Float
active : Bool
instance : LeanExe.Pipeline.Flat Entry (UInt64 × Float × Bool) :=
⟨fun e => (e.key, e.price, e.active)⟩
def insertRecord (xs : Array Entry) (i key : UInt64) : Array Entry :=
xs.insertIdx! i.toNat ⟨key, key.toFloat, true⟩
def entries (n : UInt64) : UInt64 × Array Entry :=
if n == 0 then (1, #[])
else (0, LeanExe.build n fun i => ⟨i, i.toFloat, i % 2 == 0⟩)
def boolEq (a b : Bool) : Bool := a == b
def boolNe (a b : Bool) : Bool := a != b
def boolDecide (a b : Bool) : Bool := decide (a = b)
def boolIf (a b : Bool) : UInt64 := if a = b then 7 else 9
def boolIfNe (a b : Bool) : UInt64 := if a ≠ b then 7 else 9
def boolOwn (xs : Array UInt64) (flag : Bool) : Bool :=
let ys := xs.push 7
flag && 0 < ys.size.toUInt64
def boolCalls (xs : Array UInt64) (a b : Bool) : Bool := boolOwn xs a == boolOwn xs b
def boolRecord (a b : Bool) : Entry :=
if a = b then ⟨7, 1.5, true⟩ else ⟨9, -2.5, false⟩
def boolRecords (a b : Bool) : Array Entry :=
if a ≠ b then LeanExe.build 1 fun _ => ⟨7, 1.5, true⟩ else #[]
verified_compile compiled := [inlineScalar, inlineArray, inlineLoop, setDirect, insertDirect,
eraseDirect, listed, listedCall, emptyWords, emptyFloats, entries, boolEq, boolNe, boolDecide,
boolIf, boolIfNe, boolOwn, boolCalls, boolRecord, boolRecords, insertChecked, insertFresh,
insertBorrowed, insertFloat, insertRecord, insertRead]
example : compiled.insertRead.func.modes = [.borrowed, .borrowed, .borrowed] := rfl
#print axioms compiled.inlineScalar.denote_eq
#print axioms compiled.inlineArray.implements
#print axioms compiled.inlineLoop.trapFree
#print axioms compiled.insertDirect.implements
#print axioms compiled.eraseDirect.implements
#print axioms compiled.entries.implements
#print axioms compiled.boolCalls.implements
#print axioms compiled.insertChecked.denote_eq
#print axioms compiled.insertBorrowed.trapFree
#print axioms compiled.insertRead.trapFree
#print axioms compiled.insertRecord.implements
#print axioms compiled.bytes
end Verified.Examples.Frontend