 Timestamp:
 Mar 6, 2013, 2:35:39 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/linearise.ma
r2712 r2784 4 4 5 5 definition graph_to_lin_statement : 6 ∀p : uns erialized_params.∀globals.6 ∀p : uns_params.∀globals. 7 7 ∀A.identifier_map LabelTag A → 8 8 joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝ … … 22 22 (* 23 23 lemma graph_to_lin_labels : 24 ∀p : uns erialized_params.∀globals,s.24 ∀p : uns_params.∀globals,s. 25 25 stmt_labels … (graph_to_lin_statement p globals s) = 26 26 stmt_explicit_labels … s. … … 119 119 120 120 let rec graph_visit 121 (p : uns erialized_params)121 (p : uns_params) 122 122 (globals: list ident) 123 123 (g : codeT (mk_graph_params p) globals) … … 629 629 630 630 definition good_local_sigma : 631 ∀p:uns erialized_params.631 ∀p:uns_params. 632 632 ∀globals. 633 633 ∀g:codeT (mk_graph_params p) globals. … … 658 658 659 659 definition linearise_code: 660 ∀p : uns erialized_params.∀globals.660 ∀p : uns_params.∀globals. 661 661 ∀g : codeT (mk_graph_params p) globals.code_closed … g → 662 662 ∀entry : (Σl.bool_to_Prop (code_has_label … g l)) … … 813 813 814 814 definition linearise_int_fun : 815 ∀p : uns erialized_params.815 ∀p : uns_params. 816 816 ∀globals. 817 817 ∀fn_in : joint_closed_internal_function (mk_graph_params p) globals … … 863 863  @(proj2 ?? (pi2 ?? code_sigma)) 864 864  cases daemon 865  (* We need to add this to graph_visit_ret_type as an invariant. 866 To prove the invariant at each step in graph_visit we will exploit 867 (regs_are_in_univers … (pi2 … f_sig)) 868 More generally, to close all the daemons here we need to strengthen 869 the invariant of graph_visit_ret_type so that the partial code 870 emitted is also good_if at each step *) 871 cases daemon 865 872 ] 866 873 ] 867 874 qed. 868 875 869 definition linearise : ∀p : uns erialized_params.876 definition linearise : ∀p : uns_params. 870 877 program (joint_function (mk_graph_params p)) ℕ → 871 878 program (joint_function (mk_lin_params p)) ℕ … … 876 883 (* 877 884 definition good_sigma : 878 ∀p:uns erialized_params.885 ∀p:uns_params. 879 886 ∀prog_in : joint_program (mk_graph_params p). 880 887 ((Σi.is_internal_function_of_program … prog_in i) → label → option ℕ) → Prop ≝
Note: See TracChangeset
for help on using the changeset viewer.