source: src/Clight/fresh.ma @ 1628

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

Show that the universe generated by Clight/fresh.ma is good.

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