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 | include "utilities/lists.ma". |
---|
10 | |
---|
11 | definition max_id : ident → ident → ident ≝ |
---|
12 | λa,b. match a with [ an_identifier a ⇒ |
---|
13 | match b with [ an_identifier b ⇒ |
---|
14 | an_identifier ? (max a b) |
---|
15 | ]]. |
---|
16 | |
---|
17 | definition max_id_of_env : list (ident × type) → ident ≝ |
---|
18 | foldr ?? (λit,id. max_id (\fst it) id) (an_identifier ? one). |
---|
19 | |
---|
20 | definition max_id_of_fn : function → ident ≝ |
---|
21 | λf. max_id_of_env (fn_params f @ fn_vars f). |
---|
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 ≝ |
---|
30 | foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef (\snd idf))) id) (an_identifier ? one). |
---|
31 | |
---|
32 | definition max_id_of_globvars : list (ident × region × (list init_data × type)) → ident ≝ |
---|
33 | foldr ?? (λit,id. max_id (\fst (\fst it)) id) (an_identifier ? one). |
---|
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 | |
---|
40 | definition universe_of_max : ident → universe SymbolTag ≝ |
---|
41 | λmx. match mx with [ an_identifier i ⇒ |
---|
42 | let next ≝ succ i in |
---|
43 | mk_universe SymbolTag next |
---|
44 | ]. |
---|
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 | |
---|
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 | |
---|
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 ∧ |
---|
69 | globals_fresh_for_univ ? (prog_vars ?? p) u. |
---|
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 | |
---|