- Timestamp:
- Apr 18, 2011, 5:32:46 PM (10 years ago)
- Location:
- src
- Files:
-
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTL.ma
r756 r759 14 14 15 15 inductive ertl_statement: Type[0] ≝ 16 | ertl_st_skip: ident→ ertl_statement17 | ertl_st_comment: String → ident→ ertl_statement18 | ertl_st_cost: costlabel → ident→ ertl_statement19 | ertl_st_get_hdw: register → abstract_register → ident→ ertl_statement20 | ertl_st_set_hdw: abstract_register → register → ident→ ertl_statement21 | ertl_st_hdw_to_hdw: register → register → ident→ ertl_statement22 | ertl_st_new_frame: ident→ ertl_statement23 | ertl_st_del_frame: ident→ ertl_statement24 | ertl_st_frame_size: abstract_register → ident→ ertl_statement25 | ertl_st_pop: abstract_register → ident→ ertl_statement26 | ertl_st_push: abstract_register → ident→ ertl_statement27 | ertl_st_addr_h: abstract_register → ident → ident→ ertl_statement28 | ertl_st_addr_l: abstract_register → ident → ident→ ertl_statement29 | ertl_st_int: abstract_register → Byte → ident→ ertl_statement30 | ertl_st_move: abstract_register → abstract_register → ident→ ertl_statement31 | ertl_st_opaccs: OpAccs → abstract_register → abstract_register → abstract_register → ident→ ertl_statement32 | ertl_st_op1: Op1 → abstract_register → abstract_register → ident→ ertl_statement33 | ertl_st_op2: Op2 → abstract_register → abstract_register → abstract_register → ident→ ertl_statement34 | ertl_st_clear_carry: ident→ ertl_statement35 | ertl_st_load: abstract_register → abstract_register → abstract_register → ident→ ertl_statement36 | ertl_st_store: abstract_register → abstract_register → abstract_register → ident→ ertl_statement37 | ertl_st_call_id: ident → Byte → ident→ ertl_statement38 | ertl_st_cond_acc: abstract_register → ident → ident→ ertl_statement16 | ertl_st_skip: label → ertl_statement 17 | ertl_st_comment: String → label → ertl_statement 18 | ertl_st_cost: costlabel → label → ertl_statement 19 | ertl_st_get_hdw: register → abstract_register → label → ertl_statement 20 | ertl_st_set_hdw: abstract_register → register → label → ertl_statement 21 | ertl_st_hdw_to_hdw: register → register → label → ertl_statement 22 | ertl_st_new_frame: label → ertl_statement 23 | ertl_st_del_frame: label → ertl_statement 24 | ertl_st_frame_size: abstract_register → label → ertl_statement 25 | ertl_st_pop: abstract_register → label → ertl_statement 26 | ertl_st_push: abstract_register → label → ertl_statement 27 | ertl_st_addr_h: abstract_register → label → label → ertl_statement 28 | ertl_st_addr_l: abstract_register → label → label → ertl_statement 29 | ertl_st_int: abstract_register → Byte → label → ertl_statement 30 | ertl_st_move: abstract_register → abstract_register → label → ertl_statement 31 | ertl_st_opaccs: OpAccs → abstract_register → abstract_register → abstract_register → label → ertl_statement 32 | ertl_st_op1: Op1 → abstract_register → abstract_register → label → ertl_statement 33 | ertl_st_op2: Op2 → abstract_register → abstract_register → abstract_register → label → ertl_statement 34 | ertl_st_clear_carry: label → ertl_statement 35 | ertl_st_load: abstract_register → abstract_register → abstract_register → label → ertl_statement 36 | ertl_st_store: abstract_register → abstract_register → abstract_register → label → ertl_statement 37 | ertl_st_call_id: label → Byte → label → ertl_statement 38 | ertl_st_cond_acc: abstract_register → label → label → ertl_statement 39 39 | ertl_st_return: abstract_registers → ertl_statement. 40 40 … … 48 48 ertl_if_locals: registers; 49 49 ertl_if_graph: ertl_statement_graph; 50 ertl_if_entry: ident;51 ertl_if_exit: ident50 ertl_if_entry: label; 51 ertl_if_exit: label 52 52 }. 53 54 definition ertl_if_params: ertl_internal_function → nat. 55 # E 56 cases E 57 # H1 # H2 # H3 # H4 # H5 # H6 # H7 58 @ H3 59 qed. 53 60 54 61 inductive ertl_function: Type[0] ≝ … … 60 67 ertl_pr_vars: list (ident × nat); 61 68 ertl_pr_funcs: list (ident × ertl_function); 62 ertl_pr_main: option ident69 ertl_pr_main: option label 63 70 }. 64 71 -
src/ERTL/ERTLToLTL.ma
r757 r759 2 2 include "LTL/LTL.ma". 3 3 4 axiom translate_ ERTL_func:4 axiom translate_ertl_func: 5 5 ∀globals: list ident. 6 6 list (ident × ertl_function) → list (ident × (ltl_function_definition globals)). -
src/LTL/LTLToLIN.ma
r757 r759 18 18 λl: ident. 19 19 λg: BitVectorTrieSet 16. 20 set_insert ? lg.20 set_insert ? (word_of_identifier ? l) g. 21 21 22 22 definition mark: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ 23 23 λl: ident. 24 24 λg: BitVectorTrieSet 16. 25 set_insert ? lg.25 set_insert ? (word_of_identifier ? l) g. 26 26 27 27 definition marked: ident → BitVectorTrieSet 16 → bool ≝ 28 28 λl: ident. 29 29 λg: BitVectorTrieSet 16. 30 set_member ? l g. 30 set_member ? (word_of_identifier ? l) g. 31 32 (* alias id "lookupn" = "cic:/matita/cerco/common/Identifiers/lookup.def(3)". *) 31 33 32 34 definition graph_lookup ≝ 33 λglobals. 35 λglobals: list ident. 36 λl: ident. 37 λgr: ltl_statement_graph globals. 38 lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)). 39 40 definition fetch: ∀globals: list ident. ident → ltl_statement_graph globals → option (ltl_statement globals) ≝ 41 λglobals: list ident. 34 42 λl: ident. 35 43 λg: ltl_statement_graph globals. 36 lookup LabelTag (LTLStatement globals) g (an_identifier LabelTag l).37 38 definition fetch: ∀globals: list Identifier. Identifier → LTLStatementGraph globals → option (LTLStatement globals) ≝39 λglobals: list Identifier.40 λl: Identifier.41 λg: LTLStatementGraph globals.42 44 graph_lookup globals l g. 43 45 -
src/RTL/RTLtoERTL.ma
r756 r759 1 1 include "RTL/RTL.ma". 2 include "ERTL/ERTL.ma". 2 3 3 4 definition change_exit_label ≝ 4 5 λl: label. 5 λp: rtl_internal_function. 6 let rtl_if_luniverse' ≝ rtl_if_luniverse p in 7 let rtl_if_runiverse' ≝ rtl_if_runiverse p in 8 let rtl_if_sig' ≝ rtl_if_sig p in 9 let rtl_if_result' ≝ rtl_if_result p in 10 let rtl_if_params' ≝ rtl_if_params p in 11 let rtl_if_locals' ≝ rtl_if_locals p in 12 let rtl_if_stacksize' ≝ rtl_if_stacksize p in 13 let rtl_if_graph' ≝ rtl_if_graph p in 14 let rtl_if_entry' ≝ rtl_if_entry p in 15 let rtl_if_exit' ≝ l in 16 mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse' 17 rtl_if_sig' rtl_if_result' rtl_if_params' 18 rtl_if_locals' rtl_if_stacksize' 19 rtl_if_graph' rtl_if_entry' rtl_if_exit'. 6 λp: ertl_internal_function. 7 let ertl_if_luniverse' ≝ ertl_if_luniverse p in 8 let ertl_if_runiverse' ≝ ertl_if_runiverse p in 9 let ertl_if_params' ≝ ertl_if_params p in 10 let ertl_if_locals' ≝ ertl_if_locals p in 11 let ertl_if_graph' ≝ ertl_if_graph p in 12 let ertl_if_entry' ≝ ertl_if_entry p in 13 let ertl_if_exit' ≝ l in 14 mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse' 15 ertl_if_params' ertl_if_locals' 16 ertl_if_graph' ertl_if_entry' ertl_if_exit'. 20 17 21 18 definition change_entry_label ≝ 22 19 λl: label. 23 λp: rtl_internal_function. 24 let rtl_if_luniverse' ≝ rtl_if_luniverse p in 25 let rtl_if_runiverse' ≝ rtl_if_runiverse p in 26 let rtl_if_sig' ≝ rtl_if_sig p in 27 let rtl_if_result' ≝ rtl_if_result p in 28 let rtl_if_params' ≝ rtl_if_params p in 29 let rtl_if_locals' ≝ rtl_if_locals p in 30 let rtl_if_stacksize' ≝ rtl_if_stacksize p in 31 let rtl_if_graph' ≝ rtl_if_graph p in 32 let rtl_if_entry' ≝ l in 33 let rtl_if_exit' ≝ rtl_if_exit p in 34 mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse' 35 rtl_if_sig' rtl_if_result' rtl_if_params' 36 rtl_if_locals' rtl_if_stacksize' 37 rtl_if_graph' rtl_if_entry' rtl_if_exit'. 20 λp: ertl_internal_function. 21 let ertl_if_luniverse' ≝ ertl_if_luniverse p in 22 let ertl_if_runiverse' ≝ ertl_if_runiverse p in 23 let ertl_if_params' ≝ ertl_if_params p in 24 let ertl_if_locals' ≝ ertl_if_locals p in 25 let ertl_if_graph' ≝ ertl_if_graph p in 26 let ertl_if_entry' ≝ l in 27 let ertl_if_exit' ≝ ertl_if_exit p in 28 mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse' 29 ertl_if_params' ertl_if_locals' 30 ertl_if_graph' ertl_if_entry' ertl_if_exit'. 31 32 definition add_graph ≝ 33 λl: label. 34 λstmt. 35 λp. 36 let ertl_if_luniverse' ≝ ertl_if_luniverse p in 37 let ertl_if_runiverse' ≝ ertl_if_runiverse p in 38 let ertl_if_params' ≝ ertl_if_params p in 39 let ertl_if_locals' ≝ ertl_if_locals p in 40 let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in 41 let ertl_if_entry' ≝ ertl_if_entry p in 42 let ertl_if_exit' ≝ ertl_if_exit p in 43 mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse' 44 ertl_if_params' ertl_if_locals' 45 ertl_if_graph' ertl_if_entry' ertl_if_exit'. 38 46 39 47 definition fresh_label ≝ 40 48 λdef. 41 fresh LabelTag ( rtl_if_luniverse def).49 fresh LabelTag (ertl_if_luniverse def). 42 50 43 51 definition change_label ≝ 44 λ 52 λl. 53 λe: ertl_statement. 54 match e with 55 [ ertl_st_skip _ ⇒ ertl_st_skip l 56 | ertl_st_comment s _ ⇒ ertl_st_comment s l 57 | ertl_st_cost c _ ⇒ ertl_st_cost c l 58 | ertl_st_get_hdw r1 r2 _ ⇒ ertl_st_get_hdw r1 r2 l 59 | ertl_st_set_hdw r1 r2 _ ⇒ ertl_st_set_hdw r1 r2 l 60 | ertl_st_hdw_to_hdw r1 r2 _ ⇒ ertl_st_hdw_to_hdw r1 r2 l 61 | ertl_st_new_frame _ ⇒ ertl_st_new_frame l 62 | ertl_st_del_frame _ ⇒ ertl_st_del_frame l 63 | ertl_st_frame_size r _ ⇒ ertl_st_frame_size r l 64 | ertl_st_pop r _ ⇒ ertl_st_pop r l 65 | ertl_st_push r _ ⇒ ertl_st_push r l 66 | ertl_st_addr_h r id _ ⇒ ertl_st_addr_h r id l 67 | ertl_st_addr_l r id _ ⇒ ertl_st_addr_l r id l 68 | ertl_st_int r i _ ⇒ ertl_st_int r i l 69 | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l 70 | ertl_st_opaccs opaccs d s1 s2 _ ⇒ ertl_st_opaccs opaccs d s1 s2 l 71 | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l 72 | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l 73 | ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l 74 | ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l 75 | ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l 76 | ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l 77 | ertl_st_cond_acc a i1 i2 ⇒ ertl_st_cond_acc a i1 i2 78 | ertl_st_return a ⇒ ertl_st_return a 79 ]. 80 81 let rec adds_graph (stmt_list: list ertl_statement) (start_lbl: label) (dest_lbl: label) (def: ertl_internal_function): option ertl_internal_function ≝ 82 match stmt_list with 83 [ nil ⇒ Some ? def 84 | cons hd tl ⇒ 85 match tl with 86 [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def) 87 | _ ⇒ 88 let tmp_lbl ≝ fresh_label def in 89 match tmp_lbl with 90 [ OK o ⇒ 91 let 〈lbl, univ〉 ≝ o in 92 let stmt ≝ change_label lbl hd in 93 let def ≝ add_graph start_lbl hd def in 94 adds_graph tl lbl dest_lbl def 95 | Error ⇒ None ? 96 ] 97 ] 98 ]. 99 100 let rec add_translates (translate_list: list (label → label → ertl_internal_function → ertl_internal_function)) 101 (start_lbl: label) (dest_lbl: label) 102 (def: ertl_internal_function): option ertl_internal_function ≝ 103 match translate_list with 104 [ nil ⇒ Some ? def 105 | cons hd tl ⇒ 106 match tl with 107 [ nil ⇒ Some ? (hd start_lbl dest_lbl def) 108 | _ ⇒ 109 let tmp_lbl ≝ fresh_label def in 110 match tmp_lbl with 111 [ OK o ⇒ 112 let 〈lbl, univ〉 ≝ o in 113 let def ≝ hd start_lbl lbl def in 114 add_translates tl lbl dest_lbl def 115 | Error ⇒ None ? 116 ] 117 ] 118 ]. 119 120 definition fresh_register ≝ 121 λdef. 122
Note: See TracChangeset
for help on using the changeset viewer.