Theory CTR_Tests

(* Title: CTR/Tests/CTR_Tests.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins

A test suite for the sub-framework CTR.
*)

section‹A test suite for CTR›
theory CTR_Tests
  imports
    "../CTR"
    "../../IML_UT/IML_UT"
    Complex_Main
  keywords "ctr_test" :: thy_defn
begin



subsection‹Background›

ML‹

type ctr_test_data =
  {
    ctr_type : string,
    synthesis : (string * thm list option) option,
    elems: (string, string, Facts.ref) Element.ctxt list,
    type_specs : (string * string) list,
    thm_specs : ((binding option * thm) * mixfix) list
  };

structure CTRTestData = Generic_Data
  (
    type T = ctr_test_data Symtab.table
    val empty = Symtab.empty
    val merge = Symtab.merge (K true)
  );

val get_ctr_test_data_generic = CTRTestData.get;
val get_ctr_test_data_proof = Context.Proof #> get_ctr_test_data_generic;
val get_ctr_test_data_global = Context.Theory #> get_ctr_test_data_generic;
fun test_data_of_generic context = context
  |> get_ctr_test_data_generic
  |> Symtab.lookup;
val ctr_test_data_of_proof = Context.Proof #> test_data_of_generic;

(*oversimplified: to be used with care*)
fun update_ctr_test_data k ctr_test_data =
  Local_Theory.declaration
    {pervasive=true, syntax=false, pos = ⌂}
    (fn _ => (k, ctr_test_data) |> Symtab.update |> CTRTestData.map);

fun process_ctr_test_data (k, args) (lthy : local_theory) =
  let
    fun preprocess_thm_specs lthy =
      map (apfst (apsnd (singleton (Attrib.eval_thms lthy))))
    fun process_ctrs_impl (CTR.ALG_PP _) (lthy : local_theory) = lthy
      | process_ctrs_impl
          (CTR.ALG_RP (((synthesis, elems), type_specs), thm_specs))
          (lthy : local_theory) =
          let
            val thm_specs' = preprocess_thm_specs lthy thm_specs
            val synthesis' = Option.map
              (apsnd (Option.map ((single #> Attrib.eval_thms lthy))))
              synthesis
            val data : ctr_test_data =
              {
                ctr_type = "relativization",
                synthesis = synthesis',
                elems = elems,
                type_specs = type_specs,
                thm_specs = thm_specs'
              }
          in update_ctr_test_data k data lthy end
  in process_ctrs_impl args lthy end;

val ctr_test_parser = Parse.string -- CTR.ctr_parser;

val _ =
  Outer_Syntax.local_theory
    \<^command_keyword>‹ctr_test›
    "test setup for the command ctr"
    (ctr_test_parser >> process_ctr_test_data);

›

definition mono where
  "mono f ⟷ (∀x y. x ≤ y ⟶ f x ≤ f y)"

ud ‹mono›

definition mono_ow :: 
  "'a set ⇒ ('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool"
  where "mono_ow UB leb lea f ≡ ∀x∈UB. ∀y∈UB. lea x y ⟶ leb (f x) (f y)"

typedef 'a K = ‹{xs::'a list. length xs = 2}›
  by (simp add: Ex_list_of_length)

definition KK :: "'a K ⇒ 'a K ⇒ bool" 
  where "KK k1 k2 ≡ k1 = k2"

typedef 'a L = ‹{xs::'a list. length xs = 2}›
  by (simp add: Ex_list_of_length)

definition LL :: "'a L ⇒ 'a L ⇒ bool" 
  where "LL k1 k2 ≡ k1 = k2"

definition rel_L :: 
  "('a::group_add ⇒ 'b::group_add ⇒ bool) ⇒
  'a::group_add L ⇒
  'b::group_add L ⇒
  bool" 
  where "rel_L A b c = True"

ctr_relator rel_L

definition not_binders_binrelT :: 
  "('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ bool) ⇒ 'a ⇒ 'b ⇒ bool"
  where "not_binders_binrelT R1 R2 a b = True"

definition no_dup_binrelT :: 
  "('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'b ⇒ bool"
  where "no_dup_binrelT R1 R2 a b = True"

definition not_binders_binrelT_ftv_stv :: 
  "('a ⇒ 'b ⇒ bool) ⇒ (nat ⇒ 'c ⇒ bool) ⇒ 'a ⇒ 'b ⇒ bool"
  where "not_binders_binrelT_ftv_stv R1 R2 a b = True"

definition not_type_constructor_lhs :: 
  "('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool) ⇒ 'a ⇒ 'a K ⇒ bool"
  where "not_type_constructor_lhs R1 R2 a b = True"

definition not_type_constructor_rhs :: 
  "('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool) ⇒ 'a K ⇒ 'e ⇒ bool"
  where "not_type_constructor_rhs R1 R2 a b = True"

definition not_identical_type_constructors ::
  "('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool) ⇒ 'a K ⇒ 'e L ⇒ bool"
  where "not_identical_type_constructors R1 R2 a b = True"

definition not_identical_type_constructors_lhs ::
  "('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool) ⇒ 'a K ⇒ 'b K ⇒ bool"
  where "not_identical_type_constructors_lhs R1 R2 a b = True"

definition not_identical_type_constructors_rhs ::
  "('a ⇒ 'b ⇒ bool) ⇒ 'a K ⇒ 'c K ⇒ bool"
  where "not_identical_type_constructors_rhs R1 a b = True"



subsection‹Test data›

lemma mono_ow_transfer':
  includes lifting_syntax
  assumes [transfer_domain_rule, transfer_rule]: "Domainp B = (λx. x ∈ UB)" 
    and [transfer_rule]: "right_total B" 
  shows
    "((A ===> A ===> (=)) ===> (B ===> B ===> (=)) ===> (B ===> A) ===> (=))
      (mono_ow UB) mono.with"
  unfolding mono_ow_def mono.with_def
  by (transfer_prover_start, transfer_step+) simp

ctr_test "mono_with" relativization
  synthesis ctr_simps_Collect_mem_eq
  assumes [transfer_domain_rule, transfer_rule]:
    "Domainp (B::'c⇒'d⇒bool) = (λx. x ∈ UB)"
    and [transfer_rule]: "right_total B" 
  trp (?'b ‹A::'a⇒'b⇒bool›) and (?'a B)
  in mono_ow': mono.with_def 

ctr_test "exI" relativization
  in mono_ow'': exI

ctr_test "binrel" relativization
  synthesis ctr_simps_Collect_mem_eq
  assumes [transfer_domain_rule, transfer_rule]:
    "Domainp (B::'c⇒'d⇒bool) = (λx. x ∈ UB)"
    and [transfer_rule]: "right_total B" 
  trp (?'b A) and (?'a B)
  in mono_ow': mono.with_def 

ctr_test "binrel_ftv" relativization
  synthesis ctr_simps_Collect_mem_eq
  assumes [transfer_domain_rule, transfer_rule]:
    "Domainp (B::'c⇒'d⇒bool) = (λx. x ∈ UB)"
    and [transfer_rule]: "right_total B" 
  trp (?'b ‹A::nat⇒'b⇒bool›) and (?'a B)
  in mono_ow': mono.with_def 

ctr_test "dup_stvs" relativization
  synthesis ctr_simps_Collect_mem_eq
  assumes [transfer_domain_rule, transfer_rule]:
    "Domainp (B::'c⇒'d⇒bool) = (λx. x ∈ UB)"
    and [transfer_rule]: "right_total B" 
  trp (?'b ‹A::'a⇒'b⇒bool›) and (?'b B)
  in mono_ow': mono.with_def 

ctr_test "dup_binrel_ftvs" relativization
  synthesis ctr_simps_Collect_mem_eq
  assumes [transfer_domain_rule, transfer_rule]:
    "Domainp (B::'c⇒'d⇒bool) = (λx. x ∈ UB)"
    and [transfer_rule]: "right_total B" 
  trp (?'b ‹A::'a⇒'d⇒bool›) and (?'a B)
  in mono_ow': mono.with_def 

ctr_test "no_relator" relativization
  synthesis ctr_simps_Collect_mem_eq
  assumes [transfer_domain_rule, transfer_rule]:
    "Domainp (B::'c⇒'d⇒bool) = (λx. x ∈ UB)"
    and [transfer_rule]: "right_total B" 
  trp (?'b ‹A::'a⇒'b⇒bool›) and (?'a B) 
  in KK_def

ctr_test "invalid_relator" relativization
  synthesis ctr_simps_Collect_mem_eq
  assumes [transfer_domain_rule, transfer_rule]:
    "Domainp (B::'c⇒'d⇒bool) = (λx. x ∈ UB)"
    and [transfer_rule]: "right_total B" 
  trp (?'b ‹A::'a⇒'b⇒bool›) and (?'a B)
  in LL_def



subsection‹Tests›


subsubsection‹‹process_relativization››

ML_file‹CTR_TEST_PROCESS_RELATIVIZATION.ML›

context
  includes lifting_syntax
begin
ML‹
Lecker.test_group @{context} () [ctr_test_process_relativization.test_suite]
›
end


subsubsection‹‹process_ctr_relator››

ML_file‹CTR_TEST_PROCESS_CTR_RELATOR.ML›

context
  includes lifting_syntax
begin
ML‹
Lecker.test_group @{context} () [ctr_test_process_ctr_relator.test_suite]
›
end

end