src/HOL/Bali/Term.thy

+(*  Title:      isabelle/Bali/Term.thy
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   1997 Technische Universitaet Muenchen
+*)
+
+header {* Java expressions and statements *}
+
+theory Term = Value:
+
+text {*
+design issues:
+\begin{itemize}
+\item invocation frames for local variables could be reduced to special static
+  objects (one per method). This would reduce redundancy, but yield a rather
+  non-standard execution model more difficult to understand.
+\item method bodies separated from calls to handle assumptions in axiomat. 
+  semantics
+  NB: Body is intended to be in the environment of the called method.
+\item class initialization is regarded as (auxiliary) statement 
+      (required for AxSem)
+\item result expression of method return is handled by a special result variable
+  result variable is treated uniformly with local variables
+  \begin{itemize}
+  \item[+] welltypedness and existence of the result/return expression is 
+           ensured without extra efford
+  \end{itemize}
+\end{itemize}
+
+simplifications:
+\begin{itemize}
+\item expression statement allowed for any expression
+\item no unary, binary, etc, operators
+\item This  is modeled as a special non-assignable local variable
+\item Super is modeled as a general expression with the same value as This
+\item access to field x in current class via This.x
+\item NewA creates only one-dimensional arrays;
+  initialization of further subarrays may be simulated with nested NewAs
+\item The 'Lit' constructor is allowed to contain a reference value.
+  But this is assumed to be prohibited in the input language, which is enforced
+  by the type-checking rules.
+\item a call of a static method via a type name may be simulated by a dummy 
+      variable
+\item no nested blocks with inner local variables
+\item no synchronized statements
+\item no secondary forms of if, while (e.g. no for) (may be easily simulated)
+\item no switch (may be simulated with if)
+\item the @{text try_catch_finally} statement is divided into the 
+      @{text try_catch} statement 
+      and a finally statement, which may be considered as try..finally with 
+      empty catch
+\item the @{text try_catch} statement has exactly one catch clause; 
+      multiple ones can be
+  simulated with instanceof
+\item the compiler is supposed to add the annotations {@{text _}} during 
+      type-checking. This
+  transformation is left out as its result is checked by the type rules anyway
+\end{itemize}
+*}
+
+datatype inv_mode                  (* invocation mode for method calls *)
+	= Static                   (* static *)
+	| SuperM                   (* super  *)
+	| IntVir                   (* interface or virtual *)
+
+record  sig =            (* signature of a method, cf. 8.4.2  *)
+	  name ::"mname"      (* acutally belongs to Decl.thy *)
+          parTs::"ty list"        
+
+translations
+  "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
+  "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
+
+datatype jump
+        = Break label (* break *)
+        | Cont label  (* continue *)
+        | Ret         (* return from method *)
+
+datatype var
+	= LVar                  lname(* local variable (incl. parameters) *)
+        | FVar qtname bool expr vname(*class field*)("{_,_}_.._"[10,10,85,99]90)
+	| AVar        expr expr      (* array component *) ("_.[_]"[90,10   ]90)
+
+and expr
+	= NewC qtname              (* class instance creation *)
+	| NewA ty expr             (* array creation *) ("New _[_]"[99,10   ]85)
+	| Cast ty expr             (* type cast  *)
+	| Inst expr ref_ty         (* instanceof *)     ("_ InstOf _"[85,99] 85)
+	| Lit  val                 (* literal value, references not allowed *)
+	| Super                    (* special Super keyword *)
+	| Acc  var                 (* variable access *)
+	| Ass  var expr            (* variable assign *) ("_:=_"   [90,85   ]85)
+	| Cond expr expr expr      (* conditional *)  ("_ ? _ : _" [85,85,80]80)
+        | Call ref_ty inv_mode expr mname "(ty list)" (* method call *)
+                  "(expr list)" ("{_,_}_\<cdot>_'( {_}_')"[10,10,85,99,10,10]85)
+        | Methd qtname sig          (*   (folded) method (see below) *)
+        | Body qtname stmt          (* (unfolded) method body *)
+and  stmt
+	= Skip                     (* empty      statement *)
+	| Expr  expr               (* expression statement *)
+        | Lab   label stmt         ("_\<bullet> _"(* labeled statement*)[      99,66]66)
+                                   (* handles break *)
+	| Comp  stmt stmt          ("_;; _"                     [      66,65]65)
+	| If_   expr stmt stmt     ("If'(_') _ Else _"          [   80,79,79]70)
+	| Loop  label expr stmt    ("_\<bullet> While'(_') _"           [   99,80,79]70)
+        | Do jump                  (* break, continue, return *)
+	| Throw expr
+        | TryC  stmt
+	        qtname vname stmt   ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
+	| Fin   stmt stmt          ("_ Finally _"               [      79,79]70)
+	| Init  qtname              (* class initialization *)
+
+
+text {*
+The expressions Methd and Body are artificial program constructs, in the
+sense that they are not used to define a concrete Bali program. In the 
+evaluation semantic definition they are "generated on the fly" to decompose 
+the task to define the behaviour of the Call expression. They are crucial 
+for the axiomatic semantics to give a syntactic hook to insert 
+some assertions (cf. AxSem.thy, Eval.thy).
+Also the Init statement (to initialize a class on its first use) is inserted 
+in various places by the evaluation semantics.   
+*}
+ 
+types "term" = "(expr+stmt, var, expr list) sum3"
+translations
+  "sig"   <= (type) "mname \<times> ty list"
+  "var"   <= (type) "Term.var"
+  "expr"  <= (type) "Term.expr"
+  "stmt"  <= (type) "Term.stmt"
+  "term"  <= (type) "(expr+stmt, var, expr list) sum3"
+
+syntax
+  
+  this    :: expr
+  LAcc    :: "vname \<Rightarrow>         expr" ("!!")
+  LAss    :: "vname \<Rightarrow> expr \<Rightarrow> stmt" ("_:==_" [90,85] 85)
+  Return  :: "expr \<Rightarrow> stmt"
+  StatRef :: "ref_ty \<Rightarrow> expr"
+
+translations
+  
+ "this"       == "Acc (LVar This)"
+ "!!v"        == "Acc (LVar (EName (VNam v)))"
+ "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
+ "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Do Ret" 
+                                                   (* Res := e;; Do Ret *)
+ "StatRef rt" == "Cast (RefT rt) (Lit Null)"
+  
+constdefs
+
+  is_stmt :: "term \<Rightarrow> bool"
+ "is_stmt t \<equiv> \<exists>c. t=In1r c"
+
+ML {*
+bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
+*}
+
+declare is_stmt_rews [simp]
+
+
+(* ############# Just testing syntax *)
+(** unfortunately cannot simply instantiate tnam **)
+(*
+datatype tnam_  = HasFoo_ | Base_ | Ext_
+datatype vnam_  = arr_ | vee_ | z_ | e_
+datatype label_ = lab1_
+
+consts
+
+  tnam_ :: "tnam_  \<Rightarrow> tnam"
+  vnam_ :: "vnam_  \<Rightarrow> vname"
+  label_:: "label_ \<Rightarrow> label"
+axioms  
+
+  inj_tnam_  [simp]: "(tnam_  x = tnam_  y) = (x = y)"
+  inj_vnam_  [simp]: "(vnam_  x = vnam_  y) = (x = y)"
+  inj_label_ [simp]: "(label_ x = label_ y) = (x = y)"
+  
+  
+  surj_tnam_:  "\<exists>m. n = tnam_  m"
+  surj_vnam_:  "\<exists>m. n = vnam_  m"
+  surj_label_:" \<exists>m. n = label_ m"
+
+syntax
+
+  HasFoo :: qtname
+  Base   :: qtname
+  Ext    :: qtname
+  arr :: ename
+  vee :: ename
+  z   :: ename
+  e   :: ename
+  lab1:: label
+
+consts
+  
+  foo    :: mname
+translations
+
+  "HasFoo" == "\<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
+  "Base"   == "\<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
+  "Ext"    == "\<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
+  "arr"    ==        "(vnam_ arr_)"
+  "vee"    ==        "(vnam_ vee_)"
+  "z"      ==        "(vnam_ z_)"
+  "e"      ==        "(vnam_ e_)"
+  "lab1"   ==        "label_ lab1_"
+
+constdefs test::stmt
+"test \<equiv>
+(lab1@ While(Acc  
+      (Acc ({Base,True}StatRef (ClassT Object).arr).[Lit (Intg #2)])) Skip)"
+
+consts
+ pTs :: "ty list"
+   
+constdefs 
+
+test1::stmt
+"test1 \<equiv> 
+  Expr({ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))"
+
+
+
+constdefs test::stmt
+"test \<equiv>
+(lab1\<cdot> While(Acc 
+      (Acc ({Base,True}StatRef (ClassT Object)..arr).[Lit (Intg #2)])) Skip)"
+*)
+end