Changeset 2452 for src/joint/lineariseProof.ma

Timestamp:

Nov 12, 2012, 12:50:21 PM (7 years ago)

Author:

piccolo

Message:

Completed commutation lemmas of fetch_statement

File:

• src/joint/lineariseProof.ma (modified) (1 diff)

src/joint/lineariseProof.ma

@@ -302 +302 @@
  whd in move_st1_st1';
  letin lin_prog ≝ (linearise ? graph_prog)
- letin st2' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) …
+
+ cut (joint_closed_internal_function (mk_graph_params p) (globals (graph_prog_params p p' graph_prog))) [cases daemon (*???*)] #graph_fun
+
+ cases (linearise_code_spec … p' graph_prog graph_fun
+         (joint_if_entry … graph_fun))      
+ * #lin_code_closed #sigma_entry_is_zero #sigma_spec
+ lapply (sigma_spec
+         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … st1)))
+ -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … wf_st1) |2: skip ]
+ -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec whd in sigma_spec;
+ inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
+ * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved
+ #related_lin_stm_graph_stm
+ inversion (stmt_implicit_label ???)
+ [ whd in match (opt_All ???); #stmt_implicit_spec #_
+   letin st2_opt' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) …
                (ev_genv (lin_prog_params p p' lin_prog))
                (linearise_status_fun … sigma st1 wf_st1))
- whd in st2';
- whd in match (fetch_statement ?????) in st2';
- >fetch_function_sigma_commute in st2';
- whd in match (fetch_function ????) in st2';
- XXX
- check fetch_statement
- CSC
- %{}
-
-whd in classified_st1_cl;
-whd in classified_st1_cl:(??%?);
-inversion (fetch_statement ?????) in classified_st1_cl;
-
-<classified_st1_cl -cl 
-whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ] ?);
-inversion (fetch_statement ?????)
-
-inversion (fetch_statement ?????)
-qed.
+   check st2_opt'
+   cut (∃st2': lin_abstract_status p p' lin_prog. st2_opt' = return st2')
+   [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec'
+   normalize nodelta in st2_spec'; -st2_opt'
+   %{st2'} %{(taaf_step … (taa_base …) …)}
+   [ cases daemon (* TODO, together with the previous one? *)
+   | @st2_spec' ]
+   %[%] [%]
+   [ whd
+     whd in st2_spec':(??%?); >fetch_statement_sigma_commute in st2_spec';
+     whd in move_st1_st1':(??%?);
+     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〉)
+     [ cases daemon (* TODO once and for all, consequence of graph_lookup_ok *) ]
+     #fetch_statement_ok >fetch_statement_ok in move_st1_st1';
+     whd in ⊢ (??%? → ??%? → ?); normalize nodelta
+     inversion graph_stmt in stmt_implicit_spec; normalize nodelta
+     [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ]
+     XXXXXXXXXX siamo qua, caso GOTO e RETURN
+   | cases daemon (* TODO, after the definition of label_rel, trivial *) ]
+   ]
+ | ....
+qed.