| 1 | include "LIN/joint_LTL_LIN.ma". |
|---|
| 2 | |
|---|
| 3 | definition LTL ≝ mk_graph_params LTL_LIN. |
|---|
| 4 | |
|---|
| 5 | (* aid unification *) |
|---|
| 6 | unification hint 0 ≔ |
|---|
| 7 | (*---------------*) ⊢ |
|---|
| 8 | acc_a_reg LTL ≡ unit. |
|---|
| 9 | unification hint 0 ≔ |
|---|
| 10 | (*---------------*) ⊢ |
|---|
| 11 | acc_a_arg LTL ≡ unit. |
|---|
| 12 | unification hint 0 ≔ |
|---|
| 13 | (*---------------*) ⊢ |
|---|
| 14 | acc_b_reg LTL ≡ unit. |
|---|
| 15 | unification hint 0 ≔ |
|---|
| 16 | (*---------------*) ⊢ |
|---|
| 17 | acc_a_arg LTL ≡ unit. |
|---|
| 18 | unification hint 0 ≔ |
|---|
| 19 | (*---------------*) ⊢ |
|---|
| 20 | snd_arg LTL ≡ hdw_argument. |
|---|
| 21 | unification hint 0 ≔ |
|---|
| 22 | (*---------------*) ⊢ |
|---|
| 23 | ext_seq LTL ≡ ltl_lin_seq. |
|---|
| 24 | unification hint 0 ≔ |
|---|
| 25 | (*---------------*) ⊢ |
|---|
| 26 | pair_move LTL ≡ registers_move. |
|---|
| 27 | |
|---|
| 28 | definition ltl_program ≝ joint_program LTL. |
|---|
| 29 | unification hint 0 ≔ ⊢ ltl_program ≡ joint_program LTL. |
|---|
| 30 | |
|---|
| 31 | coercion byte_to_ltl_argument : ∀b: Byte.snd_arg LTL ≝ |
|---|
| 32 | hdw_argument_from_byte on _b : Byte to snd_arg LTL. |
|---|
| 33 | coercion reg_to_ltl_argument : ∀r: Register.snd_arg LTL ≝ |
|---|
| 34 | hdw_argument_from_reg on _r : Register to snd_arg LTL. |
|---|
| 35 | |
|---|
| 36 | definition LTL_premain : ∀p : ltl_program. |
|---|
| 37 | joint_closed_internal_function LTL (prog_names … p) ≝ |
|---|
| 38 | λp. |
|---|
| 39 | let l1 : label ≝ an_identifier … one in |
|---|
| 40 | let l2 : label ≝ an_identifier … (p0 one) in |
|---|
| 41 | let l3 : label ≝ an_identifier … (p1 one) in |
|---|
| 42 | let res ≝ |
|---|
| 43 | mk_joint_internal_function LTL (prog_names … p) |
|---|
| 44 | (mk_universe … (p0 (p0 one))) |
|---|
| 45 | (mk_universe … one) |
|---|
| 46 | it it 0 0 (empty_map …) l1 in |
|---|
| 47 | (* todo: args for main? *) |
|---|
| 48 | let res ≝ add_graph … l1 |
|---|
| 49 | (sequential … (COST_LABEL … (init_cost_label … p)) l2) |
|---|
| 50 | res in |
|---|
| 51 | let res ≝ add_graph … l2 |
|---|
| 52 | (sequential … (CALL LTL ? (inl … (prog_main … p)) 0 it) l3) |
|---|
| 53 | res in |
|---|
| 54 | let res ≝ add_graph … l3 |
|---|
| 55 | (GOTO ? l3) |
|---|
| 56 | res in |
|---|
| 57 | res. |
|---|
| 58 | % |
|---|
| 59 | [ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct |
|---|
| 60 | % |
|---|
| 61 | [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct |
|---|
| 62 | |2: % |
|---|
| 63 | |4,6: % whd in ⊢ (??%%→?); #EQ destruct |
|---|
| 64 | ] |
|---|
| 65 | | ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I} |
|---|
| 66 | | ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); // |
|---|
| 67 | | ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I |
|---|
| 68 | | %{l2} %{(init_cost_label … p)} % |
|---|
| 69 | ] |
|---|
| 70 | qed. |
|---|
