Changeset 2452


Ignore:
Timestamp:
Nov 12, 2012, 12:50:21 PM (7 years ago)
Author:
piccolo
Message:

Completed commutation lemmas of fetch_statement

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2447 r2452  
    302302 whd in move_st1_st1';
    303303 letin lin_prog ≝ (linearise ? graph_prog)
    304  letin st2' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) …
     304
     305 cut (joint_closed_internal_function (mk_graph_params p) (globals (graph_prog_params p p' graph_prog))) [cases daemon (*???*)] #graph_fun
     306
     307 cases (linearise_code_spec … p' graph_prog graph_fun
     308         (joint_if_entry … graph_fun))     
     309 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
     310 lapply (sigma_spec
     311         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … st1)))
     312 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … wf_st1) |2: skip ]
     313 -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec whd in sigma_spec;
     314 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
     315 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved
     316 #related_lin_stm_graph_stm
     317 inversion (stmt_implicit_label ???)
     318 [ whd in match (opt_All ???); #stmt_implicit_spec #_
     319   letin st2_opt' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) …
    305320               (ev_genv (lin_prog_params p p' lin_prog))
    306321               (linearise_status_fun … sigma st1 wf_st1))
    307  whd in st2';
    308  whd in match (fetch_statement ?????) in st2';
    309  >fetch_function_sigma_commute in st2';
    310  whd in match (fetch_function ????) in st2';
    311  XXX
    312  check fetch_statement
    313  CSC
    314  %{}
    315 
    316 whd in classified_st1_cl;
    317 whd in classified_st1_cl:(??%?);
    318 inversion (fetch_statement ?????) in classified_st1_cl;
    319 
    320 <classified_st1_cl -cl
    321 whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ] ?);
    322 inversion (fetch_statement ?????)
    323 
    324 inversion (fetch_statement ?????)
    325 qed.
     322   check st2_opt'
     323   cut (∃st2': lin_abstract_status p p' lin_prog. st2_opt' = return st2')
     324   [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec'
     325   normalize nodelta in st2_spec'; -st2_opt'
     326   %{st2'} %{(taaf_step … (taa_base …) …)}
     327   [ cases daemon (* TODO, together with the previous one? *)
     328   | @st2_spec' ]
     329   %[%] [%]
     330   [ whd
     331     whd in st2_spec':(??%?); >fetch_statement_sigma_commute in st2_spec';
     332     whd in move_st1_st1':(??%?);
     333     cut (fetch_statement (graph_prog_params p p' graph_prog) (graph_prog_params … graph_prog) … (ev_genv (graph_prog_params … graph_prog)) … (pc … st1) = OK ? 〈graph_fun,graph_stmt〉)
     334     [ cases daemon (* TODO once and for all, consequence of graph_lookup_ok *) ]
     335     #fetch_statement_ok >fetch_statement_ok in move_st1_st1';
     336     whd in ⊢ (??%? → ??%? → ?); normalize nodelta
     337     inversion graph_stmt in stmt_implicit_spec; normalize nodelta
     338     [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ]
     339     XXXXXXXXXX siamo qua, caso GOTO e RETURN
     340   | cases daemon (* TODO, after the definition of label_rel, trivial *) ]
     341   ]
     342 | ....
     343qed.
Note: See TracChangeset for help on using the changeset viewer.