File size: 1,799 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 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 | Require Import Coq.Init.Prelude.
Require Import Coq.Lists.List.
Require Import Coq.Arith.Arith.
Require Import Coq.ZArith.ZArith.
Require Import World.ObjectKinds.
Inductive Instruction : Type :=
| IConst (idx : nat)
| ILookup (name : string)
| IBind (name : string)
| IPush (v : Value)
| IPop
| ICons
| ICar
| ICdr
| ISetCar
| ISetCdr
| IMakeClosure (code : CodeId)
| ICall (arity : nat)
| ITailCall (arity : nat)
| IReturn
| IJump (addr : nat)
| IJumpIfFalse (addr : nat)
| IPushFrame
| IPopFrame
| ICaptureContination
| IRestoreContination
| IRaise
| IInstallHandler
| IRemoveHandler
| IRequestEffect
| IPatchCode (start : nat) (new_instrs : list Instruction)
| IDefineCode (code : CodeId)
| IReplaceFunction (sym : string)
| IRewriteDispatch
| ICommitGeneration
| IRollbackGeneration
| IHalt.
Inductive MachineStatus : Type :=
| Running
| Halted
| Trapped (reason : string).
Record MachineState : Type := {
pc : nat;
current_code : CodeId;
value_stack : list Value;
frame_stack : list ObjectId;
environment : ObjectId;
status : MachineStatus;
generation : Generation;
}.
Inductive StepResult : Type :=
| Stepped (next : MachineState)
| Emitted (obs : string) (next : MachineState)
| Requested (effect : string) (next : MachineState)
| HaltedWith (result : Value) (final : MachineState)
| TrappedWith (error : string) (final : MachineState).
Definition well_formed_state (s : MachineState) : Prop :=
match status s with
| Running => True
| Halted => True
| Trapped _ => True
end.
Lemma well_formed_reflexive : forall s,
well_formed_state s <-> well_formed_state s.
Proof.
intro s; split; intro H; exact H.
Qed.
|