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@620: Require Import Name.
adamc@620: Export Name.
adamc@617: 
adamc@615: Set Implicit Arguments.
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@635:   | TGuarded : forall k, con (KRecord k) -> con (KRecord k) -> con KType -> con KType.
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@635:     | S_TGuarded : forall k2 (c2 c3 : _ -> con (KRecord k2)) c4 c2' c3' c4',
adamc@615:       subs c2 c2'
adamc@615:       -> subs c3 c3'
adamc@615:       -> subs c4 c4'
adamc@635:       -> subs (fun x => TGuarded (c2 x) (c3 x) (c4 x)) (TGuarded 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_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@619:   | Concat : forall c1 c2, exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2))
adamc@635:   | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (TGuarded c1 c2 c)
adamc@635:   | GuardedApp : forall k (c1 c2 : con (KRecord k)) t, exp (TGuarded c1 c2 t) -> disj c1 c2 -> exp t.
adamc@615: End vars.