Changeset 1271 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Sep 26, 2011, 4:24:32 PM (8 years ago)
Author:
mulligan
Message:

finished, kind of

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1263 r1271  
    22include "LTL/LTL.ma".
    33include "ERTL/spill.ma".
    4 include "ERTL/build.ma".
    54include "ERTL/uses.ma".
    65include "ASM/Arithmetic.ma".
     
    284283      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
    285284        〈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〉
    287286    | joint_instr_store addr1 addr2 srcr ⇒
    288287      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_store … it it it) l) in
     
    441440qed.
    442441
    443 let rec mapi_aux
    444   (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 n with
    447   [ O ⇒ λinvariant. λtrie: BitVectorTrie a 0. λaccu: BitVector 16.
    448     match trie return λx: nat. λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with
    449     [ Leaf l ⇒ λprf. Leaf … (f accu l)
    450     | Stub s ⇒ λprf. Stub … s
     442let 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
    451450    | 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 x with
    455     [ Leaf l ⇒ λabsrd. ⊥
    456     | Stub s ⇒ λprf. Stub … s
    457     | Node n'' l r ⇒ λprf.
    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'))
    460459  ].
    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 // ]
    481464qed.
    482465
    483 definition mapi
     466definition bvt_fold
    484467  λa, b: Type[0].
    485   λf: label → a → b.
     468  λf: label → a → b → b.
    486469  λ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
    489473    in
    490       mapi_aux a b f' 16 ? trie [[]].
     474      fold_aux a b f' seed 16 ? trie [[]].
    491475  //
    492476qed.
    493  
    494 definition translate_internal ≝
    495   λglobals.
    496   λint_fun.
    497   let graph ≝ ((empty_map …) : ltl_statement_graph globals) in
     477
     478definition 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
     488definition 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
    498493  let valuation ≝ analyse globals int_fun in
    499494  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〉
    531502  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 *)
     508qed.
     509
     510definition 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.