Import predicative Impure example

Makefile

@@ -2,7 +2,7 @@ MODULES_NODOC := Axioms AxiomsImpred Tactics MoreSpecif DepList
 MODULES_PROSE := Intro
 MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
 	MoreDep DataStruct Equality Match Reflection Firstorder Hoas Interps \
-	Extensional Intensional
+	Extensional Intensional Impure
 MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE)
 MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
 VS            := $(MODULES:%=src/%.v)

src/Axioms.v

@@ -34,3 +34,9 @@ Qed.
 
 Ltac ext_eq := (apply ext_eq || apply ext_eq_Set
   || apply ext_eq_forall); intro.
+
+
+Theorem eta : forall (A B : Type) (f : A -> B),
+  (fun x => f x) = f.
+  intros; ext_eq; trivial.
+Qed.

src/Impure.v

+(* Copyright (c) 2008, Adam Chlipala
+ * 
+ * This work is licensed under a
+ * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+ * Unported License.
+ * The license text is available at:
+ *   http://creativecommons.org/licenses/by-nc-nd/3.0/
+ *)
+
+(* begin hide *)
+Require Import Arith List Omega.
+
+Require Import Axioms Tactics.
+
+Set Implicit Arguments.
+(* end hide *)
+
+
+(** %\chapter{Modeling Impure Languages}% *)
+
+(** TODO: Prose for this chapter *)
+
+Section var.
+  Variable var : Type.
+
+  Inductive term : Type :=
+  | Var : var -> term
+  | App : term -> term -> term
+  | Abs : (var -> term) -> term
+  | Unit : term.
+End var.
+
+Implicit Arguments Unit [var].
+
+Notation "# v" := (Var v) (at level 70).
+Notation "()" := Unit.
+
+Infix "@" := App (left associativity, at level 72).
+Notation "\ x , e" := (Abs (fun x => e)) (at level 73).
+Notation "\ ? , e" := (Abs (fun _ => e)) (at level 73).
+
+
+Module predicative.
+
+  Inductive val : Type :=
+  | Func : nat -> val
+  | VUnit.
+
+  Inductive computation : Type :=
+  | Return : val -> computation
+  | Bind : computation -> (val -> computation) -> computation
+  | CAbs : (val -> computation) -> computation
+  | CApp : val -> val -> computation.
+
+  Definition func := val -> computation.
+
+  Fixpoint get (n : nat) (ls : list func) {struct ls} : option func :=
+    match ls with
+      | nil => None
+      | x :: ls' =>
+        if eq_nat_dec n (length ls')
+          then Some x
+          else get n ls'
+    end.
+
+  Inductive eval : list func -> computation -> list func -> val -> Prop :=
+  | EvalReturn : forall ds d,
+    eval ds (Return d) ds d
+  | EvalBind : forall ds c1 c2 ds' d1 ds'' d2,
+    eval ds c1 ds' d1
+    -> eval ds' (c2 d1) ds'' d2
+    -> eval ds (Bind c1 c2) ds'' d2
+  | EvalCAbs : forall ds f,
+    eval ds (CAbs f) (f :: ds) (Func (length ds))
+  | EvalCApp : forall ds i d2 f ds' d3,
+    get i ds = Some f
+    -> eval ds (f d2) ds' d3
+    -> eval ds (CApp (Func i) d2) ds' d3.
+
+  Fixpoint termDenote (e : term val) : computation :=
+    match e with
+      | Var v => Return v
+      | App e1 e2 => Bind (termDenote e1) (fun f =>
+        Bind (termDenote e2) (fun x =>
+          CApp f x))
+      | Abs e' => CAbs (fun x => termDenote (e' x))
+
+      | Unit => Return VUnit
+    end.
+
+  Definition Term := forall var, term var.
+  Definition TermDenote (E : Term) := termDenote (E _).
+
+  Definition ident : Term := fun _ => \x, #x.
+  Eval compute in TermDenote ident.
+
+  Definition unite : Term := fun _ => ().
+  Eval compute in TermDenote unite.
+
+  Definition ident_self : Term := fun _ => ident _ @ ident _.
+  Eval compute in TermDenote ident_self.
+
+  Definition ident_unit : Term := fun _ => ident _ @ unite _.
+  Eval compute in TermDenote ident_unit.
+
+  Theorem eval_ident_unit : exists ds, eval nil (TermDenote ident_unit) ds VUnit.
+    compute.
+    repeat econstructor.
+    simpl.
+    rewrite (eta Return).
+    reflexivity.
+  Qed.
+
+  Hint Constructors eval.
+
+  Lemma app_nil_start : forall A (ls : list A),
+    ls = nil ++ ls.
+    reflexivity.
+  Qed.
+
+  Lemma app_cons : forall A (x : A) (ls : list A),
+    x :: ls = (x :: nil) ++ ls.
+    reflexivity.
+  Qed.
+
+  Theorem eval_monotone : forall ds c ds' d,
+    eval ds c ds' d
+    -> exists ds'', ds' = ds'' ++ ds.
+    Hint Resolve app_nil_start app_ass app_cons.
+
+    induction 1; firstorder; subst; eauto.
+  Qed.
+
+  Lemma length_app : forall A (ds2 ds1 : list A),
+    length (ds1 ++ ds2) = length ds1 + length ds2.
+    induction ds1; simpl; intuition.
+  Qed.
+
+  Lemma get_app : forall ds2 d ds1,
+    get (length ds2) (ds1 ++ d :: ds2) = Some d.
+    Hint Rewrite length_app : cpdt.
+
+    induction ds1; crush;
+      match goal with
+        | [ |- context[if ?E then _ else _] ] => destruct E
+      end; crush.
+  Qed.
+
+  Theorem invert_ident : forall (E : Term) ds ds' d,
+    eval ds (TermDenote (fun _ => ident _ @ E _)) ds' d
+    -> eval ((fun x => Return x) :: ds) (TermDenote E) ds' d.
+    inversion 1; subst.
+    clear H.
+    inversion H3; clear H3; subst.
+    inversion H6; clear H6; subst.
+    generalize (eval_monotone H2); crush.
+    inversion H5; clear H5; subst.
+    rewrite get_app in H3.
+    inversion H3; clear H3; subst.
+    inversion H7; clear H7; subst.
+    assumption.
+  Qed.
+
+End predicative.

src/Intro.v

@@ -213,6 +213,8 @@ Extensional Transformations & \texttt{Extensional.v} \\
 \hline
 Intensional Transformations & \texttt{Intensional.v} \\
 \hline
+Modeling Impure Languages & \texttt{Impure.v} \\
+\hline
 \end{tabular} \end{center}
 
 % *)

src/toc.html

@@ -20,5 +20,6 @@
 <li><a href="Interps.html">Type-Theoretic Interpreters</a>
 <li><a href="Extensional.html">Extensional Transformations</a>
 <li><a href="Intensional.html">Intensional Transformations</a>
+<li><a href="Impure.html">Modeling Impure Languages</a>
 
 </body></html>