source: src/Clight/TypeComparison.ma @ 1635

Last change on this file since 1635 was 1515, checked in by campbell, 10 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 5.5 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 s t ⇒ match t2 return λt'. Sum (Tpointer ?? = t') (Tpointer ?? ≠ t')  with [ Tpointer s' t' ⇒
28    match eq_region_dec s s' with [ inl e1 ⇒
29      match type_eq_dec t t' with [ inl e2 ⇒ inl ???
30      | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]
31    | inr e1 ⇒ inr ?? (nmk ? (λH.match e1 with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ]
32| Tarray s t n ⇒ match t2 return λt'. Sum (Tarray ??? = t') (Tarray ??? ≠ t')  with [ Tarray s' t' n' ⇒
33    match eq_region_dec s s' with [ inl e1 ⇒
34      match type_eq_dec t t' with [ inl e2 ⇒
35        match eq_nat_dec n n' with [ inl e3 ⇒ inl ???
36        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
37        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
38        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
39        | _ ⇒ inr ?? (nmk ? (λH.?)) ]
40| Tfunction tl t ⇒ match t2 return λt'. Sum (Tfunction ?? = t') (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
41    match typelist_eq_dec tl tl' with [ inl e1 ⇒
42    match type_eq_dec t t' with [ inl e2 ⇒ inl ???
43    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
44    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
45  | _ ⇒ inr ?? (nmk ? (λH.?)) ]
46| Tstruct i fl ⇒
47    match t2 return λt'. Sum (Tstruct ?? = t') (Tstruct ?? ≠ t')  with [ Tstruct i' fl' ⇒
48    match ident_eq i i' with [ inl e1 ⇒
49    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
50    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
51    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
52    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
53| Tunion i fl ⇒
54    match t2 return λt'. Sum (Tunion ?? = t') (Tunion ?? ≠ t')  with [ Tunion i' fl' ⇒
55    match ident_eq i i' with [ inl e1 ⇒
56    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
57    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
58    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
59    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
60| Tcomp_ptr r i ⇒ match t2 return λt'. Sum (Tcomp_ptr ? ? = t') (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
61    match eq_region_dec r r' with [ inl e1 ⇒
62      match ident_eq i i' with [ inl e2 ⇒ inl ???
63      | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
64    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
65    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
66]
67and typelist_eq_dec (tl1,tl2:typelist) : Sum (tl1 = tl2) (tl1 ≠ tl2) ≝
68match tl1 return λtl'. Sum (tl' = tl2) (tl' ≠ tl2) with
69[ Tnil ⇒ match tl2 return λtl'. Sum (Tnil = tl') (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
70| Tcons t1 ts1 ⇒ match tl2 return λtl'. Sum (Tcons ?? = tl') (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
71    match type_eq_dec t1 t2 with [ inl e1 ⇒
72    match typelist_eq_dec ts1 ts2 with [ inl e2 ⇒ inl ???
73    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
74    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
75]
76and fieldlist_eq_dec (fl1,fl2:fieldlist) : Sum (fl1 = fl2) (fl1 ≠ fl2) ≝
77match fl1 return λfl'. Sum (fl' = fl2) (fl' ≠ fl2) with
78[ Fnil ⇒ match fl2 return λfl'. Sum (Fnil = fl') (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
79| Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. Sum (Fcons ??? = fl') (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
80    match ident_eq i1 i2 with [ inl e1 ⇒
81      match type_eq_dec t1 t2 with [ inl e2 ⇒
82        match fieldlist_eq_dec fs1 fs2 with [ inl e3 ⇒ 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        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
86]. try destruct; //
87qed.
88
89definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
90λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? (msg TypeMismatch)].
91
92definition type_eq : type → type → bool ≝
93λt1,t2. match type_eq_dec t1 t2 with [ inl _ ⇒ true | inr _ ⇒ false ].
94
Note: See TracBrowser for help on using the repository browser.