Theory BoolProgs_Programs

theory BoolProgs_Programs
imports
  BoolProgs_Philosophers
  BoolProgs_ReaderWriter
  BoolProgs_Simple
  BoolProgs_LeaderFilters
  CAVA_Base.Code_String
  (*"HOL-Library.List_lexord"*)
begin

definition progs :: "(String.literal, String.literal × String.literal × (nat ⇒ (bprog × config) × const_map × fun_map)) mapping"
where "progs =  mapping_from_list [
                (STR ''RW'', (STR ''Reader/Writer'', STR ''# Readers and # Writers'', λn. (reader_writer n n, rw_const n, rw_fun n))),
                (STR ''S'', (STR ''Simple Variable Setting'', STR ''# Variables'', λn. (simple n, simple_const n, simple_fun n))),
                (STR ''P'', (STR ''Dining Philosophers'', STR ''# Philosophers'', λn. (philosophers n, phil_const n, phil_fun n))),
                (STR ''LF'', (STR ''Leader Filters'', STR ''# Processes'', λn. (leader_filters n, lf_const n, lf_fun n)))
              ]"

(* ensure this is an actual key *)
definition "default_prog ≡ STR ''S''"

definition keys_of_map :: "(String.literal, 'a) mapping ⇒ String.literal list" where
  "keys_of_map ≡ Mapping.ordered_keys"

definition chose_prog :: "String.literal ⇒ nat ⇒ String.literal × String.literal × (bprog × config) × const_map × fun_map"
where "chose_prog P n = (case Mapping.lookup progs P of 
                          Some (descr, ndescr, p) ⇒ (descr, ndescr, p n) 
                        | None ⇒ let (descr, ndescr, p) = the (Mapping.lookup progs default_prog)
                                 in (descr + STR '' (fallback)'', ndescr, p n))"

definition list_progs :: "(String.literal × String.literal × String.literal) list" where
  "list_progs ≡ let keys = keys_of_map progs in
                map (λk. let (descr, ndescr, p) = the (Mapping.lookup progs k)
                         in (k, descr, ndescr)) keys"
end