Changeset 387


Ignore:
Timestamp:
Dec 7, 2010, 7:06:16 PM (9 years ago)
Author:
campbell
Message:

Sort out equality checking of types.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r386 r387  
    718718#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    719719
    720 nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝
    721 match t1 with
    722 [ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy | _ ⇒ dn ]
    723 | Tint sz sg ⇒ match t2 with [ Tint sz' sg' ⇒ match sz_eq_dec sz sz' with [ inl _ ⇒ match sg_eq_dec sg sg' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
    724 | Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
    725 | Tpointer s t ⇒ match t2 with [ Tpointer s' t' ⇒
    726     match ms_eq_dec s s' with [ inl _ ⇒
    727       match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
    728 | Tarray s t n ⇒ match t2 with [ Tarray s' t' n' ⇒
    729     match ms_eq_dec s s' with [ inl _ ⇒
    730       match assert_type_eq t t' with [ OK _ ⇒
    731         match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
    732 | Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒
    733     match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
     720nlet rec type_eq_dec (t1,t2:type) : (t1 = t2) + (t1 ≠ t2) ≝
     721match t1 return λt'. (t' = t2) + (t' ≠ t2) with
     722[ Tvoid ⇒ match t2 return λt'. (? = t') + (? ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     723| Tint sz sg ⇒ match t2 return λt'. (? = t') + (? ≠ t')  with [ Tint sz' sg' ⇒
     724    match sz_eq_dec sz sz' with [ inl e1 ⇒
     725    match sg_eq_dec sg sg' with [ inl e2 ⇒ inl ???
     726    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     727    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     728    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     729| Tfloat f ⇒ match t2 return λt'. (? = t') + (? ≠ t')  with [ Tfloat f' ⇒
     730    match fs_eq_dec f f' with [ inl e1 ⇒ inl ???
     731    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     732    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     733| Tpointer s t ⇒ match t2 return λt'. (? = t') + (? ≠ t')  with [ Tpointer s' t' ⇒
     734    match ms_eq_dec s s' with [ inl e1 ⇒
     735      match type_eq_dec t t' with [ inl e2 ⇒ inl ???
     736      | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]
     737    | inr e1 ⇒ inr ?? (nmk ? (λH.match e1 with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     738| Tarray s t n ⇒ match t2 return λt'. (? = t') + (? ≠ t')  with [ Tarray s' t' n' ⇒
     739    match ms_eq_dec s s' with [ inl e1 ⇒
     740      match type_eq_dec t t' with [ inl e2 ⇒
     741        match decidable_eq_Z_Type n n' with [ inl e3 ⇒ inl ???
     742        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     743        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     744        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     745        | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     746| Tfunction tl t ⇒ match t2 return λt'. (? = t') + (? ≠ t')  with [ Tfunction tl' t' ⇒
     747    match typelist_eq_dec tl tl' with [ inl e1 ⇒
     748    match type_eq_dec t t' with [ inl e2 ⇒ inl ???
     749    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     750    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     751  | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    734752| Tstruct i fl ⇒
    735     match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
    736       match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
     753    match t2 return λt'. (? = t') + (? ≠ t')  with [ Tstruct i' fl' ⇒
     754    match ident_eq i i' with [ inl e1 ⇒
     755    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
     756    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     757    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     758    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    737759| Tunion i fl ⇒
    738     match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
    739       match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] |  _ ⇒ dn ]
    740 | Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
     760    match t2 return λt'. (? = t') + (? ≠ t')  with [ Tunion i' fl' ⇒
     761    match ident_eq i i' with [ inl e1 ⇒
     762    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
     763    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     764    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     765    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
     766| Tcomp_ptr i ⇒ match t2 return λt'. (? = t') + (? ≠ t')  with [ Tcomp_ptr i' ⇒
     767    match ident_eq i i' with [ inl e1 ⇒ inl ???
     768    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     769    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    741770]
    742 and assert_typelist_eq (tl1,tl2:typelist) : res (tl1 = tl2) ≝
    743 match tl1 with
    744 [ Tnil ⇒ match tl2 with [ Tnil ⇒ dy | _ ⇒ dn ]
    745 | Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn | Tcons t2 ts2 ⇒
    746     match assert_type_eq t1 t2 with [ OK _ ⇒
    747       match assert_typelist_eq ts1 ts2 with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ]
     771and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝
     772match tl1 return λtl'. (tl' = tl2) + (tl' ≠ tl2) with
     773[ Tnil ⇒ match tl2 return λtl'. (? = tl') + (? ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     774| Tcons t1 ts1 ⇒ match tl2 return λtl'. (? = tl') + (? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
     775    match type_eq_dec t1 t2 with [ inl e1 ⇒
     776    match typelist_eq_dec ts1 ts2 with [ inl e2 ⇒ inl ???
     777    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     778    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
    748779]
    749 and assert_fieldlist_eq (fl1,fl2:fieldlist) : res (fl1 = fl2) ≝
    750 match fl1 with
    751 [ Fnil ⇒ match fl2 with [ Fnil ⇒ dy | _ ⇒ dn ]
    752 | Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn | Fcons i2 t2 fs2 ⇒
    753     match ident_eq i1 i2 with [ inl _ ⇒
    754       match assert_type_eq t1 t2 with [ OK _ ⇒
    755         match assert_fieldlist_eq fs1 fs2 with [ OK _ ⇒ dy | _ ⇒ dn ]
    756         | _ ⇒ dn ] | _ ⇒ dn ] ]
    757 ].
    758 (* A poor man's clear, otherwise automation picks up recursive calls without
    759    checking that the argument is smaller. *)
    760 ngeneralize in assert_type_eq;
    761 ngeneralize in assert_typelist_eq;
    762 ngeneralize in assert_fieldlist_eq; #avoid1; #_; #avoid2; #_; #avoid3; #_; nwhd; //;
    763 (* XXX: I have no idea why the first // didn't catch these. *)
    764 //; //; //; //; //; //; //; //; //;
    765 nqed.
     780and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝
     781match fl1 return λfl'. (fl' = fl2) + (fl' ≠ fl2) with
     782[ Fnil ⇒ match fl2 return λfl'. (? = fl') + (? ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     783| Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. (? = fl') + (? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
     784    match ident_eq i1 i2 with [ inl e1 ⇒
     785      match type_eq_dec t1 t2 with [ inl e2 ⇒
     786        match fieldlist_eq_dec fs1 fs2 with [ inl e3 ⇒ inl ???
     787        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     788        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     789        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
     790]. ndestruct; //; nqed.
     791
     792ndefinition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
     793λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? ].
    766794
    767795nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
  • C-semantics/CexecIOcomplete.ma

    r386 r387  
    319319  ].
    320320
    321 naxiom assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p.
    322 (*nlemma assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p.
    323 #t; napply (type_ind2l ? (λtl. ∃p.assert_typelist_eq tl tl = OK ? p) … t);
    324 ##[ @ (refl ??); // ##| #sz si; ncases sz; ncases si; @ (refl ??); //;
    325 ##| #sz; ncases sz; @ ?; //;
    326 ##| #sp ty IH; ncases sp; nwhd in ⊢ (??(λ_.??%?)); nelim IH; #p IH; nrewrite > IH; @ ?; //;
    327 ##| #sp ty n IH; ncases sp; nwhd in ⊢ (??(λ_.??%?)); nelim IH; #p IH; nrewrite > IH;
    328     nwhd in ⊢ (??(λ_.??%?)); ncases (decidable_eq_Z_Type n n);
    329     ##[ ##1,3,5,7,9,11: #H; nwhd in ⊢ (??(λ_.??%?)); @ ?; //;
    330     ##| ##*: #H; napply False_ind; /2/;
    331     ##]
    332 ##| #tys ty IH1 IH2; @ ?;
    333     ##[ ##2: nwhd in ⊢ (??%?); nelim IH1; #p1 e1;
    334     nrewrite > e1; nwhd in ⊢ (??%?);
    335     nelim IH2;
    336     *)
     321nlemma assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p.
     322#t; nwhd in ⊢ (??(λ_.??%?)); ncases (type_eq_dec t t); #E;
     323##[ @ E; //
     324##| napply False_ind; napply (absurd ?? E); //
     325##] nqed.
    337326
    338327nlemma is_not_void_true: ∀f. ¬fn_return f = Tvoid → ∃p. is_not_void (fn_return f) = OK ? p.
Note: See TracChangeset for help on using the changeset viewer.