Changeset 880 for src/Clight/Cexec.ma
- Timestamp:
- Jun 3, 2011, 5:35:31 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Cexec.ma
r797 r880 5 5 include "common/SmallstepExec.ma". 6 6 include "Clight/Csem.ma". 7 include "Clight/TypeComparison.ma". 7 8 8 9 (* … … 43 44 λA,P,a. match a with [ Error _ ⇒ True | OK v ⇒ P v ]. 44 45 45 axiom TypeMismatch : String.46 46 axiom ValueIsNotABoolean : String. 47 47 … … 333 333 ] 334 334 ] ]. 335 336 definition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).337 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.338 definition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).339 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.340 definition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).341 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.342 343 definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m).344 #n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E345 [ %1 | %2 ] @(eqb_elim … E) // #_ #H destruct qed.346 347 let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝348 match t1 return λt'. (t' = t2) + (t' ≠ t2) with349 [ Tvoid ⇒ match t2 return λt'. (Tvoid = t') + (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]350 | Tint sz sg ⇒ match t2 return λt'. (Tint ?? = t') + (Tint ?? ≠ t') with [ Tint sz' sg' ⇒351 match sz_eq_dec sz sz' with [ inl e1 ⇒352 match sg_eq_dec sg sg' with [ inl e2 ⇒ inl ???353 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]354 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]355 | _ ⇒ inr ?? (nmk ? (λH.?)) ]356 | Tfloat f ⇒ match t2 return λt'. (Tfloat ? = t') + (Tfloat ? ≠ t') with [ Tfloat f' ⇒357 match fs_eq_dec f f' with [ inl e1 ⇒ inl ???358 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]359 | _ ⇒ inr ?? (nmk ? (λH.?)) ]360 | Tpointer s t ⇒ match t2 return λt'. (Tpointer ?? = t') + (Tpointer ?? ≠ t') with [ Tpointer s' t' ⇒361 match eq_region_dec s s' with [ inl e1 ⇒362 match type_eq_dec t t' with [ inl e2 ⇒ inl ???363 | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]364 | inr e1 ⇒ inr ?? (nmk ? (λH.match e1 with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ]365 | Tarray s t n ⇒ match t2 return λt'. (Tarray ??? = t') + (Tarray ??? ≠ t') with [ Tarray s' t' n' ⇒366 match eq_region_dec s s' with [ inl e1 ⇒367 match type_eq_dec t t' with [ inl e2 ⇒368 match eq_nat_dec n n' with [ inl e3 ⇒ inl ???369 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]370 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]371 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]372 | _ ⇒ inr ?? (nmk ? (λH.?)) ]373 | Tfunction tl t ⇒ match t2 return λt'. (Tfunction ?? = t') + (Tfunction ?? ≠ t') with [ Tfunction tl' t' ⇒374 match typelist_eq_dec tl tl' with [ inl e1 ⇒375 match type_eq_dec t t' with [ inl e2 ⇒ inl ???376 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]377 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]378 | _ ⇒ inr ?? (nmk ? (λH.?)) ]379 | Tstruct i fl ⇒380 match t2 return λt'. (Tstruct ?? = t') + (Tstruct ?? ≠ t') with [ Tstruct i' fl' ⇒381 match ident_eq i i' with [ inl e1 ⇒382 match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???383 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]384 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]385 | _ ⇒ inr ?? (nmk ? (λH.?)) ]386 | Tunion i fl ⇒387 match t2 return λt'. (Tunion ?? = t') + (Tunion ?? ≠ t') with [ Tunion i' fl' ⇒388 match ident_eq i i' with [ inl e1 ⇒389 match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???390 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]391 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]392 | _ ⇒ inr ?? (nmk ? (λH.?)) ]393 | Tcomp_ptr r i ⇒ match t2 return λt'. (Tcomp_ptr ? ? = t') + (Tcomp_ptr ? ? ≠ t') with [ Tcomp_ptr r' i' ⇒394 match eq_region_dec r r' with [ inl e1 ⇒395 match ident_eq i i' with [ inl e2 ⇒ inl ???396 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]397 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]398 | _ ⇒ inr ?? (nmk ? (λH.?)) ]399 ]400 and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝401 match tl1 return λtl'. (tl' = tl2) + (tl' ≠ tl2) with402 [ Tnil ⇒ match tl2 return λtl'. (Tnil = tl') + (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]403 | Tcons t1 ts1 ⇒ match tl2 return λtl'. (Tcons ?? = tl') + (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒404 match type_eq_dec t1 t2 with [ inl e1 ⇒405 match typelist_eq_dec ts1 ts2 with [ inl e2 ⇒ inl ???406 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]407 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]408 ]409 and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝410 match fl1 return λfl'. (fl' = fl2) + (fl' ≠ fl2) with411 [ Fnil ⇒ match fl2 return λfl'. (Fnil = fl') + (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]412 | Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. (Fcons ??? = fl') + (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒413 match ident_eq i1 i2 with [ inl e1 ⇒414 match type_eq_dec t1 t2 with [ inl e2 ⇒415 match fieldlist_eq_dec fs1 fs2 with [ inl e3 ⇒ inl ???416 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]417 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]418 | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]419 ]. destruct; //; qed.420 421 definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝422 λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? (msg TypeMismatch)].423 335 424 336 let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
Note: See TracChangeset
for help on using the changeset viewer.