1.1 --- a/test/Tools/isac/Interpret/inform.sml	Mon May 14 14:47:45 2012 +0200
     1.2 +++ b/test/Tools/isac/Interpret/inform.sml	Wed May 16 08:59:09 2012 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4  "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
     1.5  "--------- Take as 1st tac, start from exp -----------------------";
     1.6  "--------- init_form, start with <NEW> (CAS input) ---------------";
     1.7 +"--------- build fun check_err_patt ------------------------------";
     1.8  "-----------------------------------------------------------------";
     1.9  "-----------------------------------------------------------------";
    1.10  "-----------------------------------------------------------------";
    1.11 @@ -786,3 +787,47 @@
    1.12  [[from sml: </SYSERROR>
    1.13  [[from sml: @@@@@end@@@@@*)
    1.14  (*step into getFormulaeFromTo --- bug corrected...*)
    1.15 +
    1.16 +"--------- build fun check_err_patt ------------------------------";
    1.17 +"--------- build fun check_err_patt ------------------------------";
    1.18 +"--------- build fun check_err_patt ------------------------------";
    1.19 +val rls = norm_Rational
    1.20 +val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
    1.21 +val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
    1.22 +val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "1 / 2");
    1.23 +
    1.24 +val (res', _, _, rewritten) =
    1.25 +  rew_sub thy 1 [] e_rew_ord e_rls false [] (Trueprop $ pat) res;
    1.26 +if rewritten then NONE else SOME "e_errpatID";
    1.27 +
    1.28 +val norm_res = case rewrite_set_ (Isac()) false rls res' of
    1.29 +  NONE => res'
    1.30 +| SOME (norm_res, _) => norm_res
    1.31 +
    1.32 +val norm_inf = case rewrite_set_ (Isac()) false rls inf of
    1.33 +  NONE => inf
    1.34 +| SOME (norm_inf, _) => norm_inf;
    1.35 +
    1.36 +res' = inf;
    1.37 +norm_res = norm_inf;
    1.38 +
    1.39 +val pat = parse_patt @{theory} "(?a + ?b)/?a = ?b";
    1.40 +val (res, inf) = (str2term "(2 + 3)/2", str2term "3");
    1.41 +if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
    1.42 +then () else error "error patt example1 changed";
    1.43 +
    1.44 +val pat = parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
    1.45 +val (res, inf) = (str2term "(2 + 3)/(2 + 4)", str2term "3 / 4");
    1.46 +if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
    1.47 +then () else error "error patt example2 changed";
    1.48 +
    1.49 +val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
    1.50 +val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
    1.51 +if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
    1.52 +then () else error "error patt example3 changed";
    1.53 +
    1.54 +val inf =  str2term "1 / 2";
    1.55 +if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
    1.56 +then () else error "error patt example3 changed";
    1.57 +
    1.58 +