Changeset 1207


Ignore:
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:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r961 r1207  
    319319alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
    320320
     321definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
     322definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
     323definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
     324definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
     325
    321326definition bitvector_of_bool:
    322327      ∀n: nat. ∀b: bool. BitVector (S n) ≝
  • src/Clight/toCminor.ma

    r1206 r1207  
    660660  ]) (OK ? s) params.
    661661
    662 definition bigu ≝ mk_universe SymbolTag [[
    663 false;true;false;false;
    664 false;false;false;false;
    665 false;false;false;false;
    666 false;false;false;false]] false.
    667 
    668 (* FIXME: the temporary handling is a bit dodgy, I'm afraid. *)
    669 definition translate_function : list (ident×region) → function → res internal_function ≝
    670 λglobals, f.
     662definition translate_function : universe SymbolTag → list (ident×region) → function → res internal_function ≝
     663λtmpuniverse, globals, f.
    671664  let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in
    672   let tmp ≝ mk_tmpgen bigu [ ] in (* FIXME *)
     665  let tmp ≝ mk_tmpgen tmpuniverse [ ] in
    673666  do 〈s,tmp〉 ← translate_statement vartypes tmp (fn_body f);
    674667  do s ← alloc_params vartypes (fn_params f) s;
     
    680673    s).
    681674
    682 definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝
    683 λglobals,f.
     675definition translate_fundef : universe SymbolTag → list (ident×region) → clight_fundef → res (fundef internal_function) ≝
     676λtmpuniverse,globals,f.
    684677match f with
    685 [ CL_Internal fn ⇒ do fn' ← translate_function globals fn; OK ? (Internal ? fn')
     678[ CL_Internal fn ⇒ do fn' ← translate_function tmpuniverse globals fn; OK ? (Internal ? fn')
    686679| CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
    687680].
     681
     682(* TODO: move universe generation to higher level once we do runtime function
     683   generation.  Cheating a bit - we only need the new identifiers to be fresh
     684   for individual functions. *)
     685include "Clight/fresh.ma".
    688686
    689687definition clight_to_cminor : clight_program → res Cminor_program ≝
    690688λp.
     689  let tmpuniverse ≝ universe_for_program p in
    691690  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
    692691  let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
    693692  let globals ≝ fun_globals @ var_globals in
    694   transform_partial_program2 ???? (translate_fundef globals) (λi. OK ? (\fst i)) p.
     693  transform_partial_program2 ???? (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)) p.
Note: See TracChangeset for help on using the changeset viewer.