# HG changeset patch # User Andreas Lochbihler # Date 1312556114 -7200 # Node ID 25011c3a5c3de5fade49da30baf0af6be55df6fb # Parent 322d1657c40c0083db4d053ff92930b7f74290b4 replace old SML code generator by new code generator in MicroJava/J diff -r 322d1657c40c -r 25011c3a5c3d src/HOL/MicroJava/J/Eval.thy --- a/src/HOL/MicroJava/J/Eval.thy Fri Aug 05 14:16:44 2011 +0200 +++ b/src/HOL/MicroJava/J/Eval.thy Fri Aug 05 16:55:14 2011 +0200 @@ -189,4 +189,55 @@ apply (fast) done + +lemma eval_LAcc_code: "G\Norm (h, l) -LAcc v\the (l v)-> Norm (h, l)" +using LAcc[of G "(h, l)" v] by simp + +lemma eval_Call_code: + "[| G\Norm s0 -e\a'-> s1; a = the_Addr a'; + G\s1 -ps[\]pvs-> (x,(h,l)); dynT = fst (the (h a)); + (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs)); + G\(np a' x,(h,(init_vars lvars)(pns[\]pvs)(This\a'))) -blk-> s3; + G\ s3 -res\v -> (x4,(h4, l4)) |] ==> + G\Norm s0 -{C}e..mn({pTs}ps)\v-> (x4,(h4,l))" +using Call[of G s0 e a' s1 a ps pvs x h l dynT md rT pns lvars blk res mn pTs s3 v x4 "(h4, l4)" C] +by simp + +lemmas [code_pred_intro] = XcptE NewC Cast Lit BinOp +lemmas [code_pred_intro LAcc_code] = eval_LAcc_code +lemmas [code_pred_intro] = LAss FAcc FAss +lemmas [code_pred_intro Call_code] = eval_Call_code +lemmas [code_pred_intro] = XcptEs Nil Cons XcptS Skip Expr Comp Cond LoopF +lemmas [code_pred_intro LoopT_code] = LoopT + +code_pred + (modes: + eval: i \ i \ i \ o \ o \ bool + and + evals: i \ i \ i \ o \ o \ bool + and + exec: i \ i \ i \ o \ bool) + eval +proof - + case eval + from eval.prems show thesis + proof(cases (no_simp)) + case LAcc with LAcc_code show ?thesis by auto + next + case (Call a b c d e f g h i j k l m n o p q r s t u v s4) + with Call_code show ?thesis + by(cases "s4")(simp, (erule meta_allE meta_impE|rule conjI refl| assumption)+) + qed(erule (3) that[OF refl]|assumption)+ +next + case evals + from evals.prems show thesis + by(cases (no_simp))(erule (3) that[OF refl]|assumption)+ +next + case exec + from exec.prems show thesis + proof(cases (no_simp)) + case LoopT thus ?thesis by(rule LoopT_code[OF refl]) + qed(erule (2) that[OF refl]|assumption)+ +qed + end diff -r 322d1657c40c -r 25011c3a5c3d src/HOL/MicroJava/J/JListExample.thy --- a/src/HOL/MicroJava/J/JListExample.thy Fri Aug 05 14:16:44 2011 +0200 +++ b/src/HOL/MicroJava/J/JListExample.thy Fri Aug 05 16:55:14 2011 +0200 @@ -11,15 +11,19 @@ declare [[syntax_ambiguity_level = 100000]] consts - list_name :: cname + list_nam :: cnam append_name :: mname - val_nam :: vnam - next_nam :: vnam - l_nam :: vnam - l1_nam :: vnam - l2_nam :: vnam - l3_nam :: vnam - l4_nam :: vnam + +axiomatization val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam :: vnam +where distinct_fields: "val_name \ next_name" + and distinct_vars: + "l_nam \ l1_nam" "l_nam \ l2_nam" "l_nam \ l3_nam" "l_nam \ l4_nam" + "l1_nam \ l2_nam" "l1_nam \ l3_nam" "l1_nam \ l4_nam" + "l2_nam \ l3_nam" "l2_nam \ l4_nam" + "l3_nam \ l4_nam" + +definition list_name :: cname where + "list_name = Cname list_nam" definition val_name :: vname where "val_name == VName val_nam" @@ -58,71 +62,119 @@ definition example_prg :: "java_mb prog" where "example_prg == [ObjectC, (list_name, list_class)]" -types_code - cname ("string") - vnam ("string") - mname ("string") - loc' ("int") +code_datatype list_nam +lemma equal_cnam_code [code]: + "HOL.equal list_nam list_nam \ True" + by(simp add: equal_cnam_def) + +code_datatype append_name +lemma equal_mname_code [code]: + "HOL.equal append_name append_name \ True" + by(simp add: equal_mname_def) -consts_code - "new_Addr" ("\new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}") -attach {* -fun new_addr p none loc hp = - let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1); - in nr 0 end; -*} +code_datatype val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam +lemma equal_vnam_code [code]: + "HOL.equal val_nam val_nam \ True" + "HOL.equal next_nam next_nam \ True" + "HOL.equal l_nam l_nam \ True" + "HOL.equal l1_nam l1_nam \ True" + "HOL.equal l2_nam l2_nam \ True" + "HOL.equal l3_nam l3_nam \ True" + "HOL.equal l4_nam l4_nam \ True" + + "HOL.equal val_nam next_nam \ False" + "HOL.equal next_nam val_nam \ False" - "undefined" ("(raise Match)") - "undefined :: val" ("{* Unit *}") - "undefined :: cname" ("\"\"") + "HOL.equal l_nam l1_nam \ False" + "HOL.equal l_nam l2_nam \ False" + "HOL.equal l_nam l3_nam \ False" + "HOL.equal l_nam l4_nam \ False" + + "HOL.equal l1_nam l_nam \ False" + "HOL.equal l1_nam l2_nam \ False" + "HOL.equal l1_nam l3_nam \ False" + "HOL.equal l1_nam l4_nam \ False" + + "HOL.equal l2_nam l_nam \ False" + "HOL.equal l2_nam l1_nam \ False" + "HOL.equal l2_nam l3_nam \ False" + "HOL.equal l2_nam l4_nam \ False" - "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\"") + "HOL.equal l3_nam l_nam \ False" + "HOL.equal l3_nam l1_nam \ False" + "HOL.equal l3_nam l2_nam \ False" + "HOL.equal l3_nam l4_nam \ False" + + "HOL.equal l4_nam l_nam \ False" + "HOL.equal l4_nam l1_nam \ False" + "HOL.equal l4_nam l2_nam \ False" + "HOL.equal l4_nam l3_nam \ False" + by(simp_all add: distinct_fields distinct_fields[symmetric] distinct_vars distinct_vars[symmetric] equal_vnam_def) + +axioms nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \ l = l'" +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) -code_module J -contains - test = "example_prg\Norm (empty, 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])))-> _" +definition undefined_cname :: cname + where [code del]: "undefined_cname = undefined" +declare undefined_cname_def[symmetric, code_inline] +code_datatype Object Xcpt Cname undefined_cname + +definition undefined_val :: val + where [code del]: "undefined_val = undefined" +declare undefined_val_def[symmetric, code_inline] +code_datatype Unit Null Bool Intg Addr undefined_val + +definition E where + "E = 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]))" + +definition test where + "test = Predicate.Pred (\s. example_prg\Norm (empty, empty) -E-> s)" -section {* Big step execution *} +lemma test_code [code]: + "test = exec_i_i_i_o example_prg (Norm (empty, empty)) E" +by(auto intro: exec_i_i_i_oI intro!: pred_eqI elim: exec_i_i_i_oE simp add: test_def) -ML {* +ML {* + val SOME ((_, (heap, locs)), _) = Predicate.yield @{code test}; + locs @{code l1_name}; + locs @{code l2_name}; + locs @{code l3_name}; + locs @{code l4_name}; -val SOME ((_, (heap, locs)), _) = DSeq.pull J.test; -locs J.l1_name; -locs J.l2_name; -locs J.l3_name; -locs J.l4_name; -snd (J.the (heap (J.Loc 0))) (J.val_name, "list"); -snd (J.the (heap (J.Loc 0))) (J.next_name, "list"); -snd (J.the (heap (J.Loc 1))) (J.val_name, "list"); -snd (J.the (heap (J.Loc 1))) (J.next_name, "list"); -snd (J.the (heap (J.Loc 2))) (J.val_name, "list"); -snd (J.the (heap (J.Loc 2))) (J.next_name, "list"); -snd (J.the (heap (J.Loc 3))) (J.val_name, "list"); -snd (J.the (heap (J.Loc 3))) (J.next_name, "list"); + fun list_fields n = + @{code snd} (@{code the} (heap (@{code Loc} (@{code "nat_to_loc'"} n)))); + fun val_field n = + list_fields n (@{code val_name}, @{code "list_name"}); + fun next_field n = + list_fields n (@{code next_name}, @{code "list_name"}); + val Suc = @{code Suc}; + val_field @{code "0 :: nat"}; + next_field @{code "0 :: nat"}; + + val_field @{code "1 :: nat"}; + next_field @{code "1 :: nat"}; + + val_field (Suc (Suc @{code "0 :: nat"})); + next_field (Suc (Suc @{code "0 :: nat"})); + + val_field (Suc (Suc (Suc @{code "0 :: nat"}))); + next_field (Suc (Suc (Suc @{code "0 :: nat"}))); *} end diff -r 322d1657c40c -r 25011c3a5c3d src/HOL/MicroJava/J/Type.thy --- a/src/HOL/MicroJava/J/Type.thy Fri Aug 05 14:16:44 2011 +0200 +++ b/src/HOL/MicroJava/J/Type.thy Fri Aug 05 16:55:14 2011 +0200 @@ -12,6 +12,20 @@ definition "HOL.equal (cn :: cnam) cn' \ cn = cn'" instance proof qed(simp add: equal_cnam_def) end +text {* These instantiations only ensure that the merge in theory @{text "MicroJava"} succeeds. FIXME *} +instantiation cnam :: typerep begin +definition "typerep_class.typerep \ \_ :: cnam itself. Typerep.Typerep (STR ''Type.cnam'') []" +instance proof qed +end +instantiation cnam :: term_of begin +definition "term_of_class.term_of (C :: cnam) \ + Code_Evaluation.Const (STR ''dummy_cnam'') (Typerep.Typerep (STR ''Type.cnam'') [])" +instance proof qed +end +instantiation cnam :: partial_term_of begin +definition "partial_term_of_class.partial_term_of (C :: cnam itself) n = undefined" +instance proof qed +end -- "exceptions" datatype @@ -31,12 +45,38 @@ definition "HOL.equal (vn :: vnam) vn' \ vn = vn'" instance proof qed(simp add: equal_vnam_def) end +instantiation vnam :: typerep begin +definition "typerep_class.typerep \ \_ :: vnam itself. Typerep.Typerep (STR ''Type.vnam'') []" +instance proof qed +end +instantiation vnam :: term_of begin +definition "term_of_class.term_of (V :: vnam) \ + Code_Evaluation.Const (STR ''dummy_vnam'') (Typerep.Typerep (STR ''Type.vnam'') [])" +instance proof qed +end +instantiation vnam :: partial_term_of begin +definition "partial_term_of_class.partial_term_of (V :: vnam itself) n = undefined" +instance proof qed +end typedecl mname -- "method name" instantiation mname :: equal begin definition "HOL.equal (M :: mname) M' \ M = M'" instance proof qed(simp add: equal_mname_def) end +instantiation mname :: typerep begin +definition "typerep_class.typerep \ \_ :: mname itself. Typerep.Typerep (STR ''Type.mname'') []" +instance proof qed +end +instantiation mname :: term_of begin +definition "term_of_class.term_of (M :: mname) \ + Code_Evaluation.Const (STR ''dummy_mname'') (Typerep.Typerep (STR ''Type.mname'') [])" +instance proof qed +end +instantiation mname :: partial_term_of begin +definition "partial_term_of_class.partial_term_of (M :: mname itself) n = undefined" +instance proof qed +end -- "names for @{text This} pointer and local/field variables" datatype vname