|
Last change
on this file since 2956 was
2952,
checked in by tranquil, 7 years ago
|
- corrected all back-end premains to not pass any arguments to the main
- premain fetching is made by fetch_function in joint_semantics.ma
- reorganised some definition between Traces.ma and joint_fullexec.ma
|
|
File size:
1.6 KB
|
| Line | |
|---|
| 1 | include "LIN/joint_LTL_LIN.ma". |
|---|
| 2 | |
|---|
| 3 | definition LIN ≝ mk_lin_params LTL_LIN. |
|---|
| 4 | |
|---|
| 5 | (* aid unification *) |
|---|
| 6 | unification hint 0 ≔ |
|---|
| 7 | (*---------------*) ⊢ |
|---|
| 8 | acc_a_reg LIN ≡ unit. |
|---|
| 9 | unification hint 0 ≔ |
|---|
| 10 | (*---------------*) ⊢ |
|---|
| 11 | acc_a_arg LIN ≡ unit. |
|---|
| 12 | unification hint 0 ≔ |
|---|
| 13 | (*---------------*) ⊢ |
|---|
| 14 | acc_b_reg LIN ≡ unit. |
|---|
| 15 | unification hint 0 ≔ |
|---|
| 16 | (*---------------*) ⊢ |
|---|
| 17 | acc_a_arg LIN ≡ unit. |
|---|
| 18 | unification hint 0 ≔ |
|---|
| 19 | (*---------------*) ⊢ |
|---|
| 20 | snd_arg LIN ≡ hdw_argument. |
|---|
| 21 | unification hint 0 ≔ |
|---|
| 22 | (*---------------*) ⊢ |
|---|
| 23 | ext_seq LIN ≡ ltl_lin_seq. |
|---|
| 24 | unification hint 0 ≔ |
|---|
| 25 | (*---------------*) ⊢ |
|---|
| 26 | pair_move LIN ≡ registers_move. |
|---|
| 27 | |
|---|
| 28 | definition lin_program ≝ joint_program LIN. |
|---|
| 29 | unification hint 0 ≔ ⊢ lin_program ≡ joint_program LIN. |
|---|
| 30 | |
|---|
| 31 | definition LIN_premain : ∀p : lin_program.joint_closed_internal_function LIN (prog_var_names ?? p) ≝ |
|---|
| 32 | λp. |
|---|
| 33 | let l3 : label ≝ an_identifier … (p1 one) in |
|---|
| 34 | let code ≝ |
|---|
| 35 | [〈None ?, sequential … (COST_LABEL LIN ? (init_cost_label … p)) it〉 ; |
|---|
| 36 | 〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 0 it) it〉 ; |
|---|
| 37 | 〈Some ? l3, GOTO ? l3〉 ] in |
|---|
| 38 | mk_joint_internal_function LIN (prog_var_names … p) |
|---|
| 39 | (mk_universe … (p0 (p0 one))) |
|---|
| 40 | (mk_universe … one) |
|---|
| 41 | it it 0 0 code 0. |
|---|
| 42 | % |
|---|
| 43 | [ * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%?→?); #EQ destruct |
|---|
| 44 | % try @I |
|---|
| 45 | [ %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct |
|---|
| 46 | |*: % whd in ⊢ (??%%→?); #EQ destruct |
|---|
| 47 | ] |
|---|
| 48 | | * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I} |
|---|
| 49 | | ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); // |
|---|
| 50 | | * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%%→?); #EQ destruct @I |
|---|
| 51 | | %{it} %{(init_cost_label … p)} % |
|---|
| 52 | ] |
|---|
| 53 | qed. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
