summaryrefslogtreecommitdiff
path: root/src/coq/Semantics.v
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-17 14:49:28 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-17 14:49:28 -0500
commit3c534cfde2dea5384113b891362bbfc1ee6b98fe (patch)
tree22617c1ba004461a1162b9349d44e94b8b65f507 /src/coq/Semantics.v
parent4f0987ddef3dc105c3883aa9c1c69c29fbe86a8a (diff)
Start of Featherweight Ur semantics
Diffstat (limited to 'src/coq/Semantics.v')
-rw-r--r--src/coq/Semantics.v156
1 files changed, 156 insertions, 0 deletions
diff --git a/src/coq/Semantics.v b/src/coq/Semantics.v
new file mode 100644
index 00000000..c3e99b5d
--- /dev/null
+++ b/src/coq/Semantics.v
@@ -0,0 +1,156 @@
+(* Copyright (c) 2009, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ * this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ * this list of conditions and the following disclaimer in the documentation
+ * and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ * derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+Require Import Arith List Omega TheoryList.
+
+Require Import Syntax.
+
+Set Implicit Arguments.
+
+
+Section row'.
+ Variable A : Type.
+
+ Inductive row' : list name -> Type :=
+ | Nil : row' nil
+ | Cons : forall n ls, A -> AllS (lt n) ls -> row' ls -> row' (n :: ls).
+End row'.
+
+Implicit Arguments Nil [A].
+
+Record row (A : Type) : Type := Row {
+ keys : list name;
+ data : row' A keys
+}.
+
+Inductive record' : forall ls, row' Set ls -> Set :=
+| RNil : record' Nil
+| RCons : forall n ls (T : Set) (pf : AllS (lt n) ls) r, T -> record' r -> record' (Cons T pf r).
+
+Definition record (r : row Set) := record' (data r).
+
+Fixpoint kDen (k : kind) : Type :=
+ match k with
+ | KType => Set
+ | KName => name
+ | KArrow k1 k2 => kDen k1 -> kDen k2
+ | KRecord k1 => row (kDen k1)
+ end.
+
+Axiom cheat : forall T, T.
+
+Fixpoint cinsert (n : name) (ls : list name) {struct ls} : list name :=
+ match ls with
+ | nil => n :: nil
+ | n' :: ls' =>
+ if eq_nat_dec n n'
+ then ls
+ else if le_lt_dec n n'
+ then n :: ls
+ else n' :: cinsert n ls'
+ end.
+
+Hint Constructors AllS.
+Hint Extern 1 (_ < _) => omega.
+
+Lemma insert_front' : forall n n',
+ n <> n'
+ -> n <= n'
+ -> forall ls, AllS (lt n') ls
+ -> AllS (lt n) ls.
+ induction 3; auto.
+Qed.
+
+Lemma insert_front : forall n n',
+ n <> n'
+ -> n <= n'
+ -> forall ls, AllS (lt n') ls
+ -> AllS (lt n) (n' :: ls).
+ Hint Resolve insert_front'.
+ eauto.
+Qed.
+
+Lemma insert_continue : forall n n',
+ n <> n'
+ -> n' < n
+ -> forall ls, AllS (lt n') ls
+ -> AllS (lt n') (cinsert n ls).
+ induction 3; simpl; auto;
+ repeat (match goal with
+ | [ |- context[if ?E then _ else _] ] => destruct E
+ end; auto).
+Qed.
+
+Fixpoint insert T (n : name) (v : T) ls (r : row' T ls) {struct r} : row' T (cinsert n ls) :=
+ match r in row' _ ls return row' T (cinsert n ls) with
+ | Nil => Cons (n := n) v (allS_nil _) Nil
+ | Cons n' ls' v' pf r' =>
+ match eq_nat_dec n n' as END
+ return row' _ (if END then _ else _) with
+ | left _ => Cons (n := n') v' pf r'
+ | right pfNe =>
+ match le_lt_dec n n' as LLD
+ return row' _ (if LLD then _ else _) with
+ | left pfLe => Cons (n := n) v (insert_front pfNe pfLe pf) (Cons (n := n') v' pf r')
+ | right pfLt => Cons (n := n') v' (insert_continue pfNe pfLt pf) (insert n v r')
+ end
+ end
+ end.
+
+Fixpoint cconcat (ls1 ls2 : list name) {struct ls1} : list name :=
+ match ls1 with
+ | nil => ls2
+ | n :: ls1' => cinsert n (cconcat ls1' ls2)
+ end.
+
+Fixpoint concat T ls1 ls2 (r1 : row' T ls1) (r2 : row' T ls2) {struct r1} : row' T (cconcat ls1 ls2) :=
+ match r1 in row' _ ls1 return row' _ (cconcat ls1 _) with
+ | Nil => r2
+ | Cons n _ v _ r1' => insert n v (concat r1' r2)
+ end.
+
+Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') ls (r : row' T ls) {struct r} : T' :=
+ match r with
+ | Nil => i
+ | Cons n _ v _ r' => f n v (cfold f i r')
+ end.
+
+Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
+ match c in con _ k return kDen k with
+ | CVar _ x => x
+ | Arrow c1 c2 => cDen c1 -> cDen c2
+ | Poly _ c1 => forall x, cDen (c1 x)
+ | CAbs _ _ c1 => fun x => cDen (c1 x)
+ | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
+ | Name n => n
+ | TRecord c1 => record (cDen c1)
+ | CEmpty _ => Row Nil
+ | CSingle _ c1 c2 => Row (Cons (n := cDen c1) (cDen c2) (allS_nil _) Nil)
+ | CConcat _ c1 c2 => Row (concat (data (cDen c1)) (data (cDen c2)))
+ | CFold k1 k2 => fun f i r => cfold f i (data r)
+ | CGuarded _ _ _ _ c => cDen c
+ end.