Changeset 400 for C-semantics/Cexec.ma


Ignore:
Timestamp:
Dec 11, 2010, 4:16:00 PM (9 years ago)
Author:
campbell
Message:

Minor changes for the new version of matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Cexec.ma

    r399 r400  
    378378nlet rec type_eq_dec (t1,t2:type) : (t1 = t2) + (t1 ≠ t2) ≝
    379379match t1 return λt'. (t' = t2) + (t' ≠ t2) with
    380 [ Tvoid ⇒ match t2 return λt'. (? = t') + (? ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    381 | Tint sz sg ⇒ match t2 return λt'. (? = t') + (? ≠ t')  with [ Tint sz' sg' ⇒
     380[ Tvoid ⇒ match t2 return λt'. (Tvoid = t') + (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     381| Tint sz sg ⇒ match t2 return λt'. (Tint ?? = t') + (Tint ?? ≠ t')  with [ Tint sz' sg' ⇒
    382382    match sz_eq_dec sz sz' with [ inl e1 ⇒
    383383    match sg_eq_dec sg sg' with [ inl e2 ⇒ inl ???
     
    385385    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    386386    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    387 | Tfloat f ⇒ match t2 return λt'. (? = t') + (? ≠ t')  with [ Tfloat f' ⇒
     387| Tfloat f ⇒ match t2 return λt'. (Tfloat ? = t') + (Tfloat ? ≠ t')  with [ Tfloat f' ⇒
    388388    match fs_eq_dec f f' with [ inl e1 ⇒ inl ???
    389389    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    390390    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    391 | Tpointer s t ⇒ match t2 return λt'. (? = t') + (? ≠ t')  with [ Tpointer s' t' ⇒
     391| Tpointer s t ⇒ match t2 return λt'. (Tpointer ?? = t') + (Tpointer ?? ≠ t')  with [ Tpointer s' t' ⇒
    392392    match ms_eq_dec s s' with [ inl e1 ⇒
    393393      match type_eq_dec t t' with [ inl e2 ⇒ inl ???
    394394      | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]
    395395    | inr e1 ⇒ inr ?? (nmk ? (λH.match e1 with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    396 | Tarray s t n ⇒ match t2 return λt'. (? = t') + (? ≠ t')  with [ Tarray s' t' n' ⇒
     396| Tarray s t n ⇒ match t2 return λt'. (Tarray ??? = t') + (Tarray ??? ≠ t')  with [ Tarray s' t' n' ⇒
    397397    match ms_eq_dec s s' with [ inl e1 ⇒
    398398      match type_eq_dec t t' with [ inl e2 ⇒
     
    402402        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    403403        | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    404 | Tfunction tl t ⇒ match t2 return λt'. (? = t') + (? ≠ t')  with [ Tfunction tl' t' ⇒
     404| Tfunction tl t ⇒ match t2 return λt'. (Tfunction ?? = t') + (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
    405405    match typelist_eq_dec tl tl' with [ inl e1 ⇒
    406406    match type_eq_dec t t' with [ inl e2 ⇒ inl ???
     
    409409  | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    410410| Tstruct i fl ⇒
    411     match t2 return λt'. (? = t') + (? ≠ t')  with [ Tstruct i' fl' ⇒
     411    match t2 return λt'. (Tstruct ?? = t') + (Tstruct ?? ≠ t')  with [ Tstruct i' fl' ⇒
    412412    match ident_eq i i' with [ inl e1 ⇒
    413413    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
     
    416416    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    417417| Tunion i fl ⇒
    418     match t2 return λt'. (? = t') + (? ≠ t')  with [ Tunion i' fl' ⇒
     418    match t2 return λt'. (Tunion ?? = t') + (Tunion ?? ≠ t')  with [ Tunion i' fl' ⇒
    419419    match ident_eq i i' with [ inl e1 ⇒
    420420    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
     
    422422    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    423423    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
    424 | Tcomp_ptr i ⇒ match t2 return λt'. (? = t') + (? ≠ t')  with [ Tcomp_ptr i' ⇒
     424| Tcomp_ptr i ⇒ match t2 return λt'. (Tcomp_ptr ? = t') + (Tcomp_ptr ? ≠ t')  with [ Tcomp_ptr i' ⇒
    425425    match ident_eq i i' with [ inl e1 ⇒ inl ???
    426426    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     
    429429and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝
    430430match tl1 return λtl'. (tl' = tl2) + (tl' ≠ tl2) with
    431 [ Tnil ⇒ match tl2 return λtl'. (? = tl') + (? ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    432 | Tcons t1 ts1 ⇒ match tl2 return λtl'. (? = tl') + (? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
     431[ Tnil ⇒ match tl2 return λtl'. (Tnil = tl') + (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     432| Tcons t1 ts1 ⇒ match tl2 return λtl'. (Tcons ?? = tl') + (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
    433433    match type_eq_dec t1 t2 with [ inl e1 ⇒
    434434    match typelist_eq_dec ts1 ts2 with [ inl e2 ⇒ inl ???
     
    438438and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝
    439439match fl1 return λfl'. (fl' = fl2) + (fl' ≠ fl2) with
    440 [ Fnil ⇒ match fl2 return λfl'. (? = fl') + (? ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    441 | Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. (? = fl') + (? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
     440[ Fnil ⇒ match fl2 return λfl'. (Fnil = fl') + (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     441| Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. (Fcons ??? = fl') + (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
    442442    match ident_eq i1 i2 with [ inl e1 ⇒
    443443      match type_eq_dec t1 t2 with [ inl e2 ⇒
Note: See TracChangeset for help on using the changeset viewer.