Mercurial > cpdt > repo
comparison src/StackMachine.v @ 19:5db67b182ef8
Translation
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Wed, 03 Sep 2008 15:59:37 -0400 |
| parents | 82618ad75252 |
| children | c0cbf324ec7d |
comparison
equal
deleted
inserted
replaced
| 18:82618ad75252 | 19:5db67b182ef8 |
|---|---|
| 718 end. | 718 end. |
| 719 | 719 |
| 720 | 720 |
| 721 (** ** Translation *) | 721 (** ** Translation *) |
| 722 | 722 |
| 723 (** To define our compilation, it is useful to have an auxiliary function for concatenating two stack machine programs. *) | |
| 724 | |
| 723 Fixpoint tconcat ts ts' ts'' (p : tprog ts ts') {struct p} : tprog ts' ts'' -> tprog ts ts'' := | 725 Fixpoint tconcat ts ts' ts'' (p : tprog ts ts') {struct p} : tprog ts' ts'' -> tprog ts ts'' := |
| 724 match p in (tprog ts ts') return (tprog ts' ts'' -> tprog ts ts'') with | 726 match p in (tprog ts ts') return (tprog ts' ts'' -> tprog ts ts'') with |
| 725 | TNil _ => fun p' => p' | 727 | TNil _ => fun p' => p' |
| 726 | TCons _ _ _ i p1 => fun p' => TCons i (tconcat p1 p') | 728 | TCons _ _ _ i p1 => fun p' => TCons i (tconcat p1 p') |
| 727 end. | 729 end. |
| 730 | |
| 731 (** With that function in place, the compilation is defined very similarly to how it was before, modulo the use of dependent typing. *) | |
| 728 | 732 |
| 729 Fixpoint tcompile t (e : texp t) (ts : tstack) {struct e} : tprog ts (t :: ts) := | 733 Fixpoint tcompile t (e : texp t) (ts : tstack) {struct e} : tprog ts (t :: ts) := |
| 730 match e in (texp t) return (tprog ts (t :: ts)) with | 734 match e in (texp t) return (tprog ts (t :: ts)) with |
| 731 | TNConst n => TCons (TINConst _ n) (TNil _) | 735 | TNConst n => TCons (TINConst _ n) (TNil _) |
| 732 | TBConst b => TCons (TIBConst _ b) (TNil _) | 736 | TBConst b => TCons (TIBConst _ b) (TNil _) |
| 733 | TBinop _ _ _ b e1 e2 => tconcat (tcompile e2 _) | 737 | TBinop _ _ _ b e1 e2 => tconcat (tcompile e2 _) |
| 734 (tconcat (tcompile e1 _) (TCons (TIBinop _ b) (TNil _))) | 738 (tconcat (tcompile e1 _) (TCons (TIBinop _ b) (TNil _))) |
| 735 end. | 739 end. |
| 736 | 740 |
| 741 (** 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 arbitary 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. | |
| 742 | |
| 743 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: *) | |
| 744 | |
| 737 Print tcompile. | 745 Print tcompile. |
| 746 | |
| 747 (** [[ | |
| 748 | |
| 749 tcompile = | |
| 750 fix tcompile (t : type) (e : texp t) (ts : tstack) {struct e} : | |
| 751 tprog ts (t :: ts) := | |
| 752 match e in (texp t0) return (tprog ts (t0 :: ts)) with | |
| 753 | TNConst n => TCons (TINConst ts n) (TNil (Nat :: ts)) | |
| 754 | TBConst b => TCons (TIBConst ts b) (TNil (Bool :: ts)) | |
| 755 | TBinop arg1 arg2 res b e1 e2 => | |
| 756 tconcat (tcompile arg2 e2 ts) | |
| 757 (tconcat (tcompile arg1 e1 (arg2 :: ts)) | |
| 758 (TCons (TIBinop ts b) (TNil (res :: ts)))) | |
| 759 end | |
| 760 : forall t : type, texp t -> forall ts : tstack, tprog ts (t :: ts) | |
| 761 ]] *) | |
| 762 | |
| 763 | |
| 764 (** We can check that the compiler generates programs that behave appropriately on our sample programs from above: *) | |
| 765 | |
| 766 Eval simpl in tprogDenote (tcompile (TNConst 42) nil) tt. | |
| 767 (** [[ | |
| 768 = (42, tt) : vstack (Nat :: nil) | |
| 769 ]] *) | |
| 770 Eval simpl in tprogDenote (tcompile (TBConst true) nil) tt. | |
| 771 (** [[ | |
| 772 = (true, tt) : vstack (Bool :: nil) | |
| 773 ]] *) | |
| 774 Eval simpl in tprogDenote (tcompile (TBinop TTimes (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)) nil) tt. | |
| 775 (** [[ | |
| 776 = (28, tt) : vstack (Nat :: nil) | |
| 777 ]] *) | |
| 778 Eval simpl in tprogDenote (tcompile (TBinop (TEq Nat) (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)) nil) tt. | |
| 779 (** [[ | |
| 780 = (false, tt) : vstack (Bool :: nil) | |
| 781 ]] *) | |
| 782 Eval simpl in tprogDenote (tcompile (TBinop TLt (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)) nil) tt. | |
| 783 (** [[ | |
| 784 = (true, tt) : vstack (Bool :: nil) | |
| 785 ]] *) | |
| 738 | 786 |
| 739 | 787 |
| 740 (** ** Translation correctness *) | 788 (** ** Translation correctness *) |
| 741 | 789 |
| 742 Lemma tcompileCorrect' : forall t (e : texp t) | 790 Lemma tcompileCorrect' : forall t (e : texp t) |