Ignore:
Timestamp:
Dec 19, 2012, 6:11:23 PM (7 years ago)
Author:
garnier
Message:

Cl to Cm progress.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2554 r2565  
    334334match classify_add ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
    335335[ add_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oadd ??) e1 e2)
    336 (*| add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2) *)
    337336(* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *)
    338337| add_case_pi n ty sz sg ⇒
     
    341340    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
    342341| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
    343 ].
    344 
     342].
    345343
    346344definition translate_sub ≝
     
    350348match classify_sub ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
    351349[ sub_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osub ??) e1 e2)
    352 (* | sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2) *)
    353350(* XXX could optimise cast as above *)
    354351| sub_case_pi n ty sz sg ⇒
Note: See TracChangeset for help on using the changeset viewer.