Mercurial > urweb

annotate src/coq/Syntax.v @ 2191:849404a3af27

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Change behavior of SQL equality to do the intuitive thing for nullable types
author Adam Chlipala <adam@chlipala.net>
date Sun, 01 Nov 2015 17:02:16 -0500
parents 75c7a69354d6
children
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@620 28 Require Import Name.
adamc@620 29 Export Name.
adamc@617 30
adamc@615 31 Set Implicit Arguments.
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@617 56 | CMap : forall k1 k2, con (KArrow (KArrow k1 k2) (KArrow (KRecord k1) (KRecord k2)))
adamc@635 57 | TGuarded : forall k, con (KRecord k) -> con (KRecord k) -> con KType -> con KType.
adamc@615 58
adamc@615 59 Variable dvar : forall k, con (KRecord k) -> con (KRecord k) -> Type.
adamc@615 60
adamc@615 61 Section subs.
adamc@615 62 Variable k1 : kind.
adamc@615 63 Variable c1 : con k1.
adamc@615 64
adamc@615 65 Inductive subs : forall k2, (cvar k1 -> con k2) -> con k2 -> Type :=
adamc@615 66 | S_Unchanged : forall k2 (c2 : con k2),
adamc@615 67 subs (fun _ => c2) c2
adamc@615 68 | S_CVar : subs (fun x => CVar x) c1
adamc@615 69 | S_Arrow : forall c2 c3 c2' c3',
adamc@615 70 subs c2 c2'
adamc@615 71 -> subs c3 c3'
adamc@615 72 -> subs (fun x => Arrow (c2 x) (c3 x)) (Arrow c2' c3')
adamc@615 73 | S_Poly : forall k (c2 : cvar k1 -> cvar k -> _) (c2' : cvar k -> _),
adamc@615 74 (forall x', subs (fun x => c2 x x') (c2' x'))
adamc@615 75 -> subs (fun x => Poly (c2 x)) (Poly c2')
adamc@615 76 | S_CAbs : forall k2 k3 (c2 : cvar k1 -> cvar k2 -> con k3) (c2' : cvar k2 -> _),
adamc@615 77 (forall x', subs (fun x => c2 x x') (c2' x'))
adamc@615 78 -> subs (fun x => CAbs (c2 x)) (CAbs c2')
adamc@615 79 | S_CApp : forall k1 k2 (c2 : _ -> con (KArrow k1 k2)) c3 c2' c3',
adamc@615 80 subs c2 c2'
adamc@615 81 -> subs c3 c3'
adamc@615 82 -> subs (fun x => CApp (c2 x) (c3 x)) (CApp c2' c3')
adamc@615 83 | S_TRecord : forall c2 c2',
adamc@615 84 subs c2 c2'
adamc@615 85 -> subs (fun x => TRecord (c2 x)) (TRecord c2')
adamc@615 86 | S_CSingle : forall k2 c2 (c3 : _ -> con k2) c2' c3',
adamc@615 87 subs c2 c2'
adamc@615 88 -> subs c3 c3'
adamc@615 89 -> subs (fun x => CSingle (c2 x) (c3 x)) (CSingle c2' c3')
adamc@615 90 | S_CConcat : forall k2 (c2 c3 : _ -> con (KRecord k2)) c2' c3',
adamc@615 91 subs c2 c2'
adamc@615 92 -> subs c3 c3'
adamc@615 93 -> subs (fun x => CConcat (c2 x) (c3 x)) (CConcat c2' c3')
adamc@635 94 | S_TGuarded : forall k2 (c2 c3 : _ -> con (KRecord k2)) c4 c2' c3' c4',
adamc@615 95 subs c2 c2'
adamc@615 96 -> subs c3 c3'
adamc@615 97 -> subs c4 c4'
adamc@635 98 -> subs (fun x => TGuarded (c2 x) (c3 x) (c4 x)) (TGuarded c2' c3' c4').
adamc@615 99 End subs.
adamc@615 100
adamc@615 101 Inductive disj : forall k, con (KRecord k) -> con (KRecord k) -> Prop :=
adamc@615 102 | DVar : forall k (c1 c2 : con (KRecord k)),
adamc@615 103 dvar c1 c2 -> disj c1 c2
adamc@615 104 | DComm : forall k (c1 c2 : con (KRecord k)),
adamc@615 105 disj c1 c2 -> disj c2 c1
adamc@615 106
adamc@615 107 | DEmpty : forall k c2,
adamc@615 108 disj (CEmpty k) c2
adamc@615 109 | DSingleKeys : forall k X1 X2 (c1 c2 : con k),
adamc@615 110 X1 <> X2
adamc@615 111 -> disj (CSingle (Name X1) c1) (CSingle (Name X2) c2)
adamc@615 112 | DSingleValues : forall k n1 n2 (c1 c2 : con k) k' (c1' c2' : con k'),
adamc@615 113 disj (CSingle n1 c1') (CSingle n2 c2')
adamc@615 114 -> disj (CSingle n1 c1) (CSingle n2 c2)
adamc@615 115
adamc@615 116 | DConcat : forall k (c1 c2 c : con (KRecord k)),
adamc@615 117 disj c1 c
adamc@615 118 -> disj c2 c
adamc@615 119 -> disj (CConcat c1 c2) c
adamc@615 120
adamc@615 121 | DEq : forall k (c1 c2 c1' : con (KRecord k)),
adamc@615 122 disj c1 c2
adamc@617 123 -> deq c1' c1
adamc@615 124 -> disj c1' c2
adamc@615 125
adamc@615 126 with deq : forall k, con k -> con k -> Prop :=
adamc@615 127 | Eq_Beta : forall k1 k2 (c1 : cvar k1 -> con k2) c2 c1',
adamc@615 128 subs c2 c1 c1'
adamc@615 129 -> deq (CApp (CAbs c1) c2) c1'
adamc@615 130 | Eq_Refl : forall k (c : con k),
adamc@615 131 deq c c
adamc@615 132 | Eq_Comm : forall k (c1 c2 : con k),
adamc@615 133 deq c2 c1
adamc@615 134 -> deq c1 c2
adamc@615 135 | Eq_Trans : forall k (c1 c2 c3 : con k),
adamc@615 136 deq c1 c2
adamc@615 137 -> deq c2 c3
adamc@615 138 -> deq c1 c3
adamc@615 139 | Eq_Cong : forall k1 k2 c1 c1' (c2 : cvar k1 -> con k2) c2' c2'',
adamc@615 140 deq c1 c1'
adamc@615 141 -> subs c1 c2 c2'
adamc@615 142 -> subs c1' c2 c2''
adamc@615 143 -> deq c2' c2''
adamc@615 144
adamc@615 145 | Eq_Concat_Empty : forall k c,
adamc@615 146 deq (CConcat (CEmpty k) c) c
adamc@617 147 | Eq_Concat_Comm : forall k (c1 c2 c3 : con (KRecord k)),
adamc@617 148 disj c1 c2
adamc@617 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@617 153 | Eq_Map_Empty : forall k1 k2 f,
adamc@617 154 deq (CApp (CApp (CMap k1 k2) f) (CEmpty _)) (CEmpty _)
adamc@617 155 | Eq_Map_Cons : forall k1 k2 f c1 c2 c3,
adamc@616 156 disj (CSingle c1 c2) c3
adamc@617 157 -> deq (CApp (CApp (CMap k1 k2) f) (CConcat (CSingle c1 c2) c3))
adamc@617 158 (CConcat (CSingle c1 (CApp f c2)) (CApp (CApp (CMap k1 k2) f) c3))
adamc@615 159
adamc@615 160 | Eq_Map_Ident : forall k c,
adamc@617 161 deq (CApp (CApp (CMap k k) (CAbs (fun x => CVar x))) c) c
adamc@615 162 | Eq_Map_Dist : forall k1 k2 f c1 c2,
adamc@617 163 deq (CApp (CApp (CMap k1 k2) f) (CConcat c1 c2))
adamc@617 164 (CConcat (CApp (CApp (CMap k1 k2) f) c1) (CApp (CApp (CMap k1 k2) f) c2))
adamc@617 165 | Eq_Map_Fuse : forall k1 k2 k3 f f' c,
adamc@617 166 deq (CApp (CApp (CMap k2 k3) f')
adamc@617 167 (CApp (CApp (CMap k1 k2) f) c))
adamc@617 168 (CApp (CApp (CMap k1 k3) (CAbs (fun x => CApp f' (CApp f (CVar x))))) c).
adamc@618 169
adamc@618 170 Variable evar : con KType -> Type.
adamc@618 171
adamc@618 172 Inductive exp : con KType -> Type :=
adamc@618 173 | Var : forall t, evar t -> exp t
adamc@618 174 | App : forall dom ran, exp (Arrow dom ran) -> exp dom -> exp ran
adamc@618 175 | Abs : forall dom ran, (evar dom -> exp ran) -> exp (Arrow dom ran)
adamc@618 176 | ECApp : forall k (dom : con k) ran ran', exp (Poly ran) -> subs dom ran ran' -> exp ran'
adamc@618 177 | ECAbs : forall k (ran : cvar k -> _), (forall X, exp (ran X)) -> exp (Poly ran)
adamc@618 178 | Cast : forall t1 t2, deq t1 t2 -> exp t1 -> exp t2
adamc@618 179 | Empty : exp (TRecord (CEmpty _))
adamc@618 180 | Single : forall c t, exp t -> exp (TRecord (CConcat (CSingle c t) (CEmpty _)))
adamc@618 181 | Proj : forall c t c', exp (TRecord (CConcat (CSingle c t) c')) -> exp t
adamc@618 182 | Cut : forall c t c', disj (CSingle c t) c' -> exp (TRecord (CConcat (CSingle c t) c')) -> exp (TRecord c')
adamc@619 183 | Concat : forall c1 c2, exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2))
adamc@635 184 | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (TGuarded c1 c2 c)
adamc@635 185 | GuardedApp : forall k (c1 c2 : con (KRecord k)) t, exp (TGuarded c1 c2 t) -> disj c1 c2 -> exp t.
adamc@615 186 End vars.