src/HOL/MicroJava/Comp/TranslComp.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 13673 2950128b8206
child 16417 9bc16273c2d4
permissions -rw-r--r--
Merged in license change from Isabelle2004
streckem@13673
     1
(*  Title:      HOL/MicroJava/Comp/TranslComp.thy
streckem@13673
     2
    ID:         $Id$
streckem@13673
     3
    Author:     Martin Strecker
streckem@13673
     4
*)
streckem@13673
     5
streckem@13673
     6
(* Compiling MicroJava into MicroJVM -- Translation functions *)
streckem@13673
     7
streckem@13673
     8
theory TranslComp =  TranslCompTp:
streckem@13673
     9
streckem@13673
    10
streckem@13673
    11
(* parameter java_mb only serves to define function index later *)
streckem@13673
    12
consts
streckem@13673
    13
 compExpr  :: "java_mb => expr      => instr list"
streckem@13673
    14
 compExprs :: "java_mb => expr list => instr list"
streckem@13673
    15
 compStmt  :: "java_mb => stmt      => instr list"
streckem@13673
    16
streckem@13673
    17
streckem@13673
    18
streckem@13673
    19
(**********************************************************************)
streckem@13673
    20
(** code generation for expressions **)
streckem@13673
    21
streckem@13673
    22
primrec
streckem@13673
    23
(*class instance creation*)
streckem@13673
    24
"compExpr jmb (NewC c) = [New c]"
streckem@13673
    25
streckem@13673
    26
(*type cast*)
streckem@13673
    27
"compExpr jmb (Cast c e) = compExpr jmb e @ [Checkcast c]" 
streckem@13673
    28
streckem@13673
    29
streckem@13673
    30
(*literals*)
streckem@13673
    31
"compExpr jmb (Lit val) = [LitPush val]" 
streckem@13673
    32
streckem@13673
    33
      
streckem@13673
    34
(* binary operation *)                         
streckem@13673
    35
"compExpr jmb (BinOp bo e1 e2) = compExpr jmb e1 @ compExpr jmb e2 @ 
streckem@13673
    36
  (case bo of Eq => [Ifcmpeq 3,LitPush(Bool False),Goto 2,LitPush(Bool True)]
streckem@13673
    37
            | Add => [IAdd])" 
streckem@13673
    38
streckem@13673
    39
(*local variable*)
streckem@13673
    40
"compExpr jmb (LAcc vn) = [Load (index jmb vn)]" 
streckem@13673
    41
streckem@13673
    42
streckem@13673
    43
(*assignement*)
streckem@13673
    44
"compExpr jmb (vn::=e) = compExpr jmb e @ [Dup , Store (index jmb vn)]" 
streckem@13673
    45
streckem@13673
    46
streckem@13673
    47
(*field access*)
streckem@13673
    48
"compExpr jmb ( {cn}e..fn ) = compExpr jmb e @ [Getfield fn cn]"
streckem@13673
    49
streckem@13673
    50
streckem@13673
    51
(*field assignement - expected syntax:  {_}_.._:=_ *)
streckem@13673
    52
"compExpr jmb (FAss cn e1 fn e2 ) = 
streckem@13673
    53
       compExpr jmb e1 @ compExpr jmb e2 @ [Dup_x1 , Putfield fn cn]"
streckem@13673
    54
streckem@13673
    55
streckem@13673
    56
(*method call*)
streckem@13673
    57
"compExpr jmb (Call cn e1 mn X ps) = 
streckem@13673
    58
        compExpr jmb e1 @ compExprs jmb ps @ [Invoke cn mn X]"
streckem@13673
    59
streckem@13673
    60
streckem@13673
    61
(** code generation expression lists **)
streckem@13673
    62
streckem@13673
    63
"compExprs jmb []     = []"
streckem@13673
    64
streckem@13673
    65
"compExprs jmb (e#es) = compExpr jmb e @ compExprs jmb es"
streckem@13673
    66
streckem@13673
    67
  
streckem@13673
    68
streckem@13673
    69
primrec
streckem@13673
    70
(** code generation for statements **)
streckem@13673
    71
streckem@13673
    72
"compStmt jmb Skip = []"			
streckem@13673
    73
streckem@13673
    74
"compStmt jmb (Expr e) = ((compExpr jmb e) @ [Pop])"
streckem@13673
    75
streckem@13673
    76
"compStmt jmb (c1;; c2) = ((compStmt jmb c1) @ (compStmt jmb c2))"
streckem@13673
    77
streckem@13673
    78
"compStmt jmb (If(e) c1 Else c2) =
streckem@13673
    79
	(let cnstf = LitPush (Bool False);
streckem@13673
    80
             cnd   = compExpr jmb e;
streckem@13673
    81
	     thn   = compStmt jmb c1;
streckem@13673
    82
	     els   = compStmt jmb c2;
streckem@13673
    83
	     test  = Ifcmpeq (int(length thn +2)); 
streckem@13673
    84
	     thnex = Goto (int(length els +1))
streckem@13673
    85
	 in
streckem@13673
    86
	 [cnstf] @ cnd @ [test] @ thn @ [thnex] @ els)"
streckem@13673
    87
streckem@13673
    88
"compStmt jmb (While(e) c) =
streckem@13673
    89
	(let cnstf = LitPush (Bool False);
streckem@13673
    90
             cnd   = compExpr jmb e;
streckem@13673
    91
	     bdy   = compStmt jmb c;
streckem@13673
    92
	     test  = Ifcmpeq (int(length bdy +2)); 
streckem@13673
    93
	     loop  = Goto (-(int((length bdy) + (length cnd) +2)))
streckem@13673
    94
	 in
streckem@13673
    95
	 [cnstf] @ cnd @ [test] @ bdy @ [loop])"
streckem@13673
    96
streckem@13673
    97
(**********************************************************************)
streckem@13673
    98
streckem@13673
    99
(*compiling methods, classes and programs*) 
streckem@13673
   100
streckem@13673
   101
(*initialising a single variable*)
streckem@13673
   102
constdefs
streckem@13673
   103
 load_default_val :: "ty => instr"
streckem@13673
   104
"load_default_val ty == LitPush (default_val ty)"
streckem@13673
   105
streckem@13673
   106
 compInit :: "java_mb => (vname * ty) => instr list"
streckem@13673
   107
"compInit jmb == \<lambda> (vn,ty). [load_default_val ty, Store (index jmb vn)]"
streckem@13673
   108
streckem@13673
   109
 compInitLvars :: "[java_mb, (vname \<times> ty) list] \<Rightarrow> bytecode"
streckem@13673
   110
 "compInitLvars jmb lvars == concat (map (compInit jmb) lvars)"
streckem@13673
   111
streckem@13673
   112
  compMethod :: "java_mb prog \<Rightarrow> cname \<Rightarrow> java_mb mdecl \<Rightarrow> jvm_method mdecl"
streckem@13673
   113
  "compMethod G C jmdl == let (sig, rT, jmb) = jmdl;
streckem@13673
   114
                        (pns,lvars,blk,res) = jmb;
streckem@13673
   115
                        mt = (compTpMethod G C jmdl);
streckem@13673
   116
                        bc = compInitLvars jmb lvars @ 
streckem@13673
   117
                             compStmt jmb blk @ compExpr jmb res @
streckem@13673
   118
                             [Return]
streckem@13673
   119
                  in (sig, rT, max_ssize mt, length lvars, bc, [])"
streckem@13673
   120
streckem@13673
   121
  compClass :: "java_mb prog => java_mb cdecl=> jvm_method cdecl"
streckem@13673
   122
  "compClass G == \<lambda> (C,cno,fdls,jmdls). (C,cno,fdls, map (compMethod G C) jmdls)"
streckem@13673
   123
streckem@13673
   124
  comp :: "java_mb prog => jvm_prog"
streckem@13673
   125
  "comp G == map (compClass G) G"
streckem@13673
   126
streckem@13673
   127
end
streckem@13673
   128
streckem@13673
   129