source: src/Clight/ClassifyOp.ma @ 2468

Last change on this file since 2468 was 2468, checked in by garnier, 7 years ago

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 size: 5.3 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_pi: ∀n,ty,sz,sg. classify_add_cases (ptr_type  ty n) (Tint sz sg)     (*ptr_type r ty n*)
23  | add_case_ip: ∀n,sz,sg,ty. classify_add_cases (Tint sz sg)     (ptr_type  ty n) (*ptr_type r ty n*)
24  | add_default: ∀ty1,ty2.    classify_add_cases ty1 ty2 (*ty'*).
25
26definition classify_add : ∀ty1,ty2. classify_add_cases ty1 ty2 ≝ λty1: type. λty2: type.
27  match ty1 return λty1. classify_add_cases ty1 ty2 with
28  [ Tint sz1 sg1 ⇒
29    match ty2 return λty2. classify_add_cases ? ty2 with
30    [ 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 ??)
31    | Tpointer ty ⇒ add_case_ip (None ?) …
32    | Tarray ty n ⇒ add_case_ip (Some ? n) …
33    | _ ⇒ add_default … ]
34  | Tpointer ty ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (None ?) … | _ ⇒ add_default … ]
35  | Tarray ty n ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (Some ? n) … | _ ⇒ add_default … ]
36  | _ ⇒ add_default …
37  ].
38
39inductive classify_sub_cases : type → type → Type[0] ≝
40  | sub_case_ii: ∀sz,sg.         classify_sub_cases (Tint sz sg)       (Tint sz sg)
41  | sub_case_pi: ∀n,ty,sz,sg.    classify_sub_cases (ptr_type  ty n)   (Tint sz sg)
42  | sub_case_pp: ∀n1,n2,ty1,ty2. classify_sub_cases (ptr_type  ty1 n1) (ptr_type  ty2 n2)
43  | sub_default: ∀ty1,ty2. classify_sub_cases ty1 ty2.
44
45definition classify_sub : ∀ty1,ty2. classify_sub_cases ty1 ty2 ≝ λty1: type. λty2: type.
46  match ty1 return λty1. classify_sub_cases ty1 ty2 with
47  [ Tint sz1 sg1 ⇒ if_type_eq (Tint sz1 sg1) ty2 (λty1, ty2. classify_sub_cases ty1 ty2) (sub_case_ii sz1 sg1) (sub_default …)
48  | Tpointer ty ⇒
49    match ty2 return λty2. classify_sub_cases ? ty2 with
50    [ Tint sz sg ⇒ sub_case_pi …
51    | Tpointer _ ⇒ sub_case_pp (None ?) (None ?) …
52    | Tarray _ n2 ⇒ sub_case_pp (None ?) (Some ? n2) …
53    | _ ⇒ sub_default …]
54  | Tarray ty n1 ⇒
55    match ty2 return λty2. classify_sub_cases ? ty2 with
56    [ Tint _ _ ⇒ sub_case_pi …
57    | Tpointer _ ⇒ sub_case_pp (Some ? n1) (None ?) …
58    | Tarray _ n2 ⇒ sub_case_pp (Some ? n1) (Some ? n2) …
59    | _ ⇒ sub_default … ]
60  | _ ⇒ sub_default …
61  ].
62
63(* NB: CompCert treats I32 Unsigned specially for div, mod and shr,
64       but we uniformly use unsigned operations on as small a type as possible
65       because we've no natural large word size.
66       
67       This is used for mul, div, mod, shr. *)
68inductive classify_aop_cases : type → type → Type[0] ≝
69  | aop_case_ii: ∀sz,sg. classify_aop_cases (Tint sz sg) (Tint sz sg)
70  | aop_default: ∀ty,ty'.classify_aop_cases ty ty'.
71
72definition classify_aop ≝ λty1: type. λty2: type.
73  match ty1 return λty1. classify_aop_cases ty1 ty2 with
74  [ Tint sz1 sg1 ⇒ if_type_eq (Tint sz1 sg1) ty2 (λty1, ty2. classify_aop_cases ty1 ty2) (aop_case_ii sz1 sg1) (aop_default …)
75  | _ ⇒ aop_default …
76  ].
77
78inductive classify_cmp_cases : type → type → Type[0] ≝
79  | cmp_case_ii: ∀sz,sg.  classify_cmp_cases (Tint sz sg)      (Tint sz sg)
80  | cmp_case_pp: ∀n,ty.   classify_cmp_cases (ptr_type  ty n)  (ptr_type  ty n)
81  | cmp_default: ∀ty,ty'. classify_cmp_cases ty ty'.
82
83definition classify_cmp ≝ λty1:type. λty2:type.
84  match ty1 return λty1. classify_cmp_cases ty1 ty2 with
85  [ Tint sz1 sg1 ⇒ if_type_eq (Tint sz1 sg1) ty2 (λty1, ty2. classify_cmp_cases ty1 ty2) (cmp_case_ii sz1 sg1) (cmp_default …)
86  | Tpointer  ty1' ⇒ if_type_eq (Tpointer  ty1') ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (None ?) …) (cmp_default …)
87  | Tarray  ty1' n1 ⇒ if_type_eq (Tarray  ty1' n1) ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (Some ? n1) …) (cmp_default …)
88  | _ ⇒ cmp_default …
89  ].
90
91inductive classify_fun_cases : Type[0] ≝
92  | fun_case_f: typelist → type → classify_fun_cases   (**r (pointer to) function *)
93  | fun_default: classify_fun_cases . (**r other *)
94
95definition classify_fun ≝ λty: type.
96  match ty with
97  [ Tfunction args res ⇒ fun_case_f args res
98  | Tpointer ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
99                                  | _ ⇒ fun_default
100                                  ]
101  | _ ⇒ fun_default
102  ].
Note: See TracBrowser for help on using the repository browser.