source: src/Clight/ClassifyOp.ma @ 1948

(* This used to be presented along with the syntax for Clight, but I wanted to
   use the type comparison functions, and it's nice to see it on its own. *)

include "Clight/TypeComparison.ma".

(* * Classification of arithmetic operations and comparisons.
  The following [classify_] functions take as arguments the types
  of the arguments of an operation.  They return enough information
  to resolve overloading for this operator applications, such as
  ``both arguments are floats'', or ``the first is a pointer
  and the second is an integer''.  These functions are used to resolve
  overloading both in the dynamic semantics (module [Csem]) and in the
  compiler (module [Cshmgen]).
*)

definition ptr_type ≝ λr,ty,n. match n with [ None ⇒ Tpointer r ty | Some n' ⇒ Tarray r ty n' ].

inductive classify_add_cases : type → type → Type[0] ≝
  (* integer addition is always done on a single type, the parser will insert any
     necessary casts *)
  | add_case_ii: ∀sz,sg.          classify_add_cases (Tint sz sg)      (Tint sz sg)      (*Tint sz sg*)
  | add_case_ff: ∀sz.             classify_add_cases (Tfloat sz)       (Tfloat sz)       (*Tfloat sz*)
  | add_case_pi: ∀n,r,ty,sz,sg.   classify_add_cases (ptr_type r ty n) (Tint sz sg)      (*ptr_type r ty n*)
  | add_case_ip: ∀n,sz,sg,r,ty.   classify_add_cases (Tint sz sg)      (ptr_type r ty n) (*ptr_type r ty n*)
  | add_default: ∀ty1,ty2.        classify_add_cases ty1 ty2 (*ty'*).

definition classify_add : ∀ty1,ty2. classify_add_cases ty1 ty2 ≝ λty1: type. λty2: type.
  match ty1 return λty1. classify_add_cases ty1 ty2 with
  [ Tint sz1 sg1 ⇒
    match ty2 return λty2. classify_add_cases ? ty2 with
    [ Tint sz2 sg2 ⇒ inttyp_eq_elim' sz1 sz2 sg1 sg2 (λsz1,sg1,sz2,sg2. classify_add_cases (Tint sz1 sg1) (Tint sz2 sg2)) (add_case_ii sz1 ?) (add_default ??)
    | Tpointer _ ty ⇒ add_case_ip (None ?) …
    | Tarray _ ty n ⇒ add_case_ip (Some ? n) …
    | _ ⇒ add_default … ]
  | 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 … ]
  | Tpointer _ ty ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (None ?) … | _ ⇒ add_default … ]
  | Tarray _ ty n ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (Some ? n) … | _ ⇒ add_default … ]
  | _ ⇒ add_default …
  ].

inductive classify_sub_cases : type → type → Type[0] ≝
  | sub_case_ii: ∀sz,sg.        classify_sub_cases (Tint sz sg)      (Tint sz sg)
  | sub_case_ff: ∀sz.           classify_sub_cases (Tfloat sz)       (Tfloat sz)
  | sub_case_pi: ∀n,r,ty,sz,sg. classify_sub_cases (ptr_type r ty n) (Tint sz sg)
  | sub_case_pp: ∀n1,n2,r1,ty1,r2,ty2. classify_sub_cases (ptr_type r1 ty1 n1) (ptr_type r2 ty2 n2)
  | sub_default: ∀ty1,ty2. classify_sub_cases ty1 ty2.

definition classify_sub : ∀ty1,ty2. classify_sub_cases ty1 ty2 ≝ λty1: type. λty2: type.
  match ty1 return λty1. classify_sub_cases ty1 ty2 with
  [ Tint sz1 sg1 ⇒ if_type_eq (Tint sz1 sg1) ty2 (λty1, ty2. classify_sub_cases ty1 ty2) (sub_case_ii sz1 sg1) (sub_default …)
  | Tfloat sz1 ⇒ if_type_eq (Tfloat sz1) ty2 (λty1,ty2. classify_sub_cases ty1 ty2) (sub_case_ff sz1) (sub_default …)
  | Tpointer _ ty ⇒
    match ty2 return λty2. classify_sub_cases ? ty2 with
    [ Tint sz sg ⇒ sub_case_pi …
    | Tpointer _ _ ⇒ sub_case_pp (None ?) (None ?) …
    | Tarray _ _ n2 ⇒ sub_case_pp (None ?) (Some ? n2) …
    | _ ⇒ sub_default …]
  | Tarray _ ty n1 ⇒
    match ty2 return λty2. classify_sub_cases ? ty2 with
    [ Tint _ _ ⇒ sub_case_pi …
    | Tpointer _ _ ⇒ sub_case_pp (Some ? n1) (None ?) …
    | Tarray _ _ n2 ⇒ sub_case_pp (Some ? n1) (Some ? n2) …
    | _ ⇒ sub_default … ]
  | _ ⇒ sub_default …
  ].

(* NB: CompCert treats I32 Unsigned specially for div, mod and shr,
       but we uniformly use unsigned operations on as small a type as possible
       because we've no natural large word size.
       
       This is used for mul, div, mod, shr. *)
inductive classify_aop_cases : type → type → Type[0] ≝
  | aop_case_ii: ∀sz,sg. classify_aop_cases (Tint sz sg) (Tint sz sg)
  | aop_case_ff: ∀sz.    classify_aop_cases (Tfloat sz)  (Tfloat sz)
  | aop_default: ∀ty,ty'.classify_aop_cases ty ty'.

definition classify_aop ≝ λty1: type. λty2: type.
  match ty1 return λty1. classify_aop_cases ty1 ty2 with
  [ Tint sz1 sg1 ⇒ if_type_eq (Tint sz1 sg1) ty2 (λty1, ty2. classify_aop_cases ty1 ty2) (aop_case_ii sz1 sg1) (aop_default …)
  | Tfloat sz1 ⇒ if_type_eq (Tfloat sz1) ty2 (λty1,ty2. classify_aop_cases ty1 ty2) (aop_case_ff sz1) (aop_default …)
  | _ ⇒ aop_default …
  ].

inductive classify_cmp_cases : type → type → Type[0] ≝
  | cmp_case_ii: ∀sz,sg.  classify_cmp_cases (Tint sz sg)      (Tint sz sg)
  | cmp_case_pp: ∀n,r,ty. classify_cmp_cases (ptr_type r ty n) (ptr_type r ty n)
  | cmp_case_ff: ∀sz.     classify_cmp_cases (Tfloat sz)       (Tfloat sz)
  | cmp_default: ∀ty,ty'. classify_cmp_cases ty ty'.

definition classify_cmp ≝ λty1:type. λty2:type.
  match ty1 return λty1. classify_cmp_cases ty1 ty2 with
  [ Tint sz1 sg1 ⇒ if_type_eq (Tint sz1 sg1) ty2 (λty1, ty2. classify_cmp_cases ty1 ty2) (cmp_case_ii sz1 sg1) (cmp_default …)
  | Tfloat sz1 ⇒ if_type_eq (Tfloat sz1) ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_ff sz1) (cmp_default …)
  | Tpointer r1 ty1' ⇒ if_type_eq (Tpointer r1 ty1') ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (None ?) …) (cmp_default …)
  | Tarray r1 ty1' n1 ⇒ if_type_eq (Tarray r1 ty1' n1) ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (Some ? n1) …) (cmp_default …)
  | _ ⇒ cmp_default …
  ].

inductive classify_fun_cases : Type[0] ≝
  | fun_case_f: typelist → type → classify_fun_cases   (**r (pointer to) function *)
  | fun_default: classify_fun_cases . (**r other *)

definition classify_fun ≝ λty: type.
  match ty with 
  [ Tfunction args res ⇒ fun_case_f args res
  | Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
                                    | _ ⇒ fun_default
                                    ]
  | _ ⇒ fun_default
  ].