# HG changeset patch # User Adam Chlipala # Date 1235243406 18000 # Node ID d828b143e147a8acea7bdb2553a5c147ace5c56d # Parent f38e009009bb4e960964975abe1c2ab4859d33d5 Finish semantics for Featherweight Ur diff -r f38e009009bb -r d828b143e147 src/coq/Name.v --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/coq/Name.v Sat Feb 21 14:10:06 2009 -0500 @@ -0,0 +1,71 @@ +(* Copyright (c) 2009, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +Set Implicit Arguments. + + +Fixpoint name' (n : nat) : Type := + match n with + | O => Empty_set + | S n' => option (name' n') + end. + +Definition name'_eq_dec : forall n (x y : name' n), {x = y} + {x <> y}. + Hint Extern 1 (_ = _ -> False) => congruence. + + induction n; simpl; intuition; + repeat match goal with + | [ x : Empty_set |- _ ] => destruct x + | [ x : option _ |- _ ] => destruct x + end; intuition; + match goal with + | [ IH : _, n1 : name' _, n2 : name' _ |- _ ] => + destruct (IHn n1 n0); subst; intuition + end. +Qed. + +Definition badName' n (P : name' n -> bool) : + {nm : _ | P nm = false} + {forall nm, P nm = true}. + Hint Constructors sig. + Hint Extern 1 (_ = true) => + match goal with + | [ nm : option _ |- _ ] => destruct nm + end; auto. + + induction n; simpl; intuition; + match goal with + | [ IH : forall P : _ -> _,_ |- _ ] => + case_eq (P None); + destruct (IH (fun nm => P (Some nm))); firstorder eauto + end. +Qed. + +Parameter numNames : nat. +Definition name := name' (S numNames). +Definition name_eq_dec : forall (x y : name), {x = y} + {x <> y} := @name'_eq_dec _. +Definition badName : forall P : name -> bool, {nm : _ | P nm = false} + {forall nm, P nm = true} := @badName' _. +Definition defaultName : name := None. diff -r f38e009009bb -r d828b143e147 src/coq/Semantics.v --- a/src/coq/Semantics.v Sat Feb 21 13:22:30 2009 -0500 +++ b/src/coq/Semantics.v Sat Feb 21 14:10:06 2009 -0500 @@ -48,6 +48,14 @@ | KRecord k1 => row (kDen k1) end. +Fixpoint kDefault (k : kind) : kDen k := + match k return kDen k with + | KType => unit + | KName => defaultName + | KArrow _ k2 => fun _ => kDefault k2 + | KRecord _ => fun _ => None + end. + Fixpoint cDen k (c : con kDen k) {struct c} : kDen k := match c in con _ k return kDen k with | CVar _ x => x @@ -67,7 +75,13 @@ | None => None | Some T => Some (f T) end - | CGuarded _ _ _ _ c => cDen c + | CGuarded _ _ c1 c2 c => + if badName (fun n => match (cDen c1) n, (cDen c2) n with + | Some _, Some _ => false + | _, _ => true + end) + then kDefault _ + else cDen c end. Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2', @@ -87,11 +101,33 @@ Definition dvar k (c1 c2 : con kDen (KRecord k)) := disjoint (cDen c1) (cDen c2). +Theorem known_badName : forall T (r1 r2 : row T) T' (v1 v2 : T'), + disjoint r1 r2 + -> (if badName (fun n => match r1 n, r2 n with + | Some _, Some _ => false + | _, _ => true + end) + then v1 + else v2) = v2. + intros; match goal with + | [ |- context[if ?E then _ else _] ] => destruct E + end; firstorder; + match goal with + | [ H : disjoint _ _, x : name |- _ ] => + generalize (H x); + repeat match goal with + | [ |- context[match ?E with None => _ | Some _ => _ end] ] => destruct E + end; tauto || congruence + end. +Qed. + +Hint Rewrite known_badName using solve [ auto ] : Semantics. + Scheme deq_mut := Minimality for deq Sort Prop with disj_mut := Minimality for disj Sort Prop. Ltac deq_disj_correct scm := - let t := repeat progress (simpl; intuition; subst) in + let t := repeat progress (simpl; intuition; subst; autorewrite with Semantics) in let rec use_disjoint' notDone E := match goal with @@ -113,7 +149,7 @@ disjoint (cDen c1) (cDen c2))); t; repeat ((unfold row; apply ext_eq) || (match goal with - | [ H : _ |- _ ] => rewrite H + | [ H : _ |- _ ] => rewrite H; [] | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H) end); t); unfold disjoint; t; @@ -124,8 +160,33 @@ use_disjoint N1; use_disjoint N2; destruct (name_eq_dec N1 N2) | [ _ : context[match cDen ?C ?E with Some _ => _ | None => _ end] |- _ ] => use_disjoint E; destruct (cDen C E) + | [ |- context[if ?E then _ else _] ] => destruct E end; t). +Lemma bool_disjoint : forall T (r1 r2 : row T), + (forall nm : name, + match r1 nm with + | Some _ => match r2 nm with + | Some _ => false + | None => true + end + | None => true + end = true) + -> disjoint r1 r2. + intros; intro; + match goal with + | [ H : _, n : name |- _ ] => generalize (H n) + end; + repeat match goal with + | [ |- context[match ?E with Some _ => _ | None => _ end] ] => destruct E + end; tauto || discriminate. +Qed. + +Implicit Arguments bool_disjoint [T r1 r2]. + +Hint Resolve bool_disjoint. +Hint Unfold dvar. + Theorem deq_correct : forall k (c1 c2 : con kDen k), deq dvar c1 c2 -> cDen c1 = cDen c2. @@ -138,8 +199,6 @@ deq_disj_correct disj_mut. Qed. -Axiom cheat : forall T, T. - Definition tDen (t : con kDen KType) : Set := cDen t. Theorem name_eq_dec_refl : forall n, name_eq_dec n n = left _ (refl_equal n). @@ -166,6 +225,8 @@ Implicit Arguments cut_disjoint [v r]. +Set Printing All. + Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t := match e in exp _ _ t return tDen t with | Var _ x => x @@ -225,5 +286,13 @@ | _ => fun x => x end ((eDen e1) n) - | _ => cheat _ + | Guarded _ c1 c2 _ e1 => + match badName (fun n => match (cDen c1) n, (cDen c2) n with + | Some _, Some _ => false + | _, _ => true + end) + as BN return (if BN return Set then _ else _) with + | inleft _ => tt + | inright pf => eDen (e1 (bool_disjoint pf)) + end end. diff -r f38e009009bb -r d828b143e147 src/coq/Syntax.v --- a/src/coq/Syntax.v Sat Feb 21 13:22:30 2009 -0500 +++ b/src/coq/Syntax.v Sat Feb 21 14:10:06 2009 -0500 @@ -25,15 +25,12 @@ * POSSIBILITY OF SUCH DAMAGE. *) -Require Import String. +Require Import Name. +Export Name. Set Implicit Arguments. -Definition name : Type := string. -Definition name_eq_dec : forall (x y : name), {x = y} + {x <> y} := string_dec. - - (** Syntax of Featherweight Ur *) Inductive kind : Type := @@ -160,9 +157,12 @@ -> deq (CApp (CApp (CMap k1 k2) f) (CConcat (CSingle c1 c2) c3)) (CConcat (CSingle c1 (CApp f c2)) (CApp (CApp (CMap k1 k2) f) c3)) - | Eq_Guarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2), - (*disj c1 c2 - ->*) deq (CGuarded c1 c2 c) c + | Eq_Guarded_Remove : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2), + disj c1 c2 + -> deq (CGuarded c1 c2 c) c + | Eq_Guarded_Cong : forall k1 k2 (c1 c2 : con (KRecord k1)) (c c' : con k2), + (dvar c1 c2 -> deq c c') + -> deq (CGuarded c1 c2 c) (CGuarded c1 c2 c') | Eq_Map_Ident : forall k c, deq (CApp (CApp (CMap k k) (CAbs (fun x => CVar x))) c) c