Ignore:
Timestamp:
Mar 28, 2013, 5:27:46 PM (7 years ago)
Author:
sacerdot
Message:

New extraction after ERTLptr abortion.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/semantics.ml

    r3001 r3019  
    5555open LTL
    5656
    57 open ERTLptrToLTL
    58 
    59 open ERTLptr
    60 
    61 open ERTLToERTLptr
     57open ERTLToLTL
    6258
    6359open ERTL
     
    306302
    307303open ERTL_semantics
    308 
    309 open ERTLptr_semantics
    310304
    311305open Joint_LTL_LIN_semantics
     
    324318    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    325319    preclassified_system_pass -> 'a1 **)
    326 let 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 __
     320let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_211 =
     321  let pcs_pcs = x_211 in h_mk_preclassified_system_pass pcs_pcs __
    328322
    329323(** val preclassified_system_pass_rect_Type5 :
    330324    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    331325    preclassified_system_pass -> 'a1 **)
    332 let 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 __
     326let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_213 =
     327  let pcs_pcs = x_213 in h_mk_preclassified_system_pass pcs_pcs __
    334328
    335329(** val preclassified_system_pass_rect_Type3 :
    336330    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    337331    preclassified_system_pass -> 'a1 **)
    338 let 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 __
     332let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_215 =
     333  let pcs_pcs = x_215 in h_mk_preclassified_system_pass pcs_pcs __
    340334
    341335(** val preclassified_system_pass_rect_Type2 :
    342336    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    343337    preclassified_system_pass -> 'a1 **)
    344 let 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 __
     338let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_217 =
     339  let pcs_pcs = x_217 in h_mk_preclassified_system_pass pcs_pcs __
    346340
    347341(** val preclassified_system_pass_rect_Type1 :
    348342    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    349343    preclassified_system_pass -> 'a1 **)
    350 let 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 __
     344let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_219 =
     345  let pcs_pcs = x_219 in h_mk_preclassified_system_pass pcs_pcs __
    352346
    353347(** val preclassified_system_pass_rect_Type0 :
    354348    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    355349    preclassified_system_pass -> 'a1 **)
    356 let 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 __
     350let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_221 =
     351  let pcs_pcs = x_221 in h_mk_preclassified_system_pass pcs_pcs __
    358352
    359353(** val pcs_pcs :
     
    432426      (SemanticsUtils.sem_graph_params_to_sem_params
    433427        ERTL_semantics.eRTL_semantics))
    434 | Compiler.Ertlptr_pass ->
    435   (fun x ->
    436     Joint_fullexec.joint_preclassified_system
    437       (SemanticsUtils.sem_graph_params_to_sem_params
    438         ERTLptr_semantics.eRTLptr_semantics))
    439428| Compiler.Ltl_pass ->
    440429  (fun x ->
     
    447436| Compiler.Assembly_pass ->
    448437  (fun prog ->
    449     let { Types.fst = eta29797; Types.snd = policy } = Obj.magic prog in
    450     let { Types.fst = code; Types.snd = sigma } = eta29797 in
     438    let { Types.fst = eta19; Types.snd = policy } = Obj.magic prog in
     439    let { Types.fst = code; Types.snd = sigma } = eta19 in
    451440    Interpret2.aSM_preclassified_system code sigma policy)
    452441| Compiler.Object_code_pass ->
Note: See TracChangeset for help on using the changeset viewer.