source: src/Clight/fresh.ma @ 2896

Last change on this file since 2896 was 1629, checked in by campbell, 8 years ago

Sort out most of the fresh names stuff in Clight to Cminor.

File size: 4.0 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".
9include "utilities/lists.ma".
10
11definition 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
17definition max_id_of_env : list (ident × type) → ident ≝
18foldr ?? (λit,id. max_id (\fst it) id) (an_identifier ? one).
19
20definition max_id_of_fn : function → ident ≝
21λf. max_id_of_env (fn_params f @ fn_vars f).
22
23definition 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
29definition max_id_of_functs : list (ident × clight_fundef) → ident ≝
30foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef (\snd idf))) id) (an_identifier ? one).
31
32definition max_id_of_globvars : list (ident × region × (list init_data × type)) → ident ≝
33foldr ?? (λit,id. max_id (\fst (\fst it)) id) (an_identifier ? one).
34
35definition 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
40definition 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
46definition 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
52definition 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
55definition 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
62definition 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
65definition 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
73lemma uni_of_max_of : ∀i. fresh_for_univ ? i (universe_of_max i).
74* #i normalize //
75qed.
76
77lemma 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
83lemma 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))
85qed.
86
87
88theorem 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   
Note: See TracBrowser for help on using the repository browser.