Changeset 2708
 Timestamp:
 Feb 22, 2013, 7:11:30 PM (7 years ago)
 Location:
 src
 Files:

 6 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASM.ma
r2705 r2708 984 984 985 985 definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction. 986 definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)).986 definition preamble ≝ list (Identifier × Word). 987 987 definition assembly_program ≝ list instruction. 988 988 definition pseudo_assembly_program ≝ preamble × (list labelled_instruction). 
src/LIN/LINToASM.ma
r2490 r2708 3 3 include "LIN/LIN.ma". 4 4 include "ASM/ASM.ma". 5 include "utilities/state.ma". 6 7 (* utilities to provide Identifier's and addresses *) 8 record ASM_universe (globals : list ident) : Type[0] := 9 { id_univ : universe ASMTag 10 ; current_funct : ident 11 ; ident_map : identifier_map SymbolTag Identifier 12 ; label_map : identifier_map SymbolTag (identifier_map LabelTag Identifier) 13 ; address_map : identifier_map SymbolTag Word 14 ; globals_are_in : ∀i : ident.i ∈ globals → i ∈ address_map 15 }. 16 17 definition new_ASM_universe : 18 ∀p : joint_program LIN.ASM_universe (prog_var_names … p) ≝ 19 λp. 20 let globals_addr_internal ≝ 21 λres_offset : identifier_map SymbolTag Word × Z. 22 λx_size: ident × region × nat. 23 let 〈res, offset〉 ≝ res_offset in 24 let 〈x, region, size〉 ≝ x_size in 25 〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat size〉 in 26 let addresses ≝ foldl … globals_addr_internal 〈empty_map …, OZ〉 (prog_vars … p) in 27 mk_ASM_universe ? (mk_universe … one) 28 (an_identifier … one (* dummy *)) 29 (empty_map …) (empty_map …) 30 (\fst addresses) ?. 31 @hide_prf 32 normalize nodelta 33 cases p p #vars #functs #main 34 #i #H 35 letin init_val ≝ (〈empty_map ? Word, OZ〉) 36 cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars)) 37 [ %2{H} ] H 38 lapply i i lapply init_val init_val elim vars vars 39 [2: ** #id #r #v #tl #IH ] #init_val #i 40 [2: * [2: * ] #H @H ] 41 * [2: #H cases (orb_Prop_true … H) H ] #H 42 @IH 43 [ %1 cases init_val normalize nodelta #init_map #off 44 >(proj1 ?? (eqb_true ???) H) @mem_set_add_id 45  %2{H} 46  %1 cases init_val in H; normalize nodelta #init_map #off #H 47 >mem_set_add @orb_Prop_r @H 48 ] 49 qed. 50 51 definition Identifier_of_label : 52 ∀globals.label → state_monad (ASM_universe globals) Identifier ≝ 53 λg,l,u. 54 let current ≝ current_funct … u in 55 let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in 56 let 〈id, univ, lmap〉 ≝ 57 match lookup … lmap l with 58 [ Some id ⇒ 〈id, id_univ … u, lmap〉 59  None ⇒ 60 let 〈id, univ〉 ≝ fresh … (id_univ … u) in 61 〈id, univ, add … lmap l id〉 62 ] in 63 〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap) 64 (address_map … u) (globals_are_in … u), id〉. 65 66 definition Identifier_of_ident : 67 ∀globals.ident → state_monad (ASM_universe globals) Identifier ≝ 68 λg,i,u. 69 let imap ≝ ident_map … u in 70 let 〈id, univ, imap〉 ≝ 71 match lookup … imap i with 72 [ Some id ⇒ 〈id, id_univ … u, imap〉 73  None ⇒ 74 let 〈id, univ〉 ≝ fresh … (id_univ … u) in 75 〈id, univ, add … imap i id〉 76 ] in 77 〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u) 78 (address_map … u) (globals_are_in … u), id〉. 79 80 definition start_funct_translation : 81 ∀globals.(ident × (joint_function LIN globals)) → 82 state_monad (ASM_universe globals) unit ≝ 83 λg,id_f,u. 84 〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u) 85 (address_map … u) (globals_are_in … u), it〉. 86 87 definition address_of_ident : 88 ∀globals,i.i ∈ globals → state_monad (ASM_universe globals) [[ data16 ]] ≝ 89 λglobals,i,prf,u. 90 〈u, DATA16 (lookup_safe … (globals_are_in … u … prf))〉. @I qed. 91 92 definition ASM_fresh : 93 ∀globals.state_monad (ASM_universe globals) Identifier ≝ 94 λg,u.let 〈id, univ〉 ≝ fresh … (id_univ … u) in 95 〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u) 96 (address_map … u) (globals_are_in … u), id〉. 5 97 6 98 definition register_address: Register → [[ acc_a; direct; registr ]] ≝ … … 22 114 ]. @I qed. 23 115 24 let rec association A B (eq_A : A → A → bool) (a : A) (l: list (A × B))25 on l: member A eq_A a (map ? ? (fst ? ?) l) → B ≝26 match l return λl. member A eq_A a (map ? ? (fst ? ?) l) → B with27 [ nil ⇒ Ⓧ28  cons hd tl ⇒29 λprf.30 If eq_A a (\fst hd) then \snd hd else with eq_prf do31 association … eq_A a tl ?32 ].33 elim (orb_Prop_true … prf)34 [ > eq_prf *35  # H36 assumption37 ]38 qed.39 40 definition association_ident ≝ association ident nat (eq_identifier ?).41 definition association_block ≝ association block Word eq_block.42 43 116 definition vector_cast : 44 117 ∀A,n,m.A → Vector A n → Vector A m ≝ … … 68 141 definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g). 69 142 70 definition statement_labels ≝71 λg: list ident.72 λs: lin_statement g.73 let 〈label, instr〉 ≝ s in74 let generated ≝75 match instr with76 [ sequential instr' _ ⇒77 match instr' with78 [ step_seq instr'' ⇒79 match instr'' with80 [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }81  _ ⇒ ∅82 ]83  COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }84 ]85  final instr' ⇒86 match instr' with87 [ GOTO lbl ⇒ {(toASM_ident ? lbl)}88  _ ⇒ ∅89 ]90 ]91 in92 match label with93 [ None ⇒ generated94  Some lbl ⇒ add_set ? generated (toASM_ident ? lbl)95 ].96 97 definition function_labels_internal ≝98 λglobals: list ident.99 λlabels: identifier_set ?.100 λstatement: lin_statement globals.101 labels ∪ (statement_labels globals statement).102 103 (* dpm: A = Identifier *)104 definition function_labels: ∀A. ∀globals. ∀f. identifier_set ? ≝105 λA: Type[0].106 λglobals: list ident.107 λf: A × (joint_function LIN globals).108 let 〈ignore, fun_def〉 ≝ f in109 match fun_def return λ_. identifier_set ? with110 [ Internal stmts ⇒111 foldl ? ? (function_labels_internal globals) ∅ (joint_if_code ?? stmts)112  External _ ⇒ ∅113 ].114 115 definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. identifier_set ? ≝116 λA: Type[0].117 λglobals: list ident.118 λlabels: identifier_set ?.119 λfunct: A × (joint_function LIN globals).120 labels ∪ (function_labels ? globals funct).121 122 (* CSC: here we are silently throwing away the region information *)123 definition program_labels ≝124 λprogram: lin_program.125 foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))126 ∅ (prog_funct … program).127 128 143 definition data_of_int ≝ λbv. DATA bv. 129 144 definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv). … … 133 148 definition asm_other_bit ≝ BIT_ADDR (zero_byte). 134 149 135 definition translate_statements ≝136 λglobals: list (ident × nat).137 λglobals_old: list ident.138 λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals).139 λ statement: joint_statement LIN globals_old.140 match statement 150 definition translate_statements : 151 ∀globals. 152 joint_statement LIN globals → 153 state_monad (ASM_universe globals) pseudo_instruction ≝ 154 λglobals,statement. 155 match statement with 141 156 [ final instr ⇒ 142 157 match instr with 143 [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl) 144  RETURN ⇒ Instruction (RET ?) 158 [ GOTO lbl ⇒ 159 ! lbl' ← Identifier_of_label … lbl ; 160 return Jmp (toASM_ident ? lbl) 161  RETURN ⇒ return Instruction (RET ?) 145 162  TAILCALL abs _ _ ⇒ Ⓧabs 146 163 ] … … 152 169 match ext with 153 170 [ SAVE_CARRY ⇒ 154 Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))171 return Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉)) 155 172  RESTORE_CARRY ⇒ 156 Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉))) 173 return Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉))) 174  LOW_ADDRESS reg lbl ⇒ 175 ! lbl' ← Identifier_of_label … lbl ; 176 return MovSuccessor (register_address reg) LOW lbl' 177  HIGH_ADDRESS reg lbl ⇒ 178 ! lbl' ← Identifier_of_label … lbl ; 179 return MovSuccessor (register_address reg) HIGH lbl' 157 180 ] 158  COMMENT comment ⇒ Comment comment 159  COST_LABEL lbl ⇒ Cost lbl 160  POP _ ⇒ Instruction (POP ? accumulator_address) 161  PUSH _ ⇒ Instruction (PUSH ? accumulator_address) 162  CLEAR_CARRY ⇒ Instruction (CLR ? CARRY) 163  CALL f _ _ ⇒ 164 match f with 165 [ inl f_id ⇒ Call (toASM_ident ? f_id) 166  inr _ ⇒ (* TODO call from ptr in DPTR *) 167 match not_implemented in False with [ ] 168 ] 181  COMMENT comment ⇒ return Comment comment 182  POP _ ⇒ return Instruction (POP ? accumulator_address) 183  PUSH _ ⇒ return Instruction (PUSH ? accumulator_address) 184  CLEAR_CARRY ⇒ return Instruction (CLR ? CARRY) 169 185  OPACCS accs _ _ _ _ ⇒ 170 match accs with186 return match accs with 171 187 [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) 172 188  DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B) 173 189 ] 174 190  OP1 op1 _ _ ⇒ 175 match op1 with191 return match op1 with 176 192 [ Cmpl ⇒ Instruction (CPL ? ACC_A) 177 193  Inc ⇒ Instruction (INC ? ACC_A) … … 179 195 ] 180 196  OP2 op2 _ _ reg ⇒ 181 match arg_address … reg197 return match arg_address … reg 182 198 return λx.is_in … [[ acc_a; 183 199 direct; … … 221 237  _ ⇒ Ⓧ 222 238 ] (subaddressing_modein …) 223  LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))224  STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))239  LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) 240  STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) 225 241  ADDRESS addr proof _ _ ⇒ 226 let look ≝ association_ident addr globals (prf ? proof) in227 Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))242 ! addr' ← address_of_ident … proof ; 243 return Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, addr'〉))))) 228 244  SET_CARRY ⇒ 229 Instruction (SETB ? CARRY)245 return Instruction (SETB ? CARRY) 230 246  MOVE regs ⇒ 231 match regs with247 return match regs with 232 248 [ to_acc _ reg ⇒ 233 249 match register_address reg return λx.is_in … [[ acc_a; … … 276 292 ] 277 293 ] 294  CALL f _ _ ⇒ 295 match f with 296 [ inl id ⇒ 297 ! id' ← Identifier_of_ident … id ; 298 return Call (toASM_ident ? id') 299  inr _ ⇒ 300 return Instruction (JMP … INDIRECT_DPTR) 301 ] 302  COST_LABEL lbl ⇒ return Cost lbl 278 303  COND _ lbl ⇒ 279 (* dpm: this should be handled in translate_code! *)280 Instruction (JNZ ? (toASM_ident ? lbl))304 ! l ← Identifier_of_label … lbl; 305 return Instruction (JNZ ? l) 281 306 ] 307  FCOND _ _ lbl_true lbl_false ⇒ 308 ! l1 ← Identifier_of_label … lbl_true; 309 ! l2 ← Identifier_of_label … lbl_false; 310 return Jnz ACC_A l1 l2 282 311 ]. 283 312 try @I 284 313 qed. 285 314 286 (*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)287 definition ident_of_label: label → Identifier ≝288 toASM_ident LabelTag.289 315 290 316 definition build_translated_statement ≝ 291 317 λglobals. 292 λglobals_old. 293 λprf. 294 λstatement: lin_statement globals_old. 295 〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉. 318 λstatement: lin_statement globals. 319 ! stmt ← translate_statements globals (\snd statement) ; 320 match \fst statement with 321 [ Some lbl ⇒ 322 ! lbl' ← Identifier_of_label globals lbl ; 323 return 〈Some ? lbl', stmt〉 324  None ⇒ 325 return 〈None ?, stmt〉 326 ]. 296 327 297 328 definition translate_code ≝ 298 λglobals: list (ident × nat). 299 λglobals_old: list ident. 300 λprf. 301 λcode: list (lin_statement globals_old). 302 map ? ? (build_translated_statement globals globals_old prf) code. 329 λglobals. 330 λcode: list (lin_statement globals). 331 m_list_map … (build_translated_statement globals) code. 303 332 304 333 definition translate_fun_def ≝ 305 λglobals: list (ident × nat). 306 λglobals_old. 307 λprf. 308 λid_def : ident × (joint_function LIN globals_old). 309 let 〈id, def〉 ≝ id_def in 310 match def with 334 λglobals. 335 λid_def : ident × (joint_function LIN globals). 336 !_ start_funct_translation … id_def ; 337 (* ^ modify current function id ^ *) 338 match \snd id_def with 311 339 [ Internal int ⇒ 312 let code ≝ joint_if_code LIN globals_old int in 313 match translate_code globals globals_old prf code with 314 [ nil ⇒ ⊥ 340 let code ≝ joint_if_code … int in 341 ! id ← Identifier_of_ident … (\fst id_def) ; 342 ! code' ← translate_code … code ; 343 match code' with 344 [ nil ⇒ return [〈Some ? id, Instruction (RET ?)〉] (* impossible, but whatever *) 315 345  cons hd tl ⇒ 316 let rest ≝ 〈Some ? (toASM_ident SymbolTag id), \snd hd〉 :: tl in 317 map ? ? ( 318 λr. 319 match fst ? ? r with 320 [ Some id' ⇒ 〈Some ? (toASM_ident ? id'), snd ? ? r〉 321  None ⇒ 〈None ?, \snd r〉 322 ]) rest 346 match \fst hd with 347 [ None ⇒ return (〈Some ? id, \snd hd〉 :: tl) 348  _ ⇒ return (〈Some ? id, Instruction (NOP ?)〉 :: hd :: tl) (* should never happen *) 349 ] 323 350 ] 324  External _ ⇒ [ ]351  External _ ⇒ return [ ] 325 352 ]. 326 cases daemon (*CSC: XXX will be fixed by an invariant later *) 327 qed. 328 329 include "common/Identifiers.ma". 330 331 let rec flatten_fun_defs 332 (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat) 333 (the_list: list ((identifier SymbolTag) × (joint_function LIN globals_old))) 334 on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝ 335 match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with 336 [ cons hd tl ⇒ 337 let fun_def ≝ \snd hd in 338 let fun_id ≝ \fst hd in 339 let translated ≝ translate_fun_def globals globals_old prf hd in 340 let size_translated ≝  translated  in 341 let 〈tail_trans, tail_map〉 ≝ flatten_fun_defs globals globals_old prf (initial_pc + size_translated) tl in 342 let new_hd ≝ translated @ tail_trans in 343 let new_map ≝ add ? ? tail_map fun_id initial_pc in 344 〈new_hd, new_map〉 345  nil ⇒ 〈[ ], empty_map …〉 346 ]. 347 348 definition translate_functs ≝ 349 λglobals. 350 λglobals_old. 351 λprf. 352 λexit_label. 353 λmain. 354 λfuncts : list (ident × (joint_function LIN ?)). 355 let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in 356 let 〈flattened, map〉 ≝ flatten_fun_defs globals globals_old prf 6 (* Size of preamble above *) functs in 357 〈preamble @ flattened, map〉. 358 359 (*CSC: region silently thrown away here *) 360 definition globals_addr ≝ 361 λl. 362 let globals_addr_internal ≝ 363 λres_offset. 364 λx_size: ident × region × nat. 365 let 〈res, offset〉 ≝ res_offset in 366 let 〈x, region, size〉 ≝ x_size in 367 〈〈x, offset〉 :: res, offset + size〉 368 in 369 \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l). 370 371 (* dpm: plays the role of the string "_exit" in the O'caml source *) 372 axiom identifier_prefix: Identifier. 373 (*CSC: XXXXXXX wrong anyway since labels from different functions can now 374 clash with each other and with names of functions *) 375 axiom fresh_prefix: identifier_set ASMTag → Identifier → Identifier. 376 377 (* dpm: fresh prefix stuff needs unifying with brian *) 353 378 354 definition lin_to_asm : lin_program → pseudo_assembly_program ≝ 379 355 λp. 380 let prog_lbls ≝ program_labels … p in 381 let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in 382 let global_addr ≝ globals_addr (prog_vars … p) in 383 let global_addr' ≝ map … (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x, bitvector_of_nat 16 off〉) global_addr in 384 let 〈translated, funct_map〉 ≝ 385 translate_functs global_addr (prog_var_names … p) ? exit_label 386 (toASM_ident … (prog_main … p)) (prog_funct ?? p) in 387 〈〈funct_map, global_addr'〉, translated〉. 388 #i normalize nodelta global_addr' global_addr exit_label prog_lbls; 389 normalize in match prog_var_names; normalize nodelta 390 elim (prog_vars … p) // 391 #hd #tl #IH whd in ⊢ (% → %); 392 whd in match globals_addr; normalize nodelta 393 whd in match (foldl ???? (hd::tl)); normalize nodelta 394 cases hd * #id #reg #size normalize nodelta 395 cases daemon (*CSC: provable using a pair of lemmas over foldl *) 396 qed. 356 state_run ?? (new_ASM_universe p) 357 (let add_translation ≝ 358 λacc,id_def. 359 ! code ← translate_fun_def … id_def ; 360 ! acc ← acc ; 361 return (code @ acc) in 362 ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ; 363 ! exit_label ← ASM_fresh … ; 364 ! main ← Identifier_of_ident … (prog_main … p) ; 365 let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in 366 (* atm no data identifier is used in the code, so preamble must be empty *) 367 return 〈[ ], code〉). 
src/joint/TranslateUtils.ma
r2688 r2708 27 27 let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in 28 28 〈set_runiverse … def runiverse, r〉. 29 30 definition state_update : ∀S.(S → S) → state_monad S unit ≝31 λS,f,s.〈f s, it〉.32 29 33 30 (* insert into a graph a list of instructions *) 
src/joint/linearise.ma
r2702 r2708 256 256 cases s in H3; [3: *] 257 257 [ * ] normalize nodelta 258 [2,4: [#f #args #dest #s'] #nxt * #EQnth_opt #H %{EQnth_opt} 259 inversion (lookup … visited nxt) in H; [2: #n'] #EQlookup 258 [1,2,4: [ #c  #f #args #dest #s'] #nxt * #EQnth_opt #H %{EQnth_opt} 259 inversion (lookup … visited nxt) in H; [2,4,6: #n'] normalize nodelta 260 #EQlookup 260 261 normalize nodelta * 261 [ #EQn' %1 >EQn' %262  #H %2{H}263  #H' lapply (All_nth … H … H')262 [1,3,5: #EQn' %1 >EQn' % 263 2,4,6: #H %2{H} 264 *: #H' lapply (All_nth … H … H') 264 265 whd in ⊢ (?%→?); >EQlookup * 265 266 ] 266  3:#a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1}267  #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1} 267 268 inversion (lookup … visited lfalse) in H2; 268 269 [ #ABS * #H' lapply (All_nth … H … H') … … 270 271  #n' #_ normalize nodelta #EQ >EQ % 271 272 ] 272  #s #H (*CSC XXXXXXXXXXXXXXXXXXXX @H *)273  #s #H @H 273 274 ] 274 275 ] … … 326 327 12: (* add_req_gen utility *) 327 328 #P whd in match add_req_gen; 328 cases statement [ * [#f #args #dest #a #ltrue  #s ] #nxt  #s  * ] 329 [2,4: normalize nodelta #l #H1 #H2 lapply (H2 … (refl …)) H2 330 cases (l ∈ add …) in H1; normalize nodelta #H1 #H2 try @H2 try @H1 try % 331 // 332 3,5: normalize nodelta [#_] #H #_ @H % 333  normalize nodelta in dest nxt ⊢ %; inversion (args ∈ add …) #EQ 334 normalize nodelta [ @nxt  @dest ] >EQ try % ] 335 14: skip 336 ] cases daemon (*CSC: XXXXXXXXX 329 cases statement [ * [ #cost  #f #args #dest #a #ltrue  #s ] #nxt  #s  * ] 330 normalize nodelta 331 [3,5: #H #_ @(H I) ] 332 inversion (nxt ∈ visited') #EQ normalize nodelta 333 #H1 #H2 [1,3,5: @(H2 … (refl …)) >EQ % *: @H1 % * ] 337 334 3: elim H #pre ** #H1 #H2 #_ 338 335 #i >mem_set_union … … 341 338 #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption 342 339  >mem_set_union 343 #H elim (orb_Prop_true … H) H (*CSC XXXXXXXXXX340 #H elim (orb_Prop_true … H) H 344 341 [ #i_expl %1 @Exists_append_l 345 342 lapply i_expl whd in match translated_statement; 346 cases statement [ * [ #f #args #dest  #a #ltrue  #s ] #nxt  #s  *] normalize nodelta #H 343 cases statement [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s  *] 344 normalize nodelta #H 347 345 lapply (mem_list_as_set … H) H #H 348 [1, 3,4: @Exists_append_r assumption ]346 [1,2,4,5: @Exists_append_r assumption ] 349 347 cases (nxt ∈ visited') in H; normalize nodelta * [2,4: * [2: * ]] 350 348 #EQ destruct(EQ) [ %1 % *: %2 %1 % ] … … 366 364 #i_vis %2 >mem_set_add @orb_Prop_r assumption 367 365 ] 368 ] *) cases daemon366 ] 369 367 ] 370 368 4,5,6: change with reverse in match rev; … … 423 421 lapply (in_map_domain … visited vis_hd) 424 422 >H3 normalize nodelta // 425  %{statement} (*CSC XXXXXXX423  %{statement} 426 424 % 427 425 [ @lookup_eq_safe … … 429 427 change with statement in match (lookup_safe ?????); 430 428 cases statement; 431 [ * [ # f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] normalize nodelta432 [1,2,3 : inversion (nxt ∈ visited') normalize nodelta #nxt_vis ]433 [1,2, 5,6: %  %2  %1 % ]434 [1,3,5,7,9,1 0,12:429 [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] normalize nodelta 430 [1,2,3,4: inversion (nxt ∈ visited') normalize nodelta #nxt_vis ] 431 [1,2,3,4,7,8: %  %2  %1 % ] 432 [1,3,5,7,9,11,13,14,16: 435 433 >nth_opt_append_r >rev_length <gen_length_prf try % 436 <minus_n_n try % whd in match graph_to_lin_statement; normalize nodelta437 >nxt_vis % 434 <minus_n_n try % try( whd in match graph_to_lin_statement; normalize nodelta 435 >nxt_vis %) 438 436 *: 439 437 lapply (in_map_domain … visited' nxt) >nxt_vis normalize nodelta 440 [1,3: * #n' ] #EQlookup >EQlookup normalize nodelta 441 [1,2: %2 >nth_opt_append_r >rev_length <gen_length_prf [2,4: %2 %1 ] 442 <minus_Sn_n % 443 *: %% 444 ] 445 ]*) cases daemon 438 [1,3,5: * #n' ] #EQlookup >EQlookup normalize nodelta 439 try (%% @False) 440 %2 >nth_opt_append_r >rev_length <gen_length_prf [2,4,6: %2 %1 ] 441 <minus_Sn_n % 442 ] 446 443 ] 447 444 ] 448 445  #NEQ #n_i >(lookup_add_miss … visited … NEQ) 449 cases daemon (*CSC XXXX450 446 #Hlookup elim (generated_prf1 … Hlookup) 451 447 #G1 * #s * #G2 #G3 … … 463 459 %{G2} 464 460 cases s in G3; 465 [ * [ #f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] 466 [1,3: * #EQnth_opt #next_spec %  * [*] #EQnth_opt [#next_spec %1 %  %2]  #EQnth_opt ] 467 [1,3,5,7: @nth_opt_append_hit_l assumption 468 2,4,6: @(eq_identifier_elim … nxt vis_hd) 469 [1,3: #EQ destruct(EQ) >lookup_add_hit whd [ %1 ] 461 [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] 462 [1,2,4: normalize nodelta #H cases H in ⊢ ?; H 463 #EQnth_opt #next_spec % 3: normalize nodelta * [*] #EQnth_opt [#next_spec %1 %  %2]  #EQnth_opt ] 464 [1,3,5,7,9: @nth_opt_append_hit_l assumption 465 2,4,6,8: @(eq_identifier_elim … nxt vis_hd) 466 [1,3,5,7: #EQ destruct(EQ) >lookup_add_hit whd 467 [1,2,3: %1] 470 468 lapply (in_map_domain … visited vis_hd) 471 469 >H3 #EQ >EQ in next_spec; * #_ #OK >OK % 472 *: #NEQ' >(lookup_add_miss … visited … NEQ') 473 lapply (in_map_domain … visited nxt) 474 inversion (nxt ∈ visited) #nxt_vis [1,3: * #n'' ] #EQlookup' 475 >EQlookup' in next_spec; whd in ⊢ (%→%); 476 [ * [ #H %1{H} ] #H %2 @nth_opt_append_hit_l assumption 477  #H @H 478 *: * >H2 470 *: #NEQ' >(lookup_add_miss … visited … NEQ') in 471 ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 472 generalize in match next_spec in ⊢ ?; 473 inversion (lookup … visited nxt) normalize nodelta 474 [2,4,6,8: #n'' ] #EQlookup' 475 [1,2,3: * [1,3,5: #H %1{H} ] #H %2 @nth_opt_append_hit_l assumption 476 4: #H @H 477 *: * #nxt_visiting @⊥ 478 >H2 in nxt_visiting; 479 479 cases pre in H1; 480 [1,3 : #_480 [1,3,5,7: #_ 481 481 *: #frst #pre_tl * #ABS #_ 482 482 ] whd in ⊢ (??%?→?); #EQ destruct(EQ) 483 [1,2 : cases NEQ' #ABS cases (ABS ?) %484 *: >nxt_vis in ABS;*483 [1,2,3,4: cases NEQ' #ABS cases (ABS ?) % 484 *: lapply ABS; whd in ⊢ (?%→?); >EQlookup' * 485 485 ] 486 486 ] 487 487 ] 488 10: @nth_opt_append_hit_l assumption 488 489 ] 489 ] *)490 ] 490 491 ] 491 492  #i whd in match visited'; … … 498 499  change with (bool_to_Prop (¬eq_identifier ??? ∧ ?)) 499 500 >eq_identifier_false [2: % #ABS <ABS in Heq; * #ABS' @ABS' % ] 500 @add_req_gen_prf [ #_  #s #next #_ #_] %501 @add_req_gen_prf [ #_  #s #next #_ ] % 501 502 ] 502 503 ] 503 504  @add_req_gen_prf 504 [ #K  # s #next #K #next_vis %1 %1 %{(GOTO … next)} % ]505 [ #K  #next #K #next_vis %1 %1 %{(GOTO … next)} % ] 505 506 whd in match generated'; whd in match translated_statement; 506 507 normalize nodelta 507 508 change with statement in match (lookup_safe ?????); 508 509 cases statement in K; 509 [ * [ # s  #a #ltrue] #nxt  #s #_ %1 %1 %{s} %  * ] normalize nodelta510 [ 2: #_ cases (true_or_false_Prop (nxt ∈ visited')) #nxt_vis510 [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s #_ %1 %1 %{s} %  * ] normalize nodelta 511 [3: #_ cases (true_or_false_Prop (nxt ∈ visited')) #nxt_vis 511 512 [ >nxt_vis normalize nodelta %1 %2 %{a} %{ltrue} %{nxt} % ] 512  #nxt_vis ]513 *: #nxt_vis ] 513 514 %2 % * >nxt_vis * 514 515  whd in match generated'; 515 @add_req_gen_prf [ #_  # s #next #_ #_ ] normalize >gen_length_prf %516 @add_req_gen_prf [ #_  #next #_ #_ ] normalize >gen_length_prf % 516 517  517 ] *)518 ] 518 519 qed. 519 520 … … 643 644 [ sequential s' nxt ⇒ 644 645 match s' with 645 [ step_seq _ ⇒ 646 (stmt_at … c n = Some ? (sequential … s' it)) ∧ 646 [ COND a ltrue ⇒ 647 (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨ 648 (stmt_at … c n = Some ? (FCOND … I a ltrue nxt)) 649  _ ⇒ 650 (stmt_at … c n = Some ? (sequential … s' it)) ∧ 647 651 ((sigma nxt = Some ? (S n)) ∨ 648 652 (stmt_at … c (S n) = Some ? (GOTO … nxt))) 649  COND a ltrue ⇒650 (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨651 (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))652  CALL _ _ _ ⇒653 (stmt_at … c n = Some ? (sequential … s' it)) ∧654 ((sigma nxt = Some ? (S n)) ∨655 (stmt_at … c (S n) = Some ? (GOTO … nxt)))656  COST_LABEL _ ⇒657 (stmt_at … c n = Some ? (sequential … s' it)) ∧658 ((sigma nxt = Some ? (S n)) ∨659 (stmt_at … c (S n) = Some ? (GOTO … nxt)))660 653 ] 661 654  final s' ⇒ … … 708 701  >commutative_plus change with (? ≤ g) % 709 702 ] 710 cases daemon qed. (*711 703 ** 712 704 #visited #required #generated normalize nodelta **** … … 725 717 * #n_lbl #EQsigma 726 718 elim (sigma_prop … EQsigma) #_ * #stmt * #_ 727 cases stmt [ * [ # s  #a #ltrue] #nxt  #s  * ] normalize nodelta728 [ * #EQnth_opt #_  * [ * ] #EQnth_opt [ #_ ] #EQnth_opt ]719 cases stmt [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] normalize nodelta 720 [1,2,4: * #EQnth_opt #_ 3: * [ * ] #EQnth_opt [ #_ ] 5: #EQnth_opt ] 729 721 >(nth_opt_index_of_label ???? n_lbl ? H) 730 [1,4,7,10: normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption 731 3: @(sequential … s it) 6: @(sequential … (COND … a ltrue) it) 732 9: @(FCOND … I a ltrue nxt) 12: @(final … s) 733 2,5,8,11: >nth_opt_filter_labels >EQnth_opt >m_return_bind >m_return_bind 734 >H2 % 722 try (normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption) 723 [1,3,5,7,9,11: 724 >nth_opt_filter_labels in ⊢ (??%?); 725 (* without the try it does not work *) 726 try >EQnth_opt in ⊢ (??%?); 727 >m_return_bind in ⊢ (??%?); 728 >m_return_bind in ⊢ (??%?); 729 >H2 in ⊢ (??%?); % 730 *: 735 731 ] 736 732  #eq_lookup elim (sigma_prop ?? eq_lookup) … … 739 735 [ @All_append 740 736 [ cases stmt in stmt_spec; 741 [ * [ #s  #a #ltrue ] #nxt  #s #_ %  * ] 742 normalize nodelta * [ #stmt_at_EQ * #nxt_spec  * #stmt_at_EQ #nxt_spec  #stmt_at_EQ ] 737 [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s #_ %  * ] 738 normalize nodelta 739 [1,2,4: * #stmt_at_EQ * #nxt_spec 3: * [ * ] #stmt_at_EQ [ #nxt_spec ]] 743 740 %{I} 744 [1,3: >nxt_spec % #ABS destruct(ABS) 745 *: lapply (in_map_domain … visited nxt) 746 >req_vis 747 [1,3: * #x #EQ >EQ % #ABS destruct(ABS) 748 2: @(proj1 … (labels_in_req (S n) (GOTO … nxt) …)) 749 whd in ⊢ (??%?); >nxt_spec % 750 4: @(proj1 … (proj2 … (labels_in_req n (FCOND … I a ltrue nxt) …))) 751 whd in ⊢ (??%?); >stmt_at_EQ % 752 ] 741 try (>nxt_spec % #ABS destruct(ABS) @False) 742 lapply (in_map_domain … visited nxt) 743 >req_vis 744 [1,3,5,7: * #x #EQ >EQ % #ABS destruct(ABS) 745 2,4,6: @(proj1 … (labels_in_req (S n) (GOTO … nxt) …)) 746 whd in ⊢ (??%?); >nxt_spec % 747 8: @(proj1 … (proj2 … (labels_in_req n (FCOND … I a ltrue nxt) …))) 748 whd in ⊢ (??%?); >stmt_at_EQ % 753 749 ] 754 750  cases stmt in stmt_spec; 755 [ * [ # s  #a #ltrue] #nxt  #s  * ] normalize nodelta756 [ * #EQ #_  * [ * #EQ #_  #EQ ] #EQ ]751 [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] normalize nodelta 752 [1,2,4: * #EQ #_ 3: * [ * ] #EQ [ #_ ] 5: #EQ ] 757 753 whd in match stmt_explicit_labels; normalize nodelta 758 [ @(All_mp … (labels_in_req n (sequential … s it) ?)) 754 [ @(All_mp … (labels_in_req n (sequential … (COST_LABEL … cost) it) ?)) 755  @(All_mp … (labels_in_req n (sequential … (CALL … f args dest) it) ?)) 756  @(All_mp … (labels_in_req n (sequential … s it) ?)) 759 757  @(All_mp … (labels_in_req n (sequential … (COND … a ltrue) it) ?)) 758 6: @(All_mp … (labels_in_req n (final … s) ?)) 760 759  cases (labels_in_req n (FCOND … I a ltrue nxt) ?) 761 760 [ #l_req #_ %{I} lapply (in_map_domain … visited ltrue) 762 761 >(req_vis … l_req) * #n #EQ' >EQ' % #ABS destruct(ABS) ] 763  @(All_mp … (labels_in_req n (final … s) ?))764 762 ] 765 [1,3,6: #l #l_req >(lookup_eq_safe … (req_vis … l_req)) % #ABS destruct(ABS) 763 [1,3,5,7,9: #l #l_req >(lookup_eq_safe … (req_vis … l_req)) 764 % #ABS destruct(ABS) 766 765 *: whd in ⊢ (??%?); >EQ % 767 766 ] 768 767 ] 769 768  cases stmt in stmt_spec; 770 [ * [ # s  #a #ltrue] #nxt  #s  * ] normalize nodelta771 [ * #EQ #H  * [ * #EQ #H  #EQ ] #EQ ]769 [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] normalize nodelta 770 [1,2,4: * #EQ #H 3: * [ * ] #EQ [ #H ] 5: #EQ ] 772 771 >stmt_at_filter_labels 773 772 whd in match (stmt_at (mk_lin_params p) ?? n); >EQ normalize nodelta 774 [ % [%] cases H H [#H %1{H}  #EQ' %2 >stmt_at_filter_labels whd in ⊢ (??%?); >EQ' % ] 773 [1,2,3: % [1,3,5: %] cases H H 774 #H try (%1{H}) %2 >stmt_at_filter_labels whd in ⊢ (??%?); >H % 775 775  %1 %{H} % 776 776  %2 % … … 796 796 cut (generated = S i) 797 797 [ @(le_to_le_to_eq … (not_lt_to_le … INEQ) ) 798 elim (option_bind_inverse ????? EQ) #x * #EQ1 #EQ2 798 whd in EQ : (??%?); inversion (nth_opt ???) in EQ; 799 [2: #x ] #EQ1 whd in ⊢ (??%%→?); #EQ2 destruct 799 800 <length_reverse 800 801 @(nth_opt_hit_length … EQ1) … … 843 844 〈«mk_joint_internal_function (mk_lin_params p) globals 844 845 (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig) 845 (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) 846 (joint_if_stacksize ?? f_sig) code entry , ?»,846 (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) (joint_if_locals ?? f_sig) 847 (joint_if_stacksize ?? f_sig) code entry entry (* exit is dummy! *), ?», 847 848 sigma〉. 848 849 normalize nodelta 
src/joint/semanticsUtils.ma
r2688 r2708 311 311 * #vars1 #functs1 #main1 312 312 * #vars2 #functs2 #main2 313 * #Mvars #Mfns #EQmain destruct 313 * 314 whd in match prog_var_names; 315 normalize nodelta; 316 #Mvars #Mfns #EQmain destruct 314 317 lapply (sym_eq ????) 315 whd in match prog_var_names in functs2 Mfns ⊢ %; 316 normalize nodelta in functs2 Mfns ⊢ %; #E 317 lapply Mfns lapply functs2 functs2 lapply Mvars Mvars lapply init_eq init_eq 318 #E 319 lapply Mfns lapply functs2 functs2 318 320 whd in match globalenv; whd in match globalenv_allocmem; 319 normalize nodelta 320 cases daemon 321 (* TODO I hate coercions *) 321 whd in match prog_var_names in E ⊢ %; 322 normalize nodelta in E ⊢ %; 323 >E normalize nodelta #functs2 #Mfns 324 @add_globals_match [ assumption  % ] 325 @add_functs_match [ assumption ] 326 % try % #p % 322 327 qed. 323 328 
src/utilities/state.ma
r1976 r2708 24 24 definition state_set : ∀S.S → state_monad S unit ≝ λS,s.λ_.〈s,it〉. 25 25 definition state_run : ∀S,X. S → (state_monad S X) → X ≝ λS,X,s,c.'pi2 (c s). 26 definition state_update : ∀S.(S → S) → state_monad S unit ≝ λS,f,s.〈f s, it〉. 26 27 27 28 definition state_pred ≝ λS.λPs : S → Prop.mk_MonadPred (state_monad S)
Note: See TracChangeset
for help on using the changeset viewer.