source: src/Clight/fresh.ma @ 1515

Last change on this file since 1515 was 1515, checked in by campbell, 10 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 1.6 KB
Line 
1(* In order to generate fresh names for Clight programs we find the largest
2   identifier used in the program, then set up a universe based on that.
3   
4   NB: This only considers variables and function names.  Goto labels and
5       field idents are ignored.
6 *)
7
8include "Clight/Csyntax.ma".
9
10definition max_id : ident → ident → ident ≝
11λa,b. match a with [ an_identifier a ⇒
12      match b with [ an_identifier b ⇒
13        an_identifier ? (max a b)
14      ]].
15
16definition max_id_of_env : list (ident × type) → ident ≝
17foldr ?? (λit,id. max_id (\fst it) id) (an_identifier ? one).
18
19definition max_id_of_fn : function → ident ≝
20λf. max_id (max_id_of_env (fn_params f)) (max_id_of_env (fn_vars f)).
21
22definition max_id_of_fundef : clight_fundef → ident ≝
23λf. match f with
24  [ CL_Internal f ⇒ max_id_of_fn f
25  | CL_External id _ _ ⇒ id
26  ].
27
28definition max_id_of_functs : list (ident × clight_fundef) → ident ≝
29foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef (\snd idf))) id) (an_identifier ? one).
30
31definition max_id_of_globvars : list (ident × region × (list init_data × type)) → ident ≝
32foldr ?? (λit,id. max_id (\fst (\fst it)) id) (an_identifier ? one).
33
34definition max_id_of_program : clight_program → ident ≝
35λp. max_id (max_id (max_id_of_functs (prog_funct ?? p))
36                   (prog_main ?? p))
37           (max_id_of_globvars (prog_vars ?? p)).
38
39definition universe_for_program : clight_program → universe SymbolTag ≝
40λp. match max_id_of_program p with [ an_identifier i ⇒
41      let next ≝ succ i in
42      mk_universe SymbolTag next
43    ].
Note: See TracBrowser for help on using the repository browser.