# HG changeset patch
# User berghofe
# Date 1007994288 -3600
# Node ID 0ecba8660de777f8c4e62d13ecf12c756049c92a
# Parent  c586d08520adde52eb76b3f9d8087f812766d3f8
Example for code generator.

diff -r c586d08520ad -r 0ecba8660de7 src/HOL/MicroJava/J/JListExample.thy
--- /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
diff -r c586d08520ad -r 0ecba8660de7 src/HOL/MicroJava/JVM/JVMListExample.thy
--- /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
+