File ‹sep_steps_test.ML›

(*
  File: sep_steps_test.ML
  Author: Bohua Zhan

  Unit test for sep_steps.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