Mercurial > urweb

comparison src/coq/Syntax.v @ 620:d828b143e147

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish semantics for Featherweight Ur
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 14:10:06 -0500
parents f38e009009bb
children 75c7a69354d6
comparison
equal deleted inserted replaced
619:f38e009009bb 620:d828b143e147
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. 28 Require Import Name.
29 Export Name.
29 30
30 Set Implicit Arguments. 31 Set Implicit Arguments.
31
32
33 Definition name : Type := string.
34 Definition name_eq_dec : forall (x y : name), {x = y} + {x <> y} := string_dec.
35 32
36 33
37 (** Syntax of Featherweight Ur *) 34 (** Syntax of Featherweight Ur *)
38 35
39 Inductive kind : Type := 36 Inductive kind : Type :=
158 | Eq_Map_Cons : forall k1 k2 f c1 c2 c3, 155 | Eq_Map_Cons : forall k1 k2 f c1 c2 c3,
159 disj (CSingle c1 c2) c3 156 disj (CSingle c1 c2) c3
160 -> deq (CApp (CApp (CMap k1 k2) f) (CConcat (CSingle c1 c2) c3)) 157 -> deq (CApp (CApp (CMap k1 k2) f) (CConcat (CSingle c1 c2) c3))
161 (CConcat (CSingle c1 (CApp f c2)) (CApp (CApp (CMap k1 k2) f) c3)) 158 (CConcat (CSingle c1 (CApp f c2)) (CApp (CApp (CMap k1 k2) f) c3))
162 159
163 | Eq_Guarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2), 160 | Eq_Guarded_Remove : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2),
164 (*disj c1 c2 161 disj c1 c2
165 ->*) deq (CGuarded c1 c2 c) c 162 -> deq (CGuarded c1 c2 c) c
163 | Eq_Guarded_Cong : forall k1 k2 (c1 c2 : con (KRecord k1)) (c c' : con k2),
164 (dvar c1 c2 -> deq c c')
165 -> deq (CGuarded c1 c2 c) (CGuarded c1 c2 c')
166 166
167 | Eq_Map_Ident : forall k c, 167 | Eq_Map_Ident : forall k c,
168 deq (CApp (CApp (CMap k k) (CAbs (fun x => CVar x))) c) c 168 deq (CApp (CApp (CMap k k) (CAbs (fun x => CVar x))) c) c
169 | Eq_Map_Dist : forall k1 k2 f c1 c2, 169 | Eq_Map_Dist : forall k1 k2 f c1 c2,
170 deq (CApp (CApp (CMap k1 k2) f) (CConcat c1 c2)) 170 deq (CApp (CApp (CMap k1 k2) f) (CConcat c1 c2))