src/HOL/Bali/Term.thy
changeset 32960 69916a850301
parent 27226 5a3e5e46d977
child 35067 af4c18c30593
     1.1 --- a/src/HOL/Bali/Term.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Bali/Term.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -67,8 +67,8 @@
     1.4          | Ret         --{* return from method *}
     1.5  
     1.6  datatype xcpt        --{* exception *}
     1.7 -	= Loc loc    --{* location of allocated execption object *}
     1.8 -	| Std xname  --{* intermediate standard exception, see Eval.thy *}
     1.9 +        = Loc loc    --{* location of allocated execption object *}
    1.10 +        | Std xname  --{* intermediate standard exception, see Eval.thy *}
    1.11  
    1.12  datatype error
    1.13         =  AccessViolation  --{* Access to a member that isn't permitted *}
    1.14 @@ -92,12 +92,12 @@
    1.15   "locals" <= (type) "(lname, val) table"
    1.16  
    1.17  datatype inv_mode                  --{* invocation mode for method calls *}
    1.18 -	= Static                   --{* static *}
    1.19 -	| SuperM                   --{* super  *}
    1.20 -	| IntVir                   --{* interface or virtual *}
    1.21 +        = Static                   --{* static *}
    1.22 +        | SuperM                   --{* super  *}
    1.23 +        | IntVir                   --{* interface or virtual *}
    1.24  
    1.25  record  sig =              --{* signature of a method, cf. 8.4.2  *}
    1.26 -	  name ::"mname"   --{* acutally belongs to Decl.thy *}
    1.27 +          name ::"mname"   --{* acutally belongs to Decl.thy *}
    1.28            parTs::"ty list"        
    1.29  
    1.30  translations
    1.31 @@ -142,7 +142,7 @@
    1.32  *}
    1.33  
    1.34  datatype var
    1.35 -	= LVar lname --{* local variable (incl. parameters) *}
    1.36 +        = LVar lname --{* local variable (incl. parameters) *}
    1.37          | FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90)
    1.38                       --{* class field *}
    1.39                       --{* @{term "{accC,statDeclC,stat}e..fn"}   *}
    1.40 @@ -153,7 +153,7 @@
    1.41                       --{* @{text stat}: static or instance field?*}
    1.42                       --{* @{text e}: reference to object*}
    1.43                       --{* @{text fn}: field name*}
    1.44 -	| AVar expr expr ("_.[_]"[90,10   ]90)
    1.45 +        | AVar expr expr ("_.[_]"[90,10   ]90)
    1.46                       --{* array component *}
    1.47                       --{* @{term "e1.[e2]"}: e1 array reference; e2 index *}
    1.48          | InsInitV stmt var 
    1.49 @@ -161,21 +161,21 @@
    1.50                       --{* of var (technical term for smallstep semantics.)*}
    1.51  
    1.52  and expr
    1.53 -	= NewC qtname         --{* class instance creation *}
    1.54 -	| NewA ty expr ("New _[_]"[99,10   ]85) 
    1.55 +        = NewC qtname         --{* class instance creation *}
    1.56 +        | NewA ty expr ("New _[_]"[99,10   ]85) 
    1.57                                --{* array creation *} 
    1.58 -	| Cast ty expr        --{* type cast  *}
    1.59 -	| Inst expr ref_ty ("_ InstOf _"[85,99] 85)   
    1.60 +        | Cast ty expr        --{* type cast  *}
    1.61 +        | Inst expr ref_ty ("_ InstOf _"[85,99] 85)   
    1.62                                --{* instanceof *}     
    1.63 -	| Lit  val              --{* literal value, references not allowed *}
    1.64 +        | Lit  val              --{* literal value, references not allowed *}
    1.65          | UnOp unop expr        --{* unary operation *}
    1.66          | BinOp binop expr expr --{* binary operation *}
    1.67          
    1.68 -	| Super               --{* special Super keyword *}
    1.69 -	| Acc  var            --{* variable access *}
    1.70 -	| Ass  var expr       ("_:=_"   [90,85   ]85)
    1.71 +        | Super               --{* special Super keyword *}
    1.72 +        | Acc  var            --{* variable access *}
    1.73 +        | Ass  var expr       ("_:=_"   [90,85   ]85)
    1.74                                --{* variable assign *} 
    1.75 -	| Cond expr expr expr ("_ ? _ : _" [85,85,80]80) --{* conditional *}  
    1.76 +        | Cond expr expr expr ("_ ? _ : _" [85,85,80]80) --{* conditional *}  
    1.77          | Call qtname ref_ty inv_mode expr mname "(ty list)" "(expr list)"  
    1.78              ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85) 
    1.79                      --{* method call *} 
    1.80 @@ -198,25 +198,25 @@
    1.81          | Callee locals expr  --{* save callers locals in callee-Frame *}
    1.82                                --{* (technical term for smallstep semantics) *}
    1.83  and  stmt
    1.84 -	= Skip                  --{* empty      statement *}
    1.85 -	| Expr  expr            --{* expression statement *}
    1.86 +        = Skip                  --{* empty      statement *}
    1.87 +        | Expr  expr            --{* expression statement *}
    1.88          | Lab   jump stmt       ("_\<bullet> _" [      99,66]66)
    1.89                                  --{* labeled statement; handles break *}
    1.90 -	| Comp  stmt stmt       ("_;; _"                  [      66,65]65)
    1.91 -	| If'   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
    1.92 -	| Loop  label expr stmt ("_\<bullet> While'(_') _"        [   99,80,79]70)
    1.93 +        | Comp  stmt stmt       ("_;; _"                  [      66,65]65)
    1.94 +        | If'   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
    1.95 +        | Loop  label expr stmt ("_\<bullet> While'(_') _"        [   99,80,79]70)
    1.96          | Jmp jump              --{* break, continue, return *}
    1.97 -	| Throw expr
    1.98 +        | Throw expr
    1.99          | TryC  stmt qtname vname stmt ("Try _ Catch'(_ _') _"  [79,99,80,79]70)
   1.100               --{* @{term "Try c1 Catch(C vn) c2"} *} 
   1.101               --{* @{text c1}: block were exception may be thrown *}
   1.102               --{* @{text C}:  execption class to catch *}
   1.103               --{* @{text vn}: local name for exception used in @{text c2}*}
   1.104               --{* @{text c2}: block to execute when exception is cateched*}
   1.105 -	| Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
   1.106 +        | Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
   1.107          | FinA abopt stmt       --{* Save abruption of first statement *} 
   1.108                                  --{* technical term  for smallstep sem.) *}
   1.109 -	| Init  qtname          --{* class initialization *}
   1.110 +        | Init  qtname          --{* class initialization *}
   1.111  
   1.112  
   1.113  text {*