source: src/LTL/LTLToLIN.ma @ 1149

Last change on this file since 1149 was 1149, checked in by mulligan, 9 years ago

changes to get everything type checking again after changing names of registers in i8051

File size: 4.7 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
[1149]12    [ joint_st_return ⇒ joint_st_return ? globals
13    | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it
14    | joint_st_goto l ⇒ joint_st_goto ? globals l
[728]15    ].
16   
[1110]17definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
18  λl: label.
[728]19  λg: BitVectorTrieSet 16.
[759]20    set_insert ? (word_of_identifier ? l) g.
[728]21   
[1110]22definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
23  λl: label.
[728]24  λg: BitVectorTrieSet 16.
[759]25    set_insert ? (word_of_identifier ? l) g.
[728]26   
[1110]27definition marked: label → BitVectorTrieSet 16 → bool ≝
28  λl: label.
[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.
[1110]36  λl: label.
[759]37  λgr: ltl_statement_graph globals.
38    lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).
39   
[1110]40definition fetch: ∀globals: list ident. label → ltl_statement_graph globals → option (ltl_statement globals) ≝
[759]41  λglobals: list ident.
[1110]42  λl: label.
[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:
[1110]49  ∀globals: list ident.
50  ∀g: ltl_statement_graph globals.
[753]51  ∀required: BitVectorTrieSet 16.
52  ∀visited: BitVectorTrieSet 16.
[1110]53  ∀generated: list (pre_lin_statement globals).
54  ∀l: label.
[753]55  ∀n: nat.
[1110]56    BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
[733]57  if marked l2 visited then
[1149]58    〈require l2 required, (joint_st_goto ? globals l2) :: generated〉
[733]59  else
60   visit globals g required visited generated l2 n.
61
[1111]62(* XXX: look at this.  way too complicated to understand whether it is correct,
63   in my opinion.
64*)
[1110]65let rec visit
66  (globals: list ident) (g: ltl_statement_graph globals)
67  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
68  (generated: list (pre_lin_statement globals)) (l: label) (n: nat)
69    on n: BitVectorTrieSet 16 × (list (pre_lin_statement globals)) ≝
[728]70  match n with
71  [ O ⇒ 〈required, generated〉
72  | S n' ⇒
73    let visited' ≝ mark l visited in
74    match fetch globals l g with
75    [ None ⇒ 〈required, generated〉 (* dpm: correct? *)
76    | Some statement ⇒
77      let translated_statement ≝ translate_statement globals statement in
78      let generated'' ≝ translated_statement :: generated in
79      match statement with
[1149]80      [ joint_st_sequential instr l2 ⇒
81        match instr with
82        [ joint_instr_cond_acc l1 ⇒
[1110]83              let required' ≝
84                if marked l2 visited' then
85                  require l2 required
86                else
87                  required in
88              let 〈required', generated''〉 ≝
89               foo l2 visited' required' globals generated'' g n' visit (*
90                if marked l2 visited' then
91                  〈required', (Joint_St_Goto ? globals l2) :: generated''〉
92                else
93                  visit globals g required' visited' generated'' l2 n'*) in
94              let required'' ≝ require l1 required' in
95                if ¬(marked l1 visited') then
96                  visit globals g required'' visited' generated'' l1 n'
97                else
98                  〈required', generated''〉
99          | _ ⇒
[728]100            let required' ≝
101              if marked l2 visited' then
102                require l2 required
103              else
104                required in
105            if marked l2 visited' then
[1149]106              〈required', joint_st_goto ? globals l2 :: generated''〉
[728]107            else
[1110]108              visit globals g required' visited' generated'' l2 n'
109          ]
110        | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
[1149]111    | joint_st_goto l ⇒
[1110]112       let required' ≝
113         if marked l visited' then
114           require l required
115         else
116           required
117       in
118         if marked l visited' then
[1149]119           〈required', joint_st_goto ? globals l :: generated''〉
[1110]120         else
121           visit globals g required' visited' generated'' l n'
[728]122    ]
[1110]123  ]
124].
[728]125
126(*
127definition translate_graph ≝
128  λglobals: list Identifier.
129  λg: LTLStatementGraph globals.
130  λentry: Identifier.
131    let visited ≝ set_empty ? in
132    let required ≝ set_insert ? entry (set_empty ?) in
133    let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in
134    let reversed ≝ rev ? translated in
135      filter (λs: PreLINStatement globals. ?) reversed.
136*)
Note: See TracBrowser for help on using the repository browser.