source: src/Clight/TypeComparison.ma @ 2433

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

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

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