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
open Fmlib
open Common
module Name_map =
struct
type t =
{map: int list String_map.t; cnt: int}
let empty: t =
{map = String_map.empty; cnt = 0}
let count (m:t): int =
m.cnt
let find (name:string) (m:t): int list =
match String_map.maybe_find name m.map with
| None ->
[]
| Some lst ->
lst
let add_unnamed (m:t): t =
{m with cnt = 1 + m.cnt}
let add (name:string) (global:bool) (m:t): t =
assert (name <> "");
if name = "_" then
add_unnamed m
else
{map =
String_map.add
name
(match String_map.maybe_find name m.map with
| None ->
[m.cnt]
| Some lst ->
if global then
m.cnt :: lst
else
[m.cnt])
m.map;
cnt =
1 + m.cnt}
let add_global (name:string) (m:t): t =
assert (name <> "");
add name true m
let add_local (name: string) (m:t) : t =
assert (name <> "");
add name false m
end
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