Mercurial > urweb

comparison src/coq/Semantics.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
comparison
equal deleted inserted replaced
614:5891f47d7cff 615:3c77133afd9a
1 (* Copyright (c) 2009, Adam Chlipala
2 * All rights reserved.
3 *
4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met:
6 *
7 * - Redistributions of source code must retain the above copyright notice,
8 * this list of conditions and the following disclaimer.
9 * - Redistributions in binary form must reproduce the above copyright notice,
10 * this list of conditions and the following disclaimer in the documentation
11 * and/or other materials provided with the distribution.
12 * - The names of contributors may not be used to endorse or promote products
13 * derived from this software without specific prior written permission.
14 *
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
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
25 * POSSIBILITY OF SUCH DAMAGE.
26 *)
27
28 Require Import Arith List Omega TheoryList.
29
30 Require Import Syntax.
31
32 Set Implicit Arguments.
33
34
35 Section row'.
36 Variable A : Type.
37
38 Inductive row' : list name -> Type :=
39 | Nil : row' nil
40 | Cons : forall n ls, A -> AllS (lt n) ls -> row' ls -> row' (n :: ls).
41 End row'.
42
43 Implicit Arguments Nil [A].
44
45 Record row (A : Type) : Type := Row {
46 keys : list name;
47 data : row' A keys
48 }.
49
50 Inductive record' : forall ls, row' Set ls -> Set :=
51 | RNil : record' Nil
52 | RCons : forall n ls (T : Set) (pf : AllS (lt n) ls) r, T -> record' r -> record' (Cons T pf r).
53
54 Definition record (r : row Set) := record' (data r).
55
56 Fixpoint kDen (k : kind) : Type :=
57 match k with
58 | KType => Set
59 | KName => name
60 | KArrow k1 k2 => kDen k1 -> kDen k2
61 | KRecord k1 => row (kDen k1)
62 end.
63
64 Axiom cheat : forall T, T.
65
66 Fixpoint cinsert (n : name) (ls : list name) {struct ls} : list name :=
67 match ls with
68 | nil => n :: nil
69 | n' :: ls' =>
70 if eq_nat_dec n n'
71 then ls
72 else if le_lt_dec n n'
73 then n :: ls
74 else n' :: cinsert n ls'
75 end.
76
77 Hint Constructors AllS.
78 Hint Extern 1 (_ < _) => omega.
79
80 Lemma insert_front' : forall n n',
81 n <> n'
82 -> n <= n'
83 -> forall ls, AllS (lt n') ls
84 -> AllS (lt n) ls.
85 induction 3; auto.
86 Qed.
87
88 Lemma insert_front : forall n n',
89 n <> n'
90 -> n <= n'
91 -> forall ls, AllS (lt n') ls
92 -> AllS (lt n) (n' :: ls).
93 Hint Resolve insert_front'.
94 eauto.
95 Qed.
96
97 Lemma insert_continue : forall n n',
98 n <> n'
99 -> n' < n
100 -> forall ls, AllS (lt n') ls
101 -> AllS (lt n') (cinsert n ls).
102 induction 3; simpl; auto;
103 repeat (match goal with
104 | [ |- context[if ?E then _ else _] ] => destruct E
105 end; auto).
106 Qed.
107
108 Fixpoint insert T (n : name) (v : T) ls (r : row' T ls) {struct r} : row' T (cinsert n ls) :=
109 match r in row' _ ls return row' T (cinsert n ls) with
110 | Nil => Cons (n := n) v (allS_nil _) Nil
111 | Cons n' ls' v' pf r' =>
112 match eq_nat_dec n n' as END
113 return row' _ (if END then _ else _) with
114 | left _ => Cons (n := n') v' pf r'
115 | right pfNe =>
116 match le_lt_dec n n' as LLD
117 return row' _ (if LLD then _ else _) with
118 | left pfLe => Cons (n := n) v (insert_front pfNe pfLe pf) (Cons (n := n') v' pf r')
119 | right pfLt => Cons (n := n') v' (insert_continue pfNe pfLt pf) (insert n v r')
120 end
121 end
122 end.
123
124 Fixpoint cconcat (ls1 ls2 : list name) {struct ls1} : list name :=
125 match ls1 with
126 | nil => ls2
127 | n :: ls1' => cinsert n (cconcat ls1' ls2)
128 end.
129
130 Fixpoint concat T ls1 ls2 (r1 : row' T ls1) (r2 : row' T ls2) {struct r1} : row' T (cconcat ls1 ls2) :=
131 match r1 in row' _ ls1 return row' _ (cconcat ls1 _) with
132 | Nil => r2
133 | Cons n _ v _ r1' => insert n v (concat r1' r2)
134 end.
135
136 Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') ls (r : row' T ls) {struct r} : T' :=
137 match r with
138 | Nil => i
139 | Cons n _ v _ r' => f n v (cfold f i r')
140 end.
141
142 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
143 match c in con _ k return kDen k with
144 | CVar _ x => x
145 | Arrow c1 c2 => cDen c1 -> cDen c2
146 | Poly _ c1 => forall x, cDen (c1 x)
147 | CAbs _ _ c1 => fun x => cDen (c1 x)
148 | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
149 | Name n => n
150 | TRecord c1 => record (cDen c1)
151 | CEmpty _ => Row Nil
152 | CSingle _ c1 c2 => Row (Cons (n := cDen c1) (cDen c2) (allS_nil _) Nil)
153 | CConcat _ c1 c2 => Row (concat (data (cDen c1)) (data (cDen c2)))
154 | CFold k1 k2 => fun f i r => cfold f i (data r)
155 | CGuarded _ _ _ _ c => cDen c
156 end.