Skip to content

C
cpdt
Commit e9410295 authored by Adam Chlipala's avatar Adam Chlipala
Browse files
Options

New release

parent 1a0cde31
Show whitespace changes
Inline Side-by-side
Showing with 6 additions and 627 deletions
src/Extensional.v
View file @ e9410295
......@@ -384,631 +384,6 @@ Module STLC.
End STLC.
(** * A Pattern Compiler *)
Module PatMatch.
Module Source.
Inductive type : Type :=
| Unit : type
| Arrow : type -> type -> type
| Prod : type -> type -> type
| Sum : type -> type -> type.
Infix "-->" := Arrow (right associativity, at level 61).
Infix "++" := Sum (right associativity, at level 60).
Infix "**" := Prod (right associativity, at level 59).
Inductive pat : type -> list type -> Type :=
| PVar : forall t,
pat t (t :: nil)
| PPair : forall t1 t2 ts1 ts2,
pat t1 ts1
-> pat t2 ts2
-> pat (t1 ** t2) (ts1 ++ ts2)
| PInl : forall t1 t2 ts,
pat t1 ts
-> pat (t1 ++ t2) ts
| PInr : forall t1 t2 ts,
pat t2 ts
-> pat (t1 ++ t2) ts.
Implicit Arguments PVar [t].
Implicit Arguments PInl [t1 t2 ts].
Implicit Arguments PInr [t1 t2 ts].
Notation "##" := PVar (at level 70) : pat_scope.
Notation "[ p1 , p2 ]" := (PPair p1 p2) : pat_scope.
Notation "'Inl' p" := (PInl p) (at level 71) : pat_scope.
Notation "'Inr' p" := (PInr p) (at level 71) : pat_scope.
Bind Scope pat_scope with pat.
Delimit Scope pat_scope with pat.
Section vars.
Variable var : type -> Type.
Inductive exp : type -> Type :=
| Var : forall t,
var t
-> exp t
| EUnit : exp Unit
| App : forall t1 t2,
exp (t1 --> t2)
-> exp t1
-> exp t2
| Abs : forall t1 t2,
(var t1 -> exp t2)
-> exp (t1 --> t2)
| Pair : forall t1 t2,
exp t1
-> exp t2
-> exp (t1 ** t2)
| EInl : forall t1 t2,
exp t1
-> exp (t1 ++ t2)
| EInr : forall t1 t2,
exp t2
-> exp (t1 ++ t2)
| Case : forall t1 t2 (tss : list (list type)),
exp t1
-> (forall ts, member ts tss -> pat t1 ts)
-> (forall ts, member ts tss -> hlist var ts -> exp t2)
-> exp t2
-> exp t2.
End vars.
Definition Exp t := forall var, exp var t.
Implicit Arguments Var [var t].
Implicit Arguments EUnit [var].
Implicit Arguments App [var t1 t2].
Implicit Arguments Abs [var t1 t2].
Implicit Arguments Pair [var t1 t2].
Implicit Arguments EInl [var t1 t2].
Implicit Arguments EInr [var t1 t2].
Implicit Arguments Case [var t1 t2].
Notation "# v" := (Var v) (at level 70) : source_scope.
Notation "()" := EUnit : source_scope.
Infix "@" := App (left associativity, at level 77) : source_scope.
Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
Notation "[ x , y ]" := (Pair x y) : source_scope.
Notation "'Inl' e" := (EInl e) (at level 71) : source_scope.
Notation "'Inr' e" := (EInr e) (at level 71) : source_scope.
Delimit Scope source_scope with source.
Bind Scope source_scope with exp.
Local Open Scope source_scope.
Fixpoint typeDenote (t : type) : Set :=
match t with
| Unit => unit
| t1 --> t2 => typeDenote t1 -> typeDenote t2
| t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
| t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type
end.
Fixpoint patDenote t ts (p : pat t ts)
: typeDenote t -> option (hlist typeDenote ts) :=
match p with
| PVar _ => fun v => Some (v ::: HNil)
| PPair _ _ _ _ p1 p2 => fun v =>
match patDenote p1 (fst v), patDenote p2 (snd v) with
| Some tup1, Some tup2 => Some (happ tup1 tup2)
| _, _ => None
end
| PInl _ _ _ p' => fun v =>
match v with
| inl v' => patDenote p' v'
| _ => None
end
| PInr _ _ _ p' => fun v =>
match v with
| inr v' => patDenote p' v'
| _ => None
end
end.
Section matchesDenote.
Variables t2 : type.
Variable default : typeDenote t2.
Fixpoint matchesDenote (tss : list (list type))
: (forall ts, member ts tss -> option (hlist typeDenote ts))
-> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
-> typeDenote t2 :=
match tss return (forall ts, member ts tss -> option (hlist typeDenote ts))
-> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
-> _ with
| nil => fun _ _ =>
default
| ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss')
-> option (hlist typeDenote ts'))
(bodies : forall ts', member ts' (ts :: tss')
-> hlist typeDenote ts' -> typeDenote t2) =>
match envs _ HFirst with
| None => matchesDenote
(fun _ mem => envs _ (HNext mem))
(fun _ mem => bodies _ (HNext mem))
| Some env => (bodies _ HFirst) env
end
end.
End matchesDenote.
Implicit Arguments matchesDenote [t2 tss].
Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
match e with
| Var _ v => v
| EUnit => tt
| App _ _ e1 e2 => (expDenote e1) (expDenote e2)
| Abs _ _ e' => fun x => expDenote (e' x)
| Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
| EInl _ _ e' => inl _ (expDenote e')
| EInr _ _ e' => inr _ (expDenote e')
| Case _ _ _ e ps es def =>
matchesDenote (expDenote def)
(fun _ mem => patDenote (ps _ mem) (expDenote e))
(fun _ mem env => expDenote (es _ mem env))
end.
Definition ExpDenote t (E : Exp t) := expDenote (E _).
End Source.
Import Source.
Module Elab.
Section vars.
Variable var : type -> Type.
Inductive exp : type -> Type :=
| Var : forall t,
var t
-> exp t
| EUnit : exp Unit
| App : forall t1 t2,
exp (t1 --> t2)
-> exp t1
-> exp t2
| Abs : forall t1 t2,
(var t1 -> exp t2)
-> exp (t1 --> t2)
| 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
| EInl : forall t1 t2,
exp t1
-> exp (t1 ++ t2)
| EInr : forall t1 t2,
exp t2
-> exp (t1 ++ t2)
| Case : forall t1 t2 t,
exp (t1 ++ t2)
-> (var t1 -> exp t)
-> (var t2 -> exp t)
-> exp t.
End vars.
Definition Exp t := forall var, exp var t.
Implicit Arguments Var [var t].
Implicit Arguments EUnit [var].
Implicit Arguments App [var t1 t2].
Implicit Arguments Abs [var t1 t2].
Implicit Arguments Pair [var t1 t2].
Implicit Arguments Fst [var t1 t2].
Implicit Arguments Snd [var t1 t2].
Implicit Arguments EInl [var t1 t2].
Implicit Arguments EInr [var t1 t2].
Implicit Arguments Case [var t1 t2 t].
Notation "# v" := (Var v) (at level 70) : elab_scope.
Notation "()" := EUnit : elab_scope.
Infix "@" := App (left associativity, at level 77) : elab_scope.
Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : elab_scope.
Notation "\ ? , e" := (Abs (fun _ => e)) (at level 78) : elab_scope.
Notation "[ x , y ]" := (Pair x y) : elab_scope.
Notation "#1 e" := (Fst e) (at level 72) : elab_scope.
Notation "#2 e" := (Snd e) (at level 72) : elab_scope.
Notation "'Inl' e" := (EInl e) (at level 71) : elab_scope.
Notation "'Inr' e" := (EInr e) (at level 71) : elab_scope.
Bind Scope elab_scope with exp.
Delimit Scope elab_scope with elab.
Open Scope elab_scope.
Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
match e with
| Var _ v => v
| EUnit => tt
| App _ _ e1 e2 => (expDenote e1) (expDenote e2)
| Abs _ _ e' => fun x => expDenote (e' x)
| Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
| Fst _ _ e' => fst (expDenote e')
| Snd _ _ e' => snd (expDenote e')
| EInl _ _ e' => inl _ (expDenote e')
| EInr _ _ e' => inr _ (expDenote e')
| Case _ _ _ e' e1 e2 =>
match expDenote e' with
| inl v => expDenote (e1 v)
| inr v => expDenote (e2 v)
end
end.
Definition ExpDenote t (E : Exp t) := expDenote (E _).
End Elab.
Import Elab.
Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%source
(right associativity, at level 76, e1 at next level) : source_scope.
Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%elab
(right associativity, at level 76, e1 at next level) : elab_scope.
Section choice_tree.
Open Scope source_scope.
Fixpoint choice_tree var (t : type) (result : Type) : Type :=
match t with
| t1 ** t2 =>
choice_tree var t1
(choice_tree var t2
result)
| t1 ++ t2 =>
choice_tree var t1 result
* choice_tree var t2 result
| t => exp var t -> result
end%type.
Fixpoint merge var t result
: (result -> result -> result)
-> choice_tree var t result -> choice_tree var t result -> choice_tree var t result :=
match t with
| _ ** _ => fun mr ct1 ct2 =>
merge _ _
(merge _ _ mr)
ct1 ct2
| _ ++ _ => fun mr ct1 ct2 =>
(merge var _ mr (fst ct1) (fst ct2),
merge var _ mr (snd ct1) (snd ct2))
| _ => fun mr ct1 ct2 e => mr (ct1 e) (ct2 e)
end.
Fixpoint everywhere var t result
: (exp var t -> result) -> choice_tree var t result :=
match t with
| t1 ** t2 => fun r =>
everywhere (t := t1) (fun e1 =>
everywhere (t := t2) (fun e2 =>
r ([e1, e2])%elab))
| _ ++ _ => fun r =>
(everywhere (fun e => r (Inl e)%elab),
everywhere (fun e => r (Inr e)%elab))
| _ => fun r => r
end.
End choice_tree.
Implicit Arguments merge [var t result].
Section elaborate.
Local Open Scope elab_scope.
Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) :
(hlist (exp var) ts -> result) -> result -> choice_tree var t1 result :=
match p with
| PVar _ => fun succ fail =>
everywhere (fun disc => succ (disc ::: HNil))
| PPair _ _ _ _ p1 p2 => fun succ fail =>
elaboratePat p1
(fun tup1 =>
elaboratePat p2
(fun tup2 =>
succ (happ tup1 tup2))
fail)
(everywhere (fun _ => fail))
| PInl _ _ _ p' => fun succ fail =>
(elaboratePat p' succ fail,
everywhere (fun _ => fail))
| PInr _ _ _ p' => fun succ fail =>
(everywhere (fun _ => fail),
elaboratePat p' succ fail)
end.
Implicit Arguments elaboratePat [var t1 ts result].
Fixpoint letify var t ts : (hlist var ts -> exp var t)
-> hlist (exp var) ts -> exp var t :=
match ts with
| nil => fun f _ => f HNil
| _ :: _ => fun f tup => letify (fun tup' => x <- hhd tup; f (x ::: tup')) (htl tup)
end.
Implicit Arguments letify [var t ts].
Fixpoint expand var result t1 t2
(out : result -> exp var t2)
: forall ct : choice_tree var t1 result,
exp var t1
-> exp var t2 :=
match t1 with
| (_ ** _)%source => fun ct disc =>
expand
(fun ct' => expand out ct' (#2 disc)%source)
ct
(#1 disc)
| (_ ++ _)%source => fun ct disc =>
Case disc
(fun x => expand out (fst ct) (#x))
(fun y => expand out (snd ct) (#y))
| _ => fun ct disc =>
x <- disc; out (ct (#x))
end.
Definition mergeOpt A (o1 o2 : option A) :=
match o1 with
| None => o2
| _ => o1
end.
Import Source.
Fixpoint elaborateMatches var t1 t2
(tss : list (list type))
: (forall ts, member ts tss -> pat t1 ts)
-> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
-> choice_tree var t1 (option (Elab.exp var t2)) :=
match tss return (forall ts, member ts tss -> pat t1 ts)
-> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
-> _ with
| nil => fun _ _ =>
everywhere (fun _ => None)
| ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts')
(es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) =>
merge (@mergeOpt _)
(elaboratePat (ps _ HFirst)
(fun ts => Some (letify
(fun ts' => es _ HFirst ts')
ts))
None)
(elaborateMatches
(fun _ mem => ps _ (HNext mem))
(fun _ mem => es _ (HNext mem)))
end.
Implicit Arguments elaborateMatches [var t1 t2 tss].
Open Scope cps_scope.
Fixpoint elaborate var t (e : Source.exp var t) : Elab.exp var t :=
match e with
| Var _ v => #v
| EUnit => ()
| App _ _ e1 e2 => elaborate e1 @ elaborate e2
| Abs _ _ e' => \x, elaborate (e' x)
| Pair _ _ e1 e2 => [elaborate e1, elaborate e2]
| EInl _ _ e' => Inl (elaborate e')
| EInr _ _ e' => Inr (elaborate e')
| Case _ _ _ e' ps es def =>
expand
(fun eo => match eo with
| None => elaborate def
| Some e => e
end)
(elaborateMatches ps (fun _ mem env => elaborate (es _ mem env)))
(elaborate e')
end.
End elaborate.
Definition Elaborate t (E : Source.Exp t) : Elab.Exp t :=
fun _ => elaborate (E _).
Fixpoint grab t result : choice_tree typeDenote t result -> typeDenote t -> result :=
match t with
| t1 ** t2 => fun ct v =>
grab t2 _ (grab t1 _ ct (fst v)) (snd v)
| t1 ++ t2 => fun ct v =>
match v with
| inl v' => grab t1 _ (fst ct) v'
| inr v' => grab t2 _ (snd ct) v'
end
| t => fun ct v => ct (#v)%elab
end%source%type.
Implicit Arguments grab [t result].
Ltac my_crush :=
crush;
repeat (match goal with
| [ |- context[match ?E with inl _ => _ | inr _ => _ end] ] =>
destruct E
end; crush).
Lemma expand_grab : forall t2 t1 result
(out : result -> Elab.exp typeDenote t2)
(ct : choice_tree typeDenote t1 result)
(disc : Elab.exp typeDenote t1),
Elab.expDenote (expand out ct disc)
= Elab.expDenote (out (grab ct (Elab.expDenote disc))).
induction t1; my_crush.
Qed.
Lemma recreate_pair : forall t1 t2
(x : Elab.exp typeDenote t1)
(x0 : Elab.exp typeDenote t2)
(v : typeDenote (t1 ** t2)),
expDenote x = fst v
-> expDenote x0 = snd v
-> @eq (typeDenote t1 * typeDenote t2) (expDenote [x, x0]) v.
destruct v; crush.
Qed.
Lemma everywhere_correct : forall t1 result
(succ : Elab.exp typeDenote t1 -> result) disc,
exists disc', grab (everywhere succ) (Elab.expDenote disc) = succ disc'
/\ Elab.expDenote disc' = Elab.expDenote disc.
Hint Resolve recreate_pair.
induction t1; my_crush; eauto; fold choice_tree;
repeat (fold typeDenote in *; crush;
match goal with
| [ IH : forall result succ, _ |- context[grab (everywhere ?S) _] ] =>
generalize (IH _ S); clear IH
| [ e : exp typeDenote (?T ** _), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
generalize (IH (#1 e)); clear IH
| [ e : exp typeDenote (_ ** ?T), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
generalize (IH (#2 e)); clear IH
| [ e : typeDenote ?T, IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
generalize (IH (#e)); clear IH
end; crush); eauto.
Qed.
Lemma merge_correct : forall t result
(ct1 ct2 : choice_tree typeDenote t result)
(mr : result -> result -> result) v,
grab (merge mr ct1 ct2) v = mr (grab ct1 v) (grab ct2 v).
induction t; crush.
Qed.
Lemma everywhere_fail : forall t result
(fail : result) v,
grab (everywhere (fun _ : Elab.exp typeDenote t => fail)) v = fail.
induction t; crush.
Qed.
Lemma elaboratePat_correct : forall t1 ts (p : pat t1 ts)
result (succ : hlist (Elab.exp typeDenote) ts -> result)
(fail : result) v env,
patDenote p v = Some env
-> exists env', grab (elaboratePat p succ fail) v = succ env'
/\ env = hmap Elab.expDenote env'.
Hint Resolve hmap_happ.
induction p; crush; fold choice_tree;
repeat (match goal with
| [ |- context[grab (everywhere ?succ) ?v] ] =>
generalize (everywhere_correct succ (#v)%elab)
| [ H : forall result succ fail, _
|- context[grab (elaboratePat _ ?S ?F) ?V] ] =>
generalize (H _ S F V); clear H
| [ H1 : context[match ?E with Some _ => _ | None => _ end],
H2 : forall env, ?E = Some env -> _ |- _ ] =>
destruct E
| [ H : forall env, Some ?E = Some env -> _ |- _ ] =>
generalize (H _ (refl_equal _)); clear H
end; crush); eauto.
Qed.
Lemma elaboratePat_fails : forall t1 ts (p : pat t1 ts)
result (succ : hlist (Elab.exp typeDenote) ts -> result)
(fail : result) v,
patDenote p v = None
-> grab (elaboratePat p succ fail) v = fail.
Hint Resolve everywhere_fail.
induction p; try solve [ crush ];
simpl; fold choice_tree; intuition; simpl in *;
repeat match goal with
| [ IH : forall result succ fail v, patDenote ?P v = _ -> _
|- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
generalize (IH _ S F V); clear IH; intro IH;
generalize (elaboratePat_correct P S F V); intros;
destruct (patDenote P V); try discriminate
| [ H : forall env, Some _ = Some env -> _ |- _ ] =>
destruct (H _ (refl_equal _)); clear H; intuition
| [ H : _ |- _ ] => rewrite H; intuition
| [ |- context[match ?v with inl _ => _ | inr _ => _ end] ] =>
destruct v; auto
end.
Qed.
Implicit Arguments letify [var t ts].
Lemma letify_correct : forall t ts (f : hlist typeDenote ts -> Elab.exp typeDenote t)
(env : hlist (Elab.exp typeDenote) ts),
Elab.expDenote (letify f env)
= Elab.expDenote (f (hmap Elab.expDenote env)).
induction ts; crush; dep_destruct env; crush.
Qed.
Theorem elaborate_correct : forall t (e : Source.exp typeDenote t),
Elab.expDenote (elaborate e) = Source.expDenote e.
Hint Rewrite expand_grab merge_correct letify_correct : cpdt.
Hint Rewrite everywhere_fail elaboratePat_fails using assumption : cpdt.
induction e; crush; try (ext_eq; crush);
match goal with
| [ tss : list (list type) |- _ ] =>
induction tss; crush;
match goal with
| [ |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
case_eq (patDenote P V); [intros env Heq;
destruct (elaboratePat_correct P S F _ Heq); crush;
match goal with
| [ H : _ |- _ ] => rewrite <- H; crush
end
| crush ]
end
end.
Qed.
Theorem Elaborate_correct : forall t (E : Source.Exp t),
Elab.ExpDenote (Elaborate E) = Source.ExpDenote E.
unfold Elab.ExpDenote, Elaborate, Source.ExpDenote;
intros; apply elaborate_correct.
Qed.
End PatMatch.
(** * Exercises *)
(** %\begin{enumerate}%#<ol>#
......
src/Intro.v
View file @ e9410295
......@@ -49,6 +49,8 @@ We would all like to have programs check that our programs are correct. Due in
There are a good number of (though definitely not "many") tools that are in wide use today for building machine-checked mathematical proofs and machine-certified programs. This is my attempt at an exhaustive list of interactive "proof assistants" satisfying a few criteria. First, the authors of each tool must intend for it to be put to use for software-related applications. Second, there must have been enough engineering effort put into the tool that someone not doing research on the tool itself would feel his time was well spent using it. A third criterion is more of an empirical validation of the second: the tool must have a significant user community outside of its own development team.
%
\medskip
\begin{tabular}{rl}
\textbf{ACL2} & \url{http://www.cs.utexas.edu/users/moore/acl2/} \\
\textbf{Coq} & \url{http://coq.inria.fr/} \\
......@@ -56,6 +58,8 @@ There are a good number of (though definitely not "many") tools that are in wide
\textbf{PVS} & \url{http://pvs.csl.sri.com/} \\
\textbf{Twelf} & \url{http://www.twelf.org/} \\
\end{tabular}
\medskip
%
#
<table align="center">
......
staging/index.html
View file @ e9410295
......@@ -29,9 +29,9 @@
<div class="project">
<h2>Status</h2>
<p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1. Last incremental update on November 23, 2009.</p>
<p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1. Last incremental update on December 9, 2009.</p>
<p>Some chapters on programming languages and compilers are empty or just contain Coq code; these should be filled in soon-ish. Additional plans: a chapter on best practices with dependent De Bruijn syntax; some examples of locally nameless syntax; more examples of Ltac design patterns; discussion of tactic debugging and maintenance.</p>
<p>Some chapters on programming languages and compilers are empty or just contain Coq code; these should be filled in soon-ish. Additional plans: a chapter on best practices with dependent De Bruijn syntax; some examples of locally nameless syntax.</p>
</div>
</body></html>
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment