source: src/Clight/TypeComparison.ma @ 2896

Last change on this file since 2896 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 6.3 KB
Line 
1
2include "Clight/Csyntax.ma".
3include "utilities/extranat.ma".
4
5definition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
6#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
7definition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
8#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
9
10let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
11match t1 return λt'. Sum (t' = t2) (t' ≠ t2) with
12[ Tvoid ⇒ match t2 return λt'. Sum (Tvoid = t') (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
13| Tint sz sg ⇒ match t2 return λt'. Sum (Tint ?? = t') (Tint ?? ≠ t')  with [ Tint sz' sg' ⇒
14    match sz_eq_dec sz sz' with [ inl e1 ⇒
15    match sg_eq_dec sg sg' with [ inl e2 ⇒ inl ???
16    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
17    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
18    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
19| Tpointer t ⇒ match t2 return λt'. Sum (Tpointer ? = t') (Tpointer ? ≠ t')  with [ Tpointer t' ⇒
20      match type_eq_dec t t' with [ inl e2 ⇒ inl ???
21      | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]
22    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
23| Tarray t n ⇒ match t2 return λt'. Sum (Tarray ?? = t') (Tarray ?? ≠ t')  with [ Tarray t' n' ⇒
24      match type_eq_dec t t' with [ inl e2 ⇒
25        match eq_nat_dec n n' with [ inl e3 ⇒ inl ???
26        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
27        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
28        | _ ⇒ inr ?? (nmk ? (λH.?)) ]
29(*
30| Tpointer s t ⇒ match t2 return λt'. Sum (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'. Sum (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*)
44| Tfunction tl t ⇒ match t2 return λt'. Sum (Tfunction ?? = t') (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
45    match typelist_eq_dec tl tl' with [ inl e1 ⇒
46    match type_eq_dec t t' with [ inl e2 ⇒ 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 ?? (nmk ? (λH.?)) ]
50| Tstruct i fl ⇒
51    match t2 return λt'. Sum (Tstruct ?? = t') (Tstruct ?? ≠ t')  with [ Tstruct i' fl' ⇒
52    match ident_eq i i' with [ inl e1 ⇒
53    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
54    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
55    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
56    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
57| Tunion i fl ⇒
58    match t2 return λt'. Sum (Tunion ?? = t') (Tunion ?? ≠ t')  with [ Tunion i' fl' ⇒
59    match ident_eq i i' with [ inl e1 ⇒
60    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
61    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
62    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
63    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
64| Tcomp_ptr i ⇒ match t2 return λt'. Sum (Tcomp_ptr ? = t') (Tcomp_ptr ? ≠ t')  with [ Tcomp_ptr i' ⇒
65      match ident_eq i i' with [ inl e2 ⇒ inl ???
66      | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
67    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
68(*
69| Tcomp_ptr r i ⇒ match t2 return λt'. Sum (Tcomp_ptr ? ? = t') (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
70    match eq_region_dec r r' with [ inl e1 ⇒
71      match ident_eq i i' with [ inl e2 ⇒ inl ???
72      | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
73    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
74    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
75*)
76]
77and typelist_eq_dec (tl1,tl2:typelist) : Sum (tl1 = tl2) (tl1 ≠ tl2) ≝
78match tl1 return λtl'. Sum (tl' = tl2) (tl' ≠ tl2) with
79[ Tnil ⇒ match tl2 return λtl'. Sum (Tnil = tl') (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
80| Tcons t1 ts1 ⇒ match tl2 return λtl'. Sum (Tcons ?? = tl') (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
81    match type_eq_dec t1 t2 with [ inl e1 ⇒
82    match typelist_eq_dec ts1 ts2 with [ inl e2 ⇒ inl ???
83    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
84    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
85]
86and fieldlist_eq_dec (fl1,fl2:fieldlist) : Sum (fl1 = fl2) (fl1 ≠ fl2) ≝
87match fl1 return λfl'. Sum (fl' = fl2) (fl' ≠ fl2) with
88[ Fnil ⇒ match fl2 return λfl'. Sum (Fnil = fl') (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
89| Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. Sum (Fcons ??? = fl') (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
90    match ident_eq i1 i2 with [ inl e1 ⇒
91      match type_eq_dec t1 t2 with [ inl e2 ⇒
92        match fieldlist_eq_dec fs1 fs2 with [ inl e3 ⇒ inl ???
93        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
94        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
95        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
96]. try destruct; //
97qed.
98
99definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
100λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? (msg TypeMismatch)].
101
102definition type_eq : type → type → bool ≝
103λt1,t2. match type_eq_dec t1 t2 with [ inl _ ⇒ true | inr _ ⇒ false ].
104
105
106definition if_type_eq : ∀t1,t2:type. ∀P:type → type → Type[0]. P t1 t1 → P t1 t2 → P t1 t2 ≝
107λ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 ].
108// qed.
Note: See TracBrowser for help on using the repository browser.