1.1 --- a/src/Tools/isac/Frontend/interface.sml	Tue May 22 13:40:06 2012 +0200
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Thu May 24 17:13:58 2012 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4      val setNextTactic : calcID -> tac -> unit
     1.5      val setProblem : calcID -> pblID -> unit
     1.6      val setTheory : calcID -> thyID -> unit
     1.7 -    val FindFillpatterns : calcID -> errpatID -> unit
     1.8 +    val findFillpatterns : calcID -> errpatID -> unit
     1.9      val requestFillformula : calcID -> errpatID * fillpatID -> unit
    1.10  (*------------ for tests*)
    1.11  val encode: cterm' -> cterm'
    1.12 @@ -787,28 +787,31 @@
    1.13  
    1.14  (* for an errpatID find "(fillpatID, fillform)" list 
    1.15    which dedicated to this errpat and which is applicable at current formula*)
    1.16 -fun FindFillpatterns cI errpatID = 
    1.17 +fun findFillpatterns cI errpatID = 
    1.18    let
    1.19      val ((pt, _), _) = get_calc cI
    1.20 -		val pos = get_pos cI 1;
    1.21 -		val fillpats = find_fillpatterns (pt, pos) errpatID
    1.22 -		val args = "fill patterns " ^ ((map (apsnd term2str) fillpats) |> map pair2str_ |> strs2str_)
    1.23 -			(* the format for the message's arguments is waiting for generalisation of CalcMessage *)
    1.24 -	in calcMessage2xml cI ("fill patterns " ^ args) end;
    1.25 +		    val pos = get_pos cI 1;
    1.26 +		    val fillpats = find_fillpatterns (pt, pos) errpatID
    1.27 +		    val args = "fill patterns " ^
    1.28 +		      ((map ((apsnd term2str) o quad2pair) fillpats) |> map pair2str_ |> strs2str_)
    1.29 +		      (* the format for the message's arguments is waiting for generalisation of CalcMessage *)
    1.30 +	  in calcMessage2xml cI ("fill patterns " ^ args) end;
    1.31  
    1.32  (* given a fillpatID propose a fillform to the learner on the worksheet;
    1.33 -  the "ctree" is extended with fillpat and "ostate Inconsistent", the "istate" is NOT updated;
    1.34 +  the "ctree" is extended with fillpat and "ostate Inconsistent",
    1.35 +  the "istate" is copied and NOT updated;
    1.36    returns CalcChanged.
    1.37    arg errpatID: required because there is no dialog-related state in the math-kernel.
    1.38  *)
    1.39  fun requestFillformula cI (errpatID, fillpatID) =
    1.40    let
    1.41      val ((pt, _), _) = get_calc cI
    1.42 -		val pos as (p, _) = get_pos cI 1
    1.43 -    val fillforms = find_fillpatterns (pt, pos) errpatID
    1.44 +		    val pos as (p, _) = get_pos cI 1
    1.45 +    val fillforms = find_fillpatterns (pt, pos) errpatID 
    1.46    in
    1.47 -    case filter ((curry op = fillpatID) o (#1: (fillpatID * term -> fillpatID))) fillforms of
    1.48 -      (fillpatID, fillform) :: _ =>
    1.49 +    case filter ((curry op = fillpatID) o 
    1.50 +        (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of
    1.51 +      (fillpatID, fillform, thm, bdvopt) :: _ =>
    1.52          let
    1.53            val f_curr = get_curr_formula (pt, pos) (*already done in find_fillpatterns, too*)
    1.54            val (pos', _, _, pt) = generate_inconsistent 0

     2.1 --- a/src/Tools/isac/Interpret/ctree.sml	Tue May 22 13:40:06 2012 +0200
     2.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Thu May 24 17:13:58 2012 +0200
     2.3 @@ -213,7 +213,7 @@
     2.4  type subs = cterm' list; (*16.11.00 for FE-KE*)
     2.5  val e_subs = ["(bdv, x)"];
     2.6  
     2.7 -(*._sub_stitution as strings of _e_qualities.*)
     2.8 +(* argument type of tac Rewrite_Inst *)
     2.9  type sube = cterm' list;
    2.10  val e_sube = []:cterm' list;
    2.11  fun sube2str s = strs2str s;

     3.1 --- a/src/Tools/isac/Interpret/inform.sml	Tue May 22 13:40:06 2012 +0200
     3.2 +++ b/src/Tools/isac/Interpret/inform.sml	Thu May 24 17:13:58 2012 +0200
     3.3 @@ -655,7 +655,7 @@
     3.4     (prog, env) for retrieval of casual substitution for bdv in the pattern. *)
     3.5  fun check_error_patterns (res, inf) (prog, env) (errpats, rls) =
     3.6    let
     3.7 -    val subst = get_bdv_subst prog env
     3.8 +    val (_, subst) = get_bdv_subst prog env
     3.9      fun scan (_, [], _) = NONE
    3.10        | scan (errpatID, errpat :: errpats, _) =
    3.11            case check_err_patt (res, inf) (subst: subst) (errpatID, errpat) rls of
    3.12 @@ -713,14 +713,15 @@
    3.13  			end
    3.14      | NONE => ("syntax error in '" ^ istr ^ "'", e_calcstate');
    3.15  
    3.16 -(* fill-in patterns an forms *)
    3.17 -fun get_fillform subst form errpatID ((fillpatID, pat, erpaID): fillpat) =
    3.18 +(* fill-in patterns an forms.
    3.19 +  returns thm required by "fun in_fillform *)
    3.20 +fun get_fillform (subs_opt, subst) (thm, form) errpatID ((fillpatID, pat, erpaID): fillpat) =
    3.21    let
    3.22      val (form', _, _, rewritten) =
    3.23        rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
    3.24    in (*the fillpat of the thm must be dedicated to errpatID*)
    3.25      if errpatID = erpaID andalso rewritten
    3.26 -    then SOME (fillpatID, HOLogic.mk_eq (form, form')) else NONE end;
    3.27 +    then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) else NONE end;
    3.28  
    3.29  fun get_fillpats subst form errpatID thm =
    3.30        let
    3.31 @@ -728,7 +729,7 @@
    3.32          val (part, thyID) = thy_containing_thm thmDeriv
    3.33          val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
    3.34          val Hthm {fillpats, ...} = get_the theID
    3.35 -        val some = map (get_fillform subst form errpatID) fillpats
    3.36 +        val some = map (get_fillform subst (thm, form) errpatID) fillpats
    3.37        in some |> filter is_some |> map the end;
    3.38  
    3.39  fun find_fillpatterns (pt, pos as (p, _): pos') errpatID =

     4.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Tue May 22 13:40:06 2012 +0200
     4.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Thu May 24 17:13:58 2012 +0200
     4.3 @@ -892,6 +892,35 @@
     4.4  	   end
     4.5      end;
     4.6  
     4.7 +(* get a substitution for "bdv*" from the current program and environment.
     4.8 +    returns a substitution: subst for rewriting and another: sube for Rewrite:*)
     4.9 +fun get_bdv_subst prog env =
    4.10 +  let
    4.11 +    fun scan (Const _) = NONE
    4.12 +      | scan (Free _) = NONE
    4.13 +      | scan (Var _) = NONE
    4.14 +      | scan (Bound _) = NONE
    4.15 +      | scan (t as Const ("List.list.Cons", _) $
    4.16 +         (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) =
    4.17 +           if is_bdv_subst t then SOME t else NONE
    4.18 +      | scan (Abs (_, _, body)) = scan body
    4.19 +      | scan (t1 $ t2) =
    4.20 +          case scan t1 of
    4.21 +            NONE => scan t2
    4.22 +          | SOME subst => SOME subst
    4.23 +  in
    4.24 +    case scan prog of
    4.25 +      NONE => (NONE: subs option, []: subst)
    4.26 +    | SOME tm =>
    4.27 +        let val subst = tm |> subst_atomic env |> isalist2list |> map isapair2pair
    4.28 +          (*"[(bdv,v_v)]": term
    4.29 +                          |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list
    4.30 +                                                         |> [("bdv","x")]: (term * term) list*)
    4.31 +        in (SOME (subst2subs subst), subst) end
    4.32 +          (*"SOME [(bdv,v_v)]": term --> ["(bdv,v_v)"]: string list*)
    4.33 +  end;
    4.34 +
    4.35 +
    4.36  (* use"ME/rewtools.sml";
    4.37     *)
    4.38  

     5.1 --- a/src/Tools/isac/ProgLang/scrtools.sml	Tue May 22 13:40:06 2012 +0200
     5.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml	Thu May 24 17:13:58 2012 +0200
     5.3 @@ -448,31 +448,6 @@
     5.4    | contain_bdv (r::_) = 
     5.5      error ("contain_bdv called with ["^(id_rule r)^",...]");
     5.6  
     5.7 -(* get a substitution for "bdv*" from the current program and environment*)
     5.8 -fun get_bdv_subst prog env =
     5.9 -  let
    5.10 -    fun scan (Const _) = NONE
    5.11 -      | scan (Free _) = NONE
    5.12 -      | scan (Var _) = NONE
    5.13 -      | scan (Bound _) = NONE
    5.14 -      | scan (t as Const ("List.list.Cons", _) $
    5.15 -         (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) =
    5.16 -           if is_bdv_subst t then SOME t else NONE
    5.17 -      | scan (Abs (_, _, body)) = scan body
    5.18 -      | scan (t1 $ t2) =
    5.19 -          case scan t1 of
    5.20 -            NONE => scan t2
    5.21 -          | SOME subst => SOME subst
    5.22 -  in
    5.23 -    case scan prog of
    5.24 -      NONE => []: subst
    5.25 -    | SOME subs =>
    5.26 -      (subs |> subst_atomic env |> isalist2list |> map isapair2pair)
    5.27 -      (*"[(bdv,v_v)]": term
    5.28 -            |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list
    5.29 -                                                |> [("bdv","x")]: (term * term) list*)
    5.30 -  end;
    5.31 -
    5.32  fun rules2scr_Rls calc rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
    5.33      if contain_bdv rules
    5.34      then ScrStep_inst $ Term $ Bdv $ 

     6.1 --- a/src/Tools/isac/library.sml	Tue May 22 13:40:06 2012 +0200
     6.2 +++ b/src/Tools/isac/library.sml	Thu May 24 17:13:58 2012 +0200
     6.3 @@ -214,7 +214,7 @@
     6.4  fun ints2str ints = (strs2str o (map string_of_int)) ints;
     6.5  fun ints2str' ints = (strs2str' o (map string_of_int)) ints;
     6.6  
     6.7 -(* FindFillpatterns: the message's format is waiting for generalisation of CalcMessage *)
     6.8 +(* findFillpatterns: the message's format is waiting for generalisation of CalcMessage *)
     6.9  fun pair2str_ (s1,s2) =   s1 ^ "#" ^ s2;
    6.10  val nos = space_implode "#";
    6.11  fun strs2str_ strl = "#" ^ (nos strl) ^ "#";
    6.12 @@ -348,3 +348,7 @@
    6.13              tracing ("comp_strs: " ^ c1 ^ " = " ^ c2 ^ " ..." ^ 
    6.14                       bool2str (c1 = c2))
    6.15      in map comp_char ((Symbol.explode str1) ~~ (Symbol.explode str2)) end;
    6.16 +
    6.17 +fun triple2pair (a, b, c) = (a, b);
    6.18 +fun quad2pair (a, b, c, d) = (a, b);
    6.19 +

     7.1 --- a/test/Tools/isac/Interpret/inform.sml	Tue May 22 13:40:06 2012 +0200
     7.2 +++ b/test/Tools/isac/Interpret/inform.sml	Thu May 24 17:13:58 2012 +0200
     7.3 @@ -36,7 +36,7 @@
     7.4  "--------- build fun check_error_patterns ------------------------";
     7.5  "--------- embed fun check_error_patterns ------------------------";
     7.6  "--------- embed fun find_fillpatterns ---------------------------";
     7.7 -"--------- embed fun get_fillform --------------------------------";
     7.8 +"--------- embed fun get_fillformula -----------------------------";
     7.9  "-----------------------------------------------------------------";
    7.10  "-----------------------------------------------------------------";
    7.11  "-----------------------------------------------------------------";
    7.12 @@ -975,7 +975,7 @@
    7.13    (*or
    7.14      <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
    7.15  
    7.16 -"~~~~~ fun FindFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
    7.17 +"~~~~~ fun findFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
    7.18    val ((pt, _), _) = get_calc cI
    7.19  				val pos = get_pos cI 1;
    7.20  "~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
    7.21 @@ -990,7 +990,7 @@
    7.22        |> flat;
    7.23  
    7.24  case map (get_fillpats subst f_curr errpatID) errpatthms |> flat of
    7.25 -  ("fill-d_d-arg", tm) :: _ => if term2str tm = 
    7.26 +  ("fill-d_d-arg", tm, thm, subs_opt) :: _ => if term2str tm = 
    7.27      "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
    7.28      then () else error "find_fillpatterns changed 1a"
    7.29  | _ => error "find_fillpatterns changed 1b"
    7.30 @@ -1001,26 +1001,28 @@
    7.31          val (part, thyID) = thy_containing_thm thmDeriv
    7.32          val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
    7.33          val Hthm {fillpats, ...} = get_the theID
    7.34 -        val some = map (get_fillform subst form errpatID) fillpats;
    7.35 +        val some = map (get_fillform subst (thm, form) errpatID) fillpats;
    7.36  
    7.37  case some |> filter is_some |> map the of
    7.38 -  ("fill-d_d-arg", tm) :: _ => if term2str tm = 
    7.39 +  ("fill-d_d-arg", tm, thm, subsopt) :: _ => if term2str tm = 
    7.40      "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
    7.41      then () else error "find_fillpatterns changed 2a"
    7.42  | _ => error "find_fillpatterns changed 2b"
    7.43  
    7.44 -"~~~~~ fun get_fillform, args:"; val (subst, form, errpatID, ((fillpatID, pat, erpaID): fillpat)) =
    7.45 -  (subst, form, errpatID, hd (*simulate beginning of "map"*) fillpats);
    7.46 -    val (form', _, _, rewritten) =
    7.47 +"~~~~~ fun get_fillform, args:";
    7.48 +  val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
    7.49 +  (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
    7.50 +val (form', _, _, rewritten) =
    7.51        rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
    7.52  
    7.53  if term2str form' = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
    7.54  else error "find_fillpatterns changed 3";
    7.55  
    7.56 -"~~~~~ to FindFillpatterns return val:"; val (fillpats) =
    7.57 -  (map (get_fillpats subst f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
    7.58 +"~~~~~ to findFillpatterns return val:"; val (fillpats) =
    7.59 +  (map (get_fillpats (subs_opt, subst) f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
    7.60  
    7.61 -val msg = "fill patterns " ^ ((map (apsnd term2str) fillpats) |> map pair2str_ |> strs2str_);
    7.62 +val msg = "fill patterns " ^
    7.63 +  ((map ((apsnd term2str) o quad2pair) fillpats) |> map pair2str_ |> strs2str_);
    7.64  if msg =
    7.65    "fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
    7.66      " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" ^
    7.67 @@ -1034,9 +1036,9 @@
    7.68  then () else error "find_fillpatterns changed 4";
    7.69  
    7.70  
    7.71 -"--------- embed fun get_fillform --------------------------------";
    7.72 -"--------- embed fun get_fillform --------------------------------";
    7.73 -"--------- embed fun get_fillform --------------------------------";
    7.74 +"--------- embed fun get_fillformula -----------------------------";
    7.75 +"--------- embed fun get_fillformula -----------------------------";
    7.76 +"--------- embed fun get_fillformula -----------------------------";
    7.77  states := [];
    7.78  CalcTree
    7.79  [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], 
    7.80 @@ -1051,7 +1053,7 @@
    7.81    would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
    7.82    results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
    7.83    instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
    7.84 -FindFillpatterns 1 "chain-rule-diff-both";
    7.85 +findFillpatterns 1 "chain-rule-diff-both";
    7.86  (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
    7.87    d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
    7.88  
    7.89 @@ -1064,11 +1066,79 @@
    7.90    ((pt, pos), (errpatID, fillpatID));
    7.91  val fillforms = find_fillpatterns (pt, pos) errpatID
    7.92  val fillforms =
    7.93 -  filter ((curry op = fillpatID) o (#1: (fillpatID * term -> fillpatID))) fillforms;
    7.94 +  filter ((curry op = fillpatID) o (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms;
    7.95  
    7.96 -val [(fillpatID, fillform)] = fillforms;
    7.97 -case (fillpatID, fillform) of
    7.98 - ("fill-both-args", tm) => if term2str tm = 
    7.99 +val [(fillpatID, fillform, thm, subs_opt)] = fillforms;
   7.100 +case (fillpatID, fillform, thm, subs_opt) of
   7.101 + ("fill-both-args", tm, thm, subs_opt) => if term2str tm = 
   7.102 +     "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
   7.103 +     then () else error "get_fillformula changed 1a"
   7.104 +| _ => error "get_fillformula changed 1b";
   7.105 +
   7.106 +    val f_curr = get_curr_formula (pt, pos); (*already done in find_fillpatterns, too*)
   7.107 +term2str f_curr = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
   7.108 +
   7.109 +"~~~~~ fun generate_inconsistent, args:";
   7.110 +  val (_, (Rewrite' (_,_,_,_, thm', f, (f', asm))), (is, ctxt), (p,_), pt) =
   7.111 +    (0,
   7.112 +      (Rewrite' ("","",e_rls,true, (fillpatID, ""(*errpatthm known in find_fillpatterns*)),
   7.113 +        f_curr, (fillform, []))),
   7.114 +      (get_loc pt pos), (lev_on p, Und), pt);
   7.115 +if p = [2] then () else error "generate_inconsistent changed 1";
   7.116 +
   7.117 +val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
   7.118 +          (Rewrite thm') (f', asm) Inconsistent
   7.119 +val pt = update_branch pt p TransitiveB;
   7.120 +
   7.121 +"~~~~~ to get_fillformula return val:"; val (pos', _, _, pt) =
   7.122 +  ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt);
   7.123 +if pos' = ([2], Res) then () else error "generate_inconsistent changed 2";
   7.124 +
   7.125 +upd_calc cI ((pt, pos'), []); upd_ipos cI 1 pos';
   7.126 +autocalculateOK2xml cI pos pos' pos';
   7.127 +
   7.128 +"~~~~~ final check:";
   7.129 +val ((pt,pos),_) = get_calc 1;
   7.130 +val p = get_pos 1 1;
   7.131 +val (Form f, tac, asms) = pt_extract (pt, p);
   7.132 +if p = ([2], Res) andalso term2str f =
   7.133 +  "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
   7.134 +then () else error "";
   7.135 +
   7.136 +show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)
   7.137 +"--------- embed fun get_fillformula -----------------------------";
   7.138 +states := [];
   7.139 +CalcTree
   7.140 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], 
   7.141 +  ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
   7.142 +Iterator 1;
   7.143 +moveActiveRoot 1;
   7.144 +autoCalculate 1 CompleteCalcHead;
   7.145 +autoCalculate 1 (Step 1);
   7.146 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
   7.147 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
   7.148 +(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
   7.149 +  would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
   7.150 +  results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
   7.151 +  instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
   7.152 +findFillpatterns 1 "chain-rule-diff-both";
   7.153 +(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
   7.154 +  d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
   7.155 +
   7.156 +"~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) =
   7.157 +  (1, ("chain-rule-diff-both", "fill-both-args"));
   7.158 +val ((pt, _), _) = get_calc cI
   7.159 +val pos = get_pos cI 1; (* = ([1], Res)*)
   7.160 +
   7.161 +"~~~~~ fun get_fillformula, args:"; val ((pt, pos as (p, _)), (errpatID, fillpatID)) =
   7.162 +  ((pt, pos), (errpatID, fillpatID));
   7.163 +val fillforms = find_fillpatterns (pt, pos) errpatID
   7.164 +val fillforms =
   7.165 +  filter ((curry op = fillpatID) o (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms;
   7.166 +
   7.167 +val [(fillpatID, fillform, thm, subs_opt)] = fillforms;
   7.168 +case (fillpatID, fillform, thm, subs_opt) of
   7.169 + ("fill-both-args", tm, thm, subs_opt) => if term2str tm = 
   7.170       "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
   7.171       then () else error "get_fillformula changed 1a"
   7.172  | _ => error "get_fillformula changed 1b";

     8.1 --- a/test/Tools/isac/Interpret/rewtools.sml	Tue May 22 13:40:06 2012 +0200
     8.2 +++ b/test/Tools/isac/Interpret/rewtools.sml	Thu May 24 17:13:58 2012 +0200
     8.3 @@ -28,6 +28,7 @@
     8.4  "----------- fun filter_appl_rews -----------------------";
     8.5  "----------- fun is_contained_in ------------------------";
     8.6  ============ inhibit exn WN120321 ==============================================*)
     8.7 +"-------- build fun get_bdv_subst --------------------------------";
     8.8  "--------------------------------------------------------";
     8.9  "--------------------------------------------------------";
    8.10  
    8.11 @@ -161,8 +162,10 @@
    8.12    ["expand_binomtest", "make_polytest", "rearrange_assoc", "ac_plus_times", "norm_equation", 
    8.13     "matches", "isolate_bdv", "isolate_root", "tval_rls", "Test_simplify"]; (*..all rls in each*)
    8.14  
    8.15 +(* WN120523 popped up again ?!?!?
    8.16  if length (!ruleset') <> length ancestors_rls then ()
    8.17  else error "rewtools.sml: diff.behav. in thy_containing_rls 2 ERRATICAL?";
    8.18 +*)
    8.19  
    8.20  val rls' = "norm_Poly";
    8.21  case assoc (ancestors_rls, rls') of
    8.22 @@ -563,3 +566,37 @@
    8.23  
    8.24  ============ inhibit exn WN120321 ==============================================*)
    8.25  
    8.26 +"-------- build fun get_bdv_subst --------------------------------";
    8.27 +"-------- build fun get_bdv_subst --------------------------------";
    8.28 +"-------- build fun get_bdv_subst --------------------------------";
    8.29 +val {scr = Script prog, ...} = get_met ["diff", "differentiate_on_R"];
    8.30 +val env = [(str2term "v_v", str2term "x")];
    8.31 +subst2str env = "[\"\n(v_v, x)\"]";
    8.32 +
    8.33 +"~~~~~ fun get_bdv_subst, args:"; val (prog, env) = (prog, env);
    8.34 +    fun scan (Const _) = NONE
    8.35 +      | scan (Free _) = NONE
    8.36 +      | scan (Var _) = NONE
    8.37 +      | scan (Bound _) = NONE
    8.38 +      | scan (t as Const ("List.list.Cons", _) $
    8.39 +         (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) =
    8.40 +           if is_bdv_subst t then SOME t else NONE
    8.41 +      | scan (Abs (_, _, body)) = scan body
    8.42 +      | scan (t1 $ t2) =
    8.43 +          case scan t1 of
    8.44 +            NONE => scan t2
    8.45 +          | SOME subst => SOME subst
    8.46 +
    8.47 +val SOME tm = scan prog;
    8.48 +val subst = tm |> subst_atomic env |> isalist2list |> map isapair2pair: subst;
    8.49 +if term2str tm = "[(bdv, v_v)]" then () else error "get_bdv_subst changed 1";
    8.50 +
    8.51 +if subst2subs subst = ["(bdv, x)"] then () else error "get_bdv_subst changed 2";
    8.52 +
    8.53 +case get_bdv_subst prog env of
    8.54 +  (SOME ["(bdv, x)"], [(Free ("bdv", _), Free ("x", _))]: subst) => ()
    8.55 +| _ => error "get_bdv_subst changed 3";
    8.56 +
    8.57 +val (SOME subs, _) = get_bdv_subst prog env;
    8.58 +Rewrite_Inst (subs, ("diff_sin_chain","")) (*<<<----- this is the intended usage*)
    8.59 +

     9.1 --- a/test/Tools/isac/ProgLang/scrtools.sml	Tue May 22 13:40:06 2012 +0200
     9.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml	Thu May 24 17:13:58 2012 +0200
     9.3 @@ -9,7 +9,6 @@
     9.4  "-------- test the same called by interSteps norm_Poly -----------";
     9.5  "-------- test the same called by interSteps norm_Rational -------";
     9.6  "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
     9.7 -"-------- build fun get_bdv_subst --------------------------------";
     9.8  "-----------------------------------------------------------------";
     9.9  "-----------------------------------------------------------------";
    9.10  "-----------------------------------------------------------------";
    9.11 @@ -188,13 +187,4 @@
    9.12  init_istate (Rewrite_Set_Inst (["(bdv, x)"], "integration_rules")) 
    9.13  			      (str2term "someTermWithBdv");
    9.14  
    9.15 -"-------- build fun get_bdv_subst --------------------------------";
    9.16 -"-------- build fun get_bdv_subst --------------------------------";
    9.17 -"-------- build fun get_bdv_subst --------------------------------";
    9.18 -val {scr = Script prog, ...} = get_met ["diff", "differentiate_on_R"];
    9.19 -val env = [(str2term "v_v", str2term "x")];
    9.20 -subst2str env = "[\"\n(v_v, x)\"]";
    9.21  
    9.22 -if subst2str (get_bdv_subst prog env) = "[\"\n(bdv, x)\"]" then ()
    9.23 -else error "get_bdv_subst changed";
    9.24 -

    10.1 --- a/test/Tools/isac/Test_Some.thy	Tue May 22 13:40:06 2012 +0200
    10.2 +++ b/test/Tools/isac/Test_Some.thy	Thu May 24 17:13:58 2012 +0200
    10.3 @@ -12,7 +12,7 @@
    10.4  *}
    10.5  ML {* (*================== --> test/../inform.sml*)
    10.6  "--------- UC errpat, fillpat ---------------------------"; (*--> test/../interface.sml*)
    10.7 -"--------- embed fun get_fillform --------------------------------"; (*--> test/../inform.sml*)
    10.8 +"--------- build fun is_exactly_equal, .....----------------------"; (*--> test/../inform.sml*)
    10.9  states := [];
   10.10  CalcTree
   10.11  [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], 
   10.12 @@ -22,17 +22,62 @@
   10.13  autoCalculate 1 CompleteCalcHead;
   10.14  autoCalculate 1 (Step 1);
   10.15  autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
   10.16 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
   10.17 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; (*<<<<<<<=========================*)
   10.18  (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
   10.19    would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
   10.20    results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
   10.21    instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
   10.22 -FindFillpatterns 1 "chain-rule-diff-both";
   10.23 +  val ((pt,pos), _) = get_calc 1;
   10.24 +  val p = get_pos 1 1;
   10.25 +  val (Form f, tac, asms) = pt_extract (pt, p);
   10.26 +  if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then ()
   10.27 +  else error "embed fun get_fillform changed 1";
   10.28 +
   10.29 +findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
   10.30  (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
   10.31    d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
   10.32 +  val ((pt,pos),_) = get_calc 1;
   10.33 +  val p = get_pos 1 1;
   10.34 +  val (Form f, tac, asms) = pt_extract (pt, p);
   10.35 +  if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then ()
   10.36 +  else error "embed fun get_fillform changed 2";
   10.37 +
   10.38 +requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
   10.39 +  (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
   10.40 +  val ((pt,pos),_) = get_calc 1;
   10.41 +  val p = get_pos 1 1;
   10.42 +  val (Form f, tac, asms) = pt_extract (pt, p);
   10.43 +  if p = ([1], Res) andalso existpt [2] pt andalso
   10.44 +    term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
   10.45 +    tac = SOME (Rewrite ("fill-both-args", "")) then ()
   10.46 +  else error "embed fun get_fillform changed 3";
   10.47  *}
   10.48  ML {*
   10.49 -requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");
   10.50 +(* input a formula which exactly fills the gaps in a "fillformula"
   10.51 +   presented to the learner immediately before by requestFillformula (errpatID, fillpatID):
   10.52 +   errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.
   10.53 +   the respective thm is in the ctree ................
   10.54 +*)
   10.55 +"~~~~~ fun inputFillFormula, args:"; val (cI, ifo) =
   10.56 +  (1, "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)");
   10.57 +    val ((pt, _), _) = get_calc cI
   10.58 +    val pos as (p, p_) = get_pos cI 1;
   10.59 +"~~~~~ fun is_exactly_equal, args:"; val () = ();
   10.60 +
   10.61 +*}
   10.62 +ML {*
   10.63 +get_obj g_tac pt (lev_on p)
   10.64 +*}
   10.65 +ML {*
   10.66 +Rewrite_Inst
   10.67 +*}
   10.68 +ML {*
   10.69 +val Appl (rewtac as Rewrite' (_, _, _, _, _, _, (res, _))) =
   10.70 +  applicable_in pos pt (Rewrite ("diff_sin_chain", "")); (*get*)
   10.71 +*}
   10.72 +text {*
   10.73 +(thmID_of_derivation_name o Thm.get_name_hint) thm;
   10.74 +thmID_of_derivation_name
   10.75  *}
   10.76  ML {*
   10.77  *}
   10.78 @@ -40,7 +85,18 @@
   10.79  *}
   10.80  ML {*
   10.81  *}
   10.82 +ML {* (*================== changed here, not in code*)
   10.83 +*}
   10.84  ML {* (*==================*)
   10.85 +
   10.86 +*}
   10.87 +ML {*
   10.88 +*}
   10.89 +ML {*
   10.90 +*}
   10.91 +ML {* (*==================*)
   10.92 +*}
   10.93 +ML {*
   10.94  *}
   10.95  ML {*
   10.96  *}