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
open Fmlib
open Common
type t = {
gamma: Gamma.t;
map: Name_map.t
}
let count (c:t): int =
Gamma.count c.gamma
let gamma (c:t): Gamma.t =
c.gamma
let name_map (c:t): Name_map.t =
c.map
let standard (): t =
let gamma = Gamma.standard () in
{gamma;
map =
Interval.fold
Name_map.empty
(fun i m ->
Name_map.add_global
Gamma.(name_at_level i gamma)
m)
0 (Gamma.count gamma)
}
let compute (t:Term.t) (c:t): Term.t =
Gamma.compute t c.gamma
let find_name (name:string) (c:t): int list =
Name_map.find name c.map
module Pretty (P:Pretty_printer.SIG) =
struct
module P0 = Term_printer.Pretty (Gamma) (P)
let print (t:Term.t) (c:t): P.t =
P0.print t c.gamma
end