source: src/LTL/LTLToLIN.ma @ 1324

Last change on this file since 1324 was 1282, checked in by sacerdot, 8 years ago

Cosmetic change: names of joint statements/instructions shortened and made
uppercase.

File size: 4.0 KB
Line 
1include "LTL/LTL.ma".
2include "LIN/LIN.ma".
3include "utilities/BitVectorTrieSet.ma".
4include alias "common/Graphs.ma".
5
6definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
7  λglobals: list ident.
8  λs: ltl_statement globals.
9  match s with
10  [ RETURN ⇒ RETURN ??
11  | sequential instr lbl ⇒ sequential … instr it
12  | GOTO l ⇒ GOTO lin_params_ globals l
13  ].
14
15(* Invariant: l has not been visited yet the very first time the
16   function is called and in the true branch of a conditional call.
17   This avoid useless gotos.
18   
19   Note: the OCaml code contains some useful explanatory comments. *)
20let rec visit
21  (globals: list ident) (g: label → option (ltl_statement globals))
22  (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)) ≝
25  match n with
26  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
27  | S n' ⇒
28    if set_member … (word_of_identifier … l) visited then
29     〈set_insert ? (word_of_identifier ? l) required, 〈None …, GOTO … globals l〉 :: generated〉
30    else
31     let visited' ≝ set_insert ? (word_of_identifier ? l) visited in
32     match g (an_identifier LabelTag (word_of_identifier … l)) with
33     [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *)
34     | Some statement ⇒
35       let translated_statement ≝ translate_statement globals statement in
36       let generated' ≝ 〈Some … l, translated_statement〉 :: generated in
37       match statement with
38       [ sequential instr l2 ⇒
39         match instr with
40         [ COND acc_a_reg l1 ⇒
41            let 〈required', generated''〉 ≝
42             visit globals g required visited' generated' l2 n' in
43            let required'' ≝ set_insert ? (word_of_identifier ? l1) required' in
44             if set_member … (word_of_identifier … l1) visited' then
45               〈required', generated''〉
46             else
47               visit globals g required'' visited' generated'' l1 n'
48         | _ ⇒ visit globals g required visited' generated' l2 n']
49     | RETURN ⇒ 〈required, generated'〉
50     | GOTO l2 ⇒ visit globals g required visited' generated' l2 n']]].
51[1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
52qed.
53
54(* CSC: The branch compression (aka tunneling) optimization is not implemented
55   in Matita *)
56definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a.
57
58definition translate_graph:
59 ∀globals. label → nat →
60  (label → option (ltl_statement globals)) → codeT … (lin_params globals)
61
62 λglobals,entry,labels_upper_bound,g.
63  let g ≝ branch_compress ? g in
64  let visited ≝ set_empty ? in
65  let required ≝ set_insert ? (word_of_identifier … entry) (set_empty ?) in
66  let 〈required', translated〉 ≝ visit globals g required visited [ ] entry labels_upper_bound in
67  let reversed ≝ rev ? translated in
68  let final ≝
69   map ??
70    (λs. let 〈l,x〉 ≝ s in
71      match l with
72       [ None ⇒ 〈None …,x〉
73       | Some l ⇒
74          〈if set_member … (word_of_identifier … l) required' then Some ? l else None ?,
75           x〉])
76    reversed
77  in
78   dp … final ?.
79(*CSC: XXXXXXX missing proof of well formedness here; but it seems false! *)
80cases daemon
81qed.
82
83definition translate_int_fun:
84 ∀globals.
85  joint_internal_function … (ltl_params globals) →
86   joint_internal_function … (lin_params globals)
87
88 λglobals,f.
89  mk_joint_internal_function globals (lin_params globals)
90   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f)
91    (translate_graph globals (joint_if_entry ?? f) (nat_of_bitvector … (next_identifier … (joint_if_luniverse … f)))
92     (lookup ?? (joint_if_code … f)))
93    ??.
94cases daemon (*CSC: XXXXXXXXX Dead code produced *)
95qed.
96
97definition ltl_to_lin : ltl_program → lin_program ≝
98 λp. transform_program … p (transf_fundef … (translate_int_fun …)).
Note: See TracBrowser for help on using the repository browser.