Source file context.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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
open Fmlib
open Common



type t = {
    gamma: Gamma.t;
    map: Name_map.t
  }


let empty: t = {
        gamma = Gamma.empty;
        map   = Name_map.empty;
}


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 index_of_level (level: int) (c: t): int =
    Gamma.index_of_level level c.gamma

let level_of_index = index_of_level



let add_new_globals (gamma: Gamma.t) (c: t): t =
    let cnt0 = count c in
    assert (cnt0 <= Gamma.count gamma);
    {
        gamma;

        map =
        Interval.fold
            c.map
            (fun i m ->
                let open Gamma in
                match
                    Name_map.add_global
                        (name_at_level i gamma)
                        (type_at_level i gamma)
                        gamma
                        m
                with
                | Error _ ->
                    Printf.printf "Context.standard Cannot add %s\n"
                        (name_at_level i gamma);
                    assert false
                | Ok map ->
                    map
            )
            cnt0
            (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



let push_local (name: string) (typ: Term.typ) (c: t): t =
    {
        gamma =
            Gamma.push_local name typ c.gamma;

        map =
            Name_map.add_local name c.map;
    }



let can_add_global (name: string) (typ: Term.typ) (c: t): bool =
    match
        Name_map.add_global name typ c.gamma c.map
    with
    | Ok _ ->
        true
    | Error _ ->
        false



let add_axiom (name: string) (typ: Term.typ) (c: t): t =
    {
        gamma =
            Gamma.add_axiom name typ c.gamma;

        map =
            Name_map.add_global_strict name typ c.gamma c.map;
    }




let add_builtin_type
    (descr: string)
    (name: string)
    (typ: Term.typ)
    (c: t)
    : t
=
    {
        gamma =
            Gamma.add_builtin_type descr name typ c.gamma;

        map =
            Name_map.add_global_strict name typ c.gamma c.map;
    }



let add_builtin_function
    (descr: string)
    (name: string)
    (typ: Term.typ)
    (c: t)
    : t
=
    {
        gamma =
            Gamma.add_builtin_function descr name typ c.gamma;

        map =
            Name_map.add_global_strict name typ c.gamma c.map;
    }




let add_definition
    (name: string) (typ: Term.typ) (exp: Term.t) (c: t)
    : (t, int) result
=
    Result.map
        (fun map ->
            {
                map;

                gamma =
                    Gamma.add_definition name typ exp c.gamma
            })
        (Name_map.add_global
            name
            typ
            c.gamma
            c.map)



let add_inductive (ind: Inductive.t) (c: t): t =
    add_new_globals
        (Gamma.add_inductive ind c.gamma)
        c





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