adamc@615: (* Copyright (c) 2009, Adam Chlipala adamc@615: * All rights reserved. adamc@615: * adamc@615: * Redistribution and use in source and binary forms, with or without adamc@615: * modification, are permitted provided that the following conditions are met: adamc@615: * adamc@615: * - Redistributions of source code must retain the above copyright notice, adamc@615: * this list of conditions and the following disclaimer. adamc@615: * - Redistributions in binary form must reproduce the above copyright notice, adamc@615: * this list of conditions and the following disclaimer in the documentation adamc@615: * and/or other materials provided with the distribution. adamc@615: * - The names of contributors may not be used to endorse or promote products adamc@615: * derived from this software without specific prior written permission. adamc@615: * adamc@615: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@615: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@615: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@615: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@615: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@615: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@615: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@615: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@615: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@615: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@615: * POSSIBILITY OF SUCH DAMAGE. adamc@615: *) adamc@615: adamc@617: Require Import String. adamc@617: adamc@615: Set Implicit Arguments. adamc@615: adamc@615: adamc@617: Definition name : Type := string. adamc@617: Definition name_eq_dec : forall (x y : name), {x = y} + {x <> y} := string_dec. adamc@615: adamc@615: adamc@615: (** Syntax of Featherweight Ur *) adamc@615: adamc@615: Inductive kind : Type := adamc@615: | KType : kind adamc@615: | KName : kind adamc@615: | KArrow : kind -> kind -> kind adamc@615: | KRecord : kind -> kind. adamc@615: adamc@615: Section vars. adamc@615: Variable cvar : kind -> Type. adamc@615: adamc@615: Inductive con : kind -> Type := adamc@615: | CVar : forall k, cvar k -> con k adamc@615: | Arrow : con KType -> con KType -> con KType adamc@615: | Poly : forall k, (cvar k -> con KType) -> con KType adamc@615: | CAbs : forall k1 k2, (cvar k1 -> con k2) -> con (KArrow k1 k2) adamc@615: | CApp : forall k1 k2, con (KArrow k1 k2) -> con k1 -> con k2 adamc@615: | Name : name -> con KName adamc@615: | TRecord : con (KRecord KType) -> con KType adamc@615: | CEmpty : forall k, con (KRecord k) adamc@615: | CSingle : forall k, con KName -> con k -> con (KRecord k) adamc@615: | CConcat : forall k, con (KRecord k) -> con (KRecord k) -> con (KRecord k) adamc@617: | CMap : forall k1 k2, con (KArrow (KArrow k1 k2) (KArrow (KRecord k1) (KRecord k2))) adamc@615: | CGuarded : forall k1 k2, con (KRecord k1) -> con (KRecord k1) -> con k2 -> con k2. adamc@615: adamc@615: Variable dvar : forall k, con (KRecord k) -> con (KRecord k) -> Type. adamc@615: adamc@615: Section subs. adamc@615: Variable k1 : kind. adamc@615: Variable c1 : con k1. adamc@615: adamc@615: Inductive subs : forall k2, (cvar k1 -> con k2) -> con k2 -> Type := adamc@615: | S_Unchanged : forall k2 (c2 : con k2), adamc@615: subs (fun _ => c2) c2 adamc@615: | S_CVar : subs (fun x => CVar x) c1 adamc@615: | S_Arrow : forall c2 c3 c2' c3', adamc@615: subs c2 c2' adamc@615: -> subs c3 c3' adamc@615: -> subs (fun x => Arrow (c2 x) (c3 x)) (Arrow c2' c3') adamc@615: | S_Poly : forall k (c2 : cvar k1 -> cvar k -> _) (c2' : cvar k -> _), adamc@615: (forall x', subs (fun x => c2 x x') (c2' x')) adamc@615: -> subs (fun x => Poly (c2 x)) (Poly c2') adamc@615: | S_CAbs : forall k2 k3 (c2 : cvar k1 -> cvar k2 -> con k3) (c2' : cvar k2 -> _), adamc@615: (forall x', subs (fun x => c2 x x') (c2' x')) adamc@615: -> subs (fun x => CAbs (c2 x)) (CAbs c2') adamc@615: | S_CApp : forall k1 k2 (c2 : _ -> con (KArrow k1 k2)) c3 c2' c3', adamc@615: subs c2 c2' adamc@615: -> subs c3 c3' adamc@615: -> subs (fun x => CApp (c2 x) (c3 x)) (CApp c2' c3') adamc@615: | S_TRecord : forall c2 c2', adamc@615: subs c2 c2' adamc@615: -> subs (fun x => TRecord (c2 x)) (TRecord c2') adamc@615: | S_CSingle : forall k2 c2 (c3 : _ -> con k2) c2' c3', adamc@615: subs c2 c2' adamc@615: -> subs c3 c3' adamc@615: -> subs (fun x => CSingle (c2 x) (c3 x)) (CSingle c2' c3') adamc@615: | S_CConcat : forall k2 (c2 c3 : _ -> con (KRecord k2)) c2' c3', adamc@615: subs c2 c2' adamc@615: -> subs c3 c3' adamc@615: -> subs (fun x => CConcat (c2 x) (c3 x)) (CConcat c2' c3') adamc@615: | S_CGuarded : forall k2 k3 (c2 c3 : _ -> con (KRecord k2)) (c4 : _ -> con k3) c2' c3' c4', adamc@615: subs c2 c2' adamc@615: -> subs c3 c3' adamc@615: -> subs c4 c4' adamc@615: -> subs (fun x => CGuarded (c2 x) (c3 x) (c4 x)) (CGuarded c2' c3' c4'). adamc@615: End subs. adamc@615: adamc@615: Inductive disj : forall k, con (KRecord k) -> con (KRecord k) -> Prop := adamc@615: | DVar : forall k (c1 c2 : con (KRecord k)), adamc@615: dvar c1 c2 -> disj c1 c2 adamc@615: | DComm : forall k (c1 c2 : con (KRecord k)), adamc@615: disj c1 c2 -> disj c2 c1 adamc@615: adamc@615: | DEmpty : forall k c2, adamc@615: disj (CEmpty k) c2 adamc@615: | DSingleKeys : forall k X1 X2 (c1 c2 : con k), adamc@615: X1 <> X2 adamc@615: -> disj (CSingle (Name X1) c1) (CSingle (Name X2) c2) adamc@615: | DSingleValues : forall k n1 n2 (c1 c2 : con k) k' (c1' c2' : con k'), adamc@615: disj (CSingle n1 c1') (CSingle n2 c2') adamc@615: -> disj (CSingle n1 c1) (CSingle n2 c2) adamc@615: adamc@615: | DConcat : forall k (c1 c2 c : con (KRecord k)), adamc@615: disj c1 c adamc@615: -> disj c2 c adamc@615: -> disj (CConcat c1 c2) c adamc@615: adamc@615: | DEq : forall k (c1 c2 c1' : con (KRecord k)), adamc@615: disj c1 c2 adamc@617: -> deq c1' c1 adamc@615: -> disj c1' c2 adamc@615: adamc@615: with deq : forall k, con k -> con k -> Prop := adamc@615: | Eq_Beta : forall k1 k2 (c1 : cvar k1 -> con k2) c2 c1', adamc@615: subs c2 c1 c1' adamc@615: -> deq (CApp (CAbs c1) c2) c1' adamc@615: | Eq_Refl : forall k (c : con k), adamc@615: deq c c adamc@615: | Eq_Comm : forall k (c1 c2 : con k), adamc@615: deq c2 c1 adamc@615: -> deq c1 c2 adamc@615: | Eq_Trans : forall k (c1 c2 c3 : con k), adamc@615: deq c1 c2 adamc@615: -> deq c2 c3 adamc@615: -> deq c1 c3 adamc@615: | Eq_Cong : forall k1 k2 c1 c1' (c2 : cvar k1 -> con k2) c2' c2'', adamc@615: deq c1 c1' adamc@615: -> subs c1 c2 c2' adamc@615: -> subs c1' c2 c2'' adamc@615: -> deq c2' c2'' adamc@615: adamc@615: | Eq_Concat_Empty : forall k c, adamc@615: deq (CConcat (CEmpty k) c) c adamc@617: | Eq_Concat_Comm : forall k (c1 c2 c3 : con (KRecord k)), adamc@617: disj c1 c2 adamc@617: -> deq (CConcat c1 c2) (CConcat c2 c1) adamc@615: | Eq_Concat_Assoc : forall k (c1 c2 c3 : con (KRecord k)), adamc@615: deq (CConcat c1 (CConcat c2 c3)) (CConcat (CConcat c1 c2) c3) adamc@615: adamc@617: | Eq_Map_Empty : forall k1 k2 f, adamc@617: deq (CApp (CApp (CMap k1 k2) f) (CEmpty _)) (CEmpty _) adamc@617: | Eq_Map_Cons : forall k1 k2 f c1 c2 c3, adamc@616: disj (CSingle c1 c2) c3 adamc@617: -> deq (CApp (CApp (CMap k1 k2) f) (CConcat (CSingle c1 c2) c3)) adamc@617: (CConcat (CSingle c1 (CApp f c2)) (CApp (CApp (CMap k1 k2) f) c3)) adamc@615: adamc@615: | Eq_Guarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2), adamc@617: (*disj c1 c2 adamc@617: ->*) deq (CGuarded c1 c2 c) c adamc@615: adamc@615: | Eq_Map_Ident : forall k c, adamc@617: deq (CApp (CApp (CMap k k) (CAbs (fun x => CVar x))) c) c adamc@615: | Eq_Map_Dist : forall k1 k2 f c1 c2, adamc@617: deq (CApp (CApp (CMap k1 k2) f) (CConcat c1 c2)) adamc@617: (CConcat (CApp (CApp (CMap k1 k2) f) c1) (CApp (CApp (CMap k1 k2) f) c2)) adamc@617: | Eq_Map_Fuse : forall k1 k2 k3 f f' c, adamc@617: deq (CApp (CApp (CMap k2 k3) f') adamc@617: (CApp (CApp (CMap k1 k2) f) c)) adamc@617: (CApp (CApp (CMap k1 k3) (CAbs (fun x => CApp f' (CApp f (CVar x))))) c). adamc@618: adamc@618: Variable evar : con KType -> Type. adamc@618: adamc@618: Inductive exp : con KType -> Type := adamc@618: | Var : forall t, evar t -> exp t adamc@618: | App : forall dom ran, exp (Arrow dom ran) -> exp dom -> exp ran adamc@618: | Abs : forall dom ran, (evar dom -> exp ran) -> exp (Arrow dom ran) adamc@618: | ECApp : forall k (dom : con k) ran ran', exp (Poly ran) -> subs dom ran ran' -> exp ran' adamc@618: | ECAbs : forall k (ran : cvar k -> _), (forall X, exp (ran X)) -> exp (Poly ran) adamc@618: | Cast : forall t1 t2, deq t1 t2 -> exp t1 -> exp t2 adamc@618: | Empty : exp (TRecord (CEmpty _)) adamc@618: | Single : forall c t, exp t -> exp (TRecord (CConcat (CSingle c t) (CEmpty _))) adamc@618: | Proj : forall c t c', exp (TRecord (CConcat (CSingle c t) c')) -> exp t adamc@618: | Cut : forall c t c', disj (CSingle c t) c' -> exp (TRecord (CConcat (CSingle c t) c')) -> exp (TRecord c') adamc@618: | Concat : forall c1 c2, disj c1 c2 -> exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2)) adamc@618: | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (CGuarded c1 c2 c). adamc@615: End vars.