Mercurial > urweb

comparison src/coq/Syntax.v @ 617:5b358e8f9f09

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
map-only syntax and semantics
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 11:23:24 -0500
parents d26d1f3acfd6
children be88d2d169f6
comparison
equal deleted inserted replaced
616:d26d1f3acfd6 617:5b358e8f9f09
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE. 25 * POSSIBILITY OF SUCH DAMAGE.
26 *) 26 *)
27 27
28 Require Import String.
29
28 Set Implicit Arguments. 30 Set Implicit Arguments.
29 31
30 32
31 Definition name := nat. 33 Definition name : Type := string.
34 Definition name_eq_dec : forall (x y : name), {x = y} + {x <> y} := string_dec.
32 35
33 36
34 (** Syntax of Featherweight Ur *) 37 (** Syntax of Featherweight Ur *)
35 38
36 Inductive kind : Type := 39 Inductive kind : Type :=
51 | Name : name -> con KName 54 | Name : name -> con KName
52 | TRecord : con (KRecord KType) -> con KType 55 | TRecord : con (KRecord KType) -> con KType
53 | CEmpty : forall k, con (KRecord k) 56 | CEmpty : forall k, con (KRecord k)
54 | CSingle : forall k, con KName -> con k -> con (KRecord k) 57 | CSingle : forall k, con KName -> con k -> con (KRecord k)
55 | CConcat : forall k, con (KRecord k) -> con (KRecord k) -> con (KRecord k) 58 | CConcat : forall k, con (KRecord k) -> con (KRecord k) -> con (KRecord k)
56 | CFold : forall k1 k2, con (KArrow (KArrow KName (KArrow k1 (KArrow k2 k2))) 59 | CMap : forall k1 k2, con (KArrow (KArrow k1 k2) (KArrow (KRecord k1) (KRecord k2)))
57 (KArrow k2 (KArrow (KRecord k1) k2)))
58 | CGuarded : forall k1 k2, con (KRecord k1) -> con (KRecord k1) -> con k2 -> con k2. 60 | CGuarded : forall k1 k2, con (KRecord k1) -> con (KRecord k1) -> con k2 -> con k2.
59 61
60 Variable dvar : forall k, con (KRecord k) -> con (KRecord k) -> Type. 62 Variable dvar : forall k, con (KRecord k) -> con (KRecord k) -> Type.
61 63
62 Section subs. 64 Section subs.
119 -> disj c2 c 121 -> disj c2 c
120 -> disj (CConcat c1 c2) c 122 -> disj (CConcat c1 c2) c
121 123
122 | DEq : forall k (c1 c2 c1' : con (KRecord k)), 124 | DEq : forall k (c1 c2 c1' : con (KRecord k)),
123 disj c1 c2 125 disj c1 c2
124 -> deq c1 c1' 126 -> deq c1' c1
125 -> disj c1' c2 127 -> disj c1' c2
126 128
127 with deq : forall k, con k -> con k -> Prop := 129 with deq : forall k, con k -> con k -> Prop :=
128 | Eq_Beta : forall k1 k2 (c1 : cvar k1 -> con k2) c2 c1', 130 | Eq_Beta : forall k1 k2 (c1 : cvar k1 -> con k2) c2 c1',
129 subs c2 c1 c1' 131 subs c2 c1 c1'
143 -> subs c1' c2 c2'' 145 -> subs c1' c2 c2''
144 -> deq c2' c2'' 146 -> deq c2' c2''
145 147
146 | Eq_Concat_Empty : forall k c, 148 | Eq_Concat_Empty : forall k c,
147 deq (CConcat (CEmpty k) c) c 149 deq (CConcat (CEmpty k) c) c
150 | Eq_Concat_Comm : forall k (c1 c2 c3 : con (KRecord k)),
151 disj c1 c2
152 -> deq (CConcat c1 c2) (CConcat c2 c1)
148 | Eq_Concat_Assoc : forall k (c1 c2 c3 : con (KRecord k)), 153 | Eq_Concat_Assoc : forall k (c1 c2 c3 : con (KRecord k)),
149 deq (CConcat c1 (CConcat c2 c3)) (CConcat (CConcat c1 c2) c3) 154 deq (CConcat c1 (CConcat c2 c3)) (CConcat (CConcat c1 c2) c3)
150 155
151 | Eq_Fold_Empty : forall k1 k2 f i, 156 | Eq_Map_Empty : forall k1 k2 f,
152 deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CEmpty _)) i 157 deq (CApp (CApp (CMap k1 k2) f) (CEmpty _)) (CEmpty _)
153 | Eq_Fold_Cons : forall k1 k2 f i c1 c2 c3, 158 | Eq_Map_Cons : forall k1 k2 f c1 c2 c3,
154 disj (CSingle c1 c2) c3 159 disj (CSingle c1 c2) c3
155 -> deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CConcat (CSingle c1 c2) c3)) 160 -> deq (CApp (CApp (CMap k1 k2) f) (CConcat (CSingle c1 c2) c3))
156 (CApp (CApp (CApp f c1) c2) (CApp (CApp (CApp (CFold k1 k2) f) i) c3)) 161 (CConcat (CSingle c1 (CApp f c2)) (CApp (CApp (CMap k1 k2) f) c3))
157 162
158 | Eq_Guarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2), 163 | Eq_Guarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2),
159 disj c1 c2 164 (*disj c1 c2
160 -> deq (CGuarded c1 c2 c) c 165 ->*) deq (CGuarded c1 c2 c) c
161 166
162 | Eq_Map_Ident : forall k c, 167 | Eq_Map_Ident : forall k c,
163 deq (CApp (CApp (CApp (CFold k (KRecord k)) 168 deq (CApp (CApp (CMap k k) (CAbs (fun x => CVar x))) c) c
164 (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CVar x2)) (CVar x3))))))
165 (CEmpty _)) c) c
166 | Eq_Map_Dist : forall k1 k2 f c1 c2, 169 | Eq_Map_Dist : forall k1 k2 f c1 c2,
167 deq (CApp (CApp (CApp (CFold k1 (KRecord k2)) 170 deq (CApp (CApp (CMap k1 k2) f) (CConcat c1 c2))
168 (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f (CVar x2))) (CVar x3)))))) 171 (CConcat (CApp (CApp (CMap k1 k2) f) c1) (CApp (CApp (CMap k1 k2) f) c2))
169 (CEmpty _)) (CConcat c1 c2)) 172 | Eq_Map_Fuse : forall k1 k2 k3 f f' c,
170 (CConcat 173 deq (CApp (CApp (CMap k2 k3) f')
171 (CApp (CApp (CApp (CFold k1 (KRecord k2)) 174 (CApp (CApp (CMap k1 k2) f) c))
172 (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f (CVar x2))) (CVar x3)))))) 175 (CApp (CApp (CMap k1 k3) (CAbs (fun x => CApp f' (CApp f (CVar x))))) c).
173 (CEmpty _)) c1)
174 (CApp (CApp (CApp (CFold k1 (KRecord k2))
175 (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f (CVar x2))) (CVar x3))))))
176 (CEmpty _)) c2))
177
178 | Eq_Fold_Fuse : forall k1 k2 k3 f i f' c,
179 deq (CApp (CApp (CApp (CFold k1 k2) f) i)
180 (CApp (CApp (CApp (CFold k3 (KRecord k1))
181 (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f' (CVar x2))) (CVar x3))))))
182 (CEmpty _)) c))
183 (CApp (CApp (CApp (CFold k3 k2)
184 (CAbs (fun x1 => CAbs (fun x2 => CApp (CApp f (CVar x1)) (CApp f' (CVar x2))))))
185 i) c).
186 End vars. 176 End vars.