source: src/Clight/TypeComparison.ma @ 880

Last change on this file since 880 was 880, checked in by campbell, 8 years ago

Add type information into Cminor.
As a result, the Clight to Cminor stage now does extra type checking.

File size: 5.5 KB
Line 
1
2include "Clight/Csyntax.ma".
3
4axiom TypeMismatch : String.
5
6definition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
7#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
8definition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
9#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
10definition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
11#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
12
13definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m).
14#n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E
15[ %1 | %2 ] @(eqb_elim … E) // #_ #H destruct qed.
16
17let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
18match t1 return λt'. (t' = t2) + (t' ≠ t2) with
19[ Tvoid ⇒ match t2 return λt'. (Tvoid = t') + (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
20| Tint sz sg ⇒ match t2 return λt'. (Tint ?? = t') + (Tint ?? ≠ t')  with [ Tint sz' sg' ⇒
21    match sz_eq_dec sz sz' with [ inl e1 ⇒
22    match sg_eq_dec sg sg' with [ inl e2 ⇒ inl ???
23    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
24    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
25    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
26| Tfloat f ⇒ match t2 return λt'. (Tfloat ? = t') + (Tfloat ? ≠ t')  with [ Tfloat f' ⇒
27    match fs_eq_dec f f' with [ inl e1 ⇒ inl ???
28    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
29    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
30| Tpointer s t ⇒ match t2 return λt'. (Tpointer ?? = t') + (Tpointer ?? ≠ t')  with [ Tpointer s' t' ⇒
31    match eq_region_dec s s' with [ inl e1 ⇒
32      match type_eq_dec t t' with [ inl e2 ⇒ inl ???
33      | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]
34    | inr e1 ⇒ inr ?? (nmk ? (λH.match e1 with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ]
35| Tarray s t n ⇒ match t2 return λt'. (Tarray ??? = t') + (Tarray ??? ≠ t')  with [ Tarray s' t' n' ⇒
36    match eq_region_dec s s' with [ inl e1 ⇒
37      match type_eq_dec t t' with [ inl e2 ⇒
38        match eq_nat_dec n n' with [ inl e3 ⇒ inl ???
39        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
40        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
41        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
42        | _ ⇒ inr ?? (nmk ? (λH.?)) ]
43| Tfunction tl t ⇒ match t2 return λt'. (Tfunction ?? = t') + (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
44    match typelist_eq_dec tl tl' with [ inl e1 ⇒
45    match type_eq_dec t t' with [ inl e2 ⇒ inl ???
46    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
47    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
48  | _ ⇒ inr ?? (nmk ? (λH.?)) ]
49| Tstruct i fl ⇒
50    match t2 return λt'. (Tstruct ?? = t') + (Tstruct ?? ≠ t')  with [ Tstruct i' fl' ⇒
51    match ident_eq i i' with [ inl e1 ⇒
52    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
53    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
54    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
55    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
56| Tunion i fl ⇒
57    match t2 return λt'. (Tunion ?? = t') + (Tunion ?? ≠ t')  with [ Tunion i' fl' ⇒
58    match ident_eq i i' with [ inl e1 ⇒
59    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
60    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
61    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
62    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
63| Tcomp_ptr r i ⇒ match t2 return λt'. (Tcomp_ptr ? ? = t') + (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
64    match eq_region_dec r r' with [ inl e1 ⇒
65      match ident_eq i i' with [ inl e2 ⇒ inl ???
66      | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
67    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
68    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
69]
70and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝
71match tl1 return λtl'. (tl' = tl2) + (tl' ≠ tl2) with
72[ Tnil ⇒ match tl2 return λtl'. (Tnil = tl') + (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
73| Tcons t1 ts1 ⇒ match tl2 return λtl'. (Tcons ?? = tl') + (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
74    match type_eq_dec t1 t2 with [ inl e1 ⇒
75    match typelist_eq_dec ts1 ts2 with [ inl e2 ⇒ inl ???
76    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
77    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
78]
79and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝
80match fl1 return λfl'. (fl' = fl2) + (fl' ≠ fl2) with
81[ Fnil ⇒ match fl2 return λfl'. (Fnil = fl') + (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
82| Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. (Fcons ??? = fl') + (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
83    match ident_eq i1 i2 with [ inl e1 ⇒
84      match type_eq_dec t1 t2 with [ inl e2 ⇒
85        match fieldlist_eq_dec fs1 fs2 with [ inl e3 ⇒ inl ???
86        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
87        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
88        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
89]. destruct; //; qed.
90
91definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
92λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? (msg TypeMismatch)].
Note: See TracBrowser for help on using the repository browser.