| 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 | |
|---|
| 8 | include "Clight/Csyntax.ma". |
|---|
| 9 | |
|---|
| 10 | definition 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 | |
|---|
| 16 | definition max_id_of_env : list (ident × type) → ident ≝ |
|---|
| 17 | foldr ?? (λit,id. max_id (\fst it) id) (an_identifier ? one). |
|---|
| 18 | |
|---|
| 19 | definition 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 | |
|---|
| 22 | definition 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 | |
|---|
| 28 | definition max_id_of_functs : list (ident × clight_fundef) → ident ≝ |
|---|
| 29 | foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef (\snd idf))) id) (an_identifier ? one). |
|---|
| 30 | |
|---|
| 31 | definition max_id_of_globvars : list (ident × region × (list init_data × type)) → ident ≝ |
|---|
| 32 | foldr ?? (λit,id. max_id (\fst (\fst it)) id) (an_identifier ? one). |
|---|
| 33 | |
|---|
| 34 | definition 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 | |
|---|
| 39 | definition 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 | ]. |
|---|
