/
common.lean
46 lines (36 loc) · 1.45 KB
/
common.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
import system.io data.buffer.parser
open parser
def number : parser ℕ :=
string.to_nat <$> many_char1 (sat char.is_digit)
def signed_number : parser ℤ :=
ch '+' >> (int.of_nat <$> number) <|>
ch '-' >> ((λ x:ℕ, -x) <$> number)
def letter : parser char := sat char.is_lower
def Letter : parser char := sat char.is_upper
def go {α} (file : string) (p : parser α) (m : α → option string) : io unit :=
do s ← io.fs.read_file file,
sum.inr a ← return $ run p s,
some str ← return $ m a,
trace str (return ())
def test {α} (inp : string) (p : parser α) (m : α → option string) : io unit :=
do sum.inr a ← return $ run p inp.to_char_buffer,
some str ← return $ m a,
trace str (return ())
def rbmap.modify {α β lt} [decidable_rel lt] (s : rbmap α β lt)
(a : α) (z : β) (f : β → β) : rbmap α β lt :=
s.insert a $ match s.find a with
| (some b) := f b
| none := z
end
def rbtree.size {α lt} [decidable_rel lt] (s : rbtree α lt) : ℕ :=
s.fold (λ _, nat.succ) 0
def modify_many {n α} (f : α → α) : ℕ → ℕ → array n α → array n α
| s 0 a := a
| s (i+1) a := if h : s < n then
let a' := a.write ⟨s, h⟩ (f (a.read ⟨s, h⟩)) in
modify_many (s+1) i a'
else a
def array.modify {α n} (i : fin n) (f : α → α) (a : array n α) : array n α :=
a.write i (f (a.read i))
def array.modify' {α n} (i : ℕ) (f : α → α) (a : array n α) : array n α :=
if h : _ then a.modify ⟨i, h⟩ f else a