1.1 --- a/test/Tools/isac/Interpret/inform.sml	Wed May 16 15:47:22 2012 +0200
     1.2 +++ b/test/Tools/isac/Interpret/inform.sml	Thu May 17 12:43:04 2012 +0200
     1.3 @@ -32,6 +32,7 @@
     1.4  "--------- Take as 1st tac, start from exp -----------------------";
     1.5  "--------- init_form, start with <NEW> (CAS input) ---------------";
     1.6  "--------- build fun check_err_patt ------------------------------";
     1.7 +"--------- build fun check_err_patt ?bdv -------------------------";
     1.8  "-----------------------------------------------------------------";
     1.9  "-----------------------------------------------------------------";
    1.10  "-----------------------------------------------------------------";
    1.11 @@ -791,12 +792,13 @@
    1.12  "--------- build fun check_err_patt ------------------------------";
    1.13  "--------- build fun check_err_patt ------------------------------";
    1.14  "--------- build fun check_err_patt ------------------------------";
    1.15 +val subst = [(str2term "bdv", str2term "x")]: subst;
    1.16  val rls = norm_Rational
    1.17  val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
    1.18  val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
    1.19  val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "1 / 2");
    1.20  
    1.21 -val (res', _, _, rewritten) =
    1.22 +val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
    1.23    rew_sub thy 1 [] e_rew_ord e_rls false [] (Trueprop $ pat) res;
    1.24  if rewritten then NONE else SOME "e_errpatID";
    1.25  
    1.26 @@ -813,21 +815,58 @@
    1.27  
    1.28  val pat = parse_patt @{theory} "(?a + ?b)/?a = ?b";
    1.29  val (res, inf) = (str2term "(2 + 3)/2", str2term "3");
    1.30 -if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
    1.31 +if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    1.32  then () else error "error patt example1 changed";
    1.33  
    1.34  val pat = parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
    1.35  val (res, inf) = (str2term "(2 + 3)/(2 + 4)", str2term "3 / 4");
    1.36 -if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
    1.37 +if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    1.38  then () else error "error patt example2 changed";
    1.39  
    1.40  val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
    1.41  val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
    1.42 -if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
    1.43 +if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    1.44  then () else error "error patt example3 changed";
    1.45  
    1.46  val inf =  str2term "1 / 2";
    1.47 -if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
    1.48 +if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
    1.49  then () else error "error patt example3 changed";
    1.50  
    1.51 +"--------- build fun check_err_patt ?bdv -------------------------";
    1.52 +"--------- build fun check_err_patt ?bdv -------------------------";
    1.53 +"--------- build fun check_err_patt ?bdv -------------------------";
    1.54 +val subst = [(str2term "bdv", str2term "x")]: subst;
    1.55 +val t = str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))";
    1.56 +val SOME (t, _) = rewrite_set_inst_ thy false subst norm_diff t;
    1.57 +if term2str t = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3" then ()
    1.58 +else error "build fun check_err_patt ?bdv changed 1"; 
    1.59  
    1.60 +val rls = norm_diff
    1.61 +val pat = parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)"; 
    1.62 +val (res, inf) = (str2term "2 * x + d_d x (sin (x ^^^ 4))", str2term "2 * x + cos (4 * x ^^^ 3)");
    1.63 +
    1.64 +val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
    1.65 +  rew_sub thy 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) res;
    1.66 +if term2str res' = "2 * x + cos (d_d x (x ^^^ 4))" andalso rewritten then ()
    1.67 +else error "build fun check_err_patt ?bdv changed 2";
    1.68 +
    1.69 +val norm_res = case rewrite_set_inst_ (Isac()) false subst rls  res' of
    1.70 +  NONE => res'
    1.71 +| SOME (norm_res, _) => norm_res;
    1.72 +if term2str norm_res = "2 * x + cos (4 * x ^^^ 3)" then ()
    1.73 +else error "build fun check_err_patt ?bdv changed 3";
    1.74 +
    1.75 +val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of
    1.76 +  NONE => inf
    1.77 +| SOME (norm_inf, _) => norm_inf;
    1.78 +if term2str norm_inf = "2 * x + cos (4 * x ^^^ 3)" then ()
    1.79 +else error "build fun check_err_patt ?bdv changed 4";
    1.80 +
    1.81 +res' = inf;
    1.82 +if norm_res = norm_inf then ()
    1.83 +else error "build fun check_err_patt ?bdv changed 5";
    1.84 +
    1.85 +if check_err_patt (res, inf) (subst: subst) ("errpatID": errpatID, pat) rls = SOME "errpatID"
    1.86 +then () else error "error patt example1 changed";
    1.87 +
    1.88 +