--- a/src/HOL/MicroJava/JVM/JVMExec.thy Mon Jul 17 13:59:10 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Mon Jul 17 14:00:53 2000 +0200
@@ -6,62 +6,22 @@
Execution of the JVM
*)
-JVMExec = LoadAndStore + Object + Method + Opstack + Control +
-
-datatype
- instr = LS load_and_store
- | CO create_object
- | MO manipulate_object
- | CH check_object
- | MI meth_inv
- | MR meth_ret
- | OS op_stack
- | BR branch
-
-types
- bytecode = instr list
- jvm_prog = "(nat \\<times> bytecode)prog"
+JVMExec = JVMExecInstr +
consts
exec :: "jvm_prog \\<times> jvm_state \\<Rightarrow> jvm_state option"
-(** exec is not recursive. recdef is just used because for pattern matching **)
+(** exec is not recursive. recdef is just used for pattern matching **)
recdef exec "{}"
"exec (G, xp, hp, []) = None"
"exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
- Some (case snd(snd(snd(the(method (G,C) sig)))) ! pc of
- LS ins \\<Rightarrow> let (stk',loc',pc') = exec_las ins stk loc pc
- in
- (None,hp,(stk',loc',C,sig,pc')#frs)
-
- | CO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_co ins G hp stk pc
- in
- (xp',hp',(stk',loc,C,sig,pc')#frs)
-
- | MO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_mo ins hp stk pc
- in
- (xp',hp',(stk',loc,C,sig,pc')#frs)
+ (let
+ i = snd(snd(snd(the(method (G,C) sig)))) ! pc
+ in
+ Some (exec_instr i G hp stk loc C sig pc frs))"
- | CH ins \\<Rightarrow> let (xp',stk',pc') = exec_ch ins G hp stk pc
- in
- (xp',hp,(stk',loc,C,sig,pc')#frs)
-
- | MI ins \\<Rightarrow> let (xp',frs',stk',pc') = exec_mi ins G hp stk pc
- in
- (xp',hp,frs'@(stk',loc,C,sig,pc')#frs)
-
- | MR ins \\<Rightarrow> let frs' = exec_mr ins stk frs in (None,hp,frs')
-
- | OS ins \\<Rightarrow> let (stk',pc') = exec_os ins stk pc
- in
- (None,hp,(stk',loc,C,sig,pc')#frs)
-
- | BR ins \\<Rightarrow> let (stk',pc') = exec_br ins stk pc
- in
- (None,hp,(stk',loc,C,sig,pc')#frs))"
-
- "exec (G, Some xp, hp, frs) = None"
+ "exec (G, Some xp, hp, frs) = None"
constdefs