wneuper/isa: test/Tools/isac/ProgLang/termC.sml@67a110289e4e

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

     2    Author: Walther Neuper 051006,

     3    (c) due to copyright terms

     4 *)

     5 "--------------------------------------------------------";

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

     7 "--------------------------------------------------------";

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

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

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

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

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

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

    14 "--------------------------------------------------------";

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

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

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

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

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

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

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

    24 else raise error "termC.sml d1_isolate_add2";

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

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

    27 val t' = inst_bdv subst t;

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

    29 else raise error "termC.sml inst_bdv 1";

    31 if string_of_thm (num_str @{thm separate_bdvs_add}) =

    32    "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\

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

    34 else raise error "termC.sml separate_bdvs_add";

    35 val subst = [(str2term"bdv_1",str2term"c"),

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

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

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

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

    40 val t' = inst_bdv subst t;

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

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

    43 else raise error "termC.sml inst_bdv 2";

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

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

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

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

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

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

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

    53 if all_Free_subst andalso

    54    term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()

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

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

    59 if not all_Free_subst andalso

    60    term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()

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

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

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

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

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

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

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

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

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

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

    73 (*val insts =

    74   ([],

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

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

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

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

    80 val t = str2term "x";

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

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

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

    84 Pattern.MATCH;

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

    87 val PARSE = Syntax.read_term_global thy;

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

    89 "-------";

    90 val (tye, tme) =

    91   (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);

    92 "-------";

    93 val (tye, tme) = Pattern.match thy (Logic.varify_global pa, tm) (Vartab.empty,

    94 							  Vartab.empty);

    95 "-------";

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

    97 				  (Vartab.empty, Vartab.empty);

    98 Vartab.dest tenv;

    99 match thy tm (Logic.varify pa);

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

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

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

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

   105 (*test/../Knowledge/polyeq.sml:

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

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

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

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

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

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

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

   114 (***

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

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

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

   118 ***)

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

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

   121 if matches thy tm pa then ()

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

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

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

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

   126   else ();

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

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

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

   131 (***

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

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

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

   135 ***)

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

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

   138 if matches thy tm pa then ()

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

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

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

   142 if matches thy tm pa then ()

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

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

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

   146   else ();*)

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

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

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

   151 (***

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

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

   154 *** . Free (0, real)

   155 ***)

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

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

   158 if matches thy tm pa then ()

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

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

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

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

   163   else ();

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

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

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

   168 val tm = str2term "M_b 0";

   169 if matches thy tm pa then ()

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

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

   172 val tm = str2term "M_b x";

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

   174   else ();

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

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

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

   180 Toplevel.debug := true;

   181 (* literal types:

   182 PolyML.addPrettyPrinter

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

   184 *)(* pretty types:

   185 PolyML.addPrettyPrinter

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

   187 print_depth 99;

   188 *)

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

   190 val str = "x + z";

   191 parse thy str;

   192 "---------------";

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

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

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

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

   197 cterm_of thy t;

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

   200 (*Makarius.1003

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

   203 term "(1.24444) :: real"

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

   206 *)

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

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

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

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

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

   214 if uminus_to_string t2 = t1 then ()

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

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

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

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 28 Sep 2010 07:28:10 +0200
branch	isac-update-Isa09-2
changeset 38025	67a110289e4e
child 38031	460c24a6a6ba
permissions	-rw-r--r--