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_fullexec.mli

    r2951 r2960  
    161161open Measurable
    162162
    163 type joint_global = { jglobals : AST.ident List.list;
    164                       jgenv : Joint_semantics.genv }
    165 
    166 val joint_global_rect_Type4 :
    167   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    168   -> 'a1) -> joint_global -> 'a1
    169 
    170 val joint_global_rect_Type5 :
    171   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    172   -> 'a1) -> joint_global -> 'a1
    173 
    174 val joint_global_rect_Type3 :
    175   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    176   -> 'a1) -> joint_global -> 'a1
    177 
    178 val joint_global_rect_Type2 :
    179   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    180   -> 'a1) -> joint_global -> 'a1
    181 
    182 val joint_global_rect_Type1 :
    183   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    184   -> 'a1) -> joint_global -> 'a1
    185 
    186 val joint_global_rect_Type0 :
    187   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    188   -> 'a1) -> joint_global -> 'a1
    189 
    190 val jglobals :
    191   Joint_semantics.sem_params -> joint_global -> AST.ident List.list
    192 
    193 val jgenv :
    194   Joint_semantics.sem_params -> joint_global -> Joint_semantics.genv
    195 
    196 val joint_global_inv_rect_Type4 :
    197   Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    198   Joint_semantics.genv -> __ -> 'a1) -> 'a1
    199 
    200 val joint_global_inv_rect_Type3 :
    201   Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    202   Joint_semantics.genv -> __ -> 'a1) -> 'a1
    203 
    204 val joint_global_inv_rect_Type2 :
    205   Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    206   Joint_semantics.genv -> __ -> 'a1) -> 'a1
    207 
    208 val joint_global_inv_rect_Type1 :
    209   Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    210   Joint_semantics.genv -> __ -> 'a1) -> 'a1
    211 
    212 val joint_global_inv_rect_Type0 :
    213   Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    214   Joint_semantics.genv -> __ -> 'a1) -> 'a1
    215 
    216 val joint_global_discr :
    217   Joint_semantics.sem_params -> joint_global -> joint_global -> __
    218 
    219 val joint_global_jmdiscr :
    220   Joint_semantics.sem_params -> joint_global -> joint_global -> __
    221 
    222 val dpi1__o__jgenv__o__inject :
    223   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    224   Joint_semantics.genv Types.sig0
    225 
    226 val dpi1__o__jgenv__o__genv_to_genv_t__o__inject :
    227   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    228   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    229   Types.sig0
    230 
    231 val dpi1__o__jgenv__o__genv_to_genv_t :
    232   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    233   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    234 
    235 val eject__o__jgenv__o__inject :
    236   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    237   Joint_semantics.genv Types.sig0
    238 
    239 val eject__o__jgenv__o__genv_to_genv_t__o__inject :
    240   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    241   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    242   Types.sig0
    243 
    244 val eject__o__jgenv__o__genv_to_genv_t :
    245   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    246   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    247 
    248 val jgenv__o__genv_to_genv_t :
    249   Joint_semantics.sem_params -> joint_global ->
    250   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    251 
    252 val jgenv__o__genv_to_genv_t__o__inject :
    253   Joint_semantics.sem_params -> joint_global ->
    254   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    255   Types.sig0
    256 
    257 val jgenv__o__inject :
    258   Joint_semantics.sem_params -> joint_global -> Joint_semantics.genv
    259   Types.sig0
    260 
    261 val dpi1__o__jgenv :
    262   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    263   Joint_semantics.genv
    264 
    265 val eject__o__jgenv :
    266   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    267   Joint_semantics.genv
    268 
    269 val eval_params_of_global :
    270   Joint_semantics.sem_params -> joint_global -> Traces.evaluation_params
    271 
    272 val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    273   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    274   Joint.unserialized_params
    275 
    276 val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    277   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    278   Joint.uns_params
    279 
    280 val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
    281   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    282   Joint.stmt_params
    283 
    284 val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp :
    285   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    286   Joint.params
    287 
    288 val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
    289   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    290   Joint_semantics.sem_state_params
    291 
    292 val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
    293   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    294   Joint.joint_closed_internal_function
    295   Joint_semantics.sem_unserialized_params
    296 
    297 val dpi1__o__eval_params_of_global__o__sparams__o__spp' :
    298   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    299   Joint_semantics.serialized_params
    300 
    301 val dpi1__o__eval_params_of_global__o__sparams :
    302   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    303   Joint_semantics.sem_params
    304 
    305 val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    306   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    307   Joint.unserialized_params
    308 
    309 val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    310   Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.uns_params
    311 
    312 val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
    313   Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.stmt_params
    314 
    315 val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp :
    316   Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.params
    317 
    318 val eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
    319   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    320   Joint_semantics.sem_state_params
    321 
    322 val eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
    323   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    324   Joint.joint_closed_internal_function
    325   Joint_semantics.sem_unserialized_params
    326 
    327 val eject__o__eval_params_of_global__o__sparams__o__spp' :
    328   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    329   Joint_semantics.serialized_params
    330 
    331 val eject__o__eval_params_of_global__o__sparams :
    332   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    333   Joint_semantics.sem_params
    334 
    335 val eval_params_of_global__o__sparams :
    336   Joint_semantics.sem_params -> joint_global -> Joint_semantics.sem_params
    337 
    338 val eval_params_of_global__o__sparams__o__spp' :
    339   Joint_semantics.sem_params -> joint_global ->
    340   Joint_semantics.serialized_params
    341 
    342 val eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
    343   Joint_semantics.sem_params -> joint_global ->
    344   Joint.joint_closed_internal_function
    345   Joint_semantics.sem_unserialized_params
    346 
    347 val eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
    348   Joint_semantics.sem_params -> joint_global ->
    349   Joint_semantics.sem_state_params
    350 
    351 val eval_params_of_global__o__sparams__o__spp'__o__spp :
    352   Joint_semantics.sem_params -> joint_global -> Joint.params
    353 
    354 val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
    355   Joint_semantics.sem_params -> joint_global -> Joint.stmt_params
    356 
    357 val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    358   Joint_semantics.sem_params -> joint_global -> Joint.uns_params
    359 
    360 val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    361   Joint_semantics.sem_params -> joint_global -> Joint.unserialized_params
    362 
    363 val dpi1__o__eval_params_of_global :
    364   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    365   Traces.evaluation_params
    366 
    367 val eject__o__eval_params_of_global :
    368   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    369   Traces.evaluation_params
    370 
    371 val make_joint_global :
    372   Joint_semantics.sem_params -> (Joint.joint_program, AST.ident -> Nat.nat
    373   Types.option) Types.prod -> joint_global
    374 
    375163val joint_exec :
    376164  Joint_semantics.sem_params -> (IO.io_out, IO.io_in)
Note: See TracChangeset for help on using the changeset viewer.