 Timestamp:
 Apr 15, 2013, 4:31:50 PM (8 years ago)
 Location:
 src/ERTL
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r3072 r3145 3 3 include "ASM/Arithmetic.ma". 4 4 include "joint/TranslateUtils.ma". 5 include "joint/joint_stacksizes.ma". 5 6 6 7 (* Note: translation is complicated by having to preserve the carry bit and … … 441 442 % 442 443 qed. 444 445 lemma ERTLToLTL_monotone_stacksizes : 446 ∀fix,col. 447 ∀p_in. 448 let cost_m ≝ \snd (\fst (ertl_to_ltl fix col p_in)) in 449 stack_cost_model_le (stack_cost ? p_in) cost_m. 450 #fix #col #p_in whd 451 @list_map_opt_All2 452 [ @(λid_def1,id_def2. 453 match \snd id_def1 with 454 [ Internal f1 ⇒ 455 match \snd id_def2 with 456 [ Internal f2 ⇒ 457 \fst id_def1 = \fst id_def2 ∧ 458 le (joint_if_stacksize … f1) (joint_if_stacksize … f2) 459  _ ⇒ False 460 ] 461  External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False  External _ ⇒ True ] 462 ]) 463  * #id * #f1 * #id' * #f2 normalize nodelta [*: * %] 464 ** #H %{H} % ] 465 @All2_of_map * #id * #f normalize nodelta [2: %] 466 % [%] 467 cases (b_graph_translate ?????) #f_out * #data ** 468 [2: #hd #tl ] * #f_lbls * #f_regs * [*] whd in ⊢ (%→?); #EQ_data 469 #props >(ss_def_out_eq … props) >EQ_data 470 generalize in match (joint_if_stacksize ???); generalize in match (spilled_no ??); 471 p_in // 472 qed. 473 
src/ERTL/ERTLToLTLAxiom.ma
r3096 r3145 6 6 include "common/AssocList.ma". 7 7 8 (* Inefficient, replace with Trie lookup *)9 definition lookup_stack_cost ≝10 λp.λid : ident.11 assoc_list_lookup ? ℕ id (eq_identifier …) p.12 13 8 axiom ERTLToLTL_ok : 14 9 ∀fix_comp : fixpoint_computer. … … 17 12 let 〈p_out, m, n〉 ≝ ertl_to_ltl fix_comp colour p_in in 18 13 (* what should we do with n? *) 19 let stacksizes ≝ lookup_stack_costm in14 let stacksizes ≝ stack_sizes m in 20 15 ∀init_in.make_initial_state 21 16 (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
Note: See TracChangeset
for help on using the changeset viewer.