Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/TypeComparison.ma

    r1872 r2176  
    2525    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    2626    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     27| Tpointer t ⇒ match t2 return λt'. Sum (Tpointer ? = t') (Tpointer ? ≠ t')  with [ Tpointer t' ⇒
     28      match type_eq_dec t t' with [ inl e2 ⇒ inl ???
     29      | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]
     30    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     31| Tarray t n ⇒ match t2 return λt'. Sum (Tarray ?? = t') (Tarray ?? ≠ t')  with [ Tarray t' n' ⇒
     32      match type_eq_dec t t' with [ inl e2 ⇒
     33        match eq_nat_dec n n' with [ inl e3 ⇒ inl ???
     34        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     35        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     36        | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     37(*
    2738| Tpointer s t ⇒ match t2 return λt'. Sum (Tpointer ?? = t') (Tpointer ?? ≠ t')  with [ Tpointer s' t' ⇒
    2839    match eq_region_dec s s' with [ inl e1 ⇒
     
    3849        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    3950        | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     51*)
    4052| Tfunction tl t ⇒ match t2 return λt'. Sum (Tfunction ?? = t') (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
    4153    match typelist_eq_dec tl tl' with [ inl e1 ⇒
     
    5870    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    5971    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
     72| Tcomp_ptr i ⇒ match t2 return λt'. Sum (Tcomp_ptr ? = t') (Tcomp_ptr ? ≠ t')  with [ Tcomp_ptr i' ⇒
     73      match ident_eq i i' with [ inl e2 ⇒ inl ???
     74      | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     75    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     76(*
    6077| Tcomp_ptr r i ⇒ match t2 return λt'. Sum (Tcomp_ptr ? ? = t') (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
    6178    match eq_region_dec r r' with [ inl e1 ⇒
     
    6481    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    6582    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     83*)
    6684]
    6785and typelist_eq_dec (tl1,tl2:typelist) : Sum (tl1 = tl2) (tl1 ≠ tl2) ≝
Note: See TracChangeset for help on using the changeset viewer.