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.joint_closed_internal_function LTL (prog_var_names ?? p) ≝ |
---|

37 | λp. |
---|

38 | let l1 : label ≝ an_identifier … one in |
---|

39 | let l2 : label ≝ an_identifier … (p0 one) in |
---|

40 | let l3 : label ≝ an_identifier … (p1 one) in |
---|

41 | let res ≝ |
---|

42 | mk_joint_internal_function LTL (prog_var_names … p) |
---|

43 | (mk_universe … (p0 (p0 one))) |
---|

44 | (mk_universe … one) |
---|

45 | it it 0 0 (empty_map …) l1 in |
---|

46 | (* todo: args for main? *) |
---|

47 | let res ≝ add_graph … l1 |
---|

48 | (sequential … (COST_LABEL … (init_cost_label … p)) l2) |
---|

49 | res in |
---|

50 | let res ≝ add_graph … l2 |
---|

51 | (sequential … (CALL LTL ? (inl … (prog_main … p)) 0 it) l3) |
---|

52 | res in |
---|

53 | let res ≝ add_graph … l3 |
---|

54 | (GOTO ? l3) |
---|

55 | res in |
---|

56 | res. |
---|

57 | % |
---|

58 | [ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct |
---|

59 | % |
---|

60 | [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct |
---|

61 | |2: % |
---|

62 | |4,6: % whd in ⊢ (??%%→?); #EQ destruct |
---|

63 | ] |
---|

64 | | ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I} |
---|

65 | | ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); // |
---|

66 | | ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I |
---|

67 | | %{l2} %{(init_cost_label … p)} % |
---|

68 | ] |
---|

69 | qed. |
---|