Ignore:
Timestamp:
Mar 26, 2013, 4:51:40 PM (7 years ago)
Author:
sacerdot
Message:

New extraction, it diverges in RTL execution now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_semantics.ml

    r2951 r2960  
    133133type 'f genv_gen = { ge : 'f AST.fundef Globalenvs.genv_t;
    134134                     stack_sizes : (AST.ident -> Nat.nat Types.option);
    135                      get_pc_from_label : (AST.ident -> Graphs.label ->
    136                                          ByteValues.program_counter
    137                                          Errors.res) }
     135                     premain : 'f;
     136                     pc_from_label : (Pointers.block Types.sig0 -> 'f ->
     137                                     Graphs.label ->
     138                                     ByteValues.program_counter Types.option) }
    138139
    139140(** val genv_gen_rect_Type4 :
    140141    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    141     (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    142     ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    143 let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_5376 =
    144   let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    145     get_pc_from_label0 } = x_5376
    146   in
    147   h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     142    (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
     143    -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
     144    'a2) -> 'a1 genv_gen -> 'a2 **)
     145let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_55 =
     146  let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
     147    pc_from_label = pc_from_label0 } = x_55
     148  in
     149  h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
    148150
    149151(** val genv_gen_rect_Type5 :
    150152    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    151     (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    152     ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    153 let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_5378 =
    154   let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    155     get_pc_from_label0 } = x_5378
    156   in
    157   h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     153    (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
     154    -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
     155    'a2) -> 'a1 genv_gen -> 'a2 **)
     156let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_57 =
     157  let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
     158    pc_from_label = pc_from_label0 } = x_57
     159  in
     160  h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
    158161
    159162(** val genv_gen_rect_Type3 :
    160163    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    161     (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    162     ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    163 let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_5380 =
    164   let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    165     get_pc_from_label0 } = x_5380
    166   in
    167   h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     164    (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
     165    -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
     166    'a2) -> 'a1 genv_gen -> 'a2 **)
     167let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_59 =
     168  let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
     169    pc_from_label = pc_from_label0 } = x_59
     170  in
     171  h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
    168172
    169173(** val genv_gen_rect_Type2 :
    170174    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    171     (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    172     ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    173 let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_5382 =
    174   let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    175     get_pc_from_label0 } = x_5382
    176   in
    177   h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     175    (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
     176    -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
     177    'a2) -> 'a1 genv_gen -> 'a2 **)
     178let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_61 =
     179  let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
     180    pc_from_label = pc_from_label0 } = x_61
     181  in
     182  h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
    178183
    179184(** val genv_gen_rect_Type1 :
    180185    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    181     (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    182     ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    183 let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_5384 =
    184   let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    185     get_pc_from_label0 } = x_5384
    186   in
    187   h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     186    (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
     187    -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
     188    'a2) -> 'a1 genv_gen -> 'a2 **)
     189let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_63 =
     190  let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
     191    pc_from_label = pc_from_label0 } = x_63
     192  in
     193  h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
    188194
    189195(** val genv_gen_rect_Type0 :
    190196    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    191     (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    192     ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    193 let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_5386 =
    194   let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    195     get_pc_from_label0 } = x_5386
    196   in
    197   h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     197    (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
     198    -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
     199    'a2) -> 'a1 genv_gen -> 'a2 **)
     200let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_65 =
     201  let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
     202    pc_from_label = pc_from_label0 } = x_65
     203  in
     204  h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
    198205
    199206(** val ge :
     
    207214  xxx.stack_sizes
    208215
    209 (** val get_pc_from_label :
    210     AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
    211     ByteValues.program_counter Errors.res **)
    212 let rec get_pc_from_label globals xxx =
    213   xxx.get_pc_from_label
     216(** val premain : AST.ident List.list -> 'a1 genv_gen -> 'a1 **)
     217let rec premain globals xxx =
     218  xxx.premain
     219
     220(** val pc_from_label :
     221    AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 -> 'a1
     222    -> Graphs.label -> ByteValues.program_counter Types.option **)
     223let rec pc_from_label globals xxx =
     224  xxx.pc_from_label
    214225
    215226(** val genv_gen_inv_rect_Type4 :
    216227    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
    217     -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
    218     Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
    219     'a2 **)
     228    -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     229    Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     230    Types.option) -> __ -> 'a2) -> 'a2 **)
    220231let genv_gen_inv_rect_Type4 x2 hterm h1 =
    221232  let hcut = genv_gen_rect_Type4 x2 h1 hterm in hcut __
     
    223234(** val genv_gen_inv_rect_Type3 :
    224235    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
    225     -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
    226     Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
    227     'a2 **)
     236    -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     237    Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     238    Types.option) -> __ -> 'a2) -> 'a2 **)
    228239let genv_gen_inv_rect_Type3 x2 hterm h1 =
    229240  let hcut = genv_gen_rect_Type3 x2 h1 hterm in hcut __
     
    231242(** val genv_gen_inv_rect_Type2 :
    232243    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
    233     -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
    234     Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
    235     'a2 **)
     244    -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     245    Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     246    Types.option) -> __ -> 'a2) -> 'a2 **)
    236247let genv_gen_inv_rect_Type2 x2 hterm h1 =
    237248  let hcut = genv_gen_rect_Type2 x2 h1 hterm in hcut __
     
    239250(** val genv_gen_inv_rect_Type1 :
    240251    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
    241     -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
    242     Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
    243     'a2 **)
     252    -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     253    Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     254    Types.option) -> __ -> 'a2) -> 'a2 **)
    244255let genv_gen_inv_rect_Type1 x2 hterm h1 =
    245256  let hcut = genv_gen_rect_Type1 x2 h1 hterm in hcut __
     
    247258(** val genv_gen_inv_rect_Type0 :
    248259    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
    249     -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
    250     Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
    251     'a2 **)
     260    -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     261    Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     262    Types.option) -> __ -> 'a2) -> 'a2 **)
    252263let genv_gen_inv_rect_Type0 x2 hterm h1 =
    253264  let hcut = genv_gen_rect_Type0 x2 h1 hterm in hcut __
     
    257268let genv_gen_discr a2 x y =
    258269  Logic.eq_rect_Type2 x
    259     (let { ge = a0; stack_sizes = a20; get_pc_from_label = a3 } = x in
    260     Obj.magic (fun _ dH -> dH __ __ __ __)) y
     270    (let { ge = a0; stack_sizes = a20; premain = a3; pc_from_label = a4 } = x
     271     in
     272    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
    261273
    262274(** val genv_gen_jmdiscr :
     
    264276let genv_gen_jmdiscr a2 x y =
    265277  Logic.eq_rect_Type2 x
    266     (let { ge = a0; stack_sizes = a20; get_pc_from_label = a3 } = x in
    267     Obj.magic (fun _ dH -> dH __ __ __ __)) y
     278    (let { ge = a0; stack_sizes = a20; premain = a3; pc_from_label = a4 } = x
     279     in
     280    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
    268281
    269282(** val dpi1__o__ge__o__inject :
     
    296309let eject__o__ge x1 x3 =
    297310  (Types.pi1 x3).ge
     311
     312(** val pre_main_id : AST.ident **)
     313let pre_main_id =
     314  Positive.One
     315
     316(** val fetch_function :
     317    AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
     318    (AST.ident, 'a1 AST.fundef) Types.prod Errors.res **)
     319let fetch_function g ge0 bl =
     320  match Z.eqZb (Pointers.block_id (Types.pi1 bl))
     321          (Z.zopp (Z.z_of_nat (Nat.S Nat.O))) with
     322  | Bool.True ->
     323    Obj.magic
     324      (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = pre_main_id;
     325        Types.snd = (AST.Internal ge0.premain) })
     326  | Bool.False ->
     327    Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
     328      List.Nil))
     329      (Obj.magic
     330        (Monad.m_bind0 (Monad.max_def Option.option)
     331          (Obj.magic (Globalenvs.symbol_for_block ge0.ge (Types.pi1 bl)))
     332          (fun id ->
     333          Monad.m_bind0 (Monad.max_def Option.option)
     334            (Obj.magic (Globalenvs.find_funct_ptr ge0.ge (Types.pi1 bl)))
     335            (fun fd ->
     336            Monad.m_return0 (Monad.max_def Option.option) { Types.fst = id;
     337              Types.snd = fd }))))
     338
     339(** val fetch_internal_function :
     340    AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
     341    (AST.ident, 'a1) Types.prod Errors.res **)
     342let fetch_internal_function g ge0 bl =
     343  Obj.magic
     344    (Monad.m_bind2 (Monad.max_def Errors.res0)
     345      (Obj.magic (fetch_function g ge0 bl)) (fun id fd ->
     346      match fd with
     347      | AST.Internal ifd ->
     348        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = id;
     349          Types.snd = ifd }
     350      | AST.External x ->
     351        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
     352          ErrorMessages.BadFunction), List.Nil)))))
     353
     354(** val code_block_of_block :
     355    Pointers.block -> Pointers.block Types.sig0 Types.option **)
     356let code_block_of_block bl =
     357  (match Pointers.block_region bl with
     358   | AST.XData -> (fun _ -> Types.None)
     359   | AST.Code -> (fun _ -> Types.Some bl)) __
     360
     361(** val block_of_funct_id :
     362    'a1 Globalenvs.genv_t -> PreIdentifiers.identifier -> Pointers.block
     363    Types.sig0 Errors.res **)
     364let block_of_funct_id ge0 id =
     365  Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
     366    (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
     367    (Obj.magic
     368      (Monad.m_bind0 (Monad.max_def Option.option)
     369        (Obj.magic (Globalenvs.find_symbol ge0 id)) (fun bl ->
     370        Obj.magic (code_block_of_block bl))))
     371
     372(** val gen_pc_from_label :
     373    AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
     374    ByteValues.program_counter Errors.res **)
     375let gen_pc_from_label g ge0 id lbl =
     376  Obj.magic
     377    (Monad.m_bind0 (Monad.max_def Errors.res0)
     378      (Obj.magic (block_of_funct_id ge0.ge id)) (fun bl ->
     379      Monad.m_bind2 (Monad.max_def Errors.res0)
     380        (Obj.magic (fetch_internal_function g ge0 bl)) (fun ignore f_def ->
     381        Obj.magic
     382          (Errors.opt_to_res (List.Cons ((Errors.MSG
     383            ErrorMessages.LabelNotFound), (List.Cons ((Errors.CTX
     384            (PreIdentifiers.LabelTag, lbl)), List.Nil))))
     385            (ge0.pc_from_label bl f_def lbl)))))
    298386
    299387type genv = Joint.joint_closed_internal_function genv_gen
     
    341429    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    342430    'a1) -> sem_state_params -> 'a1 **)
    343 let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_5406 =
     431let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_86 =
    344432  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    345     load_sp0; save_sp = save_sp0 } = x_5406
     433    load_sp0; save_sp = save_sp0 } = x_86
    346434  in
    347435  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    351439    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    352440    'a1) -> sem_state_params -> 'a1 **)
    353 let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_5408 =
     441let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_88 =
    354442  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    355     load_sp0; save_sp = save_sp0 } = x_5408
     443    load_sp0; save_sp = save_sp0 } = x_88
    356444  in
    357445  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    361449    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    362450    'a1) -> sem_state_params -> 'a1 **)
    363 let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_5410 =
     451let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_90 =
    364452  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    365     load_sp0; save_sp = save_sp0 } = x_5410
     453    load_sp0; save_sp = save_sp0 } = x_90
    366454  in
    367455  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    371459    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    372460    'a1) -> sem_state_params -> 'a1 **)
    373 let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_5412 =
     461let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_92 =
    374462  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    375     load_sp0; save_sp = save_sp0 } = x_5412
     463    load_sp0; save_sp = save_sp0 } = x_92
    376464  in
    377465  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    381469    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    382470    'a1) -> sem_state_params -> 'a1 **)
    383 let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_5414 =
     471let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_94 =
    384472  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    385     load_sp0; save_sp = save_sp0 } = x_5414
     473    load_sp0; save_sp = save_sp0 } = x_94
    386474  in
    387475  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    391479    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    392480    'a1) -> sem_state_params -> 'a1 **)
    393 let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_5416 =
     481let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_96 =
    394482  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    395     load_sp0; save_sp = save_sp0 } = x_5416
     483    load_sp0; save_sp = save_sp0 } = x_96
    396484  in
    397485  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    472560let rec internal_stack_rect_Type4 h_empty_is h_one_is h_both_is = function
    473561| Empty_is -> h_empty_is
    474 | One_is x_5442 -> h_one_is x_5442
    475 | Both_is (x_5444, x_5443) -> h_both_is x_5444 x_5443
     562| One_is x_122 -> h_one_is x_122
     563| Both_is (x_124, x_123) -> h_both_is x_124 x_123
    476564
    477565(** val internal_stack_rect_Type5 :
     
    480568let rec internal_stack_rect_Type5 h_empty_is h_one_is h_both_is = function
    481569| Empty_is -> h_empty_is
    482 | One_is x_5449 -> h_one_is x_5449
    483 | Both_is (x_5451, x_5450) -> h_both_is x_5451 x_5450
     570| One_is x_129 -> h_one_is x_129
     571| Both_is (x_131, x_130) -> h_both_is x_131 x_130
    484572
    485573(** val internal_stack_rect_Type3 :
     
    488576let rec internal_stack_rect_Type3 h_empty_is h_one_is h_both_is = function
    489577| Empty_is -> h_empty_is
    490 | One_is x_5456 -> h_one_is x_5456
    491 | Both_is (x_5458, x_5457) -> h_both_is x_5458 x_5457
     578| One_is x_136 -> h_one_is x_136
     579| Both_is (x_138, x_137) -> h_both_is x_138 x_137
    492580
    493581(** val internal_stack_rect_Type2 :
     
    496584let rec internal_stack_rect_Type2 h_empty_is h_one_is h_both_is = function
    497585| Empty_is -> h_empty_is
    498 | One_is x_5463 -> h_one_is x_5463
    499 | Both_is (x_5465, x_5464) -> h_both_is x_5465 x_5464
     586| One_is x_143 -> h_one_is x_143
     587| Both_is (x_145, x_144) -> h_both_is x_145 x_144
    500588
    501589(** val internal_stack_rect_Type1 :
     
    504592let rec internal_stack_rect_Type1 h_empty_is h_one_is h_both_is = function
    505593| Empty_is -> h_empty_is
    506 | One_is x_5470 -> h_one_is x_5470
    507 | Both_is (x_5472, x_5471) -> h_both_is x_5472 x_5471
     594| One_is x_150 -> h_one_is x_150
     595| Both_is (x_152, x_151) -> h_both_is x_152 x_151
    508596
    509597(** val internal_stack_rect_Type0 :
     
    512600let rec internal_stack_rect_Type0 h_empty_is h_one_is h_both_is = function
    513601| Empty_is -> h_empty_is
    514 | One_is x_5477 -> h_one_is x_5477
    515 | Both_is (x_5479, x_5478) -> h_both_is x_5479 x_5478
     602| One_is x_157 -> h_one_is x_157
     603| Both_is (x_159, x_158) -> h_both_is x_159 x_158
    516604
    517605(** val internal_stack_inv_rect_Type4 :
     
    597685    sem_state_params -> (__ Types.option -> internal_stack ->
    598686    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
    599 let rec state_rect_Type4 semp h_mk_state x_5527 =
     687let rec state_rect_Type4 semp h_mk_state x_207 =
    600688  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    601     m = m0; stack_usage = stack_usage0 } = x_5527
     689    m = m0; stack_usage = stack_usage0 } = x_207
    602690  in
    603691  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
     
    606694    sem_state_params -> (__ Types.option -> internal_stack ->
    607695    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
    608 let rec state_rect_Type5 semp h_mk_state x_5529 =
     696let rec state_rect_Type5 semp h_mk_state x_209 =
    609697  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    610     m = m0; stack_usage = stack_usage0 } = x_5529
     698    m = m0; stack_usage = stack_usage0 } = x_209
    611699  in
    612700  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
     
    615703    sem_state_params -> (__ Types.option -> internal_stack ->
    616704    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
    617 let rec state_rect_Type3 semp h_mk_state x_5531 =
     705let rec state_rect_Type3 semp h_mk_state x_211 =
    618706  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    619     m = m0; stack_usage = stack_usage0 } = x_5531
     707    m = m0; stack_usage = stack_usage0 } = x_211
    620708  in
    621709  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
     
    624712    sem_state_params -> (__ Types.option -> internal_stack ->
    625713    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
    626 let rec state_rect_Type2 semp h_mk_state x_5533 =
     714let rec state_rect_Type2 semp h_mk_state x_213 =
    627715  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    628     m = m0; stack_usage = stack_usage0 } = x_5533
     716    m = m0; stack_usage = stack_usage0 } = x_213
    629717  in
    630718  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
     
    633721    sem_state_params -> (__ Types.option -> internal_stack ->
    634722    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
    635 let rec state_rect_Type1 semp h_mk_state x_5535 =
     723let rec state_rect_Type1 semp h_mk_state x_215 =
    636724  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    637     m = m0; stack_usage = stack_usage0 } = x_5535
     725    m = m0; stack_usage = stack_usage0 } = x_215
    638726  in
    639727  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
     
    642730    sem_state_params -> (__ Types.option -> internal_stack ->
    643731    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
    644 let rec state_rect_Type0 semp h_mk_state x_5537 =
     732let rec state_rect_Type0 semp h_mk_state x_217 =
    645733  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    646     m = m0; stack_usage = stack_usage0 } = x_5537
     734    m = m0; stack_usage = stack_usage0 } = x_217
    647735  in
    648736  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
     
    720808    sem_state_params -> (state -> ByteValues.program_counter ->
    721809    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    722 let 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
     810let rec state_pc_rect_Type4 semp h_mk_state_pc x_233 =
     811  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_233 in
    724812  h_mk_state_pc st_no_pc0 pc0 last_pop0
    725813
     
    727815    sem_state_params -> (state -> ByteValues.program_counter ->
    728816    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    729 let 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
     817let rec state_pc_rect_Type5 semp h_mk_state_pc x_235 =
     818  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_235 in
    731819  h_mk_state_pc st_no_pc0 pc0 last_pop0
    732820
     
    734822    sem_state_params -> (state -> ByteValues.program_counter ->
    735823    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    736 let 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
     824let rec state_pc_rect_Type3 semp h_mk_state_pc x_237 =
     825  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_237 in
    738826  h_mk_state_pc st_no_pc0 pc0 last_pop0
    739827
     
    741829    sem_state_params -> (state -> ByteValues.program_counter ->
    742830    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    743 let 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
     831let rec state_pc_rect_Type2 semp h_mk_state_pc x_239 =
     832  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_239 in
    745833  h_mk_state_pc st_no_pc0 pc0 last_pop0
    746834
     
    748836    sem_state_params -> (state -> ByteValues.program_counter ->
    749837    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    750 let 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
     838let rec state_pc_rect_Type1 semp h_mk_state_pc x_241 =
     839  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_241 in
    752840  h_mk_state_pc st_no_pc0 pc0 last_pop0
    753841
     
    755843    sem_state_params -> (state -> ByteValues.program_counter ->
    756844    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    757 let 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
     845let rec state_pc_rect_Type0 semp h_mk_state_pc x_243 =
     846  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_243 in
    759847  h_mk_state_pc st_no_pc0 pc0 last_pop0
    760848
     
    895983  { st_frms = (Types.Some frms); istack = st.istack; carry = st.carry; regs =
    896984    st.regs; m = st.m; stack_usage = st.stack_usage }
    897 
    898 (** val fetch_function :
    899     'a1 Globalenvs.genv_t -> Pointers.block Types.sig0 -> (AST.ident, 'a1)
    900     Types.prod Errors.res **)
    901 let fetch_function ge0 bl =
    902   Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
    903     List.Nil))
    904     (Obj.magic
    905       (Monad.m_bind0 (Monad.max_def Option.option)
    906         (Obj.magic (Globalenvs.symbol_for_block ge0 (Types.pi1 bl)))
    907         (fun id ->
    908         Monad.m_bind0 (Monad.max_def Option.option)
    909           (Obj.magic (Globalenvs.find_funct_ptr ge0 (Types.pi1 bl)))
    910           (fun fd ->
    911           Monad.m_return0 (Monad.max_def Option.option) { Types.fst = id;
    912             Types.snd = fd }))))
    913 
    914 (** val fetch_internal_function :
    915     'a1 AST.fundef Globalenvs.genv_t -> Pointers.block Types.sig0 ->
    916     (AST.ident, 'a1) Types.prod Errors.res **)
    917 let fetch_internal_function ge0 bl =
    918   Obj.magic
    919     (Monad.m_bind2 (Monad.max_def Errors.res0)
    920       (Obj.magic (fetch_function ge0 bl)) (fun id fd ->
    921       match fd with
    922       | AST.Internal ifd ->
    923         Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = id;
    924           Types.snd = ifd }
    925       | AST.External x ->
    926         Obj.magic (Errors.Error (List.Cons ((Errors.MSG
    927           ErrorMessages.BadFunction), List.Nil)))))
    928985
    929986type call_kind =
     
    10941151    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    10951152    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1096 let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_5618 =
     1153let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_298 =
    10971154  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    10981155    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    11061163    set_result0; call_args_for_main = call_args_for_main0;
    11071164    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1108     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5618
     1165    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_298
    11091166  in
    11101167  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    11351192    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    11361193    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1137 let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_5620 =
     1194let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_300 =
    11381195  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    11391196    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    11471204    set_result0; call_args_for_main = call_args_for_main0;
    11481205    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1149     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5620
     1206    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_300
    11501207  in
    11511208  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    11761233    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    11771234    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1178 let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_5622 =
     1235let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_302 =
    11791236  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    11801237    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    11881245    set_result0; call_args_for_main = call_args_for_main0;
    11891246    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1190     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5622
     1247    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_302
    11911248  in
    11921249  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    12171274    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    12181275    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1219 let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_5624 =
     1276let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_304 =
    12201277  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    12211278    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    12291286    set_result0; call_args_for_main = call_args_for_main0;
    12301287    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1231     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5624
     1288    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_304
    12321289  in
    12331290  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    12581315    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    12591316    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1260 let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_5626 =
     1317let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_306 =
    12611318  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    12621319    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    12701327    set_result0; call_args_for_main = call_args_for_main0;
    12711328    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1272     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5626
     1329    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_306
    12731330  in
    12741331  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    12991356    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    13001357    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1301 let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_5628 =
     1358let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_308 =
    13021359  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    13031360    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    13111368    set_result0; call_args_for_main = call_args_for_main0;
    13121369    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1313     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5628
     1370    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_308
    13141371  in
    13151372  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    17611818    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17621819    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
    1763 let rec serialized_params_rect_Type4 h_mk_serialized_params x_5698 =
     1820let rec serialized_params_rect_Type4 h_mk_serialized_params x_378 =
    17641821  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1765     point_of_offset = point_of_offset0 } = x_5698
     1822    point_of_offset = point_of_offset0 } = x_378
    17661823  in
    17671824  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     
    17721829    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17731830    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
    1774 let rec serialized_params_rect_Type5 h_mk_serialized_params x_5700 =
     1831let rec serialized_params_rect_Type5 h_mk_serialized_params x_380 =
    17751832  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1776     point_of_offset = point_of_offset0 } = x_5700
     1833    point_of_offset = point_of_offset0 } = x_380
    17771834  in
    17781835  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     
    17831840    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17841841    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
    1785 let rec serialized_params_rect_Type3 h_mk_serialized_params x_5702 =
     1842let rec serialized_params_rect_Type3 h_mk_serialized_params x_382 =
    17861843  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1787     point_of_offset = point_of_offset0 } = x_5702
     1844    point_of_offset = point_of_offset0 } = x_382
    17881845  in
    17891846  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     
    17941851    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17951852    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
    1796 let rec serialized_params_rect_Type2 h_mk_serialized_params x_5704 =
     1853let rec serialized_params_rect_Type2 h_mk_serialized_params x_384 =
    17971854  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1798     point_of_offset = point_of_offset0 } = x_5704
     1855    point_of_offset = point_of_offset0 } = x_384
    17991856  in
    18001857  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     
    18051862    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    18061863    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
    1807 let rec serialized_params_rect_Type1 h_mk_serialized_params x_5706 =
     1864let rec serialized_params_rect_Type1 h_mk_serialized_params x_386 =
    18081865  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1809     point_of_offset = point_of_offset0 } = x_5706
     1866    point_of_offset = point_of_offset0 } = x_386
    18101867  in
    18111868  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     
    18161873    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    18171874    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
    1818 let rec serialized_params_rect_Type0 h_mk_serialized_params x_5708 =
     1875let rec serialized_params_rect_Type0 h_mk_serialized_params x_388 =
    18191876  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1820     point_of_offset = point_of_offset0 } = x_5708
     1877    point_of_offset = point_of_offset0 } = x_388
    18211878  in
    18221879  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     
    19101967    (serialized_params -> (Joint.joint_program ->
    19111968    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
    1912 let 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
     1969let rec sem_params_rect_Type4 h_mk_sem_params x_406 =
     1970  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_406 in
    19141971  h_mk_sem_params spp'0 pre_main_generator0
    19151972
     
    19171974    (serialized_params -> (Joint.joint_program ->
    19181975    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
    1919 let 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
     1976let rec sem_params_rect_Type5 h_mk_sem_params x_408 =
     1977  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_408 in
    19211978  h_mk_sem_params spp'0 pre_main_generator0
    19221979
     
    19241981    (serialized_params -> (Joint.joint_program ->
    19251982    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
    1926 let 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
     1983let rec sem_params_rect_Type3 h_mk_sem_params x_410 =
     1984  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_410 in
    19281985  h_mk_sem_params spp'0 pre_main_generator0
    19291986
     
    19311988    (serialized_params -> (Joint.joint_program ->
    19321989    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
    1933 let 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
     1990let rec sem_params_rect_Type2 h_mk_sem_params x_412 =
     1991  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_412 in
    19351992  h_mk_sem_params spp'0 pre_main_generator0
    19361993
     
    19381995    (serialized_params -> (Joint.joint_program ->
    19391996    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
    1940 let 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
     1997let rec sem_params_rect_Type1 h_mk_sem_params x_414 =
     1998  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_414 in
    19421999  h_mk_sem_params spp'0 pre_main_generator0
    19432000
     
    19452002    (serialized_params -> (Joint.joint_program ->
    19462003    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
    1947 let 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
     2004let rec sem_params_rect_Type0 h_mk_sem_params x_416 =
     2005  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_416 in
    19492006  h_mk_sem_params spp'0 pre_main_generator0
    19502007
     
    20342091
    20352092(** val fetch_statement :
    2036     sem_params -> AST.ident List.list -> Joint.joint_function
    2037     Globalenvs.genv_t -> ByteValues.program_counter -> ((AST.ident,
    2038     Joint.joint_closed_internal_function) Types.prod, Joint.joint_statement)
    2039     Types.prod Errors.res **)
     2093    sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter
     2094    -> ((AST.ident, Joint.joint_closed_internal_function) Types.prod,
     2095    Joint.joint_statement) Types.prod Errors.res **)
    20402096let fetch_statement p globals ge0 ptr =
    20412097  Obj.magic
    20422098    (Monad.m_bind2 (Monad.max_def Errors.res0)
    2043       (Obj.magic (fetch_internal_function ge0 ptr.ByteValues.pc_block))
     2099      (Obj.magic
     2100        (fetch_internal_function globals ge0 ptr.ByteValues.pc_block))
    20442101      (fun id fn ->
    20452102      let pt = point_of_pc p ptr in
     
    20542111
    20552112(** val pc_of_label :
    2056     sem_params -> AST.ident List.list -> Joint.joint_function
    2057     Globalenvs.genv_t -> Pointers.block Types.sig0 -> Graphs.label ->
    2058     ByteValues.program_counter Errors.res **)
     2113    sem_params -> AST.ident List.list -> genv -> Pointers.block Types.sig0 ->
     2114    Graphs.label -> ByteValues.program_counter Errors.res **)
    20592115let pc_of_label p globals ge0 bl lbl =
    20602116  Obj.magic
    20612117    (Monad.m_bind2 (Monad.max_def Errors.res0)
    2062       (Obj.magic (fetch_internal_function ge0 bl)) (fun i fn ->
     2118      (Obj.magic (fetch_internal_function globals ge0 bl)) (fun i fn ->
    20632119      Monad.m_bind0 (Monad.max_def Errors.res0)
    20642120        (Obj.magic
     
    20802136
    20812137(** val goto :
    2082     sem_params -> AST.ident List.list -> Joint.joint_function
    2083     Globalenvs.genv_t -> Graphs.label -> state_pc -> state_pc Errors.res **)
     2138    sem_params -> AST.ident List.list -> genv -> Graphs.label -> state_pc ->
     2139    state_pc Errors.res **)
    20842140let goto p globals ge0 l st =
    20852141  Obj.magic
     
    20962152
    20972153(** val next_of_call_pc :
    2098     sem_params -> AST.ident List.list -> Joint.joint_function
    2099     Globalenvs.genv_t -> ByteValues.program_counter -> __ Errors.res **)
     2154    sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter
     2155    -> __ Errors.res **)
    21002156let next_of_call_pc p globals ge0 pc0 =
    21012157  Obj.magic
     
    22892345    p.spp'.msu_pars.eval_ext_seq globals ge0 c curr_id st
    22902346
    2291 (** val code_block_of_block :
    2292     Pointers.block -> Pointers.block Types.sig0 Types.option **)
    2293 let code_block_of_block bl =
    2294   (match Pointers.block_region bl with
    2295    | AST.XData -> (fun _ -> Types.None)
    2296    | AST.Code -> (fun _ -> Types.Some bl)) __
    2297 
    2298 (** val block_of_funct_id :
    2299     sem_state_params -> 'a1 Globalenvs.genv_t -> PreIdentifiers.identifier ->
    2300     Pointers.block Types.sig0 Errors.res **)
    2301 let block_of_funct_id sp0 ge0 id =
    2302   Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
    2303     (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
    2304     (Obj.magic
    2305       (Monad.m_bind0 (Monad.max_def Option.option)
    2306         (Obj.magic (Globalenvs.find_symbol ge0 id)) (fun bl ->
    2307         Obj.magic (code_block_of_block bl))))
    2308 
    23092347(** val block_of_call :
    23102348    sem_params -> AST.ident List.list -> Joint.joint_function
     
    24232461    Obj.magic x) (fun bl ->
    24242462    Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    2425       (let x =
    2426          IOMonad.err_to_io
    2427            (fetch_function
    2428              (let p0 = spp'__o__spp p in
    2429              let globals0 = globals in let g = ge0 in g.ge) bl)
    2430        in
     2463      (let x = IOMonad.err_to_io (fetch_function globals ge0 bl) in
    24312464      Obj.magic x) (fun i fd ->
    24322465      match fd with
     
    24882521      (fun st' call_pc ->
    24892522      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 ->
     2523        (Obj.magic (next_of_call_pc p globals ge0 call_pc)) (fun nxt ->
    24952524        let st'' =
    24962525          set_last_pop p.spp'.msu_pars.st_pars
     
    25152544    Obj.magic x) (fun bl ->
    25162545    Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    2517       (let x =
    2518          IOMonad.err_to_io
    2519            (fetch_function
    2520              (let p0 = spp'__o__spp p in
    2521              let globals0 = globals in let g = ge0 in g.ge) bl)
    2522        in
     2546      (let x = IOMonad.err_to_io (fetch_function globals ge0 bl) in
    25232547      Obj.magic x) (fun i fd ->
    25242548      match fd with
     
    25772601               (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
    25782602               match b with
    2579                | Bool.True ->
    2580                  Obj.magic
    2581                    (goto p g
    2582                      (let p0 = spp'__o__spp p in
    2583                      let globals = g in let g0 = ge0 in g0.ge) l st)
     2603               | Bool.True -> Obj.magic (goto p g ge0 l st)
    25842604               | Bool.False ->
    25852605                 Monad.m_return0 (Monad.max_def Errors.res0) (next p nxt st)))))
     
    25902610    let curr_ret = (Types.pi1 curr_fn).Joint.joint_if_result in
    25912611    (match s0 with
    2592      | Joint.GOTO l ->
    2593        IOMonad.err_to_io
    2594          (goto p g
    2595            (let p0 = spp'__o__spp p in
    2596            let globals = g in let g0 = ge0 in g0.ge) l st)
     2612     | Joint.GOTO l -> IOMonad.err_to_io (goto p g ge0 l st)
    25972613     | Joint.RETURN ->
    25982614       IOMonad.err_to_io
     
    26112627            (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
    26122628            match b with
    2613             | Bool.True ->
    2614               Obj.magic
    2615                 (goto p g
    2616                   (let p0 = spp'__o__spp p in
    2617                   let globals = g in let g0 = ge0 in g0.ge) lbltrue st)
    2618             | Bool.False ->
    2619               Obj.magic
    2620                 (goto p g
    2621                   (let p0 = spp'__o__spp p in
    2622                   let globals = g in let g0 = ge0 in g0.ge) lblfalse st)))))
     2629            | Bool.True -> Obj.magic (goto p g ge0 lbltrue st)
     2630            | Bool.False -> Obj.magic (goto p g ge0 lblfalse st)))))
    26232631
    26242632(** val eval_state :
     
    26282636  Obj.magic
    26292637    (Monad.m_bind3 (Monad.max_def IOMonad.iOMonad)
    2630       (let x =
    2631          IOMonad.err_to_io
    2632            (fetch_statement p globals
    2633              (let p0 = spp'__o__spp p in
    2634              let globals0 = globals in let g = ge0 in g.ge) st.pc)
    2635        in
     2638      (let x = IOMonad.err_to_io (fetch_statement p globals ge0 st.pc) in
    26362639      Obj.magic x) (fun id fn s ->
    26372640      Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
Note: See TracChangeset for help on using the changeset viewer.