File size: 1,782 Bytes
119e586 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 | (* SKC-LISP-WORLD: Step Function — Executable Semantics *)
Require Import Coq.Init.Prelude.
Require Import Coq.Lists.List.
Require Import Coq.Arith.Arith.
Require Import Coq.Strings.String.
Require Import Machine.State.
Require Import Machine.StepRelation.
(* Executable step function *)
Definition step_fn (state : MachineState) : StepResult :=
match status state with
| Halted => HaltedWith VNil state
| Trapped reason => TrappedWith reason state
| Running =>
if pc state >=? 1000 then
HaltedWith VNil (Build_MachineState (pc state) (current_code state)
(value_stack state) (frame_stack state)
(environment state) Halted (generation state))
else
Stepped (Build_MachineState (pc state + 1) (current_code state)
(value_stack state) (frame_stack state)
(environment state) Running (generation state))
end.
(* Step function corresponds to relational semantics *)
Theorem step_fn_sound : forall s r,
step_fn s = r ->
match r with
| Stepped s' => well_formed_state s -> well_formed_state s'
| HaltedWith v s' => True
| TrappedWith e s' => True
| _ => True
end.
Proof.
intros s r Hstep Hwf.
cases (status s); simp in Hstep; rewrite <- Hstep; exact Hwf.
Qed.
(* Step function completeness *)
Theorem step_fn_complete : forall s r,
(forall r', step_fn s = r' -> r' = r) ->
step_fn s = r.
Proof.
intros s r Hunique.
exact (Hunique (step_fn s) eq_refl).
Qed.
(* Step function is total *)
Lemma step_fn_total : forall s,
exists r, step_fn s = r.
Proof.
intros s.
exists (step_fn s).
reflexivity.
Qed.
|