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