Changeset 1224 for src/RTLabs

Timestamp:

Sep 16, 2011, 6:39:05 PM (9 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:

• RTLAbstoRTL.ma (modified) (1 diff)
• syntax.ma (modified) (1 diff)

src/RTLabs/RTLAbstoRTL.ma

@@ -1286 +1286 @@
 
 definition translate ≝
-  λp: program (fundef internal_function) unit.
+  λp: program (λ_.fundef internal_function) nat.
   let f_funct ≝ λid_fun_def.
     let 〈id, fun_def〉 ≝ id_fun_def in
-      〈id, translate_fun_def fun_def〉
-  in
-  let vars' ≝ map ? ? (λx.
-    let 〈id_init_ignore, ignore〉 ≝ x in
-    let 〈id_init, ignore〉 ≝ id_init_ignore in
-    let 〈id, init〉 ≝ id_init in
-    let init_total ≝ foldr ? ? plus 0 (map ? ? init_data_to_nat init) in
-      〈id, init_total〉) (prog_vars ? ? p)
-  in
+      〈id, translate_fun_def fun_def〉 in
+  (*CSC: bug here: we are throwing away the regions doing no checks at all *)
+  let vars' ≝ map … (λx. let 〈id,reg,n〉 ≝ x in 〈id,n〉) (prog_vars … p) in
   let functs' ≝ map ? ? f_funct (prog_funct ? ? p) in
   let main' ≝ prog_main ? ? p in

src/RTLabs/syntax.ma

@@ -43 +43 @@
    allocate. *)
 
-definition RTLabs_program ≝ program (fundef internal_function) nat.
-
+definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.