Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Algol p272.cob Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/MicroJava/Comp/TranslCompTp.thy
    Author:     Martin Strecker
*)

theory TranslCompTp
imports Index "../BV/JVMType"
begin

(**********************************************************************)

definition comb :: "['a \ 'b list \ 'c, 'c \ 'b list \ 'd, 'a] \ 'b list \ 'd"
  (infixr "\" 55)
where
  "comb == (\ f1 f2 x0. let (xs1, x1) = f1 x0;
                            (xs2, x2) = f2 x1
                        in  (xs1 @ xs2, x2))"

definition comb_nil :: "'a \ 'b list \ 'a" where
  "comb_nil a == ([], a)"

lemma comb_nil_left [simp]: "comb_nil \ f = f"
  by (simp add: comb_def comb_nil_def split_beta)

lemma comb_nil_right [simp]: "f \ comb_nil = f"
  by (simp add: comb_def comb_nil_def split_beta)

lemma comb_assoc [simp]: "(fa \ fb) \ fc = fa \ (fb \ fc)"
  by (simp add: comb_def split_beta)

lemma comb_inv:
  "(xs', x') = (f1 \ f2) x0 \
  \<exists>xs1 x1 xs2 x2. (xs1, x1) = (f1 x0) \<and> (xs2, x2) = f2 x1 \<and> xs'= xs1 @ xs2 \<and> x'=x2"
  by (case_tac "f1 x0") (simp add: comb_def split_beta)

(**********************************************************************)

abbreviation (input)
  mt_of :: "method_type \ state_type \ method_type"
  where "mt_of == fst"

abbreviation (input)
  sttp_of :: "method_type \ state_type \ state_type"
  where "sttp_of == snd"

definition nochangeST :: "state_type \ method_type \ state_type" where
  "nochangeST sttp == ([Some sttp], sttp)"

definition pushST :: "[ty list, state_type] \ method_type \ state_type" where
  "pushST tps == (\ (ST, LT). ([Some (ST, LT)], (tps @ ST, LT)))"

definition dupST :: "state_type \ method_type \ state_type" where
  "dupST == (\ (ST, LT). ([Some (ST, LT)], (hd ST # ST, LT)))"

definition dup_x1ST :: "state_type \ method_type \ state_type" where
  "dup_x1ST == (\ (ST, LT). ([Some (ST, LT)],
                             (hd ST # hd (tl ST) # hd ST # (tl (tl ST)), LT)))"

definition popST :: "[nat, state_type] \ method_type \ state_type" where
  "popST n == (\ (ST, LT). ([Some (ST, LT)], (drop n ST, LT)))"

definition replST :: "[nat, ty, state_type] \ method_type \ state_type" where
  "replST n tp == (\ (ST, LT). ([Some (ST, LT)], (tp # (drop n ST), LT)))"

definition storeST :: "[nat, ty, state_type] \ method_type \ state_type" where
  "storeST i tp == (\ (ST, LT). ([Some (ST, LT)], (tl ST, LT [i:= OK tp])))"

(* Expressions *)

primrec compTpExpr :: "java_mb \ java_mb prog \ expr \
    state_type \<Rightarrow> method_type \<times> state_type"
  and compTpExprs :: "java_mb \ java_mb prog \ expr list \
    state_type \<Rightarrow> method_type \<times> state_type"
where
  "compTpExpr jmb G (NewC c) = pushST [Class c]"
| "compTpExpr jmb G (Cast c e) = (compTpExpr jmb G e) \ (replST 1 (Class c))"
| "compTpExpr jmb G (Lit val) = pushST [the (typeof (\v. None) val)]"
| "compTpExpr jmb G (BinOp bo e1 e2) =
     (compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box>
     (case bo of
       Eq => popST 2 \<box> pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]
     | Add => replST 2 (PrimT Integer))"
| "compTpExpr jmb G (LAcc vn) = (\ (ST, LT).
      pushST [ok_val (LT ! (index jmb vn))] (ST, LT))"
| "compTpExpr jmb G (vn::=e) =
      (compTpExpr jmb G e) \<box> dupST \<box> (popST 1)"
| "compTpExpr jmb G ( {cn}e..fn ) =
      (compTpExpr jmb G e) \<box> replST 1 (snd (the (field (G,cn) fn)))"
| "compTpExpr jmb G (FAss cn e1 fn e2 ) =
      (compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box> dup_x1ST \<box> (popST 2)"
| "compTpExpr jmb G ({C}a..mn({fpTs}ps)) =
       (compTpExpr jmb G a) \<box> (compTpExprs jmb G ps) \<box>
       (replST ((length ps) + 1) (method_rT (the (method (G,C) (mn,fpTs)))))"
| "compTpExprs jmb G [] = comb_nil"
| "compTpExprs jmb G (e#es) = (compTpExpr jmb G e) \ (compTpExprs jmb G es)"

(* Statements *)
primrec compTpStmt :: "java_mb \ java_mb prog \ stmt \
    state_type \<Rightarrow> method_type \<times> state_type"
where
  "compTpStmt jmb G Skip = comb_nil"
| "compTpStmt jmb G (Expr e) = (compTpExpr jmb G e) \ popST 1"
| "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) \ (compTpStmt jmb G c2)"
| "compTpStmt jmb G (If(e) c1 Else c2) =
      (pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
      (compTpStmt jmb G c1) \<box> nochangeST \<box> (compTpStmt jmb G c2)"
| "compTpStmt jmb G (While(e) c) =
      (pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
      (compTpStmt jmb G c) \<box> nochangeST"

definition compTpInit :: "java_mb \ (vname * ty)
                   \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type" where
  "compTpInit jmb == (\ (vn,ty). (pushST [ty]) \ (storeST (index jmb vn) ty))"

primrec compTpInitLvars :: "[java_mb, (vname \ ty) list] \
    state_type \<Rightarrow> method_type \<times> state_type"
where
  "compTpInitLvars jmb [] = comb_nil"
| "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \ (compTpInitLvars jmb lvars)"

definition start_ST :: "opstack_type" where
  "start_ST == []"

definition start_LT :: "cname \ ty list \ nat \ locvars_type" where
  "start_LT C pTs n == (OK (Class C))#((map OK pTs))@(replicate n Err)"

definition compTpMethod  :: "[java_mb prog, cname, java_mb mdecl] \ method_type" where
  "compTpMethod G C == \ ((mn,pTs),rT, jmb).
                         let (pns,lvars,blk,res) = jmb
                         in (mt_of
                            ((compTpInitLvars jmb lvars \<box>
                              compTpStmt jmb G blk \<box>
                              compTpExpr jmb G res \<box>
                              nochangeST)
                                (start_ST, start_LT C pTs (length lvars))))"

definition compTp :: "java_mb prog => prog_type" where
  "compTp G C sig == let (D, rT, jmb) = (the (method (G, C) sig))
                      in compTpMethod G C (sig, rT, jmb)"

(**********************************************************************)
  (* Computing the maximum stack size from the method_type *)

definition ssize_sto :: "(state_type option) \ nat" where
  "ssize_sto sto == case sto of None \ 0 | (Some (ST, LT)) \ length ST"

definition max_of_list :: "nat list \ nat" where
  "max_of_list xs == foldr max xs 0"

definition max_ssize :: "method_type \ nat" where
  "max_ssize mt == max_of_list (map ssize_sto mt)"

end

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.