Mercurial > urweb

comparison src/coq/Semantics.v @ 620:d828b143e147

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish semantics for Featherweight Ur
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 14:10:06 -0500
parents f38e009009bb
children 75c7a69354d6
comparison
equal deleted inserted replaced
619:f38e009009bb 620:d828b143e147
46 | KName => name 46 | KName => name
47 | KArrow k1 k2 => kDen k1 -> kDen k2 47 | KArrow k1 k2 => kDen k1 -> kDen k2
48 | KRecord k1 => row (kDen k1) 48 | KRecord k1 => row (kDen k1)
49 end. 49 end.
50 50
51 Fixpoint kDefault (k : kind) : kDen k :=
52 match k return kDen k with
53 | KType => unit
54 | KName => defaultName
55 | KArrow _ k2 => fun _ => kDefault k2
56 | KRecord _ => fun _ => None
57 end.
58
51 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k := 59 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
52 match c in con _ k return kDen k with 60 match c in con _ k return kDen k with
53 | CVar _ x => x 61 | CVar _ x => x
54 | Arrow c1 c2 => cDen c1 -> cDen c2 62 | Arrow c1 c2 => cDen c1 -> cDen c2
55 | Poly _ c1 => forall x, cDen (c1 x) 63 | Poly _ c1 => forall x, cDen (c1 x)
65 end 73 end
66 | CMap k1 k2 => fun f r n => match r n with 74 | CMap k1 k2 => fun f r n => match r n with
67 | None => None 75 | None => None
68 | Some T => Some (f T) 76 | Some T => Some (f T)
69 end 77 end
70 | CGuarded _ _ _ _ c => cDen c 78 | CGuarded _ _ c1 c2 c =>
79 if badName (fun n => match (cDen c1) n, (cDen c2) n with
80 | Some _, Some _ => false
81 | _, _ => true
82 end)
83 then kDefault _
84 else cDen c
71 end. 85 end.
72 86
73 Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2', 87 Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2',
74 subs c1 c2 c2' 88 subs c1 c2 c2'
75 -> cDen (c2 (cDen c1)) = cDen c2'. 89 -> cDen (c2 (cDen c1)) = cDen c2'.
85 | _, _ => True 99 | _, _ => True
86 end. 100 end.
87 Definition dvar k (c1 c2 : con kDen (KRecord k)) := 101 Definition dvar k (c1 c2 : con kDen (KRecord k)) :=
88 disjoint (cDen c1) (cDen c2). 102 disjoint (cDen c1) (cDen c2).
89 103
104 Theorem known_badName : forall T (r1 r2 : row T) T' (v1 v2 : T'),
105 disjoint r1 r2
106 -> (if badName (fun n => match r1 n, r2 n with
107 | Some _, Some _ => false
108 | _, _ => true
109 end)
110 then v1
111 else v2) = v2.
112 intros; match goal with
113 | [ |- context[if ?E then _ else _] ] => destruct E
114 end; firstorder;
115 match goal with
116 | [ H : disjoint _ _, x : name |- _ ] =>
117 generalize (H x);
118 repeat match goal with
119 | [ |- context[match ?E with None => _ | Some _ => _ end] ] => destruct E
120 end; tauto || congruence
121 end.
122 Qed.
123
124 Hint Rewrite known_badName using solve [ auto ] : Semantics.
125
90 Scheme deq_mut := Minimality for deq Sort Prop 126 Scheme deq_mut := Minimality for deq Sort Prop
91 with disj_mut := Minimality for disj Sort Prop. 127 with disj_mut := Minimality for disj Sort Prop.
92 128
93 Ltac deq_disj_correct scm := 129 Ltac deq_disj_correct scm :=
94 let t := repeat progress (simpl; intuition; subst) in 130 let t := repeat progress (simpl; intuition; subst; autorewrite with Semantics) in
95 131
96 let rec use_disjoint' notDone E := 132 let rec use_disjoint' notDone E :=
97 match goal with 133 match goal with
98 | [ H : disjoint _ _ |- _ ] => 134 | [ H : disjoint _ _ |- _ ] =>
99 notDone H; generalize (H E); use_disjoint' 135 notDone H; generalize (H E); use_disjoint'
111 cDen c1 = cDen c2) 147 cDen c1 = cDen c2)
112 (fun k (c1 c2 : con kDen (KRecord k)) => 148 (fun k (c1 c2 : con kDen (KRecord k)) =>
113 disjoint (cDen c1) (cDen c2))); t; 149 disjoint (cDen c1) (cDen c2))); t;
114 repeat ((unfold row; apply ext_eq) 150 repeat ((unfold row; apply ext_eq)
115 || (match goal with 151 || (match goal with
116 | [ H : _ |- _ ] => rewrite H 152 | [ H : _ |- _ ] => rewrite H; []
117 | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H) 153 | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H)
118 end); t); 154 end); t);
119 unfold disjoint; t; 155 unfold disjoint; t;
120 repeat (match goal with 156 repeat (match goal with
121 | [ |- context[match cDen ?C ?E with Some _ => _ | None => _ end] ] => 157 | [ |- context[match cDen ?C ?E with Some _ => _ | None => _ end] ] =>
122 use_disjoint E; destruct (cDen C E) 158 use_disjoint E; destruct (cDen C E)
123 | [ |- context[if name_eq_dec ?N1 ?N2 then _ else _] ] => 159 | [ |- context[if name_eq_dec ?N1 ?N2 then _ else _] ] =>
124 use_disjoint N1; use_disjoint N2; destruct (name_eq_dec N1 N2) 160 use_disjoint N1; use_disjoint N2; destruct (name_eq_dec N1 N2)
125 | [ _ : context[match cDen ?C ?E with Some _ => _ | None => _ end] |- _ ] => 161 | [ _ : context[match cDen ?C ?E with Some _ => _ | None => _ end] |- _ ] =>
126 use_disjoint E; destruct (cDen C E) 162 use_disjoint E; destruct (cDen C E)
163 | [ |- context[if ?E then _ else _] ] => destruct E
127 end; t). 164 end; t).
165
166 Lemma bool_disjoint : forall T (r1 r2 : row T),
167 (forall nm : name,
168 match r1 nm with
169 | Some _ => match r2 nm with
170 | Some _ => false
171 | None => true
172 end
173 | None => true
174 end = true)
175 -> disjoint r1 r2.
176 intros; intro;
177 match goal with
178 | [ H : _, n : name |- _ ] => generalize (H n)
179 end;
180 repeat match goal with
181 | [ |- context[match ?E with Some _ => _ | None => _ end] ] => destruct E
182 end; tauto || discriminate.
183 Qed.
184
185 Implicit Arguments bool_disjoint [T r1 r2].
186
187 Hint Resolve bool_disjoint.
188 Hint Unfold dvar.
128 189
129 Theorem deq_correct : forall k (c1 c2 : con kDen k), 190 Theorem deq_correct : forall k (c1 c2 : con kDen k),
130 deq dvar c1 c2 191 deq dvar c1 c2
131 -> cDen c1 = cDen c2. 192 -> cDen c1 = cDen c2.
132 deq_disj_correct deq_mut. 193 deq_disj_correct deq_mut.
135 Theorem disj_correct : forall k (c1 c2 : con kDen (KRecord k)), 196 Theorem disj_correct : forall k (c1 c2 : con kDen (KRecord k)),
136 disj dvar c1 c2 197 disj dvar c1 c2
137 -> disjoint (cDen c1) (cDen c2). 198 -> disjoint (cDen c1) (cDen c2).
138 deq_disj_correct disj_mut. 199 deq_disj_correct disj_mut.
139 Qed. 200 Qed.
140
141 Axiom cheat : forall T, T.
142 201
143 Definition tDen (t : con kDen KType) : Set := cDen t. 202 Definition tDen (t : con kDen KType) : Set := cDen t.
144 203
145 Theorem name_eq_dec_refl : forall n, name_eq_dec n n = left _ (refl_equal n). 204 Theorem name_eq_dec_refl : forall n, name_eq_dec n n = left _ (refl_equal n).
146 intros; destruct (name_eq_dec n n); intuition; [ 205 intros; destruct (name_eq_dec n n); intuition; [
163 end; rewrite name_eq_dec_refl; 222 end; rewrite name_eq_dec_refl;
164 destruct (r n1); intuition. 223 destruct (r n1); intuition.
165 Qed. 224 Qed.
166 225
167 Implicit Arguments cut_disjoint [v r]. 226 Implicit Arguments cut_disjoint [v r].
227
228 Set Printing All.
168 229
169 Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t := 230 Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t :=
170 match e in exp _ _ t return tDen t with 231 match e in exp _ _ t return tDen t with
171 | Var _ x => x 232 | Var _ x => x
172 | App _ _ e1 e2 => (eDen e1) (eDen e2) 233 | App _ _ e1 e2 => (eDen e1) (eDen e2)
223 end with 284 end with
224 | None => fun _ => (eDen e2) n 285 | None => fun _ => (eDen e2) n
225 | _ => fun x => x 286 | _ => fun x => x
226 end ((eDen e1) n) 287 end ((eDen e1) n)
227 288
228 | _ => cheat _ 289 | Guarded _ c1 c2 _ e1 =>
229 end. 290 match badName (fun n => match (cDen c1) n, (cDen c2) n with
291 | Some _, Some _ => false
292 | _, _ => true
293 end)
294 as BN return (if BN return Set then _ else _) with
295 | inleft _ => tt
296 | inright pf => eDen (e1 (bool_disjoint pf))
297 end
298 end.