Changeset 1236 for src/LTL


Ignore:
Timestamp:
Sep 21, 2011, 3:56:54 PM (8 years ago)
Author:
sacerdot
Message:

LTLToLin.ma completed (up to a couple of daemons used to provide dead code/data
that will be removed from the joint status later)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLIN.ma

    r1233 r1236  
    22include "LIN/LIN.ma".
    33include "utilities/BitVectorTrieSet.ma".
     4include "utilities/lists.ma".
    45
    56definition translate_statement: ∀globals. ltl_statement globals → lin_statement globals ≝
     
    1920   Note: the OCaml code contains some useful explanatory comments. *)
    2021let rec visit
    21   (globals: list ident) (g: graph (ltl_statement globals))
     22  (globals: list ident) (g: label → option (ltl_statement globals))
    2223  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
    23   (generated: list (lin_statement globals)) (l: label) (n: nat)
    24     on n: BitVectorTrieSet 16 × (list (lin_statement globals)) ≝
     24  (generated: list ((option label) × (lin_statement globals))) (l: label) (n: nat)
     25    on n: BitVectorTrieSet 16 × (list ((option label) × (lin_statement globals))) ≝
    2526  match n with
    2627  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
    2728  | S n' ⇒
    2829    if set_member … (word_of_identifier … l) visited then
    29      〈set_insert ? (word_of_identifier ? l) required, joint_st_goto … globals l :: generated〉
     30     〈set_insert ? (word_of_identifier ? l) required, 〈None …, joint_st_goto … globals l〉 :: generated〉
    3031    else
    3132     let visited' ≝ set_insert ? (word_of_identifier ? l) visited in
    32      match lookup LabelTag ? g (an_identifier LabelTag (word_of_identifier … l)) with
     33     match g (an_identifier LabelTag (word_of_identifier … l)) with
    3334     [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *)
    3435     | Some statement ⇒
    3536       let translated_statement ≝ translate_statement globals statement in
    36        let generated' ≝ translated_statement :: generated in
     37       let generated' ≝ 〈Some … l, translated_statement〉 :: generated in
    3738       match statement with
    3839       [ joint_st_sequential instr l2 ⇒
     
    5657(* CSC: The branch compression (aka tunneling) optimization is not implemented
    5758   in Matita *)
    58 definition branch_compress ≝ λglobals.λa:graph (ltl_statement globals).a.
     59definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a.
    5960
    60 definition translate_graph ≝
    61   λglobals: list Identifier.
    62   λg: graph (ltl_statement globals).
    63   λentry: label.
    64     let g ≝ branch_compress ? g in
    65     let visited ≝ set_empty ? in
    66     let required ≝ set_insert ? (word_of_identifier … entry) (set_empty ?) in
    67     let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in
    68     let reversed ≝ rev ? translated in
    69       filter (λs: PreLINStatement globals. ?) reversed.
     61definition translate_graph:
     62 ∀globals. label → nat →
     63  (label → option (ltl_statement globals)) → (label → option (lin_statement globals))
     64
     65 λglobals,entry,labels_upper_bound,g.
     66  let g ≝ branch_compress ? g in
     67  let visited ≝ set_empty ? in
     68  let required ≝ set_insert ? (word_of_identifier … entry) (set_empty ?) in
     69  let 〈required', translated〉 ≝ visit globals g required visited [ ] entry labels_upper_bound in
     70  let reversed ≝ rev ? translated in
     71  let final ≝
     72   map ??
     73    (λs. let 〈l,x〉 ≝ s in
     74      match l with
     75       [ None ⇒ 〈None …,x〉
     76       | Some l ⇒
     77          〈if set_member … (word_of_identifier … l) required' then Some ? l else None ?,
     78           x〉])
     79    reversed in
     80  λl.
     81   find ?? (λs. let 〈l',x〉 ≝ s in
     82    match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) final.
     83
     84definition translate_int_fun:
     85 ∀globals.
     86  joint_internal_function ltl_params globals →
     87   joint_internal_function lin_params globals
     88
     89 λglobals,f.
     90  mk_joint_internal_function lin_params globals
     91   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f)
     92    (translate_graph globals (joint_if_entry ?? f) (nat_of_bitvector … (next_identifier … (joint_if_luniverse … f)))
     93     (joint_if_lookup ?? f))
     94    ??.
     95cases daemon (*CSC: XXXXXXXXX Dead code produced *)
     96qed.
     97
     98definition ltl_to_lin : ltl_program → lin_program ≝
     99 λp. transform_program … p (transf_fundef … (translate_int_fun …)).
Note: See TracChangeset for help on using the changeset viewer.