Ignore:
Timestamp:
Mar 7, 2013, 1:29:31 PM (7 years ago)
Author:
piccolo
Message:

Partial commit not yet finished

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrUtils.ma

    r2786 r2801  
    240240   (ps_reg_store r).
    241241#prog #f_lbls #r #restr #Hreg whd in match ps_reg_store; normalize nodelta
    242 #bv * #psd_r #hw_r @mfr_bind1
    243 [ @(sigma_register_env prog f_lbls restr)
    244 | whd in match reg_store; whd in match sigma_regs; normalize nodelta
    245   #x #x_spec %{(add RegisterTag beval psd_r r bv)} % // whd in x_spec : (???%);
    246   destruct whd in match sigma_register_env; normalize nodelta >map_add
     242#bv * #psd_r #hw_r @mfr_return_eq1
     243whd in match reg_store; whd in match sigma_regs; normalize nodelta
     244whd in match sigma_register_env; normalize nodelta >map_add
    247245  >add_set_minus [% | assumption]
    248 | #z @mfr_return_eq1 %
    249 qed. 
     246qed.
    250247(* 
    251248   lapply(update_ok_to_lookup ?????? x_spec) * * #_ #EQpsd #_
     
    705702include alias "basics/lists/listb.ma".
    706703
     704check eval_seq_no_pc
     705
     706xxxxxxxxxxxxxxxxxxxxxxxx
     707
    707708lemma eval_seq_no_pc_no_call_ok :
    708709∀prog : ertl_program.
     
    710711∀f_lbls : lbl_funct. ∀f_regs : regs_funct.
    711712∀stack_size.
    712 ∀bl.∀id. ∀fn : (joint_closed_internal_function ? (prog_var_names ?? prog)).
    713 ∀fn_out : (joint_closed_internal_function ? (prog_var_names ?? trans_prog)).
     713∀bl.∀id.
    714714∀seq.
    715 (∀l. code_has_label … (joint_if_code … fn) l → 
     715(∀fn : joint_closed_internal_function ERTL (prog_var_names … prog).
     716∀l. code_has_label … (joint_if_code … fn) l → 
    716717opt_All …
    717718       (λlabs.(All … (λreg.bool_to_Prop(¬(reg ∈ labs)))
     
    723724      (eval_seq_no_pc ERTL_semantics
    724725             (globals (mk_prog_params ERTL_semantics prog stack_size))
    725              (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id fn seq)
     726             (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id seq)
    726727      (eval_seq_no_pc ERTLptr_semantics
    727728             (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size))
    728729             (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size))
    729              id fn_out (seq_embed … seq)).
    730 #prog #f_lbls #f_regs #stack_size #bl #f #fn #fn_out #seq #fresh_regs
     730             id (seq_embed … seq)).
     731#prog #f_lbls #f_regs #stack_size #bl #f #seq #fresh_regs
    731732cases seq in fresh_regs;
    732733[ #c #_ #st @mfr_return1
     
    11621163qed.
    11631164
    1164 (*TO BE MOVED *)
    11651165lemma excluded_middle_list :
    1166 ∀A : Type[0]. ∀P : A → Prop. (∀a.decidable … (P a)) → ∀ l.
     1166∀A : Type[0]. ∀P : A → Prop.∀ l : list A. (∀a : A.In A l a → decidable … (P a)) →
    11671167All … P l ∨ Exists … (λa.¬(P a)) l.
    1168 #A #P #Dec #l elim l [% %] #hd #tl #IH
    1169 cases IH [ cases(Dec hd) [ #H1 #H2 % whd % assumption | #H #_ %2 whd % assumption]
     1168#A #P #l elim l [#_  % %] #hd #tl #IH #Dec
     1169cases IH [ cases(Dec hd ?)
     1170            [ #H1 #H2 % whd % assumption
     1171            | #H #_ %2 whd % assumption
     1172            | % %
     1173            ]
    11701174         | #H %2 whd %2 assumption
     1175         | #a #H @Dec %2 assumption
    11711176         ]
    11721177qed.
     
    15251530] qed.
    15261531
     1532
    15271533lemma ertl_save_frame_ok : ∀prog : ertl_program.
    15281534∀f_lbls.∀f_regs : regs_funct.∀kind,restr.
    15291535preserving1 ?? res_preserve1 ????
    1530            (λst. match fetch_internal_function … (globalenv_noinit … prog)
     1536      (λst : Σs: state_pc ERTLptr_semantics.
     1537             sigma_pc_opt prog f_lbls (pc … s) ≠ None ?
     1538      . match fetch_internal_function … (globalenv_noinit … prog)
    15311539                       (pc_block (pc … st)) with
    15321540                 [ OK y ⇒ let 〈f,fn〉 ≝ y in
     
    15411549           (ertl_save_frame kind it)
    15421550           (match kind with
    1543             [ID ⇒ ertlptr_save_frame ID it
     1551            [ID ⇒ ertlptr_save_frame kind it
    15441552            |PTR ⇒ λst. !st' ← push_ra … st (pc … st);
    1545                         ertlptr_save_frame ID it (set_no_pc … st' st)
     1553                        ertlptr_save_frame kind it (set_no_pc … st' st)
    15461554            ]).
    1547 cases daemon (*TODO *)
    1548 qed.
    1549 
    1550 
    1551 
     1555#prog #f_lbls #f_regs * #restr * #st #st_prf
     1556inversion(fetch_internal_function ???) normalize nodelta
     1557[1,3: * #f #fn #EQfn normalize nodelta whd in match ertl_save_frame; whd in match ertlptr_save_frame;
     1558      normalize nodelta @mfr_bind1
     1559      [2,5: @push_ra_ok [1,2: assumption] |1,4: skip
     1560      |*: #st1 [ >m_return_bind] @mfr_bind_inversion1
     1561          [1,4: @(λf.match sigma_frames_opt prog f_lbls f_regs f with [Some g ⇒  g | None ⇒ [ ]])
     1562          |2,5: @opt_to_res_preserve1 whd in match sigma_state; whd in match set_no_pc;
     1563                normalize nodelta cases(st_frms … st1) [1,3: @opt_preserve_none1]
     1564                #frames #frames1 whd in match sigma_frames; normalize nodelta
     1565                >m_return_bind #EQframes %{frames} % [%] >EQframes %
     1566          |*: #frames #H lapply(opt_eq_from_res ???? H) -H whd in match sigma_state;
     1567              normalize nodelta #EQt_frames #H lapply(opt_eq_from_res ???? H) -H
     1568              whd in match set_no_pc; normalize nodelta #EQframes >EQframes in EQt_frames;
     1569              whd in match sigma_frames; normalize nodelta >m_return_bind
     1570              inversion(sigma_frames_opt ???) [1,3: #_ #ABS destruct(ABS)]
     1571              #t_frames #EQt_frames #_ @mfr_return_eq1 normalize nodelta @eq_f
     1572              whd in match set_frms; normalize nodelta >m_return_bind
     1573              cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2.
     1574                    a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 →
     1575                      mk_state ERTL_semantics a1 b1 c1 d1 e1 =
     1576                      mk_state ERTL_semantics a2 b2 c2 d2 e2)
     1577              [1,3: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14
     1578                    #H15 //] #APP @APP try %
     1579              [1,3: whd in match sigma_frames_opt; whd in match m_list_map;
     1580                    normalize nodelta  whd in match (foldr ?????); normalize nodelta
     1581                    >EQfn >m_return_bind normalize nodelta
     1582                    change with (sigma_frames_opt prog f_lbls f_regs frames)
     1583                                                         in match (foldr ?????);
     1584                    >EQt_frames >m_return_bind whd in match sigma_regs;
     1585                    normalize nodelta cases(regs … st1) #ps_reg #hw_reg
     1586                    >(pc_block_eq … st_prf) %
     1587              |*: whd in match set_regs; whd in match sigma_regs; normalize nodelta
     1588                  cases(regs … st1) #ps_r #hw_r normalize nodelta
     1589                  whd in match sigma_register_env; normalize nodelta
     1590                  @eq_f2 // change with (empty_map RegisterTag beval) in match (map RegisterTag ????);
     1591                  <(empty_set_minus … restr) %
     1592              ]
     1593          ]
     1594      ]   
     1595|*: #e #_ #x whd in match ertl_save_frame; normalize nodelta normalize nodelta
     1596    #H @('bind_inversion H) -H #y whd in match push_ra; normalize nodelta
     1597    #H @('bind_inversion H) -H #z whd in match push; normalize nodelta
     1598    whd in match (istack ??); whd in match is_push; normalize nodelta
     1599    >m_return_bind whd in match set_istack; normalize nodelta whd in ⊢ (??%% →?);
     1600    #EQ destruct(EQ) normalize nodelta >m_return_bind whd in ⊢ (??%% → ?);
     1601    #EQ destruct(EQ) whd in match (st_frms ??); whd in ⊢ (??%% → ?);
     1602    #EQ destruct(EQ)
     1603]
     1604qed.
Note: See TracChangeset for help on using the changeset viewer.