src/HOL/Bali/Term.thy
author schirmer
Thu Jul 11 09:36:41 2002 +0200 (2002-07-11)
changeset 13345 bd611943cbc2
parent 13337 f75dfc606ac7
child 13358 c837ba4cfb62
permissions -rw-r--r--
Fixed markup error in comment.
     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  -- {*{\tt ^}   bitwise Xor*}
   132                | Xor     -- {*{\tt ^}   boolean Xor*}
   133                | BitOr   -- {*{\tt |}   bitwise Or*}
   134                | Or      -- {*{\tt |}   boolean Or*}
   135 text{* The boolean operators {\tt &} and {\tt |} strictly evaluate both
   136 of their arguments. The lazy operators {\tt &&} and {\tt ||} are modeled
   137 as instances of the @{text Cond} expression: {\tt a && b = a?b:false} and
   138   {\tt a || b = a?true:b}
   139 *}
   140 datatype var
   141 	= LVar                  lname(* local variable (incl. parameters) *)
   142         | FVar qtname qtname bool expr vname
   143                                 (*class field*)("{_,_,_}_.._"[10,10,10,85,99]90)
   144 	| AVar expr expr    (* array component *) ("_.[_]"[90,10   ]90)
   145         | InsInitV stmt var (* insertion of initialization before
   146                                    evaluation of var (for smallstep sem.) *)
   147 
   148 and expr
   149 	= NewC qtname         (* class instance creation *)
   150 	| NewA ty expr        (* array creation *) ("New _[_]"[99,10   ]85)
   151 	| Cast ty expr        (* type cast  *)
   152 	| Inst expr ref_ty    (* instanceof *)     ("_ InstOf _"[85,99] 85)
   153 	| Lit  val            (* literal value, references not allowed *)
   154         | UnOp unop expr        (* unary operation *)
   155         | BinOp binop expr expr (* binary operation *)
   156         
   157 	| Super               (* special Super keyword *)
   158 	| Acc  var            (* variable access *)
   159 	| Ass  var expr       (* variable assign *) ("_:=_"   [90,85   ]85)
   160 	| Cond expr expr expr (* conditional *)  ("_ ? _ : _" [85,85,80]80)
   161         | Call qtname ref_ty inv_mode expr mname "(ty list)" 
   162                "(expr list)"  (* method call *) 
   163                               ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85)
   164         | Methd qtname sig    (*   (folded) method (see below) *)
   165         | Body qtname stmt    (* (unfolded) method body *)
   166         | InsInitE stmt expr      (* insertion of initialization before
   167                                    evaluation of expr (for smallstep sem.) *)
   168         | Callee locals expr      (* save Callers locals in Callee-Frame
   169                                      (for smallstep semantics) *)
   170 and  stmt
   171 	= Skip                  (* empty      statement *)
   172 	| Expr  expr            (* expression statement *)
   173         | Lab   jump stmt       ("_\<bullet> _"(* labeled statement*)[      99,66]66)
   174                                 (* handles break *)
   175 	| Comp  stmt stmt       ("_;; _"                  [      66,65]65)
   176 	| If_   expr stmt stmt  ("If'(_') _ Else _"          [   80,79,79]70)
   177 	| Loop  label expr stmt ("_\<bullet> While'(_') _"           [   99,80,79]70)
   178         | Do jump               (* break, continue, return *)
   179 	| Throw expr
   180         | TryC  stmt
   181 	     qtname vname stmt ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
   182 	| Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
   183         | FinA abopt stmt        (* Save abruption of first statement 
   184                                     (for smallstep sem.) *)
   185 	| Init  qtname              (* class initialization *)
   186 
   187 
   188 text {*
   189 The expressions Methd and Body are artificial program constructs, in the
   190 sense that they are not used to define a concrete Bali program. In the 
   191 operational semantic's they are "generated on the fly" 
   192 to decompose the task to define the behaviour of the Call expression. 
   193 They are crucial for the axiomatic semantics to give a syntactic hook to insert 
   194 some assertions (cf. AxSem.thy, Eval.thy). 
   195 The Init statement (to initialize a class on its first use) is 
   196 inserted in various places by the semantics. 
   197 Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps in the
   198 smallstep (transition) semantics (cf. Trans.thy). Callee is used to save the 
   199 local variables of the caller for method return. So ve avoid modelling a 
   200 frame stack.
   201 The InsInitV/E terms are only used by the smallstep semantics to model the
   202 intermediate steps of class-initialisation.
   203 *}
   204  
   205 types "term" = "(expr+stmt,var,expr list) sum3"
   206 translations
   207   "sig"   <= (type) "mname \<times> ty list"
   208   "var"   <= (type) "Term.var"
   209   "expr"  <= (type) "Term.expr"
   210   "stmt"  <= (type) "Term.stmt"
   211   "term"  <= (type) "(expr+stmt,var,expr list) sum3"
   212 
   213 syntax
   214   
   215   this    :: expr
   216   LAcc    :: "vname \<Rightarrow> expr" ("!!")
   217   LAss    :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
   218   Return  :: "expr \<Rightarrow> stmt"
   219   StatRef :: "ref_ty \<Rightarrow> expr"
   220 
   221 translations
   222   
   223  "this"       == "Acc (LVar This)"
   224  "!!v"        == "Acc (LVar (EName (VNam v)))"
   225  "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
   226  "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Do Ret" 
   227                                                    (* Res := e;; Do Ret *)
   228  "StatRef rt" == "Cast (RefT rt) (Lit Null)"
   229   
   230 constdefs
   231 
   232   is_stmt :: "term \<Rightarrow> bool"
   233  "is_stmt t \<equiv> \<exists>c. t=In1r c"
   234 
   235 ML {*
   236 bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
   237 *}
   238 
   239 declare is_stmt_rews [simp]
   240 
   241 axclass inj_term < "type"
   242 consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83)
   243 
   244 instance stmt::inj_term ..
   245 
   246 defs (overloaded)
   247 stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
   248 
   249 lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
   250 by (simp add: stmt_inj_term_def)
   251 
   252 instance expr::inj_term ..
   253 
   254 defs (overloaded)
   255 expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
   256 
   257 lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
   258 by (simp add: expr_inj_term_def)
   259 
   260 instance var::inj_term ..
   261 
   262 defs (overloaded)
   263 var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
   264 
   265 lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
   266 by (simp add: var_inj_term_def)
   267 
   268 instance "list":: (type) inj_term ..
   269 
   270 defs (overloaded)
   271 expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
   272 
   273 lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
   274 by (simp add: expr_list_inj_term_def)
   275 
   276 end