1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/ProgLang/termC.sml Tue Sep 28 07:28:10 2010 +0200
1.3 @@ -0,0 +1,219 @@
1.4 +(* Title: tests on ProgLang/termC.sml
1.5 + Author: Walther Neuper 051006,
1.6 + (c) due to copyright terms
1.7 +*)
1.8 +"--------------------------------------------------------";
1.9 +"table of contents --------------------------------------";
1.10 +"--------------------------------------------------------";
1.11 +"----------- inst_bdv -----------------------------------";
1.12 +"----------- subst_atomic_all ---------------------------";
1.13 +"----------- Pattern.match ------------------------------";
1.14 +"----------- fun matches --------------------------------";
1.15 +"------------parse---------------------------------------";
1.16 +"----------- uminus_to_string ---------------------------";
1.17 +"--------------------------------------------------------";
1.18 +"--------------------------------------------------------";
1.19 +
1.20 +
1.21 +(*===== inhibit exn ============================================================
1.22 +"----------- inst_bdv -----------------------------------";
1.23 +"----------- inst_bdv -----------------------------------";
1.24 +"----------- inst_bdv -----------------------------------";
1.25 +if (term2str o prop_of o num_str) @{thm d1_isolate_add2} =
1.26 + "~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)" then ()
1.27 +else raise error "termC.sml d1_isolate_add2";
1.28 +val subst = [(str2term "bdv", str2term "x")];
1.29 +val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
1.30 +val t' = inst_bdv subst t;
1.31 +if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
1.32 +else raise error "termC.sml inst_bdv 1";
1.33 +
1.34 +if string_of_thm (num_str @{thm separate_bdvs_add}) =
1.35 + "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
1.36 + \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
1.37 +else raise error "termC.sml separate_bdvs_add";
1.38 +val subst = [(str2term"bdv_1",str2term"c"),
1.39 + (str2term"bdv_2",str2term"c_2"),
1.40 + (str2term"bdv_3",str2term"c_3"),
1.41 + (str2term"bdv_4",str2term"c_4")];
1.42 +val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});
1.43 +val t' = inst_bdv subst t;
1.44 +if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
1.45 + \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
1.46 +else raise error "termC.sml inst_bdv 2";
1.47 +
1.48 +
1.49 +"----------- subst_atomic_all ---------------------------";
1.50 +"----------- subst_atomic_all ---------------------------";
1.51 +"----------- subst_atomic_all ---------------------------";
1.52 +val t = str2term "(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";
1.53 +val env = [(str2term"vs_::real list",str2term"[c, c_2]"),
1.54 + (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")];
1.55 +val (all_Free_subst, t') = subst_atomic_all env t;
1.56 +if all_Free_subst andalso
1.57 + term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
1.58 +else raise error "termC.sml subst_atomic_all should be 'true'";
1.59 +
1.60 +
1.61 +val (all_Free_subst, t') = subst_atomic_all (tl env) t;
1.62 +if not all_Free_subst andalso
1.63 + term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
1.64 +else raise error "termC.sml subst_atomic_all should be 'false'";
1.65 +===== inhibit exn ============================================================*)
1.66 +
1.67 +
1.68 +"----------- Pattern.match ------------------------------";
1.69 +"----------- Pattern.match ------------------------------";
1.70 +"----------- Pattern.match ------------------------------";
1.71 +(*===== inhibit exn ============================================================
1.72 +val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
1.73 +val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
1.74 +(* !^^^^^^^^!... necessary for Pattern.match*)
1.75 +val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
1.76 +(*val insts =
1.77 + ([],
1.78 + [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
1.79 + (("a",0),Free ("3","RealDef.real"))])
1.80 + : (indexname * typ) list * (indexname * term) list*)
1.81 +
1.82 +"----- throws exn MATCH...";
1.83 +val t = str2term "x";
1.84 +(Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))
1.85 +handle MATCH => ([(* (Term.indexname * Term.typ) *)],
1.86 + [(* (Term.indexname * Term.term) *)]);
1.87 +Pattern.MATCH;
1.88 +
1.89 +val thy = @{theory "Complex_Main"};
1.90 +val PARSE = Syntax.read_term_global thy;
1.91 +val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real");
1.92 +"-------";
1.93 +val (tye, tme) =
1.94 + (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
1.95 +"-------";
1.96 +val (tye, tme) = Pattern.match thy (Logic.varify_global pa, tm) (Vartab.empty,
1.97 + Vartab.empty);
1.98 +"-------";
1.99 +val (tyenv, tenv) = Pattern.match thy (Logic.varify_global pa, tm)
1.100 + (Vartab.empty, Vartab.empty);
1.101 +Vartab.dest tenv;
1.102 +match thy tm (Logic.varify pa);
1.103 +===== inhibit exn ============================================================*)
1.104 +
1.105 +"----------- fun matches --------------------------------";
1.106 +"----------- fun matches --------------------------------";
1.107 +"----------- fun matches --------------------------------";
1.108 +(*test/../Knowledge/polyeq.sml:
1.109 + Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
1.110 +(*test/../Interpret/ptyps.sml:
1.111 + |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
1.112 +val thy = @{theory "Complex_Main"};
1.113 +
1.114 +"----- test 1: OK";
1.115 +val pa = Logic.varify_global @{term "a = (0::real)"}; (*<<<<<<<---------------*)
1.116 +tracing "paIsa=..."; atomty pa; tracing "...=paIsa";
1.117 +(***
1.118 +*** Const (op =, real => real => bool)
1.119 +*** . Var ((a, 0), real)
1.120 +*** . Const (Groups.zero_class.zero, real)
1.121 +***)
1.122 +"----- test 1a true";
1.123 +val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"}; (*<<<<<<<---------------*)
1.124 +if matches thy tm pa then ()
1.125 + else error "termC.sml diff.behav. in matches true 1";
1.126 +"----- test 1b false";
1.127 +val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"}; (*<<<<<<<---------------*)
1.128 +if matches thy tm pa then error "termC.sml diff.behav. in matches false 1"
1.129 + else ();
1.130 +
1.131 +"----- test 2: Nok";
1.132 +val pa = Logic.varify_global (str2term "a = (0::real)");(*<<<<<<<-------------*)
1.133 +tracing "paLo2=..."; atomty pa; tracing "...=paLo2";
1.134 +(***
1.135 +*** Const (op =, real => real => bool)
1.136 +*** . Var ((a, 0), real)
1.137 +*** . Var ((0, 0), real)
1.138 +***)
1.139 +"----- test 2a true";
1.140 +val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
1.141 +if matches thy tm pa then ()
1.142 + else error "termC.sml diff.behav. in matches true 2";
1.143 +"----- test 2b false";
1.144 +val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
1.145 +if matches thy tm pa then ()
1.146 + else error "termC.sml diff.behav. in matches false 2";
1.147 +(* i.e. !!!!!!!!!!!!!!!!! THIS KIND OF PATTERN IS NOT RELIABLE !!!!!!!!!!!!!!!!!
1.148 +if matches thy tm pa then error "termC.sml diff.behav. in matches false 2"
1.149 + else ();*)
1.150 +
1.151 +"----- test 3: OK";
1.152 +val pa = free2var (str2term "a = (0::real)");(*<<<<<<<-------------*)
1.153 +tracing "paF2=..."; atomty pa; tracing "...=paF2";
1.154 +(***
1.155 +*** Const (op =, real => real => bool)
1.156 +*** . Var ((a, 0), real)
1.157 +*** . Free (0, real)
1.158 +***)
1.159 +"----- test 3a true";
1.160 +val tm = str2term "-8 - 2 * x + x ^ 2 = (0::real)"; (*<<<<<<<-------------*)
1.161 +if matches thy tm pa then ()
1.162 + else error "termC.sml diff.behav. in matches true 3";
1.163 +"----- test 3b false";
1.164 +val tm = str2term "-8 - 2 * x + x ^ 2 = (3::real)"; (*<<<<<<<-------------*)
1.165 +if matches thy tm pa then error "termC.sml diff.behav. in matches false 3"
1.166 + else ();
1.167 +
1.168 +"----- test 4=3 with specific data";
1.169 +val pa = free2var (str2term "M_b 0");
1.170 +"----- test 4a true";
1.171 +val tm = str2term "M_b 0";
1.172 +if matches thy tm pa then ()
1.173 + else error "termC.sml diff.behav. in matches true 4";
1.174 +"----- test 4b false";
1.175 +val tm = str2term "M_b x";
1.176 +if matches thy tm pa then error "termC.sml diff.behav. in matches false 4"
1.177 + else ();
1.178 +
1.179 +
1.180 +"------------parse---------------------------------------";
1.181 +"------------parse---------------------------------------";
1.182 +"------------parse---------------------------------------";
1.183 +Toplevel.debug := true;
1.184 +(* literal types:
1.185 +PolyML.addPrettyPrinter
1.186 + (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
1.187 +*)(* pretty types:
1.188 +PolyML.addPrettyPrinter
1.189 + (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
1.190 +print_depth 99;
1.191 +*)
1.192 +val thy = @{theory "Complex_Main"};
1.193 +val str = "x + z";
1.194 +parse thy str;
1.195 +"---------------";
1.196 +val str = "x + 2*z";
1.197 +val t = (Syntax.read_term_global thy str);
1.198 +val t = numbers_to_string (Syntax.read_term_global thy str);
1.199 +val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
1.200 +cterm_of thy t;
1.201 +val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";
1.202 +
1.203 +(*Makarius.1003
1.204 +ML {* @{term "2::int"} *}
1.205 +
1.206 +term "(1.24444) :: real"
1.207 +
1.208 +ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *}
1.209 +*)
1.210 +
1.211 +
1.212 +"----------- uminus_to_string ---------------------------";
1.213 +"----------- uminus_to_string ---------------------------";
1.214 +"----------- uminus_to_string ---------------------------";
1.215 +val t1 = numbers_to_string @{term "-2::real"};
1.216 +val t2 = numbers_to_string @{term "- 2::real"};
1.217 +if uminus_to_string t2 = t1 then ()
1.218 +else error "termC.sml diff.behav. in uminus_to_string";
1.219 +
1.220 +
1.221 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.
1.222 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.*)