(* Title: tests on ProgLang/termC.sml

   Author: Walther Neuper 051006,

   (c) due to copyright terms

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- numerals in Isabelle2011/12/13 -------------";

"----------- inst_bdv -----------------------------------";

"----------- subst_atomic_all ---------------------------";

"----------- Pattern.match ------------------------------";

"----------- fun TermC.matches --------------------------------";

"----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------";

"----------- fun TermC.vars_of ---------------------------------------------------------------";

"----------- fun TermC.vars --------------------------------------------------------------------";

"----------- *** Problem.prep_input: syntax error in '#Where' of [v";

"----------- check writeln, tracing for string markup ---";

"----------- build fun TermC.is_bdv_subst ------------------------------------------------------------";

"----------- fun str_of_int --------------------------------------------------------------------";

"----------- fun TermC.scala_of_term -----------------------------------------------------------------";

"----------- fun TermC.contains_Var ------------------------------------------------------------------";

"----------- fun int_opt_of_string, fun is_num -------------------------------------------------";

"----------- fun TermC.is_f_x ------------------------------------------------------------------------";

"----------- fun list2isalist, fun isalist2list ------------------------------------------------";

"----------- fun TermC.strip_imp_prems' --------------------------------------------------------------";

"----------- fun TermC.ins_concl ---------------------------------------------------------------------";

"----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";

"----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";

"----------- fun TermC.is_list -----------------------------------------------------------------------";

"----------- fun inst_abs ----------------------------------------------------------------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

"----------- numerals in Isabelle2011/12/13 -------------";

"----------- numerals in Isabelle2011/12/13 -------------";

"----------- numerals in Isabelle2011/12/13 -------------";

"***Isabelle2011 ~= Isabelle2012 = Isabelle2013";

"***Isabelle2011**********************************************************************************";

@{term "0::nat"};

(*Const (\<^const_name>\<open>zero_class.zero\<close>, "Nat.nat")*)

@{term "1::nat"};

(*Const (\<^const_name>\<open>one_class.one\<close>, "Nat.nat")*)

@{term "5::nat"};

(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Nat.nat") $

     (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

       (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)

(*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)

@{term "0::int"};

(*Const (\<^const_name>\<open>zero_class.zero\<close>, "Int.int")*)

@{term "1::int"};

(*Const (\<^const_name>\<open>one_class.one\<close>, "Int.int")*)

@{term "5::int"};

(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Int.int") $

     (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

       (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)

@{term "-5::int"};

(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Int.int") $

     (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

       (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)

@{term "- 5::int"};

(*Const (\<^const_name>\<open>uminus\<close>, "Int.int \<Rightarrow> Int.int") $

     (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> Int.int") $

       (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $

           (Const ("Int.Bit1...", "Int.int \<Rightarrow> Int.int") $ Const (...)))))*)

(*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)

@{term "0::real"};

(*Const (\<^const_name>\<open>zero_class.zero\<close>, "Real.real")*)

@{term "1::real"};

(**)

@{term "5::real"};

(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> "Real.real") $

     (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

       (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)

@{term "-5::real"};

(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> "Real.real") $

     (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

       (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)

@{term "- 5::real"};

(*Const (\<^const_name>\<open>uminus\<close>, "Real.real \<Rightarrow> "Real.real") $

     (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> "Real.real") $

       (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $

         (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $

           (Const ("Int.Bit1...", "Int.int \<Rightarrow> Int.int") $ Const (...)))))*)

"***Isabelle2012**********************************************************************************";

@{term "0::nat"};

(*Const (\<^const_name>\<open>zero_class.zero\<close>, "nat")*)

@{term "1::nat"};

(*Const (\<^const_name>\<open>one_class.one\<close>, "nat")*)

@{term "5::nat"};

(*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> nat") $

     (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

       (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

(*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)

@{term "0::int"};

(*Const (\<^const_name>\<open>zero_class.zero\<close>, "int")*)

@{term "1::int"};

(*Const (\<^const_name>\<open>one_class.one\<close>, "int")*)

@{term "5::int"};

(*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> int") $

     (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

       (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

@{term "-5::int"};

(*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> int") $

     (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

       (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

@{term "- 5::int"};

(*Const (\<^const_name>\<open>uminus\<close>, "int \<Rightarrow> int") $

     (Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> int") $

       (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

         (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*)

(*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)

@{term "0::real"};

(*Const (\<^const_name>\<open>zero_class.zero\<close>, "real")*)

@{term "1::real"};

(*Const (\<^const_name>\<open>one_class.one\<close>, "real")*)

@{term "5::real"};

(*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> real") $

     (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

       (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

@{term "-5::real"};

(*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> real") $

     (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

       (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

@{term "- 5::real"};

(*Const (\<^const_name>\<open>uminus\<close>, "real \<Rightarrow> real") $

     (Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> real") $

       (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

         (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*)

"***Isabelle2013**********************************************************************************";

@{term "0::nat"};

(*Const (\<^const_name>\<open>zero_class.zero\<close>, "nat")*)

@{term "1::nat"};

(*Const (\<^const_name>\<open>one_class.one\<close>, "nat")*)

@{term "5::nat"};

(*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> nat") $

     (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

       (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

(*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)

@{term "0::int"};

(*Const (\<^const_name>\<open>zero_class.zero\<close>, "int")*)

@{term "1::int"};

(*Const (\<^const_name>\<open>one_class.one\<close>, "int")*)

@{term "5::int"};

(*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> int") $

     (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

       (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

@{term "-5::int"};

(*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> int") $

     (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

       (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

@{term "- 5::int"};

(*Const (\<^const_name>\<open>uminus\<close>, "int \<Rightarrow> int") $

     (Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> int") $

       (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

         (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*)

(*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)

@{term "0::real"};

(*Const (\<^const_name>\<open>zero_class.zero\<close>, "real")*)

@{term "1::real"};

(*Const (\<^const_name>\<open>one_class.one\<close>, "real")*)

@{term "5::real"};

(*Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> real") $

     (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

       (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

@{term "-5::real"};

(*Const ("Num.neg_numeral_class.neg_numeral", "num \<Rightarrow> real") $

     (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

       (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const (\<^const_name>\<open>num.One\<close>, "num")))*)

@{term "- 5::real"};

(*Const (\<^const_name>\<open>uminus\<close>, "real \<Rightarrow> real") $

     (Const (\<^const_name>\<open>numeral\<close>, "num \<Rightarrow> real") $

       (Const (\<^const_name>\<open>num.Bit1\<close>, "num \<Rightarrow> num") $

         (Const (\<^const_name>\<open>num.Bit0\<close>, "num \<Rightarrow> num") $ Const ("...", "num"))))*)

"----------- inst_bdv -----------------------------------";

"----------- inst_bdv -----------------------------------";

"----------- inst_bdv -----------------------------------";

 if (UnparseC.term o Thm.prop_of) @{thm d1_isolate_add2} = 

     "\<not> ?bdv occurs_in ?a \<Longrightarrow>\n(?a + ?bdv = 0) = (?bdv = - 1 * ?a)"

   then ()

   else error "termC.sml d1_isolate_add2";

 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];

 val t = (Eval.norm o Thm.prop_of)  @{thm d1_isolate_add2};

 val t' = TermC.inst_bdv subst t;

 if UnparseC.term t' = "\<not> x occurs_in ?a \<Longrightarrow> (?a + x = 0) = (x = - 1 * ?a)"

   then ()

   else error "termC.sml inst_bdv 1";

if (UnparseC.term o Thm.prop_of) @{thm separate_bdvs_add} = 

  "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0,\n         " ^

  "?bdv_4.0] occur_exactly_in ?a \<Longrightarrow>\n(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)"

then () else error "termC.sml separate_bdvs_add";

(*default_print_depth 5;*)

val subst = 

  [(TermC.parse_test @{context} "bdv_1", TermC.parse_test @{context} "c"),

 	   (TermC.parse_test @{context} "bdv_2", TermC.parse_test @{context} "c_2"),

 	   (TermC.parse_test @{context} "bdv_3", TermC.parse_test @{context} "c_3"),

 	   (TermC.parse_test @{context} "bdv_4", TermC.parse_test @{context} "c_4")];

val t = (Eval.norm o Thm.prop_of)  @{thm separate_bdvs_add};

val t' = TermC.inst_bdv subst t;

if UnparseC.term t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a \<Longrightarrow>\n" ^

  "(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)"

then () else error "termC.sml inst_bdv 2";

"----------- subst_atomic_all ---------------------------";

"----------- subst_atomic_all ---------------------------";

"----------- subst_atomic_all ---------------------------";

 val t = TermC.parse_test @{context} "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))";

 val env = [(TermC.parse_test @{context} "vs_vs::real list", TermC.parse_test @{context} "[c, c_2]"),

 	   (TermC.parse_test @{context} "es_es::bool list", TermC.parse_test @{context} "[c_2 = 0, c + c_2 = 1]")];

 val (all_Free_subst, t') = TermC.subst_atomic_all env t;

 if all_Free_subst andalso 

    UnparseC.term t' = "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1 [c_2 = 0, c + c_2 = 1]"

   then ()

   else error "termC.sml subst_atomic_all should be 'true'";

 val (all_Free_subst, t') = TermC.subst_atomic_all (tl env) t;

 if not all_Free_subst andalso 

    UnparseC.term t' = "tl vs_vs from vs_vs occur_exactly_in NTH 1 [c_2 = 0, c + c_2 = 1]" then ()

 else error "TermC.subst_atomic_all should be 'false'";

"----------- Pattern.match ------------------------------";

"----------- Pattern.match ------------------------------";

"----------- Pattern.match ------------------------------";

 val t = TermC.parse_test @{context} "3 * x\<up>2 = (1::real)";

 val pat = (TermC.free2var o TermC.parse_test @{context}) "a * b\<up>2 = (c::real)";

 (*        ! \<up>  \<up> ^^!... necessary for Pattern.match, see Logic.varify_global below*)

 val insts = Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty);

(*default_print_depth 3; 999*) insts; 

 (*val insts =

   ({}, 

    {(("a", 0), ("Real.real", Free ("3", "Real.real"))), 

     (("b", 0), ("Real.real", Free ("x", "Real.real"))),

     (("c", 0), ("Real.real", Free ("1", "Real.real")))})*)

 "----- throws exn MATCH...";

(* val t = TermC.parse_test @{context} "x";

 (Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty))

 handle MATCH => ???; *)

 val thy = @{theory "Complex_Main"};

 val PARSE = Syntax.read_term_global thy;

 val (pa, tm) = (PARSE "a + b::real", PARSE  "x + 2*z::real");

 val (tye, tme) = (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);

 val (tyenv, tenv) = Pattern.match thy (Logic.varify_global pa, tm) (tye, tme);

 Vartab.dest tenv;

"----------- fun TermC.matches --------------------------------";

"----------- fun TermC.matches --------------------------------";

"----------- fun TermC.matches --------------------------------";

 (*examples see

   test/../Knowledge/polyeq.sml:     

   Where=[Correct "matches (?a = 0) (-8 - 2 * x + x \<up> 2 = 0)"*)

 (*test/../Specify/refine.sml:        

   |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)"],*)

  val thy = @{theory "Complex_Main"}; 

"----- test 1: OK";

 val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*)

 tracing "paIsa=..."; TermC.atomty pa; tracing "...=paIsa";

(*** 

*** Const (op =, real => real => bool)

*** . Var ((a, 0), real)

*** . Const (Groups.zero_class.zero, real)

***)

"----- test 1a true";

 val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"};    (*<<<<<<<---------------*)

 if TermC.matches thy tm pa then () 

   else error "termC.sml diff.behav. in TermC.matches true 1";

"----- test 1b false";

 val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"};    (*<<<<<<<---------------*)

 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 1"

  else ();

"----- test 2: Nok";

 val pa = Logic.varify_global (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)

 tracing "paLo2=..."; TermC.atomty pa; tracing "...=paLo2";

(*** 

*** Const (op =, real => real => bool)

*** . Var ((a, 0), real)

*** . Var ((0, 0), real)

***)

"----- test 2a true";

 val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)

 if TermC.matches thy tm pa then () 

   else error "termC.sml diff.behav. in TermC.matches true 2";

"----- test 2b false";

 val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)";     (*<<<<<<<-------------*)

 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 2"

   else ();

(* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!!

if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 2"

  else ();*)

"----- test 3: OK";

 val pa = TermC.free2var (TermC.parse_test @{context} "a = (0::real)");(*<<<<<<<-------------*)

 tracing "paF2=..."; TermC.atomty pa; tracing "...=paF2";

(*** 

*** Const (op =, real => real => bool)

*** . Var ((a, 0), real)

*** . Free (0, real)

***)

"----- test 3a true";

 val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)

 if TermC.matches thy tm pa then () 

   else error "termC.sml diff.behav. in TermC.matches true 3";

"----- test 3b false";

 val tm = TermC.parse_test @{context} "-8 - 2 * x + x ^ 2 = (3::real)";     (*<<<<<<<-------------*)

 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 3"

   else ();

"----- test 4=3 with specific data";

 val pa = TermC.free2var (TermC.parse_test @{context} "M_b 0");

"----- test 4a true";

 val tm = TermC.parse_test @{context} "M_b 0";

 if TermC.matches thy tm pa then () 

   else error "termC.sml diff.behav. in TermC.matches true 4";

"----- test 4b false";

 val tm = TermC.parse_test @{context} "M_b x";

 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 4"

   else ();

"----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------";

"----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------";

"----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------";

(* added after Isabelle2015->17

> val (SOME ct) = TermC.parse thy "(-#5)\<up>#3"; 

> TermC.atomty (Thm.term_of ct);

*** -------------

*** Const ( Nat.op ^, ['a, nat] => 'a)

***   Const ( uminus, 'a => 'a)

***     Free ( #5, 'a)

***   Free ( #3, nat)                

> val (SOME ct) = TermC.parse thy "R=R"; 

> TermC.atomty (Thm.term_of ct);

*** -------------

*** Const ( op =, [real, real] => bool)

***   Free ( R, real)

***   Free ( R, real)

THIS IS THE OUTPUT FOR VERSION (3) above at TermC.typ_a2real !!!!!

*** -------------

*** Const ( op =, [RealDef.real, RealDef.real] => bool)

***   Free ( R, RealDef.real)

***   Free ( R, RealDef.real)                  *)

 val thy = @{theory "Complex_Main"};

 val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge")

 val str = "x + z";

 TermC.parseNEW' ctxt str;

"---------------";

 val str = "x + 2*z";

 val t =  Syntax.read_term_global thy str;

 val t = TermC.typ_a2real (Syntax.read_term_global thy str);

 Thm.global_cterm_of thy t;

 case TermC.parseNEW ctxt str of

   SOME t' => t'

 | NONE => error "termC.sml parsing 'x + 2*z' failed";

"===== fun TermC.parse_patt caused error in fun T_a2real ===";

 val thy = @{theory "Poly"};

 TermC.parse_patt thy "?p is_addUnordered";

 TermC.parse_patt thy "?p :: real";

"===== fun TermC.parse_patt caused error in fun T_a2real ===";

 val thy = @{theory "Poly"};

 TermC.parse_patt thy "?p is_addUnordered";

 TermC.parse_patt thy "?p :: real";

(* Christian Urban, 101001 

theory Test

imports Main Complex

begin

let

  val parser = Args.context -- Scan.lift Args.name_source

  fun term_pat (ctxt, str) = str |> Proof_Context.read_term_pattern ctxt

  |> ML_Syntax.print_term |> ML_Syntax.atomic

in

  ML_Antiquote.inline "term_pat" (parser >> term_pat)

end

  val t = @{term "a + b * x = (0 ::real)"};

  val pat = @{term_pat "?l = (?r ::real)"};

  val precond = @{term_pat "is_polynomial (?l::real)"};

  val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);

  Envir.subst_term inst precond

  |> Syntax.string_of_term @{context}

  |> writeln

end *)

"----------- fun TermC.vars_of ---------------------------------------------------------------";

"----------- fun TermC.vars_of ---------------------------------------------------------------";

"----------- fun TermC.vars_of ---------------------------------------------------------------";

val thy = @{theory Partial_Fractions};

val ctxt = Proof_Context.init_global @{theory}

val SOME t = TermC.parseNEW ctxt "x \<up> 2 + -1 * x * y";

case TermC.vars_of t of [Free ("x", _), Free ("y", _)] => ()

| _ => error "TermC.vars_of (x \<up> 2 + -1 * x * y) ..changed";

val SOME t = TermC.parseNEW ctxt "3 = 3 * AA / 4";

case TermC.vars_of t of [Const (\<^const_name>\<open>AA\<close>, _), Const (\<^const_name>\<open>HOL.eq\<close>, _)] => ()

| _ => error "TermC.vars_of (3 = 3 * AA / 4) ..changed (! use only for polynomials, not equations!)";

"----------- *** Problem.prep_input: syntax error in '#Where' of [v";

"----------- *** Problem.prep_input: syntax error in '#Where' of [v";

"----------- *** Problem.prep_input: syntax error in '#Where' of [v";

"===== deconstruct datatype typ ===";

 val str = "?a";

 val t = (thy, str) |>> Proof_Context.init_global

                    |-> Proof_Context.read_term_pattern;

 val Var (("a", 0), ty) = t;

 val TVar ((str, i), srt) = ty;

 if str = "'a" andalso i = 1 andalso srt = [] 

   then ()

   else error "termC.sml type-structure of \"?a\" changed";

"----- real type in pattern ---";

 val str = "?a :: real";

 val t = (thy, str) |>> Proof_Context.init_global 

                    |-> Proof_Context.read_term_pattern;

 val Var (("a", 0), ty) = t;

 val Type (str, tys) = ty;

 if str = \<^type_name>\<open>real\<close> andalso tys = [] andalso ty = HOLogic.realT

   then ()

   else error "termC.sml type-structure of \"?a :: real\" changed";

"===== Not (matchsub (?a + (?b + ?c)) t_t |... ===";

val (thy, str) = (thy, "Not (matchsub (?a + (?b + ?c)) t_t | " ^

	                "     matchsub (?a + (?b - ?c)) t_t | " ^

	                "     matchsub (?a - (?b + ?c)) t_t | " ^

	                "     matchsub (?a + (?b - ?c)) t_t )");

val ctxt = Proof_Context.init_global thy;

val ctxt = Config.put show_types true ctxt;

"----- read_term_pattern ---";

val t = (thy, str) |>> Proof_Context.init_global 

                    |-> Proof_Context.read_term_pattern;

val t_real = TermC.typ_a2real t;

if UnparseC.term_in_ctxt ctxt t_real =

  "\<not> (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) \<or>\n        "

  ^ "matchsub (?a + (?b - ?c)) t_t \<or>\n        "

  ^ "matchsub (?a - (?b + ?c)) t_t \<or> matchsub (?a + (?b - ?c)) t_t)" then ()

else error "matchsub";

"----------- check writeln, tracing for string markup ---";

"----------- check writeln, tracing for string markup ---";

"----------- check writeln, tracing for string markup ---";

 val t = @{term "x + 1"};

 val str_markup = (Syntax.string_of_term

       (Proof_Context.init_global (ThyC.get_theory "Isac_Knowledge"))) t;

 val str = UnparseC.term_by_thyID "Isac_Knowledge" t;

 writeln "----------------writeln str_markup---";

 writeln str_markup;

 writeln "----------------writeln str---";

 writeln str;

 writeln "----------------SAME output: no markup----";

 writeln "----------------writeln PolyML.makestring str_markup---";

 writeln (@{make_string} str_markup);

 writeln "----------------writeln PolyML.makestring str---";

 writeln (@{make_string} str);

 writeln "----------------DIFFERENT output----";

 tracing "----------------tracing str_markup---";

 tracing str_markup;

 tracing "----------------tracing str---";

 tracing str;

 tracing "----------------SAME output: no markup----";

 tracing "----------------writeln PolyML.makestring str_markup---";

 tracing (@{make_string} str_markup);

 tracing "----------------writeln PolyML.makestring str---";

 tracing (@{make_string} str);

 tracing "----------------DIFFERENT output----";

(*

 redirect_tracing "../../tmp/";

 tracing "----------------writeln str_markup---";

 tracing str_markup;

 tracing "----------------writeln str---";

 tracing str;

 tracing "----------------DIFFERENT output----";

*)

"----------- check writeln, tracing for string markup ---";

 val t = @{term "x + 1"};

 val str_markup = (Syntax.string_of_term

       (Proof_Context.init_global (ThyC.get_theory "Isac_Knowledge"))) t;

 val str = UnparseC.term_by_thyID "Isac_Knowledge" t;

 writeln "----------------writeln str_markup---";

 writeln str_markup;

 writeln "----------------writeln str---";

 writeln str;

 writeln "----------------SAME output: no markup----";

 writeln "----------------writeln PolyML.makestring str_markup---";

 writeln (@{make_string} str_markup);

 writeln "----------------writeln PolyML.makestring str---";

 writeln (@{make_string} str);

 writeln "----------------DIFFERENT output----";

 tracing "----------------tracing str_markup---";

 tracing str_markup;

 tracing "----------------tracing str---";

 tracing str;

 tracing "----------------SAME output: no markup----";

 tracing "----------------writeln PolyML.makestring str_markup---";

 tracing (@{make_string} str_markup);

 tracing "----------------writeln PolyML.makestring str---";

 tracing (@{make_string} str);

 tracing "----------------DIFFERENT output----";

(*

 redirect_tracing "../../tmp/";

 tracing "----------------writeln str_markup---";

 tracing str_markup;

 tracing "----------------writeln str---";

 tracing str;

 tracing "----------------DIFFERENT output----";

*)

"----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";

"----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";

"----------- fun TermC.is_bdv_subst ------------------------------------------------------------------";

if TermC.is_bdv_subst (TermC.parse_test @{context} "[(''bdv'', v_v)]") then ()

else error "TermC.is_bdv_subst canged 1";

if TermC.is_bdv_subst (TermC.parse_test @{context} "[(''bdv_1'', v_s1),(''bdv_2'', v_s2)]") then ()

else error "TermC.is_bdv_subst canged 2";

"----------- fun str_of_int --------------------------------------------------------------------";

"----------- fun str_of_int --------------------------------------------------------------------";

"----------- fun str_of_int --------------------------------------------------------------------";

if TermC.str_of_int 1 = "1" then () else error "str_of_int 1";

if TermC.str_of_int ~1 = "-1" then () else error "str_of_int -1";

"----------- fun TermC.scala_of_term -----------------------------------------------------------------";

"----------- fun TermC.scala_of_term -----------------------------------------------------------------";

"----------- fun TermC.scala_of_term -----------------------------------------------------------------";

val t = @{term "aaa::real"};

if TermC.scala_of_term t = "Free(\"aaa\", Type(\"Real.real\", List()))"

then () else error "TermC.scala_of_term  aaa::real";

val t = @{term "aaa + bbb"};

if TermC.scala_of_term t = "App(App(Const (\"Groups.plus_class.plus\", Type(\"fun\", List(TFree(\"'a\", List(\"Groups.plus\")), Type(\"fun\", List(TFree(\"'a\", List(\"Groups.plus\")), TFree(\"'a\", List(\"Groups.plus\"))))))), Free(\"aaa\", TFree(\"'a\", List(\"Groups.plus\")))), Free(\"bbb\", TFree(\"'a\", List(\"Groups.plus\"))))"

then () else error "TermC.scala_of_term  aaa + bbb";

"----------- fun TermC.contains_Var ------------------------------------------------------------------";

"----------- fun TermC.contains_Var ------------------------------------------------------------------";

"----------- fun TermC.contains_Var ------------------------------------------------------------------";

val t = TermC.parse_patt @{theory} "?z = 3";

if TermC.contains_Var t = true then () else error "TermC.contains_Var  ?z = 3";

val t = TermC.parse_patt @{theory} "z = 3";

if TermC.contains_Var t = false then () else error "TermC.contains_Var  ?z = 3";

"----------- fun int_opt_of_string, fun is_num -------------------------------------------------";

"----------- fun int_opt_of_string, fun is_num -------------------------------------------------";

"----------- fun int_opt_of_string, fun is_num -------------------------------------------------";

case ThmC_Def.int_opt_of_string "123" of

  SOME 123 => () | _ => raise error "ThmC_Def.int_opt_of_string  123  changed";

case ThmC_Def.int_opt_of_string "(-123)" of

  SOME ~123 => () | _ => raise error "ThmC_Def.int_opt_of_string  (-123)  changed";

case ThmC_Def.int_opt_of_string "#123" of

  NONE => () | _ => raise error "ThmC_Def.int_opt_of_string  #123  changed";

case ThmC_Def.int_opt_of_string "-123" of

  SOME ~123 => () | _ => raise error "ThmC_Def.int_opt_of_string  -123  changed";

val t = TermC.parse_test @{context} "1";

if TermC.is_num t = true then () else error "TermC.is_num   1";

val t = TermC.parse_test @{context} "-1";

if TermC.is_num t = true then () else error "TermC.is_num  -1";

val t = TermC.parse_test @{context} "a123";

if TermC.is_num t = false then () else error "TermC.is_num   a123";

"----------- fun TermC.is_f_x ------------------------------------------------------------------------";

"----------- fun TermC.is_f_x ------------------------------------------------------------------------";

"----------- fun TermC.is_f_x ------------------------------------------------------------------------";

val t = TermC.parse_test @{context} "q_0/2 * L * x";

if TermC.is_f_x t = false then () else error "TermC.is_f_x   q_0/2 * L * x";

val t = TermC.parse_test @{context} "M_b x";

if TermC.is_f_x t = true then () else error "M_b x";

"----------- fun list2isalist, fun isalist2list ------------------------------------------------";

"----------- fun list2isalist, fun isalist2list ------------------------------------------------";

"----------- fun list2isalist, fun isalist2list ------------------------------------------------";

val t = TermC.parse_test @{context} "R=(R::real)";

val T = type_of t;

val ss = TermC.list2isalist T [t,t,t];

if UnparseC.term ss = "[R = R, R = R, R = R]" then () else error "list2isalist 1";

val t = TermC.parse_test @{context} "[a=b,c=d,e=f]";

val il = TermC.isalist2list t;

if UnparseC.terms il = "[\"a = b\", \"c = d\", \"e = f\"]" then () else error "isalist2list 2";

val t = TermC.parse_test @{context} "[a=b,c=d,e=f]";

val il = TermC.isalist2list t;

if UnparseC.terms il = "[\"a = b\", \"c = d\", \"e = f\"]" then () else error "isalist2list 3";

val t = TermC.parse_test @{context} "ss___s::bool list";

(TermC.isalist2list t; error "isalist2list 1") handle TERM ("isalist2list applied to NON-list: ", _) =>();

"----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------";

"----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------";

"----------- fun TermC.strip_imp_prems', fun TermC.ins_concl -----------------------------------------------";

val prop = Thm.prop_of @{thm real_mult_div_cancel2};

UnparseC.term prop = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";

val t as Const (\<^const_name>\<open>Pure.imp\<close>, _) $

      (Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Var (("k", 0), _) $ Const (\<^const_name>\<open>Groups.zero\<close>, _)))) $

      (Const (\<^const_name>\<open>Trueprop\<close>, _) $

        (Const (\<^const_name>\<open>HOL.eq\<close>, _) $

          (Const (\<^const_name>\<open>divide\<close>, _) $ (Const (\<^const_name>\<open>times\<close>, _) $ Var (("m", 0), _) $ Var (("k", 0), _)) $

            (Const (\<^const_name>\<open>times\<close>, _) $ Var (("n", 0), _) $ Var (("k", 0), _))) $

          (Const (\<^const_name>\<open>divide\<close>, _) $ Var (("m", 0), _) $ Var (("n", 0), _)))) = prop;

val SOME t' = TermC.strip_imp_prems' t;

if  UnparseC.term t' = "(\<Longrightarrow>) (?k \<noteq> 0)" then () else error "TermC.strip_imp_prems' changed";

val thm = @{thm frac_sym_conv};

val prop = Thm.prop_of thm;

val concl = Logic.strip_imp_concl prop;

val SOME prems = TermC.strip_imp_prems' prop;

val prop' = TermC.ins_concl prems concl;

if prop = prop' then () else error "TermC.ins_concl o strip_imp_concl";

"----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";

"----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";

"----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";

val T =  type_of (TermC.parseNEW' ctxt "12::real");

val t = TermC.mk_factroot "SqRoot.sqrt" T 2 3;

if UnparseC.term t = "2 * ??.SqRoot.sqrt 3" then () else error "mk_factroot";

val t = TermC.parse_test @{context} "aaa + bbb";

val op_ as Const (\<^const_name>\<open>plus\<close>, Top) $ Free ("aaa", T1) $ Free ("bbb", T2) = t;

val t' = TermC.mk_num_op_num T1 T2 (\<^const_name>\<open>plus\<close>, Top) 2 3;

if UnparseC.term t' = "2 + 3" then () else error "mk_num_op_num";

"----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";

"----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";

"----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";

val t = TermC.parseNEW' ctxt "(3::real) ^ 4";

val hT = type_of (head_of t);

if (HOLogic.realT, HOLogic.natT, HOLogic.realT) = TermC.dest_binop_typ hT

then () else error "TermC.dest_binop_typ";

"----------- fun TermC.is_list -----------------------------------------------------------------------";

"----------- fun TermC.is_list -----------------------------------------------------------------------";

"----------- fun TermC.is_list -----------------------------------------------------------------------";

val (SOME ct) = TermC.parseNEW ctxt "lll::real list";

val t = TermC.parse_test @{context} "lll::real list";

val ty = Term.type_of ct;

if TermC.is_list t = false then () else error "TermC.is_list   lll::real list";

val t = TermC.parse_test @{context} "[a, b, c]";

val ty = Term.type_of ct;

if TermC.is_list t = true then () else error "TermC.is_list  [a, b, c]";

"----------- fun mk_frac, proper term with uminus ----------------------------------------------";

"----------- fun mk_frac, proper term with uminus ----------------------------------------------";

"----------- fun mk_frac, proper term with uminus ----------------------------------------------";

     TermC.mk_frac: typ -> int * (int * int) -> term;

     TermC.mk_frac HOLogic.realT (~1, (6, 8));

"~~~~~ fun mk_frac , args:"; val (T, (sg, (i1, i2))) = (HOLogic.realT, (~1, (6, 8)));

val xxx = (*return value*) Const (\<^const_name>\<open>divide\<close>, T --> T) $

      mk_negative T (HOLogic.mk_number T i1) $ HOLogic.mk_number T i2;

val (T_div, T_uminus) =

case xxx of

  Const (\<^const_name>\<open>divide\<close>, T_div) $                                  (* divide *)

    (Const (\<^const_name>\<open>uminus\<close>, T_uminus) $                           (* uminus *)

      (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ _ ))) $

    (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ _ )) 

    => (T_div, T_uminus)

| _ => error "mk_frac 6 / - 8 \<longrightarrow> - 3 / 4 CHANGED";

case T_div of

  Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>real\<close>, []), Type (\<^type_name>\<open>real\<close>, [])]) => ()

| _ => error "T_div CHANGED in fun mk_frac";

case T_uminus of

  Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>real\<close>, []), Type (\<^type_name>\<open>real\<close>, [])]) => ()

| _ => error "T_uminus CHANGED in fun mk_frac";

(* IMproper term for "6 / - 8 = - 3 / (4::real)"

  (Const (\<^const_name>\<open>uminus\<close>, _) $                                    (* uminus *)

    (Const (\<^const_name>\<open>divide\<close>, _) $                                   (* divide *)

      (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ _ ))) $

      (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ _ ) ))))

*)