1.1 --- a/src/Tools/isac/Interpret/solve.sml Tue May 17 15:02:43 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve.sml Tue May 17 17:38:35 2011 +0200
1.3 @@ -143,45 +143,36 @@
1.4 val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
1.5 *)
1.6 fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ptree, (pos as (p,_))) =
1.7 - let val {srls, ...} = get_met mI;
1.8 - val PblObj {meth=itms, ...} = get_obj I pt p;
1.9 - val thy' = get_obj g_domID pt p;
1.10 - val thy = assoc_thy thy';
1.11 - val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
1.12 - val ini = init_form thy sc env;
1.13 - val p = lev_dn p;
1.14 - in
1.15 - case ini of
1.16 - SOME t => (* val SOME t = ini;
1.17 - *)
1.18 - let val (pos,c,_,pt) =
1.19 - generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
1.20 - (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
1.21 - in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
1.22 - ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate')
1.23 - end
1.24 - | NONE => (*execute the first tac in the Script, compare solve m*)
1.25 - let val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
1.26 - val d = e_rls (*FIXME: get simplifier from domID*);
1.27 - in
1.28 - case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt') of
1.29 - Steps (is'', ss as (m'',f',pt',p',c')::_) =>
1.30 -(* val Steps (is'', ss as (m'',f',pt',p',c')::_) =
1.31 - locate_gen (thy',srls) m' (pt,(p,Res)) (sc,d) is';
1.32 - *)
1.33 - ("ok", (map step2taci ss, c', (pt',p')))
1.34 - | NotLocatable =>
1.35 - let val (p,ps,f,pt) =
1.36 - generate_hard (assoc_thy "Isac") m (p,Frm) pt;
1.37 - in ("not-found-in-script",
1.38 - ([(tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p))) end
1.39 - (*just-before------------------------------------------------------
1.40 - ("ok",([(Apply_Method mI,Apply_Method'(mI,NONE,e_istate),
1.41 - (pos, is))],
1.42 - [], (update_env pt (fst pos) (SOME is),pos)))
1.43 - -----------------------------------------------------------------*)
1.44 - end
1.45 - end
1.46 + let val {srls, ...} = get_met mI;
1.47 + val PblObj {meth=itms, ctxt, ...} = get_obj I pt p;
1.48 + val thy' = get_obj g_domID pt p;
1.49 + val thy = assoc_thy thy';
1.50 + val (is as ScrState (env,_,_,_,_,_), _, sc) = init_scrstate thy itms mI;
1.51 + val ini = init_form thy sc env;
1.52 + val p = lev_dn p;
1.53 + in
1.54 + case ini of
1.55 + SOME t =>
1.56 + let val (pos,c,_,pt) =
1.57 + generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
1.58 + (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
1.59 + in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
1.60 + ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate')
1.61 + end
1.62 + | NONE => (*execute the first tac in the Script, compare solve m*)
1.63 + let
1.64 + val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
1.65 + val d = e_rls (*FIXME: get simplifier from domID*);
1.66 + in
1.67 + case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt') of
1.68 + Steps (is'', ss as (m'',f',pt',p',c')::_) =>
1.69 + ("ok", (map step2taci ss, c', (pt',p')))
1.70 + | NotLocatable =>
1.71 + let val (p,ps,f,pt) =
1.72 + generate_hard (assoc_thy "Isac") m (p,Frm) pt;
1.73 + in ("not-found-in-script", ([(tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p))) end
1.74 + end
1.75 + end
1.76
1.77 | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) =
1.78 let (*val _=tracing"###solve Free_Solve";*)
1.79 @@ -350,28 +341,16 @@
1.80 | nxt_solv (End_Proof'') _ ptp = ([], [], ptp)
1.81
1.82 | nxt_solv tac_ is (pt, pos as (p,p_)) =
1.83 -(* val (pt, pos as (p,p_)) = ptp;
1.84 - *)
1.85 - let val pos = case pos of
1.86 - (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
1.87 - | (p, Res) => (lev_on p,Res) (*somewhere in script*)
1.88 - | _ => pos (*somewhere in script*)
1.89 - (*val _= tracing"### nxt_solv4 Apply_Method: stored is =";
1.90 - val _= tracing(istate2str is);*)
1.91 - val (pos',c,_,pt) = generate1 (assoc_thy "Isac") tac_ is pos pt;
1.92 - in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
1.93 + let
1.94 + val pos =
1.95 + case pos of
1.96 + (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
1.97 + | (p, Res) => (lev_on p,Res) (*somewhere in script*)
1.98 + | _ => pos
1.99 + val (pos',c,_,pt) = generate1 (assoc_thy "Isac") tac_ is pos pt;
1.100 + in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
1.101
1.102 -
1.103 - (*(p,p_), (([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe, pt*)
1.104 -
1.105 -
1.106 -(*.find the next tac from the script, nxt_solv will update the ptree.*)
1.107 -(* val (ptp as (pt,pos as (p,p_))) = ptp';
1.108 - val (ptp as (pt, pos as (p,p_))) = ptp'';
1.109 - val (ptp as (pt, pos as (p,p_))) = ptp;
1.110 - val (ptp as (pt, pos as (p,p_))) = (pt,ip);
1.111 - val (ptp as (pt, pos as (p,p_))) = (pt, pos);
1.112 - *)
1.113 +(* find the next tac from the script, nxt_solv will update the ptree *)
1.114 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
1.115 if e_metID = get_obj g_metID pt (par_pblobj pt p)
1.116 then ([], [], (pt,(p,p_))):calcstate'