# HG changeset patch # User Adam Chlipala # Date 1234900168 18000 # Node ID 3c77133afd9afd28c15c0f6964ee461bd851846c # Parent 5891f47d7cff42adeb05030f4733c06ecf8ac15f Start of Featherweight Ur semantics diff -r 5891f47d7cff -r 3c77133afd9a .hgignore --- a/.hgignore Sun Feb 15 13:03:09 2009 -0500 +++ b/.hgignore Tue Feb 17 14:49:28 2009 -0500 @@ -33,3 +33,7 @@ *.pdf *.ps *.toc + +.depend +Makefile.coq +*.vo diff -r 5891f47d7cff -r 3c77133afd9a src/coq/Semantics.v --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/coq/Semantics.v Tue Feb 17 14:49:28 2009 -0500 @@ -0,0 +1,156 @@ +(* 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. + *) + +Require Import Arith List Omega TheoryList. + +Require Import Syntax. + +Set Implicit Arguments. + + +Section row'. + Variable A : Type. + + Inductive row' : list name -> Type := + | Nil : row' nil + | Cons : forall n ls, A -> AllS (lt n) ls -> row' ls -> row' (n :: ls). +End row'. + +Implicit Arguments Nil [A]. + +Record row (A : Type) : Type := Row { + keys : list name; + data : row' A keys +}. + +Inductive record' : forall ls, row' Set ls -> Set := +| RNil : record' Nil +| RCons : forall n ls (T : Set) (pf : AllS (lt n) ls) r, T -> record' r -> record' (Cons T pf r). + +Definition record (r : row Set) := record' (data r). + +Fixpoint kDen (k : kind) : Type := + match k with + | KType => Set + | KName => name + | KArrow k1 k2 => kDen k1 -> kDen k2 + | KRecord k1 => row (kDen k1) + end. + +Axiom cheat : forall T, T. + +Fixpoint cinsert (n : name) (ls : list name) {struct ls} : list name := + match ls with + | nil => n :: nil + | n' :: ls' => + if eq_nat_dec n n' + then ls + else if le_lt_dec n n' + then n :: ls + else n' :: cinsert n ls' + end. + +Hint Constructors AllS. +Hint Extern 1 (_ < _) => omega. + +Lemma insert_front' : forall n n', + n <> n' + -> n <= n' + -> forall ls, AllS (lt n') ls + -> AllS (lt n) ls. + induction 3; auto. +Qed. + +Lemma insert_front : forall n n', + n <> n' + -> n <= n' + -> forall ls, AllS (lt n') ls + -> AllS (lt n) (n' :: ls). + Hint Resolve insert_front'. + eauto. +Qed. + +Lemma insert_continue : forall n n', + n <> n' + -> n' < n + -> forall ls, AllS (lt n') ls + -> AllS (lt n') (cinsert n ls). + induction 3; simpl; auto; + repeat (match goal with + | [ |- context[if ?E then _ else _] ] => destruct E + end; auto). +Qed. + +Fixpoint insert T (n : name) (v : T) ls (r : row' T ls) {struct r} : row' T (cinsert n ls) := + match r in row' _ ls return row' T (cinsert n ls) with + | Nil => Cons (n := n) v (allS_nil _) Nil + | Cons n' ls' v' pf r' => + match eq_nat_dec n n' as END + return row' _ (if END then _ else _) with + | left _ => Cons (n := n') v' pf r' + | right pfNe => + match le_lt_dec n n' as LLD + return row' _ (if LLD then _ else _) with + | left pfLe => Cons (n := n) v (insert_front pfNe pfLe pf) (Cons (n := n') v' pf r') + | right pfLt => Cons (n := n') v' (insert_continue pfNe pfLt pf) (insert n v r') + end + end + end. + +Fixpoint cconcat (ls1 ls2 : list name) {struct ls1} : list name := + match ls1 with + | nil => ls2 + | n :: ls1' => cinsert n (cconcat ls1' ls2) + end. + +Fixpoint concat T ls1 ls2 (r1 : row' T ls1) (r2 : row' T ls2) {struct r1} : row' T (cconcat ls1 ls2) := + match r1 in row' _ ls1 return row' _ (cconcat ls1 _) with + | Nil => r2 + | Cons n _ v _ r1' => insert n v (concat r1' r2) + end. + +Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') ls (r : row' T ls) {struct r} : T' := + match r with + | Nil => i + | Cons n _ v _ r' => f n v (cfold f i r') + end. + +Fixpoint cDen k (c : con kDen k) {struct c} : kDen k := + match c in con _ k return kDen k with + | CVar _ x => x + | Arrow c1 c2 => cDen c1 -> cDen c2 + | Poly _ c1 => forall x, cDen (c1 x) + | CAbs _ _ c1 => fun x => cDen (c1 x) + | CApp _ _ c1 c2 => (cDen c1) (cDen c2) + | Name n => n + | TRecord c1 => record (cDen c1) + | CEmpty _ => Row Nil + | CSingle _ c1 c2 => Row (Cons (n := cDen c1) (cDen c2) (allS_nil _) Nil) + | CConcat _ c1 c2 => Row (concat (data (cDen c1)) (data (cDen c2))) + | CFold k1 k2 => fun f i r => cfold f i (data r) + | CGuarded _ _ _ _ c => cDen c + end. diff -r 5891f47d7cff -r 3c77133afd9a src/coq/Syntax.v --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/coq/Syntax.v Tue Feb 17 14:49:28 2009 -0500 @@ -0,0 +1,213 @@ +(* 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. + + +Definition name := nat. + + +(** Syntax of Featherweight Ur *) + +Inductive kind : Type := +| KType : kind +| KName : kind +| KArrow : kind -> kind -> kind +| KRecord : kind -> kind. + +Section vars. + Variable cvar : kind -> Type. + + Inductive con : kind -> Type := + | CVar : forall k, cvar k -> con k + | Arrow : con KType -> con KType -> con KType + | Poly : forall k, (cvar k -> con KType) -> con KType + | CAbs : forall k1 k2, (cvar k1 -> con k2) -> con (KArrow k1 k2) + | CApp : forall k1 k2, con (KArrow k1 k2) -> con k1 -> con k2 + | Name : name -> con KName + | TRecord : con (KRecord KType) -> con KType + | CEmpty : forall k, con (KRecord k) + | CSingle : forall k, con KName -> con k -> con (KRecord k) + | CConcat : forall k, con (KRecord k) -> con (KRecord k) -> con (KRecord k) + | CFold : forall k1 k2, con (KArrow (KArrow KName (KArrow k1 (KArrow k2 k2))) + (KArrow k2 (KArrow (KRecord k1) k2))) + | CGuarded : forall k1 k2, con (KRecord k1) -> con (KRecord k1) -> con k2 -> con k2. + + Variable dvar : forall k, con (KRecord k) -> con (KRecord k) -> Type. + + Section subs. + Variable k1 : kind. + Variable c1 : con k1. + + Inductive subs : forall k2, (cvar k1 -> con k2) -> con k2 -> Type := + | S_Unchanged : forall k2 (c2 : con k2), + subs (fun _ => c2) c2 + | S_CVar : subs (fun x => CVar x) c1 + | S_Arrow : forall c2 c3 c2' c3', + subs c2 c2' + -> subs c3 c3' + -> subs (fun x => Arrow (c2 x) (c3 x)) (Arrow c2' c3') + | S_Poly : forall k (c2 : cvar k1 -> cvar k -> _) (c2' : cvar k -> _), + (forall x', subs (fun x => c2 x x') (c2' x')) + -> subs (fun x => Poly (c2 x)) (Poly c2') + | S_CAbs : forall k2 k3 (c2 : cvar k1 -> cvar k2 -> con k3) (c2' : cvar k2 -> _), + (forall x', subs (fun x => c2 x x') (c2' x')) + -> subs (fun x => CAbs (c2 x)) (CAbs c2') + | S_CApp : forall k1 k2 (c2 : _ -> con (KArrow k1 k2)) c3 c2' c3', + subs c2 c2' + -> subs c3 c3' + -> subs (fun x => CApp (c2 x) (c3 x)) (CApp c2' c3') + | S_TRecord : forall c2 c2', + subs c2 c2' + -> subs (fun x => TRecord (c2 x)) (TRecord c2') + | S_CSingle : forall k2 c2 (c3 : _ -> con k2) c2' c3', + subs c2 c2' + -> subs c3 c3' + -> subs (fun x => CSingle (c2 x) (c3 x)) (CSingle c2' c3') + | S_CConcat : forall k2 (c2 c3 : _ -> con (KRecord k2)) c2' c3', + subs c2 c2' + -> subs c3 c3' + -> subs (fun x => CConcat (c2 x) (c3 x)) (CConcat c2' c3') + | S_CGuarded : forall k2 k3 (c2 c3 : _ -> con (KRecord k2)) (c4 : _ -> con k3) c2' c3' c4', + subs c2 c2' + -> subs c3 c3' + -> subs c4 c4' + -> subs (fun x => CGuarded (c2 x) (c3 x) (c4 x)) (CGuarded c2' c3' c4'). + End subs. + + Inductive disj : forall k, con (KRecord k) -> con (KRecord k) -> Prop := + | DVar : forall k (c1 c2 : con (KRecord k)), + dvar c1 c2 -> disj c1 c2 + | DComm : forall k (c1 c2 : con (KRecord k)), + disj c1 c2 -> disj c2 c1 + + | DEmpty : forall k c2, + disj (CEmpty k) c2 + | DSingleKeys : forall k X1 X2 (c1 c2 : con k), + X1 <> X2 + -> disj (CSingle (Name X1) c1) (CSingle (Name X2) c2) + | DSingleValues : forall k n1 n2 (c1 c2 : con k) k' (c1' c2' : con k'), + disj (CSingle n1 c1') (CSingle n2 c2') + -> disj (CSingle n1 c1) (CSingle n2 c2) + + | DConcat : forall k (c1 c2 c : con (KRecord k)), + disj c1 c + -> disj c2 c + -> disj (CConcat c1 c2) c + + | DEq : forall k (c1 c2 c1' : con (KRecord k)), + disj c1 c2 + -> deq c1 c1' + -> disj c1' c2 + + with deq : forall k, con k -> con k -> Prop := + | Eq_Beta : forall k1 k2 (c1 : cvar k1 -> con k2) c2 c1', + subs c2 c1 c1' + -> deq (CApp (CAbs c1) c2) c1' + | Eq_Refl : forall k (c : con k), + deq c c + | Eq_Comm : forall k (c1 c2 : con k), + deq c2 c1 + -> deq c1 c2 + | Eq_Trans : forall k (c1 c2 c3 : con k), + deq c1 c2 + -> deq c2 c3 + -> deq c1 c3 + | Eq_Cong : forall k1 k2 c1 c1' (c2 : cvar k1 -> con k2) c2' c2'', + deq c1 c1' + -> subs c1 c2 c2' + -> subs c1' c2 c2'' + -> deq c2' c2'' + + | Eq_Concat_Empty : forall k c, + deq (CConcat (CEmpty k) c) c + | Eq_Concat_Comm : forall k (c1 c2 : con (KRecord k)), + deq (CConcat c1 c2) (CConcat c2 c1) + | Eq_Concat_Assoc : forall k (c1 c2 c3 : con (KRecord k)), + deq (CConcat c1 (CConcat c2 c3)) (CConcat (CConcat c1 c2) c3) + + | Eq_Fold_Empty : forall k1 k2 f i, + deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CEmpty _)) i + | Eq_Fold_Cons : forall k1 k2 f i c1 c2 c3, + deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CConcat (CSingle c1 c2) c3)) + (CApp (CApp (CApp f c1) c2) (CApp (CApp (CApp (CFold k1 k2) f) i) c3)) + + | Eq_Guarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2), + disj c1 c2 + -> deq (CGuarded c1 c2 c) c + + | Eq_Map_Ident : forall k c, + deq (CApp (CApp (CApp (CFold k (KRecord k)) + (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CVar x2)) (CVar x3)))))) + (CEmpty _)) c) c + | Eq_Map_Dist : forall k1 k2 f c1 c2, + deq (CApp (CApp (CApp (CFold k1 (KRecord k2)) + (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f (CVar x2))) (CVar x3)))))) + (CEmpty _)) (CConcat c1 c2)) + (CConcat + (CApp (CApp (CApp (CFold k1 (KRecord k2)) + (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f (CVar x2))) (CVar x3)))))) + (CEmpty _)) c1) + (CApp (CApp (CApp (CFold k1 (KRecord k2)) + (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f (CVar x2))) (CVar x3)))))) + (CEmpty _)) c2)) + + | Eq_Fold_Fuse : forall k1 k2 k3 f i f' c, + deq (CApp (CApp (CApp (CFold k1 k2) f) i) + (CApp (CApp (CApp (CFold k3 (KRecord k1)) + (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f' (CVar x2))) (CVar x3)))))) + (CEmpty _)) c)) + (CApp (CApp (CApp (CFold k3 k2) + (CAbs (fun x1 => CAbs (fun x2 => CApp (CApp f (CVar x1)) (CApp f' (CVar x2)))))) + i) c). + + Inductive wf : forall k, con k -> Type := + | HK_CVar : forall k (x : cvar k), + wf (CVar x) + | HK_Arrow : forall c1 c2, + wf c1 -> wf c2 -> wf (Arrow c1 c2) + | HK_Poly : forall k (c1 : cvar k -> _), + (forall x, wf (c1 x)) -> wf (Poly c1) + | HK_CAbs : forall k1 k2 (c1 : cvar k1 -> con k2), + (forall x, wf (c1 x)) -> wf (CAbs c1) + | HK_CApp : forall k1 k2 (c1 : con (KArrow k1 k2)) c2, + wf c1 -> wf c2 -> wf (CApp c1 c2) + | HK_Name : forall X, + wf (Name X) + | HK_TRecord : forall c, + wf c -> wf (TRecord c) + | HK_CEmpty : forall k, + wf (CEmpty k) + | HK_CSingle : forall k c1 (c2 : con k), + wf c1 -> wf c2 -> wf (CSingle c1 c2) + | HK_CConcat : forall k (c1 c2 : con (KRecord k)), + wf c2 -> wf c2 -> disj c1 c2 -> wf (CConcat c1 c2) + | HK_CFold : forall k1 k2, + wf (CFold k1 k2) + | HK_CGuarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2), + wf c1 -> wf c2 -> (disj c1 c2 -> wf c) -> wf (CGuarded c1 c2 c). +End vars.