 Timestamp:
 Sep 28, 2011, 2:43:37 AM (9 years ago)
 Location:
 src/joint
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Joint.ma
r1275 r1280 17 17 18 18 ; extend_statements: Type[0] 19 20 ; resultT: Type[0]21 ; localsT: Type[0]22 ; paramsT: Type[0]23 19 }. 24 20 … … 27 23 ; succ: Type[0] 28 24 }. 25 26 (* One common instantiation of params via Graphs of joint_statements 27 (all languages but LIN) *) 28 definition graph_params_ : params__ → params_ ≝ 29 λpars__. mk_params_ pars__ label. 29 30 30 31 inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝ … … 52 53  joint_st_return: joint_statement p globals. 53 54 55 record params0: Type[1] ≝ 56 { pars__' :> params__ 57 ; resultT: Type[0] 58 ; paramsT: Type[0] 59 }. 60 61 record params1 : Type[1] ≝ 62 { pars0 :> params0 63 ; localsT: Type[0] 64 }. 54 65 55 66 record params (globals: list ident): Type[1] ≝ 56 { pars_:> params_ 67 { succ_ : Type[0] 68 ; pars1 :> params1 57 69 ; codeT: Type[0] 58 ; lookup: codeT → label → option (joint_statement pars_globals)70 ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals) 59 71 }. 72 73 definition params__of_params: ∀globals. params globals → params_ ≝ 74 λglobals,pars. mk_params_ pars (succ_ … pars). 75 coercion params__of_params: ∀globals.∀p: params globals. params_ ≝ params__of_params 76 on _p: params ? to params_. 60 77 61 78 include alias "common/Graphs.ma". (* To pick the right lookup *) 62 79 63 (* One common instantiation of params via Graphs of joint_statements *) 64 definition graph_params: params_ → ∀globals: list ident. params globals ≝ 65 λparams_,globals. mk_params globals params_ (graph (joint_statement params_ globals)) (lookup …). 80 (* One common instantiation of params via Graphs of joint_statements 81 (all languages but LIN) *) 82 definition graph_params: params1 → ∀globals: list ident. params globals ≝ 83 λpars1,globals. 84 mk_params globals label pars1 85 (graph (joint_statement (graph_params_ pars1) globals)) (lookup …). 86 87 88 (* CSC: special case where localsT is a list of register (RTL and ERTL) *) 89 definition rtl_ertl_params1 ≝ λpars0. mk_params1 pars0 (list register). 90 definition rtl_ertl_params ≝ λpars0. graph_params (rtl_ertl_params1 pars0). 66 91 67 92 record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝ … … 123 148 (* Specialized for graph_params *) 124 149 definition add_graph ≝ 125 λpars _,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars_globals).150 λpars1,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars1 globals). 126 151 let code ≝ add … (joint_if_code ?? p) l stmt in 127 mk_joint_internal_function … (graph_params pars_globals)152 mk_joint_internal_function … (graph_params … globals) 128 153 (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) 129 154 (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
Note: See TracChangeset
for help on using the changeset viewer.