[1207] | 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". |
---|
[1629] | 9 | include "utilities/lists.ma". |
---|
[1207] | 10 | |
---|
| 11 | definition max_id : ident → ident → ident ≝ |
---|
| 12 | λa,b. match a with [ an_identifier a ⇒ |
---|
| 13 | match b with [ an_identifier b ⇒ |
---|
[1515] | 14 | an_identifier ? (max a b) |
---|
[1207] | 15 | ]]. |
---|
| 16 | |
---|
| 17 | definition max_id_of_env : list (ident × type) → ident ≝ |
---|
[1515] | 18 | foldr ?? (λit,id. max_id (\fst it) id) (an_identifier ? one). |
---|
[1207] | 19 | |
---|
| 20 | definition max_id_of_fn : function → ident ≝ |
---|
[1628] | 21 | λf. max_id_of_env (fn_params f @ fn_vars f). |
---|
[1207] | 22 | |
---|
| 23 | definition max_id_of_fundef : clight_fundef → ident ≝ |
---|
| 24 | λf. match f with |
---|
| 25 | [ CL_Internal f ⇒ max_id_of_fn f |
---|
| 26 | | CL_External id _ _ ⇒ id |
---|
| 27 | ]. |
---|
| 28 | |
---|
| 29 | definition max_id_of_functs : list (ident × clight_fundef) → ident ≝ |
---|
[1515] | 30 | foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef (\snd idf))) id) (an_identifier ? one). |
---|
[1207] | 31 | |
---|
| 32 | definition max_id_of_globvars : list (ident × region × (list init_data × type)) → ident ≝ |
---|
[1515] | 33 | foldr ?? (λit,id. max_id (\fst (\fst it)) id) (an_identifier ? one). |
---|
[1207] | 34 | |
---|
| 35 | definition max_id_of_program : clight_program → ident ≝ |
---|
| 36 | λp. max_id (max_id (max_id_of_functs (prog_funct ?? p)) |
---|
| 37 | (prog_main ?? p)) |
---|
| 38 | (max_id_of_globvars (prog_vars ?? p)). |
---|
| 39 | |
---|
[1628] | 40 | definition universe_of_max : ident → universe SymbolTag ≝ |
---|
| 41 | λmx. match mx with [ an_identifier i ⇒ |
---|
[1515] | 42 | let next ≝ succ i in |
---|
| 43 | mk_universe SymbolTag next |
---|
[1207] | 44 | ]. |
---|
[1628] | 45 | |
---|
| 46 | definition universe_for_program : clight_program → universe SymbolTag ≝ |
---|
| 47 | λp. universe_of_max (max_id_of_program p). |
---|
| 48 | |
---|
| 49 | |
---|
| 50 | (* A specification for the result *) |
---|
| 51 | |
---|
| 52 | definition fn_fresh_for_univ : function → universe SymbolTag → Prop ≝ |
---|
| 53 | λf,u. All ? (λit. fresh_for_univ ? (\fst it) u) (fn_params f @ fn_vars f). |
---|
| 54 | |
---|
| 55 | definition fd_fresh_for_univ : clight_fundef → universe SymbolTag → Prop ≝ |
---|
| 56 | λfd,u. |
---|
| 57 | match fd with |
---|
| 58 | [ CL_Internal f ⇒ fn_fresh_for_univ f u |
---|
| 59 | | CL_External id _ _ ⇒ fresh_for_univ ? id u |
---|
| 60 | ]. |
---|
| 61 | |
---|
[1629] | 62 | definition globals_fresh_for_univ : ∀V:Type[0]. list (ident × region × V) → universe SymbolTag → Prop ≝ |
---|
| 63 | λV,gl,u. All ? (λv. fresh_for_univ ? (\fst (\fst v)) u) gl. |
---|
| 64 | |
---|
[1628] | 65 | definition prog_fresh_for_univ : clight_program → universe SymbolTag → Prop ≝ |
---|
| 66 | λp,u. |
---|
| 67 | All ? (λifd. fresh_for_univ ? (\fst ifd) u ∧ fd_fresh_for_univ (\snd ifd) u) (prog_funct ?? p) ∧ |
---|
| 68 | fresh_for_univ ? (prog_main ?? p) u ∧ |
---|
[1629] | 69 | globals_fresh_for_univ ? (prog_vars ?? p) u. |
---|
[1628] | 70 | |
---|
| 71 | (* And they match up. *) |
---|
| 72 | |
---|
| 73 | lemma uni_of_max_of : ∀i. fresh_for_univ ? i (universe_of_max i). |
---|
| 74 | * #i normalize // |
---|
| 75 | qed. |
---|
| 76 | |
---|
| 77 | lemma uni_max_l : ∀i,j,k. fresh_for_univ ? i (universe_of_max j) → fresh_for_univ ? i (universe_of_max (max_id j k)). |
---|
| 78 | * #i * #j * #k normalize @leb_elim normalize |
---|
| 79 | [ #H #H' @(transitive_le … (succ j)) /2/ |
---|
| 80 | | /2/ |
---|
| 81 | ] qed. |
---|
| 82 | |
---|
| 83 | lemma uni_max_r : ∀i,j,k. fresh_for_univ ? i (universe_of_max k) → fresh_for_univ ? i (universe_of_max (max_id j k)). |
---|
| 84 | * #i * #j * #k whd in ⊢ (? → ???(?%)); >commutative_max @(uni_max_l ? (an_identifier ? k) (an_identifier ? j)) |
---|
| 85 | qed. |
---|
| 86 | |
---|
| 87 | |
---|
| 88 | theorem prog_fresh : ∀p. prog_fresh_for_univ p (universe_for_program p). |
---|
| 89 | * #vars #fns #main |
---|
| 90 | % |
---|
| 91 | [ % |
---|
| 92 | [ @All_alt * #id #fd #pre #post #Efns % |
---|
| 93 | [ @uni_max_l @uni_max_l >Efns elim pre |
---|
| 94 | [ @uni_max_l @uni_max_l // |
---|
| 95 | | #x #y #H @uni_max_r @H |
---|
| 96 | ] |
---|
| 97 | | cases fd in Efns ⊢ %; |
---|
| 98 | [ #fn #Efns @All_alt >Efns * #id' #ty #envpre #envpost #Eenv |
---|
| 99 | @uni_max_l @uni_max_l elim pre |
---|
| 100 | [ @uni_max_l @uni_max_r |
---|
| 101 | whd in ⊢ (???(?%)); >Eenv elim envpre |
---|
| 102 | [ @uni_max_l // |
---|
| 103 | | #x #y #H @uni_max_r // |
---|
| 104 | ] |
---|
| 105 | | #x #y #H @uni_max_r @H |
---|
| 106 | ] |
---|
| 107 | | #id' #tys #ty #Efn >Efn |
---|
| 108 | @uni_max_l @uni_max_l elim pre |
---|
| 109 | [ @uni_max_l @uni_max_r // |
---|
| 110 | | #x #y #H @uni_max_r @H |
---|
| 111 | ] |
---|
| 112 | ] |
---|
| 113 | ] |
---|
| 114 | | @uni_max_l @uni_max_r // |
---|
| 115 | ] |
---|
| 116 | | @All_alt * * #id #r #init #pre #post #E @uni_max_r >E elim pre |
---|
| 117 | [ @uni_max_l // |
---|
| 118 | | #x #y #H @uni_max_r @H |
---|
| 119 | ] |
---|
| 120 | ] qed. |
---|
| 121 | |
---|
| 122 | |
---|