 Timestamp:
 Oct 6, 2011, 5:27:32 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1307 r1308 127 127 λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl. 128 128 129 axiom split_into_bytes: 130 ∀size. 131 ∀int: bvint size. 132 Σbytes: list Byte. bytes = size_intsize size. 133 134 lemma eqb_implies_eq: 135 ∀m, n: nat. 136 eqb m n = true → m = n. 137 #M 138 elim M 139 [1: #N normalize 140 cases N 141 [1: normalize // 142 2: #M' normalize #HYP destruct(HYP) 143 ] 144 2: #M' #IND_HYP #N 145 normalize 146 cases N 147 [1: normalize #HYP destruct(HYP) 148 2: #M'' normalize #HYP 149 @eq_f @(IND_HYP M'') 150 assumption 151 ] 152 ] 153 qed. 154 129 155 let rec translate_cst 130 156 (globals: list ident) (cst: constant) (destrs: list register) … … 134 160 [ Ointconst size const ⇒ 135 161 match destrs with 136 [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def 137  cons hd tl ⇒ ? 162 [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def 163  _ ⇒ 164 let size' ≝ size_intsize size in 165 match eqb size' (destrs) return λx. (eqb size' (destrs)) = x → rtl_internal_function globals with 166 [ true ⇒ λgood_case. 167 match split_into_bytes size const with 168 [ dp bytes bytes_length_proof ⇒ 169 let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in 170 adds_graph rtl_params1 globals mapped start_lbl dest_lbl def 171 ] 172  false ⇒ λbad_case. ? 173 ] (refl … (eqb size' (destrs))) 138 174 ] 139 175  Ofloatconst float ⇒ ⊥ 140  Oaddrsymbol id offset ⇒ ? 141  Oaddrstack offset ⇒ ? 142 ]. 143 [5: cases not_implemented (* XXX: float, error_float in o'caml *) 176  Oaddrsymbol id offset ⇒ 177 let 〈r1, r2〉 ≝ make_addr … destrs ? in 178 add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def 179  Oaddrstack offset ⇒ 180 let 〈r1, r2〉 ≝ make_addr … destrs ? in 181 add_graph rtl_params1 globals start_lbl (sequential … (STACK_ADDRESS rtl_params_ globals r1 r2) dest_lbl) def 182 ]. 183 [1: >bytes_length_proof 184 cut(size' = destrs) 185 [1: @eqb_implies_eq 186 assumption 187 2: #EQ_HYP 188 <EQ_HYP % 189 ] 190 5: cases not_implemented (* XXX: float, error_float in o'caml *) 144 191 ]. 145 192
Note: See TracChangeset
for help on using the changeset viewer.