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/joint_semantics.ml

    r2933 r2951  
    141141    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    142142    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    143 let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_25736 =
     143let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_5376 =
    144144  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    145     get_pc_from_label0 } = x_25736
     145    get_pc_from_label0 } = x_5376
    146146  in
    147147  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     
    151151    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    152152    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    153 let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_25738 =
     153let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_5378 =
    154154  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    155     get_pc_from_label0 } = x_25738
     155    get_pc_from_label0 } = x_5378
    156156  in
    157157  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     
    161161    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    162162    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    163 let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_25740 =
     163let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_5380 =
    164164  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    165     get_pc_from_label0 } = x_25740
     165    get_pc_from_label0 } = x_5380
    166166  in
    167167  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     
    171171    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    172172    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    173 let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_25742 =
     173let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_5382 =
    174174  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    175     get_pc_from_label0 } = x_25742
     175    get_pc_from_label0 } = x_5382
    176176  in
    177177  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     
    181181    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    182182    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    183 let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_25744 =
     183let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_5384 =
    184184  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    185     get_pc_from_label0 } = x_25744
     185    get_pc_from_label0 } = x_5384
    186186  in
    187187  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     
    191191    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    192192    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    193 let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_25746 =
     193let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_5386 =
    194194  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    195     get_pc_from_label0 } = x_25746
     195    get_pc_from_label0 } = x_5386
    196196  in
    197197  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     
    341341    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    342342    'a1) -> sem_state_params -> 'a1 **)
    343 let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_25766 =
     343let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_5406 =
    344344  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    345     load_sp0; save_sp = save_sp0 } = x_25766
     345    load_sp0; save_sp = save_sp0 } = x_5406
    346346  in
    347347  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    351351    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    352352    'a1) -> sem_state_params -> 'a1 **)
    353 let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_25768 =
     353let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_5408 =
    354354  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    355     load_sp0; save_sp = save_sp0 } = x_25768
     355    load_sp0; save_sp = save_sp0 } = x_5408
    356356  in
    357357  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    361361    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    362362    'a1) -> sem_state_params -> 'a1 **)
    363 let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_25770 =
     363let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_5410 =
    364364  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    365     load_sp0; save_sp = save_sp0 } = x_25770
     365    load_sp0; save_sp = save_sp0 } = x_5410
    366366  in
    367367  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    371371    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    372372    'a1) -> sem_state_params -> 'a1 **)
    373 let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_25772 =
     373let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_5412 =
    374374  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    375     load_sp0; save_sp = save_sp0 } = x_25772
     375    load_sp0; save_sp = save_sp0 } = x_5412
    376376  in
    377377  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    381381    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    382382    'a1) -> sem_state_params -> 'a1 **)
    383 let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_25774 =
     383let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_5414 =
    384384  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    385     load_sp0; save_sp = save_sp0 } = x_25774
     385    load_sp0; save_sp = save_sp0 } = x_5414
    386386  in
    387387  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    391391    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    392392    'a1) -> sem_state_params -> 'a1 **)
    393 let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_25776 =
     393let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_5416 =
    394394  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    395     load_sp0; save_sp = save_sp0 } = x_25776
     395    load_sp0; save_sp = save_sp0 } = x_5416
    396396  in
    397397  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    472472let rec internal_stack_rect_Type4 h_empty_is h_one_is h_both_is = function
    473473| Empty_is -> h_empty_is
    474 | One_is x_25802 -> h_one_is x_25802
    475 | Both_is (x_25804, x_25803) -> h_both_is x_25804 x_25803
     474| One_is x_5442 -> h_one_is x_5442
     475| Both_is (x_5444, x_5443) -> h_both_is x_5444 x_5443
    476476
    477477(** val internal_stack_rect_Type5 :
     
    480480let rec internal_stack_rect_Type5 h_empty_is h_one_is h_both_is = function
    481481| Empty_is -> h_empty_is
    482 | One_is x_25809 -> h_one_is x_25809
    483 | Both_is (x_25811, x_25810) -> h_both_is x_25811 x_25810
     482| One_is x_5449 -> h_one_is x_5449
     483| Both_is (x_5451, x_5450) -> h_both_is x_5451 x_5450
    484484
    485485(** val internal_stack_rect_Type3 :
     
    488488let rec internal_stack_rect_Type3 h_empty_is h_one_is h_both_is = function
    489489| Empty_is -> h_empty_is
    490 | One_is x_25816 -> h_one_is x_25816
    491 | Both_is (x_25818, x_25817) -> h_both_is x_25818 x_25817
     490| One_is x_5456 -> h_one_is x_5456
     491| Both_is (x_5458, x_5457) -> h_both_is x_5458 x_5457
    492492
    493493(** val internal_stack_rect_Type2 :
     
    496496let rec internal_stack_rect_Type2 h_empty_is h_one_is h_both_is = function
    497497| Empty_is -> h_empty_is
    498 | One_is x_25823 -> h_one_is x_25823
    499 | Both_is (x_25825, x_25824) -> h_both_is x_25825 x_25824
     498| One_is x_5463 -> h_one_is x_5463
     499| Both_is (x_5465, x_5464) -> h_both_is x_5465 x_5464
    500500
    501501(** val internal_stack_rect_Type1 :
     
    504504let rec internal_stack_rect_Type1 h_empty_is h_one_is h_both_is = function
    505505| Empty_is -> h_empty_is
    506 | One_is x_25830 -> h_one_is x_25830
    507 | Both_is (x_25832, x_25831) -> h_both_is x_25832 x_25831
     506| One_is x_5470 -> h_one_is x_5470
     507| Both_is (x_5472, x_5471) -> h_both_is x_5472 x_5471
    508508
    509509(** val internal_stack_rect_Type0 :
     
    512512let rec internal_stack_rect_Type0 h_empty_is h_one_is h_both_is = function
    513513| Empty_is -> h_empty_is
    514 | One_is x_25837 -> h_one_is x_25837
    515 | Both_is (x_25839, x_25838) -> h_both_is x_25839 x_25838
     514| One_is x_5477 -> h_one_is x_5477
     515| Both_is (x_5479, x_5478) -> h_both_is x_5479 x_5478
    516516
    517517(** val internal_stack_inv_rect_Type4 :
     
    591591
    592592type state = { st_frms : __ Types.option; istack : internal_stack;
    593                carry : ByteValues.bebit; regs : __; m : BEMem.bemem }
     593               carry : ByteValues.bebit; regs : __; m : BEMem.bemem;
     594               stack_usage : Nat.nat }
    594595
    595596(** val state_rect_Type4 :
    596597    sem_state_params -> (__ Types.option -> internal_stack ->
    597     ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    598 let rec state_rect_Type4 semp h_mk_state x_25887 =
     598    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
     599let rec state_rect_Type4 semp h_mk_state x_5527 =
    599600  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    600     m = m0 } = x_25887
    601   in
    602   h_mk_state st_frms0 istack0 carry0 regs0 m0
     601    m = m0; stack_usage = stack_usage0 } = x_5527
     602  in
     603  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
    603604
    604605(** val state_rect_Type5 :
    605606    sem_state_params -> (__ Types.option -> internal_stack ->
    606     ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    607 let rec state_rect_Type5 semp h_mk_state x_25889 =
     607    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
     608let rec state_rect_Type5 semp h_mk_state x_5529 =
    608609  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    609     m = m0 } = x_25889
    610   in
    611   h_mk_state st_frms0 istack0 carry0 regs0 m0
     610    m = m0; stack_usage = stack_usage0 } = x_5529
     611  in
     612  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
    612613
    613614(** val state_rect_Type3 :
    614615    sem_state_params -> (__ Types.option -> internal_stack ->
    615     ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    616 let rec state_rect_Type3 semp h_mk_state x_25891 =
     616    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
     617let rec state_rect_Type3 semp h_mk_state x_5531 =
    617618  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    618     m = m0 } = x_25891
    619   in
    620   h_mk_state st_frms0 istack0 carry0 regs0 m0
     619    m = m0; stack_usage = stack_usage0 } = x_5531
     620  in
     621  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
    621622
    622623(** val state_rect_Type2 :
    623624    sem_state_params -> (__ Types.option -> internal_stack ->
    624     ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    625 let rec state_rect_Type2 semp h_mk_state x_25893 =
     625    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
     626let rec state_rect_Type2 semp h_mk_state x_5533 =
    626627  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    627     m = m0 } = x_25893
    628   in
    629   h_mk_state st_frms0 istack0 carry0 regs0 m0
     628    m = m0; stack_usage = stack_usage0 } = x_5533
     629  in
     630  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
    630631
    631632(** val state_rect_Type1 :
    632633    sem_state_params -> (__ Types.option -> internal_stack ->
    633     ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    634 let rec state_rect_Type1 semp h_mk_state x_25895 =
     634    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
     635let rec state_rect_Type1 semp h_mk_state x_5535 =
    635636  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    636     m = m0 } = x_25895
    637   in
    638   h_mk_state st_frms0 istack0 carry0 regs0 m0
     637    m = m0; stack_usage = stack_usage0 } = x_5535
     638  in
     639  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
    639640
    640641(** val state_rect_Type0 :
    641642    sem_state_params -> (__ Types.option -> internal_stack ->
    642     ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    643 let rec state_rect_Type0 semp h_mk_state x_25897 =
     643    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
     644let rec state_rect_Type0 semp h_mk_state x_5537 =
    644645  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    645     m = m0 } = x_25897
    646   in
    647   h_mk_state st_frms0 istack0 carry0 regs0 m0
     646    m = m0; stack_usage = stack_usage0 } = x_5537
     647  in
     648  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
    648649
    649650(** val st_frms : sem_state_params -> state -> __ Types.option **)
     
    667668  xxx.m
    668669
     670(** val stack_usage : sem_state_params -> state -> Nat.nat **)
     671let rec stack_usage semp xxx =
     672  xxx.stack_usage
     673
    669674(** val state_inv_rect_Type4 :
    670675    sem_state_params -> state -> (__ Types.option -> internal_stack ->
    671     ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1 **)
     676    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
    672677let state_inv_rect_Type4 x1 hterm h1 =
    673678  let hcut = state_rect_Type4 x1 h1 hterm in hcut __
     
    675680(** val state_inv_rect_Type3 :
    676681    sem_state_params -> state -> (__ Types.option -> internal_stack ->
    677     ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1 **)
     682    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
    678683let state_inv_rect_Type3 x1 hterm h1 =
    679684  let hcut = state_rect_Type3 x1 h1 hterm in hcut __
     
    681686(** val state_inv_rect_Type2 :
    682687    sem_state_params -> state -> (__ Types.option -> internal_stack ->
    683     ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1 **)
     688    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
    684689let state_inv_rect_Type2 x1 hterm h1 =
    685690  let hcut = state_rect_Type2 x1 h1 hterm in hcut __
     
    687692(** val state_inv_rect_Type1 :
    688693    sem_state_params -> state -> (__ Types.option -> internal_stack ->
    689     ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1 **)
     694    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
    690695let state_inv_rect_Type1 x1 hterm h1 =
    691696  let hcut = state_rect_Type1 x1 h1 hterm in hcut __
     
    693698(** val state_inv_rect_Type0 :
    694699    sem_state_params -> state -> (__ Types.option -> internal_stack ->
    695     ByteValues.bebit -> __ -> BEMem.bemem -> __ -> 'a1) -> 'a1 **)
     700    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **)
    696701let state_inv_rect_Type0 x1 hterm h1 =
    697702  let hcut = state_rect_Type0 x1 h1 hterm in hcut __
    698 
    699 (** val state_discr : sem_state_params -> state -> state -> __ **)
    700 let state_discr a1 x y =
    701   Logic.eq_rect_Type2 x
    702     (let { st_frms = a0; istack = a10; carry = a2; regs = a3; m = a4 } = x in
    703     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
    704703
    705704(** val state_jmdiscr : sem_state_params -> state -> state -> __ **)
    706705let state_jmdiscr a1 x y =
    707706  Logic.eq_rect_Type2 x
    708     (let { st_frms = a0; istack = a10; carry = a2; regs = a3; m = a4 } = x in
    709     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
     707    (let { st_frms = a0; istack = a10; carry = a2; regs = a3; m = a4;
     708       stack_usage = a5 } = x
     709     in
     710    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
    710711
    711712(** val sp : sem_state_params -> state -> ByteValues.xpointer Errors.res **)
     
    719720    sem_state_params -> (state -> ByteValues.program_counter ->
    720721    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    721 let rec state_pc_rect_Type4 semp h_mk_state_pc x_25913 =
    722   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25913 in
     722let rec state_pc_rect_Type4 semp h_mk_state_pc x_5553 =
     723  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5553 in
    723724  h_mk_state_pc st_no_pc0 pc0 last_pop0
    724725
     
    726727    sem_state_params -> (state -> ByteValues.program_counter ->
    727728    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    728 let rec state_pc_rect_Type5 semp h_mk_state_pc x_25915 =
    729   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25915 in
     729let rec state_pc_rect_Type5 semp h_mk_state_pc x_5555 =
     730  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5555 in
    730731  h_mk_state_pc st_no_pc0 pc0 last_pop0
    731732
     
    733734    sem_state_params -> (state -> ByteValues.program_counter ->
    734735    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    735 let rec state_pc_rect_Type3 semp h_mk_state_pc x_25917 =
    736   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25917 in
     736let rec state_pc_rect_Type3 semp h_mk_state_pc x_5557 =
     737  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5557 in
    737738  h_mk_state_pc st_no_pc0 pc0 last_pop0
    738739
     
    740741    sem_state_params -> (state -> ByteValues.program_counter ->
    741742    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    742 let rec state_pc_rect_Type2 semp h_mk_state_pc x_25919 =
    743   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25919 in
     743let rec state_pc_rect_Type2 semp h_mk_state_pc x_5559 =
     744  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5559 in
    744745  h_mk_state_pc st_no_pc0 pc0 last_pop0
    745746
     
    747748    sem_state_params -> (state -> ByteValues.program_counter ->
    748749    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    749 let rec state_pc_rect_Type1 semp h_mk_state_pc x_25921 =
    750   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25921 in
     750let rec state_pc_rect_Type1 semp h_mk_state_pc x_5561 =
     751  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5561 in
    751752  h_mk_state_pc st_no_pc0 pc0 last_pop0
    752753
     
    754755    sem_state_params -> (state -> ByteValues.program_counter ->
    755756    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    756 let rec state_pc_rect_Type0 semp h_mk_state_pc x_25923 =
    757   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25923 in
     757let rec state_pc_rect_Type0 semp h_mk_state_pc x_5563 =
     758  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5563 in
    758759  h_mk_state_pc st_no_pc0 pc0 last_pop0
    759760
     
    838839  (Types.pi1 x2).st_no_pc
    839840
    840 (** val exit_pc : ByteValues.program_counter **)
    841 let exit_pc =
     841(** val init_pc : ByteValues.program_counter **)
     842let init_pc =
    842843  { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O)));
    843844    ByteValues.pc_offset = Positive.One }
     
    851852let set_m p m0 st =
    852853  { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs =
    853     st.regs; m = m0 }
     854    st.regs; m = m0; stack_usage = st.stack_usage }
    854855
    855856(** val set_regs : sem_state_params -> __ -> state -> state **)
    856857let set_regs p regs0 st =
    857858  { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = regs0;
    858     m = st.m }
     859    m = st.m; stack_usage = st.stack_usage }
    859860
    860861(** val set_sp :
     
    863864  let regs' = p.save_sp st.regs sp0 in
    864865  { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = regs';
    865   m = st.m }
     866  m = st.m; stack_usage = st.stack_usage }
    866867
    867868(** val set_carry :
     
    869870let set_carry p carry0 st =
    870871  { st_frms = st.st_frms; istack = st.istack; carry = carry0; regs = st.regs;
    871     m = st.m }
     872    m = st.m; stack_usage = st.stack_usage }
    872873
    873874(** val set_istack : sem_state_params -> internal_stack -> state -> state **)
    874875let set_istack p is st =
    875876  { st_frms = st.st_frms; istack = is; carry = st.carry; regs = st.regs; m =
    876     st.m }
     877    st.m; stack_usage = st.stack_usage }
    877878
    878879(** val set_pc :
     
    886887
    887888(** val set_last_pop :
    888     sem_state_params -> ByteValues.program_counter -> (state,
    889     ByteValues.program_counter) Types.prod -> state_pc **)
    890 let set_last_pop p s st =
    891   { st_no_pc = st.Types.fst; pc = st.Types.snd; last_pop = s }
     889    sem_state_params -> state -> ByteValues.program_counter -> state_pc **)
     890let set_last_pop p st pc0 =
     891  { st_no_pc = st; pc = pc0; last_pop = pc0 }
    892892
    893893(** val set_frms : sem_state_params -> __ -> state -> state **)
    894894let set_frms p frms st =
    895895  { st_frms = (Types.Some frms); istack = st.istack; carry = st.carry; regs =
    896     st.regs; m = st.m }
     896    st.regs; m = st.m; stack_usage = st.stack_usage }
    897897
    898898(** val fetch_function :
     
    10941094    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    10951095    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1096 let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_25978 =
     1096let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_5618 =
    10971097  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    10981098    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    11061106    set_result0; call_args_for_main = call_args_for_main0;
    11071107    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1108     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25978
     1108    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5618
    11091109  in
    11101110  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    11351135    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    11361136    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1137 let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_25980 =
     1137let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_5620 =
    11381138  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    11391139    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    11471147    set_result0; call_args_for_main = call_args_for_main0;
    11481148    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1149     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25980
     1149    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5620
    11501150  in
    11511151  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    11761176    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    11771177    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1178 let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_25982 =
     1178let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_5622 =
    11791179  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    11801180    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    11881188    set_result0; call_args_for_main = call_args_for_main0;
    11891189    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1190     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25982
     1190    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5622
    11911191  in
    11921192  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    12171217    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    12181218    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1219 let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_25984 =
     1219let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_5624 =
    12201220  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    12211221    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    12291229    set_result0; call_args_for_main = call_args_for_main0;
    12301230    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1231     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25984
     1231    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5624
    12321232  in
    12331233  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    12581258    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    12591259    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1260 let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_25986 =
     1260let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_5626 =
    12611261  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    12621262    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    12701270    set_result0; call_args_for_main = call_args_for_main0;
    12711271    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1272     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25986
     1272    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5626
    12731273  in
    12741274  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    12991299    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    13001300    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1301 let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_25988 =
     1301let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_5628 =
    13021302  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    13031303    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    13111311    set_result0; call_args_for_main = call_args_for_main0;
    13121312    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1313     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25988
     1313    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5628
    13141314  in
    13151315  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    17511751            Types.snd = pr }))))
    17521752
    1753 type sem_params = { spp : Joint.params;
    1754                     msu_pars : Joint.joint_closed_internal_function
    1755                                sem_unserialized_params;
    1756                     offset_of_point : (__ -> Positive.pos);
    1757                     point_of_offset : (Positive.pos -> __) }
    1758 
    1759 (** val sem_params_rect_Type4 :
     1753type serialized_params = { spp : Joint.params;
     1754                           msu_pars : Joint.joint_closed_internal_function
     1755                                      sem_unserialized_params;
     1756                           offset_of_point : (__ -> Positive.pos);
     1757                           point_of_offset : (Positive.pos -> __) }
     1758
     1759(** val serialized_params_rect_Type4 :
    17601760    (Joint.params -> Joint.joint_closed_internal_function
    17611761    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    1762     -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1763 let rec sem_params_rect_Type4 h_mk_sem_params x_26058 =
     1762    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
     1763let rec serialized_params_rect_Type4 h_mk_serialized_params x_5698 =
    17641764  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1765     point_of_offset = point_of_offset0 } = x_26058
    1766   in
    1767   h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
    1768 
    1769 (** val sem_params_rect_Type5 :
     1765    point_of_offset = point_of_offset0 } = x_5698
     1766  in
     1767  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     1768    __
     1769
     1770(** val serialized_params_rect_Type5 :
    17701771    (Joint.params -> Joint.joint_closed_internal_function
    17711772    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    1772     -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1773 let rec sem_params_rect_Type5 h_mk_sem_params x_26060 =
     1773    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
     1774let rec serialized_params_rect_Type5 h_mk_serialized_params x_5700 =
    17741775  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1775     point_of_offset = point_of_offset0 } = x_26060
    1776   in
    1777   h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
    1778 
    1779 (** val sem_params_rect_Type3 :
     1776    point_of_offset = point_of_offset0 } = x_5700
     1777  in
     1778  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     1779    __
     1780
     1781(** val serialized_params_rect_Type3 :
    17801782    (Joint.params -> Joint.joint_closed_internal_function
    17811783    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    1782     -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1783 let rec sem_params_rect_Type3 h_mk_sem_params x_26062 =
     1784    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
     1785let rec serialized_params_rect_Type3 h_mk_serialized_params x_5702 =
    17841786  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1785     point_of_offset = point_of_offset0 } = x_26062
    1786   in
    1787   h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
    1788 
    1789 (** val sem_params_rect_Type2 :
     1787    point_of_offset = point_of_offset0 } = x_5702
     1788  in
     1789  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     1790    __
     1791
     1792(** val serialized_params_rect_Type2 :
    17901793    (Joint.params -> Joint.joint_closed_internal_function
    17911794    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    1792     -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1793 let rec sem_params_rect_Type2 h_mk_sem_params x_26064 =
     1795    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
     1796let rec serialized_params_rect_Type2 h_mk_serialized_params x_5704 =
    17941797  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1795     point_of_offset = point_of_offset0 } = x_26064
    1796   in
    1797   h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
    1798 
    1799 (** val sem_params_rect_Type1 :
     1798    point_of_offset = point_of_offset0 } = x_5704
     1799  in
     1800  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     1801    __
     1802
     1803(** val serialized_params_rect_Type1 :
    18001804    (Joint.params -> Joint.joint_closed_internal_function
    18011805    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    1802     -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1803 let rec sem_params_rect_Type1 h_mk_sem_params x_26066 =
     1806    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
     1807let rec serialized_params_rect_Type1 h_mk_serialized_params x_5706 =
    18041808  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1805     point_of_offset = point_of_offset0 } = x_26066
    1806   in
    1807   h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
    1808 
    1809 (** val sem_params_rect_Type0 :
     1809    point_of_offset = point_of_offset0 } = x_5706
     1810  in
     1811  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     1812    __
     1813
     1814(** val serialized_params_rect_Type0 :
    18101815    (Joint.params -> Joint.joint_closed_internal_function
    18111816    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    1812     -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1813 let rec sem_params_rect_Type0 h_mk_sem_params x_26068 =
     1817    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
     1818let rec serialized_params_rect_Type0 h_mk_serialized_params x_5708 =
    18141819  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1815     point_of_offset = point_of_offset0 } = x_26068
    1816   in
    1817   h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
    1818 
    1819 (** val spp : sem_params -> Joint.params **)
     1820    point_of_offset = point_of_offset0 } = x_5708
     1821  in
     1822  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     1823    __
     1824
     1825(** val spp : serialized_params -> Joint.params **)
    18201826let rec spp xxx =
    18211827  xxx.spp
    18221828
    18231829(** val msu_pars :
    1824     sem_params -> Joint.joint_closed_internal_function
     1830    serialized_params -> Joint.joint_closed_internal_function
    18251831    sem_unserialized_params **)
    18261832let rec msu_pars xxx =
    18271833  xxx.msu_pars
    18281834
    1829 (** val offset_of_point : sem_params -> __ -> Positive.pos **)
     1835(** val offset_of_point : serialized_params -> __ -> Positive.pos **)
    18301836let rec offset_of_point xxx =
    18311837  xxx.offset_of_point
    18321838
    1833 (** val point_of_offset : sem_params -> Positive.pos -> __ **)
     1839(** val point_of_offset : serialized_params -> Positive.pos -> __ **)
    18341840let rec point_of_offset xxx =
    18351841  xxx.point_of_offset
    18361842
    1837 (** val sem_params_inv_rect_Type4 :
    1838     sem_params -> (Joint.params -> Joint.joint_closed_internal_function
    1839     sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    1840     -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    1841 let sem_params_inv_rect_Type4 hterm h1 =
    1842   let hcut = sem_params_rect_Type4 h1 hterm in hcut __
    1843 
    1844 (** val sem_params_inv_rect_Type3 :
    1845     sem_params -> (Joint.params -> Joint.joint_closed_internal_function
    1846     sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    1847     -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    1848 let sem_params_inv_rect_Type3 hterm h1 =
    1849   let hcut = sem_params_rect_Type3 h1 hterm in hcut __
    1850 
    1851 (** val sem_params_inv_rect_Type2 :
    1852     sem_params -> (Joint.params -> Joint.joint_closed_internal_function
    1853     sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    1854     -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    1855 let sem_params_inv_rect_Type2 hterm h1 =
    1856   let hcut = sem_params_rect_Type2 h1 hterm in hcut __
    1857 
    1858 (** val sem_params_inv_rect_Type1 :
    1859     sem_params -> (Joint.params -> Joint.joint_closed_internal_function
    1860     sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    1861     -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    1862 let sem_params_inv_rect_Type1 hterm h1 =
    1863   let hcut = sem_params_rect_Type1 h1 hterm in hcut __
    1864 
    1865 (** val sem_params_inv_rect_Type0 :
    1866     sem_params -> (Joint.params -> Joint.joint_closed_internal_function
    1867     sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    1868     -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    1869 let sem_params_inv_rect_Type0 hterm h1 =
    1870   let hcut = sem_params_rect_Type0 h1 hterm in hcut __
    1871 
    1872 (** val sem_params_jmdiscr : sem_params -> sem_params -> __ **)
    1873 let sem_params_jmdiscr x y =
     1843(** val serialized_params_inv_rect_Type4 :
     1844    serialized_params -> (Joint.params ->
     1845    Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
     1846    Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     1847let serialized_params_inv_rect_Type4 hterm h1 =
     1848  let hcut = serialized_params_rect_Type4 h1 hterm in hcut __
     1849
     1850(** val serialized_params_inv_rect_Type3 :
     1851    serialized_params -> (Joint.params ->
     1852    Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
     1853    Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     1854let serialized_params_inv_rect_Type3 hterm h1 =
     1855  let hcut = serialized_params_rect_Type3 h1 hterm in hcut __
     1856
     1857(** val serialized_params_inv_rect_Type2 :
     1858    serialized_params -> (Joint.params ->
     1859    Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
     1860    Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     1861let serialized_params_inv_rect_Type2 hterm h1 =
     1862  let hcut = serialized_params_rect_Type2 h1 hterm in hcut __
     1863
     1864(** val serialized_params_inv_rect_Type1 :
     1865    serialized_params -> (Joint.params ->
     1866    Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
     1867    Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     1868let serialized_params_inv_rect_Type1 hterm h1 =
     1869  let hcut = serialized_params_rect_Type1 h1 hterm in hcut __
     1870
     1871(** val serialized_params_inv_rect_Type0 :
     1872    serialized_params -> (Joint.params ->
     1873    Joint.joint_closed_internal_function sem_unserialized_params -> (__ ->
     1874    Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     1875let serialized_params_inv_rect_Type0 hterm h1 =
     1876  let hcut = serialized_params_rect_Type0 h1 hterm in hcut __
     1877
     1878(** val serialized_params_jmdiscr :
     1879    serialized_params -> serialized_params -> __ **)
     1880let serialized_params_jmdiscr x y =
    18741881  Logic.eq_rect_Type2 x
    18751882    (let { spp = a0; msu_pars = a1; offset_of_point = a2; point_of_offset =
     
    18781885    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
    18791886
    1880 (** val spp__o__stmt_pars : sem_params -> Joint.stmt_params **)
     1887(** val spp__o__stmt_pars : serialized_params -> Joint.stmt_params **)
    18811888let spp__o__stmt_pars x0 =
    18821889  x0.spp.Joint.stmt_pars
    18831890
    1884 (** val spp__o__stmt_pars__o__uns_pars : sem_params -> Joint.uns_params **)
     1891(** val spp__o__stmt_pars__o__uns_pars :
     1892    serialized_params -> Joint.uns_params **)
    18851893let spp__o__stmt_pars__o__uns_pars x0 =
    18861894  Joint.stmt_pars__o__uns_pars x0.spp
    18871895
    18881896(** val spp__o__stmt_pars__o__uns_pars__o__u_pars :
    1889     sem_params -> Joint.unserialized_params **)
     1897    serialized_params -> Joint.unserialized_params **)
    18901898let spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
    18911899  Joint.stmt_pars__o__uns_pars__o__u_pars x0.spp
    18921900
    1893 (** val msu_pars__o__st_pars : sem_params -> sem_state_params **)
     1901(** val msu_pars__o__st_pars : serialized_params -> sem_state_params **)
    18941902let msu_pars__o__st_pars x0 =
    18951903  x0.msu_pars.st_pars
     1904
     1905type sem_params = { spp' : serialized_params;
     1906                    pre_main_generator : (Joint.joint_program ->
     1907                                         Joint.joint_closed_internal_function) }
     1908
     1909(** val sem_params_rect_Type4 :
     1910    (serialized_params -> (Joint.joint_program ->
     1911    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
     1912let rec sem_params_rect_Type4 h_mk_sem_params x_5726 =
     1913  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5726 in
     1914  h_mk_sem_params spp'0 pre_main_generator0
     1915
     1916(** val sem_params_rect_Type5 :
     1917    (serialized_params -> (Joint.joint_program ->
     1918    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
     1919let rec sem_params_rect_Type5 h_mk_sem_params x_5728 =
     1920  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5728 in
     1921  h_mk_sem_params spp'0 pre_main_generator0
     1922
     1923(** val sem_params_rect_Type3 :
     1924    (serialized_params -> (Joint.joint_program ->
     1925    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
     1926let rec sem_params_rect_Type3 h_mk_sem_params x_5730 =
     1927  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5730 in
     1928  h_mk_sem_params spp'0 pre_main_generator0
     1929
     1930(** val sem_params_rect_Type2 :
     1931    (serialized_params -> (Joint.joint_program ->
     1932    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
     1933let rec sem_params_rect_Type2 h_mk_sem_params x_5732 =
     1934  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5732 in
     1935  h_mk_sem_params spp'0 pre_main_generator0
     1936
     1937(** val sem_params_rect_Type1 :
     1938    (serialized_params -> (Joint.joint_program ->
     1939    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
     1940let rec sem_params_rect_Type1 h_mk_sem_params x_5734 =
     1941  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5734 in
     1942  h_mk_sem_params spp'0 pre_main_generator0
     1943
     1944(** val sem_params_rect_Type0 :
     1945    (serialized_params -> (Joint.joint_program ->
     1946    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
     1947let rec sem_params_rect_Type0 h_mk_sem_params x_5736 =
     1948  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5736 in
     1949  h_mk_sem_params spp'0 pre_main_generator0
     1950
     1951(** val spp' : sem_params -> serialized_params **)
     1952let rec spp' xxx =
     1953  xxx.spp'
     1954
     1955(** val pre_main_generator :
     1956    sem_params -> Joint.joint_program -> Joint.joint_closed_internal_function **)
     1957let rec pre_main_generator xxx =
     1958  xxx.pre_main_generator
     1959
     1960(** val sem_params_inv_rect_Type4 :
     1961    sem_params -> (serialized_params -> (Joint.joint_program ->
     1962    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
     1963let sem_params_inv_rect_Type4 hterm h1 =
     1964  let hcut = sem_params_rect_Type4 h1 hterm in hcut __
     1965
     1966(** val sem_params_inv_rect_Type3 :
     1967    sem_params -> (serialized_params -> (Joint.joint_program ->
     1968    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
     1969let sem_params_inv_rect_Type3 hterm h1 =
     1970  let hcut = sem_params_rect_Type3 h1 hterm in hcut __
     1971
     1972(** val sem_params_inv_rect_Type2 :
     1973    sem_params -> (serialized_params -> (Joint.joint_program ->
     1974    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
     1975let sem_params_inv_rect_Type2 hterm h1 =
     1976  let hcut = sem_params_rect_Type2 h1 hterm in hcut __
     1977
     1978(** val sem_params_inv_rect_Type1 :
     1979    sem_params -> (serialized_params -> (Joint.joint_program ->
     1980    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
     1981let sem_params_inv_rect_Type1 hterm h1 =
     1982  let hcut = sem_params_rect_Type1 h1 hterm in hcut __
     1983
     1984(** val sem_params_inv_rect_Type0 :
     1985    sem_params -> (serialized_params -> (Joint.joint_program ->
     1986    Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
     1987let sem_params_inv_rect_Type0 hterm h1 =
     1988  let hcut = sem_params_rect_Type0 h1 hterm in hcut __
     1989
     1990(** val sem_params_jmdiscr : sem_params -> sem_params -> __ **)
     1991let sem_params_jmdiscr x y =
     1992  Logic.eq_rect_Type2 x
     1993    (let { spp' = a0; pre_main_generator = a1 } = x in
     1994    Obj.magic (fun _ dH -> dH __ __)) y
     1995
     1996(** val spp'__o__msu_pars :
     1997    sem_params -> Joint.joint_closed_internal_function
     1998    sem_unserialized_params **)
     1999let spp'__o__msu_pars x0 =
     2000  x0.spp'.msu_pars
     2001
     2002(** val spp'__o__msu_pars__o__st_pars : sem_params -> sem_state_params **)
     2003let spp'__o__msu_pars__o__st_pars x0 =
     2004  msu_pars__o__st_pars x0.spp'
     2005
     2006(** val spp'__o__spp : sem_params -> Joint.params **)
     2007let spp'__o__spp x0 =
     2008  x0.spp'.spp
     2009
     2010(** val spp'__o__spp__o__stmt_pars : sem_params -> Joint.stmt_params **)
     2011let spp'__o__spp__o__stmt_pars x0 =
     2012  spp__o__stmt_pars x0.spp'
     2013
     2014(** val spp'__o__spp__o__stmt_pars__o__uns_pars :
     2015    sem_params -> Joint.uns_params **)
     2016let spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
     2017  spp__o__stmt_pars__o__uns_pars x0.spp'
     2018
     2019(** val spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
     2020    sem_params -> Joint.unserialized_params **)
     2021let spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
     2022  spp__o__stmt_pars__o__uns_pars__o__u_pars x0.spp'
    18962023
    18972024(** val pc_of_point :
     
    18992026    ByteValues.program_counter **)
    19002027let pc_of_point p bl pt =
    1901   { ByteValues.pc_block = bl; ByteValues.pc_offset = (p.offset_of_point pt) }
     2028  { ByteValues.pc_block = bl; ByteValues.pc_offset =
     2029    (p.spp'.offset_of_point pt) }
    19022030
    19032031(** val point_of_pc : sem_params -> ByteValues.program_counter -> __ **)
    19042032let point_of_pc p ptr =
    1905   p.point_of_offset ptr.ByteValues.pc_offset
     2033  p.spp'.point_of_offset ptr.ByteValues.pc_offset
    19062034
    19072035(** val fetch_statement :
     
    19202048          (Errors.opt_to_res
    19212049            (Errors.msg ErrorMessages.ProgramCounterOutOfCode)
    1922             (p.spp.Joint.stmt_at globals (Types.pi1 fn).Joint.joint_if_code
    1923               pt))) (fun stmt ->
     2050            ((spp'__o__spp p).Joint.stmt_at globals
     2051              (Types.pi1 fn).Joint.joint_if_code pt))) (fun stmt ->
    19242052        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    19252053          { Types.fst = id; Types.snd = fn }; Types.snd = stmt })))
     
    19382066            ErrorMessages.LabelNotFound), (List.Cons ((Errors.CTX
    19392067            (PreIdentifiers.LabelTag, lbl)), List.Nil))))
    1940             (p.spp.Joint.point_of_label globals
     2068            ((spp'__o__spp p).Joint.point_of_label globals
    19412069              (Types.pi1 fn).Joint.joint_if_code lbl))) (fun pt ->
    19422070        Monad.m_return0 (Monad.max_def Errors.res0) { ByteValues.pc_block =
    1943           bl; ByteValues.pc_offset = (p.offset_of_point pt) })))
     2071          bl; ByteValues.pc_offset = (p.spp'.offset_of_point pt) })))
    19442072
    19452073(** val succ_pc :
     
    19482076let succ_pc p ptr nxt =
    19492077  let curr = point_of_pc p ptr in
    1950   pc_of_point p ptr.ByteValues.pc_block (p.spp.Joint.point_of_succ curr nxt)
     2078  pc_of_point p ptr.ByteValues.pc_block
     2079    ((spp'__o__spp p).Joint.point_of_succ curr nxt)
    19512080
    19522081(** val goto :
     
    19592088      (fun newpc ->
    19602089      Monad.m_return0 (Monad.max_def Errors.res0)
    1961         (set_pc (msu_pars__o__st_pars p) newpc st)))
     2090        (set_pc (spp'__o__msu_pars__o__st_pars p) newpc st)))
    19622091
    19632092(** val next : sem_params -> __ -> state_pc -> state_pc **)
    19642093let next p l st =
    1965   let newpc = succ_pc p st.pc l in set_pc (msu_pars__o__st_pars p) newpc st
     2094  let newpc = succ_pc p st.pc l in
     2095  set_pc (spp'__o__msu_pars__o__st_pars p) newpc st
    19662096
    19672097(** val next_of_call_pc :
     
    19992129  match seq with
    20002130  | Joint.COMMENT x ->
    2001 prerr_endline "COMMENT";
    20022131    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st)
    20032132  | Joint.MOVE dst_src ->
    2004 prerr_endline "MOVE";
    20052133    Obj.magic
    2006       (pair_reg_move (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2007         p.msu_pars st dst_src)
     2134      (pair_reg_move (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2135        p.spp'.msu_pars st dst_src)
    20082136  | Joint.POP dst ->
    2009 prerr_endline "POP";
    20102137    Obj.magic
    20112138      (Monad.m_bind2 (Monad.max_def Errors.res0)
    2012         (Obj.magic (pop (msu_pars__o__st_pars p) st)) (fun v st' ->
     2139        (Obj.magic (pop (spp'__o__msu_pars__o__st_pars p) st)) (fun v st' ->
    20132140        Obj.magic
    2014           (acca_store (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2015             p.msu_pars dst v st')))
     2141          (acca_store (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2142            (spp'__o__msu_pars p) dst v st')))
    20162143  | Joint.PUSH src ->
    2017 prerr_endline "PUSH";
    20182144    Obj.magic
    20192145      (Monad.m_bind0 (Monad.max_def Errors.res0)
    20202146        (Obj.magic
    2021           (acca_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2022             p.msu_pars st src)) (fun v ->
    2023         Obj.magic (push (msu_pars__o__st_pars p) st v)))
     2147          (acca_arg_retrieve
     2148            (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2149            p.spp'.msu_pars st src)) (fun v ->
     2150        Obj.magic (push (spp'__o__msu_pars__o__st_pars p) st v)))
    20242151  | Joint.ADDRESS (id, ldest, hdest) ->
    2025 prerr_endline "ADDRESS";
    20262152    let addr_block =
    20272153      Option.opt_safe
    20282154        (Globalenvs.find_symbol
    2029           (let p0 = p.spp in let globals0 = globals in let g = ge0 in g.ge)
    2030           id)
     2155          (let p0 = spp'__o__spp p in
     2156          let globals0 = globals in let g = ge0 in g.ge) id)
    20312157    in
    20322158    let { Types.fst = laddr; Types.snd = haddr } =
     
    20372163      (Monad.m_bind0 (Monad.max_def Errors.res0)
    20382164        (Obj.magic
    2039           (dpl_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p) p.msu_pars
    2040             ldest laddr st)) (fun st' ->
     2165          (dpl_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
     2166            p.spp'.msu_pars ldest laddr st)) (fun st' ->
    20412167        Obj.magic
    2042           (dph_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p) p.msu_pars
    2043             hdest haddr st')))
     2168          (dph_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
     2169            p.spp'.msu_pars hdest haddr st')))
    20442170  | Joint.OPACCS (op, dacc_a_reg, dacc_b_reg, sacc_a_reg, sacc_b_reg) ->
    20452171    Obj.magic
    20462172      (Monad.m_bind0 (Monad.max_def Errors.res0)
    20472173        (Obj.magic
    2048           (acca_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2049             p.msu_pars st sacc_a_reg)) (fun v1 ->
     2174          (acca_arg_retrieve
     2175            (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2176            p.spp'.msu_pars st sacc_a_reg)) (fun v1 ->
    20502177        Monad.m_bind0 (Monad.max_def Errors.res0)
    20512178          (Obj.magic
    20522179            (accb_arg_retrieve
    2053               (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp) p.msu_pars st
    2054               sacc_b_reg)) (fun v2 ->
     2180              (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2181              p.spp'.msu_pars st sacc_b_reg)) (fun v2 ->
    20552182          Monad.m_bind2 (Monad.max_def Errors.res0)
    20562183            (Obj.magic (BackEndOps.be_opaccs op v1 v2)) (fun v1' v2' ->
    20572184            Monad.m_bind0 (Monad.max_def Errors.res0)
    20582185              (Obj.magic
    2059                 (acca_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p)
    2060                   p.msu_pars dacc_a_reg v1' st)) (fun st' ->
     2186                (acca_store
     2187                  (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
     2188                  p.spp'.msu_pars dacc_a_reg v1' st)) (fun st' ->
    20612189              Obj.magic
    2062                 (accb_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p)
    2063                   p.msu_pars dacc_b_reg v2' st'))))))
     2190                (accb_store
     2191                  (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
     2192                  p.spp'.msu_pars dacc_b_reg v2' st'))))))
    20642193  | Joint.OP1 (op, dacc_a, sacc_a) ->
    2065 prerr_endline "OP1";
    20662194    Obj.magic
    20672195      (Monad.m_bind0 (Monad.max_def Errors.res0)
    20682196        (Obj.magic
    2069           (acca_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2070             p.msu_pars st sacc_a)) (fun v ->
     2197          (acca_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2198            p.spp'.msu_pars st sacc_a)) (fun v ->
    20712199        Monad.m_bind0 (Monad.max_def Errors.res0)
    20722200          (Obj.magic (BackEndOps.be_op1 op v)) (fun v' ->
    20732201          Obj.magic
    2074             (acca_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p)
    2075               p.msu_pars dacc_a v' st))))
     2202            (acca_store
     2203              (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
     2204              p.spp'.msu_pars dacc_a v' st))))
    20762205  | Joint.OP2 (op, dacc_a, sacc_a, src) ->
    2077 prerr_endline "OP2";
    20782206    Obj.magic
    20792207      (Monad.m_bind0 (Monad.max_def Errors.res0)
    20802208        (Obj.magic
    2081           (acca_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2082             p.msu_pars st sacc_a)) (fun v1 ->
     2209          (acca_arg_retrieve
     2210            (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2211            p.spp'.msu_pars st sacc_a)) (fun v1 ->
    20832212        Monad.m_bind0 (Monad.max_def Errors.res0)
    20842213          (Obj.magic
    2085             (snd_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2086               p.msu_pars st src)) (fun v2 ->
     2214            (snd_arg_retrieve
     2215              (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2216              p.spp'.msu_pars st src)) (fun v2 ->
    20872217          Monad.m_bind2 (Monad.max_def Errors.res0)
    20882218            (Obj.magic (BackEndOps.be_op2 st.carry op v1 v2))
    20892219            (fun v' carry0 ->
    2090 (if op = BackEndOps.Sub then
    2091 (if carry0 = ByteValues.BBbit Bool.True then prerr_endline "CARRY = 1" else prerr_endline "CARRY = 0"));
    20922220            Monad.m_bind0 (Monad.max_def Errors.res0)
    20932221              (Obj.magic
    2094                 (acca_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p)
    2095                   p.msu_pars dacc_a v' st)) (fun st' ->
     2222                (acca_store
     2223                  (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
     2224                  p.spp'.msu_pars dacc_a v' st)) (fun st' ->
    20962225              Monad.m_return0 (Monad.max_def Errors.res0)
    2097                 (set_carry p.msu_pars.st_pars carry0 st'))))))
     2226                (set_carry p.spp'.msu_pars.st_pars carry0 st'))))))
    20982227  | Joint.CLEAR_CARRY ->
    2099 prerr_endline "CLEAR_CARRY";
    21002228    Obj.magic
    21012229      (Monad.m_return0 (Monad.max_def Errors.res0)
    2102         (set_carry (msu_pars__o__st_pars p) (ByteValues.BBbit Bool.False) st))
     2230        (set_carry (spp'__o__msu_pars__o__st_pars p) (ByteValues.BBbit
     2231          Bool.False) st))
    21032232  | Joint.SET_CARRY ->
    2104 prerr_endline "SET_CARRY";
    21052233    Obj.magic
    21062234      (Monad.m_return0 (Monad.max_def Errors.res0)
    2107         (set_carry (msu_pars__o__st_pars p) (ByteValues.BBbit Bool.True) st))
     2235        (set_carry (spp'__o__msu_pars__o__st_pars p) (ByteValues.BBbit
     2236          Bool.True) st))
    21082237  | Joint.LOAD (dst, addrl, addrh) ->
    2109 prerr_endline "LOAD";
    21102238    Obj.magic
    21112239      (Monad.m_bind0 (Monad.max_def Errors.res0)
    21122240        (Obj.magic
    2113           (dph_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2114             p.msu_pars st addrh)) (fun vaddrh ->
     2241          (dph_arg_retrieve
     2242            (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2243            p.spp'.msu_pars st addrh)) (fun vaddrh ->
    21152244        Monad.m_bind0 (Monad.max_def Errors.res0)
    21162245          (Obj.magic
    2117             (dpl_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2118               p.msu_pars st addrl)) (fun vaddrl ->
     2246            (dpl_arg_retrieve
     2247              (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2248              p.spp'.msu_pars st addrl)) (fun vaddrl ->
    21192249          Monad.m_bind0 (Monad.max_def Errors.res0)
    21202250            (Obj.magic
     
    21262256                  (GenMem.beloadv st.m vaddr))) (fun v ->
    21272257              Obj.magic
    2128                 (acca_store (spp__o__stmt_pars__o__uns_pars__o__u_pars p)
    2129                   p.msu_pars dst v st))))))
     2258                (acca_store
     2259                  (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p)
     2260                  p.spp'.msu_pars dst v st))))))
    21302261  | Joint.STORE (addrl, addrh, src) ->
    2131 prerr_endline "STORE";
    21322262    Obj.magic
    21332263      (Monad.m_bind0 (Monad.max_def Errors.res0)
    21342264        (Obj.magic
    2135           (dph_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2136             p.msu_pars st addrh)) (fun vaddrh ->
     2265          (dph_arg_retrieve
     2266            (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2267            p.spp'.msu_pars st addrh)) (fun vaddrh ->
    21372268        Monad.m_bind0 (Monad.max_def Errors.res0)
    21382269          (Obj.magic
    2139             (dpl_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2140               p.msu_pars st addrl)) (fun vaddrl ->
     2270            (dpl_arg_retrieve
     2271              (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2272              p.spp'.msu_pars st addrl)) (fun vaddrl ->
    21412273          Monad.m_bind0 (Monad.max_def Errors.res0)
    21422274            (Obj.magic
     
    21462278              (Obj.magic
    21472279                (acca_arg_retrieve
    2148                   (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp) p.msu_pars
    2149                   st src)) (fun v ->
     2280                  (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2281                  p.spp'.msu_pars st src)) (fun v ->
    21502282              Monad.m_bind0 (Monad.max_def Errors.res0)
    21512283                (Obj.magic
     
    21532285                    (GenMem.bestorev st.m vaddr v))) (fun m' ->
    21542286                Monad.m_return0 (Monad.max_def Errors.res0)
    2155                   (set_m (msu_pars__o__st_pars p) m' st)))))))
    2156   | Joint.Extension_seq c -> p.msu_pars.eval_ext_seq globals ge0 c curr_id st
     2287                  (set_m (spp'__o__msu_pars__o__st_pars p) m' st)))))))
     2288  | Joint.Extension_seq c ->
     2289    p.spp'.msu_pars.eval_ext_seq globals ge0 c curr_id st
    21572290
    21582291(** val code_block_of_block :
     
    21902323       Monad.m_bind0 (Monad.max_def Errors.res0)
    21912324         (Obj.magic
    2192            (dpl_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2193              p.msu_pars st addr.Types.fst)) (fun addr_l ->
     2325           (dpl_arg_retrieve
     2326             (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2327             p.spp'.msu_pars st addr.Types.fst)) (fun addr_l ->
    21942328         Monad.m_bind0 (Monad.max_def Errors.res0)
    21952329           (Obj.magic
    21962330             (dph_arg_retrieve
    2197                (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp) p.msu_pars st
    2198                addr.Types.snd)) (fun addr_h ->
     2331               (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2332               p.spp'.msu_pars st addr.Types.snd)) (fun addr_h ->
    21992333           Monad.m_bind0 (Monad.max_def Errors.res0)
    22002334             (Obj.magic
     
    22202354let eval_external_call p fn args dest st =
    22212355  Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    2222     (let x = IOMonad.err_to_io (p.msu_pars.fetch_external_args fn st args) in
     2356    (let x =
     2357       IOMonad.err_to_io
     2358         ((spp'__o__msu_pars p).fetch_external_args fn st args)
     2359     in
    22232360    Obj.magic x) (fun params ->
    22242361    Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
     
    22352372          ((IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres), List.Nil)
    22362373        in
    2237         Obj.magic (IOMonad.err_to_io (p.msu_pars.set_result vs dest st)))))
     2374        Obj.magic
     2375          (IOMonad.err_to_io ((spp'__o__msu_pars p).set_result vs dest st)))))
     2376
     2377(** val increment_stack_usage :
     2378    sem_state_params -> Nat.nat -> state -> state **)
     2379let increment_stack_usage p n st =
     2380  { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs =
     2381    st.regs; m = st.m; stack_usage = (Nat.plus n st.stack_usage) }
     2382
     2383(** val decrement_stack_usage :
     2384    sem_state_params -> Nat.nat -> state -> state **)
     2385let decrement_stack_usage p n st =
     2386  { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs =
     2387    st.regs; m = st.m; stack_usage = (Nat.minus st.stack_usage n) }
    22382388
    22392389(** val eval_internal_call :
     
    22472397        (PreIdentifiers.SymbolTag, i)), List.Nil)))) (ge0.stack_sizes i)))
    22482398    (fun stack_size ->
    2249     Obj.magic
    2250       (p.msu_pars.setup_call stack_size fn.Joint.joint_if_params args st))
     2399    Monad.m_bind0 (Monad.max_def Errors.res0)
     2400      (Obj.magic
     2401        (p.spp'.msu_pars.setup_call stack_size fn.Joint.joint_if_params args
     2402          st)) (fun st' ->
     2403      Monad.m_return0 (Monad.max_def Errors.res0)
     2404        (increment_stack_usage p.spp'.msu_pars.st_pars stack_size st')))
    22512405
    22522406(** val is_inl : ('a1, 'a2) Types.sum -> Bool.bool **)
     
    22642418         (Obj.magic
    22652419           (block_of_call p globals
    2266              (let p0 = p.spp in
     2420             (let p0 = spp'__o__spp p in
    22672421             let globals0 = globals in let g = ge0 in g.ge) f st.st_no_pc))
    22682422     in
     
    22722426         IOMonad.err_to_io
    22732427           (fetch_function
    2274              (let p0 = p.spp in
     2428             (let p0 = spp'__o__spp p in
    22752429             let globals0 = globals in let g = ge0 in g.ge) bl)
    22762430       in
     
    22832437              (Monad.m_bind0 (Monad.max_def Errors.res0)
    22842438                (Obj.magic
    2285                   (p.msu_pars.save_frame
     2439                  (p.spp'.msu_pars.save_frame
    22862440                    (kind_of_call
    2287                       (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp) f) dest
    2288                     st)) (fun st' ->
     2441                      (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) f)
     2442                    dest st)) (fun st' ->
    22892443                Monad.m_bind0 (Monad.max_def Errors.res0)
    22902444                  (eval_internal_call p globals ge0 i (Types.pi1 ifd) args
     
    23212475
    23222476(** val eval_return :
    2323     sem_params -> AST.ident List.list -> genv -> AST.ident -> __ -> state ->
    2324     __ **)
     2477    sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier ->
     2478    __ -> state -> __ **)
    23252479let eval_return p globals ge0 curr_id curr_ret st =
    2326 prerr_endline "eval_return";
    23272480  Monad.m_bind0 (Monad.max_def Errors.res0)
    2328     (Obj.magic (p.msu_pars.pop_frame globals ge0 curr_id curr_ret st))
    2329     (fun st' ->
    2330     Monad.m_bind0 (Monad.max_def Errors.res0)
    2331       (Obj.magic
    2332         (next_of_call_pc p globals
    2333           (let p0 = p.spp in let globals0 = globals in let g = ge0 in g.ge)
    2334           st'.Types.snd)) (fun nxt ->
    2335       Monad.m_return0 (Monad.max_def Errors.res0)
    2336         (next p nxt (set_last_pop p.msu_pars.st_pars st'.Types.snd st'))))
     2481    (Obj.magic
     2482      (Errors.opt_to_res (List.Cons ((Errors.MSG
     2483        ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX
     2484        (PreIdentifiers.SymbolTag, curr_id)), List.Nil))))
     2485        (ge0.stack_sizes curr_id))) (fun stack_size ->
     2486    Monad.m_bind2 (Monad.max_def Errors.res0)
     2487      (Obj.magic (p.spp'.msu_pars.pop_frame globals ge0 curr_id curr_ret st))
     2488      (fun st' call_pc ->
     2489      Monad.m_bind0 (Monad.max_def Errors.res0)
     2490        (Obj.magic
     2491          (next_of_call_pc p globals
     2492            (let p0 = spp'__o__spp p in
     2493            let globals0 = globals in let g = ge0 in g.ge) call_pc))
     2494        (fun nxt ->
     2495        let st'' =
     2496          set_last_pop p.spp'.msu_pars.st_pars
     2497            (decrement_stack_usage p.spp'.msu_pars.st_pars stack_size st')
     2498            call_pc
     2499        in
     2500        Monad.m_return0 (Monad.max_def Errors.res0) (next p nxt st''))))
    23372501
    23382502(** val eval_tailcall :
    23392503    sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier,
    2340     (__, __) Types.prod) Types.sum -> __ -> AST.ident -> __ -> state_pc -> __ **)
     2504    (__, __) Types.prod) Types.sum -> __ -> PreIdentifiers.identifier -> __
     2505    -> state_pc -> __ **)
    23412506let eval_tailcall p globals ge0 f args curr_f curr_ret st =
    23422507  Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
     
    23452510         (Obj.magic
    23462511           (block_of_call p globals
    2347              (let p0 = p.spp in
     2512             (let p0 = spp'__o__spp p in
    23482513             let globals0 = globals in let g = ge0 in g.ge) f st.st_no_pc))
    23492514     in
     
    23532518         IOMonad.err_to_io
    23542519           (fetch_function
    2355              (let p0 = p.spp in
     2520             (let p0 = spp'__o__spp p in
    23562521             let globals0 = globals in let g = ge0 in g.ge) bl)
    23572522       in
     
    23632528            (Obj.magic
    23642529              (Monad.m_bind0 (Monad.max_def Errors.res0)
    2365                 (eval_internal_call p globals ge0 i (Types.pi1 ifd) args
    2366                   st.st_no_pc) (fun st' ->
    2367                 let pc0 =
    2368                   pc_of_point p bl (Types.pi1 ifd).Joint.joint_if_entry
     2530                (Obj.magic
     2531                  (Errors.opt_to_res (List.Cons ((Errors.MSG
     2532                    ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX
     2533                    (PreIdentifiers.SymbolTag, curr_f)), List.Nil))))
     2534                    (ge0.stack_sizes curr_f))) (fun stack_size ->
     2535                let st' =
     2536                  decrement_stack_usage (spp'__o__msu_pars__o__st_pars p)
     2537                    stack_size st.st_no_pc
    23692538                in
    2370                 Monad.m_return0 (Monad.max_def Errors.res0) { st_no_pc = st';
    2371                   pc = pc0; last_pop = st.last_pop }))))
     2539                Monad.m_bind0 (Monad.max_def Errors.res0)
     2540                  (eval_internal_call p globals ge0 i (Types.pi1 ifd) args
     2541                    st') (fun st'' ->
     2542                  let pc0 =
     2543                    pc_of_point p bl (Types.pi1 ifd).Joint.joint_if_entry
     2544                  in
     2545                  Monad.m_return0 (Monad.max_def Errors.res0) { st_no_pc =
     2546                    st''; pc = pc0; last_pop = st.last_pop })))))
    23722547      | AST.External efd ->
    23732548        Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
     
    23872562    (match s0 with
    23882563     | Joint.COST_LABEL x ->
    2389 prerr_endline "COST";
    23902564       Obj.magic
    23912565         (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) (next p nxt st))
    23922566     | Joint.CALL (f, args, dest) ->
    2393 prerr_endline "CALL";
    23942567       Obj.magic (eval_call p g ge0 f args dest nxt st)
    23952568     | Joint.COND (a, l) ->
    2396 prerr_endline "COND";
    23972569       IOMonad.err_to_io
    23982570         (Obj.magic
    23992571           (Monad.m_bind0 (Monad.max_def Errors.res0)
    24002572             (Obj.magic
    2401                (acca_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2402                  p.msu_pars st.st_no_pc a)) (fun v ->
     2573               (acca_retrieve
     2574                 (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2575                 p.spp'.msu_pars st.st_no_pc a)) (fun v ->
    24032576             Monad.m_bind0 (Monad.max_def Errors.res0)
    24042577               (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
     
    24072580                 Obj.magic
    24082581                   (goto p g
    2409                      (let p0 = p.spp in
     2582                     (let p0 = spp'__o__spp p in
    24102583                     let globals = g in let g0 = ge0 in g0.ge) l st)
    24112584               | Bool.False ->
     
    24182591    (match s0 with
    24192592     | Joint.GOTO l ->
    2420 prerr_endline "GOTO";
    24212593       IOMonad.err_to_io
    24222594         (goto p g
    2423            (let p0 = p.spp in let globals = g in let g0 = ge0 in g0.ge) l st)
     2595           (let p0 = spp'__o__spp p in
     2596           let globals = g in let g0 = ge0 in g0.ge) l st)
    24242597     | Joint.RETURN ->
    2425 prerr_endline "RETURN";
    24262598       IOMonad.err_to_io
    24272599         (Obj.magic (eval_return p g ge0 curr_id curr_ret st.st_no_pc))
    24282600     | Joint.TAILCALL (f, args) ->
    2429 prerr_endline "TAILCALL";
    24302601       Obj.magic (eval_tailcall p g ge0 f args curr_id curr_ret st))
    24312602  | Joint.FCOND (a, lbltrue, lblfalse) ->
    2432 prerr_endline "FCOND";
    24332603    IOMonad.err_to_io
    24342604      (Obj.magic
    24352605        (Monad.m_bind0 (Monad.max_def Errors.res0)
    24362606          (Obj.magic
    2437             (acca_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp)
    2438               p.msu_pars st.st_no_pc a)) (fun v ->
     2607            (acca_retrieve
     2608              (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp)
     2609              p.spp'.msu_pars st.st_no_pc a)) (fun v ->
    24392610          Monad.m_bind0 (Monad.max_def Errors.res0)
    24402611            (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
     
    24432614              Obj.magic
    24442615                (goto p g
    2445                   (let p0 = p.spp in
     2616                  (let p0 = spp'__o__spp p in
    24462617                  let globals = g in let g0 = ge0 in g0.ge) lbltrue st)
    24472618            | Bool.False ->
    24482619              Obj.magic
    24492620                (goto p g
    2450                   (let p0 = p.spp in
     2621                  (let p0 = spp'__o__spp p in
    24512622                  let globals = g in let g0 = ge0 in g0.ge) lblfalse st)))))
    24522623
     
    24602631         IOMonad.err_to_io
    24612632           (fetch_statement p globals
    2462              (let p0 = p.spp in
     2633             (let p0 = spp'__o__spp p in
    24632634             let globals0 = globals in let g = ge0 in g.ge) st.pc)
    24642635       in
    24652636      Obj.magic x) (fun id fn s ->
    2466 prerr_endline ("ID == " ^ string_of_int (Glue.int_of_matitapos id));
    2467        let res =
    24682637      Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    24692638        (let x =
     
    24722641         in
    24732642        Obj.magic x) (fun st' ->
    2474         let st'' = set_no_pc (msu_pars__o__st_pars p) st' st in
    2475         Obj.magic (eval_statement_advance p globals ge0 id fn s st''))
    2476     in
    2477      match Obj.magic res with
    2478      | Wrong e ->
    2479         print_string "fun_";
    2480         print_int (Glue.int_of_matitapos id);
    2481         print_string ":";
    2482         let point = pc_offset (pc (msu_pars__o__st_pars p) st) in
    2483         print_int (Glue.int_of_matitapos point);
    2484         print_string ":";
    2485         res
    2486      | _ -> res))
    2487 
    2488 (** val is_final :
    2489     sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter
    2490     -> state_pc -> Integers.int Types.option **)
    2491 let is_final p globals ge0 exit st =
    2492   Errors.res_to_opt
    2493     (Obj.magic
    2494       (Monad.m_bind3 (Monad.max_def Errors.res0)
    2495         (Obj.magic
    2496           (fetch_statement p globals
    2497             (let p0 = p.spp in let globals0 = globals in let g = ge0 in g.ge)
    2498             st.pc)) (fun id fn s ->
    2499         match s with
    2500         | Joint.Sequential (x, x0) -> Obj.magic (Errors.Error List.Nil)
    2501         | Joint.Final s' ->
    2502           (match s' with
    2503            | Joint.GOTO x -> Obj.magic (Errors.Error List.Nil)
    2504            | Joint.RETURN ->
    2505              let curr_ret = (Types.pi1 fn).Joint.joint_if_result in
    2506              Monad.m_bind0 (Monad.max_def Errors.res0)
    2507                (Obj.magic
    2508                  (p.msu_pars.pop_frame globals ge0 id curr_ret st.st_no_pc))
    2509                (fun st' ->
    2510                match ByteValues.eq_program_counter st'.Types.snd exit with
    2511                | Bool.True ->
    2512                  Monad.m_bind0 (Monad.max_def Errors.res0)
    2513                    (Obj.magic
    2514                      (p.msu_pars.read_result globals
    2515                        (let p0 = p.spp in
    2516                        let globals0 = globals in let g = ge0 in g.ge)
    2517                        curr_ret st.st_no_pc)) (fun vals ->
    2518                    Obj.magic (ByteValues.word_of_list_beval vals))
    2519                | Bool.False -> Obj.magic (Errors.Error List.Nil))
    2520            | Joint.TAILCALL (x0, x1) -> Obj.magic (Errors.Error List.Nil))
    2521         | Joint.FCOND (x0, x1, x2) -> Obj.magic (Errors.Error List.Nil))))
     2643        let st'' = set_no_pc (spp'__o__msu_pars__o__st_pars p) st' st in
     2644        Obj.magic (eval_statement_advance p globals ge0 id fn s st''))))
     2645
Note: See TracChangeset for help on using the changeset viewer.