wneuper/isa: test/Tools/isac/ProgLang/termC.sml@130688f277ba

     1 (* Title: tests on ProgLang/termC.sml

     2    Author: Walther Neuper 051006,

     3    (c) due to copyright terms

     4 *)

     6 "--------------------------------------------------------";

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

     8 "--------------------------------------------------------";

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

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

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

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

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

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

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

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

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

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

    19 "--------------------------------------------------------";

    20 "--------------------------------------------------------";

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

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

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

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

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

    27 @{term "0::nat"};

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

    29 @{term "1::nat"};

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

    31 @{term "5::nat"};

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

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

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

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

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

    37 @{term "0::int"};

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

    39 @{term "1::int"};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    58 @{term "0::real"};

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

    60 @{term "1::real"};

    61 (**)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    79 @{term "0::nat"};

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

    81 @{term "1::nat"};

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

    83 @{term "5::nat"};

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

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

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

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

    88 @{term "0::int"};

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

    90 @{term "1::int"};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   106 @{term "0::real"};

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

   108 @{term "1::real"};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   124 @{term "0::nat"};

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

   126 @{term "1::nat"};

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

   128 @{term "5::nat"};

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

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

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

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

   133 @{term "0::int"};

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

   135 @{term "1::int"};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   151 @{term "0::real"};

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

   153 @{term "1::real"};

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   174    then ()

   175    else error "termC.sml d1_isolate_add2";

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

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

   178  val t' = inst_bdv subst t;

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

   180    then ()

   181    else error "termC.sml inst_bdv 1";

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

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

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

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

   186 print_depth 5;

   188 val subst =

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

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

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

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

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

   194 val t' = inst_bdv subst t;

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

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

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

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

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

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

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

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

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

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

   208  if all_Free_subst andalso

   209     term2str t' = "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1 [c_2 = 0, c + c_2 = 1]"

   210    then ()

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

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

   214  if not all_Free_subst andalso

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

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

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

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

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

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

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

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

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

   225 print_depth 3; (*999*) insts;

   226  (*val insts =

   227    ({},

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

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

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

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

   233 (* val t = str2term "x";

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

   235  handle MATCH => ???; *)

   237  val thy = @{theory "Complex_Main"};

   238  val PARSE = Syntax.read_term_global thy;

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

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

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

   243  Vartab.dest tenv;

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

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

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

   248  (*examples see

   249    test/../Knowledge/polyeq.sml:

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

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

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

   253   val thy = @{theory "Complex_Main"};

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

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

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

   258 (***

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

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

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

   262 ***)

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

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

   265  if matches thy tm pa then ()

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

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

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

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

   270   else ();

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

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

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

   275 (***

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

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

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

   279 ***)

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

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

   282  if matches thy tm pa then ()

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

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

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

   286  if matches thy tm pa then ()

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

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

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

   290   else ();*)

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

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

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

   295 (***

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

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

   298 *** . Free (0, real)

   299 ***)

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

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

   302  if matches thy tm pa then ()

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

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

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

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

   307    else ();

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

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

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

   312  val tm = str2term "M_b 0";

   313  if matches thy tm pa then ()

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

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

   316  val tm = str2term "M_b x";

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

   318    else ();

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

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

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

   324  val thy = @{theory "Complex_Main"};

   325  val str = "x + z";

   326  parse thy str;

   327 "---------------";

   328  val str = "x + 2*z";

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

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

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

   332  cterm_of thy t;

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

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

   336  val thy = @{theory "Poly"};

   337  parse_patt thy "?p is_addUnordered";

   338  parse_patt thy "?p :: real";

   340  val str = "x + z";

   341  parse thy str;

   342 "---------------";

   343  val str = "x + 2*z";

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

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

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

   347  cterm_of thy t;

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

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

   351  val thy = @{theory "Poly"};

   352  parse_patt thy "?p is_addUnordered";

   353  parse_patt thy "?p :: real";

   355 (* Christian Urban, 101001

   356 theory Test

   357 imports Main Complex

   358 begin

   360 let

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

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

   363   |> ML_Syntax.print_term |> ML_Syntax.atomic

   364 in

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

   366 end

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

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

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

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

   373   Envir.subst_term inst precond

   374   |> Syntax.string_of_term @{context}

   375   |> writeln

   378 end *)

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

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

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

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

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

   385  if uminus_to_string t2 = t1

   386    then ()

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

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

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

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

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

   393  val str = "?a";

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

   395                     |-> Proof_Context.read_term_pattern

   396                     |> numbers_to_string;

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

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

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

   400    then ()

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

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

   404  val str = "?a :: real";

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

   406                     |-> Proof_Context.read_term_pattern

   407                     |> numbers_to_string;

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

   409  val Type (str, tys) = ty;

   410  if str = "Real.real" andalso tys = [] andalso ty = HOLogic.realT

   411    then ()

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

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

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

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

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

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

   419 val ctxt = Proof_Context.init_global thy;

   420 val ctxt = Config.put show_types true ctxt;

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

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

   423                     |-> Proof_Context.read_term_pattern

   424                     |> numbers_to_string;

   425 val t_real = typ_a2real t;

   426 if term_to_string' ctxt t_real =

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

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

   429 else error "";

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

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

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

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

   435  val str_markup = (Syntax.string_of_term

   436        (Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;

   437  val str = term_to_string'' "Isac" t;

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

   440  writeln str_markup;

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

   442  writeln str;

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

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

   446  writeln (PolyML.makestring str_markup);

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

   448  writeln (PolyML.makestring str);

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

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

   452  tracing str_markup;

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

   454  tracing str;

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

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

   458  tracing (PolyML.makestring str_markup);

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

   460  tracing (PolyML.makestring str);

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

   462 (*

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

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

   465  tracing str_markup;

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

   467  tracing str;

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

   469 *)

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

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

   473  val str_markup = (Syntax.string_of_term

   474        (Proof_Context.init_global (Thy_Info.get_theory "Isac"))) t;

   475  val str = term_to_string'' "Isac" t;

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

   478  writeln str_markup;

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

   480  writeln str;

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

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

   484  writeln (PolyML.makestring str_markup);

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

   486  writeln (PolyML.makestring str);

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

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

   490  tracing str_markup;

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

   492  tracing str;

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

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

   496  tracing (PolyML.makestring str_markup);

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

   498  tracing (PolyML.makestring str);

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

   500 (*

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

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

   503  tracing str_markup;

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

   505  tracing str;

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

   507 *)

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

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

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

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

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

   514   | is_bdv_subst _ = false;

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

   517 else error "is_bdv_subst canged 1";

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

   520 else error "is_bdv_subst canged 2";

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 21 Nov 2013 18:12:17 +0100
changeset 55279	130688f277ba
parent 52101	c3f399ce32af
child 59111	c730b643bc0e
permissions	-rw-r--r--