1.1 --- a/src/Tools/isac/Interpret/inform.sml Wed May 16 15:47:22 2012 +0200
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu May 17 12:43:04 2012 +0200
1.3 @@ -632,18 +632,18 @@
1.4 end;
1.5
1.6 (* check if (agreed result, input formula) matches an error pattern modulo simplifier rls*)
1.7 -fun check_err_patt (res, inf) (errpatID: errpatID, pat) rls =
1.8 +fun check_err_patt (res, inf) (subst: subst) (errpatID: errpatID, pat) rls =
1.9 let
1.10 val (res', _, _, rewritten) =
1.11 - rew_sub (Isac()) 1 [] e_rew_ord e_rls false [] (Trueprop $ pat) res;
1.12 + rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) res;
1.13 in
1.14 if rewritten
1.15 then
1.16 let
1.17 - val norm_res = case rewrite_set_ (Isac()) false rls res' of
1.18 + val norm_res = case rewrite_set_inst_ (Isac()) false subst rls res' of
1.19 NONE => res'
1.20 | SOME (norm_res, _) => norm_res
1.21 - val norm_inf = case rewrite_set_ (Isac()) false rls inf of
1.22 + val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of
1.23 NONE => inf
1.24 | SOME (norm_inf, _) => norm_inf
1.25 in if norm_res = norm_inf then SOME errpatID else NONE
1.26 @@ -658,7 +658,8 @@
1.27 formula, which is no CAS-command:
1.28 compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
1.29 collect all the tacs applied by the way;
1.30 - if "no derivation found" then check_error_patterns.*)
1.31 + if "no derivation found" then check_error_patterns.
1.32 + ALTERNATIVE to check_error_patterns within compare_step seems too expensive.*)
1.33 fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
1.34 case parse (assoc_thy "Isac") istr of
1.35 SOME ifo =>
1.36 @@ -677,14 +678,25 @@
1.37 SOME (pt, _) => ("ok",([], [], (pt, (p, Met))))
1.38 | NONE =>
1.39 let val msg_calcstate' = compare_step ([], [], (pt, lev_back pos)) ifo
1.40 - (*last step re-calc in compare_step TODO before WN09*)
1.41 + (*last step re-calc in compare_step TODO before WN09*)
1.42 in
1.43 case msg_calcstate' of
1.44 - ("no derivation found", _) => msg_calcstate' (*GOON*)
1.45 + ("no derivation found", calcstate') =>
1.46 +(*GOON
1.47 + let
1.48 + val pp = par_pblobj pt p
1.49 + val {errpats, nrls, ...} = get_met (get_obj g_metID pt pp)
1.50 + in
1.51 + case check_error_patterns (fo, ifo) ?subst? errpats nrls of
1.52 + SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
1.53 + | NONE => msg_calcstate'
1.54 + end
1.55 +GOON*)
1.56 + msg_calcstate'
1.57 | _ => msg_calcstate'
1.58 end
1.59 end
1.60 - | NONE => ("syntax error in '"^istr^"'", e_calcstate');
1.61 + | NONE => ("syntax error in '" ^ istr ^ "'", e_calcstate');
1.62
1.63
1.64 (*------------------------------------------------------------------(**)
2.1 --- a/src/Tools/isac/Knowledge/Diff.thy Wed May 16 15:47:22 2012 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Thu May 17 12:43:04 2012 +0200
2.3 @@ -228,12 +228,12 @@
2.4 ML {*
2.5 (*.normalisation for checking user-input.*)
2.6 val norm_diff =
2.7 - Rls {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI),
2.8 - erls = Erls, srls = Erls, calc = [],
2.9 - rules = [Rls_ diff_rules,
2.10 - Rls_ norm_Poly
2.11 - ],
2.12 - scr = EmptyScr};
2.13 + Rls
2.14 + {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI),
2.15 + erls = Erls, srls = Erls, calc = [],
2.16 + rules = [Rls_ diff_rules, Rls_ norm_Poly ],
2.17 + scr = EmptyScr};
2.18 +
2.19 ruleset' :=
2.20 overwritelthy @{theory} (!ruleset',
2.21 [("diff_rules", prep_rls norm_diff),
3.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Wed May 16 15:47:22 2012 +0200
3.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Thu May 17 12:43:04 2012 +0200
3.3 @@ -448,6 +448,31 @@
3.4 | contain_bdv (r::_) =
3.5 error ("contain_bdv called with ["^(id_rule r)^",...]");
3.6
3.7 +(* get a substitution for "bdv*" from the current program and environment*)
3.8 +fun get_bdv_subst prog env =
3.9 + let
3.10 + fun scan (Const _) = NONE
3.11 + | scan (Free _) = NONE
3.12 + | scan (Var _) = NONE
3.13 + | scan (Bound _) = NONE
3.14 + | scan (t as Const ("List.list.Cons", _) $
3.15 + (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) =
3.16 + if is_bdv_subst t then SOME t else NONE
3.17 + | scan (Abs (_, _, body)) = scan body
3.18 + | scan (t1 $ t2) =
3.19 + case scan t1 of
3.20 + NONE => scan t2
3.21 + | SOME subst => SOME subst
3.22 + in
3.23 + case scan prog of
3.24 + NONE => []: subst
3.25 + | SOME subs =>
3.26 + (subs |> subst_atomic env |> isalist2list |> map isapair2pair)
3.27 + (*"[(bdv,v_v)]": term
3.28 + |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list
3.29 + |> [("bdv","x")]: (term * term) list*)
3.30 + end;
3.31 +
3.32 fun rules2scr_Rls calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
3.33 if contain_bdv rules
3.34 then ScrStep_inst $ Term $ Bdv $
4.1 --- a/src/Tools/isac/ProgLang/termC.sml Wed May 16 15:47:22 2012 +0200
4.2 +++ b/src/Tools/isac/ProgLang/termC.sml Thu May 17 12:43:04 2012 +0200
4.3 @@ -243,6 +243,11 @@
4.4 fun is_bdv_ (Free (s,_)) = is_bdv s
4.5 | is_bdv_ _ = false;
4.6
4.7 +(* is a term a substitution for a bdv as found in programs *)
4.8 +fun is_bdv_subst (Const ("List.list.Cons", _) $
4.9 + (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) = is_bdv str
4.10 + | is_bdv_subst _ = false;
4.11 +
4.12 fun free2str (Free (s,_)) = s
4.13 | free2str t = error ("free2str not for "^ term2str t);
4.14 fun free2int (t as Free (s, _)) = ((str2int s)
5.1 --- a/test/Tools/isac/Interpret/inform.sml Wed May 16 15:47:22 2012 +0200
5.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu May 17 12:43:04 2012 +0200
5.3 @@ -32,6 +32,7 @@
5.4 "--------- Take as 1st tac, start from exp -----------------------";
5.5 "--------- init_form, start with <NEW> (CAS input) ---------------";
5.6 "--------- build fun check_err_patt ------------------------------";
5.7 +"--------- build fun check_err_patt ?bdv -------------------------";
5.8 "-----------------------------------------------------------------";
5.9 "-----------------------------------------------------------------";
5.10 "-----------------------------------------------------------------";
5.11 @@ -791,12 +792,13 @@
5.12 "--------- build fun check_err_patt ------------------------------";
5.13 "--------- build fun check_err_patt ------------------------------";
5.14 "--------- build fun check_err_patt ------------------------------";
5.15 +val subst = [(str2term "bdv", str2term "x")]: subst;
5.16 val rls = norm_Rational
5.17 val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
5.18 val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
5.19 val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "1 / 2");
5.20
5.21 -val (res', _, _, rewritten) =
5.22 +val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
5.23 rew_sub thy 1 [] e_rew_ord e_rls false [] (Trueprop $ pat) res;
5.24 if rewritten then NONE else SOME "e_errpatID";
5.25
5.26 @@ -813,21 +815,58 @@
5.27
5.28 val pat = parse_patt @{theory} "(?a + ?b)/?a = ?b";
5.29 val (res, inf) = (str2term "(2 + 3)/2", str2term "3");
5.30 -if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
5.31 +if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
5.32 then () else error "error patt example1 changed";
5.33
5.34 val pat = parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
5.35 val (res, inf) = (str2term "(2 + 3)/(2 + 4)", str2term "3 / 4");
5.36 -if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
5.37 +if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
5.38 then () else error "error patt example2 changed";
5.39
5.40 val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
5.41 val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
5.42 -if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
5.43 +if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
5.44 then () else error "error patt example3 changed";
5.45
5.46 val inf = str2term "1 / 2";
5.47 -if check_err_patt (res, inf) ("errpatID", pat) rls = SOME "errpatID"
5.48 +if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
5.49 then () else error "error patt example3 changed";
5.50
5.51 +"--------- build fun check_err_patt ?bdv -------------------------";
5.52 +"--------- build fun check_err_patt ?bdv -------------------------";
5.53 +"--------- build fun check_err_patt ?bdv -------------------------";
5.54 +val subst = [(str2term "bdv", str2term "x")]: subst;
5.55 +val t = str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))";
5.56 +val SOME (t, _) = rewrite_set_inst_ thy false subst norm_diff t;
5.57 +if term2str t = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3" then ()
5.58 +else error "build fun check_err_patt ?bdv changed 1";
5.59
5.60 +val rls = norm_diff
5.61 +val pat = parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)";
5.62 +val (res, inf) = (str2term "2 * x + d_d x (sin (x ^^^ 4))", str2term "2 * x + cos (4 * x ^^^ 3)");
5.63 +
5.64 +val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
5.65 + rew_sub thy 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) res;
5.66 +if term2str res' = "2 * x + cos (d_d x (x ^^^ 4))" andalso rewritten then ()
5.67 +else error "build fun check_err_patt ?bdv changed 2";
5.68 +
5.69 +val norm_res = case rewrite_set_inst_ (Isac()) false subst rls res' of
5.70 + NONE => res'
5.71 +| SOME (norm_res, _) => norm_res;
5.72 +if term2str norm_res = "2 * x + cos (4 * x ^^^ 3)" then ()
5.73 +else error "build fun check_err_patt ?bdv changed 3";
5.74 +
5.75 +val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of
5.76 + NONE => inf
5.77 +| SOME (norm_inf, _) => norm_inf;
5.78 +if term2str norm_inf = "2 * x + cos (4 * x ^^^ 3)" then ()
5.79 +else error "build fun check_err_patt ?bdv changed 4";
5.80 +
5.81 +res' = inf;
5.82 +if norm_res = norm_inf then ()
5.83 +else error "build fun check_err_patt ?bdv changed 5";
5.84 +
5.85 +if check_err_patt (res, inf) (subst: subst) ("errpatID": errpatID, pat) rls = SOME "errpatID"
5.86 +then () else error "error patt example1 changed";
5.87 +
5.88 +
6.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Wed May 16 15:47:22 2012 +0200
6.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Thu May 17 12:43:04 2012 +0200
6.3 @@ -9,6 +9,7 @@
6.4 "-------- test the same called by interSteps norm_Poly -----------";
6.5 "-------- test the same called by interSteps norm_Rational -------";
6.6 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
6.7 +"-------- build fun get_bdv_subst --------------------------------";
6.8 "-----------------------------------------------------------------";
6.9 "-----------------------------------------------------------------";
6.10 "-----------------------------------------------------------------";
6.11 @@ -173,8 +174,6 @@
6.12 ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
6.13 | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
6.14
6.15 -
6.16 -
6.17 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
6.18 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
6.19 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
6.20 @@ -188,3 +187,14 @@
6.21 two_scr_arg auto_script;
6.22 init_istate (Rewrite_Set_Inst (["(bdv, x)"], "integration_rules"))
6.23 (str2term "someTermWithBdv");
6.24 +
6.25 +"-------- build fun get_bdv_subst --------------------------------";
6.26 +"-------- build fun get_bdv_subst --------------------------------";
6.27 +"-------- build fun get_bdv_subst --------------------------------";
6.28 +val {scr = Script prog, ...} = get_met ["diff", "differentiate_on_R"];
6.29 +val env = [(str2term "v_v", str2term "x")];
6.30 +subst2str env = "[\"\n(v_v, x)\"]";
6.31 +
6.32 +if subst2str (get_bdv_subst prog env) = "[\"\n(bdv, x)\"]" then ()
6.33 +else error "get_bdv_subst changed";
6.34 +
7.1 --- a/test/Tools/isac/ProgLang/termC.sml Wed May 16 15:47:22 2012 +0200
7.2 +++ b/test/Tools/isac/ProgLang/termC.sml Thu May 17 12:43:04 2012 +0200
7.3 @@ -14,6 +14,7 @@
7.4 "----------- uminus_to_string ---------------------------";
7.5 "----------- *** prep_pbt: syntax error in '#Where' of [v";
7.6 "----------- check writeln, tracing for string markup ---";
7.7 +"-------- build fun is_bdv_subst ---------------------------------";
7.8 "--------------------------------------------------------";
7.9 "--------------------------------------------------------";
7.10
7.11 @@ -359,3 +360,17 @@
7.12 tracing str;
7.13 tracing "----------------DIFFERENT output----";
7.14 *)
7.15 +
7.16 +"-------- build fun is_bdv_subst ---------------------------------";
7.17 +"-------- build fun is_bdv_subst ---------------------------------";
7.18 +"-------- build fun is_bdv_subst ---------------------------------";
7.19 +fun is_bdv_subst (Const ("List.list.Cons", _) $
7.20 + (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) = is_bdv str
7.21 + | is_bdv_subst _ = false;
7.22 +
7.23 +if is_bdv_subst (str2term "[(bdv, v_v)]") then ()
7.24 +else error "is_bdv_subst canged 1";
7.25 +
7.26 +if is_bdv_subst (str2term "[(bdv_1, v_s1),(bdv_2, v_s2)]") then ()
7.27 +else error "is_bdv_subst canged 2";
7.28 +
8.1 --- a/test/Tools/isac/Test_Some.thy Wed May 16 15:47:22 2012 +0200
8.2 +++ b/test/Tools/isac/Test_Some.thy Thu May 17 12:43:04 2012 +0200
8.3 @@ -1,7 +1,7 @@
8.4
8.5 theory Test_Some imports Isac begin
8.6
8.7 -use"../../../test/Tools/isac/Interpret/inform.sml"
8.8 +use"../../../test/Tools/isac/ProgLang/termC.sml"
8.9
8.10 ML {*
8.11 val thy = @{theory "Isac"};
8.12 @@ -11,10 +11,37 @@
8.13 ML {*
8.14 *}
8.15 ML {* (*==================*)
8.16 +fun is_bdv_subst (Const ("List.list.Cons", _) $
8.17 + (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) = is_bdv str
8.18 + | is_bdv_subst _ = false;
8.19 *}
8.20 -ML {*
8.21 -*}
8.22 -ML {*
8.23 +ML {* (*==================*)
8.24 +"-------- build fun get_bdv_subst --------------------------------";
8.25 +(* get a substitution for "bdv*" from the current program and environment*)
8.26 +fun get_bdv_subst prog env =
8.27 + let
8.28 + fun scan (Const _) = NONE
8.29 + | scan (Free _) = NONE
8.30 + | scan (Var _) = NONE
8.31 + | scan (Bound _) = NONE
8.32 + | scan (t as Const ("List.list.Cons", _) $
8.33 + (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) =
8.34 + if is_bdv_subst t then SOME t else NONE
8.35 + | scan (Abs (_, _, body)) = scan body
8.36 + | scan (t1 $ t2) =
8.37 + case scan t1 of
8.38 + NONE => scan t2
8.39 + | SOME subst => SOME subst
8.40 + in
8.41 + case scan prog of
8.42 + NONE => []: subst
8.43 + | SOME subs =>
8.44 + (subs |> subst_atomic env |> isalist2list |> map isapair2pair)
8.45 + (*"[(bdv,v_v)]": term
8.46 + |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list
8.47 + |> [("bdv","x")]: (term * term) list*)
8.48 + end;
8.49 +
8.50 *}
8.51 ML {*
8.52 *}
8.53 @@ -25,6 +52,23 @@
8.54 ML {*
8.55 *}
8.56 ML {* (*==================*)
8.57 +val errpats = [e_errpat]: errpat list;
8.58 +val errpats =
8.59 +[("chain-rule-diff-both",
8.60 + [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
8.61 + parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
8.62 + parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
8.63 + parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
8.64 + parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
8.65 + [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
8.66 + @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
8.67 +*}
8.68 +ML {*
8.69 +*}
8.70 +ML {*
8.71 +*}
8.72 +ML {* (*==================*)
8.73 +"--------- build fun check_error_patterns ------------------------";
8.74 states:=[];
8.75 CalcTree
8.76 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
8.77 @@ -63,16 +107,26 @@
8.78 (*term2str fo = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)"*)
8.79 fo = ifo; (* = false*)
8.80 cas_input ifo; (* = NONE*)
8.81 -
8.82 -"~~~~~ fun compare_step, args:"; val (((tacis, c, ptp as (pt, pos as (p,p_))): calcstate'), ifo) =
8.83 - (([], [], (pt, lev_back pos)), ifo);
8.84 +val msg_calcstate' = compare_step ([], [], (pt, lev_back pos)) ifo
8.85 +*}
8.86 +ML {* (*###################### new code ######################*)
8.87 +val pp = par_pblobj pt p
8.88 *}
8.89 ML {*
8.90 - val fo =
8.91 - case p_ of
8.92 - Frm => get_obj g_form pt p
8.93 - | Res => (fst o (get_obj g_result pt)) p
8.94 - | _ => e_term (*on PblObj is fo <> ifo*);
8.95 +val {errpats, nrls, ...} = get_met (get_obj g_metID pt pp);
8.96 +*}
8.97 +ML {*
8.98 +val ScrState (env, loc_, topt, t, safe, bool) = get_istate pt pos
8.99 +*}
8.100 +ML {*
8.101 +*}
8.102 +ML {*
8.103 +val [a,b,c] = env;
8.104 +(str2term "v_v", str2term "x") = b
8.105 +*}
8.106 +ML {*
8.107 +*}
8.108 +ML {* (*###################### new code ######################*)
8.109 *}
8.110 ML {*
8.111 *}
8.112 @@ -81,6 +135,7 @@
8.113 ML {*
8.114 compare_step;
8.115 e_calcstate';
8.116 +writeln ("#####"^env2str env^"#####"); (*----- (v_v, x) -----*)
8.117 *}
8.118 ML {*
8.119
8.120 @@ -112,6 +167,10 @@
8.121 ML {*
8.122 *}
8.123 ML {* (*==================*)
8.124 +*}
8.125 +ML {* (*==================*)
8.126 +*}
8.127 +ML {* (*==================*)
8.128 "~~~~~ fun , args:"; val () = ();
8.129 "~~~~~ to return val:"; val () = ();
8.130