Changeset 1559 for src/RTLabs
- Timestamp:
- Nov 24, 2011, 6:49:51 PM (9 years ago)
- Location:
- src/RTLabs
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/Traces.ma
r1552 r1559 42 42 inversion H try #a try #b try #c try #d try #e try #f destruct 43 43 qed. 44 45 (* Before attempting to construct a structured trace, let's show that we can 46 form flat traces with evidence that they were constructed from an execution. 47 48 For now we don't consider I/O. *) 49 50 51 coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝ 52 | noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c) 53 | noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e) 54 | noio_wrong : ∀m. exec_no_io o i (e_wrong … m). 55 56 (* add I/O? *) 57 coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝ 58 | ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s 59 | ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s 60 | ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s. 61 62 let corec make_flat_trace ge s 63 (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) : 64 flat_trace io_out io_in ge s ≝ 65 let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in 66 match e return λx. e = x → ? with 67 [ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?) 68 | e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?) 69 | e_wrong m ⇒ λE. ft_wrong … s m ? 70 | e_interact o f ⇒ λE. ⊥ 71 ] (refl ? e). 72 [ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E; 73 cases (eval_statement ge s) 74 [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct 75 | 2,5: * #tr #s1 whd in ⊢ (??%? → ?); 76 >(?:is_final ????? = RTLabs_is_final s1) // 77 lapply (refl ? (RTLabs_is_final s1)) 78 cases (RTLabs_is_final s1) in ⊢ (???% → %); 79 [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct 80 | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl 81 | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct 82 ] 83 | *: #m whd in ⊢ (??%? → ?); #E destruct 84 ] 85 | whd in E:(??%?); >exec_inf_aux_unfold in E; 86 cases (eval_statement ge s) 87 [ #O #K whd in ⊢ (??%? → ?); #E destruct 88 | * #tr #s1 whd in ⊢ (??%? → ?); 89 cases (is_final ?????) 90 [ whd in ⊢ (??%? → ?); #E destruct @refl 91 | #i whd in ⊢ (??%? → ?); #E destruct 92 ] 93 | #m whd in ⊢ (??%? → ?); #E destruct 94 ] 95 | whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E; 96 cases (eval_statement ge s) 97 [ #O #K whd in ⊢ (??%? → ?); #E destruct 98 | * #tr #s1 whd in ⊢ (??%? → ?); 99 cases (is_final ?????) 100 [ whd in ⊢ (??%? → ?); #E 101 change with (eval_statement ge s1) in E:(??(??????(?????%))?); 102 destruct 103 inversion H 104 [ #a #b #c #E1 destruct 105 | #trx #sx #ex #H1 #E2 #E3 destruct @H1 106 | #m #E1 destruct 107 ] 108 | #i whd in ⊢ (??%? → ?); #E destruct 109 ] 110 | #m whd in ⊢ (??%? → ?); #E destruct 111 ] 112 | whd in E:(??%?); >exec_inf_aux_unfold in E; 113 cases (eval_statement ge s) 114 [ #O #K whd in ⊢ (??%? → ?); #E destruct 115 | * #tr1 #s1 whd in ⊢ (??%? → ?); 116 cases (is_final ?????) 117 [ whd in ⊢ (??%? → ?); #E destruct 118 | #i whd in ⊢ (??%? → ?); #E destruct 119 ] 120 | #m whd in ⊢ (??%? → ?); #E destruct @refl 121 ] 122 | whd in E:(??%?); >E in H; #H 123 inversion H 124 [ #a #b #c #E destruct 125 | #a #b #c #d #E1 destruct 126 | #m #E1 destruct 127 ] 128 ] qed. 129 130 let corec make_whole_flat_trace p s 131 (H:exec_no_io … (exec_inf … RTLabs_fullexec p)) 132 (I:make_initial_state ??? p = OK ? s) : 133 flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝ 134 let ge ≝ make_global … p in 135 let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in 136 match e return λx. e = x → ? with 137 [ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ? 138 | e_step _ _ e' ⇒ λE. make_flat_trace ge s ? 139 | e_wrong m ⇒ λE. ⊥ 140 | e_interact o f ⇒ λE. ⊥ 141 ] (refl ? e). 142 [ whd in E:(??%?); >exec_inf_aux_unfold in E; 143 whd in ⊢ (??%? → ?); 144 >(?:is_final ????? = RTLabs_is_final s) // 145 lapply (refl ? (RTLabs_is_final s)) 146 cases (RTLabs_is_final s) in ⊢ (???% → %); 147 [ #_ whd in ⊢ (??%? → ?); #E destruct 148 | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct 149 ] 150 | whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?); 151 >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????) 152 [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H 153 [ #a #b #c #E1 destruct 154 | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1) 155 @H1 156 | #m #E1 destruct 157 ] 158 | #i whd in ⊢ (??%? → ???% → ?); #E destruct 159 ] 160 | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); 161 cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct 162 | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); 163 cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct 164 ] qed. 165 -
src/RTLabs/semantics.ma
r1535 r1559 197 197 ] qed. 198 198 199 definition is_final : state → option int ≝199 definition RTLabs_is_final : state → option int ≝ 200 200 λs. match s with 201 201 [ State _ _ _ ⇒ None ? … … 212 212 213 213 definition RTLabs_exec : trans_system io_out io_in ≝ 214 mk_trans_system … ? (λ_. is_final) eval_statement.214 mk_trans_system … ? (λ_.RTLabs_is_final) eval_statement. 215 215 216 216 definition make_global : RTLabs_program → genv ≝
Note: See TracChangeset
for help on using the changeset viewer.