aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/csymtable.ml
blob: 7e1a5d5b7e79951f6d09037148c27cb6f5c82632 (plain)
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
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Created by Bruno Barras for Benjamin Grégoire as part of the
   bytecode-based reduction machine, Oct 2004 *)
(* Bug fix #1419 by Jean-Marc Notin, Mar 2007 *)

(* This file manages the table of global symbols for the bytecode machine *)

open Util
open Names
open Term
open Context
open Vm
open Cemitcodes
open Cbytecodes
open Declarations
open Pre_env
open Cbytegen


external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"

(*******************)
(* Linkage du code *)
(*******************)

(* Table des globaux *)

(* [global_data] contient les valeurs des constantes globales
   (axiomes,definitions), les annotations des switch et les structured
   constant *)
external global_data : unit -> values array = "get_coq_global_data"

(* [realloc_global_data n] augmente de n la taille de [global_data] *)
external realloc_global_data : int -> unit = "realloc_coq_global_data"

let check_global_data n =
  if n >= Array.length (global_data()) then realloc_global_data n

let num_global = ref 0

let set_global v =
  let n = !num_global in
  check_global_data n;
  (global_data()).(n) <- v;
  incr num_global;
  n

(* table pour les structured_constant et les annotations des switchs *)

let rec eq_structured_constant c1 c2 = match c1, c2 with
| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
| Const_sorts _, _ -> false
| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
| Const_ind _, _ -> false
| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
| Const_proj _, _ -> false
| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
| Const_b0 _, _ -> false
| Const_bn (t1, a1), Const_bn (t2, a2) ->
  Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
| Const_bn _, _ -> false
| Const_univ_level l1 , Const_univ_level l2 -> Univ.eq_levels l1 l2
| Const_univ_level _ , _ -> false
| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2
| Const_type _ , _ -> false

let rec hash_structured_constant c =
  let open Hashset.Combine in
  match c with
  | Const_sorts s -> combinesmall 1 (Sorts.hash s)
  | Const_ind i -> combinesmall 2 (ind_hash i)
  | Const_proj p -> combinesmall 3 (Constant.hash p)
  | Const_b0 t -> combinesmall 4 (Int.hash t)
  | Const_bn (t, a) ->
    let fold h c = combine h (hash_structured_constant c) in
    let h = Array.fold_left fold 0 a in
    combinesmall 5 (combine (Int.hash t) h)
  | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l)
  | Const_type u -> combinesmall 7 (Univ.Universe.hash u)

module SConstTable = Hashtbl.Make (struct
  type t = structured_constant
  let equal = eq_structured_constant
  let hash = hash_structured_constant
end)

let eq_annot_switch asw1 asw2 =
  let eq_ci ci1 ci2 =
    eq_ind ci1.ci_ind ci2.ci_ind &&
    Int.equal ci1.ci_npar ci2.ci_npar &&
    Array.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
  in
  let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in
  eq_ci asw1.ci asw2.ci &&
  Array.equal eq_rlc asw1.rtbl asw2.rtbl &&
  (asw1.tailcall : bool) == asw2.tailcall

let hash_annot_switch asw =
  let open Hashset.Combine in
  let h1 = Constr.case_info_hash asw.ci in
  let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
  let h3 = if asw.tailcall then 1 else 0 in
  combine3 h1 h2 h3

module AnnotTable = Hashtbl.Make (struct
  type t = annot_switch
  let equal = eq_annot_switch
  let hash = hash_annot_switch
end)

let str_cst_tbl : int SConstTable.t = SConstTable.create 31

let annot_tbl : int AnnotTable.t = AnnotTable.create 31
    (* (annot_switch * int) Hashtbl.t  *)

(*************************************************************)
(*** Mise a jour des valeurs des variables et des constantes *)
(*************************************************************)

exception NotEvaluated

let key rk =
  match !rk with
  | None -> raise NotEvaluated
  | Some k ->
      try CEphemeron.get k
      with CEphemeron.InvalidKey -> raise NotEvaluated

(************************)
(* traduction des patch *)

(* slot_for_*, calcul la valeur de l'objet, la place
   dans la table global, rend sa position dans la table *)

let slot_for_str_cst key =
  try SConstTable.find str_cst_tbl key
  with Not_found ->
    let n = set_global (val_of_str_const key) in
    SConstTable.add str_cst_tbl key n;
    n

let slot_for_annot key =
  try AnnotTable.find annot_tbl key
  with Not_found ->
    let n =  set_global (val_of_annot_switch key) in
    AnnotTable.add annot_tbl key n;
    n

let rec slot_for_getglobal env kn =
  let (cb,(_,rk)) = lookup_constant_key kn env in
  try key rk
  with NotEvaluated ->
(*    Pp.msgnl(str"not yet evaluated");*)
    let pos =
      match cb.const_body_code with
      | None -> set_global (val_of_constant kn)
      | Some code ->
	 match Cemitcodes.force code with
	 | BCdefined(code,pl,fv) ->
           let v = eval_to_patch env (code,pl,fv) in
           set_global v
	 | BCalias kn' -> slot_for_getglobal env kn'
	 | BCconstant -> set_global (val_of_constant kn)
    in
(*Pp.msgnl(str"value stored at: "++int pos);*)
    rk := Some (CEphemeron.create pos);
    pos

and slot_for_fv env fv =
  let fill_fv_cache cache id v_of_id env_of_id b =
    let v,d =
      match b with
      | None -> v_of_id id, Id.Set.empty
      | Some c ->
          val_of_constr (env_of_id id env) c,
          Environ.global_vars_set (Environ.env_of_pre_env env) c in
    build_lazy_val cache (v, d); v in
  let val_of_rel i = val_of_rel (nb_rel env - i) in
  let idfun _ x = x in
  match fv with
  | FVnamed id ->
      let nv = Pre_env.lookup_named_val id env in
      begin match force_lazy_val nv with
      | None ->
          let _, b, _ = Context.lookup_named id env.env_named_context in
          fill_fv_cache nv id val_of_named idfun b
      | Some (v, _) -> v
      end
  | FVrel i ->
      let rv = Pre_env.lookup_rel_val i env in
      begin match force_lazy_val rv with
      | None ->
          let _, b, _ = lookup_rel i env.env_rel_context in
          fill_fv_cache rv i val_of_rel env_of_rel b
      | Some (v, _) -> v
      end
  | FVuniv_var idu ->
    assert false

and eval_to_patch env (buff,pl,fv) =
  (* copy code *before* patching because of nested evaluations:
     the code we are patching might be called (and thus "concurrently" patched)
     and results in wrong results. Side-effects... *)
  let buff = Cemitcodes.copy buff in
  let patch = function
    | Reloc_annot a, pos -> patch_int buff pos (slot_for_annot a)
    | Reloc_const sc, pos -> patch_int buff pos (slot_for_str_cst sc)
    | Reloc_getglobal kn, pos ->
(*      Pp.msgnl (str"patching global: "++str(debug_string_of_con kn));*)
	patch_int buff pos (slot_for_getglobal env kn);
(*      Pp.msgnl (str"patch done: "++str(debug_string_of_con kn))*)
  in
  List.iter patch pl;
  let vm_env = Array.map (slot_for_fv env) fv in
  let tc = tcode_of_code buff (length buff) in
  eval_tcode tc vm_env

and val_of_constr env c =
  let (_,fun_code,_ as ccfv) =
    try match compile true env c with
	| Some v -> v
	| None -> assert false
    with reraise ->
      let reraise = Errors.push reraise in
      let () = print_string "can not compile \n" in
      let () = Format.print_flush () in
      iraise reraise
  in
  eval_to_patch env (to_memory ccfv)

let set_transparent_const kn = () (* !?! *)
let set_opaque_const kn = () (* !?! *)