Changeset 3397


Ignore:
Timestamp:
Nov 21, 2013, 8:20:02 PM (6 years ago)
Author:
piccolo
Message:

partial commit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3396 r3397  
    1818include "../src/utilities/option.ma".
    1919include "basics/jmeq.ma".
     20
     21discriminator option.
    2022
    2123record instr_params : Type[1] ≝
     
    9597}.
    9698
    97 record env_item (p : env_params) (p' : instr_params) : Type[0] ≝
     99record signature (p : env_params) (p' : instr_params) : Type[0] ≝
    98100{ f_name : FunctionName
    99101; f_pars : form_params_type p
     102; f_ret : return_type p'
     103}.
     104
     105record env_item (p : env_params) (p' : instr_params) : Type[0] ≝
     106{ f_sig :> signature p p'
    100107; f_lab : CallCostLabel
    101108; f_body : Instructions p'
    102 ; f_ret : return_type p'
    103109}.
    104110
     
    126132; eval_cond_cond : cond_instr p → state p → option (bool × (store_type p))
    127133; eval_loop_cond : loop_instr p → state p → option (bool × (store_type p))
    128 ; eval_call : env_item p p → act_params_type p → state p → option (store_type p)
     134; eval_call : signature p p → act_params_type p → state p → option (store_type p)
    129135; eval_after_return : return_type p → store_type p → option (store_type p)
    130136; init_store : store_type p
     
    516522   [ None ⇒ 〈False,nil ?〉
    517523   | Some w ⇒
    518       match \fst y with
     524      match \fst z with
    519525       [ ret_act opt_x ⇒
    520526           match ret_costed_abs keep opt_x with
     
    522528                               get_element … m lbl = lbl :: (\fst w),(nil ?)〉
    523529           | None ⇒
    524               〈\fst z = ret_act (None ?) ∧ \fst x ∧ \snd w = \snd y,\fst w〉
     530              〈\fst y = ret_act (None ?) ∧ \fst x ∧ \snd w = \snd y,\fst w〉
    525531           ]
    526532       | cost_act opt_x ⇒
     
    624630           (λi,x.let 〈t_env,n,m,keep〉 ≝ x in
    625631           let info ≝ call_post_trans … (f_body … i) n (nil ?) in
    626                    〈(mk_env_item … (f_name … i) (f_pars … i) (f_lab … i)
    627                                   (t_code … info) (f_ret … i)) :: t_env,
     632                   〈(mk_env_item ??
     633                       (mk_signature ??(f_name ?? i) (f_pars … i) (f_ret … i))
     634                       (f_lab … i) (f_body … i)) :: t_env,
    628635                     fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 ::
    629636                                     ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉)
    630637          (〈nil ?,max_all,nil ?,nil ?〉) (env … prog)) in
    631638〈mk_Program ?? t_env (t_code … (call_post_trans … (main … prog) n (nil ?))),m,keep〉 .
    632 
    633 discriminator option.
    634639
    635640definition map_labels_on_trace :
     
    642647 #m #l1 elim l1 // #hd #tl #IH #l2 >associative_append <IH //
    643648qed.
     649
     650include "../src/common/Errors.ma".
    644651
    645652lemma correctness : ∀p,p',prog.
     
    664671  normalize nodelta inversion (foldr2 ???????) [ #_ *] * #H1 #l2 #EQHl2
    665672  >m_return_bind normalize nodelta
    666  
    667673  inversion (call_post_clean ?????) [ #_ **** ]
    668674  * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta
    669   cases lab1 in Hio11 Hl1 EQcont11 H; normalize nodelta
    670  
    671   [ whd in match is_silent_cost_act_b; normalize nodelta
     675  cases l1' (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta
     676  [1,4: [ #x #y ] (*#_ #_ #_ #H*) ****
     677  | #x cases (ret_costed_abs ??) normalize nodelta [|#c] *****[|*] #EQ @⊥ >EQ in Hl1;
     678    normalize * /2/ ] *
     679  [ (*#Hio11 #_ #EQcont11 #H*) normalize nodelta ***** #EQ destruct(EQ)
     680    #HH1 #EQ destruct(EQ) >EQcode11 inversion(code … s1')
     681    [
     682    | #x
     683    | #seq #lbl #i #_
     684    | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
     685    | #cond #ltrue #i1 #lfalse #i2 #_ #_
     686    | #f #act_p #ret_post #i #_
     687    | #l_in #io #l_out #i #_
     688    ]
     689    [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)]
     690         cases(call_post_clean ?????) normalize nodelta
     691         [1,3,5,7,9: #EQ destruct(EQ)] cases daemon (* da fare assurdi!!!*) ]
     692    #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11
     693    cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 …)
     694    [2: whd whd in match check_continuations; normalize nodelta >EQHl2
     695        normalize nodelta % // % // % // @EQcode_c_st12 ]
     696    #l3 * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{l3} %{st3'}
     697    %{(t_ind … (cost_act (None ?)) …  t')}
     698    [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉)
     699      [3: assumption |4: assumption |*:] /3 by nmk/ ]
     700    % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'}
     701    whd in match (get_costlabels_of_trace ????);
     702    whd in match (get_costlabels_of_trace ????); >EQcosts %
     703  | #lbl #Hiost11 #_ #EQcontst11 #H normalize nodelta ****** #EQ destruct(EQ)
     704    #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 inversion(code … s1')
     705    [
     706    | #x
     707    | #seq #lbl #i #_
     708    | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
     709    | #cond #ltrue #i1 #lfalse #i2 #_ #_
     710    | #f #act_p #ret_post #i #_
     711    | #l_in #io #l_out #i #_
     712    ]
     713    [|*: #_ whd in ⊢ (??%% → ?); #EQ cases daemon (* da fare assurdi !!!*) ]
     714    #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio
     715    cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l3 …)
     716    [2: whd whd in match check_continuations; normalize nodelta >EQHl2
     717        normalize nodelta % // % // % // @EQcode_c_st12 ]
     718    #l3' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen %{l3'} %{st3'}
     719    %{(t_ind … (cost_act (Some ? lbl)) … t')}
     720    [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉)
     721      [3: assumption |4: assumption |*:] /3 by nmk/ ]
     722    % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'}
     723    whd in match (get_costlabels_of_trace ????);
     724    whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
     725    whd in match map_labels_on_trace; normalize nodelta
     726    whd in match (foldr ?????);
     727    change with (map_labels_on_trace ??) in match (foldr ?????); >EQget_el
     728    whd in match (append ???); whd in match (append ???) in ⊢ (???%); @eq_f
     729    whd in match (append ???) in ⊢ (??(???%)(??%?)); @EQcost
     730  ]   
     731| #seq #i #store * [| #lbl] #EQcode11 #EQstore #EQ destruct(EQ) #EQcont
     732  #EQ destruct(EQ) #Hio_st11 #Hio_st12 #EQ destruct(EQ) #EQ1 #EQ2 destruct(EQ1 EQ2)
     733  #EQ destruct(EQ) #tl #IH #st3 #l1 whd in ⊢ (% → ?);
     734  inversion(check_continuations ?????) [1,3: #_ *] * #H1 #l2
     735  [ >EQcont in ⊢ (% → ?); | >EQcont in ⊢ (% → ?); ] #EQcheck normalize nodelta
     736  *** #HH1 [ >EQcode11 in ⊢ (% → ?); | >EQcode11 in ⊢ (% → ?); ]
     737  inversion(code … st3)
     738  [1,2,4,5,6,7,8,9,11,12,13,14: (*assurdi da fare *) cases daemon ]
     739  #seq1 #opt_l #i1 #_ #EQcode_st3 change with (m_bind ?????) in ⊢ (??%? → ?);
     740  cases daemon
     741|8: #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
     742    #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
     743    destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #IH #st1' #l1 whd in ⊢ (% → ?);
     744    inversion(check_continuations ??????) [1,3: #_ *] * #H1 #l2 #EQcheck
     745    normalize nodelta *** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1')
     746    [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_
     747    #EQcode_st1' #EQclean #EQstore #EQio
     748    cut(∃env_it',n.lookup p p (env … trans_prog) f = return env_it' ∧
     749          t_code … (call_post_trans … (f_body … env_it) n (nil ?)) = f_body … env_it')
     750    [1,3: cases daemon (*TODO*) ] * #env_it' * #fresh' * #EQenv_it' #EQtrans
     751    cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) l2 …)
     752    [2: whd >EQcont12 change with (m_bind ??? (check_continuations ??????) ?) in match (check_continuations ??????);
     753        >EQcheck >m_return_bind change with (m_bind ?????) in EQclean : (??%?);
     754    inversion(call_post_clean ?????) in EQclean; [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
     755    * #l3 #i'' #EQi'' >m_return_bind cases opt_l' in EQcode_st1'; [| #lbl'] #EQcode_st1'
     756    normalize nodelta
     757    [2: inversion(memb ???) normalize nodelta #Hlbl_keep
     758        [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
     759          #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta
     760          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
     761          lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
     762          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' l3)
     763          #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
     764          #EQ destruct(EQ) whd in match ret_costed_abs; normalize nodelta >Hlbl_keep
     765          normalize nodelta % // % // % [ % // % // % //] >EQcode12 <EQtrans
     766          cases daemon (*TODO*)
     767        | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     768          whd in match ret_costed_abs; normalize nodelta
     769           * [ #_ #l3'
     770    cases(bind_inversion ????? H) in ⊢ ?;
     771
     772   
     773    >EQcost normalize
     774   
     775    %{l1}
     776  xxxxxxxx
     777   whd in match is_silent_cost_act_b; normalize nodelta
    672778    cases lab1 in H Hio11; normalize nodelta
    673779    [1,2,4: [1,2: #x [ #y]] #H #Hio11 #EQ destruct]
Note: See TracChangeset for help on using the changeset viewer.