Theory IsaSAT_ACIDS_LLVM

theory IsaSAT_ACIDS_LLVM
  imports IsaSAT_Literals_LLVM
    IsaSAT_ACIDS
    Pairing_Heaps_Impl_LLVM
    IsaSAT_Trail_LLVM
begin

definition acids_assn2 where
  ‹acids_assn2 = acids_assn ×⇩a uint64_nat_assn›

sepref_register ACIDS.mop_prio_insert_unchanged ACIDS.mop_prio_insert_raw_unchanged
sepref_def mop_prio_insert_raw_unchanged_impl
  is ‹uncurry ACIDS.mop_prio_insert_raw_unchanged›
  :: ‹atom_assn⇧k *⇩a acids_assn⇧d →⇩a acids_assn›
  unfolding ACIDS.mop_prio_insert_raw_unchanged_def
  by sepref

sepref_def mop_prio_insert_unchanged_impl
  is ‹uncurry ACIDS.mop_prio_insert_unchanged›
  :: ‹atom_assn⇧k *⇩a acids_assn⇧d →⇩a acids_assn›
  unfolding ACIDS.mop_prio_insert_unchanged_def
  by sepref

sepref_def acids_tl_impl
  is ‹uncurry acids_tl›
  :: ‹atom_assn⇧k *⇩a acids_assn2⇧d →⇩a acids_assn2›
  unfolding acids_assn2_def acids_tl_def max_def
  by sepref

sepref_def acids_pop_min_impl
  is acids_pop_min
  :: ‹acids_assn2⇧d →⇩a atom_assn ×⇩a acids_assn2›
  unfolding acids_pop_min_def acids_assn2_def
  by sepref

term ACIDS.mop_prio_insert_maybe

sepref_register ACIDS.mop_prio_insert_maybe
sepref_def mop_prio_insert_maybe_impl
  is ‹uncurry2 (PR_CONST ACIDS.mop_prio_insert_maybe)›
  ::  ‹atom_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a acids_assn⇧d →⇩a acids_assn›
  unfolding ACIDS.mop_prio_insert_maybe_def PR_CONST_def
  by sepref

sepref_def acids_push_literal_impl
  is ‹uncurry acids_push_literal›
  :: ‹atom_assn⇧k *⇩a acids_assn2⇧d →⇩a acids_assn2›
  unfolding acids_push_literal_def acids_assn2_def
    min_def
  apply (annot_unat_const ‹TYPE(64)›)
  by sepref

definition bottom_acids0 :: ‹_› where
  ‹bottom_acids0 = ((replicate 0 None, replicate 0 None, replicate 0 None, replicate 0 None, replicate 0 0, None))›

definition bottom_acids :: ‹_› where
  ‹bottom_acids = (bottom_acids0, None)›

sepref_def bottom_acids0_impl
  is ‹uncurry0 (RETURN bottom_acids0)›
  :: ‹unit_assn⇧k →⇩a hp_assn›
  unfolding bottom_acids0_def
  apply (rewrite at ‹(_, _, _, _, replicate 0 ⌑ , _)›
    unat_const_fold[where 'a=64])
  unfolding hp_assn_def atom.fold_option array_fold_custom_replicate
    al_fold_custom_empty[where 'l=64]
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

definition empty_acids0 where
  ‹empty_acids0 = ({#}, {#}, λ_::nat. 0::nat)›


definition empty_acids where
  ‹empty_acids = (empty_acids0, 0)›

lemma bottom_acids0:
  ‹(uncurry0 (RETURN bottom_acids0), uncurry0 (RETURN empty_acids0)) ∈ 
   unit_rel →⇩f ⟨((⟨⟨nat_rel⟩option_rel, ⟨nat_rel⟩option_rel⟩pairing_heaps_rel)) O
   acids_encoded_hmrel⟩nres_rel›
proof -
  have [intro!]: ‹Me ∈# {#} ⟹ False›for Me
    by auto
  have 1: ‹(({#}, (λ_. None, λ_. None, λ_. None, λ_. None, λ_. None), None), empty_acids0) ∈ acids_encoded_hmrel›
    by (auto simp: acids_encoded_hmrel_def bottom_acids0_def pairing_heaps_rel_def map_fun_rel_def
      ACIDS.hmrel_def encoded_hp_prop_list_conc_def encoded_hp_prop_def empty_outside_def empty_acids0_def
      intro!: relcompI)

  show ?thesis
    unfolding uncurry0_def
    apply (intro frefI nres_relI)
    apply (auto intro!:  relcompI[OF _ 1])
    by(auto simp: acids_encoded_hmrel_def bottom_acids0_def pairing_heaps_rel_def map_fun_rel_def
      ACIDS.hmrel_def encoded_hp_prop_list_conc_def encoded_hp_prop_def empty_outside_def)
qed

lemmas [sepref_fr_rules] =
  bottom_acids0_impl.refine[FCOMP bottom_acids0, unfolded hr_comp_assoc[symmetric] acids_assn_def[symmetric]]

sepref_def empty_acids_code
  is ‹uncurry0 (RETURN empty_acids)›
  :: ‹unit_assn⇧k →⇩a acids_assn2›
  unfolding empty_acids_def acids_assn2_def
  apply (annot_unat_const ‹TYPE(64)›)
  by sepref

schematic_goal free_acids_assn[sepref_frame_free_rules]: ‹MK_FREE acids_assn ?a›
  unfolding acids_assn_def hp_assn_def
  by synthesize_free


schematic_goal free_acids_assn2[sepref_frame_free_rules]: ‹MK_FREE acids_assn2 ?a›
  unfolding acids_assn2_def
  by synthesize_free

sepref_def free_acids
  is ‹mop_free›
  :: ‹acids_assn2⇧d →⇩a unit_assn›
  by sepref

lemma free_acids_assn2': ‹MK_FREE acids_assn2 free_acids›
  unfolding free_acids_def
  by (rule back_subst[of ‹MK_FREE acids_assn2›, OF free_acids_assn2])
    (auto intro!: ext)

end