 Timestamp:
 Jul 6, 2012, 11:25:43 AM (8 years ago)
 Location:
 src/joint
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Joint_paolo.ma
r1976 r2155 7 7 include "common/LabelledObjects.ma". 8 8 include "ASM/Util.ma". 9 include "basics/deqsets.ma". 10 include "basics/finset.ma". (* for DeqNat *) 9 include "common/StructuredTraces.ma". 11 10 12 11 (* Here is the structure of parameter records (downward edges are coercions, … … 37 36 params : adds type of code and related properties *) 38 37 38 inductive possible_flows : Type[0] ≝ 39  Labels : list label → possible_flows 40  Call : possible_flows. 41 39 42 record step_params : Type[1] ≝ 40 43 { acc_a_reg: Type[0] (* registers that will eventually need to be A *) … … 50 53 ; call_args: Type[0] (* arguments of function calls *) 51 54 ; call_dest: Type[0] (* possible destination of function computation *) 52 ; ext_step: Type[0] (* other instructions not fitting in the general framework *) 53 ; ext_step_labels : ext_step → list label 54 ; ext_fin_stmt: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *) 55 ; ext_fin_stmt_labels : ext_fin_stmt → list label 55 (* other instructions not fitting in the general framework *) 56 ; ext_seq : Type[0] 57 (* ; ext_branch : Type[0] 58 ; ext_branch_labels : ext_branch → list label*) 59 ; ext_call : Type[0] 60 ; ext_tailcall : Type[0] 61 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *) 56 62 }. 57 58 inductive joint_s tep(p:step_params) (globals: list ident): Type[0] ≝59  COMMENT: String → joint_s tepp globals60  COST_LABEL: costlabel → joint_s tepp globals61  MOVE: pair_move p → joint_s tepp globals62  POP: acc_a_reg p → joint_s tepp globals63  PUSH: acc_a_arg p → joint_s tepp globals64  ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_s tepp globals65  OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_s tepp globals66  OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_s tepp globals67  OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_s tepp globals63 64 inductive joint_seq (p:step_params) (globals: list ident): Type[0] ≝ 65  COMMENT: String → joint_seq p globals 66  COST_LABEL: costlabel → joint_seq p globals 67  MOVE: pair_move p → joint_seq p globals 68  POP: acc_a_reg p → joint_seq p globals 69  PUSH: acc_a_arg p → joint_seq p globals 70  ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_seq p globals 71  OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals 72  OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals 73  OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_seq p globals 68 74 (* int done with generic move *) 69 (* INT: generic_reg p → Byte → joint_step p globals *) 70  CLEAR_CARRY: joint_step p globals 71  SET_CARRY: joint_step p globals 72  LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_step p globals 73  STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_step p globals 74  CALL_ID: ident → call_args p → call_dest p → joint_step p globals 75  COND: acc_a_reg p → label → joint_step p globals 76  extension: ext_step p → joint_step p globals. 75 (* INT: generic_reg p → Byte → joint_seq p globals *) 76  CLEAR_CARRY: joint_seq p globals 77  SET_CARRY: joint_seq p globals 78  LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals 79  STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals 80  extension_seq : ext_seq p → joint_seq p globals. 77 81 78 82 axiom EmptyString : String. … … 92 96 interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2). 93 97 94 coercion extension_to_step : ∀p,globals.∀s : ext_step p.joint_step p globals ≝ 95 extension on _s : ext_step ? to joint_step ??. 98 coercion extension_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝ 99 extension_seq on _s : ext_seq ? to joint_seq ??. 100 101 inductive joint_call (p : step_params) : Type[0] ≝ 102  CALL_ID: ident → call_args p → call_dest p → joint_call p 103  extension_call : ext_call p → joint_call p. 104 105 coercion extension_to_call : ∀p.∀s : ext_call p.joint_call p ≝ 106 extension_call on _s : ext_call ? to joint_call ?. 107 108 inductive joint_branch (p : step_params) : Type[0] ≝ 109  COND: acc_a_reg p → label → joint_branch p 110 (* extension_branch : ext_branch p → joint_branch p*). 111 112 (*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝ 113 extension_branch on _s : ext_branch ? to joint_branch ?.*) 114 115 inductive joint_step (p : step_params) (globals : list ident) : Type[0] ≝ 116  step_seq : joint_seq p globals → joint_step p globals 117  step_call : joint_call p → joint_step p globals 118  step_branch : joint_branch p → joint_step p globals. 119 120 coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝ 121 step_seq on _s : joint_seq ?? to joint_step ??. 122 coercion call_to_step : ∀p,globals.∀s : joint_call p.joint_step p globals ≝ 123 step_call on _s : joint_call ? to joint_step ??. 124 coercion branch_to_step : ∀p,globals.∀s : joint_branch p.joint_step p globals ≝ 125 step_branch on _s : joint_branch ? to joint_step ??. 126 127 definition step_flows ≝ λp,globals.λs : joint_step p globals. 128 match s with 129 [ step_seq _ ⇒ Labels … [ ] 130  step_call _ ⇒ Call 131  step_branch s ⇒ 132 match s with 133 [ COND _ l ⇒ Labels … [l] 134 (* extension_branch s' ⇒ Labels … (ext_branch_labels … s')*) 135 ] 136 ]. 96 137 97 138 definition step_labels ≝ 98 139 λp, globals.λs : joint_step p globals. 99 match s with 100 [ COND _ l ⇒ [l] 101  extension ext_s ⇒ ext_step_labels ? ext_s 102  _ ⇒ [ ] 140 match step_flows … s with 141 [ Labels lbls ⇒ lbls 142  Call ⇒ [ ] 103 143 ]. 104 144 … … 106 146 (label → Prop) → joint_step p globals → Prop ≝ 107 147 λp,g,P,inst. All … P (step_labels … inst). 108 148 149 definition step_classifier : 150 ∀p : step_params.∀globals. 151 joint_step p globals → status_class ≝ λp,g,s. 152 match s with 153 [ step_seq _ ⇒ cl_other 154  step_call _ ⇒ cl_call 155  step_branch _ ⇒ cl_jump 156 ]. 157 109 158 record funct_params : Type[1] ≝ 110 159 { resultT : Type[0] … … 117 166 }. 118 167 119 120 168 record unserialized_params : Type[1] ≝ 121 169 { u_inst_pars :> step_params … … 129 177 }. 130 178 131 inductive joint_fin_step (p: stmt_params) (globals: list ident): Type[0] ≝ 132  GOTO: label → joint_fin_step p globals 133  RETURN: joint_fin_step p globals 134  extension_fin : ext_fin_stmt p → joint_fin_step p globals. 179 inductive joint_fin_step (p: step_params): Type[0] ≝ 180  GOTO: label → joint_fin_step p 181  RETURN: joint_fin_step p 182  tailcall : ext_tailcall p → joint_fin_step p. 183 184 definition fin_step_flows ≝ λp.λs : joint_fin_step p. 185 match s with 186 [ GOTO l ⇒ Labels … [l] 187  _ ⇒ Labels … [ ] (* tailcalls will need to be integrated in structured traces *) 188 ]. 189 190 definition fin_step_labels ≝ 191 λp.λs : joint_fin_step p. 192 match fin_step_flows … s with 193 [ Labels lbls ⇒ lbls 194  Call ⇒ [ ] 195 ]. 196 197 definition fin_step_classifier : 198 ∀p : stmt_params. 199 joint_fin_step p → status_class 200 ≝ λp,s. 201 match s with 202 [ GOTO _ ⇒ cl_other 203  _ ⇒ cl_return 204 ]. 135 205 136 206 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝ 137 207  sequential: joint_step p globals → succ p → joint_statement p globals 138  final: joint_fin_step p globals → joint_statement p globals. 139 140 coercion extension_fin_to_fin_step : ∀p : stmt_params.∀globals. 141 ∀s : ext_fin_stmt p.joint_fin_step p globals ≝ 142 extension_fin on _s : ext_fin_stmt ? to joint_fin_step ??. 208  final: joint_fin_step p → joint_statement p globals. 209 210 definition stmt_classifier : 211 ∀p : stmt_params.∀globals. 212 joint_statement p globals → status_class 213 ≝ λp,g,s. 214 match s with 215 [ sequential stp _ ⇒ step_classifier p g stp 216  final stp ⇒ fin_step_classifier p stp 217 ]. 218 219 coercion extension_fin_to_fin_step : ∀p : stmt_params. 220 ∀s : ext_tailcall p.joint_fin_step p ≝ 221 tailcall on _s : ext_tailcall ? to joint_fin_step ?. 143 222 144 223 coercion fin_step_to_stmt : ∀p : stmt_params.∀globals. 145 ∀s : joint_fin_step p globals.joint_statement p globals ≝146 final on _s : joint_fin_step ? ?to joint_statement ??.224 ∀s : joint_fin_step p.joint_statement p globals ≝ 225 final on _s : joint_fin_step ? to joint_statement ??. 147 226 148 227 record params : Type[1] ≝ 149 228 { stmt_pars :> stmt_params 150 229 ; codeT: list ident → Type[0] 151 ; code_point : DeqSet230 ; code_point : Type[0] 152 231 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals) 153 232 ; point_of_label : ∀globals.codeT globals → label → option code_point … … 192 271 [ Some pt ⇒ code_has_point … c pt 193 272  None ⇒ false 194 ].195 196 definition fin_step_labels ≝197 λp,globals.λs : joint_fin_step p globals.198 match s with199 [ GOTO l ⇒ [ l ]200  RETURN ⇒ [ ]201  extension_fin c ⇒ ext_fin_stmt_labels … c202 273 ]. 203 274 … … 254 325 255 326 record lin_params : Type[1] ≝ 256 { l_u_pars : >unserialized_params }.327 { l_u_pars : unserialized_params }. 257 328 258 329 lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (l). … … 290 361 λlp : lin_params. 291 362 mk_params 292 (mk_stmt_params lpunit (λ_.None ?))363 (mk_stmt_params (l_u_pars lp) unit (λ_.None ?)) 293 364 (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals))) 294 (* code_point ≝ *) DeqNat365 (* code_point ≝ *)ℕ 295 366 (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls) 296 367 (* point_of_label ≝ *)(λglobals,c,lbl. … … 325 396 326 397 record graph_params : Type[1] ≝ 327 { g_u_pars : >unserialized_params }.398 { g_u_pars : unserialized_params }. 328 399 329 400 (* One common instantiation of params via Graphs of joint_statements … … 332 403 λgp : graph_params. 333 404 mk_params 334 (mk_stmt_params gplabel (Some ?))405 (mk_stmt_params (g_u_pars gp) label (Some ?)) 335 406 (* codeT ≝ *)(λglobals.graph (joint_statement ? globals)) 336 (* code_point ≝ *) (Deq_identifier LabelTag)407 (* code_point ≝ *)label 337 408 (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code) 338 409 (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl) 
src/joint/TranslateUtils_paolo.ma
r1882 r2155 1 1 include "joint/Joint_paolo.ma". 2 include " utilities/bindLists.ma".2 include "joint/blocks.ma". 3 3 4 4 (* general type of functions generating fresh things *) … … 35 35 36 36 (* insert into a graph a block of instructions *) 37 let rec adds_graph 37 let rec adds_graph_list 38 38 (g_pars: graph_params) 39 39 (globals: list ident) 40 (insts: list (joint_s tepg_pars globals))40 (insts: list (joint_seq g_pars globals)) 41 41 (src : label) 42 (de st : label)43 (def: joint_internal_function … g_pars) on insts≝42 (def: joint_internal_function … g_pars) on insts 43 : (joint_internal_function … g_pars) × label ≝ 44 44 match insts with 45 [ nil ⇒ add_graph … src (GOTO … dest) def45 [ nil ⇒ 〈def, src〉 46 46  cons instr others ⇒ 47 match others with 48 [ nil ⇒ (* only one instruction *) 49 add_graph … src (sequential … instr dest) def 50  _ ⇒ (* need to generate label *) 51 let 〈def, tmp_lbl〉 ≝ fresh_label … def in 52 adds_graph g_pars globals others tmp_lbl dest 53 (add_graph … src (sequential … instr tmp_lbl) def) 54 ] 47 let 〈def, mid〉 ≝ fresh_label … def in 48 let def ≝ add_graph … src (sequential … instr mid) def in 49 adds_graph_list g_pars globals others mid def 50 ]. 51 52 definition adds_graph : 53 ∀g_pars : graph_params. 54 ∀globals: list ident. 55 ∀b : seq_block g_pars globals (joint_step g_pars globals) + 56 seq_block g_pars globals (joint_fin_step g_pars). 57 label → if is_inl … b then label else unit → 58 joint_internal_function … g_pars → joint_internal_function … g_pars ≝ 59 λg_pars,globals,insts,src. 60 match insts return λx.if is_inl … x then ? else ? → ? → ? with 61 [ inl b ⇒ λdst,def. 62 let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in 63 add_graph … mid (sequential … (\snd b) dst) def 64  inr b ⇒ λdst,def. 65 let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in 66 add_graph … mid (final … (\snd b)) def 55 67 ]. 56 68 … … 60 72 (* fresh register creation *) 61 73 freshT globals g_pars (localsT … g_pars) → 62 ∀ insts: bind_list (localsT … g_pars) (joint_step g_pars globals).63 ∀src : label.64 ∀dest : label.74 ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) + 75 bind_seq_block g_pars globals (joint_fin_step g_pars). 76 label → if is_inl … b then label else unit → 65 77 joint_internal_function globals g_pars → 66 78 joint_internal_function globals g_pars ≝ 67 λg_pars,globals,fresh_r,insts,src,dest,def. 68 let 〈def', stmts〉 ≝ bcompile … fresh_r insts def in 69 adds_graph … stmts src dest def'. 79 λg_pars,globals,fresh_r,insts,src. 80 match insts return λx.if is_inl … x then ? else ? → ? → ? with 81 [ inl b ⇒ λdst,def. 82 let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in 83 adds_graph … (inl … stmts) src dst def 84  inr b ⇒ λdst,def. 85 let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in 86 adds_graph … (inr … stmts) src dst def 87 ]. 70 88 71 89 (* translation with inline fresh register allocation *) … … 75 93 (* fresh register creation *) 76 94 freshT globals dst_g_pars (localsT dst_g_pars) → 77 (* function dictating the translation *)78 (label → joint_step src_g_pars globals →79 bind_list (localsT dst_g_pars) (joint_step dst_g_pars globals)80 (* this can be added to allow redirections: × label *)) →81 (label → ext_fin_stmt src_g_pars →82 bind_new (localsT dst_g_pars)83 ((list (joint_step dst_g_pars globals))84 ×85 (joint_statement dst_g_pars globals))) →86 95 (* initialized function definition with empty graph *) 87 96 joint_internal_function globals dst_g_pars → 97 (* functions dictating the translation *) 98 (label → joint_step src_g_pars globals → 99 bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) → 100 (label → joint_fin_step src_g_pars → 101 bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) → 88 102 (* source function *) 89 103 joint_internal_function globals src_g_pars → 90 104 (* destination function *) 91 joint_internal_function globals dst_g_pars ≝ 92 λsrc_g_pars,dst_g_pars,globals,fresh_reg, trans,trans',empty,def.105 joint_internal_function globals dst_g_pars ≝ 106 λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def. 93 107 let f : label → joint_statement (src_g_pars : params) globals → 94 108 joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝ 95 109 λlbl,stmt,def. 96 110 match stmt with 97 [ sequential inst next ⇒ b_adds_graph … fresh_reg (trans lbl inst) lbl next def 98  GOTO next ⇒ add_graph … lbl (GOTO … next) def 99  RETURN ⇒ add_graph … lbl (RETURN …) def 100  extension_fin c ⇒ 101 let 〈def', p〉 ≝ bcompile … fresh_reg (trans' lbl c) def in 102 let 〈insts, fin〉 ≝ p in 103 let 〈def'', tmp_lbl〉 ≝ fresh_label … def' in 104 adds_graph … insts lbl tmp_lbl (add_graph … tmp_lbl fin def) 111 [ sequential inst next ⇒ 112 b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def 113  final inst ⇒ 114 b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def 105 115 ] in 106 116 foldi … f (joint_if_code … def) empty. 107 117 (* 108 118 (* translation without register allocation *) 109 119 definition graph_translate : … … 137 147 ] in 138 148 foldi ??? f (joint_if_code ?? def) empty. 139 149 *) 150 (* 140 151 definition graph_to_lin_statement : 141 152 ∀p : unserialized_params.∀globals. 142 153 joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝ 143 λp,globals,stmt.match stmt return λ_.joint_statement (mk_lin_params p) globalswith154 λp,globals,stmt.match stmt with 144 155 [ sequential c _ ⇒ sequential … c it 145  GOTO l ⇒ GOTO … l 146  RETURN ⇒ RETURN … 147  extension_fin c ⇒ extension_fin … c 156  final c ⇒ 157 final ?? match c return λx.joint_fin_step (mk_lin_params p) globals with 158 [ GOTO l ⇒ GOTO … l 159  RETURN ⇒ RETURN … 160  extension_fin c ⇒ extension_fin ?? c 161 ] 148 162 ]. 149 163 … … 152 166 stmt_labels … (graph_to_lin_statement p globals s) = 153 167 stmt_explicit_labels … s. 154 #p#globals * //168 #p#globals * [//] * // 155 169 qed. 156 170 … … 216 230 (**)⊢ 217 231 list lo ≡ codeT lp globals. 232 218 233 219 234 definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals. … … 791 806 #f_out * #f_out_closed #H assumption 792 807 qed. 793 794 808 *) 795 809 796 810 
src/joint/blocks.ma
r2042 r2155 1 1 include "joint/Joint_paolo.ma". 2 include "utilities/bind_new.ma". 3 4 definition uncurry_helper : ∀A,B,C : Type[0].(A → B → C) → (A×B) → C ≝ 5 λA,B,C,f,p.f (\fst p) (\snd p). 6 7 inductive stmt_type : Type[0] ≝ 8  SEQ : stmt_type 9  FIN : stmt_type. 10 11 definition stmt_type_if : ∀A : Type[1].stmt_type → A → A → A ≝ 12 λA,t,x,y.match t with [ SEQ ⇒ x  FIN ⇒ y ]. 13 14 definition block_cont ≝ λp : params.λglobals,ty. 15 (list (joint_step p globals)) × 16 (stmt_type_if ? ty (joint_step p) (joint_fin_step p) globals). 17 18 definition Skip : ∀p,globals.block_cont p globals SEQ ≝ 19 λp,globals.〈[ ], NOOP …〉. 20 21 definition instr_block ≝ λp : params.λglobals,ty. 22 bind_new (localsT p) (block_cont p globals ty). 23 unification hint 0 ≔ p, globals, ty; 24 B ≟ block_cont p globals ty, R ≟ localsT p 2 include "utilities/bindLists.ma". 3 4 inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝ 5  block_seq : joint_seq p globals → block_step p globals 6  block_skip : label → block_step p globals. 7 8 definition if_seq : ∀p,globals.∀A:Type[2].block_step p globals → A → A → A ≝ 9 λp,g,A,s.match s with 10 [ block_seq _ ⇒ λx,y.x 11  _ ⇒ λx,y.y 12 ]. 13 14 definition stmt_of_block_step : ∀p : stmt_params.∀globals. 15 ∀s : block_step p globals.if_seq … s (succ p) unit → joint_statement p globals ≝ 16 λp,g,s.match s return λx.if_seq ??? x ?? → joint_statement ?? with 17 [ block_seq s' ⇒ λnxt.sequential … s' nxt 18  block_skip l ⇒ λ_.GOTO … l 19 ]. 20 21 definition seq_to_block_step_list : ∀p : stmt_params.∀globals. 22 list (joint_seq p globals) → 23 list (block_step p globals) ≝ λp,globals.map ?? (block_seq ??). 24 25 coercion block_step_from_seq_list : ∀p : stmt_params.∀globals. 26 ∀l:list (joint_seq p globals). 27 list (block_step p globals) ≝ 28 seq_to_block_step_list 29 on _l:list (joint_seq ??) 30 to list (block_step ??). 31 32 definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with 33 [ inl _ ⇒ true 34  inr _ ⇒ false 35 ]. 36 definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with 37 [ inl _ ⇒ true 38  inr _ ⇒ false 39 ]. 40 41 definition skip_block ≝ λp,globals,A. 42 (list (block_step p globals)) × A. 43 44 definition seq_block ≝ λp : stmt_params.λglobals,A. 45 (list (joint_seq p globals)) × A. 46 47 definition seq_to_skip_block : 48 ∀p,g,A.seq_block p g A → skip_block p g A 49 ≝ λp,g,A,b.〈\fst b, \snd b〉. 50 51 coercion skip_from_seq_block : 52 ∀p,g,A.∀b : seq_block p g A.skip_block p g A ≝ 53 seq_to_skip_block on _b : seq_block ??? to skip_block ???. 54 55 definition bind_seq_block ≝ λp : stmt_params.λglobals,A. 56 bind_new (localsT p) (seq_block p globals A). 57 unification hint 0 ≔ p : stmt_params, g, X; 58 R ≟ localsT p, 59 P ≟ seq_block p g X 25 60 (**)⊢ 26 instr_block p globals ty ≡ bind_new R B. 27 28 definition block_cont_append : 29 ∀p,g,ty. 30 ∀b1 : block_cont p g SEQ. 31 ∀b2 : block_cont p g ty. 32 block_cont p g ty ≝ 33 λp,globals,ty,b1,b2.〈\fst b1 @ \snd b1 :: \fst b2, \snd b2〉. 34 35 definition block_cont_cons ≝ λp,g,ty,x.λb : block_cont p g ty.〈x :: \fst b,\snd b〉. 36 37 interpretation "block contents cons" 'cons x b = (block_cont_cons ??? x b). 38 interpretation "block contents append" 'append b1 b2 = (block_cont_append ??? b1 b2). 39 40 definition step_to_block : ∀p : params.∀g. 41 joint_step p g → block_cont p g SEQ ≝ λp,g,s.〈[ ], s〉. 42 43 definition fin_step_to_block : ∀p : params.∀g. 44 joint_fin_step p g → block_cont p g FIN ≝ λp,g,s.〈[ ], s〉. 45 46 coercion block_from_step : ∀p : params.∀g.∀s : joint_step p g. 47 block_cont p g SEQ ≝ step_to_block on _s : joint_step ?? to block_cont ?? SEQ. 48 49 coercion block_from_fin_step : ∀p : params.∀g.∀s : joint_fin_step p g. 50 block_cont p g FIN ≝ fin_step_to_block 51 on _s : joint_fin_step ?? to block_cont ?? FIN. 52 53 definition block_cons : 54 ∀p : params.∀globals,ty. 55 joint_step p globals → instr_block p globals ty → instr_block p globals ty 56 ≝ λp,globals,ty,x.m_map … (block_cont_cons … x). 57 58 definition block_append : 59 ∀p : params.∀globals,ty. 60 instr_block p globals SEQ → instr_block p globals ty → instr_block p globals ty ≝ 61 λp,globals,ty.m_bin_op … (block_cont_append …). 62 63 interpretation "instruction block cons" 'cons x b = (block_cons ??? x b). 64 interpretation "instruction block append" 'append b1 b2 = (block_append ??? b1 b2). 65 66 let rec is_block_instance (p : params) g ty (b : instr_block p g ty) (l : list (localsT p)) (b' : block_cont p g ty) on b : Prop ≝ 61 bind_seq_block p g X ≡ bind_new R P. 62 63 definition bind_seq_list ≝ λp : stmt_params.λglobals. 64 bind_new (localsT p) (list (joint_seq p globals)). 65 unification hint 0 ≔ p : stmt_params, g; 66 R ≟ localsT p, 67 S ≟ joint_seq p g, 68 L ≟ list S 69 (**)⊢ 70 bind_seq_list p g ≡ bind_new R L. 71 72 definition bind_skip_block ≝ λp : stmt_params.λglobals,A. 73 bind_new (localsT p) (skip_block p globals A). 74 unification hint 0 ≔ p : stmt_params, g, A; 75 B ≟ skip_block p g A, R ≟ localsT p 76 (**)⊢ 77 bind_skip_block p g A ≡ bind_new R B. 78 79 definition bind_seq_to_skip_block : 80 ∀p,g,A.bind_seq_block p g A → bind_skip_block p g A ≝ 81 λp,g,A.m_map ? (seq_block p g A) (skip_block p g A) 82 (λx.x). 83 84 coercion bind_skip_from_seq_block : 85 ∀p,g,A.∀b:bind_seq_block p g A.bind_skip_block p g A ≝ 86 bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???. 87 (* 88 definition block_classifier ≝ 89 λp,g.λb : other_block p g. 90 seq_or_fin_step_classifier ?? (\snd b). 91 *) 92 93 let rec split_on_last A (dflt : A) (l : list A) on l : (list A) × A ≝ 94 match l with 95 [ nil ⇒ 〈[ ], dflt〉 96  cons hd tl ⇒ 97 match tl with 98 [ nil ⇒ 〈[ ], hd〉 99  _ ⇒ 100 let 〈pref, post〉 ≝ split_on_last A dflt tl in 101 〈hd :: pref, post〉 102 ] 103 ]. 104 105 lemma split_on_last_ok : 106 ∀A,dflt,l. 107 match l with 108 [ nil ⇒ True 109  _ ⇒ l = (let 〈pre, post〉 ≝ split_on_last A dflt l in pre @ [post]) 110 ]. 111 #A #dflt #l elim l normalize nodelta 112 [ % 113  #hd * [ #_ %] 114 #hd' #tl #IH whd in match (split_on_last ???); >IH in ⊢ (??%?); 115 elim (split_on_last ???) #a #b % 116 ] 117 qed. 118 119 definition seq_block_from_seq_list : 120 ∀p : stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝ 121 λp,g,l.let 〈pre,post〉 ≝ split_on_last … (NOOP ??) l in 〈pre, (post : joint_step ??)〉. 122 123 definition bind_seq_block_from_bind_seq_list : 124 ∀p : stmt_params.∀g.bind_new (localsT p) (list (joint_seq p g)) → 125 bind_seq_block p g (joint_step p g) ≝ λp.λg.m_map … (seq_block_from_seq_list …). 126 127 definition bind_seq_block_step : 128 ∀p,g.bind_seq_block p g (joint_step p g) → 129 bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝ 130 λp,g.inl …. 131 coercion bind_seq_block_from_step : 132 ∀p,g.∀b:bind_seq_block p g (joint_step p g). 133 bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝ 134 bind_seq_block_step on _b : bind_seq_block ?? (joint_step ??) to 135 bind_seq_block ?? (joint_step ??) + bind_seq_block ?? (joint_fin_step ?). 136 137 definition bind_seq_block_fin_step : 138 ∀p,g.bind_seq_block p g (joint_fin_step p) → 139 bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝ 140 λp,g.inr …. 141 coercion bind_seq_block_from_fin_step : 142 ∀p,g.∀b:bind_seq_block p g (joint_fin_step p). 143 bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝ 144 bind_seq_block_fin_step on _b : bind_seq_block ?? (joint_fin_step ?) to 145 bind_seq_block ?? (joint_step ??) + bind_seq_block ?? (joint_fin_step ?). 146 147 definition seq_block_bind_seq_block : 148 ∀p : stmt_params.∀g,A.seq_block p g A → bind_seq_block p g A ≝ λp,g,A.bret …. 149 coercion seq_block_to_bind_seq_block : 150 ∀p : stmt_params.∀g,A.∀b:seq_block p g A.bind_seq_block p g A ≝ 151 seq_block_bind_seq_block 152 on _b : seq_block ??? to bind_seq_block ???. 153 154 definition joint_step_seq_block : ∀p : stmt_params.∀g.joint_step p g → seq_block p g (joint_step p g) ≝ 155 λp,g,x.〈[ ], x〉. 156 coercion joint_step_to_seq_block : ∀p : stmt_params.∀g.∀b : joint_step p g.seq_block p g (joint_step p g) ≝ 157 joint_step_seq_block on _b : joint_step ?? to seq_block ?? (joint_step ??). 158 159 definition joint_fin_step_seq_block : ∀p : stmt_params.∀g.joint_fin_step p → seq_block p g (joint_fin_step p) ≝ 160 λp,g,x.〈[ ], x〉. 161 coercion joint_fin_step_to_seq_block : ∀p : stmt_params.∀g.∀b : joint_fin_step p.seq_block p g (joint_fin_step p) ≝ 162 joint_fin_step_seq_block on _b : joint_fin_step ? to seq_block ?? (joint_fin_step ?). 163 164 definition seq_list_seq_block : 165 ∀p:stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝ 166 λp,g,l.let pr ≝ split_on_last … (NOOP ??) l in 〈\fst pr, \snd pr〉. 167 coercion seq_list_to_seq_block : 168 ∀p:stmt_params.∀g.∀l:list (joint_seq p g).seq_block p g (joint_step p g) ≝ 169 seq_list_seq_block on _l : list (joint_seq ??) to seq_block ?? (joint_step ??). 170 171 definition bind_seq_list_bind_seq_block : 172 ∀p:stmt_params.∀g.bind_new (localsT p) (list (joint_seq p g)) → bind_seq_block p g (joint_step p g) ≝ 173 λp,g.m_map ??? (λx : list (joint_seq ??).(x : seq_block ???)). 174 175 coercion bind_seq_list_to_bind_seq_block : 176 ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝ 177 bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??). 178 179 (* 180 181 definition seq_block_append : 182 ∀p,g. 183 ∀b1 : Σb.is_safe_block p g b. 184 ∀b2 : seq_block p g. 185 seq_block p g ≝ λp,g,b1,b2. 186 〈match b1 with 187 [ mk_Sig instr prf ⇒ 188 match \snd instr return λx.bool_to_Prop (is_inl … x) ∧ seq_or_fin_step_classifier … x = ? → ? with 189 [ inl i ⇒ λprf.\fst b1 @ i :: \fst b2 190  inr _ ⇒ λprf.⊥ 191 ] prf 192 ],\snd b2〉. 193 cases prf #H1 #H2 assumption 194 qed. 195 196 definition other_block_append : 197 ∀p,g. 198 (Σb.block_classifier ?? b = cl_other) → 199 other_block p g → 200 other_block p g ≝ λp,g,b1,b2. 201 〈\fst b1 @ «\snd b1, pi2 … b1» :: \fst b2, \snd b2〉. 202 203 definition seq_block_cons : ∀p : stmt_params.∀g.(Σs.step_classifier p g s = cl_other) → 204 seq_block p g → seq_block p g ≝ 205 λp,g,x,b.〈x :: \fst b,\snd b〉. 206 definition other_block_cons : ∀p,g. 207 (Σs.seq_or_fin_step_classifier p g s = cl_other) → other_block p g → 208 other_block p g ≝ 209 λp,g,x,b.〈x :: \fst b,\snd b〉. 210 211 interpretation "seq block cons" 'cons x b = (seq_block_cons ?? x b). 212 interpretation "other block cons" 'vcons x b = (other_block_cons ?? x b). 213 interpretation "seq block append" 'append b1 b2 = (seq_block_append ?? b1 b2). 214 interpretation "other block append" 'vappend b1 b2 = (other_block_append ?? b1 b2). 215 216 definition step_to_block : ∀p,g. 217 seq_or_fin_step p g → seq_block p g ≝ λp,g,s.〈[ ], s〉. 218 219 coercion block_from_step : ∀p,g.∀s : seq_or_fin_step p g. 220 seq_block p g ≝ step_to_block on _s : seq_or_fin_step ?? to seq_block ??. 221 222 definition bind_seq_block_cons : 223 ∀p : stmt_params.∀g,is_seq. 224 (Σs.step_classifier p g s = cl_other) → bind_seq_block p g is_seq → 225 bind_seq_block p g is_seq ≝ 226 λp,g,is_seq,x.m_map ??? (λb.〈x::\fst b,\snd b〉). 227 228 definition bind_other_block_cons : 229 ∀p,g.(Σs.seq_or_fin_step_classifier p g s = cl_other) → bind_other_block p g → bind_other_block p g ≝ 230 λp,g,x.m_map … (other_block_cons … x). 231 232 let rec bind_pred_aux B X (P : X → Prop) (c : bind_new B X) on c : Prop ≝ 233 match c with 234 [ bret x ⇒ P x 235  bnew f ⇒ ∀b.bind_pred_aux B X P (f b) 236 ]. 237 238 let rec bind_pred_inj_aux B X (P : X → Prop) (c : bind_new B X) on c : 239 bind_pred_aux B X P c → bind_new B (Σx.P x) ≝ 240 match c return λx.bind_pred_aux B X P x → bind_new B (Σx.P x) with 241 [ bret x ⇒ λprf.return «x, prf» 242  bnew f ⇒ λprf.bnew … (λx.bind_pred_inj_aux B X P (f x) (prf x)) 243 ]. 244 245 definition bind_pred ≝ λB. 246 mk_InjMonadPred (BindNew B) 247 (mk_MonadPred ? 248 (bind_pred_aux B) 249 ???) 250 (λX,P,c_sig.bind_pred_inj_aux B X P c_sig (pi2 … c_sig)) 251 ?. 252 [ #X #P #Q #H #y elim y [ #x @H  #f #IH #G #b @IH @G] 253  #X #Y #Pin #Pout #m elim m [#x  #f #IH] #H #g #G [ @G @H  #b @(IH … G) @H] 254  #X #P #x #Px @Px 255  #X #P * #m elim m [#x  #f #IH] #H [ %  @bnew_proper #b @IH] 256 ] 257 qed. 258 259 definition bind_seq_block_append : 260 ∀p,g,is_seq.(Σb : bind_seq_block p g true.bind_pred ? (λb.step_classifier p g (\snd b) = cl_other) b) → 261 bind_seq_block p g is_seq → bind_seq_block p g is_seq ≝ 262 λp,g,is_seq,b1,b2. 263 !«p, prf» ← mp_inject … b1; 264 !〈post, last〉 ← b2; 265 return 〈\fst p @ «\snd p, prf» :: post, last〉. 266 267 definition bind_other_block_append : 268 ∀p,g.(Σb : bind_other_block p g.bind_pred ? 269 (λx.block_classifier ?? x = cl_other) b) → 270 bind_other_block p g → bind_other_block p g ≝ 271 λp,g,b1.m_bin_op … (other_block_append ??) (mp_inject … b1). 272 273 interpretation "bind seq block cons" 'cons x b = (bind_seq_block_cons ??? x b). 274 interpretation "bind other block cons" 'vcons x b = (bind_other_block_cons ?? x b). 275 interpretation "bind seq block append" 'append b1 b2 = (bind_seq_block_append ??? b1 b2). 276 interpretation "bind other block append" 'vappend b1 b2 = (bind_other_block_append ?? b1 b2). 277 278 let rec instantiates_to B X 279 (b : bind_new B X) (l : list B) (x : X) on b : Prop ≝ 67 280 match b with 68 281 [ bret B ⇒ 69 282 match l with 70 [ nil ⇒ B = b'71  cons __ ⇒ False283 [ nil ⇒ x = B 284  _ ⇒ False 72 285 ] 73 286  bnew f ⇒ … … 75 288 [ nil ⇒ False 76 289  cons r l' ⇒ 77 i s_block_instance p g ty (f r) l' b'290 instantiates_to B X (f r) l' x 78 291 ] 79 292 ]. 80 293 81 lemma is_block_instance_append : ∀p,globals,ty,b1,b2,l1,l2,b1',b2'. 82 is_block_instance p globals SEQ b1 l1 b1' → 83 is_block_instance p globals ty b2 l2 b2' → 84 is_block_instance p globals ty (b1 @ b2) (l1 @ l2) (b1' @ b2'). 85 #p#globals#ty #b1 elim b1 86 [ #B1  #f1 #IH1 ] #b2 * [2,4: #r1 #l1' ] #l2 #b1' #b2' [1,4: *] 87 normalize in ⊢ (%→?); 294 lemma instantiates_to_bind_pred : 295 ∀B,X,P,b,l,x.instantiates_to B X b l x → bind_pred B P b → P x. 296 #B #X #P #b elim b 297 [ #x * [ #y #EQ >EQ normalize //  #hd #tl #y *] 298  #f #IH * [ #y *  #hd #tl normalize #b #H #G @(IH … H) @G ] 299 ] 300 qed. 301 302 lemma seq_block_append_proof_irr : 303 ∀p,g,b1,b1',b2.pi1 ?? b1 = pi1 ?? b1' → 304 seq_block_append p g b1 b2 = seq_block_append p g b1' b2. 305 #p #g * #b1 #b1prf * #b1' #b1prf' #b2 #EQ destruct(EQ) % 306 qed. 307 308 lemma other_block_append_proof_irr : 309 ∀p,g,b1,b1',b2.pi1 ?? b1 = pi1 ?? b1' → 310 other_block_append p g b1 b2 = other_block_append p g b1' b2. 311 #p #g * #b1 #b1prf * #b1' #b1prf' #b2 #EQ destruct(EQ) % 312 qed. 313 314 (* 315 lemma is_seq_block_instance_append : ∀p,g,is_seq. 316 ∀B1. 317 ∀B2 : bind_seq_block p g is_seq. 318 ∀l1,l2. 319 ∀b1 : Σb.is_safe_block p g b. 320 ∀b2 : seq_block p g. 321 instantiates_to ? (seq_block p g) B1 l1 (pi1 … b1) → 322 instantiates_to ? (seq_block p g) B2 l2 b2 → 323 instantiates_to ? (seq_block p g) (B1 @ B2) (l1 @ l2) (b1 @ b2). 324 #p #g * #B1 elim B1 B1 325 [ #B1  #f1 #IH1 ] 326 #B1prf whd in B1prf; 327 #B2 * [2,4: #r1 #l1' ] #l2 #b1 #b2 [1,4: *] 328 whd in ⊢ (%→?); 88 329 [ @IH1 89  #EQ destruct(EQ) lapply b2' b2' lapply l2 l2 elim b2 90 [ #B2  #f2 #IH2] * [2,4: #r2 #l2'] #b2' [1,4: *] 91 normalize in ⊢ (%→?); [2: //] #H2 92 change with (is_block_instance ??? ('new ?) (r2 :: ?) ?) whd 93 @(IH2 … H2) 330  #EQ destruct(EQ) lapply b2 b2 lapply l2 l2 elim B2 B2 331 [ #B2  #f2 #IH2] * [2,4: #r2 #l2'] #b2 [1,4: *] 332 whd in ⊢ (%→?); 333 [ @IH2 334  #EQ' whd destruct @seq_block_append_proof_irr % 335 ] 94 336 ] 95 337 qed. 96 338 97 definition tunnel_step : ∀p,g.codeT p g → relation (code_point p) ≝ 98 λp,g,c,x,y.∃l.stmt_at … c x = Some ? (GOTO … l) ∧ point_of_label … c l = Some ? y. 99 100 notation > "x ~~> y 'in' c" with precedence 56 for @{'tunnel_step $c $x $y}. 101 notation < "hvbox(x ~~> y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_step $c $x $y}. 102 interpretation "tunnel step in code" 'tunnel_step c x y = (tunnel_step ?? c x y). 103 104 let rec tunnel_through p g (c : codeT p g) x through y on through : Prop ≝ 105 match through with 106 [ nil ⇒ x = y 107  cons hd tl ⇒ x ~~> hd in c ∧ tunnel_through … hd tl y 108 ]. 109 110 definition tunnel ≝ λp,g,c,x,y.∃through.tunnel_through p g c x through y. 111 112 notation > "x ~~>^* y 'in' c" with precedence 56 for @{'tunnel $c $x $y}. 113 notation < "hvbox(x \nbsp ~~>^* \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel $c $x $y}. 114 interpretation "tunnel in code" 'tunnel c x y = (tunnel ?? c x y). 115 116 lemma tunnel_refl : ∀p,g.∀c : codeT p g.reflexive ? (tunnel p g c). 117 #p #g #c #x %{[]} % qed. 118 119 lemma tunnel_trans : ∀p,g.∀c : codeT p g. 120 transitive ? (tunnel p g c). 121 #p#g#c #x#y#z * #l1 #H1 * #l2 #H2 %{(l1@l2)} 122 lapply H1 H1 lapply x x elim l1 l1 123 [ #x #H1 >H1 @H2 124  #hd #tl #IH #x * #H11 #H12 125 %{H11} @IH @H12 126 ] qed. 127 128 definition tunnel_plus ≝ λp,g.λc : codeT p g.λx,y. 129 ∃mid.x ~~> mid in c ∧ mid ~~>^* y in c. 130 131 notation > "x ~~>^+ y 'in' c" with precedence 56 for @{'tunnel_plus $c $x $y}. 132 notation < "hvbox(x \nbsp ~~>^+ \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_plus $c $x $y}. 133 interpretation "tunnel in code" 'tunnel_plus c x y = (tunnel_plus ?? c x y). 134 135 lemma tunnel_plus_to_star : ∀p,g.∀c : codeT p g.∀x,y.x ~~>^+ y in c → x ~~>^* y in c. 136 #p #g #c #x #y * #mid * #H1 * #through #H2 %{(mid :: through)} 137 %{H1 H2} qed. 138 139 lemma tunnel_plus_trans : ∀p,g.∀c : codeT p g.transitive ? (tunnel_plus p g c). 140 #p #g #c #x #y #z * #mid * #H1 #H2 141 #H3 %{mid} %{H1} @(tunnel_trans … H2) /2 by tunnel_plus_to_star/ 142 qed. 143 144 lemma tunnel_tunnel_plus : ∀p,g.∀c : codeT p g.∀x,y,z. 145 x ~~>^* y in c → y ~~>^+ z in c → x ~~>^+ z in c. 146 #p #g #c #x #y #z * #through 147 lapply x x elim through 148 [ #x #H1 >H1 // 149  #hd #tl #IH #x * #H1 #H2 #H3 150 %{hd} %{H1} @(tunnel_trans ???? y) 151 [ %{tl} assumption  /2 by tunnel_plus_to_star/] 339 lemma is_other_block_instance_append : ∀p,g. 340 ∀B1 : Σb.bind_pred ? (λx.block_classifier p g x = cl_other) b. 341 ∀B2 : bind_other_block p g. 342 ∀l1,l2. 343 ∀b1 : Σb.block_classifier p g b = cl_other. 344 ∀b2 : other_block p g. 345 instantiates_to ? (other_block p g) B1 l1 (pi1 … b1) → 346 instantiates_to ? (other_block p g) B2 l2 b2 → 347 instantiates_to ? (other_block p g) (B1 @@ B2) (l1 @ l2) (b1 @@ b2). 348 #p #g * #B1 elim B1 B1 349 [ #B1  #f1 #IH1 ] 350 #B1prf whd in B1prf; 351 #B2 * [2,4: #r1 #l1' ] #l2 #b1 #b2 [1,4: *] 352 whd in ⊢ (%→?); 353 [ @IH1 354  #EQ destruct(EQ) lapply b2 b2 lapply l2 l2 elim B2 B2 355 [ #B2  #f2 #IH2] * [2,4: #r2 #l2'] #b2 [1,4: *] 356 whd in ⊢ (%→?); 357 [ @IH2 358  #EQ' whd destruct @other_block_append_proof_irr % 359 ] 152 360 ] 153 361 qed. 154 362 155 lemma tunnel_plus_tunnel : ∀p,g.∀c : codeT p g.∀x,y,z. 156 x ~~>^+ y in c → y ~~>^* z in c → x ~~>^+ z in c. 157 #p #g #c #x #y #z * #mid * #H1 #H2 #H3 %{mid} %{H1} 158 @(tunnel_trans … H2 H3) 159 qed. 160 161 let rec seq_list_in_code (p : params) g (c : codeT p g) 162 src l dst on l : Prop ≝ 163 match l with 363 lemma other_fin_step_has_one_label : 364 ∀p,g.∀s:(Σs.fin_step_classifier p g s = cl_other). 365 match fin_step_labels ?? s with 366 [ nil ⇒ False 367  cons _ tl ⇒ 368 match tl with 369 [ nil ⇒ True 370  _ ⇒ False 371 ] 372 ]. 373 #p #g ** [#lbl  #ext] 374 normalize 375 [3: cases (ext_fin_step_flows p ext) 376 [* [2: #lbl' * [2: #lbl'' #tl']]] normalize nodelta ] 377 #EQ destruct % 378 qed. 379 380 definition label_of_other_fin_step : ∀p,g. 381 (Σs.fin_step_classifier p g s = cl_other) → label ≝ 382 λp,g,s. 383 match fin_step_labels p ? s return λx.match x with [ nil ⇒ ?  cons _ tl ⇒ ?] → ? with 384 [ nil ⇒ Ⓧ 385  cons lbl tl ⇒ λ_.lbl 386 ] (other_fin_step_has_one_label p g s). 387 388 (* 389 definition point_seq_transition : ∀p,g.codeT p g → 390 code_point p → code_point p → Prop ≝ 391 λp,g,c,src,dst. 392 match stmt_at … c src with 393 [ Some stmt ⇒ match stmt with 394 [ sequential sq nxt ⇒ 395 point_of_succ … src nxt = dst 396  final fn ⇒ 397 match fin_step_labels … fn with 398 [ nil ⇒ False 399  cons lbl tl ⇒ 400 match tl with 401 [ nil ⇒ point_of_label … c lbl = Some ? dst 402  _ ⇒ False 403 ] 404 ] 405 ] 406  None ⇒ False 407 ]. 408 409 lemma point_seq_transition_label_of_other_fin_step : 410 ∀p,c,src.∀s : (Σs.fin_step_classifier p s = cl_other).∀dst. 411 stmt_at ?? c src = Some ? s → 412 point_seq_transition p c src dst → 413 point_of_label … c (label_of_other_fin_step p s) = Some ? dst. 414 #p #c #src ** [#lbl  #ext] #EQ1 415 #dst #EQ2 416 whd in match point_seq_transition; normalize nodelta 417 >EQ2 normalize nodelta whd in ⊢ (?→??(????%)?); 418 [#H @H  * ] 419 lapply (other_fin_step_has_one_label ? «ext,?») 420 cases (fin_step_labels p ? ext) normalize nodelta [*] 421 #hd * normalize nodelta [2: #_ #_ *] * 422 #H @H 423 qed. 424 425 lemma point_seq_transition_succ : 426 ∀p,c,src.∀s,nxt.∀dst. 427 stmt_at ?? c src = Some ? (sequential ?? s nxt) → 428 point_seq_transition p c src dst → 429 point_of_succ … src nxt = dst. 430 #p #c #src #s #nxt #dst #EQ 431 whd in match point_seq_transition; normalize nodelta 432 >EQ normalize nodelta #H @H 433 qed. 434 *) 435 436 definition if_other : ∀p,g.∀A : Type[2].seq_or_fin_step p g → A → A → A ≝ 437 λp,g,A,c.match seq_or_fin_step_classifier p g c with 438 [ cl_other ⇒ λx,y.x 439  _ ⇒ λx,y.y 440 ]. 441 442 definition other_step_in_code ≝ 443 λp,g. 444 λc : codeT p g. 445 λsrc : code_point p. 446 λs : seq_or_fin_step p g. 447 match s return λx.if_other p g ? x (code_point p) unit → Prop with 448 [ inl s'' ⇒ λdst.∃n.stmt_at … c src = Some ? (sequential … s'' n) ∧ ? 449  inr s'' ⇒ λdst.stmt_at … c src = Some ? (final … s'') ∧ ? 450 ]. 451 [ whd in dst; cases (seq_or_fin_step_classifier ???) in dst; 452 normalize nodelta [1,2,3: #_ @True *: #dst 453 @(point_of_succ … src n = dst)] 454  whd in dst; 455 lapply dst dst 456 lapply (refl … (seq_or_fin_step_classifier ?? (inr … s''))) 457 cases (seq_or_fin_step_classifier ?? (inr … s'')) in ⊢ (???%→%); 458 normalize nodelta 459 [1,2,3: #_ #_ @True 460 *: #EQ #dst 461 @(point_of_label … c (label_of_other_fin_step p g «s'', EQ») = Some ? dst) 462 ] 463 ] 464 qed. 465 466 definition if_other_sig : 467 ∀p,g.∀B,C : Type[0].∀s : Σs.seq_or_fin_step_classifier p g s = cl_other. 468 if_other p g ? s B C → B ≝ 469 λp,g,B,C.?. 470 ** #s whd in match (if_other ??????); 471 cases (seq_or_fin_step_classifier ???) normalize nodelta #EQ destruct(EQ) 472 #x @x 473 qed. 474 475 definition if_other_block_sig : 476 ∀p,g.∀B,C : Type[0].∀b : Σb.block_classifier p g b = cl_other. 477 if_other p g ? (\snd b) B C → B ≝ 478 λp,g,B,C.?. 479 ** #l #s 480 #prf #x @(if_other_sig ???? «s, prf» x) 481 qed. 482 483 coercion other_sig_to_if nocomposites: 484 ∀p,g.∀B,C : Type[0].∀s : Σs.seq_or_fin_step_classifier p g s = cl_other. 485 ∀x : if_other p g ? s B C.B ≝ if_other_sig 486 on _x : if_other ?? Type[0] ??? to ?. 487 488 coercion other_block_sig_to_if nocomposites: 489 ∀p,g.∀B,C : Type[0].∀s : Σs.block_classifier p g s = cl_other. 490 ∀x : if_other p g ? (\snd s) B C.B ≝ if_other_block_sig 491 on _x : if_other ?? Type[0] (\snd ?) ?? to ?. 492 493 let rec other_list_in_code p g (c : codeT p g) 494 src 495 (b : list (Σs.seq_or_fin_step_classifier p g s = cl_other)) 496 dst on b : Prop ≝ 497 match b with 164 498 [ nil ⇒ src = dst 165  cons hd tl ⇒ 166 ∃n.stmt_at … c src = Some ? (sequential … hd n) ∧ 167 seq_list_in_code p g c (point_of_succ … src n) tl dst 168 ]. 169 170 (* 171 definition seq_block_cont_to_list : ∀p,g.block_cont p g SEQ → list (joint_step p g) ≝ 172 λp,g,b.\fst b @ [\snd b]. 173 174 coercion list_from_seq_block_cont : ∀p,g.∀b:block_cont p g SEQ.list (joint_step p g) ≝ 175 seq_block_cont_to_list on _b : block_cont ?? SEQ to list (joint_step ??). 176 *) 177 178 definition unit_deqset: DeqSet ≝ mk_DeqSet unit (λ_.λ_.true) ?. 179 * * /2/ 180 qed. 181 182 definition block_cont_in_code : ∀p,g.codeT p g → ∀ty. 183 code_point p → block_cont p g ty → stmt_type_if ? ty (code_point p) unit_deqset → Prop ≝ 184 λp,g.λc : codeT p g.λty,src,b,dst. 185 ∃mid.seq_list_in_code p g c src (\fst b) mid ∧ 186 match ty 187 return λx.stmt_type_if ? x ??? → 188 stmt_type_if ? x ? unit_deqset → Prop 189 with 190 [ SEQ ⇒ λs,dst. 191 ∃n.stmt_at … c mid = Some ? (sequential … s n) ∧ 192 point_of_succ … mid n = dst 193  FIN ⇒ λs.λ_.stmt_at … c mid = Some ? (final … s) 194 ] (\snd b) dst. 195 499  cons hd tl ⇒ ∃mid. 500 other_step_in_code p g c src hd mid ∧ other_list_in_code p g c mid tl dst 501 ]. 196 502 197 503 notation > "x ~❨ B ❩~> y 'in' c" with precedence 56 for … … 201 507 @{'block_in_code $c $x $B $y}. 202 508 203 interpretation "block cont in code" 'block_in_code c x B y = 204 (block_cont_in_code ?? c ? x B y). 205 206 lemma seq_list_in_code_append : ∀p,g.∀c : codeT p g.∀x,l1,y,l2,z. 207 seq_list_in_code p g c x l1 y → 208 seq_list_in_code p g c y l2 z → 209 seq_list_in_code p g c x (l1@l2) z. 210 #p#g#c#x#l1 lapply x x 211 elim l1 [2: #hd #tl #IH] #x #y #l2 #z normalize in ⊢ (%→?); 212 [ * #n * #EQ1 #H #G %{n} %{EQ1} @(IH … H G) 213  #EQ destruct(EQ) // 214 ] 215 qed. 216 217 lemma block_cont_in_code_append : ∀p,g.∀c : codeT p g.∀ty,x. 218 ∀B1 : block_cont p g SEQ.∀y.∀B2 : block_cont p g ty.∀z. 219 x ~❨B1❩~> y in c → y ~❨B2❩~> z in c → x ~❨B1@B2❩~> z in c. 220 #p#g#c #ty #x * whd in match stmt_type_if in ⊢ (?→%→%→?); normalize nodelta 221 #l1 #s1 #y * #l2 #s2 #z * normalize nodelta 222 #mid1 * #H1 * #n * #EQ1 #EQ2 * #mid2 * #H2 #H3 223 %{mid2} % 224 [ whd in match (〈?,?〉@?); 225 @(seq_list_in_code_append … H1) 226 %{n} %{EQ1} >EQ2 assumption 227  assumption 228 ] 229 qed. 230 509 interpretation "list in code" 'block_in_code c x B y = 510 (other_list_in_code ?? c x B y). 511 512 definition other_block_in_code : ∀p,g.codeT p g → 513 code_point p → ∀b : other_block p g. 514 if_other … (\snd b) (code_point p) unit → Prop ≝ 515 λp,g,c,src,b,dst. 516 ∃mid.src ~❨\fst b❩~> mid in c ∧ 517 other_step_in_code p g c mid (\snd b) dst. 518 519 interpretation "block in code" 'block_in_code c x B y = 520 (other_block_in_code ?? c x B y). 521 522 lemma other_list_in_code_append : ∀p,g.∀c : codeT p g. 523 ∀x.∀b1 : list ?. 524 ∀y.∀b2 : list ?.∀z. 525 x ~❨b1❩~> y in c→ y ~❨b2❩~> z in c → x ~❨b1@b2❩~> z in c. 526 #p#g#c#x#b1 lapply x x 527 elim b1 [2: ** #hd #hd_prf #tl #IH] #x #y #b2 #z 528 [3: #EQ normalize in EQ; destruct #H @H] 529 * #mid * normalize nodelta [ *#n ] #H1 #H2 #H3 530 whd normalize nodelta %{mid} 531 %{(IH … H2 H3)} 532 [ %{n} ] @H1 533 qed. 534 535 lemma other_block_in_code_append : ∀p,g.∀c : codeT p g.∀x. 536 ∀B1 : Σb.block_classifier p g b = cl_other. 537 ∀y. 538 ∀B2 : other_block p g. 539 ∀z. 540 x ~❨B1❩~> y in c → y ~❨B2❩~> z in c → 541 x ~❨B1@@B2❩~> z in c. 542 #p#g#c #x ** #hd1 *#tl1 #tl1prf 543 #y * #hd2 #tl2 #z 544 * #mid1 * #H1 #H2 545 * #mid2 * #G1 #G2 546 %{mid2} %{G2} 547 whd in match (\fst ?); 548 @(other_list_in_code_append … H1) 549 %{y} %{H2 G1} 550 qed. 551 552 (* 231 553 definition instr_block_in_function : 232 ∀p,g.∀fn : joint_internal_function g p.∀ty. 233 instr_block p g ty → 554 ∀p : evaluation_params.∀fn : joint_internal_function (globals p) p. 234 555 code_point p → 556 ∀b : bind_other_block p. 235 557 ? → Prop ≝ 236 λp, g,fn,ty,B,src,dst.558 λp,fn,src,B,dst. 237 559 ∃vars,B'. 238 560 All ? (In ? (joint_if_locals … fn)) vars ∧ 239 i s_block_instance… B vars B' ∧561 instantiates_to … B vars B' ∧ 240 562 src ~❨B'❩~> dst in joint_if_code … fn. 241 563 242 interpretation " instrblock in function" 'block_in_code fn x B y =243 (instr_block_in_function ? ? fn ? B xy).564 interpretation "bind block in function" 'block_in_code fn x B y = 565 (instr_block_in_function ? fn x B y). 244 566 245 567 lemma instr_block_in_function_trans : 246 ∀p,g.∀fn : joint_internal_function g p.∀ty,src. 247 ∀B1 : instr_block p g SEQ. 248 ∀mid.∀B2 : instr_block p g ty.∀dst. 249 src ~❨B1❩~> mid in fn → 568 ∀p,fn,src. 569 ∀B1 : ΣB.bind_pred ? (λb.block_classifier p b = cl_other) B. 570 ∀mid. 571 ∀B2 : bind_other_block p. 572 ∀dst. 573 src ~❨B1❩~> Some ? mid in fn → 250 574 mid ~❨B2❩~> dst in fn → 251 src ~❨B1@ B2❩~> dst in fn.252 #p# g#fn#ty#src#B1#mid#B2#dst575 src ~❨B1@@B2❩~> dst in fn. 576 #p#fn#src*#B1#B1prf#mid#B2#dst 253 577 * #vars1 * #b1 ** #vars1_ok #b1B1 #b1_in 254 578 * #vars2 * #b2 ** #vars2_ok #b2B2 #b2_in 255 %{(vars1@vars2)} %{(b1 @ b2)} 256 /4 by All_append, conj, is_block_instance_append, block_cont_in_code_append/ 257 qed. 579 %{(vars1@vars2)} %{(«b1,instantiates_to_bind_pred … b1B1 B1prf» @@ b2)} 580 /4 by All_append, conj, is_other_block_instance_append, other_block_in_code_append/ 581 qed. 582 *) 583 *) 584 *)
Note: See TracChangeset
for help on using the changeset viewer.