Ignore:
Timestamp:
Mar 28, 2013, 1:02:48 PM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/semantics.ml

    r2960 r3001  
    324324    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    325325    preclassified_system_pass -> 'a1 **)
    326 let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_108 =
    327   let pcs_pcs = x_108 in h_mk_preclassified_system_pass pcs_pcs __
     326let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_16776 =
     327  let pcs_pcs = x_16776 in h_mk_preclassified_system_pass pcs_pcs __
    328328
    329329(** val preclassified_system_pass_rect_Type5 :
    330330    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    331331    preclassified_system_pass -> 'a1 **)
    332 let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_110 =
    333   let pcs_pcs = x_110 in h_mk_preclassified_system_pass pcs_pcs __
     332let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_16778 =
     333  let pcs_pcs = x_16778 in h_mk_preclassified_system_pass pcs_pcs __
    334334
    335335(** val preclassified_system_pass_rect_Type3 :
    336336    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    337337    preclassified_system_pass -> 'a1 **)
    338 let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_112 =
    339   let pcs_pcs = x_112 in h_mk_preclassified_system_pass pcs_pcs __
     338let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_16780 =
     339  let pcs_pcs = x_16780 in h_mk_preclassified_system_pass pcs_pcs __
    340340
    341341(** val preclassified_system_pass_rect_Type2 :
    342342    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    343343    preclassified_system_pass -> 'a1 **)
    344 let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_114 =
    345   let pcs_pcs = x_114 in h_mk_preclassified_system_pass pcs_pcs __
     344let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_16782 =
     345  let pcs_pcs = x_16782 in h_mk_preclassified_system_pass pcs_pcs __
    346346
    347347(** val preclassified_system_pass_rect_Type1 :
    348348    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    349349    preclassified_system_pass -> 'a1 **)
    350 let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_116 =
    351   let pcs_pcs = x_116 in h_mk_preclassified_system_pass pcs_pcs __
     350let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_16784 =
     351  let pcs_pcs = x_16784 in h_mk_preclassified_system_pass pcs_pcs __
    352352
    353353(** val preclassified_system_pass_rect_Type0 :
    354354    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    355355    preclassified_system_pass -> 'a1 **)
    356 let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_118 =
    357   let pcs_pcs = x_118 in h_mk_preclassified_system_pass pcs_pcs __
     356let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_16786 =
     357  let pcs_pcs = x_16786 in h_mk_preclassified_system_pass pcs_pcs __
    358358
    359359(** val pcs_pcs :
     
    397397    SmallstepExec.fullexec **)
    398398let pcs_pcs__o__pcs_exec x0 x1 =
    399   (pcs_pcs x0 x1).Measurable.pcs_exec
     399  Measurable.pcs_exec (pcs_pcs x0 x1)
    400400
    401401(** val pcs_pcs__o__pcs_exec__o__es1 :
     
    447447| Compiler.Assembly_pass ->
    448448  (fun prog ->
    449     let { Types.fst = eta26; Types.snd = policy } = Obj.magic prog in
    450     let { Types.fst = code; Types.snd = sigma } = eta26 in
     449    let { Types.fst = eta29797; Types.snd = policy } = Obj.magic prog in
     450    let { Types.fst = code; Types.snd = sigma } = eta29797 in
    451451    Interpret2.aSM_preclassified_system code sigma policy)
    452452| Compiler.Object_code_pass ->
     
    461461  let pcs = preclassified_system_of_pass pass prog in
    462462  let prog0 = prog in
    463   let g = (pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0 in
    464   (match (pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_initial_state
     463  let g = SmallstepExec.make_global (pcs_pcs__o__pcs_exec pass pcs) prog0 in
     464  (match SmallstepExec.make_initial_state (pcs_pcs__o__pcs_exec pass pcs)
    465465           prog0 with
    466466   | Errors.OK s0 ->
     
    469469       Measurable.observe_all_in_measurable n
    470470         (Measurable.pcs_to_cs (pcs_pcs pass pcs)
    471            ((pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0))
     471           (SmallstepExec.make_global (pcs_pcs__o__pcs_exec pass pcs) prog0))
    472472         print_event List.Nil s0
    473473     in
Note: See TracChangeset for help on using the changeset viewer.