Ignore:
Timestamp:
Oct 3, 2011, 8:35:23 AM (9 years ago)
Author:
sacerdot
Message:

Bugs fixed: fresh_label changes the label universe, but this was not propagated
correctly. Fixed in RTLtoERTL. To be fixed in RTLAbsToRTL and (maybe) in
ERTLtoRTL.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r1283 r1284  
    3535qed.
    3636
    37 definition fresh_label ≝
    38   λglobals,params. λdef: joint_internal_function globals params.
    39     fresh LabelTag (joint_if_luniverse … def).
    40 
    41 let rec adds_graph
    42   (pars1: params1) (globals: list ident)
    43   (stmt_list: list (label → joint_statement (graph_params_ pars1) globals))
    44   (start_lbl: label) (dest_lbl: label)
    45   (def: joint_internal_function … (graph_params pars1 globals))
    46     on stmt_list ≝
    47   match stmt_list with
    48   [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
    49   | cons stmt stmt_list ⇒
    50     match stmt_list with
    51     [ nil ⇒ add_graph … start_lbl (stmt dest_lbl) def
    52     | _ ⇒
    53       let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
    54       let def ≝ add_graph … start_lbl (stmt tmp_lbl) def in
    55         adds_graph pars1 globals stmt_list tmp_lbl dest_lbl def]].
     37definition fresh_label:
     38 ∀pars0,globals. joint_internal_function … (graph_params pars0 globals) → label × (joint_internal_function … (graph_params pars0 globals)) ≝
     39  λpars0,globals,def.
     40    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
     41     〈r,set_luniverse … def luniverse〉.
    5642
    5743let rec add_translates
     
    6652    [ nil ⇒ trans start_lbl dest_lbl def
    6753    | _ ⇒
    68       let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
     54      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
    6955      let def ≝ trans start_lbl tmp_lbl def in
    7056        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
     57
     58definition adds_graph ≝
     59 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
     60  add_translates … (map … (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
Note: See TracChangeset for help on using the changeset viewer.