(* 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 ≝ λty,n. match n with [ None ⇒ Tpointer  ty | Some n' ⇒ Tarray  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_pi: ∀n,ty,sz,sg. classify_add_cases (ptr_type  ty n) (Tint sz sg)     (*ptr_type r ty n*)
  | add_case_ip: ∀n,sz,sg,ty. classify_add_cases (Tint sz sg)     (ptr_type  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 … ]
  | 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_pi: ∀n,ty,sz,sg.    classify_sub_cases (ptr_type  ty n)   (Tint sz sg)
  | sub_case_pp: ∀n1,n2,ty1,ty2. classify_sub_cases (ptr_type  ty1 n1) (ptr_type  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 …)
  | 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_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 …)
  | _ ⇒ 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,ty.   classify_cmp_cases (ptr_type  ty n)  (ptr_type  ty n)
  | 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 …)
  | Tpointer  ty1' ⇒ if_type_eq (Tpointer  ty1') ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (None ?) …) (cmp_default …)
  | Tarray  ty1' n1 ⇒ if_type_eq (Tarray  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
  ].