Theory VIMP_Program

theory VIMP_Program
  imports VIMP_Proc
begin

section ‹Whole programs›

text ‹
  ‹declared_global_vars› is the declared-global list in source order; a list,
  so finiteness is by type. ‹declared_global› is the derived classifier every
  program-level operation uses; procedure-level interfaces take the classifier
  as an explicit ‹vname ⇒ bool› argument instead.
›

record imp_prog =
  proc_rep :: "(pname * proc_decl) list"
  declared_global_vars :: "vname list"

definition declared_global :: "imp_prog ⇒ vname ⇒ bool" where
  "declared_global p x ⟷ x ∈ set (declared_global_vars p)"

lemma declared_global_iff [simp]:
  "declared_global p x ⟷ x ∈ set (declared_global_vars p)"
  by (simp add: declared_global_def)

text ‹The ‹program› parser fixes the entry name and rejects formals on it, so
  ‹main› is an ordinary ‹proc_rep› entry. ‹prog_main› is total through
  \<^const>‹main_body›'s aborting fallback;
  ‹wf_source_program›'s entry conjunct is what makes the lookup meaningful.›

definition prog_table :: "imp_prog ⇒ proc_table" where
  "prog_table p = map_of (proc_rep p)"

definition prog_procs :: "imp_prog ⇒ pname list" where
  "prog_procs p = filter (λn. n ≠ prog_main_name) (map fst (proc_rep p))"

definition prog_main :: "imp_prog ⇒ com" where
  "prog_main p = main_body (prog_table p)"

lemma prog_main_eq_main_body [simp]: "main_body (prog_table p) = prog_main p"
  by (simp add: prog_main_def)

text ‹‹mk_program› conses the entry onto ‹proc_rep›, so a program built through
  it satisfies ‹wf_source_program›'s entry conjunct by construction.›
definition mk_program :: "(pname * proc_decl) list ⇒ com ⇒ vname list ⇒ imp_prog" where
  "mk_program ps m gv = imp_prog.make ((prog_main_name, ⦇formals = [], body = m⦈) # ps) gv"

lemma mk_program_simps [simp]:
  "prog_table (mk_program ps m gv) = (map_of ps)(prog_main_name ↦ ⦇formals = [], body = m⦈)"
  "prog_main (mk_program ps m gv) = m"
  "declared_global_vars (mk_program ps m gv) = gv"
  "prog_main_name ∉ set (map fst ps) ⟹ prog_procs (mk_program ps m gv) = map fst ps"
  by (force simp: prog_table_def prog_main_def main_body_def prog_procs_def mk_program_def
      imp_prog.make_def filter_id_conv)+

text ‹The finite variable scope of an activation: every declared global, the
  activation's formals and body occurrences, and the reserved return location.›

definition scope_vnames :: "imp_prog ⇒ pname ⇒ vname set" where
  "scope_vnames p owner =
    set (declared_global_vars p) ∪ {ret_var} ∪
    (case prog_table p owner of
      None ⇒ {} |
      Some decl ⇒ set (formals decl) ∪ com_vnames (body decl))"

lemma finite_scope_vnames [simp]: "finite (scope_vnames p owner)"
  unfolding scope_vnames_def by (auto split: option.splits)

definition scope_vnames_list :: "imp_prog ⇒ pname ⇒ vname list" where
  "scope_vnames_list p owner = sorted_list_of_set (scope_vnames p owner)"

lemma set_scope_vnames_list [simp]:
  "set (scope_vnames_list p owner) = scope_vnames p owner"
  unfolding scope_vnames_list_def by simp

text ‹Every variable some procedure of the program declares: a program-wide
  superset of any one activation's scope.›

definition program_vars :: "imp_prog ⇒ vname list" where
  "program_vars p =
     remdups (concat (map (scope_vnames_list p) (prog_main_name # prog_procs p)))"

end