Theory IICF_Array_of_Array_List

theory IICF_Array_of_Array_List
imports "../Intf/IICF_List_List" "../../../ds/Array_of_Array_List"
begin
  
  abbreviation "raw_aal_assn TYPE('l::len2) TYPE('ll::len2) 
     (Array_of_Array_List.aal_assn :: (_,('l,_,'ll) array_array_list)dr_assn)"

  definition aal_assn where "aal_assn A  hr_comp (raw_aal_assn TYPE(_) TYPE(_)) (the_pure Alist_rellist_rel)"
  lemmas [safe_constraint_rules] = CN_FALSEI[of is_pure "aal_assn A" for A]

  abbreviation aal_assn' where "aal_assn' TYPE('l::len2) TYPE('ll::len2)  aal_assn :: _  _  ('l,_,'ll) array_array_list  _"
  

  context 
    fixes l_dummy :: "'l::len2 itself"
    fixes ll_dummy :: "'ll::len2 itself"
    fixes L LL AA
    defines [simp]: "L  (LENGTH ('l))"
    defines [simp]: "LL  (LENGTH ('ll))"
    defines [simp]: "AA  raw_aal_assn TYPE('l::len2) TYPE('ll::len2)"
  begin  

    private lemma n_unf: "hr_comp AA (the_pure Alist_rellist_rel) = aal_assn A" unfolding aal_assn_def AA_def ..
  
    private lemma params: 
      "(L,L)nat_rel"
      "(LL,LL)nat_rel"
      "(max_snat, max_snat)  Id  Id"
      by auto
    
    context 
      notes [fcomp_norm_unfold] = n_unf
      notes [param] = params
    begin
    
      private method p_hnr = unfold snat_rel_def snat.assn_is_rel[symmetric]; sepref_to_hoare; vcg
    
      lemma aal_push_back_hnr_aux: "(uncurry2 aal_push_back, uncurry2 (RETURN ooo op_list_list_push_back)) 
         [λ((xss,i),x). i < length xss  length (xss!i) + 1 < max_snat LL]a 
            AAd *a snat_assnk *a id_assnk  AA"
        by p_hnr
    
      sepref_decl_impl aal_push_back_hnr_aux
        unfolding short_circuit_conv by parametricity
                
      lemma aal_pop_back_hnr_aux: "(uncurry aal_pop_back, uncurry (RETURN oo op_list_list_pop_back)) 
         [λ(xss,i). i<length xss  xss!i[]]a AAd *a snat_assnk  id_assn ×a AA"
        by p_hnr

      sepref_decl_impl aal_pop_back_hnr_aux    
        unfolding short_circuit_conv conv_to_is_Nil by parametricity

      lemma aal_idx_hnr_aux: "(uncurry2 aal_idx, uncurry2 (RETURN ooo op_list_list_idx)) 
         [λ((xss,i),j). i<length xss  j < length (xss!i)]a AAk *a snat_assnk *a snat_assnk  id_assn"
        by p_hnr

      sepref_decl_impl aal_idx_hnr_aux         
        unfolding short_circuit_conv by parametricity

      lemma aal_upd_hnr_aux: "(uncurry3 aal_upd, uncurry3 (RETURN oooo op_list_list_upd)) 
         [λ(((xss,i),j),x). i<length xss  j < length (xss!i)]a AAd *a snat_assnk *a snat_assnk *a id_assnk  AA"
        by p_hnr

      sepref_decl_impl aal_upd_hnr_aux         
        unfolding short_circuit_conv by parametricity
        
                
      lemma aal_llen_hnr_aux: "(uncurry aal_llen, uncurry (RETURN oo op_list_list_llen)) 
         [λ(xss,i). i<length xss]a AAk *a snat_assnk  snat_assn"
        by p_hnr
        
      sepref_decl_impl aal_llen_hnr_aux .
                
      lemma aal_len_hnr_aux: "(aal_len,RETURN o op_list_list_len)  AAk a snat_assn" by p_hnr
      sepref_decl_impl aal_len_hnr_aux .
                
      lemma aal_empty_hnr_aux: "(aal_new_raw, RETURN o op_list_list_lempty)  [λ_. 4<LL]a snat_assnk  AA"
        by p_hnr

      sepref_decl_impl (no_register) aal_empty: aal_empty_hnr_aux .

      
      lemma aal_take_hnr_aux: "(uncurry2 aal_take, uncurry2 (RETURN ooo op_list_list_take)) 
         [λ((xss,i),l). i<length xss  l  length (xss!i)]a AAd *a snat_assnk *a snat_assnk  AA"
        by p_hnr

      sepref_decl_impl aal_take_hnr_aux    
        unfolding short_circuit_conv by parametricity
      
    end
  end  

  definition op_aal_lempty where [simp]: "op_aal_lempty TYPE('l::len2) TYPE('ll::len2)  op_list_list_lempty"
  sepref_register "op_aal_lempty TYPE('l::len2) TYPE('ll::len2)"
  
  lemma aal_lempty_hnr[sepref_fr_rules]: 
    "(aal_new_raw, RETURN  (PR_CONST (op_aal_lempty TYPE('l::len2) TYPE('ll::len2)))) 
       [λx. 4 < LENGTH('ll)]a snat_assnk  aal_assn' TYPE('l) TYPE('ll) A"
    using aal_empty_hnr by simp
    
  lemma aal_fold_custom_empty:
    "replicate n [] = op_aal_lempty TYPE('l::len2) TYPE('ll::len2) n"
    "op_list_list_lempty n = op_aal_lempty TYPE('l::len2) TYPE('ll::len2) n"
    "mop_list_list_lempty n = RETURN (op_aal_lempty TYPE('l::len2) TYPE('ll::len2) n)"
    by simp_all
  
    
  (* TODO: Move *)  
  lemma rdomp_conv_pure_part: "rdomp A a  (c. pure_part (A a c))"
    unfolding rdomp_def pure_part_def by blast
    
  lemma pure_part_EXS_conv[simp]: "pure_part (EXS x. A x)  (x. pure_part (A x))"  
    by (auto simp: pure_part_def)
    
  lemma pure_part_set_imgD:
    assumes "pure_part (⋃*iI. f i)"  
    shows "iI. pure_part (f i)"
  proof (cases "finite I")  
    assume "finite I"
    thus ?thesis using assms
      by (induction I) (auto dest!: pure_part_split_conj)
  next
    assume "infinite I"  
    with assms have False by simp
    thus ?thesis ..
  qed
    
  
  lemma pure_part_arl_assnD[vcg_prep_ext_rules]: "pure_part (arl_assn xs (a::(_,'l::len2) array_list)) 
     length xs < max_snat LENGTH('l)"
    unfolding arl_assn_def arl_assn'_def
    apply (cases a)
    by (auto dest!: pure_part_split_conj snat.vcg_prep_delete_assn)
    

  lemma aal_assn_boundsD_aux1:
    assumes A: "rdomp (aal_assn' TYPE('l::len2) TYPE('ll::len2) A) xss"  
    shows "length xss < max_snat LENGTH('l)" (is ?G1)
      and "xsset xss. length xs < max_snat LENGTH('ll)" (is ?G2)
      (*and "∀xs∈set xss. ∀x∈set xs. rdomp A x" (is ?G3)*)
      
  proof -    
    from A obtain x :: "('b,'ll) array_list list" and y where
      REL: "(y, xss)  the_pure Alist_rellist_rel"
      and "length x = length y"
      and PP: "xa{0..<length y}. pure_part (arl_assn (y ! xa) (x ! xa))"
      and LENY: "length y < max_snat LENGTH('l)"
      unfolding 
        IICF_Array_of_Array_List.aal_assn_def
        Array_of_Array_List.aal_assn_def
        nao_assn_def 
      apply (auto simp: rdomp_hrcomp_conv)
      apply (auto 
        simp: rdomp_conv_pure_part in_set_conv_nth
        dest!: pure_part_split_conj pure_part_set_imgD snat.vcg_prep_delete_assn) 
        
      done

    from REL have [simp]: "length xss = length y"  
      by (auto dest!: list_rel_imp_same_length)
      
    from LENY show "length xss < max_snat LENGTH('l)" by simp 
      
    have "xsset xss. length xs < max_snat LENGTH('ll) ⌦‹∧ (∀x∈set xs. rdomp A x)›"
    proof (rule ballI; clarsimp simp: in_set_conv_nth)  
      fix i
      assume ILEN: "i<length y"
    
      from REL ILEN have "(y!i,xss!i)the_pure Alist_rel"
        by parametricity simp_all
      then have [simp]: "length (xss!i) = length (y!i)"
        by (auto dest!: list_rel_imp_same_length)
    
      from PP ILEN have "pure_part (arl_assn (y ! i) (x ! i))" by auto
      hence "length (y!i) < max_snat LENGTH('ll)"
        by (auto dest!: pure_part_arl_assnD)
      then show "length (xss ! i) < max_snat LENGTH('ll)" by auto
    qed
    thus ?G2 by blast
  qed      

  lemma aal_assn_boundsD':
    assumes A: "rdomp (aal_assn' TYPE('l::len2) TYPE('ll::len2) A) xss"  
    shows "length xss < max_snat LENGTH('l) 
       (xsset xss. length xs < max_snat LENGTH('ll))"
    using aal_assn_boundsD_aux1[OF A] by auto
      
  lemma aal_assn_boundsD[sepref_bounds_dest]:  
    assumes A: "rdomp (aal_assn' TYPE('l::len2) TYPE('ll::len2) A) xss"  
    shows "length xss < max_snat LENGTH('l)"
    using aal_assn_boundsD_aux1[OF A] by auto
    
  subsection Ad-Hoc Regression Tests
    
  experiment
  begin
    sepref_definition example [llvm_code] is "λn. do {
      let l = replicate n [];
      
      let l = op_list_list_push_back l (n-1) 42;
      let l = op_list_list_push_back l (n-1) 43;
      let (x,l) = op_list_list_pop_back l (n-1);
      let l = op_list_list_push_back l (n-1) x;
      let l = op_list_list_take l (n-1) 1;
      
      RETURN l
    }" :: "[λn. n{1..150}]a (snat_assn' TYPE(32))k  aal_assn' TYPE(32) TYPE(32) (snat_assn' TYPE(32))"
    apply (rewrite aal_fold_custom_empty[where 'l=32 and 'll=32])
    apply (annot_snat_const "TYPE(32)")
    apply sepref
    done
  
    export_llvm (no_header) example is example
  
    
  end  
  
  
  
            
        
end