(* tests on Scripts/term_G.sml

    author: Walther Neuper

    051006,

    (c) due to copyright terms

 use"../smltest/Scripts/term_G.sml";

 use"term_G.sml";

 *)

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

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

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

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

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

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

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

 "------------parse------------------------------------------------";

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

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

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

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

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

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

 if string_of_thm (num_str @{thm d1_isolate_add2}) = 

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

 else raise error "term_G.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 raise error "term_G.sml inst_bdv 1";

 if string_of_thm (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 raise error "term_G.sml separate_bdvs_add";

 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 raise error "term_G.sml inst_bdv 2";

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

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

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

 val t = str2term"(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";

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

 	   (str2term"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 raise error "term_G.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_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()

 else raise error "term_G.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";

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

 (*        !^^^^^^^^!... necessary for Pattern.match*)

 val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);

 (*val insts =

   ([],

    [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),

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

   : (indexname * typ) list * (indexname * term) list*)

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

 val t = str2term "x";

 (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)) 

 handle MATCH => ([(* (Term.indexname * Term.typ) *)],

 		 [(* (Term.indexname * Term.term) *)]);

 Pattern.MATCH;

 (*ML {**)

 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 (tye, tme) = Pattern.match thy (Logic.varify pa, tm) (Vartab.empty, 

 							  Vartab.empty);

 "-------";

 val (tyenv, tenv) = Pattern.match thy (Logic.varify pa, tm)

 				  (Vartab.empty, Vartab.empty);

 Vartab.dest tenv;

 match thy tm (Logic.varify pa);

 (**}*)

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

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

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

 (*smltest/IsacKnowledge/polyeq.sml:     

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

 (*smltest/ME/ptyps.sml:        

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

 (*ML {**) 

 val thy = @{theory "Complex_Main"};

 "----- test 1";

 val pa = Logic.varify @{term "a = (0::real)"};

 "----- test 1 true";

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

 if matches thy tm pa then () 

   else error "term_G.sml diff.behav. in matches true";

 "----- test 2 false";

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

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

   else ();

 (**}*)

 "------------parse------------------------------------------------";

 "------------parse------------------------------------------------";

 "------------parse------------------------------------------------";

 (*ML {**)

 Toplevel.debug := true;

 (* literal types:

 PolyML.addPrettyPrinter

   (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);

 *)(* pretty types:

 PolyML.addPrettyPrinter

   (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);

 print_depth 99;

 *)

 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 "term_G.sml parsing 'x + 2*z' failed";

 (**}*)

 (*Makarius.1003

 ML {* @{term "2::int"} *}

 term "(1.24444) :: real"

 ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *}

 *)

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

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

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

 (*ML {*)

 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 "term_G.sml diff.behav. in uminus_to_string";

 (*}*)