(* 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 matches --------------------------------";

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

"----------- uminus_to_string ---------------------------";

"----------- *** prep_pbt: syntax error in '#Where' of [v";

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

"-------- build fun is_bdv_subst ---------------------------------";

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

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

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

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

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

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

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

@{term "0::nat"};

(*Const ("Groups.zero_class.zero", "Nat.nat")*)

@{term "1::nat"};

(*Const ("Groups.one_class.one", "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 ("Groups.zero_class.zero", "Int.int")*)

@{term "1::int"};

(*Const ("Groups.one_class.one", "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 ("Groups.uminus_class.uminus", "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 ("Groups.zero_class.zero", "RealDef.real")*)

@{term "1::real"};

(**)

@{term "5::real"};

(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> RealDef.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> RealDef.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 ("Groups.uminus_class.uminus", "RealDef.real \<Rightarrow> RealDef.real") $

     (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> RealDef.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 ("Groups.zero_class.zero", "nat")*)

@{term "1::nat"};

(*Const ("Groups.one_class.one", "nat")*)

@{term "5::nat"};

(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> nat") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

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

@{term "0::int"};

(*Const ("Groups.zero_class.zero", "int")*)

@{term "1::int"};

(*Const ("Groups.one_class.one", "int")*)

@{term "5::int"};

(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

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

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

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

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

(*Const ("Groups.uminus_class.uminus", "int \<Rightarrow> int") $

     (Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $

       (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

         (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)

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

@{term "0::real"};

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

@{term "1::real"};

(*Const ("Groups.one_class.one", "real")*)

@{term "5::real"};

(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

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

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

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

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

(*Const ("Groups.uminus_class.uminus", "real \<Rightarrow> real") $

     (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $

       (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

         (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)

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

@{term "0::nat"};

(*Const ("Groups.zero_class.zero", "nat")*)

@{term "1::nat"};

(*Const ("Groups.one_class.one", "nat")*)

@{term "5::nat"};

(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> nat") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

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

@{term "0::int"};

(*Const ("Groups.zero_class.zero", "int")*)

@{term "1::int"};

(*Const ("Groups.one_class.one", "int")*)

@{term "5::int"};

(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

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

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

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

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

(*Const ("Groups.uminus_class.uminus", "int \<Rightarrow> int") $

     (Const ("Num.numeral_class.numeral", "num \<Rightarrow> int") $

       (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

         (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)

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

@{term "0::real"};

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

@{term "1::real"};

(*Const ("Groups.one_class.one", "real")*)

@{term "5::real"};

(*Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

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

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

     (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

       (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))*)

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

(*Const ("Groups.uminus_class.uminus", "real \<Rightarrow> real") $

     (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $

       (Const ("Num.num.Bit1", "num \<Rightarrow> num") $

         (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("...", "num"))))*)

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

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

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

 if (term2str o prop_of o num_str) @{thm d1_isolate_add2} = 

     "~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)" 

   then ()

   else error "termC.sml d1_isolate_add2";

 val subst = [(str2term "bdv", str2term "x")];

 val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});

 val t' = inst_bdv subst t;

 if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" 

   then ()

   else error "termC.sml inst_bdv 1";

if (term2str o prop_of o num_str) @{thm separate_bdvs_add} = 

  "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n==>" ^

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

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

print_depth 5; 

val subst = 

  [(str2term "bdv_1", str2term "c"),

 	   (str2term "bdv_2", str2term "c_2"),

 	   (str2term "bdv_3", str2term "c_3"),

 	   (str2term "bdv_4", str2term "c_4")];

val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});

val t' = inst_bdv subst t;

if term2str t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a\n\

 		 \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" 

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

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

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

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

 val t = str2term "(tl vs_vs) from vs_vs occur_exactly_in (NTH 1 (es_es::bool list))";

 val env = [(str2term "vs_vs::real list", str2term "[c, c_2]"),

 	   (str2term "es_es::bool list", str2term "[c_2 = 0, c + c_2 = 1]")];

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

 if all_Free_subst andalso 

    term2str 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') = subst_atomic_all (tl env) t;

 if not all_Free_subst andalso 

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

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

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

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

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

 val t = (term_of o the o (parse thy)) "3 * x^^^2 = (1::real)";

 val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = (c::real)";

 (*        !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*)

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

print_depth 3; (*999*) insts; 

 (*val insts =

   ({}, 

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

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

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

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

(* val t = str2term "x";

 (Pattern.match @{theory "Isac"} (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 matches --------------------------------";

"----------- fun matches --------------------------------";

"----------- fun matches --------------------------------";

 (*examples see

   test/../Knowledge/polyeq.sml:     

   Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)

 (*test/../Interpret/ptyps.sml:        

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

  val thy = @{theory "Complex_Main"}; 

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

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

 tracing "paIsa=..."; 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 matches thy tm pa then () 

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

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

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

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

  else ();

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

 val pa = Logic.varify_global (str2term "a = (0::real)");(*<<<<<<<-------------*)

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

(*** 

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

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

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

***)

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

 val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)

 if matches thy tm pa then () 

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

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

 val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)";     (*<<<<<<<-------------*)

 if matches thy tm pa then () 

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

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

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

  else ();*)

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

 val pa = free2var (str2term "a = (0::real)");(*<<<<<<<-------------*)

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

(*** 

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

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

*** . Free (0, real)

***)

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

 val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)";     (*<<<<<<<-------------*)

 if matches thy tm pa then () 

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

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

 val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)";     (*<<<<<<<-------------*)

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

   else ();

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

 val pa = free2var (str2term "M_b 0");

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

 val tm = str2term "M_b 0";

 if matches thy tm pa then () 

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

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

 val tm = str2term "M_b x";

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

   else ();

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

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

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

 val thy = @{theory "Complex_Main"};

 val str = "x + z";

 parse thy str;

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

 val str = "x + 2*z";

 val t = (Syntax.read_term_global thy str);

 val t = numbers_to_string (Syntax.read_term_global thy str);

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

 cterm_of thy t;

 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";

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

 val thy = @{theory "Poly"};

 parse_patt thy "?p is_addUnordered";

 parse_patt thy "?p :: real";

 val str = "x + z";

 parse thy str;

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

 val str = "x + 2*z";

 val t = (Syntax.read_term_global thy str);

 val t = numbers_to_string (Syntax.read_term_global thy str);

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

 cterm_of thy t;

 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";

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

 val thy = @{theory "Poly"};

 parse_patt thy "?p is_addUnordered";

 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 *)

"----------- uminus_to_string ---------------------------";

"----------- uminus_to_string ---------------------------";

"----------- uminus_to_string ---------------------------";

 val t1 = numbers_to_string @{term "-2::real"};

 val t2 = numbers_to_string @{term "- 2::real"};

 if uminus_to_string t2 = t1 

   then ()

   else error "termC.sml diff.behav. in uminus_to_string";

"----------- *** prep_pbt: syntax error in '#Where' of [v";

"----------- *** prep_pbt: syntax error in '#Where' of [v";

"----------- *** prep_pbt: syntax error in '#Where' of [v";

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

 val str = "?a";

 val t = (thy, str) |>> thy2ctxt 

                    |-> Proof_Context.read_term_pattern

                    |> numbers_to_string;

 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) |>> thy2ctxt 

                    |-> Proof_Context.read_term_pattern

                    |> numbers_to_string;

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

 val Type (str, tys) = ty;

 if str = "RealDef.real" 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) |>> thy2ctxt 

                    |-> Proof_Context.read_term_pattern

                    |> numbers_to_string;

val t_real = typ_a2real t;

if term_to_string' ctxt t_real =

"~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n   matchsub (?a + (?b - ?c))" ^

" t_t |\n   matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)" then ()

else error "";

"----------- 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 (Thy_Info.get_theory "Isac"))) t;

 val str = term_to_string'' "Isac" 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 (PolyML.makestring str_markup);

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

 writeln (PolyML.makestring 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 (PolyML.makestring str_markup);

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

 tracing (PolyML.makestring 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 (Thy_Info.get_theory "Isac"))) t;

 val str = term_to_string'' "Isac" 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 (PolyML.makestring str_markup);

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

 writeln (PolyML.makestring 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 (PolyML.makestring str_markup);

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

 tracing (PolyML.makestring str);

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

(*

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

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

 tracing str_markup;

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

 tracing str;

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

*)

"-------- build fun is_bdv_subst ---------------------------------";

"-------- build fun is_bdv_subst ---------------------------------";

"-------- build fun is_bdv_subst ---------------------------------";

fun is_bdv_subst (Const ("List.list.Cons", _) $

      (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) = is_bdv str

  | is_bdv_subst _ = false;

if is_bdv_subst (str2term "[(bdv, v_v)]") then ()

else error "is_bdv_subst canged 1";

if is_bdv_subst (str2term "[(bdv_1, v_s1),(bdv_2, v_s2)]") then ()

else error "is_bdv_subst canged 2";