Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/J/Type.thy
author oheimb
Thu, 01 Feb 2001 20:53:13 +0100
changeset 11026 a50365d21144
parent 10069 c7226e6f9625
child 11070 cc421547e744
permissions -rw-r--r--
converted to Isar, simplifying recursion on class hierarchy

(*  Title:      HOL/MicroJava/J/Type.thy
    ID:         $Id$
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen

Java types
*)

theory Type = JBasis:

typedecl cname  (* class name *)
typedecl vnam   (* variable or field name *)
typedecl mname  (* method name *)
arities  cname :: "term"
         vnam  :: "term"
         mname :: "term"

datatype vname    (* names for This pointer and local/field variables *)
  = This
  | VName vnam

datatype prim_ty  (* primitive type, cf. 4.2 *)
  = Void          (* 'result type' of void methods *)
  | Boolean
  | Integer

datatype ref_ty   (* reference type, cf. 4.3 *)
  = NullT         (* null type, cf. 4.1 *)
  | ClassT cname  (* class type *)

datatype ty       (* any type, cf. 4.1 *)
  = PrimT prim_ty (* primitive type *)
  | RefT  ref_ty  (* reference type *)

syntax
  NT    :: "          ty"
  Class :: "cname  => ty"

translations
  "NT"      == "RefT NullT"
  "Class C" == "RefT (ClassT C)"

end
isabelle