Changeset 1252 for src/joint


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.