1.1 --- a/src/Tools/isac/Frontend/interface.sml Wed Dec 21 08:57:47 2016 +0100
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Wed Dec 21 09:21:26 2016 +0100
1.3 @@ -12,7 +12,7 @@
1.4 signature KERNEL =
1.5 sig
1.6 val appendFormula : calcID -> cterm' -> XML.tree (*unit future*)
1.7 - val autoCalculate : calcID -> auto -> XML.tree (*unit future*)
1.8 + val autoCalculate : calcID -> Solve.auto -> XML.tree (*unit future*)
1.9 val applyTactic : calcID -> pos' -> tac -> XML.tree
1.10 val CalcTree : fmz list -> XML.tree
1.11 val checkContext : calcID -> pos' -> guh -> XML.tree
2.1 --- a/src/Tools/isac/Interpret/inform.sml Wed Dec 21 08:57:47 2016 +0100
2.2 +++ b/src/Tools/isac/Interpret/inform.sml Wed Dec 21 09:21:26 2016 +0100
2.3 @@ -396,14 +396,14 @@
2.4 then ("no derivation found", (tacis, c, ptp): Chead.calcstate')
2.5 else
2.6 let
2.7 - val cs' as (tacis, c', ptp) = nxt_solve_ ptp; (*<---------------------*)
2.8 + val cs' as (tacis, c', ptp) = Solve.nxt_solve_ ptp; (*<---------------------*)
2.9 val (tacis, c'', ptp) = case tacis of
2.10 ((Subproblem _, _, _)::_) =>
2.11 let
2.12 val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)
2.13 val mI = get_obj g_metID pt p
2.14 in
2.15 - nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
2.16 + Solve.nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
2.17 end
2.18 | _ => cs';
2.19 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
3.1 --- a/src/Tools/isac/Interpret/mathengine.sml Wed Dec 21 08:57:47 2016 +0100
3.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed Dec 21 09:21:26 2016 +0100
3.3 @@ -9,9 +9,9 @@
3.4 signature MATH_ENGINE =
3.5 sig
3.6 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
3.7 - val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Generate.mout * tac'_ * safe * ptree
3.8 + val me : Solve.tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Generate.mout * Solve.tac'_ * safe * ptree
3.9 val autocalc :
3.10 - pos' list -> pos' -> (ptree * pos') * Generate.taci list -> auto -> string * pos' list * (ptree * pos')
3.11 + pos' list -> pos' -> (ptree * pos') * Generate.taci list -> Solve.auto -> string * pos' list * (ptree * pos')
3.12 val locatetac :
3.13 tac -> ptree * (posel list * pos_) -> string * (Generate.taci list * pos' list * (ptree * pos'))
3.14 val step : pos' -> Chead.calcstate -> string * Chead.calcstate'
3.15 @@ -68,7 +68,7 @@
3.16 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
3.17 fun loc_solve_ m (pt, pos) =
3.18 let
3.19 - val (msg, cs') = solve m (pt, pos);
3.20 + val (msg, cs') = Solve.solve m (pt, pos);
3.21 in
3.22 case msg of "ok" => Updated cs' | msg => ERror msg
3.23 end
3.24 @@ -82,13 +82,13 @@
3.25 fun locatetac _ (ptp as (_, ([], Res))) = ("end-of-calculation", ([], [], ptp))
3.26 | locatetac tac (ptp as (pt, p)) =
3.27 let
3.28 - val (mI, m) = mk_tac'_ tac;
3.29 + val (mI, m) = Solve.mk_tac'_ tac;
3.30 in
3.31 case Applicable.applicable_in p pt m of
3.32 Chead.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
3.33 | Chead.Appl m =>
3.34 let
3.35 - val x = if member op = specsteps mI
3.36 + val x = if member op = Solve.specsteps mI
3.37 then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
3.38 in
3.39 case x of
3.40 @@ -129,7 +129,7 @@
3.41 in
3.42 case tac of
3.43 Apply_Method mI =>
3.44 - nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
3.45 + Solve.nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
3.46 | _ => Chead.nxt_specif tac ptp
3.47 end
3.48 end
3.49 @@ -198,7 +198,7 @@
3.50 let val (pt',c',p') = Generate.generate tacis (pt,[],p)
3.51 in ("ok", (tacis, c', (pt', p'))) end
3.52 else (case (if member op = [Pbl, Met] p_
3.53 - then nxt_specify_ (pt, ip) else nxt_solve_ (pt, ip))
3.54 + then nxt_specify_ (pt, ip) else Solve.nxt_solve_ (pt, ip))
3.55 handle ERROR msg => (writeln ("*** " ^ msg);
3.56 ([], [], ptp)) (*e.g. Add_Given "equality///"*) of
3.57 cs as ([],_,_) => ("helpless", cs)
3.58 @@ -208,7 +208,7 @@
3.59 | SOME _ => (*vvvvvv: Apply_Method without init_form*)
3.60 (case if member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p))
3.61 then nxt_specify_ (pt, ip)
3.62 - else (nxt_solve_ (pt,ip))
3.63 + else (Solve.nxt_solve_ (pt,ip))
3.64 handle ERROR msg => (writeln ("*** " ^ msg);
3.65 ([],[],ptp)) (*e.g. Add_Given "equality///"*) of
3.66 cs as ([],_,_) =>("helpless", cs) (*FIXXME del.handle*)
3.67 @@ -221,7 +221,7 @@
3.68 TODO.WN0512 ? redesign after the phases have been more separated
3.69 at the fron-end in 05:
3.70 eg. CompleteCalcHead could be done by a separate fun !!!*)
3.71 -fun autocalc c ip cs (Step s) =
3.72 +fun autocalc c ip cs (Solve.Step s) =
3.73 if s <= 1
3.74 then
3.75 let val (str, (_, c', ptp)) = step ip cs; (* autoord = 1, probably does 1 step too much*)
3.76 @@ -230,14 +230,14 @@
3.77 let val (str, (_, c', ptp as (_, p))) = step ip cs;
3.78 in
3.79 if str = "ok"
3.80 - then autocalc (c@c') p (ptp, []) (Step (s - 1))
3.81 + then autocalc (c@c') p (ptp, []) (Solve.Step (s - 1))
3.82 else (str, c@c', ptp) end
3.83 (* handles autoord <= 3, autoord > 3 handled by all_solve, complete_solve *)
3.84 | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
3.85 - if autoord auto > 3 andalso just_created (pt, pos)
3.86 + if Solve.autoord auto > 3 andalso just_created (pt, pos)
3.87 then
3.88 let val ptp = Chead.all_modspec (pt, pos);
3.89 - in all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
3.90 + in Solve.all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
3.91 else
3.92 if member op = [Pbl, Met] p_
3.93 then
3.94 @@ -245,26 +245,26 @@
3.95 then
3.96 let val ptp = Chead.complete_mod (pt, pos) (*... auto = 2 | 3 *)
3.97 in
3.98 - if autoord auto < 3 then ("ok", c, ptp)
3.99 + if Solve.autoord auto < 3 then ("ok", c, ptp)
3.100 else
3.101 if not (Chead.is_complete_spec ptp)
3.102 then
3.103 let val ptp = Chead.complete_spec ptp
3.104 in
3.105 - if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
3.106 + if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
3.107 end
3.108 - else if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
3.109 + else if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
3.110 end
3.111 else
3.112 if not (Chead.is_complete_spec (pt,pos))
3.113 then
3.114 let val ptp = Chead.complete_spec (pt, pos)
3.115 in
3.116 - if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
3.117 + if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
3.118 end
3.119 else
3.120 - if autoord auto = 3 then ("ok", c, (pt, pos)) else all_solve auto c (pt, pos)
3.121 - else complete_solve auto c (pt, pos);
3.122 + if Solve.autoord auto = 3 then ("ok", c, (pt, pos)) else Solve.all_solve auto c (pt, pos)
3.123 + else Solve.complete_solve auto c (pt, pos);
3.124
3.125 (*.initialiye matching; before 'tryMatch' get the pblID to match with:
3.126 if no pbl has been specified, take the init from origin.*)
3.127 @@ -351,7 +351,7 @@
3.128 if null cn
3.129 then
3.130 if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
3.131 - then detailrls pt pos
3.132 + then Solve.detailrls pt pos
3.133 else ("no-Rewrite_Set...", EmptyPtree, e_pos')
3.134 else ("donesteps", pt, (p @ [length (children (get_nd pt p))], Res))
3.135 end;
3.136 @@ -418,7 +418,7 @@
3.137 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
3.138 | _ => if p = ([], Res) then End_Proof' else Empty_Tac;
3.139 in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
3.140 - (tac2IDstr tac, tac):tac'_, Sundef, pt)
3.141 + (tac2IDstr tac, tac): Solve.tac'_, Sundef, pt)
3.142 end
3.143
3.144 (* for quick test-print-out, until 'type inout' is removed *)
4.1 --- a/src/Tools/isac/Interpret/solve.sml Wed Dec 21 08:57:47 2016 +0100
4.2 +++ b/src/Tools/isac/Interpret/solve.sml Wed Dec 21 09:21:26 2016 +0100
4.3 @@ -5,6 +5,10 @@
4.4 10 20 30 40 50 60 70 80 90 100
4.5 *)
4.6
4.7 +structure Solve =
4.8 +struct
4.9 +(*open Ctree;*)
4.10 +
4.11 fun safe (ScrState (_,_,_,_,s,_)) = s
4.12 | safe (RrlsState _) = Safe;
4.13
4.14 @@ -73,7 +77,6 @@
4.15
4.16 | Empty_Tac => ("Empty_Tac",Empty_Tac)
4.17 | Tac string => ("Tac",Tac string)
4.18 -| User => ("User",User)
4.19 | End_Proof' => ("End_Proof'",End_Proof');
4.20
4.21 (*Detail*)
4.22 @@ -131,7 +134,6 @@
4.23 "Add_Relation","Del_Relation",
4.24 "Specify_Theory","Specify_Problem","Specify_Method"];
4.25
4.26 -"-----------------------------------------------------------------------";
4.27
4.28
4.29 fun step2taci ((tac_, _, pt, p, _) : Lucin.step) = (*FIXXME.040312: redesign step*)
4.30 @@ -479,3 +481,4 @@
4.31 else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_))
4.32 in (*f*) Generate.EmptyMout end;
4.33
4.34 +end
4.35 \ No newline at end of file
5.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Wed Dec 21 08:57:47 2016 +0100
5.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Wed Dec 21 09:21:26 2016 +0100
5.3 @@ -325,7 +325,7 @@
5.4 fun xml_to_pos (XML.Elem (("POSITION", []), [is, pp])) = (xml_to_ints is, xml_to_pos_ pp) (*: pos'*)
5.5 | xml_to_pos tree = raise ERROR ("xml_to_pos: wrong XML.tree \n" ^ xmlstr 0 tree)
5.6
5.7 -fun xml_of_auto (Step i) =
5.8 +fun xml_of_auto (Solve.Step i) =
5.9 XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text (string_of_int i)])
5.10 | xml_of_auto CompleteModel = XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])
5.11 | xml_of_auto CompleteCalcHead = XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])
5.12 @@ -333,12 +333,12 @@
5.13 | xml_of_auto CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])
5.14 | xml_of_auto CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])
5.15 fun xml_to_auto (XML.Elem (("AUTO", []), [
5.16 - XML.Elem (("STEP", []), [XML.Text i])])) = Step (int_of_str i |> the)
5.17 - | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])) = CompleteModel
5.18 - | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])) = CompleteCalcHead
5.19 - | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])) = CompleteToSubpbl
5.20 - | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])) = CompleteSubpbl
5.21 - | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])) = CompleteCalc
5.22 + XML.Elem (("STEP", []), [XML.Text i])])) = Solve.Step (int_of_str i |> the)
5.23 + | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])) = Solve.CompleteModel
5.24 + | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])) = Solve.CompleteCalcHead
5.25 + | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])) = Solve.CompleteToSubpbl
5.26 + | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])) = Solve.CompleteSubpbl
5.27 + | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])) = Solve.CompleteCalc
5.28 | xml_to_auto tree = raise ERROR ("xml_to_auto: wrong XML.tree \n" ^ xmlstr 0 tree)
5.29
5.30 fun filterpbl str =
6.1 --- a/test/Tools/isac/Test_Isac.thy Wed Dec 21 08:57:47 2016 +0100
6.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Dec 21 09:21:26 2016 +0100
6.3 @@ -78,7 +78,8 @@
6.4 open Generate; (*NONE*)
6.5 (*open Ctree; (*? ?*) *)
6.6 open Specify; show_ptyps;
6.7 - open Applicable (*TODO*)
6.8 + open Applicable; (*TODO*)
6.9 + open Solve; (*TODO*)
6.10 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.11 *}
6.12 ML {*
7.1 --- a/test/Tools/isac/Test_Some.thy Wed Dec 21 08:57:47 2016 +0100
7.2 +++ b/test/Tools/isac/Test_Some.thy Wed Dec 21 09:21:26 2016 +0100
7.3 @@ -9,9 +9,11 @@
7.4 open Inform; cas_input;
7.5 open Rtools; trtas2str;
7.6 open Chead; pt_extract;
7.7 - open Ctree; (*//*)
7.8 + open Generate; (*NONE*)
7.9 +(*open Ctree; (*? ?*) *)
7.10 open Specify; show_ptyps;
7.11 - open Applicable. (*TODO*)
7.12 + open Applicable; (*TODO*)
7.13 + open Solve; (*TODO*)
7.14 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.15 *}
7.16 ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"