# HG changeset patch # User Adam Chlipala # Date 1227030286 18000 # Node ID 094bd1e353dd868a04a034fca7ef2678647c30dd # Parent 0198181d1b647bb86e7bceffbe7a541979cc8697 Import predicative Impure example diff -r 0198181d1b64 -r 094bd1e353dd Makefile --- a/Makefile Mon Nov 17 10:36:02 2008 -0500 +++ b/Makefile Tue Nov 18 12:44:46 2008 -0500 @@ -2,7 +2,7 @@ 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) diff -r 0198181d1b64 -r 094bd1e353dd src/Axioms.v --- a/src/Axioms.v Mon Nov 17 10:36:02 2008 -0500 +++ b/src/Axioms.v Tue Nov 18 12:44:46 2008 -0500 @@ -34,3 +34,9 @@ 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. diff -r 0198181d1b64 -r 094bd1e353dd src/Impure.v --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Impure.v Tue Nov 18 12:44:46 2008 -0500 @@ -0,0 +1,164 @@ +(* 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. diff -r 0198181d1b64 -r 094bd1e353dd src/Intro.v --- a/src/Intro.v Mon Nov 17 10:36:02 2008 -0500 +++ b/src/Intro.v Tue Nov 18 12:44:46 2008 -0500 @@ -213,6 +213,8 @@ \hline Intensional Transformations & \texttt{Intensional.v} \\ \hline +Modeling Impure Languages & \texttt{Impure.v} \\ +\hline \end{tabular} \end{center} % *) diff -r 0198181d1b64 -r 094bd1e353dd src/toc.html --- a/src/toc.html Mon Nov 17 10:36:02 2008 -0500 +++ b/src/toc.html Tue Nov 18 12:44:46 2008 -0500 @@ -20,5 +20,6 @@
  • Type-Theoretic Interpreters
  • Extensional Transformations
  • Intensional Transformations +
  • Modeling Impure Languages