File ‹sep_steps_test.ML›
local
open SepUtil
val ctxt = @{context}
val ctxt' = ctxt |> fold Proof_Context.augment [
Free ("P", assnT), Free ("Q", assnT), Free ("R", assnT),
Free ("S", natT --> assnT), Free ("T", natT --> assnT)]
in
val test_normalize_assn =
let
val test_data = [
("P * (Q * R)", "P * Q * R"),
("P * ↑(b)", "P * ↑(b)"),
("↑(b) * P", "P * ↑(b)"),
("P * ↑(b) * Q", "P * Q * ↑(b)"),
("↑(b) * (P * ↑(c)) * Q", "P * Q * ↑(b) * ↑(c)"),
("EXA x. S x", "EXA x. S x"),
("(EXA x. S x) * P", "EXA x. P * S x"),
("P * (EXA x. S x)", "EXA x. P * S x"),
("(EXA x. S x) * (EXA y. T y)", "EXA x y. S x * T y"),
("EXA x. S x * ↑(B x) * T x", "EXA x. S x * T x * ↑(B x)"),
("P * true * true", "P * true"),
("true * P * true", "P * true"),
("true * P * true * ↑(b)", "P * true * ↑(b)"),
("(EXA x. S x) * P * Q", "EXA x. P * Q * S x"),
("↑(b1 & b2)", "↑b1 * ↑b2")
]
in
map (Util.test_conv ctxt' (SepUtil.normalize_assn_cv ctxt')
"normalize_assn")
test_data
end
val test_contract_hoare =
let
val test_data = [
("<P * ↑(b)> c <S>", "<P * ↑(b)> c <S>"),
("b --> <P> c <S>", "<P * ↑(b)> c <S>"),
("b1 --> b2 --> <P> c <S>", "<P * ↑(b2) * ↑(b1)> c <S>"),
("b1 --> <P * ↑(b2)> c <S>", "<P * ↑(b2) * ↑(b1)> c <S>"),
("<Q * P> c <S>", "<P * Q> c <S>")
]
in
map (Util.test_conv ctxt' (SepLogic.contract_hoare_cv ctxt')
"contract_hoare")
test_data
end
val test_normalize_hoare_goal =
let
val test_data = [
("~<P> c <S>", "~<P> c <S>"),
("~<↑(b)> c <S>", "~<emp> c <S> & b"),
("~<P * ↑(b)> c <S>", "~<P> c <S> & b"),
("~<↑(b1) * ↑(b2)> c <S>", "(~<emp> c <S> & b1) & b2"),
("~<P * Q> c <S>", "~<P * Q> c <S>"),
("EX x. ~<T x> c <S>", "EX x. ~<T x> c <S>"),
("EX x. ~<↑(b x)> c <S>", "EX x. ~<emp> c <S> & b x")
]
in
map (Util.test_conv ctxt' (SepLogic.normalize_hoare_goal_cv ctxt')
"normalize_hoare_goal")
test_data
end
val test_normalize_entail_goal =
let
val test_data = [
("~(entails P Q)", "~(entails P Q)"),
("~(entails (↑b) Q)", "~(entails emp Q) & b"),
("~(entails (↑b * P) Q)", "~(entails P Q) & b"),
("~(entails (EXA x. S x) Q)", "EX x. ~(entails (S x) Q)")
]
in
map (Util.test_conv ctxt' (SepLogic.normalize_entail_goal_cv ctxt')
"normalize_entail_goal")
test_data
end
end