1.1 --- a/src/Tools/isac/Interpret/inform.sml Mon Jun 24 14:02:39 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Jun 24 14:44:51 2019 +0200
1.3 @@ -11,19 +11,20 @@
1.4 type icalhd = Ctree.pos' * Rule.cterm' * imodel * Ctree.pos_ * Celem.spec
1.5 val fetchErrorpatterns : Tac.tac -> Rule.errpatID list
1.6 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
1.7 - val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
1.8 val find_fillpatterns : Ctree.state -> Rule.errpatID -> (Celem.fillpatID * term * thm * Selem.subs option) list
1.9 val is_exactly_equal : Ctree.state -> string -> string * Tac.tac
1.10 +(*cp here from "! aktivate for Test_Isac" below due to LucinNEW*)
1.11 + val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
1.12 + Rule.rls -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
1.13 + val mk_tacis: Rule.rew_ord' * 'a -> Rule.rls -> term * Rule.rule * (term * term list) -> Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))
1.14 +
1.15 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.16 (* NONE *)
1.17 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.18 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
1.19 val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
1.20 val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
1.21 - val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
1.22 val check_err_patt : term * term -> Rule.subst -> Rule.errpatID * term -> Rule.rls -> Rule.errpatID option
1.23 - val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
1.24 - Rule.rls -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
1.25 val check_error_patterns :
1.26 term * term ->
1.27 term * (term * term) list -> (Rule.errpatID * term list * 'a list) list * Rule.rls -> Rule.errpatID option
1.28 @@ -39,7 +40,7 @@
1.29 ('c * ''b * bool * 'd * Model.itm_) list
1.30 end
1.31
1.32 -structure Inform(**): INPUT_FORMULAS(**) =
1.33 +structure Inform(** ): INPUT_FORMULAS( **) =
1.34 struct
1.35
1.36 (*** handle an input calc-head ***)
1.37 @@ -368,47 +369,6 @@
1.38 else (false, [])
1.39 end
1.40
1.41 -(* compare inform with ctree.form at current pos by nrls;
1.42 - if found, embed the derivation generated during comparison
1.43 - if not, let the mat-engine compute the next ctree.form *)
1.44 -(* code's structure is copied from complete_solve
1.45 - CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
1.46 - all_modspec etc. has to be inserted at Subproblem'*)
1.47 -fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): Chead.calcstate') ifo =
1.48 - let
1.49 - val fo =
1.50 - case p_ of
1.51 - Ctree.Frm => Ctree.get_obj Ctree.g_form pt p
1.52 - | Ctree.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.53 - | _ => Rule.e_term (*on PblObj is fo <> ifo*);
1.54 - val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
1.55 - val {rew_ord, erls, rules, ...} = Rule.rep_rls nrls
1.56 - val (found, der) = concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
1.57 - in
1.58 - if found
1.59 - then
1.60 - let
1.61 - val tacis' = map (mk_tacis rew_ord erls) der;
1.62 - val (c', ptp) = Generate.embed_deriv tacis' ptp;
1.63 - in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
1.64 - else
1.65 - if pos = ([], Ctree.Res) (*TODO: we should stop earlier with trying subproblems *)
1.66 - then ("no derivation found", (tacis, c, ptp): Chead.calcstate')
1.67 - else
1.68 - let
1.69 - val cs' as (tacis, c', ptp) = Solve.nxt_solve_ ptp; (*<---------------------*)
1.70 - val (tacis, c'', ptp) = case tacis of
1.71 - ((Tac.Subproblem _, _, _)::_) =>
1.72 - let
1.73 - val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)
1.74 - val mI = Ctree.get_obj Ctree.g_metID pt p
1.75 - in
1.76 - Solve.nxt_solv (Tac.Apply_Method' (mI, NONE, Selem.e_istate, Selem.e_ctxt)) (Selem.e_istate, Selem.e_ctxt) ptp
1.77 - end
1.78 - | _ => cs';
1.79 - in compare_step (tacis, c @ c' @ c'', ptp) ifo end
1.80 - end
1.81 -
1.82 (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
1.83 fun check_err_patt (res, inf) subst (errpatID, pat) rls =
1.84 let
1.85 @@ -446,54 +406,6 @@
1.86 | SOME errpatID => SOME errpatID
1.87 in scans errpats end;
1.88
1.89 -(*.handle a user-input formula, which may be a CAS-command, too.
1.90 -CAS-command:
1.91 - create a calchead, and do 1 step
1.92 - TOOODO.WN0602 works only for the root-problem !!!
1.93 -formula, which is no CAS-command:
1.94 - compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
1.95 - collect all the tacs applied by the way;
1.96 - if "no derivation found" then check_error_patterns.
1.97 - ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*)
1.98 -fun inform (cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =
1.99 - case TermC.parse (Celem.assoc_thy "Isac") istr of
1.100 - SOME f_in =>
1.101 - let
1.102 - val f_in = Thm.term_of f_in
1.103 - val f_succ = Ctree.get_curr_formula (pt, pos);
1.104 - in
1.105 - if f_succ = f_in
1.106 - then ("same-formula", cs) (* ctree not cut with replaceFormula *)
1.107 - else
1.108 - case cas_input f_in of
1.109 - SOME (pt, _) => ("ok",([], [], (pt, (p, Ctree.Met))))
1.110 - | NONE =>
1.111 - let
1.112 - val pos_pred = Ctree.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
1.113 - val f_pred = Ctree.get_curr_formula (pt, pos_pred)
1.114 - val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*)
1.115 - (*last step re-calc in compare_step TODO before WN09*)
1.116 - in
1.117 - case msg_calcstate' of
1.118 - ("no derivation found", calcstate') =>
1.119 - let
1.120 - val pp = Ctree.par_pblobj pt p
1.121 - val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
1.122 - {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
1.123 - | _ => error "inform: uncovered case of get_met"
1.124 - val env = case Ctree.get_istate pt pos of
1.125 - Selem.ScrState (env, _, _, _, _, _) => env
1.126 - | _ => error "inform: uncovered case of get_istate"
1.127 - in
1.128 - case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
1.129 - SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
1.130 - | NONE => msg_calcstate'
1.131 - end
1.132 - | _ => msg_calcstate'
1.133 - end
1.134 - end
1.135 - | NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate')
1.136 -
1.137 (* fill-in patterns an forms.
1.138 returns thm required by "fun in_fillform *)
1.139 fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) =
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Jun 24 14:02:39 2019 +0200
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Jun 24 14:44:51 2019 +0200
2.3 @@ -7,7 +7,15 @@
2.4 sig
2.5 val next_tac : (*diss: next-tactic-function*)
2.6 Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> Selem.istate * 'a -> Tac.tac_ * (Selem.istate * 'a) * (term * Selem.safe)
2.7 + val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
2.8 + val nxt_solve_ : Ctree.ctree * Ctree.pos' ->
2.9 + (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list *
2.10 + Ctree.pos' list * Ctree.state
2.11
2.12 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.13 + val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
2.14 +
2.15 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.16 end
2.17
2.18 structure LucinNEW(** ): LUCAS_INTERPRETER( **) = (*LucinNEW \<rightarrow> Lucin after code re-arrangement*)
2.19 @@ -265,4 +273,155 @@
2.20 (m', (Selem.ScrState scrst, ctxt), (v, Selem.Sundef))) (*next stac*)
2.21 | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (Selem.istate2str is));
2.22
2.23 +(* FIXME.WN050821 compare fun solve ... fun nxt_solv
2.24 + nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *)
2.25 +fun nxt_solv (Tac.Apply_Method' (mI, _, _, _)) _ (pt, pos as (p, _)) =
2.26 + let
2.27 + val {ppc, ...} = Specify.get_met mI;
2.28 + val (itms, oris, probl) = case get_obj I pt p of
2.29 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
2.30 + | _ => error "nxt_solv Apply_Method': uncovered case get_obj"
2.31 + val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
2.32 + val thy' = get_obj g_domID pt p;
2.33 + val thy = Celem.assoc_thy thy';
2.34 +(*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
2.35 +val itms =
2.36 + if mI = ["Biegelinien", "ausBelastung"]
2.37 + then itms @
2.38 + [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
2.39 + [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
2.40 + (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
2.41 + [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
2.42 + (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
2.43 + [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
2.44 + (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
2.45 + [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
2.46 + else itms
2.47 +(*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
2.48 + val (is, env, ctxt, scr) = case Lucin.init_scrstate thy itms mI of
2.49 + (is as Selem.ScrState (env,_,_,_,_,_), ctxt, scr) => (is, env, ctxt, scr)
2.50 + | _ => error "nxt_solv Apply_Method': uncovered case init_scrstate"
2.51 + val ini = Lucin.init_form thy scr env;
2.52 + in
2.53 + case ini of
2.54 + SOME t =>
2.55 + let
2.56 + val pos = ((lev_on o lev_dn) p, Frm)
2.57 + val tac_ = Tac.Apply_Method' (mI, SOME t, is, ctxt);
2.58 + val (pos, c, _, pt) = Generate.generate1 thy tac_ (is, ctxt) pos pt (* implicit Take *)
2.59 + in
2.60 + ([(Tac.Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos))
2.61 + end
2.62 + | NONE =>
2.63 + let
2.64 + val pt = update_env pt (fst pos) (SOME (is, ctxt))
2.65 + val (tacis, c, ptp) = nxt_solve_ (pt, pos)
2.66 + in (tacis @ [(Tac.Apply_Method mI, Tac.Apply_Method' (mI, NONE, Selem.e_istate, ctxt), (pos, (is, ctxt)))],
2.67 + c, ptp)
2.68 + end
2.69 + end
2.70 + | nxt_solv (Tac.Check_Postcond' (pI, _)) _ (pt, (p, p_)) =
2.71 + let
2.72 + val pp = par_pblobj pt p
2.73 + val asm = (case get_obj g_tac pt p of
2.74 + Tac.Check_elementwise _ => (snd o (get_obj g_result pt)) p (*collects and instantiates asms*)
2.75 + | _ => get_assumptions_ pt (p, p_))
2.76 + handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)
2.77 + val metID = get_obj g_metID pt pp;
2.78 + val {srls = srls, scr = sc, ...} = Specify.get_met metID;
2.79 + val (loc, E, l, a, b, ctxt) = case get_loc pt (p, p_) of
2.80 + loc as (Selem.ScrState (E,l,a,_,_,b), ctxt) => (loc, E, l, a, b, ctxt)
2.81 + | _ => error "nxt_solv Check_Postcond': uncovered case get_loc"
2.82 + val thy' = get_obj g_domID pt pp;
2.83 + val thy = Celem.assoc_thy thy';
2.84 + val (_, _, (scval, scsaf)) = next_tac (thy', srls) (pt, (p, p_)) sc loc;
2.85 + in
2.86 + if pp = []
2.87 + then
2.88 + let
2.89 + val is = Selem.ScrState (E, l, a, scval, scsaf, b)
2.90 + val tac_ = Tac.Check_Postcond'(pI,(scval, asm))
2.91 + val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;
2.92 + in ([(Tac.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p, p_))) end
2.93 + else
2.94 + let (*resume script of parpbl, transfer value of subpbl-script*)
2.95 + val ppp = par_pblobj pt (lev_up p);
2.96 + val thy' = get_obj g_domID pt ppp;
2.97 + val thy = Celem.assoc_thy thy';
2.98 + val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of
2.99 + (Selem.ScrState (E,l,a,_,_,b), ctxt') => (E, l, a, b, ctxt')
2.100 + | _ => error "nxt_solv Check_Postcond' script of parpbl: uncovered case get_loc"
2.101 + val ctxt'' = Stool.from_subpbl_to_caller ctxt scval ctxt'
2.102 + val tac_ = Tac.Check_Postcond' (pI, (scval, asm))
2.103 + val is = Selem.ScrState (E,l,a,scval,scsaf,b)
2.104 + val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
2.105 + in ([(Tac.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p, p_))) end
2.106 + end
2.107 + | nxt_solv (Tac.End_Proof'') _ ptp = ([], [], ptp)
2.108 + | nxt_solv tac_ is (pt, pos) =
2.109 + let
2.110 + val pos = case pos of
2.111 + (p, Met) => ((lev_on o lev_dn) p, Frm) (* begin script *)
2.112 + | (p, Res) => (lev_on p, Res) (* somewhere in script *)
2.113 + | _ => pos
2.114 + val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac") tac_ is pos pt;
2.115 + in
2.116 + ([(Lucin.tac_2tac tac_, tac_, (pos, is))], c, (pt, pos'))
2.117 + end
2.118 +(* find the next tac from the script, nxt_solv will update the ctree *)
2.119 +and nxt_solve_ (ptp as (pt, pos as (p, p_))) =
2.120 + if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)
2.121 + then ([], [], (pt, (p, p_)))
2.122 + else
2.123 + let
2.124 + val thy' = get_obj g_domID pt (par_pblobj pt p);
2.125 + val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
2.126 + val (tac_, is, (t, _)) = next_tac (thy', srls) (pt, pos) sc is;
2.127 + (* TODO here ^^^ return finished/helpless/ok !*)
2.128 + in case tac_ of
2.129 + Tac.End_Detail' _ => ([(Tac.End_Detail, Tac.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos))
2.130 + | _ => nxt_solv tac_ is ptp
2.131 + end;
2.132 +
2.133 +(* compare inform with ctree.form at current pos by nrls;
2.134 + if found, embed the derivation generated during comparison
2.135 + if not, let the mat-engine compute the next ctree.form *)
2.136 +(* code's structure is copied from complete_solve
2.137 + CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
2.138 + all_modspec etc. has to be inserted at Subproblem'*)
2.139 +fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): Chead.calcstate') ifo =
2.140 + let
2.141 + val fo =
2.142 + case p_ of
2.143 + Ctree.Frm => Ctree.get_obj Ctree.g_form pt p
2.144 + | Ctree.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
2.145 + | _ => Rule.e_term (*on PblObj is fo <> ifo*);
2.146 + val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
2.147 + val {rew_ord, erls, rules, ...} = Rule.rep_rls nrls
2.148 + val (found, der) = Inform.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
2.149 + in
2.150 + if found
2.151 + then
2.152 + let
2.153 + val tacis' = map (Inform.mk_tacis rew_ord erls) der;
2.154 + val (c', ptp) = Generate.embed_deriv tacis' ptp;
2.155 + in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
2.156 + else
2.157 + if pos = ([], Ctree.Res) (*TODO: we should stop earlier with trying subproblems *)
2.158 + then ("no derivation found", (tacis, c, ptp): Chead.calcstate')
2.159 + else
2.160 + let
2.161 + val cs' as (tacis, c', ptp) = nxt_solve_ ptp; (*<---------------------*)
2.162 + val (tacis, c'', ptp) = case tacis of
2.163 + ((Tac.Subproblem _, _, _)::_) =>
2.164 + let
2.165 + val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)
2.166 + val mI = Ctree.get_obj Ctree.g_metID pt p
2.167 + in
2.168 + nxt_solv (Tac.Apply_Method' (mI, NONE, Selem.e_istate, Selem.e_ctxt)) (Selem.e_istate, Selem.e_ctxt) ptp
2.169 + end
2.170 + | _ => cs';
2.171 + in compare_step (tacis, c @ c' @ c'', ptp) ifo end
2.172 + end
2.173 +
2.174 end
3.1 --- a/src/Tools/isac/Interpret/mathengine.sml Mon Jun 24 14:02:39 2019 +0200
3.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Mon Jun 24 14:44:51 2019 +0200
3.3 @@ -132,7 +132,7 @@
3.4 in
3.5 case tac of
3.6 Tac.Apply_Method mI =>
3.7 - Solve.nxt_solv (Tac.Apply_Method' (mI, NONE, Selem.e_istate, Selem.e_ctxt)) (Selem.e_istate, Selem.e_ctxt) ptp
3.8 + LucinNEW.nxt_solv (Tac.Apply_Method' (mI, NONE, Selem.e_istate, Selem.e_ctxt)) (Selem.e_istate, Selem.e_ctxt) ptp
3.9 | _ => Chead.nxt_specif tac ptp
3.10 end
3.11 end
3.12 @@ -201,7 +201,7 @@
3.13 let val (pt',c',p') = Generate.generate tacis (pt,[],p)
3.14 in ("ok", (tacis, c', (pt', p'))) end
3.15 else (case (if member op = [Ctree.Pbl, Ctree.Met] p_
3.16 - then nxt_specify_ (pt, ip) else Solve.nxt_solve_ (pt, ip))
3.17 + then nxt_specify_ (pt, ip) else LucinNEW.nxt_solve_ (pt, ip))
3.18 handle ERROR msg => (writeln ("*** " ^ msg);
3.19 ([], [], ptp)) (*e.g. Add_Given "equality///"*) of
3.20 cs as ([],_,_) => ("helpless", cs)
3.21 @@ -212,7 +212,7 @@
3.22 (case if member op = [Ctree.Pbl, Ctree.Met] p_
3.23 andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p))
3.24 then nxt_specify_ (pt, ip)
3.25 - else (Solve.nxt_solve_ (pt,ip))
3.26 + else (LucinNEW.nxt_solve_ (pt,ip))
3.27 handle ERROR msg => (writeln ("*** " ^ msg);
3.28 ([],[],ptp)) (*e.g. Add_Given "equality///"*) of
3.29 cs as ([],_,_) =>("helpless", cs) (*FIXXME del.handle*)
4.1 --- a/src/Tools/isac/Interpret/solve.sml Mon Jun 24 14:02:39 2019 +0200
4.2 +++ b/src/Tools/isac/Interpret/solve.sml Mon Jun 24 14:44:51 2019 +0200
4.3 @@ -12,14 +12,10 @@
4.4 val mk_tac'_ : Tac.tac -> string * Tac.tac
4.5 val specsteps : string list
4.6
4.7 - val nxt_solve_ : Ctree.ctree * Ctree.pos' ->
4.8 - (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list *
4.9 - Ctree.pos' list * Ctree.state
4.10 val all_solve : auto -> Ctree.pos' list -> Ctree.state ->
4.11 string * Ctree.pos' list * (Ctree.ctree * (int list * Ctree.pos_))
4.12 val complete_solve :
4.13 auto -> Ctree.pos' list -> Ctree.state -> string * Ctree.pos' list * Ctree.state
4.14 - val nxt_solv : Tac.tac_ -> Selem.istate * Proof.context -> Ctree.state -> Chead.calcstate'
4.15 val solve : string * Tac.tac_ -> Ctree.state -> string * Chead.calcstate'
4.16
4.17 val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
4.18 @@ -234,116 +230,6 @@
4.19 end
4.20 end;
4.21
4.22 -(* FIXME.WN050821 compare fun solve ... fun nxt_solv
4.23 - nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *)
4.24 -fun nxt_solv (Tac.Apply_Method' (mI, _, _, _)) _ (pt, pos as (p, _)) =
4.25 - let
4.26 - val {ppc, ...} = Specify.get_met mI;
4.27 - val (itms, oris, probl) = case get_obj I pt p of
4.28 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
4.29 - | _ => error "nxt_solv Apply_Method': uncovered case get_obj"
4.30 - val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
4.31 - val thy' = get_obj g_domID pt p;
4.32 - val thy = Celem.assoc_thy thy';
4.33 -(*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
4.34 -val itms =
4.35 - if mI = ["Biegelinien", "ausBelastung"]
4.36 - then itms @
4.37 - [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
4.38 - [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
4.39 - (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
4.40 - [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
4.41 - (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
4.42 - [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
4.43 - (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
4.44 - [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
4.45 - else itms
4.46 -(*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
4.47 - val (is, env, ctxt, scr) = case Lucin.init_scrstate thy itms mI of
4.48 - (is as Selem.ScrState (env,_,_,_,_,_), ctxt, scr) => (is, env, ctxt, scr)
4.49 - | _ => error "nxt_solv Apply_Method': uncovered case init_scrstate"
4.50 - val ini = Lucin.init_form thy scr env;
4.51 - in
4.52 - case ini of
4.53 - SOME t =>
4.54 - let
4.55 - val pos = ((lev_on o lev_dn) p, Frm)
4.56 - val tac_ = Tac.Apply_Method' (mI, SOME t, is, ctxt);
4.57 - val (pos, c, _, pt) = Generate.generate1 thy tac_ (is, ctxt) pos pt (* implicit Take *)
4.58 - in
4.59 - ([(Tac.Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos))
4.60 - end
4.61 - | NONE =>
4.62 - let
4.63 - val pt = update_env pt (fst pos) (SOME (is, ctxt))
4.64 - val (tacis, c, ptp) = nxt_solve_ (pt, pos)
4.65 - in (tacis @ [(Tac.Apply_Method mI, Tac.Apply_Method' (mI, NONE, Selem.e_istate, ctxt), (pos, (is, ctxt)))],
4.66 - c, ptp)
4.67 - end
4.68 - end
4.69 - | nxt_solv (Tac.Check_Postcond' (pI, _)) _ (pt, (p, p_)) =
4.70 - let
4.71 - val pp = par_pblobj pt p
4.72 - val asm = (case get_obj g_tac pt p of
4.73 - Tac.Check_elementwise _ => (snd o (get_obj g_result pt)) p (*collects and instantiates asms*)
4.74 - | _ => get_assumptions_ pt (p, p_))
4.75 - handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)
4.76 - val metID = get_obj g_metID pt pp;
4.77 - val {srls = srls, scr = sc, ...} = Specify.get_met metID;
4.78 - val (loc, E, l, a, b, ctxt) = case get_loc pt (p, p_) of
4.79 - loc as (Selem.ScrState (E,l,a,_,_,b), ctxt) => (loc, E, l, a, b, ctxt)
4.80 - | _ => error "nxt_solv Check_Postcond': uncovered case get_loc"
4.81 - val thy' = get_obj g_domID pt pp;
4.82 - val thy = Celem.assoc_thy thy';
4.83 - val (_, _, (scval, scsaf)) = LucinNEW.next_tac (thy', srls) (pt, (p, p_)) sc loc;
4.84 - in
4.85 - if pp = []
4.86 - then
4.87 - let
4.88 - val is = Selem.ScrState (E, l, a, scval, scsaf, b)
4.89 - val tac_ = Tac.Check_Postcond'(pI,(scval, asm))
4.90 - val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;
4.91 - in ([(Tac.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p, p_))) end
4.92 - else
4.93 - let (*resume script of parpbl, transfer value of subpbl-script*)
4.94 - val ppp = par_pblobj pt (lev_up p);
4.95 - val thy' = get_obj g_domID pt ppp;
4.96 - val thy = Celem.assoc_thy thy';
4.97 - val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of
4.98 - (Selem.ScrState (E,l,a,_,_,b), ctxt') => (E, l, a, b, ctxt')
4.99 - | _ => error "nxt_solv Check_Postcond' script of parpbl: uncovered case get_loc"
4.100 - val ctxt'' = Stool.from_subpbl_to_caller ctxt scval ctxt'
4.101 - val tac_ = Tac.Check_Postcond' (pI, (scval, asm))
4.102 - val is = Selem.ScrState (E,l,a,scval,scsaf,b)
4.103 - val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
4.104 - in ([(Tac.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p, p_))) end
4.105 - end
4.106 - | nxt_solv (Tac.End_Proof'') _ ptp = ([], [], ptp)
4.107 - | nxt_solv tac_ is (pt, pos) =
4.108 - let
4.109 - val pos = case pos of
4.110 - (p, Met) => ((lev_on o lev_dn) p, Frm) (* begin script *)
4.111 - | (p, Res) => (lev_on p, Res) (* somewhere in script *)
4.112 - | _ => pos
4.113 - val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac") tac_ is pos pt;
4.114 - in
4.115 - ([(Lucin.tac_2tac tac_, tac_, (pos, is))], c, (pt, pos'))
4.116 - end
4.117 -(* find the next tac from the script, nxt_solv will update the ctree *)
4.118 -and nxt_solve_ (ptp as (pt, pos as (p, p_))) =
4.119 - if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)
4.120 - then ([], [], (pt, (p, p_)))
4.121 - else
4.122 - let
4.123 - val thy' = get_obj g_domID pt (par_pblobj pt p);
4.124 - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
4.125 - val (tac_, is, (t, _)) = LucinNEW.next_tac (thy', srls) (pt, pos) sc is;
4.126 - (* TODO here ^^^ return finished/helpless/ok !*)
4.127 - in case tac_ of
4.128 - Tac.End_Detail' _ => ([(Tac.End_Detail, Tac.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos))
4.129 - | _ => nxt_solv tac_ is ptp
4.130 - end;
4.131 -
4.132 (* says how may steps of a calculation should be done by "fun autocalc"
4.133 FIXXXME040624: does NOT match interfaces/ITOCalc.java
4.134 TODO.WN0512 redesign togehter with autocalc ? *)
4.135 @@ -376,7 +262,7 @@
4.136 val (_, c', ptp) = all_solve auto c ptp
4.137 in complete_solve auto (c @ c') ptp end
4.138 else
4.139 - case nxt_solve_ ptp of
4.140 + case LucinNEW.nxt_solve_ ptp of
4.141 ((Tac.Subproblem _, _, _) :: _, c', ptp') =>
4.142 if autoord auto < 5
4.143 then ("ok", c @ c', ptp)
4.144 @@ -398,7 +284,7 @@
4.145 let
4.146 val (_, _, mI) = get_obj g_spec pt p
4.147 val ctxt = get_ctxt pt pos
4.148 - val (_, c', ptp) = nxt_solv (Tac.Apply_Method' (mI, NONE, Selem.e_istate, ctxt)) (Selem.e_istate, ctxt) ptp
4.149 + val (_, c', ptp) = LucinNEW.nxt_solv (Tac.Apply_Method' (mI, NONE, Selem.e_istate, ctxt)) (Selem.e_istate, ctxt) ptp
4.150 in
4.151 complete_solve auto (c @ c') ptp
4.152 end;