src/HOL/Bali/Term.thy
author berghofe
Mon Sep 30 16:14:02 2002 +0200 (2002-09-30)
changeset 13601 fd3e3d6b37b2
parent 13384 a34e38154413
child 13688 a0b16d42d489
permissions -rw-r--r--
Adapted to new simplifier.
     1 (*  Title:      HOL/Bali/Term.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 
     7 header {* Java expressions and statements *}
     8 
     9 theory Term = Value + Table:
    10 
    11 text {*
    12 design issues:
    13 \begin{itemize}
    14 \item invocation frames for local variables could be reduced to special static
    15   objects (one per method). This would reduce redundancy, but yield a rather
    16   non-standard execution model more difficult to understand.
    17 \item method bodies separated from calls to handle assumptions in axiomat. 
    18   semantics
    19   NB: Body is intended to be in the environment of the called method.
    20 \item class initialization is regarded as (auxiliary) statement 
    21       (required for AxSem)
    22 \item result expression of method return is handled by a special result variable
    23   result variable is treated uniformly with local variables
    24   \begin{itemize}
    25   \item[+] welltypedness and existence of the result/return expression is 
    26            ensured without extra efford
    27   \end{itemize}
    28 \end{itemize}
    29 
    30 simplifications:
    31 \begin{itemize}
    32 \item expression statement allowed for any expression
    33 \item no unary, binary, etc, operators
    34 \item This  is modeled as a special non-assignable local variable
    35 \item Super is modeled as a general expression with the same value as This
    36 \item access to field x in current class via This.x
    37 \item NewA creates only one-dimensional arrays;
    38   initialization of further subarrays may be simulated with nested NewAs
    39 \item The 'Lit' constructor is allowed to contain a reference value.
    40   But this is assumed to be prohibited in the input language, which is enforced
    41   by the type-checking rules.
    42 \item a call of a static method via a type name may be simulated by a dummy 
    43       variable
    44 \item no nested blocks with inner local variables
    45 \item no synchronized statements
    46 \item no secondary forms of if, while (e.g. no for) (may be easily simulated)
    47 \item no switch (may be simulated with if)
    48 \item the @{text try_catch_finally} statement is divided into the 
    49       @{text try_catch} statement 
    50       and a finally statement, which may be considered as try..finally with 
    51       empty catch
    52 \item the @{text try_catch} statement has exactly one catch clause; 
    53       multiple ones can be
    54   simulated with instanceof
    55 \item the compiler is supposed to add the annotations {@{text _}} during 
    56       type-checking. This
    57   transformation is left out as its result is checked by the type rules anyway
    58 \end{itemize}
    59 *}
    60 
    61 
    62 
    63 types locals = "(lname, val) table"  --{* local variables *}
    64 
    65 
    66 datatype jump
    67         = Break label --{* break *}
    68         | Cont label  --{* continue *}
    69         | Ret         --{* return from method *}
    70 
    71 datatype xcpt        --{* exception *}
    72 	= Loc loc    --{* location of allocated execption object *}
    73 	| Std xname  --{* intermediate standard exception, see Eval.thy *}
    74 
    75 datatype error
    76        = AccessViolation --{* Access to a member that isn't permitted *}
    77 
    78 datatype abrupt       --{* abrupt completion *} 
    79         = Xcpt xcpt   --{* exception *}
    80         | Jump jump   --{* break, continue, return *}
    81         | Error error -- {* runtime errors, we wan't to detect and proof absent
    82                             in welltyped programms *}
    83 types
    84   abopt  = "abrupt option"
    85 
    86 text {* Local variable store and exception. 
    87 Anticipation of State.thy used by smallstep semantics. For a method call, 
    88 we save the local variables of the caller in the term Callee to restore them 
    89 after method return. Also an exception must be restored after the finally
    90 statement *}
    91 
    92 translations
    93  "locals" <= (type) "(lname, val) table"
    94 
    95 datatype inv_mode                  --{* invocation mode for method calls *}
    96 	= Static                   --{* static *}
    97 	| SuperM                   --{* super  *}
    98 	| IntVir                   --{* interface or virtual *}
    99 
   100 record  sig =              --{* signature of a method, cf. 8.4.2  *}
   101 	  name ::"mname"   --{* acutally belongs to Decl.thy *}
   102           parTs::"ty list"        
   103 
   104 translations
   105   "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
   106   "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
   107 
   108 --{* function codes for unary operations *}
   109 datatype unop =  UPlus    -- {*{\tt +} unary plus*} 
   110                | UMinus   -- {*{\tt -} unary minus*}
   111                | UBitNot  -- {*{\tt ~} bitwise NOT*}
   112                | UNot     -- {*{\tt !} logical complement*}
   113 
   114 --{* function codes for binary operations *}
   115 datatype binop = Mul     -- {*{\tt * }   multiplication*}
   116                | Div     -- {*{\tt /}   division*}
   117                | Mod     -- {*{\tt \%}   remainder*}
   118                | Plus    -- {*{\tt +}   addition*}
   119                | Minus   -- {*{\tt -}   subtraction*}
   120                | LShift  -- {*{\tt <<}  left shift*}
   121                | RShift  -- {*{\tt >>}  signed right shift*}
   122                | RShiftU -- {*{\tt >>>} unsigned right shift*}
   123                | Less    -- {*{\tt <}   less than*}
   124                | Le      -- {*{\tt <=}  less than or equal*}
   125                | Greater -- {*{\tt >}   greater than*}
   126                | Ge      -- {*{\tt >=}  greater than or equal*}
   127                | Eq      -- {*{\tt ==}  equal*}
   128                | Neq     -- {*{\tt !=}  not equal*}
   129                | BitAnd  -- {*{\tt \&}   bitwise AND*}
   130                | And     -- {*{\tt \&}   boolean AND*}
   131                | BitXor  -- {*{\texttt \^}   bitwise Xor*}
   132                | Xor     -- {*{\texttt \^}   boolean Xor*}
   133                | BitOr   -- {*{\tt |}   bitwise Or*}
   134                | Or      -- {*{\tt |}   boolean Or*}
   135                | CondAnd -- {*{\tt \&\&}  conditional And*}
   136                | CondOr  -- {*{\tt ||}  conditional Or *}
   137 text{* The boolean operators {\tt \&} and {\tt |} strictly evaluate both
   138 of their arguments. The conditional operators {\tt \&\&} and {\tt ||} only 
   139 evaluate the second argument if the value of the whole expression isn't 
   140 allready determined by the first argument.
   141 e.g.: {\tt false \&\& e} e is not evaluated;  
   142       {\tt true || e} e is not evaluated; 
   143 *}
   144 
   145 datatype var
   146 	= LVar lname --{* local variable (incl. parameters) *}
   147         | FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90)
   148                      --{* class field *}
   149                      --{* @{term "{accC,statDeclC,stat}e..fn"}   *}
   150                      --{* @{text accC}: accessing class (static class were *}
   151                      --{* the code is declared. Annotation only needed for *}
   152                      --{* evaluation to check accessibility) *}
   153                      --{* @{text statDeclC}: static declaration class of field*}
   154                      --{* @{text stat}: static or instance field?*}
   155                      --{* @{text e}: reference to object*}
   156                      --{* @{text fn}: field name*}
   157 	| AVar expr expr ("_.[_]"[90,10   ]90)
   158                      --{* array component *}
   159                      --{* @{term "e1.[e2]"}: e1 array reference; e2 index *}
   160         | InsInitV stmt var 
   161                      --{* insertion of initialization before evaluation   *}
   162                      --{* of var (technical term for smallstep semantics.)*}
   163 
   164 and expr
   165 	= NewC qtname         --{* class instance creation *}
   166 	| NewA ty expr ("New _[_]"[99,10   ]85) 
   167                               --{* array creation *} 
   168 	| Cast ty expr        --{* type cast  *}
   169 	| Inst expr ref_ty ("_ InstOf _"[85,99] 85)   
   170                               --{* instanceof *}     
   171 	| Lit  val              --{* literal value, references not allowed *}
   172         | UnOp unop expr        --{* unary operation *}
   173         | BinOp binop expr expr --{* binary operation *}
   174         
   175 	| Super               --{* special Super keyword *}
   176 	| Acc  var            --{* variable access *}
   177 	| Ass  var expr       ("_:=_"   [90,85   ]85)
   178                               --{* variable assign *} 
   179 	| Cond expr expr expr ("_ ? _ : _" [85,85,80]80) --{* conditional *}  
   180         | Call qtname ref_ty inv_mode expr mname "(ty list)" "(expr list)"  
   181             ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85) 
   182                     --{* method call *} 
   183                     --{* @{term "{accC,statT,mode}e\<cdot>mn({pTs}args)"} " *}
   184                     --{* @{text accC}: accessing class (static class were *}
   185                     --{* the call code is declared. Annotation only needed for*}
   186                     --{* evaluation to check accessibility) *}
   187                     --{* @{text statT}: static declaration class/interface of *}
   188                     --{* method *}
   189                     --{* @{text mode}: invocation mode *}
   190                     --{* @{text e}: reference to object*}
   191                     --{* @{text mn}: field name*}   
   192                     --{* @{text pTs}: types of parameters *}
   193                     --{* @{text args}: the actual parameters/arguments *} 
   194         | Methd qtname sig    --{*   (folded) method (see below) *}
   195         | Body qtname stmt    --{* (unfolded) method body *}
   196         | InsInitE stmt expr  
   197                  --{* insertion of initialization before *}
   198                  --{* evaluation of expr (technical term for smallstep sem.) *}
   199         | Callee locals expr  --{* save callers locals in callee-Frame *}
   200                               --{* (technical term for smallstep semantics) *}
   201 and  stmt
   202 	= Skip                  --{* empty      statement *}
   203 	| Expr  expr            --{* expression statement *}
   204         | Lab   jump stmt       ("_\<bullet> _" [      99,66]66)
   205                                 --{* labeled statement; handles break *}
   206 	| Comp  stmt stmt       ("_;; _"                  [      66,65]65)
   207 	| If_   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
   208 	| Loop  label expr stmt ("_\<bullet> While'(_') _"        [   99,80,79]70)
   209         | Do jump               --{* break, continue, return *}
   210 	| Throw expr
   211         | TryC  stmt qtname vname stmt ("Try _ Catch'(_ _') _"  [79,99,80,79]70)
   212              --{* @{term "Try c1 Catch(C vn) c2"} *} 
   213              --{* @{text c1}: block were exception may be thrown *}
   214              --{* @{text C}:  execption class to catch *}
   215              --{* @{text vn}: local name for exception used in @{text c2}*}
   216              --{* @{text c2}: block to execute when exception is cateched*}
   217 	| Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
   218         | FinA abopt stmt       --{* Save abruption of first statement *} 
   219                                 --{* technical term  for smallstep sem.) *}
   220 	| Init  qtname          --{* class initialization *}
   221 
   222 
   223 text {*
   224 The expressions Methd and Body are artificial program constructs, in the
   225 sense that they are not used to define a concrete Bali program. In the 
   226 operational semantic's they are "generated on the fly" 
   227 to decompose the task to define the behaviour of the Call expression. 
   228 They are crucial for the axiomatic semantics to give a syntactic hook to insert 
   229 some assertions (cf. AxSem.thy, Eval.thy). 
   230 The Init statement (to initialize a class on its first use) is 
   231 inserted in various places by the semantics. 
   232 Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps in the
   233 smallstep (transition) semantics (cf. Trans.thy). Callee is used to save the 
   234 local variables of the caller for method return. So ve avoid modelling a 
   235 frame stack.
   236 The InsInitV/E terms are only used by the smallstep semantics to model the
   237 intermediate steps of class-initialisation.
   238 *}
   239  
   240 types "term" = "(expr+stmt,var,expr list) sum3"
   241 translations
   242   "sig"   <= (type) "mname \<times> ty list"
   243   "var"   <= (type) "Term.var"
   244   "expr"  <= (type) "Term.expr"
   245   "stmt"  <= (type) "Term.stmt"
   246   "term"  <= (type) "(expr+stmt,var,expr list) sum3"
   247 
   248 syntax
   249   
   250   this    :: expr
   251   LAcc    :: "vname \<Rightarrow> expr" ("!!")
   252   LAss    :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
   253   Return  :: "expr \<Rightarrow> stmt"
   254   StatRef :: "ref_ty \<Rightarrow> expr"
   255 
   256 translations
   257   
   258  "this"       == "Acc (LVar This)"
   259  "!!v"        == "Acc (LVar (EName (VNam v)))"
   260  "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
   261  "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Do Ret" 
   262                   --{* \tt Res := e;; Do Ret *}
   263  "StatRef rt" == "Cast (RefT rt) (Lit Null)"
   264   
   265 constdefs
   266 
   267   is_stmt :: "term \<Rightarrow> bool"
   268  "is_stmt t \<equiv> \<exists>c. t=In1r c"
   269 
   270 ML {*
   271 bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
   272 *}
   273 
   274 declare is_stmt_rews [simp]
   275 
   276 axclass inj_term < "type"
   277 consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83)
   278 
   279 instance stmt::inj_term ..
   280 
   281 defs (overloaded)
   282 stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
   283 
   284 lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
   285 by (simp add: stmt_inj_term_def)
   286 
   287 instance expr::inj_term ..
   288 
   289 defs (overloaded)
   290 expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
   291 
   292 lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
   293 by (simp add: expr_inj_term_def)
   294 
   295 instance var::inj_term ..
   296 
   297 defs (overloaded)
   298 var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
   299 
   300 lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
   301 by (simp add: var_inj_term_def)
   302 
   303 instance "list":: (type) inj_term ..
   304 
   305 defs (overloaded)
   306 expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
   307 
   308 lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
   309 by (simp add: expr_list_inj_term_def)
   310 
   311 end