Theory Decl

(*  Title:      JinjaThreads/Common/Decl.thy
    Author:     David von Oheimb, Andreas Lochbihler

    Based on the Jinja theory Common/Decl.thy by David von Oheimb
*)

section ‹Class Declarations and Programs›

theory Decl
imports
  Type
begin

type_synonym volatile = bool

record fmod =
  volatile :: volatile

type_synonym fdecl    = "vname × ty × fmod"        ― ‹field declaration›
type_synonym 'm mdecl = "mname × ty list × ty × 'm"     ― ‹method = name, arg. types, return type, body›
type_synonym 'm mdecl' = "mname × ty list × ty × 'm option"     ― ‹method = name, arg. types, return type, possible body›
type_synonym 'm "class" = "cname × fdecl list × 'm mdecl' list"       ― ‹class = superclass, fields, methods›
type_synonym 'm cdecl = "cname × 'm class"  ― ‹class declaration›

datatype
  'm prog = Program "'m cdecl list" 

translations
  (type) "fdecl"   <= (type) "String.literal × ty × fmod"
  (type) "'c mdecl" <= (type) "String.literal × ty list × ty × 'c"
  (type) "'c mdecl'" <= (type) "String.literal × ty list × ty × 'c option"
  (type) "'c class" <= (type) "String.literal × fdecl list × ('c mdecl) list"
  (type) "'c cdecl" <= (type) "String.literal × ('c class)"

notation (input) None ("Native")

primrec "classes" :: "'m prog ⇒ 'm cdecl list"
where
  "classes (Program P) = P"

primrec "class" :: "'m prog ⇒ cname ⇀ 'm class"
where
  "class (Program p) = map_of p"

locale prog =
  fixes P :: "'m prog"

definition is_class :: "'m prog ⇒ cname ⇒ bool"
where
  "is_class P C  ≡  class P C ≠ None"

lemma finite_is_class: "finite {C. is_class P C}"
(*<*)
apply(cases P)
apply (unfold is_class_def)
apply (fold dom_def)
apply(simp add: finite_dom_map_of)
done
(*>*)

primrec is_type :: "'m prog ⇒ ty ⇒ bool"
where
  is_type_void:   "is_type P Void = True"
| is_type_bool:   "is_type P Boolean = True"
| is_type_int:    "is_type P Integer = True"
| is_type_nt:     "is_type P NT = True"
| is_type_class:  "is_type P (Class C) = is_class P C"
| is_type_array:  "is_type P (A⌊⌉) = (case ground_type A of NT ⇒ False | Class C ⇒ is_class P C | _ ⇒ True)"

lemma is_type_ArrayD: "is_type P (T⌊⌉) ⟹ is_type P T"
by(induct T) auto

lemma is_type_ground_type:
  "is_type P T ⟹ is_type P (ground_type T)"
by(induct T)(auto, metis is_type_ArrayD is_type_array)

abbreviation "types" :: "'m prog ⇒ ty set"
where "types P ≡ {T. is_type P T}"

abbreviation is_htype :: "'m prog ⇒ htype ⇒ bool"
where "is_htype P hT ≡ is_type P (ty_of_htype hT)"

subsection ‹Code generation›

lemma is_class_intros [code_pred_intro]:
  "class P C ≠ None ⟹ is_class P C"
by(auto simp add: is_class_def)

code_pred 
  (modes: i ⇒ i ⇒ bool)
  is_class 
unfolding is_class_def by simp

declare is_class_def[code]

end