Changeset 3492 for LTS/Vm.ma


Ignore:
Timestamp:
Sep 24, 2014, 6:44:14 PM (5 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3491 r3492  
    891891  | @eqb_elim normalize nodelta
    892892    [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #a1 #good_st_a1 #labels
     893    >(rewrite_in_dependent_map ??? [])
     894    [ whd in ⊢ (???% → ?); #EQ destruct whd >act_neutral >act_neutral
     895      lapply (instr_map_ok … good … prf …)
    893896   
    894       >(rewrite_in_dependent_map …) [2: @eq_f [2: @get_cost_label_append |]|
    895       >rewrite_in_dependent_map [2:
    896       @chop_append_singleton
    897       whd in ⊢ (??%% → ?); whd in match (dependent_map ????);
    898      
    899        >(act_neutral … a1) in H;
    900      
    901      
    902        #H #H1
    903       cases st2 in prf; -st2 [3: #st2] #prf
    904       lapply(instr_map_ok … good … prf … rel_fin)
    905      
    906        lapply prf *
    907       #EQpc_st2 #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct
    908       >act_neutral >act_neutral @(instr_map_ok … good … rel_fin)
    909      
    910      
    911        @opt_safe_elim #k_init
    912       #EQk_init whd in ⊢ (??%% → ?); whd in match (dependent_map ????); #EQ destruct
    913       >act_neutral whd in match (big_op ??); >act_op >act_neutral
    914      
    915      
    916        #H >act_neutral whd in prf;
    917        
    918         cases l in prf H1 H2;
    919         [1,4: #f #lbl |2,5: * [2,4: #lbl] |*: * [2,4: #lbl] ] #prf
    920         ** [normalize in ⊢ (% → ?);
    921          ⊢ (??%% → ?);
    922 
    923  #st * #st3 * #t1 * #l * #prf * #ABS cases(tbase_tind_append … ABS) ]
    924   cases st -st [3: #x] * #H #_ whd in ⊢ (??%% → ?); @eqb_elim [2: * #ABS @⊥ @ABS %]
    925    #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin_a1
    926    #labels whd in ⊢ (???% → ?); #EQ destruct >act_neutral >act_neutral assumption
    927 | -st1 -st2 * [3: #st1] * [3,6,9: #st2] #st3 #l whd in ⊢ (% → ?); *
    928   [ #no_final #Hstep #tl #IH whd in ⊢ (% → ?);
    929    (*
    930     #EQlabels
    931   #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta
    932   [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st
    933     normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    934     #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption
    935   | ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta
    936     #H cases(bind_inversion ????? H) -H *
    937     [ #seq * [|#lbl1]
    938     | #newpc
    939     | #cond #newpc #ltrue #lfalse
    940     | #lin #io #lout
    941     | #f
    942     |
    943     ]
    944     * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate;
    945     normalize nodelta >EQfetch >m_return_bind normalize nodelta
    946     cases(asm_is_io ??) normalize nodelta
    947     [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
    948     |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_
    949       [3: cases x normalize nodelta
    950       |6: #H cases(bind_inversion ????? H) -H #y * #_
    951       ]
    952     ]
    953     whd in ⊢ (??%% → ?); #EQ destruct
    954     [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]]
    955     >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
    956     #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ >EQ >neutral_r
    957     >act_neutral
    958     @(instr_map_ok … good … EQfetch … good_st_a1) /2/
    959   ]*)
    960 | -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
     897      >(act_neutral ?? (act_abs ? abs_t) a1))
     898      change
     899      with (get_costlabels_of_trace ??? (?@?))
     900      in match (get_costlabels_of_trace ????);
     901      cases l
     902   
     903      >(rewrite_in_dependent_map …) [2: @eq_f [2: @get_cost_label_append |skip]|3:skip]
     904      cases daemon
     905    | cases daemon ]]
     906| -st1 #st1 #st3 #st4 #l whd in ⊢ (% → ?);
     907
     908 * #H3 #H4
     909
     910  -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
    961911  #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????);
    962912  whd #costs >dependent_map_append
Note: See TracChangeset for help on using the changeset viewer.