source: src/Clight/TypeComparison.ma @ 1369

Last change on this file since 1369 was 1352, checked in by sacerdot, 9 years ago

This commit is made necessary by the last Matita change.
Inclusion is now order of magnitudes faster in some situations.
However, some explicit "include alias" are now required to
achieve the old semantics.

File size: 5.7 KB
RevLine 
[880]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
[882]15[ %1 | %2 ] lapply E @eqb_elim // #_ #H destruct qed.
[880]16
17let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
[891]18match t1 return λt'. Sum (t' = t2) (t' ≠ t2) with
19[ Tvoid ⇒ match t2 return λt'. Sum (Tvoid = t') (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
20| Tint sz sg ⇒ match t2 return λt'. Sum (Tint ?? = t') (Tint ?? ≠ t')  with [ Tint sz' sg' ⇒
[880]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.?)) ]
[891]26| Tfloat f ⇒ match t2 return λt'. Sum (Tfloat ? = t') (Tfloat ? ≠ t')  with [ Tfloat f' ⇒
[880]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.?)) ]
[891]30| Tpointer s t ⇒ match t2 return λt'. Sum (Tpointer ?? = t') (Tpointer ?? ≠ t')  with [ Tpointer s' t' ⇒
[880]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.?)) ]
[891]35| Tarray s t n ⇒ match t2 return λt'. Sum (Tarray ??? = t') (Tarray ??? ≠ t')  with [ Tarray s' t' n' ⇒
[880]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.?)) ]
[891]43| Tfunction tl t ⇒ match t2 return λt'. Sum (Tfunction ?? = t') (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
[880]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 ⇒
[891]50    match t2 return λt'. Sum (Tstruct ?? = t') (Tstruct ?? ≠ t')  with [ Tstruct i' fl' ⇒
[880]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 ⇒
[891]57    match t2 return λt'. Sum (Tunion ?? = t') (Tunion ?? ≠ t')  with [ Tunion i' fl' ⇒
[880]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.?)) ]
[891]63| Tcomp_ptr r i ⇒ match t2 return λt'. Sum (Tcomp_ptr ? ? = t') (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
[880]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]
[891]70and typelist_eq_dec (tl1,tl2:typelist) : Sum (tl1 = tl2) (tl1 ≠ tl2) ≝
71match tl1 return λtl'. Sum (tl' = tl2) (tl' ≠ tl2) with
72[ Tnil ⇒ match tl2 return λtl'. Sum (Tnil = tl') (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
73| Tcons t1 ts1 ⇒ match tl2 return λtl'. Sum (Tcons ?? = tl') (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
[880]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]
[891]79and fieldlist_eq_dec (fl1,fl2:fieldlist) : Sum (fl1 = fl2) (fl1 ≠ fl2) ≝
80match fl1 return λfl'. Sum (fl' = fl2) (fl' ≠ fl2) with
81[ Fnil ⇒ match fl2 return λfl'. Sum (Fnil = fl') (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
82| Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. Sum (Fcons ??? = fl') (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
[880]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' ? ])) ] ]
[1352]89]. (*Wilmer:XXXX try destruct //*) cases daemon qed.
[880]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)].
[1198]93
94definition type_eq : type → type → bool ≝
95λt1,t2. match type_eq_dec t1 t2 with [ inl _ ⇒ true | inr _ ⇒ false ].
96
Note: See TracBrowser for help on using the repository browser.