Changeset 1281 for src/RTLabs


Ignore:
Timestamp:
Sep 28, 2011, 11:08:37 PM (8 years ago)
Author:
sacerdot
Message:

Porting of all transformation to the joint syntax practically completed.
Some functions remain to be ported in RTLAbstoRTL, but it is just repetitive
coding.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1280 r1281  
    66include "joint/TranslateUtils.ma".
    77
    8 (*
    98let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
    109  match n with
    11   [ O ⇒ [ ]
    12   | S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n')
    13   ].
    14 *)
     10  [ O ⇒ 〈[],runiverse〉
     11  | S n' ⇒
     12     let 〈r,runiverse〉 ≝ fresh … runiverse in
     13     let 〈res,runiverse〉 ≝ register_freshes runiverse n' in
     14      〈r::res,runiverse〉 ].
    1515
    1616definition choose_rest ≝
     
    8787  λr: register.λbvt. lookup … (word_of_identifier … r) bvt [].
    8888
    89 (*
    9089definition initialize_local_env_internal ≝
    91   λruniverse.
    92   λlenv.
     90  λlenv_runiverse.
    9391  λr_sig.
     92  let 〈lenv,runiverse〉 ≝ lenv_runiverse in
    9493  let 〈r, sig〉 ≝ r_sig in
    9594  let size ≝ size_of_sig_type sig in
    96   let rs ≝ register_freshes runiverse size in
    97     add_local_env r rs lenv.
     95  let 〈rs,runiverse〉 ≝ register_freshes runiverse size in
     96    〈add_local_env r rs lenv,runiverse〉.
    9897
    9998definition initialize_local_env ≝
     
    107106    ]
    108107  in
    109     foldl ? ? (initialize_local_env_internal runiverse) (Stub …) registers.
    110 *)
     108    foldl ? ? initialize_local_env_internal 〈Stub …,runiverse〉 registers.
    111109
    112110definition map_list_local_env_internal ≝
     
    219217    ] start_lbl dest_lbl def.
    220218
     219(*
    221220definition translate_cast_signed ≝
    222221  λglobals.
     
    10071006  ]
    10081007qed.
     1008*)
    10091009
    10101010definition translate_stmt ≝
    1011   λlenv.
     1011  λglobals.
     1012  λlenv: local_env.
    10121013  λlbl: label.
    10131014  λstmt.
    1014   λdef: rtl_internal_function.
     1015  λdef: joint_internal_function … (rtl_params globals).
    10151016  match stmt with
    1016   [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
     1017  [ St_skip lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def
     1018  | _ ⇒ ? ].
     1019(*
    10171020  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
    10181021  | St_const destr cst lbl' ⇒
     
    10541057  |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *)
    10551058  ]
     1059*) cases daemon
    10561060qed.
    10571061
     
    10611065   skip instructions at these nodes. *)
    10621066definition translate_internal ≝
    1063   λdef.
     1067  λglobals,def.
    10641068  let runiverse ≝ f_reggen def in
    1065   let lenv ≝ initialize_local_env runiverse
     1069  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
    10661070    (f_params def @ f_locals def) (f_result def) in
    10671071  let params ≝ map_list_local_env lenv (map ? ? \fst (f_params def)) in
     
    10831087  let entry' ≝ f_entry def in
    10841088  let exit' ≝ f_exit def in
    1085   let graph' ≝ add ? ? (empty_map ? ?) entry' (rtl_st_skip entry') in
    1086   let graph' ≝ add ? ? graph' exit' (rtl_st_skip exit') in
     1089  let graph' ≝ add … (empty_map ? ?) entry' (joint_st_goto … entry') in
     1090  let graph' ≝ add … graph' exit' (joint_st_goto … exit') in
    10871091  let res ≝
    1088     mk_rtl_internal_function luniverse' runiverse' result' params'
    1089                          locals' stack_size' graph' ? ? in
    1090     foldi ? ? ? (translate_stmt lenv) (f_graph def) res.
    1091   [1: %
    1092       [1: @entry'
    1093       |2: normalize nodelta;
    1094           @graph_add_lookup
    1095           @graph_add
    1096       ]
    1097   |2: %
    1098       [1: @exit'
    1099       |2: normalize nodelta;
    1100           @graph_add
    1101       ]
    1102   ]
     1092    mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
     1093     locals' stack_size' graph' ? ? in
     1094    foldi … (translate_stmt … lenv) (f_graph def) res.
     1095[ % [@entry' | @graph_add_lookup @graph_add]
     1096| % [@exit'  | @graph_add]]
    11031097qed.
    11041098
     
    11061100  because of CompCert heritage *)
    11071101definition rtlabs_to_rtl : RTLabs_program → rtl_program ≝
    1108  λp. transform_program … p (transf_fundef … translate_internal).
     1102 λp. transform_program ??? p (transf_fundef … (translate_internal (prog_var_names …))).
Note: See TracChangeset for help on using the changeset viewer.