# HG changeset patch # User Adam Chlipala # Date 1226854491 18000 # Node ID 24b99e025fe8def4852838a38f7a071e58892ba5 # Parent ec44782bffdd0f7cb2beaae14c9331a69de41b2d Start of Intensional diff -r ec44782bffdd -r 24b99e025fe8 Makefile --- a/Makefile Mon Nov 10 17:27:55 2008 -0500 +++ b/Makefile Sun Nov 16 11:54:51 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 + Extensional Intensional MODULES_DOC := $(MODULES_PROSE) $(MODULES_CODE) MODULES := $(MODULES_NODOC) $(MODULES_DOC) VS := $(MODULES:%=src/%.v) diff -r ec44782bffdd -r 24b99e025fe8 src/Extensional.v --- a/src/Extensional.v Mon Nov 10 17:27:55 2008 -0500 +++ b/src/Extensional.v Sun Nov 16 11:54:51 2008 -0500 @@ -10,7 +10,7 @@ (* begin hide *) Require Import String List. -Require Import AxiomsImpred Tactics DepList. +Require Import Axioms Tactics DepList. Set Implicit Arguments. (* end hide *) diff -r ec44782bffdd -r 24b99e025fe8 src/Intensional.v --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Intensional.v Sun Nov 16 11:54:51 2008 -0500 @@ -0,0 +1,271 @@ +(* 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 String List. + +Require Import Axioms Tactics DepList. + +Set Implicit Arguments. +(* end hide *) + + +(** %\chapter{Intensional Transformations}% *) + +(** TODO: Prose for this chapter *) + + +(** * Closure Conversion *) + +Module Source. + Inductive type : Type := + | TNat : type + | Arrow : type -> type -> type. + + Notation "'Nat'" := TNat : source_scope. + Infix "-->" := Arrow (right associativity, at level 60) : source_scope. + + Open Scope source_scope. + Bind Scope source_scope with type. + Delimit Scope source_scope with source. + + Section vars. + Variable var : type -> Type. + + Inductive exp : type -> Type := + | Var : forall t, + var t + -> exp t + + | Const : nat -> exp Nat + | Plus : exp Nat -> exp Nat -> exp Nat + + | App : forall t1 t2, + exp (t1 --> t2) + -> exp t1 + -> exp t2 + | Abs : forall t1 t2, + (var t1 -> exp t2) + -> exp (t1 --> t2). + End vars. + + Definition Exp t := forall var, exp var t. + + Implicit Arguments Var [var t]. + Implicit Arguments Const [var]. + Implicit Arguments Plus [var]. + Implicit Arguments App [var t1 t2]. + Implicit Arguments Abs [var t1 t2]. + + Notation "# v" := (Var v) (at level 70) : source_scope. + + Notation "^ n" := (Const n) (at level 70) : source_scope. + Infix "+^" := Plus (left associativity, at level 79) : source_scope. + + Infix "@" := App (left associativity, at level 77) : source_scope. + Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope. + Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope. + + Bind Scope source_scope with exp. + + Definition zero : Exp Nat := fun _ => ^0. + Definition one : Exp Nat := fun _ => ^1. + Definition zpo : Exp Nat := fun _ => zero _ +^ one _. + Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x. + Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _. + Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => + \f, \x, #f @ #x. + Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _. + + Fixpoint typeDenote (t : type) : Set := + match t with + | Nat => nat + | t1 --> t2 => typeDenote t1 -> typeDenote t2 + end. + + Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := + match e in (exp _ t) return (typeDenote t) with + | Var _ v => v + + | Const n => n + | Plus e1 e2 => expDenote e1 + expDenote e2 + + | App _ _ e1 e2 => (expDenote e1) (expDenote e2) + | Abs _ _ e' => fun x => expDenote (e' x) + end. + + Definition ExpDenote t (e : Exp t) := expDenote (e _). + + Section exp_equiv. + Variables var1 var2 : type -> Type. + + Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop := + | EqVar : forall G t (v1 : var1 t) v2, + In (existT _ t (v1, v2)) G + -> exp_equiv G (#v1) (#v2) + + | EqConst : forall G n, + exp_equiv G (^n) (^n) + | EqPlus : forall G x1 y1 x2 y2, + exp_equiv G x1 x2 + -> exp_equiv G y1 y2 + -> exp_equiv G (x1 +^ y1) (x2 +^ y2) + + | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2, + exp_equiv G f1 f2 + -> exp_equiv G x1 x2 + -> exp_equiv G (f1 @ x1) (f2 @ x2) + | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2, + (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2)) + -> exp_equiv G (Abs f1) (Abs f2). + End exp_equiv. + + Axiom Exp_equiv : forall t (E : Exp t) var1 var2, + exp_equiv nil (E var1) (E var2). +End Source. + +Section Closed. + Inductive type : Type := + | TNat : type + | Arrow : type -> type -> type + | Code : type -> type -> type -> type + | Prod : type -> type -> type + | TUnit : type. + + Notation "'Nat'" := TNat : cc_scope. + Notation "'Unit'" := TUnit : cc_scope. + Infix "-->" := Arrow (right associativity, at level 60) : cc_scope. + Infix "**" := Prod (right associativity, at level 59) : cc_scope. + Notation "env @@ dom ---> ran" := (Code env dom ran) (no associativity, at level 62, dom at next level) : cc_scope. + + Bind Scope cc_scope with type. + Delimit Scope cc_scope with cc. + + Open Local Scope cc_scope. + + Section vars. + Variable var : type -> Set. + + Inductive exp : type -> Type := + | Var : forall t, + var t + -> exp t + + | Const : nat -> exp Nat + | Plus : exp Nat -> exp Nat -> exp Nat + + | App : forall dom ran, + exp (dom --> ran) + -> exp dom + -> exp ran + + | Pack : forall env dom ran, + exp (env @@ dom ---> ran) + -> exp env + -> exp (dom --> ran) + + | EUnit : exp Unit + + | Pair : forall t1 t2, + exp t1 + -> exp t2 + -> exp (t1 ** t2) + | Fst : forall t1 t2, + exp (t1 ** t2) + -> exp t1 + | Snd : forall t1 t2, + exp (t1 ** t2) + -> exp t2. + + Section funcs. + Variable T : Type. + + Inductive funcs : Type := + | Main : T -> funcs + | Abs : forall env dom ran, + (var env -> var dom -> exp ran) + -> (var (env @@ dom ---> ran) -> funcs) + -> funcs. + End funcs. + + Definition prog t := funcs (exp t). + End vars. + + Implicit Arguments Var [var t]. + Implicit Arguments Const [var]. + Implicit Arguments EUnit [var]. + Implicit Arguments Fst [var t1 t2]. + Implicit Arguments Snd [var t1 t2]. + + Implicit Arguments Main [var T]. + Implicit Arguments Abs [var T env dom ran]. + + Notation "# v" := (Var v) (at level 70) : cc_scope. + + Notation "^ n" := (Const n) (at level 70) : cc_scope. + Infix "+^" := Plus (left associativity, at level 79) : cc_scope. + + Infix "@@" := App (no associativity, at level 75) : cc_scope. + Infix "##" := Pack (no associativity, at level 71) : cc_scope. + + Notation "()" := EUnit : cc_scope. + + Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : cc_scope. + Notation "#1 x" := (Fst x) (at level 72) : cc_scope. + Notation "#2 x" := (Snd x) (at level 72) : cc_scope. + + Notation "f <= \\ x , y , e ; fs" := + (Abs (fun x y => e) (fun f => fs)) + (right associativity, at level 80, e at next level) : cc_scope. + + Bind Scope cc_scope with exp funcs prog. + + Fixpoint typeDenote (t : type) : Set := + match t with + | Nat => nat + | Unit => unit + | dom --> ran => typeDenote dom -> typeDenote ran + | t1 ** t2 => typeDenote t1 * typeDenote t2 + | env @@ dom ---> ran => typeDenote env -> typeDenote dom -> typeDenote ran + end%type. + + Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := + match e in (exp _ t) return (typeDenote t) with + | Var _ v => v + + | Const n => n + | Plus e1 e2 => expDenote e1 + expDenote e2 + + | App _ _ f x => (expDenote f) (expDenote x) + | Pack _ _ _ f env => (expDenote f) (expDenote env) + + | EUnit => tt + + | Pair _ _ e1 e2 => (expDenote e1, expDenote e2) + | Fst _ _ e' => fst (expDenote e') + | Snd _ _ e' => snd (expDenote e') + end. + + Fixpoint funcsDenote T (fs : funcs typeDenote T) : T := + match fs with + | Main v => v + | Abs _ _ _ e fs => + funcsDenote (fs (fun env arg => expDenote (e env arg))) + end. + + Definition progDenote t (p : prog typeDenote t) : typeDenote t := + expDenote (funcsDenote p). + + Definition Exp t := forall var, exp var t. + Definition Prog t := forall var, prog var t. + + Definition ExpDenote t (E : Exp t) := expDenote (E _). + Definition ProgDenote t (P : Prog t) := progDenote (P _). +End Closed. + diff -r ec44782bffdd -r 24b99e025fe8 src/Intro.v --- a/src/Intro.v Mon Nov 10 17:27:55 2008 -0500 +++ b/src/Intro.v Sun Nov 16 11:54:51 2008 -0500 @@ -211,6 +211,8 @@ \hline Extensional Transformations & \texttt{Extensional.v} \\ \hline +Intensional Transformations & \texttt{Intensional.v} \\ +\hline \end{tabular} \end{center} % *) diff -r ec44782bffdd -r 24b99e025fe8 src/toc.html --- a/src/toc.html Mon Nov 10 17:27:55 2008 -0500 +++ b/src/toc.html Sun Nov 16 11:54:51 2008 -0500 @@ -19,5 +19,6 @@
  • Higher-Order Abstract Syntax
  • Type-Theoretic Interpreters
  • Extensional Transformations +
  • Intensional Transformations