# HG changeset patch # User haftmann # Date 1160556569 -7200 # Node ID 1e7df197b8b818f581e7d6bf3a84bd4fda26920f # Parent c2a342e548a9281a1847b11a4d8acbf6733fd917 added code generator setup diff -r c2a342e548a9 -r 1e7df197b8b8 src/HOL/MicroJava/JVM/JVMListExample.thy --- a/src/HOL/MicroJava/JVM/JVMListExample.thy Wed Oct 11 10:49:28 2006 +0200 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Wed Oct 11 10:49:29 2006 +0200 @@ -112,6 +112,66 @@ "val_nam" ("\"val\"") "next_nam" ("\"next\"") +code_type cnam and vnam and mname and loc_ + (SML target_atom "string" and target_atom "string" and target_atom "string" and target_atom "IntInf.int") + +instance cnam :: eq + and cname :: eq + and vname :: eq + and mname :: eq + and ty :: eq + and instr :: eq .. + +definition + arbitrary_val :: val + "arbitrary_val = arbitrary" + arbitrary_cname :: cname + "arbitrary_cname = arbitrary" + +declare arbitrary_val_def [symmetric, code inline] +declare arbitrary_cname_def [symmetric, code inline] + +definition + "unit' = Unit" + "object' = Object" + +code_constsubst + arbitrary_val \ unit' + arbitrary_cname \ object' + +code_const list_nam and test_nam and append_name and makelist_name and val_nam and next_nam + (SML target_atom "\"list\"" and target_atom "\"test\"" and target_atom "\"append\"" + and target_atom "\"makelist\"" and target_atom "\"val\"" and target_atom "\"next\"") + +axiomatization + incr_loc :: "loc_ \ loc_" + and zero_loc :: "loc_" + +code_const incr_loc and zero_loc + (SML target_atom "(_ + 1)" and target_atom "0") + +axiomatization + test_loc :: "(loc_ \ bool) \ (loc_ \ 'a) \ loc_ \ 'a" where + "test_loc p v l = (if p l then v l else test_loc p v (incr l))" + +definition + new_addr' :: "(loc \ (cname \ (vname \ cname \ val option)) option) \ loc \ val option" + "new_addr' hp = + test_loc (\i. is_none (hp (Loc i) )) (\i. (Loc i, None)) zero_loc" + +lemma [code func]: + "wf_class = wf_class" .. + +code_const + wf_class (SML target_atom "(fn _ => true)") + +code_constsubst + new_Addr \ new_addr' + +definition + "test = exec (E, start_state E test_name makelist_name)" + + subsection {* Single step execution *} code_module JVM