[2532] | 1 | (* include "joint/TranslateUtils.ma". *) |
---|
| 2 | include "joint/Joint.ma". |
---|
[2200] | 3 | include "utilities/hide.ma". |
---|
[2182] | 4 | |
---|
| 5 | definition graph_to_lin_statement : |
---|
[2784] | 6 | ∀p : uns_params.∀globals. |
---|
[2532] | 7 | ∀A.identifier_map LabelTag A → |
---|
[2182] | 8 | joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝ |
---|
[2532] | 9 | λp,globals,A,visited,stmt. |
---|
| 10 | match stmt return λ_.joint_statement (mk_lin_params ?) ? with |
---|
| 11 | [ sequential c nxt ⇒ |
---|
| 12 | match c with |
---|
| 13 | [ COND a ltrue ⇒ |
---|
| 14 | if nxt ∈ visited then FCOND … I a ltrue nxt else |
---|
| 15 | sequential (mk_lin_params p) … c it |
---|
[2562] | 16 | | _ ⇒ sequential (mk_lin_params p) … c it |
---|
[2532] | 17 | ] |
---|
[2182] | 18 | | final c ⇒ final … c |
---|
[2532] | 19 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
[2182] | 20 | ]. |
---|
| 21 | |
---|
[2532] | 22 | (* |
---|
[2182] | 23 | lemma graph_to_lin_labels : |
---|
[2784] | 24 | ∀p : uns_params.∀globals,s. |
---|
[2182] | 25 | stmt_labels … (graph_to_lin_statement p globals s) = |
---|
| 26 | stmt_explicit_labels … s. |
---|
| 27 | #p#globals * [//] * // |
---|
| 28 | qed. |
---|
[2532] | 29 | *) |
---|
[2182] | 30 | |
---|
| 31 | (* discard all elements passing test, return first element failing it *) |
---|
| 32 | (* and the rest of the list, if any. *) |
---|
| 33 | let rec chop A (test : A → bool) (l : list A) on l : option (A × (list A)) ≝ |
---|
| 34 | match l with |
---|
| 35 | [ nil ⇒ None ? |
---|
| 36 | | cons x l' ⇒ if test x then chop A test l' else return 〈x, l'〉 |
---|
| 37 | ]. |
---|
| 38 | |
---|
| 39 | lemma chop_ok : ∀A,f,l. |
---|
| 40 | match chop A f l with |
---|
| 41 | [ Some pr ⇒ |
---|
| 42 | let x ≝ \fst pr in |
---|
| 43 | let post ≝ \snd pr in |
---|
| 44 | ∃pre.All ? (λx.bool_to_Prop (f x)) pre ∧ |
---|
| 45 | l = pre @ x :: post ∧ ¬bool_to_Prop (f x) |
---|
| 46 | | None ⇒ All A (λx.bool_to_Prop (f x)) l |
---|
| 47 | ]. |
---|
| 48 | #A #f #l elim l |
---|
| 49 | [ % |
---|
| 50 | | #hd #tl #IH whd in match (chop ???); |
---|
| 51 | elim (true_or_false_Prop (f hd)) #H >H normalize nodelta |
---|
| 52 | [ lapply IH elim (chop ???) normalize nodelta |
---|
| 53 | [ #G %{H G} |
---|
| 54 | | #pr * #pre ** #H1 #H2 #H3 %{(hd :: pre)} %{H3} % |
---|
| 55 | [ %{H H1} |
---|
| 56 | | >H2 % |
---|
| 57 | ] |
---|
| 58 | ] |
---|
| 59 | | %{[ ]} %{H} %% |
---|
| 60 | ] |
---|
| 61 | ] |
---|
| 62 | qed. |
---|
| 63 | |
---|
| 64 | unification hint 0 ≔ p, globals; |
---|
| 65 | lp ≟ lin_params_to_params p, |
---|
| 66 | sp ≟ stmt_pars lp, |
---|
| 67 | js ≟ joint_statement sp globals, |
---|
| 68 | lo ≟ labelled_obj LabelTag js |
---|
| 69 | (*----------------------------*)⊢ |
---|
| 70 | list lo ≡ codeT lp globals. |
---|
| 71 | |
---|
| 72 | definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals. |
---|
| 73 | λentry : label. |
---|
| 74 | (Σ〈visited' : identifier_map LabelTag ℕ, |
---|
| 75 | required' : identifier_set LabelTag, |
---|
| 76 | generated' : codeT (mk_lin_params p) globals〉.'hide ( |
---|
| 77 | And (And (And (And |
---|
| 78 | (lookup ?? visited' entry = Some ? 0) |
---|
| 79 | (required' ⊆ visited')) |
---|
[2532] | 80 | ((∃last.stmt_at … generated' 0 = Some ? (final … last)) ∨ |
---|
| 81 | (∃a,ltrue,lfalse.stmt_at … generated' 0 = Some ? (FCOND … I a ltrue lfalse)))) |
---|
[2182] | 82 | (code_forall_labels … (λl.bool_to_Prop (l∈required')) (rev … generated'))) |
---|
| 83 | (∀l,n.lookup ?? visited' l = Some ? n → |
---|
| 84 | And (bool_to_Prop (code_has_label … (rev ? generated') l)) |
---|
[2532] | 85 | (∃s.And |
---|
[2182] | 86 | (lookup … g l = Some ? s) |
---|
[2532] | 87 | (match s with |
---|
| 88 | [ sequential s' nxt ⇒ |
---|
| 89 | match s' with |
---|
[2562] | 90 | [ COND a ltrue ⇒ |
---|
| 91 | Or |
---|
| 92 | (And (nth_opt … n (rev … generated') = |
---|
| 93 | Some ? 〈Some ? l, sequential … (COND … a ltrue) it〉) |
---|
| 94 | (lookup … visited' nxt = Some ? (S n))) |
---|
| 95 | (nth_opt … n (rev … generated') = |
---|
| 96 | Some ? 〈Some ? l, FCOND … I a ltrue nxt〉) |
---|
| 97 | | _ ⇒ |
---|
[2532] | 98 | And |
---|
| 99 | (nth_opt … n (rev … generated') = |
---|
| 100 | Some ? 〈Some ? l, sequential … s' it〉) |
---|
| 101 | (Or (lookup … visited' nxt = Some ? (S n)) |
---|
| 102 | (nth_opt … (S n) (rev … generated') = |
---|
| 103 | Some ? 〈None ?, GOTO … nxt〉)) |
---|
[2562] | 104 | |
---|
[2532] | 105 | ] |
---|
| 106 | | final s' ⇒ |
---|
| 107 | nth_opt … n (rev … generated') = |
---|
| 108 | Some ? 〈Some ? l, final … s'〉 |
---|
| 109 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
| 110 | ]))))). |
---|
[2182] | 111 | |
---|
| 112 | unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit. |
---|
| 113 | |
---|
| 114 | include alias "common/Identifiers.ma". |
---|
| 115 | |
---|
| 116 | lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf. |
---|
[2532] | 117 | (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf) ≝ |
---|
| 118 | λtag,A,P,m,i,prf,H.(H … (lookup_eq_safe …)). |
---|
[2182] | 119 | |
---|
| 120 | let rec graph_visit |
---|
[2784] | 121 | (p : uns_params) |
---|
[2182] | 122 | (globals: list ident) |
---|
| 123 | (g : codeT (mk_graph_params p) globals) |
---|
| 124 | (* = graph (joint_statement (mk_graph_params p) globals *) |
---|
| 125 | (required: identifier_set LabelTag) |
---|
| 126 | (visited: identifier_map LabelTag ℕ) (* the reversed index of labels in the new code *) |
---|
| 127 | (generated: codeT (mk_lin_params p) globals) |
---|
| 128 | (* ≝ list ((option label)×(joint_statement (mk_lin_params p) globals)) *) |
---|
| 129 | (visiting: list label) |
---|
| 130 | (gen_length : ℕ) |
---|
| 131 | (n: nat) |
---|
| 132 | (entry : label) |
---|
| 133 | (g_prf : code_closed … g) |
---|
| 134 | (required_prf1 : ∀i.i∈required → Or (In ? visiting i) (bool_to_Prop (i∈visited))) |
---|
| 135 | (required_prf2 : code_forall_labels … (λl.bool_to_Prop (l ∈ required)) (rev … generated)) |
---|
| 136 | (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop ( |
---|
| 137 | And (bool_to_Prop (code_has_label … (rev ? generated) l)) |
---|
[2532] | 138 | (∃s.And |
---|
[2182] | 139 | (lookup … g l = Some ? s) |
---|
[2532] | 140 | (match s with |
---|
| 141 | [ sequential s' nxt ⇒ |
---|
| 142 | match s' with |
---|
[2562] | 143 | [ COND a ltrue ⇒ |
---|
[2532] | 144 | Or |
---|
| 145 | (And (nth_opt … n (rev … generated) = |
---|
| 146 | Some ? 〈Some ? l, sequential … (COND … a ltrue) it〉) |
---|
| 147 | (match lookup … visited nxt with |
---|
| 148 | [ Some n' ⇒ n' = S n |
---|
| 149 | | None ⇒ And (nth_opt ? 0 visiting = Some ? nxt) (S n = gen_length) |
---|
| 150 | ])) |
---|
| 151 | (nth_opt … n (rev … generated) = |
---|
| 152 | Some ? 〈Some ? l, FCOND … I a ltrue nxt〉) |
---|
[2562] | 153 | | _ ⇒ |
---|
| 154 | And |
---|
| 155 | (nth_opt … n (rev … generated) = |
---|
| 156 | Some ? 〈Some ? l, sequential … s' it〉) |
---|
| 157 | (match lookup … visited nxt with |
---|
| 158 | [ Some n' ⇒ Or (n' = S n) (nth_opt … (S n) (rev … generated) = Some ? 〈None ?, GOTO … nxt〉) |
---|
| 159 | | None ⇒ And (nth_opt ? 0 visiting = Some ? nxt) (S n = gen_length) |
---|
| 160 | ]) |
---|
[2532] | 161 | ] |
---|
| 162 | | final s' ⇒ |
---|
| 163 | nth_opt … n (rev … generated) = |
---|
| 164 | Some ? 〈Some ? l, final … s'〉 |
---|
| 165 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
| 166 | ])))) |
---|
[2182] | 167 | (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated)) |
---|
| 168 | (generated_prf3 : (∃last.stmt_at … generated 0 = Some ? (final … last)) ∨ |
---|
[2532] | 169 | (∃a,ltrue,lfalse.stmt_at … generated 0 = Some ? (FCOND … a ltrue lfalse)) ∨ |
---|
[2182] | 170 | (¬All ? (λx.bool_to_Prop (x∈visited)) visiting)) |
---|
| 171 | (visiting_prf : All … (λl.bool_to_Prop (l∈g)) visiting) |
---|
| 172 | (gen_length_prf : gen_length = length ? generated) |
---|
| 173 | (entry_prf : Or (And (And (visiting = [entry]) (gen_length = 0)) (Not (bool_to_Prop (entry∈visited)))) |
---|
| 174 | (lookup … visited entry = Some ? 0)) |
---|
| 175 | (n_prf : le (id_map_size … g) (plus n (id_map_size … visited))) |
---|
| 176 | on n |
---|
| 177 | : graph_visit_ret_type … g entry ≝ |
---|
| 178 | match chop ? (λx.x∈visited) visiting |
---|
| 179 | return λx.? → graph_visit_ret_type … g entry with |
---|
| 180 | [ None ⇒ λH. |
---|
| 181 | «〈visited, required, generated〉, ?» |
---|
| 182 | | Some pr ⇒ λH. |
---|
| 183 | let vis_hd ≝ \fst pr in |
---|
| 184 | let vis_tl ≝ \snd pr in |
---|
| 185 | match n return λx.? → graph_visit_ret_type … g entry with |
---|
| 186 | [ O ⇒ λn_prf'.⊥ |
---|
| 187 | | S n' ⇒ λn_prf'. |
---|
| 188 | (* add the label to the visited ones *) |
---|
| 189 | let visited' ≝ add … visited vis_hd gen_length in |
---|
| 190 | (* take l's statement *) |
---|
| 191 | let hd_vis_in_g ≝ (hide_prf ? ?) in |
---|
| 192 | let statement ≝ lookup_safe ?? g vis_hd hd_vis_in_g in |
---|
| 193 | (* translate it to its linear version *) |
---|
[2532] | 194 | let translated_statement ≝ graph_to_lin_statement … visited' statement in |
---|
[2182] | 195 | (* add the translated statement to the code (which will be reversed later) *) |
---|
| 196 | let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in |
---|
[2532] | 197 | let required' ≝ union_set ??? |
---|
| 198 | (set_from_list … (stmt_explicit_labels … translated_statement)) |
---|
| 199 | required in |
---|
[2182] | 200 | (* put successors in the visiting worklist *) |
---|
| 201 | let visiting' ≝ stmt_labels … statement @ vis_tl in |
---|
| 202 | (* finally, check the implicit successor *) |
---|
| 203 | (* if it has been already visited, we need to add a GOTO *) |
---|
| 204 | let add_req_gen ≝ |
---|
[2532] | 205 | match statement with |
---|
| 206 | [ sequential s nxt ⇒ |
---|
| 207 | match s with |
---|
| 208 | [ COND _ _ ⇒ 〈0, ∅, [ ]〉 |
---|
| 209 | | _ ⇒ |
---|
| 210 | if nxt ∈ visited' then |
---|
| 211 | 〈1, {(nxt)}, [〈None label, (GOTO … nxt : joint_statement ??)〉]〉 |
---|
| 212 | else 〈0, ∅, [ ]〉 |
---|
| 213 | ] |
---|
| 214 | | _ ⇒ 〈0, ∅, [ ]〉 |
---|
[2182] | 215 | ] in |
---|
| 216 | (* prepare a common utility to deal with add_req_gen *) |
---|
| 217 | let add_req_gen_prf : |
---|
| 218 | ∀P : (ℕ × (identifier_set LabelTag) × (codeT (mk_lin_params p) globals)) → Prop. |
---|
[2532] | 219 | (match statement with |
---|
| 220 | [ sequential s nxt ⇒ |
---|
| 221 | match s with [ COND _ _ ⇒ True | _ ⇒ ¬bool_to_Prop (nxt ∈ visited') ] |
---|
| 222 | | _ ⇒ True] → P 〈0,∅,[ ]〉) → |
---|
[2562] | 223 | (∀nxt.match statement with |
---|
| 224 | [ sequential s nxt' ⇒ |
---|
| 225 | match s with [ COND _ _ ⇒ False | _ ⇒ |
---|
| 226 | nxt = nxt'] |
---|
| 227 | | _ ⇒ False] |
---|
| 228 | → nxt ∈ visited' → P 〈1, {(nxt)}, [〈None ?, GOTO (mk_lin_params p) nxt〉]〉) → |
---|
[2182] | 229 | P add_req_gen ≝ hide_prf ?? in |
---|
| 230 | graph_visit ??? |
---|
| 231 | (union_set ??? (\snd (\fst add_req_gen)) required') |
---|
| 232 | visited' |
---|
| 233 | (\snd add_req_gen @ generated') |
---|
| 234 | visiting' |
---|
| 235 | (plus (\fst (\fst add_req_gen)) (S gen_length)) |
---|
| 236 | n' entry g_prf ????????? |
---|
| 237 | ] n_prf |
---|
| 238 | ] (chop_ok ? (λx.x∈visited) visiting). |
---|
[2823] | 239 | cases daemon (*) |
---|
[2182] | 240 | whd |
---|
| 241 | [ (* base case, visiting is all visited *) |
---|
| 242 | %[%[%[%]]] |
---|
| 243 | [ elim entry_prf |
---|
| 244 | [ ** #eq_visiting #gen_length_O #entry_vis >eq_visiting in H; * >entry_vis * |
---|
| 245 | | // |
---|
| 246 | ] |
---|
| 247 | | #l #l_req |
---|
| 248 | elim (required_prf1 … l_req) #G |
---|
| 249 | [ @(All_In … H G) |
---|
| 250 | | assumption |
---|
| 251 | ] |
---|
[2532] | 252 | | cases generated_prf3 [/2 by /] |
---|
[2182] | 253 | * #ABS @⊥ @ABS assumption |
---|
| 254 | | assumption |
---|
[2532] | 255 | | #l #n #H elim (generated_prf1 … H) -H |
---|
| 256 | #H1 * #s * #H2 #H3 %{H1} %{s} %{H2} |
---|
| 257 | cases s in H3; [3: *] |
---|
| 258 | [ * ] normalize nodelta |
---|
[2708] | 259 | [1,2,4: [ #c | #f #args #dest |#s'] #nxt * #EQnth_opt #H %{EQnth_opt} |
---|
| 260 | inversion (lookup … visited nxt) in H; [2,4,6: #n'] normalize nodelta |
---|
| 261 | #EQlookup |
---|
[2182] | 262 | normalize nodelta * |
---|
[2708] | 263 | [1,3,5: #EQn' %1 >EQn' % |
---|
| 264 | |2,4,6: #H %2{H} |
---|
| 265 | |*: #H' lapply (All_nth … H … H') |
---|
[2532] | 266 | whd in ⊢ (?%→?); >EQlookup * |
---|
[2182] | 267 | ] |
---|
[2708] | 268 | | #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1} |
---|
[2532] | 269 | inversion (lookup … visited lfalse) in H2; |
---|
| 270 | [ #ABS * #H' lapply (All_nth … H … H') |
---|
| 271 | whd in ⊢ (?%→?); >ABS * |
---|
| 272 | | #n' #_ normalize nodelta #EQ >EQ % |
---|
| 273 | ] |
---|
[2708] | 274 | | #s #H @H |
---|
[2182] | 275 | ] |
---|
| 276 | ] |
---|
| 277 | (* first, close goals where add_gen_req plays no role *) |
---|
| 278 | |13: (* vis_hd is in g *) |
---|
| 279 | elim H #pre ** #_ #H2 #_ |
---|
| 280 | @(All_split … visiting_prf … H2) |
---|
| 281 | |2: (* n = 0 absrud *) |
---|
| 282 | elim H #pre ** #_ #H2 #H3 |
---|
| 283 | @(absurd … n_prf') |
---|
| 284 | @lt_to_not_le |
---|
| 285 | lapply (add_size … visited vis_hd 0 (* dummy value *)) |
---|
| 286 | >H3 normalize nodelta |
---|
| 287 | whd in match (lt ? ?); |
---|
| 288 | whd in match (1 + ?); |
---|
| 289 | #EQ <EQ @subset_card @add_subset |
---|
| 290 | [ @(All_split ? (λx.bool_to_Prop (x∈g)) ????? H2) @(All_mp … visiting_prf) |
---|
| 291 | #a elim g #gm whd in ⊢ (?→?%); #H >(lookup_eq_safe … H) % |
---|
| 292 | | #l #H |
---|
[2532] | 293 | elim (generated_prf1 … (lookup_eq_safe … H)) #_ * #s * #s_in_g #_ |
---|
[2182] | 294 | whd in ⊢ (?%); >s_in_g % |
---|
| 295 | ] |
---|
| 296 | |8: |
---|
| 297 | elim H #pre ** #_ #H2 #_ |
---|
| 298 | @All_append |
---|
| 299 | [ elim(g_prf … vis_hd statement ?) [2:@lookup_eq_safe] #G1 #G2 |
---|
| 300 | @(All_append … G1) |
---|
[2532] | 301 | cases statement in G2; [2: // |3: * ] |
---|
| 302 | #s #nxt #G' %{G'} % |
---|
[2182] | 303 | | >H2 in visiting_prf; |
---|
| 304 | #H' lapply (All_append_r … H') -H' * #_ // |
---|
| 305 | ] |
---|
| 306 | |10: |
---|
| 307 | elim H #pre ** #_ #H2 #H3 -add_req_gen_prf |
---|
| 308 | %2 elim entry_prf |
---|
| 309 | [ ** >H2 cases pre |
---|
| 310 | [2: #x' #pre' #ABS normalize in ABS; destruct(ABS) |
---|
| 311 | cases pre' in e0; [2: #x'' #pre''] #ABS' normalize in ABS'; destruct(ABS') |
---|
| 312 | |1: #EQ normalize in EQ; destruct(EQ) |
---|
| 313 | #eq_gen_length #_ |
---|
| 314 | >lookup_add_hit >eq_gen_length % |
---|
| 315 | ] |
---|
| 316 | | #lookup_entry cut (entry ≠ vis_hd) |
---|
| 317 | [ % whd in match vis_hd; #entry_vis_hd <entry_vis_hd in H3; |
---|
| 318 | whd in ⊢ (?(?%)→?); >lookup_entry * #ABS @ABS % ] |
---|
| 319 | #entry_not_vis_hd >(lookup_add_miss ?????? entry_not_vis_hd) assumption |
---|
| 320 | ] |
---|
| 321 | |11: |
---|
| 322 | elim H #pre ** #_ #_ #H3 |
---|
| 323 | >commutative_plus |
---|
| 324 | >add_size >H3 normalize nodelta |
---|
| 325 | whd in match (1 + ?); |
---|
| 326 | >commutative_plus |
---|
| 327 | assumption |
---|
| 328 | |12: (* add_req_gen utility *) |
---|
| 329 | #P whd in match add_req_gen; |
---|
[2708] | 330 | cases statement [ * [ #cost | #f #args #dest| #a #ltrue | #s ] #nxt | #s | * ] |
---|
| 331 | normalize nodelta |
---|
| 332 | [3,5: #H #_ @(H I) ] |
---|
| 333 | inversion (nxt ∈ visited') #EQ normalize nodelta |
---|
| 334 | #H1 #H2 [1,3,5: @(H2 … (refl …)) >EQ % |*: @H1 % * ] |
---|
[2532] | 335 | |3: elim H #pre ** #H1 #H2 #_ |
---|
[2182] | 336 | #i >mem_set_union |
---|
| 337 | #H elim (orb_Prop_true … H) -H |
---|
| 338 | [ @add_req_gen_prf [ #_ >mem_set_empty * ] |
---|
[2562] | 339 | #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption |
---|
[2182] | 340 | | >mem_set_union |
---|
[2708] | 341 | #H elim (orb_Prop_true … H) -H |
---|
[2532] | 342 | [ #i_expl %1 @Exists_append_l |
---|
| 343 | lapply i_expl whd in match translated_statement; |
---|
[2708] | 344 | cases statement [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | *] |
---|
| 345 | normalize nodelta #H |
---|
[2532] | 346 | lapply (mem_list_as_set … H) -H #H |
---|
[2708] | 347 | [1,2,4,5: @Exists_append_r assumption ] |
---|
[2532] | 348 | cases (nxt ∈ visited') in H; normalize nodelta * [2,4: * [2: * ]] |
---|
| 349 | #EQ destruct(EQ) [ %1 % |*: %2 %1 % ] |
---|
[2182] | 350 | | (* i was already required *) |
---|
| 351 | #i_req |
---|
| 352 | elim (required_prf1 … i_req) |
---|
| 353 | [ >H2 #H elim (Exists_append … H) -H |
---|
| 354 | [ (* i in preamble → i∈visited *) |
---|
| 355 | #i_pre %2 >mem_set_add @orb_Prop_r |
---|
[2532] | 356 | @(All_In … H1 i_pre) |
---|
[2182] | 357 | | * |
---|
| 358 | [ (* i is vis_hd *) |
---|
| 359 | #eq_i >eq_i %2 @mem_set_add_id |
---|
| 360 | | (* i in vis_tl → i∈visiting' *) |
---|
| 361 | #i_post % @Exists_append_r assumption |
---|
| 362 | ] |
---|
| 363 | ] |
---|
| 364 | | (* i in visited *) |
---|
| 365 | #i_vis %2 >mem_set_add @orb_Prop_r assumption |
---|
| 366 | ] |
---|
[2708] | 367 | ] |
---|
[2182] | 368 | ] |
---|
| 369 | |4,5,6: change with reverse in match rev; |
---|
| 370 | >reverse_append whd in match (reverse ??); >rev_append_def |
---|
| 371 | >associative_append |
---|
| 372 | [ #pt #s |
---|
| 373 | @(leb_elim (S pt) (|generated|)) #cmp |
---|
| 374 | whd in match (stmt_at ????); |
---|
| 375 | [ >nth_opt_append_l [2: >length_reverse assumption ] |
---|
| 376 | change with (stmt_at ???? = ? → ?) |
---|
| 377 | #EQ lapply(required_prf2 … EQ) @All_mp |
---|
| 378 | #l #l_req >mem_set_union @orb_Prop_r |
---|
| 379 | >mem_set_union @orb_Prop_r @l_req |
---|
| 380 | | >nth_opt_append_r [2: >length_reverse @not_lt_to_le assumption ] |
---|
| 381 | cases (pt - ?) |
---|
| 382 | [ whd in match (nth_opt ???); whd in ⊢ (??%?→?); |
---|
[2532] | 383 | #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ) whd |
---|
[2182] | 384 | whd in match required'; |
---|
[2532] | 385 | cut (∀p : lin_params.∀globals.∀s. |
---|
| 386 | stmt_implicit_label p globals s = None ?) |
---|
| 387 | [ #p #globals * normalize // ] |
---|
| 388 | #lin_implicit_label change with (? @ ?) in match (stmt_labels ???); |
---|
| 389 | >lin_implicit_label |
---|
| 390 | change with (All ?? (stmt_explicit_labels ???)) |
---|
| 391 | generalize in match (stmt_explicit_labels … translated_statement); |
---|
[2182] | 392 | #l @list_as_set_All |
---|
| 393 | #i >mem_set_union >mem_set_union |
---|
[2532] | 394 | #i_l @orb_Prop_r @orb_Prop_l assumption |
---|
[2182] | 395 | | @add_req_gen_prf |
---|
[2562] | 396 | [ #_ | #next #_ #next_vis * |
---|
[2182] | 397 | [ whd in ⊢ (??%?→?); |
---|
| 398 | #EQ' destruct(EQ') whd %{I} >mem_set_union |
---|
| 399 | @orb_Prop_l @mem_set_add_id ]] |
---|
| 400 | #n whd in ⊢ (??%?→?); #ABS destruct(ABS) |
---|
| 401 | ] |
---|
| 402 | ] |
---|
| 403 | | elim H #pre ** #H1 #H2 #H3 |
---|
| 404 | #i whd in match visited'; |
---|
| 405 | @(eq_identifier_elim … i vis_hd) |
---|
| 406 | [ #EQi >EQi -i #pos |
---|
[2532] | 407 | >lookup_add_hit in ⊢ (%→?); #EQpos (* too slow: destruct(EQpos) *) |
---|
[2182] | 408 | cut (gen_length = pos) |
---|
[2532] | 409 | [ -visited destruct(EQpos) %] |
---|
[2182] | 410 | -EQpos #EQpos <EQpos -pos |
---|
| 411 | % |
---|
| 412 | [ >lin_code_has_label |
---|
| 413 | @add_req_gen_prf |
---|
| 414 | [ #_ |
---|
[2562] | 415 | | #next #_ #next_vis |
---|
[2182] | 416 | change with (? @ ([?] @ [?])) in match (? @ [? ; ?]); |
---|
| 417 | <associative_append >occurs_exactly_once_None |
---|
| 418 | ] |
---|
| 419 | >occurs_exactly_once_Some_eq >eq_identifier_refl |
---|
| 420 | normalize nodelta |
---|
| 421 | @generated_prf2 |
---|
| 422 | lapply (in_map_domain … visited vis_hd) |
---|
| 423 | >H3 normalize nodelta // |
---|
[2708] | 424 | | %{statement} |
---|
[2532] | 425 | % |
---|
[2182] | 426 | [ @lookup_eq_safe |
---|
[2532] | 427 | | normalize nodelta |
---|
| 428 | change with statement in match (lookup_safe ?????); |
---|
| 429 | cases statement; |
---|
[2708] | 430 | [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta |
---|
| 431 | [1,2,3,4: inversion (nxt ∈ visited') normalize nodelta #nxt_vis ] |
---|
| 432 | [1,2,3,4,7,8: % | %2 | %1 % ] |
---|
| 433 | [1,3,5,7,9,11,13,14,16: |
---|
[2532] | 434 | >nth_opt_append_r >rev_length <gen_length_prf try % |
---|
[2708] | 435 | <minus_n_n try % try( whd in match graph_to_lin_statement; normalize nodelta |
---|
| 436 | >nxt_vis %) |
---|
[2532] | 437 | |*: |
---|
| 438 | lapply (in_map_domain … visited' nxt) >nxt_vis normalize nodelta |
---|
[2708] | 439 | [1,3,5: * #n' ] #EQlookup >EQlookup normalize nodelta |
---|
| 440 | try (%% @False) |
---|
| 441 | %2 >nth_opt_append_r >rev_length <gen_length_prf [2,4,6: %2 %1 ] |
---|
| 442 | <minus_Sn_n % |
---|
| 443 | ] |
---|
[2182] | 444 | ] |
---|
| 445 | ] |
---|
| 446 | | #NEQ #n_i >(lookup_add_miss … visited … NEQ) |
---|
| 447 | #Hlookup elim (generated_prf1 … Hlookup) |
---|
[2532] | 448 | #G1 * #s * #G2 #G3 |
---|
[2182] | 449 | % |
---|
| 450 | [ >lin_code_has_label <associative_append |
---|
| 451 | >occurs_exactly_once_append |
---|
| 452 | @orb_Prop_l @andb_Prop |
---|
| 453 | [ >occurs_exactly_once_Some_eq |
---|
| 454 | >eq_identifier_false [2: % #ABS >ABS in NEQ; * #ABS' @ABS' % ] |
---|
| 455 | normalize nodelta >lin_code_has_label in G1; #K @K |
---|
| 456 | | @add_req_gen_prf |
---|
[2562] | 457 | [ #_ % | #next #_ #_ % ] |
---|
[2182] | 458 | ] |
---|
| 459 | | %{s} |
---|
[2532] | 460 | %{G2} |
---|
| 461 | cases s in G3; |
---|
[2708] | 462 | [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] |
---|
| 463 | [1,2,4: normalize nodelta #H cases H in ⊢ ?; -H |
---|
| 464 | #EQnth_opt #next_spec % |3: normalize nodelta * [*] #EQnth_opt [#next_spec %1 % | %2] | #EQnth_opt ] |
---|
| 465 | [1,3,5,7,9: @nth_opt_append_hit_l assumption |
---|
| 466 | |2,4,6,8: @(eq_identifier_elim … nxt vis_hd) |
---|
| 467 | [1,3,5,7: #EQ destruct(EQ) >lookup_add_hit whd |
---|
| 468 | [1,2,3: %1] |
---|
[2182] | 469 | lapply (in_map_domain … visited vis_hd) |
---|
[2532] | 470 | >H3 #EQ >EQ in next_spec; * #_ #OK >OK % |
---|
[2708] | 471 | |*: #NEQ' >(lookup_add_miss … visited … NEQ') in |
---|
| 472 | ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); |
---|
| 473 | generalize in match next_spec in ⊢ ?; |
---|
| 474 | inversion (lookup … visited nxt) normalize nodelta |
---|
| 475 | [2,4,6,8: #n'' ] #EQlookup' |
---|
| 476 | [1,2,3: * [1,3,5: #H %1{H} ] #H %2 @nth_opt_append_hit_l assumption |
---|
| 477 | |4: #H @H |
---|
| 478 | |*: * #nxt_visiting @⊥ |
---|
| 479 | >H2 in nxt_visiting; |
---|
[2532] | 480 | cases pre in H1; |
---|
[2708] | 481 | [1,3,5,7: #_ |
---|
[2532] | 482 | |*: #frst #pre_tl * #ABS #_ |
---|
| 483 | ] whd in ⊢ (??%?→?); #EQ destruct(EQ) |
---|
[2708] | 484 | [1,2,3,4: cases NEQ' #ABS cases (ABS ?) % |
---|
| 485 | |*: lapply ABS; whd in ⊢ (?%→?); >EQlookup' * |
---|
[2182] | 486 | ] |
---|
| 487 | ] |
---|
| 488 | ] |
---|
[2708] | 489 | |10: @nth_opt_append_hit_l assumption |
---|
[2182] | 490 | ] |
---|
[2708] | 491 | ] |
---|
[2182] | 492 | ] |
---|
| 493 | | #i whd in match visited'; |
---|
| 494 | @(eq_identifier_elim … i vis_hd) #Heq |
---|
| 495 | [ >Heq >lookup_add_hit #ABS destruct(ABS) ] |
---|
| 496 | >(lookup_add_miss ?????? Heq) |
---|
| 497 | #i_n_vis |
---|
| 498 | >does_not_occur_append @andb_Prop |
---|
| 499 | [ @generated_prf2 assumption |
---|
| 500 | | change with (bool_to_Prop (¬eq_identifier ??? ∧ ?)) |
---|
| 501 | >eq_identifier_false [2: % #ABS <ABS in Heq; * #ABS' @ABS' % ] |
---|
[2708] | 502 | @add_req_gen_prf [ #_ | #s #next #_ ] % |
---|
[2182] | 503 | ] |
---|
| 504 | ] |
---|
| 505 | | @add_req_gen_prf |
---|
[2708] | 506 | [ #K | #next #K #next_vis %1 %1 %{(GOTO … next)} % ] |
---|
[2182] | 507 | whd in match generated'; whd in match translated_statement; |
---|
[2532] | 508 | normalize nodelta |
---|
| 509 | change with statement in match (lookup_safe ?????); |
---|
| 510 | cases statement in K; |
---|
[2708] | 511 | [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s #_ %1 %1 %{s} % | * ] normalize nodelta |
---|
| 512 | [3: #_ cases (true_or_false_Prop (nxt ∈ visited')) #nxt_vis |
---|
[2532] | 513 | [ >nxt_vis normalize nodelta %1 %2 %{a} %{ltrue} %{nxt} % ] |
---|
[2708] | 514 | |*: #nxt_vis ] |
---|
[2532] | 515 | %2 % * >nxt_vis * |
---|
[2182] | 516 | | whd in match generated'; |
---|
[2708] | 517 | @add_req_gen_prf [ #_ | #next #_ #_ ] normalize >gen_length_prf % |
---|
[2532] | 518 | | |
---|
[2708] | 519 | ] |
---|
[2823] | 520 | *) |
---|
[2562] | 521 | qed. |
---|
[2182] | 522 | |
---|
| 523 | (* CSC: The branch compression (aka tunneling) optimization is not implemented |
---|
| 524 | in Matita *) |
---|
| 525 | definition branch_compress |
---|
| 526 | ≝ λp: graph_params.λglobals.λg:codeT p globals. |
---|
| 527 | λentry : Σl.bool_to_Prop (code_has_label … g l).g. |
---|
| 528 | |
---|
| 529 | lemma branch_compress_closed : ∀p,globals,g,l.code_closed ?? g → |
---|
| 530 | code_closed … (branch_compress p globals g l). |
---|
| 531 | #p#globals#g#l#H @H qed. |
---|
| 532 | |
---|
| 533 | lemma branch_compress_has_entry : ∀p,globals,g,l. |
---|
| 534 | code_has_label … (branch_compress p globals g l) l. |
---|
| 535 | #p#globals#g*#l#l_prf @l_prf qed. |
---|
| 536 | |
---|
| 537 | definition filter_labels ≝ λtag,A.λtest : identifier tag → bool.λc : list (labelled_obj tag A). |
---|
| 538 | map ?? |
---|
| 539 | (λs. let 〈l_opt,x〉 ≝ s in |
---|
| 540 | 〈! l ← l_opt ; if test l then return l else None ?, x〉) c. |
---|
| 541 | |
---|
| 542 | lemma does_not_occur_filter_labels : |
---|
| 543 | ∀tag,A,test,id,c. |
---|
| 544 | does_not_occur ?? id (filter_labels tag A test c) = |
---|
| 545 | (does_not_occur ?? id c ∨ ¬ test id). |
---|
| 546 | #tag #A #test #id #c elim c |
---|
| 547 | [ // |
---|
| 548 | | ** [2: #lbl] #s #tl #IH |
---|
| 549 | whd in match (filter_labels ????); normalize nodelta |
---|
| 550 | whd in match (does_not_occur ????) in ⊢ (??%%); |
---|
| 551 | [2: @IH] |
---|
| 552 | normalize in match (! l ← ? ; ?); >IH |
---|
| 553 | @(eq_identifier_elim ?? lbl id) #Heq [<Heq] |
---|
| 554 | elim (test lbl) normalize nodelta |
---|
| 555 | change with (eq_identifier ???) in match (instruction_matches_identifier ????); |
---|
| 556 | [1,2: >eq_identifier_refl [2: >commutative_orb] normalize % |
---|
| 557 | |*: >(eq_identifier_false ??? Heq) normalize nodelta % |
---|
| 558 | ] |
---|
| 559 | ] |
---|
| 560 | qed. |
---|
| 561 | |
---|
| 562 | lemma occurs_exactly_once_filter_labels : |
---|
| 563 | ∀tag,A,test,id,c. |
---|
| 564 | occurs_exactly_once ?? id (filter_labels tag A test c) = |
---|
| 565 | (occurs_exactly_once ?? id c ∧ test id). |
---|
| 566 | #tag #A #test #id #c elim c |
---|
| 567 | [ // |
---|
| 568 | | ** [2: #lbl] #s #tl #IH |
---|
| 569 | whd in match (filter_labels ????); normalize nodelta |
---|
| 570 | whd in match (occurs_exactly_once ????) in ⊢ (??%%); |
---|
| 571 | [2: @IH] |
---|
| 572 | normalize in match (! l ← ? ; ?); >IH |
---|
| 573 | >does_not_occur_filter_labels |
---|
| 574 | @(eq_identifier_elim ?? lbl id) #Heq [<Heq] |
---|
| 575 | elim (test lbl) normalize nodelta |
---|
| 576 | change with (eq_identifier ???) in match (instruction_matches_identifier ????); |
---|
| 577 | [1,2: >eq_identifier_refl >commutative_andb [ >(commutative_andb ? true) >commutative_orb | >(commutative_andb ? false)] normalize % |
---|
| 578 | |*: >(eq_identifier_false ??? Heq) normalize nodelta % |
---|
| 579 | ] |
---|
| 580 | ] |
---|
| 581 | qed. |
---|
| 582 | |
---|
| 583 | lemma nth_opt_filter_labels : ∀tag,A,test,instrs,n. |
---|
| 584 | nth_opt ? n (filter_labels tag A test instrs) = |
---|
| 585 | ! 〈lopt, s〉 ← nth_opt ? n instrs ; |
---|
| 586 | return 〈 ! lbl ← lopt; if test lbl then return lbl else None ?, s〉. |
---|
| 587 | #tag #A #test #instrs elim instrs |
---|
| 588 | [ * [2: #n'] % |
---|
| 589 | | * #lopt #s #tl #IH * [2: #n'] |
---|
| 590 | whd in match (filter_labels ????); normalize nodelta |
---|
| 591 | whd in match (nth_opt ???) in ⊢ (??%%); [>IH] % |
---|
| 592 | ] |
---|
| 593 | qed. |
---|
| 594 | |
---|
| 595 | lemma stmt_at_filter_labels : ∀p : lin_params.∀globals,test.∀c : codeT p globals. |
---|
| 596 | ∀i.stmt_at p globals (filter_labels ?? test c) i = stmt_at p globals c i. |
---|
| 597 | #p#globals#test #c#i |
---|
| 598 | whd in ⊢ (??%%); >nth_opt_filter_labels |
---|
| 599 | elim (nth_opt ???); // |
---|
| 600 | qed. |
---|
| 601 | |
---|
[2570] | 602 | (* spostato in ExtraMonads.ma |
---|
[2182] | 603 | lemma option_bind_inverse : ∀A,B.∀m : option A.∀f : A → option B.∀r. |
---|
| 604 | ! x ← m ; f x = return r → |
---|
| 605 | ∃x.m = return x ∧ f x = return r. |
---|
| 606 | #A #B * normalize [2:#x] #f #r #EQ destruct |
---|
| 607 | %{x} %{EQ} % |
---|
| 608 | qed. |
---|
[2570] | 609 | *) |
---|
[2182] | 610 | |
---|
| 611 | lemma nth_opt_reverse_hit : |
---|
| 612 | ∀A,l,n.n < |l| → nth_opt A n (reverse ? l) = nth_opt A (|l| - (S n)) l. |
---|
| 613 | #A #l elim l |
---|
| 614 | [ #n #ABS normalize in ABS; @⊥ -A /2 by absurd/ |
---|
| 615 | | #hd #tl #IH #n #lim whd in match (reverse ??); >rev_append_def |
---|
| 616 | @(leb_elim (S n) (|tl|)) #H |
---|
| 617 | [ >nth_opt_append_l [2: >length_reverse @H ] |
---|
| 618 | >(IH … H) >(minus_Sn_m … H) % |
---|
| 619 | | >(le_to_le_to_eq … (le_S_S_to_le … lim) (not_lt_to_le … H)) |
---|
| 620 | >nth_opt_append_r >length_reverse [2: % ] |
---|
| 621 | <minus_n_n <minus_n_n % |
---|
| 622 | ] |
---|
| 623 | ] |
---|
| 624 | qed. |
---|
| 625 | |
---|
| 626 | lemma nth_opt_reverse_hit_inv : |
---|
| 627 | ∀A,l,n.n < |l| → nth_opt A (|l| - (S n)) (reverse ? l) = nth_opt A n l. |
---|
| 628 | #A #l #n #H <(reverse_reverse ? l) in ⊢ (???%); @sym_eq |
---|
| 629 | <length_reverse @nth_opt_reverse_hit >length_reverse @H |
---|
| 630 | qed. |
---|
| 631 | |
---|
[2473] | 632 | definition good_local_sigma : |
---|
[2784] | 633 | ∀p:uns_params. |
---|
[2473] | 634 | ∀globals. |
---|
| 635 | ∀g:codeT (mk_graph_params p) globals. |
---|
| 636 | (Σl.bool_to_Prop (code_has_label … g l)) → |
---|
| 637 | codeT (mk_lin_params p) globals → |
---|
| 638 | (label → option ℕ) → Prop ≝ |
---|
| 639 | λp,globals,g,entry,c,sigma. |
---|
| 640 | sigma entry = Some ? 0 ∧ |
---|
[2529] | 641 | (∀l,n.point_of_label … c l = Some ? n → sigma l = Some ? n) ∧ |
---|
[2473] | 642 | ∀l,n.sigma l = Some ? n → |
---|
[2529] | 643 | ∃s. stmt_at … g l = Some ? s ∧ |
---|
[2532] | 644 | All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧ |
---|
| 645 | (match s with |
---|
| 646 | [ sequential s' nxt ⇒ |
---|
| 647 | match s' with |
---|
[2708] | 648 | [ COND a ltrue ⇒ |
---|
[2532] | 649 | (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨ |
---|
| 650 | (stmt_at … c n = Some ? (FCOND … I a ltrue nxt)) |
---|
[2708] | 651 | | _ ⇒ |
---|
| 652 | (stmt_at … c n = Some ? (sequential … s' it)) ∧ |
---|
[2702] | 653 | ((sigma nxt = Some ? (S n)) ∨ |
---|
[2708] | 654 | (stmt_at … c (S n) = Some ? (GOTO … nxt))) |
---|
[2532] | 655 | ] |
---|
| 656 | | final s' ⇒ |
---|
| 657 | stmt_at … c n = Some ? (final … s') |
---|
| 658 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
| 659 | ]). |
---|
[2473] | 660 | |
---|
[2182] | 661 | definition linearise_code: |
---|
[2784] | 662 | ∀p : uns_params.∀globals. |
---|
[2182] | 663 | ∀g : codeT (mk_graph_params p) globals.code_closed … g → |
---|
[2473] | 664 | ∀entry : (Σl.bool_to_Prop (code_has_label … g l)) |
---|
[2712] | 665 | .Σc_sigma. |
---|
| 666 | let c ≝ \fst c_sigma in |
---|
| 667 | let sigma ≝ \snd c_sigma in |
---|
[2473] | 668 | good_local_sigma … g entry c sigma ∧ |
---|
| 669 | code_closed … c |
---|
| 670 | (* ∧ |
---|
[2182] | 671 | ∃ sigma : identifier_map LabelTag ℕ. |
---|
| 672 | lookup … sigma entry = Some ? 0 ∧ |
---|
| 673 | ∀l,n.lookup … sigma l = Some ? n → |
---|
| 674 | ∃s. lookup … g l = Some ? s ∧ |
---|
| 675 | opt_Exists ? |
---|
| 676 | (λls.let 〈lopt, ts〉 ≝ ls in |
---|
| 677 | opt_All ? (eq ? l) lopt ∧ |
---|
| 678 | ts = graph_to_lin_statement … s ∧ |
---|
| 679 | opt_All ? |
---|
| 680 | (λnext.Or (lookup … sigma next = Some ? (S n)) |
---|
| 681 | (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) |
---|
[2473] | 682 | (stmt_implicit_label … s)) (nth_opt … n c)*) |
---|
[2182] | 683 | ≝ |
---|
| 684 | λp,globals,g,g_prf,entry_sig. |
---|
| 685 | let g ≝ branch_compress (mk_graph_params p) ? g entry_sig in |
---|
| 686 | let g_prf ≝ branch_compress_closed … g entry_sig g_prf in |
---|
| 687 | match graph_visit p globals g ∅ (empty_map …) [ ] [entry_sig] 0 (|g|) |
---|
| 688 | (entry_sig) g_prf ????????? |
---|
| 689 | with |
---|
| 690 | [ mk_Sig triple H ⇒ |
---|
| 691 | let sigma ≝ \fst (\fst triple) in |
---|
| 692 | let required ≝ \snd (\fst triple) in |
---|
| 693 | let crev ≝ \snd triple in |
---|
| 694 | let lbld_code ≝ rev ? crev in |
---|
[2473] | 695 | 〈filter_labels … (λl.l∈required) lbld_code, lookup … sigma〉 ]. |
---|
| 696 | [ cases (graph_visit ????????????????????) |
---|
| 697 | (* done later *) |
---|
[2182] | 698 | | #i >mem_set_empty * |
---|
| 699 | |3,4: #a #b whd in ⊢ (??%?→?); #ABS destruct(ABS) |
---|
| 700 | | #l #_ % |
---|
| 701 | | %2 % * >mem_set_empty * |
---|
| 702 | | % [2: %] @(branch_compress_has_entry … g entry_sig) |
---|
| 703 | | % |
---|
| 704 | | % % [% %] cases (pi1 … entry_sig) normalize #_ % // |
---|
| 705 | | >commutative_plus change with (? ≤ |g|) % |
---|
| 706 | ] |
---|
[2823] | 707 | cases daemon (*) |
---|
[2473] | 708 | ** |
---|
| 709 | #visited #required #generated normalize nodelta **** |
---|
[2182] | 710 | #entry_O #req_vis #last_fin #labels_in_req #sigma_prop |
---|
[2473] | 711 | % |
---|
[2529] | 712 | [ % [ % [assumption]] |
---|
| 713 | #lbl #n |
---|
| 714 | [ change with (If ? then with prf do ? else ? = ? → ?) |
---|
| 715 | @If_elim [2: #_ #ABS destruct(ABS) ] |
---|
| 716 | #H lapply H |
---|
| 717 | >occurs_exactly_once_filter_labels |
---|
| 718 | elim (true_or_false_Prop … (occurs_exactly_once ?? lbl ?)) |
---|
| 719 | [1,2: #H1 >H1 |*:] [2: * ] |
---|
| 720 | elim (true_or_false_Prop … (lbl ∈ required)) #H2 >H2 * |
---|
| 721 | lapply (in_map_domain … visited lbl) >(req_vis … H2) |
---|
| 722 | * #n_lbl #EQsigma |
---|
[2532] | 723 | elim (sigma_prop … EQsigma) #_ * #stmt * #_ |
---|
[2708] | 724 | cases stmt [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta |
---|
| 725 | [1,2,4: * #EQnth_opt #_ |3: * [ * ] #EQnth_opt [ #_ ] |5: #EQnth_opt ] |
---|
[2532] | 726 | >(nth_opt_index_of_label ???? n_lbl ? H) |
---|
[2708] | 727 | try (normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption) |
---|
| 728 | [1,3,5,7,9,11: |
---|
| 729 | >nth_opt_filter_labels in ⊢ (??%?); |
---|
| 730 | (* without the try it does not work *) |
---|
| 731 | try >EQnth_opt in ⊢ (??%?); |
---|
| 732 | >m_return_bind in ⊢ (??%?); |
---|
| 733 | >m_return_bind in ⊢ (??%?); |
---|
| 734 | >H2 in ⊢ (??%?); % |
---|
| 735 | |*: |
---|
[2529] | 736 | ] |
---|
| 737 | | #eq_lookup elim (sigma_prop ?? eq_lookup) |
---|
[2532] | 738 | #lbl_in_gen * #stmt * #stmt_in_g #stmt_spec |
---|
| 739 | % [2: % [ % [ assumption ]] |] |
---|
[2529] | 740 | [ @All_append |
---|
[2532] | 741 | [ cases stmt in stmt_spec; |
---|
[2708] | 742 | [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s #_ % | * ] |
---|
| 743 | normalize nodelta |
---|
| 744 | [1,2,4: * #stmt_at_EQ * #nxt_spec |3: * [ * ] #stmt_at_EQ [ #nxt_spec ]] |
---|
[2532] | 745 | %{I} |
---|
[2708] | 746 | try (>nxt_spec % #ABS destruct(ABS) @False) |
---|
| 747 | lapply (in_map_domain … visited nxt) |
---|
| 748 | >req_vis |
---|
| 749 | [1,3,5,7: * #x #EQ >EQ % #ABS destruct(ABS) |
---|
| 750 | |2,4,6: @(proj1 … (labels_in_req (S n) (GOTO … nxt) …)) |
---|
| 751 | whd in ⊢ (??%?); >nxt_spec % |
---|
| 752 | |8: @(proj1 … (proj2 … (labels_in_req n (FCOND … I a ltrue nxt) …))) |
---|
| 753 | whd in ⊢ (??%?); >stmt_at_EQ % |
---|
[2529] | 754 | ] |
---|
[2532] | 755 | | cases stmt in stmt_spec; |
---|
[2708] | 756 | [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta |
---|
| 757 | [1,2,4: * #EQ #_ |3: * [ * ] #EQ [ #_ ] |5: #EQ ] |
---|
[2532] | 758 | whd in match stmt_explicit_labels; normalize nodelta |
---|
[2708] | 759 | [ @(All_mp … (labels_in_req n (sequential … (COST_LABEL … cost) it) ?)) |
---|
| 760 | | @(All_mp … (labels_in_req n (sequential … (CALL … f args dest) it) ?)) |
---|
| 761 | | @(All_mp … (labels_in_req n (sequential … s it) ?)) |
---|
[2532] | 762 | | @(All_mp … (labels_in_req n (sequential … (COND … a ltrue) it) ?)) |
---|
[2708] | 763 | |6: @(All_mp … (labels_in_req n (final … s) ?)) |
---|
[2532] | 764 | | cases (labels_in_req n (FCOND … I a ltrue nxt) ?) |
---|
| 765 | [ #l_req #_ %{I} lapply (in_map_domain … visited ltrue) |
---|
| 766 | >(req_vis … l_req) * #n #EQ' >EQ' % #ABS destruct(ABS) ] |
---|
[2529] | 767 | ] |
---|
[2708] | 768 | [1,3,5,7,9: #l #l_req >(lookup_eq_safe … (req_vis … l_req)) |
---|
| 769 | % #ABS destruct(ABS) |
---|
[2532] | 770 | |*: whd in ⊢ (??%?); >EQ % |
---|
| 771 | ] |
---|
[2529] | 772 | ] |
---|
[2532] | 773 | | cases stmt in stmt_spec; |
---|
[2708] | 774 | [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta |
---|
| 775 | [1,2,4: * #EQ #H |3: * [ * ] #EQ [ #H ] |5: #EQ ] |
---|
[2532] | 776 | >stmt_at_filter_labels |
---|
| 777 | whd in match (stmt_at (mk_lin_params p) ?? n); >EQ normalize nodelta |
---|
[2708] | 778 | [1,2,3: % [1,3,5: %] cases H -H |
---|
| 779 | #H try (%1{H}) %2 >stmt_at_filter_labels whd in ⊢ (??%?); >H % |
---|
[2532] | 780 | | %1 %{H} % |
---|
| 781 | | %2 % |
---|
| 782 | | % |
---|
| 783 | ] |
---|
[2529] | 784 | ] |
---|
[2473] | 785 | ] |
---|
| 786 | | #i #s |
---|
[2182] | 787 | >stmt_at_filter_labels #EQ |
---|
| 788 | % |
---|
| 789 | [ @stmt_forall_labels_explicit |
---|
| 790 | @(All_mp … (labels_in_req … EQ)) |
---|
| 791 | #l #l_req >lin_code_has_label |
---|
| 792 | >occurs_exactly_once_filter_labels >l_req |
---|
| 793 | >commutative_andb whd in ⊢ (?%); |
---|
| 794 | elim (sigma_prop ?? (lookup_eq_safe … (req_vis … l_req))) |
---|
| 795 | >lin_code_has_label #H #_ @H |
---|
[2532] | 796 | | lapply EQ cases s [ #s' * | #s' #_ % | * #a #ltrue #lfalse #_ % ] |
---|
| 797 | -EQ #EQ change with (bool_to_Prop (code_has_point ????)) |
---|
[2182] | 798 | whd in match (point_of_succ ???); |
---|
| 799 | >lin_code_has_point @leb_elim [ #_ % ] >length_map >length_reverse |
---|
| 800 | #INEQ |
---|
| 801 | cut (|generated| = S i) |
---|
| 802 | [ @(le_to_le_to_eq … (not_lt_to_le … INEQ) ) |
---|
[2708] | 803 | whd in EQ : (??%?); inversion (nth_opt ???) in EQ; |
---|
| 804 | [2: #x ] #EQ1 whd in ⊢ (??%%→?); #EQ2 destruct |
---|
[2182] | 805 | <length_reverse |
---|
| 806 | @(nth_opt_hit_length … EQ1) |
---|
| 807 | ] #EQ_length |
---|
[2532] | 808 | elim last_fin * [ #fin | #a * #ltrue * #lfalse ] #EQ' |
---|
[2182] | 809 | lapply EQ whd in match (stmt_at ????); |
---|
[2532] | 810 | >nth_opt_reverse_hit >EQ_length [2,4: % ] <minus_n_n |
---|
[2182] | 811 | change with (stmt_at ???? = ? → ?) |
---|
| 812 | >EQ' #ABS destruct(ABS) |
---|
| 813 | ] |
---|
| 814 | ] |
---|
[2823] | 815 | *) |
---|
[2182] | 816 | qed. |
---|
| 817 | |
---|
| 818 | definition linearise_int_fun : |
---|
[2784] | 819 | ∀p : uns_params. |
---|
[2182] | 820 | ∀globals. |
---|
[2473] | 821 | ∀fn_in : joint_closed_internal_function (mk_graph_params p) globals |
---|
[2712] | 822 | .Σfn_out_sigma : |
---|
| 823 | (joint_closed_internal_function (mk_lin_params p) globals × ?). |
---|
[2473] | 824 | good_local_sigma … (joint_if_code … fn_in) (joint_if_entry … fn_in) |
---|
[2712] | 825 | (joint_if_code … (\fst fn_out_sigma)) (\snd fn_out_sigma) |
---|
[2182] | 826 | (* ∃sigma : identifier_map LabelTag ℕ. |
---|
| 827 | let g ≝ joint_if_code ?? (pi1 … fin) in |
---|
| 828 | let c ≝ joint_if_code ?? (pi1 … fout) in |
---|
| 829 | let entry ≝ joint_if_entry ?? (pi1 … fin) in |
---|
| 830 | lookup … sigma entry = Some ? 0 ∧ |
---|
| 831 | ∀l,n.lookup … sigma l = Some ? n → |
---|
| 832 | ∃s. lookup … g l = Some ? s ∧ |
---|
| 833 | opt_Exists ? |
---|
| 834 | (λls.let 〈lopt, ts〉 ≝ ls in |
---|
| 835 | opt_All ? (eq ? l) lopt ∧ |
---|
| 836 | ts = graph_to_lin_statement … s ∧ |
---|
| 837 | opt_All ? |
---|
| 838 | (λnext.Or (lookup … sigma next = Some ? (S n)) |
---|
| 839 | (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) |
---|
| 840 | (stmt_implicit_label … s)) (nth_opt … n c)*) ≝ |
---|
[2473] | 841 | λp,globals,f_sig. |
---|
| 842 | let code_sigma ≝ linearise_code … |
---|
| 843 | (joint_if_code … f_sig) |
---|
[2712] | 844 | (code_is_closed … (pi2 … f_sig)) |
---|
[2473] | 845 | (joint_if_entry … f_sig) in |
---|
| 846 | let code ≝ \fst code_sigma in |
---|
| 847 | let sigma ≝ \snd code_sigma in |
---|
[2712] | 848 | «〈«mk_joint_internal_function (mk_lin_params p) globals |
---|
[2473] | 849 | (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig) |
---|
[2712] | 850 | (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) |
---|
[2808] | 851 | (joint_if_stacksize ?? f_sig) (joint_if_local_stacksize ?? f_sig) |
---|
[2823] | 852 | code 0 (* exit is dummy! *), hide_prf ??», |
---|
[2712] | 853 | sigma〉, proj1 ?? (pi2 ?? code_sigma)». |
---|
[2823] | 854 | cases daemon (*) |
---|
[2712] | 855 | [2: whd in match code; cases code_sigma -code_sigma * #code #sigma |
---|
| 856 | normalize nodelta *** #H3 #H4 #H5 |
---|
| 857 | elim (H5 … H3) |
---|
[2532] | 858 | #s ** #_ #_ >lin_code_has_point cases code |
---|
[2712] | 859 | [ cases s [ * [ #cost | #f #args #dest | #a #ltrue | #s' ] #nxt | #s' | * ] |
---|
| 860 | [1,2,4: * #EQnth_opt #_ |3: * [ * ] #EQnth_opt [ #_ ] |5: #EQnth_opt ] |
---|
| 861 | normalize in EQnth_opt; destruct(EQnth_opt) |
---|
| 862 | | #hd #tl #_ #_ % |
---|
[2532] | 863 | ] |
---|
[2712] | 864 | | @hide_prf % |
---|
| 865 | (* TODO *) |
---|
| 866 | [ cases daemon |
---|
| 867 | | cases daemon |
---|
| 868 | | @(proj2 ?? (pi2 ?? code_sigma)) |
---|
| 869 | | cases daemon |
---|
[2784] | 870 | | (* We need to add this to graph_visit_ret_type as an invariant. |
---|
| 871 | To prove the invariant at each step in graph_visit we will exploit |
---|
| 872 | (regs_are_in_univers … (pi2 … f_sig)) |
---|
| 873 | More generally, to close all the daemons here we need to strengthen |
---|
| 874 | the invariant of graph_visit_ret_type so that the partial code |
---|
| 875 | emitted is also good_if at each step *) |
---|
| 876 | cases daemon |
---|
[2712] | 877 | ] |
---|
[2182] | 878 | ] |
---|
[2823] | 879 | *) |
---|
[2182] | 880 | qed. |
---|
[2422] | 881 | |
---|
[2784] | 882 | definition linearise : ∀p : uns_params. |
---|
[2422] | 883 | program (joint_function (mk_graph_params p)) ℕ → |
---|
[2473] | 884 | program (joint_function (mk_lin_params p)) ℕ |
---|
| 885 | ≝ |
---|
[2422] | 886 | λp,pr.transform_program ??? pr |
---|
[2946] | 887 | mk_joint_program |
---|
| 888 | (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))) |
---|
| 889 | (init_cost_label … pr). |
---|
[2473] | 890 | |
---|
[2529] | 891 | (* |
---|
[2473] | 892 | definition good_sigma : |
---|
[2784] | 893 | ∀p:uns_params. |
---|
[2473] | 894 | ∀prog_in : joint_program (mk_graph_params p). |
---|
| 895 | ((Σi.is_internal_function_of_program … prog_in i) → label → option ℕ) → Prop ≝ |
---|
| 896 | λp,prog_in,sigma. |
---|
| 897 | let prog_out ≝ linearise … prog_in in |
---|
[2481] | 898 | ∀i : Σi.is_internal_function_of_program … prog_in i.∀prf. |
---|
| 899 | let fn_in ≝ if_of_function … i in |
---|
| 900 | let i' : Σi.is_internal_function_of_program … prog_out i ≝ «pi1 ?? i, prf» in |
---|
| 901 | let fn_out ≝ if_of_function … i' in |
---|
[2473] | 902 | let sigma_local ≝ sigma i in |
---|
| 903 | good_local_sigma ?? (joint_if_code ?? fn_in) (joint_if_entry … fn_in) |
---|
| 904 | (joint_if_code ?? fn_out) sigma_local. |
---|
| 905 | |
---|
| 906 | lemma linearise_spec : ∀p,prog.∃sigma.good_sigma p prog sigma. |
---|
| 907 | #p #prog |
---|
| 908 | letin sigma ≝ |
---|
[2529] | 909 | (λi : Σi.is_internal_function_of_program … prog i. let fn_in ≝ if_of_function … i in |
---|
[2473] | 910 | \snd (linearise_int_fun … fn_in)) |
---|
| 911 | %{sigma} |
---|
[2481] | 912 | #i #prf >(prog_if_of_function_transform … i) [2: % ] |
---|
[2473] | 913 | normalize nodelta |
---|
| 914 | cases (linearise_int_fun ???) * #fn_out #sigma_loc |
---|
| 915 | normalize nodelta #prf @prf |
---|
| 916 | qed. |
---|
[2547] | 917 | *) |
---|