1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Thu Apr 23 15:48:31 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Fri Apr 24 08:51:05 2020 +0200
1.3 @@ -26,7 +26,7 @@
1.4 ML_file "exec-def.sml" (*rename identifiers by use of struct.id*)
1.5 ML_file "rewrite-order.sml" (*rename identifiers by use of struct.id*)
1.6 ML_file rule.sml
1.7 -ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*)
1.8 +ML_file "error-pattern-def.sml"
1.9 ML_file "rule-set.sml"
1.10
1.11 ML_file "store.sml"
1.12 @@ -71,7 +71,7 @@
1.13 val add_mets: (Meth_Def.T * Spec.id) list -> theory -> theory
1.14 val get_thes: theory -> (Thy_Html.thydata Store.node) list
1.15 val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.16 - val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
1.17 + val insert_fillpats: (Thy_Html.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
1.18 val get_ref_thy: unit -> theory
1.19 val set_ref_thy: theory -> unit
1.20 end;
2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Thu Apr 23 15:48:31 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Fri Apr 24 08:51:05 2020 +0200
2.3 @@ -17,7 +17,7 @@
2.4 val maxthy: theory -> theory -> theory
2.5
2.6 type pbt_ = string * (term * term)
2.7 - val update_hrls: Thy_Html.thydata -> Error_Fill_Def.errpatID list -> Thy_Html.thydata
2.8 + val update_hrls: Thy_Html.thydata -> Error_Pattern_Def.id list -> Thy_Html.thydata
2.9
2.10 (*/------- to ? from Celem -------\*)
2.11 val knowthys: unit -> theory list
3.1 --- a/src/Tools/isac/BaseDefinitions/error-fill-def.sml Thu Apr 23 15:48:31 2020 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,49 +0,0 @@
3.4 -(* Title: BaseDefinitions/error-pattern-def.sml
3.5 - Author: Walther Neuper
3.6 - (c) due to copyright terms
3.7 -
3.8 -ODO: use "Error_Fill_Def" for renaming identifiers -- go back to Rule_Def.*
3.9 -*)
3.10 -signature ERROR_FILL_PATTERN_DEFINITION =
3.11 -sig
3.12 - eqtype errpatID
3.13 - type errpat = errpatID * term list * thm list
3.14 - val errpats2str : errpat list -> string
3.15 - type fillpatID
3.16 - type fillpat
3.17 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.18 - (*NONE*)
3.19 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.20 - (*NONE*)
3.21 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.22 -end
3.23 -
3.24 -(**)
3.25 -structure Error_Fill_Def(**): ERROR_FILL_PATTERN_DEFINITION(**) =
3.26 -struct
3.27 -(**)
3.28 -
3.29 -type errpatID = Rule_Def.errpatID
3.30 -
3.31 -type errpat =
3.32 - errpatID (* one identifier for a list of patterns
3.33 - DESIGN ?TODO: errpatID list for hierarchy of errpats ? *)
3.34 - * term list (* error patterns *)
3.35 - * thm list (* thms related to error patterns; note that respective lhs
3.36 - do not match (which reflects student's error).
3.37 - fillpatterns are stored with these thms. *)
3.38 -fun errpat2str (id, tms, thms) =
3.39 - "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC_Def.string_of_thms thms
3.40 -fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
3.41 -
3.42 -(* for (at least) 2 kinds of access:
3.43 - (1) given an errpatID, find the respective fillpats (e.g. in fun find_fill_pats)
3.44 - (2) given a thm, find respective fillpats *)
3.45 -type fillpatID = string
3.46 -type fillpat =
3.47 - fillpatID (* DESIGN ?TODO: give an order w.r.t difficulty ? *)
3.48 - * term (* the pattern with fill-in gaps *)
3.49 - * errpatID; (* which the fillpat would be a help for
3.50 - DESIGN ?TODO: list for several patterns ? *)
3.51 -
3.52 -(**)end(**)
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Tools/isac/BaseDefinitions/error-pattern-def.sml Fri Apr 24 08:51:05 2020 +0200
4.3 @@ -0,0 +1,42 @@
4.4 +(* Title: BaseDefinitions/error-pattern-def.sml
4.5 + Author: Walther Neuper
4.6 + (c) due to copyright terms
4.7 +*)
4.8 +signature ERROR_PATTERN_DEFINITION =
4.9 +sig
4.10 + eqtype id
4.11 + type T = id * term list * thm list
4.12 + val s_to_string : T list -> string
4.13 +
4.14 + type fill_in_id
4.15 + type fill_in
4.16 +end
4.17 +
4.18 +(**)
4.19 +structure Error_Pattern_Def(**): ERROR_PATTERN_DEFINITION(**) =
4.20 +struct
4.21 +(**)
4.22 +
4.23 +type id = Rule_Def.errpatID
4.24 +
4.25 +type T =
4.26 + id (* one identifier for a list of patterns *)
4.27 + * term list (* error patterns *)
4.28 + * thm list (* thms related to error patterns; note that respective lhs
4.29 + do not match (which reflects student's error).
4.30 + fillpatterns are stored with these thms. *)
4.31 +fun errpat2str (id, tms, thms) =
4.32 + "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC_Def.string_of_thms thms
4.33 +fun s_to_string errpats = (strs2str' o (map errpat2str)) errpats
4.34 +
4.35 +(* for (at least) 2 kinds of access:
4.36 + (1) given an id, find the respective fill_in's (e.g. in fun find_fill_patterns)
4.37 + (2) given a thm, find respective fill_in's *)
4.38 +type fill_in_id = string
4.39 +type fill_in =
4.40 + fill_in_id (* DESIGN ?TODO: give an order w.r.t difficulty ? *)
4.41 + * term (* the pattern with fill-in gaps *)
4.42 + * id; (* which the fill_in would be a help for
4.43 + DESIGN ?TODO: list for several patterns ? *)
4.44 +
4.45 +(**)end(**)
5.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml Thu Apr 23 15:48:31 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Fri Apr 24 08:51:05 2020 +0200
5.3 @@ -48,7 +48,7 @@
5.4 srls : Rule_Set.T, (* for evaluating list expressions in scr *)
5.5 crls : Rule_Set.T, (* for check_elementwise, ie. formulae in calc. *)
5.6 nrls : Rule_Set.T, (* canonical simplifier specific for this met *)
5.7 - errpats : Error_Fill_Def.errpat list,(* error patterns expected in this method *)
5.8 + errpats : Error_Pattern_Def.T list,(* error patterns expected in this method *)
5.9 calc : Rule_Def.calc list, (* Theory_Data in fun prep_met *)
5.10 (*branch : TransitiveB set in append_problem at generation ob pblobj *)
5.11 scr : Rule.program, (* progam, empty as @{thm refl} or Rfuns *)
6.1 --- a/src/Tools/isac/BaseDefinitions/thy-html.sml Thu Apr 23 15:48:31 2020 +0200
6.2 +++ b/src/Tools/isac/BaseDefinitions/thy-html.sml Fri Apr 24 08:51:05 2020 +0200
6.3 @@ -11,7 +11,7 @@
6.4 = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
6.5 | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rule_Def.rew_ord_}
6.6 | Hrls of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
6.7 - | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Check_Unique.id, mathauthors: authors, thm: thm}
6.8 + | Hthm of {coursedesign: authors, fillpats: Error_Pattern_Def.fill_in list, guh: Check_Unique.id, mathauthors: authors, thm: thm}
6.9 | Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}
6.10 type theID
6.11 val theID2str: string list -> string
6.12 @@ -29,7 +29,7 @@
6.13 val theID2guh: theID -> Check_Unique.id
6.14
6.15 val add_thydata: string list * string list -> thydata -> thydata Store.T -> thydata Store.T
6.16 - val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
6.17 + val update_hthm: thydata -> Error_Pattern_Def.fill_in list -> thydata
6.18 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.19 (*NONE*)
6.20 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.21 @@ -54,7 +54,7 @@
6.22 (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
6.23 datatype thydata =
6.24 Html of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, html: string}
6.25 -| Hthm of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
6.26 +| Hthm of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, fillpats: Error_Pattern_Def.fill_in list,
6.27 thm: thm} (* here no sym_thm, thus no thmID required *)
6.28 | Hrls of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
6.29 | Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
7.1 --- a/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Thu Apr 23 15:48:31 2020 +0200
7.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Fri Apr 24 08:51:05 2020 +0200
7.3 @@ -124,7 +124,7 @@
7.4 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
7.5 XML.Elem (("MESSAGE", []), [XML.Text e])])
7.6
7.7 -fun fetchproposedtacticOK2xml (calcid : calcID) tac (errpatIDs : Error_Fill_Def.errpatID list) =
7.8 +fun fetchproposedtacticOK2xml (calcid : calcID) tac (errpatIDs : Error_Pattern_Def.id list) =
7.9 XML.Elem (("NEXTTAC", []), [
7.10 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
7.11 XML.Elem (("TACTICERRORPATTERNS", []), [xml_of_strs errpatIDs]),
8.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Thu Apr 23 15:48:31 2020 +0200
8.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Fri Apr 24 08:51:05 2020 +0200
8.3 @@ -19,7 +19,7 @@
8.4 val DEconstrCalcTree : calcID -> XML.tree
8.5 val fetchApplicableTactics : calcID -> int -> Pos.pos' -> XML.tree
8.6 val fetchProposedTactic : calcID -> XML.tree
8.7 - val findFillpatterns : calcID -> Error_Fill_Def.errpatID -> XML.tree
8.8 + val findFillpatterns : calcID -> Error_Pattern_Def.id -> XML.tree
8.9 val getAccumulatedAsms : calcID -> Pos.pos' -> XML.tree
8.10 val getActiveFormula : calcID -> XML.tree
8.11 val getAssumptions : calcID -> Pos.pos' -> XML.tree
8.12 @@ -49,7 +49,7 @@
8.13 val refFormula : calcID -> Pos.pos' -> XML.tree
8.14 val refineProblem : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
8.15 val replaceFormula : calcID -> TermC.as_string -> XML.tree
8.16 - val requestFillformula : calcID -> Error_Fill_Def.errpatID * Error_Fill_Def.fillpatID -> XML.tree
8.17 + val requestFillformula : calcID -> Error_Pattern_Def.id * Error_Pattern_Def.fill_in_id -> XML.tree
8.18 val resetCalcHead : calcID -> XML.tree
8.19 val setContext : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
8.20 val setMethod : calcID -> Method.id -> XML.tree
8.21 @@ -164,7 +164,7 @@
8.22 let
8.23 val _= upd_tacis cI tacis
8.24 val (tac, _, _) = last_elem tacis
8.25 - in fetchproposedtacticOK2xml cI tac (Error_Fill_Pattern.fetchErrorpatterns tac) end
8.26 + in fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store tac) end
8.27 | ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
8.28 | ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
8.29 | ("end-of-calculation", _) =>
8.30 @@ -654,13 +654,15 @@
8.31 ) handle _ => sysERROR2xml cI "error in kernel 36")
8.32 | str => sysERROR2xml cI ("checkContext: str = " ^ str)
8.33
8.34 -(* for an errpatID find "(fillpatID, fillform)" list
8.35 - which dedicated to this errpat and which is applicable at current formula *)
8.36 +(*
8.37 + for an Error_Pattern.id find "(fill_in_id * fill_in) list"
8.38 + which is applicable to the current formula.
8.39 +*)
8.40 fun findFillpatterns cI errpatID =
8.41 let
8.42 val ((pt, _), _) = get_calc cI
8.43 val pos = get_pos cI 1;
8.44 - val fillpats = Error_Fill_Pattern.find_fillpatterns (pt, pos) errpatID
8.45 + val fillpats = Error_Pattern.find_fill_patterns (pt, pos) errpatID
8.46 in findFillpatterns2xml cI (map #1 fillpats) end
8.47
8.48 (* given a fillpatID propose a fillform to the learner on the worksheet;
8.49 @@ -673,10 +675,10 @@
8.50 let
8.51 val ((pt, _), _) = get_calc cI
8.52 val pos = get_pos cI 1
8.53 - val fillforms = Error_Fill_Pattern.find_fillpatterns (pt, pos) errpatID
8.54 + val fillforms = Error_Pattern.find_fill_patterns (pt, pos) errpatID
8.55 in
8.56 case filter ((curry op = fillpatID) o
8.57 - (#1: (Error_Fill_Def.fillpatID * term * thm * (Selem.subs option) -> Error_Fill_Def.fillpatID))) fillforms of
8.58 + (#1: (Error_Pattern_Def.fill_in_id * term * thm * (Selem.subs option) -> Error_Pattern_Def.fill_in_id))) fillforms of
8.59 (_, fillform, thm, sube_opt) :: _ =>
8.60 let
8.61 val (pt, pos') = Generate.generate_inconsistent_rew (sube_opt, ThmC.of_thm thm)
8.62 @@ -697,7 +699,7 @@
8.63 val ((pt, _), _) = get_calc cI
8.64 val pos = get_pos cI 1;
8.65 in
8.66 - case Error_Fill_Pattern.is_exactly_equal (pt, pos) ifo of
8.67 + case Error_Pattern.filled_exactly (pt, pos) ifo of
8.68 ("ok", tac) =>
8.69 let
8.70 in (* cp from applyTactic *)
9.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Apr 23 15:48:31 2020 +0200
9.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Fri Apr 24 08:51:05 2020 +0200
9.3 @@ -15,7 +15,7 @@
9.4 val collect_thms: string -> theory -> (Thy_Html.theID * Thy_Html.thydata) list
9.5
9.6 val hierarchy_guh: 'a Store.T -> string
9.7 - val insert_errpatIDs: 'a -> Thy_Html.theID -> Error_Fill_Def.errpatID list ->
9.8 + val insert_errpatIDs: 'a -> Thy_Html.theID -> Error_Pattern_Def.id list ->
9.9 Thy_Html.thydata * Thy_Html.theID
9.10
9.11 val makeHcal: string * ThyC.id -> string * Rule_Def.calc -> Thy_Html.theID * Thy_Html.thydata
10.1 --- a/src/Tools/isac/Interpret/Interpret.thy Thu Apr 23 15:48:31 2020 +0200
10.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Fri Apr 24 08:51:05 2020 +0200
10.3 @@ -12,7 +12,7 @@
10.4 ML_file istate.sml
10.5 ML_file "sub-problem.sml"
10.6 ML_file rewtools.sml
10.7 - ML_file "error-fill-pattern.sml"
10.8 + ML_file "error-pattern.sml"
10.9 ML_file derive.sml
10.10 ML_file "li-tool.sml"
10.11 ML_file "lucas-interpreter.sml"
11.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 23 15:48:31 2020 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,175 +0,0 @@
11.4 -(* Handle user-input during the specify- and the solve-phase.
11.5 - author: Walther Neuper
11.6 - 0603
11.7 - (c) due to copyright terms
11.8 -
11.9 -In case a term is input, which contains an "error pattern" (provided by a mathauthor),
11.10 -several "fill patterns" can be presented as help for the next step.)
11.11 -*)
11.12 -
11.13 -signature ERROR_FILL_PATTERN =
11.14 -sig
11.15 - type errpatID = Rule_Def.errpatID
11.16 - type errpat = errpatID * term list * thm list
11.17 - val errpats2str : errpat list -> string
11.18 -
11.19 - val find_fillpatterns : Calc.T -> Error_Fill_Def.errpatID ->
11.20 - (Error_Fill_Def.fillpatID * term * thm * Selem.subs option) list
11.21 - val fetchErrorpatterns : Tactic.input -> Error_Fill_Def.errpatID list
11.22 - val is_exactly_equal : Calc.T -> string -> string * Tactic.input
11.23 - val check_for : term * term -> term * (term * term) list ->
11.24 - (Error_Fill_Def.errpatID * term list * 'a list) list * Rule_Set.T ->
11.25 - Error_Fill_Def.errpatID option
11.26 -
11.27 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.28 - (* NONE *)
11.29 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
11.30 - val check_err_patt : term * term -> UnparseC.subst -> Error_Fill_Def.errpatID * term -> Rule_Set.T -> Error_Fill_Def.errpatID option
11.31 - val get_fillform :
11.32 - 'a * (term * term) list -> 'b * term -> Error_Fill_Def.errpatID -> Error_Fill_Def.fillpat -> (Error_Fill_Def.fillpatID * term * 'b * 'a) option
11.33 - val get_fillpats :
11.34 - 'a * (term * term) list -> term -> Error_Fill_Def.errpatID -> thm -> (Error_Fill_Def.fillpatID * term * thm * 'a) list
11.35 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
11.36 -
11.37 -end
11.38 -(**)
11.39 -structure Error_Fill_Pattern(**): ERROR_FILL_PATTERN(**) =
11.40 -struct
11.41 -(**)
11.42 -
11.43 -type errpatID = Rule_Def.errpatID
11.44 -
11.45 -
11.46 -(* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
11.47 -fun check_err_patt (res, inf) subst (errpatID, pat) rls =
11.48 - let
11.49 - val (res', _, _, rewritten) =
11.50 - Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
11.51 - in
11.52 - if rewritten then
11.53 - let
11.54 - val norm_res = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls res' of
11.55 - NONE => res'
11.56 - | SOME (norm_res, _) => norm_res
11.57 - val norm_inf = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls inf of
11.58 - NONE => inf
11.59 - | SOME (norm_inf, _) => norm_inf
11.60 - in if norm_res = norm_inf then SOME errpatID else NONE
11.61 - end
11.62 - else NONE
11.63 - end;
11.64 -
11.65 -(*
11.66 - check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
11.67 - (prog, env) for retrieval of casual substitution for bdv in the pattern.
11.68 -*)
11.69 -fun check_for (res, inf) (prog, env) (errpats, rls) =
11.70 - let
11.71 - val (_, subst) = Rtools.get_bdv_subst prog env
11.72 - fun scan (_, [], _) = NONE
11.73 - | scan (errpatID, errpat :: errpats, _) =
11.74 - case check_err_patt (res, inf) subst (errpatID, errpat) rls of
11.75 - NONE => scan (errpatID, errpats, [])
11.76 - | SOME errpatID => SOME errpatID
11.77 - fun scans [] = NONE
11.78 - | scans (group :: groups) =
11.79 - case scan group of
11.80 - NONE => scans groups
11.81 - | SOME errpatID => SOME errpatID
11.82 - in scans errpats end;
11.83 -
11.84 -(* fill-in patterns an forms.
11.85 - returns thm required by "fun in_fillform *)
11.86 -fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) =
11.87 - let
11.88 - val (form', _, _, rewritten) =
11.89 - Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
11.90 - in (*the fillpat of the thm must be dedicated to errpatID*)
11.91 - if errpatID = erpaID andalso rewritten then
11.92 - SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
11.93 - else NONE
11.94 - end
11.95 -
11.96 -fun get_fillpats subst form errpatID thm =
11.97 - let
11.98 - val thmDeriv = Thm.get_name_hint thm
11.99 - val (part, thyID) = Rtools.thy_containing_thm thmDeriv
11.100 - val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
11.101 - val fillpats = case Specify.get_the theID of
11.102 - Thy_Html.Hthm {fillpats, ...} => fillpats
11.103 - | _ => error "get_fillpats: uncovered case of get_the"
11.104 - val some = map (get_fillform subst (thm, form) errpatID) fillpats
11.105 - in some |> filter is_some |> map the end
11.106 -
11.107 -fun find_fillpatterns (pt, pos as (p, _): Pos.pos') errpatID =
11.108 - let
11.109 - val f_curr = Ctree.get_curr_formula (pt, pos);
11.110 - val pp = Ctree.par_pblobj pt p
11.111 - val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
11.112 - {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
11.113 - | _ => error "find_fillpatterns: uncovered case of get_met"
11.114 - val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
11.115 - val subst = Rtools.get_bdv_subst prog env
11.116 - val errpatthms = errpats
11.117 - |> filter ((curry op = errpatID) o (#1: Error_Fill_Def.errpat -> Error_Fill_Def.errpatID))
11.118 - |> map (#3: Error_Fill_Def.errpat -> thm list)
11.119 - |> flat
11.120 - in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end
11.121 -
11.122 -(* check if an input formula is exactly equal to the rewrite from a rule
11.123 - which is stored at the pos where the input is stored of "ok". *)
11.124 -fun is_exactly_equal (pt, pos as (p, _)) istr =
11.125 - case TermC.parseNEW (ThyC.get_theory "Isac_Knowledge" |> ThyC.to_ctxt) istr of
11.126 - NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
11.127 - | SOME ifo =>
11.128 - let
11.129 - val p' = Pos.lev_on p;
11.130 - val tac = Ctree.get_obj Ctree.g_tac pt p';
11.131 - in
11.132 - case Applicable.applicable_in pos pt tac of
11.133 - Applicable.Notappl msg => (msg, Tactic.Tac "")
11.134 - | Applicable.Appl rew =>
11.135 - let
11.136 - val res = case rew of
11.137 - Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
11.138 - |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
11.139 - | t => error ("is_exactly_equal: uncovered case for " ^ Tactic.string_of t)
11.140 - in
11.141 - if not (ifo = res) then
11.142 - ("input does not exactly fill the gaps", Tactic.Tac "")
11.143 - else ("ok", tac)
11.144 - end
11.145 - end
11.146 -
11.147 -(* fetch errpatIDs from an arbitrary tactic *)
11.148 -fun fetchErrorpatterns tac =
11.149 - let
11.150 - val rlsID =
11.151 - case tac of
11.152 - Tactic.Rewrite_Set rlsID => rlsID
11.153 - |Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID
11.154 - | _ => "empty"
11.155 - val (part, thyID) = Rtools.thy_containing_rls "Isac_Knowledge" rlsID;
11.156 - val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
11.157 - Thy_Html.Hrls {thy_rls = (_, rls), ...} => rls
11.158 - | _ => error "fetchErrorpatterns: uncovered case of get_the"
11.159 - in case rls of
11.160 - Rule_Def.Repeat {errpatts, ...} => errpatts
11.161 - | Rule_Set.Sequence {errpatts, ...} => errpatts
11.162 - | Rule_Set.Rrls {errpatts, ...} => errpatts
11.163 - | Rule_Set.Empty => []
11.164 - end
11.165 -
11.166 -type errpatID = Rule_Def.errpatID
11.167 -type errpat =
11.168 - errpatID (* one identifier for a list of patterns
11.169 - DESIGN ?TODO: errpatID list for hierarchy of errpats ? *)
11.170 - * term list (* error patterns *)
11.171 - * thm list (* thms related to error patterns; note that respective lhs
11.172 - do not match (which reflects student's error).
11.173 - fillpatterns are stored with these thms. *)
11.174 -fun errpat2str (id, tms, thms) =
11.175 - "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC.string_of_thms thms
11.176 -fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
11.177 -
11.178 -(**)end(**)
11.179 \ No newline at end of file
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Fri Apr 24 08:51:05 2020 +0200
12.3 @@ -0,0 +1,174 @@
12.4 +(* title: Interpret/error-pattern.sml
12.5 + author: Walther Neuper
12.6 + 0603
12.7 + (c) due to copyright terms
12.8 +
12.9 +In case a term is input, which contains an "error pattern" (provided by a mathauthor),
12.10 +several "fill patterns" can be presented as help for the next step.)
12.11 +*)
12.12 +
12.13 +signature ERROR_PATTERN =
12.14 +sig
12.15 + type id = Error_Pattern_Def.id
12.16 + type T = Error_Pattern_Def.T
12.17 + val s_to_string : T list -> string
12.18 +
12.19 + type fill_in_id = Error_Pattern_Def.fill_in_id
12.20 + type fill_in = Error_Pattern_Def.fill_in
12.21 + type record
12.22 +
12.23 + val from_store: Tactic.input -> Error_Pattern_Def.id list
12.24 + val filled_exactly: Calc.T -> string -> string * Tactic.input
12.25 + val check_for: term * term -> term * Env.T -> T list * Rule_Set.T -> id option
12.26 +
12.27 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
12.28 + val find_fill_patterns: Calc.T -> id -> record list
12.29 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
12.30 + val check_for': term * term -> UnparseC.subst -> id * term -> Rule_Set.T -> id option
12.31 + val fill_from_store: Selem.subs option * (term * term) list -> term -> id -> thm ->
12.32 + record list
12.33 + val fill_form: Selem.subs option * (term * term) list -> thm * term -> id -> fill_in ->
12.34 + record option
12.35 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
12.36 +end
12.37 +
12.38 +(**)
12.39 +structure Error_Pattern(**): ERROR_PATTERN(**) =
12.40 +struct
12.41 +(**)
12.42 +
12.43 +type id = Error_Pattern_Def.id;
12.44 +type T = Error_Pattern_Def.T;
12.45 +val s_to_string = Error_Pattern_Def.s_to_string;
12.46 +
12.47 +type fill_in_id = Error_Pattern_Def.fill_in_id;
12.48 +type fill_in = Error_Pattern_Def.fill_in;
12.49 +type record = (fill_in_id * term * thm * Selem.subs option);
12.50 +
12.51 +(*
12.52 + check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls
12.53 +*)
12.54 +fun check_for' (res, inf) subst (id, pat) rls =
12.55 + let
12.56 + val (res', _, _, rewritten) = Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord
12.57 + Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
12.58 + in
12.59 + if rewritten then
12.60 + let
12.61 + val norm_res = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls res' of
12.62 + NONE => res'
12.63 + | SOME (norm_res, _) => norm_res
12.64 + val norm_inf = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls inf of
12.65 + NONE => inf
12.66 + | SOME (norm_inf, _) => norm_inf
12.67 + in
12.68 + if norm_res = norm_inf then SOME id else NONE
12.69 + end
12.70 + else NONE
12.71 + end;
12.72 +
12.73 +(*
12.74 + check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
12.75 + (prog, env) for retrieval of casual substitution for bdv in the pattern.
12.76 +*)
12.77 +fun check_for (res, inf) (prog, env) (errpats, rls) =
12.78 + let
12.79 + val (_, subst) = Rtools.get_bdv_subst prog env
12.80 + fun scan (_, [], _) = NONE
12.81 + | scan (id, T :: errpats, _) =
12.82 + case check_for' (res, inf) subst (id, T) rls of
12.83 + NONE => scan (id, errpats, [])
12.84 + | SOME id => SOME id
12.85 + fun scans [] = NONE
12.86 + | scans (group :: groups) =
12.87 + case scan group of
12.88 + NONE => scans groups
12.89 + | SOME id => SOME id
12.90 + in scans errpats end;
12.91 +
12.92 +(* fill-in patterns an forms.
12.93 + returns thm required by "fun in_fillform *)
12.94 +fun fill_form (subs_opt, subst) (thm, form) id (fillpatID, pat, erpaID) =
12.95 + let
12.96 + val (form', _, _, rewritten) =
12.97 + Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
12.98 + in (*the fillpat of the thm must be dedicated to id*)
12.99 + if id = erpaID andalso rewritten then
12.100 + SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
12.101 + else NONE
12.102 + end
12.103 +
12.104 +fun fill_from_store subst form id thm =
12.105 + let
12.106 + val thmDeriv = Thm.get_name_hint thm
12.107 + val (part, thyID) = Rtools.thy_containing_thm thmDeriv
12.108 + val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
12.109 + val fillpats = case Specify.get_the theID of
12.110 + Thy_Html.Hthm {fillpats, ...} => fillpats
12.111 + | _ => raise ERROR "fill_from_store: uncovered case of get_the"
12.112 + val some = map (fill_form subst (thm, form) id) fillpats
12.113 + in some |> filter is_some |> map the end
12.114 +
12.115 +fun find_fill_patterns (pt, pos as (p, _): Pos.pos') id =
12.116 + let
12.117 + val f_curr = Ctree.get_curr_formula (pt, pos);
12.118 + val pp = Ctree.par_pblobj pt p
12.119 + val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
12.120 + {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
12.121 + | _ => raise ERROR "find_fill_patterns: uncovered case of get_met"
12.122 + val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
12.123 + val subst = Rtools.get_bdv_subst prog env
12.124 + val errpatthms = errpats
12.125 + |> filter ((curry op = id) o (#1: Error_Pattern_Def.T -> Error_Pattern_Def.id))
12.126 + |> map (#3: Error_Pattern_Def.T -> thm list)
12.127 + |> flat
12.128 + in map (fill_from_store subst f_curr id) errpatthms |> flat end
12.129 +
12.130 +(*
12.131 + Check input on a fill-pattern:
12.132 + check if input is exactly equal to the rewrite from a rule
12.133 + which is stored at the pos where the input is stored of "ok".
12.134 +*)
12.135 +fun filled_exactly (pt, pos as (p, _)) istr =
12.136 + case TermC.parseNEW (ThyC.get_theory "Isac_Knowledge" |> ThyC.to_ctxt) istr of
12.137 + NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
12.138 + | SOME ifo =>
12.139 + let
12.140 + val p' = Pos.lev_on p;
12.141 + val tac = Ctree.get_obj Ctree.g_tac pt p';
12.142 + in
12.143 + case Applicable.applicable_in pos pt tac of
12.144 + Applicable.Notappl msg => (msg, Tactic.Tac "")
12.145 + | Applicable.Appl rew =>
12.146 + let
12.147 + val res = case rew of
12.148 + Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
12.149 + |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
12.150 + | t => raise ERROR ("filled_exactly: uncovered case for " ^ Tactic.string_of t)
12.151 + in
12.152 + if not (ifo = res) then
12.153 + ("input does not exactly fill the gaps", Tactic.Tac "")
12.154 + else ("ok", tac)
12.155 + end
12.156 + end
12.157 +
12.158 +(* fetch errpatIDs from an arbitrary tactic *)
12.159 +fun from_store tac =
12.160 + let
12.161 + val rlsID =
12.162 + case tac of
12.163 + Tactic.Rewrite_Set rlsID => rlsID
12.164 + |Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID
12.165 + | _ => "empty"
12.166 + val (part, thyID) = Rtools.thy_containing_rls "Isac_Knowledge" rlsID;
12.167 + val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
12.168 + Thy_Html.Hrls {thy_rls = (_, rls), ...} => rls
12.169 + | _ => raise ERROR "from_store: uncovered case of get_the"
12.170 + in case rls of
12.171 + Rule_Def.Repeat {errpatts, ...} => errpatts
12.172 + | Rule_Set.Sequence {errpatts, ...} => errpatts
12.173 + | Rule_Set.Rrls {errpatts, ...} => errpatts
12.174 + | Rule_Set.Empty => []
12.175 + end
12.176 +
12.177 +(**)end(**)
12.178 \ No newline at end of file
13.1 --- a/src/Tools/isac/Interpret/step-solve.sml Thu Apr 23 15:48:31 2020 +0200
13.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Fri Apr 24 08:51:05 2020 +0200
13.3 @@ -86,8 +86,8 @@
13.4 (*
13.5 Locate a step in a program, which has been determined by input of a term.
13.6 Special case: if the term is a CAS-command, then create a calchead, and do 1 step.
13.7 - If "no derivation found" then Error_Fill_Pattern.check_for.
13.8 - (Error_Fill_Pattern.check_for *within* compare_step seems too expensive)
13.9 + If "no derivation found" then Error_Pattern.check_for.
13.10 + (Error_Pattern.check_for *within* compare_step seems too expensive)
13.11 *)
13.12 (*fun by_term (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =*)
13.13 fun by_term (pt, pos as (p, _)) istr =
13.14 @@ -117,7 +117,7 @@
13.15 | _ => error "inform: uncovered case of get_met"
13.16 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
13.17 in
13.18 - case Error_Fill_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) of
13.19 + case Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) of
13.20 SOME errpatID => ("error pattern #" ^ errpatID ^ "#", Chead.e_calcstate')
13.21 | NONE => ("no derivation found", Chead.e_calcstate')
13.22 end
14.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Apr 23 15:48:31 2020 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Fri Apr 24 08:51:05 2020 +0200
14.3 @@ -135,7 +135,7 @@
14.4 ("fill-inner-deriv",
14.5 TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
14.6 ("fill-all",
14.7 - TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: Error_Fill_Def.fillpat list))
14.8 + TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: Error_Pattern_Def.fill_in list))
14.9 ]
14.10 \<close>
14.11
15.1 --- a/src/Tools/isac/Specify/ptyps.sml Thu Apr 23 15:48:31 2020 +0200
15.2 +++ b/src/Tools/isac/Specify/ptyps.sml Fri Apr 24 08:51:05 2020 +0200
15.3 @@ -53,7 +53,7 @@
15.4 Problem.T * Problem.id
15.5 val prep_met : theory -> string -> string list -> Problem.id ->
15.6 string list * (string * string list) list *
15.7 - {calc: 'a, crls: Rule_Set.T, errpats: Error_Fill_Def.errpat list, nrls: Rule_Set.T, prls: Rule_Set.T,
15.8 + {calc: 'a, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T, prls: Rule_Set.T,
15.9 rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T} * thm ->
15.10 Method.T * Method.id
15.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
15.12 @@ -62,7 +62,7 @@
15.13 datatype match' = Matches' of Model.item Model.ppc | NoMatch' of Model.item Model.ppc
15.14 val match_pbl : Selem.fmz_ -> Problem.T -> match'
15.15 val refine : Selem.fmz_ -> Problem.id -> Stool.match list
15.16 - val e_errpat : Error_Fill_Def.errpat
15.17 + val e_errpat : Error_Pattern_Def.T
15.18 val show_pblguhs : unit -> unit
15.19 val sort_pblguhs : unit -> unit
15.20 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
15.21 @@ -285,7 +285,7 @@
15.22 |> map flattup;
15.23 in (oris, ctxt) end;
15.24
15.25 -val e_errpat = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}]): Error_Fill_Def.errpat
15.26 +val e_errpat = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}]): Error_Pattern_Def.T
15.27 val e_fillpat = ("e_fillpatID", TermC.parse_patt @{theory} "?a = _", "e_errpatID")
15.28
15.29 (** breadth-first search on hierarchy of problem-types **)
16.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Apr 23 15:48:31 2020 +0200
16.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri Apr 24 08:51:05 2020 +0200
16.3 @@ -1466,9 +1466,9 @@
16.4
16.5 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
16.6 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
16.7 - ("diff_sum", thm)) => () | _ => error "embed fun get_fillform changed 0"
16.8 - | _ => error "embed fun get_fillform changed 1"
16.9 -else error "embed fun get_fillform changed 2";
16.10 + ("diff_sum", thm)) => () | _ => error "embed fun fill_form changed 0"
16.11 + | _ => error "embed fun fill_form changed 1"
16.12 +else error "embed fun fill_form changed 2";
16.13
16.14 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
16.15 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
16.16 @@ -1481,7 +1481,7 @@
16.17 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
16.18 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
16.19 then ()
16.20 - else error "embed fun get_fillform changed 2";
16.21 + else error "embed fun fill_form changed 2";
16.22
16.23 (* if we assume, that the fill-patterns are ordered such that the 1st has large gaps
16.24 and the last has no gaps, then the number of fill-patterns would suffice
16.25 @@ -1494,7 +1494,7 @@
16.26 if p = ([1], Res) andalso existpt [2] pt andalso
16.27 UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
16.28 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"))
16.29 - then () else error "embed fun get_fillform changed 3";
16.30 + then () else error "embed fun fill_form changed 3";
16.31
16.32 inputFillFormula 1 "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";(*<<<<<<<=====*)
16.33 val ((pt, _),_) = get_calc 1;
17.1 --- a/test/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 23 15:48:31 2020 +0200
17.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
17.3 @@ -1,1385 +0,0 @@
17.4 -(* Title: "Interpret/error-fill-pattern.sml"
17.5 - Author: Walther Neuper 060225,
17.6 - (c) due to copyright terms
17.7 -
17.8 -Strange ERROR "Undefined fact: "all_left""
17.9 -*)
17.10 -
17.11 -"-----------------------------------------------------------------";
17.12 -"table of contents -----------------------------------------------";
17.13 -"-----------------------------------------------------------------";
17.14 -"appendForm with miniscript with mini-subpbl:";
17.15 -"--------- appendFormula: on Res + equ_nrls ----------------------";
17.16 -"--------- appendFormula: on Frm + equ_nrls ----------------------";
17.17 -"--------- appendFormula: on Res + NO deriv ----------------------";
17.18 -"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
17.19 -"replaceForm with miniscript with mini-subpbl:";
17.20 -"--------- replaceFormula: on Res + = ----------------------------";
17.21 -"--------- replaceFormula: on Res + = 1st Nd ---------------------";
17.22 -"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
17.23 -"--------- replaceFormula: cut calculation -----------------------";
17.24 -"--------- replaceFormula: cut calculation -----------------------";
17.25 -(* 040307 copied from informtest.sml ... old versions
17.26 -"--------- maximum-example, UC: Modeling / modifyCalcHead --------";*)
17.27 -"--------- syntax error ------------------------------------------";
17.28 -"CAS-command:";
17.29 -"--------- CAS-command on ([],Pbl) -------------------------------";
17.30 -"--------- CAS-command on ([],Pbl) FE-interface ------------------";
17.31 -"--------- locate_input_term [rational,simplification] ----------------------";
17.32 -"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
17.33 -"--------- Take as 1st tac, start from exp -----------------------";
17.34 -"--------- implicit_take, start with <NEW> (CAS input) ---------------";
17.35 -"--------- build fun check_err_patt ------------------------------";
17.36 -"--------- build fun check_err_patt ?bdv -------------------------";
17.37 -"--------- build fun Error_Pattern.check_for ------------------------";
17.38 -"--------- embed fun Error_Pattern.check_for ------------------------";
17.39 -"--------- build fun get_fillpats --------------------------------";
17.40 -"--------- embed fun find_fillpatterns ---------------------------";
17.41 -"--------- build fun is_exactly_equal, inputFillFormula ----------";
17.42 -"--------- fun appl_adds -----------------------------------------";
17.43 -"--------- fun concat_deriv --------------------------------------";
17.44 -"--------- handle an input formula -------------------------------";
17.45 -"--------- fun dropwhile' ----------------------------------------";
17.46 -"-----------------------------------------------------------------";
17.47 -"-----------------------------------------------------------------";
17.48 -"-----------------------------------------------------------------";
17.49 -
17.50 -
17.51 -"--------- appendFormula: on Res + equ_nrls ----------------------";
17.52 -"--------- appendFormula: on Res + equ_nrls ----------------------";
17.53 -"--------- appendFormula: on Res + equ_nrls ----------------------";
17.54 - val Prog sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
17.55 - (writeln o UnparseC.term) sc;
17.56 - val Prog sc = (#scr o get_met) ["Test","solve_linear"];
17.57 - (writeln o UnparseC.term) sc;
17.58 -
17.59 - reset_states ();
17.60 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
17.61 - ("Test", ["sqroot-test","univariate","equation","test"],
17.62 - ["Test","squ-equ-test-subpbl1"]))];
17.63 - Iterator 1; moveActiveRoot 1;
17.64 - autoCalculate 1 CompleteCalcHead;
17.65 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
17.66 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
17.67 -
17.68 - appendFormula 1 "-2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1);
17.69 - val ((pt,_),_) = get_calc 1;
17.70 - val str = pr_ctree pr_short pt;
17.71 -if str =
17.72 -(". ----- pblobj -----\n" ^
17.73 -"1. x + 1 = 2\n" ^
17.74 -"2. x + 1 + -1 * 2 = 0\n" ^
17.75 -"2.1. x + 1 + -1 * 2 = 0\n" ^
17.76 -"2.2. 1 + x + -1 * 2 = 0\n" ^
17.77 -"2.3. 1 + (x + -1 * 2) = 0\n" ^
17.78 -"2.4. 1 + (x + -2) = 0\n" ^
17.79 -"2.5. 1 + (x + -2 * 1) = 0\n" ^
17.80 -"2.6. 1 + x + -2 * 1 = 0\n" ) then ()
17.81 -else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
17.82 -
17.83 - moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
17.84 - moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
17.85 -
17.86 - (*the seven steps of detailed derivation*)
17.87 - moveDown 1 ([1 ],Res); refFormula 1 ([2,1],Frm);
17.88 - moveDown 1 ([2,1],Frm); refFormula 1 ([2,1],Res);
17.89 - moveDown 1 ([2,1],Res); refFormula 1 ([2,2],Res);
17.90 - moveDown 1 ([2,2],Res); refFormula 1 ([2,3],Res);
17.91 - moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);
17.92 - moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
17.93 - moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
17.94 - val ((pt,_),_) = get_calc 1;
17.95 - if "-2 * 1 + (1 + x) = 0" = UnparseC.term (fst (get_obj g_result pt [2,6])) then()
17.96 - else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
17.97 -
17.98 - fetchProposedTactic 1; (*takes Iterator 1 _1_*)
17.99 -(* <ERROR> error in kernel </ERROR> ALREADY IN 2009-2*)
17.100 -(*========== inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 =============
17.101 - val (_,(tac,_,_)::_) = get_calc 1;
17.102 - if tac = Rewrite_Set "Test_simplify" then ()
17.103 - else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
17.104 -============ inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============*)
17.105 -
17.106 - autoCalculate 1 CompleteCalc;
17.107 - val ((pt,_),_) = get_calc 1;
17.108 - if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
17.109 - else error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
17.110 - (* autoCalculate 1 CompleteCalc;
17.111 - val ((pt,p),_) = get_calc 1;
17.112 - (writeln o istates2str) (get_obj g_loc pt [ ]);
17.113 - (writeln o istates2str) (get_obj g_loc pt [1]);
17.114 - (writeln o istates2str) (get_obj g_loc pt [2]);
17.115 - (writeln o istates2str) (get_obj g_loc pt [3]);
17.116 - (writeln o istates2str) (get_obj g_loc pt [3,1]);
17.117 - (writeln o istates2str) (get_obj g_loc pt [3,2]);
17.118 - (writeln o istates2str) (get_obj g_loc pt [4]);
17.119 -
17.120 - *)
17.121 -"----------------------------------------------------------";
17.122 -
17.123 - val fod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls
17.124 - ((#rules o Rule_Set.rep) Test_simplify)
17.125 - (sqrt_right false (@{theory "Pure"})) NONE
17.126 - (str2term "x + 1 + -1 * 2 = 0");
17.127 - (writeln o Derive.trtas2str) fod;
17.128 -
17.129 - val ifod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls
17.130 - ((#rules o Rule_Set.rep) Test_simplify)
17.131 - (sqrt_right false (@{theory "Pure"})) NONE
17.132 - (str2term "-2 * 1 + (1 + x) = 0");
17.133 - (writeln o Derive.trtas2str) ifod;
17.134 - fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
17.135 - val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
17.136 - val der = fod' @ (map Derive.rev_deriv' rifod');
17.137 - (writeln o Derive.trtas2str) der;
17.138 - "----------------------------------------------------------";
17.139 -DEconstrCalcTree 1;
17.140 -
17.141 -"--------- appendFormula: on Frm + equ_nrls ----------------------";
17.142 -"--------- appendFormula: on Frm + equ_nrls ----------------------";
17.143 -"--------- appendFormula: on Frm + equ_nrls ----------------------";
17.144 - reset_states ();
17.145 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
17.146 - ("Test", ["sqroot-test","univariate","equation","test"],
17.147 - ["Test","squ-equ-test-subpbl1"]))];
17.148 - Iterator 1; moveActiveRoot 1;
17.149 - autoCalculate 1 CompleteCalcHead;
17.150 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
17.151 - appendFormula 1 "2+ -1 + x = 2" (*|> Future.join*); refFormula 1 (get_pos 1 1);
17.152 -
17.153 - moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
17.154 -
17.155 - moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm);
17.156 - moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res);
17.157 - moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res);
17.158 - moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res);
17.159 - moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res);
17.160 - moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res);
17.161 - moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res);
17.162 - val ((pt,_),_) = get_calc 1;
17.163 - if "2 + -1 + x = 2" = UnparseC.term (fst (get_obj g_result pt [1,6])) then()
17.164 - else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";
17.165 -
17.166 - fetchProposedTactic 1; (*takes Iterator 1 _1_*)
17.167 - val (_,(tac,_,_)::_) = get_calc 1;
17.168 - case tac of Rewrite_Set "norm_equation" => ()
17.169 - | _ => error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
17.170 - autoCalculate 1 CompleteCalc;
17.171 - val ((pt,_),_) = get_calc 1;
17.172 - if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
17.173 - else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
17.174 -DEconstrCalcTree 1;
17.175 -
17.176 -"--------- appendFormula: on Res + NO deriv ----------------------";
17.177 -"--------- appendFormula: on Res + NO deriv ----------------------";
17.178 -"--------- appendFormula: on Res + NO deriv ----------------------";
17.179 - reset_states ();
17.180 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
17.181 - ("Test", ["sqroot-test","univariate","equation","test"],
17.182 - ["Test","squ-equ-test-subpbl1"]))];
17.183 - Iterator 1; moveActiveRoot 1;
17.184 - autoCalculate 1 CompleteCalcHead;
17.185 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
17.186 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
17.187 -
17.188 - appendFormula 1 "x = 2" (*|> Future.join*);
17.189 - val ((pt,p),_) = get_calc 1;
17.190 - val str = pr_ctree pr_short pt;
17.191 - writeln str;
17.192 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res)
17.193 - then ()
17.194 - else error "inform.sml: diff.behav.appendFormula: Res + NOder 1";
17.195 -
17.196 - fetchProposedTactic 1;
17.197 - val (_,(tac,_,_)::_) = get_calc 1;
17.198 - case tac of Rewrite_Set "Test_simplify" => ()
17.199 - | _ => error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
17.200 - autoCalculate 1 CompleteCalc;
17.201 - val ((pt,_),_) = get_calc 1;
17.202 - if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
17.203 - else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
17.204 -DEconstrCalcTree 1;
17.205 -
17.206 -"--------- appendFormula: on Res + late deriv --------------------";
17.207 -"--------- appendFormula: on Res + late deriv --------------------";
17.208 -"--------- appendFormula: on Res + late deriv --------------------";
17.209 -(*cp with "fun me" to test/../lucas-interpreter.sml:
17.210 - re-build: fun locate_input_term ---------------------------------------------------";
17.211 -*)
17.212 - reset_states ();
17.213 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
17.214 - ("Test", ["sqroot-test","univariate","equation","test"],
17.215 - ["Test","squ-equ-test-subpbl1"]))];
17.216 - Iterator 1; moveActiveRoot 1;
17.217 - autoCalculate 1 CompleteCalcHead;
17.218 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
17.219 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
17.220 -
17.221 - appendFormula 1 "x = 1" (*|> Future.join*);
17.222 - val ((pt,p),_) = get_calc 1;
17.223 - val str = pr_ctree pr_short pt;
17.224 - writeln str;
17.225 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n3.2.1. x = 0 + -1 * -1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res)
17.226 - then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
17.227 - else error "inform.sml: diff.behav.appendFormula: Res + late d 1";
17.228 -
17.229 - fetchProposedTactic 1;
17.230 - val (_,(tac,_,_)::_) = get_calc 1;
17.231 - case tac of Check_Postcond ["LINEAR", "univariate", "equation", "test"] => ()
17.232 - | _ => error "inform.sml: diff.behav.appendFormula: Res + late d 2";
17.233 - autoCalculate 1 CompleteCalc;
17.234 - val ((pt,_),_) = get_calc 1;
17.235 - if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
17.236 - else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
17.237 -DEconstrCalcTree 1;
17.238 -
17.239 -"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
17.240 -"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
17.241 -"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
17.242 - reset_states ();
17.243 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
17.244 - ("Test", ["sqroot-test","univariate","equation","test"],
17.245 - ["Test","squ-equ-test-subpbl1"]))];
17.246 - Iterator 1; moveActiveRoot 1;
17.247 - autoCalculate 1 CompleteCalcHead;
17.248 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
17.249 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
17.250 - appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*);
17.251 - val ((pt,p),_) = get_calc 1;
17.252 - val str = pr_ctree pr_short pt;
17.253 - writeln str;
17.254 - if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = -2 + 3]\n4.3. [x = 3 + -2]\n" then ()
17.255 - else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
17.256 - autoCalculate 1 CompleteCalc;
17.257 - val ((pt,p),_) = get_calc 1;
17.258 - if "[x = 3 + -2 * 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
17.259 - (* ~~~~~~~~~~ simplify as last step in any script ?!*)
17.260 - else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
17.261 -DEconstrCalcTree 1;
17.262 -
17.263 -"--------- replaceFormula: on Res + = ----------------------------";
17.264 -"--------- replaceFormula: on Res + = ----------------------------";
17.265 -"--------- replaceFormula: on Res + = ----------------------------";
17.266 - reset_states ();
17.267 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
17.268 - ("Test", ["sqroot-test","univariate","equation","test"],
17.269 - ["Test","squ-equ-test-subpbl1"]))];
17.270 - Iterator 1; moveActiveRoot 1;
17.271 - autoCalculate 1 CompleteCalcHead;
17.272 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
17.273 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
17.274 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*-1 + x*);
17.275 -
17.276 - replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
17.277 - val ((pt,_),_) = get_calc 1;
17.278 - val str = pr_ctree pr_short pt;
17.279 -
17.280 -(* before AK110725 this was
17.281 -". ----- pblobj -----\n
17.282 -1. x + 1 = 2\n
17.283 -2. x + 1 + -1 * 2 = 0\n
17.284 -2.1. x + 1 + -1 * 2 = 0\n
17.285 -2.2. 1 + x + -1 * 2 = 0\n
17.286 -2.3. 1 + (x + -1 * 2) = 0\n
17.287 -2.4. 1 + (x + -2) = 0\n
17.288 -2.5. 1 + (x + -2 * 1) = 0\n
17.289 -2.6. 1 + x + -2 * 1 = 0\n";
17.290 -*)
17.291 -if str =
17.292 -". ----- pblobj -----\n"^
17.293 -"1. x + 1 = 2\n"^
17.294 -"2. x + 1 + -1 * 2 = 0\n"^
17.295 -"2.1. x + 1 + -1 * 2 = 0\n"^
17.296 -"2.2. 1 + x + -1 * 2 = 0\n"^
17.297 -"2.3. 1 + (x + -1 * 2) = 0\n"^
17.298 -"2.4. 1 + (x + -2) = 0\n"^
17.299 -"2.5. 1 + (x + -2 * 1) = 0\n"^
17.300 -"2.6. 1 + x + -2 * 1 = 0\n" then()
17.301 -else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
17.302 -
17.303 - autoCalculate 1 CompleteCalc;
17.304 - val ((pt,pos as (p,_)),_) = get_calc 1;
17.305 - if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst) (get_obj g_result pt p) then()
17.306 - else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
17.307 -DEconstrCalcTree 1;
17.308 -
17.309 -"--------- replaceFormula: on Res + = 1st Nd ---------------------";
17.310 -"--------- replaceFormula: on Res + = 1st Nd ---------------------";
17.311 -"--------- replaceFormula: on Res + = 1st Nd ---------------------";
17.312 - reset_states ();
17.313 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
17.314 - ("Test", ["sqroot-test","univariate","equation","test"],
17.315 - ["Test","squ-equ-test-subpbl1"]))];
17.316 - Iterator 1; moveActiveRoot 1;
17.317 - autoCalculate 1 CompleteCalcHead;
17.318 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
17.319 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
17.320 -
17.321 - replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
17.322 - val ((pt,_),_) = get_calc 1;
17.323 - val str = pr_ctree pr_short pt;
17.324 - writeln str;
17.325 - if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
17.326 - else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
17.327 - autoCalculate 1 CompleteCalc;
17.328 - val ((pt,pos as (p,_)),_) = get_calc 1;
17.329 - if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
17.330 - else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
17.331 -DEconstrCalcTree 1;
17.332 -
17.333 -"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
17.334 -"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
17.335 -"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
17.336 - reset_states ();
17.337 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
17.338 - ("Test", ["sqroot-test","univariate","equation","test"],
17.339 - ["Test","squ-equ-test-subpbl1"]))];
17.340 - Iterator 1; moveActiveRoot 1;
17.341 - autoCalculate 1 CompleteCalcHead;
17.342 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
17.343 -
17.344 - replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
17.345 - val ((pt,_),_) = get_calc 1;
17.346 - val str = pr_ctree pr_short pt;
17.347 - writeln str;
17.348 - if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
17.349 - else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
17.350 - autoCalculate 1 CompleteCalc;
17.351 - val ((pt,pos as (p,_)),_) = get_calc 1;
17.352 - if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
17.353 - else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
17.354 -DEconstrCalcTree 1;
17.355 -
17.356 -"--------- replaceFormula: cut calculation -----------------------";
17.357 -"--------- replaceFormula: cut calculation -----------------------";
17.358 -"--------- replaceFormula: cut calculation -----------------------";
17.359 - reset_states ();
17.360 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
17.361 - ("Test", ["sqroot-test","univariate","equation","test"],
17.362 - ["Test","squ-equ-test-subpbl1"]))];
17.363 - Iterator 1; moveActiveRoot 1;
17.364 - autoCalculate 1 CompleteCalc;
17.365 - moveActiveRoot 1; moveActiveDown 1;
17.366 - if get_pos 1 1 = ([1], Frm) then ()
17.367 - else error "inform.sml: diff.behav. cut calculation 1";
17.368 -
17.369 - replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
17.370 - val ((pt,p),_) = get_calc 1;
17.371 - val str = pr_ctree pr_short pt;
17.372 - writeln str;
17.373 - if p = ([1], Res) then ()
17.374 - else error "inform.sml: diff.behav. cut calculation 2";
17.375 -
17.376 -
17.377 -(* 040307 copied from informtest.sml; ... old version
17.378 - "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
17.379 - "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
17.380 - "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
17.381 -
17.382 - val p = ([],Pbl);
17.383 - val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
17.384 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
17.385 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
17.386 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
17.387 - (*^^^ these are the elements for the root-problem (in variants)*)
17.388 - (*vvv these are elements required for subproblems*)
17.389 - "boundVariable a","boundVariable b","boundVariable alpha",
17.390 - "interval {x::real. 0 <= x & x <= 2*r}",
17.391 - "interval {x::real. 0 <= x & x <= 2*r}",
17.392 - "interval {x::real. 0 <= x & x <= pi}",
17.393 - "errorBound (eps=(0::real))"]
17.394 - (*specifying is not interesting for this example*)
17.395 - val spec = ("DiffApp", ["maximum_of","function"],
17.396 - ["DiffApp","max_by_calculus"]);
17.397 - (*the empty model with descriptions for user-guidance by Model_Problem*)
17.398 - val empty_model = [Given ["fixedValues []"],
17.399 - Find ["maximum", "valuesFor"],
17.400 - Relate ["relations []"]];
17.401 -
17.402 -
17.403 - (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*)
17.404 - val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)];
17.405 - (*val nxt = ("Model_Problem", ...*)
17.406 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
17.407 -
17.408 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.409 - (*nxt = Add_Given "fixedValues [r = Arbfix]"*)
17.410 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
17.411 -(*[
17.412 -(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),
17.413 -(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),
17.414 -(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
17.415 -(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)
17.416 -
17.417 - (*the empty CalcHead is checked w.r.t the model and re-established as such*)
17.418 - val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, Spec.empty);
17.419 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
17.420 - if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then () else error "informtest.sml: diff.behav. max 1";
17.421 -
17.422 - (*there is one input to the model (could be more)*)
17.423 - val (b,pt,ocalhd) =
17.424 - input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
17.425 - Find ["maximum", "valuesFor"],
17.426 - Relate ["relations"]], Pbl, Spec.empty);
17.427 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
17.428 - if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then ()
17.429 - else error "informtest.sml: diff.behav. max 2";
17.430 -
17.431 - (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME
17.432 - val (b,pt''''',ocalhd) =
17.433 - input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
17.434 - Find ["maximum A", "valuesFor [a,b]"],
17.435 - Relate ["relations [A=a*b, a/2=r*sin alpha, \
17.436 - \b/2=r*cos alpha]"]], Pbl, Spec.empty);
17.437 - val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
17.438 - if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*)
17.439 -
17.440 - (*this input is complete in variant 1 (variant 3 does not work yet)*)
17.441 - val (b,pt''''',ocalhd) =
17.442 - input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
17.443 - Find ["maximum A", "valuesFor [a,b]"],
17.444 - Relate ["relations [A=a*b, \
17.445 - \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]],
17.446 - Pbl, Spec.empty);
17.447 - val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
17.448 -
17.449 - modifycalcheadOK2xml 111 (bool2str b) ocalhd;
17.450 -*)
17.451 -DEconstrCalcTree 1;
17.452 -
17.453 -"--------- syntax error ------------------------------------------";
17.454 -"--------- syntax error ------------------------------------------";
17.455 -"--------- syntax error ------------------------------------------";
17.456 - reset_states ();
17.457 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
17.458 - ("Test", ["sqroot-test","univariate","equation","test"],
17.459 - ["Test","squ-equ-test-subpbl1"]))];
17.460 - Iterator 1; moveActiveRoot 1;
17.461 - autoCalculate 1 CompleteCalcHead;
17.462 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
17.463 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
17.464 -
17.465 - appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
17.466 - val ((pt,_),_) = get_calc 1;
17.467 - val str = pr_ctree pr_short pt;
17.468 - writeln str;
17.469 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
17.470 - else error "inform.sml: diff.behav.appendFormula: syntax error";
17.471 -DEconstrCalcTree 1;
17.472 -
17.473 -"--------- CAS-command on ([],Pbl) -------------------------------";
17.474 -"--------- CAS-command on ([],Pbl) -------------------------------";
17.475 -"--------- CAS-command on ([],Pbl) -------------------------------";
17.476 -val (p,_,f,nxt,_,pt) =
17.477 - CalcTreeTEST [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
17.478 -val ifo = "solve(x+1=2,x)";
17.479 -val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve(x+1=2,x)";
17.480 -show_pt pt;
17.481 -val nxt = (Apply_Method ["Test","squ-equ-test-subpbl1"]);
17.482 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.483 -if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()
17.484 -else error "inform.sml: diff.behav. CAScmd ([],Pbl)";
17.485 -DEconstrCalcTree 1;
17.486 -
17.487 -"--------- CAS-command on ([],Pbl) FE-interface ------------------";
17.488 -"--------- CAS-command on ([],Pbl) FE-interface ------------------";
17.489 -"--------- CAS-command on ([],Pbl) FE-interface ------------------";
17.490 -reset_states ();
17.491 -CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
17.492 -Iterator 1;
17.493 -moveActiveRoot 1;
17.494 -replaceFormula 1 "solve(x+1=2,x)";
17.495 -autoCalculate 1 CompleteCalc;
17.496 -val ((pt,p),_) = get_calc 1;
17.497 -show_pt pt;
17.498 -if p = ([], Res) then ()
17.499 -else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
17.500 -DEconstrCalcTree 1;
17.501 -
17.502 -"--------- inform [rational,simplification] ----------------------";
17.503 -"--------- inform [rational,simplification] ----------------------";
17.504 -"--------- inform [rational,simplification] ----------------------";
17.505 -reset_states ();
17.506 -CalcTree [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"],
17.507 - ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
17.508 -Iterator 1; moveActiveRoot 1;
17.509 -autoCalculate 1 CompleteCalcHead;
17.510 -
17.511 -"--- (-1) give a preview on the calculation without any input";
17.512 -(*
17.513 -autoCalculate 1 CompleteCalc;
17.514 -val ((pt, p), _) = get_calc 1;
17.515 -show_pt pt;
17.516 -[
17.517 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
17.518 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
17.519 -(([1], Res), a / b + c / d + e / f), <--- (1) input arbitrary
17.520 -(([2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
17.521 -(([3], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
17.522 -(([4], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f)), <--- (2) input next
17.523 -(([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))] <--- (3) is also final result
17.524 - EXAMPLE NOT OPTIMAL
17.525 -*)
17.526 -"--- (0) user input as the *first* step does not work, thus impdo at least 1 step";
17.527 -autoCalculate 1 (Steps 1);
17.528 -autoCalculate 1 (Steps 1);
17.529 -val ((pt, p), _) = get_calc 1;
17.530 -(*show_pt pt;
17.531 -[
17.532 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
17.533 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
17.534 -(([1], Res), a / b + c / d + e / f)]
17.535 -*)
17.536 -"--- (1) input an arbitrary next formula";
17.537 -appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f" (*|> Future.join*);
17.538 -val ((pt, p), _) = get_calc 1;
17.539 -(*show_pt pt;
17.540 -[
17.541 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
17.542 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
17.543 -(([1], Res), a / b + c / d + e / f),
17.544 -(([2,1], Frm), a / b + c / d + e / f),
17.545 -(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
17.546 -(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
17.547 -(([2], Res), (a * d + c * b) / (b * d) + e / f)]
17.548 -*)
17.549 -val ((pt,p),_) = get_calc 1;
17.550 -if p = ([2], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
17.551 -else error ("inform.sml: [rational,simplification] 1");
17.552 -
17.553 -"--- (2) input the next formula that would be presented by mat-engine";
17.554 -(* generate a preview:
17.555 -autoCalculate 1 (Steps 1);
17.556 -val ((pt, p), _) = get_calc 1;
17.557 -show_pt pt;
17.558 -[
17.559 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
17.560 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
17.561 -(([1], Res), a / b + c / d + e / f),
17.562 -(([2,1], Frm), a / b + c / d + e / f),
17.563 -(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
17.564 -(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
17.565 -(([2], Res), (a * d + c * b) / (b * d) + e / f),
17.566 -(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))] <--- input this
17.567 -*)
17.568 -appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
17.569 -val ((pt, p), _) = get_calc 1;
17.570 -(*show_pt pt;
17.571 -[
17.572 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
17.573 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
17.574 -(([1], Res), a / b + c / d + e / f),
17.575 -(([2,1], Frm), a / b + c / d + e / f),
17.576 -(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
17.577 -(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
17.578 -(([2], Res), (a * d + c * b) / (b * d) + e / f),
17.579 -(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))]
17.580 -*)
17.581 -if p = ([3], Res) andalso (length o children o (get_nd pt)) (fst p) = 0 then ()
17.582 -else error ("inform.sml: [rational,simplification] 2");
17.583 -
17.584 -"--- (3) input the exact final result";
17.585 -appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
17.586 -val ((pt, p), _) = get_calc 1;
17.587 -(*show_pt pt;
17.588 -[
17.589 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
17.590 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
17.591 -(([1], Res), a / b + c / d + e / f),
17.592 -(([2,1], Frm), a / b + c / d + e / f),
17.593 -(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
17.594 -(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
17.595 -(([2], Res), (a * d + c * b) / (b * d) + e / f),
17.596 -(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
17.597 -(([4,1], Frm), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
17.598 -(([4,1], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
17.599 -(([4,2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
17.600 -(([4], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))]
17.601 -*)
17.602 -if p = ([4], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
17.603 -else error ("inform.sml: [rational,simplification] 3");
17.604 -
17.605 -"--- (4) finish the calculation + check the postcondition (in the future)";
17.606 -autoCalculate 1 CompleteCalc;
17.607 -val ((pt, p), _) = get_calc 1;
17.608 -val (t, asm) = get_obj g_result pt [];
17.609 -if UnparseC.term t = "(a * d * f + b * c * f + b * d * e) / (b * d * f)" andalso
17.610 -UnparseC.terms asm = "[\"b * d * f \<noteq> 0\",\"d \<noteq> 0\",\"b \<noteq> 0\",\"a * x / (b * x) + c * x / (d * x) + e / f is_ratpolyexp\"]"
17.611 -then () else error "inform [rational,simplification] changed at end";
17.612 -(*show_pt pt;
17.613 -[
17.614 -(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
17.615 -(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
17.616 -(([1], Res), a / b + c / d + e / f),
17.617 -(([2,1], Frm), a / b + c / d + e / f),
17.618 -(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
17.619 -(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
17.620 -(([2], Res), (a * d + c * b) / (b * d) + e / f),
17.621 -(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
17.622 -(([4,1], Frm), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
17.623 -(([4,1], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
17.624 -(([4,2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
17.625 -(([4], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
17.626 -(([5], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
17.627 -(([6], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f)),
17.628 -(([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))]
17.629 -*)
17.630 -DEconstrCalcTree 1;
17.631 -
17.632 -"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
17.633 -"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
17.634 -"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
17.635 -val t = str2term "Diff (x^^^2 + x + 1, x)";
17.636 -case t of Const ("Diff.Diff", _) $ _ => ()
17.637 - | _ => raise
17.638 - error "diff.sml behav.changed for CAS Diff (..., x)";
17.639 -atomty t;
17.640 -"-----------------------------------------------------------------";
17.641 -(*1>*)reset_states ();
17.642 -(*2>*)CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
17.643 -(*3>*)Iterator 1;moveActiveRoot 1;
17.644 -"----- here the Headline has been finished";
17.645 -(*4>*)moveActiveFormula 1 ([],Pbl);
17.646 -(*5>*)replaceFormula 1 "Diff (x^2 + x + 1, x)";
17.647 -val ((pt,_),_) = get_calc 1;
17.648 -val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
17.649 -val NONE = env;
17.650 -val (SOME istate, NONE) = loc;
17.651 -(*default_print_depth 5;*)
17.652 -writeln"-----------------------------------------------------------";
17.653 -spec;
17.654 -writeln (itms2str_ ctxt probl);
17.655 -writeln (itms2str_ ctxt meth);
17.656 -writeln (Istate.string_of (fst istate));
17.657 -
17.658 -refFormula 1 ([],Pbl) (*--> correct CalcHead*);
17.659 - (*081016 NOT necessary (but leave it in Java):*)
17.660 -(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
17.661 -"----- here the CalcHead has been completed --- ONCE MORE ?????";
17.662 -
17.663 -(***difference II***)
17.664 -val ((pt,p),_) = get_calc 1;
17.665 -(*val p = ([], Pbl)*)
17.666 -val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
17.667 -val NONE = env;
17.668 -val (SOME istate, NONE) = loc;
17.669 -(*default_print_depth 5;*) writeln (Istate.string_of (fst istate)); (*default_print_depth 3;*)
17.670 -(*Pstate ([],
17.671 - [], NONE,
17.672 - ??.empty, Sundef, false)*)
17.673 -(*default_print_depth 5;*) spec; (*default_print_depth 3;*)
17.674 -(*("Isac_Knowledge",
17.675 - ["derivative_of", "function"],
17.676 - ["diff", "differentiate_on_R"]) : spec*)
17.677 -writeln (itms2str_ ctxt probl);
17.678 -(*[
17.679 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
17.680 -(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
17.681 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
17.682 -writeln (itms2str_ ctxt meth);
17.683 -(*[
17.684 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
17.685 -(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
17.686 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
17.687 -writeln"-----------------------------------------------------------";
17.688 -(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
17.689 -(*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
17.690 -autoCalculate 1 CompleteCalc;
17.691 -val ((pt,p),_) = get_calc 1;
17.692 -val Form res = (#1 o pt_extract) (pt, ([],Res));
17.693 -show_pt pt;
17.694 -if p = ([], Res) andalso UnparseC.term res = "1 + 2 * x" then ()
17.695 -else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
17.696 -DEconstrCalcTree 1;
17.697 -
17.698 -"--------- Take as 1st tac, start from exp -----------------------";
17.699 -"--------- Take as 1st tac, start from exp -----------------------";
17.700 -"--------- Take as 1st tac, start from exp -----------------------";
17.701 -(*the following input is copied from BridgeLog Java <==> SML,
17.702 - omitting unnecessary inputs*)
17.703 -(*1>*)reset_states ();
17.704 -(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac_Knowledge",["derivative_of","function"],["diff","differentiate_on_R"]))];
17.705 -(*3>*)Iterator 1; moveActiveRoot 1;
17.706 -
17.707 -(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
17.708 -(***difference II***)
17.709 -val ((pt,_),_) = get_calc 1;
17.710 -val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
17.711 -val NONE = env;
17.712 -val (SOME istate, NONE) = loc;
17.713 -(*default_print_depth 5;*) writeln (Istate.string_of (fst istate)); (*default_print_depth 3;*)
17.714 -(*Pstate ([],
17.715 - [], NONE,
17.716 - ??.empty, Sundef, false)*)
17.717 -(*default_print_depth 5;*) spec; (*default_print_depth 3;*)
17.718 -(*("Isac_Knowledge",
17.719 - ["derivative_of", "function"],
17.720 - ["diff", "differentiate_on_R"]) : spec*)
17.721 -writeln (itms2str_ ctxt probl);
17.722 -(*[
17.723 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
17.724 -(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
17.725 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
17.726 -writeln (itms2str_ ctxt meth);
17.727 -(*[
17.728 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
17.729 -(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
17.730 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
17.731 -writeln"-----------------------------------------------------------";
17.732 -(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
17.733 -autoCalculate 1 (Steps 1);
17.734 -val ((pt,p),_) = get_calc 1;
17.735 -val Form res = (#1 o pt_extract) (pt, p);
17.736 -if UnparseC.term res = "d_d x (x ^^^ 2 + x + 1)" then ()
17.737 -else error "diff.sml Diff (x^2 + x + 1, x) from exp";
17.738 -DEconstrCalcTree 1;
17.739 -
17.740 -"--------- implicit_take, start with <NEW> (CAS input) ---------------";
17.741 -"--------- implicit_take, start with <NEW> (CAS input) ---------------";
17.742 -"--------- implicit_take, start with <NEW> (CAS input) ---------------";
17.743 -reset_states ();
17.744 -CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
17.745 -(*[[from sml: > @@@@@begin@@@@@
17.746 -[[from sml: 1
17.747 -[[from sml: <CALCTREE>
17.748 -[[from sml: <CALCID> 1 </CALCID>
17.749 -[[from sml: </CALCTREE>
17.750 -[[from sml: @@@@@end@@@@@*)
17.751 -Iterator 1;
17.752 -(*[[from sml: > @@@@@begin@@@@@
17.753 -[[from sml: 1
17.754 -[[from sml: <ADDUSER>
17.755 -[[from sml: <CALCID> 1 </CALCID>
17.756 -[[from sml: <USERID> 1 </USERID>
17.757 -[[from sml: </ADDUSER>
17.758 -[[from sml: @@@@@end@@@@@*)
17.759 -moveActiveRoot 1;
17.760 -(*[[from sml: > @@@@@begin@@@@@
17.761 -[[from sml: 1
17.762 -[[from sml: <CALCITERATOR>
17.763 -[[from sml: <CALCID> 1 </CALCID>
17.764 -[[from sml: <POSITION>
17.765 -[[from sml: <INTLIST>
17.766 -[[from sml: </INTLIST>
17.767 -[[from sml: <POS> Pbl </POS>
17.768 -[[from sml: </POSITION>
17.769 -[[from sml: </CALCITERATOR>
17.770 -[[from sml: @@@@@end@@@@@*)
17.771 -getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
17.772 -(*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
17.773 -[[from sml: 1
17.774 -[[from sml: <GETELEMENTSFROMTO>
17.775 -[[from sml: <CALCID> 1 </CALCID>
17.776 -[[from sml: <FORMHEADS>
17.777 -[[from sml: <CALCFORMULA>
17.778 -[[from sml: <POSITION>
17.779 -[[from sml: <INTLIST>
17.780 -[[from sml: </INTLIST>
17.781 -[[from sml: <POS> Pbl </POS>
17.782 -[[from sml: </POSITION>
17.783 -[[from sml: <FORMULA>
17.784 -[[from sml: <MATHML>
17.785 -[[from sml: <ISA> ________________________________________________ </ISA>
17.786 -[[from sml: </MATHML>
17.787 -[[from sml:
17.788 -[[from sml: </FORMULA>
17.789 -[[from sml: </CALCFORMULA>
17.790 -[[from sml: </FORMHEADS>
17.791 -[[from sml: </GETELEMENTSFROMTO>
17.792 -[[from sml: @@@@@end@@@@@*)
17.793 -refFormula 1 ([],Pbl);
17.794 -(*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
17.795 -[[from sml: 1
17.796 -[[from sml: <REFFORMULA>
17.797 -[[from sml: <CALCID> 1 </CALCID>
17.798 -[[from sml: <CALCHEAD status = "incorrect">
17.799 -[[from sml: <POSITION>
17.800 -[[from sml: <INTLIST>
17.801 -[[from sml: </INTLIST>
17.802 -[[from sml: <POS> Pbl </POS>
17.803 -[[from sml: </POSITION>
17.804 -[[from sml: <HEAD>
17.805 -[[from sml: <MATHML>
17.806 -[[from sml: <ISA> Problem (ThyC.id_empty, [e_pblID]) </ISA>
17.807 -[[from sml: </MATHML>
17.808 -[[from sml: </HEAD>
17.809 -[[from sml: <MODEL>
17.810 -[[from sml: <GIVEN> </GIVEN>
17.811 -[[from sml: <WHERE> </WHERE>
17.812 -[[from sml: <FIND> </FIND>
17.813 -[[from sml: <RELATE> </RELATE>
17.814 -[[from sml: </MODEL>
17.815 -[[from sml: <BELONGSTO> Pbl </BELONGSTO>
17.816 -[[from sml: <SPECIFICATION>
17.817 -[[from sml: <THEORYID> ThyC.id_empty </THEORYID>
17.818 -[[from sml: <PROBLEMID>
17.819 -[[from sml: <STRINGLIST>
17.820 -[[from sml: <STRING> Problem.id_empty </STRING>
17.821 -[[from sml: </STRINGLIST>
17.822 -[[from sml: </PROBLEMID>
17.823 -[[from sml: <METHODID>
17.824 -[[from sml: <STRINGLIST>
17.825 -[[from sml: <STRING> e_metID </STRING>
17.826 -[[from sml: </STRINGLIST>
17.827 -[[from sml: </METHODID>
17.828 -[[from sml: </SPECIFICATION>
17.829 -[[from sml: </CALCHEAD>
17.830 -[[from sml: </REFFORMULA>
17.831 -[[from sml: @@@@@end@@@@@*)
17.832 -moveActiveFormula 1 ([],Pbl);
17.833 -(*[[from sml: > @@@@@begin@@@@@
17.834 -[[from sml: 1
17.835 -[[from sml: <CALCITERATOR>
17.836 -[[from sml: <CALCID> 1 </CALCID>
17.837 -[[from sml: <POSITION>
17.838 -[[from sml: <INTLIST>
17.839 -[[from sml: </INTLIST>
17.840 -[[from sml: <POS> Pbl </POS>
17.841 -[[from sml: </POSITION>
17.842 -[[from sml: </CALCITERATOR>
17.843 -[[from sml: @@@@@end@@@@@*)
17.844 -replaceFormula 1 "Simplify (1+2)";
17.845 -(*[[from sml: > @@@@@begin@@@@@
17.846 -[[from sml: 1
17.847 -[[from sml: <REPLACEFORMULA>
17.848 -[[from sml: <CALCID> 1 </CALCID>
17.849 -[[from sml: <CALCCHANGED>
17.850 -[[from sml: <UNCHANGED>
17.851 -[[from sml: <INTLIST>
17.852 -[[from sml: </INTLIST>
17.853 -[[from sml: <POS> Pbl </POS>
17.854 -[[from sml: </UNCHANGED>
17.855 -[[from sml: <DELETED>
17.856 -[[from sml: <INTLIST>
17.857 -[[from sml: </INTLIST>
17.858 -[[from sml: <POS> Pbl </POS>
17.859 -[[from sml: </DELETED>
17.860 -[[from sml: <GENERATED>
17.861 -[[from sml: <INTLIST>
17.862 -[[from sml: </INTLIST>
17.863 -[[from sml: <POS> Met </POS> DIFFERENCE: Pbl
17.864 -[[from sml: </GENERATED>
17.865 -[[from sml: </CALCCHANGED>
17.866 -[[from sml: </REPLACEFORMULA>
17.867 -[[from sml: @@@@@end@@@@@*)
17.868 -getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false(* DIFFERENCE: Pbl*);
17.869 -(*@@@@@begin@@@@@
17.870 - 1
17.871 -<GETELEMENTSFROMTO>
17.872 - <CALCID> 1 </CALCID>
17.873 - <FORMHEADS>
17.874 - <CALCFORMULA>
17.875 - <POSITION>
17.876 - <INTLIST>
17.877 - </INTLIST>
17.878 - <POS> Pbl </POS>
17.879 - </POSITION>
17.880 - <FORMULA>
17.881 - <MATHML>
17.882 - <ISA> Simplify (1 + 2) </ISA> WORKS !!!!!
17.883 - </MATHML>
17.884 - </FORMULA>
17.885 - </CALCFORMULA>
17.886 - </FORMHEADS>
17.887 -</GETELEMENTSFROMTO>
17.888 -@@@@@end@@@@@*)
17.889 -getFormulaeFromTo 1 ([],Pbl) ([],Met) 0 false;
17.890 -(*[[from sml: > @@@@@begin@@@@@
17.891 -[[from sml: 1
17.892 -[[from sml: <SYSERROR>
17.893 -[[from sml: <CALCID> 1 </CALCID>
17.894 -[[from sml: <ERROR> error in getFormulaeFromTo </ERROR>
17.895 -[[from sml: </SYSERROR>
17.896 -[[from sml: @@@@@end@@@@@*)
17.897 -(*step into getFormulaeFromTo --- bug corrected...*)
17.898 -
17.899 -"--------- build fun check_err_patt ------------------------------";
17.900 -"--------- build fun check_err_patt ------------------------------";
17.901 -"--------- build fun check_err_patt ------------------------------";
17.902 -val subst = [(str2term "bdv", str2term "x")]: subst;
17.903 -val rls = norm_Rational
17.904 -val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
17.905 -val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
17.906 -val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "1 / 2");
17.907 -
17.908 -val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
17.909 - rew_sub thy 1 [] e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
17.910 -if rewritten then NONE else SOME "e_errpatID";
17.911 -
17.912 -val norm_res = case rewrite_set_ (Isac()) false rls res' of
17.913 - NONE => res'
17.914 -| SOME (norm_res, _) => norm_res
17.915 -
17.916 -val norm_inf = case rewrite_set_ (Isac()) false rls inf of
17.917 - NONE => inf
17.918 -| SOME (norm_inf, _) => norm_inf;
17.919 -
17.920 -res' = inf;
17.921 -norm_res = norm_inf;
17.922 -
17.923 -val pat = parse_patt @{theory} "(?a + ?b)/?a = ?b";
17.924 -val (res, inf) = (str2term "(2 + 3)/2", str2term "3");
17.925 -if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
17.926 -then () else error "error patt example1 changed";
17.927 -
17.928 -val pat = parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
17.929 -val (res, inf) = (str2term "(2 + 3)/(2 + 4)", str2term "3 / 4");
17.930 -if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
17.931 -then () else error "error patt example2 changed";
17.932 -
17.933 -val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
17.934 -val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
17.935 -if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
17.936 -then () else error "error patt example3 changed";
17.937 -
17.938 -val inf = str2term "1 / 2";
17.939 -if check_err_patt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
17.940 -then () else error "error patt example3 changed";
17.941 -
17.942 -"--------- build fun check_err_patt ?bdv -------------------------";
17.943 -"--------- build fun check_err_patt ?bdv -------------------------";
17.944 -"--------- build fun check_err_patt ?bdv -------------------------";
17.945 -val subst = [(str2term "bdv", str2term "x")]: subst;
17.946 -val t = str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))";
17.947 -val SOME (t, _) = rewrite_set_inst_ thy false subst norm_diff t;
17.948 -if UnparseC.term t = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3" then ()
17.949 -else error "build fun check_err_patt ?bdv changed 1";
17.950 -
17.951 -val rls = norm_diff
17.952 -val pat = parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)";
17.953 -val (res, inf) = (str2term "2 * x + d_d x (sin (x ^^^ 4))", str2term "2 * x + cos (4 * x ^^^ 3)");
17.954 -
17.955 -val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
17.956 - rew_sub thy 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
17.957 -if UnparseC.term res' = "2 * x + cos (d_d x (x ^^^ 4))" andalso rewritten then ()
17.958 -else error "build fun check_err_patt ?bdv changed 2";
17.959 -
17.960 -val norm_res = case rewrite_set_inst_ (Isac()) false subst rls res' of
17.961 - NONE => res'
17.962 -| SOME (norm_res, _) => norm_res;
17.963 -if UnparseC.term norm_res = "2 * x + cos (4 * x ^^^ 3)" then ()
17.964 -else error "build fun check_err_patt ?bdv changed 3";
17.965 -
17.966 -val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of
17.967 - NONE => inf
17.968 -| SOME (norm_inf, _) => norm_inf;
17.969 -if UnparseC.term norm_inf = "2 * x + cos (4 * x ^^^ 3)" then ()
17.970 -else error "build fun check_err_patt ?bdv changed 4";
17.971 -
17.972 -res' = inf;
17.973 -if norm_res = norm_inf then ()
17.974 -else error "build fun check_err_patt ?bdv changed 5";
17.975 -
17.976 -if check_err_patt (res, inf) (subst: subst) ("errpatID": errpatID, pat) rls = SOME "errpatID"
17.977 -then () else error "error patt example1 changed";
17.978 -
17.979 -"--------- build fun Error_Pattern.check_for ------------------------";
17.980 -"--------- build fun Error_Pattern.check_for ------------------------";
17.981 -"--------- build fun Error_Pattern.check_for ------------------------";
17.982 -val (res, inf) =
17.983 - (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
17.984 - str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
17.985 -val {errpats, nrls = rls, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"]
17.986 -
17.987 -val env = [(str2term "v_v", str2term "x")];
17.988 -val errpats =
17.989 - [e_errpat, (*generalised for testing*)
17.990 - ("chain-rule-diff-both",
17.991 - [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
17.992 - parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
17.993 - parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
17.994 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
17.995 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
17.996 - [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
17.997 - @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
17.998 -case Error_Pattern.check_for (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
17.999 -| NONE => error "Error_Pattern.check_for broken";
17.1000 -DEconstrCalcTree 1;
17.1001 -
17.1002 -"--------- embed fun Error_Pattern.check_for ------------------------";
17.1003 -"--------- embed fun Error_Pattern.check_for ------------------------";
17.1004 -"--------- embed fun Error_Pattern.check_for ------------------------";
17.1005 -reset_states ();
17.1006 -CalcTree
17.1007 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
17.1008 - ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
17.1009 -Iterator 1;
17.1010 -moveActiveRoot 1;
17.1011 -autoCalculate 1 CompleteCalcHead;
17.1012 -autoCalculate 1 (Steps 1);
17.1013 -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
17.1014 -(*autoCalculate 1 (Steps 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
17.1015 -
17.1016 -"~~~~~ fun appendFormula , args:"; val (cI, (ifo:TermC.as_string)) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
17.1017 -"~~~~~ fun appendFormula' , args:"; val (cI, (ifo: TermC.as_string)) = (cI, ifo);
17.1018 - val cs = get_calc cI
17.1019 - val pos = get_pos cI 1;
17.1020 -(*+*)if pos = ([1], Res) then () else error "inform with (positive) Error_Pattern.check_for broken 1";
17.1021 - val ("ok", cs' as (_, _, ptp)) = (*case*) Step.do_next pos cs (*of*);
17.1022 - (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*ERROR WAS: "no derivation found"*)
17.1023 -"~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Chead.calcstate'), istr)
17.1024 - = (cs', (encode ifo));
17.1025 - val ctxt = get_ctxt pt pos (*see TODO.thy*)
17.1026 - val SOME f_in = (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
17.1027 - val f_in = Thm.term_of f_in
17.1028 - val pos_pred = lev_back' pos
17.1029 - val f_pred = Ctree.get_curr_formula (pt, pos_pred);
17.1030 - (*if*) f_pred = f_in; (*else*)
17.1031 - val NONE = (*case*) In_Chead.cas_input f_in (*of*);
17.1032 - (*old* )val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
17.1033 - (*old*)val {scr = prog, ...} = Specify.get_met metID
17.1034 - (*old*)val istate = get_istate_LI pt pos
17.1035 - (*old*)val ctxt = get_ctxt pt pos
17.1036 - ( *old*)
17.1037 - val LI.Not_Derivable =
17.1038 - (*case*) LI.locate_input_term (pt, pos) f_in (*of*);
17.1039 - val pp = Ctree.par_pblobj pt p
17.1040 - val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
17.1041 - {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
17.1042 - | _ => error "inform: uncovered case of get_met"
17.1043 -;
17.1044 -(*+*)if errpats2str errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\",\"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\",\"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)\",\"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\",\"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\",\"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\",\"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1) * d_d ?bdv ?u\",\"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\",\"d_d ?bdv (E_ ^^^ ?u) = E_ ^^^ ?u * d_d ?x ?u\"]]"
17.1045 -(*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
17.1046 -
17.1047 - val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
17.1048 -;
17.1049 -(*+*)if UnparseC.term f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
17.1050 -(*+*) UnparseC.term f_in = "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)"
17.1051 -(*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2";
17.1052 -
17.1053 - val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
17.1054 -
17.1055 -"--- final check:";
17.1056 -(*+*)val (_, _, ptp') = cs';
17.1057 -case Step_Solve.by_term ptp' (encode ifo) of
17.1058 - ("error pattern #chain-rule-diff-both#", calcstate') => ()
17.1059 -| _ => error "inform with (positive) Error_Pattern.check_for broken"
17.1060 -
17.1061 -
17.1062 -"--------- embed fun find_fillpatterns ---------------------------";
17.1063 -"--------- embed fun find_fillpatterns ---------------------------";
17.1064 -"--------- embed fun find_fillpatterns ---------------------------";
17.1065 -reset_states ();
17.1066 -CalcTree
17.1067 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
17.1068 - ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
17.1069 -Iterator 1;
17.1070 -moveActiveRoot 1;
17.1071 -autoCalculate 1 CompleteCalcHead;
17.1072 -autoCalculate 1 (Steps 1);
17.1073 -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
17.1074 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);
17.1075 - (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
17.1076 - (*or
17.1077 - <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
17.1078 -
17.1079 -"~~~~~ fun findFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
17.1080 - val ((pt, _), _) = get_calc cI
17.1081 - val pos = get_pos cI 1;
17.1082 -"~~~~~ fun find_fillpatterns , args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
17.1083 - val f_curr = Ctree.get_curr_formula (pt, pos);
17.1084 - val pp = Ctree.par_pblobj pt p
17.1085 - val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
17.1086 - {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
17.1087 - | _ => error "find_fillpatterns: uncovered case of get_met"
17.1088 - val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
17.1089 - val subst = Rtools.get_bdv_subst prog env
17.1090 - val errpatthms = errpats
17.1091 - |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
17.1092 - |> map (#3: errpat -> thm list)
17.1093 - |> flat;
17.1094 -
17.1095 -case map (get_fillpats subst f_curr errpatID) errpatthms |> flat of
17.1096 - ("fill-d_d-arg", tm, thm, subs_opt) :: _ => if UnparseC.term tm =
17.1097 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
17.1098 - then () else error "find_fillpatterns changed 1a"
17.1099 -| _ => error "find_fillpatterns changed 1b"
17.1100 -
17.1101 -"~~~~~ fun get_fillpats, args:"; val (subst, form, errpatID, thm) =
17.1102 - (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
17.1103 - val thmDeriv = Thm.get_name_hint thm
17.1104 - val (part, thyID) = thy_containing_thm thmDeriv
17.1105 - val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
17.1106 - val Hthm {fillpats, ...} = get_the theID
17.1107 - val some = map (get_fillform subst (thm, form) errpatID) fillpats;
17.1108 -
17.1109 -case some |> filter is_some |> map the of
17.1110 - ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term tm =
17.1111 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
17.1112 - then () else error "find_fillpatterns changed 2a"
17.1113 -| _ => error "find_fillpatterns changed 2b"
17.1114 -
17.1115 -"~~~~~ fun get_fillform, args:";
17.1116 - val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
17.1117 - (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
17.1118 -val (form', _, _, rewritten) =
17.1119 - rew_sub (Isac()) 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
17.1120 -
17.1121 -if UnparseC.term form' = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
17.1122 -else error "find_fillpatterns changed 3";
17.1123 -
17.1124 -"~~~~~ to findFillpatterns return val:"; val (fillpats) =
17.1125 - (map (get_fillpats (subs_opt, subst) f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
17.1126 -
17.1127 -"vvv--- dropped this code WN120730";
17.1128 -val msg = "fill patterns " ^
17.1129 - ((map ((apsnd UnparseC.term) o quad2pair) fillpats) |> map pair2str_ |> strs2str_);
17.1130 -msg =
17.1131 - "fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
17.1132 - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" ^
17.1133 - "#fill-both-args#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
17.1134 - " =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3" ^
17.1135 - "#fill-d_d#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
17.1136 - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1 x (x ^^^ 4)" ^
17.1137 - "#fill-inner-deriv#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
17.1138 - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1" ^
17.1139 - "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#";
17.1140 -"^^^--- dropped this code WN120730";
17.1141 -
17.1142 -if (map #1 fillpats) =
17.1143 - ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"]
17.1144 -then () else error "find_fillpatterns changed 4b";
17.1145 -DEconstrCalcTree 1;
17.1146 -
17.1147 -"--------- build fun is_exactly_equal, inputFillFormula ----------";
17.1148 -"--------- build fun is_exactly_equal, inputFillFormula ----------";
17.1149 -"--------- build fun is_exactly_equal, inputFillFormula ----------";
17.1150 -reset_states ();
17.1151 -CalcTree
17.1152 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
17.1153 - ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
17.1154 -Iterator 1;
17.1155 -moveActiveRoot 1;
17.1156 -autoCalculate 1 CompleteCalcHead;
17.1157 -autoCalculate 1 (Steps 1);
17.1158 -autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
17.1159 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*)
17.1160 -(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
17.1161 - would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
17.1162 - results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
17.1163 - instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
17.1164 - val ((pt,pos), _) = get_calc 1;
17.1165 - val p = get_pos 1 1;
17.1166 - val (Form f, _, asms) = pt_extract (pt, p);
17.1167 -
17.1168 - if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
17.1169 - case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
17.1170 - ("diff_sum", thm)) =>
17.1171 - if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
17.1172 - else error "embed fun get_fillform changed 11"
17.1173 - | _ => error "embed fun get_fillform changed 12"
17.1174 - else error "embed fun get_fillform changed 13";
17.1175 -
17.1176 -findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
17.1177 -(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
17.1178 - d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
17.1179 - val ((pt,pos),_) = get_calc 1;
17.1180 - val p = get_pos 1 1;
17.1181 -
17.1182 - val (Form f, _, asms) = pt_extract (pt, p);
17.1183 - if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
17.1184 - case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
17.1185 - ("diff_sum", thm)) =>
17.1186 - if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
17.1187 - else error "embed fun get_fillform changed 21"
17.1188 - | _ => error "embed fun get_fillform changed 22"
17.1189 - else error "embed fun get_fillform changed 23";
17.1190 -
17.1191 -requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
17.1192 - (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
17.1193 - val ((pt,pos),_) = get_calc 1;
17.1194 - val p = get_pos 1 1;
17.1195 - val (Form f, _, asms) = pt_extract (pt, p);
17.1196 - if p = ([1], Res) andalso existpt [2] pt
17.1197 - andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
17.1198 - then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
17.1199 - ("diff_sum", thm)) =>
17.1200 - if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
17.1201 - else error "embed fun get_fillform changed 31"
17.1202 - | _ => error "embed fun get_fillform changed 32"
17.1203 - else error "embed fun get_fillform changed 33";
17.1204 -
17.1205 -(* input a formula which exactly fills the gaps in a "fillformula"
17.1206 - presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
17.1207 - errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.
17.1208 - the respective thm is in the ctree ................
17.1209 -*)
17.1210 -"~~~~~ fun inputFillFormula, args:"; val (cI, ifo) =
17.1211 - (1, "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)");
17.1212 - val ((pt, _), _) = get_calc cI
17.1213 - val pos = get_pos cI 1;
17.1214 -
17.1215 -"~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo);
17.1216 - val SOME ifo = parseNEW (ThyC.get_theory "Isac_Knowledge" |> ThyC.to_ctxt) istr
17.1217 - val p' = lev_on p;
17.1218 - val tac = get_obj g_tac pt p';
17.1219 -val Rewrite_Inst ([bbb as "(''bdv'', x)"], ("diff_sin_chain", ttt)) = tac;
17.1220 -if (UnparseC.term o Thm.prop_of) ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
17.1221 -else error "inputFillFormula changed 10";
17.1222 - val Appl rew = applicable_in pos pt tac;
17.1223 - val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
17.1224 -
17.1225 -"~~~~~ to inputFillFormula return val:"; val ("ok", tac) = ("ok", tac);
17.1226 - val ("ok", (_, c, ptp as (_,p'))) = Step.by_tactic tac (pt, pos);
17.1227 - upd_calc cI (ptp, []);
17.1228 - upd_ipos cI 1 p';
17.1229 - autocalculateOK2xml cI pos (if null c then p' else last_elem c) p';
17.1230 -
17.1231 -"~~~~~ final check:";
17.1232 -val ((pt, _),_) = get_calc 1;
17.1233 -val p = get_pos 1 1;
17.1234 -val (Form f, _, asms) = pt_extract (pt, p);
17.1235 - if p = ([2], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)"
17.1236 - then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
17.1237 - ("diff_sin_chain", thm)) =>
17.1238 - if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
17.1239 - else error "inputFillFormula changed 111"
17.1240 - | _ => error "inputFillFormula changed 112"
17.1241 - else error "inputFillFormula changed 113";
17.1242 -
17.1243 -"--------- fun appl_adds -----------------------------------------";
17.1244 -"--------- fun appl_adds -----------------------------------------";
17.1245 -"--------- fun appl_adds -----------------------------------------";
17.1246 -(* val (dI, oris, ppc, pbt, selct::ss) =
17.1247 - (dI, pors, probl, ppc, map itms2fstr probl);
17.1248 - ...vvv
17.1249 - *)
17.1250 -(* val (dI, oris, ppc, pbt, (selct::ss))=
17.1251 - (#1 (some_spec ospec spec), oris, []:itm list,
17.1252 - ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
17.1253 - val iii = appl_adds dI oris ppc pbt (selct::ss);
17.1254 - tracing(itms2str_ thy iii);
17.1255 -
17.1256 - val itm = appl_add' dI oris ppc pbt selct;
17.1257 - val ppc = insert_ppc' itm ppc;
17.1258 -
17.1259 - val _::selct::ss = (selct::ss);
17.1260 - val itm = appl_add' dI oris ppc pbt selct;
17.1261 - val ppc = insert_ppc' itm ppc;
17.1262 -
17.1263 - val _::selct::ss = (selct::ss);
17.1264 - val itm = appl_add' dI oris ppc pbt selct;
17.1265 - val ppc = insert_ppc' itm ppc;
17.1266 - tracing(itms2str_ thy ppc);
17.1267 -
17.1268 - val _::selct::ss = (selct::ss);
17.1269 - val itm = appl_add' dI oris ppc pbt selct;
17.1270 - val ppc = insert_ppc' itm ppc;
17.1271 - *)
17.1272 -"--------- fun concat_deriv --------------------------------------";
17.1273 -"--------- fun concat_deriv --------------------------------------";
17.1274 -"--------- fun concat_deriv --------------------------------------";
17.1275 -(*
17.1276 - val ({rew_ord, erls, rules,...}, fo, ifo) =
17.1277 - (Rule_Set.rep Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
17.1278 - (tracing o Derive.trtas2str) fod';
17.1279 -> ["
17.1280 -(x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))","
17.1281 -(-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))","
17.1282 -(-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))","
17.1283 -(1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
17.1284 -val it = () : unit
17.1285 - (tracing o Derive.trtas2str) (map Derive.rev_deriv' rifod');
17.1286 -> ["
17.1287 -(1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))","
17.1288 -(1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))","
17.1289 -(-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"]
17.1290 -val it = () : unit
17.1291 -*)
17.1292 -"--------- handle an input formula -------------------------------";
17.1293 -"--------- handle an input formula -------------------------------";
17.1294 -"--------- handle an input formula -------------------------------";
17.1295 -(*
17.1296 -Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler:
17.1297 -Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden,
17.1298 -wenn Abteilungen nur auf gleichem Level gesucht werden ?
17.1299 -WN.040216
17.1300 -
17.1301 -Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml
17.1302 -
17.1303 -------------------------------------------------------------------------------
17.1304 -"Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
17.1305 -------------------------------------------------------------------------------
17.1306 -1. "5 * x / (x - 2) - x / (x + 2) = 4"
17.1307 -...
17.1308 -4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalise", "poly"..
17.1309 -...
17.1310 -4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate"..
17.1311 -...
17.1312 -4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions"
17.1313 -...
17.1314 -"[x = -4 / 3]"
17.1315 -------------------------------------------------------------------------------
17.1316 -(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
17.1317 -
17.1318 -(4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
17.1319 -------------------------------------------------------------------------------
17.1320 -
17.1321 -
17.1322 -------------------------------------------------------------------------------
17.1323 -"Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
17.1324 -------------------------------------------------------------------------------
17.1325 -1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x"
17.1326 -...
17.1327 -4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))"
17.1328 - Subproblem["normalise", "polynomial", "univariate"..
17.1329 -...
17.1330 -4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..
17.1331 -...
17.1332 -4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
17.1333 -4.4.5. "[x = 0, x = 6 / 5]"
17.1334 -...
17.1335 -5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
17.1336 - "[x = 6 / 5]"
17.1337 -------------------------------------------------------------------------------
17.1338 -(1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x]
17.1339 -
17.1340 -(4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.]
17.1341 -------------------------------------------------------------------------------
17.1342 -
17.1343 -
17.1344 -------------------------------------------------------------------------------
17.1345 -"Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
17.1346 -------------------------------------------------------------------------------
17.1347 -1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)"
17.1348 -...
17.1349 -6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
17.1350 - Subproblem["sq", "rootX", "univariate", "equation"]
17.1351 -...
17.1352 -6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
17.1353 - Subproblem["normalise", "polynomial", "univariate", "equation"]
17.1354 -...
17.1355 -6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"]
17.1356 -... Or_to_List
17.1357 -6.6.3.2 "UniversalList"
17.1358 -------------------------------------------------------------------------------
17.1359 -(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n]
17.1360 -
17.1361 -(6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n]
17.1362 -------------------------------------------------------------------------------
17.1363 -*)
17.1364 -(*sh. comments auf 498*)
17.1365 -"--------- fun dropwhile' ----------------------------------------";
17.1366 -"--------- fun dropwhile' ----------------------------------------";
17.1367 -"--------- fun dropwhile' ----------------------------------------";
17.1368 -(*
17.1369 - fun equal a b = a=b;
17.1370 - val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5];
17.1371 - val r_foder = rev foder; val r_ifoder = rev ifoder;
17.1372 - dropwhile' equal r_foder r_ifoder;
17.1373 -> vval it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list
17.1374 -
17.1375 - val foder = [3,4,5]; val ifoder = [11,12,3,4,5];
17.1376 - val r_foder = rev foder; val r_ifoder = rev ifoder;
17.1377 - dropwhile' equal r_foder r_ifoder;
17.1378 -> val it = ([3], [3, 12, 11]) : int list * int list
17.1379 -
17.1380 - val foder = [5]; val ifoder = [11,12,3,4,5];
17.1381 - val r_foder = rev foder; val r_ifoder = rev ifoder;
17.1382 - dropwhile' equal r_foder r_ifoder;
17.1383 -> val it = ([5], [5, 4, 3, 12, 11]) : int list * int list
17.1384 -
17.1385 - val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5];
17.1386 - val r_foder = rev foder; val r_ifoder = rev ifoder;
17.1387 - dropwhile' equal r_foder r_ifoder;
17.1388 -> *** dropwhile': did not start with equal elements*)
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Fri Apr 24 08:51:05 2020 +0200
18.3 @@ -0,0 +1,1384 @@
18.4 +(* Title: "Interpret/error-pattern.sml"
18.5 + Author: Walther Neuper 060225,
18.6 + (c) due to copyright terms
18.7 +
18.8 +Strange ERROR "Undefined fact: "all_left""
18.9 +*)
18.10 +
18.11 +"-----------------------------------------------------------------";
18.12 +"table of contents -----------------------------------------------";
18.13 +"-----------------------------------------------------------------";
18.14 +"appendForm with miniscript with mini-subpbl:";
18.15 +"--------- appendFormula: on Res + equ_nrls ----------------------";
18.16 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
18.17 +"--------- appendFormula: on Res + NO deriv ----------------------";
18.18 +"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
18.19 +"replaceForm with miniscript with mini-subpbl:";
18.20 +"--------- replaceFormula: on Res + = ----------------------------";
18.21 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
18.22 +"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
18.23 +"--------- replaceFormula: cut calculation -----------------------";
18.24 +"--------- replaceFormula: cut calculation -----------------------";
18.25 +(* 040307 copied from informtest.sml ... old versions
18.26 +"--------- maximum-example, UC: Modeling / modifyCalcHead --------";*)
18.27 +"--------- syntax error ------------------------------------------";
18.28 +"CAS-command:";
18.29 +"--------- CAS-command on ([],Pbl) -------------------------------";
18.30 +"--------- CAS-command on ([],Pbl) FE-interface ------------------";
18.31 +"--------- locate_input_term [rational,simplification] ----------------------";
18.32 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
18.33 +"--------- Take as 1st tac, start from exp -----------------------";
18.34 +"--------- implicit_take, start with <NEW> (CAS input) ---------------";
18.35 +"--------- build fun check_for' ------------------------------";
18.36 +"--------- build fun check_for' ?bdv -------------------------";
18.37 +"--------- build fun check_for ------------------------";
18.38 +"--------- embed fun check_for ------------------------";
18.39 +"--------- embed fun find_fill_patterns ---------------------------";
18.40 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
18.41 +"--------- fun appl_adds -----------------------------------------";
18.42 +"--------- fun concat_deriv --------------------------------------";
18.43 +"--------- handle an input formula -------------------------------";
18.44 +"--------- fun dropwhile' ----------------------------------------";
18.45 +"-----------------------------------------------------------------";
18.46 +"-----------------------------------------------------------------";
18.47 +"-----------------------------------------------------------------";
18.48 +
18.49 +
18.50 +"--------- appendFormula: on Res + equ_nrls ----------------------";
18.51 +"--------- appendFormula: on Res + equ_nrls ----------------------";
18.52 +"--------- appendFormula: on Res + equ_nrls ----------------------";
18.53 + val Prog sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
18.54 + (writeln o UnparseC.term) sc;
18.55 + val Prog sc = (#scr o get_met) ["Test","solve_linear"];
18.56 + (writeln o UnparseC.term) sc;
18.57 +
18.58 + reset_states ();
18.59 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
18.60 + ("Test", ["sqroot-test","univariate","equation","test"],
18.61 + ["Test","squ-equ-test-subpbl1"]))];
18.62 + Iterator 1; moveActiveRoot 1;
18.63 + autoCalculate 1 CompleteCalcHead;
18.64 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
18.65 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
18.66 +
18.67 + appendFormula 1 "-2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1);
18.68 + val ((pt,_),_) = get_calc 1;
18.69 + val str = pr_ctree pr_short pt;
18.70 +if str =
18.71 +(". ----- pblobj -----\n" ^
18.72 +"1. x + 1 = 2\n" ^
18.73 +"2. x + 1 + -1 * 2 = 0\n" ^
18.74 +"2.1. x + 1 + -1 * 2 = 0\n" ^
18.75 +"2.2. 1 + x + -1 * 2 = 0\n" ^
18.76 +"2.3. 1 + (x + -1 * 2) = 0\n" ^
18.77 +"2.4. 1 + (x + -2) = 0\n" ^
18.78 +"2.5. 1 + (x + -2 * 1) = 0\n" ^
18.79 +"2.6. 1 + x + -2 * 1 = 0\n" ) then ()
18.80 +else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
18.81 +
18.82 + moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
18.83 + moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
18.84 +
18.85 + (*the seven steps of detailed derivation*)
18.86 + moveDown 1 ([1 ],Res); refFormula 1 ([2,1],Frm);
18.87 + moveDown 1 ([2,1],Frm); refFormula 1 ([2,1],Res);
18.88 + moveDown 1 ([2,1],Res); refFormula 1 ([2,2],Res);
18.89 + moveDown 1 ([2,2],Res); refFormula 1 ([2,3],Res);
18.90 + moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);
18.91 + moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
18.92 + moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
18.93 + val ((pt,_),_) = get_calc 1;
18.94 + if "-2 * 1 + (1 + x) = 0" = UnparseC.term (fst (get_obj g_result pt [2,6])) then()
18.95 + else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
18.96 +
18.97 + fetchProposedTactic 1; (*takes Iterator 1 _1_*)
18.98 +(* <ERROR> error in kernel </ERROR> ALREADY IN 2009-2*)
18.99 +(*========== inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 =============
18.100 + val (_,(tac,_,_)::_) = get_calc 1;
18.101 + if tac = Rewrite_Set "Test_simplify" then ()
18.102 + else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
18.103 +============ inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============*)
18.104 +
18.105 + autoCalculate 1 CompleteCalc;
18.106 + val ((pt,_),_) = get_calc 1;
18.107 + if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
18.108 + else error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
18.109 + (* autoCalculate 1 CompleteCalc;
18.110 + val ((pt,p),_) = get_calc 1;
18.111 + (writeln o istates2str) (get_obj g_loc pt [ ]);
18.112 + (writeln o istates2str) (get_obj g_loc pt [1]);
18.113 + (writeln o istates2str) (get_obj g_loc pt [2]);
18.114 + (writeln o istates2str) (get_obj g_loc pt [3]);
18.115 + (writeln o istates2str) (get_obj g_loc pt [3,1]);
18.116 + (writeln o istates2str) (get_obj g_loc pt [3,2]);
18.117 + (writeln o istates2str) (get_obj g_loc pt [4]);
18.118 +
18.119 + *)
18.120 +"----------------------------------------------------------";
18.121 +
18.122 + val fod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls
18.123 + ((#rules o Rule_Set.rep) Test_simplify)
18.124 + (sqrt_right false (@{theory "Pure"})) NONE
18.125 + (str2term "x + 1 + -1 * 2 = 0");
18.126 + (writeln o Derive.trtas2str) fod;
18.127 +
18.128 + val ifod = Derive.do_one (@{theory "Isac_Knowledge"}) Atools_erls
18.129 + ((#rules o Rule_Set.rep) Test_simplify)
18.130 + (sqrt_right false (@{theory "Pure"})) NONE
18.131 + (str2term "-2 * 1 + (1 + x) = 0");
18.132 + (writeln o Derive.trtas2str) ifod;
18.133 + fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
18.134 + val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
18.135 + val der = fod' @ (map Derive.rev_deriv' rifod');
18.136 + (writeln o Derive.trtas2str) der;
18.137 + "----------------------------------------------------------";
18.138 +DEconstrCalcTree 1;
18.139 +
18.140 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
18.141 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
18.142 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
18.143 + reset_states ();
18.144 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
18.145 + ("Test", ["sqroot-test","univariate","equation","test"],
18.146 + ["Test","squ-equ-test-subpbl1"]))];
18.147 + Iterator 1; moveActiveRoot 1;
18.148 + autoCalculate 1 CompleteCalcHead;
18.149 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
18.150 + appendFormula 1 "2+ -1 + x = 2" (*|> Future.join*); refFormula 1 (get_pos 1 1);
18.151 +
18.152 + moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
18.153 +
18.154 + moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm);
18.155 + moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res);
18.156 + moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res);
18.157 + moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res);
18.158 + moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res);
18.159 + moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res);
18.160 + moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res);
18.161 + val ((pt,_),_) = get_calc 1;
18.162 + if "2 + -1 + x = 2" = UnparseC.term (fst (get_obj g_result pt [1,6])) then()
18.163 + else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";
18.164 +
18.165 + fetchProposedTactic 1; (*takes Iterator 1 _1_*)
18.166 + val (_,(tac,_,_)::_) = get_calc 1;
18.167 + case tac of Rewrite_Set "norm_equation" => ()
18.168 + | _ => error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
18.169 + autoCalculate 1 CompleteCalc;
18.170 + val ((pt,_),_) = get_calc 1;
18.171 + if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
18.172 + else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
18.173 +DEconstrCalcTree 1;
18.174 +
18.175 +"--------- appendFormula: on Res + NO deriv ----------------------";
18.176 +"--------- appendFormula: on Res + NO deriv ----------------------";
18.177 +"--------- appendFormula: on Res + NO deriv ----------------------";
18.178 + reset_states ();
18.179 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
18.180 + ("Test", ["sqroot-test","univariate","equation","test"],
18.181 + ["Test","squ-equ-test-subpbl1"]))];
18.182 + Iterator 1; moveActiveRoot 1;
18.183 + autoCalculate 1 CompleteCalcHead;
18.184 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
18.185 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
18.186 +
18.187 + appendFormula 1 "x = 2" (*|> Future.join*);
18.188 + val ((pt,p),_) = get_calc 1;
18.189 + val str = pr_ctree pr_short pt;
18.190 + writeln str;
18.191 + if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res)
18.192 + then ()
18.193 + else error "inform.sml: diff.behav.appendFormula: Res + NOder 1";
18.194 +
18.195 + fetchProposedTactic 1;
18.196 + val (_,(tac,_,_)::_) = get_calc 1;
18.197 + case tac of Rewrite_Set "Test_simplify" => ()
18.198 + | _ => error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
18.199 + autoCalculate 1 CompleteCalc;
18.200 + val ((pt,_),_) = get_calc 1;
18.201 + if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
18.202 + else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
18.203 +DEconstrCalcTree 1;
18.204 +
18.205 +"--------- appendFormula: on Res + late deriv --------------------";
18.206 +"--------- appendFormula: on Res + late deriv --------------------";
18.207 +"--------- appendFormula: on Res + late deriv --------------------";
18.208 +(*cp with "fun me" to test/../lucas-interpreter.sml:
18.209 + re-build: fun locate_input_term ---------------------------------------------------";
18.210 +*)
18.211 + reset_states ();
18.212 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
18.213 + ("Test", ["sqroot-test","univariate","equation","test"],
18.214 + ["Test","squ-equ-test-subpbl1"]))];
18.215 + Iterator 1; moveActiveRoot 1;
18.216 + autoCalculate 1 CompleteCalcHead;
18.217 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
18.218 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
18.219 +
18.220 + appendFormula 1 "x = 1" (*|> Future.join*);
18.221 + val ((pt,p),_) = get_calc 1;
18.222 + val str = pr_ctree pr_short pt;
18.223 + writeln str;
18.224 + if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n3.2.1. x = 0 + -1 * -1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res)
18.225 + then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
18.226 + else error "inform.sml: diff.behav.appendFormula: Res + late d 1";
18.227 +
18.228 + fetchProposedTactic 1;
18.229 + val (_,(tac,_,_)::_) = get_calc 1;
18.230 + case tac of Check_Postcond ["LINEAR", "univariate", "equation", "test"] => ()
18.231 + | _ => error "inform.sml: diff.behav.appendFormula: Res + late d 2";
18.232 + autoCalculate 1 CompleteCalc;
18.233 + val ((pt,_),_) = get_calc 1;
18.234 + if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
18.235 + else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
18.236 +DEconstrCalcTree 1;
18.237 +
18.238 +"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
18.239 +"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
18.240 +"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
18.241 + reset_states ();
18.242 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
18.243 + ("Test", ["sqroot-test","univariate","equation","test"],
18.244 + ["Test","squ-equ-test-subpbl1"]))];
18.245 + Iterator 1; moveActiveRoot 1;
18.246 + autoCalculate 1 CompleteCalcHead;
18.247 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
18.248 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
18.249 + appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*);
18.250 + val ((pt,p),_) = get_calc 1;
18.251 + val str = pr_ctree pr_short pt;
18.252 + writeln str;
18.253 + if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = -2 + 3]\n4.3. [x = 3 + -2]\n" then ()
18.254 + else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
18.255 + autoCalculate 1 CompleteCalc;
18.256 + val ((pt,p),_) = get_calc 1;
18.257 + if "[x = 3 + -2 * 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
18.258 + (* ~~~~~~~~~~ simplify as last step in any script ?!*)
18.259 + else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
18.260 +DEconstrCalcTree 1;
18.261 +
18.262 +"--------- replaceFormula: on Res + = ----------------------------";
18.263 +"--------- replaceFormula: on Res + = ----------------------------";
18.264 +"--------- replaceFormula: on Res + = ----------------------------";
18.265 + reset_states ();
18.266 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
18.267 + ("Test", ["sqroot-test","univariate","equation","test"],
18.268 + ["Test","squ-equ-test-subpbl1"]))];
18.269 + Iterator 1; moveActiveRoot 1;
18.270 + autoCalculate 1 CompleteCalcHead;
18.271 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
18.272 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
18.273 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*-1 + x*);
18.274 +
18.275 + replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
18.276 + val ((pt,_),_) = get_calc 1;
18.277 + val str = pr_ctree pr_short pt;
18.278 +
18.279 +(* before AK110725 this was
18.280 +". ----- pblobj -----\n
18.281 +1. x + 1 = 2\n
18.282 +2. x + 1 + -1 * 2 = 0\n
18.283 +2.1. x + 1 + -1 * 2 = 0\n
18.284 +2.2. 1 + x + -1 * 2 = 0\n
18.285 +2.3. 1 + (x + -1 * 2) = 0\n
18.286 +2.4. 1 + (x + -2) = 0\n
18.287 +2.5. 1 + (x + -2 * 1) = 0\n
18.288 +2.6. 1 + x + -2 * 1 = 0\n";
18.289 +*)
18.290 +if str =
18.291 +". ----- pblobj -----\n"^
18.292 +"1. x + 1 = 2\n"^
18.293 +"2. x + 1 + -1 * 2 = 0\n"^
18.294 +"2.1. x + 1 + -1 * 2 = 0\n"^
18.295 +"2.2. 1 + x + -1 * 2 = 0\n"^
18.296 +"2.3. 1 + (x + -1 * 2) = 0\n"^
18.297 +"2.4. 1 + (x + -2) = 0\n"^
18.298 +"2.5. 1 + (x + -2 * 1) = 0\n"^
18.299 +"2.6. 1 + x + -2 * 1 = 0\n" then()
18.300 +else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
18.301 +
18.302 + autoCalculate 1 CompleteCalc;
18.303 + val ((pt,pos as (p,_)),_) = get_calc 1;
18.304 + if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst) (get_obj g_result pt p) then()
18.305 + else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
18.306 +DEconstrCalcTree 1;
18.307 +
18.308 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
18.309 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
18.310 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
18.311 + reset_states ();
18.312 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
18.313 + ("Test", ["sqroot-test","univariate","equation","test"],
18.314 + ["Test","squ-equ-test-subpbl1"]))];
18.315 + Iterator 1; moveActiveRoot 1;
18.316 + autoCalculate 1 CompleteCalcHead;
18.317 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
18.318 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
18.319 +
18.320 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
18.321 + val ((pt,_),_) = get_calc 1;
18.322 + val str = pr_ctree pr_short pt;
18.323 + writeln str;
18.324 + if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
18.325 + else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
18.326 + autoCalculate 1 CompleteCalc;
18.327 + val ((pt,pos as (p,_)),_) = get_calc 1;
18.328 + if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
18.329 + else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
18.330 +DEconstrCalcTree 1;
18.331 +
18.332 +"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
18.333 +"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
18.334 +"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
18.335 + reset_states ();
18.336 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
18.337 + ("Test", ["sqroot-test","univariate","equation","test"],
18.338 + ["Test","squ-equ-test-subpbl1"]))];
18.339 + Iterator 1; moveActiveRoot 1;
18.340 + autoCalculate 1 CompleteCalcHead;
18.341 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
18.342 +
18.343 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
18.344 + val ((pt,_),_) = get_calc 1;
18.345 + val str = pr_ctree pr_short pt;
18.346 + writeln str;
18.347 + if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
18.348 + else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
18.349 + autoCalculate 1 CompleteCalc;
18.350 + val ((pt,pos as (p,_)),_) = get_calc 1;
18.351 + if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
18.352 + else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
18.353 +DEconstrCalcTree 1;
18.354 +
18.355 +"--------- replaceFormula: cut calculation -----------------------";
18.356 +"--------- replaceFormula: cut calculation -----------------------";
18.357 +"--------- replaceFormula: cut calculation -----------------------";
18.358 + reset_states ();
18.359 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
18.360 + ("Test", ["sqroot-test","univariate","equation","test"],
18.361 + ["Test","squ-equ-test-subpbl1"]))];
18.362 + Iterator 1; moveActiveRoot 1;
18.363 + autoCalculate 1 CompleteCalc;
18.364 + moveActiveRoot 1; moveActiveDown 1;
18.365 + if get_pos 1 1 = ([1], Frm) then ()
18.366 + else error "inform.sml: diff.behav. cut calculation 1";
18.367 +
18.368 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
18.369 + val ((pt,p),_) = get_calc 1;
18.370 + val str = pr_ctree pr_short pt;
18.371 + writeln str;
18.372 + if p = ([1], Res) then ()
18.373 + else error "inform.sml: diff.behav. cut calculation 2";
18.374 +
18.375 +
18.376 +(* 040307 copied from informtest.sml; ... old version
18.377 + "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
18.378 + "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
18.379 + "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
18.380 +
18.381 + val p = ([],Pbl);
18.382 + val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
18.383 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
18.384 + "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
18.385 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
18.386 + (*^^^ these are the elements for the root-problem (in variants)*)
18.387 + (*vvv these are elements required for subproblems*)
18.388 + "boundVariable a","boundVariable b","boundVariable alpha",
18.389 + "interval {x::real. 0 <= x & x <= 2*r}",
18.390 + "interval {x::real. 0 <= x & x <= 2*r}",
18.391 + "interval {x::real. 0 <= x & x <= pi}",
18.392 + "errorBound (eps=(0::real))"]
18.393 + (*specifying is not interesting for this example*)
18.394 + val spec = ("DiffApp", ["maximum_of","function"],
18.395 + ["DiffApp","max_by_calculus"]);
18.396 + (*the empty model with descriptions for user-guidance by Model_Problem*)
18.397 + val empty_model = [Given ["fixedValues []"],
18.398 + Find ["maximum", "valuesFor"],
18.399 + Relate ["relations []"]];
18.400 +
18.401 +
18.402 + (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*)
18.403 + val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)];
18.404 + (*val nxt = ("Model_Problem", ...*)
18.405 + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.406 +
18.407 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.408 + (*nxt = Add_Given "fixedValues [r = Arbfix]"*)
18.409 + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.410 +(*[
18.411 +(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),
18.412 +(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),
18.413 +(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
18.414 +(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)
18.415 +
18.416 + (*the empty CalcHead is checked w.r.t the model and re-established as such*)
18.417 + val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, Spec.empty);
18.418 + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.419 + if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then () else error "informtest.sml: diff.behav. max 1";
18.420 +
18.421 + (*there is one input to the model (could be more)*)
18.422 + val (b,pt,ocalhd) =
18.423 + input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
18.424 + Find ["maximum", "valuesFor"],
18.425 + Relate ["relations"]], Pbl, Spec.empty);
18.426 + val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.427 + if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then ()
18.428 + else error "informtest.sml: diff.behav. max 2";
18.429 +
18.430 + (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME
18.431 + val (b,pt''''',ocalhd) =
18.432 + input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
18.433 + Find ["maximum A", "valuesFor [a,b]"],
18.434 + Relate ["relations [A=a*b, a/2=r*sin alpha, \
18.435 + \b/2=r*cos alpha]"]], Pbl, Spec.empty);
18.436 + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.437 + if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*)
18.438 +
18.439 + (*this input is complete in variant 1 (variant 3 does not work yet)*)
18.440 + val (b,pt''''',ocalhd) =
18.441 + input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
18.442 + Find ["maximum A", "valuesFor [a,b]"],
18.443 + Relate ["relations [A=a*b, \
18.444 + \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]],
18.445 + Pbl, Spec.empty);
18.446 + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.447 +
18.448 + modifycalcheadOK2xml 111 (bool2str b) ocalhd;
18.449 +*)
18.450 +DEconstrCalcTree 1;
18.451 +
18.452 +"--------- syntax error ------------------------------------------";
18.453 +"--------- syntax error ------------------------------------------";
18.454 +"--------- syntax error ------------------------------------------";
18.455 + reset_states ();
18.456 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
18.457 + ("Test", ["sqroot-test","univariate","equation","test"],
18.458 + ["Test","squ-equ-test-subpbl1"]))];
18.459 + Iterator 1; moveActiveRoot 1;
18.460 + autoCalculate 1 CompleteCalcHead;
18.461 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
18.462 + autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
18.463 +
18.464 + appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
18.465 + val ((pt,_),_) = get_calc 1;
18.466 + val str = pr_ctree pr_short pt;
18.467 + writeln str;
18.468 + if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
18.469 + else error "inform.sml: diff.behav.appendFormula: syntax error";
18.470 +DEconstrCalcTree 1;
18.471 +
18.472 +"--------- CAS-command on ([],Pbl) -------------------------------";
18.473 +"--------- CAS-command on ([],Pbl) -------------------------------";
18.474 +"--------- CAS-command on ([],Pbl) -------------------------------";
18.475 +val (p,_,f,nxt,_,pt) =
18.476 + CalcTreeTEST [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
18.477 +val ifo = "solve(x+1=2,x)";
18.478 +val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve(x+1=2,x)";
18.479 +show_pt pt;
18.480 +val nxt = (Apply_Method ["Test","squ-equ-test-subpbl1"]);
18.481 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
18.482 +if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()
18.483 +else error "inform.sml: diff.behav. CAScmd ([],Pbl)";
18.484 +DEconstrCalcTree 1;
18.485 +
18.486 +"--------- CAS-command on ([],Pbl) FE-interface ------------------";
18.487 +"--------- CAS-command on ([],Pbl) FE-interface ------------------";
18.488 +"--------- CAS-command on ([],Pbl) FE-interface ------------------";
18.489 +reset_states ();
18.490 +CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
18.491 +Iterator 1;
18.492 +moveActiveRoot 1;
18.493 +replaceFormula 1 "solve(x+1=2,x)";
18.494 +autoCalculate 1 CompleteCalc;
18.495 +val ((pt,p),_) = get_calc 1;
18.496 +show_pt pt;
18.497 +if p = ([], Res) then ()
18.498 +else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
18.499 +DEconstrCalcTree 1;
18.500 +
18.501 +"--------- inform [rational,simplification] ----------------------";
18.502 +"--------- inform [rational,simplification] ----------------------";
18.503 +"--------- inform [rational,simplification] ----------------------";
18.504 +reset_states ();
18.505 +CalcTree [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"],
18.506 + ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
18.507 +Iterator 1; moveActiveRoot 1;
18.508 +autoCalculate 1 CompleteCalcHead;
18.509 +
18.510 +"--- (-1) give a preview on the calculation without any input";
18.511 +(*
18.512 +autoCalculate 1 CompleteCalc;
18.513 +val ((pt, p), _) = get_calc 1;
18.514 +show_pt pt;
18.515 +[
18.516 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
18.517 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
18.518 +(([1], Res), a / b + c / d + e / f), <--- (1) input arbitrary
18.519 +(([2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
18.520 +(([3], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
18.521 +(([4], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f)), <--- (2) input next
18.522 +(([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))] <--- (3) is also final result
18.523 + EXAMPLE NOT OPTIMAL
18.524 +*)
18.525 +"--- (0) user input as the *first* step does not work, thus impdo at least 1 step";
18.526 +autoCalculate 1 (Steps 1);
18.527 +autoCalculate 1 (Steps 1);
18.528 +val ((pt, p), _) = get_calc 1;
18.529 +(*show_pt pt;
18.530 +[
18.531 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
18.532 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
18.533 +(([1], Res), a / b + c / d + e / f)]
18.534 +*)
18.535 +"--- (1) input an arbitrary next formula";
18.536 +appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f" (*|> Future.join*);
18.537 +val ((pt, p), _) = get_calc 1;
18.538 +(*show_pt pt;
18.539 +[
18.540 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
18.541 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
18.542 +(([1], Res), a / b + c / d + e / f),
18.543 +(([2,1], Frm), a / b + c / d + e / f),
18.544 +(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
18.545 +(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
18.546 +(([2], Res), (a * d + c * b) / (b * d) + e / f)]
18.547 +*)
18.548 +val ((pt,p),_) = get_calc 1;
18.549 +if p = ([2], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
18.550 +else error ("inform.sml: [rational,simplification] 1");
18.551 +
18.552 +"--- (2) input the next formula that would be presented by mat-engine";
18.553 +(* generate a preview:
18.554 +autoCalculate 1 (Steps 1);
18.555 +val ((pt, p), _) = get_calc 1;
18.556 +show_pt pt;
18.557 +[
18.558 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
18.559 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
18.560 +(([1], Res), a / b + c / d + e / f),
18.561 +(([2,1], Frm), a / b + c / d + e / f),
18.562 +(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
18.563 +(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
18.564 +(([2], Res), (a * d + c * b) / (b * d) + e / f),
18.565 +(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))] <--- input this
18.566 +*)
18.567 +appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
18.568 +val ((pt, p), _) = get_calc 1;
18.569 +(*show_pt pt;
18.570 +[
18.571 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
18.572 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
18.573 +(([1], Res), a / b + c / d + e / f),
18.574 +(([2,1], Frm), a / b + c / d + e / f),
18.575 +(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
18.576 +(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
18.577 +(([2], Res), (a * d + c * b) / (b * d) + e / f),
18.578 +(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))]
18.579 +*)
18.580 +if p = ([3], Res) andalso (length o children o (get_nd pt)) (fst p) = 0 then ()
18.581 +else error ("inform.sml: [rational,simplification] 2");
18.582 +
18.583 +"--- (3) input the exact final result";
18.584 +appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
18.585 +val ((pt, p), _) = get_calc 1;
18.586 +(*show_pt pt;
18.587 +[
18.588 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
18.589 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
18.590 +(([1], Res), a / b + c / d + e / f),
18.591 +(([2,1], Frm), a / b + c / d + e / f),
18.592 +(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
18.593 +(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
18.594 +(([2], Res), (a * d + c * b) / (b * d) + e / f),
18.595 +(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
18.596 +(([4,1], Frm), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
18.597 +(([4,1], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
18.598 +(([4,2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
18.599 +(([4], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))]
18.600 +*)
18.601 +if p = ([4], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
18.602 +else error ("inform.sml: [rational,simplification] 3");
18.603 +
18.604 +"--- (4) finish the calculation + check the postcondition (in the future)";
18.605 +autoCalculate 1 CompleteCalc;
18.606 +val ((pt, p), _) = get_calc 1;
18.607 +val (t, asm) = get_obj g_result pt [];
18.608 +if UnparseC.term t = "(a * d * f + b * c * f + b * d * e) / (b * d * f)" andalso
18.609 +UnparseC.terms asm = "[\"b * d * f \<noteq> 0\",\"d \<noteq> 0\",\"b \<noteq> 0\",\"a * x / (b * x) + c * x / (d * x) + e / f is_ratpolyexp\"]"
18.610 +then () else error "inform [rational,simplification] changed at end";
18.611 +(*show_pt pt;
18.612 +[
18.613 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
18.614 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
18.615 +(([1], Res), a / b + c / d + e / f),
18.616 +(([2,1], Frm), a / b + c / d + e / f),
18.617 +(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
18.618 +(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
18.619 +(([2], Res), (a * d + c * b) / (b * d) + e / f),
18.620 +(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
18.621 +(([4,1], Frm), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
18.622 +(([4,1], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
18.623 +(([4,2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
18.624 +(([4], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
18.625 +(([5], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
18.626 +(([6], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f)),
18.627 +(([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))]
18.628 +*)
18.629 +DEconstrCalcTree 1;
18.630 +
18.631 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
18.632 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
18.633 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
18.634 +val t = str2term "Diff (x^^^2 + x + 1, x)";
18.635 +case t of Const ("Diff.Diff", _) $ _ => ()
18.636 + | _ => raise
18.637 + error "diff.sml behav.changed for CAS Diff (..., x)";
18.638 +atomty t;
18.639 +"-----------------------------------------------------------------";
18.640 +(*1>*)reset_states ();
18.641 +(*2>*)CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
18.642 +(*3>*)Iterator 1;moveActiveRoot 1;
18.643 +"----- here the Headline has been finished";
18.644 +(*4>*)moveActiveFormula 1 ([],Pbl);
18.645 +(*5>*)replaceFormula 1 "Diff (x^2 + x + 1, x)";
18.646 +val ((pt,_),_) = get_calc 1;
18.647 +val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
18.648 +val NONE = env;
18.649 +val (SOME istate, NONE) = loc;
18.650 +(*default_print_depth 5;*)
18.651 +writeln"-----------------------------------------------------------";
18.652 +spec;
18.653 +writeln (itms2str_ ctxt probl);
18.654 +writeln (itms2str_ ctxt meth);
18.655 +writeln (Istate.string_of (fst istate));
18.656 +
18.657 +refFormula 1 ([],Pbl) (*--> correct CalcHead*);
18.658 + (*081016 NOT necessary (but leave it in Java):*)
18.659 +(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
18.660 +"----- here the CalcHead has been completed --- ONCE MORE ?????";
18.661 +
18.662 +(***difference II***)
18.663 +val ((pt,p),_) = get_calc 1;
18.664 +(*val p = ([], Pbl)*)
18.665 +val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
18.666 +val NONE = env;
18.667 +val (SOME istate, NONE) = loc;
18.668 +(*default_print_depth 5;*) writeln (Istate.string_of (fst istate)); (*default_print_depth 3;*)
18.669 +(*Pstate ([],
18.670 + [], NONE,
18.671 + ??.empty, Sundef, false)*)
18.672 +(*default_print_depth 5;*) spec; (*default_print_depth 3;*)
18.673 +(*("Isac_Knowledge",
18.674 + ["derivative_of", "function"],
18.675 + ["diff", "differentiate_on_R"]) : spec*)
18.676 +writeln (itms2str_ ctxt probl);
18.677 +(*[
18.678 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
18.679 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
18.680 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
18.681 +writeln (itms2str_ ctxt meth);
18.682 +(*[
18.683 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
18.684 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
18.685 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
18.686 +writeln"-----------------------------------------------------------";
18.687 +(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
18.688 +(*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
18.689 +autoCalculate 1 CompleteCalc;
18.690 +val ((pt,p),_) = get_calc 1;
18.691 +val Form res = (#1 o pt_extract) (pt, ([],Res));
18.692 +show_pt pt;
18.693 +if p = ([], Res) andalso UnparseC.term res = "1 + 2 * x" then ()
18.694 +else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
18.695 +DEconstrCalcTree 1;
18.696 +
18.697 +"--------- Take as 1st tac, start from exp -----------------------";
18.698 +"--------- Take as 1st tac, start from exp -----------------------";
18.699 +"--------- Take as 1st tac, start from exp -----------------------";
18.700 +(*the following input is copied from BridgeLog Java <==> SML,
18.701 + omitting unnecessary inputs*)
18.702 +(*1>*)reset_states ();
18.703 +(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac_Knowledge",["derivative_of","function"],["diff","differentiate_on_R"]))];
18.704 +(*3>*)Iterator 1; moveActiveRoot 1;
18.705 +
18.706 +(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
18.707 +(***difference II***)
18.708 +val ((pt,_),_) = get_calc 1;
18.709 +val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
18.710 +val NONE = env;
18.711 +val (SOME istate, NONE) = loc;
18.712 +(*default_print_depth 5;*) writeln (Istate.string_of (fst istate)); (*default_print_depth 3;*)
18.713 +(*Pstate ([],
18.714 + [], NONE,
18.715 + ??.empty, Sundef, false)*)
18.716 +(*default_print_depth 5;*) spec; (*default_print_depth 3;*)
18.717 +(*("Isac_Knowledge",
18.718 + ["derivative_of", "function"],
18.719 + ["diff", "differentiate_on_R"]) : spec*)
18.720 +writeln (itms2str_ ctxt probl);
18.721 +(*[
18.722 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
18.723 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
18.724 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
18.725 +writeln (itms2str_ ctxt meth);
18.726 +(*[
18.727 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
18.728 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
18.729 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
18.730 +writeln"-----------------------------------------------------------";
18.731 +(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
18.732 +autoCalculate 1 (Steps 1);
18.733 +val ((pt,p),_) = get_calc 1;
18.734 +val Form res = (#1 o pt_extract) (pt, p);
18.735 +if UnparseC.term res = "d_d x (x ^^^ 2 + x + 1)" then ()
18.736 +else error "diff.sml Diff (x^2 + x + 1, x) from exp";
18.737 +DEconstrCalcTree 1;
18.738 +
18.739 +"--------- implicit_take, start with <NEW> (CAS input) ---------------";
18.740 +"--------- implicit_take, start with <NEW> (CAS input) ---------------";
18.741 +"--------- implicit_take, start with <NEW> (CAS input) ---------------";
18.742 +reset_states ();
18.743 +CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
18.744 +(*[[from sml: > @@@@@begin@@@@@
18.745 +[[from sml: 1
18.746 +[[from sml: <CALCTREE>
18.747 +[[from sml: <CALCID> 1 </CALCID>
18.748 +[[from sml: </CALCTREE>
18.749 +[[from sml: @@@@@end@@@@@*)
18.750 +Iterator 1;
18.751 +(*[[from sml: > @@@@@begin@@@@@
18.752 +[[from sml: 1
18.753 +[[from sml: <ADDUSER>
18.754 +[[from sml: <CALCID> 1 </CALCID>
18.755 +[[from sml: <USERID> 1 </USERID>
18.756 +[[from sml: </ADDUSER>
18.757 +[[from sml: @@@@@end@@@@@*)
18.758 +moveActiveRoot 1;
18.759 +(*[[from sml: > @@@@@begin@@@@@
18.760 +[[from sml: 1
18.761 +[[from sml: <CALCITERATOR>
18.762 +[[from sml: <CALCID> 1 </CALCID>
18.763 +[[from sml: <POSITION>
18.764 +[[from sml: <INTLIST>
18.765 +[[from sml: </INTLIST>
18.766 +[[from sml: <POS> Pbl </POS>
18.767 +[[from sml: </POSITION>
18.768 +[[from sml: </CALCITERATOR>
18.769 +[[from sml: @@@@@end@@@@@*)
18.770 +getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
18.771 +(*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
18.772 +[[from sml: 1
18.773 +[[from sml: <GETELEMENTSFROMTO>
18.774 +[[from sml: <CALCID> 1 </CALCID>
18.775 +[[from sml: <FORMHEADS>
18.776 +[[from sml: <CALCFORMULA>
18.777 +[[from sml: <POSITION>
18.778 +[[from sml: <INTLIST>
18.779 +[[from sml: </INTLIST>
18.780 +[[from sml: <POS> Pbl </POS>
18.781 +[[from sml: </POSITION>
18.782 +[[from sml: <FORMULA>
18.783 +[[from sml: <MATHML>
18.784 +[[from sml: <ISA> ________________________________________________ </ISA>
18.785 +[[from sml: </MATHML>
18.786 +[[from sml:
18.787 +[[from sml: </FORMULA>
18.788 +[[from sml: </CALCFORMULA>
18.789 +[[from sml: </FORMHEADS>
18.790 +[[from sml: </GETELEMENTSFROMTO>
18.791 +[[from sml: @@@@@end@@@@@*)
18.792 +refFormula 1 ([],Pbl);
18.793 +(*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
18.794 +[[from sml: 1
18.795 +[[from sml: <REFFORMULA>
18.796 +[[from sml: <CALCID> 1 </CALCID>
18.797 +[[from sml: <CALCHEAD status = "incorrect">
18.798 +[[from sml: <POSITION>
18.799 +[[from sml: <INTLIST>
18.800 +[[from sml: </INTLIST>
18.801 +[[from sml: <POS> Pbl </POS>
18.802 +[[from sml: </POSITION>
18.803 +[[from sml: <HEAD>
18.804 +[[from sml: <MATHML>
18.805 +[[from sml: <ISA> Problem (ThyC.id_empty, [e_pblID]) </ISA>
18.806 +[[from sml: </MATHML>
18.807 +[[from sml: </HEAD>
18.808 +[[from sml: <MODEL>
18.809 +[[from sml: <GIVEN> </GIVEN>
18.810 +[[from sml: <WHERE> </WHERE>
18.811 +[[from sml: <FIND> </FIND>
18.812 +[[from sml: <RELATE> </RELATE>
18.813 +[[from sml: </MODEL>
18.814 +[[from sml: <BELONGSTO> Pbl </BELONGSTO>
18.815 +[[from sml: <SPECIFICATION>
18.816 +[[from sml: <THEORYID> ThyC.id_empty </THEORYID>
18.817 +[[from sml: <PROBLEMID>
18.818 +[[from sml: <STRINGLIST>
18.819 +[[from sml: <STRING> Problem.id_empty </STRING>
18.820 +[[from sml: </STRINGLIST>
18.821 +[[from sml: </PROBLEMID>
18.822 +[[from sml: <METHODID>
18.823 +[[from sml: <STRINGLIST>
18.824 +[[from sml: <STRING> e_metID </STRING>
18.825 +[[from sml: </STRINGLIST>
18.826 +[[from sml: </METHODID>
18.827 +[[from sml: </SPECIFICATION>
18.828 +[[from sml: </CALCHEAD>
18.829 +[[from sml: </REFFORMULA>
18.830 +[[from sml: @@@@@end@@@@@*)
18.831 +moveActiveFormula 1 ([],Pbl);
18.832 +(*[[from sml: > @@@@@begin@@@@@
18.833 +[[from sml: 1
18.834 +[[from sml: <CALCITERATOR>
18.835 +[[from sml: <CALCID> 1 </CALCID>
18.836 +[[from sml: <POSITION>
18.837 +[[from sml: <INTLIST>
18.838 +[[from sml: </INTLIST>
18.839 +[[from sml: <POS> Pbl </POS>
18.840 +[[from sml: </POSITION>
18.841 +[[from sml: </CALCITERATOR>
18.842 +[[from sml: @@@@@end@@@@@*)
18.843 +replaceFormula 1 "Simplify (1+2)";
18.844 +(*[[from sml: > @@@@@begin@@@@@
18.845 +[[from sml: 1
18.846 +[[from sml: <REPLACEFORMULA>
18.847 +[[from sml: <CALCID> 1 </CALCID>
18.848 +[[from sml: <CALCCHANGED>
18.849 +[[from sml: <UNCHANGED>
18.850 +[[from sml: <INTLIST>
18.851 +[[from sml: </INTLIST>
18.852 +[[from sml: <POS> Pbl </POS>
18.853 +[[from sml: </UNCHANGED>
18.854 +[[from sml: <DELETED>
18.855 +[[from sml: <INTLIST>
18.856 +[[from sml: </INTLIST>
18.857 +[[from sml: <POS> Pbl </POS>
18.858 +[[from sml: </DELETED>
18.859 +[[from sml: <GENERATED>
18.860 +[[from sml: <INTLIST>
18.861 +[[from sml: </INTLIST>
18.862 +[[from sml: <POS> Met </POS> DIFFERENCE: Pbl
18.863 +[[from sml: </GENERATED>
18.864 +[[from sml: </CALCCHANGED>
18.865 +[[from sml: </REPLACEFORMULA>
18.866 +[[from sml: @@@@@end@@@@@*)
18.867 +getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false(* DIFFERENCE: Pbl*);
18.868 +(*@@@@@begin@@@@@
18.869 + 1
18.870 +<GETELEMENTSFROMTO>
18.871 + <CALCID> 1 </CALCID>
18.872 + <FORMHEADS>
18.873 + <CALCFORMULA>
18.874 + <POSITION>
18.875 + <INTLIST>
18.876 + </INTLIST>
18.877 + <POS> Pbl </POS>
18.878 + </POSITION>
18.879 + <FORMULA>
18.880 + <MATHML>
18.881 + <ISA> Simplify (1 + 2) </ISA> WORKS !!!!!
18.882 + </MATHML>
18.883 + </FORMULA>
18.884 + </CALCFORMULA>
18.885 + </FORMHEADS>
18.886 +</GETELEMENTSFROMTO>
18.887 +@@@@@end@@@@@*)
18.888 +getFormulaeFromTo 1 ([],Pbl) ([],Met) 0 false;
18.889 +(*[[from sml: > @@@@@begin@@@@@
18.890 +[[from sml: 1
18.891 +[[from sml: <SYSERROR>
18.892 +[[from sml: <CALCID> 1 </CALCID>
18.893 +[[from sml: <ERROR> error in getFormulaeFromTo </ERROR>
18.894 +[[from sml: </SYSERROR>
18.895 +[[from sml: @@@@@end@@@@@*)
18.896 +(*step into getFormulaeFromTo --- bug corrected...*)
18.897 +
18.898 +"--------- build fun check_for' ------------------------------";
18.899 +"--------- build fun check_for' ------------------------------";
18.900 +"--------- build fun check_for' ------------------------------";
18.901 +val subst = [(str2term "bdv", str2term "x")]: subst;
18.902 +val rls = norm_Rational
18.903 +val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
18.904 +val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
18.905 +val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "1 / 2");
18.906 +
18.907 +val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
18.908 + rew_sub thy 1 [] e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
18.909 +if rewritten then NONE else SOME "e_errpatID";
18.910 +
18.911 +val norm_res = case rewrite_set_ (Isac()) false rls res' of
18.912 + NONE => res'
18.913 +| SOME (norm_res, _) => norm_res
18.914 +
18.915 +val norm_inf = case rewrite_set_ (Isac()) false rls inf of
18.916 + NONE => inf
18.917 +| SOME (norm_inf, _) => norm_inf;
18.918 +
18.919 +res' = inf;
18.920 +norm_res = norm_inf;
18.921 +
18.922 +val pat = parse_patt @{theory} "(?a + ?b)/?a = ?b";
18.923 +val (res, inf) = (str2term "(2 + 3)/2", str2term "3");
18.924 +if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
18.925 +then () else error "error patt example1 changed";
18.926 +
18.927 +val pat = parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
18.928 +val (res, inf) = (str2term "(2 + 3)/(2 + 4)", str2term "3 / 4");
18.929 +if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
18.930 +then () else error "error patt example2 changed";
18.931 +
18.932 +val pat = parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
18.933 +val (res, inf) = (str2term "(2 + 3)/(3 + 4)", str2term "2 / 4");
18.934 +if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
18.935 +then () else error "error patt example3 changed";
18.936 +
18.937 +val inf = str2term "1 / 2";
18.938 +if check_for' (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
18.939 +then () else error "error patt example3 changed";
18.940 +
18.941 +"--------- build fun check_for' ?bdv -------------------------";
18.942 +"--------- build fun check_for' ?bdv -------------------------";
18.943 +"--------- build fun check_for' ?bdv -------------------------";
18.944 +val subst = [(str2term "bdv", str2term "x")]: subst;
18.945 +val t = str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))";
18.946 +val SOME (t, _) = rewrite_set_inst_ thy false subst norm_diff t;
18.947 +if UnparseC.term t = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3" then ()
18.948 +else error "build fun check_for' ?bdv changed 1";
18.949 +
18.950 +val rls = norm_diff
18.951 +val pat = parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)";
18.952 +val (res, inf) = (str2term "2 * x + d_d x (sin (x ^^^ 4))", str2term "2 * x + cos (4 * x ^^^ 3)");
18.953 +
18.954 +val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern matches in res*)
18.955 + rew_sub thy 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
18.956 +if UnparseC.term res' = "2 * x + cos (d_d x (x ^^^ 4))" andalso rewritten then ()
18.957 +else error "build fun check_for' ?bdv changed 2";
18.958 +
18.959 +val norm_res = case rewrite_set_inst_ (Isac()) false subst rls res' of
18.960 + NONE => res'
18.961 +| SOME (norm_res, _) => norm_res;
18.962 +if UnparseC.term norm_res = "2 * x + cos (4 * x ^^^ 3)" then ()
18.963 +else error "build fun check_for' ?bdv changed 3";
18.964 +
18.965 +val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of
18.966 + NONE => inf
18.967 +| SOME (norm_inf, _) => norm_inf;
18.968 +if UnparseC.term norm_inf = "2 * x + cos (4 * x ^^^ 3)" then ()
18.969 +else error "build fun check_for' ?bdv changed 4";
18.970 +
18.971 +res' = inf;
18.972 +if norm_res = norm_inf then ()
18.973 +else error "build fun check_for' ?bdv changed 5";
18.974 +
18.975 +if Error_Pattern.check_for' (res, inf) (subst: subst) ("errpatID": errpatID, pat) rls = SOME "errpatID"
18.976 +then () else error "error patt example1 changed";
18.977 +
18.978 +"--------- build fun check_for ------------------------";
18.979 +"--------- build fun check_for ------------------------";
18.980 +"--------- build fun check_for ------------------------";
18.981 +val (res, inf) =
18.982 + (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
18.983 + str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
18.984 +val {errpats, nrls = rls, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"]
18.985 +
18.986 +val env = [(str2term "v_v", str2term "x")];
18.987 +val errpats =
18.988 + [e_errpat, (*generalised for testing*)
18.989 + ("chain-rule-diff-both",
18.990 + [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
18.991 + parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
18.992 + parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
18.993 + parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
18.994 + parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
18.995 + [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
18.996 + @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
18.997 +case Error_Pattern.check_for (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
18.998 +| NONE => error "Error_Pattern.check_for broken";
18.999 +DEconstrCalcTree 1;
18.1000 +
18.1001 +"--------- embed fun check_for ------------------------";
18.1002 +"--------- embed fun check_for ------------------------";
18.1003 +"--------- embed fun check_for ------------------------";
18.1004 +reset_states ();
18.1005 +CalcTree
18.1006 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
18.1007 + ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
18.1008 +Iterator 1;
18.1009 +moveActiveRoot 1;
18.1010 +autoCalculate 1 CompleteCalcHead;
18.1011 +autoCalculate 1 (Steps 1);
18.1012 +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
18.1013 +(*autoCalculate 1 (Steps 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
18.1014 +
18.1015 +"~~~~~ fun appendFormula , args:"; val (cI, (ifo:TermC.as_string)) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
18.1016 +"~~~~~ fun appendFormula' , args:"; val (cI, (ifo: TermC.as_string)) = (cI, ifo);
18.1017 + val cs = get_calc cI
18.1018 + val pos = get_pos cI 1;
18.1019 +(*+*)if pos = ([1], Res) then () else error "inform with (positive) Error_Pattern.check_for broken 1";
18.1020 + val ("ok", cs' as (_, _, ptp)) = (*case*) Step.do_next pos cs (*of*);
18.1021 + (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*ERROR WAS: "no derivation found"*)
18.1022 +"~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Chead.calcstate'), istr)
18.1023 + = (cs', (encode ifo));
18.1024 + val ctxt = get_ctxt pt pos (*see TODO.thy*)
18.1025 + val SOME f_in = (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
18.1026 + val f_in = Thm.term_of f_in
18.1027 + val pos_pred = lev_back' pos
18.1028 + val f_pred = Ctree.get_curr_formula (pt, pos_pred);
18.1029 + (*if*) f_pred = f_in; (*else*)
18.1030 + val NONE = (*case*) In_Chead.cas_input f_in (*of*);
18.1031 + (*old* )val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
18.1032 + (*old*)val {scr = prog, ...} = Specify.get_met metID
18.1033 + (*old*)val istate = get_istate_LI pt pos
18.1034 + (*old*)val ctxt = get_ctxt pt pos
18.1035 + ( *old*)
18.1036 + val LI.Not_Derivable =
18.1037 + (*case*) LI.locate_input_term (pt, pos) f_in (*of*);
18.1038 + val pp = Ctree.par_pblobj pt p
18.1039 + val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
18.1040 + {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
18.1041 + | _ => error "inform: uncovered case of get_met"
18.1042 +;
18.1043 +(*+*)if errpats2str errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\",\"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\",\"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)\",\"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\",\"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\",\"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\",\"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1) * d_d ?bdv ?u\",\"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\",\"d_d ?bdv (E_ ^^^ ?u) = E_ ^^^ ?u * d_d ?x ?u\"]]"
18.1044 +(*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
18.1045 +
18.1046 + val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
18.1047 +;
18.1048 +(*+*)if UnparseC.term f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
18.1049 +(*+*) UnparseC.term f_in = "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)"
18.1050 +(*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2";
18.1051 +
18.1052 + val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
18.1053 +
18.1054 +"--- final check:";
18.1055 +(*+*)val (_, _, ptp') = cs';
18.1056 +case Step_Solve.by_term ptp' (encode ifo) of
18.1057 + ("error pattern #chain-rule-diff-both#", calcstate') => ()
18.1058 +| _ => error "inform with (positive) Error_Pattern.check_for broken"
18.1059 +
18.1060 +
18.1061 +"--------- embed fun find_fill_patterns ---------------------------";
18.1062 +"--------- embed fun find_fill_patterns ---------------------------";
18.1063 +"--------- embed fun find_fill_patterns ---------------------------";
18.1064 +reset_states ();
18.1065 +CalcTree
18.1066 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
18.1067 + ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
18.1068 +Iterator 1;
18.1069 +moveActiveRoot 1;
18.1070 +autoCalculate 1 CompleteCalcHead;
18.1071 +autoCalculate 1 (Steps 1);
18.1072 +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
18.1073 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);
18.1074 + (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
18.1075 + (*or
18.1076 + <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
18.1077 +
18.1078 +"~~~~~ fun findFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
18.1079 + val ((pt, _), _) = get_calc cI
18.1080 + val pos = get_pos cI 1;
18.1081 +"~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
18.1082 + val f_curr = Ctree.get_curr_formula (pt, pos);
18.1083 + val pp = Ctree.par_pblobj pt p
18.1084 + val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
18.1085 + {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
18.1086 + | _ => error "find_fill_patterns: uncovered case of get_met"
18.1087 + val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
18.1088 + val subst = Rtools.get_bdv_subst prog env
18.1089 + val errpatthms = errpats
18.1090 + |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
18.1091 + |> map (#3: errpat -> thm list)
18.1092 + |> flat;
18.1093 +
18.1094 +case map (Error_Pattern.fill_from_store subst f_curr errpatID) errpatthms |> flat of
18.1095 + ("fill-d_d-arg", tm, thm, subs_opt) :: _ => if UnparseC.term tm =
18.1096 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
18.1097 + then () else error "find_fill_patterns changed 1a"
18.1098 +| _ => error "find_fill_patterns changed 1b"
18.1099 +
18.1100 +"~~~~~ fun fill_from_store, args:"; val (subst, form, errpatID, thm) =
18.1101 + (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
18.1102 + val thmDeriv = Thm.get_name_hint thm
18.1103 + val (part, thyID) = thy_containing_thm thmDeriv
18.1104 + val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
18.1105 + val Hthm {fillpats, ...} = get_the theID
18.1106 + val some = map (Error_Pattern.fill_form subst (thm, form) errpatID) fillpats;
18.1107 +
18.1108 +case some |> filter is_some |> map the of
18.1109 + ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term tm =
18.1110 + "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
18.1111 + then () else error "find_fill_patterns changed 2a"
18.1112 +| _ => error "find_fill_patterns changed 2b"
18.1113 +
18.1114 +"~~~~~ fun fill_form, args:";
18.1115 + val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
18.1116 + (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
18.1117 +val (form', _, _, rewritten) =
18.1118 + rew_sub (Isac()) 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
18.1119 +
18.1120 +if UnparseC.term form' = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
18.1121 +else error "find_fill_patterns changed 3";
18.1122 +
18.1123 +"~~~~~ to findFillpatterns return val:"; val (fillpats) =
18.1124 + (map (Error_Pattern.fill_from_store (subs_opt, subst) f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
18.1125 +
18.1126 +"vvv--- dropped this code WN120730";
18.1127 +val msg = "fill patterns " ^
18.1128 + ((map ((apsnd UnparseC.term) o quad2pair) fillpats) |> map pair2str_ |> strs2str_);
18.1129 +msg =
18.1130 + "fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
18.1131 + " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" ^
18.1132 + "#fill-both-args#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
18.1133 + " =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3" ^
18.1134 + "#fill-d_d#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
18.1135 + " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1 x (x ^^^ 4)" ^
18.1136 + "#fill-inner-deriv#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
18.1137 + " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1" ^
18.1138 + "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#";
18.1139 +"^^^--- dropped this code WN120730";
18.1140 +
18.1141 +if (map #1 fillpats) =
18.1142 + ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"]
18.1143 +then () else error "find_fill_patterns changed 4b";
18.1144 +DEconstrCalcTree 1;
18.1145 +
18.1146 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
18.1147 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
18.1148 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
18.1149 +reset_states ();
18.1150 +CalcTree
18.1151 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
18.1152 + ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
18.1153 +Iterator 1;
18.1154 +moveActiveRoot 1;
18.1155 +autoCalculate 1 CompleteCalcHead;
18.1156 +autoCalculate 1 (Steps 1);
18.1157 +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
18.1158 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*)
18.1159 +(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
18.1160 + would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
18.1161 + results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
18.1162 + instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
18.1163 + val ((pt,pos), _) = get_calc 1;
18.1164 + val p = get_pos 1 1;
18.1165 + val (Form f, _, asms) = pt_extract (pt, p);
18.1166 +
18.1167 + if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
18.1168 + case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
18.1169 + ("diff_sum", thm)) =>
18.1170 + if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
18.1171 + else error "embed fun fill_form changed 11"
18.1172 + | _ => error "embed fun fill_form changed 12"
18.1173 + else error "embed fun fill_form changed 13";
18.1174 +
18.1175 +findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
18.1176 +(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
18.1177 + d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
18.1178 + val ((pt,pos),_) = get_calc 1;
18.1179 + val p = get_pos 1 1;
18.1180 +
18.1181 + val (Form f, _, asms) = pt_extract (pt, p);
18.1182 + if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
18.1183 + case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
18.1184 + ("diff_sum", thm)) =>
18.1185 + if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
18.1186 + else error "embed fun fill_form changed 21"
18.1187 + | _ => error "embed fun fill_form changed 22"
18.1188 + else error "embed fun fill_form changed 23";
18.1189 +
18.1190 +requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
18.1191 + (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
18.1192 + val ((pt,pos),_) = get_calc 1;
18.1193 + val p = get_pos 1 1;
18.1194 + val (Form f, _, asms) = pt_extract (pt, p);
18.1195 + if p = ([1], Res) andalso existpt [2] pt
18.1196 + andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
18.1197 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
18.1198 + ("diff_sum", thm)) =>
18.1199 + if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
18.1200 + else error "embed fun fill_form changed 31"
18.1201 + | _ => error "embed fun fill_form changed 32"
18.1202 + else error "embed fun fill_form changed 33";
18.1203 +
18.1204 +(* input a formula which exactly fills the gaps in a "fillformula"
18.1205 + presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
18.1206 + errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.
18.1207 + the respective thm is in the ctree ................
18.1208 +*)
18.1209 +"~~~~~ fun inputFillFormula, args:"; val (cI, ifo) =
18.1210 + (1, "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)");
18.1211 + val ((pt, _), _) = get_calc cI
18.1212 + val pos = get_pos cI 1;
18.1213 +
18.1214 +"~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo);
18.1215 + val SOME ifo = parseNEW (ThyC.get_theory "Isac_Knowledge" |> ThyC.to_ctxt) istr
18.1216 + val p' = lev_on p;
18.1217 + val tac = get_obj g_tac pt p';
18.1218 +val Rewrite_Inst ([bbb as "(''bdv'', x)"], ("diff_sin_chain", ttt)) = tac;
18.1219 +if (UnparseC.term o Thm.prop_of) ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
18.1220 +else error "inputFillFormula changed 10";
18.1221 + val Appl rew = applicable_in pos pt tac;
18.1222 + val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
18.1223 +
18.1224 +"~~~~~ to inputFillFormula return val:"; val ("ok", tac) = ("ok", tac);
18.1225 + val ("ok", (_, c, ptp as (_,p'))) = Step.by_tactic tac (pt, pos);
18.1226 + upd_calc cI (ptp, []);
18.1227 + upd_ipos cI 1 p';
18.1228 + autocalculateOK2xml cI pos (if null c then p' else last_elem c) p';
18.1229 +
18.1230 +"~~~~~ final check:";
18.1231 +val ((pt, _),_) = get_calc 1;
18.1232 +val p = get_pos 1 1;
18.1233 +val (Form f, _, asms) = pt_extract (pt, p);
18.1234 + if p = ([2], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)"
18.1235 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
18.1236 + ("diff_sin_chain", thm)) =>
18.1237 + if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
18.1238 + else error "inputFillFormula changed 111"
18.1239 + | _ => error "inputFillFormula changed 112"
18.1240 + else error "inputFillFormula changed 113";
18.1241 +
18.1242 +"--------- fun appl_adds -----------------------------------------";
18.1243 +"--------- fun appl_adds -----------------------------------------";
18.1244 +"--------- fun appl_adds -----------------------------------------";
18.1245 +(* val (dI, oris, ppc, pbt, selct::ss) =
18.1246 + (dI, pors, probl, ppc, map itms2fstr probl);
18.1247 + ...vvv
18.1248 + *)
18.1249 +(* val (dI, oris, ppc, pbt, (selct::ss))=
18.1250 + (#1 (some_spec ospec spec), oris, []:itm list,
18.1251 + ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
18.1252 + val iii = appl_adds dI oris ppc pbt (selct::ss);
18.1253 + tracing(itms2str_ thy iii);
18.1254 +
18.1255 + val itm = appl_add' dI oris ppc pbt selct;
18.1256 + val ppc = insert_ppc' itm ppc;
18.1257 +
18.1258 + val _::selct::ss = (selct::ss);
18.1259 + val itm = appl_add' dI oris ppc pbt selct;
18.1260 + val ppc = insert_ppc' itm ppc;
18.1261 +
18.1262 + val _::selct::ss = (selct::ss);
18.1263 + val itm = appl_add' dI oris ppc pbt selct;
18.1264 + val ppc = insert_ppc' itm ppc;
18.1265 + tracing(itms2str_ thy ppc);
18.1266 +
18.1267 + val _::selct::ss = (selct::ss);
18.1268 + val itm = appl_add' dI oris ppc pbt selct;
18.1269 + val ppc = insert_ppc' itm ppc;
18.1270 + *)
18.1271 +"--------- fun concat_deriv --------------------------------------";
18.1272 +"--------- fun concat_deriv --------------------------------------";
18.1273 +"--------- fun concat_deriv --------------------------------------";
18.1274 +(*
18.1275 + val ({rew_ord, erls, rules,...}, fo, ifo) =
18.1276 + (Rule_Set.rep Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
18.1277 + (tracing o Derive.trtas2str) fod';
18.1278 +> ["
18.1279 +(x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))","
18.1280 +(-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))","
18.1281 +(-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))","
18.1282 +(1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
18.1283 +val it = () : unit
18.1284 + (tracing o Derive.trtas2str) (map Derive.rev_deriv' rifod');
18.1285 +> ["
18.1286 +(1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))","
18.1287 +(1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))","
18.1288 +(-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"]
18.1289 +val it = () : unit
18.1290 +*)
18.1291 +"--------- handle an input formula -------------------------------";
18.1292 +"--------- handle an input formula -------------------------------";
18.1293 +"--------- handle an input formula -------------------------------";
18.1294 +(*
18.1295 +Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler:
18.1296 +Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden,
18.1297 +wenn Abteilungen nur auf gleichem Level gesucht werden ?
18.1298 +WN.040216
18.1299 +
18.1300 +Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml
18.1301 +
18.1302 +------------------------------------------------------------------------------
18.1303 +"Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
18.1304 +------------------------------------------------------------------------------
18.1305 +1. "5 * x / (x - 2) - x / (x + 2) = 4"
18.1306 +...
18.1307 +4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalise", "poly"..
18.1308 +...
18.1309 +4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate"..
18.1310 +...
18.1311 +4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions"
18.1312 +...
18.1313 +"[x = -4 / 3]"
18.1314 +------------------------------------------------------------------------------
18.1315 +(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
18.1316 +
18.1317 +(4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
18.1318 +------------------------------------------------------------------------------
18.1319 +
18.1320 +
18.1321 +------------------------------------------------------------------------------
18.1322 +"Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
18.1323 +------------------------------------------------------------------------------
18.1324 +1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x"
18.1325 +...
18.1326 +4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))"
18.1327 + Subproblem["normalise", "polynomial", "univariate"..
18.1328 +...
18.1329 +4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..
18.1330 +...
18.1331 +4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
18.1332 +4.4.5. "[x = 0, x = 6 / 5]"
18.1333 +...
18.1334 +5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
18.1335 + "[x = 6 / 5]"
18.1336 +------------------------------------------------------------------------------
18.1337 +(1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x]
18.1338 +
18.1339 +(4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.]
18.1340 +------------------------------------------------------------------------------
18.1341 +
18.1342 +
18.1343 +------------------------------------------------------------------------------
18.1344 +"Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
18.1345 +------------------------------------------------------------------------------
18.1346 +1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)"
18.1347 +...
18.1348 +6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
18.1349 + Subproblem["sq", "rootX", "univariate", "equation"]
18.1350 +...
18.1351 +6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
18.1352 + Subproblem["normalise", "polynomial", "univariate", "equation"]
18.1353 +...
18.1354 +6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"]
18.1355 +... Or_to_List
18.1356 +6.6.3.2 "UniversalList"
18.1357 +------------------------------------------------------------------------------
18.1358 +(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n]
18.1359 +
18.1360 +(6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n]
18.1361 +------------------------------------------------------------------------------
18.1362 +*)
18.1363 +(*sh. comments auf 498*)
18.1364 +"--------- fun dropwhile' ----------------------------------------";
18.1365 +"--------- fun dropwhile' ----------------------------------------";
18.1366 +"--------- fun dropwhile' ----------------------------------------";
18.1367 +(*
18.1368 + fun equal a b = a=b;
18.1369 + val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5];
18.1370 + val r_foder = rev foder; val r_ifoder = rev ifoder;
18.1371 + dropwhile' equal r_foder r_ifoder;
18.1372 +> vval it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list
18.1373 +
18.1374 + val foder = [3,4,5]; val ifoder = [11,12,3,4,5];
18.1375 + val r_foder = rev foder; val r_ifoder = rev ifoder;
18.1376 + dropwhile' equal r_foder r_ifoder;
18.1377 +> val it = ([3], [3, 12, 11]) : int list * int list
18.1378 +
18.1379 + val foder = [5]; val ifoder = [11,12,3,4,5];
18.1380 + val r_foder = rev foder; val r_ifoder = rev ifoder;
18.1381 + dropwhile' equal r_foder r_ifoder;
18.1382 +> val it = ([5], [5, 4, 3, 12, 11]) : int list * int list
18.1383 +
18.1384 + val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5];
18.1385 + val r_foder = rev foder; val r_ifoder = rev ifoder;
18.1386 + dropwhile' equal r_foder r_ifoder;
18.1387 +> *** dropwhile': did not start with equal elements*)
19.1 --- a/test/Tools/isac/Specify/generate.sml Thu Apr 23 15:48:31 2020 +0200
19.2 +++ b/test/Tools/isac/Specify/generate.sml Fri Apr 24 08:51:05 2020 +0200
19.3 @@ -37,7 +37,7 @@
19.4 (1, ("chain-rule-diff-both", "fill-both-args"));
19.5 val ((pt, _), _) = get_calc cI
19.6 val pos as (p, _) = get_pos cI 1;
19.7 - val fillforms = find_fillpatterns (pt, pos) errpatID;
19.8 + val fillforms = Error_Pattern.find_fill_patterns (pt, pos) errpatID;
19.9
19.10 if pos = ([1], Res) then () else error "generate_inconsistent_rew changed 1";
19.11
20.1 --- a/test/Tools/isac/Test_Isac.thy Thu Apr 23 15:48:31 2020 +0200
20.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Apr 24 08:51:05 2020 +0200
20.3 @@ -97,8 +97,8 @@
20.4 open Env;
20.5 open LI; scan_dn;
20.6 open Istate;
20.7 - open Error_Fill_Pattern;
20.8 - open Error_Fill_Def;
20.9 + open Error_Pattern;
20.10 + open Error_Pattern_Def;
20.11 open In_Chead;
20.12 open Rtools; .trtas2str;
20.13 open Chead; pt_extract;
20.14 @@ -249,7 +249,7 @@
20.15 ML_file "Interpret/istate.sml"
20.16 ML_file "Interpret/sub-problem.sml"
20.17 ML_file "Interpret/rewtools.sml"
20.18 - ML_file "Interpret/error-fill-pattern.sml"
20.19 + ML_file "Interpret/error-pattern.sml"
20.20 ML_file "Interpret/li-tool.sml"
20.21 ML_file "Interpret/lucas-interpreter.sml"
20.22 ML_file "Interpret/step-solve.sml"
21.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Apr 23 15:48:31 2020 +0200
21.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Fri Apr 24 08:51:05 2020 +0200
21.3 @@ -97,8 +97,8 @@
21.4 open Env;
21.5 open LI; scan_dn;
21.6 open Istate;
21.7 - open Error_Fill_Pattern;
21.8 - open Error_Fill_Def;
21.9 + open Error_Pattern;
21.10 + open Error_Pattern_Def;
21.11 open In_Chead;
21.12 open Rtools;
21.13 open Chead; pt_extract;
21.14 @@ -249,7 +249,7 @@
21.15 ML_file "Interpret/istate.sml"
21.16 ML_file "Interpret/sub-problem.sml"
21.17 ML_file "Interpret/rewtools.sml"
21.18 - ML_file "Interpret/error-fill-pattern.sml"
21.19 + ML_file "Interpret/error-pattern.sml"
21.20 ML_file "Interpret/li-tool.sml"
21.21 ML_file "Interpret/lucas-interpreter.sml"
21.22 ML_file "Interpret/step-solve.sml"
22.1 --- a/test/Tools/isac/Test_Some.thy Thu Apr 23 15:48:31 2020 +0200
22.2 +++ b/test/Tools/isac/Test_Some.thy Fri Apr 24 08:51:05 2020 +0200
22.3 @@ -17,8 +17,8 @@
22.4 open Env;
22.5 open LI; scan_dn;
22.6 open Istate;
22.7 - open Error_Fill_Pattern;
22.8 - open Error_Fill_Def;
22.9 + open Error_Pattern;
22.10 + open Error_Pattern_Def;
22.11 open In_Chead;
22.12 open Rtools; .trtas2str;
22.13 open Chead; pt_extract;