wneuper/isa: src/Pure/isac/smltest/Scripts/term

     1 (* tests on Scripts/term_G.sml

     2    author: Walther Neuper

     3    051006,

     4    (c) due to copyright terms

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

     7 use"term_G.sml";

     8 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    26 if string_of_thm (num_str d1_isolate_add2) =

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

    28 else raise error "term_G.sml d1_isolate_add2";

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

    30 val t = (norm o #prop o rep_thm) (num_str d1_isolate_add2);

    31 val t' = inst_bdv subst t;

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

    33 else raise error "term_G.sml inst_bdv 1";

    35 if string_of_thm (num_str separate_bdvs_add) =

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

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

    38 else raise error "term_G.sml separate_bdvs_add";

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

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

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

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

    43 val t = (norm o #prop o rep_thm) (num_str separate_bdvs_add);

    44 val t' = inst_bdv subst t;

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

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

    47 else raise error "term_G.sml inst_bdv 2";

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

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

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

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

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

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

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

    57 if all_Free_subst andalso

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

    59 else raise error "term_G.sml subst_atomic_all should be 'true'";

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

    63 if not all_Free_subst andalso

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

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

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

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

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

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

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

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

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

    75 (*val insts =

    76   ([],

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

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

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

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

    82 val t = str2term "x";

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

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

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

    86 Pattern.MATCH;

    88 (*ML {**)

    89 val thy = @{theory Complex_Main};

    90 val PARSE = Syntax.read_term_global thy;

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

    92 "-------";

    93 val (tye, tme) =

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

    95 "-------";

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

    97 							  Vartab.empty);

    98 "-------";

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

   100 				  (Vartab.empty, Vartab.empty);

   101 Vartab.dest tenv;

   102 match thy tm (Logic.varify pa);

   104 (**}*)

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

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

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

   109 (*smltest/IsacKnowledge/polyeq.sml:

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

   111 (*smltest/ME/ptyps.sml:

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

   113 (*ML {**)

   114 val thy = @{theory Complex_Main};

   115 "----- test 1";

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

   117 "----- test 1 true";

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

   119 if matches thy tm pa then ()

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

   121 "----- test 2 false";

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

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

   124   else ();

   125 (**}*)

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

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

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

   130 (*ML {**)

   131 Toplevel.debug := true;

   132 (* literal types:

   133 PolyML.addPrettyPrinter

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

   135 *)(* pretty types:

   136 PolyML.addPrettyPrinter

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

   138 print_depth 99;

   139 *)

   140 val thy = @{theory Complex_Main};

   141 val str = "x + z";

   142 parse thy str;

   143 "---------------";

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

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

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

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

   148 cterm_of thy t;

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

   150 (**}*)

   151 (*Makarius.1003

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

   154 term "(1.24444) :: real"

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

   157 *)

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

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

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

   163 (*ML {*)

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

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

   166 if uminus_to_string t2 = t1 then ()

   167 else error "term_G.sml diff.behav. in uminus_to_string";

   168 (*}*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 21 Jul 2010 13:53:39 +0200
branch	isac-from-Isabelle2009-2
changeset 37871	875b6efa7ced
permissions	-rw-r--r--