1.1 --- a/src/Tools/isac/Interpret/solve.sml Thu Oct 27 10:48:24 2016 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve.sml Sat Nov 12 17:21:43 2016 +0100
1.3 @@ -134,8 +134,8 @@
1.4 "-----------------------------------------------------------------------";
1.5
1.6
1.7 -fun step2taci ((tac_, _, pt, p, _):step) = (*FIXXME.040312: redesign step*)
1.8 - (tac_2tac tac_, tac_, (p, get_loc pt p)):taci;
1.9 +fun step2taci ((tac_, _, pt, p, _) : Lucin.step) = (*FIXXME.040312: redesign step*)
1.10 + (Lucin.tac_2tac tac_, tac_, (p, get_loc pt p)):taci;
1.11
1.12
1.13 (*FIXME.WN050821 compare solve ... nxt_solv*)
1.14 @@ -147,8 +147,8 @@
1.15 val PblObj {meth=itms, ...} = get_obj I pt p;
1.16 val thy' = get_obj g_domID pt p;
1.17 val thy = assoc_thy thy';
1.18 - val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
1.19 - val ini = init_form thy sc env;
1.20 + val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = Lucin.init_scrstate thy itms mI;
1.21 + val ini = Lucin.init_form thy sc env;
1.22 val p = lev_dn p;
1.23 in
1.24 case ini of
1.25 @@ -161,16 +161,17 @@
1.26 end
1.27 | NONE => (*execute the first tac in the Script, compare solve m*)
1.28 let
1.29 - val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
1.30 + val (m', (is', ctxt'), _) = Lucin.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
1.31 val d = e_rls (*FIXME: get simplifier from domID*);
1.32 in
1.33 - case locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of
1.34 - Steps (is'', ss as (m'',f',pt',p',c')::_) =>
1.35 + case Lucin.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of
1.36 + Lucin.Steps (is'', ss as (m'',f',pt',p',c')::_) =>
1.37 ("ok", (map step2taci ss, c', (pt',p')))
1.38 | NotLocatable =>
1.39 - let val (p,ps,f,pt) =
1.40 - generate_hard (assoc_thy "Isac") m (p,Frm) pt;
1.41 - in ("not-found-in-script", ([(tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p))) end
1.42 + let val (p,ps,f,pt) = generate_hard (assoc_thy "Isac") m (p,Frm) pt;
1.43 + in
1.44 + ("not-found-in-script",([(Lucin.tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p)))
1.45 + end
1.46 end
1.47 end
1.48
1.49 @@ -195,7 +196,7 @@
1.50 val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
1.51 val thy' = get_obj g_domID pt pp;
1.52 val thy = assoc_thy thy';
1.53 - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
1.54 + val (_,_,(scval,scsaf)) = Lucin.next_tac (thy',srls) (pt,(p,p_)) sc loc;
1.55 in
1.56 if pp = []
1.57 then
1.58 @@ -233,8 +234,8 @@
1.59 val r = (fst o (get_obj g_result pt)) p'
1.60 (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
1.61 val thy' = get_obj g_domID pt pp
1.62 - val (srls, is, sc) = from_pblobj' thy' pr pt
1.63 - val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
1.64 + val (srls, is, sc) = Lucin.from_pblobj' thy' pr pt
1.65 + val (tac_,is',_) = Lucin.next_tac (thy',srls) (pt,pr) sc is
1.66 in ("ok", ([(End_Detail, End_Detail' t ,
1.67 ((p,p_), get_loc pt (p,p_)))], [], (pt,pr)))
1.68 end
1.69 @@ -253,11 +254,11 @@
1.70 else
1.71 let
1.72 val thy' = get_obj g_domID pt (par_pblobj pt p);
1.73 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
1.74 + val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
1.75 val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
1.76 in
1.77 - case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
1.78 - Steps (is', ss as (m',f',pt',p',c')::_) =>
1.79 + case Lucin.locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
1.80 + Lucin.Steps (is', ss as (m',f',pt',p',c')::_) =>
1.81 let
1.82 (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
1.83 in ("ok", (map step2taci ss, c', (pt',p'))) end
1.84 @@ -265,7 +266,7 @@
1.85 let val (p,ps,f,pt) =
1.86 generate_hard (assoc_thy "Isac") m (p,p_) pt;
1.87 in ("not-found-in-script",
1.88 - ([(tac_2tac m, m, (po,is))], ps, (pt,p)))
1.89 + ([(Lucin.tac_2tac m, m, (po,is))], ps, (pt,p)))
1.90 end
1.91 end;
1.92
1.93 @@ -278,8 +279,8 @@
1.94 val itms = if itms <> [] then itms else complete_metitms oris probl [] ppc
1.95 val thy' = get_obj g_domID pt p;
1.96 val thy = assoc_thy thy';
1.97 - val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = init_scrstate thy itms mI;
1.98 - val ini = init_form thy scr env;
1.99 + val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = Lucin.init_scrstate thy itms mI;
1.100 + val ini = Lucin.init_form thy scr env;
1.101 in
1.102 case ini of
1.103 SOME t =>
1.104 @@ -314,7 +315,7 @@
1.105 val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
1.106 val thy' = get_obj g_domID pt pp;
1.107 val thy = assoc_thy thy';
1.108 - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
1.109 + val (_,_,(scval,scsaf)) = Lucin.next_tac (thy',srls) (pt,(p,p_)) sc loc;
1.110 in
1.111 if pp = []
1.112 then
1.113 @@ -349,7 +350,7 @@
1.114 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
1.115 | _ => pos
1.116 val (pos',c,_,pt) = generate1 (assoc_thy "Isac") tac_ is pos pt;
1.117 - in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
1.118 + in ([(Lucin.tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
1.119
1.120 (* find the next tac from the script, nxt_solv will update the ptree *)
1.121 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
1.122 @@ -358,8 +359,8 @@
1.123 else
1.124 let
1.125 val thy' = get_obj g_domID pt (par_pblobj pt p);
1.126 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
1.127 - val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
1.128 + val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
1.129 + val (tac_,is,(t,_)) = Lucin.next_tac (thy',srls) (pt,pos) sc is;
1.130 (*TODO here ^^^ return finished/helpless/ok !*)
1.131 in case tac_ of
1.132 End_Detail' _ => ([(End_Detail, End_Detail' (t,[(*FIXME.040215*)]),