Changeset 1224 for src/RTLabs
- Timestamp:
- Sep 16, 2011, 6:39:05 PM (9 years ago)
- Location:
- src/RTLabs
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLAbstoRTL.ma
r1149 r1224 1286 1286 1287 1287 definition translate ≝ 1288 λp: program ( fundef internal_function) unit.1288 λp: program (λ_.fundef internal_function) nat. 1289 1289 let f_funct ≝ λid_fun_def. 1290 1290 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 1300 1294 let functs' ≝ map ? ? f_funct (prog_funct ? ? p) in 1301 1295 let main' ≝ prog_main ? ? p in -
src/RTLabs/syntax.ma
r1147 r1224 43 43 allocate. *) 44 44 45 definition RTLabs_program ≝ program (fundef internal_function) nat. 46 45 definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
Note: See TracChangeset
for help on using the changeset viewer.