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