Theory WB_Sort_SML

theory WB_Sort_SML
  imports WB_Sort WB_More_IICF_SML
begin

named_theorems isasat_codegen

lemma swap_match[isasat_codegen]: ‹WB_More_Refinement_List.swap = IICF_List.swap›
  by (auto simp: WB_More_Refinement_List.swap_def IICF_List.swap_def intro!: ext)

sepref_register choose_pivot3

text ‹Example instantiation code for pivot›
sepref_definition choose_pivot3_impl_code
  is ‹uncurry2 (choose_pivot3_impl)›
  :: ‹(arl_assn nat_assn)⇧k  *⇩a  nat_assn⇧k *⇩a nat_assn⇧k→⇩a nat_assn›
  unfolding choose_pivot3_impl_def choose_pivot3_def id_def
  by sepref

declare choose_pivot3_impl_code.refine[sepref_fr_rules]



text ‹Example instantiation for \<^term>‹partition_main››
definition partition_main_impl where
  ‹partition_main_impl = partition_main (≤) id›

sepref_register partition_main_impl

text ‹Example instantiation code for \<^term>‹partition_main››
sepref_definition partition_main_code
  is ‹uncurry2 (partition_main_impl)›
  :: ‹nat_assn⇧k *⇩a nat_assn⇧k *⇩a (arl_assn nat_assn)⇧d →⇩a
      arl_assn nat_assn *a nat_assn›
  unfolding partition_main_impl_def partition_main_def
    id_def isasat_codegen
  by sepref

declare partition_main_code.refine[sepref_fr_rules]


text ‹Example instantiation for partition›
definition partition_between_impl where
  ‹partition_between_impl = partition_between_ref (≤) id›

sepref_register partition_between_ref

text ‹Example instantiation code for partition›
sepref_definition partition_between_code
  is ‹uncurry2 (partition_between_impl)›
  :: ‹nat_assn⇧k *⇩a nat_assn⇧k *⇩a (arl_assn nat_assn)⇧d →⇩a
      arl_assn nat_assn *a nat_assn›
  unfolding partition_between_ref_def partition_between_impl_def
    choose_pivot3_impl_def[symmetric] partition_main_impl_def[symmetric]
  unfolding  id_def isasat_codegen
  by sepref

declare partition_between_code.refine[sepref_fr_rules]


― ‹Example implementation›
definition quicksort_impl where
  ‹quicksort_impl a b c ≡ quicksort_ref (≤) id (a,b,c)›

sepref_register quicksort_impl

― ‹Example implementation code›
sepref_definition
  quicksort_code
  is ‹uncurry2 quicksort_impl›
  :: ‹nat_assn⇧k *⇩a nat_assn⇧k *⇩a (arl_assn nat_assn)⇧d →⇩a
      arl_assn nat_assn›
  unfolding partition_between_impl_def[symmetric]
    quicksort_impl_def quicksort_ref_def
  by sepref

declare quicksort_code.refine[sepref_fr_rules]

text ‹Executable code for the example instance›
sepref_definition full_quicksort_code
  is ‹full_quicksort_impl›
  :: ‹(arl_assn nat_assn)⇧d →⇩a
      arl_assn nat_assn›
  unfolding full_quicksort_impl_def full_quicksort_ref_def quicksort_impl_def[symmetric] List.null_def
  by sepref

text ‹Export the code›
export_code ‹nat_of_integer› ‹integer_of_nat› ‹partition_between_code› ‹full_quicksort_code› in SML_imp module_name IsaQuicksort file "code/quicksort.sml"

end