 Timestamp:
 Sep 22, 2011, 2:49:18 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Joint.ma
r1250 r1252 3 3 include "common/AST.ma". 4 4 include "common/Registers.ma". 5 include "utilities/extralib.ma". (* CSC: Only for Sigma type projections *) 5 6 include "common/Graphs.ma". 6 7 … … 56 57 }. 57 58 59 include alias "common/Graphs.ma". (* To pick the right lookup *) 60 61 (* One common instantiation of params via Graphs of joint_statements *) 62 definition graph_params: params_ → ∀globals: list ident. params globals ≝ 63 λparams_,globals. mk_params globals params_ (graph (joint_statement params_ globals)) (lookup …). 64 58 65 record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝ 59 66 { joint_if_luniverse: universe LabelTag; (*CSC: used only for compilation*) … … 74 81 (* Currified form *) 75 82 definition set_joint_if_exit ≝ 76 λ pars,globals.83 λglobals,pars. 77 84 λexit: label. 78 λp: joint_internal_function pars globals.85 λp:joint_internal_function globals pars. 79 86 λprf: lookup … (joint_if_code … p) exit ≠ None ?. 80 mk_joint_internal_function pars globals87 mk_joint_internal_function globals pars 81 88 (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) 82 89 (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) … … 84 91 85 92 definition 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. 89 95 λ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 *) 102 definition 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 112 qed. 113 114 definition 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). 101 122 102 123 definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
Note: See TracChangeset
for help on using the changeset viewer.