Theory IICF

section ‹The LLVM Imperative Isabelle Collection Framework›
theory IICF
imports 
  (* Sets *)
  "Intf/IICF_Set"

  (* Multisets *)
  "Intf/IICF_Multiset"
  "Intf/IICF_Prio_Bag"

  "Impl/Heaps/IICF_Impl_Heap"
  

  (* Maps *)
  "Intf/IICF_Map"
  "Intf/IICF_Prio_Map"

  "Impl/IICF_Array_Map"
  "Impl/IICF_Array_Map_Total"

  
  "Impl/Heaps/IICF_Impl_Heapmap"
    
  (* Lists *)
  "Intf/IICF_List"

  "Impl/IICF_Array"
  "Impl/IICF_Array_List"
  "Impl/IICF_Array_of_Array_List"
  (* Matrix *)
  (*"Intf/IICF_Matrix"*)


begin

subsection ‹Regression Tests›  
experiment
begin
  (* TODO: Augment! *)

  text ‹Free parameter›
  sepref_definition test_free1 is "λxs. doN { 
    ASSERT(length xs = 10); 
    r ← mop_list_get xs 1;
    mop_free xs;
    RETURN r
  }" :: "(array_assn bool1_assn)⇧d →⇩a bool1_assn"
    apply (annot_snat_const "TYPE(64)")
    by sepref

  
  text ‹Free bound var before it goes out of scope›
  sepref_definition test_free2 is "λN. doN { 
    ASSERT(N>10); 
    xs ← mop_array_custom_replicate N False;
    xs ← mop_list_set xs 3 True;
    r1 ← mop_list_get xs 2;
    r2 ← mop_list_get xs 3;
    mop_free xs;
    xs ← mop_array_custom_replicate N False;
    RETURN (r1 ∧ r2) 
  }" :: "(snat_assn' TYPE(64))⇧k →⇩a bool1_assn"
    apply (annot_snat_const "TYPE(64)")
    by sepref
    
  text ‹Free bound var + parameter›
  sepref_definition test_free3 is "λxs. doN { 
    ASSERT(length xs = 10); 
    xs2 ← mop_array_custom_replicate 10 False;
    xs2 ← mop_list_set xs2 3 True;
    r1 ← mop_list_get xs2 1;
    mop_free xs2;
    r2 ← mop_list_get xs 1;
    mop_free xs;
    RETURN (r1 ∧ r2) 
  }" :: "(array_assn bool1_assn)⇧d →⇩a bool1_assn"
    apply (annot_snat_const "TYPE(64)")
    by sepref
  


end



end