source: src/LTL/LTLToLIN.ma @ 1086

Last change on this file since 1086 was 759, checked in by mulligan, 10 years ago

More work on the RTL to ERTL pass.

File size: 4.6 KB
RevLine 
[714]1include "LTL/LTL.ma".
2include "LIN/LIN.ma".
[728]3include "utilities/BitVectorTrieSet.ma".
4include "common/Graphs.ma".
[714]5
[753]6axiom LTLTag: String.
7
[757]8definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
9  λglobals: list ident.
10  λs: ltl_statement globals.
[714]11    match s with
[757]12    [ joint_st_return ⇒ joint_st_return ? globals
13    | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it
14    | joint_st_goto lbl ⇒ joint_st_goto ? globals lbl
[728]15    ].
16   
[757]17definition require: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
18  λl: ident.
[728]19  λg: BitVectorTrieSet 16.
[759]20    set_insert ? (word_of_identifier ? l) g.
[728]21   
[757]22definition mark: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
23  λl: ident.
[728]24  λg: BitVectorTrieSet 16.
[759]25    set_insert ? (word_of_identifier ? l) g.
[728]26   
[757]27definition marked: ident → BitVectorTrieSet 16 → bool ≝
28  λl: ident.
[728]29  λg: BitVectorTrieSet 16.
[759]30    set_member ? (word_of_identifier ? l) g.
[728]31   
[759]32(* alias id "lookupn" = "cic:/matita/cerco/common/Identifiers/lookup.def(3)". *)
33   
[753]34definition graph_lookup ≝
[759]35  λglobals: list ident.
[757]36  λl: ident.
[759]37  λgr: ltl_statement_graph globals.
38    lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).
39   
40definition fetch: ∀globals: list ident. ident → ltl_statement_graph globals → option (ltl_statement globals) ≝
41  λglobals: list ident.
42  λl: ident.
[757]43  λg: ltl_statement_graph globals.
[753]44    graph_lookup globals l g.
[728]45
[753]46definition foo ≝
47  λl2, visited, required, globals, generated, g, n.
48  λvisit:
49  ∀globals: list Identifier.
50  ∀g: LTLStatementGraph globals.
51  ∀required: BitVectorTrieSet 16.
52  ∀visited: BitVectorTrieSet 16.
53  ∀generated: list (PreLINStatement globals).
54  ∀l: Identifier.
55  ∀n: nat.
56    BitVectorTrieSet 16 × (list (PreLINStatement globals)).
[733]57  if marked l2 visited then
[753]58    〈require l2 required, (Joint_St_Goto ? globals l2) :: generated〉
[733]59  else
60   visit globals g required visited generated l2 n.
61
[757]62let rec visit (globals: list ident) (g: ltl_statement_graph globals)
[728]63              (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
[757]64              (generated: list (pre_lin_statement globals)) (l: ident) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝
[728]65  match n with
66  [ O ⇒ 〈required, generated〉
67  | S n' ⇒
68    let visited' ≝ mark l visited in
69    match fetch globals l g with
70    [ None ⇒ 〈required, generated〉 (* dpm: correct? *)
71    | Some statement ⇒
72      let translated_statement ≝ translate_statement globals statement in
73      let generated'' ≝ translated_statement :: generated in
74      match statement with
[757]75      [ joint_st_sequential instr l2 ⇒
[728]76        match instr with
[757]77        [ joint_instr_cond_acc l1 ⇒
[728]78            let required' ≝
79              if marked l2 visited' then
80                require l2 required
81              else
82                required in
83            let 〈required', generated''〉 ≝
[733]84             foo l2 visited' required' globals generated'' g n' visit (*
[728]85              if marked l2 visited' then
86                〈required', (Joint_St_Goto ? globals l2) :: generated''〉
87              else
[733]88                visit globals g required' visited' generated'' l2 n'*) in
[728]89            let required'' ≝ require l1 required' in
90              if ¬(marked l1 visited') then
91                visit globals g required'' visited' generated'' l1 n'
92              else
93                〈required', generated''〉
94        | _ ⇒
95          let required' ≝
96            if marked l2 visited' then
97              require l2 required
98            else
99              required in
100          if marked l2 visited' then
101            〈required', Joint_St_Goto ? globals l2 :: generated''〉
102          else
103            visit globals g required' visited' generated'' l2 n'
104        ]
[757]105      | joint_st_goto lbl ⇒
[728]106        let required' ≝
107          if marked lbl visited' then
108            require lbl required
109          else
110            required in
111        if marked lbl visited' then
112          〈required', (Joint_St_Goto ? globals lbl) :: generated''〉
113        else
114          visit globals g required' visited' generated'' lbl n'
[757]115      | joint_st_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
[728]116      ]
117    ]
118  ].
119
120(*
121definition translate_graph ≝
122  λglobals: list Identifier.
123  λg: LTLStatementGraph globals.
124  λentry: Identifier.
125    let visited ≝ set_empty ? in
126    let required ≝ set_insert ? entry (set_empty ?) in
127    let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in
128    let reversed ≝ rev ? translated in
129      filter (λs: PreLINStatement globals. ?) reversed.
130*)
Note: See TracBrowser for help on using the repository browser.