--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/JListExample.thy Mon Dec 10 15:24:48 2001 +0100
@@ -0,0 +1,131 @@
+(* Title: HOL/MicroJava/JVM/JVMListExample.thy
+ ID: $Id$
+ Author: Stefan Berghofer
+*)
+
+header {* Example for generating executable code from Java semantics *}
+
+theory JListExample = Eval:
+
+ML {* Syntax.ambiguity_level := 100000 *}
+
+consts
+ list_name :: cname
+ append_name :: mname
+ val_nam :: vnam
+ next_nam :: vnam
+ l_nam :: vnam
+ l1_nam :: vnam
+ l2_nam :: vnam
+ l3_nam :: vnam
+ l4_nam :: vnam
+
+constdefs
+ val_name :: vname
+ "val_name == VName val_nam"
+
+ next_name :: vname
+ "next_name == VName next_nam"
+
+ l_name :: vname
+ "l_name == VName l_nam"
+
+ l1_name :: vname
+ "l1_name == VName l1_nam"
+
+ l2_name :: vname
+ "l2_name == VName l2_nam"
+
+ l3_name :: vname
+ "l3_name == VName l3_nam"
+
+ l4_name :: vname
+ "l4_name == VName l4_nam"
+
+ list_class :: "java_mb class"
+ "list_class ==
+ (Object,
+ [(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))],
+ [((append_name, [RefT (ClassT list_name)]), PrimT Void,
+ ([l_name], [],
+ If(BinOp Eq ({list_name}(LAcc This)..next_name) (Lit Null))
+ Expr ({list_name}(LAcc This)..next_name:=LAcc l_name)
+ Else
+ Expr ({list_name}({list_name}(LAcc This)..next_name)..
+ append_name({[RefT (ClassT list_name)]}[LAcc l_name])),
+ Lit Unit))])"
+
+ example_prg :: "java_mb prog"
+ "example_prg == [ObjectC, (list_name, list_class)]"
+
+types_code
+ cname ("string")
+ vnam ("string")
+ mname ("string")
+ loc ("int")
+
+consts_code
+ "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}")
+ "cast_ok" ("true????")
+
+ "wf" ("true?")
+
+ "arbitrary" ("(raise ERROR)")
+ "arbitrary" :: "val" ("{* Unit *}")
+ "arbitrary" :: "cname" ("\"\"")
+
+ "Object" ("\"Object\"")
+ "list_name" ("\"list\"")
+ "append_name" ("\"append\"")
+ "val_nam" ("\"val\"")
+ "next_nam" ("\"next\"")
+ "l_nam" ("\"l\"")
+ "l1_nam" ("\"l1\"")
+ "l2_nam" ("\"l2\"")
+ "l3_nam" ("\"l3\"")
+ "l4_nam" ("\"l4\"")
+
+ML {*
+fun new_addr p none hp =
+ let fun nr i = if p (hp i) then (i, none) else nr (i+1);
+ in nr 0 end;
+*}
+
+generate_code
+ test = "query (example_prg\<turnstile>Norm (Map.empty, Map.empty)
+ -(Expr (l1_name::=NewC list_name);;
+ Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));;
+ Expr (l2_name::=NewC list_name);;
+ Expr ({list_name}(LAcc l2_name)..val_name:=Lit (Intg 2));;
+ Expr (l3_name::=NewC list_name);;
+ Expr ({list_name}(LAcc l3_name)..val_name:=Lit (Intg 3));;
+ Expr (l4_name::=NewC list_name);;
+ Expr ({list_name}(LAcc l4_name)..val_name:=Lit (Intg 4));;
+ Expr ({list_name}(LAcc l1_name)..
+ append_name({[RefT (ClassT list_name)]}[LAcc l2_name]));;
+ Expr ({list_name}(LAcc l1_name)..
+ append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));;
+ Expr ({list_name}(LAcc l1_name)..
+ append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> s1)"
+
+subsection {* Big step execution *}
+
+ML {*
+
+val Library.Some ((_, (heap, locs)), _) = Seq.pull test;
+locs l1_name;
+locs l2_name;
+locs l3_name;
+locs l4_name;
+snd (the (heap 0)) (val_name, "list");
+snd (the (heap 0)) (next_name, "list");
+snd (the (heap 1)) (val_name, "list");
+snd (the (heap 1)) (next_name, "list");
+snd (the (heap 2)) (val_name, "list");
+snd (the (heap 2)) (next_name, "list");
+snd (the (heap 3)) (val_name, "list");
+snd (the (heap 3)) (next_name, "list");
+
+*}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Mon Dec 10 15:24:48 2001 +0100
@@ -0,0 +1,173 @@
+(* Title: HOL/MicroJava/JVM/JVMListExample.thy
+ ID: $Id$
+ Author: Stefan Berghofer
+*)
+
+header {* Example for generating executable code from JVM semantics *}
+
+theory JVMListExample = JVMExec:
+
+consts
+ list_name :: cname
+ test_name :: cname
+ append_name :: mname
+ makelist_name :: mname
+ val_nam :: vnam
+ next_nam :: vnam
+
+constdefs
+ val_name :: vname
+ "val_name == VName val_nam"
+
+ next_name :: vname
+ "next_name == VName next_nam"
+
+ list_class :: "(nat * nat * bytecode) class"
+ "list_class ==
+ (Object,
+ [(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))],
+ [((append_name, [RefT (ClassT list_name)]), PrimT Integer,
+ (0, 0,
+ [Load 0,
+ Getfield next_name list_name,
+ Dup,
+ LitPush Null,
+ Ifcmpeq 4,
+ Load 1,
+ Invoke list_name append_name [RefT (ClassT list_name)],
+ Return,
+ Pop,
+ Load 0,
+ Load 1,
+ Putfield next_name list_name,
+ LitPush Unit,
+ Return]))])"
+
+ test_class :: "(nat * nat * bytecode) class"
+ "test_class ==
+ (Object, [],
+ [((makelist_name, []), PrimT Integer,
+ (0, 3,
+ [New list_name,
+ Dup,
+ Store 0,
+ LitPush (Intg 1),
+ Putfield val_name list_name,
+ New list_name,
+ Dup,
+ Store 1,
+ LitPush (Intg 2),
+ Putfield val_name list_name,
+ New list_name,
+ Dup,
+ Store 2,
+ LitPush (Intg 3),
+ Putfield val_name list_name,
+ Load 0,
+ Load 1,
+ Invoke list_name append_name [RefT (ClassT list_name)],
+ Load 0,
+ Load 2,
+ Invoke list_name append_name [RefT (ClassT list_name)],
+ LitPush Unit,
+ Return]))])"
+
+ example_prg :: jvm_prog
+ "example_prg == [ObjectC, (list_name, list_class), (test_name, test_class)]"
+
+ start_state :: jvm_state
+ "start_state ==
+ (None, empty, [([], Unit # Unit # Unit # [], test_name, (makelist_name, []), 0)])"
+
+types_code
+ cname ("string")
+ vnam ("string")
+ mname ("string")
+ loc ("int")
+
+consts_code
+ "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}")
+ "cast_ok" ("true????")
+
+ "wf" ("true?")
+
+ "arbitrary" ("(raise ERROR)")
+ "arbitrary" :: "val" ("{* Unit *}")
+ "arbitrary" :: "cname" ("\"\"")
+
+ "Object" ("\"Object\"")
+ "list_name" ("\"list\"")
+ "test_name" ("\"test\"")
+ "append_name" ("\"append\"")
+ "makelist_name" ("\"makelist\"")
+ "val_nam" ("\"val\"")
+ "next_nam" ("\"next\"")
+
+ML {*
+fun new_addr p none hp =
+ let fun nr i = if p (hp i) then (i, none) else nr (i+1);
+ in nr 0 end;
+*}
+
+subsection {* Single step execution *}
+
+generate_code
+ test = "exec (example_prg, start_state)"
+
+ML {* test *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+ML {* exec (example_prg, the it) *}
+
+end
+