Theory Coll_Test

theory Coll_Test
imports 
  Collections.Refine_Dflt 
  Succ_Graph
begin

declare [[autoref_trace_failed_id]]

context begin interpretation autoref_syn .

schematic_goal "(?c::?'c,
  RETURN (({(1::nat,2::nat),(3,4)}):::(⟨⟨nat_rel,nat_rel⟩prod_rel⟩(map2set_rel (ahm_rel ?bhc))) )
)∈?R"
  apply autoref_monadic
  done

term dflt_ahs_rel

schematic_goal "(?c::?'c, λ(a::'a::hashable) (b::'a::hashable).
  ({(a,b)}:::⟨?Rk::(?'b::hashable×_) set⟩dflt_ahs_rel)
)∈?R"
  apply (autoref (keep_goal))
  done

subsection "Foreach-Loops"
schematic_goal "(?c::?'c,
  FOREACH {1,2,3::nat} (λi s. RETURN (i+s)) 0
)∈?R"
  apply autoref_monadic
  done

schematic_goal "(?c::?'c,
  FOREACH (map_to_set [1::nat↦True, 2↦False]) (λ(k,v) s. RETURN (k+s)) 0
)∈?R"
  apply autoref_monadic
  done

(* TODO: generic algorithm for bounded hash code of sets! *)
schematic_goal "(?c::?'c,
  FOREACH 
    (map_to_set ([{1::nat}↦True, {2}↦False]:::⟨⟨nat_rel⟩dflt_rs_rel,bool_rel⟩(rbt_map_rel ?cmp))) 
    (λ(k,v) s. RETURN (v∧s)) False
)∈?R"
  apply autoref_monadic
  done

subsection "Array Hash Map Tests"

schematic_goal
  "(?f::?'c, λm. (m)(1::nat↦2::nat)) ∈ ?R"
  apply (autoref (keep_goal))
  done


schematic_goal
  "(?f::?'c, λm. (m:::⟨Id,Id⟩dflt_ahm_rel)(1::nat↦2::nat)) ∈ ?R"
apply (autoref (keep_goal))
done

schematic_goal
  "(?f::?'c, Map.empty:::⟨Id,Id⟩dflt_ahm_rel) ∈ ?R"
apply (autoref)
done

schematic_goal
  fixes mi m
  (* TODO: Obviously, we cannot override the tyREL-rule for 
    "nat⇀nat" with this: *)
  assumes [autoref_rules]: "(mi,m)∈⟨nat_rel,nat_rel⟩dflt_ahm_rel"
  shows "(?f::?'c, 
    RETURN (card (dom (m:::⟨nat_rel,nat_rel⟩dflt_ahm_rel)))) ∈ ?R"
  apply (autoref_monadic)
  done

(* Optimizations *)

subsection "List Map Tests"

definition foo::"(nat⇀nat) nres" where "foo ≡
  do {
    let X = Map.empty;
    ASSERT (1 ∉ dom X);
    RETURN (X(1 ↦ 2))
  }"

schematic_goal list_map_update_dj_test:
  "(?f::?'c, foo ::: ⟨⟨Id,Id⟩list_map_rel⟩nres_rel) ∈ ?R"
  unfolding foo_def 
  apply autoref_monadic
  done

schematic_goal 
  "(?f::?'c, [1::nat ↦ 2::nat, 3↦4] ::: ⟨nat_rel,nat_rel⟩list_map_rel) ∈ ?R"
  apply autoref
  done

schematic_goal list_map_test:
  "(?f::?'c, RETURN (([1 ↦ 2, 3::nat ↦ 4::nat]
       :::⟨nat_rel,nat_rel⟩list_map_rel) |`(-{1}))) ∈ ?R"
apply (autoref_monadic)
done
concrete_definition list_map_test uses list_map_test
value list_map_test

(* Why does this work:*)
schematic_goal
  "(?f::?'c, RETURN (card (dom ([1 ↦ 2, 3::nat ↦ 4::nat]
       :::⟨nat_rel,nat_rel⟩list_map_rel)))) ∈ ?R"
apply (autoref_monadic)
done

(* But this doesn't? This is not specific to list_map;
   it doesn't work with dflt_rbt_rel either.*)
(*schematic_lemma
  "(?f::?'c, RETURN (dom ([1 ↦ 2, 3::nat ↦ 4::nat]
       :::⟨nat_rel,nat_rel⟩list_map_rel))) ∈ ?R"
apply (autoref_monadic)
done*)


subsection "Array-Map Tests"

term "{1,2::nat} ∪ {3,4}"

schematic_goal array_set_test_code:
  "(?f::?'c, RETURN (({1,2::nat} ∪ {3,4} 
       ::: ⟨nat_rel⟩iam_set_rel )))∈?R" 
by (autoref_monadic (trace))

concrete_definition array_set_test uses array_set_test_code
print_theorems
value [nbe] array_set_test

schematic_goal
  "(?f::?'c, RETURN (({1} ::: ⟨nat_rel⟩dflt_rs_rel) = {}))∈?R" 
apply (autoref_monadic (trace))
done

schematic_goal
  "(?f::?'c, RETURN (card {1,2,3::nat}))∈?R" 
apply (autoref_monadic (trace))
done

schematic_goal
  "(?f::?'c, RETURN (∀x∈{1,2,3::nat}. x<4))∈?R" 
apply (autoref_monadic (trace))
done

schematic_goal
  "(?f::?'c, RETURN (∃x∈{1,2,3::nat}. x<4))∈?R" 
apply (autoref_monadic (trace))
done

schematic_goal
  "(?f::?'c, RETURN (({1} ::: ⟨nat_rel⟩iam_set_rel) = {}))∈?R" 
  apply (autoref_monadic (trace))
  done

schematic_goal
  assumes [autoref_rules]: "(f,f')∈nat_rel→Rb"
  shows "(?f::?'c,f' 3)∈?R"
  by (autoref)


schematic_goal "(?f::?'c,
  RETURN (({1,2::nat} × {3,4::nat}) ::: ⟨⟨Id,Id⟩prod_rel⟩dflt_rs_rel)
)∈?R"
  by autoref_monadic

schematic_goal "(?f::?'c,
  RETURN ({1,2::nat} ∩ ({3,4::nat}) ::: ⟨Id⟩list_set_rel)
)∈?R"
  by autoref_monadic

schematic_goal "(?f::?'c,
  RETURN ({1,2::nat} ∩ ({3,4::nat}) ::: ⟨Id⟩dflt_rs_rel)
)∈?R"
  by autoref_monadic

schematic_goal "(?f::?'c,
  RETURN (card (dom ([ 1::nat ↦ True, 2↦False ] ::: ⟨Id,Id⟩dflt_rm_rel )))
)∈?R"
  by autoref_monadic

text ‹A hairy case for the operator identification heuristics for maps:›
schematic_goal 
  shows "(?f::?'c,
  λm (x::'a::linorder) (y::'b::linorder). case_option
    None
    (λm'. m' y)
    (m x)
)∈?R"
  by (autoref (keep_goal))


schematic_goal 
  shows "(?f::?'c,
  λm (x::'a::hashable) (y::'b::hashable). case_option
    None
    (λm'. m' y)
    (m x)
)∈?R"
  apply (autoref (keep_goal))
  done


schematic_goal 
  shows "(?f::?'c,
  λm (x::'a::hashable) (y::'b::linorder). case_option
    None
    (λm'. m' y)
    (m (x:::Id))
)∈?R"
  by (autoref (keep_goal))


schematic_goal "(?f::?'c,
  {1,2::'a::numeral} × {3,4::'a}
)∈?R"
  by (autoref (keep_goal))

schematic_goal "(?f::?'c,
  {1,2::'a::{numeral,hashable}} × ({3,4::'a} ::: ⟨Id⟩dflt_ahs_rel)
)∈?R"
  by (autoref (keep_goal))

schematic_goal "(?f::?'c,
  {1,2::nat} × {3,4::nat}
)∈?R"
  by (autoref (keep_goal))

schematic_goal "(?f::?'c,
  {1,2::nat} ∩ {3,4::nat}
)∈?R"
  by (autoref (keep_goal))

schematic_goal "(?f::?'c,
  RETURN (({1,2::nat} × {3,4::nat}) ::: ⟨⟨Id,Id⟩prod_rel⟩dflt_rs_rel)
)∈?R"
  by autoref_monadic

(* TODO: ty_REL hint is ignored. Reason: Seems to not properly work with GAs! *)
schematic_goal 
  notes [autoref_tyrel] = ty_REL[where 'a = "(nat×nat) set" 
    and R="⟨⟨Id,Id⟩prod_rel⟩dflt_rs_rel"] 
  shows "(?f::?'c,
    RETURN (({1,2::nat} × {3,4::nat}))
  )∈?R"
  by autoref_monadic

(* TODO: Iterator optimization does not capture 
    foldli ((map fst ∘ rbt_to_list) x)
pattern!
*)

text ‹We have an optimized version for add on red-black trees›
schematic_goal "(?f::?'c,
  [ 1::nat ↦ True, 2::nat ↦ False ] ++ [ 3::nat ↦ True, 4::nat ↦ False ]
)∈?R"
  by (autoref (keep_goal))

text ‹The optimized version is also transfered through the map2set converter›
schematic_goal "(?f::?'c,
  {1,2::nat} ∪ {3,4}
)∈?R"
  by (autoref (keep_goal))

text ‹For list-sets, the generic version is used›
schematic_goal "(?f::?'c,
  {1,2::nat} ∪ {3,4} ::: ⟨Id⟩list_set_rel
)∈?R"
  by (autoref (keep_goal))


lemma is_refgoal: "(c,a)∈R ⟹ (c,a)∈R" .

schematic_goal "(?f::?'c,
  ({{1::nat}:::⟨Id⟩ map2set_rel dflt_rm_rel} ) 
  ∪ ({{2,3,4,5,5,6,7,8,98,9,0}}) 
)∈?R"
  by (autoref (keep_goal))


text ‹The next two lemmas demonstrate optimization: The insert-operation
  is translated by @{term "(#)"}›
schematic_goal "(?f::?'c, {1,2,3,4::nat}:::⟨Id⟩list_set_rel
  )∈?R"
  by (autoref (keep_goal))

schematic_goal 
  "(?f::?'c, {{1},{2},{3},{4::nat}}:::⟨?R'::(?'d×_) set⟩list_set_rel
  )∈?R"
  by (autoref (keep_goal))


schematic_goal "(?f::?'c,
  SPEC (λx. x∈({1,2,3::nat}:::⟨Id⟩dflt_rs_rel)) 
)∈?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?f::?'c,
  λs::nat set. {s} ∪ {{1,2,3}} = {{1}}
)∈?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?f::?'c,
  ∀(k,v)∈map_to_set [1::nat↦2::nat]. k>v
)∈?R"
  by (autoref (keep_goal))

schematic_goal "(?f::?'c, do {
  let s = ({1,2,3::nat}:::⟨Id⟩dflt_rs_rel);
  FOREACH s (λn s. RETURN (n+s)) 0
}
)∈?R"
  by autoref_monadic

schematic_goal "(?f::?'c, do {
  let s = ({{1,2,3::nat}, {}, {1,2}});
  FOREACH s (λn s. RETURN (n ∪ s)) {}
}
)∈?R"
  by (autoref_monadic)

schematic_goal "(?f::?'c,
  ({{1::nat}} ) 
  ∪ ({{2,3,4,5,5,6,7,8,98,9,0}}) 
)∈?R"
  by (autoref (keep_goal))

schematic_goal "(?f::?'c,
  SPEC (λx. x∈({1,2,3::nat})) 
)∈?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?f::?'c,
  λs::nat set. {s} ∪ {{1,2,3}} = {{1}}
)∈?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?f::?'c,
  ∀(k,v)∈map_to_set [1::nat↦2::nat]. k>v
)∈?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?f::?'c,
  [ 1::nat ↦ [ 2::nat ↦ 3::nat, 1::nat ↦ 3::nat ] ]
)∈?R"
  apply (autoref (keep_goal))
  done

end

text ‹Indirect Annotation›
consts 
  rel_set1 :: rel_name
  rel_set2 :: rel_name


context begin interpretation autoref_syn .

definition 
  "algo ≡ ( {1,2,3::nat}::#rel_set1, {1,2,3::nat}::#rel_set2 )"

schematic_goal 
  notes [autoref_rel_indirect] = 
    REL_INDIRECT[of rel_set1 "⟨Rk⟩list_set_rel" for Rk]
    REL_INDIRECT[of rel_set2 "⟨Rk⟩dflt_rs_rel" for Rk]
  shows "(?f::?'c,algo) ∈ ?R"
  unfolding algo_def
  by (autoref)

schematic_goal 
  notes [autoref_rel_indirect] = 
    REL_INDIRECT[of rel_set1 "⟨Rk⟩dflt_rs_rel" for Rk]
    REL_INDIRECT[of rel_set2 "⟨Rk⟩dflt_rs_rel" for Rk]
  shows "(?f::?'c,algo) ∈ ?R"
  unfolding algo_def
  by (autoref)



text ‹A witness of the red algorithm is a node on the stack and a path
  to this node›
type_synonym 'v red_witness = "('v list × 'v) option"
text ‹Prepend node to red witness›
fun prep_wit_red :: "'v ⇒ 'v red_witness ⇒ 'v red_witness" where
  "prep_wit_red v None = None"
| "prep_wit_red v (Some (p,u)) = Some (v#p,u)"

text ‹
  Initial witness for node ‹u› with onstack successor ‹v› 
›
definition red_init_witness :: "'v ⇒ 'v ⇒ 'v red_witness" where
  "red_init_witness u v = Some ([u],v)"

definition red_dfs where
  "red_dfs E onstack V u ≡ 
    REC⇩T (λD (V,u). do {
      let V=(insert u V);

      ― ‹Check whether we have a successor on stack›
      brk ← FOREACH⇩C (E``{u}) (λbrk. brk=None) 
        (λt _. if t∈onstack then RETURN (red_init_witness u t) else RETURN None)
        None;

      ― ‹Recurse for successors›
      case brk of
        None ⇒
          FOREACH⇩C ((E``{u})) (λ(V,brk). brk=None)
            (λt (V,_). 
              if t∉V then do {
                (V,brk) ← D (V,t);
                RETURN (V,prep_wit_red u brk)
              } else RETURN (V,None))
            (V,None)
      | _ ⇒ RETURN (V,brk)
    }) (V,u)
  "

abbreviation "i_red_witness ≡ ⟨⟨⟨i_nat⟩⇩ii_list,i_nat⟩⇩ii_prod⟩⇩ii_option"
lemma [autoref_itype]:
  "red_init_witness ::⇩i i_nat →⇩i i_nat →⇩i i_red_witness"
  "prep_wit_red ::⇩i i_nat →⇩i i_red_witness →⇩i i_red_witness"
  by auto

abbreviation "red_witness_rel ≡ ⟨⟨⟨nat_rel⟩list_rel,nat_rel⟩prod_rel⟩option_rel"

lemma [autoref_rules_raw]:
  "(red_init_witness,red_init_witness) ∈ nat_rel→nat_rel→red_witness_rel"
  "(prep_wit_red,prep_wit_red) ∈ nat_rel → red_witness_rel → red_witness_rel"
  by (auto)

(*schematic_lemma 
  "(?f, RECT (λD x. D x)) ∈ (?R::(?'c×_) set)"
  apply (autoref (keep_goal))
  done*)

schematic_goal red_dfs_impl:
  notes [[goals_limit = 1]]
  fixes u'::"nat" and V'::"nat set"
  assumes [autoref_rules]:
    "(u,u')∈nat_rel" 
    "(V,V')∈⟨nat_rel⟩dflt_rs_rel" 
    "(onstack,onstack')∈⟨nat_rel⟩dflt_rs_rel" 
    "(E,E')∈⟨nat_rel⟩slg_rel"
  shows "(?f, red_dfs E' onstack' V' u') ∈ (?R::(?'c×_) set)"
  apply -
  unfolding red_dfs_def
  apply (autoref_monadic (trace))
  done

concrete_definition red_dfs_impl for E onstack V u uses red_dfs_impl 

prepare_code_thms red_dfs_impl_def

export_code red_dfs_impl checking SML


end
end