1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Fri Mar 20 19:31:55 2020 +0100
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Mon Mar 23 13:31:29 2020 +0100
1.3 @@ -279,7 +279,7 @@
1.4 "may have intermediate steps above them")
1.5 else
1.6 let val ip' = lev_pred' pt ip
1.7 - in case Math_Engine.detailstep pt ip of
1.8 + in case Detail_Step.go pt ip of
1.9 ("detailrls", pt, lastpos) =>
1.10 (upd_calc cI ((pt, p), tacis); interStepsOK cI ip' ip' lastpos)
1.11 | ("no-Rewrite_Set...", _, _) => sysERROR2xml cI "no Rewrite_Set..."
2.1 --- a/src/Tools/isac/Build_Isac.thy Fri Mar 20 19:31:55 2020 +0100
2.2 +++ b/src/Tools/isac/Build_Isac.thy Mon Mar 23 13:31:29 2020 +0100
2.3 @@ -73,8 +73,10 @@
2.4 *) "Interpret/Interpret"
2.5 (*
2.6 theory MathEngine imports "~~/src/Tools/isac/Interpret/Interpret"
2.7 + ML_file "fetch-tactics.sml"
2.8 ML_file solve.sml
2.9 ML_file step.sml
2.10 + ML_file "detail-step.sml"
2.11 ML_file "mathengine-stateless.sml"
2.12 ML_file messages.sml
2.13 ML_file states.sml
3.1 --- a/src/Tools/isac/Interpret/li-tool.sml Fri Mar 20 19:31:55 2020 +0100
3.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Mon Mar 23 13:31:29 2020 +0100
3.3 @@ -349,7 +349,7 @@
3.4 (* decide, where to get program/istate/ctxt from:
3.5 (* 1 *) from PblObj: at begin of program if no init_form
3.6 (* 2 *) from PblObj/PrfObj: if Prog_Tac is in the middle of the program
3.7 - (* 3 *) from PrfOb: in case of Math_Engine.detailstep
3.8 + (* 3 *) from PrfOb: in case of Detail_Step.go
3.9 *)
3.10 fun resume_prog thy (p, p_) pt =
3.11 if Pos.on_specification p_
4.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Fri Mar 20 19:31:55 2020 +0100
4.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Mar 23 13:31:29 2020 +0100
4.3 @@ -1,9 +1,6 @@
4.4 (* Title: Interpret/lucas-interpreter.sml
4.5 Author: Walther Neuper 2019
4.6 (c) due to copyright terms
4.7 -
4.8 -latex paper:
4.9 -/usr/local/isabisac//bin/isabelle build -D .
4.10 *)
4.11
4.12 signature LUCAS_INTERPRETER =
5.1 --- a/src/Tools/isac/MathEngine/MathEngine.thy Fri Mar 20 19:31:55 2020 +0100
5.2 +++ b/src/Tools/isac/MathEngine/MathEngine.thy Mon Mar 23 13:31:29 2020 +0100
5.3 @@ -9,6 +9,7 @@
5.4 ML_file "fetch-tactics.sml"
5.5 ML_file solve.sml
5.6 ML_file step.sml
5.7 + ML_file "detail-step.sml"
5.8 ML_file "mathengine-stateless.sml"
5.9 ML_file messages.sml
5.10 ML_file states.sml
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Tools/isac/MathEngine/detail-step.sml Mon Mar 23 13:31:29 2020 +0100
6.3 @@ -0,0 +1,68 @@
6.4 +(* Title: MathEngine/detail-step.sml
6.5 + Author: Walther Neuper 2020
6.6 + (c) due to copyright terms
6.7 +
6.8 +Within one step go into detailed steps on request by the user
6.9 +*)
6.10 +
6.11 +signature DETAIL_STEP =
6.12 +sig
6.13 + val go : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
6.14 + val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
6.15 +end
6.16 +
6.17 +(**)
6.18 +structure Detail_Step(**): DETAIL_STEP(**) =
6.19 +struct
6.20 +(**)
6.21 +open Ctree;
6.22 +open Pos
6.23 +
6.24 +(* aux.fun for detailrls with Rrls, reverse rewriting *)
6.25 +fun rul_terms_2nds _ nds _ [] = nds
6.26 + | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =
6.27 + (append_atomic [] (NONE(*guessed*), (Istate.e_istate, ContextC.e_ctxt)) t (Tactic.rule2tac thy [] rule) res Complete EmptyPtree) ::
6.28 + (rul_terms_2nds thy nds t' rts);
6.29 +
6.30 +(* detail steps done internally by Rewrite_Set* into Ctree
6.31 + by use of a program *)
6.32 +fun detailrls pt (pos as (p, _)) =
6.33 + let
6.34 + val t = get_obj g_form pt p
6.35 + val tac = get_obj g_tac pt p
6.36 + val rls = (assoc_rls o Tactic.rls_of) tac
6.37 + val ctxt = get_ctxt pt pos
6.38 + in
6.39 + case rls of
6.40 + Rule.Rrls {scr = Rule.Rfuns {init_state, ...}, ...} =>
6.41 + let
6.42 + val (_, _, _, rul_terms) = init_state t
6.43 + val newnds = rul_terms_2nds (Proof_Context.theory_of ctxt) [] t rul_terms
6.44 + val pt''' = ins_chn newnds pt p
6.45 + in ("detailrls", pt''', (p @ [length newnds], Res)) end
6.46 + | _ =>
6.47 + let
6.48 + val is = Generate.init_istate tac t
6.49 + val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
6.50 + val pos' = ((lev_on o lev_dn) p, Frm)
6.51 + val (_, _, _, pt') = Generate.generate1 tac_ (is, ctxt) (pt, pos') (* implicit Take *)
6.52 + val (_,_, (pt'', _)) = Solve.complete_solve Solve.CompleteSubpbl [] (pt', pos')
6.53 + val newnds = children (get_nd pt'' p)
6.54 + val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*)
6.55 + in ("detailrls", pt''', (p @ [length newnds], Res)) end
6.56 + end;
6.57 +
6.58 +fun go pt (pos as (p, _)) =
6.59 + let
6.60 + val nd = Ctree.get_nd pt p
6.61 + val cn = Ctree.children nd
6.62 + in
6.63 + if null cn
6.64 + then
6.65 + if (Tactic.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)]
6.66 + then detailrls pt pos
6.67 + else ("no-Rewrite_Set...", Ctree.EmptyPtree, Pos.e_pos')
6.68 + else ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Pos.Res))
6.69 + end;
6.70 +
6.71 +end
7.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Fri Mar 20 19:31:55 2020 +0100
7.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon Mar 23 13:31:29 2020 +0100
7.3 @@ -9,7 +9,6 @@
7.4 sig
7.5 val autocalc : Ctree.pos' list -> Ctree.pos' -> (Calc.T) * Generate.taci list ->
7.6 Solve.auto -> string * Ctree.pos' list * (Calc.T)
7.7 - val detailstep : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
7.8
7.9 val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list
7.10 val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * Model.itm list * (bool * term) list
7.11 @@ -212,17 +211,4 @@
7.12 | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre)
7.13 end
7.14
7.15 -fun detailstep pt (pos as (p, _)) =
7.16 - let
7.17 - val nd = Ctree.get_nd pt p
7.18 - val cn = Ctree.children nd
7.19 - in
7.20 - if null cn
7.21 - then
7.22 - if (Tactic.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)]
7.23 - then Solve.detailrls pt pos
7.24 - else ("no-Rewrite_Set...", Ctree.EmptyPtree, Pos.e_pos')
7.25 - else ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Pos.Res))
7.26 - end;
7.27 -
7.28 (**)end(**)
8.1 --- a/src/Tools/isac/MathEngine/solve.sml Fri Mar 20 19:31:55 2020 +0100
8.2 +++ b/src/Tools/isac/MathEngine/solve.sml Mon Mar 23 13:31:29 2020 +0100
8.3 @@ -14,7 +14,6 @@
8.4 val complete_solve :
8.5 auto -> Ctree.pos' list -> Calc.T -> string * Ctree.pos' list * Calc.T
8.6
8.7 - val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
8.8 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.9 (*NONE*)
8.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.11 @@ -93,39 +92,4 @@
8.12 complete_solve auto (c @ c') ptp
8.13 end;
8.14
8.15 -(* aux.fun for detailrls with Rrls, reverse rewriting *)
8.16 -fun rul_terms_2nds _ nds _ [] = nds
8.17 - | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =
8.18 - (append_atomic [] (NONE(*guessed*), (Istate.e_istate, ContextC.e_ctxt)) t (Tactic.rule2tac thy [] rule) res Complete EmptyPtree) ::
8.19 - (rul_terms_2nds thy nds t' rts);
8.20 -
8.21 -(* detail steps done internally by Rewrite_Set* into Ctree
8.22 - by use of a program *)
8.23 -fun detailrls pt (pos as (p, _)) =
8.24 - let
8.25 - val t = get_obj g_form pt p
8.26 - val tac = get_obj g_tac pt p
8.27 - val rls = (assoc_rls o Tactic.rls_of) tac
8.28 - val ctxt = get_ctxt pt pos
8.29 - in
8.30 - case rls of
8.31 - Rule.Rrls {scr = Rule.Rfuns {init_state, ...}, ...} =>
8.32 - let
8.33 - val (_, _, _, rul_terms) = init_state t
8.34 - val newnds = rul_terms_2nds (Proof_Context.theory_of ctxt) [] t rul_terms
8.35 - val pt''' = ins_chn newnds pt p
8.36 - in ("detailrls", pt''', (p @ [length newnds], Res)) end
8.37 - | _ =>
8.38 - let
8.39 - val is = Generate.init_istate tac t
8.40 - val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
8.41 - val pos' = ((lev_on o lev_dn) p, Frm)
8.42 - val thy = Celem.assoc_thy "Isac_Knowledge"
8.43 - val (_, _, _, pt') = Generate.generate1 tac_ (is, ctxt) (pt, pos') (* implicit Take *)
8.44 - val (_,_, (pt'', _)) = complete_solve CompleteSubpbl [] (pt', pos')
8.45 - val newnds = children (get_nd pt'' p)
8.46 - val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*)
8.47 - in ("detailrls", pt''', (p @ [length newnds], Res)) end
8.48 - end;
8.49 -
8.50 end
8.51 \ No newline at end of file
9.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Fri Mar 20 19:31:55 2020 +0100
9.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Mon Mar 23 13:31:29 2020 +0100
9.3 @@ -228,7 +228,7 @@
9.4 | prep_rls _ (Rule.Rrls {id, ...}) =
9.5 error ("prep_rls: not required for Rrls \"" ^ id ^ "\"");
9.6
9.7 -(* on the fly generate a Prog from an rls for Math_Engine.detailstep.
9.8 +(* on the fly generate a Prog from an rls for Detail_Step.go.
9.9 Types are not precise, but these are not required by LI.
9.10 Argument "thy" is only required for lookup in KEStore.
9.11 *)
10.1 --- a/test/Tools/isac/Knowledge/poly.sml Fri Mar 20 19:31:55 2020 +0100
10.2 +++ b/test/Tools/isac/Knowledge/poly.sml Mon Mar 23 13:31:29 2020 +0100
10.3 @@ -652,12 +652,12 @@
10.4 autoCalculate 1 CompleteCalc;
10.5 val ((pt,p),_) = get_calc 1; show_pt pt;
10.6
10.7 -interSteps 1 ([1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
10.8 +interSteps 1 ([1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
10.9 val ((pt,p),_) = get_calc 1; show_pt pt;
10.10 if existpt' ([1,1], Frm) pt then ()
10.11 else error "poly.sml: interSteps doesnt work again 1";
10.12
10.13 -interSteps 1 ([1,1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
10.14 +interSteps 1 ([1,1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
10.15 val ((pt,p),_) = get_calc 1; show_pt pt;
10.16 (*============ inhibit exn WN120316 ==============================================
10.17 if existpt' ([1,1,1], Frm) pt then ()
11.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Fri Mar 20 19:31:55 2020 +0100
11.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Mar 23 13:31:29 2020 +0100
11.3 @@ -433,7 +433,7 @@
11.4 val ((pt,p), tacis) = get_calc cI;
11.5 (not o is_interpos) ip = false;
11.6 val ip' = lev_pred' pt ip;
11.7 -"~~~~~ fun detailstep, args:"; val (pt, (pos as (p,p_):pos')) = (pt, ip);
11.8 +"~~~~~ fun go, args:"; val (pt, (pos as (p,p_):pos')) = (pt, ip);
11.9 (* ^^^^^^^^^ not in test/../ *)
11.10 val nd = get_nd pt p
11.11 val cn = children nd;
12.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Fri Mar 20 19:31:55 2020 +0100
12.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon Mar 23 13:31:29 2020 +0100
12.3 @@ -65,12 +65,12 @@
12.4
12.5 (*+*)show_pt pt; (* 11 lines, as produced by autoCalculate CompleteCalc *)
12.6
12.7 -val ("detailrls", pt''''', _) = (*case*) Math_Engine.detailstep pt ip (*of*);
12.8 +val ("detailrls", pt''''', _) = (*case*) Detail_Step.go pt ip (*of*);
12.9
12.10 (*+*)show_pt pt'''''; (* added [2,1]..[2,6] after ([1], Res)*)
12.11
12.12 (*//-------------------------- 1. go down along calls to error ------------------------------\\*)
12.13 -"~~~~~ fun detailstep , args:"; val (pt, (pos as (p, _))) = (pt, ip);
12.14 +"~~~~~ fun go , args:"; val (pt, (pos as (p, _))) = (pt, ip);
12.15 (*+*)p = [2];
12.16 (*+*)pos = ([2], Res);
12.17
12.18 @@ -80,7 +80,7 @@
12.19 (*if*) null cn (*then*);
12.20 (*if*) (Tactic.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)] (*then*);
12.21
12.22 - Solve.detailrls pt pos;
12.23 + Detail_Step.detailrls pt pos;
12.24 "~~~~~ fun detailrls , args:"; val (pt, (pos as (p, _))) = (pt, pos);
12.25 val t = get_obj g_form pt p
12.26 val tac = get_obj g_tac pt p
12.27 @@ -148,7 +148,7 @@
12.28 (*+*)ip = ([3, 1], Res);
12.29 (*+*)ip' = ([3, 1], Frm);
12.30
12.31 -val ("detailrls", pt, _) = (*case*) Math_Engine.detailstep pt''''' ip (*of*);
12.32 +val ("detailrls", pt, _) = (*case*) Detail_Step.go pt''''' ip (*of*);
12.33
12.34 show_pt pt; (* added ([3,1,1], Frm), ([3,1,1], Res) after ([3,1], Frm)*)
12.35
13.1 --- a/test/Tools/isac/Minisubpbl/710-interSteps-short.sml Fri Mar 20 19:31:55 2020 +0100
13.2 +++ b/test/Tools/isac/Minisubpbl/710-interSteps-short.sml Mon Mar 23 13:31:29 2020 +0100
13.3 @@ -2,7 +2,7 @@
13.4 Author: Walther Neuper
13.5 (c) copyright due to lincense terms.
13.6
13.7 -Shorter than Minisubplb/700-interSteps.sml +++ Math_Engine.detailstep pt ([3,2], Res)
13.8 +Shorter than Minisubplb/700-interSteps.sml +++ Detail_Step.go pt ([3,2], Res)
13.9 *)
13.10 "----------- Minisubplb/710-interSteps-short.sml -----------------------------------------------";
13.11 "----------- Minisubplb/710-interSteps-short.sml -----------------------------------------------";
13.12 @@ -43,15 +43,15 @@
13.13 (*+*)show_pt pt; (* 11 lines, as produced by autoCalculate CompleteCalc *)
13.14
13.15 (* called by fun interSteps ---------------------- vvvvvvvvvvvvvvvvvvvvvv *)
13.16 -val ("detailrls", pt, ([2, 6], Res)) = (*case*) Math_Engine.detailstep pt ([2], Res) (*of*);
13.17 +val ("detailrls", pt, ([2, 6], Res)) = (*case*) Detail_Step.go pt ([2], Res) (*of*);
13.18
13.19 (*+*)show_pt_tac pt; (* ^^^ + ([2,1], Frm)..([2,6], Res) after ([1], Res)*)
13.20
13.21 -val ("detailrls", pt, ([3, 1, 1], Res)) = (*case*) Math_Engine.detailstep pt ([3,1], Res) (*of*);
13.22 +val ("detailrls", pt, ([3, 1, 1], Res)) = (*case*) Detail_Step.go pt ([3,1], Res) (*of*);
13.23
13.24 (*+*)show_pt_tac pt; (* ^^^ +++ ([3,1,1], Frm),([3,1,1], Res) after ([3,1], Frm)*)
13.25
13.26 -val ("detailrls", pt, ([3, 2, 2], Res)) = (*case*) Math_Engine.detailstep pt ([3,2], Res) (*of*);
13.27 +val ("detailrls", pt, ([3, 2, 2], Res)) = (*case*) Detail_Step.go pt ([3,2], Res) (*of*);
13.28
13.29 (*+*)show_pt_tac pt; (* ^^^ +++ +++ ([3,2,1], Frm)..([3,2,2], Res) after ([3,1], Res)*)
13.30
14.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Fri Mar 20 19:31:55 2020 +0100
14.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Mon Mar 23 13:31:29 2020 +0100
14.3 @@ -115,9 +115,9 @@
14.4 (*if*) (not o is_interpos) ip = false;
14.5 val ip' = lev_pred' pt ip;
14.6
14.7 -(*Math_Engine.detailstep pt ip ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)
14.8 -val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Math_Engine.detailstep pt ip;
14.9 -"~~~~~ fun detailstep, args:"; val (pt, (pos as (p, _))) = (pt, ip);
14.10 +(*Detail_Step.go pt ip ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)
14.11 +val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Detail_Step.go pt ip;
14.12 +"~~~~~ fun go, args:"; val (pt, (pos as (p, _))) = (pt, ip);
14.13 val nd = Ctree.get_nd pt p
14.14 val cn = Ctree.children nd;
14.15 (*if*) null cn = false;
15.1 --- a/test/Tools/isac/Test_Isac_Short.thy Fri Mar 20 19:31:55 2020 +0100
15.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Mar 23 13:31:29 2020 +0100
15.3 @@ -270,7 +270,7 @@
15.4 ML_file "Knowledge/diff.sml"
15.5 ML_file "Knowledge/integrate.sml"
15.6 ML_file "Knowledge/eqsystem.sml"
15.7 - ML_file "Knowledge/test.sml"
15.8 + ML_file "Knowledge/test.sml"
15.9 ML_file "Knowledge/polyminus.sml"
15.10 ML_file "Knowledge/vect.sml"
15.11 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
16.1 --- a/test/Tools/isac/Test_Some.thy Fri Mar 20 19:31:55 2020 +0100
16.2 +++ b/test/Tools/isac/Test_Some.thy Mon Mar 23 13:31:29 2020 +0100
16.3 @@ -16,7 +16,7 @@
16.4 open Env;
16.5 open LI; scan_dn;
16.6 open Istate;
16.7 - open Inform; cas_input;
16.8 + open Error_Pattern;
16.9 open Rtools; trtas2str;
16.10 open Chead; pt_extract;
16.11 open Generate; (* NONE *)
16.12 @@ -86,6 +86,18 @@
16.13 \<close> ML \<open>
16.14 \<close>
16.15
16.16 +section \<open>======= for test/../integrate.sml =====================================\<close>
16.17 +ML \<open>
16.18 +\<close> ML \<open>
16.19 +\<close> ML \<open>
16.20 +\<close>
16.21 +
16.22 +section \<open>===================================================================================\<close>
16.23 +ML \<open>
16.24 +\<close> ML \<open>
16.25 +\<close> ML \<open>
16.26 +\<close>
16.27 +
16.28 section \<open>========== broken after 6871316e75c3, waits here until ctxt cleaned ===============\<close>
16.29 ML \<open>
16.30 \<close> ML \<open>