source: driver/extracted/semanticsUtils.ml @ 3106

Last change on this file since 3106 was 3059, checked in by sacerdot, 7 years ago

New extraction

File size: 28.4 KB
Line 
1open Preamble
2
3open ExtraGlobalenvs
4
5open I8051bis
6
7open String
8
9open Sets
10
11open Listb
12
13open LabelledObjects
14
15open BitVectorTrie
16
17open Graphs
18
19open I8051
20
21open Order
22
23open Registers
24
25open BackEndOps
26
27open Joint
28
29open BEMem
30
31open CostLabel
32
33open Events
34
35open IOMonad
36
37open IO
38
39open Extra_bool
40
41open Coqlib
42
43open Values
44
45open FrontEndVal
46
47open Hide
48
49open ByteValues
50
51open Division
52
53open Z
54
55open BitVectorZ
56
57open Pointers
58
59open GenMem
60
61open FrontEndMem
62
63open Proper
64
65open PositiveMap
66
67open Deqsets
68
69open Extralib
70
71open Lists
72
73open Identifiers
74
75open Exp
76
77open Arithmetic
78
79open Vector
80
81open Div_and_mod
82
83open Util
84
85open FoldStuff
86
87open BitVector
88
89open Extranat
90
91open Integers
92
93open AST
94
95open ErrorMessages
96
97open Option
98
99open Setoids
100
101open Monad
102
103open Jmeq
104
105open Russell
106
107open Positive
108
109open PreIdentifiers
110
111open Bool
112
113open Relations
114
115open Nat
116
117open List
118
119open Hints_declaration
120
121open Core_notation
122
123open Pts
124
125open Logic
126
127open Types
128
129open Errors
130
131open Globalenvs
132
133open Joint_semantics
134
135open Deqsets_extra
136
137open State
138
139open Bind_new
140
141open BindLists
142
143open Blocks
144
145open TranslateUtils
146
147open ExtraMonads
148
149(** val reg_store :
150    PreIdentifiers.identifier -> ByteValues.beval -> ByteValues.beval
151    Identifiers.identifier_map -> ByteValues.beval Identifiers.identifier_map **)
152let reg_store reg v locals =
153  Identifiers.add PreIdentifiers.RegisterTag locals reg v
154
155(** val reg_retrieve :
156    ByteValues.beval Registers.register_env -> Registers.register ->
157    ByteValues.beval Errors.res **)
158let reg_retrieve locals reg =
159  Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadRegister),
160    (List.Cons ((Errors.CTX (PreIdentifiers.RegisterTag, reg)), List.Nil))))
161    (Identifiers.lookup PreIdentifiers.RegisterTag locals reg)
162
163type hw_register_env = { reg_env : ByteValues.beval
164                                   BitVectorTrie.bitVectorTrie;
165                         other_bit : ByteValues.bebit }
166
167(** val hw_register_env_rect_Type4 :
168    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
169    -> hw_register_env -> 'a1 **)
170let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_25009 =
171  let { reg_env = reg_env0; other_bit = other_bit0 } = x_25009 in
172  h_mk_hw_register_env reg_env0 other_bit0
173
174(** val hw_register_env_rect_Type5 :
175    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
176    -> hw_register_env -> 'a1 **)
177let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_25011 =
178  let { reg_env = reg_env0; other_bit = other_bit0 } = x_25011 in
179  h_mk_hw_register_env reg_env0 other_bit0
180
181(** val hw_register_env_rect_Type3 :
182    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
183    -> hw_register_env -> 'a1 **)
184let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_25013 =
185  let { reg_env = reg_env0; other_bit = other_bit0 } = x_25013 in
186  h_mk_hw_register_env reg_env0 other_bit0
187
188(** val hw_register_env_rect_Type2 :
189    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
190    -> hw_register_env -> 'a1 **)
191let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_25015 =
192  let { reg_env = reg_env0; other_bit = other_bit0 } = x_25015 in
193  h_mk_hw_register_env reg_env0 other_bit0
194
195(** val hw_register_env_rect_Type1 :
196    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
197    -> hw_register_env -> 'a1 **)
198let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_25017 =
199  let { reg_env = reg_env0; other_bit = other_bit0 } = x_25017 in
200  h_mk_hw_register_env reg_env0 other_bit0
201
202(** val hw_register_env_rect_Type0 :
203    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
204    -> hw_register_env -> 'a1 **)
205let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_25019 =
206  let { reg_env = reg_env0; other_bit = other_bit0 } = x_25019 in
207  h_mk_hw_register_env reg_env0 other_bit0
208
209(** val reg_env :
210    hw_register_env -> ByteValues.beval BitVectorTrie.bitVectorTrie **)
211let rec reg_env xxx =
212  xxx.reg_env
213
214(** val other_bit : hw_register_env -> ByteValues.bebit **)
215let rec other_bit xxx =
216  xxx.other_bit
217
218(** val hw_register_env_inv_rect_Type4 :
219    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
220    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
221let hw_register_env_inv_rect_Type4 hterm h1 =
222  let hcut = hw_register_env_rect_Type4 h1 hterm in hcut __
223
224(** val hw_register_env_inv_rect_Type3 :
225    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
226    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
227let hw_register_env_inv_rect_Type3 hterm h1 =
228  let hcut = hw_register_env_rect_Type3 h1 hterm in hcut __
229
230(** val hw_register_env_inv_rect_Type2 :
231    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
232    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
233let hw_register_env_inv_rect_Type2 hterm h1 =
234  let hcut = hw_register_env_rect_Type2 h1 hterm in hcut __
235
236(** val hw_register_env_inv_rect_Type1 :
237    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
238    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
239let hw_register_env_inv_rect_Type1 hterm h1 =
240  let hcut = hw_register_env_rect_Type1 h1 hterm in hcut __
241
242(** val hw_register_env_inv_rect_Type0 :
243    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
244    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
245let hw_register_env_inv_rect_Type0 hterm h1 =
246  let hcut = hw_register_env_rect_Type0 h1 hterm in hcut __
247
248(** val hw_register_env_discr : hw_register_env -> hw_register_env -> __ **)
249let hw_register_env_discr x y =
250  Logic.eq_rect_Type2 x
251    (let { reg_env = a0; other_bit = a1 } = x in
252    Obj.magic (fun _ dH -> dH __ __)) y
253
254(** val hw_register_env_jmdiscr :
255    hw_register_env -> hw_register_env -> __ **)
256let hw_register_env_jmdiscr x y =
257  Logic.eq_rect_Type2 x
258    (let { reg_env = a0; other_bit = a1 } = x in
259    Obj.magic (fun _ dH -> dH __ __)) y
260
261(** val hwreg_retrieve :
262    hw_register_env -> I8051.register -> ByteValues.beval **)
263let hwreg_retrieve env r =
264  BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
265    (I8051.bitvector_of_register r) env.reg_env ByteValues.BVundef
266
267(** val hwreg_store :
268    I8051.register -> ByteValues.beval -> hw_register_env -> hw_register_env **)
269let hwreg_store r v env =
270  { reg_env =
271    (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
272      Nat.O)))))) (I8051.bitvector_of_register r) v env.reg_env); other_bit =
273    env.other_bit }
274
275(** val hwreg_set_other :
276    ByteValues.bebit -> hw_register_env -> hw_register_env **)
277let hwreg_set_other v env =
278  { reg_env = env.reg_env; other_bit = v }
279
280(** val hwreg_retrieve_sp :
281    hw_register_env -> ByteValues.xpointer Errors.res **)
282let hwreg_retrieve_sp env =
283  let spl = hwreg_retrieve env I8051.registerSPL in
284  let sph = hwreg_retrieve env I8051.registerSPH in
285  Obj.magic
286    (Monad.m_bind0 (Monad.max_def Errors.res0)
287      (Obj.magic
288        (BEMem.pointer_of_address { Types.fst = spl; Types.snd = sph }))
289      (fun ptr ->
290      (match Pointers.ptype ptr with
291       | AST.XData ->
292         (fun _ -> Monad.m_return0 (Monad.max_def Errors.res0) ptr)
293       | AST.Code ->
294         (fun _ ->
295           Obj.magic (Errors.Error (List.Cons ((Errors.MSG
296             ErrorMessages.BadPointer), List.Nil))))) __))
297
298(** val hwreg_store_sp :
299    hw_register_env -> ByteValues.xpointer -> hw_register_env **)
300let hwreg_store_sp env sp =
301  let { Types.fst = spl; Types.snd = sph } =
302    ByteValues.beval_pair_of_pointer (Types.pi1 sp)
303  in
304  hwreg_store I8051.registerSPH sph (hwreg_store I8051.registerSPL spl env)
305
306(** val init_hw_register_env : ByteValues.xpointer -> hw_register_env **)
307let init_hw_register_env =
308  hwreg_store_sp { reg_env = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S
309    (Nat.S (Nat.S Nat.O))))))); other_bit = ByteValues.BBundef }
310
311type sem_graph_params = { sgp_pars : Joint.uns_params;
312                          sgp_sup : (__ -> __
313                                    Joint_semantics.sem_unserialized_params);
314                          graph_pre_main_generator : (Joint.joint_program ->
315                                                     Joint.joint_closed_internal_function) }
316
317(** val sem_graph_params_rect_Type4 :
318    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
319    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
320    -> sem_graph_params -> 'a1 **)
321let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_25035 =
322  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
323    graph_pre_main_generator0 } = x_25035
324  in
325  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
326
327(** val sem_graph_params_rect_Type5 :
328    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
329    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
330    -> sem_graph_params -> 'a1 **)
331let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_25037 =
332  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
333    graph_pre_main_generator0 } = x_25037
334  in
335  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
336
337(** val sem_graph_params_rect_Type3 :
338    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
339    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
340    -> sem_graph_params -> 'a1 **)
341let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_25039 =
342  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
343    graph_pre_main_generator0 } = x_25039
344  in
345  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
346
347(** val sem_graph_params_rect_Type2 :
348    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
349    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
350    -> sem_graph_params -> 'a1 **)
351let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_25041 =
352  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
353    graph_pre_main_generator0 } = x_25041
354  in
355  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
356
357(** val sem_graph_params_rect_Type1 :
358    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
359    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
360    -> sem_graph_params -> 'a1 **)
361let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_25043 =
362  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
363    graph_pre_main_generator0 } = x_25043
364  in
365  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
366
367(** val sem_graph_params_rect_Type0 :
368    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
369    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
370    -> sem_graph_params -> 'a1 **)
371let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_25045 =
372  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
373    graph_pre_main_generator0 } = x_25045
374  in
375  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
376
377(** val sgp_pars : sem_graph_params -> Joint.uns_params **)
378let rec sgp_pars xxx =
379  xxx.sgp_pars
380
381(** val sgp_sup0 :
382    sem_graph_params -> 'a1 Joint_semantics.sem_unserialized_params **)
383let rec sgp_sup0 xxx =
384  (let { sgp_pars = x; sgp_sup = yyy; graph_pre_main_generator = x0 } = xxx
385   in
386  Obj.magic yyy) __
387
388(** val graph_pre_main_generator :
389    sem_graph_params -> Joint.joint_program ->
390    Joint.joint_closed_internal_function **)
391let rec graph_pre_main_generator xxx =
392  xxx.graph_pre_main_generator
393
394(** val sem_graph_params_inv_rect_Type4 :
395    sem_graph_params -> (Joint.uns_params -> (__ -> __
396    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
397    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
398let sem_graph_params_inv_rect_Type4 hterm h1 =
399  let hcut = sem_graph_params_rect_Type4 h1 hterm in hcut __
400
401(** val sem_graph_params_inv_rect_Type3 :
402    sem_graph_params -> (Joint.uns_params -> (__ -> __
403    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
404    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
405let sem_graph_params_inv_rect_Type3 hterm h1 =
406  let hcut = sem_graph_params_rect_Type3 h1 hterm in hcut __
407
408(** val sem_graph_params_inv_rect_Type2 :
409    sem_graph_params -> (Joint.uns_params -> (__ -> __
410    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
411    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
412let sem_graph_params_inv_rect_Type2 hterm h1 =
413  let hcut = sem_graph_params_rect_Type2 h1 hterm in hcut __
414
415(** val sem_graph_params_inv_rect_Type1 :
416    sem_graph_params -> (Joint.uns_params -> (__ -> __
417    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
418    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
419let sem_graph_params_inv_rect_Type1 hterm h1 =
420  let hcut = sem_graph_params_rect_Type1 h1 hterm in hcut __
421
422(** val sem_graph_params_inv_rect_Type0 :
423    sem_graph_params -> (Joint.uns_params -> (__ -> __
424    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
425    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
426let sem_graph_params_inv_rect_Type0 hterm h1 =
427  let hcut = sem_graph_params_rect_Type0 h1 hterm in hcut __
428
429(** val sem_graph_params_jmdiscr :
430    sem_graph_params -> sem_graph_params -> __ **)
431let sem_graph_params_jmdiscr x y =
432  Logic.eq_rect_Type2 x
433    (let { sgp_pars = a0; sgp_sup = a1; graph_pre_main_generator = a2 } = x
434     in
435    Obj.magic (fun _ dH -> dH __ __ __)) y
436
437(** val sem_graph_params_to_graph_params :
438    sem_graph_params -> Joint.graph_params **)
439let sem_graph_params_to_graph_params pars =
440  pars.sgp_pars
441
442(** val sem_graph_params_to_sem_params :
443    sem_graph_params -> Joint_semantics.sem_params **)
444let sem_graph_params_to_sem_params pars =
445  { Joint_semantics.spp' = { Joint_semantics.spp =
446    (let x = sem_graph_params_to_graph_params pars in
447    Joint.graph_params_to_params x); Joint_semantics.msu_pars =
448    (sgp_sup0 pars); Joint_semantics.offset_of_point =
449    (Obj.magic (Identifiers.word_of_identifier PreIdentifiers.LabelTag));
450    Joint_semantics.point_of_offset = (Obj.magic (fun x -> x)) };
451    Joint_semantics.pre_main_generator = pars.graph_pre_main_generator }
452
453(** val sem_params_from_sem_graph_params__o__spp' :
454    sem_graph_params -> Joint_semantics.serialized_params **)
455let sem_params_from_sem_graph_params__o__spp' x0 =
456  (sem_graph_params_to_sem_params x0).Joint_semantics.spp'
457
458(** val sem_params_from_sem_graph_params__o__spp'__o__msu_pars :
459    sem_graph_params -> Joint.joint_closed_internal_function
460    Joint_semantics.sem_unserialized_params **)
461let sem_params_from_sem_graph_params__o__spp'__o__msu_pars x0 =
462  Joint_semantics.spp'__o__msu_pars (sem_graph_params_to_sem_params x0)
463
464(** val sem_params_from_sem_graph_params__o__spp'__o__msu_pars__o__st_pars :
465    sem_graph_params -> Joint_semantics.sem_state_params **)
466let sem_params_from_sem_graph_params__o__spp'__o__msu_pars__o__st_pars x0 =
467  Joint_semantics.spp'__o__msu_pars__o__st_pars
468    (sem_graph_params_to_sem_params x0)
469
470(** val sem_params_from_sem_graph_params__o__spp'__o__spp :
471    sem_graph_params -> Joint.params **)
472let sem_params_from_sem_graph_params__o__spp'__o__spp x0 =
473  Joint_semantics.spp'__o__spp (sem_graph_params_to_sem_params x0)
474
475(** val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars :
476    sem_graph_params -> Joint.stmt_params **)
477let sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars x0 =
478  Joint_semantics.spp'__o__spp__o__stmt_pars
479    (sem_graph_params_to_sem_params x0)
480
481(** val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
482    sem_graph_params -> Joint.uns_params **)
483let sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
484  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars
485    (sem_graph_params_to_sem_params x0)
486
487(** val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
488    sem_graph_params -> Joint.unserialized_params **)
489let sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
490  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
491    (sem_graph_params_to_sem_params x0)
492
493type sem_lin_params = { slp_pars : Joint.uns_params;
494                        slp_sup : (__ -> __
495                                  Joint_semantics.sem_unserialized_params);
496                        lin_pre_main_generator : (Joint.joint_program ->
497                                                 Joint.joint_closed_internal_function) }
498
499(** val sem_lin_params_rect_Type4 :
500    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
501    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
502    -> sem_lin_params -> 'a1 **)
503let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_25062 =
504  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
505    lin_pre_main_generator0 } = x_25062
506  in
507  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
508
509(** val sem_lin_params_rect_Type5 :
510    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
511    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
512    -> sem_lin_params -> 'a1 **)
513let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_25064 =
514  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
515    lin_pre_main_generator0 } = x_25064
516  in
517  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
518
519(** val sem_lin_params_rect_Type3 :
520    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
521    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
522    -> sem_lin_params -> 'a1 **)
523let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_25066 =
524  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
525    lin_pre_main_generator0 } = x_25066
526  in
527  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
528
529(** val sem_lin_params_rect_Type2 :
530    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
531    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
532    -> sem_lin_params -> 'a1 **)
533let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_25068 =
534  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
535    lin_pre_main_generator0 } = x_25068
536  in
537  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
538
539(** val sem_lin_params_rect_Type1 :
540    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
541    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
542    -> sem_lin_params -> 'a1 **)
543let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_25070 =
544  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
545    lin_pre_main_generator0 } = x_25070
546  in
547  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
548
549(** val sem_lin_params_rect_Type0 :
550    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
551    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
552    -> sem_lin_params -> 'a1 **)
553let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_25072 =
554  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
555    lin_pre_main_generator0 } = x_25072
556  in
557  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
558
559(** val slp_pars : sem_lin_params -> Joint.uns_params **)
560let rec slp_pars xxx =
561  xxx.slp_pars
562
563(** val slp_sup0 :
564    sem_lin_params -> 'a1 Joint_semantics.sem_unserialized_params **)
565let rec slp_sup0 xxx =
566  (let { slp_pars = x; slp_sup = yyy; lin_pre_main_generator = x0 } = xxx in
567  Obj.magic yyy) __
568
569(** val lin_pre_main_generator :
570    sem_lin_params -> Joint.joint_program ->
571    Joint.joint_closed_internal_function **)
572let rec lin_pre_main_generator xxx =
573  xxx.lin_pre_main_generator
574
575(** val sem_lin_params_inv_rect_Type4 :
576    sem_lin_params -> (Joint.uns_params -> (__ -> __
577    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
578    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
579let sem_lin_params_inv_rect_Type4 hterm h1 =
580  let hcut = sem_lin_params_rect_Type4 h1 hterm in hcut __
581
582(** val sem_lin_params_inv_rect_Type3 :
583    sem_lin_params -> (Joint.uns_params -> (__ -> __
584    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
585    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
586let sem_lin_params_inv_rect_Type3 hterm h1 =
587  let hcut = sem_lin_params_rect_Type3 h1 hterm in hcut __
588
589(** val sem_lin_params_inv_rect_Type2 :
590    sem_lin_params -> (Joint.uns_params -> (__ -> __
591    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
592    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
593let sem_lin_params_inv_rect_Type2 hterm h1 =
594  let hcut = sem_lin_params_rect_Type2 h1 hterm in hcut __
595
596(** val sem_lin_params_inv_rect_Type1 :
597    sem_lin_params -> (Joint.uns_params -> (__ -> __
598    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
599    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
600let sem_lin_params_inv_rect_Type1 hterm h1 =
601  let hcut = sem_lin_params_rect_Type1 h1 hterm in hcut __
602
603(** val sem_lin_params_inv_rect_Type0 :
604    sem_lin_params -> (Joint.uns_params -> (__ -> __
605    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
606    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
607let sem_lin_params_inv_rect_Type0 hterm h1 =
608  let hcut = sem_lin_params_rect_Type0 h1 hterm in hcut __
609
610(** val sem_lin_params_jmdiscr : sem_lin_params -> sem_lin_params -> __ **)
611let sem_lin_params_jmdiscr x y =
612  Logic.eq_rect_Type2 x
613    (let { slp_pars = a0; slp_sup = a1; lin_pre_main_generator = a2 } = x in
614    Obj.magic (fun _ dH -> dH __ __ __)) y
615
616(** val sem_lin_params_to_lin_params : sem_lin_params -> Joint.lin_params **)
617let sem_lin_params_to_lin_params pars =
618  pars.slp_pars
619
620(** val sem_lin_params_to_sem_params :
621    sem_lin_params -> Joint_semantics.sem_params **)
622let sem_lin_params_to_sem_params pars =
623  { Joint_semantics.spp' = { Joint_semantics.spp =
624    (let x = sem_lin_params_to_lin_params pars in
625    Joint.lin_params_to_params x); Joint_semantics.msu_pars =
626    (slp_sup0 pars); Joint_semantics.offset_of_point =
627    (Obj.magic Positive.succ_pos_of_nat); Joint_semantics.point_of_offset =
628    (fun p -> Obj.magic (Nat.pred (Positive.nat_of_pos p))) };
629    Joint_semantics.pre_main_generator = pars.lin_pre_main_generator }
630
631(** val sem_params_from_sem_lin_params__o__spp' :
632    sem_lin_params -> Joint_semantics.serialized_params **)
633let sem_params_from_sem_lin_params__o__spp' x0 =
634  (sem_lin_params_to_sem_params x0).Joint_semantics.spp'
635
636(** val sem_params_from_sem_lin_params__o__spp'__o__msu_pars :
637    sem_lin_params -> Joint.joint_closed_internal_function
638    Joint_semantics.sem_unserialized_params **)
639let sem_params_from_sem_lin_params__o__spp'__o__msu_pars x0 =
640  Joint_semantics.spp'__o__msu_pars (sem_lin_params_to_sem_params x0)
641
642(** val sem_params_from_sem_lin_params__o__spp'__o__msu_pars__o__st_pars :
643    sem_lin_params -> Joint_semantics.sem_state_params **)
644let sem_params_from_sem_lin_params__o__spp'__o__msu_pars__o__st_pars x0 =
645  Joint_semantics.spp'__o__msu_pars__o__st_pars
646    (sem_lin_params_to_sem_params x0)
647
648(** val sem_params_from_sem_lin_params__o__spp'__o__spp :
649    sem_lin_params -> Joint.params **)
650let sem_params_from_sem_lin_params__o__spp'__o__spp x0 =
651  Joint_semantics.spp'__o__spp (sem_lin_params_to_sem_params x0)
652
653(** val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars :
654    sem_lin_params -> Joint.stmt_params **)
655let sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars x0 =
656  Joint_semantics.spp'__o__spp__o__stmt_pars
657    (sem_lin_params_to_sem_params x0)
658
659(** val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
660    sem_lin_params -> Joint.uns_params **)
661let sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
662  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars
663    (sem_lin_params_to_sem_params x0)
664
665(** val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
666    sem_lin_params -> Joint.unserialized_params **)
667let sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
668  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
669    (sem_lin_params_to_sem_params x0)
670
671(** val match_genv_t_rect_Type4 :
672    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
673    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
674let rec match_genv_t_rect_Type4 m vars ge1 ge2 h_mk_match_genv_t =
675  h_mk_match_genv_t __ __ __
676
677(** val match_genv_t_rect_Type5 :
678    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
679    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
680let rec match_genv_t_rect_Type5 m vars ge1 ge2 h_mk_match_genv_t =
681  h_mk_match_genv_t __ __ __
682
683(** val match_genv_t_rect_Type3 :
684    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
685    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
686let rec match_genv_t_rect_Type3 m vars ge1 ge2 h_mk_match_genv_t =
687  h_mk_match_genv_t __ __ __
688
689(** val match_genv_t_rect_Type2 :
690    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
691    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
692let rec match_genv_t_rect_Type2 m vars ge1 ge2 h_mk_match_genv_t =
693  h_mk_match_genv_t __ __ __
694
695(** val match_genv_t_rect_Type1 :
696    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
697    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
698let rec match_genv_t_rect_Type1 m vars ge1 ge2 h_mk_match_genv_t =
699  h_mk_match_genv_t __ __ __
700
701(** val match_genv_t_rect_Type0 :
702    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
703    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
704let rec match_genv_t_rect_Type0 m vars ge1 ge2 h_mk_match_genv_t =
705  h_mk_match_genv_t __ __ __
706
707(** val match_genv_t_inv_rect_Type4 :
708    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
709    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
710let match_genv_t_inv_rect_Type4 x1 x2 x3 x4 h1 =
711  let hcut = match_genv_t_rect_Type4 x1 x2 x3 x4 h1 in hcut __
712
713(** val match_genv_t_inv_rect_Type3 :
714    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
715    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
716let match_genv_t_inv_rect_Type3 x1 x2 x3 x4 h1 =
717  let hcut = match_genv_t_rect_Type3 x1 x2 x3 x4 h1 in hcut __
718
719(** val match_genv_t_inv_rect_Type2 :
720    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
721    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
722let match_genv_t_inv_rect_Type2 x1 x2 x3 x4 h1 =
723  let hcut = match_genv_t_rect_Type2 x1 x2 x3 x4 h1 in hcut __
724
725(** val match_genv_t_inv_rect_Type1 :
726    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
727    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
728let match_genv_t_inv_rect_Type1 x1 x2 x3 x4 h1 =
729  let hcut = match_genv_t_rect_Type1 x1 x2 x3 x4 h1 in hcut __
730
731(** val match_genv_t_inv_rect_Type0 :
732    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
733    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
734let match_genv_t_inv_rect_Type0 x1 x2 x3 x4 h1 =
735  let hcut = match_genv_t_rect_Type0 x1 x2 x3 x4 h1 in hcut __
736
737(** val match_genv_t_discr :
738    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
739    Globalenvs.genv_t -> __ **)
740let match_genv_t_discr a1 a2 a3 a4 =
741  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
742
743(** val match_genv_t_jmdiscr :
744    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
745    Globalenvs.genv_t -> __ **)
746let match_genv_t_jmdiscr a1 a2 a3 a4 =
747  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
748
749(** val joint_globalenv :
750    Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
751    Nat.nat Types.option) -> Joint_semantics.genv **)
752let joint_globalenv p prog stacksizes =
753  let genv = Globalenvs.globalenv (fun x -> x) prog.Joint.joint_prog in
754  let pc_from_lbl = fun bl fn lbl ->
755    Monad.m_bind0 (Monad.max_def Option.option)
756      (Obj.magic
757        ((Joint_semantics.spp'__o__spp p).Joint.point_of_label
758          (Joint.prog_names (Joint_semantics.spp'__o__spp p) prog)
759          (Types.pi1 fn).Joint.joint_if_code lbl)) (fun pt ->
760      Monad.m_return0 (Monad.max_def Option.option) { ByteValues.pc_block =
761        bl; ByteValues.pc_offset =
762        (p.Joint_semantics.spp'.Joint_semantics.offset_of_point pt) })
763  in
764  { Joint_semantics.ge = genv; Joint_semantics.stack_sizes = stacksizes;
765  Joint_semantics.premain = (p.Joint_semantics.pre_main_generator prog);
766  Joint_semantics.pc_from_label = (Obj.magic pc_from_lbl) }
767
Note: See TracBrowser for help on using the repository browser.