Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (8 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/ClassifyOp.ma

    r2176 r2468  
    2020     necessary casts *)
    2121  | add_case_ii: ∀sz,sg.      classify_add_cases (Tint sz sg)     (Tint sz sg)     (*Tint sz sg*)
    22   | add_case_ff: ∀sz.         classify_add_cases (Tfloat sz)      (Tfloat sz)      (*Tfloat sz*)
    2322  | add_case_pi: ∀n,ty,sz,sg. classify_add_cases (ptr_type  ty n) (Tint sz sg)     (*ptr_type r ty n*)
    2423  | add_case_ip: ∀n,sz,sg,ty. classify_add_cases (Tint sz sg)     (ptr_type  ty n) (*ptr_type r ty n*)
     
    3332    | Tarray ty n ⇒ add_case_ip (Some ? n) …
    3433    | _ ⇒ add_default … ]
    35   | Tfloat sz1 ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [ Tfloat sz2 ⇒ floatsize_eq_elim sz1 sz2 (λsz1,sz2. classify_add_cases (Tfloat sz1) (Tfloat sz2)) (add_case_ff sz1) (add_default …) | _ ⇒ add_default … ]
    3634  | Tpointer ty ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (None ?) … | _ ⇒ add_default … ]
    3735  | Tarray ty n ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (Some ? n) … | _ ⇒ add_default … ]
     
    4139inductive classify_sub_cases : type → type → Type[0] ≝
    4240  | sub_case_ii: ∀sz,sg.         classify_sub_cases (Tint sz sg)       (Tint sz sg)
    43   | sub_case_ff: ∀sz.            classify_sub_cases (Tfloat sz)        (Tfloat sz)
    4441  | sub_case_pi: ∀n,ty,sz,sg.    classify_sub_cases (ptr_type  ty n)   (Tint sz sg)
    4542  | sub_case_pp: ∀n1,n2,ty1,ty2. classify_sub_cases (ptr_type  ty1 n1) (ptr_type  ty2 n2)
     
    4946  match ty1 return λty1. classify_sub_cases ty1 ty2 with
    5047  [ Tint sz1 sg1 ⇒ if_type_eq (Tint sz1 sg1) ty2 (λty1, ty2. classify_sub_cases ty1 ty2) (sub_case_ii sz1 sg1) (sub_default …)
    51   | Tfloat sz1 ⇒ if_type_eq (Tfloat sz1) ty2 (λty1,ty2. classify_sub_cases ty1 ty2) (sub_case_ff sz1) (sub_default …)
    5248  | Tpointer ty ⇒
    5349    match ty2 return λty2. classify_sub_cases ? ty2 with
     
    7268inductive classify_aop_cases : type → type → Type[0] ≝
    7369  | aop_case_ii: ∀sz,sg. classify_aop_cases (Tint sz sg) (Tint sz sg)
    74   | aop_case_ff: ∀sz.    classify_aop_cases (Tfloat sz)  (Tfloat sz)
    7570  | aop_default: ∀ty,ty'.classify_aop_cases ty ty'.
    7671
     
    7873  match ty1 return λty1. classify_aop_cases ty1 ty2 with
    7974  [ Tint sz1 sg1 ⇒ if_type_eq (Tint sz1 sg1) ty2 (λty1, ty2. classify_aop_cases ty1 ty2) (aop_case_ii sz1 sg1) (aop_default …)
    80   | Tfloat sz1 ⇒ if_type_eq (Tfloat sz1) ty2 (λty1,ty2. classify_aop_cases ty1 ty2) (aop_case_ff sz1) (aop_default …)
    8175  | _ ⇒ aop_default …
    8276  ].
     
    8579  | cmp_case_ii: ∀sz,sg.  classify_cmp_cases (Tint sz sg)      (Tint sz sg)
    8680  | cmp_case_pp: ∀n,ty.   classify_cmp_cases (ptr_type  ty n)  (ptr_type  ty n)
    87   | cmp_case_ff: ∀sz.     classify_cmp_cases (Tfloat sz)       (Tfloat sz)
    8881  | cmp_default: ∀ty,ty'. classify_cmp_cases ty ty'.
    8982
     
    9184  match ty1 return λty1. classify_cmp_cases ty1 ty2 with
    9285  [ Tint sz1 sg1 ⇒ if_type_eq (Tint sz1 sg1) ty2 (λty1, ty2. classify_cmp_cases ty1 ty2) (cmp_case_ii sz1 sg1) (cmp_default …)
    93   | Tfloat sz1 ⇒ if_type_eq (Tfloat sz1) ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_ff sz1) (cmp_default …)
    9486  | Tpointer  ty1' ⇒ if_type_eq (Tpointer  ty1') ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (None ?) …) (cmp_default …)
    9587  | Tarray  ty1' n1 ⇒ if_type_eq (Tarray  ty1' n1) ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (Some ? n1) …) (cmp_default …)
Note: See TracChangeset for help on using the changeset viewer.