source: src/LTL/LTLToLIN.ma @ 1236

Last change on this file since 1236 was 1236, checked in by sacerdot, 9 years ago

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 size: 4.3 KB
Line 
1include "LTL/LTL.ma".
2include "LIN/LIN.ma".
3include "utilities/BitVectorTrieSet.ma".
4include "utilities/lists.ma".
5
6definition translate_statement: ∀globals. ltl_statement globals → lin_statement globals ≝
7  λglobals: list ident.
8  λs: ltl_statement globals.
9  match s with
10  [ joint_st_return ⇒ joint_st_return …
11  | joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it
12  | joint_st_goto l ⇒ joint_st_goto … l
13  | joint_st_extension ext ⇒ joint_st_extension lin_params … ext
14  ].
15
16(* Invariant: l has not been visited yet the very first time the
17   function is called and in the true branch of a conditional call.
18   This avoid useless gotos.
19   
20   Note: the OCaml code contains some useful explanatory comments. *)
21let rec visit
22  (globals: list ident) (g: label → option (ltl_statement globals))
23  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
24  (generated: list ((option label) × (lin_statement globals))) (l: label) (n: nat)
25    on n: BitVectorTrieSet 16 × (list ((option label) × (lin_statement globals))) ≝
26  match n with
27  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
28  | S n' ⇒
29    if set_member … (word_of_identifier … l) visited then
30     〈set_insert ? (word_of_identifier ? l) required, 〈None …, joint_st_goto … globals l〉 :: generated〉
31    else
32     let visited' ≝ set_insert ? (word_of_identifier ? l) visited in
33     match g (an_identifier LabelTag (word_of_identifier … l)) with
34     [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *)
35     | Some statement ⇒
36       let translated_statement ≝ translate_statement globals statement in
37       let generated' ≝ 〈Some … l, translated_statement〉 :: generated in
38       match statement with
39       [ joint_st_sequential instr l2 ⇒
40         match instr with
41         [ joint_instr_cond acc_a_reg l1 ⇒
42            let 〈required', generated''〉 ≝
43             visit globals g required visited' generated' l2 n' in
44            let required'' ≝ set_insert ? (word_of_identifier ? l1) required' in
45             if set_member … (word_of_identifier … l1) visited' then
46               〈required', generated''〉
47             else
48               visit globals g required'' visited' generated'' l1 n'
49         | _ ⇒ visit globals g required visited' generated' l2 n']
50     | joint_st_return ⇒ 〈required, generated'〉
51     | joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n'
52     | joint_st_extension ext ⇒ ⊥ ]]].
53[3: @ext
54|1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
55qed.
56
57(* CSC: The branch compression (aka tunneling) optimization is not implemented
58   in Matita *)
59definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a.
60
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 TracBrowser for help on using the repository browser.