Changeset 1207

Timestamp:

Sep 12, 2011, 4:20:57 PM (8 years ago)

Author:

campbell

Message:

Second part of fixing temporaries in Clight to Cminor stage.

Location:

src

Files:

• ASM/Arithmetic.ma (modified) (1 diff)
• Clight/fresh.ma (added)
• Clight/toCminor.ma (modified) (2 diffs)

src/ASM/Arithmetic.ma

@@ -319 +319 @@
 alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
 
+definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
+definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
+definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
+definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
+
 definition bitvector_of_bool:
       ∀n: nat. ∀b: bool. BitVector (S n) ≝

src/Clight/toCminor.ma

@@ -660 +660 @@
   ]) (OK ? s) params.
 
-definition bigu ≝ mk_universe SymbolTag [[
-false;true;false;false;
-false;false;false;false;
-false;false;false;false;
-false;false;false;false]] false.
-
-(* FIXME: the temporary handling is a bit dodgy, I'm afraid. *)
-definition translate_function : list (ident×region) → function → res internal_function ≝
-λglobals, f.
+definition translate_function : universe SymbolTag → list (ident×region) → function → res internal_function ≝
+λtmpuniverse, globals, f.
   let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in
-  let tmp ≝ mk_tmpgen bigu [ ] in (* FIXME *)
+  let tmp ≝ mk_tmpgen tmpuniverse [ ] in
   do 〈s,tmp〉 ← translate_statement vartypes tmp (fn_body f);
   do s ← alloc_params vartypes (fn_params f) s;
@@ -680 +673 @@
     s).
 
-definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝
-λglobals,f.
+definition translate_fundef : universe SymbolTag → list (ident×region) → clight_fundef → res (fundef internal_function) ≝
+λtmpuniverse,globals,f.
 match f with
-[ CL_Internal fn ⇒ do fn' ← translate_function globals fn; OK ? (Internal ? fn')
+[ CL_Internal fn ⇒ do fn' ← translate_function tmpuniverse globals fn; OK ? (Internal ? fn')
 | CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
 ].
+
+(* TODO: move universe generation to higher level once we do runtime function
+   generation.  Cheating a bit - we only need the new identifiers to be fresh
+   for individual functions. *)
+include "Clight/fresh.ma".
 
 definition clight_to_cminor : clight_program → res Cminor_program ≝
 λp.
+  let tmpuniverse ≝ universe_for_program p in
   let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
   let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
   let globals ≝ fun_globals @ var_globals in
-  transform_partial_program2 ???? (translate_fundef globals) (λi. OK ? (\fst i)) p.
+  transform_partial_program2 ???? (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)) p.