Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/semanticsUtils.ml

    r2890 r2951  
    146146
    147147open 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)
    148162
    149163type hw_register_env = { reg_env : ByteValues.beval
     
    154168    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    155169    -> hw_register_env -> 'a1 **)
    156 let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_26260 =
    157   let { reg_env = reg_env0; other_bit = other_bit0 } = x_26260 in
     170let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_5847 =
     171  let { reg_env = reg_env0; other_bit = other_bit0 } = x_5847 in
    158172  h_mk_hw_register_env reg_env0 other_bit0
    159173
     
    161175    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    162176    -> hw_register_env -> 'a1 **)
    163 let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_26262 =
    164   let { reg_env = reg_env0; other_bit = other_bit0 } = x_26262 in
     177let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_5849 =
     178  let { reg_env = reg_env0; other_bit = other_bit0 } = x_5849 in
    165179  h_mk_hw_register_env reg_env0 other_bit0
    166180
     
    168182    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    169183    -> hw_register_env -> 'a1 **)
    170 let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_26264 =
    171   let { reg_env = reg_env0; other_bit = other_bit0 } = x_26264 in
     184let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_5851 =
     185  let { reg_env = reg_env0; other_bit = other_bit0 } = x_5851 in
    172186  h_mk_hw_register_env reg_env0 other_bit0
    173187
     
    175189    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    176190    -> hw_register_env -> 'a1 **)
    177 let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_26266 =
    178   let { reg_env = reg_env0; other_bit = other_bit0 } = x_26266 in
     191let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_5853 =
     192  let { reg_env = reg_env0; other_bit = other_bit0 } = x_5853 in
    179193  h_mk_hw_register_env reg_env0 other_bit0
    180194
     
    182196    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    183197    -> hw_register_env -> 'a1 **)
    184 let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_26268 =
    185   let { reg_env = reg_env0; other_bit = other_bit0 } = x_26268 in
     198let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_5855 =
     199  let { reg_env = reg_env0; other_bit = other_bit0 } = x_5855 in
    186200  h_mk_hw_register_env reg_env0 other_bit0
    187201
     
    189203    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    190204    -> hw_register_env -> 'a1 **)
    191 let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_26270 =
    192   let { reg_env = reg_env0; other_bit = other_bit0 } = x_26270 in
     205let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_5857 =
     206  let { reg_env = reg_env0; other_bit = other_bit0 } = x_5857 in
    193207  h_mk_hw_register_env reg_env0 other_bit0
    194208
     
    244258    (let { reg_env = a0; other_bit = a1 } = x in
    245259    Obj.magic (fun _ dH -> dH __ __)) y
    246 
    247 (** val empty_hw_register_env : hw_register_env **)
    248 let 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 }
    251260
    252261(** val hwreg_retrieve :
     
    295304  hwreg_store I8051.registerSPH sph (hwreg_store I8051.registerSPL spl env)
    296305
    297 type 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 **)
    303 let rec reg_sp_rect_Type4 h_mk_reg_sp x_26286 =
    304   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26286 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 **)
    310 let rec reg_sp_rect_Type5 h_mk_reg_sp x_26288 =
    311   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26288 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 **)
    317 let rec reg_sp_rect_Type3 h_mk_reg_sp x_26290 =
    318   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26290 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 **)
    324 let rec reg_sp_rect_Type2 h_mk_reg_sp x_26292 =
    325   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26292 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 **)
    331 let rec reg_sp_rect_Type1 h_mk_reg_sp x_26294 =
    332   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26294 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 **)
    338 let rec reg_sp_rect_Type0 h_mk_reg_sp x_26296 =
    339   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26296 in
    340   h_mk_reg_sp reg_sp_env0 stackp0
    341 
    342 (** val reg_sp_env :
    343     reg_sp -> ByteValues.beval Identifiers.identifier_map **)
    344 let rec reg_sp_env xxx =
    345   xxx.reg_sp_env
    346 
    347 (** val stackp : reg_sp -> ByteValues.xpointer **)
    348 let 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 **)
    354 let 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 **)
    360 let 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 **)
    366 let 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 **)
    372 let 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 **)
    378 let 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 -> __ **)
    382 let 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 -> __ **)
    388 let 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 **)
    396 let 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 **)
    402 let 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 **)
    407 let 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 **)
    412 let 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 **)
    417 let 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 **)
    423 let 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 **)
    429 let 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 **)
    436 let 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 **)
    442 let reg_sp_retrieve locals =
    443   reg_retrieve locals.reg_sp_env
    444 
    445 (** val reg_sp_init : ByteValues.xpointer -> reg_sp **)
    446 let reg_sp_init x =
    447   { reg_sp_env = (Identifiers.empty_map PreIdentifiers.RegisterTag); stackp =
    448     x }
    449 
    450306(** val init_hw_register_env : ByteValues.xpointer -> hw_register_env **)
    451 let init_hw_register_env sp =
    452   hwreg_store_sp empty_hw_register_env sp
     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 }
    453310
    454311type sem_graph_params = { sgp_pars : Joint.uns_params;
    455312                          sgp_sup : (__ -> __
    456                                     Joint_semantics.sem_unserialized_params) }
     313                                    Joint_semantics.sem_unserialized_params);
     314                          graph_pre_main_generator : (Joint.joint_program ->
     315                                                     Joint.joint_closed_internal_function) }
    457316
    458317(** val sem_graph_params_rect_Type4 :
    459318    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    460     -> 'a1) -> sem_graph_params -> 'a1 **)
    461 let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_26312 =
    462   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26312 in
    463   h_mk_sem_graph_params sgp_pars0 sgp_sup0
     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_5873 =
     322  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
     323    graph_pre_main_generator0 } = x_5873
     324  in
     325  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
    464326
    465327(** val sem_graph_params_rect_Type5 :
    466328    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    467     -> 'a1) -> sem_graph_params -> 'a1 **)
    468 let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_26314 =
    469   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26314 in
    470   h_mk_sem_graph_params sgp_pars0 sgp_sup0
     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_5875 =
     332  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
     333    graph_pre_main_generator0 } = x_5875
     334  in
     335  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
    471336
    472337(** val sem_graph_params_rect_Type3 :
    473338    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    474     -> 'a1) -> sem_graph_params -> 'a1 **)
    475 let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_26316 =
    476   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26316 in
    477   h_mk_sem_graph_params sgp_pars0 sgp_sup0
     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_5877 =
     342  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
     343    graph_pre_main_generator0 } = x_5877
     344  in
     345  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
    478346
    479347(** val sem_graph_params_rect_Type2 :
    480348    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    481     -> 'a1) -> sem_graph_params -> 'a1 **)
    482 let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_26318 =
    483   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26318 in
    484   h_mk_sem_graph_params sgp_pars0 sgp_sup0
     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_5879 =
     352  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
     353    graph_pre_main_generator0 } = x_5879
     354  in
     355  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
    485356
    486357(** val sem_graph_params_rect_Type1 :
    487358    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    488     -> 'a1) -> sem_graph_params -> 'a1 **)
    489 let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_26320 =
    490   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26320 in
    491   h_mk_sem_graph_params sgp_pars0 sgp_sup0
     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_5881 =
     362  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
     363    graph_pre_main_generator0 } = x_5881
     364  in
     365  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
    492366
    493367(** val sem_graph_params_rect_Type0 :
    494368    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    495     -> 'a1) -> sem_graph_params -> 'a1 **)
    496 let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_26322 =
    497   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26322 in
    498   h_mk_sem_graph_params sgp_pars0 sgp_sup0
     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_5883 =
     372  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
     373    graph_pre_main_generator0 } = x_5883
     374  in
     375  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
    499376
    500377(** val sgp_pars : sem_graph_params -> Joint.uns_params **)
     
    505382    sem_graph_params -> 'a1 Joint_semantics.sem_unserialized_params **)
    506383let rec sgp_sup0 xxx =
    507   (let { sgp_pars = x; sgp_sup = yyy } = xxx in Obj.magic yyy) __
     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
    508393
    509394(** val sem_graph_params_inv_rect_Type4 :
    510395    sem_graph_params -> (Joint.uns_params -> (__ -> __
    511     Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
     396    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     397    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
    512398let sem_graph_params_inv_rect_Type4 hterm h1 =
    513399  let hcut = sem_graph_params_rect_Type4 h1 hterm in hcut __
     
    515401(** val sem_graph_params_inv_rect_Type3 :
    516402    sem_graph_params -> (Joint.uns_params -> (__ -> __
    517     Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
     403    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     404    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
    518405let sem_graph_params_inv_rect_Type3 hterm h1 =
    519406  let hcut = sem_graph_params_rect_Type3 h1 hterm in hcut __
     
    521408(** val sem_graph_params_inv_rect_Type2 :
    522409    sem_graph_params -> (Joint.uns_params -> (__ -> __
    523     Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
     410    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     411    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
    524412let sem_graph_params_inv_rect_Type2 hterm h1 =
    525413  let hcut = sem_graph_params_rect_Type2 h1 hterm in hcut __
     
    527415(** val sem_graph_params_inv_rect_Type1 :
    528416    sem_graph_params -> (Joint.uns_params -> (__ -> __
    529     Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
     417    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     418    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
    530419let sem_graph_params_inv_rect_Type1 hterm h1 =
    531420  let hcut = sem_graph_params_rect_Type1 h1 hterm in hcut __
     
    533422(** val sem_graph_params_inv_rect_Type0 :
    534423    sem_graph_params -> (Joint.uns_params -> (__ -> __
    535     Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
     424    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     425    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
    536426let sem_graph_params_inv_rect_Type0 hterm h1 =
    537427  let hcut = sem_graph_params_rect_Type0 h1 hterm in hcut __
     
    541431let sem_graph_params_jmdiscr x y =
    542432  Logic.eq_rect_Type2 x
    543     (let { sgp_pars = a0; sgp_sup = a1 } = x in
    544     Obj.magic (fun _ dH -> dH __ __)) y
     433    (let { sgp_pars = a0; sgp_sup = a1; graph_pre_main_generator = a2 } = x
     434     in
     435    Obj.magic (fun _ dH -> dH __ __ __)) y
    545436
    546437(** val sem_graph_params_to_graph_params :
     
    552443    sem_graph_params -> Joint_semantics.sem_params **)
    553444let sem_graph_params_to_sem_params pars =
    554   { Joint_semantics.spp =
     445  { Joint_semantics.spp' = { Joint_semantics.spp =
    555446    (let x = sem_graph_params_to_graph_params pars in
    556447    Joint.graph_params_to_params x); Joint_semantics.msu_pars =
    557448    (sgp_sup0 pars); Joint_semantics.offset_of_point =
    558449    (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 :
     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 :
    562459    sem_graph_params -> Joint.joint_closed_internal_function
    563460    Joint_semantics.sem_unserialized_params **)
    564 let 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 :
     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 :
    568465    sem_graph_params -> Joint_semantics.sem_state_params **)
    569 let 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 :
     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 :
    573471    sem_graph_params -> Joint.params **)
    574 let 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 :
     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 :
    578476    sem_graph_params -> Joint.stmt_params **)
    579 let 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 :
     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 :
    583482    sem_graph_params -> Joint.uns_params **)
    584 let 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
     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
    586485    (sem_graph_params_to_sem_params x0)
    587486
    588 (** val sem_params_from_sem_graph_params__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
     487(** val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    589488    sem_graph_params -> Joint.unserialized_params **)
    590 let 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
     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
    592491    (sem_graph_params_to_sem_params x0)
    593492
    594493type sem_lin_params = { slp_pars : Joint.uns_params;
    595494                        slp_sup : (__ -> __
    596                                   Joint_semantics.sem_unserialized_params) }
     495                                  Joint_semantics.sem_unserialized_params);
     496                        lin_pre_main_generator : (Joint.joint_program ->
     497                                                 Joint.joint_closed_internal_function) }
    597498
    598499(** val sem_lin_params_rect_Type4 :
    599500    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    600     -> 'a1) -> sem_lin_params -> 'a1 **)
    601 let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_26339 =
    602   let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26339 in
    603   h_mk_sem_lin_params slp_pars0 slp_sup0
     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_5900 =
     504  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
     505    lin_pre_main_generator0 } = x_5900
     506  in
     507  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
    604508
    605509(** val sem_lin_params_rect_Type5 :
    606510    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    607     -> 'a1) -> sem_lin_params -> 'a1 **)
    608 let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_26341 =
    609   let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26341 in
    610   h_mk_sem_lin_params slp_pars0 slp_sup0
     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_5902 =
     514  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
     515    lin_pre_main_generator0 } = x_5902
     516  in
     517  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
    611518
    612519(** val sem_lin_params_rect_Type3 :
    613520    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    614     -> 'a1) -> sem_lin_params -> 'a1 **)
    615 let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_26343 =
    616   let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26343 in
    617   h_mk_sem_lin_params slp_pars0 slp_sup0
     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_5904 =
     524  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
     525    lin_pre_main_generator0 } = x_5904
     526  in
     527  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
    618528
    619529(** val sem_lin_params_rect_Type2 :
    620530    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    621     -> 'a1) -> sem_lin_params -> 'a1 **)
    622 let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_26345 =
    623   let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26345 in
    624   h_mk_sem_lin_params slp_pars0 slp_sup0
     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_5906 =
     534  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
     535    lin_pre_main_generator0 } = x_5906
     536  in
     537  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
    625538
    626539(** val sem_lin_params_rect_Type1 :
    627540    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    628     -> 'a1) -> sem_lin_params -> 'a1 **)
    629 let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_26347 =
    630   let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26347 in
    631   h_mk_sem_lin_params slp_pars0 slp_sup0
     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_5908 =
     544  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
     545    lin_pre_main_generator0 } = x_5908
     546  in
     547  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
    632548
    633549(** val sem_lin_params_rect_Type0 :
    634550    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    635     -> 'a1) -> sem_lin_params -> 'a1 **)
    636 let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_26349 =
    637   let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26349 in
    638   h_mk_sem_lin_params slp_pars0 slp_sup0
     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_5910 =
     554  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
     555    lin_pre_main_generator0 } = x_5910
     556  in
     557  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
    639558
    640559(** val slp_pars : sem_lin_params -> Joint.uns_params **)
     
    645564    sem_lin_params -> 'a1 Joint_semantics.sem_unserialized_params **)
    646565let rec slp_sup0 xxx =
    647   (let { slp_pars = x; slp_sup = yyy } = xxx in Obj.magic yyy) __
     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
    648574
    649575(** val sem_lin_params_inv_rect_Type4 :
    650576    sem_lin_params -> (Joint.uns_params -> (__ -> __
    651     Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
     577    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     578    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
    652579let sem_lin_params_inv_rect_Type4 hterm h1 =
    653580  let hcut = sem_lin_params_rect_Type4 h1 hterm in hcut __
     
    655582(** val sem_lin_params_inv_rect_Type3 :
    656583    sem_lin_params -> (Joint.uns_params -> (__ -> __
    657     Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
     584    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     585    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
    658586let sem_lin_params_inv_rect_Type3 hterm h1 =
    659587  let hcut = sem_lin_params_rect_Type3 h1 hterm in hcut __
     
    661589(** val sem_lin_params_inv_rect_Type2 :
    662590    sem_lin_params -> (Joint.uns_params -> (__ -> __
    663     Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
     591    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     592    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
    664593let sem_lin_params_inv_rect_Type2 hterm h1 =
    665594  let hcut = sem_lin_params_rect_Type2 h1 hterm in hcut __
     
    667596(** val sem_lin_params_inv_rect_Type1 :
    668597    sem_lin_params -> (Joint.uns_params -> (__ -> __
    669     Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
     598    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     599    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
    670600let sem_lin_params_inv_rect_Type1 hterm h1 =
    671601  let hcut = sem_lin_params_rect_Type1 h1 hterm in hcut __
     
    673603(** val sem_lin_params_inv_rect_Type0 :
    674604    sem_lin_params -> (Joint.uns_params -> (__ -> __
    675     Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1 **)
     605    Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     606    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
    676607let sem_lin_params_inv_rect_Type0 hterm h1 =
    677608  let hcut = sem_lin_params_rect_Type0 h1 hterm in hcut __
     
    680611let sem_lin_params_jmdiscr x y =
    681612  Logic.eq_rect_Type2 x
    682     (let { slp_pars = a0; slp_sup = a1 } = x in
    683     Obj.magic (fun _ dH -> dH __ __)) y
     613    (let { slp_pars = a0; slp_sup = a1; lin_pre_main_generator = a2 } = x in
     614    Obj.magic (fun _ dH -> dH __ __ __)) y
    684615
    685616(** val sem_lin_params_to_lin_params : sem_lin_params -> Joint.lin_params **)
     
    690621    sem_lin_params -> Joint_semantics.sem_params **)
    691622let sem_lin_params_to_sem_params pars =
    692   { Joint_semantics.spp =
     623  { Joint_semantics.spp' = { Joint_semantics.spp =
    693624    (let x = sem_lin_params_to_lin_params pars in
    694625    Joint.lin_params_to_params x); Joint_semantics.msu_pars =
    695626    (slp_sup0 pars); Joint_semantics.offset_of_point =
    696627    (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 :
     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 :
    700637    sem_lin_params -> Joint.joint_closed_internal_function
    701638    Joint_semantics.sem_unserialized_params **)
    702 let 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 :
     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 :
    706643    sem_lin_params -> Joint_semantics.sem_state_params **)
    707 let 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 :
     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 :
    711649    sem_lin_params -> Joint.params **)
    712 let 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 :
     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 :
    716654    sem_lin_params -> Joint.stmt_params **)
    717 let 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 :
     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 :
    721660    sem_lin_params -> Joint.uns_params **)
    722 let 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
     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
    724663    (sem_lin_params_to_sem_params x0)
    725664
    726 (** val sem_params_from_sem_lin_params__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
     665(** val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    727666    sem_lin_params -> Joint.unserialized_params **)
    728 let 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
     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
    730669    (sem_lin_params_to_sem_params x0)
     670
     671(** val pre_main_id : AST.ident **)
     672let pre_main_id =
     673  Positive.One
     674
     675(** val joint_globalenv :
     676    Joint_semantics.sem_params -> Joint.joint_program ->
     677    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
     678let joint_globalenv pars prog =
     679  let genv =
     680    Globalenvs.drop_fn pre_main_id
     681      (Globalenvs.globalenv (fun x -> x) prog.Joint.joint_prog)
     682  in
     683  { Globalenvs.functions =
     684  (PositiveMap.insert Positive.One (AST.Internal
     685    (pars.Joint_semantics.pre_main_generator prog))
     686    genv.Globalenvs.functions); Globalenvs.nextfunction =
     687  genv.Globalenvs.nextfunction; Globalenvs.symbols =
     688  (Identifiers.add PreIdentifiers.SymbolTag genv.Globalenvs.symbols
     689    pre_main_id (Z.zopp (Z.z_of_nat (Nat.S Nat.O)))) }
    731690
    732691(** val match_genv_t_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.