Theory Sepref_Minitests
section ‹Miscellaneous Tests›
theory Sepref_Minitests
imports
"../IICF/IICF"
Sepref_Graph
"HOL-Library.Code_Target_Numeral"
begin
definition [simp]: "mop_plus = RETURN oo (+)"
definition [simp]: "mop_plusi = return oo (+)"
lemma [sepref_fr_rules]: "(uncurry mop_plusi,uncurry mop_plus) ∈ nat_assn⇧k*⇩anat_assn⇧k →⇩a nat_assn"
by (sep_auto intro!: hfrefI hn_refineI simp: pure_def)
sepref_register mop_plus
sepref_definition copy_test is "(λx. do {
let y = x+ x;
mop_plus y y
})" :: "((nat_assn)⇧k →⇩a UNSPEC)"
by sepref
definition "bar s ≡ do {
x←RETURN (insert (1::nat) s);
y←RETURN (insert (1::nat) x);
ASSERT (y≠{});
if 1∈y then
RETURN (y)
else RETURN (insert (1::nat) y)
}"
definition "bar2 s ≡ do {
if (1::nat)∈s then
RETURN True
else RETURN False
}"
definition "bar' ≡ do {
y ← RETURN {1,1::nat};
if 1∈y then
RETURN (y)
else RETURN (insert 1 y)
}"
definition "foo ≡ do {
s ← RETURN [1,1,1::nat];
y ← RETURN ({}::nat set);
RECT (λD l.
case l of
[] ⇒ RETURN (case [0,1] of [] ⇒ {} | x#xs ⇒ {x})
| x#l ⇒ do {
r ← D l;
RETURN (if x<1 then insert x r else insert (x+1) r)
}) s
}
"
definition "simple_rec ≡ do {
RECT (λD l. case l of
[] ⇒ RETURN 0
| x#xs ⇒ do {
a←D xs;
RETURN (a+x)
}
) [1,0::nat]
}"
definition "simple_while ≡ do {
WHILEIT (λ(i,m). i ∉ dom m) (λ(i,m). i≥1) (λ(i,m). do {
let i=i+1;
RETURN (i,m)
}) (10::nat, Map.empty::nat ⇀ nat)
}"
definition "lst_mem_to_sets ≡ do {
l←RETURN [0,1,0::nat];
RECT (λD l.
case l of
[] ⇒ RETURN []
| x#l ⇒ do {
r ← D l;
RETURN ({x}#r)
}) l
}
"
definition "lst_mem_to_sets_nonlin ≡ do {
l←RETURN [0,1,0::nat];
RECT (λD l.
case l of
[] ⇒ RETURN []
| x#l ⇒ do {
r ← D l;
RETURN ({x,x}#r)
}) l
}
"
definition "lst_mem_to_sets_nonlin2 ≡ do {
l←RETURN [0,1,0::nat];
RECT (λD l.
case l of
[] ⇒ RETURN []
| x#l ⇒ do {
r ← D l;
RETURN ({x}#r@r)
}) l
}
"
definition "lst_nonlin ≡ do {
l←RETURN [0::nat];
RETURN (case l of [] ⇒ l | x#xs ⇒ x#l)
}"
definition "lst_nonlin2 ≡ do {
l←RETURN [0::nat];
RETURN (case l of [] ⇒ [] | x#xs ⇒ x#(x#xs))
}"
definition "lst_nonlin3 ≡ do {
l←RETURN [{0::nat}];
RETURN (case l of [] ⇒ [] | x#xs ⇒ x#(x#xs))
}"
definition "lst_nonlin4 ≡ do {
l←RETURN [{0::nat}];
RETURN (l@l)
}"
definition "dup_arg == do {
x <- RETURN [1::nat];
RETURN (x@x)
}"
definition "big_list == RETURN [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1::nat]"
definition "big_list2 == do {
x1 <- RETURN ({}::nat set);
x2 <- RETURN {};
x3 <- RETURN {};
x4 <- RETURN {};
x5 <- RETURN {};
x6 <- RETURN {};
x7 <- RETURN {};
x8 <- RETURN {};
RETURN [x1,x2,x3,x4,x5,x6,x7,x8]
}"
term Set.insert
definition "foo1 ≡
case [] of
[] ⇒ RETURN {}
| x#l ⇒ do {
r ← RETURN ({}::nat set);
RETURN (if x<1 then insert x r else insert x r)
}
"
definition "basic_foreach ≡ do {
FOREACH⇩C {0,1::nat} (λs. s>1) (λx s. RETURN (x+s)) 0
}"
definition "basic_foreach2 ≡ do {
FOREACH⇩C {0,1::nat} (λ_. True) (λx s. RETURN (insert x s)) {}
}"
definition "basic_option ≡ do {
let a={};
let b=Some a;
let c=Some (0::nat);
let d=Some (1::nat);
RETURN (b,c=d)
}"
definition dfs :: "(('a×'a) set) ⇒ 'a ⇒ 'a ⇒ ('a set × bool) nres"
where
"⋀E vd v0. dfs E vd v0 ≡ REC⇩T (λD (V,v).
if v=vd then RETURN (V,True)
else if v∈V then RETURN (V,False)
else do {
let V=insert v V;
FOREACH⇩C (E``{v}) (λ(_,b). b=False) (λv' (V,_). D (V,v')) (V,False) }
) ({},v0)"
lemma ID_unfold_vars: "ID x y T ⟹ x≡y" by simp
schematic_goal testsuite_basic_param:
fixes s
notes [id_rules] =
itypeI[Pure.of s "TYPE(nat set)"]
shows
"hn_refine (emp * hn_ctxt (hs.assn id_assn) s s') (?c1::?'c1 Heap) ?Γ1' ?R1 (bar s)"
"hn_refine (emp * hn_ctxt (hs.assn id_assn) s s') (?c2::?'c2 Heap) ?Γ2' ?R2 (bar2 s)"
unfolding bar_def bar2_def
using [[id_debug]]
by sepref+
term case_list
thm id_rules
lemmas [id_rules] =
itypeI[Pure.of RECT "TYPE ((('a ⇒ 'b) ⇒ 'a ⇒ 'b) ⇒ 'a ⇒ 'b)"]
itypeI[Pure.of case_list "TYPE('a ⇒ ('b ⇒ 'b list ⇒ 'a) ⇒ 'b list ⇒ 'a)"]
ML ‹
fun is_eta_norm t = t aconv (Envir.eta_contract t)
fun find_not_eta_norm (a$b) = (find_not_eta_norm a @ find_not_eta_norm b)
| find_not_eta_norm (t as Abs (_,_,t'$Bound 0)) = t :: find_not_eta_norm t'
| find_not_eta_norm (Abs (_,_,t)) = find_not_eta_norm t
| find_not_eta_norm _ = []
fun is_eta_norm_tac st = if is_eta_norm (Thm.prop_of st) then Seq.single st
else (raise TERM ("¬eta-norm",find_not_eta_norm (Thm.prop_of st)))
›
definition "xfoo ≡ do {
s ← RETURN [1::nat];
y ← RETURN ({}::nat set);
RECT (λD l.
case l of
[] ⇒ RETURN ({0})
| x#l ⇒ do {
r ← D l;
RETURN (insert x r)
}) s
}
"
schematic_goal testsuite_basic1:
notes [sepref_fr_rules] = HOL_list_empty_hnr hs.hnr_op_empty[of nat_assn]
shows "hn_refine emp (?c1::?'c1 Heap) ?Γ1' ?R1 bar'"
and "hn_refine emp (?c2::?'c2 Heap) ?Γ2' ?R2 foo"
and "hn_refine emp (?c3::?'c3 Heap) ?Γ3' ?R3 simple_rec"
and "hn_refine emp (?c4::?'c4 Heap) ?Γ4' ?R4 lst_mem_to_sets"
and "hn_refine emp (?c5::?'c5 Heap) ?Γ5' ?R5 lst_mem_to_sets_nonlin"
and "hn_refine emp (?c7::?'c7 Heap) ?Γ7' ?R7 lst_nonlin"
and "hn_refine emp (?c8::?'c8 Heap) ?Γ8' ?R8 lst_nonlin2"
unfolding bar'_def foo_def simple_rec_def lst_mem_to_sets_def
lst_mem_to_sets_nonlin_def lst_mem_to_sets_nonlin2_def
lst_nonlin_def lst_nonlin2_def lst_nonlin3_def lst_nonlin4_def
using [[goals_limit = 1]]
apply sepref+
done
schematic_goal testsuite_basic2:
notes [sepref_fr_rules] = HOL_list_empty_hnr hs.hnr_op_empty hm.empty_hnr
shows "hn_refine emp (?c1::?'c1 Heap) ?Γ1' ?R1 dup_arg"
and "hn_refine emp (?c2::?'c2 Heap) ?Γ2' ?R2 big_list"
and "hn_refine emp (?c3::?'c3 Heap) ?Γ3' ?R3 big_list2"
and "hn_refine emp (?c4::?'c4 Heap) ?Γ4' ?R4 foo1"
and "hn_refine emp (?c5::?'c5 Heap) ?Γ5' ?R5 basic_foreach"
and "hn_refine emp (?c6::?'c6 Heap) ?Γ6' ?R6 basic_foreach2"
and "hn_refine emp (?c7::?'c7 Heap) ?Γ7' ?R7 basic_option"
and "hn_refine emp (?c8::?'c8 Heap) ?Γ8' ?R8 simple_while"
unfolding dup_arg_def big_list_def big_list2_def foo1_def
basic_foreach_def basic_foreach2_def simple_while_def
basic_option_def
using [[goals_limit = 1, id_debug]]
apply sepref+
done
sepref_definition imp_dfs is "uncurry2 dfs" :: "((adjg_assn nat_assn)⇧k *⇩a nat_assn⇧k *⇩a nat_assn⇧k →⇩a prod_assn (hs.assn nat_assn) bool_assn)"
unfolding dfs_def[abs_def]
apply (rewrite in "FOREACHc ⌑" op_graph_succ_def[symmetric])
apply (rewrite in "(⌑,_)" hs.fold_custom_empty)
using [[goals_limit = 1]]
by sepref
export_code imp_dfs checking SML_imp
definition "simple_algo a c m x = do {
let s = {m};
RECT (λD (x,s,l).
if x∈s then RETURN l
else D ((a*x+c) mod m,insert x s,l+1)
) (x::nat,s,0::nat)
}"
schematic_goal sa_impl:
notes [autoref_tyrel] = ty_REL[where 'a = "nat set"
and R="⟨nat_rel⟩iam_set_rel"]
assumes [autoref_rules]: "(a,a)∈nat_rel"
assumes [autoref_rules]: "(c,c)∈nat_rel"
assumes [autoref_rules]: "(m,m)∈nat_rel"
assumes [autoref_rules]: "(x,x)∈nat_rel"
shows "(?c::?'c,simple_algo a c m x)∈?R"
unfolding simple_algo_def[abs_def]
using [[autoref_trace_failed_id]]
apply autoref_monadic
done
concrete_definition sa_impl uses sa_impl
prepare_code_thms sa_impl_def
export_code sa_impl checking SML
sepref_definition sai_impl is
"(uncurry2 (uncurry simple_algo))"
:: "(nat_assn⇧k*⇩anat_assn⇧k*⇩anat_assn⇧k*⇩anat_assn⇧k →⇩a nat_assn)"
unfolding simple_algo_def[abs_def]
unfolding ias.fold_custom_empty
using [[goals_limit = 1]]
using [[id_debug]]
by sepref
export_code sai_impl checking SML
term Array.upd
definition "sad_impl a c m x ≡ do {
s←Array.new m False;
heap.fixp_fun (λD (x,s,l). do {
brk←Array.nth s x;
if brk then return l
else do {
_←Array.len s;
_←if x<l then return True else return False;
s←Array.upd x True s;
D ((a*x+c) mod m,s,l+1)
}
}) (x,s,0::nat)
}"
definition "sad_impl2 a c m x ≡ do {
s←Array.new m False;
heap.fixp_fun (λD (x,l). do {
brk←Array.nth s x;
if brk then return l
else do {
Array.upd x True s;
D ((a*x+c) mod m,l+1)
}
}) (x,0::nat)
}"
prepare_code_thms sad_impl_def
prepare_code_thms sad_impl2_def
code_thms sai_impl
lemma
"ias_ins k a = do {
l←Array.len a;
if k<l then
Array.upd k True a
else do {
let newsz = max (k+1) (2 * l + 3);
a←Array_Blit.array_grow a newsz False;
Array.upd k True a
}
}"
unfolding ias_ins_def
apply (fo_rule cong[OF arg_cong])
apply (auto)
done
export_code sa_impl sad_impl sad_impl2 sai_impl
checking SML_imp
schematic_goal
shows "hn_refine emp (?c1::?'c1 Heap) ?Γ1' ?R1
(do {
let x=(1::nat);
RETURN {x,x}
})"
apply (rewrite in "RETURN ⌑" hs.fold_custom_empty)
apply sepref
done
term hn_invalid
definition "remdup l ≡
RECT (λremdup. λ(
[],s) ⇒ RETURN op_HOL_list_empty
| (x#xs,s) ⇒ if x∈s then
remdup (xs,s )
else do {
l ← remdup (xs, insert x s);
RETURN (x#l)
}
) (l,op_hs_empty)
"
schematic_goal
fixes l :: "nat list"
notes [id_rules] = itypeI[Pure.of l "TYPE(nat list)"]
shows "hn_refine ( (hn_ctxt (list_assn (pure Id))) l li) (?c::?'c Heap) ?Γ ?R (remdup l)"
unfolding remdup_def
using [[id_debug]]
by sepref
text ‹Test structural frame-inference and merging (on product type)›
definition "smart_match_test1 ≡ λ(p1,p2). RETURN (p1+p2)"
sepref_definition smart_match_test1_impl is "smart_match_test1" :: "((prod_assn nat_assn nat_assn)⇧k →⇩a nat_assn)"
unfolding smart_match_test1_def
by sepref
sepref_register smart_match_test1
lemmas [sepref_fr_rules] = smart_match_test1_impl.refine
definition "smart_match_test2 ≡ do {
let p = (2::nat,2::nat);
f ← if True then
case p of (a,b) ⇒ RETURN (Some b)
else
case p of (a,b) ⇒ RETURN (Some a);
smart_match_test1 p
}"
sepref_thm smart_match_test2_impl is "uncurry0 smart_match_test2" :: "unit_assn⇧k →⇩a nat_assn"
unfolding smart_match_test2_def
by sepref
sepref_thm regr_incomplete_monadify is "RETURN o (λl. fold (λx. (#) (case x of (x, xa) ⇒ x + xa)) l [])" :: "(list_assn (prod_assn nat_assn nat_assn))⇧k →⇩a list_assn nat_assn"
unfolding test_def[abs_def] "HOL_list.fold_custom_empty"
by sepref
end