fork download 
  1. Inductive sinstr : Type :=
  2. | SPush : nat -> sinstr
  3. | SLoad : id -> sinstr
  4. | SPlus : sinstr
  5. | SMinus : sinstr
  6. | SMult : sinstr.
  7.  
  8. (** Write a function to evaluate programs in the stack language. It
  9.     takes as input a state, a stack represented as a list of
  10.     numbers (top stack item is the head of the list), and a program
  11.     represented as a list of instructions, and returns the stack after
  12.     executing the program. Test your function on the examples below.
  13.     Note that the specification leaves unspecified what to do when
  14.     encountering an [SPlus], [SMinus], or [SMult] instruction if the
  15.     stack contains less than two elements.  In a sense, it is
  16.     immaterial what we do, since our compiler will never emit such a
  17.     malformed program. *)
  18.  
  19. Fixpoint s_execute (st : state) (stack : list nat)
  20.                    (prog : list sinstr)
  21.                  : list nat :=
  22.   match prog with
  23.   | [] => stack
  24.   | ins :: prog' => 
  25.     match ins with
  26.     | SPush n => s_execute st (n :: stack) prog'
  27.     | SLoad x => s_execute st (st x :: stack) prog'
  28.     | SPlus => 
  29.       match stack with
  30.       | na :: nb :: stack' => s_execute st (nb+na :: stack') prog'
  31.       | _ => s_execute st stack prog'
  32.       end
  33.     | SMinus => 
  34.       match stack with
  35.       | na :: nb :: stack' => s_execute st (nb-na :: stack') prog'
  36.       | _ => s_execute st stack prog'
  37.       end
  38.     | SMult =>
  39.       match stack with
  40.       | na :: nb :: stack' => s_execute st (nb*na :: stack') prog'
  41.       | _ => s_execute st stack prog'
  42.       end
  43.     end
  44.   end.
  45.  
  46. Eval compute in 
  47.      s_execute empty_state []
  48.        [SPush 5; SPush 3; SPush 1; SMinus].
  49.  
  50. Eval compute in
  51.      s_execute (update empty_state X 3) [3;4]
  52.        [SPush 4; SLoad X; SMult; SPlus].
  53.  
  54.  
  55. Fixpoint s_compile (e : aexp) : list sinstr :=
  56. match e with
  57. | ANum n => [SPush n]
  58. | AId id => [SLoad id]
  59. | APlus a1 a2 => (s_compile a1) ++ (s_compile a2) ++ [SPlus]
  60. | AMinus a1 a2 => (s_compile a1) ++ (s_compile a2) ++ [SMinus]
  61. | AMult a1 a2 => (s_compile a1) ++ (s_compile a2) ++ [SMult]
  62. end
  63. .
  64.  
  65. (** After you've defined [s_compile], prove the following to test
  66.     that it works. *)
  67.  
  68. Example s_compile1 :
  69.     s_compile (AMinus (AId X) (AMult (ANum 2) (AId Y)))
  70.   = [SLoad X; SPush 2; SLoad Y; SMult; SMinus].
  71. Proof.
  72. simpl. auto.
  73. Qed.
  74.  
  75. (** **** Exercise: 3 stars, advanced (stack_compiler_correct)  *)
  76. (** The task of this exercise is to prove the correctness of the
  77.     compiler implemented in the previous exercise.  Remember that
  78.     the specification left unspecified what to do when encountering an
  79.     [SPlus], [SMinus], or [SMult] instruction if the stack contains
  80.     less than two elements.  (In order to make your correctness proof
  81.     easier you may find it useful to go back and change your
  82.     implementation!)
  83.     Prove the following theorem, stating that the [compile] function
  84.     behaves correctly.  You will need to start by stating a more
  85.     general lemma to get a usable induction hypothesis; the main
  86.     theorem will then be a simple corollary of this lemma. *)
  87.  
  88.  
  89. Lemma s_compile_correct' : forall (st:state) (l0:list nat) (l1:list sinstr) (l2:list sinstr),
  90. s_execute st l0 (l1++l2) = s_execute st (s_execute st l0 l1) l2.
  91. Proof.
  92. intros. generalize dependent l0. induction l1. simpl. auto. intros. destruct a; try apply IHl1.
  93. destruct l0. simpl; try apply IHl1. destruct l0. simpl; try apply IHl1. apply IHl1.
  94. destruct l0. simpl; try apply IHl1. destruct l0. simpl; try apply IHl1. apply IHl1.
  95. destruct l0. simpl; try apply IHl1. destruct l0. simpl; try apply IHl1. apply IHl1.
  96. Qed.
  97.  
  98.  
  99. Theorem s_compile_correct'' : forall (st : state) (e : aexp) (l:list nat),
  100.   s_execute st l (s_compile e) = (aeval st e) :: l.
  101. Proof.
  102. intros. generalize dependent st. generalize dependent l. induction e; intros; auto. simpl. rewrite s_compile_correct'.
  103. rewrite s_compile_correct'. rewrite IHe1. rewrite IHe2. auto.
  104. simpl. rewrite s_compile_correct'. rewrite s_compile_correct'. rewrite IHe1. rewrite IHe2. auto.
  105. simpl. rewrite s_compile_correct'. rewrite s_compile_correct'. rewrite IHe1. rewrite IHe2. auto.
  106. Qed.
  107.  
  108.  
  109.  
  110. Theorem s_compile_correct : forall (st : state) (e : aexp),
  111.   s_execute st [] (s_compile e) = [ aeval st e ].
  112. Proof.
  113. intros.
  114. assert(H:=s_compile_correct'' st e []). auto.
  115. Qed.
  116.  
  117.  
  118. (*-- Check --*)
  119. Check s_compile1 :
  120.     s_compile (AMinus (AId X) (AMult (ANum 2) (AId Y)))
  121.   = [SLoad X; SPush 2; SLoad Y; SMult; SMinus].
  122.  
  123. Check s_compile_correct : forall (st : state) (e : aexp),
  124.   s_execute st [] (s_compile e) = [ aeval st e ].
Not running #stdin #stdout 0s 0KB
comments (?)
stdin 
Standard input is empty
stdout 
Standard output is empty
https://ideone.com/DyVPfW
language:
Text (text 6.10)
created:
9 years ago
visibility:
public

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!