(* Title: tests on ProgLang/termC.sml

   Author: Walther Neuper 051006,

   (c) due to copyright terms

*)

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

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

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

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

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

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

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

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

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

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

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

(*===== inhibit exn ============================================================

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

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

===== inhibit exn ============================================================*)

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

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

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

(*===== inhibit exn ============================================================

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;

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_global pa, tm) (Vartab.empty, 

							  Vartab.empty);

"-------";

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

				  (Vartab.empty, Vartab.empty);

Vartab.dest tenv;

match thy tm (Logic.varify pa);

===== inhibit exn ============================================================*)

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

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

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

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

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

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

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

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 "termC.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 ---------------------------";

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";

(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.

-.-.-.-.-.-.-isolate response.-.-.-.-.-.*)