source: src/Clight/fresh.ma @ 1603

Last change on this file since 1603 was 1515, checked in by campbell, 8 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.