1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/smltest/Scripts/term_G.sml	Mon Dec 10 11:09:26 2007 +0100
     1.3 @@ -0,0 +1,82 @@
     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 +"table of contents -----------------------------------------------";
    1.14 +"-----------------------------------------------------------------";
    1.15 +"----------- inst_bdv --------------------------------------------";
    1.16 +"----------- subst_atomic_all ------------------------------------";
    1.17 +"----------- Pattern.match ---------------------------------------";
    1.18 +"-----------------------------------------------------------------";
    1.19 +"-----------------------------------------------------------------";
    1.20 +"-----------------------------------------------------------------";
    1.21 +
    1.22 +
    1.23 +"----------- inst_bdv --------------------------------------------";
    1.24 +"----------- inst_bdv --------------------------------------------";
    1.25 +"----------- inst_bdv --------------------------------------------";
    1.26 +if string_of_thm (num_str d1_isolate_add2) = 
    1.27 +    "\"~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)\"" then ()
    1.28 +else raise error "term_G.sml d1_isolate_add2";
    1.29 +val subst = [(str2term "bdv", str2term "x")];
    1.30 +val t = (norm o #prop o rep_thm) (num_str d1_isolate_add2);
    1.31 +val t' = inst_bdv subst t;
    1.32 +if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
    1.33 +else raise error "term_G.sml inst_bdv 1";
    1.34 +
    1.35 +if string_of_thm (num_str separate_bdvs_add) = 
    1.36 +   "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
    1.37 +   \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
    1.38 +else raise error "term_G.sml separate_bdvs_add";
    1.39 +val subst = [(str2term"bdv_1",str2term"c"),
    1.40 +	    (str2term"bdv_2",str2term"c_2"),
    1.41 +	    (str2term"bdv_3",str2term"c_3"),
    1.42 +	    (str2term"bdv_4",str2term"c_4")];
    1.43 +val t = (norm o #prop o rep_thm) (num_str separate_bdvs_add);
    1.44 +val t' = inst_bdv subst t;
    1.45 +if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
    1.46 +		 \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
    1.47 +else raise error "term_G.sml inst_bdv 2";
    1.48 +
    1.49 +
    1.50 +"----------- subst_atomic_all ------------------------------------";
    1.51 +"----------- subst_atomic_all ------------------------------------";
    1.52 +"----------- subst_atomic_all ------------------------------------";
    1.53 +val t = str2term"(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";
    1.54 +val env = [(str2term"vs_::real list",str2term"[c, c_2]"),
    1.55 +	   (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")];
    1.56 +val (all_Free_subst, t') = subst_atomic_all env t;
    1.57 +if all_Free_subst andalso 
    1.58 +   term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
    1.59 +else raise error "term_G.sml subst_atomic_all should be 'true'";
    1.60 +
    1.61 +
    1.62 +val (all_Free_subst, t') = subst_atomic_all (tl env) t;
    1.63 +if not all_Free_subst andalso 
    1.64 +   term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
    1.65 +else raise error "term_G.sml subst_atomic_all should be 'false'";
    1.66 +
    1.67 +
    1.68 +"----------- Pattern.match ---------------------------------------";
    1.69 +"----------- Pattern.match ---------------------------------------";
    1.70 +"----------- Pattern.match ---------------------------------------";
    1.71 +val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
    1.72 +val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
    1.73 +(*        !^^^^^^^^!... necessary for Pattern.match*)
    1.74 +val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
    1.75 +(*val insts =
    1.76 +  ([],
    1.77 +   [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
    1.78 +    (("a",0),Free ("3","RealDef.real"))])
    1.79 +  : (indexname * typ) list * (indexname * term) list*)
    1.80 +
    1.81 +"----- throws exn MATCH...";
    1.82 +val t = str2term "x";
    1.83 +(Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)) 
    1.84 +handle MATCH => ([(* (Term.indexname * Term.typ) *)],
    1.85 +		 [(* (Term.indexname * Term.term) *)]);