src/HOL/Bali/Term.thy
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Bali/Term.thy	Mon Jan 28 17:00:19 2002 +0100
     1.3 @@ -0,0 +1,231 @@
     1.4 +(*  Title:      isabelle/Bali/Term.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   1997 Technische Universitaet Muenchen
     1.8 +*)
     1.9 +
    1.10 +header {* Java expressions and statements *}
    1.11 +
    1.12 +theory Term = Value:
    1.13 +
    1.14 +text {*
    1.15 +design issues:
    1.16 +\begin{itemize}
    1.17 +\item invocation frames for local variables could be reduced to special static
    1.18 +  objects (one per method). This would reduce redundancy, but yield a rather
    1.19 +  non-standard execution model more difficult to understand.
    1.20 +\item method bodies separated from calls to handle assumptions in axiomat. 
    1.21 +  semantics
    1.22 +  NB: Body is intended to be in the environment of the called method.
    1.23 +\item class initialization is regarded as (auxiliary) statement 
    1.24 +      (required for AxSem)
    1.25 +\item result expression of method return is handled by a special result variable
    1.26 +  result variable is treated uniformly with local variables
    1.27 +  \begin{itemize}
    1.28 +  \item[+] welltypedness and existence of the result/return expression is 
    1.29 +           ensured without extra efford
    1.30 +  \end{itemize}
    1.31 +\end{itemize}
    1.32 +
    1.33 +simplifications:
    1.34 +\begin{itemize}
    1.35 +\item expression statement allowed for any expression
    1.36 +\item no unary, binary, etc, operators
    1.37 +\item This  is modeled as a special non-assignable local variable
    1.38 +\item Super is modeled as a general expression with the same value as This
    1.39 +\item access to field x in current class via This.x
    1.40 +\item NewA creates only one-dimensional arrays;
    1.41 +  initialization of further subarrays may be simulated with nested NewAs
    1.42 +\item The 'Lit' constructor is allowed to contain a reference value.
    1.43 +  But this is assumed to be prohibited in the input language, which is enforced
    1.44 +  by the type-checking rules.
    1.45 +\item a call of a static method via a type name may be simulated by a dummy 
    1.46 +      variable
    1.47 +\item no nested blocks with inner local variables
    1.48 +\item no synchronized statements
    1.49 +\item no secondary forms of if, while (e.g. no for) (may be easily simulated)
    1.50 +\item no switch (may be simulated with if)
    1.51 +\item the @{text try_catch_finally} statement is divided into the 
    1.52 +      @{text try_catch} statement 
    1.53 +      and a finally statement, which may be considered as try..finally with 
    1.54 +      empty catch
    1.55 +\item the @{text try_catch} statement has exactly one catch clause; 
    1.56 +      multiple ones can be
    1.57 +  simulated with instanceof
    1.58 +\item the compiler is supposed to add the annotations {@{text _}} during 
    1.59 +      type-checking. This
    1.60 +  transformation is left out as its result is checked by the type rules anyway
    1.61 +\end{itemize}
    1.62 +*}
    1.63 +
    1.64 +datatype inv_mode                  (* invocation mode for method calls *)
    1.65 +	= Static                   (* static *)
    1.66 +	| SuperM                   (* super  *)
    1.67 +	| IntVir                   (* interface or virtual *)
    1.68 +
    1.69 +record  sig =            (* signature of a method, cf. 8.4.2  *)
    1.70 +	  name ::"mname"      (* acutally belongs to Decl.thy *)
    1.71 +          parTs::"ty list"        
    1.72 +
    1.73 +translations
    1.74 +  "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
    1.75 +  "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
    1.76 +
    1.77 +datatype jump
    1.78 +        = Break label (* break *)
    1.79 +        | Cont label  (* continue *)
    1.80 +        | Ret         (* return from method *)
    1.81 +
    1.82 +datatype var
    1.83 +	= LVar                  lname(* local variable (incl. parameters) *)
    1.84 +        | FVar qtname bool expr vname(*class field*)("{_,_}_.._"[10,10,85,99]90)
    1.85 +	| AVar        expr expr      (* array component *) ("_.[_]"[90,10   ]90)
    1.86 +
    1.87 +and expr
    1.88 +	= NewC qtname              (* class instance creation *)
    1.89 +	| NewA ty expr             (* array creation *) ("New _[_]"[99,10   ]85)
    1.90 +	| Cast ty expr             (* type cast  *)
    1.91 +	| Inst expr ref_ty         (* instanceof *)     ("_ InstOf _"[85,99] 85)
    1.92 +	| Lit  val                 (* literal value, references not allowed *)
    1.93 +	| Super                    (* special Super keyword *)
    1.94 +	| Acc  var                 (* variable access *)
    1.95 +	| Ass  var expr            (* variable assign *) ("_:=_"   [90,85   ]85)
    1.96 +	| Cond expr expr expr      (* conditional *)  ("_ ? _ : _" [85,85,80]80)
    1.97 +        | Call ref_ty inv_mode expr mname "(ty list)" (* method call *)
    1.98 +                  "(expr list)" ("{_,_}_\<cdot>_'( {_}_')"[10,10,85,99,10,10]85)
    1.99 +        | Methd qtname sig          (*   (folded) method (see below) *)
   1.100 +        | Body qtname stmt          (* (unfolded) method body *)
   1.101 +and  stmt
   1.102 +	= Skip                     (* empty      statement *)
   1.103 +	| Expr  expr               (* expression statement *)
   1.104 +        | Lab   label stmt         ("_\<bullet> _"(* labeled statement*)[      99,66]66)
   1.105 +                                   (* handles break *)
   1.106 +	| Comp  stmt stmt          ("_;; _"                     [      66,65]65)
   1.107 +	| If_   expr stmt stmt     ("If'(_') _ Else _"          [   80,79,79]70)
   1.108 +	| Loop  label expr stmt    ("_\<bullet> While'(_') _"           [   99,80,79]70)
   1.109 +        | Do jump                  (* break, continue, return *)
   1.110 +	| Throw expr
   1.111 +        | TryC  stmt
   1.112 +	        qtname vname stmt   ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
   1.113 +	| Fin   stmt stmt          ("_ Finally _"               [      79,79]70)
   1.114 +	| Init  qtname              (* class initialization *)
   1.115 +
   1.116 +
   1.117 +text {*
   1.118 +The expressions Methd and Body are artificial program constructs, in the
   1.119 +sense that they are not used to define a concrete Bali program. In the 
   1.120 +evaluation semantic definition they are "generated on the fly" to decompose 
   1.121 +the task to define the behaviour of the Call expression. They are crucial 
   1.122 +for the axiomatic semantics to give a syntactic hook to insert 
   1.123 +some assertions (cf. AxSem.thy, Eval.thy).
   1.124 +Also the Init statement (to initialize a class on its first use) is inserted 
   1.125 +in various places by the evaluation semantics.   
   1.126 +*}
   1.127 + 
   1.128 +types "term" = "(expr+stmt, var, expr list) sum3"
   1.129 +translations
   1.130 +  "sig"   <= (type) "mname \<times> ty list"
   1.131 +  "var"   <= (type) "Term.var"
   1.132 +  "expr"  <= (type) "Term.expr"
   1.133 +  "stmt"  <= (type) "Term.stmt"
   1.134 +  "term"  <= (type) "(expr+stmt, var, expr list) sum3"
   1.135 +
   1.136 +syntax
   1.137 +  
   1.138 +  this    :: expr
   1.139 +  LAcc    :: "vname \<Rightarrow>         expr" ("!!")
   1.140 +  LAss    :: "vname \<Rightarrow> expr \<Rightarrow> stmt" ("_:==_" [90,85] 85)
   1.141 +  Return  :: "expr \<Rightarrow> stmt"
   1.142 +  StatRef :: "ref_ty \<Rightarrow> expr"
   1.143 +
   1.144 +translations
   1.145 +  
   1.146 + "this"       == "Acc (LVar This)"
   1.147 + "!!v"        == "Acc (LVar (EName (VNam v)))"
   1.148 + "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
   1.149 + "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Do Ret" 
   1.150 +                                                   (* Res := e;; Do Ret *)
   1.151 + "StatRef rt" == "Cast (RefT rt) (Lit Null)"
   1.152 +  
   1.153 +constdefs
   1.154 +
   1.155 +  is_stmt :: "term \<Rightarrow> bool"
   1.156 + "is_stmt t \<equiv> \<exists>c. t=In1r c"
   1.157 +
   1.158 +ML {*
   1.159 +bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
   1.160 +*}
   1.161 +
   1.162 +declare is_stmt_rews [simp]
   1.163 +
   1.164 +
   1.165 +(* ############# Just testing syntax *)
   1.166 +(** unfortunately cannot simply instantiate tnam **)
   1.167 +(*
   1.168 +datatype tnam_  = HasFoo_ | Base_ | Ext_
   1.169 +datatype vnam_  = arr_ | vee_ | z_ | e_
   1.170 +datatype label_ = lab1_
   1.171 +
   1.172 +consts
   1.173 +
   1.174 +  tnam_ :: "tnam_  \<Rightarrow> tnam"
   1.175 +  vnam_ :: "vnam_  \<Rightarrow> vname"
   1.176 +  label_:: "label_ \<Rightarrow> label"
   1.177 +axioms  
   1.178 +
   1.179 +  inj_tnam_  [simp]: "(tnam_  x = tnam_  y) = (x = y)"
   1.180 +  inj_vnam_  [simp]: "(vnam_  x = vnam_  y) = (x = y)"
   1.181 +  inj_label_ [simp]: "(label_ x = label_ y) = (x = y)"
   1.182 +  
   1.183 +  
   1.184 +  surj_tnam_:  "\<exists>m. n = tnam_  m"
   1.185 +  surj_vnam_:  "\<exists>m. n = vnam_  m"
   1.186 +  surj_label_:" \<exists>m. n = label_ m"
   1.187 +
   1.188 +syntax
   1.189 +
   1.190 +  HasFoo :: qtname
   1.191 +  Base   :: qtname
   1.192 +  Ext    :: qtname
   1.193 +  arr :: ename
   1.194 +  vee :: ename
   1.195 +  z   :: ename
   1.196 +  e   :: ename
   1.197 +  lab1:: label
   1.198 +
   1.199 +consts
   1.200 +  
   1.201 +  foo    :: mname
   1.202 +translations
   1.203 +
   1.204 +  "HasFoo" == "\<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
   1.205 +  "Base"   == "\<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
   1.206 +  "Ext"    == "\<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
   1.207 +  "arr"    ==        "(vnam_ arr_)"
   1.208 +  "vee"    ==        "(vnam_ vee_)"
   1.209 +  "z"      ==        "(vnam_ z_)"
   1.210 +  "e"      ==        "(vnam_ e_)"
   1.211 +  "lab1"   ==        "label_ lab1_"
   1.212 +
   1.213 +constdefs test::stmt
   1.214 +"test \<equiv>
   1.215 +(lab1@ While(Acc  
   1.216 +      (Acc ({Base,True}StatRef (ClassT Object).arr).[Lit (Intg #2)])) Skip)"
   1.217 +
   1.218 +consts
   1.219 + pTs :: "ty list"
   1.220 +   
   1.221 +constdefs 
   1.222 +
   1.223 +test1::stmt
   1.224 +"test1 \<equiv> 
   1.225 +  Expr({ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))"
   1.226 +
   1.227 +
   1.228 +
   1.229 +constdefs test::stmt
   1.230 +"test \<equiv>
   1.231 +(lab1\<cdot> While(Acc 
   1.232 +      (Acc ({Base,True}StatRef (ClassT Object)..arr).[Lit (Intg #2)])) Skip)"
   1.233 +*)
   1.234 +end
   1.235 \ No newline at end of file