Changeset 2882


Ignore:
Timestamp:
Mar 15, 2013, 5:52:58 PM (4 years ago)
Author:
sacerdot
Message:

...

Location:
extracted
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • extracted/blocks.ml

    r2797 r2882  
    145145    Joint.params -> AST.ident List.list -> Joint.joint_seq List.list ->
    146146    step_block **)
    147 let ensure_step_block p g l =
    148   match split_on_last l with
    149   | Types.None ->
    150     { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
    151       Joint.Step_seq
    152       (Joint.nOOP (Joint.stmt_pars__o__uns_pars__o__u_pars p) g)) };
    153       Types.snd = List.Nil }
    154   | Types.Some pr ->
    155     { Types.fst = { Types.fst = (add_dummy_variance pr.Types.fst);
    156       Types.snd = (fun x -> Joint.Step_seq pr.Types.snd) }; Types.snd =
    157       List.Nil }
     147let ensure_step_block p g = function
     148| List.Nil ->
     149  { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x -> Joint.Step_seq
     150    (Joint.nOOP (Joint.stmt_pars__o__uns_pars__o__u_pars p) g)) };
     151    Types.snd = List.Nil }
     152| List.Cons (hd, tl) ->
     153  { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x -> Joint.Step_seq
     154    hd) }; Types.snd = tl }
    158155
    159156(** val map_eval : ('a1 -> 'a2) List.list -> 'a1 -> 'a2 List.list **)
  • extracted/joint_semantics.ml

    r2873 r2882  
    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_25710 =
     143let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_3 =
    144144  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    145     get_pc_from_label0 } = x_25710
     145    get_pc_from_label0 } = x_3
    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_25712 =
     153let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_5 =
    154154  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    155     get_pc_from_label0 } = x_25712
     155    get_pc_from_label0 } = x_5
    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_25714 =
     163let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_7 =
    164164  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    165     get_pc_from_label0 } = x_25714
     165    get_pc_from_label0 } = x_7
    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_25716 =
     173let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_9 =
    174174  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    175     get_pc_from_label0 } = x_25716
     175    get_pc_from_label0 } = x_9
    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_25718 =
     183let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_11 =
    184184  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    185     get_pc_from_label0 } = x_25718
     185    get_pc_from_label0 } = x_11
    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_25720 =
     193let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_13 =
    194194  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    195     get_pc_from_label0 } = x_25720
     195    get_pc_from_label0 } = x_13
    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_25740 =
     343let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_33 =
    344344  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    345     load_sp0; save_sp = save_sp0 } = x_25740
     345    load_sp0; save_sp = save_sp0 } = x_33
    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_25742 =
     353let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_35 =
    354354  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    355     load_sp0; save_sp = save_sp0 } = x_25742
     355    load_sp0; save_sp = save_sp0 } = x_35
    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_25744 =
     363let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_37 =
    364364  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    365     load_sp0; save_sp = save_sp0 } = x_25744
     365    load_sp0; save_sp = save_sp0 } = x_37
    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_25746 =
     373let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_39 =
    374374  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    375     load_sp0; save_sp = save_sp0 } = x_25746
     375    load_sp0; save_sp = save_sp0 } = x_39
    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_25748 =
     383let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_41 =
    384384  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    385     load_sp0; save_sp = save_sp0 } = x_25748
     385    load_sp0; save_sp = save_sp0 } = x_41
    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_25750 =
     393let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_43 =
    394394  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    395     load_sp0; save_sp = save_sp0 } = x_25750
     395    load_sp0; save_sp = save_sp0 } = x_43
    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_25776 -> h_one_is x_25776
    475 | Both_is (x_25778, x_25777) -> h_both_is x_25778 x_25777
     474| One_is x_69 -> h_one_is x_69
     475| Both_is (x_71, x_70) -> h_both_is x_71 x_70
    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_25783 -> h_one_is x_25783
    483 | Both_is (x_25785, x_25784) -> h_both_is x_25785 x_25784
     482| One_is x_76 -> h_one_is x_76
     483| Both_is (x_78, x_77) -> h_both_is x_78 x_77
    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_25790 -> h_one_is x_25790
    491 | Both_is (x_25792, x_25791) -> h_both_is x_25792 x_25791
     490| One_is x_83 -> h_one_is x_83
     491| Both_is (x_85, x_84) -> h_both_is x_85 x_84
    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_25797 -> h_one_is x_25797
    499 | Both_is (x_25799, x_25798) -> h_both_is x_25799 x_25798
     498| One_is x_90 -> h_one_is x_90
     499| Both_is (x_92, x_91) -> h_both_is x_92 x_91
    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_25804 -> h_one_is x_25804
    507 | Both_is (x_25806, x_25805) -> h_both_is x_25806 x_25805
     506| One_is x_97 -> h_one_is x_97
     507| Both_is (x_99, x_98) -> h_both_is x_99 x_98
    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_25811 -> h_one_is x_25811
    515 | Both_is (x_25813, x_25812) -> h_both_is x_25813 x_25812
     514| One_is x_104 -> h_one_is x_104
     515| Both_is (x_106, x_105) -> h_both_is x_106 x_105
    516516
    517517(** val internal_stack_inv_rect_Type4 :
     
    596596    sem_state_params -> (__ Types.option -> internal_stack ->
    597597    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    598 let rec state_rect_Type4 semp h_mk_state x_25861 =
     598let rec state_rect_Type4 semp h_mk_state x_154 =
    599599  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    600     m = m0 } = x_25861
     600    m = m0 } = x_154
    601601  in
    602602  h_mk_state st_frms0 istack0 carry0 regs0 m0
     
    605605    sem_state_params -> (__ Types.option -> internal_stack ->
    606606    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    607 let rec state_rect_Type5 semp h_mk_state x_25863 =
     607let rec state_rect_Type5 semp h_mk_state x_156 =
    608608  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    609     m = m0 } = x_25863
     609    m = m0 } = x_156
    610610  in
    611611  h_mk_state st_frms0 istack0 carry0 regs0 m0
     
    614614    sem_state_params -> (__ Types.option -> internal_stack ->
    615615    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    616 let rec state_rect_Type3 semp h_mk_state x_25865 =
     616let rec state_rect_Type3 semp h_mk_state x_158 =
    617617  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    618     m = m0 } = x_25865
     618    m = m0 } = x_158
    619619  in
    620620  h_mk_state st_frms0 istack0 carry0 regs0 m0
     
    623623    sem_state_params -> (__ Types.option -> internal_stack ->
    624624    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    625 let rec state_rect_Type2 semp h_mk_state x_25867 =
     625let rec state_rect_Type2 semp h_mk_state x_160 =
    626626  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    627     m = m0 } = x_25867
     627    m = m0 } = x_160
    628628  in
    629629  h_mk_state st_frms0 istack0 carry0 regs0 m0
     
    632632    sem_state_params -> (__ Types.option -> internal_stack ->
    633633    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    634 let rec state_rect_Type1 semp h_mk_state x_25869 =
     634let rec state_rect_Type1 semp h_mk_state x_162 =
    635635  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    636     m = m0 } = x_25869
     636    m = m0 } = x_162
    637637  in
    638638  h_mk_state st_frms0 istack0 carry0 regs0 m0
     
    641641    sem_state_params -> (__ Types.option -> internal_stack ->
    642642    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    643 let rec state_rect_Type0 semp h_mk_state x_25871 =
     643let rec state_rect_Type0 semp h_mk_state x_164 =
    644644  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    645     m = m0 } = x_25871
     645    m = m0 } = x_164
    646646  in
    647647  h_mk_state st_frms0 istack0 carry0 regs0 m0
     
    719719    sem_state_params -> (state -> ByteValues.program_counter ->
    720720    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    721 let rec state_pc_rect_Type4 semp h_mk_state_pc x_25887 =
    722   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25887 in
     721let rec state_pc_rect_Type4 semp h_mk_state_pc x_180 =
     722  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_180 in
    723723  h_mk_state_pc st_no_pc0 pc0 last_pop0
    724724
     
    726726    sem_state_params -> (state -> ByteValues.program_counter ->
    727727    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    728 let rec state_pc_rect_Type5 semp h_mk_state_pc x_25889 =
    729   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25889 in
     728let rec state_pc_rect_Type5 semp h_mk_state_pc x_182 =
     729  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_182 in
    730730  h_mk_state_pc st_no_pc0 pc0 last_pop0
    731731
     
    733733    sem_state_params -> (state -> ByteValues.program_counter ->
    734734    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    735 let rec state_pc_rect_Type3 semp h_mk_state_pc x_25891 =
    736   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25891 in
     735let rec state_pc_rect_Type3 semp h_mk_state_pc x_184 =
     736  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_184 in
    737737  h_mk_state_pc st_no_pc0 pc0 last_pop0
    738738
     
    740740    sem_state_params -> (state -> ByteValues.program_counter ->
    741741    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    742 let rec state_pc_rect_Type2 semp h_mk_state_pc x_25893 =
    743   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25893 in
     742let rec state_pc_rect_Type2 semp h_mk_state_pc x_186 =
     743  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_186 in
    744744  h_mk_state_pc st_no_pc0 pc0 last_pop0
    745745
     
    747747    sem_state_params -> (state -> ByteValues.program_counter ->
    748748    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    749 let rec state_pc_rect_Type1 semp h_mk_state_pc x_25895 =
    750   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25895 in
     749let rec state_pc_rect_Type1 semp h_mk_state_pc x_188 =
     750  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_188 in
    751751  h_mk_state_pc st_no_pc0 pc0 last_pop0
    752752
     
    754754    sem_state_params -> (state -> ByteValues.program_counter ->
    755755    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    756 let rec state_pc_rect_Type0 semp h_mk_state_pc x_25897 =
    757   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25897 in
     756let rec state_pc_rect_Type0 semp h_mk_state_pc x_190 =
     757  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_190 in
    758758  h_mk_state_pc st_no_pc0 pc0 last_pop0
    759759
     
    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_25952 =
     1096let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_245 =
    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_25952
     1108    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_245
    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_25954 =
     1137let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_247 =
    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_25954
     1149    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_247
    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_25956 =
     1178let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_249 =
    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_25956
     1190    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_249
    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_25958 =
     1219let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_251 =
    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_25958
     1231    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_251
    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_25960 =
     1260let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_253 =
    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_25960
     1272    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_253
    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_25962 =
     1301let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_255 =
    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_25962
     1313    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_255
    13141314  in
    13151315  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    17461746        Monad.m_bind0 (Monad.max_def Errors.res0)
    17471747          (Obj.magic
    1748             (ByteValues.pc_of_bevals (List.Cons (addrh, (List.Cons (addrl,
     1748            (ByteValues.pc_of_bevals (List.Cons (addrl, (List.Cons (addrh,
    17491749              List.Nil)))))) (fun pr ->
    17501750          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st'';
     
    17611761    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17621762    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1763 let rec sem_params_rect_Type4 h_mk_sem_params x_26032 =
     1763let rec sem_params_rect_Type4 h_mk_sem_params x_325 =
    17641764  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1765     point_of_offset = point_of_offset0 } = x_26032
     1765    point_of_offset = point_of_offset0 } = x_325
    17661766  in
    17671767  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
     
    17711771    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17721772    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1773 let rec sem_params_rect_Type5 h_mk_sem_params x_26034 =
     1773let rec sem_params_rect_Type5 h_mk_sem_params x_327 =
    17741774  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1775     point_of_offset = point_of_offset0 } = x_26034
     1775    point_of_offset = point_of_offset0 } = x_327
    17761776  in
    17771777  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
     
    17811781    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17821782    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1783 let rec sem_params_rect_Type3 h_mk_sem_params x_26036 =
     1783let rec sem_params_rect_Type3 h_mk_sem_params x_329 =
    17841784  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1785     point_of_offset = point_of_offset0 } = x_26036
     1785    point_of_offset = point_of_offset0 } = x_329
    17861786  in
    17871787  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
     
    17911791    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17921792    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1793 let rec sem_params_rect_Type2 h_mk_sem_params x_26038 =
     1793let rec sem_params_rect_Type2 h_mk_sem_params x_331 =
    17941794  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1795     point_of_offset = point_of_offset0 } = x_26038
     1795    point_of_offset = point_of_offset0 } = x_331
    17961796  in
    17971797  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
     
    18011801    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    18021802    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1803 let rec sem_params_rect_Type1 h_mk_sem_params x_26040 =
     1803let rec sem_params_rect_Type1 h_mk_sem_params x_333 =
    18041804  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1805     point_of_offset = point_of_offset0 } = x_26040
     1805    point_of_offset = point_of_offset0 } = x_333
    18061806  in
    18071807  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
     
    18111811    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    18121812    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1813 let rec sem_params_rect_Type0 h_mk_sem_params x_26042 =
     1813let rec sem_params_rect_Type0 h_mk_sem_params x_335 =
    18141814  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1815     point_of_offset = point_of_offset0 } = x_26042
     1815    point_of_offset = point_of_offset0 } = x_335
    18161816  in
    18171817  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
  • extracted/rTLToERTL.ml

    r2867 r2882  
    246246          Types.snd = pr.Types.snd }) sregs))
    247247      (List.append (List.Cons ((Joint.PUSH
    248         (Obj.magic (Joint.psd_argument_from_reg srah))), (List.Cons
    249         ((Joint.PUSH (Obj.magic (Joint.psd_argument_from_reg sral))),
     248        (Obj.magic (Joint.psd_argument_from_reg sral))), (List.Cons
     249        ((Joint.PUSH (Obj.magic (Joint.psd_argument_from_reg srah))),
    250250        (List.Cons
    251251        ((ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_del_frame)),
     
    263263      ((let x = ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_new_frame)
    264264        in
    265        x), (List.Cons ((Joint.POP (Obj.magic sral)), (List.Cons ((Joint.POP
    266       (Obj.magic srah)), List.Nil))))))
     265       x), (List.Cons ((Joint.POP (Obj.magic srah)), (List.Cons ((Joint.POP
     266      (Obj.magic sral)), List.Nil))))))
    267267      (List.append (save_hdws globals sregs)
    268268        (get_params globals tmpr addr1 addr2 params))
  • extracted/toCminor.ml

    r2827 r2882  
    198198    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    199199let rec var_type_rect_Type4 h_Global h_Stack h_Local = function
    200 | Global x_13042 -> h_Global x_13042
    201 | Stack x_13043 -> h_Stack x_13043
     200| Global x_634 -> h_Global x_634
     201| Stack x_635 -> h_Stack x_635
    202202| Local -> h_Local
    203203
     
    205205    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    206206let rec var_type_rect_Type5 h_Global h_Stack h_Local = function
    207 | Global x_13048 -> h_Global x_13048
    208 | Stack x_13049 -> h_Stack x_13049
     207| Global x_640 -> h_Global x_640
     208| Stack x_641 -> h_Stack x_641
    209209| Local -> h_Local
    210210
     
    212212    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    213213let rec var_type_rect_Type3 h_Global h_Stack h_Local = function
    214 | Global x_13054 -> h_Global x_13054
    215 | Stack x_13055 -> h_Stack x_13055
     214| Global x_646 -> h_Global x_646
     215| Stack x_647 -> h_Stack x_647
    216216| Local -> h_Local
    217217
     
    219219    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    220220let rec var_type_rect_Type2 h_Global h_Stack h_Local = function
    221 | Global x_13060 -> h_Global x_13060
    222 | Stack x_13061 -> h_Stack x_13061
     221| Global x_652 -> h_Global x_652
     222| Stack x_653 -> h_Stack x_653
    223223| Local -> h_Local
    224224
     
    226226    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    227227let rec var_type_rect_Type1 h_Global h_Stack h_Local = function
    228 | Global x_13066 -> h_Global x_13066
    229 | Stack x_13067 -> h_Stack x_13067
     228| Global x_658 -> h_Global x_658
     229| Stack x_659 -> h_Stack x_659
    230230| Local -> h_Local
    231231
     
    233233    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    234234let rec var_type_rect_Type0 h_Global h_Stack h_Local = function
    235 | Global x_13072 -> h_Global x_13072
    236 | Stack x_13073 -> h_Stack x_13073
     235| Global x_664 -> h_Global x_664
     236| Stack x_665 -> h_Stack x_665
    237237| Local -> h_Local
    238238
     
    12211221let rec destination_rect_Type4 vars h_IdDest h_MemDest = function
    12221222| IdDest (id, ty) -> h_IdDest id ty __
    1223 | MemDest x_14528 -> h_MemDest x_14528
     1223| MemDest x_712 -> h_MemDest x_712
    12241224
    12251225(** val destination_rect_Type5 :
     
    12281228let rec destination_rect_Type5 vars h_IdDest h_MemDest = function
    12291229| IdDest (id, ty) -> h_IdDest id ty __
    1230 | MemDest x_14533 -> h_MemDest x_14533
     1230| MemDest x_717 -> h_MemDest x_717
    12311231
    12321232(** val destination_rect_Type3 :
     
    12351235let rec destination_rect_Type3 vars h_IdDest h_MemDest = function
    12361236| IdDest (id, ty) -> h_IdDest id ty __
    1237 | MemDest x_14538 -> h_MemDest x_14538
     1237| MemDest x_722 -> h_MemDest x_722
    12381238
    12391239(** val destination_rect_Type2 :
     
    12421242let rec destination_rect_Type2 vars h_IdDest h_MemDest = function
    12431243| IdDest (id, ty) -> h_IdDest id ty __
    1244 | MemDest x_14543 -> h_MemDest x_14543
     1244| MemDest x_727 -> h_MemDest x_727
    12451245
    12461246(** val destination_rect_Type1 :
     
    12491249let rec destination_rect_Type1 vars h_IdDest h_MemDest = function
    12501250| IdDest (id, ty) -> h_IdDest id ty __
    1251 | MemDest x_14548 -> h_MemDest x_14548
     1251| MemDest x_732 -> h_MemDest x_732
    12521252
    12531253(** val destination_rect_Type0 :
     
    12561256let rec destination_rect_Type0 vars h_IdDest h_MemDest = function
    12571257| IdDest (id, ty) -> h_IdDest id ty __
    1258 | MemDest x_14553 -> h_MemDest x_14553
     1258| MemDest x_737 -> h_MemDest x_737
    12591259
    12601260(** val destination_inv_rect_Type4 :
     
    13821382    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13831383    'a1) -> labgen -> 'a1 **)
    1384 let rec labgen_rect_Type4 h_mk_labgen x_14588 =
    1385   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1386     x_14588
     1384let rec labgen_rect_Type4 h_mk_labgen x_772 =
     1385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_772
    13871386  in
    13881387  h_mk_labgen labuniverse0 label_genlist0 __
     
    13911390    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13921391    'a1) -> labgen -> 'a1 **)
    1393 let rec labgen_rect_Type5 h_mk_labgen x_14590 =
    1394   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1395     x_14590
     1392let rec labgen_rect_Type5 h_mk_labgen x_774 =
     1393  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_774
    13961394  in
    13971395  h_mk_labgen labuniverse0 label_genlist0 __
     
    14001398    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14011399    'a1) -> labgen -> 'a1 **)
    1402 let rec labgen_rect_Type3 h_mk_labgen x_14592 =
    1403   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1404     x_14592
     1400let rec labgen_rect_Type3 h_mk_labgen x_776 =
     1401  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_776
    14051402  in
    14061403  h_mk_labgen labuniverse0 label_genlist0 __
     
    14091406    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14101407    'a1) -> labgen -> 'a1 **)
    1411 let rec labgen_rect_Type2 h_mk_labgen x_14594 =
    1412   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1413     x_14594
     1408let rec labgen_rect_Type2 h_mk_labgen x_778 =
     1409  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_778
    14141410  in
    14151411  h_mk_labgen labuniverse0 label_genlist0 __
     
    14181414    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14191415    'a1) -> labgen -> 'a1 **)
    1420 let rec labgen_rect_Type1 h_mk_labgen x_14596 =
    1421   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1422     x_14596
     1416let rec labgen_rect_Type1 h_mk_labgen x_780 =
     1417  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_780
    14231418  in
    14241419  h_mk_labgen labuniverse0 label_genlist0 __
     
    14271422    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14281423    'a1) -> labgen -> 'a1 **)
    1429 let rec labgen_rect_Type0 h_mk_labgen x_14598 =
    1430   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1431     x_14598
     1424let rec labgen_rect_Type0 h_mk_labgen x_782 =
     1425  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_782
    14321426  in
    14331427  h_mk_labgen labuniverse0 label_genlist0 __
     
    15541548    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15551549    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14614 =
    1557   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14614 in
     1550let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_798 =
     1551  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_798 in
    15581552  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15591553
     
    15611555    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15621556    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14616 =
    1564   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14616 in
     1557let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_800 =
     1558  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_800 in
    15651559  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15661560
     
    15681562    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15691563    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14618 =
    1571   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14618 in
     1564let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_802 =
     1565  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_802 in
    15721566  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15731567
     
    15751569    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15761570    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14620 =
    1578   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14620 in
     1571let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_804 =
     1572  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_804 in
    15791573  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15801574
     
    15821576    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15831577    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14622 =
    1585   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14622 in
     1578let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_806 =
     1579  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_806 in
    15861580  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15871581
     
    15891583    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15901584    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14624 =
    1592   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14624 in
     1585let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_808 =
     1586  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_808 in
    15931587  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15941588
     
    16741668let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
    16751669| DoNotConvert -> h_DoNotConvert
    1676 | ConvertTo (x_14646, x_14645) -> h_ConvertTo x_14646 x_14645
     1670| ConvertTo (x_830, x_829) -> h_ConvertTo x_830 x_829
    16771671
    16781672(** val convert_flag_rect_Type5 :
     
    16811675let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
    16821676| DoNotConvert -> h_DoNotConvert
    1683 | ConvertTo (x_14651, x_14650) -> h_ConvertTo x_14651 x_14650
     1677| ConvertTo (x_835, x_834) -> h_ConvertTo x_835 x_834
    16841678
    16851679(** val convert_flag_rect_Type3 :
     
    16881682let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
    16891683| DoNotConvert -> h_DoNotConvert
    1690 | ConvertTo (x_14656, x_14655) -> h_ConvertTo x_14656 x_14655
     1684| ConvertTo (x_840, x_839) -> h_ConvertTo x_840 x_839
    16911685
    16921686(** val convert_flag_rect_Type2 :
     
    16951689let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
    16961690| DoNotConvert -> h_DoNotConvert
    1697 | ConvertTo (x_14661, x_14660) -> h_ConvertTo x_14661 x_14660
     1691| ConvertTo (x_845, x_844) -> h_ConvertTo x_845 x_844
    16981692
    16991693(** val convert_flag_rect_Type1 :
     
    17021696let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
    17031697| DoNotConvert -> h_DoNotConvert
    1704 | ConvertTo (x_14666, x_14665) -> h_ConvertTo x_14666 x_14665
     1698| ConvertTo (x_850, x_849) -> h_ConvertTo x_850 x_849
    17051699
    17061700(** val convert_flag_rect_Type0 :
     
    17091703let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
    17101704| DoNotConvert -> h_DoNotConvert
    1711 | ConvertTo (x_14671, x_14670) -> h_ConvertTo x_14671 x_14670
     1705| ConvertTo (x_855, x_854) -> h_ConvertTo x_855 x_854
    17121706
    17131707(** val convert_flag_inv_rect_Type4 :
     
    18321826                Obj.magic (Errors.OK { Types.fst = { Types.fst = uv2;
    18331827                  Types.snd = ul }; Types.snd = (Cminor_syntax.St_seq
    1834                   ((Cminor_syntax.St_store (AST.ASTptr, (Cminor_syntax.Id
    1835                   (AST.ASTptr, tmp2)), (Types.pi1 e1'))),
    1836                   (Cminor_syntax.St_seq ((Cminor_syntax.St_call ((Types.Some
    1837                   { Types.fst = tmp; Types.snd =
    1838                   (Csyntax.typ_of_type (Csyntax.typeof e1)) }),
     1828                  ((Cminor_syntax.St_assign (AST.ASTptr, tmp2,
     1829                  (Types.pi1 e1'))), (Cminor_syntax.St_seq
     1830                  ((Cminor_syntax.St_call ((Types.Some { Types.fst = tmp;
     1831                  Types.snd = (Csyntax.typ_of_type (Csyntax.typeof e1)) }),
    18391832                  (Types.pi1 ef'0), (Types.pi1 args'))),
    18401833                  (Cminor_syntax.St_store
    18411834                  ((Csyntax.typ_of_type (Csyntax.typeof e1)),
    1842                   (Types.pi1 e1'), (Cminor_syntax.Id
     1835                  (Cminor_syntax.Id (AST.ASTptr, tmp2)), (Cminor_syntax.Id
    18431836                  ((Csyntax.typ_of_type (Csyntax.typeof e1)), tmp)))))))) })))
    18441837                  __)) __)))))
     
    20442037    Obj.magic
    20452038      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2046         (fun eta2436 ->
    2047         let result = eta2436 in
     2039        (fun eta244 ->
     2040        let result = eta244 in
    20482041        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20492042        (fun _ ->
Note: See TracChangeset for help on using the changeset viewer.