source: src/Clight/ClassifyOp.ma @ 2176

Last change on this file since 2176 was 2176, checked in by campbell, 7 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File size: 6.2 KB
Line 
1(* This used to be presented along with the syntax for Clight, but I wanted to
2   use the type comparison functions, and it's nice to see it on its own. *)
3
4include "Clight/TypeComparison.ma".
5
6(* * Classification of arithmetic operations and comparisons.
7  The following [classify_] functions take as arguments the types
8  of the arguments of an operation.  They return enough information
9  to resolve overloading for this operator applications, such as
10  ``both arguments are floats'', or ``the first is a pointer
11  and the second is an integer''.  These functions are used to resolve
12  overloading both in the dynamic semantics (module [Csem]) and in the
13  compiler (module [Cshmgen]).
14*)
15
16definition ptr_type ≝ λty,n. match n with [ None ⇒ Tpointer  ty | Some n' ⇒ Tarray  ty n' ].
17
18inductive classify_add_cases : type → type → Type[0] ≝
19  (* integer addition is always done on a single type, the parser will insert any
20     necessary casts *)
21  | 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*)
23  | add_case_pi: ∀n,ty,sz,sg. classify_add_cases (ptr_type  ty n) (Tint sz sg)     (*ptr_type r ty n*)
24  | add_case_ip: ∀n,sz,sg,ty. classify_add_cases (Tint sz sg)     (ptr_type  ty n) (*ptr_type r ty n*)
25  | add_default: ∀ty1,ty2.    classify_add_cases ty1 ty2 (*ty'*).
26
27definition classify_add : ∀ty1,ty2. classify_add_cases ty1 ty2 ≝ λty1: type. λty2: type.
28  match ty1 return λty1. classify_add_cases ty1 ty2 with
29  [ Tint sz1 sg1 ⇒
30    match ty2 return λty2. classify_add_cases ? ty2 with
31    [ 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 ??)
32    | Tpointer ty ⇒ add_case_ip (None ?) …
33    | Tarray ty n ⇒ add_case_ip (Some ? n) …
34    | _ ⇒ 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 … ]
36  | Tpointer ty ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (None ?) … | _ ⇒ add_default … ]
37  | Tarray ty n ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (Some ? n) … | _ ⇒ add_default … ]
38  | _ ⇒ add_default …
39  ].
40
41inductive classify_sub_cases : type → type → Type[0] ≝
42  | 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)
44  | sub_case_pi: ∀n,ty,sz,sg.    classify_sub_cases (ptr_type  ty n)   (Tint sz sg)
45  | sub_case_pp: ∀n1,n2,ty1,ty2. classify_sub_cases (ptr_type  ty1 n1) (ptr_type  ty2 n2)
46  | sub_default: ∀ty1,ty2. classify_sub_cases ty1 ty2.
47
48definition classify_sub : ∀ty1,ty2. classify_sub_cases ty1 ty2 ≝ λty1: type. λty2: type.
49  match ty1 return λty1. classify_sub_cases ty1 ty2 with
50  [ 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 …)
52  | Tpointer ty ⇒
53    match ty2 return λty2. classify_sub_cases ? ty2 with
54    [ Tint sz sg ⇒ sub_case_pi …
55    | Tpointer _ ⇒ sub_case_pp (None ?) (None ?) …
56    | Tarray _ n2 ⇒ sub_case_pp (None ?) (Some ? n2) …
57    | _ ⇒ sub_default …]
58  | Tarray ty n1 ⇒
59    match ty2 return λty2. classify_sub_cases ? ty2 with
60    [ Tint _ _ ⇒ sub_case_pi …
61    | Tpointer _ ⇒ sub_case_pp (Some ? n1) (None ?) …
62    | Tarray _ n2 ⇒ sub_case_pp (Some ? n1) (Some ? n2) …
63    | _ ⇒ sub_default … ]
64  | _ ⇒ sub_default …
65  ].
66
67(* NB: CompCert treats I32 Unsigned specially for div, mod and shr,
68       but we uniformly use unsigned operations on as small a type as possible
69       because we've no natural large word size.
70       
71       This is used for mul, div, mod, shr. *)
72inductive classify_aop_cases : type → type → Type[0] ≝
73  | 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)
75  | aop_default: ∀ty,ty'.classify_aop_cases ty ty'.
76
77definition classify_aop ≝ λty1: type. λty2: type.
78  match ty1 return λty1. classify_aop_cases ty1 ty2 with
79  [ 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 …)
81  | _ ⇒ aop_default …
82  ].
83
84inductive classify_cmp_cases : type → type → Type[0] ≝
85  | cmp_case_ii: ∀sz,sg.  classify_cmp_cases (Tint sz sg)      (Tint sz sg)
86  | 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)
88  | cmp_default: ∀ty,ty'. classify_cmp_cases ty ty'.
89
90definition classify_cmp ≝ λty1:type. λty2:type.
91  match ty1 return λty1. classify_cmp_cases ty1 ty2 with
92  [ 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 …)
94  | Tpointer  ty1' ⇒ if_type_eq (Tpointer  ty1') ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (None ?) …) (cmp_default …)
95  | Tarray  ty1' n1 ⇒ if_type_eq (Tarray  ty1' n1) ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (Some ? n1) …) (cmp_default …)
96  | _ ⇒ cmp_default …
97  ].
98
99inductive classify_fun_cases : Type[0] ≝
100  | fun_case_f: typelist → type → classify_fun_cases   (**r (pointer to) function *)
101  | fun_default: classify_fun_cases . (**r other *)
102
103definition classify_fun ≝ λty: type.
104  match ty with
105  [ Tfunction args res ⇒ fun_case_f args res
106  | Tpointer ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
107                                  | _ ⇒ fun_default
108                                  ]
109  | _ ⇒ fun_default
110  ].
Note: See TracBrowser for help on using the repository browser.