Changeset 1252


Ignore:
Timestamp:
Sep 22, 2011, 2:49:18 PM (8 years ago)
Author:
sacerdot
Message:

graph_params added to joint/Joint.ma, together with useful common setters/getters

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1248 r1252  
    1919definition ertl_statement ≝ joint_statement ertl_params_.
    2020
    21 definition ertl_params: ∀globals. params globals ≝
    22   λglobals.
    23     mk_params globals ertl_params_ (graph (ertl_statement globals)) (lookup …).
    24 
     21definition ertl_params: ∀globals. params globals ≝ graph_params ertl_params_.
    2522
    2623definition ertl_internal_function ≝
  • src/LTL/LTL.ma

    r1246 r1252  
    77definition ltl_statement ≝ joint_statement ltl_params_.
    88
    9 definition ltl_params: ∀globals. params globals ≝
    10  λglobals. mk_params globals ltl_params_ (graph (ltl_statement globals)) (lookup …).
     9definition ltl_params: ∀globals. params globals ≝ graph_params ltl_params_.
    1110
    1211definition ltl_program ≝ joint_program ltl_params.
  • src/RTL/RTLtoERTL.ma

    r1250 r1252  
    33include "common/Identifiers.ma".
    44include "ERTL/ERTL.ma".
    5 include "utilities/extralib.ma". (* CSC: Only for Sigma type projections *)
    6                      
    7 definition add_graph ≝
    8   λglobals.λl: label.λstmt.λp: joint_internal_function … (ertl_params globals).
    9    let code ≝ add … (joint_if_code … p) l stmt in
    10     mk_joint_internal_function … (ertl_params globals)
    11      (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    12      (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    13      code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
    14   normalize nodelta;
    15   [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
    16   #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
    17 qed.
    185                           
    196definition fresh_label ≝
     
    2512  match e with
    2613  [ joint_st_goto _ ⇒ joint_st_goto … l
    27   | joint_st_return ⇒ joint_st_return …
    28   | joint_st_sequential instr _ ⇒ joint_st_sequential … instr l
    29   | joint_st_extension ].
    30   | ertl_st_comment s _ ⇒ ertl_st_comment s l
    31   | ertl_st_cost c _ ⇒ ertl_st_cost c l
    32   | ertl_st_get_hdw r1 r2 _ ⇒ ertl_st_get_hdw r1 r2 l
    33   | ertl_st_set_hdw r1 r2 _ ⇒ ertl_st_set_hdw r1 r2 l
    34   | ertl_st_hdw_to_hdw r1 r2 _ ⇒ ertl_st_hdw_to_hdw r1 r2 l
    35   | ertl_st_new_frame _ ⇒ ertl_st_new_frame l
    36   | ertl_st_del_frame _ ⇒ ertl_st_del_frame l
    37   | ertl_st_frame_size r _ ⇒ ertl_st_frame_size r l
    38   | ertl_st_pop r _ ⇒ ertl_st_pop r l
    39   | ertl_st_push r _ ⇒ ertl_st_push r l
    40   | ertl_st_addr r1 r2 x _ ⇒ ertl_st_addr r1 r2 x l
    41   | ertl_st_int r i _ ⇒ ertl_st_int r i l
    42   | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
    43   | ertl_st_opaccs opaccs d1 d2 s1 s2 _ ⇒ ertl_st_opaccs opaccs d1 s1 s1 s2 l
    44   | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
    45   | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
    46   | ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l
    47   | ertl_st_set_carry _ ⇒ ertl_st_set_carry l
    48   | ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l
    49   | ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l
    50   | ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l
    51   | ertl_st_cond a i1 i2 ⇒ ertl_st_cond a i1 i2
    52   | ertl_st_return ⇒ ertl_st_return
    53   ].
    54  
     14  | joint_st_return ⇒ joint_st_return ??
     15  | joint_st_sequential instr _ ⇒ joint_st_sequential … instr l].
     16
     17(* 
    5518let rec adds_graph
    5619  (stmt_list: list ertl_statement) (start_lbl: label)
     
    8548    ]
    8649  ].
     50*)
    8751
    8852axiom register_fresh: universe RegisterTag → register.
  • src/joint/Joint.ma

    r1250 r1252  
    33include "common/AST.ma".
    44include "common/Registers.ma".
     5include "utilities/extralib.ma". (* CSC: Only for Sigma type projections *)
    56include "common/Graphs.ma".
    67
     
    5657 }.
    5758
     59include alias "common/Graphs.ma". (* To pick the right lookup *)
     60
     61(* One common instantiation of params via Graphs of joint_statements *)
     62definition graph_params: params_ → ∀globals: list ident. params globals ≝
     63 λparams_,globals. mk_params globals params_ (graph (joint_statement params_ globals)) (lookup …).
     64
    5865record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
    5966{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
     
    7481(* Currified form *)
    7582definition set_joint_if_exit ≝
    76   λpars,globals.
     83  λglobals,pars.
    7784  λexit: label.
    78   λp: joint_internal_function pars globals.
     85  λp:joint_internal_function globals pars.
    7986  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
    80    mk_joint_internal_function pars globals
     87   mk_joint_internal_function globals pars
    8188    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    8289    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     
    8491
    8592definition set_luniverse ≝
    86   λglobals  : list ident.
    87   λp:params globals.
    88   λint_fun  : joint_internal_function globals p.
     93  λglobals,pars.
     94  λp : joint_internal_function globals pars.
    8995  λluniverse: universe LabelTag.
    90   let runiverse ≝ joint_if_runiverse … int_fun in
    91   let params    ≝ joint_if_params … int_fun in
    92   let locals    ≝ joint_if_locals … int_fun in
    93   let result    ≝ joint_if_result … int_fun in
    94   let stacksize ≝ joint_if_stacksize … int_fun in
    95   let code      ≝ joint_if_code … int_fun in
    96   let entry     ≝ joint_if_entry … int_fun in
    97   let exit      ≝ joint_if_exit … int_fun in
    98     mk_joint_internal_function globals p
    99       luniverse runiverse result params locals
    100       stacksize code entry exit.
     96   mk_joint_internal_function globals pars
     97    luniverse (joint_if_runiverse … p) (joint_if_result … p)
     98    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     99    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
     100
     101(* Specialized for graph_params *)
     102definition add_graph ≝
     103  λpars_,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars_ globals).
     104   let code ≝ add … (joint_if_code ?? p) l stmt in
     105    mk_joint_internal_function … (graph_params pars_ globals)
     106     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     107     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     108     code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
     109  normalize nodelta;
     110  [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
     111  #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
     112qed.
     113
     114definition set_locals ≝
     115  λglobals,pars.
     116  λp : joint_internal_function globals pars.
     117  λlocals.
     118   mk_joint_internal_function globals pars
     119    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     120    (joint_if_params … p) locals (joint_if_stacksize … p)
     121    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
    101122
    102123definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
Note: See TracChangeset for help on using the changeset viewer.