include "Clight/Csyntax.ma". axiom TypeMismatch : String. definition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2). #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed. definition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2). #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed. definition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2). #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed. definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m). #n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E [ %1 | %2 ] lapply E @eqb_elim // #_ #H destruct qed. let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝ match t1 return λt'. Sum (t' = t2) (t' ≠ t2) with [ Tvoid ⇒ match t2 return λt'. Sum (Tvoid = t') (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ] | Tint sz sg ⇒ match t2 return λt'. Sum (Tint ?? = t') (Tint ?? ≠ t') with [ Tint sz' sg' ⇒ match sz_eq_dec sz sz' with [ inl e1 ⇒ match sg_eq_dec sg sg' with [ inl e2 ⇒ inl ??? | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ] | Tfloat f ⇒ match t2 return λt'. Sum (Tfloat ? = t') (Tfloat ? ≠ t') with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl e1 ⇒ inl ??? | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ] | Tpointer s t ⇒ match t2 return λt'. Sum (Tpointer ?? = t') (Tpointer ?? ≠ t') with [ Tpointer s' t' ⇒ match eq_region_dec s s' with [ inl e1 ⇒ match type_eq_dec t t' with [ inl e2 ⇒ inl ??? | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ] | inr e1 ⇒ inr ?? (nmk ? (λH.match e1 with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ] | Tarray s t n ⇒ match t2 return λt'. Sum (Tarray ??? = t') (Tarray ??? ≠ t') with [ Tarray s' t' n' ⇒ match eq_region_dec s s' with [ inl e1 ⇒ match type_eq_dec t t' with [ inl e2 ⇒ match eq_nat_dec n n' with [ inl e3 ⇒ inl ??? | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ] | Tfunction tl t ⇒ match t2 return λt'. Sum (Tfunction ?? = t') (Tfunction ?? ≠ t') with [ Tfunction tl' t' ⇒ match typelist_eq_dec tl tl' with [ inl e1 ⇒ match type_eq_dec t t' with [ inl e2 ⇒ inl ??? | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ] | Tstruct i fl ⇒ match t2 return λt'. Sum (Tstruct ?? = t') (Tstruct ?? ≠ t') with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl e1 ⇒ match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ??? | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ] | Tunion i fl ⇒ match t2 return λt'. Sum (Tunion ?? = t') (Tunion ?? ≠ t') with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl e1 ⇒ match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ??? | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ] | Tcomp_ptr r i ⇒ match t2 return λt'. Sum (Tcomp_ptr ? ? = t') (Tcomp_ptr ? ? ≠ t') with [ Tcomp_ptr r' i' ⇒ match eq_region_dec r r' with [ inl e1 ⇒ match ident_eq i i' with [ inl e2 ⇒ inl ??? | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ] ] and typelist_eq_dec (tl1,tl2:typelist) : Sum (tl1 = tl2) (tl1 ≠ tl2) ≝ match tl1 return λtl'. Sum (tl' = tl2) (tl' ≠ tl2) with [ Tnil ⇒ match tl2 return λtl'. Sum (Tnil = tl') (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ] | Tcons t1 ts1 ⇒ match tl2 return λtl'. Sum (Tcons ?? = tl') (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒ match type_eq_dec t1 t2 with [ inl e1 ⇒ match typelist_eq_dec ts1 ts2 with [ inl e2 ⇒ inl ??? | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ] ] and fieldlist_eq_dec (fl1,fl2:fieldlist) : Sum (fl1 = fl2) (fl1 ≠ fl2) ≝ match fl1 return λfl'. Sum (fl' = fl2) (fl' ≠ fl2) with [ Fnil ⇒ match fl2 return λfl'. Sum (Fnil = fl') (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ] | Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. Sum (Fcons ??? = fl') (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒ match ident_eq i1 i2 with [ inl e1 ⇒ match type_eq_dec t1 t2 with [ inl e2 ⇒ match fieldlist_eq_dec fs1 fs2 with [ inl e3 ⇒ inl ??? | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ] ]. try destruct; // qed. definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝ λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? (msg TypeMismatch)]. definition type_eq : type → type → bool ≝ λt1,t2. match type_eq_dec t1 t2 with [ inl _ ⇒ true | inr _ ⇒ false ].