1.1 --- a/src/Tools/isac/Build_Isac.thy Tue Jun 25 16:21:18 2019 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Jul 03 15:09:16 2019 +0200
1.3 @@ -14,6 +14,7 @@
1.4 (* structure inherited from migration which began with Isabelle2009. improve?
1.5 theory KEStore
1.6 ML_file "~~/src/Tools/isac/library.sml"
1.7 + ML_file "~~/src/Tools/isac/ThydataC/rule.sml"
1.8 ML_file "~~/src/Tools/isac/calcelems.sml"
1.9 theory ListC
1.10 imports "~~/src/Tools/isac/KEStore"
1.11 @@ -81,7 +82,7 @@
1.12 ML \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close>
1.13 ML \<open>print_exn_unit\<close>
1.14 ML \<open>list_rls (*from Atools.thy WN130615??? or ProgLang???*)\<close>
1.15 -
1.16 +
1.17 ML \<open>eval_occurs_in (*from Atools.thy*)\<close>
1.18 ML \<open>@{thm last_thmI} (*from Atools.thy*)\<close>
1.19 ML \<open>@{thm Querkraft_Belastung}\<close>
2.1 --- a/src/Tools/isac/Frontend/interface.sml Tue Jun 25 16:21:18 2019 +0200
2.2 +++ b/src/Tools/isac/Frontend/interface.sml Wed Jul 03 15:09:16 2019 +0200
2.3 @@ -443,7 +443,7 @@
2.4 in
2.5 case Math_Engine.step pos cs of
2.6 ("ok", cs') =>
2.7 - (case LucinNEW.locate_input_formula cs' (encode ifo) of
2.8 + (case Solve.inform cs' (encode ifo) of
2.9 ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) =>
2.10 (upd_calc cI (ptp, []); upd_ipos cI 1 p;
2.11 appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
2.12 @@ -463,7 +463,7 @@
2.13 val ((pt, _), _) = get_calc cI
2.14 val p = get_pos cI 1
2.15 in
2.16 - case LucinNEW.locate_input_formula (([], [], (pt, p)): Chead.calcstate') (encode ifo) of
2.17 + case Solve.inform (([], [], (pt, p)): Chead.calcstate')(encode ifo) of
2.18 ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) =>
2.19 let
2.20 val unc = if null (fst p) then p else move_up [] pt p
3.1 --- a/src/Tools/isac/Interpret/calchead.sml Tue Jun 25 16:21:18 2019 +0200
3.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed Jul 03 15:09:16 2019 +0200
3.3 @@ -1041,7 +1041,7 @@
3.4 (for ev. finding several more tacs due to hide) *)
3.5 (* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *)
3.6 (* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *)
3.7 -(* WN.24.10.03 fun nxt_solv = ...................................?? *)
3.8 +(* WN.24.10.03 fun begin_end_prog = ...................................?? *)
3.9 fun nxt_specif (tac as Tac.Model_Problem) (pt, pos as (p, _)) =
3.10 let
3.11 val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
4.1 --- a/src/Tools/isac/Interpret/ctree-basic.sml Tue Jun 25 16:21:18 2019 +0200
4.2 +++ b/src/Tools/isac/Interpret/ctree-basic.sml Wed Jul 03 15:09:16 2019 +0200
4.3 @@ -193,7 +193,7 @@
4.4 exceptions: Begin/End_Trans
4.5 # thus generate(1) called in
4.6 .# assy, locate_input_tactic
4.7 -.# nxt_solv (tac_ -cases); general case:
4.8 +.# begin_end_prog (tac_ -cases); general case:
4.9 val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
4.10 # WN050220, S(604):
4.11 generate1...(Rewrite(f,..,res))..(pos, pos_)
5.1 --- a/src/Tools/isac/Interpret/ctree-navi.sml Tue Jun 25 16:21:18 2019 +0200
5.2 +++ b/src/Tools/isac/Interpret/ctree-navi.sml Wed Jul 03 15:09:16 2019 +0200
5.3 @@ -13,6 +13,7 @@
5.4 val lev_dn_ : CTbasic.pos' -> CTbasic.pos'
5.5 val lev_up : CTbasic.pos -> CTbasic.pos
5.6 val lev_back' : CTbasic.pos' -> CTbasic.pos' (* for inform.sml *)
5.7 + val lev_back : CTbasic.pos' -> CTbasic.pos' (* for inform.sml *)
5.8
5.9 val lev_dn : CTbasic.pos -> CTbasic.pos (* duplicate in ctree-basic.sml *)
5.10 val lev_on : CTbasic.pos -> CTbasic.pos (* duplicate in ctree-basic.sml *)
5.11 @@ -49,11 +50,15 @@
5.12 fun lev_up [] = raise PTREE "lev_up []"
5.13 | lev_up p = (drop_last p):pos;
5.14
5.15 -(*040216: for locate_input_formula --> embed_deriv: remains on same level TODO.WN120517 compare lev_pred*)
5.16 +(*040216: for inform --> embed_deriv: remains on same level TODO.WN120517 compare lev_pred*)
5.17 fun lev_back' ([], _) = raise PTREE "lev_back': called by ([],_)"
5.18 | lev_back' (p, _) =
5.19 if last_elem p <= 1 then (p, Frm)
5.20 else ((drop_last p) @ [(nth (length p) p) - 1], Res);
5.21 +fun lev_back ([], p_) = ([], p_)
5.22 + | lev_back (p, _) =
5.23 + if last_elem p <= 1 then (p, Frm)
5.24 + else ((drop_last p) @ [(nth (length p) p) - 1], Res);
5.25 (* increase pos by n within a level *)
5.26 fun pos_plus 0 pos = pos
5.27 | pos_plus n (p, Frm) = pos_plus (n - 1) (p, Res)
6.1 --- a/src/Tools/isac/Interpret/generate.sml Tue Jun 25 16:21:18 2019 +0200
6.2 +++ b/src/Tools/isac/Interpret/generate.sml Wed Jul 03 15:09:16 2019 +0200
6.3 @@ -387,7 +387,7 @@
6.4 | _ => error ("generate_hard: call by " ^ pos'2str (p,p_))
6.5 in generate1 thy m' (Selem.e_istate, Selem.e_ctxt) (p,p_) pt end
6.6
6.7 -(* tacis are in reverse order from nxt_solve_/specify_: last = fst to insert *)
6.8 +(* tacis are in reverse order from do_solve_step/specify_: last = fst to insert *)
6.9 fun generate ([]: taci list) ptp = ptp
6.10 | generate tacis (pt, c, _: pos'(*!dropped!WN0504redesign generate/tacis?*))=
6.11 let
7.1 --- a/src/Tools/isac/Interpret/inform.sml Tue Jun 25 16:21:18 2019 +0200
7.2 +++ b/src/Tools/isac/Interpret/inform.sml Wed Jul 03 15:09:16 2019 +0200
7.3 @@ -438,7 +438,7 @@
7.4 | _ => error "find_fillpatterns: uncovered case of get_met"
7.5 val env = case Ctree.get_istate pt pos of
7.6 Selem.ScrState (env, _, _, _, _, _) => env
7.7 - | _ => error "locate_input_formula: uncovered case of get_istate"
7.8 + | _ => error "find_fillpatterns: uncovered case of get_istate"
7.9 val subst = Rtools.get_bdv_subst prog env
7.10 val errpatthms = errpats
7.11 |> filter ((curry op = errpatID) o (#1: Rule.errpat -> Rule.errpatID))
8.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Jun 25 16:21:18 2019 +0200
8.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Jul 03 15:09:16 2019 +0200
8.3 @@ -1,4 +1,4 @@
8.4 -(* Title: Interpret/lucase-interpreter.sml
8.5 +(* Title: Interpret/lucas-interpreter.sml
8.6 Author: Walther Neuper 2019
8.7 (c) due to copyright terms
8.8 *)
8.9 @@ -12,10 +12,14 @@
8.10 val locate_input_tactic : Rule.theory' * Rule.rls -> Tac.tac_ -> Ctree.state -> Rule.scr * 'a ->
8.11 Selem.istate * Proof.context -> locate
8.12
8.13 - val locate_input_formula : Chead.calcstate' -> string -> string (*..drop*)* Chead.calcstate'
8.14 - val nxt_solv : Tac.tac_ -> Selem.istate * Proof.context -> Ctree.state ->
8.15 + datatype input_formula_result =
8.16 + Step of Ctree.state * Selem.istate * Proof.context
8.17 + | Not_Derivable of Chead.calcstate'
8.18 + val locate_input_formula : Rule.scr -> Ctree.state -> Selem.istate -> Proof.context -> term
8.19 + -> input_formula_result
8.20 + val begin_end_prog : Tac.tac_ -> Selem.istate * Proof.context -> Ctree.state ->
8.21 (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state
8.22 - val nxt_solve_ : Ctree.state ->
8.23 + val do_solve_step : Ctree.state ->
8.24 (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state
8.25
8.26 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.27 @@ -49,7 +53,8 @@
8.28 | go (Celem.R :: p) (_ $ t2) = go p t2
8.29 | go l _ = error ("go: no " ^ Celem.loc_2str l);
8.30
8.31 -(** find the next tactic by executing the program **)
8.32 +
8.33 +(**** find the next tactic by executing the program ****)
8.34
8.35 (*appy, nxt_up, nstep_up scanning for determine_next_tactic.
8.36 search is clearly separated into (1)-(2):
8.37 @@ -266,7 +271,8 @@
8.38 | determine_next_tactic _ _ _ (is, _) =
8.39 error ("determine_next_tactic: not impl for " ^ (Selem.istate2str is));
8.40
8.41 -(** locate an input tactic in the program **)
8.42 +
8.43 +(**** locate an input tactic in the program ****)
8.44
8.45 datatype assoc = (* ExprVal in the sense of denotational semantics *)
8.46 Assoc of (* the stac is associated, strongly or weakly *)
8.47 @@ -546,19 +552,35 @@
8.48 error ("locate_input_tactic: wrong arguments,\n tac= " ^ Tac.tac_2str m ^ ",\n " ^
8.49 "scr= " ^ Rule.scr2str sc ^ ",\n istate= " ^ Selem.istate2str is);
8.50
8.51 -(** locate an input formula in the program **)
8.52
8.53 -(* FIXME.WN050821 compare fun solve ... fun nxt_solv
8.54 - nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *)
8.55 -fun nxt_solv (Tac.Apply_Method' (mI, _, _, _)) _ (pt, pos as (p, _)) =
8.56 - let
8.57 - val {ppc, ...} = Specify.get_met mI;
8.58 - val (itms, oris, probl) = case get_obj I pt p of
8.59 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
8.60 - | _ => error "nxt_solv Apply_Method': uncovered case get_obj"
8.61 - val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
8.62 - val thy' = get_obj g_domID pt p;
8.63 - val thy = Celem.assoc_thy thy';
8.64 +(**** locate an input formula in the program ****)
8.65 +(* in more detail: compare (modulo a specific rule-set) the input formula
8.66 + with formulas calculated by "fun determine_next_tactic".
8.67 + "determine_next_tactic" is iterated until the main program is executed to the end
8.68 + (which might entail executing sub-programs of sub-problems).
8.69 +
8.70 + This kind of stepwise iteration is captured in the SOLVE_PHASE,
8.71 + which provides different signatures. hus the specific "fun begin_end_prog" and
8.72 + "fun TODO"
8.73 + are pulled out from the SOLVE_PHASE and put here.
8.74 + And thus the third essential function of the Lucas-Interpreter has a signature
8.75 + different from the other two essential function.
8.76 +*)
8.77 +datatype input_formula_result =
8.78 + Step of Ctree.state * Selem.istate * Proof.context
8.79 + | Not_Derivable of Chead.calcstate'
8.80 +
8.81 +(* FIXME.WN050821 compare fun solve ... fun begin_end_prog
8.82 + begin_end_prog (Apply_Method' vvv FIXME: get args in applicable_in *)
8.83 +fun begin_end_prog (Tac.Apply_Method' (mI, _, _, _)) _ (pt, pos as (p, _)) =
8.84 + let
8.85 + val {ppc, ...} = Specify.get_met mI;
8.86 + val (itms, oris, probl) = case get_obj I pt p of
8.87 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
8.88 + | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"
8.89 + val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
8.90 + val thy' = get_obj g_domID pt p;
8.91 + val thy = Celem.assoc_thy thy';
8.92 (*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
8.93 val itms =
8.94 if mI = ["Biegelinien", "ausBelastung"]
8.95 @@ -574,8 +596,8 @@
8.96 else itms
8.97 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
8.98 val (is, env, ctxt, scr) = case Lucin.init_scrstate thy itms mI of
8.99 - (is as Selem.ScrState (env,_,_,_,_,_), ctxt, scr) => (is, env, ctxt, scr)
8.100 - | _ => error "nxt_solv Apply_Method': uncovered case init_scrstate"
8.101 + (is as Selem.ScrState (env,_,_,_,_,_), ctxt, scr) => (is, env, ctxt, scr)
8.102 + | _ => error "begin_end_prog Apply_Method': uncovered case init_scrstate"
8.103 val ini = Lucin.init_form thy scr env;
8.104 in
8.105 case ini of
8.106 @@ -590,12 +612,12 @@
8.107 | NONE =>
8.108 let
8.109 val pt = update_env pt (fst pos) (SOME (is, ctxt))
8.110 - val (tacis, c, ptp) = nxt_solve_ (pt, pos)
8.111 + val (tacis, c, ptp) = do_solve_step (pt, pos)
8.112 in (tacis @ [(Tac.Apply_Method mI, Tac.Apply_Method' (mI, NONE, Selem.e_istate, ctxt), (pos, (is, ctxt)))],
8.113 c, ptp)
8.114 end
8.115 end
8.116 - | nxt_solv (Tac.Check_Postcond' (pI, _)) _ (pt, (p, p_)) =
8.117 + | begin_end_prog (Tac.Check_Postcond' (pI, _)) _ (pt, (p, p_)) =
8.118 let
8.119 val pp = par_pblobj pt p
8.120 val asm = (case get_obj g_tac pt p of
8.121 @@ -606,7 +628,7 @@
8.122 val {srls = srls, scr = sc, ...} = Specify.get_met metID;
8.123 val (loc, E, l, a, b, ctxt) = case get_loc pt (p, p_) of
8.124 loc as (Selem.ScrState (E,l,a,_,_,b), ctxt) => (loc, E, l, a, b, ctxt)
8.125 - | _ => error "nxt_solv Check_Postcond': uncovered case get_loc"
8.126 + | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc"
8.127 val thy' = get_obj g_domID pt pp;
8.128 val thy = Celem.assoc_thy thy';
8.129 val (_, _, (scval, scsaf)) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;
8.130 @@ -625,15 +647,15 @@
8.131 val thy = Celem.assoc_thy thy';
8.132 val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of
8.133 (Selem.ScrState (E,l,a,_,_,b), ctxt') => (E, l, a, b, ctxt')
8.134 - | _ => error "nxt_solv Check_Postcond' script of parpbl: uncovered case get_loc"
8.135 + | _ => error "begin_end_prog Check_Postcond' script of parpbl: uncovered case get_loc"
8.136 val ctxt'' = Stool.from_subpbl_to_caller ctxt scval ctxt'
8.137 val tac_ = Tac.Check_Postcond' (pI, (scval, asm))
8.138 val is = Selem.ScrState (E,l,a,scval,scsaf,b)
8.139 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
8.140 in ([(Tac.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p, p_))) end
8.141 end
8.142 - | nxt_solv (Tac.End_Proof'') _ ptp = ([], [], ptp)
8.143 - | nxt_solv tac_ is (pt, pos) =
8.144 + | begin_end_prog (Tac.End_Proof'') _ ptp = ([], [], ptp)
8.145 + | begin_end_prog tac_ is (pt, pos) =
8.146 let
8.147 val pos = case pos of
8.148 (p, Met) => ((lev_on o lev_dn) p, Frm) (* begin script *)
8.149 @@ -643,8 +665,8 @@
8.150 in
8.151 ([(Lucin.tac_2tac tac_, tac_, (pos, is))], c, (pt, pos'))
8.152 end
8.153 -(* find the next tac from the script, nxt_solv will update the ctree *)
8.154 -and nxt_solve_ (ptp as (pt, pos as (p, p_))) =
8.155 +(* find the next tac from the script, begin_end_prog will update the ctree *)
8.156 +and do_solve_step (ptp as (pt, pos as (p, p_))) =
8.157 if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)
8.158 then ([], [], (pt, (p, p_)))
8.159 else
8.160 @@ -655,10 +677,10 @@
8.161 (* TODO here ^^^ return finished/helpless/ok !*)
8.162 in case tac_ of
8.163 Tac.End_Detail' _ => ([(Tac.End_Detail, Tac.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos))
8.164 - | _ => nxt_solv tac_ is ptp
8.165 + | _ => begin_end_prog tac_ is ptp
8.166 end;
8.167
8.168 -(* compare locate_input_formula with ctree.form at current pos by nrls;
8.169 +(* compare inform with ctree.form at current pos by nrls;
8.170 if found, embed the derivation generated during comparison
8.171 if not, let the mat-engine compute the next ctree.form *)
8.172 (* code's structure is copied from complete_solve
8.173 @@ -686,14 +708,14 @@
8.174 then ("no derivation found", (tacis, c, ptp): Chead.calcstate')
8.175 else
8.176 let
8.177 - val cs' as (tacis, c', ptp) = nxt_solve_ ptp; (*<---------------------*)
8.178 + val cs' as (tacis, c', ptp) = do_solve_step ptp; (*<---------------------*)
8.179 val (tacis, c'', ptp) = case tacis of
8.180 ((Tac.Subproblem _, _, _)::_) =>
8.181 let
8.182 val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)
8.183 val mI = Ctree.get_obj Ctree.g_metID pt p
8.184 in
8.185 - nxt_solv (Tac.Apply_Method' (mI, NONE, Selem.e_istate, Selem.e_ctxt)) (Selem.e_istate, Selem.e_ctxt) ptp
8.186 + begin_end_prog (Tac.Apply_Method' (mI, NONE, Selem.e_istate, Selem.e_ctxt)) (Selem.e_istate, Selem.e_ctxt) ptp
8.187 end
8.188 | _ => cs';
8.189 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
8.190 @@ -708,43 +730,18 @@
8.191 collect all the tacs applied by the way;
8.192 if "no derivation found" then check_error_patterns.
8.193 ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*)
8.194 -fun locate_input_formula (cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =
8.195 - case TermC.parse (Celem.assoc_thy "Isac") istr of
8.196 - SOME f_in =>
8.197 - let
8.198 - val f_in = Thm.term_of f_in
8.199 - val f_succ = Ctree.get_curr_formula (pt, pos);
8.200 - in
8.201 - if f_succ = f_in
8.202 - then ("same-formula", cs) (* ctree not cut with replaceFormula *)
8.203 - else
8.204 - case Inform.cas_input f_in of
8.205 - SOME (pt, _) => ("ok",([], [], (pt, (p, Ctree.Met))))
8.206 - | NONE =>
8.207 - let
8.208 - val pos_pred = Ctree.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
8.209 - val f_pred = Ctree.get_curr_formula (pt, pos_pred)
8.210 - val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*)
8.211 - (*last step re-calc in compare_step TODO before WN09*)
8.212 - in
8.213 - case msg_calcstate' of
8.214 - ("no derivation found", calcstate') =>
8.215 - let
8.216 - val pp = Ctree.par_pblobj pt p
8.217 - val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
8.218 - {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
8.219 - | _ => error "locate_input_formula: uncovered case of get_met"
8.220 - val env = case Ctree.get_istate pt pos of
8.221 - Selem.ScrState (env, _, _, _, _, _) => env
8.222 - | _ => error "locate_input_formula: uncovered case of get_istate"
8.223 - in
8.224 - case Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
8.225 - SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
8.226 - | NONE => msg_calcstate'
8.227 - end
8.228 - | _ => msg_calcstate'
8.229 - end
8.230 - end
8.231 - | NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate')
8.232 +(* vvvv vvvvvv vvvv NEW args for compare_step *)
8.233 +fun locate_input_formula (Rule.Prog prog) ((pt, pos) : Ctree.state) (istate : Selem.istate) (ctxt : Proof.context) tm =
8.234 + let
8.235 + val pos_pred = Ctree.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
8.236 + val f_pred = Ctree.get_curr_formula (pt, pos_pred)
8.237 + in
8.238 + (*TODO: use prog, istate, ctxt in compare_step ...*)
8.239 + case compare_step ([], [], (pt, pos_pred)) tm of
8.240 + ("no derivation found", calcstate') => Not_Derivable calcstate'
8.241 + | ("ok", (_, _, cstate as (pt', pos'))) =>
8.242 + Step (cstate, get_istate pt' pos', get_ctxt pt' pos')
8.243 + | _ => raise ERROR "compare_step: uncovered case"
8.244 + end
8.245
8.246 end
9.1 --- a/src/Tools/isac/Interpret/mathengine.sml Tue Jun 25 16:21:18 2019 +0200
9.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed Jul 03 15:09:16 2019 +0200
9.3 @@ -132,7 +132,7 @@
9.4 in
9.5 case tac of
9.6 Tac.Apply_Method mI =>
9.7 - LucinNEW.nxt_solv (Tac.Apply_Method' (mI, NONE, Selem.e_istate, Selem.e_ctxt)) (Selem.e_istate, Selem.e_ctxt) ptp
9.8 + LucinNEW.begin_end_prog (Tac.Apply_Method' (mI, NONE, Selem.e_istate, Selem.e_ctxt)) (Selem.e_istate, Selem.e_ctxt) ptp
9.9 | _ => Chead.nxt_specif tac ptp
9.10 end
9.11 end
9.12 @@ -201,7 +201,7 @@
9.13 let val (pt',c',p') = Generate.generate tacis (pt,[],p)
9.14 in ("ok", (tacis, c', (pt', p'))) end
9.15 else (case (if member op = [Ctree.Pbl, Ctree.Met] p_
9.16 - then nxt_specify_ (pt, ip) else LucinNEW.nxt_solve_ (pt, ip))
9.17 + then nxt_specify_ (pt, ip) else LucinNEW.do_solve_step (pt, ip))
9.18 handle ERROR msg => (writeln ("*** " ^ msg);
9.19 ([], [], ptp)) (*e.g. Add_Given "equality///"*) of
9.20 cs as ([],_,_) => ("helpless", cs)
9.21 @@ -212,7 +212,7 @@
9.22 (case if member op = [Ctree.Pbl, Ctree.Met] p_
9.23 andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p))
9.24 then nxt_specify_ (pt, ip)
9.25 - else (LucinNEW.nxt_solve_ (pt,ip))
9.26 + else (LucinNEW.do_solve_step (pt,ip))
9.27 handle ERROR msg => (writeln ("*** " ^ msg);
9.28 ([],[],ptp)) (*e.g. Add_Given "equality///"*) of
9.29 cs as ([],_,_) =>("helpless", cs) (*FIXXME del.handle*)
10.1 --- a/src/Tools/isac/Interpret/script.sml Tue Jun 25 16:21:18 2019 +0200
10.2 +++ b/src/Tools/isac/Interpret/script.sml Wed Jul 03 15:09:16 2019 +0200
10.3 @@ -638,7 +638,7 @@
10.4 val metID = get_obj g_metID pt p'
10.5 val {srls,...} = Specify.get_met metID
10.6 in (srls, get_loc pt (p,p_), (#scr o Specify.get_met) metID) end
10.7 - else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_input_formula, determine_next_tactic*) (* 3 *)
10.8 + else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in inform, determine_next_tactic*) (* 3 *)
10.9 (Rule.e_rls, get_loc pt (p,p_),
10.10 case rls' of
10.11 Rule.Rls {scr = scr,...} => scr
11.1 --- a/src/Tools/isac/Interpret/solve.sml Tue Jun 25 16:21:18 2019 +0200
11.2 +++ b/src/Tools/isac/Interpret/solve.sml Wed Jul 03 15:09:16 2019 +0200
11.3 @@ -3,7 +3,7 @@
11.4 (c) copyright due to lincense terms.
11.5 *)
11.6
11.7 -signature SOLVE =
11.8 +signature SOLVE_PHASE =
11.9 sig
11.10 datatype auto = CompleteCalc | CompleteCalcHead | CompleteModel | CompleteSubpbl
11.11 | CompleteToSubpbl | Step of int
11.12 @@ -18,6 +18,8 @@
11.13 auto -> Ctree.pos' list -> Ctree.state -> string * Ctree.pos' list * Ctree.state
11.14 val solve : string * Tac.tac_ -> Ctree.state -> string * Chead.calcstate'
11.15
11.16 + val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
11.17 +
11.18 val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
11.19 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.20 val get_form : tac'_ -> Ctree.pos' -> Ctree.ctree -> Generate.mout
11.21 @@ -30,7 +32,7 @@
11.22 end
11.23
11.24 (**)
11.25 -structure Solve(**): SOLVE(**) =
11.26 +structure Solve(**): SOLVE_PHASE(**) =
11.27 struct
11.28 (**)
11.29 open Ctree;
11.30 @@ -110,7 +112,7 @@
11.31 fun step2taci ((tac_, _, pt, p, _) : Lucin.step) = (*FIXXME.040312: redesign step*)
11.32 (Lucin.tac_2tac tac_, tac_, (p, Ctree.get_loc pt p)): Generate.taci;
11.33
11.34 -(*FIXME.WN050821 compare solve ... nxt_solv*)
11.35 +(*FIXME.WN050821 compare solve ... begin_end_prog*)
11.36 fun solve ("Apply_Method", m as Tac.Apply_Method' (mI, _, _, _)) (pt, (pos as (p, _))) =
11.37 let val {srls, ...} = Specify.get_met mI;
11.38 val itms = case get_obj I pt p of
11.39 @@ -262,7 +264,7 @@
11.40 val (_, c', ptp) = all_solve auto c ptp
11.41 in complete_solve auto (c @ c') ptp end
11.42 else
11.43 - case LucinNEW.nxt_solve_ ptp of
11.44 + case LucinNEW.do_solve_step ptp of
11.45 ((Tac.Subproblem _, _, _) :: _, c', ptp') =>
11.46 if autoord auto < 5
11.47 then ("ok", c @ c', ptp)
11.48 @@ -284,7 +286,7 @@
11.49 let
11.50 val (_, _, mI) = get_obj g_spec pt p
11.51 val ctxt = get_ctxt pt pos
11.52 - val (_, c', ptp) = LucinNEW.nxt_solv (Tac.Apply_Method' (mI, NONE, Selem.e_istate, ctxt)) (Selem.e_istate, ctxt) ptp
11.53 + val (_, c', ptp) = LucinNEW.begin_end_prog (Tac.Apply_Method' (mI, NONE, Selem.e_istate, ctxt)) (Selem.e_istate, ctxt) ptp
11.54 in
11.55 complete_solve auto (c @ c') ptp
11.56 end;
11.57 @@ -334,5 +336,51 @@
11.58 let val (_, _, f, _, _, _) = Chead.specify m (p, p_) [] pt
11.59 in f end
11.60 else Generate.EmptyMout;
11.61 -
11.62 +
11.63 +fun inform (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =
11.64 + let
11.65 + val ctxt = get_ctxt pt pos (*see TODO.thy*)
11.66 + in
11.67 + case TermC.parse (Celem.assoc_thy "Isac") istr of
11.68 + NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate' (*TODO: previous cs'*))
11.69 + | SOME f_in =>
11.70 + let
11.71 + val f_in = Thm.term_of f_in
11.72 + val pos_pred = lev_back(*'*) pos
11.73 + val f_pred = Ctree.get_curr_formula (pt, pos_pred);
11.74 + val f_succ = Ctree.get_curr_formula (pt, pos);
11.75 + in
11.76 + if f_succ = f_in
11.77 + then ("same-formula", next_cs) (* ctree not cut with replaceFormula *)
11.78 + else
11.79 + case Inform.cas_input f_in of
11.80 + SOME (pt, _) => ("ok",([], [], (pt, (p, Ctree.Met))))
11.81 + | NONE => (*/-------------------------------------- NEW fun locate_input_formula------*)
11.82 + let
11.83 + (*NEW*)val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
11.84 + (*NEW*)val {scr = prog, ...} = Specify.get_met metID
11.85 + (*NEW*)val istate = get_istate pt pos
11.86 + (*NEW*)val ctxt = get_ctxt pt pos
11.87 + in
11.88 + case LucinNEW.locate_input_formula prog (pt, pos) istate ctxt f_in of
11.89 + LucinNEW.Step (cstate, _(*istate*), _(*ctxt*)) =>
11.90 + ("ok" , ([], [], cstate (* already contains istate, ctxt *)))
11.91 + | LucinNEW.Not_Derivable calcstate' =>
11.92 + let
11.93 + val pp = Ctree.par_pblobj pt p
11.94 + val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
11.95 + {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
11.96 + | _ => error "inform: uncovered case of get_met"
11.97 + val env = case Ctree.get_istate pt pos of
11.98 + Selem.ScrState (env, _, _, _, _, _) => env
11.99 + | _ => error "inform: uncovered case of get_istate"
11.100 + in
11.101 + case Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
11.102 + SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
11.103 + | NONE => ("no derivation found", calcstate')
11.104 + end
11.105 + end
11.106 + end
11.107 + end
11.108 +
11.109 end
11.110 \ No newline at end of file
12.1 --- a/src/Tools/isac/TODO.thy Tue Jun 25 16:21:18 2019 +0200
12.2 +++ b/src/Tools/isac/TODO.thy Wed Jul 03 15:09:16 2019 +0200
12.3 @@ -24,11 +24,22 @@
12.4 val pblterm: Rule.domID -> Celem.pblID -> term vvv vvv\\
12.5 val subpbl: string -> string list -> term unify with ^^^
12.6
12.7 -\item lucin: test/../partial_fractions: repair different behaviour of
12.8 - --- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ----
12.9 - --- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ----
12.10 -\item lucin: finish output of trace_script with Check_Postcond (useful for SubProblem)
12.11 -\item lucin: extract common code from assod .. stac2tac_
12.12 +\item Lucin
12.13 + \begin{itemize}
12.14 + \item language definition: use (f #> g) x = x |> f |> g instead of @
12.15 + see implementation.pdf p.16
12.16 + \item xxx
12.17 + \item xxx
12.18 + \item xxx
12.19 + \item rename type scr --> type program + rename field scr in meth
12.20 + \item inform:
12.21 + TermC.parse (Celem.assoc_thy "Isac") istr --> parseNEW context istr
12.22 + \item lucin: test/../partial_fractions: repair different behaviour of
12.23 + --- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ----
12.24 + --- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ----
12.25 + \item lucin: finish output of trace_script with Check_Postcond (useful for SubProblem)
12.26 + \item lucin: extract common code from assod .. stac2tac_
12.27 + \end{itemize}
12.28 \item prep_met: check match between args of partial_function and model-pattern of meth;
12.29 provide error message.
12.30 \item Diff.thy
13.1 --- a/src/Tools/isac/ThydataC/rule.sml Tue Jun 25 16:21:18 2019 +0200
13.2 +++ b/src/Tools/isac/ThydataC/rule.sml Wed Jul 03 15:09:16 2019 +0200
13.3 @@ -108,9 +108,12 @@
13.4
13.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
13.6 val terms2str': term list -> string (* shift up to Unparse *)
13.7 + val thm2str: thm -> string
13.8 + val thms2str : thm list -> string
13.9 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
13.10 val string_of_thm': theory -> thm -> string (* shift up to Unparse *)
13.11 val string_of_thm: thm -> string (* shift up to Unparse *)
13.12 + val errpats2str : errpat list -> string
13.13 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
13.14
13.15 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
13.16 @@ -175,7 +178,43 @@
13.17 fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro))
13.18 handle _ => error ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
13.19
13.20 +(* Since Isabelle2017 sessions in theory identifiers are enforced.
13.21 + However, we leave theory identifiers short, in particular in use as keys into KEStore. *)
13.22 +fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)
13.23 +fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*)
13.24 +fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
13.25 +fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*)
13.26
13.27 +fun term_to_string' ctxt t =
13.28 + let
13.29 + val ctxt' = Config.put show_markup false ctxt
13.30 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
13.31 +fun term_to_string'' thyID t =
13.32 + let
13.33 + val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
13.34 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
13.35 +fun term_to_string''' thy t =
13.36 + let
13.37 + val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
13.38 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
13.39 +
13.40 +fun term2str t = term_to_string' (thy2ctxt' "Isac") t;
13.41 +fun t2str thy t = term_to_string' (thy2ctxt thy) t;
13.42 +fun ts2str thy ts = ts |> map (t2str thy) |> strs2str';
13.43 +fun terms2strs ts = map term2str ts; (* terms2strs [t1,t2] = ["1 + 2", "abc"]; *)
13.44 +val terms2str = strs2str o terms2strs; (* terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]"; *)
13.45 +val terms2str' = strs2str' o terms2strs; (* terms2str' [t1,t2] = "[1 + 2,abc]"; *)
13.46 +fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
13.47 + | termopt2str NONE = "NONE";
13.48 +
13.49 +fun thm2str thm =
13.50 + let
13.51 + val t = Thm.prop_of thm
13.52 + val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac"))
13.53 + val ctxt' = Config.put show_markup false ctxt
13.54 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
13.55 +fun thms2str thms = (strs2str o (map thm2str)) thms
13.56 +
13.57 (* error patterns and fill patterns *)
13.58 type errpatID = string
13.59 type errpat =
13.60 @@ -185,6 +224,9 @@
13.61 * thm list (* thms related to error patterns; note that respective lhs
13.62 do not match (which reflects student's error).
13.63 fillpatterns are stored with these thms. *)
13.64 +fun errpat2str (id, tms, thms) =
13.65 + "(\"" ^ id ^ "\",\n" ^ terms2str tms ^ ",\n" ^ thms2str thms
13.66 +fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
13.67
13.68 datatype rule =
13.69 Erule (*.the empty rule .*)
13.70 @@ -304,35 +346,6 @@
13.71 | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
13.72 | eq_rule _ = false;
13.73
13.74 -(* Since Isabelle2017 sessions in theory identifiers are enforced.
13.75 - However, we leave theory identifiers short, in particular in use as keys into KEStore. *)
13.76 -fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)
13.77 -fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*)
13.78 -fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
13.79 -fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*)
13.80 -
13.81 -fun term_to_string' ctxt t =
13.82 - let
13.83 - val ctxt' = Config.put show_markup false ctxt
13.84 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
13.85 -fun term_to_string'' thyID t =
13.86 - let
13.87 - val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
13.88 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
13.89 -fun term_to_string''' thy t =
13.90 - let
13.91 - val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
13.92 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
13.93 -
13.94 -fun term2str t = term_to_string' (thy2ctxt' "Isac") t;
13.95 -fun t2str thy t = term_to_string' (thy2ctxt thy) t;
13.96 -fun ts2str thy ts = ts |> map (t2str thy) |> strs2str';
13.97 -fun terms2strs ts = map term2str ts; (* terms2strs [t1,t2] = ["1 + 2", "abc"]; *)
13.98 -val terms2str = strs2str o terms2strs; (* terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]"; *)
13.99 -val terms2str' = strs2str' o terms2strs; (* terms2str' [t1,t2] = "[1 + 2,abc]"; *)
13.100 -fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
13.101 - | termopt2str NONE = "NONE";
13.102 -
13.103 (*ad thm':
13.104 there are two kinds of theorems ...
13.105 (1) known by isabelle
14.1 --- a/src/Tools/isac/calcelems.sml Tue Jun 25 16:21:18 2019 +0200
14.2 +++ b/src/Tools/isac/calcelems.sml Wed Jul 03 15:09:16 2019 +0200
14.3 @@ -108,7 +108,6 @@
14.4 val thm''_of_thm: thm -> thm''
14.5 val thm_of_thm: Rule.rule -> thm
14.6 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
14.7 - val thm2str: thm -> string
14.8 val pats2str' : pat list -> string
14.9 val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list ->
14.10 thydata ptyp list
14.11 @@ -213,13 +212,6 @@
14.12 # ???
14.13 *)
14.14
14.15 -fun thm2str thm =
14.16 - let
14.17 - val t = Thm.prop_of thm
14.18 - val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac"))
14.19 - val ctxt' = Config.put show_markup false ctxt
14.20 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
14.21 -
14.22 fun id_of_thm (Rule.Thm (id, _)) = id (* TODO re-arrange code for rule2str *)
14.23 | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *))
14.24 fun thm_of_thm (Rule.Thm (_, thm)) = thm (* TODO re-arrange code for rule2str *)
15.1 --- a/test/Tools/isac/Interpret/inform.sml Tue Jun 25 16:21:18 2019 +0200
15.2 +++ b/test/Tools/isac/Interpret/inform.sml Wed Jul 03 15:09:16 2019 +0200
15.3 @@ -10,7 +10,6 @@
15.4 "--------- appendFormula: on Res + equ_nrls ----------------------";
15.5 "--------- appendFormula: on Frm + equ_nrls ----------------------";
15.6 "--------- appendFormula: on Res + NO deriv ----------------------";
15.7 -"--------- appendFormula: on Res + late deriv --------------------";
15.8 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
15.9 "replaceForm with miniscript with mini-subpbl:";
15.10 "--------- replaceFormula: on Res + = ----------------------------";
15.11 @@ -469,7 +468,7 @@
15.12 val (p,_,f,nxt,_,pt) =
15.13 CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
15.14 val ifo = "solve(x+1=2,x)";
15.15 -val (_,(_,c,(pt,p))) = locate_input_formula ([],[],(pt,p)) "solve(x+1=2,x)";
15.16 +val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "solve(x+1=2,x)";
15.17 show_pt pt;
15.18 val nxt = ("Apply_Method",Apply_Method ["Test","squ-equ-test-subpbl1"]);
15.19 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.20 @@ -492,9 +491,9 @@
15.21 else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
15.22 DEconstrCalcTree 1;
15.23
15.24 -"--------- locate_input_formula [rational,simplification] ----------------------";
15.25 -"--------- locate_input_formula [rational,simplification] ----------------------";
15.26 -"--------- locate_input_formula [rational,simplification] ----------------------";
15.27 +"--------- inform [rational,simplification] ----------------------";
15.28 +"--------- inform [rational,simplification] ----------------------";
15.29 +"--------- inform [rational,simplification] ----------------------";
15.30 reset_states ();
15.31 CalcTree [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"],
15.32 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
15.33 @@ -996,7 +995,7 @@
15.34 "--------- embed fun check_error_patterns ------------------------";
15.35 "--------- embed fun check_error_patterns ------------------------";
15.36 "--------- embed fun check_error_patterns ------------------------";
15.37 -reset_states ();
15.38 +reset_states ();
15.39 CalcTree
15.40 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
15.41 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
15.42 @@ -1007,112 +1006,51 @@
15.43 autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
15.44 (*autoCalculate 1 (Step 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
15.45
15.46 -"~~~~~ fun appendFormula, args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
15.47 -val cs = get_calc cI
15.48 -val pos as (_,p_) = get_pos cI 1; (*pos = ([1], Res)*)
15.49 -val cs' =
15.50 - case step pos cs of
15.51 - ("ok", cs') => cs';
15.52 +"~~~~~ fun appendFormula , args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
15.53 +"~~~~~ fun appendFormula' , args:"; val (cI, (ifo: Rule.cterm')) = (cI, ifo);
15.54 + val cs = get_calc cI
15.55 + val pos = get_pos cI 1;
15.56 +(*+*)if pos = ([1], Res) then () else error "inform with (positive) check_error_patterns broken 1";
15.57 + val ("ok", cs') = (*case*) step pos cs (*of*);
15.58 + (*case*) Solve.inform cs' (encode ifo) (*of*); (*ERROR WAS: "no derivation found"*)
15.59 +"~~~~~ fun inform , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Chead.calcstate'), istr)
15.60 + = (cs', (encode ifo));
15.61 + val ctxt = get_ctxt pt pos (*see TODO.thy*)
15.62 + val SOME f_in = (*case*) TermC.parse (Celem.assoc_thy "Isac") istr (*of*);
15.63 + val f_in = Thm.term_of f_in
15.64 + val pos_pred = lev_back' pos
15.65 + val f_pred = Ctree.get_curr_formula (pt, pos_pred);
15.66 + (*if*) f_pred = f_in; (*else*)
15.67 + val NONE = (*case*) Inform.cas_input f_in (*of*);
15.68 + (*NEW*)val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
15.69 + (*NEW*)val {scr = prog, ...} = Specify.get_met metID
15.70 + (*NEW*)val istate = get_istate pt pos
15.71 + (*NEW*)val ctxt = get_ctxt pt pos
15.72 + val LucinNEW.Not_Derivable calcstate' =
15.73 + (*case*) LucinNEW.locate_input_formula prog (pt, pos) istate ctxt f_in (*of*);
15.74 + val pp = Ctree.par_pblobj pt p
15.75 + val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
15.76 + {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
15.77 + | _ => error "inform: uncovered case of get_met"
15.78 +;
15.79 +(*+*)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\"]]"
15.80 +(*+*)then () else error "inform with (positive) check_error_patterns broken 3";
15.81
15.82 -val (_, _, (pt, ([2], Res))) = cs';
15.83 -(*show_pt pt;
15.84 - [(([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
15.85 - (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
15.86 - (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))), <<=== input follos: "...+ cos(4.x^3)"
15.87 - (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4))] *)
15.88 + val env = case Ctree.get_istate pt pos of
15.89 + Selem.ScrState (env, _, _, _, _, _) => env
15.90 + | _ => error "inform: uncovered case of get_istate"
15.91 +;
15.92 +(*+*)if term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
15.93 +(*+*) term2str f_in = "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)"
15.94 +(*+*)then () else error "inform with (positive) check_error_patterns broken 2";
15.95
15.96 -"~~~~~ fun locate_input_formula , args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
15.97 - (cs', (encode ifo));
15.98 -val SOME f_in = parse (assoc_thy "Isac") istr
15.99 -val f_in = Thm.term_of f_in
15.100 -val pos_pred = lev_back' pos
15.101 - (* f_pred ---"step pos cs"---> f_succ in appendFormula
15.102 - TODO.WN120517: one starting point for redesign of pos' *)
15.103 -val (f_pred, f_succ) = (get_curr_formula (pt, pos_pred), get_curr_formula (pt, pos));
15.104 -
15.105 -term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
15.106 -term2str f_succ = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";
15.107 -
15.108 - f_succ = f_in; (* = false*)
15.109 -cas_input f_in; (* = NONE*)
15.110 -val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in
15.111 -val ("no derivation found", calcstate') = msg_calcstate';
15.112 - val pp = par_pblobj pt p
15.113 - val {errpats, nrls, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
15.114 - val ScrState (env, _, _, _, _, _) = get_istate pt pos;
15.115 - case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
15.116 - SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
15.117 - | NONE => msg_calcstate';
15.118 -
15.119 -"~~~~~ from locate_input_formula return val:"; val () = ();
15.120 -case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
15.121 - SOME errpatID => ()
15.122 - | NONE => error "check_error_patterns broken";
15.123 + val SOME "chain-rule-diff-both" = (*case*) Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
15.124
15.125 "--- final check:";
15.126 -case locate_input_formula cs' (encode ifo) of
15.127 +case inform cs' (encode ifo) of
15.128 ("error pattern #chain-rule-diff-both#", calcstate') => ()
15.129 -| _ => error "locate_input_formula with (positive) check_error_patterns broken"
15.130 +| _ => error "inform with (positive) check_error_patterns broken"
15.131
15.132 -"--------- build fun get_fillpats --------------------------------";
15.133 -"--------- build fun get_fillpats --------------------------------";
15.134 -"--------- build fun get_fillpats --------------------------------";
15.135 -(*cause for this test was: wrong thy in Build_Thydata.thy in
15.136 - insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]*)
15.137 -val f_curr = str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
15.138 -val errpatID = "chain-rule-diff-both"
15.139 - val {errpats, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"]
15.140 -val env =
15.141 - [(str2term "f_f", str2term "x ^^^ 2 + sin (x ^^^ 4)"),
15.142 - (str2term "v_v", str2term "x"),
15.143 - (str2term "f_f'", str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))")]
15.144 - val subst = get_bdv_subst prog env
15.145 - val errpatthms = errpats
15.146 - |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
15.147 - |> map (#3: errpat -> thm list)
15.148 - |> flat;
15.149 -"~~~~~ fun get_fillpats, args:"; val (subst, form, errpatID, thm) =
15.150 - (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
15.151 - val thmDeriv = Thm.get_name_hint thm
15.152 - val (part, thyID) = thy_containing_thm thmDeriv
15.153 - val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
15.154 - val Hthm {fillpats, ...} = get_the theID
15.155 - val some = map (get_fillform subst (thm, form) errpatID) fillpats;
15.156 -"~~~~~ fun get_fillform, args:";
15.157 - val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
15.158 - (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
15.159 - val (form', _, _, rewritten) =
15.160 - rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (HOLogic.Trueprop $ pat) form;
15.161 -"~~~~~ fun rew_sub, args:"; val (thy, i, bdv, tless, rls, put_asm, lrd:lrd list, r, t) =
15.162 - ((Isac()), 1, subst, e_rew_ord, e_rls, false, [], (HOLogic.Trueprop $ pat), form);
15.163 - val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
15.164 - o Logic.strip_imp_concl) r;
15.165 -(*/-------------catch the planned exception*)
15.166 -(let
15.167 - val r' = Envir.subst_term (Pattern.match thy (lhs, t)
15.168 - (Vartab.empty, Vartab.empty)) r;
15.169 -in 111 end
15.170 -) handle PATTERN (*because only a subterm matches*) => 111;
15.171 -case t of t1 $ t2 =>
15.172 - let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2
15.173 - in
15.174 - if rew2 then (t1 $ t2', asm2, lrd, true) else
15.175 - let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1
15.176 - in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
15.177 - end;
15.178 -(*catch the planned exception-------------/*)
15.179 -
15.180 -val t1 $ t2 = t;
15.181 -val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2;
15.182 -"~~~~~ fun rew_sub, args:"; val (thy, i, bdv, tless, rls, put_asm, lrd:lrd list, r, t) =
15.183 - (thy, i, bdv, tless, rls, put_asm, (lrd@[R]), r, t2);
15.184 - val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r;
15.185 - val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r;
15.186 - val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'));
15.187 - val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r';
15.188 -if term2str t' = "cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
15.189 - else error "get_fillpats changed 1"
15.190 -DEconstrCalcTree 1;
15.191
15.192 "--------- embed fun find_fillpatterns ---------------------------";
15.193 "--------- embed fun find_fillpatterns ---------------------------";
16.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Jun 25 16:21:18 2019 +0200
16.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Jul 03 15:09:16 2019 +0200
16.3 @@ -7,6 +7,7 @@
16.4 "table of contents -----------------------------------------------------------------------------";
16.5 "-----------------------------------------------------------------------------------------------";
16.6 "----------- Take as 1st stac in program -------------------------------------------------------";
16.7 +"----------- build: fun locate_input_formula ---------------------------------------------------";
16.8 "-----------------------------------------------------------------------------------------------";
16.9 "-----------------------------------------------------------------------------------------------";
16.10 "-----------------------------------------------------------------------------------------------";
16.11 @@ -66,3 +67,147 @@
16.12 (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)
16.13
16.14
16.15 +"----------- build: fun locate_input_formula ---------------------------------------------------";
16.16 +"----------- build: fun locate_input_formula ---------------------------------------------------";
16.17 +"----------- build: fun locate_input_formula ---------------------------------------------------";
16.18 +(*co from ---input.sml: ------ appendFormula: on Res + late deriv ----*)
16.19 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
16.20 +val (dI',pI',mI') =
16.21 + ("Test", ["sqroot-test","univariate","equation","test"],
16.22 + ["Test","squ-equ-test-subpbl1"]);
16.23 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
16.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
16.31 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*FormKF "x + 1 = 2"*)
16.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*FormKF "x + 1 + -1 * 2 = 0"*)
16.33 +
16.34 +(*+*)if p = ([1], Res) then () else error "reset_states 1";
16.35 +(*+*)show_pt_tac pt; (*[
16.36 +([], Frm), solve (x + 1 = 2, x)
16.37 +. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
16.38 +([1], Frm), x + 1 = 2
16.39 +. . . . . . . . . . Rewrite_Set "norm_equation",
16.40 +([1], Res), x + 1 + -1 * 2 = 0
16.41 +. . . . . . . . . . Check_Postcond ["sqroot-test","univariate","equation","test"]]
16.42 +val it = (): unit*)
16.43 +(*NEW*)val ifo = "x = 1";
16.44 +(*NEW*)val ("ok", cs' as (_, _, (pt, p))) = (*case*) Math_Engine.step p ((pt, p),[]);
16.45 +
16.46 +(*case*) inform cs' (encode ifo) (*of*);
16.47 +"~~~~~ fun inform , args:"; val ((cs as (_, _, (pt, pos as (p, _))): Chead.calcstate'), istr)
16.48 + = (cs', (encode ifo));
16.49 +val SOME f_in = (*case*) TermC.parse (Celem.assoc_thy "Isac") istr (*of*);
16.50 + (* NONE \<longrightarrow> ("syntax error in '" ^ istr ^ "'", cs )*)
16.51 + val f_in = Thm.term_of f_in
16.52 + val f_succ = Ctree.get_curr_formula (pt, pos);
16.53 + (*if*) f_succ = f_in; (*then \<longrightarrow> "same-formula"*) (*else*)
16.54 + val NONE = (*case*) Inform.cas_input f_in (*of*);
16.55 + (*NEW*)val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
16.56 + (*NEW*)val {scr = prog, ...} = get_met metID
16.57 + (*NEW*)val PrfObj {loc = (_, SOME (istate, ctxt)), ...} = get_obj I pt p;
16.58 +
16.59 +(*NEW*)"~~~~~ fun locate_input_formula , args:"; val (prog, cstate, istate, ctxt, tm)
16.60 + = (prog, (pt, pos), istate, ctxt, f_in);
16.61 + val pos_pred = Ctree.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
16.62 + val f_pred = Ctree.get_curr_formula (pt, pos_pred)
16.63 +;
16.64 +(*+*)if term2str f_pred = "x + 1 + -1 * 2 = 0" then ()
16.65 + else error "result after locate_input_formula changed 1";
16.66 + case compare_step ([], [], (pt, pos_pred)) f_in of
16.67 + ("no derivation found", calcstate') => Not_Derivable calcstate'
16.68 + | ("ok", (_, _, cstate as (pt', pos'))) =>
16.69 + LucinNEW.Step (cstate, get_istate pt' pos', get_ctxt pt' pos')
16.70 + | _ => raise ERROR "compare_step: uncovered case"
16.71 +;
16.72 +locate_input_formula: scr -> state -> istate -> Proof.context -> term -> input_formula_result;
16.73 +"~~~~~ to inform return val:"; val () = ();
16.74 + case locate_input_formula prog (pt, pos) istate ctxt f_in of
16.75 + LucinNEW.Step (cstate, _(*istate*), _(*ctxt*)) =>
16.76 + ("ok" , ([], [], cstate (* already contains istate, ctxt *)))
16.77 + | Not_Derivable calcstate' =>
16.78 + let
16.79 + (*NEW*)val f_pred = Ctree.get_curr_formula (pt, pos_pred)
16.80 + val pp = Ctree.par_pblobj pt p
16.81 + val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
16.82 + {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
16.83 + | _ => error "inform: uncovered case of get_met"
16.84 + val env = case Ctree.get_istate pt pos of
16.85 + Selem.ScrState (env, _, _, _, _, _) => env
16.86 + | _ => error "inform: uncovered case of get_istate"
16.87 + in
16.88 + case Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
16.89 + SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
16.90 + | NONE => ("no derivation found", calcstate')
16.91 + end
16.92 +;
16.93 +"~~~~~ to appendFormula / me return val:"; val () = ();
16.94 +(*+*)val ("ok", (_, _, (pt, p))) = inform cs' (encode ifo)
16.95 +;
16.96 +(*+*)(*copy from "fun me "*)
16.97 + val (_, ts) =
16.98 + (case step p ((pt, Ctree.e_pos'),[]) of
16.99 + ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
16.100 + | ("helpless", _) => ("helpless: cannot propose tac", [])
16.101 + | ("no-fmz-spec", _) => error "no-fmz-spec"
16.102 + | ("end-of-calculation", (ts, _, _)) => ("", ts)
16.103 + | _ => error "me: uncovered case")
16.104 + handle ERROR msg => raise ERROR msg
16.105 + val tac =
16.106 + case ts of
16.107 + tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
16.108 + | _ => if p = ([], Ctree.Res) then Tac.End_Proof' else Tac.Empty_Tac;
16.109 +(*+*)(*copy from "fun me "*)val nxt = (Tac.tac2IDstr tac, tac)
16.110 +
16.111 +(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
16.112 +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
16.113 +(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
16.114 +
16.115 +if f2str f = "[x = 1]"andalso fst nxt = "End_Proof'"andalso p = ([], Res) then ()
16.116 +else error "result after locate_input_formula changed 3";
16.117 +
16.118 +if pr_ctree pr_short pt = (*=isabisacREP*)
16.119 +". ----- pblobj -----\n" ^
16.120 +"1. x + 1 = 2\n" ^
16.121 +"2. x + 1 + -1 * 2 = 0\n" ^
16.122 +"3. ----- pblobj -----\n" ^
16.123 +"3.1. -1 + x = 0\n" ^
16.124 +"3.2. x = 0 + -1 * -1\n" ^
16.125 +"3.2.1. x = 0 + -1 * -1\n" ^
16.126 +"3.2.2. x = 0 + 1\n" ^
16.127 +"4. [x = 1]\n" then ()
16.128 +else error "build fun locate_input_formula changed 4";
16.129 +(*show_pt_tac pt; [
16.130 +([], Frm), solve (x + 1 = 2, x)
16.131 +. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
16.132 +([1], Frm), x + 1 = 2
16.133 +. . . . . . . . . . Rewrite_Set "norm_equation",
16.134 +([1], Res), x + 1 + -1 * 2 = 0
16.135 +. . . . . . . . . . Rewrite_Set "Test_simplify",
16.136 +([2], Res), -1 + x = 0
16.137 +. . . . . . . . . . Subproblem (Test, ["LINEAR","univariate","equation","test"]),
16.138 +([3], Pbl), solve (-1 + x = 0, x)
16.139 +. . . . . . . . . . Apply_Method ["Test","solve_linear"],
16.140 +([3,1], Frm), -1 + x = 0
16.141 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
16.142 +([3,1], Res), x = 0 + -1 * -1
16.143 +. . . . . . . . . . Derive Test_simplify,
16.144 +([3,2,1], Frm), x = 0 + -1 * -1
16.145 +. . . . . . . . . . Rewrite ("#: -1 * -1 = 1", "-1 * -1 = 1"),
16.146 +([3,2,1], Res), x = 0 + 1
16.147 +. . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
16.148 +([3,2,2], Res), x = 1
16.149 +. . . . . . . . . . tac2str not impl. for ?!,
16.150 +([3,2], Res), x = 1
16.151 +. . . . . . . . . . Check_Postcond ["LINEAR","univariate","equation","test"],
16.152 +([3], Res), [x = 1]
16.153 +. . . . . . . . . . Check_elementwise "Assumptions",
16.154 +([4], Res), [x = 1]
16.155 +. . . . . . . . . . Check_Postcond ["sqroot-test","univariate","equation","test"],
16.156 +([], Res), [x = 1]]
16.157 +val it = (): unit*)
16.158 +
17.1 --- a/test/Tools/isac/Interpret/mathengine.sml Tue Jun 25 16:21:18 2019 +0200
17.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Wed Jul 03 15:09:16 2019 +0200
17.3 @@ -144,7 +144,7 @@
17.4 val ("ok", cs' as (_,_,(pt,p))) = step p cs;
17.5 val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2";
17.6 (*
17.7 - val ("no derivation found", (_,_,(pt, p))) = locate_input_formula cs' ((*encode*) ifo);
17.8 + val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo);
17.9 here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
17.10 *)
17.11
17.12 @@ -415,25 +415,25 @@
17.13 (auto, c, ptp);
17.14 val (_,_,mI) = get_obj g_spec pt p
17.15 val ctxt = get_ctxt pt pos
17.16 - val (ttt, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
17.17 + val (ttt, c', ptp) = begin_end_prog (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
17.18 (* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
17.19 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
17.20 (auto, (c @ c'), ptp);
17.21 p = ([], Res) (*false p = ([1], Frm)*);
17.22 member op = [Pbl,Met] p_ (*false*);
17.23 -val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "norm_equation"*)
17.24 +val (ttt, c', ptp') = do_solve_step ptp; (*ttt = Rewrite_Set "norm_equation"*)
17.25 (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
17.26 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
17.27 (auto, (c @ c'), ptp');
17.28 p = ([], Res) (*false p = ([1], Res)*);
17.29 member op = [Pbl,Met] p_ (*false*);
17.30 -val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "Test_simplify"*)
17.31 +val (ttt, c', ptp') = do_solve_step ptp; (*ttt = Rewrite_Set "Test_simplify"*)
17.32 (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
17.33 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
17.34 (auto, (c @ c'), ptp');
17.35 p = ([], Res) (*false p = ([2], Res)*);
17.36 member op = [Pbl,Met] p_ (*false*);
17.37 -val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp;
17.38 +val ((Subproblem _, tac_, (_, is))::_, c', ptp') = do_solve_step ptp;
17.39 autoord auto < 5 (*false*);
17.40 (* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)
17.41 "~~~~~ fun all_modspec, args:"; val (pt, pos as (p,_)) = (ptp');
17.42 @@ -507,7 +507,7 @@
17.43 ip = ([],Res); (*false*)
17.44 ip = p; (*false*)
17.45 member op = [Pbl,Met] p_; (*false*)
17.46 -"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
17.47 +"~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
17.48 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
17.49 val thy' = get_obj g_domID pt (par_pblobj pt p);
17.50 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
17.51 @@ -608,10 +608,10 @@
17.52 (CompleteSubpbl, [], (pt',pos'));
17.53 p = ([], Res) = false;
17.54 member op = [Pbl,Met] p_ = false;
17.55 -val (_, c', ptp') = nxt_solve_ ptp;
17.56 +val (_, c', ptp') = do_solve_step ptp;
17.57 (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
17.58 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
17.59 -"~~~~~ fun nxt_solve_, args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
17.60 +"~~~~~ fun do_solve_step, args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
17.61 e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
17.62 val thy' = get_obj g_domID pt (par_pblobj pt p);
17.63 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
17.64 @@ -631,7 +631,7 @@
17.65 (*----------------------------------------------------------------------------------------------*)
17.66 ;
17.67 (*SEARCH FOR THE ERROR WENT DOWN TO THE END OF THIS TEST, AND THEN UP TO HERE AGAIN*)
17.68 -"~~~~~ fun nxt_solv, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp);
17.69 +"~~~~~ fun begin_end_prog, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp);
17.70 val pos =
17.71 case pos of
17.72 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
17.73 @@ -716,8 +716,8 @@
17.74 (* val cs = get_calc cI (* we improve from the calcstate here [*] *);
17.75 val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);*)
17.76 val ("ok", cs') = step pos cs;
17.77 -(*val ("ok", (_, c, ptp as (_,p))) = *)locate_input_formula cs' (encode ifo);
17.78 -"~~~~~ fun locate_input_formula , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
17.79 +(*val ("ok", (_, c, ptp as (_,p))) = *)inform cs' (encode ifo);
17.80 +"~~~~~ fun inform , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
17.81 (cs', (encode ifo));
17.82 val SOME f_in = parse (assoc_thy "Isac") istr
17.83 val f_in = Thm.term_of f_in
18.1 --- a/test/Tools/isac/Knowledge/atools.sml Tue Jun 25 16:21:18 2019 +0200
18.2 +++ b/test/Tools/isac/Knowledge/atools.sml Wed Jul 03 15:09:16 2019 +0200
18.3 @@ -273,7 +273,7 @@
18.4 if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
18.5 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
18.6
18.7 -val SOME (t', _) = rewrite_set_inst_ thy false subst make_polynomial_in ppp;
18.8 +val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
18.9 if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
18.10 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
18.11
19.1 --- a/test/Tools/isac/Knowledge/diff.sml Tue Jun 25 16:21:18 2019 +0200
19.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Jul 03 15:09:16 2019 +0200
19.3 @@ -20,7 +20,7 @@
19.4 "----------- autoCalculate diff after_simplification ----";
19.5 "----------- autoCalculate differentiate_equality -------";
19.6 "----------- tests for examples -------------------------";
19.7 -"------------locate_input_formula for x^2+x+1 -------------------------";
19.8 +"------------inform for x^2+x+1 -------------------------";
19.9 "--------------------------------------------------------";
19.10 "--------------------------------------------------------";
19.11 "--------------------------------------------------------";
19.12 @@ -409,9 +409,9 @@
19.13 val subs = [(str2term "bdv", str2term "l")];
19.14 val f = str2term "G' = d_d l (l * sqrt (7 * s ^^^ 2 - l ^^^ 2))";
19.15
19.16 -"------------locate_input_formula for x^2+x+1 -------------------------";
19.17 -"------------locate_input_formula for x^2+x+1 -------------------------";
19.18 -"------------locate_input_formula for x^2+x+1 -------------------------";
19.19 +"------------inform for x^2+x+1 -------------------------";
19.20 +"------------inform for x^2+x+1 -------------------------";
19.21 +"------------inform for x^2+x+1 -------------------------";
19.22 reset_states ();
19.23 CalcTree
19.24 [(["functionTerm (x^2 + x + 1)",
20.1 --- a/test/Tools/isac/Knowledge/inssort.sml Tue Jun 25 16:21:18 2019 +0200
20.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Wed Jul 03 15:09:16 2019 +0200
20.3 @@ -118,7 +118,7 @@
20.4 "----------- insertion sort: CAS-command -------------------------------------";
20.5 "----------- insertion sort: CAS-command -------------------------------------";
20.6 val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
20.7 -val (_,(_,c,(pt,p))) = locate_input_formula ([],[],(pt,p)) "Sort {||1, 3, 2||}";
20.8 +val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "Sort {||1, 3, 2||}";
20.9 show_pt pt;
20.10 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method",..*)
20.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
21.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Tue Jun 25 16:21:18 2019 +0200
21.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Wed Jul 03 15:09:16 2019 +0200
21.3 @@ -49,7 +49,7 @@
21.4 tacis; " = []";
21.5 pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*)
21.6 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";
21.7 -(*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
21.8 +(*do_solve_step (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
21.9 THIS MEANS: replace no_meth by [no_meth] in Script.*)
21.10 (*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *)
21.11 (*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)
21.12 @@ -69,7 +69,7 @@
21.13 pIopt (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*);
21.14 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); " = false";
21.15 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into
21.16 -nxt_solve_, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
21.17 +do_solve_step, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
21.18 This ERROR seems to be introduced together with ctxt, concerns Apply_Method without init_form.
21.19 See TODO.txt
21.20 *)
22.1 --- a/test/Tools/isac/Knowledge/rateq.sml Tue Jun 25 16:21:18 2019 +0200
22.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Jul 03 15:09:16 2019 +0200
22.3 @@ -100,7 +100,7 @@
22.4 1-1 associated to metID ["RatEq", "solve_rat_equation"]*)
22.5 tacis; (*= []*)
22.6 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
22.7 -"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
22.8 +"~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
22.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
22.10 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
22.11 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
22.12 @@ -288,7 +288,7 @@
22.13 ip = ([],Res); (* = false*)
22.14 tacis; (* = []*)
22.15 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (* = false*)
22.16 -"~~~~~ and nxt_solve_, args:"; val ((ptp as (pt, pos as (p,p_)))) = ((pt,ip));
22.17 +"~~~~~ and do_solve_step, args:"; val ((ptp as (pt, pos as (p,p_)))) = ((pt,ip));
22.18 e_metID = get_obj g_metID pt (par_pblobj pt p); (* = false*)
22.19 val thy' = get_obj g_domID pt (par_pblobj pt p);
22.20 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
22.21 @@ -319,7 +319,7 @@
22.22 nxt_up thy ptp (Prog sc) E up ay (go up sc) a v;
22.23 nstep_up thy ptp sc E l Skip_ a v;
22.24 determine_next_tactic (thy',srls) (pt,pos) sc is;
22.25 -nxt_solve_ (pt,ip);
22.26 +do_solve_step (pt,ip);
22.27 step p ((pt, e_pos'),[]);
22.28 *)
22.29 val (p,_,f,nxt,_,pt) = me nxt p''' [1] pt''';
23.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Tue Jun 25 16:21:18 2019 +0200
23.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Wed Jul 03 15:09:16 2019 +0200
23.3 @@ -100,7 +100,7 @@
23.4 tacis; (*= []*)
23.5 pIopt; (*= SOME ["sq", "rootX", "univariate", "equation"]*)
23.6 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
23.7 -"~~~~~ fun nxt_solve_, args:"; (*stopped due to strange exn
23.8 +"~~~~~ fun do_solve_step, args:"; (*stopped due to strange exn
23.9 "check_elementwise: no set 1 = 2 + -2 * sqrt x"*)
23.10
23.11 (*---- 2nd try: we investigate the script ["RootEq","solve_sq_root_equation"] found via pbl*)
23.12 @@ -112,7 +112,7 @@
23.13 [univariate,equation] and to refine to ["sq", "rootX", "univariate", "equation"] in 2002*)
23.14
23.15 (*(*these are the errors during stepping into the code:*)
23.16 -nxt_solve_ (pt,ip); (*check_elementwise: no set 1 = 2 + -2 * sqrt x: fun mk_set raises
23.17 +do_solve_step (pt,ip); (*check_elementwise: no set 1 = 2 + -2 * sqrt x: fun mk_set raises
23.18 this exn in Check_elementwise ONLY ?!?*)
23.19 step p ((pt, e_pos'),[]); (* = ("helpless",*)
23.20 *)
24.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Jun 25 16:21:18 2019 +0200
24.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Jul 03 15:09:16 2019 +0200
24.3 @@ -126,7 +126,7 @@
24.4 case tacis of [] => ();
24.5 case pIopt of SONE => ();
24.6 member op = [Ctree.Pbl, Ctree.Met] p_ andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (* = false*);
24.7 -"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt,ip);
24.8 +"~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt,ip);
24.9 Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*);
24.10 val thy' = get_obj g_domID pt (par_pblobj pt p);
24.11 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
25.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Jun 25 16:21:18 2019 +0200
25.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Jul 03 15:09:16 2019 +0200
25.3 @@ -104,7 +104,7 @@
25.4 (*if*) ip = p = false;
25.5 (*if*) member op = [Pbl, Met] p_ = false;
25.6
25.7 -"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
25.8 +"~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
25.9 e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
25.10 val thy' = get_obj g_domID pt (par_pblobj pt p);
25.11 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
26.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Tue Jun 25 16:21:18 2019 +0200
26.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Jul 03 15:09:16 2019 +0200
26.3 @@ -61,7 +61,7 @@
26.4 val pIopt = get_pblID (pt,ip);
26.5 tacis; (*= []*)
26.6 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
26.7 -"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
26.8 +"~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
26.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
26.10 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
26.11 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)),
27.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Tue Jun 25 16:21:18 2019 +0200
27.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Wed Jul 03 15:09:16 2019 +0200
27.3 @@ -42,13 +42,13 @@
27.4 tacis; (*= []*)
27.5 val SOME pI = pIopt;
27.6 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
27.7 -"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
27.8 +"~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
27.9 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
27.10 val thy' = get_obj g_domID pt (par_pblobj pt p);
27.11 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
27.12 val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is;
27.13 ;tac_; (* = Check_Postcond' *)
27.14 -"~~~~~ fun nxt_solv, args:"; val ((Check_Postcond' (pI,_)), _, (pt, pos as (p,p_))) =
27.15 +"~~~~~ fun begin_end_prog, args:"; val ((Check_Postcond' (pI,_)), _, (pt, pos as (p,p_))) =
27.16 (tac_, is, ptp);
27.17 val pp = par_pblobj pt p
27.18 val asm =
28.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Tue Jun 25 16:21:18 2019 +0200
28.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Jul 03 15:09:16 2019 +0200
28.3 @@ -52,7 +52,7 @@
28.4 val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
28.5 tacis; (*= []*)
28.6 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
28.7 -"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
28.8 +"~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
28.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
28.10 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
28.11 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)),
29.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Tue Jun 25 16:21:18 2019 +0200
29.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Jul 03 15:09:16 2019 +0200
29.3 @@ -104,9 +104,9 @@
29.4 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_, p_)))) = (CompleteSubpbl, [], (pt', pos'));
29.5 (*if*) p = ([], Res) (* = false*);
29.6 (*if*) member op = [Pbl,Met] p_ (* = false*);
29.7 -(*case*) nxt_solve_ ptp (*of*)
29.8 +(*case*) do_solve_step ptp (*of*)
29.9 ;
29.10 -"~~~~~ and nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (ptp);
29.11 +"~~~~~ and do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (ptp);
29.12 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false isabisac = ?*);
29.13 val thy' = get_obj g_domID pt (par_pblobj pt p);
29.14 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
30.1 --- a/test/Tools/isac/OLDTESTS/tacis.sml Tue Jun 25 16:21:18 2019 +0200
30.2 +++ b/test/Tools/isac/OLDTESTS/tacis.sml Wed Jul 03 15:09:16 2019 +0200
30.3 @@ -46,7 +46,7 @@
30.4 autoCalculate 1 CompleteCalcHead; refFormula 1 (get_pos 1 1) (*OK*);
30.5 (*###########################################autoCalculate 1 (Step 1);*)
30.6 fetchProposedTactic 1 (*'Apply_Method Test solve_linear' in tacis*);
30.7 - (* there was the only error ^^^^^^^^^ in step/nxt_solv ..Apply_Method..
30.8 + (* there was the only error ^^^^^^^^^ in step/begin_end_prog ..Apply_Method..
30.9 val (str', (tacis', (pt',p'))) = step ip (ptp, tacis);
30.10 writeln (tacis2str tacis');
30.11 ######################################################################*)