Changeset 1224 for src/RTLabs


Ignore:
Timestamp:
Sep 16, 2011, 6:39:05 PM (8 years ago)
Author:
sacerdot
Message:

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1149 r1224  
    12861286
    12871287definition translate ≝
    1288   λp: program (fundef internal_function) unit.
     1288  λp: program (λ_.fundef internal_function) nat.
    12891289  let f_funct ≝ λid_fun_def.
    12901290    let 〈id, fun_def〉 ≝ id_fun_def in
    1291       〈id, translate_fun_def fun_def〉
    1292   in
    1293   let vars' ≝ map ? ? (λx.
    1294     let 〈id_init_ignore, ignore〉 ≝ x in
    1295     let 〈id_init, ignore〉 ≝ id_init_ignore in
    1296     let 〈id, init〉 ≝ id_init in
    1297     let init_total ≝ foldr ? ? plus 0 (map ? ? init_data_to_nat init) in
    1298       〈id, init_total〉) (prog_vars ? ? p)
    1299   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
    13001294  let functs' ≝ map ? ? f_funct (prog_funct ? ? p) in
    13011295  let main' ≝ prog_main ? ? p in
  • src/RTLabs/syntax.ma

    r1147 r1224  
    4343   allocate. *)
    4444
    45 definition RTLabs_program ≝ program (fundef internal_function) nat.
    46 
     45definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
Note: See TracChangeset for help on using the changeset viewer.