Theory IICF_Impl_Heap

section ‹Implementation of Heaps with Arrays›
theory IICF_Impl_Heap
imports 
  IICF_Abs_Heap 
  "../IICF_Array" 
  "../IICF_Array_List" 
begin

  (* TODO: Move *)
  
  term al_assn

  (* TODO: Move *)      
  lemma size_mset_param[param]: "(size,size)∈⟨A⟩mset_rel → nat_rel"  
    by (auto simp: mset_rel_def p2rel_def rel_mset_size)
    

  (* TODO: Move *)
  lemma rdomp_ref_mk_assn_iff[simp]: "rdomp ↿(mk_assn A) = rdomp A"
    by (auto simp: rdomp_def)
  
  thm vcg_prep_ext_rules  
    
  find_theorems pure_part  
    
  lemma rdomp_arl_assn_len:
    assumes "rdomp ↿(arl_assn:: ('a::llvm_rep list, 'l::len2 word × 'l word × 'a ptr) dr_assn) xs"
    shows "length xs < max_snat LENGTH('l)"
    using assms
    by (auto 
      simp: rdomp_def arl_assn_def arl_assn'_def sep_algebra_simps pred_lift_extract_simps
      simp: snat.assn_def
      )

  find_theorems vassn_tag hn_refine

      
  (* TODO: Very specialized workaround lemma, to work around invalid-recombination
    problem for case that B is pure 
  *)    
  lemma workaround_invalid_recombine_pure2: "is_pure B ⟹ hn_ctxt (invalid_assn A ×⇩a B) ax px ⊢ hn_invalid (A ×⇩a B) ax px"
    unfolding hn_ctxt_def invalid_assn_def prod_assn_def entails_def
    by (auto split: prod.split elim!: is_pureE 
      simp: sep_algebra_simps pure_part_pure_conj_eq)
    
  (* TODO: Move
    TODO: Should be generic algorithm!
  *)  
  lemma mop_list_swap_unfold: "mop_list_swap xs i j = do {
    xi ← mop_list_get xs i;
    xj ← mop_list_get xs j;
    xs ← mop_list_set xs i xj;
    mop_list_set xs j xi
  }"
  by (auto simp: pw_eq_iff refine_pw_simps swap_def)
  
    


  text ‹We implement the heap data structure by an array.
    The implementation is automatically synthesized by the Sepref-tool.
    ›
  subsection ‹Setup of the Sepref-Tool›

  (* TODO: Move *)
  lemma mset_rel_id: "⟨Id⟩mset_rel = Id"
    unfolding mset_rel_def apply (simp add: rel2p multiset.rel_eq)
    by (simp only: p2rel)
  
  
  locale heap_impl = heapstruct prio for prio :: "'e ⇒ 'p::linorder" +
    fixes prio_assn :: "'p ⇒ 'pi::llvm_rep ⇒ assn"
      and elem_assn :: "'e ⇒ 'ei::llvm_rep ⇒ assn"
      and prio_impl le_prio_impl lt_prio_impl
      and ltype :: "'l::len2 itself"
    assumes prio_is_pure[safe_constraint_rules]: "is_pure prio_assn"
    assumes elem_is_pure[safe_constraint_rules]: "is_pure elem_assn"  
    assumes prio_impl_refine[sepref_fr_rules]: "(prio_impl, RETURN o prio)∈elem_assn⇧k →⇩a prio_assn"
    assumes le_prio_impl_refine[sepref_fr_rules]: 
      "(uncurry le_prio_impl, uncurry (RETURN oo (≤))) ∈ prio_assn⇧k *⇩a prio_assn⇧k →⇩a bool1_assn"
    assumes lt_prio_impl_refine[sepref_fr_rules]: 
      "(uncurry lt_prio_impl, uncurry (RETURN oo (<))) ∈ prio_assn⇧k *⇩a prio_assn⇧k →⇩a bool1_assn"
      
    fixes N defines "N≡LENGTH('l)"
    (*assumes l_len[simp,arith]: "4 < LENGTH('l)"*)
  begin
      
    abbreviation "assn ≡ al_assn' TYPE('l) elem_assn"
    abbreviation "idx_assn ≡ snat_assn' TYPE('l)"
    definition "heap_assn ≡ hr_comp (al_assn elem_assn) heap_rel1"

    lemma mk_free_heap_assn[sepref_frame_free_rules]: "MK_FREE heap_assn arl_free"
      unfolding heap_assn_def
      by (rule sepref_frame_free_rules)+
  
    (*context
      assumes l_len_pre: "(4 < LENGTH('l))"
    begin  
      private lemma l_len: "4 < LENGTH('l)" using l_len_pre unfolding vcg_tag_defs by auto
    *)  
  
      sepref_register prio
  
      sepref_register "(≤) :: 'p ⇒ 'p ⇒ bool"
      sepref_register "(<) :: 'p ⇒ 'p ⇒ bool"
      
      lemmas [sepref_frame_free_rules] = 
        mk_free_is_pure[OF prio_is_pure]
        mk_free_is_pure[OF elem_is_pure]
          
      sepref_register update_op
      sepref_definition update_impl is "uncurry2 update_op" 
        :: "assn⇧d *⇩a idx_assn⇧k *⇩a elem_assn⇧k →⇩a assn"
        unfolding update_op_def[abs_def]
        apply (annot_snat_const "TYPE('l)")
        by sepref
      lemmas [sepref_fr_rules] = update_impl.refine
          
      sepref_register val_of_op
      sepref_definition val_of_impl is "uncurry val_of_op" :: "assn⇧k *⇩a idx_assn⇧k →⇩a elem_assn"
        unfolding val_of_op_def[abs_def]
        apply (annot_snat_const "TYPE('l)")
        by sepref
      lemmas [sepref_fr_rules] = val_of_impl.refine
    
      sepref_register exch_op
      sepref_definition exch_impl is "uncurry2 exch_op" :: "assn⇧d *⇩a idx_assn⇧k *⇩a idx_assn⇧k →⇩a assn"
        unfolding exch_op_def[abs_def] mop_list_swap_unfold
        apply (annot_snat_const "TYPE('l)")
        by sepref
        
      lemmas [sepref_fr_rules] = exch_impl.refine
    
      sepref_register valid
      sepref_definition valid_impl is "uncurry (RETURN oo valid)" :: "assn⇧k *⇩a idx_assn⇧k →⇩a bool1_assn"
        unfolding valid_def[abs_def]
        apply (annot_snat_const "TYPE('l)")
        by sepref
      lemmas [sepref_fr_rules] = valid_impl.refine
          
      sepref_register prio_of_op  
      sepref_definition prio_of_impl is "uncurry (PR_CONST prio_of_op)" :: "assn⇧k *⇩a idx_assn⇧k →⇩a prio_assn"
        unfolding prio_of_op_def[abs_def] PR_CONST_def
        by sepref
      lemmas [sepref_fr_rules] = prio_of_impl.refine
      
      sepref_definition append_impl is "uncurry mop_list_append" 
        :: "[λ(xs,_). length xs + 1 < max_snat LENGTH('l)]⇩a assn⇧d *⇩a elem_assn⇧k → assn"
        by sepref
      lemmas [sepref_fr_rules] = append_impl.refine 
      
      sepref_register swim_op
      sepref_definition swim_impl is 
        "uncurry (PR_CONST swim_op)" :: "[λ_. 4<LENGTH('l)]⇩a assn⇧d *⇩a idx_assn⇧k → assn"
        unfolding swim_op_def[abs_def] parent_def PR_CONST_def
        apply (annot_snat_const "TYPE('l)")
        (* TODO: Workaround/Hack *)
        supply [sepref_frame_match_rules] = workaround_invalid_recombine_pure2[where B=snat_assn, simplified]
        by sepref_dbg_keep
  
      lemmas [sepref_fr_rules] = swim_impl.refine
  
      
      lemma overflow_safe_hbound_check: "2*k≤n ⟷ k≤n div 2" for k n :: nat by auto
      
      (*lemma bound_aux1: "rdomp assn xs ⟹ j≤length xs div 2 ⟹ 2*j < max_snat LENGTH('l)"  
        apply sepref_bounds*)

      (*          
      lemma bound_aux2: "⟦rdomp assn a1'; 2 * a2' < length a1'⟧ 
        ⟹ Suc (2 * a2') < max_snat LENGTH('l)"  
        apply sepref_bounds
        apply (drule al_assn_len_bound)
        by auto
      *)
        
      sepref_register sink_op
      sepref_definition sink_impl is "uncurry (PR_CONST sink_op)" :: "[λ_. 4<LENGTH('l)]⇩a assn⇧d *⇩a idx_assn⇧k → assn"
        unfolding sink_op_opt_def[abs_def] sink_op_opt_eq[symmetric,abs_def]  PR_CONST_def
        unfolding overflow_safe_hbound_check Suc_eq_plus1
        (* TODO: Workaround/Hack *)
        supply [sepref_frame_match_rules] = workaround_invalid_recombine_pure2[where B=snat_assn, simplified]
        apply (annot_snat_const "TYPE('l)")
        by sepref
        
      lemmas [sepref_fr_rules] = sink_impl.refine
  
      
      lemma prenorm_heaprel1_len: "(h,m)∈heap_rel1 ⟹ length h = size m"
        unfolding heap_rel1_def in_br_conv
        by auto
      lemma max_snat_param: "(max_snat,max_snat)∈nat_rel → nat_rel" by simp

      context
        notes [fcomp_norm_unfold] = heap_assn_def[symmetric] list_rel_id_simp mset_rel_id
        notes [fcomp_prenorm_simps] = prenorm_heaprel1_len
        notes [param] = IdI[of N] max_snat_param
      begin    
      
        sepref_definition empty_impl is "uncurry0 empty_op" :: "[λ_. 4<N]⇩a unit_assn⇧k → assn"
          unfolding empty_op_def N_def
          apply (rewrite al_fold_custom_empty[where 'l='l])
          by sepref
        sepref_decl_impl (no_register) heap_empty: empty_impl.refine[FCOMP empty_op_refine] 
          uses op_mset_empty.fref[of Id] .
    
        sepref_definition is_empty_impl is "is_empty_op" :: "assn⇧k →⇩a bool1_assn"
          unfolding is_empty_op_def[abs_def]
          apply (annot_snat_const "TYPE('l)")
          by sepref
        sepref_decl_impl heap_is_empty: is_empty_impl.refine[FCOMP is_empty_op_refine] 
          uses op_mset_is_empty.fref[of Id] .  
    
        sepref_definition insert_impl
          is "uncurry insert_op" :: "[λ(_,xs). 4<N ∧ length xs+1 < max_snat N]⇩a elem_assn⇧k *⇩a assn⇧d → assn"
          unfolding insert_op_def[abs_def] append_op_def N_def
          by sepref
        sepref_decl_impl heap_insert: insert_impl.refine[FCOMP insert_op_refine] 
          uses op_mset_insert.fref[of Id] .
          
        sepref_definition pop_min_impl is "pop_min_op" :: "[λ_. 4<N]⇩a assn⇧d → elem_assn ×⇩a assn"
          unfolding pop_min_op_def[abs_def] butlast_op_def N_def
          apply (annot_snat_const "TYPE('l)")
          by sepref
        sepref_decl_impl (no_mop) heap_pop_min: pop_min_impl.refine[FCOMP pop_min_op_refine] 
          uses op_prio_pop_min.fref[of Id] .
        
        
    
        sepref_definition peek_min_impl is "peek_min_op" :: "assn⇧k →⇩a elem_assn"
          unfolding peek_min_op_def[abs_def]
          apply (annot_snat_const "TYPE('l)")
          by sepref
        sepref_decl_impl (no_mop) heap_peek_min: peek_min_impl.refine[FCOMP peek_min_op_refine] 
          uses op_prio_peek_min.fref[of Id] .
                  
      end
    (*end        *)

  end  
    

  global_interpretation heap_impl id snat_assn snat_assn Mreturn ll_icmp_sle ll_icmp_slt "TYPE('l::len2)" "LENGTH('l)"
    defines h_update_impl = update_impl
        and h_val_of_impl = val_of_impl
        and h_exch_impl = exch_impl
        and h_valid_impl = valid_impl
        and h_prio_of_impl = prio_of_impl
        and h_append_impl = append_impl
        and h_swim_impl = swim_impl
        and h_sink_impl = sink_impl
        and h_empty_impl = empty_impl
        and h_is_empty_impl = is_empty_impl
        and h_insert_impl = insert_impl
        and h_pop_min_impl = pop_min_impl
        and h_peek_min_impl = peek_min_impl
  
    apply unfold_locales
    apply (rule pure_pure)
    apply sepref
    apply sepref
    apply sepref
    apply simp
    done

   
  lemmas heap_impl_inlines = 
    heap_impl.valid_impl_def[OF heap_impl_axioms]  
    heap_impl.prio_of_impl_def[OF heap_impl_axioms]
    heap_impl.val_of_impl_def[OF heap_impl_axioms]
    heap_impl.append_impl_def[OF heap_impl_axioms]
    heap_impl.exch_impl_def[OF heap_impl_axioms]
    heap_impl.empty_impl_def[OF heap_impl_axioms]
    heap_impl.is_empty_impl_def[OF heap_impl_axioms]
    heap_impl.insert_impl_def[OF heap_impl_axioms]
    heap_impl.pop_min_impl_def[OF heap_impl_axioms]
    heap_impl.peek_min_impl_def[OF heap_impl_axioms]
    
    h_swim_impl_def[symmetric]
    h_sink_impl_def[symmetric]
    
  lemmas [llvm_inline] = update_impl_def 
  lemmas [llvm_inline] = val_of_impl_def 
  lemmas [llvm_inline] = exch_impl_def    
  lemmas [llvm_inline] = h_valid_impl_def[unfolded heap_impl_inlines]
  lemmas [llvm_inline] = h_prio_of_impl_def[unfolded heap_impl_inlines]
  lemmas [llvm_inline] = h_append_impl_def[unfolded heap_impl_inlines]
  lemmas [llvm_code] = h_swim_impl_def[unfolded heap_impl.swim_impl_def[OF heap_impl_axioms], unfolded heap_impl_inlines]
  lemmas [llvm_code] = h_sink_impl_def[unfolded heap_impl.sink_impl_def[OF heap_impl_axioms], unfolded heap_impl_inlines]
  lemmas [llvm_inline] = h_empty_impl_def[unfolded heap_impl_inlines]
  lemmas [llvm_inline] = h_is_empty_impl_def[unfolded heap_impl_inlines]
  lemmas [llvm_inline] = h_insert_impl_def[unfolded heap_impl_inlines]
  lemmas [llvm_inline] = h_pop_min_impl_def[unfolded heap_impl_inlines]
  lemmas [llvm_inline] = h_peek_min_impl_def[unfolded heap_impl_inlines]
  
  definition [simp]: "op_heap_custom_empty (_::'a::len2 itself) (_::'l::len2 itself) ≡ op_mset_empty"
  context fixes Q T :: "_::len2 itself" begin sepref_register "op_heap_custom_empty Q T" end
  
  lemma op_heap_custom_empty_hnr[sepref_fr_rules]:
    shows "(
      uncurry0 (empty_impl::('a::len2 word,'l)array_list llM ), 
      uncurry0 (RETURN (PR_CONST (op_heap_custom_empty TYPE('a) TYPE('l))))) ∈ [λ_. 4<LENGTH('l::len2)]⇩a unit_assn⇧k → heap_assn"
    unfolding op_heap_custom_empty_def PR_CONST_def
    by (rule heap_empty_hnr[unfolded PRECOND_def])
    
  lemma heap_fold_custom_empty: 
    "{#} = op_heap_custom_empty TYPE('a::len2) TYPE('l::len2)"
    "op_mset_empty = op_heap_custom_empty TYPE('a::len2) TYPE('l::len2)"
    "mop_mset_empty = RETURN (op_heap_custom_empty TYPE('a::len2) TYPE('l::len2))"
    by auto
  
    
      
  
    
definition "sort_by_prio l⇩0 ≡ do {
  q ← nfoldli l⇩0 (λ_. True) (λx q. do { ASSERT (size q < length l⇩0); mop_mset_insert x q }) {#};
  ASSERT (q = mset l⇩0);
  (l,q) ← WHILEIT (λ(l,q). sorted l ∧ (∀x∈set l. ∀y∈#q. x≤y) ∧ mset l + q = mset l⇩0) 
    (λ(l,q). ¬op_mset_is_empty q) (λ(l,q). 
  do {
    (x,q) ← mop_prio_pop_min id q;
    ASSERT (size l < length l⇩0);
    RETURN (l@[x],q)
  }) (op_list_empty,q);
  RETURN l
}"

lemma sort_by_prio_correct: "sort_by_prio l ≤ SPEC (λl'. sorted l' ∧ mset l' = mset l)"
  unfolding sort_by_prio_def mop_prio_pop_min_def
  
  apply (refine_vcg 
    nfoldli_rule[where I="λll _ q. q = mset ll"]
    WHILEIT_rule[where R="measure (λ(l,q). size q)"]
    )
  apply (auto 0 3 dest: in_diffD simp: size_Diff1_less sorted_append_bigger)
  subgoal by (metis add_cancel_right_right le_add1 nat_less_le size_eq_0_iff_empty size_mset size_union) 
  subgoal by (metis insert_DiffM union_iff) 
  done
  


(* TODO: Move  *)
function list_intv_induction where
  "list_intv_induction l u = (if l<u then list_intv_induction (Suc l) u else ())"
  by pat_completeness auto

termination
  apply (relation "measure (λ(l,u). u-l)")
  by auto
  
  
(*  
lemma nfoldli_range_to_while: "nfoldli [l..<u] c f σ = do {
    (_,σ) ← WHILET 
      (λ(i,σ). i<u ∧ c σ) 
      (λ(i,σ). do { σ ← f i σ; ASSERT (i<u); RETURN (i+1,σ) })
      (l,σ);
    RETURN σ
  }"
proof (induction l u arbitrary: σ rule: list_intv_induction.induct)
  case (1 l u)
  show ?case proof (cases "l<u")
    case False thus ?thesis
      by (rewrite WHILET_unfold) simp
      
  next
    case True 
    thm "1.IH"[OF True, abs_def]
    thus ?thesis 
      by (rewrite WHILET_unfold) (simp add: upt_conv_Cons "1.IH"[OF True, abs_def])
  qed
qed
*)  



sepref_definition sort_impl [llvm_code] is 
  "sort_by_prio" :: "[λl. length l < max_snat LENGTH(64)]⇩a (al_assn' TYPE(64) (snat_assn' TYPE(64)))⇧k → al_assn' TYPE(64) (snat_assn' TYPE(64))"
  unfolding sort_by_prio_def[abs_def] 
  apply (rewrite nfoldli_by_idx)
  apply (rewrite nfoldli_upt_by_while)
  apply (rewrite heap_fold_custom_empty[where 'l=64 and 'a="64"])
  apply (rewrite at op_list_empty al_fold_custom_empty[where 'l=64])
  apply (annot_snat_const "TYPE(64)")
  by sepref

  
  
export_llvm (no_header)
  sort_impl is "sort" 
  "arl_new_raw :: (64 word,64) array_list llM" is "arl_new"
  "arl_push_back :: _ ⇒ _ ⇒ (64 word,64) array_list llM" is "arl_push_back"
  file "sort.ll"
  (* CAREFUL: The calling conventions generated by this LLVM code are hard/impossible to 
    interface from C !? *)
  
end