Changeset 759 for src


Ignore:
Timestamp:
Apr 18, 2011, 5:32:46 PM (9 years ago)
Author:
mulligan
Message:

More work on the RTL to ERTL pass.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed

  • src/ERTL/ERTL.ma

    r756 r759  
    1414
    1515inductive ertl_statement: Type[0] ≝
    16   | ertl_st_skip: ident → ertl_statement
    17   | ertl_st_comment: String → ident → ertl_statement
    18   | ertl_st_cost: costlabel → ident → ertl_statement
    19   | ertl_st_get_hdw: register → abstract_register → ident → ertl_statement
    20   | ertl_st_set_hdw: abstract_register → register → ident → ertl_statement
    21   | ertl_st_hdw_to_hdw: register → register → ident → ertl_statement
    22   | ertl_st_new_frame: ident → ertl_statement
    23   | ertl_st_del_frame: ident → ertl_statement
    24   | ertl_st_frame_size: abstract_register → ident → ertl_statement
    25   | ertl_st_pop: abstract_register → ident → ertl_statement
    26   | ertl_st_push: abstract_register → ident → ertl_statement
    27   | ertl_st_addr_h: abstract_register → ident → ident → ertl_statement
    28   | ertl_st_addr_l: abstract_register → ident → ident → ertl_statement
    29   | ertl_st_int: abstract_register → Byte → ident → ertl_statement
    30   | ertl_st_move: abstract_register → abstract_register → ident → ertl_statement
    31   | ertl_st_opaccs: OpAccs → abstract_register → abstract_register → abstract_register → ident → ertl_statement
    32   | ertl_st_op1: Op1 → abstract_register → abstract_register → ident → ertl_statement
    33   | ertl_st_op2: Op2 → abstract_register → abstract_register → abstract_register → ident → ertl_statement
    34   | ertl_st_clear_carry: ident → ertl_statement
    35   | ertl_st_load: abstract_register → abstract_register → abstract_register → ident → ertl_statement
    36   | ertl_st_store: abstract_register → abstract_register → abstract_register → ident → ertl_statement
    37   | ertl_st_call_id: ident → Byte → ident → ertl_statement
    38   | ertl_st_cond_acc: abstract_register → ident → ident → ertl_statement
     16  | 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
    3939  | ertl_st_return: abstract_registers → ertl_statement.
    4040
    … …  
    4848  ertl_if_locals: registers;
    4949  ertl_if_graph: ertl_statement_graph;
    50   ertl_if_entry: ident;
    51   ertl_if_exit: ident
     50  ertl_if_entry: label;
     51  ertl_if_exit: label
    5252}.
     53
     54definition ertl_if_params: ertl_internal_function → nat.
     55  # E
     56  cases E
     57  # H1 # H2 # H3 # H4 # H5 # H6 # H7
     58  @ H3
     59qed.
    5360
    5461inductive ertl_function: Type[0] ≝
    … …  
    6067  ertl_pr_vars: list (ident × nat);
    6168  ertl_pr_funcs: list (ident × ertl_function);
    62   ertl_pr_main: option ident
     69  ertl_pr_main: option label
    6370}.
    6471

  • src/ERTL/ERTLToLTL.ma

    r757 r759  
    22include "LTL/LTL.ma".
    33 
    4 axiom translate_ERTL_func:
     4axiom translate_ertl_func:
    55  ∀globals: list ident.
    66    list (ident × ertl_function) → list (ident × (ltl_function_definition globals)).

  • src/LTL/LTLToLIN.ma

    r757 r759  
    1818  λl: ident.
    1919  λg: BitVectorTrieSet 16.
    20     set_insert ? l g.
     20    set_insert ? (word_of_identifier ? l) g.
    2121   
    2222definition mark: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    2323  λl: ident.
    2424  λg: BitVectorTrieSet 16.
    25     set_insert ? l g.
     25    set_insert ? (word_of_identifier ? l) g.
    2626   
    2727definition marked: ident → BitVectorTrieSet 16 → bool ≝
    2828  λl: ident.
    2929  λ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)". *)
    3133   
    3234definition 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   
     40definition fetch: ∀globals: list ident. ident → ltl_statement_graph globals → option (ltl_statement globals) ≝
     41  λglobals: list ident.
    3442  λl: ident.
    3543  λ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.
    4244    graph_lookup globals l g.
    4345

  • src/RTL/RTLtoERTL.ma

    r756 r759  
    11include "RTL/RTL.ma".
     2include "ERTL/ERTL.ma".
    23
    34definition change_exit_label ≝
    45  λ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'.
    2017
    2118definition change_entry_label ≝
    2219  λ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                             
     32definition 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'.
    3846                             
    3947definition fresh_label ≝
    4048  λdef.
    41     fresh LabelTag (rtl_if_luniverse def).
     49    fresh LabelTag (ertl_if_luniverse def).
    4250   
    4351definition 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 
     81let 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
     100let 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 
     120definition fresh_register ≝
     121  λdef.
     122   
Note: See TracChangeset for help on using the changeset viewer.