src/HOL/MicroJava/J/JListExample.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24783 5a3e336a2e37
child 28524 644b62cf678f
permissions -rw-r--r--
Name.uu, Name.aT;
kleing@12951
     1
(*  Title:      HOL/MicroJava/J/JListExample.thy
berghofe@12442
     2
    ID:         $Id$
berghofe@12442
     3
    Author:     Stefan Berghofer
berghofe@12442
     4
*)
berghofe@12442
     5
kleing@12911
     6
header {* \isaheader{Example for generating executable code from Java semantics} *}
berghofe@12442
     7
haftmann@16417
     8
theory JListExample imports Eval SystemClasses begin
berghofe@12442
     9
berghofe@12442
    10
ML {* Syntax.ambiguity_level := 100000 *}
berghofe@12442
    11
berghofe@12442
    12
consts
berghofe@12442
    13
  list_name :: cname
berghofe@12442
    14
  append_name :: mname
berghofe@12442
    15
  val_nam :: vnam
berghofe@12442
    16
  next_nam :: vnam
berghofe@12442
    17
  l_nam :: vnam
berghofe@12442
    18
  l1_nam :: vnam
berghofe@12442
    19
  l2_nam :: vnam
berghofe@12442
    20
  l3_nam :: vnam
berghofe@12442
    21
  l4_nam :: vnam
berghofe@12442
    22
berghofe@12442
    23
constdefs
berghofe@12442
    24
  val_name :: vname
berghofe@12442
    25
  "val_name == VName val_nam"
berghofe@12442
    26
berghofe@12442
    27
  next_name :: vname
berghofe@12442
    28
  "next_name == VName next_nam"
berghofe@12442
    29
berghofe@12442
    30
  l_name :: vname
berghofe@12442
    31
  "l_name == VName l_nam"
berghofe@12442
    32
berghofe@12442
    33
  l1_name :: vname
berghofe@12442
    34
  "l1_name == VName l1_nam"
berghofe@12442
    35
berghofe@12442
    36
  l2_name :: vname
berghofe@12442
    37
  "l2_name == VName l2_nam"
berghofe@12442
    38
berghofe@12442
    39
  l3_name :: vname
berghofe@12442
    40
  "l3_name == VName l3_nam"
berghofe@12442
    41
berghofe@12442
    42
  l4_name :: vname
berghofe@12442
    43
  "l4_name == VName l4_nam"
berghofe@12442
    44
berghofe@12442
    45
  list_class :: "java_mb class"
berghofe@12442
    46
  "list_class ==
berghofe@12442
    47
    (Object,
berghofe@12442
    48
     [(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))],
berghofe@12442
    49
     [((append_name, [RefT (ClassT list_name)]), PrimT Void,
berghofe@12442
    50
      ([l_name], [],
berghofe@12442
    51
       If(BinOp Eq ({list_name}(LAcc This)..next_name) (Lit Null))
berghofe@12442
    52
         Expr ({list_name}(LAcc This)..next_name:=LAcc l_name)
berghofe@12442
    53
       Else
berghofe@12442
    54
         Expr ({list_name}({list_name}(LAcc This)..next_name)..
berghofe@12442
    55
           append_name({[RefT (ClassT list_name)]}[LAcc l_name])), 
berghofe@12442
    56
       Lit Unit))])"
berghofe@12442
    57
berghofe@12442
    58
  example_prg :: "java_mb prog"
berghofe@12442
    59
  "example_prg == [ObjectC, (list_name, list_class)]"
berghofe@12442
    60
berghofe@12442
    61
types_code
berghofe@12442
    62
  cname ("string")
berghofe@12442
    63
  vnam ("string")
berghofe@12442
    64
  mname ("string")
wenzelm@24783
    65
  loc' ("int")
berghofe@12442
    66
berghofe@12442
    67
consts_code
berghofe@16770
    68
  "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}")
berghofe@16770
    69
attach {*
berghofe@16770
    70
fun new_addr p none loc hp =
berghofe@16770
    71
  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
berghofe@16770
    72
  in nr 0 end;
berghofe@16770
    73
*}
berghofe@12442
    74
wenzelm@18679
    75
  "arbitrary" ("(raise Match)")
haftmann@22921
    76
  "arbitrary :: val" ("{* Unit *}")
haftmann@22921
    77
  "arbitrary :: cname" ("\"\"")
berghofe@12442
    78
berghofe@12442
    79
  "Object" ("\"Object\"")
berghofe@12442
    80
  "list_name" ("\"list\"")
berghofe@12442
    81
  "append_name" ("\"append\"")
berghofe@12442
    82
  "val_nam" ("\"val\"")
berghofe@12442
    83
  "next_nam" ("\"next\"")
berghofe@12442
    84
  "l_nam" ("\"l\"")
berghofe@12442
    85
  "l1_nam" ("\"l1\"")
berghofe@12442
    86
  "l2_nam" ("\"l2\"")
berghofe@12442
    87
  "l3_nam" ("\"l3\"")
berghofe@12442
    88
  "l4_nam" ("\"l4\"")
berghofe@12442
    89
berghofe@17145
    90
code_module J
berghofe@17145
    91
contains
nipkow@13890
    92
  test = "example_prg\<turnstile>Norm (empty, empty)
berghofe@12442
    93
    -(Expr (l1_name::=NewC list_name);;
berghofe@12442
    94
      Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));;
berghofe@12442
    95
      Expr (l2_name::=NewC list_name);;
berghofe@12442
    96
      Expr ({list_name}(LAcc l2_name)..val_name:=Lit (Intg 2));;
berghofe@12442
    97
      Expr (l3_name::=NewC list_name);;
berghofe@12442
    98
      Expr ({list_name}(LAcc l3_name)..val_name:=Lit (Intg 3));;
berghofe@12442
    99
      Expr (l4_name::=NewC list_name);;
berghofe@12442
   100
      Expr ({list_name}(LAcc l4_name)..val_name:=Lit (Intg 4));;
berghofe@12442
   101
      Expr ({list_name}(LAcc l1_name)..
berghofe@12442
   102
        append_name({[RefT (ClassT list_name)]}[LAcc l2_name]));;
berghofe@12442
   103
      Expr ({list_name}(LAcc l1_name)..
berghofe@12442
   104
        append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));;
berghofe@12442
   105
      Expr ({list_name}(LAcc l1_name)..
berghofe@12565
   106
        append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> _"
berghofe@12442
   107
kleing@12911
   108
section {* Big step execution *}
berghofe@12442
   109
berghofe@12442
   110
ML {*
berghofe@12442
   111
berghofe@24460
   112
val SOME ((_, (heap, locs)), _) = DSeq.pull J.test;
berghofe@17145
   113
locs J.l1_name;
berghofe@17145
   114
locs J.l2_name;
berghofe@17145
   115
locs J.l3_name;
berghofe@17145
   116
locs J.l4_name;
berghofe@17145
   117
snd (J.the (heap (J.Loc 0))) (J.val_name, "list");
berghofe@17145
   118
snd (J.the (heap (J.Loc 0))) (J.next_name, "list");
berghofe@17145
   119
snd (J.the (heap (J.Loc 1))) (J.val_name, "list");
berghofe@17145
   120
snd (J.the (heap (J.Loc 1))) (J.next_name, "list");
berghofe@17145
   121
snd (J.the (heap (J.Loc 2))) (J.val_name, "list");
berghofe@17145
   122
snd (J.the (heap (J.Loc 2))) (J.next_name, "list");
berghofe@17145
   123
snd (J.the (heap (J.Loc 3))) (J.val_name, "list");
berghofe@17145
   124
snd (J.the (heap (J.Loc 3))) (J.next_name, "list");
berghofe@12442
   125
berghofe@12442
   126
*}
berghofe@12442
   127
berghofe@12442
   128
end