1.1 --- a/test/Tools/isac/ProgLang/term_G.sml Mon Sep 13 18:37:16 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,168 +0,0 @@
1.4 -(* tests on Scripts/term_G.sml
1.5 - author: Walther Neuper
1.6 - 051006,
1.7 - (c) due to copyright terms
1.8 -
1.9 -use"../smltest/Scripts/term_G.sml";
1.10 -use"term_G.sml";
1.11 -*)
1.12 -
1.13 -"-----------------------------------------------------------------";
1.14 -"table of contents -----------------------------------------------";
1.15 -"-----------------------------------------------------------------";
1.16 -"----------- inst_bdv --------------------------------------------";
1.17 -"----------- subst_atomic_all ------------------------------------";
1.18 -"----------- Pattern.match ---------------------------------------";
1.19 -"----------- fun matches -----------------------------------------";
1.20 -"------------parse------------------------------------------------";
1.21 -"----------- uminus_to_string ------------------------------------";
1.22 -"-----------------------------------------------------------------";
1.23 -"-----------------------------------------------------------------";
1.24 -
1.25 -
1.26 -"----------- inst_bdv --------------------------------------------";
1.27 -"----------- inst_bdv --------------------------------------------";
1.28 -"----------- inst_bdv --------------------------------------------";
1.29 -if string_of_thm (num_str @{thm d1_isolate_add2}) =
1.30 - "\"~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)\"" then ()
1.31 -else raise error "term_G.sml d1_isolate_add2";
1.32 -val subst = [(str2term "bdv", str2term "x")];
1.33 -val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
1.34 -val t' = inst_bdv subst t;
1.35 -if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
1.36 -else raise error "term_G.sml inst_bdv 1";
1.37 -
1.38 -if string_of_thm (num_str @{thm separate_bdvs_add}) =
1.39 - "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
1.40 - \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
1.41 -else raise error "term_G.sml separate_bdvs_add";
1.42 -val subst = [(str2term"bdv_1",str2term"c"),
1.43 - (str2term"bdv_2",str2term"c_2"),
1.44 - (str2term"bdv_3",str2term"c_3"),
1.45 - (str2term"bdv_4",str2term"c_4")];
1.46 -val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});
1.47 -val t' = inst_bdv subst t;
1.48 -if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
1.49 - \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
1.50 -else raise error "term_G.sml inst_bdv 2";
1.51 -
1.52 -
1.53 -"----------- subst_atomic_all ------------------------------------";
1.54 -"----------- subst_atomic_all ------------------------------------";
1.55 -"----------- subst_atomic_all ------------------------------------";
1.56 -val t = str2term"(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";
1.57 -val env = [(str2term"vs_::real list",str2term"[c, c_2]"),
1.58 - (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")];
1.59 -val (all_Free_subst, t') = subst_atomic_all env t;
1.60 -if all_Free_subst andalso
1.61 - term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
1.62 -else raise error "term_G.sml subst_atomic_all should be 'true'";
1.63 -
1.64 -
1.65 -val (all_Free_subst, t') = subst_atomic_all (tl env) t;
1.66 -if not all_Free_subst andalso
1.67 - term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
1.68 -else raise error "term_G.sml subst_atomic_all should be 'false'";
1.69 -
1.70 -
1.71 -"----------- Pattern.match ---------------------------------------";
1.72 -"----------- Pattern.match ---------------------------------------";
1.73 -"----------- Pattern.match ---------------------------------------";
1.74 -val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
1.75 -val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
1.76 -(* !^^^^^^^^!... necessary for Pattern.match*)
1.77 -val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
1.78 -(*val insts =
1.79 - ([],
1.80 - [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
1.81 - (("a",0),Free ("3","RealDef.real"))])
1.82 - : (indexname * typ) list * (indexname * term) list*)
1.83 -
1.84 -"----- throws exn MATCH...";
1.85 -val t = str2term "x";
1.86 -(Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))
1.87 -handle MATCH => ([(* (Term.indexname * Term.typ) *)],
1.88 - [(* (Term.indexname * Term.term) *)]);
1.89 -Pattern.MATCH;
1.90 -
1.91 -(*ML {**)
1.92 -val thy = @{theory "Complex_Main"};
1.93 -val PARSE = Syntax.read_term_global thy;
1.94 -val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real");
1.95 -"-------";
1.96 -val (tye, tme) =
1.97 - (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
1.98 -"-------";
1.99 -val (tye, tme) = Pattern.match thy (Logic.varify pa, tm) (Vartab.empty,
1.100 - Vartab.empty);
1.101 -"-------";
1.102 -val (tyenv, tenv) = Pattern.match thy (Logic.varify pa, tm)
1.103 - (Vartab.empty, Vartab.empty);
1.104 -Vartab.dest tenv;
1.105 -match thy tm (Logic.varify pa);
1.106 -
1.107 -(**}*)
1.108 -
1.109 -"----------- fun matches -----------------------------------------";
1.110 -"----------- fun matches -----------------------------------------";
1.111 -"----------- fun matches -----------------------------------------";
1.112 -(*smltest/IsacKnowledge/polyeq.sml:
1.113 - Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
1.114 -(*smltest/ME/ptyps.sml:
1.115 - |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
1.116 -(*ML {**)
1.117 -val thy = @{theory "Complex_Main"};
1.118 -"----- test 1";
1.119 -val pa = Logic.varify @{term "a = (0::real)"};
1.120 -"----- test 1 true";
1.121 -val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"};
1.122 -if matches thy tm pa then ()
1.123 - else error "term_G.sml diff.behav. in matches true";
1.124 -"----- test 2 false";
1.125 -val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"};
1.126 -if matches thy tm pa then error "term_G.sml diff.behav. in matches false"
1.127 - else ();
1.128 -(**}*)
1.129 -
1.130 -"------------parse------------------------------------------------";
1.131 -"------------parse------------------------------------------------";
1.132 -"------------parse------------------------------------------------";
1.133 -(*ML {**)
1.134 -Toplevel.debug := true;
1.135 -(* literal types:
1.136 -PolyML.addPrettyPrinter
1.137 - (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
1.138 -*)(* pretty types:
1.139 -PolyML.addPrettyPrinter
1.140 - (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
1.141 -print_depth 99;
1.142 -*)
1.143 -val thy = @{theory "Complex_Main"};
1.144 -val str = "x + z";
1.145 -parse thy str;
1.146 -"---------------";
1.147 -val str = "x + 2*z";
1.148 -val t = (Syntax.read_term_global thy str);
1.149 -val t = numbers_to_string (Syntax.read_term_global thy str);
1.150 -val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
1.151 -cterm_of thy t;
1.152 -val t = (the (parse thy str)) handle _ => error "term_G.sml parsing 'x + 2*z' failed";
1.153 -(**}*)
1.154 -(*Makarius.1003
1.155 -ML {* @{term "2::int"} *}
1.156 -
1.157 -term "(1.24444) :: real"
1.158 -
1.159 -ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *}
1.160 -*)
1.161 -
1.162 -
1.163 -"----------- uminus_to_string ------------------------------------";
1.164 -"----------- uminus_to_string ------------------------------------";
1.165 -"----------- uminus_to_string ------------------------------------";
1.166 -(*ML {*)
1.167 -val t1 = numbers_to_string @{term "-2::real"};
1.168 -val t2 = numbers_to_string @{term "- 2::real"};
1.169 -if uminus_to_string t2 = t1 then ()
1.170 -else error "term_G.sml diff.behav. in uminus_to_string";
1.171 -(*}*)