Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (7 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/TypeComparison.ma

    r2176 r2468  
    99definition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
    1010#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
    11 definition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
    12 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
    1311
    1412let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
     
    1917    match sg_eq_dec sg sg' with [ inl e2 ⇒ inl ???
    2018    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    21     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    22     | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    23 | Tfloat f ⇒ match t2 return λt'. Sum (Tfloat ? = t') (Tfloat ? ≠ t')  with [ Tfloat f' ⇒
    24     match fs_eq_dec f f' with [ inl e1 ⇒ inl ???
    2519    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    2620    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
Note: See TracChangeset for help on using the changeset viewer.