src/HOL/Bali/Term.thy
author schirmer
Mon, 28 Jan 2002 17:00:19 +0100
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
permissions -rw-r--r--
Isabelle/Bali sources;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     1
(*  Title:      isabelle/Bali/Term.thy
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
    Copyright   1997 Technische Universitaet Muenchen
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
header {* Java expressions and statements *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
theory Term = Value:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
design issues:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
\item invocation frames for local variables could be reduced to special static
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
  objects (one per method). This would reduce redundancy, but yield a rather
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
  non-standard execution model more difficult to understand.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
\item method bodies separated from calls to handle assumptions in axiomat. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
  semantics
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
  NB: Body is intended to be in the environment of the called method.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
\item class initialization is regarded as (auxiliary) statement 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
      (required for AxSem)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
\item result expression of method return is handled by a special result variable
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
  result variable is treated uniformly with local variables
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
  \begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
  \item[+] welltypedness and existence of the result/return expression is 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
           ensured without extra efford
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
  \end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
simplifications:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
\item expression statement allowed for any expression
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
\item no unary, binary, etc, operators
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
\item This  is modeled as a special non-assignable local variable
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
\item Super is modeled as a general expression with the same value as This
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
\item access to field x in current class via This.x
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
\item NewA creates only one-dimensional arrays;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
  initialization of further subarrays may be simulated with nested NewAs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
\item The 'Lit' constructor is allowed to contain a reference value.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
  But this is assumed to be prohibited in the input language, which is enforced
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
  by the type-checking rules.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
\item a call of a static method via a type name may be simulated by a dummy 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
      variable
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
\item no nested blocks with inner local variables
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
\item no synchronized statements
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
\item no secondary forms of if, while (e.g. no for) (may be easily simulated)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
\item no switch (may be simulated with if)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
\item the @{text try_catch_finally} statement is divided into the 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
      @{text try_catch} statement 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
      and a finally statement, which may be considered as try..finally with 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
      empty catch
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
\item the @{text try_catch} statement has exactly one catch clause; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
      multiple ones can be
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
  simulated with instanceof
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
\item the compiler is supposed to add the annotations {@{text _}} during 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
      type-checking. This
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
  transformation is left out as its result is checked by the type rules anyway
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
datatype inv_mode                  (* invocation mode for method calls *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
	= Static                   (* static *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
	| SuperM                   (* super  *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
	| IntVir                   (* interface or virtual *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
record  sig =            (* signature of a method, cf. 8.4.2  *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
	  name ::"mname"      (* acutally belongs to Decl.thy *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
          parTs::"ty list"        
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
  "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
  "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
datatype jump
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
        = Break label (* break *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
        | Cont label  (* continue *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
        | Ret         (* return from method *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
datatype var
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
	= LVar                  lname(* local variable (incl. parameters) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
        | FVar qtname bool expr vname(*class field*)("{_,_}_.._"[10,10,85,99]90)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
	| AVar        expr expr      (* array component *) ("_.[_]"[90,10   ]90)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
and expr
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
	= NewC qtname              (* class instance creation *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
	| NewA ty expr             (* array creation *) ("New _[_]"[99,10   ]85)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
	| Cast ty expr             (* type cast  *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
	| Inst expr ref_ty         (* instanceof *)     ("_ InstOf _"[85,99] 85)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
	| Lit  val                 (* literal value, references not allowed *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
	| Super                    (* special Super keyword *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
	| Acc  var                 (* variable access *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
	| Ass  var expr            (* variable assign *) ("_:=_"   [90,85   ]85)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
	| Cond expr expr expr      (* conditional *)  ("_ ? _ : _" [85,85,80]80)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
        | Call ref_ty inv_mode expr mname "(ty list)" (* method call *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
                  "(expr list)" ("{_,_}_\<cdot>_'( {_}_')"[10,10,85,99,10,10]85)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
        | Methd qtname sig          (*   (folded) method (see below) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
        | Body qtname stmt          (* (unfolded) method body *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
and  stmt
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
	= Skip                     (* empty      statement *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
	| Expr  expr               (* expression statement *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
        | Lab   label stmt         ("_\<bullet> _"(* labeled statement*)[      99,66]66)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
                                   (* handles break *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
	| Comp  stmt stmt          ("_;; _"                     [      66,65]65)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
	| If_   expr stmt stmt     ("If'(_') _ Else _"          [   80,79,79]70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
	| Loop  label expr stmt    ("_\<bullet> While'(_') _"           [   99,80,79]70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
        | Do jump                  (* break, continue, return *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
	| Throw expr
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
        | TryC  stmt
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
	        qtname vname stmt   ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
	| Fin   stmt stmt          ("_ Finally _"               [      79,79]70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
	| Init  qtname              (* class initialization *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
The expressions Methd and Body are artificial program constructs, in the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
sense that they are not used to define a concrete Bali program. In the 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
evaluation semantic definition they are "generated on the fly" to decompose 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
the task to define the behaviour of the Call expression. They are crucial 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
for the axiomatic semantics to give a syntactic hook to insert 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
some assertions (cf. AxSem.thy, Eval.thy).
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
Also the Init statement (to initialize a class on its first use) is inserted 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
in various places by the evaluation semantics.   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
types "term" = "(expr+stmt, var, expr list) sum3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
  "sig"   <= (type) "mname \<times> ty list"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
  "var"   <= (type) "Term.var"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
  "expr"  <= (type) "Term.expr"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
  "stmt"  <= (type) "Term.stmt"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
  "term"  <= (type) "(expr+stmt, var, expr list) sum3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
  this    :: expr
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
  LAcc    :: "vname \<Rightarrow>         expr" ("!!")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
  LAss    :: "vname \<Rightarrow> expr \<Rightarrow> stmt" ("_:==_" [90,85] 85)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
  Return  :: "expr \<Rightarrow> stmt"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
  StatRef :: "ref_ty \<Rightarrow> expr"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
 "this"       == "Acc (LVar This)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
 "!!v"        == "Acc (LVar (EName (VNam v)))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
 "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
 "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Do Ret" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
                                                   (* Res := e;; Do Ret *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
 "StatRef rt" == "Cast (RefT rt) (Lit Null)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
  is_stmt :: "term \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
 "is_stmt t \<equiv> \<exists>c. t=In1r c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
ML {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
declare is_stmt_rews [simp]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
(* ############# Just testing syntax *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
(** unfortunately cannot simply instantiate tnam **)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
datatype tnam_  = HasFoo_ | Base_ | Ext_
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
datatype vnam_  = arr_ | vee_ | z_ | e_
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
datatype label_ = lab1_
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
  tnam_ :: "tnam_  \<Rightarrow> tnam"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
  vnam_ :: "vnam_  \<Rightarrow> vname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
  label_:: "label_ \<Rightarrow> label"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
axioms  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
  inj_tnam_  [simp]: "(tnam_  x = tnam_  y) = (x = y)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
  inj_vnam_  [simp]: "(vnam_  x = vnam_  y) = (x = y)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
  inj_label_ [simp]: "(label_ x = label_ y) = (x = y)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
  surj_tnam_:  "\<exists>m. n = tnam_  m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
  surj_vnam_:  "\<exists>m. n = vnam_  m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
  surj_label_:" \<exists>m. n = label_ m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
  HasFoo :: qtname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
  Base   :: qtname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
  Ext    :: qtname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
  arr :: ename
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
  vee :: ename
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
  z   :: ename
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
  e   :: ename
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
  lab1:: label
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
  foo    :: mname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
  "HasFoo" == "\<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
  "Base"   == "\<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
  "Ext"    == "\<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
  "arr"    ==        "(vnam_ arr_)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
  "vee"    ==        "(vnam_ vee_)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
  "z"      ==        "(vnam_ z_)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
  "e"      ==        "(vnam_ e_)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
  "lab1"   ==        "label_ lab1_"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
constdefs test::stmt
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
"test \<equiv>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
(lab1@ While(Acc  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
      (Acc ({Base,True}StatRef (ClassT Object).arr).[Lit (Intg #2)])) Skip)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
 pTs :: "ty list"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
constdefs 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
test1::stmt
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
"test1 \<equiv> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
  Expr({ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
constdefs test::stmt
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
"test \<equiv>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
(lab1\<cdot> While(Acc 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
      (Acc ({Base,True}StatRef (ClassT Object)..arr).[Lit (Intg #2)])) Skip)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
end