1.1 --- a/src/Tools/isac/Interpret/solve.sml Tue Mar 13 15:04:27 2018 +0100
1.2 +++ b/src/Tools/isac/Interpret/solve.sml Thu Mar 15 10:17:44 2018 +0100
1.3 @@ -121,7 +121,7 @@
1.4 PblObj {meth=itms, ...} => itms
1.5 | _ => error "solve Apply_Method: uncovered case get_obj"
1.6 val thy' = get_obj g_domID pt p;
1.7 - val thy = assoc_thy thy';
1.8 + val thy = Celem.assoc_thy thy';
1.9 val (is, env, ctxt, sc) = case Lucin.init_scrstate thy itms mI of
1.10 (is as Selem.ScrState (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
1.11 | _ => error "solve Apply_Method: uncovered case init_scrstate"
1.12 @@ -139,13 +139,13 @@
1.13 | NONE => (*execute the first tac in the Script, compare solve m*)
1.14 let
1.15 val (m', (is', ctxt'), _) = Lucin.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
1.16 - val d = e_rls (*FIXME: get simplifier from domID*);
1.17 + val d = Celem.e_rls (*FIXME: get simplifier from domID*);
1.18 in
1.19 case Lucin.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of
1.20 Lucin.Steps (_, ss as (_, _, pt', p', c') :: _) =>
1.21 ("ok", (map step2taci ss, c', (pt', p')))
1.22 | _ => (* NotLocatable *)
1.23 - let val (p, ps, _, pt) = Generate.generate_hard (assoc_thy "Isac") m (p, Frm) pt;
1.24 + let val (p, ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac") m (p, Frm) pt;
1.25 in
1.26 ("not-found-in-script",([(Lucin.tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt, p)))
1.27 end
1.28 @@ -154,7 +154,7 @@
1.29 | solve ("Free_Solve", Tac.Free_Solve') (pt, po as (p, _)) =
1.30 let
1.31 val p' = lev_dn_ (p, Res);
1.32 - val pt = update_metID pt (par_pblobj pt p) e_metID;
1.33 + val pt = update_metID pt (par_pblobj pt p) Celem.e_metID;
1.34 in
1.35 ("ok", ([(Tac.Empty_Tac, Tac.Empty_Tac_, (po, (Selem.Uistate, Selem.e_ctxt)))], [], (pt,p')))
1.36 end
1.37 @@ -173,7 +173,7 @@
1.38 loc as (Selem.ScrState (E, l, a, _, _, b), ctxt) => (loc, E, l, a, b, ctxt)
1.39 | _ => error "solve Check_Postcond: uncovered case get_loc"
1.40 val thy' = get_obj g_domID pt pp;
1.41 - val thy = assoc_thy thy';
1.42 + val thy = Celem.assoc_thy thy';
1.43 val (_, _, (scval, scsaf)) = Lucin.next_tac (thy', srls) (pt, (p, p_)) sc loc;
1.44 in
1.45 if pp = []
1.46 @@ -187,7 +187,7 @@
1.47 let (*resume script of parpbl, transfer value of subpbl-script*)
1.48 val ppp = par_pblobj pt (lev_up p);
1.49 val thy' = get_obj g_domID pt ppp;
1.50 - val thy = assoc_thy thy';
1.51 + val thy = Celem.assoc_thy thy';
1.52 val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of
1.53 (Selem.ScrState (E, l, a, _, _, b), ctxt') => (E, l, a, b, ctxt')
1.54 | _ => error "solve Check_Postcond resume script of parpbl: uncovered case get_loc"
1.55 @@ -206,11 +206,11 @@
1.56 ("ok", ([(Tac.End_Detail, Tac.End_Detail' t , ((p, p_), get_loc pt (p, p_)))], [], (pt, pr)))
1.57 end
1.58 | solve (_, m) (pt, po as (p, p_)) =
1.59 - if e_metID = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
1.60 + if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
1.61 then
1.62 let
1.63 val ctxt = get_ctxt pt po
1.64 - val ((p,p_),ps,_,pt) = Generate.generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
1.65 + val ((p,p_),ps,_,pt) = Generate.generate1 (Celem.assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
1.66 m (Selem.e_istate, ctxt) (p, p_) pt;
1.67 in ("no-method-specified", (*Free_Solve*)
1.68 ([(Tac.Empty_Tac, Tac.Empty_Tac_, ((p, p_), (Selem.Uistate, ctxt)))], ps, (pt, (p, p_))))
1.69 @@ -219,7 +219,7 @@
1.70 let
1.71 val thy' = get_obj g_domID pt (par_pblobj pt p);
1.72 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
1.73 - val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
1.74 + val d = Celem.e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
1.75 in
1.76 case Lucin.locate_gen (thy',srls) m (pt,(p, p_)) (sc,d) is of
1.77 Lucin.Steps (_, ss as (_, _, pt', p', c') :: _) =>
1.78 @@ -227,7 +227,7 @@
1.79 (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
1.80 | _ => (* NotLocatable *)
1.81 let
1.82 - val (p,ps, _, pt) = Generate.generate_hard (assoc_thy "Isac") m (p, p_) pt;
1.83 + val (p,ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac") m (p, p_) pt;
1.84 in
1.85 ("not-found-in-script", ([(Lucin.tac_2tac m, m, (po, is))], ps, (pt, p)))
1.86 end
1.87 @@ -243,7 +243,7 @@
1.88 | _ => error "nxt_solv Apply_Method': uncovered case get_obj"
1.89 val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
1.90 val thy' = get_obj g_domID pt p;
1.91 - val thy = assoc_thy thy';
1.92 + val thy = Celem.assoc_thy thy';
1.93 val (is, env, ctxt, scr) = case Lucin.init_scrstate thy itms mI of
1.94 (is as Selem.ScrState (env,_,_,_,_,_), ctxt, scr) => (is, env, ctxt, scr)
1.95 | _ => error "nxt_solv Apply_Method': uncovered case init_scrstate"
1.96 @@ -279,7 +279,7 @@
1.97 loc as (Selem.ScrState (E,l,a,_,_,b), ctxt) => (loc, E, l, a, b, ctxt)
1.98 | _ => error "nxt_solv Check_Postcond': uncovered case get_loc"
1.99 val thy' = get_obj g_domID pt pp;
1.100 - val thy = assoc_thy thy';
1.101 + val thy = Celem.assoc_thy thy';
1.102 val (_, _, (scval, scsaf)) = Lucin.next_tac (thy', srls) (pt, (p, p_)) sc loc;
1.103 in
1.104 if pp = []
1.105 @@ -293,7 +293,7 @@
1.106 let (*resume script of parpbl, transfer value of subpbl-script*)
1.107 val ppp = par_pblobj pt (lev_up p);
1.108 val thy' = get_obj g_domID pt ppp;
1.109 - val thy = assoc_thy thy';
1.110 + val thy = Celem.assoc_thy thy';
1.111 val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of
1.112 (Selem.ScrState (E,l,a,_,_,b), ctxt') => (E, l, a, b, ctxt')
1.113 | _ => error "nxt_solv Check_Postcond' script of parpbl: uncovered case get_loc"
1.114 @@ -310,13 +310,13 @@
1.115 (p, Met) => ((lev_on o lev_dn) p, Frm) (* begin script *)
1.116 | (p, Res) => (lev_on p, Res) (* somewhere in script *)
1.117 | _ => pos
1.118 - val (pos', c, _, pt) = Generate.generate1 (assoc_thy "Isac") tac_ is pos pt;
1.119 + val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac") tac_ is pos pt;
1.120 in
1.121 ([(Lucin.tac_2tac tac_, tac_, (pos, is))], c, (pt, pos'))
1.122 end
1.123 (* find the next tac from the script, nxt_solv will update the ctree *)
1.124 and nxt_solve_ (ptp as (pt, pos as (p, p_))) =
1.125 - if e_metID = get_obj g_metID pt (par_pblobj pt p)
1.126 + if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)
1.127 then ([], [], (pt, (p, p_)))
1.128 else
1.129 let
1.130 @@ -403,7 +403,7 @@
1.131 val ctxt = get_ctxt pt pos
1.132 in
1.133 case rls of
1.134 - Rrls {scr = Rfuns {init_state,...},...} =>
1.135 + Celem.Rrls {scr = Celem.Rfuns {init_state,...},...} =>
1.136 let
1.137 val (_, _, _, rul_terms) = init_state t
1.138 val newnds = rul_terms_2nds (Proof_Context.theory_of ctxt) [] t rul_terms
1.139 @@ -414,9 +414,9 @@
1.140 val is = Generate.init_istate tac t
1.141 (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
1.142 is wrong for simpl, but working ?!? *)
1.143 - val tac_ = Tac.Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
1.144 + val tac_ = Tac.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
1.145 val pos' = ((lev_on o lev_dn) p, Frm)
1.146 - val thy = assoc_thy "Isac"
1.147 + val thy = Celem.assoc_thy "Isac"
1.148 val (_, _, _, pt') = Generate.generate1 thy tac_ (is, ctxt) pos' pt (* implicit Take *)
1.149 val (_,_, (pt'', _)) = complete_solve CompleteSubpbl [] (pt', pos')
1.150 val newnds = children (get_nd pt'' p)