source: extracted/semanticsUtils.ml @ 2829

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

Semantics files committed.

File size: 28.0 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
149type hw_register_env = { reg_env : ByteValues.beval
150                                   BitVectorTrie.bitVectorTrie;
151                         other_bit : ByteValues.bebit }
152
153(** val hw_register_env_rect_Type4 :
154    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
155    -> hw_register_env -> 'a1 **)
156let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_3 =
157  let { reg_env = reg_env0; other_bit = other_bit0 } = x_3 in
158  h_mk_hw_register_env reg_env0 other_bit0
159
160(** val hw_register_env_rect_Type5 :
161    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
162    -> hw_register_env -> 'a1 **)
163let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_5 =
164  let { reg_env = reg_env0; other_bit = other_bit0 } = x_5 in
165  h_mk_hw_register_env reg_env0 other_bit0
166
167(** val hw_register_env_rect_Type3 :
168    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
169    -> hw_register_env -> 'a1 **)
170let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_7 =
171  let { reg_env = reg_env0; other_bit = other_bit0 } = x_7 in
172  h_mk_hw_register_env reg_env0 other_bit0
173
174(** val hw_register_env_rect_Type2 :
175    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
176    -> hw_register_env -> 'a1 **)
177let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_9 =
178  let { reg_env = reg_env0; other_bit = other_bit0 } = x_9 in
179  h_mk_hw_register_env reg_env0 other_bit0
180
181(** val hw_register_env_rect_Type1 :
182    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
183    -> hw_register_env -> 'a1 **)
184let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_11 =
185  let { reg_env = reg_env0; other_bit = other_bit0 } = x_11 in
186  h_mk_hw_register_env reg_env0 other_bit0
187
188(** val hw_register_env_rect_Type0 :
189    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
190    -> hw_register_env -> 'a1 **)
191let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_13 =
192  let { reg_env = reg_env0; other_bit = other_bit0 } = x_13 in
193  h_mk_hw_register_env reg_env0 other_bit0
194
195(** val reg_env :
196    hw_register_env -> ByteValues.beval BitVectorTrie.bitVectorTrie **)
197let rec reg_env xxx =
198  xxx.reg_env
199
200(** val other_bit : hw_register_env -> ByteValues.bebit **)
201let rec other_bit xxx =
202  xxx.other_bit
203
204(** val hw_register_env_inv_rect_Type4 :
205    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
206    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
207let hw_register_env_inv_rect_Type4 hterm h1 =
208  let hcut = hw_register_env_rect_Type4 h1 hterm in hcut __
209
210(** val hw_register_env_inv_rect_Type3 :
211    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
212    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
213let hw_register_env_inv_rect_Type3 hterm h1 =
214  let hcut = hw_register_env_rect_Type3 h1 hterm in hcut __
215
216(** val hw_register_env_inv_rect_Type2 :
217    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
218    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
219let hw_register_env_inv_rect_Type2 hterm h1 =
220  let hcut = hw_register_env_rect_Type2 h1 hterm in hcut __
221
222(** val hw_register_env_inv_rect_Type1 :
223    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
224    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
225let hw_register_env_inv_rect_Type1 hterm h1 =
226  let hcut = hw_register_env_rect_Type1 h1 hterm in hcut __
227
228(** val hw_register_env_inv_rect_Type0 :
229    hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
230    ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
231let hw_register_env_inv_rect_Type0 hterm h1 =
232  let hcut = hw_register_env_rect_Type0 h1 hterm in hcut __
233
234(** val hw_register_env_discr : hw_register_env -> hw_register_env -> __ **)
235let hw_register_env_discr x y =
236  Logic.eq_rect_Type2 x
237    (let { reg_env = a0; other_bit = a1 } = x in
238    Obj.magic (fun _ dH -> dH __ __)) y
239
240(** val hw_register_env_jmdiscr :
241    hw_register_env -> hw_register_env -> __ **)
242let hw_register_env_jmdiscr x y =
243  Logic.eq_rect_Type2 x
244    (let { reg_env = a0; other_bit = a1 } = x in
245    Obj.magic (fun _ dH -> dH __ __)) y
246
247(** val empty_hw_register_env : hw_register_env **)
248let empty_hw_register_env =
249  { reg_env = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
250    Nat.O))))))); other_bit = ByteValues.BBundef }
251
252(** val hwreg_retrieve :
253    hw_register_env -> I8051.register -> ByteValues.beval **)
254let hwreg_retrieve env r =
255  BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
256    (I8051.bitvector_of_register r) env.reg_env ByteValues.BVundef
257
258(** val hwreg_store :
259    I8051.register -> ByteValues.beval -> hw_register_env -> hw_register_env **)
260let hwreg_store r v env =
261  { reg_env =
262    (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
263      Nat.O)))))) (I8051.bitvector_of_register r) v env.reg_env); other_bit =
264    env.other_bit }
265
266(** val hwreg_set_other :
267    ByteValues.bebit -> hw_register_env -> hw_register_env **)
268let hwreg_set_other v env =
269  { reg_env = env.reg_env; other_bit = v }
270
271(** val hwreg_retrieve_sp :
272    hw_register_env -> ByteValues.xpointer Errors.res **)
273let hwreg_retrieve_sp env =
274  let spl = hwreg_retrieve env I8051.registerSPL in
275  let sph = hwreg_retrieve env I8051.registerSPH in
276  Obj.magic
277    (Monad.m_bind0 (Monad.max_def Errors.res0)
278      (Obj.magic
279        (BEMem.pointer_of_address { Types.fst = spl; Types.snd = sph }))
280      (fun ptr ->
281      (match Pointers.ptype ptr with
282       | AST.XData ->
283         (fun _ -> Monad.m_return0 (Monad.max_def Errors.res0) ptr)
284       | AST.Code ->
285         (fun _ ->
286           Obj.magic (Errors.Error (List.Cons ((Errors.MSG
287             ErrorMessages.BadPointer), List.Nil))))) __))
288
289(** val hwreg_store_sp :
290    hw_register_env -> ByteValues.xpointer -> hw_register_env **)
291let hwreg_store_sp env sp =
292  let { Types.fst = spl; Types.snd = sph } =
293    ByteValues.beval_pair_of_pointer (Types.pi1 sp)
294  in
295  hwreg_store I8051.registerSPH sph (hwreg_store I8051.registerSPL spl env)
296
297type reg_sp = { reg_sp_env : ByteValues.beval Identifiers.identifier_map;
298                stackp : ByteValues.xpointer }
299
300(** val reg_sp_rect_Type4 :
301    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
302    'a1) -> reg_sp -> 'a1 **)
303let rec reg_sp_rect_Type4 h_mk_reg_sp x_29 =
304  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_29 in
305  h_mk_reg_sp reg_sp_env0 stackp0
306
307(** val reg_sp_rect_Type5 :
308    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
309    'a1) -> reg_sp -> 'a1 **)
310let rec reg_sp_rect_Type5 h_mk_reg_sp x_31 =
311  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_31 in
312  h_mk_reg_sp reg_sp_env0 stackp0
313
314(** val reg_sp_rect_Type3 :
315    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
316    'a1) -> reg_sp -> 'a1 **)
317let rec reg_sp_rect_Type3 h_mk_reg_sp x_33 =
318  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_33 in
319  h_mk_reg_sp reg_sp_env0 stackp0
320
321(** val reg_sp_rect_Type2 :
322    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
323    'a1) -> reg_sp -> 'a1 **)
324let rec reg_sp_rect_Type2 h_mk_reg_sp x_35 =
325  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_35 in
326  h_mk_reg_sp reg_sp_env0 stackp0
327
328(** val reg_sp_rect_Type1 :
329    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
330    'a1) -> reg_sp -> 'a1 **)
331let rec reg_sp_rect_Type1 h_mk_reg_sp x_37 =
332  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_37 in
333  h_mk_reg_sp reg_sp_env0 stackp0
334
335(** val reg_sp_rect_Type0 :
336    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
337    'a1) -> reg_sp -> 'a1 **)
338let rec reg_sp_rect_Type0 h_mk_reg_sp x_39 =
339  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_39 in
340  h_mk_reg_sp reg_sp_env0 stackp0
341
342(** val reg_sp_env :
343    reg_sp -> ByteValues.beval Identifiers.identifier_map **)
344let rec reg_sp_env xxx =
345  xxx.reg_sp_env
346
347(** val stackp : reg_sp -> ByteValues.xpointer **)
348let rec stackp xxx =
349  xxx.stackp
350
351(** val reg_sp_inv_rect_Type4 :
352    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
353    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
354let reg_sp_inv_rect_Type4 hterm h1 =
355  let hcut = reg_sp_rect_Type4 h1 hterm in hcut __
356
357(** val reg_sp_inv_rect_Type3 :
358    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
359    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
360let reg_sp_inv_rect_Type3 hterm h1 =
361  let hcut = reg_sp_rect_Type3 h1 hterm in hcut __
362
363(** val reg_sp_inv_rect_Type2 :
364    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
365    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
366let reg_sp_inv_rect_Type2 hterm h1 =
367  let hcut = reg_sp_rect_Type2 h1 hterm in hcut __
368
369(** val reg_sp_inv_rect_Type1 :
370    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
371    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
372let reg_sp_inv_rect_Type1 hterm h1 =
373  let hcut = reg_sp_rect_Type1 h1 hterm in hcut __
374
375(** val reg_sp_inv_rect_Type0 :
376    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
377    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
378let reg_sp_inv_rect_Type0 hterm h1 =
379  let hcut = reg_sp_rect_Type0 h1 hterm in hcut __
380
381(** val reg_sp_discr : reg_sp -> reg_sp -> __ **)
382let reg_sp_discr x y =
383  Logic.eq_rect_Type2 x
384    (let { reg_sp_env = a0; stackp = a1 } = x in
385    Obj.magic (fun _ dH -> dH __ __)) y
386
387(** val reg_sp_jmdiscr : reg_sp -> reg_sp -> __ **)
388let reg_sp_jmdiscr x y =
389  Logic.eq_rect_Type2 x
390    (let { reg_sp_env = a0; stackp = a1 } = x in
391    Obj.magic (fun _ dH -> dH __ __)) y
392
393(** val dpi1__o__reg_sp_env__o__inject :
394    (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
395    Types.sig0 **)
396let dpi1__o__reg_sp_env__o__inject x2 =
397  x2.Types.dpi1.reg_sp_env
398
399(** val eject__o__reg_sp_env__o__inject :
400    reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map
401    Types.sig0 **)
402let eject__o__reg_sp_env__o__inject x2 =
403  (Types.pi1 x2).reg_sp_env
404
405(** val reg_sp_env__o__inject :
406    reg_sp -> ByteValues.beval Identifiers.identifier_map Types.sig0 **)
407let reg_sp_env__o__inject x1 =
408  x1.reg_sp_env
409
410(** val dpi1__o__reg_sp_env :
411    (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map **)
412let dpi1__o__reg_sp_env x1 =
413  x1.Types.dpi1.reg_sp_env
414
415(** val eject__o__reg_sp_env :
416    reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map **)
417let eject__o__reg_sp_env x1 =
418  (Types.pi1 x1).reg_sp_env
419
420(** val reg_store :
421    PreIdentifiers.identifier -> ByteValues.beval -> ByteValues.beval
422    Identifiers.identifier_map -> ByteValues.beval Identifiers.identifier_map **)
423let reg_store reg v locals =
424  Identifiers.add PreIdentifiers.RegisterTag locals reg v
425
426(** val reg_retrieve :
427    ByteValues.beval Registers.register_env -> Registers.register ->
428    ByteValues.beval Errors.res **)
429let reg_retrieve locals reg =
430  Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadRegister),
431    (List.Cons ((Errors.CTX (PreIdentifiers.RegisterTag, reg)), List.Nil))))
432    (Identifiers.lookup PreIdentifiers.RegisterTag locals reg)
433
434(** val reg_sp_store :
435    PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp **)
436let reg_sp_store reg v locals =
437  let locals' = reg_store reg v locals.reg_sp_env in
438  { reg_sp_env = locals'; stackp = locals.stackp }
439
440(** val reg_sp_retrieve :
441    reg_sp -> Registers.register -> ByteValues.beval Errors.res **)
442let reg_sp_retrieve locals =
443  reg_retrieve locals.reg_sp_env
444
445(** val reg_sp_init : ByteValues.xpointer -> reg_sp **)
446let reg_sp_init x =
447  { reg_sp_env = (Identifiers.empty_map PreIdentifiers.RegisterTag); stackp =
448    x }
449
450(** val init_hw_register_env : ByteValues.xpointer -> hw_register_env **)
451let init_hw_register_env sp =
452  hwreg_store_sp empty_hw_register_env sp
453
454type sem_graph_params = { sgp_pars : Joint.uns_params;
455                          sgp_sup : (__ -> __
456                                    Joint_semantics.sem_unserialized_params) }
457
458(** val sem_graph_params_rect_Type4 :
459    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
460    -> 'a1) -> sem_graph_params -> 'a1 **)
461let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_55 =
462  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_55 in
463  h_mk_sem_graph_params sgp_pars0 sgp_sup0
464
465(** val sem_graph_params_rect_Type5 :
466    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
467    -> 'a1) -> sem_graph_params -> 'a1 **)
468let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_57 =
469  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_57 in
470  h_mk_sem_graph_params sgp_pars0 sgp_sup0
471
472(** val sem_graph_params_rect_Type3 :
473    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
474    -> 'a1) -> sem_graph_params -> 'a1 **)
475let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_59 =
476  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_59 in
477  h_mk_sem_graph_params sgp_pars0 sgp_sup0
478
479(** val sem_graph_params_rect_Type2 :
480    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
481    -> 'a1) -> sem_graph_params -> 'a1 **)
482let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_61 =
483  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_61 in
484  h_mk_sem_graph_params sgp_pars0 sgp_sup0
485
486(** val sem_graph_params_rect_Type1 :
487    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
488    -> 'a1) -> sem_graph_params -> 'a1 **)
489let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_63 =
490  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_63 in
491  h_mk_sem_graph_params sgp_pars0 sgp_sup0
492
493(** val sem_graph_params_rect_Type0 :
494    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
495    -> 'a1) -> sem_graph_params -> 'a1 **)
496let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_65 =
497  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_65 in
498  h_mk_sem_graph_params sgp_pars0 sgp_sup0
499
500(** val sgp_pars : sem_graph_params -> Joint.uns_params **)
501let rec sgp_pars xxx =
502  xxx.sgp_pars
503
504(** val sgp_sup0 :
505    sem_graph_params -> 'a1 Joint_semantics.sem_unserialized_params **)
506let rec sgp_sup0 xxx =
507  (let { sgp_pars = x; sgp_sup = yyy } = xxx in Obj.magic yyy) __
508
509(** val sem_graph_params_inv_rect_Type4 :
510    sem_graph_params -> (Joint.uns_params -> (__ -> __
511    Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
512let sem_graph_params_inv_rect_Type4 hterm h1 =
513  let hcut = sem_graph_params_rect_Type4 h1 hterm in hcut __
514
515(** val sem_graph_params_inv_rect_Type3 :
516    sem_graph_params -> (Joint.uns_params -> (__ -> __
517    Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
518let sem_graph_params_inv_rect_Type3 hterm h1 =
519  let hcut = sem_graph_params_rect_Type3 h1 hterm in hcut __
520
521(** val sem_graph_params_inv_rect_Type2 :
522    sem_graph_params -> (Joint.uns_params -> (__ -> __
523    Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
524let sem_graph_params_inv_rect_Type2 hterm h1 =
525  let hcut = sem_graph_params_rect_Type2 h1 hterm in hcut __
526
527(** val sem_graph_params_inv_rect_Type1 :
528    sem_graph_params -> (Joint.uns_params -> (__ -> __
529    Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
530let sem_graph_params_inv_rect_Type1 hterm h1 =
531  let hcut = sem_graph_params_rect_Type1 h1 hterm in hcut __
532
533(** val sem_graph_params_inv_rect_Type0 :
534    sem_graph_params -> (Joint.uns_params -> (__ -> __
535    Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
536let sem_graph_params_inv_rect_Type0 hterm h1 =
537  let hcut = sem_graph_params_rect_Type0 h1 hterm in hcut __
538
539(** val sem_graph_params_jmdiscr :
540    sem_graph_params -> sem_graph_params -> __ **)
541let sem_graph_params_jmdiscr x y =
542  Logic.eq_rect_Type2 x
543    (let { sgp_pars = a0; sgp_sup = a1 } = x in
544    Obj.magic (fun _ dH -> dH __ __)) y
545
546(** val sem_graph_params_to_graph_params :
547    sem_graph_params -> Joint.graph_params **)
548let sem_graph_params_to_graph_params pars =
549  pars.sgp_pars
550
551(** val sem_graph_params_to_sem_params :
552    sem_graph_params -> Joint_semantics.sem_params **)
553let sem_graph_params_to_sem_params pars =
554  { Joint_semantics.spp =
555    (let x = sem_graph_params_to_graph_params pars in
556    Joint.graph_params_to_params x); Joint_semantics.msu_pars =
557    (sgp_sup0 pars); Joint_semantics.offset_of_point =
558    (Obj.magic (Identifiers.word_of_identifier PreIdentifiers.LabelTag));
559    Joint_semantics.point_of_offset = (Obj.magic (fun x -> x)) }
560
561(** val sem_params_from_sem_graph_params__o__msu_pars :
562    sem_graph_params -> Joint.joint_closed_internal_function
563    Joint_semantics.sem_unserialized_params **)
564let sem_params_from_sem_graph_params__o__msu_pars x0 =
565  (sem_graph_params_to_sem_params x0).Joint_semantics.msu_pars
566
567(** val sem_params_from_sem_graph_params__o__msu_pars__o__st_pars :
568    sem_graph_params -> Joint_semantics.sem_state_params **)
569let sem_params_from_sem_graph_params__o__msu_pars__o__st_pars x0 =
570  Joint_semantics.msu_pars__o__st_pars (sem_graph_params_to_sem_params x0)
571
572(** val sem_params_from_sem_graph_params__o__spp :
573    sem_graph_params -> Joint.params **)
574let sem_params_from_sem_graph_params__o__spp x0 =
575  (sem_graph_params_to_sem_params x0).Joint_semantics.spp
576
577(** val sem_params_from_sem_graph_params__o__spp__o__stmt_pars :
578    sem_graph_params -> Joint.stmt_params **)
579let sem_params_from_sem_graph_params__o__spp__o__stmt_pars x0 =
580  Joint_semantics.spp__o__stmt_pars (sem_graph_params_to_sem_params x0)
581
582(** val sem_params_from_sem_graph_params__o__spp__o__stmt_pars__o__uns_pars :
583    sem_graph_params -> Joint.uns_params **)
584let sem_params_from_sem_graph_params__o__spp__o__stmt_pars__o__uns_pars x0 =
585  Joint_semantics.spp__o__stmt_pars__o__uns_pars
586    (sem_graph_params_to_sem_params x0)
587
588(** val sem_params_from_sem_graph_params__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
589    sem_graph_params -> Joint.unserialized_params **)
590let sem_params_from_sem_graph_params__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
591  Joint_semantics.spp__o__stmt_pars__o__uns_pars__o__u_pars
592    (sem_graph_params_to_sem_params x0)
593
594type sem_lin_params = { slp_pars : Joint.uns_params;
595                        slp_sup : (__ -> __
596                                  Joint_semantics.sem_unserialized_params) }
597
598(** val sem_lin_params_rect_Type4 :
599    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
600    -> 'a1) -> sem_lin_params -> 'a1 **)
601let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_82 =
602  let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_82 in
603  h_mk_sem_lin_params slp_pars0 slp_sup0
604
605(** val sem_lin_params_rect_Type5 :
606    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
607    -> 'a1) -> sem_lin_params -> 'a1 **)
608let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_84 =
609  let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_84 in
610  h_mk_sem_lin_params slp_pars0 slp_sup0
611
612(** val sem_lin_params_rect_Type3 :
613    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
614    -> 'a1) -> sem_lin_params -> 'a1 **)
615let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_86 =
616  let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_86 in
617  h_mk_sem_lin_params slp_pars0 slp_sup0
618
619(** val sem_lin_params_rect_Type2 :
620    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
621    -> 'a1) -> sem_lin_params -> 'a1 **)
622let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_88 =
623  let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_88 in
624  h_mk_sem_lin_params slp_pars0 slp_sup0
625
626(** val sem_lin_params_rect_Type1 :
627    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
628    -> 'a1) -> sem_lin_params -> 'a1 **)
629let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_90 =
630  let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_90 in
631  h_mk_sem_lin_params slp_pars0 slp_sup0
632
633(** val sem_lin_params_rect_Type0 :
634    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
635    -> 'a1) -> sem_lin_params -> 'a1 **)
636let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_92 =
637  let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_92 in
638  h_mk_sem_lin_params slp_pars0 slp_sup0
639
640(** val slp_pars : sem_lin_params -> Joint.uns_params **)
641let rec slp_pars xxx =
642  xxx.slp_pars
643
644(** val slp_sup0 :
645    sem_lin_params -> 'a1 Joint_semantics.sem_unserialized_params **)
646let rec slp_sup0 xxx =
647  (let { slp_pars = x; slp_sup = yyy } = xxx in Obj.magic yyy) __
648
649(** val sem_lin_params_inv_rect_Type4 :
650    sem_lin_params -> (Joint.uns_params -> (__ -> __
651    Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
652let sem_lin_params_inv_rect_Type4 hterm h1 =
653  let hcut = sem_lin_params_rect_Type4 h1 hterm in hcut __
654
655(** val sem_lin_params_inv_rect_Type3 :
656    sem_lin_params -> (Joint.uns_params -> (__ -> __
657    Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
658let sem_lin_params_inv_rect_Type3 hterm h1 =
659  let hcut = sem_lin_params_rect_Type3 h1 hterm in hcut __
660
661(** val sem_lin_params_inv_rect_Type2 :
662    sem_lin_params -> (Joint.uns_params -> (__ -> __
663    Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
664let sem_lin_params_inv_rect_Type2 hterm h1 =
665  let hcut = sem_lin_params_rect_Type2 h1 hterm in hcut __
666
667(** val sem_lin_params_inv_rect_Type1 :
668    sem_lin_params -> (Joint.uns_params -> (__ -> __
669    Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
670let sem_lin_params_inv_rect_Type1 hterm h1 =
671  let hcut = sem_lin_params_rect_Type1 h1 hterm in hcut __
672
673(** val sem_lin_params_inv_rect_Type0 :
674    sem_lin_params -> (Joint.uns_params -> (__ -> __
675    Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
676let sem_lin_params_inv_rect_Type0 hterm h1 =
677  let hcut = sem_lin_params_rect_Type0 h1 hterm in hcut __
678
679(** val sem_lin_params_jmdiscr : sem_lin_params -> sem_lin_params -> __ **)
680let sem_lin_params_jmdiscr x y =
681  Logic.eq_rect_Type2 x
682    (let { slp_pars = a0; slp_sup = a1 } = x in
683    Obj.magic (fun _ dH -> dH __ __)) y
684
685(** val sem_lin_params_to_lin_params : sem_lin_params -> Joint.lin_params **)
686let sem_lin_params_to_lin_params pars =
687  pars.slp_pars
688
689(** val sem_lin_params_to_sem_params :
690    sem_lin_params -> Joint_semantics.sem_params **)
691let sem_lin_params_to_sem_params pars =
692  { Joint_semantics.spp =
693    (let x = sem_lin_params_to_lin_params pars in
694    Joint.lin_params_to_params x); Joint_semantics.msu_pars =
695    (slp_sup0 pars); Joint_semantics.offset_of_point =
696    (Obj.magic Positive.succ_pos_of_nat); Joint_semantics.point_of_offset =
697    (fun p -> Obj.magic (Nat.pred (Positive.nat_of_pos p))) }
698
699(** val sem_params_from_sem_lin_params__o__msu_pars :
700    sem_lin_params -> Joint.joint_closed_internal_function
701    Joint_semantics.sem_unserialized_params **)
702let sem_params_from_sem_lin_params__o__msu_pars x0 =
703  (sem_lin_params_to_sem_params x0).Joint_semantics.msu_pars
704
705(** val sem_params_from_sem_lin_params__o__msu_pars__o__st_pars :
706    sem_lin_params -> Joint_semantics.sem_state_params **)
707let sem_params_from_sem_lin_params__o__msu_pars__o__st_pars x0 =
708  Joint_semantics.msu_pars__o__st_pars (sem_lin_params_to_sem_params x0)
709
710(** val sem_params_from_sem_lin_params__o__spp :
711    sem_lin_params -> Joint.params **)
712let sem_params_from_sem_lin_params__o__spp x0 =
713  (sem_lin_params_to_sem_params x0).Joint_semantics.spp
714
715(** val sem_params_from_sem_lin_params__o__spp__o__stmt_pars :
716    sem_lin_params -> Joint.stmt_params **)
717let sem_params_from_sem_lin_params__o__spp__o__stmt_pars x0 =
718  Joint_semantics.spp__o__stmt_pars (sem_lin_params_to_sem_params x0)
719
720(** val sem_params_from_sem_lin_params__o__spp__o__stmt_pars__o__uns_pars :
721    sem_lin_params -> Joint.uns_params **)
722let sem_params_from_sem_lin_params__o__spp__o__stmt_pars__o__uns_pars x0 =
723  Joint_semantics.spp__o__stmt_pars__o__uns_pars
724    (sem_lin_params_to_sem_params x0)
725
726(** val sem_params_from_sem_lin_params__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
727    sem_lin_params -> Joint.unserialized_params **)
728let sem_params_from_sem_lin_params__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
729  Joint_semantics.spp__o__stmt_pars__o__uns_pars__o__u_pars
730    (sem_lin_params_to_sem_params x0)
731
732(** val match_genv_t_rect_Type4 :
733    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
734    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
735let rec match_genv_t_rect_Type4 m vars ge1 ge2 h_mk_match_genv_t =
736  h_mk_match_genv_t __ __ __
737
738(** val match_genv_t_rect_Type5 :
739    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
740    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
741let rec match_genv_t_rect_Type5 m vars ge1 ge2 h_mk_match_genv_t =
742  h_mk_match_genv_t __ __ __
743
744(** val match_genv_t_rect_Type3 :
745    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
746    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
747let rec match_genv_t_rect_Type3 m vars ge1 ge2 h_mk_match_genv_t =
748  h_mk_match_genv_t __ __ __
749
750(** val match_genv_t_rect_Type2 :
751    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
752    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
753let rec match_genv_t_rect_Type2 m vars ge1 ge2 h_mk_match_genv_t =
754  h_mk_match_genv_t __ __ __
755
756(** val match_genv_t_rect_Type1 :
757    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
758    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
759let rec match_genv_t_rect_Type1 m vars ge1 ge2 h_mk_match_genv_t =
760  h_mk_match_genv_t __ __ __
761
762(** val match_genv_t_rect_Type0 :
763    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
764    Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
765let rec match_genv_t_rect_Type0 m vars ge1 ge2 h_mk_match_genv_t =
766  h_mk_match_genv_t __ __ __
767
768(** val match_genv_t_inv_rect_Type4 :
769    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
770    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
771let match_genv_t_inv_rect_Type4 x1 x2 x3 x4 h1 =
772  let hcut = match_genv_t_rect_Type4 x1 x2 x3 x4 h1 in hcut __
773
774(** val match_genv_t_inv_rect_Type3 :
775    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
776    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
777let match_genv_t_inv_rect_Type3 x1 x2 x3 x4 h1 =
778  let hcut = match_genv_t_rect_Type3 x1 x2 x3 x4 h1 in hcut __
779
780(** val match_genv_t_inv_rect_Type2 :
781    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
782    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
783let match_genv_t_inv_rect_Type2 x1 x2 x3 x4 h1 =
784  let hcut = match_genv_t_rect_Type2 x1 x2 x3 x4 h1 in hcut __
785
786(** val match_genv_t_inv_rect_Type1 :
787    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
788    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
789let match_genv_t_inv_rect_Type1 x1 x2 x3 x4 h1 =
790  let hcut = match_genv_t_rect_Type1 x1 x2 x3 x4 h1 in hcut __
791
792(** val match_genv_t_inv_rect_Type0 :
793    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
794    Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
795let match_genv_t_inv_rect_Type0 x1 x2 x3 x4 h1 =
796  let hcut = match_genv_t_rect_Type0 x1 x2 x3 x4 h1 in hcut __
797
798(** val match_genv_t_discr :
799    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
800    Globalenvs.genv_t -> __ **)
801let match_genv_t_discr a1 a2 a3 a4 =
802  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
803
804(** val match_genv_t_jmdiscr :
805    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
806    Globalenvs.genv_t -> __ **)
807let match_genv_t_jmdiscr a1 a2 a3 a4 =
808  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
809
Note: See TracBrowser for help on using the repository browser.