source: src/Clight/fresh.ma @ 1684

Last change on this file since 1684 was 1629, checked in by campbell, 10 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.