Source file name_map.ml

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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
open Fmlib
open Common


type entry =
    | Global of int Term_trie.t * int list
    | Local of int


type t =
    {map: entry String_map.t; has_locs: bool; cnt: int}


let empty: t =
    {map = String_map.empty; has_locs = false; cnt = 0}


let count (m:t): int =
    m.cnt


let has_locals (m: t): bool =
    m.has_locs




let find (name:string) (m:t): int list =
    match String_map.maybe_find name m.map with
    | None ->
        []
    | Some e ->
        match e with
        | Global (_, lst) ->
            lst
        | Local i ->
            [i]



let add_unnamed (m: t): t =
    { m with
        cnt = 1 + m.cnt;
    }



let add_to_trie
    (typ: Term.typ)
    (gamma: Gamma.t)
    (trie: int Term_trie.t)
    : (int Term_trie.t, int) result
    =
    let cnt = Gamma.count gamma
    in
    Term_trie.add_new typ cnt cnt trie



let add_global
    (name: string)
    (typ: Term.typ)
    (gamma: Gamma.t)
    (m: t)
    : (t, int) result
    =
    assert (name <> "");
    assert (not (has_locals m));
    if name = "_" then
        Ok (add_unnamed m)
    else
        let module Algo = Gamma_algo.Make (Gamma)
        in
        let typ =
            Algo.normalize typ gamma
        in
        Result.(map
            (fun value ->
                {m with
                    map = String_map.add name value m.map;
                    cnt = m.cnt + 1})
            (
                match String_map.maybe_find name m.map with
                | None ->
                    map
                        (fun trie ->
                            Global (trie, [m.cnt]))
                        (add_to_trie typ gamma Term_trie.empty)

                | Some (Global (trie, lst)) ->
                    map
                        (fun trie ->
                            Global (trie, m.cnt :: lst))
                        (add_to_trie typ gamma trie)

                | Some (Local _) ->
                    assert false (* Cannot happen, there are no locals. *)
            )
        )


let add_global_strict
    (name: string)
    (typ: Term.typ)
    (gamma: Gamma.t)
    (m: t)
    : t
=
    match add_global name typ gamma m with
    | Ok m ->
        m
    | _ ->
        assert false (* Illegal call! *)



let add_local (name: string) (m: t) : t =
    assert (name <> "");
    if name = "_" then
        add_unnamed m
    else
    {
        map = String_map.add name (Local m.cnt) m.map;

        has_locs = true;

        cnt = 1 + m.cnt;
    }