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
(** {1 De Bruijn environments} *)
type 'a t = {
size : int;
stack : 'a option list;
}
let empty = { size=0; stack=[]; }
let is_empty env = env.size = 0
let make size = {
size;
stack = CCList.range 0 size |> List.map (fun _ -> None);
}
let singleton x = { size=1; stack = [Some x]; }
let push env x = {size=env.size+1; stack=(Some x) :: env.stack; }
let push_l_same_order env l = List.fold_right (fun x e -> push e x) l env
let push_l_rev env l = List.fold_left push env l
let push_none env = {size=env.size+1; stack=None :: env.stack; }
let rec push_none_multiple env n =
if n <= 0 then env else push_none (push_none_multiple env (n-1))
let size env = env.size
let pop env = match env.stack with
| [] -> raise (Invalid_argument "Env.pop: empty env")
| _::tl -> {size=env.size-1; stack=tl; }
let rec pop_many env n = match n with
| 0 -> env
| _ -> pop_many (pop env) (n-1)
let find env n =
assert (n>=0);
if n < env.size then List.nth env.stack n else None
let find_exn env n =
if n < env.size
then match List.nth env.stack n with
| None -> failwith "DBEnv.find_exn"
| Some x -> x
else failwith "DBEnv.find_exn"
let mem env n =
if n < env.size then List.nth env.stack n <> None else false
let set env n x =
if n<0 || n >= env.size then raise (Invalid_argument "DBEnv.set");
{env with stack= CCList.set_at_idx n (Some x) env.stack; }
let num_bindings db =
let rec count acc l = match l with
| [] -> acc
| None :: l' -> count acc l'
| Some _ :: l' -> count (1+acc) l'
in count 0 db.stack
let map f db =
let stack = List.map
(function
| None -> None
| Some x -> Some (f x))
db.stack
in
{ db with stack; }
let filteri f db =
let stack =
CCList.foldi
(fun acc i o -> match o with
| Some x when f i x -> Some x :: acc
| _ -> None :: acc)
[] db.stack
|> List.rev
in
{ db with stack; }
let of_list l =
let max = List.fold_left (fun acc (b,_) -> max acc b) ~-1 l in
let env = make (max+1) in
List.fold_left
(fun env (db, v) -> set env db v)
env l
let to_list e = e.stack
let to_list_i e =
List.mapi (fun i x -> CCOpt.map (CCPair.make i) x) e.stack
let pp pp_x out e =
let pp_item out = function
| None -> CCFormat.string out "_"
| Some x -> Format.fprintf out "[@[%a@]]" pp_x x
in
Format.fprintf out "@[<hv2>%a@]" (Util.pp_list ~sep:"," pp_item) e.stack
let to_string ppx = CCFormat.to_string (pp ppx)