Theory Sorting_Export_Code

theory Sorting_Export_Code
imports Sorting_Parsort Sorting_Strings
begin

section ‹Code Export›

text ‹
  We instantiate Introsort and Pdqsort for unsigned ‹i64›, and for dynamic arrays of ‹i8›s ‹string_assn›.
  We then export code and generate a C header file to interface the code.
›


 (* TODO: Move! *)
lemmas [llvm_inline] = 
  array_swap_def word_log2_impl_def 

global_interpretation unat_sort: pure_sort_impl_context "(≤)" "(<)" ll_icmp_ult unat_assn
  defines unat_par_sort_impl = unat_sort.par_sort_impl
      and unat_introsort_impl = unat_sort.introsort_impl
      and unat_pdqsort_impl = unat_sort.pdqsort_impl
  by (rule unat_sort_impl_context)
  
abbreviation "string_assn ≡ string_assn' TYPE(size_t) TYPE(8)"  
  
global_interpretation str_sort: sort_impl_context "(≤)" "(<)" strcmp_impl string_assn
  defines str_par_sort_impl = str_sort.par_sort_impl
      and str_introsort_impl = str_sort.introsort_impl
      and str_pdqsort_impl = str_sort.pdqsort_impl
  by (rule strcmp_sort_impl_context)
  
  
(* Wrapper functions for export to LLVM. Only used for testing and profiling. *)
definition str_init :: "(8 word,size_t)array_list ptr ⇒ unit llM" where [llvm_code]:
  "str_init sp ≡ doM {
    ll_store init sp
  }"

definition str_append :: "(8 word,size_t)array_list ptr ⇒ 8 word ⇒ unit llM" where [llvm_code]:
  "str_append sp x ≡ doM {
    s ← ll_load sp;
    s ← arl_push_back s x;
    ll_store s sp
  }"

definition str_free :: "(8 word,size_t)array_list ptr ⇒ unit llM" where [llvm_code]:
  "str_free ap ≡ doM {
    a ← ll_load ap;
    arl_free a
  }"
  
  
definition llstrcmp :: "(8 word,size_t)array_list ptr ⇒ _ ⇒ 8 word llM" where [llvm_code]:
  "llstrcmp ap bp ≡ doM {
    a ← ll_load ap;
    b ← ll_load bp;
    r ← strcmp_impl a b;
    if r≠0 then Mreturn 1 else Mreturn 0
  }"

  
  

declare [[llc_compile_par_call=true]]

export_llvm (timing)
  "unat_par_sort_impl :: 64 word ptr ⇒ _" is "uint64_t* par_sort(uint64_t*, int64_t)"
  "unat_introsort_impl :: 64 word ptr ⇒ _" is "uint64_t* introsort(uint64_t*, int64_t, int64_t)"
  "unat_pdqsort_impl :: 64 word ptr ⇒ _" is "uint64_t* pdqsort(uint64_t*, int64_t, int64_t)"
  
  "str_init" is "void str_init(llstring * )"
  "str_append" is "void str_append(llstring *, char)"
  "llstrcmp" is "char llstrcmp(llstring*,llstring* )"
  "str_free" is "void str_free(llstring* )"
  
  "str_par_sort_impl" is "llstring* str_par_sort(llstring*, int64_t)"  
  "str_introsort_impl" is "llstring* str_introsort(llstring*, int64_t, int64_t)"  
  "str_pdqsort_impl" is "llstring* str_pdqsort(llstring*, int64_t, int64_t)"  
  
  defines ‹typedef struct {int64_t size; struct {int64_t capacity; char *data;};} llstring;›
  file "../code/introsort.ll"

export_llvm (timing)
  "unat_par_sort_impl :: 64 word ptr ⇒ _" is "uint64_t* par_sort(uint64_t*, int64_t)"
  "unat_introsort_impl :: 64 word ptr ⇒ _" is "uint64_t* introsort(uint64_t*, int64_t, int64_t)"
  "unat_pdqsort_impl :: 64 word ptr ⇒ _" is "uint64_t* pdqsort(uint64_t*, int64_t, int64_t)"
  
  "str_init" is "void str_init(llstring * )"
  "str_append" is "void str_append(llstring *, char)"
  "llstrcmp" is "char llstrcmp(llstring*,llstring* )"
  "str_free" is "void str_free(llstring* )"
  
  "str_par_sort_impl" is "llstring* str_par_sort(llstring*, int64_t)"  
  "str_introsort_impl" is "llstring* str_introsort(llstring*, int64_t, int64_t)"  
  "str_pdqsort_impl" is "llstring* str_pdqsort(llstring*, int64_t, int64_t)"  
  
  defines ‹typedef struct {int64_t size; struct {int64_t capacity; char *data;};} llstring;›
  file "../../../regression/gencode/sorting.ll"
  
text ‹Correctness lemmas for what we just exported.›
thm unat_sort.par_sort_impl_correct
thm unat_sort.introsort_impl_correct
thm unat_sort.pdqsort_impl.refine

thm str_sort.par_sort_impl_correct
thm str_sort.introsort_impl_correct
thm str_sort.pdqsort_impl.refine

text ‹We explicitly unfold one here, to be similar to the one displayed in the paper:›
lemma "llvm_htriple 
  (woarray_slice_assn unat_assn xs xsi ∧* snat_assn n ni ∧* ↑(n = length xs)) 
  (unat_par_sort_impl xsi ni)
  (λr. ↑(r = xsi) ∧* (λs. ∃xs'. (woarray_slice_assn unat_assn xs' xsi ∧* ↑(sorted xs' ∧ mset xs'=mset xs)) s))"
  using unat_sort.par_sort_impl_correct[of xs xsi n ni] 
  unfolding sort_spec_def
  by (auto simp: conj_commute)
  
  
end