Changeset 1640 for src/joint/Joint_paolo.ma
 Timestamp:
 Jan 11, 2012, 5:41:45 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Joint_paolo.ma
r1635 r1640 6 6 7 7 (* Here is the structure of parameter records (downward edges are coercions, 8 the ¦ edge is the only explicitly defined coercion): 9 10 _____graph_params___ 11 / ¦ \ 12 / params \ 13 / / \  14 / stmt_params local_params 15 \   8 the ↓ edges are the only explicitly defined coercions). lin_params and 9 graph_params are simple wrappers of unserialized_params, and the coercions 10 from them to params instantiate the missing bits with values for linarized 11 programs and graph programs respectively. 12 13 lin_params graph_params 14  \_____ /____  15  / \  16 \_______ / ↓ ↓ 17 \ _\____ params 18 \_/ \  19 / \ \ ↓ 20 _____/ unserialized_params 21 / _______/  22 / /  23 stmt_params / local_params 24  __/  16 25 inst_params funct_params 17 26 … … 34 43 ; dph_arg: Type[0] (* high address registers *) 35 44 ; snd_arg : Type[0] (* second argument of binary op *) 36 ; operator1 : Type[0] (* = Op1 in all but RTLabs *)37 ; operator2 : Type[0] (* = Op2 in all but RTLabs *)38 45 ; pair_move: Type[0] (* argument of move instructions *) 39 46 ; call_args: Type[0] (* arguments of function calls *) … … 51 58  ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals 52 59  OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_instruction p globals 53  OP1: operator1 p→ acc_a_reg p → acc_a_reg p → joint_instruction p globals54  OP2: operator2 p→ acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals55 (* int , clear and set carry can bedone with generic move *)56 (* INT: generic_reg p → Byte → joint_instruction p globals 60  OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals 61  OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals 62 (* int done with generic move *) 63 (* INT: generic_reg p → Byte → joint_instruction p globals *) 57 64  CLEAR_CARRY: joint_instruction p globals 58  SET_CARRY: joint_instruction p globals *)65  SET_CARRY: joint_instruction p globals 59 66  LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_instruction p globals 60 67  STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_instruction p globals … … 62 69  COND: acc_a_reg p → label → joint_instruction p globals 63 70  extension: extend_statements p → joint_instruction p globals. 71 72 (* Paolo: to be moved elsewhere *) 73 74 notation "r ← a1 .op. a2" with precedence 50 for 75 @{'op2 $op $r $a1 $a2}. 76 notation "r ← . op . a" with precedence 50 for 77 @{'op1 $op $r $a}. 78 notation "r ← a" with precedence 50 for 79 @{'mov $r $a}. (* to be set in individual languages *) 80 notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for 81 @{'opaccs $op $r $s $a1 $a2}. 82 83 interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2). 84 interpretation "op1" 'op1 op r a = (OP1 ? ? op r a). 85 interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2). 86 87 64 88 65 89 definition inst_forall_labels : ∀p : inst_params.∀globals. … … 70 94  _ ⇒ True 71 95 ]. 72 73 record stmt_params : Type[1] ≝74 { inst_pars :> inst_params75 ; succ : Type[0]76 ; succ_choice : (succ = label) + (succ = unit)77 }.78 79 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝80  sequential: joint_instruction p globals → succ p → joint_statement p globals81  GOTO: label → joint_statement p globals82  RETURN: joint_statement p globals.83 84 (* for all labels in statement. Uses succ_choice to consider the successor of85 a statement when such successors are labels *)86 definition stmt_forall_labels : ∀p : stmt_params.∀globals.87 (label → Prop) → joint_statement p globals → Prop.88 *#i_pr#succ#succ_choice#globals#P*89 [#instr cases succ_choice #eq >eq #next90 [@(inst_forall_labels … P instr ∧ P next)91 @(inst_forall_labels … P instr)92 ]93 @P94 @True95 ]qed.96 96 97 97 record funct_params : Type[1] ≝ … … 105 105 }. 106 106 107 record unserialized_params : Type[1] ≝ 108 { u_inst_pars :> inst_params 109 ; u_local_pars :> local_params 110 }. 111 112 record stmt_params : Type[1] ≝ 113 { unserialized_pars :> unserialized_params 114 ; succ : Type[0] 115 ; succ_forall_labels : (label → Prop) → succ → Prop 116 }. 117 118 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝ 119  sequential: joint_instruction p globals → succ p → joint_statement p globals 120  GOTO: label → joint_statement p globals 121  RETURN: joint_statement p globals. 122 107 123 record params : Type[1] ≝ 108 124 { stmt_pars :> stmt_params 109 ; local_pars :> local_params110 125 ; codeT: list ident → Type[0] 111 126 ; lookup: ∀globals.codeT globals → label → option (joint_statement stmt_pars globals) 112 127 }. 113 128 129 130 (* for all labels in statement. Uses succ_choice to consider the successor of 131 a statement when such successors are labels *) 132 definition stmt_forall_labels : ∀p : stmt_params.∀globals. 133 (label → Prop) → joint_statement p globals → Prop ≝ 134 λp,g,P,stmt. match stmt with 135 [ sequential inst next ⇒ inst_forall_labels p g P inst ∧ succ_forall_labels p P next 136  GOTO l ⇒ P l 137  RETURN ⇒ True 138 ]. 139 140 record lin_params : Type[1] ≝ 141 { l_u_pars :> unserialized_params }. 142 143 include "utilities/option.ma". 144 145 definition lin_params_to_params ≝ 146 λlp : lin_params. mk_params 147 (mk_stmt_params lp unit (λ_.λ_.True)) 148 (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals))) 149 (* lookup ≝ *)(λglobals,code,lbl.find ?? 150 (λl_stmt. let 〈lbl_opt, stmt〉 ≝ l_stmt in 151 ! lbl' ← lbl_opt ; 152 if eq_identifier … lbl lbl' then return stmt else None ?) code). 153 154 coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params 155 on _lp : lin_params to params. 156 114 157 record graph_params : Type[1] ≝ 115 { g_inst_pars :> inst_params 116 ; g_local_pars :> local_params 117 }. 158 { g_u_pars :> unserialized_params }. 159 160 include alias "common/Graphs.ma". (* To pick the right lookup *) 161 162 (* One common instantiation of params via Graphs of joint_statements 163 (all languages but LIN) *) 164 definition graph_params_to_params ≝ 165 λgp : graph_params. mk_params 166 (mk_stmt_params gp label (λP.P)) 167 (* codeT ≝ *)(λglobals.graph (joint_statement ? globals)) 168 (* lookup ≝ *)(λglobals.lookup …). 169 170 coercion gp_to_p : ∀gp:graph_params.params ≝ λgp.graph_params_to_params gp 171 on _gp : graph_params to params. 172 118 173 119 174 definition labels_present : ∀p : params.∀globals. … … 130 185 forall_stmts … (labels_present … code) code. 131 186 132 include alias "common/Graphs.ma". (* To pick the right lookup *)133 134 135 (* One common instantiation of params via Graphs of joint_statements136 (all languages but LIN) *)137 definition params_of_graph_params: graph_params → params ≝138 λgp.139 let stmt_pars ≝ mk_stmt_params gp label (inl … (refl …)) in140 mk_params141 stmt_pars142 gp143 (* codeT ≝ *)(λglobals.graph (joint_statement stmt_pars globals))144 (λglobals.lookup …).145 146 coercion graph_params_to_params :147 ∀gp : graph_params.params ≝148 λgp.params_of_graph_params gp149 on _gp : graph_params to params.150 151 187 (* CSC: special case where localsT is a list of registers (RTL and ERTL) *) 152 definition rtl_ertl_params ≝ λinst_pars,funct_pars.153 params_of_graph_params (mk_graph_params inst_pars (mk_local_params funct_pars (list register))).188 definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars. 189 (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars (list register)))). 154 190 155 191 record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
Note: See TracChangeset
for help on using the changeset viewer.