Changeset 1271 for src/ERTL/ERTLToLTL.ma
 Timestamp:
 Sep 26, 2011, 4:24:32 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1263 r1271 2 2 include "LTL/LTL.ma". 3 3 include "ERTL/spill.ma". 4 include "ERTL/build.ma".5 4 include "ERTL/uses.ma". 6 5 include "ASM/Arithmetic.ma". … … 284 283 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in 285 284 〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉 286  joint_instr_call_id f ignore ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_call_id … f ignore) l) graph, luniv〉285  joint_instr_call_id f ignore ignore' ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_call_id … f ignore ignore') l) graph, luniv〉 287 286  joint_instr_store addr1 addr2 srcr ⇒ 288 287 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_store … it it it) l) in … … 441 440 qed. 442 441 443 let rec mapi_aux444 (a : Type[0]) (b: Type[0]) (f: BitVector 16 → a →b) (n: nat)445 on n: n ≤ 16 → BitVectorTrie a n → BitVector (16  n) → BitVectorTrie b n≝446 match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16  n) → BitVectorTrie b nwith447 [ O ⇒ λinvariant. λtrie: BitVectorTrie a 0. λaccu: BitVector 16.448 match trie return λx: nat. λtrie : BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b xwith449 [ Leaf l ⇒ λprf. Leaf … (f accu l)450  Stub s ⇒ λprf. Stub … s442 let rec fold_aux 443 (a, b: Type[0]) (f: BitVector 16 → a → b → b) (seed: b) (n: nat) 444 on n: n ≤ 16 → BitVectorTrie a n → BitVector (16  n) → b ≝ 445 match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16  n) → b with 446 [ O ⇒ λinvariant: 0 ≤ 16. λtrie: BitVectorTrie a 0. λpath: BitVector 16. 447 match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = 0. b with 448 [ Leaf l ⇒ λproof. f path l seed 449  Stub s ⇒ λproof. seed 451 450  Node n' l r ⇒ λabsrd. ⊥ 452 ] (refl … 0) 453  S n' ⇒ λinvariant . λtrie: BitVectorTrie a (S n'). λaccu: BitVector (16  (S n')).454 match trie return λx: nat. λtrie : BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b xwith455 [ Leaf l ⇒ λabsrd. ⊥456  Stub s ⇒ λprf. Stub … s457  Node n'' l r ⇒ λpr f.458 Node ? n'' ? ?459 ] (refl nat(S n'))451 ] (refl … 0) 452  S n' ⇒ λinvariant: S n' ≤ 16. λtrie: BitVectorTrie a (S n'). λpath: BitVector (16  S n'). 453 match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = S n'. b with 454 [ Leaf l ⇒ λabsrd. ⊥ 455  Stub s ⇒ λproof. seed 456  Node n'' l r ⇒ λproof. 457 fold_aux a b f (fold_aux a b f seed n' ? (l⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((false:::path)⌈S (16  S n') ↦ 16  n'⌉)) n' ? (r⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((true:::path)⌈S (16  S n') ↦ 16  n'⌉) 458 ] (refl … (S n')) 460 459 ]. 461 [ 1,2: destruct(absrd) 462  3 : destruct(prf) 463 @(mapi_aux a b f n' ? l ((false ::: accu)⌈S (16  S n') ↦ 16  n'⌉)) 464 [ 1: @Sm_leq_n_m_leq_n 465 assumption 466  2: <minus_Sn_m 467 [ 1: >minus_S_S % 468  2: assumption 469 ] 470 ] 471  4 : destruct(prf) 472 @(mapi_aux a b f n' ? r ((true ::: accu)⌈S (16  S n') ↦ 16  n'⌉)) 473 [ 1: @Sm_leq_n_m_leq_n 474 assumption 475  2: <minus_Sn_m 476 [ 1: >minus_S_S % 477  2: assumption 478 ] 479 ] 480 ] 460 [ 1, 2: destruct(absrd) 461  3,8: >minus_S_S <minus_Sn_m // @le_S_S_to_le // 462  4,7: destruct(proof) % 463  5,6: @Sm_leq_n_m_leq_n // ] 481 464 qed. 482 465 483 definition mapi≝466 definition bvt_fold ≝ 484 467 λa, b: Type[0]. 485 λf: label → a → b .468 λf: label → a → b → b. 486 469 λtrie: BitVectorTrie a 16. 487 let f' ≝ λbv: BitVector 16. λa. 488 f (an_identifier LabelTag bv) a 470 λseed: b. 471 let f' ≝ λbv: BitVector 16. λa. λb. 472 f (an_identifier LabelTag bv) a b 489 473 in 490 mapi_aux a b f'16 ? trie [[]].474 fold_aux a b f' seed 16 ? trie [[]]. 491 475 // 492 476 qed. 493 494 definition translate_internal ≝ 495 λglobals. 496 λint_fun. 497 let graph ≝ ((empty_map …) : ltl_statement_graph globals) in 477 478 definition graph_fold ≝ 479 λglobals. 480 λb : Type[0]. 481 λf : label → ertl_statement globals → b → b. 482 λgraph: graph (ertl_statement globals). 483 λseed : b. 484 match graph with 485 [ an_id_map tree ⇒ bvt_fold (ertl_statement globals) b f tree seed 486 ]. 487 488 definition translate_internal: ∀globals: list ident. 489 ertl_internal_function globals → ltl_internal_function globals ≝ 490 λglobals: list ident. 491 λint_fun: ertl_internal_function globals. 492 let graph ≝ (empty_map … : ltl_statement_graph globals) in 498 493 let valuation ≝ analyse globals int_fun in 499 494 let coloured_graph ≝ build valuation in 500 let liveafter ≝ analyse globals int_fun in 501 let blah ≝ mapi … (λlabel. λstmt_graph_luniv. 502 let stmt ≝ 503 match eliminable globals (liveafter label) stmt with 504 [ Some successor ⇒ 〈joint_st_goto … successor, graph, joint_if_luniverse … int_fun〉 505  None ⇒ translate_statement globals int_fun valuation coloured_graph graph stmt 506 ] 507 in 508 ?) (joint_if_code … int_fun) 509 in ?. 510 511 512 513 let stmt = 514 match Liveness.eliminable (G.liveafter label) stmt with 515  Some successor > 516 LTL.St_skip successor 517  None > 518 I.translate_statement stmt 519 in 520 graph := Label.Map.add label stmt !graph 521 ) int_fun.ERTL.f_graph 522 523 definition translate_funct ≝ 524 λname_def. 525 let 〈name, def〉 ≝ name_def in 526 let def' ≝ 527 match def with 528 [ Internal def ⇒ Internal ? (translate_internal name def) 529  External def ⇒ External ? def 530 ] 495 let 〈graph, luniv〉 ≝ graph_fold globals ((ltl_statement_graph globals) × (universe LabelTag)) (λlabel: label. λstmt: ertl_statement globals. λgraph_luniv: (? × (universe LabelTag)). 496 let 〈graph, luniv〉 ≝ graph_luniv in 497 match eliminable globals (valuation label) stmt with 498 [ Some successor ⇒ 〈add_graph globals label (joint_st_goto … successor) graph, luniv〉 499  None ⇒ 500 translate_statement globals int_fun valuation coloured_graph graph stmt label 501 ]) (joint_if_code globals (ertl_params globals) int_fun) 〈graph, joint_if_luniverse … int_fun〉 531 502 in 532 〈name, def'〉. 533 534 definition translate ≝ 535 λp. 536 let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in 537 mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p). 503 mk_joint_internal_function globals (ltl_params globals) 504 luniv (joint_if_runiverse … int_fun) 505 it it it (joint_if_stacksize … int_fun) 506 graph ? ?. 507 cases daemon (* XXX *) 508 qed. 509 510 definition ertl_to_ltl : ertl_program → ltl_program ≝ 511 λp. transform_program … p (transf_fundef … (translate_internal …)).
Note: See TracChangeset
for help on using the changeset viewer.