Mercurial > urweb

annotate src/coq/Syntax.v @ 615:3c77133afd9a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of Featherweight Ur semantics
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Feb 2009 14:49:28 -0500
parents
children d26d1f3acfd6
rev   line source
adamc@615 1 (* Copyright (c) 2009, Adam Chlipala
adamc@615 2 * All rights reserved.
adamc@615 3 *
adamc@615 4 * Redistribution and use in source and binary forms, with or without
adamc@615 5 * modification, are permitted provided that the following conditions are met:
adamc@615 6 *
adamc@615 7 * - Redistributions of source code must retain the above copyright notice,
adamc@615 8 * this list of conditions and the following disclaimer.
adamc@615 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@615 10 * this list of conditions and the following disclaimer in the documentation
adamc@615 11 * and/or other materials provided with the distribution.
adamc@615 12 * - The names of contributors may not be used to endorse or promote products
adamc@615 13 * derived from this software without specific prior written permission.
adamc@615 14 *
adamc@615 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@615 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@615 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@615 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@615 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@615 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@615 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@615 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@615 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@615 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@615 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@615 26 *)
adamc@615 27
adamc@615 28 Set Implicit Arguments.
adamc@615 29
adamc@615 30
adamc@615 31 Definition name := nat.
adamc@615 32
adamc@615 33
adamc@615 34 (** Syntax of Featherweight Ur *)
adamc@615 35
adamc@615 36 Inductive kind : Type :=
adamc@615 37 | KType : kind
adamc@615 38 | KName : kind
adamc@615 39 | KArrow : kind -> kind -> kind
adamc@615 40 | KRecord : kind -> kind.
adamc@615 41
adamc@615 42 Section vars.
adamc@615 43 Variable cvar : kind -> Type.
adamc@615 44
adamc@615 45 Inductive con : kind -> Type :=
adamc@615 46 | CVar : forall k, cvar k -> con k
adamc@615 47 | Arrow : con KType -> con KType -> con KType
adamc@615 48 | Poly : forall k, (cvar k -> con KType) -> con KType
adamc@615 49 | CAbs : forall k1 k2, (cvar k1 -> con k2) -> con (KArrow k1 k2)
adamc@615 50 | CApp : forall k1 k2, con (KArrow k1 k2) -> con k1 -> con k2
adamc@615 51 | Name : name -> con KName
adamc@615 52 | TRecord : con (KRecord KType) -> con KType
adamc@615 53 | CEmpty : forall k, con (KRecord k)
adamc@615 54 | CSingle : forall k, con KName -> con k -> con (KRecord k)
adamc@615 55 | CConcat : forall k, con (KRecord k) -> con (KRecord k) -> con (KRecord k)
adamc@615 56 | CFold : forall k1 k2, con (KArrow (KArrow KName (KArrow k1 (KArrow k2 k2)))
adamc@615 57 (KArrow k2 (KArrow (KRecord k1) k2)))
adamc@615 58 | CGuarded : forall k1 k2, con (KRecord k1) -> con (KRecord k1) -> con k2 -> con k2.
adamc@615 59
adamc@615 60 Variable dvar : forall k, con (KRecord k) -> con (KRecord k) -> Type.
adamc@615 61
adamc@615 62 Section subs.
adamc@615 63 Variable k1 : kind.
adamc@615 64 Variable c1 : con k1.
adamc@615 65
adamc@615 66 Inductive subs : forall k2, (cvar k1 -> con k2) -> con k2 -> Type :=
adamc@615 67 | S_Unchanged : forall k2 (c2 : con k2),
adamc@615 68 subs (fun _ => c2) c2
adamc@615 69 | S_CVar : subs (fun x => CVar x) c1
adamc@615 70 | S_Arrow : forall c2 c3 c2' c3',
adamc@615 71 subs c2 c2'
adamc@615 72 -> subs c3 c3'
adamc@615 73 -> subs (fun x => Arrow (c2 x) (c3 x)) (Arrow c2' c3')
adamc@615 74 | S_Poly : forall k (c2 : cvar k1 -> cvar k -> _) (c2' : cvar k -> _),
adamc@615 75 (forall x', subs (fun x => c2 x x') (c2' x'))
adamc@615 76 -> subs (fun x => Poly (c2 x)) (Poly c2')
adamc@615 77 | S_CAbs : forall k2 k3 (c2 : cvar k1 -> cvar k2 -> con k3) (c2' : cvar k2 -> _),
adamc@615 78 (forall x', subs (fun x => c2 x x') (c2' x'))
adamc@615 79 -> subs (fun x => CAbs (c2 x)) (CAbs c2')
adamc@615 80 | S_CApp : forall k1 k2 (c2 : _ -> con (KArrow k1 k2)) c3 c2' c3',
adamc@615 81 subs c2 c2'
adamc@615 82 -> subs c3 c3'
adamc@615 83 -> subs (fun x => CApp (c2 x) (c3 x)) (CApp c2' c3')
adamc@615 84 | S_TRecord : forall c2 c2',
adamc@615 85 subs c2 c2'
adamc@615 86 -> subs (fun x => TRecord (c2 x)) (TRecord c2')
adamc@615 87 | S_CSingle : forall k2 c2 (c3 : _ -> con k2) c2' c3',
adamc@615 88 subs c2 c2'
adamc@615 89 -> subs c3 c3'
adamc@615 90 -> subs (fun x => CSingle (c2 x) (c3 x)) (CSingle c2' c3')
adamc@615 91 | S_CConcat : forall k2 (c2 c3 : _ -> con (KRecord k2)) c2' c3',
adamc@615 92 subs c2 c2'
adamc@615 93 -> subs c3 c3'
adamc@615 94 -> subs (fun x => CConcat (c2 x) (c3 x)) (CConcat c2' c3')
adamc@615 95 | S_CGuarded : forall k2 k3 (c2 c3 : _ -> con (KRecord k2)) (c4 : _ -> con k3) c2' c3' c4',
adamc@615 96 subs c2 c2'
adamc@615 97 -> subs c3 c3'
adamc@615 98 -> subs c4 c4'
adamc@615 99 -> subs (fun x => CGuarded (c2 x) (c3 x) (c4 x)) (CGuarded c2' c3' c4').
adamc@615 100 End subs.
adamc@615 101
adamc@615 102 Inductive disj : forall k, con (KRecord k) -> con (KRecord k) -> Prop :=
adamc@615 103 | DVar : forall k (c1 c2 : con (KRecord k)),
adamc@615 104 dvar c1 c2 -> disj c1 c2
adamc@615 105 | DComm : forall k (c1 c2 : con (KRecord k)),
adamc@615 106 disj c1 c2 -> disj c2 c1
adamc@615 107
adamc@615 108 | DEmpty : forall k c2,
adamc@615 109 disj (CEmpty k) c2
adamc@615 110 | DSingleKeys : forall k X1 X2 (c1 c2 : con k),
adamc@615 111 X1 <> X2
adamc@615 112 -> disj (CSingle (Name X1) c1) (CSingle (Name X2) c2)
adamc@615 113 | DSingleValues : forall k n1 n2 (c1 c2 : con k) k' (c1' c2' : con k'),
adamc@615 114 disj (CSingle n1 c1') (CSingle n2 c2')
adamc@615 115 -> disj (CSingle n1 c1) (CSingle n2 c2)
adamc@615 116
adamc@615 117 | DConcat : forall k (c1 c2 c : con (KRecord k)),
adamc@615 118 disj c1 c
adamc@615 119 -> disj c2 c
adamc@615 120 -> disj (CConcat c1 c2) c
adamc@615 121
adamc@615 122 | DEq : forall k (c1 c2 c1' : con (KRecord k)),
adamc@615 123 disj c1 c2
adamc@615 124 -> deq c1 c1'
adamc@615 125 -> disj c1' c2
adamc@615 126
adamc@615 127 with deq : forall k, con k -> con k -> Prop :=
adamc@615 128 | Eq_Beta : forall k1 k2 (c1 : cvar k1 -> con k2) c2 c1',
adamc@615 129 subs c2 c1 c1'
adamc@615 130 -> deq (CApp (CAbs c1) c2) c1'
adamc@615 131 | Eq_Refl : forall k (c : con k),
adamc@615 132 deq c c
adamc@615 133 | Eq_Comm : forall k (c1 c2 : con k),
adamc@615 134 deq c2 c1
adamc@615 135 -> deq c1 c2
adamc@615 136 | Eq_Trans : forall k (c1 c2 c3 : con k),
adamc@615 137 deq c1 c2
adamc@615 138 -> deq c2 c3
adamc@615 139 -> deq c1 c3
adamc@615 140 | Eq_Cong : forall k1 k2 c1 c1' (c2 : cvar k1 -> con k2) c2' c2'',
adamc@615 141 deq c1 c1'
adamc@615 142 -> subs c1 c2 c2'
adamc@615 143 -> subs c1' c2 c2''
adamc@615 144 -> deq c2' c2''
adamc@615 145
adamc@615 146 | Eq_Concat_Empty : forall k c,
adamc@615 147 deq (CConcat (CEmpty k) c) c
adamc@615 148 | Eq_Concat_Comm : forall k (c1 c2 : con (KRecord k)),
adamc@615 149 deq (CConcat c1 c2) (CConcat c2 c1)
adamc@615 150 | Eq_Concat_Assoc : forall k (c1 c2 c3 : con (KRecord k)),
adamc@615 151 deq (CConcat c1 (CConcat c2 c3)) (CConcat (CConcat c1 c2) c3)
adamc@615 152
adamc@615 153 | Eq_Fold_Empty : forall k1 k2 f i,
adamc@615 154 deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CEmpty _)) i
adamc@615 155 | Eq_Fold_Cons : forall k1 k2 f i c1 c2 c3,
adamc@615 156 deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CConcat (CSingle c1 c2) c3))
adamc@615 157 (CApp (CApp (CApp f c1) c2) (CApp (CApp (CApp (CFold k1 k2) f) i) c3))
adamc@615 158
adamc@615 159 | Eq_Guarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2),
adamc@615 160 disj c1 c2
adamc@615 161 -> deq (CGuarded c1 c2 c) c
adamc@615 162
adamc@615 163 | Eq_Map_Ident : forall k c,
adamc@615 164 deq (CApp (CApp (CApp (CFold k (KRecord k))
adamc@615 165 (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CVar x2)) (CVar x3))))))
adamc@615 166 (CEmpty _)) c) c
adamc@615 167 | Eq_Map_Dist : forall k1 k2 f c1 c2,
adamc@615 168 deq (CApp (CApp (CApp (CFold k1 (KRecord k2))
adamc@615 169 (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f (CVar x2))) (CVar x3))))))
adamc@615 170 (CEmpty _)) (CConcat c1 c2))
adamc@615 171 (CConcat
adamc@615 172 (CApp (CApp (CApp (CFold k1 (KRecord k2))
adamc@615 173 (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f (CVar x2))) (CVar x3))))))
adamc@615 174 (CEmpty _)) c1)
adamc@615 175 (CApp (CApp (CApp (CFold k1 (KRecord k2))
adamc@615 176 (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f (CVar x2))) (CVar x3))))))
adamc@615 177 (CEmpty _)) c2))
adamc@615 178
adamc@615 179 | Eq_Fold_Fuse : forall k1 k2 k3 f i f' c,
adamc@615 180 deq (CApp (CApp (CApp (CFold k1 k2) f) i)
adamc@615 181 (CApp (CApp (CApp (CFold k3 (KRecord k1))
adamc@615 182 (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f' (CVar x2))) (CVar x3))))))
adamc@615 183 (CEmpty _)) c))
adamc@615 184 (CApp (CApp (CApp (CFold k3 k2)
adamc@615 185 (CAbs (fun x1 => CAbs (fun x2 => CApp (CApp f (CVar x1)) (CApp f' (CVar x2))))))
adamc@615 186 i) c).
adamc@615 187
adamc@615 188 Inductive wf : forall k, con k -> Type :=
adamc@615 189 | HK_CVar : forall k (x : cvar k),
adamc@615 190 wf (CVar x)
adamc@615 191 | HK_Arrow : forall c1 c2,
adamc@615 192 wf c1 -> wf c2 -> wf (Arrow c1 c2)
adamc@615 193 | HK_Poly : forall k (c1 : cvar k -> _),
adamc@615 194 (forall x, wf (c1 x)) -> wf (Poly c1)
adamc@615 195 | HK_CAbs : forall k1 k2 (c1 : cvar k1 -> con k2),
adamc@615 196 (forall x, wf (c1 x)) -> wf (CAbs c1)
adamc@615 197 | HK_CApp : forall k1 k2 (c1 : con (KArrow k1 k2)) c2,
adamc@615 198 wf c1 -> wf c2 -> wf (CApp c1 c2)
adamc@615 199 | HK_Name : forall X,
adamc@615 200 wf (Name X)
adamc@615 201 | HK_TRecord : forall c,
adamc@615 202 wf c -> wf (TRecord c)
adamc@615 203 | HK_CEmpty : forall k,
adamc@615 204 wf (CEmpty k)
adamc@615 205 | HK_CSingle : forall k c1 (c2 : con k),
adamc@615 206 wf c1 -> wf c2 -> wf (CSingle c1 c2)
adamc@615 207 | HK_CConcat : forall k (c1 c2 : con (KRecord k)),
adamc@615 208 wf c2 -> wf c2 -> disj c1 c2 -> wf (CConcat c1 c2)
adamc@615 209 | HK_CFold : forall k1 k2,
adamc@615 210 wf (CFold k1 k2)
adamc@615 211 | HK_CGuarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2),
adamc@615 212 wf c1 -> wf c2 -> (disj c1 c2 -> wf c) -> wf (CGuarded c1 c2 c).
adamc@615 213 End vars.