1.1 --- a/src/Tools/isac/Frontend/interface.sml Thu Mar 15 15:48:52 2018 +0100
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Fri Mar 23 10:14:39 2018 +0100
1.3 @@ -563,7 +563,7 @@
1.4 (*.initContext Thy_ is conceptually impossible at [Pbl,Met]
1.5 and at positions with Check_Postcond and End_Trans;
1.6 at possible pos's there can be NO rewrite (returned as a context, too).*)
1.7 -fun initContext cI Thy_ (pos as (p, p_):pos') =
1.8 +fun initContext cI Celem.Thy_ (pos as (p, p_):pos') =
1.9 ((if member op = [Pbl, Met] p_
1.10 then message2xml cI "thy-context not to calchead"
1.11 else if pos = ([], Res) then message2xml cI "no thy-context at result"
1.12 @@ -601,7 +601,7 @@
1.13 val chd = Math_Engine.initcontext_pbl pt (pp,p_)
1.14 in contextpblOK2xml cI chd end)
1.15 handle _ => sysERROR2xml cI "error in kernel 32")
1.16 - | initContext cI Met_ (p, p_) =
1.17 + | initContext cI Celem.Met_ (p, p_) =
1.18 ((let
1.19 val ((pt,_),_) = get_calc cI
1.20 val pp = par_pblobj pt p
2.1 --- a/src/Tools/isac/Interpret/ctree.sml Thu Mar 15 15:48:52 2018 +0100
2.2 +++ b/src/Tools/isac/Interpret/ctree.sml Fri Mar 23 10:14:39 2018 +0100
2.3 @@ -24,7 +24,7 @@
2.4 The above "open Ctree" creates an unclear situation with structures, in particular in test/.
2.5 This is work in progress, but urges to make policy explicit:
2.6
2.7 -(1) All structures are closed with a signature; this for prepares re-arrangement of structures.
2.8 +(1) All structures are closed with a signature; this prepares for re-arrangement of structures.
2.9 (2) Some structures are pervasive (e.g. Ctree) such, that an "open" ensures readability locally.
2.10 (3) test/ is preceeded by "open" for all structures, in order to ease copy&paste from scr/ to test/
2.11
3.1 --- a/src/Tools/isac/Interpret/generate.sml Thu Mar 15 15:48:52 2018 +0100
3.2 +++ b/src/Tools/isac/Interpret/generate.sml Fri Mar 23 10:14:39 2018 +0100
3.3 @@ -18,7 +18,7 @@
3.4 | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)
3.5 val generate1 : theory -> Tac.tac_ -> Selem.istate * Proof.context ->
3.6 Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree (* for calchead.sml------------- ^^^ *)
3.7 - val init_istate : Tac.tac -> term -> Selem.istate (* for solve.sml *)
3.8 + val init_istate : Tac.tac -> term -> Selem.istate
3.9 val init_pbl : (string * (term * 'a)) list -> Model.itm list
3.10 val init_pbl' : (string * (term * term)) list -> Model.itm list
3.11 val embed_deriv : taci list -> Ctree.state -> Ctree.pos' list * (Ctree.state) (* for inform.sml *)
3.12 @@ -46,14 +46,18 @@
3.13 fun init_istate (Tac.Rewrite_Set rls) t =
3.14 (case assoc_rls rls of
3.15 Celem.Rrls {scr = Celem.Rfuns {init_state = ii, ...}, ...} => Selem.RrlsState (ii t)
3.16 - | Celem.Rls {scr = EmptyScr, ...} =>
3.17 + | Celem.Rls {scr = Celem.EmptyScr, ...} =>
3.18 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
3.19 "use prep_rls' for storing rule-sets !")
3.20 - | Celem.Rls {scr = Celem.Prog s, ...} => (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, Celem.e_term, Selem.Sundef, true))
3.21 - | Celem.Seq {scr=EmptyScr,...} =>
3.22 + | Celem.Rls {scr = Celem.Prog s, ...} =>
3.23 + (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, Celem.e_term, Selem.Sundef, true))
3.24 + | Celem.Seq {scr = EmptyScr,...} =>
3.25 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
3.26 - "use prep_rls' for storing rule-sets !")
3.27 - | Celem.Seq {scr = Celem.Prog s,...} => (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, Celem.e_term, Selem.Sundef, true))
3.28 + " Use prep_rls' for storing rule-sets !")
3.29 + | Celem.Seq {scr = Celem.Prog s,...} =>
3.30 +(writeln ("### init_istate: rls = \"" ^ "rls" ^ "\", Prog = \"" ^ Celem.term2str s ^ "\"");
3.31 + (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, Celem.e_term, Selem.Sundef, true))
3.32 +)
3.33 | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")
3.34 | init_istate (Tac.Rewrite_Set_Inst (subs, rls)) t =
3.35 let
3.36 @@ -62,14 +66,14 @@
3.37 | _ => error "init_istate: uncovered case "
3.38 (*...we suppose the substitution of only _one_ bound variable*)
3.39 in case assoc_rls rls of
3.40 - Celem.Rls {scr = EmptyScr, ...} =>
3.41 + Celem.Rls {scr = Celem.EmptyScr, ...} =>
3.42 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
3.43 "use prep_rls' for storing rule-sets !")
3.44 | Celem.Rls {scr = Celem.Prog s, ...} =>
3.45 let val (form, bdv) = LTool.two_scr_arg s
3.46 in (Selem.ScrState ([(form, t), (bdv, v)], [], NONE, Celem.e_term, Selem.Sundef,true))
3.47 end
3.48 - | Celem.Seq {scr = EmptyScr, ...} =>
3.49 + | Celem.Seq {scr = Celem.EmptyScr, ...} =>
3.50 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
3.51 "use prep_rls' for storing rule-sets !")
3.52 | Celem.Seq {scr = Celem.Prog s,...} =>
4.1 --- a/src/Tools/isac/Interpret/mathengine.sml Thu Mar 15 15:48:52 2018 +0100
4.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Fri Mar 23 10:14:39 2018 +0100
4.3 @@ -9,14 +9,14 @@
4.4 signature MATH_ENGINE =
4.5 sig
4.6 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
4.7 - val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ctree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Selem.safe * Ctree.ctree
4.8 - val autocalc :
4.9 - Ctree.pos' list -> Ctree.pos' -> (Ctree.state) * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.state)
4.10 + val me : Solve.tac'_ -> Ctree.pos' -> NEW ->
4.11 + Ctree.ctree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Selem.safe * Ctree.ctree
4.12 + val autocalc : Ctree.pos' list -> Ctree.pos' -> (Ctree.state) * Generate.taci list ->
4.13 + Solve.auto -> string * Ctree.pos' list * (Ctree.state)
4.14 val locatetac :
4.15 Tac.tac -> Ctree.state -> string * (Generate.taci list * Ctree.pos' list * (Ctree.state))
4.16 val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
4.17 - val detailstep :
4.18 - Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
4.19 + val detailstep : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
4.20 val get_pblID : Ctree.state -> Celem.pblID option
4.21
4.22 val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Celem.scr * Model.itm list * (bool * term) list
5.1 --- a/src/Tools/isac/Interpret/ptyps.sml Thu Mar 15 15:48:52 2018 +0100
5.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Fri Mar 23 10:14:39 2018 +0100
5.3 @@ -641,8 +641,8 @@
5.4 handle _ => error ("pblID2guh: not for \"" ^ strs2str' pblID ^ "\""));
5.5 fun metID2guh metID = (((#guh o get_met) metID)
5.6 handle _ => error ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));
5.7 -fun kestoreID2guh Pbl_ kestoreID = pblID2guh kestoreID
5.8 - | kestoreID2guh Met_ kestoreID = metID2guh kestoreID
5.9 +fun kestoreID2guh Celem.Pbl_ kestoreID = pblID2guh kestoreID
5.10 + | kestoreID2guh Celem.Met_ kestoreID = metID2guh kestoreID
5.11 | kestoreID2guh ketype kestoreID =
5.12 error ("kestoreID2guh: \"" ^ Celem.ketype2str ketype ^ "\" not for \"" ^ strs2str' kestoreID ^ "\"");
5.13
6.1 --- a/src/Tools/isac/Interpret/rewtools.sml Thu Mar 15 15:48:52 2018 +0100
6.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Fri Mar 23 10:14:39 2018 +0100
6.3 @@ -429,7 +429,7 @@
6.4 error ("context_thy: not for tac " ^ Tac.tac2str tac ^ " at " ^ Ctree.pos'2str p)
6.5
6.6 (* get all theorems in a rule set (recursivley containing rule sets) *)
6.7 -fun thm_of_rule Erule = []
6.8 +fun thm_of_rule Celem.Erule = []
6.9 | thm_of_rule (thm as Celem.Thm _) = [thm]
6.10 | thm_of_rule (Celem.Calc _) = []
6.11 | thm_of_rule (Celem.Cal1 _) = []
7.1 --- a/src/Tools/isac/Interpret/script.sml Thu Mar 15 15:48:52 2018 +0100
7.2 +++ b/src/Tools/isac/Interpret/script.sml Fri Mar 23 10:14:39 2018 +0100
7.3 @@ -42,6 +42,8 @@
7.4 val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
7.5 val nstep_up : Celem.theory' * Celem.rls -> Ctree.state -> Celem.scr -> LTool.env ->
7.6 Celem.lrd list -> appy_ -> term option -> term -> appy
7.7 + val nxt_up: Celem.theory' * Celem.rls -> Ctree.state -> Celem.scr -> LTool.env ->
7.8 + Celem.lrd list -> appy_ -> term -> term option -> term -> appy
7.9 val stac2tac : Ctree.ctree -> theory -> term -> Tac.tac
7.10 val stac2tac_ : Ctree.ctree -> theory -> term -> Tac.tac * Tac.tac_
7.11 val upd_env_opt : LTool.env -> term option * term -> LTool.env
7.12 @@ -55,7 +57,7 @@
7.13 (* traces the leaves (ie. non-tactical nodes) of Prog found by next_tac, see "and scr" *)
7.14 val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
7.15
7.16 -structure Lucin(**): LUCAS_INTERPRETER(**) =
7.17 +structure Lucin(*: LUCAS_INTERPRETER*) =
7.18 struct
7.19 open Ctree
7.20
7.21 @@ -117,9 +119,9 @@
7.22
7.23 (*go at a location in a script and fetch the contents*)
7.24 fun go [] t = t
7.25 - | go (D::p) (Abs(_, _, t0)) = go (p : Celem.loc_) t0
7.26 - | go (L::p) (t1 $ _) = go p t1
7.27 - | go (R::p) (_ $ t2) = go p t2
7.28 + | go (Celem.D :: p) (Abs(_, _, t0)) = go (p : Celem.loc_) t0
7.29 + | go (Celem.L :: p) (t1 $ _) = go p t1
7.30 + | go (Celem.R :: p) (_ $ t2) = go p t2
7.31 | go l _ = error ("go: no " ^ Celem.loc_2str l);
7.32
7.33 (*.get argument of first stactic in a script for init_form.*)
7.34 @@ -1045,7 +1047,7 @@
7.35 (Tac.Rewrite' (thy, "e_rew_ord", Celem.e_rls, false, thm'', f, (Celem.e_term, [(*!?!8.6.03*)])),
7.36 (Selem.Uistate, ctxt), (Celem.e_term, Selem.Sundef)) (*next stac*)
7.37 | _ => error "next_tac: uncovered case next_rule")
7.38 - | next_tac thy (ptp as (pt, (p, _)):ctree * pos') (sc as Celem.Prog (_ $ body))
7.39 + | next_tac thy (ptp as (pt, (p, _))) (sc as Celem.Prog (_ $ body))
7.40 (Selem.ScrState (E,l,a,v,s,_), ctxt) =
7.41 (case if l = [] then appy thy ptp E [Celem.R] body NONE v
7.42 else nstep_up thy ptp sc E l Skip_ a v of
8.1 --- a/src/Tools/isac/Interpret/solve.sml Thu Mar 15 15:48:52 2018 +0100
8.2 +++ b/src/Tools/isac/Interpret/solve.sml Fri Mar 23 10:14:39 2018 +0100
8.3 @@ -403,7 +403,7 @@
8.4 val ctxt = get_ctxt pt pos
8.5 in
8.6 case rls of
8.7 - Celem.Rrls {scr = Celem.Rfuns {init_state,...},...} =>
8.8 + Celem.Rrls {scr = Celem.Rfuns {init_state, ...}, ...} =>
8.9 let
8.10 val (_, _, _, rul_terms) = init_state t
8.11 val newnds = rul_terms_2nds (Proof_Context.theory_of ctxt) [] t rul_terms
8.12 @@ -421,7 +421,7 @@
8.13 val (_,_, (pt'', _)) = complete_solve CompleteSubpbl [] (pt', pos')
8.14 val newnds = children (get_nd pt'' p)
8.15 val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*)
8.16 - in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
8.17 + in ("detailrls", pt''', (p @ [length newnds], Res)) end
8.18 end;
8.19
8.20 fun get_form (mI, m) (p,p_) pt =
9.1 --- a/src/Tools/isac/KEStore.thy Thu Mar 15 15:48:52 2018 +0100
9.2 +++ b/src/Tools/isac/KEStore.thy Fri Mar 23 10:14:39 2018 +0100
9.3 @@ -182,8 +182,7 @@
9.4
9.5 section {* Functions for checking KEStore_Elems *}
9.6 ML {*
9.7 -fun short_string_of_rls Erls = "Erls"
9.8 -(*
9.9 +fun short_string_of_rls Celem.Erls = "Erls"
9.10 | short_string_of_rls (Celem.Rls {calc, rules, ...}) =
9.11 "Rls {#calc = " ^ string_of_int (length calc) ^
9.12 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
9.13 @@ -191,7 +190,6 @@
9.14 "Seq {#calc = " ^ string_of_int (length calc) ^
9.15 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
9.16 | short_string_of_rls (Celem.Rrls _) = "Rrls {...}";
9.17 -*)
9.18 fun check_kestore_rls (rls', (thyID, rls)) =
9.19 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
9.20
10.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu Mar 15 15:48:52 2018 +0100
10.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Fri Mar 23 10:14:39 2018 +0100
10.3 @@ -100,7 +100,7 @@
10.4 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
10.5 ("#Find" ,["Biegelinie b_b"]),
10.6 ("#Relate",["Randbedingungen r_b"])],
10.7 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),
10.8 + Celem.append_rls "e_rls" Celem.e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),
10.9 (Specify.prep_pbt @{theory} "pbl_bieg_mom" [] Celem.e_pblID
10.10 (["MomentBestimmte","Biegelinien"],
10.11 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
10.12 @@ -108,31 +108,31 @@
10.13 ("#Find" ,["Biegelinie b_b"]),
10.14 ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
10.15 ],
10.16 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
10.17 + Celem.append_rls "e_rls" Celem.e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
10.18 (Specify.prep_pbt @{theory} "pbl_bieg_momg" [] Celem.e_pblID
10.19 - (["MomentGegebene","Biegelinien"], [], Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [], NONE,
10.20 + (["MomentGegebene","Biegelinien"], [], Celem.append_rls "e_rls" Celem.e_rls [], NONE,
10.21 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])),
10.22 (Specify.prep_pbt @{theory} "pbl_bieg_einf" [] Celem.e_pblID
10.23 - (["einfache","Biegelinien"], [], Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [], NONE,
10.24 + (["einfache","Biegelinien"], [], Celem.append_rls "e_rls" Celem.e_rls [], NONE,
10.25 [["IntegrierenUndKonstanteBestimmen","4x4System"]])),
10.26 (Specify.prep_pbt @{theory} "pbl_bieg_momquer" [] Celem.e_pblID
10.27 - (["QuerkraftUndMomentBestimmte","Biegelinien"], [], Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [], NONE,
10.28 + (["QuerkraftUndMomentBestimmte","Biegelinien"], [], Celem.append_rls "e_rls" Celem.e_rls [], NONE,
10.29 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])),
10.30 (Specify.prep_pbt @{theory} "pbl_bieg_vonq" [] Celem.e_pblID
10.31 (["vonBelastungZu","Biegelinien"],
10.32 [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
10.33 ("#Find" ,["Funktionen funs'''"])],
10.34 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [], NONE, [["Biegelinien","ausBelastung"]])),
10.35 + Celem.append_rls "e_rls" Celem.e_rls [], NONE, [["Biegelinien","ausBelastung"]])),
10.36 (Specify.prep_pbt @{theory} "pbl_bieg_randbed" [] Celem.e_pblID
10.37 (["setzeRandbedingungen","Biegelinien"],
10.38 [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
10.39 ("#Find" ,["Gleichungen equs'''"])],
10.40 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),
10.41 + Celem.append_rls "e_rls" Celem.e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),
10.42 (Specify.prep_pbt @{theory} "pbl_equ_fromfun" [] Celem.e_pblID
10.43 (["makeFunctionTo","equation"],
10.44 [("#Given" ,["functionEq fu_n","substitution su_b"]),
10.45 ("#Find" ,["equality equ'''"])],
10.46 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [], NONE, [["Equation","fromFunction"]]))] *}
10.47 + Celem.append_rls "e_rls" Celem.e_rls [], NONE, [["Equation","fromFunction"]]))] *}
10.48 ML {*
10.49 (** methods **)
10.50
11.1 --- a/src/Tools/isac/Knowledge/Diff.thy Thu Mar 15 15:48:52 2018 +0100
11.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Fri Mar 23 10:14:39 2018 +0100
11.3 @@ -253,7 +253,7 @@
11.4 (["derivative_of","function"],
11.5 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
11.6 ("#Find" ,["derivative f_f'"])],
11.7 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [],
11.8 + Celem.append_rls "e_rls" Celem.e_rls [],
11.9 SOME "Diff (f_f, v_v)", [["diff","differentiate_on_R"],
11.10 ["diff","after_simplification"]])),
11.11 (*here "named" is used differently from Integration"*)
11.12 @@ -261,7 +261,7 @@
11.13 (["named","derivative_of","function"],
11.14 [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
11.15 ("#Find" ,["derivativeEq f_f'"])],
11.16 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [],
11.17 + Celem.append_rls "e_rls" Celem.e_rls [],
11.18 SOME "Differentiate (f_f, v_v)",
11.19 [["diff","differentiate_equality"]]))] *}
11.20
12.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Thu Mar 15 15:48:52 2018 +0100
12.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Fri Mar 23 10:14:39 2018 +0100
12.3 @@ -36,7 +36,7 @@
12.4 (* TODO: drop ^^^^^*)
12.5 ("#Where" ,[]),
12.6 ("#Find" ,["boolTestFind s_s"])],
12.7 - {rew_ord' = "xxxe_rew_ordxxx", rls' = tval_rls, srls = Celem.e_rls, prls = Celem.e_rls, calc = [],
12.8 + {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Celem.e_rls, prls = Celem.e_rls, calc = [],
12.9 crls = tval_rls, errpats = [], nrls = Test_simplify},
12.10 "Script Diophant_equation (e_e::bool) (v_v::int)= " ^
12.11 "(Repeat " ^
13.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Mar 15 15:48:52 2018 +0100
13.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Fri Mar 23 10:14:39 2018 +0100
13.3 @@ -294,7 +294,7 @@
13.4 ML {*
13.5 val isolate_bdvs =
13.6 Celem.Rls {id="isolate_bdvs", preconds = [],
13.7 - rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord),
13.8 + rew_ord = ("e_rew_ord", Celem.e_rew_ord),
13.9 erls = Celem.append_rls "erls_isolate_bdvs" Celem.e_rls
13.10 [(Celem.Calc ("EqSystem.occur'_exactly'_in",
13.11 eval_occur_exactly_in
13.12 @@ -310,7 +310,7 @@
13.13 ML {*
13.14 val isolate_bdvs_4x4 =
13.15 Celem.Rls {id="isolate_bdvs_4x4", preconds = [],
13.16 - rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord),
13.17 + rew_ord = ("e_rew_ord", Celem.e_rew_ord),
13.18 erls = Celem.append_rls
13.19 "erls_isolate_bdvs_4x4" Celem.e_rls
13.20 [Celem.Calc ("EqSystem.occur'_exactly'_in",
13.21 @@ -345,9 +345,9 @@
13.22
13.23 val prls_triangular =
13.24 Celem.Rls {id="prls_triangular", preconds = [],
13.25 - rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord),
13.26 + rew_ord = ("e_rew_ord", Celem.e_rew_ord),
13.27 erls = Celem.Rls {id="erls_prls_triangular", preconds = [],
13.28 - rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord),
13.29 + rew_ord = ("e_rew_ord", Celem.e_rew_ord),
13.30 erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
13.31 rules = [(*for precond NTH_CONS ...*)
13.32 Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
13.33 @@ -374,9 +374,9 @@
13.34 more similarity to prls_triangular desirable*)
13.35 val prls_triangular4 =
13.36 Celem.Rls {id="prls_triangular4", preconds = [],
13.37 - rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord),
13.38 + rew_ord = ("e_rew_ord", Celem.e_rew_ord),
13.39 erls = Celem.Rls {id="erls_prls_triangular4", preconds = [],
13.40 - rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord),
13.41 + rew_ord = ("e_rew_ord", Celem.e_rew_ord),
13.42 erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
13.43 rules = [(*for precond NTH_CONS ...*)
13.44 Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
13.45 @@ -416,13 +416,13 @@
13.46 (["system"],
13.47 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
13.48 ("#Find" ,["solution ss'''"](*''' is copy-named*))],
13.49 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
13.50 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
13.51 (Specify.prep_pbt thy "pbl_equsys_lin" [] Celem.e_pblID
13.52 (["LINEAR", "system"],
13.53 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
13.54 (*TODO.WN050929 check linearity*)
13.55 ("#Find" ,["solution ss'''"])],
13.56 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
13.57 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
13.58 (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Celem.e_pblID
13.59 (["2x2", "LINEAR", "system"],
13.60 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
13.61 @@ -447,7 +447,7 @@
13.62 (["normalise", "2x2", "LINEAR", "system"],
13.63 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
13.64 ("#Find" ,["solution ss'''"])],
13.65 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)],
13.66 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)],
13.67 SOME "solveSystem e_s v_s",
13.68 [["EqSystem","normalise","2x2"]])),
13.69 (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Celem.e_pblID
13.70 @@ -492,7 +492,7 @@
13.71 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
13.72 (*LENGTH is checked 1 level above*)
13.73 ("#Find" ,["solution ss'''"])],
13.74 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)],
13.75 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)],
13.76 SOME "solveSystem e_s v_s",
13.77 [["EqSystem","normalise","4x4"]]))] *}
13.78
14.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Thu Mar 15 15:48:52 2018 +0100
14.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Fri Mar 23 10:14:39 2018 +0100
14.3 @@ -342,7 +342,7 @@
14.4 (["integrate","function"],
14.5 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
14.6 ("#Find" ,["antiDerivative F_F"])],
14.7 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)],
14.8 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)],
14.9 SOME "Integrate (f_f, v_v)",
14.10 [["diff","integration"]])),
14.11 (*here "named" is used differently from Differentiation"*)
14.12 @@ -350,7 +350,7 @@
14.13 (["named","integrate","function"],
14.14 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
14.15 ("#Find" ,["antiDerivativeName F_F"])],
14.16 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)],
14.17 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)],
14.18 SOME "Integrate (f_f, v_v)",
14.19 [["diff","integration","named"]]))] *}
14.20
15.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Mar 15 15:48:52 2018 +0100
15.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri Mar 23 10:14:39 2018 +0100
15.3 @@ -56,13 +56,13 @@
15.4 because "inverse" = Const ("Rings.inverse_class.inverse", ..*)
15.5 [("#Given" ,["filterExpression (X_eq::bool)"]),
15.6 ("#Find" ,["stepResponse (n_eq::bool)"])],
15.7 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], NONE,
15.8 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], NONE,
15.9 [["SignalProcessing","Z_Transform","Inverse"]])),
15.10 (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID
15.11 (["Inverse", "Z_Transform", "SignalProcessing"],
15.12 [("#Given" ,["filterExpression X_eq"]),
15.13 ("#Find" ,["stepResponse n_eq"])],
15.14 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], NONE,
15.15 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], NONE,
15.16 [["SignalProcessing","Z_Transform","Inverse"]]))] *}
15.17
15.18 subsection {*Define Name and Signature for the Method*}
16.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Thu Mar 15 15:48:52 2018 +0100
16.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Fri Mar 23 10:14:39 2018 +0100
16.3 @@ -100,7 +100,7 @@
16.4 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
16.5 val LinEq_simplify = prep_rls'(
16.6 Celem.Rls {id = "LinEq_simplify", preconds = [],
16.7 - rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord),
16.8 + rew_ord = ("e_rew_ord", Celem.e_rew_ord),
16.9 erls = LinEq_erls,
16.10 srls = Celem.Erls,
16.11 calc = [], errpatts = [],
17.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Mar 15 15:48:52 2018 +0100
17.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Fri Mar 23 10:14:39 2018 +0100
17.3 @@ -175,7 +175,7 @@
17.4 ("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
17.5 ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
17.6 ("#Find" ,["decomposedFunction p_p'''"])],
17.7 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_ TODO*)],
17.8 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_ TODO*)],
17.9 NONE,
17.10 [["simplification","of_rationals","to_partial_fraction"]]))] *}
17.11
18.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Mar 15 15:48:52 2018 +0100
18.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Fri Mar 23 10:14:39 2018 +0100
18.3 @@ -1601,7 +1601,7 @@
18.4 [("#Given" ,["Term t_t"]),
18.5 ("#Where" ,["t_t is_polyexp"]),
18.6 ("#Find" ,["normalform n_n"])],
18.7 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)
18.8 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)
18.9 Celem.Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
18.10 SOME "Simplify t_t",
18.11 [["simplification","for_polynomials"]]))] *}
19.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Mar 15 15:48:52 2018 +0100
19.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Fri Mar 23 10:14:39 2018 +0100
19.3 @@ -422,7 +422,7 @@
19.4
19.5 val cancel_leading_coeff = prep_rls'(
19.6 Celem.Rls {id = "cancel_leading_coeff", preconds = [],
19.7 - rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
19.8 + rew_ord = ("e_rew_ord",Celem.e_rew_ord),
19.9 erls = PolyEq_erls, srls = Celem.Erls, calc = [], errpatts = [],
19.10 rules =
19.11 [Celem.Thm ("cancel_leading_coeff1",TermC.num_str @{thm cancel_leading_coeff1}),
19.12 @@ -445,7 +445,7 @@
19.13 ML{*
19.14 val complete_square = prep_rls'(
19.15 Celem.Rls {id = "complete_square", preconds = [],
19.16 - rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
19.17 + rew_ord = ("e_rew_ord",Celem.e_rew_ord),
19.18 erls = PolyEq_erls, srls = Celem.Erls, calc = [], errpatts = [],
19.19 rules = [Celem.Thm ("complete_square1",TermC.num_str @{thm complete_square1}),
19.20 Celem.Thm ("complete_square2",TermC.num_str @{thm complete_square2}),
19.21 @@ -490,7 +490,7 @@
19.22 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
19.23 val d0_polyeq_simplify = prep_rls'(
19.24 Celem.Rls {id = "d0_polyeq_simplify", preconds = [],
19.25 - rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
19.26 + rew_ord = ("e_rew_ord",Celem.e_rew_ord),
19.27 erls = PolyEq_erls,
19.28 srls = Celem.Erls,
19.29 calc = [], errpatts = [],
19.30 @@ -504,7 +504,7 @@
19.31 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
19.32 val d1_polyeq_simplify = prep_rls'(
19.33 Celem.Rls {id = "d1_polyeq_simplify", preconds = [],
19.34 - rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
19.35 + rew_ord = ("e_rew_ord",Celem.e_rew_ord),
19.36 erls = PolyEq_erls,
19.37 srls = Celem.Erls,
19.38 calc = [], errpatts = [],
19.39 @@ -525,7 +525,7 @@
19.40 (* isolate the bound variable in an d2 equation with bdv only;
19.41 "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *)
19.42 val d2_polyeq_bdv_only_simplify = prep_rls'(
19.43 - Celem.Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
19.44 + Celem.Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",Celem.e_rew_ord),
19.45 erls = PolyEq_erls, srls = Celem.Erls, calc = [], errpatts = [],
19.46 rules =
19.47 [Celem.Thm ("d2_prescind1", TermC.num_str @{thm d2_prescind1}), (* ax+bx^2=0 -> x(a+bx)=0 *)
19.48 @@ -547,7 +547,7 @@
19.49 'bdv' is a meta-constant*)
19.50 val d2_polyeq_sq_only_simplify = prep_rls'(
19.51 Celem.Rls {id = "d2_polyeq_sq_only_simplify", preconds = [],
19.52 - rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
19.53 + rew_ord = ("e_rew_ord",Celem.e_rew_ord),
19.54 erls = PolyEq_erls,
19.55 srls = Celem.Erls,
19.56 calc = [], errpatts = [],
19.57 @@ -574,7 +574,7 @@
19.58 'bdv' is a meta-constant*)
19.59 val d2_polyeq_pqFormula_simplify = prep_rls'(
19.60 Celem.Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],
19.61 - rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,
19.62 + rew_ord = ("e_rew_ord",Celem.e_rew_ord), erls = PolyEq_erls,
19.63 srls = Celem.Erls, calc = [], errpatts = [],
19.64 rules = [Celem.Thm("d2_pqformula1",TermC.num_str @{thm d2_pqformula1}),
19.65 (* q+px+ x^2=0 *)
19.66 @@ -620,7 +620,7 @@
19.67 'bdv' is a meta-constant*)
19.68 val d2_polyeq_abcFormula_simplify = prep_rls'(
19.69 Celem.Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],
19.70 - rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,
19.71 + rew_ord = ("e_rew_ord",Celem.e_rew_ord), erls = PolyEq_erls,
19.72 srls = Celem.Erls, calc = [], errpatts = [],
19.73 rules = [Celem.Thm("d2_abcformula1",TermC.num_str @{thm d2_abcformula1}),
19.74 (*c+bx+cx^2=0 *)
19.75 @@ -668,7 +668,7 @@
19.76 'bdv' is a meta-constant*)
19.77 val d2_polyeq_simplify = prep_rls'(
19.78 Celem.Rls {id = "d2_polyeq_simplify", preconds = [],
19.79 - rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,
19.80 + rew_ord = ("e_rew_ord",Celem.e_rew_ord), erls = PolyEq_erls,
19.81 srls = Celem.Erls, calc = [], errpatts = [],
19.82 rules = [Celem.Thm("d2_pqformula1",TermC.num_str @{thm d2_pqformula1}),
19.83 (* p+qx+ x^2=0 *)
19.84 @@ -728,7 +728,7 @@
19.85 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
19.86 val d3_polyeq_simplify = prep_rls'(
19.87 Celem.Rls {id = "d3_polyeq_simplify", preconds = [],
19.88 - rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,
19.89 + rew_ord = ("e_rew_ord",Celem.e_rew_ord), erls = PolyEq_erls,
19.90 srls = Celem.Erls, calc = [], errpatts = [],
19.91 rules =
19.92 [Celem.Thm("d3_reduce_equation1",TermC.num_str @{thm d3_reduce_equation1}),
19.93 @@ -801,7 +801,7 @@
19.94 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
19.95 val d4_polyeq_simplify = prep_rls'(
19.96 Celem.Rls {id = "d4_polyeq_simplify", preconds = [],
19.97 - rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,
19.98 + rew_ord = ("e_rew_ord",Celem.e_rew_ord), erls = PolyEq_erls,
19.99 srls = Celem.Erls, calc = [], errpatts = [],
19.100 rules =
19.101 [Celem.Thm("d4_sub_u1",TermC.num_str @{thm d4_sub_u1})
20.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Thu Mar 15 15:48:52 2018 +0100
20.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Fri Mar 23 10:14:39 2018 +0100
20.3 @@ -451,7 +451,7 @@
20.4 [("#Given", ["Term t_t"]),
20.5 ("#Where", ["t_t is_polyexp"]),
20.6 ("#Find", ["normalform n_n"])],
20.7 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)
20.8 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)
20.9 Celem.Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
20.10 SOME "Vereinfache t_t",
20.11 [["simplification","for_polynomials","with_parentheses_mult"]])),
21.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Mar 15 15:48:52 2018 +0100
21.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri Mar 23 10:14:39 2018 +0100
21.3 @@ -891,7 +891,7 @@
21.4 [("#Given" ,["Term t_t"]),
21.5 ("#Where" ,["t_t is_ratpolyexp"]),
21.6 ("#Find" ,["normalform n_n"])],
21.7 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)],
21.8 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)],
21.9 SOME "Simplify t_t", [["simplification","of_rationals"]]))] *}
21.10
21.11 section {* A methods for simplification of rationals *}
22.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Thu Mar 15 15:48:52 2018 +0100
22.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Fri Mar 23 10:14:39 2018 +0100
22.3 @@ -33,12 +33,12 @@
22.4 (["simplification"],
22.5 [("#Given" ,["Term t_t"]),
22.6 ("#Find" ,["normalform n_n"])],
22.7 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], SOME "Simplify t_t", [])),
22.8 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], SOME "Simplify t_t", [])),
22.9 (Specify.prep_pbt thy "pbl_vereinfache" [] Celem.e_pblID
22.10 (["vereinfachen"],
22.11 [("#Given", ["Term t_t"]),
22.12 ("#Find", ["normalform n_n"])],
22.13 - Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], SOME "Vereinfache t_t", []))] *}
22.14 + Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], SOME "Vereinfache t_t", []))] *}
22.15
22.16 (** methods **)
22.17 setup {* KEStore_Elems.add_mets
23.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Mar 15 15:48:52 2018 +0100
23.2 +++ b/src/Tools/isac/Knowledge/Test.thy Fri Mar 23 10:14:39 2018 +0100
23.3 @@ -282,7 +282,7 @@
23.4 (*make () dissappear*)
23.5 val rearrange_assoc =
23.6 Celem.Rls{id = "rearrange_assoc", preconds = [],
23.7 - rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
23.8 + rew_ord = ("e_rew_ord",Celem.e_rew_ord),
23.9 erls = Celem.e_rls, srls = Celem.e_rls, calc = [], errpatts = [],
23.10 rules =
23.11 [Celem.Thm ("sym_add_assoc",TermC.num_str (@{thm add.assoc} RS @{thm sym})),
23.12 @@ -305,7 +305,7 @@
23.13
23.14 (*todo: replace by Rewrite("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add)*)
23.15 val norm_equation =
23.16 - Celem.Rls{id = "norm_equation", preconds = [], rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
23.17 + Celem.Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Celem.e_rew_ord),
23.18 erls = tval_rls, srls = Celem.e_rls, calc = [], errpatts = [],
23.19 rules = [Celem.Thm ("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add})
23.20 ],
23.21 @@ -428,7 +428,7 @@
23.22
23.23 (*isolate the root in a root-equation*)
23.24 val isolate_root =
23.25 - Celem.Rls{id = "isolate_root", preconds = [], rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
23.26 + Celem.Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Celem.e_rew_ord),
23.27 erls=tval_rls,srls = Celem.e_rls, calc=[], errpatts = [],
23.28 rules = [Celem.Thm ("rroot_to_lhs",TermC.num_str @{thm rroot_to_lhs}),
23.29 Celem.Thm ("rroot_to_lhs_mult",TermC.num_str @{thm rroot_to_lhs_mult}),
23.30 @@ -442,7 +442,7 @@
23.31
23.32 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
23.33 val isolate_bdv =
23.34 - Celem.Rls{id = "isolate_bdv", preconds = [], rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
23.35 + Celem.Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Celem.e_rew_ord),
23.36 erls=tval_rls,srls = Celem.e_rls, calc= [], errpatts = [],
23.37 rules =
23.38 [Celem.Thm ("risolate_bdv_add",TermC.num_str @{thm risolate_bdv_add}),
23.39 @@ -539,7 +539,7 @@
23.40 [("#Given" ,["equality e_e","solveFor v_v"]),
23.41 ("#Where" ,["matches (?a = ?b) e_e"]),
23.42 ("#Find" ,["solutions v_v'i'"])],
23.43 - {rew_ord' = "xxxe_rew_ordxxx", rls' = tval_rls, srls = Celem.e_rls,
23.44 + {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Celem.e_rls,
23.45 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
23.46 nrls = Test_simplify},
23.47 "Script Solve_linear (e_e::bool) (v_v::real)= " ^
23.48 @@ -552,7 +552,7 @@
23.49 (["Test","testeq"],
23.50 [("#Given" ,["boolTestGiven g_g"]),
23.51 ("#Find" ,["boolTestFind f_f"])],
23.52 - {rew_ord'="xxxe_rew_ordxxx",rls'="tval_rls",asm_rls=[], asm_thm=[("square_equation_left","")]},
23.53 + {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[], asm_thm=[("square_equation_left","")]},
23.54 "Script Testeq (e_q::bool) = " ^
23.55 "Repeat " ^
23.56 " (let e_e = Try (Repeat (Rewrite rroot_square_inv False e_q)); " ^
23.57 @@ -799,7 +799,7 @@
23.58 [("#Given" ,["equality e_e","solveFor v_v"]),
23.59 ("#Where" ,["contains_root (e_e::bool)"]),
23.60 ("#Find" ,["solutions v_v'i'"])],
23.61 - {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
23.62 + {rew_ord'="e_rew_ord",rls'=tval_rls,
23.63 srls = Celem.append_rls "srls_contains_root" Celem.e_rls
23.64 [Celem.Calc ("Test.contains'_root",eval_contains_root "")],
23.65 prls = Celem.append_rls "prls_contains_root" Celem.e_rls
23.66 @@ -825,7 +825,7 @@
23.67 (["Test","squ-equ-test2"],
23.68 [("#Given" ,["equality e_e","solveFor v_v"]),
23.69 ("#Find" ,["solutions v_v'i'"])],
23.70 - {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
23.71 + {rew_ord'="e_rew_ord",rls'=tval_rls,
23.72 srls = Celem.append_rls "srls_contains_root" Celem.e_rls
23.73 [Celem.Calc ("Test.contains'_root",eval_contains_root"")],
23.74 prls=Celem.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls(*,asm_rls=[],
23.75 @@ -852,7 +852,7 @@
23.76 [("#Given" ,["equality e_e","solveFor v_v"]),
23.77 ("#Where" ,["precond_rootmet v_v"]),
23.78 ("#Find" ,["solutions v_v'i'"])],
23.79 - {rew_ord' = "xxxe_rew_ordxxx", rls' = tval_rls, srls = Celem.e_rls,
23.80 + {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Celem.e_rls,
23.81 prls = Celem.append_rls "prls_met_test_squ_sub" Celem.e_rls
23.82 [Celem.Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
23.83 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
23.84 @@ -870,7 +870,7 @@
23.85 (["Test","squ-equ-test-subpbl2"],
23.86 [("#Given" ,["equality e_e","solveFor v_v"]),
23.87 ("#Find" ,["solutions v_v'i'"])],
23.88 - {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,srls=Celem.e_rls,prls=Celem.e_rls,calc=[], crls=tval_rls,
23.89 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls=Celem.e_rls,prls=Celem.e_rls,calc=[], crls=tval_rls,
23.90 errpats = [], nrls = Celem.e_rls (*, asm_rls=[],asm_thm=[("square_equation_left",""),
23.91 ("square_equation_right","")]*)},
23.92 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.93 @@ -883,7 +883,7 @@
23.94 (["Test","square_equation...notTerminating"],
23.95 [("#Given" ,["equality e_e","solveFor v_v"]),
23.96 ("#Find" ,["solutions v_v'i'"])],
23.97 - {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
23.98 + {rew_ord'="e_rew_ord",rls'=tval_rls,
23.99 srls = Celem.append_rls "srls_contains_root" Celem.e_rls
23.100 [Celem.Calc ("Test.contains'_root",eval_contains_root"")],
23.101 prls=Celem.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls(*,asm_rls=[],
23.102 @@ -908,7 +908,7 @@
23.103 (["Test","square_equation1"],
23.104 [("#Given" ,["equality e_e","solveFor v_v"]),
23.105 ("#Find" ,["solutions v_v'i'"])],
23.106 - {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
23.107 + {rew_ord'="e_rew_ord",rls'=tval_rls,
23.108 srls = Celem.append_rls "srls_contains_root" Celem.e_rls
23.109 [Celem.Calc ("Test.contains'_root",eval_contains_root"")], prls=Celem.e_rls, calc=[], crls=tval_rls,
23.110 errpats = [], nrls = Celem.e_rls(*,asm_rls=[], asm_thm=[("square_equation_left",""),
23.111 @@ -932,7 +932,7 @@
23.112 (["Test","square_equation2"],
23.113 [("#Given" ,["equality e_e","solveFor v_v"]),
23.114 ("#Find" ,["solutions v_v'i'"])],
23.115 - {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
23.116 + {rew_ord'="e_rew_ord",rls'=tval_rls,
23.117 srls = Celem.append_rls "srls_contains_root" Celem.e_rls
23.118 [Celem.Calc ("Test.contains'_root",eval_contains_root"")],
23.119 prls=Celem.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls(*,asm_rls=[],
23.120 @@ -957,7 +957,7 @@
23.121 (["Test","square_equation"],
23.122 [("#Given" ,["equality e_e","solveFor v_v"]),
23.123 ("#Find" ,["solutions v_v'i'"])],
23.124 - {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,
23.125 + {rew_ord'="e_rew_ord",rls'=tval_rls,
23.126 srls = Celem.append_rls "srls_contains_root" Celem.e_rls
23.127 [Celem.Calc ("Test.contains'_root",eval_contains_root"")],
23.128 prls=Celem.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Celem.e_rls (*,asm_rls=[],
23.129 @@ -986,7 +986,7 @@
23.130 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
23.131 "(matches ( v_v ^^^2 = 0) e_e)"]),
23.132 ("#Find" ,["solutions v_v'i'"])],
23.133 - {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,calc=[],srls=Celem.e_rls,
23.134 + {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Celem.e_rls,
23.135 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Celem.e_rls(*,
23.136 asm_rls=[],asm_thm=[]*)},
23.137 "Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
23.138 @@ -1001,7 +1001,7 @@
23.139 [("#Given",["equality e_e","solveFor v_v"]),
23.140 ("#Where" ,[]),
23.141 ("#Find" ,["solutions v_v'i'"])],
23.142 - {rew_ord'="xxxe_rew_ordxxx",rls'=tval_rls,srls = Celem.e_rls,prls=Celem.e_rls, calc=[], crls=tval_rls,
23.143 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls = Celem.e_rls,prls=Celem.e_rls, calc=[], crls=tval_rls,
23.144 errpats = [], nrls = Celem.e_rls},
23.145 "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
23.146 " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^
23.147 @@ -1014,7 +1014,7 @@
23.148 [("#Given" ,["intTestGiven t_t"]),
23.149 ("#Where" ,[]),
23.150 ("#Find" ,["intTestFind s_s"])],
23.151 - {rew_ord' = "xxxe_rew_ordxxx", rls' = tval_rls, srls = Celem.e_rls, prls = Celem.e_rls, calc = [],
23.152 + {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Celem.e_rls, prls = Celem.e_rls, calc = [],
23.153 crls = tval_rls, errpats = [], nrls = Test_simplify},
23.154 "Script STest_simplify (t_t::int) = " ^
23.155 "(Repeat " ^
24.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Thu Mar 15 15:48:52 2018 +0100
24.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Fri Mar 23 10:14:39 2018 +0100
24.3 @@ -306,15 +306,15 @@
24.4 (* prepare the input for an rls for use:
24.5 # generate a script for stepwise execution of the rls
24.6 # filter the operators for Calc out of the script ?WN111014?
24.7 - !!!use this function while storing by or integrate into KEStore_Elems.add_rlss.*)
24.8 -fun prep_rls _ Celem.Erls = error "prep_rls' not impl. for Erls"
24.9 + !!!use this function while storing (TODO integrate..) into KEStore_Elems.add_rlss *)
24.10 +fun prep_rls _ Celem.Erls = error "prep_rls: not required for Erls"
24.11 | prep_rls thy (Celem.Rls {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
24.12 let val sc = (rules2scr_Rls thy rules)
24.13 in Celem.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls,
24.14 srls = srls,
24.15 calc = get_calcs thy sc,
24.16 rules = rules,
24.17 - errpatts=errpatts,
24.18 + errpatts = errpatts,
24.19 scr = Celem.Prog sc} end
24.20 | prep_rls thy (Celem.Seq {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
24.21 let val sc = (rules2scr_Seq thy rules)
24.22 @@ -325,6 +325,6 @@
24.23 errpatts = errpatts,
24.24 scr = Celem.Prog sc} end
24.25 | prep_rls _ (Celem.Rrls {id, ...}) =
24.26 - error ("prep_rls' not required for Rrls \"" ^ id ^ "\"");
24.27 + error ("prep_rls: not required for Rrls \"" ^ id ^ "\"");
24.28
24.29 end
24.30 \ No newline at end of file
25.1 --- a/src/Tools/isac/calcelems.sml Thu Mar 15 15:48:52 2018 +0100
25.2 +++ b/src/Tools/isac/calcelems.sml Fri Mar 23 10:14:39 2018 +0100
25.3 @@ -195,7 +195,7 @@
25.4 val thm_of_thm: rule -> thm
25.5 val remove_rls: string -> rls -> rule list -> rls
25.6
25.7 -(*---------------------- ^^^ make public on a minimalist way down to Build?Isac -----------------
25.8 +(*---------------------- vvv^ make public for Test_Isac ------------------------------------
25.9 val Html_default: theID -> thydata
25.10 val a_term: term
25.11 val a_type: typ
25.12 @@ -204,7 +204,6 @@
25.13 val e_guh: guh
25.14 val e_kestoreID: string list
25.15 val e_met: met
25.16 - val e_pbt: pbt
25.17 val e_pbt_: pbt_
25.18 val e_rew_ord': rew_ord'
25.19 val e_rew_ord_: subst -> term * term -> bool
25.20 @@ -222,7 +221,6 @@
25.21 val insert_merge_rls: rlss_elem -> rlss_elem list -> rlss_elem list
25.22 val insthy: 'a -> 'b * 'c -> 'b * ('a * 'c)
25.23 val kestoreID2str: string list -> string
25.24 - val knowthys: unit -> theory list
25.25 val ldr2str: lrd -> string
25.26 val lim_rewrite: int Unsynchronized.ref
25.27 val memrls: rule -> rls -> bool
25.28 @@ -245,25 +243,27 @@
25.29 next_rule: rule list list -> term -> rule option, normal_form: term -> (term * term list) option, prepat: (term list * term) list, rew_ord: rew_ord}
25.30 val rep_thm_G': rule -> string * thm
25.31 val str2ketype: string -> ketype
25.32 - val string_of_thm: thm -> string
25.33 - val string_of_thm': theory -> thm -> string
25.34 val string_to_bool: string -> bool
25.35 type subs' = (cterm' * cterm') list
25.36 - val term_to_string'': thyID -> term -> string
25.37 - val terms2str': term list -> string
25.38 type thehier = thydata ptyp list
25.39 val theory2str': theory -> string
25.40 - val thm2str: thm -> string
25.41 eqtype thmDeriv
25.42 val thy2ctxt: theory -> Proof.context
25.43 val type_to_string': Proof.context -> typ -> string
25.44 val type_to_string'': thyID -> typ -> string
25.45 val type_to_string''': theory -> typ -> string
25.46 - ----------------------------------------- ^^^ make public -----------------------------------*)
25.47 + ---------------------- vvv^ make public for Test_Isac ------------------------------------*)
25.48 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
25.49 (* NONE *)
25.50 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
25.51 val terms2strs: term list -> string list
25.52 + val terms2str': term list -> string
25.53 + val term_to_string'': thyID -> term -> string
25.54 + val string_of_thm': theory -> thm -> string
25.55 + val string_of_thm: thm -> string
25.56 + val knowthys: unit -> theory list
25.57 + val thm2str: thm -> string
25.58 + val e_pbt: pbt
25.59 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
25.60 end
25.61
25.62 @@ -783,11 +783,12 @@
25.63 The association list is required for 'rewrite.."rew_ord"..'
25.64 WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
25.65 val rew_ord' = Unsynchronized.ref
25.66 - ([]:(rew_ord' * (*the key for the association list *)
25.67 - (subst (*the bound variables - they get high order*)
25.68 - -> (term * term) (*(t1, t2) to be compared *)
25.69 - -> bool)) (*if t1 <= t2 then true else false *)
25.70 - list); (*association list *)
25.71 + ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
25.72 + : (rew_ord' * (* the key for the association list *)
25.73 + (subst (* the bound variables - they get high order*)
25.74 + -> (term * term) (* (t1, t2) to be compared *)
25.75 + -> bool)) (* if t1 <= t2 then true else false *)
25.76 + list); (* association list *)
25.77
25.78 (* NOT ACCEPTED BY struct
25.79 rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),
26.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Thu Mar 15 15:48:52 2018 +0100
26.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Fri Mar 23 10:14:39 2018 +0100
26.3 @@ -191,7 +191,7 @@
26.4 writeln(authors2xml 2 "MATHAUTHORS"
26.5 ["isac-team 2001", "Richard Lang 2003"]);
26.6 *)
26.7 -fun scr2xml j EmptyScr =
26.8 +fun scr2xml j Celem.EmptyScr =
26.9 indt j ^"<SCRIPT> </SCRIPT>\n"
26.10 | scr2xml j (Celem.Prog term) =
26.11 if term = Celem.e_term
26.12 @@ -508,7 +508,7 @@
26.13 XML.Text term])])) = (ID, Rewrite.assoc_thm'' (Celem.Isac ()) ID)
26.14 | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
26.15
26.16 -fun xml_of_src EmptyScr =
26.17 +fun xml_of_src Celem.EmptyScr =
26.18 XML.Elem (("NOCODE", []), [XML.Text "empty"])
26.19 | xml_of_src (Celem.Prog term) =
26.20 XML.Elem (("CODE", []), [
27.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Thu Mar 15 15:48:52 2018 +0100
27.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Fri Mar 23 10:14:39 2018 +0100
27.3 @@ -121,6 +121,11 @@
27.4 *}
27.5
27.6 ML {*
27.7 +*} ML {*
27.8 +Celem.terms2strs (Ctree.get_assumptions_ pt p)
27.9 +*}
27.10 +
27.11 +ML {*
27.12 if Celem.terms2strs (Ctree.get_assumptions_ pt p) =
27.13 ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
27.14 then () else error "All_Ctx: asms after finishing SubProblem";
27.15 @@ -136,6 +141,11 @@
27.16 text {* assumptions collected during lucas-interpretation for proof of postcondition *}
27.17
27.18 ML {*
27.19 +*} ML {*
27.20 +Celem.terms2strs (Ctree.get_assumptions_ pt p)
27.21 +*}
27.22 +
27.23 +ML {*
27.24 if Celem.terms2strs (Ctree.get_assumptions_ pt p) =
27.25 ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
27.26 then () else error "All_Ctx at final result";
28.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
28.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Fri Mar 23 10:14:39 2018 +0100
28.3 @@ -0,0 +1,70 @@
28.4 +(* Title: 250-Rewrite_Set-from-method.sml
28.5 + Author: Walther Neuper 1803
28.6 + (c) copyright due to lincense terms.
28.7 +*)
28.8 +
28.9 +"----------- Minisubplb/250-Rewrite_Set-from-method.sml ----------";
28.10 +"----------- Minisubplb/250-Rewrite_Set-from-method.sml ----------";
28.11 +"----------- Minisubplb/250-Rewrite_Set-from-method.sml ----------";
28.12 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
28.13 +val (dI',pI',mI') =
28.14 + ("Test", ["sqroot-test","univariate","equation","test"],
28.15 + ["Test","squ-equ-test-subpbl1"]);
28.16 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
28.17 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28.18 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28.19 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28.20 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28.21 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28.22 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
28.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
28.25 +
28.26 +if p = ([1], Frm) andalso f = FormKF "x + 1 = 2" andalso fst nxt = "Rewrite_Set"
28.27 +then () else error "250-Rewrite_Set-from-method.sml: start of test CHANGED";
28.28 +
28.29 +(* isabisac17: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28.30 + f = FormKF "x + 1 + -1 * 2 = 0" ... OK
28.31 + nxt = ("Empty_Tac", Empty_Tac ... NOT ok *)
28.32 +"~~~~~ fun me, args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [], pt);
28.33 +val ("ok", (_, _, ptp)) = (*case*) locatetac tac (pt,p) (*of*);
28.34 + val (pt, p) = ptp;
28.35 +
28.36 +(* isabisac17: val ("helpless", _) = (*case*) step p ((pt, Ctree.e_pos'),[]) (*of*)*)
28.37 +"~~~~~ fun step, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
28.38 +val pIopt = get_pblID (pt,ip);
28.39 +(*if*) ip = ([], Ctree.Res) = false;
28.40 +val _ = (*case*) tacis (*of*);
28.41 +(*if*) ip = p = false;
28.42 +(*if*) member op = [Pbl, Met] p_ = false;
28.43 +
28.44 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
28.45 +e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
28.46 + val thy' = get_obj g_domID pt (par_pblobj pt p);
28.47 + val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
28.48 +
28.49 +(* isabisac17: val (tac_, is, (t, _)) = Lucin.next_tac (thy', srls) (pt, pos) sc is;
28.50 +go: no [L,L,R] *)
28.51 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Prog (_ $ body)),
28.52 + (ScrState (E,l,a,v,s,_), ctxt) ) = ((thy', srls), (pt, pos), sc, is);
28.53 +(*if*) l = [] = false;
28.54 +
28.55 +(* isabisac17: nstep_up thy ptp sc E l Skip_ a v ERROR go: no [L,L,R] *)
28.56 +(* isabisac15: val Appy (tac_, scrstate) = nstep_up thy ptp sc E l Skip_ a v *)
28.57 +"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
28.58 + (thy, ptp, sc, E, l, Skip_, a, v);
28.59 +1 < length l = true;
28.60 +val up = drop_last l;
28.61 +
28.62 +if up = [R, L, R, L, L, R] then () else error "250-Rewrite_Set: nstep_up CHANGED";
28.63 +(*isabisac17: nxt_up thy ptp (Celem.Prog sc) E up ay (go up sc) a v ERROR go: no [L,L,R]*)
28.64 +(*isabisac17: (go up sc) ERROR go: no [L,L,R]*)
28.65 +(*isabisac15:*)
28.66 +val ttt as Const ("Script.Try", _) $ (Const ("Script.Rewrite'_Set", _) $ Free ("norm_equation", _) $
28.67 + Const ("HOL.False", _)) = (go up sc)
28.68 +val (Const ("Script.Try"(*2*), _) $ _) = ttt;
28.69 +if term2str ttt = "Try (Rewrite_Set norm_equation False)"
28.70 +then () else error "250-Rewrite_Set: (go up sc) CHANGED";
28.71 +
28.72 +"~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, _, (Const ("Script.Try"(*2*), _) $ _), a, v) =
28.73 + (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v );
29.1 --- a/test/Tools/isac/ProgLang/calculate.sml Thu Mar 15 15:48:52 2018 +0100
29.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Fri Mar 23 10:14:39 2018 +0100
29.3 @@ -9,7 +9,8 @@
29.4 "-calculate.thy: provides 'setup' -----------------------";
29.5 "----------- fun norm -----------------------------------";
29.6 "----------- check return value of adhoc_thm ----";
29.7 -"----------- fun calculate_ -----------------------------";
29.8 +"----------- fun calculate_ --------------------------------------------------------------------";
29.9 +"----------- calculate from Prog --------------------------------- -----------------------------";
29.10 "----------- calculate from script --requires 'setup'----";
29.11 "----------- calculate check test-root-equ --------------";
29.12 "----------- check calcul,ate bottom up -----------------";
29.13 @@ -37,42 +38,41 @@
29.14 handle TERM _ =>
29.15 error "calculate.sml: adhoc_thm must return Trueprop";
29.16
29.17 -"----------- fun calculate_ -----------------------------";
29.18 -"----------- fun calculate_ -----------------------------";
29.19 -"----------- fun calculate_ -----------------------------";
29.20 +"----------- fun calculate_ --------------------------------------------------------------------";
29.21 +"----------- fun calculate_ --------------------------------------------------------------------";
29.22 +"----------- fun calculate_ --------------------------------------------------------------------";
29.23 +(* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
29.24 +val t = str2term "((1+2)*4/3)^^^2";
29.25 +val thy = @{theory};
29.26 +val times = ("Groups.times_class.times", eval_binop "#mult_") : string * eval_fn;
29.27 +val plus = ("Groups.plus_class.plus",eval_binop "#add_") : string * eval_fn;
29.28 +val divide = ("Rings.divide_class.divide" ,eval_cancel "#divide_e") : string * eval_fn;
29.29 +val pow = ("Atools.pow" ,eval_binop "#power_") : string * eval_fn;
29.30 +
29.31 +"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t);
29.32 +val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
29.33 +val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord e_rls true adh_thm t;
29.34 +if term2str t' = "(3 * 4 / 3) ^^^ 2" then () else error "calculate_ 1 + 2 = 3 changed";
29.35 +
29.36 +"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
29.37 +val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
29.38 +val SOME (t'', []) = rewrite__ thy 0 [] e_rew_ord e_rls true adh_thm t;
29.39 +if term2str t'' = "(12 / 3) ^^^ 2" then () else error "calculate_ 3 * 4 = 12 changed";
29.40 +
29.41 +"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
29.42 +val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
29.43 +val SOME (t''', []) = rewrite__ thy 0 [] e_rew_ord e_rls true adh_thm t;
29.44 +if term2str t''' = "4 ^^^ 2" then () else error "calculate_ 12 / 3 = 4 changed";
29.45 +
29.46 +"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
29.47 +val SOME ("#: 4 ^^^ 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
29.48 +val SOME (t'''', []) = rewrite__ thy 0 [] e_rew_ord e_rls true adh_thm t;
29.49 +if term2str t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed";
29.50 +
29.51 +"----------- calculate from Prog --------------------------------- -----------------------------";
29.52 +"----------- calculate from Prog --------------------------------- -----------------------------";
29.53 +"----------- calculate from Prog --------------------------------- -----------------------------";
29.54 val thy = @{theory "Test"};
29.55 -"===== test 1";
29.56 -val t = (Thm.term_of o the o (parse thy)) "1+2";
29.57 -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
29.58 -term2str (Thm.prop_of thm) = "1 + 2 = 3";
29.59 -
29.60 -"===== test 2";
29.61 -val t = (Thm.term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
29.62 -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
29.63 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
29.64 -if term2str t = "(3 * 4 / 3) ^^^ 2" then ()
29.65 -else error "calculate.sml: ((1+2)*4/3)^^^2 --> (3 * 4 / 3) ^^^ 2";
29.66 -
29.67 -"===== test 3b -- 2 contiued";
29.68 -val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES"))) t;
29.69 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
29.70 -term2str t;
29.71 -(*val it = "(#12 // #3) ^^^ #2" : string*)
29.72 -
29.73 -"===== test 4";
29.74 -val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"DIVIDE")))t;
29.75 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
29.76 -term2str t;
29.77 -(*it = "#4 ^^^ #2" : string*)
29.78 -
29.79 -"===== test 5";
29.80 -val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"POWER")))t;
29.81 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
29.82 -(*show_types := false;*)
29.83 -if term2str t <> "16" then error "calculate.sml: new behaviour in calculate_"
29.84 -else ();
29.85 -
29.86 -
29.87 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
29.88 val (dI',pI',mI') =
29.89 ("Test",["calculate","test"],["Test","test_calculate"]);
30.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Thu Mar 15 15:48:52 2018 +0100
30.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Fri Mar 23 10:14:39 2018 +0100
30.3 @@ -24,6 +24,7 @@
30.4 "----------- fun assoc_thm' -----------------------------";
30.5 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
30.6 "----------- fun mk_thm ------------------------------------------------------------------------";
30.7 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
30.8 "--------------------------------------------------------";
30.9 "--------------------------------------------------------";
30.10 "--------------------------------------------------------";
30.11 @@ -654,3 +655,17 @@
30.12
30.13 val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
30.14 if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
30.15 +
30.16 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
30.17 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
30.18 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
30.19 +(* norm_equation is defined in Test.thy, other rls see Knowledg/**)
30.20 +val thy = @{theory};
30.21 +val rls = norm_equation;
30.22 +val term = str2term "x + 1 = 2";
30.23 +
30.24 +val SOME (t, asm) = rewrite_set_ thy false rls term;
30.25 +if term2str t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
30.26 +
30.27 +"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
30.28 +"~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
31.1 --- a/test/Tools/isac/Test_Isac.thy Thu Mar 15 15:48:52 2018 +0100
31.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Mar 23 10:14:39 2018 +0100
31.3 @@ -146,6 +146,114 @@
31.4 ML_file "ProgLang/rewrite.sml"
31.5 ML_file "ProgLang/listC.sml"
31.6 ML_file "ProgLang/scrtools.sml"
31.7 +
31.8 +ML {*
31.9 +"~~~~~ fun xxx, args:"; val () = ();
31.10 +*} ML {*
31.11 +"-------- test the same called by interSteps norm_Poly -----------";
31.12 +"-------- test the same called by interSteps norm_Poly -----------";
31.13 +"-------- test the same called by interSteps norm_Poly -----------";
31.14 +val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
31.15 +writeln(term2str auto_script);
31.16 +(*Script Stepwise t_t =
31.17 + (Try (Rewrite_Set discard_minus False) @@
31.18 + Try (Rewrite_Set expand_poly_ False) @@
31.19 + Try (Repeat (Calculate TIMES)) @@
31.20 + Try (Rewrite_Set order_mult_rls_ False) @@
31.21 + Try (Rewrite_Set simplify_power_ False) @@
31.22 + Try (Rewrite_Set calc_add_mult_pow_ False) @@
31.23 + Try (Rewrite_Set reduce_012_mult_ False) @@
31.24 + Try (Rewrite_Set order_add_rls_ False) @@
31.25 + Try (Rewrite_Set collect_numerals_ False) @@
31.26 + Try (Rewrite_Set reduce_012_ False) @@
31.27 + Try (Rewrite_Set discard_parentheses1 False))
31.28 + ??.empty ..WORKS, NEVERTHELESS *)
31.29 +atomty auto_script;
31.30 +
31.31 +reset_states ();
31.32 +CalcTree
31.33 +[(["Term (b + a - b)", "normalform N"],
31.34 + ("Poly",["polynomial","simplification"],
31.35 + ["simplification","for_polynomials"]))];
31.36 +Iterator 1;
31.37 +moveActiveRoot 1;
31.38 +autoCalculate 1 CompleteCalc;
31.39 +
31.40 +val ((pt,p),_) = get_calc 1;
31.41 +show_pt pt;
31.42 +(* isabisac17 = 15 [
31.43 +(([], Frm), Simplify (b + a - b)),
31.44 +(([1], Frm), b + a - b),
31.45 +(([1], Res), a),
31.46 +(([], Res), a)] *)
31.47 +
31.48 +interSteps 1 ([], Res);
31.49 +val ((pt,p),_) = get_calc 1;
31.50 +show_pt pt;
31.51 +(* isabisac17 = 15 [
31.52 +(([], Frm), Simplify (b + a - b)),
31.53 +(([1], Frm), b + a - b),
31.54 +(([1], Res), a),
31.55 +(([], Res), a)] *)
31.56 +
31.57 +interSteps 1 ([1], Res);
31.58 +(*interSteps 1 ([1], Res)<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
31.59 +"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
31.60 + val ((pt, p), tacis) = get_calc cI;
31.61 +(*if*) (not o is_interpos) ip = false;
31.62 +val ip' = lev_pred' pt ip;
31.63 +
31.64 +(*Math_Engine.detailstep pt ip ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)
31.65 +"~~~~~ fun detailstep, args:"; val (pt, (pos as (p, _))) = (pt, ip);
31.66 + val nd = Ctree.get_nd pt p
31.67 + val cn = Ctree.children nd;
31.68 +(*if*) null cn = true;
31.69 +(*if*) (Tac.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)] = true;
31.70 +
31.71 +(*Solve.detailrls pt pos ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)
31.72 +"~~~~~ fun detailrls, args:"; val (pt, (pos as (p, _))) = (pt, pos);
31.73 + val t = get_obj g_form pt p
31.74 + val tac = get_obj g_tac pt p
31.75 + val rls = (assoc_rls o Tac.rls_of) tac
31.76 + val ctxt = get_ctxt pt pos
31.77 +val Seq _ = (*case*) rls (*of*);
31.78 +
31.79 +(* val is = Generate.init_istate tac t ..ERROR ,,>..>init_istate: "norm_Poly" has EmptyScr*)
31.80 +"~~~~~ fun init_istate, args:"; val ((Tac.Rewrite_Set rls), t) = (tac, t);
31.81 +val Celem.Seq {scr = Celem.Prog s,...} = (*case*) assoc_rls rls (*of*);
31.82 +
31.83 +"~~~~~ to detailrls return val:"; val is = (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, Celem.e_term, Selem.Sundef, true))
31.84 + val tac_ = Tac.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
31.85 + val pos' = ((lev_on o lev_dn) p, Ctree.Frm)
31.86 + val thy = Celem.assoc_thy "Isac"
31.87 + val (_, _, _, pt') = Generate.generate1 thy tac_ (is, ctxt) pos' pt (* implicit Take *)
31.88 + val (_,_, (pt'', _)) = complete_solve CompleteSubpbl [] (pt', pos')
31.89 + val newnds = children (get_nd pt'' p)
31.90 + val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*);
31.91 +
31.92 +"~~~~~ to detailstep return val:"; val xxx = ("detailrls", pt''', (p @ [length newnds], Res));
31.93 +"~~~~~ to interSteps return val:"; val ("detailrls", pt, lastpos) = xxx;
31.94 +show_pt pt;
31.95 +(*[
31.96 +(([], Frm), Simplify (b + a - b)),
31.97 +(([1], Frm), b + a - b),
31.98 +(([1,1], Frm), b + a - b),
31.99 +(([1,1], Res), b + a + -1 * b),
31.100 +(([1,2], Res), a + b + -1 * b),
31.101 +(([1,3], Res), a + 0 * b),
31.102 +(([1,4], Res), a),
31.103 +(([1], Res), a),
31.104 +(([], Res), a)]*)
31.105 +if existpt' ([1,4], Res) pt then ()
31.106 +else error "scrtools.sml: auto-generated norm_Poly doesnt work";
31.107 +*} ML {*
31.108 +*} ML {*
31.109 +*} ML {*
31.110 +*} ML {*
31.111 +*} ML {*
31.112 +"~~~~~ fun xxx, args:"; val () = ();
31.113 +*}
31.114 +
31.115 ML_file "ProgLang/tools.sml"
31.116 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
31.117 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
31.118 @@ -155,6 +263,7 @@
31.119 ML_file "Minisubpbl/100-init-rootpbl.sml"
31.120 ML_file "Minisubpbl/150-add-given.sml"
31.121 ML_file "Minisubpbl/200-start-method.sml"
31.122 + ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
31.123 ML_file "Minisubpbl/300-init-subpbl.sml"
31.124 ML_file "Minisubpbl/400-start-meth-subpbl.sml"
31.125 ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"