Theory JVMListExample

(*  Title:      HOL/MicroJava/JVM/JVMListExample.thy
    Author:     Stefan Berghofer
*)

section ‹Example for generating executable code from JVM semantics \label{sec:JVMListExample}›

theory JVMListExample
imports "../J/SystemClasses" JVMExec
begin

text ‹
  Since the types \<^typ>‹cnam›, ‹vnam›, and ‹mname› are 
  anonymous, we describe distinctness of names in the example by axioms:
›
axiomatization list_nam test_nam :: cnam
  where distinct_classes: "list_nam ≠ test_nam"

axiomatization append_name makelist_name :: mname
  where distinct_methods: "append_name ≠ makelist_name"

axiomatization val_nam next_nam :: vnam
  where distinct_fields: "val_nam ≠ next_nam"

axiomatization
  where nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' ⟷ l = l'"

definition list_name :: cname
  where "list_name = Cname list_nam"
  
definition test_name :: cname
  where "test_name = Cname test_nam"

definition val_name :: vname
  where "val_name = VName val_nam"

definition next_name :: vname
  where "next_name = VName next_nam"

definition append_ins :: bytecode where
  "append_ins =
       [Load 0,
        Getfield next_name list_name,
        Dup,
        LitPush Null,
        Ifcmpeq 4,
        Load 1,       
        Invoke list_name append_name [Class list_name],
        Return,
        Pop,
        Load 0,
        Load 1,
        Putfield next_name list_name,
        LitPush Unit,
        Return]"

definition list_class :: "jvm_method class" where
  "list_class =
    (Object,
     [(val_name, PrimT Integer), (next_name, Class list_name)],
     [((append_name, [Class list_name]), PrimT Void,
        (3, 0, append_ins,[(1,2,8,Xcpt NullPointer)]))])"

definition make_list_ins :: bytecode where
  "make_list_ins =
       [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 [Class list_name],
        Pop,
        Load 0,
        Load 2,
        Invoke list_name append_name [Class list_name],
        Return]"

definition test_class :: "jvm_method class" where
  "test_class =
    (Object, [],
     [((makelist_name, []), PrimT Void, (3, 2, make_list_ins,[]))])"

definition E :: jvm_prog where
  "E = SystemClasses @ [(list_name, list_class), (test_name, test_class)]"

code_datatype list_nam test_nam
lemma equal_cnam_code [code]:
  "HOL.equal list_nam list_nam ⟷ True"
  "HOL.equal test_nam test_nam ⟷ True"
  "HOL.equal list_nam test_nam ⟷ False"
  "HOL.equal test_nam list_nam ⟷ False"
  by(simp_all add: distinct_classes distinct_classes[symmetric] equal_cnam_def)

code_datatype append_name makelist_name
lemma equal_mname_code [code]: 
  "HOL.equal append_name append_name ⟷ True"
  "HOL.equal makelist_name makelist_name ⟷ True"
  "HOL.equal append_name makelist_name ⟷ False"
  "HOL.equal makelist_name append_name ⟷ False"
  by(simp_all add: distinct_methods distinct_methods[symmetric] equal_mname_def)

code_datatype val_nam next_nam
lemma equal_vnam_code [code]: 
  "HOL.equal val_nam val_nam ⟷ True"
  "HOL.equal next_nam next_nam ⟷ True"
  "HOL.equal val_nam next_nam ⟷ False"
  "HOL.equal next_nam val_nam ⟷ False"
  by(simp_all add: distinct_fields distinct_fields[symmetric] equal_vnam_def)


lemma equal_loc'_code [code]:
  "HOL.equal (nat_to_loc' l) (nat_to_loc' l') ⟷ l = l'"
  by(simp add: equal_loc'_def nat_to_loc'_inject)

definition undefined_cname :: cname 
  where [code del]: "undefined_cname = undefined"
code_datatype Object Xcpt Cname undefined_cname
declare undefined_cname_def[symmetric, code_unfold]

definition undefined_val :: val
  where [code del]: "undefined_val = undefined"
declare undefined_val_def[symmetric, code_unfold]
code_datatype Unit Null Bool Intg Addr undefined_val

definition
  "test = exec (E, start_state E test_name makelist_name)"

ML_val ‹
  @{code test}; 
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
  @{code exec} (@{code E}, @{code the} it);
›

end