src/HOL/MicroJava/J/JListExample.thy
author wenzelm
Fri Feb 17 15:42:26 2012 +0100 (2012-02-17)
changeset 46512 4f9f61f9b535
parent 46506 c7faa011bfa7
child 51272 9c8d63b4b6be
permissions -rw-r--r--
simplified configuration options for syntax ambiguity;
     1 (*  Title:      HOL/MicroJava/J/JListExample.thy
     2     Author:     Stefan Berghofer
     3 *)
     4 
     5 header {* \isaheader{Example for generating executable code from Java semantics} *}
     6 
     7 theory JListExample
     8 imports Eval
     9 begin
    10 
    11 declare [[syntax_ambiguity_warning = false]]
    12 
    13 consts
    14   list_nam :: cnam
    15   append_name :: mname
    16 
    17 axiomatization val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam :: vnam
    18 where distinct_fields: "val_name \<noteq> next_name"
    19   and distinct_vars:
    20   "l_nam \<noteq> l1_nam" "l_nam \<noteq> l2_nam" "l_nam \<noteq> l3_nam" "l_nam \<noteq> l4_nam"
    21   "l1_nam \<noteq> l2_nam" "l1_nam \<noteq> l3_nam" "l1_nam \<noteq> l4_nam"
    22   "l2_nam \<noteq> l3_nam" "l2_nam \<noteq> l4_nam"
    23   "l3_nam \<noteq> l4_nam"
    24 
    25 definition list_name :: cname where
    26   "list_name = Cname list_nam"
    27 
    28 definition val_name :: vname where
    29   "val_name == VName val_nam"
    30 
    31 definition next_name :: vname where
    32   "next_name == VName next_nam"
    33 
    34 definition l_name :: vname where
    35   "l_name == VName l_nam"
    36 
    37 definition l1_name :: vname where
    38   "l1_name == VName l1_nam"
    39 
    40 definition l2_name :: vname where
    41   "l2_name == VName l2_nam"
    42 
    43 definition l3_name :: vname where
    44   "l3_name == VName l3_nam"
    45 
    46 definition l4_name :: vname where
    47   "l4_name == VName l4_nam"
    48 
    49 definition list_class :: "java_mb class" where
    50   "list_class ==
    51     (Object,
    52      [(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))],
    53      [((append_name, [RefT (ClassT list_name)]), PrimT Void,
    54       ([l_name], [],
    55        If(BinOp Eq ({list_name}(LAcc This)..next_name) (Lit Null))
    56          Expr ({list_name}(LAcc This)..next_name:=LAcc l_name)
    57        Else
    58          Expr ({list_name}({list_name}(LAcc This)..next_name)..
    59            append_name({[RefT (ClassT list_name)]}[LAcc l_name])), 
    60        Lit Unit))])"
    61 
    62 definition example_prg :: "java_mb prog" where
    63   "example_prg == [ObjectC, (list_name, list_class)]"
    64 
    65 code_datatype list_nam
    66 lemma equal_cnam_code [code]:
    67   "HOL.equal list_nam list_nam \<longleftrightarrow> True"
    68   by(simp add: equal_cnam_def)
    69 
    70 code_datatype append_name
    71 lemma equal_mname_code [code]:
    72   "HOL.equal append_name append_name \<longleftrightarrow> True"
    73   by(simp add: equal_mname_def)
    74 
    75 code_datatype val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam 
    76 lemma equal_vnam_code [code]: 
    77   "HOL.equal val_nam val_nam \<longleftrightarrow> True"
    78   "HOL.equal next_nam next_nam \<longleftrightarrow> True"
    79   "HOL.equal l_nam l_nam \<longleftrightarrow> True"
    80   "HOL.equal l1_nam l1_nam \<longleftrightarrow> True"
    81   "HOL.equal l2_nam l2_nam \<longleftrightarrow> True"
    82   "HOL.equal l3_nam l3_nam \<longleftrightarrow> True"
    83   "HOL.equal l4_nam l4_nam \<longleftrightarrow> True"
    84 
    85   "HOL.equal val_nam next_nam \<longleftrightarrow> False"
    86   "HOL.equal next_nam val_nam \<longleftrightarrow> False"
    87 
    88   "HOL.equal l_nam l1_nam \<longleftrightarrow> False"
    89   "HOL.equal l_nam l2_nam \<longleftrightarrow> False"
    90   "HOL.equal l_nam l3_nam \<longleftrightarrow> False"
    91   "HOL.equal l_nam l4_nam \<longleftrightarrow> False"
    92 
    93   "HOL.equal l1_nam l_nam \<longleftrightarrow> False"
    94   "HOL.equal l1_nam l2_nam \<longleftrightarrow> False"
    95   "HOL.equal l1_nam l3_nam \<longleftrightarrow> False"
    96   "HOL.equal l1_nam l4_nam \<longleftrightarrow> False"
    97 
    98   "HOL.equal l2_nam l_nam \<longleftrightarrow> False"
    99   "HOL.equal l2_nam l1_nam \<longleftrightarrow> False"
   100   "HOL.equal l2_nam l3_nam \<longleftrightarrow> False"
   101   "HOL.equal l2_nam l4_nam \<longleftrightarrow> False"
   102 
   103   "HOL.equal l3_nam l_nam \<longleftrightarrow> False"
   104   "HOL.equal l3_nam l1_nam \<longleftrightarrow> False"
   105   "HOL.equal l3_nam l2_nam \<longleftrightarrow> False"
   106   "HOL.equal l3_nam l4_nam \<longleftrightarrow> False"
   107 
   108   "HOL.equal l4_nam l_nam \<longleftrightarrow> False"
   109   "HOL.equal l4_nam l1_nam \<longleftrightarrow> False"
   110   "HOL.equal l4_nam l2_nam \<longleftrightarrow> False"
   111   "HOL.equal l4_nam l3_nam \<longleftrightarrow> False"
   112   by(simp_all add: distinct_fields distinct_fields[symmetric] distinct_vars distinct_vars[symmetric] equal_vnam_def)
   113 
   114 axiomatization where
   115   nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
   116 
   117 lemma equal_loc'_code [code]:
   118   "HOL.equal (nat_to_loc' l) (nat_to_loc' l') \<longleftrightarrow> l = l'"
   119   by(simp add: equal_loc'_def nat_to_loc'_inject)
   120 
   121 definition undefined_cname :: cname 
   122   where [code del]: "undefined_cname = undefined"
   123 declare undefined_cname_def[symmetric, code_unfold]
   124 code_datatype Object Xcpt Cname undefined_cname
   125 
   126 definition undefined_val :: val
   127   where [code del]: "undefined_val = undefined"
   128 declare undefined_val_def[symmetric, code_unfold]
   129 code_datatype Unit Null Bool Intg Addr undefined_val
   130 
   131 definition E where 
   132   "E = Expr (l1_name::=NewC list_name);;
   133        Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));;
   134        Expr (l2_name::=NewC list_name);;
   135        Expr ({list_name}(LAcc l2_name)..val_name:=Lit (Intg 2));;
   136        Expr (l3_name::=NewC list_name);;
   137        Expr ({list_name}(LAcc l3_name)..val_name:=Lit (Intg 3));;
   138        Expr (l4_name::=NewC list_name);;
   139        Expr ({list_name}(LAcc l4_name)..val_name:=Lit (Intg 4));;
   140        Expr ({list_name}(LAcc l1_name)..
   141          append_name({[RefT (ClassT list_name)]}[LAcc l2_name]));;
   142        Expr ({list_name}(LAcc l1_name)..
   143          append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));;
   144        Expr ({list_name}(LAcc l1_name)..
   145          append_name({[RefT (ClassT list_name)]}[LAcc l4_name]))"
   146 
   147 definition test where
   148   "test = Predicate.Pred (\<lambda>s. example_prg\<turnstile>Norm (empty, empty) -E-> s)"
   149 
   150 lemma test_code [code]:
   151   "test = exec_i_i_i_o example_prg (Norm (empty, empty)) E"
   152 by(auto intro: exec_i_i_i_oI intro!: pred_eqI elim: exec_i_i_i_oE simp add: test_def)
   153 
   154 ML {* 
   155   val SOME ((_, (heap, locs)), _) = Predicate.yield @{code test};
   156   locs @{code l1_name};
   157   locs @{code l2_name};
   158   locs @{code l3_name};
   159   locs @{code l4_name};
   160 
   161   fun list_fields n = 
   162     @{code snd} (@{code the} (heap (@{code Loc} (@{code "nat_to_loc'"} n))));
   163   fun val_field n =
   164     list_fields n (@{code val_name}, @{code "list_name"});
   165   fun next_field n =
   166     list_fields n (@{code next_name}, @{code "list_name"});
   167   val Suc = @{code Suc};
   168 
   169   val_field @{code "0 :: nat"};
   170   next_field @{code "0 :: nat"};
   171 
   172   val_field @{code "1 :: nat"};
   173   next_field @{code "1 :: nat"};
   174 
   175   val_field (Suc (Suc @{code "0 :: nat"}));
   176   next_field (Suc (Suc @{code "0 :: nat"}));
   177 
   178   val_field (Suc (Suc (Suc @{code "0 :: nat"})));
   179   next_field (Suc (Suc (Suc @{code "0 :: nat"})));
   180 *}
   181 
   182 end