Changeset 1239


Ignore:
Timestamp:
Sep 21, 2011, 5:21:39 PM (8 years ago)
Author:
sacerdot
Message:

RTLAbstoRTL ported to new datatypes.

Note: RTL syntax/semantics is not (yet?) an instance of Joint.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r1115 r1239  
    5151
    5252definition rtl_function_definition ≝ fundef rtl_internal_function.
    53  
    54 record rtl_program: Type[0] ≝
    55 {
    56   rtl_pr_vars: list (ident × nat);
    57   rtl_pr_functs: list (ident × rtl_function_definition);
    58   rtl_pr_main: option ident
    59 }.
     53
     54definition rtl_program: Type[0] ≝ program (λ_.rtl_function_definition) nat.
  • src/RTLabs/RTLAbstoRTL.ma

    r1224 r1239  
    12641264qed.
    12651265
    1266 definition translate_fun_def ≝
    1267   λfdef: fundef internal_function.
    1268   match fdef with
    1269   [ Internal f ⇒ Internal ? (translate_internal f)
    1270   | External e ⇒ External ? e
    1271   ].
    1272 
    1273 (* XXX: change, we need to propagate the region information, not ignore it *)
    1274 definition init_data_to_nat ≝
    1275   λi: init_data.
    1276   match i with
    1277   [ Init_int8 i8 ⇒ 8
    1278   | Init_int16 i16 ⇒ 16
    1279   | Init_int32 i32 ⇒ 32
    1280   | Init_float32 f32 ⇒ 32
    1281   | Init_float64 f64 ⇒ 64
    1282   | Init_space s ⇒ s
    1283   | Init_null r ⇒ 0
    1284   | Init_addrof r i o ⇒ 8 (* XXX: not at all sure about this one *)
    1285   ].
    1286 
    1287 definition translate ≝
    1288   λp: program (λ_.fundef internal_function) nat.
    1289   let f_funct ≝ λid_fun_def.
    1290     let 〈id, fun_def〉 ≝ id_fun_def in
    1291       〈id, translate_fun_def fun_def〉 in
    1292   (*CSC: bug here: we are throwing away the regions doing no checks at all *)
    1293   let vars' ≝ map … (λx. let 〈id,reg,n〉 ≝ x in 〈id,n〉) (prog_vars … p) in
    1294   let functs' ≝ map ? ? f_funct (prog_funct ? ? p) in
    1295   let main' ≝ prog_main ? ? p in
    1296     mk_rtl_program vars' functs' (Some ? main').
     1266(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
     1267  because of CompCert heritage *)
     1268definition rtlabs_to_rtl : RTLabs_program → rtl_program ≝
     1269 λp. transform_program … p (transf_fundef … translate_internal).
Note: See TracChangeset for help on using the changeset viewer.