Certified Programming with Dependent Types: src/StackMachine.v comparison

comparison src/StackMachine.v @ 207:a7be5d9a2fd4

Converted StackMachine

author	Adam Chlipala <adamc@hcoop.net>
date	Fri, 06 Nov 2009 17:10:27 -0500
parents	3f4576f15130
children	b149a07b9b5b

comparison

equal deleted inserted replaced

-:3f4576f15130
+:a7be5d9a2fd4
 | true, true => true
 | false, false => true
 | _, _ => false
 end.
-Fixpoint eq_nat (n1 n2 : nat) {struct n1} : bool :=
+Fixpoint eq_nat (n1 n2 : nat) : bool :=
 match n1, n2 with
 | O, O => true
 | S n1', S n2' => eq_nat n1' n2'
 | _, _ => false
 end.
-Fixpoint lt (n1 n2 : nat) {struct n1} : bool :=
+Fixpoint lt (n1 n2 : nat) : bool :=
 match n1, n2 with
 | O, S _ => true
 | S n1', S n2' => lt n1' n2'
 | _, _ => false
 end.
 (** Now we can interpret binary operators: *)
 Definition tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
 : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
-match b in (tbinop arg1 arg2 res) return (typeDenote arg1 -> typeDenote arg2 -> typeDenote res) with
+match b in (tbinop arg1 arg2 res)
+return (typeDenote arg1 -> typeDenote arg2 -> typeDenote res) with
 | TPlus => plus
 | TTimes => mult
 | TEq Nat => eq_nat
 | TEq Bool => eq_bool
 | TLt => lt
 end.
-(** This function has just a few differences from the denotation functions we saw earlier.  First, [tbinop] is an indexed type, so its indices become additional arguments to [tbinopDenote].  Second, we need to perform a genuine %\textit{%#<i>#dependent pattern match#</i>#%}% to come up with a definition of this function that type-checks.  In each branch of the [match], we need to use branch-specific information about the indices to [tbinop].  General type inference that takes such information into account is undecidable, and Coq avoids pursuing special heuristics for the problem, instead asking users to write annotations, like we see above on the line with [match].
+(** This function has just a few differences from the denotation functions we saw earlier.  First, [tbinop] is an indexed type, so its indices become additional arguments to [tbinopDenote].  Second, we need to perform a genuine %\textit{%#<i>#dependent pattern match#</i>#%}% to come up with a definition of this function that type-checks.  In each branch of the [match], we need to use branch-specific information about the indices to [tbinop].  General type inference that takes such information into account is undecidable, so it is often necessary to write annotations, like we see above on the line with [match].
 The [in] annotation restates the type of the term being case-analyzed.  Though we use the same names for the indices as we use in the type of the original argument binder, these are actually fresh variables, and they are %\textit{%#<i>#binding occurrences#</i>#%}%.  Their scope is the [return] clause.  That is, [arg1], [arg2], and [arg3] are new bound variables bound only within the return clause [typeDenote arg1 -> typeDenote arg2 -> typeDenote res].  By being explicit about the functional relationship between the type indices and the match result, we regain decidable type inference.
+In fact, recent Coq versions use some heuristics that can save us the trouble of writing [match] annotations, and those heuristics get the job done in this case.  We can get away with writing just: *)
+(* begin hide *)
+Reset tbinopDenote.
+(* end hide *)
+Definition tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
+: typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
+match b with
+| TPlus => plus
+| TTimes => mult
+| TEq Nat => eq_nat
+| TEq Bool => eq_bool
+| TLt => lt
+end.
+(**
 The same tricks suffice to define an expression denotation function in an unsurprising way:
 *)
-Fixpoint texpDenote t (e : texp t) {struct e} : typeDenote t :=
+Fixpoint texpDenote t (e : texp t) : typeDenote t :=
-match e in (texp t) return (typeDenote t) with
+match e with
 | TNConst n => n
 | TBConst b => b
 | TBinop _ _ _ b e1 e2 => (tbinopDenote b) (texpDenote e1) (texpDenote e2)
 end.
 (** We can evaluate a few example programs to convince ourselves that this semantics is correct. *)
 Eval simpl in texpDenote (TNConst 42).
-(** [[
+(** [= 42 : typeDenote Nat] *)
-= 42 : typeDenote Nat
-]] *)
 Eval simpl in texpDenote (TBConst true).
-(** [[
+(** [= true : typeDenote Bool] *)
-= true : typeDenote Bool
-]] *)
 Eval simpl in texpDenote (TBinop TTimes (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)).
-(** [[
+(** [= 28 : typeDenote Nat] *)
-= 28 : typeDenote Nat
-]] *)
 Eval simpl in texpDenote (TBinop (TEq Nat) (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)).
-(** [[
+(** [= false : typeDenote Bool] *)
-= false : typeDenote Bool
-]] *)
 Eval simpl in texpDenote (TBinop TLt (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)).
-(** [[
+(** [= true : typeDenote Bool] *)
-= true : typeDenote Bool
-]] *)
 (** ** Target Language *)
 (** Now we want to define a suitable stack machine target for compilation.  In the example of the untyped language, stack machine programs could encounter stack underflows and "get stuck."  This was unfortunate, since we had to deal with this complication even though we proved that our compiler never produced underflowing programs.  We could have used dependent types to force all stack machine programs to be underflow-free.
 | t :: ts' => typeDenote t * vstack ts'
 end%type.
 (** This is another [Set]-valued function.  This time it is recursive, which is perfectly valid, since [Set] is not treated specially in determining which functions may be written.  We say that the value stack of an empty stack type is any value of type [unit], which has just a single value, [tt].  A nonempty stack type leads to a value stack that is a pair, whose first element has the proper type and whose second element follows the representation for the remainder of the stack type.
-This idea of programming with types can take a while to internalize, but it enables a very simple definition of instruction denotation.  We have the same kind of type annotations for the dependent [match], but everything else is like what you might expect from a Lisp-like version of ML that ignored type information.  Nonetheless, the fact that [tinstrDenote] passes the type-checker guarantees that our stack machine programs can never go wrong. *)
+This idea of programming with types can take a while to internalize, but it enables a very simple definition of instruction denotation.  Our definition is like what you might expect from a Lisp-like version of ML that ignored type information.  Nonetheless, the fact that [tinstrDenote] passes the type-checker guarantees that our stack machine programs can never go wrong. *)
 Definition tinstrDenote ts ts' (i : tinstr ts ts') : vstack ts -> vstack ts' :=
-match i in (tinstr ts ts') return (vstack ts -> vstack ts') with
+match i with
 | TINConst _ n => fun s => (n, s)
 | TIBConst _ b => fun s => (b, s)
 | TIBinop _ _ _ _ b => fun s =>
 match s with
 (arg1, (arg2, s')) => ((tbinopDenote b) arg1 arg2, s')
 (** Why do we choose to use an anonymous function to bind the initial stack in every case of the [match]?  Consider this well-intentioned but invalid alternative version:
 [[
 Definition tinstrDenote ts ts' (i : tinstr ts ts') (s : vstack ts) : vstack ts' :=
-match i in (tinstr ts ts') return (vstack ts') with
+match i with
 | TINConst _ n => (n, s)
 | TIBConst _ b => (b, s)
 | TIBinop _ _ _ _ b =>
 match s with
 (arg1, (arg2, s')) => ((tbinopDenote b) arg1 arg2, s')
 The Coq type-checker complains that:
 [[
 The term "(n, s)" has type "(nat * vstack ts)%type"
-while it is expected to have type "vstack (Nat :: t)"
+while it is expected to have type "vstack ?119".
+]]
+The text [?119] stands for a unification variable.  We can try to help Coq figure out the value of this variable with an explicit annotation on our [match] expression.
+[[
+Definition tinstrDenote ts ts' (i : tinstr ts ts') (s : vstack ts) : vstack ts' :=
+match i in tinstr ts ts' return vstack ts' with
+| TINConst _ n => (n, s)
+| TIBConst _ b => (b, s)
+| TIBinop _ _ _ _ b =>
+match s with
+(arg1, (arg2, s')) => ((tbinopDenote b) arg1 arg2, s')
+end
+end.
+]]
+Now the error message changes.
+[[
+The term "(n, s)" has type "(nat * vstack ts)%type"
+while it is expected to have type "vstack (Nat :: t)".
 ]]
 Recall from our earlier discussion of [match] annotations that we write the annotations to express to the type-checker the relationship between the type indices of the case object and the result type of the [match].  Coq chooses to assign to the wildcard [_] after [TINConst] the name [t], and the type error is telling us that the type checker cannot prove that [t] is the same as [ts].  By moving [s] out of the [match], we lose the ability to express, with [in] and [return] clauses, the relationship between the shared index [ts] of [s] and [i].
 There %\textit{%#<i>#are#</i>#%}% reasonably general ways of getting around this problem without pushing binders inside [match]es.  However, the alternatives are significantly more involved, and the technique we use here is almost certainly the best choice, whenever it applies.
 *)
 (** We finish the semantics with a straightforward definition of program denotation. *)
-Fixpoint tprogDenote ts ts' (p : tprog ts ts') {struct p} : vstack ts -> vstack ts' :=
+Fixpoint tprogDenote ts ts' (p : tprog ts ts') : vstack ts -> vstack ts' :=
-match p in (tprog ts ts') return (vstack ts -> vstack ts') with
+match p with
 | TNil _ => fun s => s
 | TCons _ _ _ i p' => fun s => tprogDenote p' (tinstrDenote i s)
 end.
 (** ** Translation *)
 (** To define our compilation, it is useful to have an auxiliary function for concatenating two stack machine programs. *)
-Fixpoint tconcat ts ts' ts'' (p : tprog ts ts') {struct p} : tprog ts' ts'' -> tprog ts ts'' :=
+Fixpoint tconcat ts ts' ts'' (p : tprog ts ts') : tprog ts' ts'' -> tprog ts ts'' :=
-match p in (tprog ts ts') return (tprog ts' ts'' -> tprog ts ts'') with
+match p with
 | TNil _ => fun p' => p'
 | TCons _ _ _ i p1 => fun p' => TCons i (tconcat p1 p')
 end.
 (** With that function in place, the compilation is defined very similarly to how it was before, modulo the use of dependent typing. *)
-Fixpoint tcompile t (e : texp t) (ts : tstack) {struct e} : tprog ts (t :: ts) :=
+Fixpoint tcompile t (e : texp t) (ts : tstack) : tprog ts (t :: ts) :=
-match e in (texp t) return (tprog ts (t :: ts)) with
+match e with
 | TNConst n => TCons (TINConst _ n) (TNil _)
 | TBConst b => TCons (TIBConst _ b) (TNil _)
 | TBinop _ _ _ b e1 e2 => tconcat (tcompile e2 _)
 (tconcat (tcompile e1 _) (TCons (TIBinop _ b) (TNil _)))
 end.
 (** One interesting feature of the definition is the underscores appearing to the right of [=>] arrows.  Haskell and ML programmers are quite familiar with compilers that infer type parameters to polymorphic values.  In Coq, it is possible to go even further and ask the system to infer arbitrary terms, by writing underscores in place of specific values.  You may have noticed that we have been calling functions without specifying all of their arguments.  For instance, the recursive calls here to [tcompile] omit the [t] argument.  Coq's %\textit{%#<i>#implicit argument#</i>#%}% mechanism automatically inserts underscores for arguments that it will probably be able to infer.  Inference of such values is far from complete, though; generally, it only works in cases similar to those encountered with polymorphic type instantiation in Haskell and ML.
 The underscores here are being filled in with stack types.  That is, the Coq type inferencer is, in a sense, inferring something about the flow of control in the translated programs.  We can take a look at exactly which values are filled in: *)
 Print tcompile.
+(** [[
-(** [[
 tcompile =
 fix tcompile (t : type) (e : texp t) (ts : tstack) {struct e} :
 tprog ts (t :: ts) :=
 match e in (texp t0) return (tprog ts (t0 :: ts)) with
 | TNConst n => TCons (TINConst ts n) (TNil (Nat :: ts))
 (** We can check that the compiler generates programs that behave appropriately on our sample programs from above: *)
 Eval simpl in tprogDenote (tcompile (TNConst 42) nil) tt.
-(** [[
+(** [= (42, tt) : vstack (Nat :: nil)] *)
-= (42, tt) : vstack (Nat :: nil)
-]] *)
 Eval simpl in tprogDenote (tcompile (TBConst true) nil) tt.
-(** [[
+(** [= (true, tt) : vstack (Bool :: nil)] *)
-= (true, tt) : vstack (Bool :: nil)
-]] *)
 Eval simpl in tprogDenote (tcompile (TBinop TTimes (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)) nil) tt.
-(** [[
+(** [= (28, tt) : vstack (Nat :: nil)] *)
-= (28, tt) : vstack (Nat :: nil)
-]] *)
 Eval simpl in tprogDenote (tcompile (TBinop (TEq Nat) (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)) nil) tt.
-(** [[
+(** [= (false, tt) : vstack (Bool :: nil)] *)
-= (false, tt) : vstack (Bool :: nil)
-]] *)
 Eval simpl in tprogDenote (tcompile (TBinop TLt (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)) nil) tt.
-(** [[
+(** [= (true, tt) : vstack (Bool :: nil)] *)
-= (true, tt) : vstack (Bool :: nil)
-]] *)
 (** ** Translation Correctness *)
 (** We can state a correctness theorem similar to the last one. *)
-Theorem tcompile_correct : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
+Theorem tcompile_correct : forall t (e : texp t),
+tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
 (* begin hide *)
 Abort.
 (* end hide *)
 (* begin thide *)
 (** Again, we need to strengthen the theorem statement so that the induction will go through.  This time, I will develop an alternative approach to this kind of proof, stating the key lemma as: *)
-Lemma tcompile_correct' : forall t (e : texp t)
+Lemma tcompile_correct' : forall t (e : texp t) ts (s : vstack ts),
-ts (s : vstack ts),
+tprogDenote (tcompile e ts) s = (texpDenote e, s).
-tprogDenote (tcompile e ts) s
-= (texpDenote e, s).
 (** While lemma [compile_correct'] quantified over a program that is the "continuation" for the expression we are considering, here we avoid drawing in any extra syntactic elements.  In addition to the source expression and its type, we also quantify over an initial stack type and a stack compatible with it.  Running the compilation of the program starting from that stack, we should arrive at a stack that differs only in having the program's denotation pushed onto it.
 Let us try to prove this theorem in the same way that we settled on in the last section. *)
 induction e; crush.
 (** We are left with this unproved conclusion:
 [[
 tprogDenote
 (tconcat (tcompile e2 ts)
 (tconcat (tcompile e1 (arg2 :: ts))
 (TCons (TIBinop ts t) (TNil (res :: ts))))) s =
 (tbinopDenote t (texpDenote e1) (texpDenote e2), s)
 ]]
 We need an analogue to the [app_ass] theorem that we used to rewrite the goal in the last section.  We can abort this proof and prove such a lemma about [tconcat].
 *)
 Abort.
 Lemma tconcat_correct : forall ts ts' ts'' (p : tprog ts ts') (p' : tprog ts' ts'')
 (s : vstack ts),
 tprogDenote (tconcat p p') s
 Hint Rewrite tconcat_correct : cpdt.
 (** We ask that the lemma be used for left-to-right rewriting, and we ask for the hint to be added to the hint database called [cpdt], which is the database used by [crush].  Now we are ready to return to [tcompile_correct'], proving it automatically this time. *)
-Lemma tcompile_correct' : forall t (e : texp t)
+Lemma tcompile_correct' : forall t (e : texp t) ts (s : vstack ts),
-ts (s : vstack ts),
+tprogDenote (tcompile e ts) s = (texpDenote e, s).
-tprogDenote (tcompile e ts) s
-= (texpDenote e, s).
 induction e; crush.
 Qed.
 (** We can register this main lemma as another hint, allowing us to prove the final theorem trivially. *)
 Hint Rewrite tcompile_correct' : cpdt.
-Theorem tcompile_correct : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
+Theorem tcompile_correct : forall t (e : texp t),
+tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
 crush.
 Qed.
 (* end thide *)

Mercurial > cpdt > repo

comparison src/StackMachine.v @ 207:a7be5d9a2fd4