source: src/LTL/LTLToLIN.ma @ 1233

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

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

File size: 3.1 KB
Line 
1include "LTL/LTL.ma".
2include "LIN/LIN.ma".
3include "utilities/BitVectorTrieSet.ma".
4
5definition translate_statement: ∀globals. ltl_statement globals → lin_statement globals ≝
6  λglobals: list ident.
7  λs: ltl_statement globals.
8  match s with
9  [ joint_st_return ⇒ joint_st_return …
10  | joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it
11  | joint_st_goto l ⇒ joint_st_goto … l
12  | joint_st_extension ext ⇒ joint_st_extension lin_params … ext
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: graph (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, joint_st_goto … globals l :: generated〉
30    else
31     let visited' ≝ set_insert ? (word_of_identifier ? l) visited in
32     match lookup LabelTag ? 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' ≝ translated_statement :: generated in
37       match statement with
38       [ joint_st_sequential instr l2 ⇒
39         match instr with
40         [ joint_instr_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     | joint_st_return ⇒ 〈required, generated'〉
50     | joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n'
51     | joint_st_extension ext ⇒ ⊥ ]]].
52[3: @ext
53|1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
54qed.
55
56(* CSC: The branch compression (aka tunneling) optimization is not implemented
57   in Matita *)
58definition branch_compress ≝ λglobals.λa:graph (ltl_statement globals).a.
59
60definition 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.
Note: See TracBrowser for help on using the repository browser.