replace Prog. in prep_rls by Auto_Prog.gen, which generates Prog. on the fly
Note: introduction of funpack (see repository Jun 2019) enforced string encoded as char list;
since then (recursive) storing programs in rls (almost) blew up Build_Thydata.
1.1 --- a/src/Tools/isac/Interpret/li-tool.sml Sun Feb 09 16:55:41 2020 +0100
1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Mon Feb 10 17:01:49 2020 +0100
1.3 @@ -18,10 +18,8 @@
1.4 val init_pstate : Rule.rls -> Proof.context -> Model.itm list -> Celem.metID -> Istate.T * Proof.context * Program.T
1.5
1.6 val get_simplifier : Calc.T -> Rule.rls
1.7 -(*DEPR ^*)val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
1.8 - Rule.rls(*..\<in> ist*) * (Istate.T * Proof.context) * Program.T
1.9 -(*DEPR*)val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
1.10 - Rule.rls(*..\<in> ist*) * (Istate.T * Proof.context) * Program.T
1.11 + val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
1.12 + Rule.rls(*..\<in> ist \<rightarrow> REMOVE*) * (Istate.T * Proof.context) * Program.T
1.13 val rule2thm'' : Rule.rule -> Celem.thm''
1.14 val rule2rls' : Rule.rule -> string
1.15 val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Tactic.input list
1.16 @@ -32,9 +30,8 @@
1.17 val check_leaf : (*TODO190625: shift to lucas-interpreter.sml ? <- sel_rules, sel_appl_atomic_tacs !*)
1.18 string -> Proof.context -> Rule.rls -> (Env.T * (term option * term)) -> term ->
1.19 Program.leaf * term option
1.20 -
1.21 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.22 - (*NONE*)
1.23 + val de_esc_underscore: string -> string
1.24 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.25 val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
1.26 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.27 @@ -470,21 +467,22 @@
1.28 in srls end
1.29
1.30 (* decide, where to get program/istate from:
1.31 - (* 1 *) from PblObj.Env.update: at begin of program if no init_form
1.32 + (* 1 *) from PblObj: at begin of program if no init_form
1.33 (* 2 *) from PblObj/PrfObj: if Prog_Tac is in the middle of the program
1.34 - (* 3 *) from rls/PrfObj: in case of Math_Engine.detailstep *)
1.35 -fun from_pblobj_or_detail' _ (p, p_) pt =
1.36 - if member op = [Pbl, Met] p_
1.37 - then case get_obj g_env (*?DEPRECATED?*) pt p of
1.38 - NONE => error "from_pblobj_or_detail': no istate"
1.39 - | SOME (Istate.Pstate pst, ctxt) =>
1.40 - let
1.41 - val metID = get_obj g_metID pt p
1.42 - val {srls, ...} = Specify.get_met metID
1.43 - in
1.44 - (srls, (Istate.Pstate (Istate.set_eval srls pst), ctxt), (#scr o Specify.get_met) metID)
1.45 - end
1.46 - | _ => raise ERROR "from_pblobj_or_detail': unexpected result from g_env"
1.47 + (* 3 *) from PrfOb: in case of Math_Engine.detailstep
1.48 + *)
1.49 +fun from_pblobj_or_detail' thy (p, p_) pt =
1.50 + if Pos.on_specification p_ (* 1 *)
1.51 + then case get_obj g_env (*!DEPRECATED!*) pt p of
1.52 + NONE => error "from_pblobj_or_detail': no istate"
1.53 + | SOME (Istate.Pstate pst, ctxt) =>
1.54 + let
1.55 + val metID = get_obj g_metID pt p
1.56 + val {srls, ...} = Specify.get_met metID
1.57 + in
1.58 + (srls, (Istate.Pstate (Istate.set_eval srls pst), ctxt), (#scr o Specify.get_met) metID)
1.59 + end
1.60 + | _ => raise ERROR "from_pblobj_or_detail': unexpected result from g_env"
1.61 else
1.62 let val (pbl, p', rls') = par_pbl_det pt p
1.63 in if pbl
1.64 @@ -497,37 +495,12 @@
1.65 (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
1.66 | _ => raise ERROR "from_pblobj_or_detail': unexpected result from get_loc"
1.67 in (srls, (is, ctxt), (#scr o Specify.get_met) metID) end
1.68 - else
1.69 - let
1.70 - (*TODO.thy Auto_Prog.generate SHOULD REPLACE ALL HIS..*)
1.71 - val prog = case rls' of
1.72 - Rule.Rls {scr = Rule.Prog prog,...} => prog
1.73 - | Rule.Seq {scr = Rule.Prog prog,...} => prog
1.74 - | _ => raise ERROR ("from_pblobj_or_detail': not for rule-set \"" ^ Rule.id_rls rls' ^ "\"")
1.75 - val t = get_last_formula (pt, (p, p_))
1.76 - val prog' = Auto_Prog.subst_typs prog (type_of t) (TermC.guess_bdv_typ t)
1.77 - in (Rule.e_rls(*!!!*), get_loc pt (p, p_), Rule.Prog prog') end
1.78 + else (* 3 *)
1.79 + (Rule.e_rls(*!!!*),
1.80 + get_loc pt (p, p_),
1.81 + Rule.Prog (Auto_Prog.gen (Celem.assoc_thy thy) (get_last_formula (pt, (p, p_))) rls'))
1.82 end
1.83
1.84 -fun from_pblobj' thy' (p,p_) pt = (*.get script and istate, UNUSED; see above ( * 1 *)
1.85 - let
1.86 - val p' = par_pblobj pt p
1.87 - val itms =
1.88 - (case get_obj I pt p' of
1.89 - PblObj {meth = itms, ...} => itms
1.90 - | PrfObj _ => error "from_pblobj' NOT with PrfObj")
1.91 - val metID = get_obj g_metID pt p'
1.92 - val {srls, scr, ...} = Specify.get_met metID
1.93 - in
1.94 - if last_elem p = 0 (*nothing written to pt yet*)
1.95 - then
1.96 - let
1.97 - val ctxt = ContextC.initialise thy' (Model.vars_of itms)
1.98 - val (is, ctxt, scr) = init_pstate srls ctxt itms metID
1.99 - in (srls(*..\<in> is*), (is, ctxt), scr) end
1.100 - else (srls(*..\<in> is*), get_loc pt (p,p_), scr)
1.101 - end;
1.102 -
1.103 (* handle a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr. *)
1.104 fun check_leaf call ctxt srls (E, (a, v)) t =
1.105 case Prog_Tac.eval_leaf E a v t of
2.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Sun Feb 09 16:55:41 2020 +0100
2.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Mon Feb 10 17:01:49 2020 +0100
2.3 @@ -49,9 +49,7 @@
2.4 Rls {calc = [], erls = Erls, errpatts = [], id = "e_rls", preconds = [], rew_ord =
2.5 ("dummy_ord", _), rules = [], scr = EmptyScr, srls = Erls},
2.6 errpatts = [], id = "rls111", preconds = [], rew_ord = ("termlessI", _), rules =
2.7 - [Thm ("thm111", _), Thm ("refl", _)], scr =
2.8 - Prog (Const ("HOL.eq", _) $ (Const ("Auto_Prog.auto_generated", _) $ Free ("t_t", _)) $ _),
2.9 - srls = Erls})) => ()
2.10 + [Thm ("thm111", _), Thm ("refl", _)], scr = EmptyScr, srls = Erls})) => ()
2.11 | _ => error "test/../thy-hierarchy CHANGED 4";
2.12 \<close> ML \<open>
2.13 case eee of
2.14 @@ -61,10 +59,7 @@
2.15 Rls {calc = [], erls = Erls, errpatts = [], id = "e_rls", preconds = [], rew_ord =
2.16 ("dummy_ord", _), rules = [], scr = EmptyScr, srls = Erls},
2.17 errpatts = [], id = "rls222", preconds = [], rew_ord = ("termlessI", _), rules =
2.18 - [Thm ("sym_thm111", _), Thm ("o_def", _)],
2.19 - scr =
2.20 - Prog (Const ("HOL.eq", _) $ (Const ("Auto_Prog.auto_generated", _) $ Free ("t_t", _)) $ _),
2.21 - srls = Erls})) => ()
2.22 + [Thm ("sym_thm111", _), Thm ("o_def", _)], scr = EmptyScr, srls = Erls})) => ()
2.23 | _ => error "test/../thy-hierarchy CHANGED 5";
2.24 \<close>
2.25
3.1 --- a/src/Tools/isac/MathEngine/solve.sml Sun Feb 09 16:55:41 2020 +0100
3.2 +++ b/src/Tools/isac/MathEngine/solve.sml Mon Feb 10 17:01:49 2020 +0100
3.3 @@ -59,7 +59,7 @@
3.4 if p = ([], Res)
3.5 then ("end-of-calculation", [], ptp)
3.6 else
3.7 - if member op = [Pbl,Met] p_
3.8 + if member op = [Pbl, Met] p_
3.9 then
3.10 let
3.11 val ptp = Chead.all_modspec ptp
3.12 @@ -99,7 +99,8 @@
3.13 (append_atomic [] (Istate.e_istate, ContextC.e_ctxt) t (Tactic.rule2tac thy [] rule) res Complete EmptyPtree) ::
3.14 (rul_terms_2nds thy nds t' rts);
3.15
3.16 -(* detail steps done internally by Rewrite_Set* into ctree by use of a script *)
3.17 +(* detail steps done internally by Rewrite_Set* into Ctree
3.18 + by use of a program *)
3.19 fun detailrls pt (pos as (p, _)) =
3.20 let
3.21 val t = get_obj g_form pt p
3.22 @@ -117,8 +118,6 @@
3.23 | _ =>
3.24 let
3.25 val is = Generate.init_istate tac t
3.26 - (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
3.27 - is wrong for simpl, but working ?!? *)
3.28 val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
3.29 val pos' = ((lev_on o lev_dn) p, Frm)
3.30 val thy = Celem.assoc_thy "Isac_Knowledge"
4.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Sun Feb 09 16:55:41 2020 +0100
4.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Mon Feb 10 17:01:49 2020 +0100
4.3 @@ -34,6 +34,7 @@
4.4 val op_of_calc: term -> string
4.5 val get_calcs: theory -> term -> (Rule.prog_calcID * (Rule.calID * Rule.eval_fn)) list
4.6 val prep_rls: theory -> Rule.rls -> Rule.rls (*ren insert*)
4.7 + val gen: theory -> term -> Rule.rls -> term
4.8 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.9 (* NONE *)
4.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.11 @@ -201,30 +202,47 @@
4.12 then FunID_Term_Bdv $ (((#> o (map (rule2stac_inst thy))) rules) $ Rule.e_term)
4.13 else FunID_Term $ (((#> o (map (rule2stac thy))) rules) $ Rule.e_term);
4.14
4.15 -(* prepare the input for an rls for use:
4.16 - # generate a script for stepwise execution of the rls
4.17 +(* REPLACED BY Auto_Prog.gen:
4.18 + prepare the input for an rls for use:
4.19 + # generate a program for stepwise execution of the rls
4.20 # filter the operators for Num_Calc out of the script ?WN111014?
4.21 - !!!use this function while storing (TODO integrate..) into KEStore_Elems.add_rlss *)
4.22 + use this function while storing (TODO integrate..) into KEStore_Elems.add_rlss
4.23 +*)
4.24 fun prep_rls _ Rule.Erls = error "prep_rls: not required for Erls"
4.25 | prep_rls thy (Rule.Rls {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
4.26 - let val sc = (rules2scr_Rls thy rules)
4.27 - in Rule.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls,
4.28 - srls = srls,
4.29 - calc = get_calcs thy sc,
4.30 - rules = rules,
4.31 - errpatts = errpatts,
4.32 - scr = Rule.Prog sc} end
4.33 + let
4.34 + val sc = (rules2scr_Rls thy rules)
4.35 + in
4.36 + Rule.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
4.37 + calc = get_calcs thy sc,
4.38 + rules = rules, errpatts = errpatts,
4.39 + scr = Rule.EmptyScr (*Rule.Prog sc AD-HOC REPLACED BY Auto_Prog.gen*)} end
4.40 | prep_rls thy (Rule.Seq {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
4.41 - let val sc = (rules2scr_Seq thy rules)
4.42 - in Rule.Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls,
4.43 - srls = srls,
4.44 - calc = get_calcs thy sc,
4.45 - rules = rules,
4.46 - errpatts = errpatts,
4.47 - scr = Rule.Prog sc} end
4.48 + let
4.49 + val sc = (rules2scr_Seq thy rules)
4.50 + in
4.51 + Rule.Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
4.52 + calc = get_calcs thy sc,
4.53 + rules = rules, errpatts = errpatts,
4.54 + scr = Rule.EmptyScr (*Rule.Prog sc AD-HOC REPLACED BY Auto_Prog.gen*)} end
4.55 | prep_rls _ (Rule.Rrls {id, ...}) =
4.56 error ("prep_rls: not required for Rrls \"" ^ id ^ "\"");
4.57
4.58 +(* on the fly generate a Prog from an rls for Math_Engine.detailstep.
4.59 + Note: introduction of funpack (see repository Jun 2019) enforced string encoded as char list;
4.60 + since then (recursive) storing programs in rls (almost) blew up Build_Thydata.
4.61 + Arg. thy is required for (assoc_calc thy c); drop with better acces to Thydata?
4.62 +*)
4.63 +fun gen thy t rls =
4.64 + let
4.65 + val prog = case rls of
4.66 + Rule.Rls {rules, ...} => rules2scr_Rls thy rules
4.67 + | Rule.Seq {rules, ...} => rules2scr_Seq thy rules
4.68 + | _ => raise ERROR ("Auto_Prog.gen: not for rule-set \"" ^ Rule.id_rls rls ^ "\"")
4.69 + in
4.70 + subst_typs prog (type_of t) (TermC.guess_bdv_typ t)
4.71 + end
4.72 +
4.73 (**)end(**)
4.74 \<close> ML \<open>
4.75 \<close> ML \<open>
5.1 --- a/src/Tools/isac/Specify/generate.sml Sun Feb 09 16:55:41 2020 +0100
5.2 +++ b/src/Tools/isac/Specify/generate.sml Mon Feb 10 17:01:49 2020 +0100
5.3 @@ -44,39 +44,25 @@
5.4 open Ctree
5.5 open Pos
5.6
5.7 -(* initialize istate for Detail_Set TODO remove with *_Detail*)
5.8 +(* initialize istate for Detail_Set *)
5.9 fun init_istate (Tactic.Rewrite_Set rls) t =
5.10 - (case assoc_rls rls of
5.11 - Rule.Rrls {scr = Rule.Rfuns {init_state = ii, ...}, ...} => Istate_Def.RrlsState (ii t)
5.12 - | Rule.Rls {scr = Rule.EmptyScr, ...} =>
5.13 - error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
5.14 - "use prep_rls' for storing rule-sets !")
5.15 - | Rule.Rls {scr = Rule.Prog s, ...} =>
5.16 - (Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true [(hd (Program.formal_args s), t)]))
5.17 - | Rule.Seq {scr = Rule.EmptyScr,...} =>
5.18 - error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
5.19 - " Use prep_rls' for storing rule-sets !")
5.20 - | Rule.Seq {scr = Rule.Prog s,...} =>
5.21 - (Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true [(hd (Program.formal_args s), t)]))
5.22 - | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")
5.23 + let
5.24 + val thy = Celem.assoc_thy "Isac_Knowledge"
5.25 + val args = Auto_Prog.gen thy t (assoc_rls rls) |> Program.formal_args
5.26 + in
5.27 + Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true [(hd args, t)])
5.28 + end
5.29 | init_istate (Tactic.Rewrite_Set_Inst (subs, rls)) t =
5.30 let
5.31 - val v = case Selem.subs2subst (Celem.assoc_thy "Isac_Knowledge") subs of
5.32 - (_, v) :: _ => v
5.33 - | _ => error "init_istate: uncovered case "
5.34 - (*...we suppose the substitution of only _one_ bound variable*)
5.35 - in case assoc_rls rls of
5.36 - Rule.Rls {scr = Rule.EmptyScr, ...} =>
5.37 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
5.38 - "use prep_rls' for storing rule-sets !")
5.39 - | Rule.Rls {scr = Rule.Prog s, ...} =>
5.40 - Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true ((Program.formal_args s) ~~ [t, v]))
5.41 - | Rule.Seq {scr = Rule.EmptyScr, ...} =>
5.42 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
5.43 - "use prep_rls' for storing rule-sets !")
5.44 - | Rule.Seq {scr = Rule.Prog s,...} =>
5.45 - Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true ((Program.formal_args s) ~~ [t, v]))
5.46 - | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls"
5.47 + val thy = Celem.assoc_thy "Isac_Knowledge"
5.48 + val rls' = assoc_rls rls
5.49 + val v = case Selem.subs2subst thy subs of
5.50 + (_, v) :: _ => v (*...we suppose the substitution of only ONE bound variable*)
5.51 + | _ => raise ERROR "init_istate: uncovered case"
5.52 + val prog = Auto_Prog.gen thy t rls'
5.53 + val args = Program.formal_args prog
5.54 + in
5.55 + Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true (args ~~ [t, v]))
5.56 end
5.57 | init_istate tac _ = error ("init_istate: uncovered definition for " ^ Tactic.tac2str tac)
5.58
6.1 --- a/src/Tools/isac/TODO.thy Sun Feb 09 16:55:41 2020 +0100
6.2 +++ b/src/Tools/isac/TODO.thy Mon Feb 10 17:01:49 2020 +0100
6.3 @@ -24,13 +24,14 @@
6.4 subsection \<open>Current changeset\<close>
6.5 text \<open>
6.6 \begin{itemize}
6.7 - \item xxx
6.8 \item xxx
6.9 + \item collect from_pblobj_or_detail*,
6.10 + -> Rule.rls(*..\<in> ist \<rightarrow> REMOVE*) * (Istate.T * Proof.context) * Program.T
6.11 + \item init_istate ?-> Detail_Rls?
6.12 \item xxx
6.13 - \item xxx
6.14 - \item xxx
6.15 \item xxx
6.16 - \item xxx
6.17 + \item xxx
6.18 + \item xxx
6.19 \item xxx
6.20 \item xxx
6.21 \item xxx
6.22 @@ -51,18 +52,12 @@
6.23 text \<open>
6.24 \begin{itemize}
6.25 \item xxx
6.26 + \item xxx
6.27 + \item xxx
6.28 + \item xxx
6.29 \item generate, generate1: NO thy as arg.
6.30 - \item xxx
6.31 - \item decompose do_next, by_tactic: mutual recursion only avoids multiple generate1
6.32 - ! ^^^ in find_next_step --- ? ? ? in locate_input_tactic ?
6.33 - \item xxx
6.34 \item Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
6.35 \item xxx
6.36 - \item NEW structure Step.applicable Step.add
6.37 - ^applicable_in ^generate1
6.38 - \item xxx
6.39 - \item revise Pstate {or, ...}; strange occurrence in program without Tactical.Or documented here
6.40 - \item xxx
6.41 \item shift tests into NEW model.sml (upd, upds_envv, ..)
6.42 \item xxx
6.43 \item xxx
6.44 @@ -97,25 +92,6 @@
6.45 \item complete mstools.sml (* survey on handling contexts:
6.46 \item xxx
6.47 \item xxx
6.48 - \item istate
6.49 - \begin{itemize}
6.50 - \item datatype L,R,D --> Istate
6.51 - \item xxx
6.52 - \item xxx
6.53 - \item xxx
6.54 - \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
6.55 - \item xxx
6.56 - \item pstate2str --> pstate2str
6.57 - \item xxx
6.58 - \item after review of Rrls, detail ?-->? istate
6.59 - \item locate_input_tactic: get_simplifier cstate (*TODO: shift to init_istate*)
6.60 - \item xxx
6.61 - \item push srls into pstate
6.62 - \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule.e_rls)
6.63 - ^^^^^^^^^^
6.64 - \item xxx
6.65 - \item xxx
6.66 - \end{itemize}
6.67 \item xxx
6.68 \item trace_script: replace ' by " in writeln
6.69 \item xxx
6.70 @@ -444,11 +420,18 @@
6.71 let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*)
6.72 \item xxx
6.73 \item xxx
6.74 + \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
6.75 + \item locate_input_tactic: get_simplifier cstate (*TODO: shift to init_istate*)
6.76 + \item push srls into pstate
6.77 + \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule.e_rls)
6.78 + ^^^^^^^^^^
6.79 \item xxx
6.80 \end{itemize}
6.81 \<close>
6.82 subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>
6.83 text \<open>
6.84 +remove Rfuns -> Rule.Prog, Rule.EmptyScr
6.85 +consider separating spec.funs. to ?Inter_Steps?
6.86 \begin{itemize}
6.87 \item removing from_pblobj_or_detail' causes many strange errors
6.88 \item ^^^+ see from_pblobj_or_detail_thm, from_pblobj_or_detail_calc, ...
6.89 @@ -497,17 +480,7 @@
6.90 two issues:
6.91 (1) fun prep_rls creates a Program with too general and wrong types.
6.92 (2) generated Programs (huge since strings are coded in ASCII) stored in rls drives
6.93 - Build_Thydata towards limits of resources.
6.94 - \begin{itemize}
6.95 - \item rename Auto_Prog.prep_rls --> Auto_Prog.generate
6.96 - \item Auto_Prog.generate : term -> rls -> (*Program*)term
6.97 - Ctree.current_formula---^^^^
6.98 - \item xxx
6.99 - \item xxx
6.100 - \item generate Program on demand in from_pblobj_or_detail'
6.101 - \item xxx
6.102 - \item xxx
6.103 - \end{itemize}
6.104 + Build_Thydata towards limits of resources. ...............................................DONE
6.105 \<close>
6.106 subsection \<open>Redesign thms for equation solver\<close>
6.107 text \<open>
7.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sun Feb 09 16:55:41 2020 +0100
7.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Mon Feb 10 17:01:49 2020 +0100
7.3 @@ -1,5 +1,4 @@
7.4 -(* Title: "xmlsrc/thy-hierarchy.sml"
7.5 - tests for xmlsrc/thy-hierarchy.sml
7.6 +(* Title: "BridgeLibisabelle/thy-hierarchy.sml"
7.7 Authors: Walther Neuper 060113
7.8 (c) due to copyright terms
7.9
7.10 @@ -258,11 +257,14 @@
7.11 " <STRING> e_rls </STRING>\n" ^
7.12 " <GUH> thy_isac_Poly-rls-e_rls </GUH>\n" ^
7.13 " </SRLS>\n" ^
7.14 +" <SCRIPT> </SCRIPT>\n" ^
7.15 +(*
7.16 " <SCRIPT>\n" ^
7.17 " <MATHML>\n" ^
7.18 " <ISA> auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''distrib_right'')) #>\n Try (Repeat (Rewrite ''distrib_left'')))\n ??.empty) </ISA>\n" ^
7.19 " </MATHML>\n" ^
7.20 " </SCRIPT>\n" ^
7.21 +*)
7.22 " </RULESET>\n" ^
7.23 " <EXPLANATIONS> </EXPLANATIONS>\n" ^
7.24 " <MATHAUTHORS>\n" ^
8.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sun Feb 09 16:55:41 2020 +0100
8.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Feb 10 17:01:49 2020 +0100
8.3 @@ -120,7 +120,7 @@
8.4 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
8.5 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
8.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
8.7 - val (_, is, sc) = LItool.from_pblobj' thy' (p,p_) pt;
8.8 + val (_, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
8.9
8.10 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
8.11 "~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
9.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Sun Feb 09 16:55:41 2020 +0100
9.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon Feb 10 17:01:49 2020 +0100
9.3 @@ -88,8 +88,9 @@
9.4 val ctxt = get_ctxt pt pos
9.5 val _ = (*case*) rls (*of*);
9.6 val is = Generate.init_istate tac t
9.7 - (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
9.8 - is wrong for simpl, but working ?!? *)
9.9 +
9.10 +(*+*)val Rls {scr = EmptyProg, ...} = rls; (*this prog is replaced by Auto_Prog.gen on the fly*)
9.11 +
9.12 val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
9.13 val pos' = ((lev_on o lev_dn) p, Frm)
9.14 val thy = Celem.assoc_thy "Isac_Knowledge"
9.15 @@ -101,7 +102,9 @@
9.16 = (CompleteSubpbl, [], (pt', pos'));
9.17 (*if*) p = ([], Res) (*else*);
9.18 (*if*) member op = [Pbl,Met] p_ (*else*);
9.19 - val (_, ([(Rewrite ("radd_commute", _), _, _)], c', ptp')) = (*case*)Step_Solve.do_next ptp (*of*);
9.20 +
9.21 + val (_, ([(Rewrite ("radd_commute", _), _, _)], c', ptp')) =
9.22 + (*case*) Step_Solve.do_next ptp (*of*);
9.23
9.24 (*+*)c' = [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)];
9.25 (*+*)show_pt (fst ptp');(*[
9.26 @@ -111,7 +114,14 @@
9.27 (([2,1], Frm), x + 1 + -1 * 2 = 0),
9.28 (([2,1], Res), 1 + x + -1 * 2 = 0)]*)
9.29
9.30 - (** )val (_, c', ptp') =( **)
9.31 +(*+*)val (keep_c', keep_ptp') = (c', ptp');
9.32 +"~~~~~ and Step_Solve.do_next , args:"; val () = ();
9.33 +(*+*)(*STOPPED HERE:
9.34 + NOTE: prog.xxx found by LItool.from_pblobj_or_detail' from Rls {scr = Prog xxx, ...}*)
9.35 +
9.36 +(*+*)val (c', ptp') = (keep_c', keep_ptp');
9.37 +
9.38 + (** )val (_, c', ptp') =( **)
9.39 complete_solve auto (c @ c') ptp';
9.40 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))
9.41 = (auto, (c @ c'), ptp');
9.42 @@ -141,6 +151,8 @@
9.43 val ("detailrls", pt, _) = (*case*) Math_Engine.detailstep pt''''' ip (*of*);
9.44
9.45 show_pt pt; (* added ([3,1,1], Frm), ([3,1,1], Res) after ([3,1], Frm)*)
9.46 +
9.47 +(*---------- final test ----------------------------------------------------------\\*)
9.48 if pr_ctree pr_short pt =
9.49 ". ----- pblobj -----\n1" ^
9.50 ". x + 1 = 2\n" ^
10.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Sun Feb 09 16:55:41 2020 +0100
10.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Mon Feb 10 17:01:49 2020 +0100
10.3 @@ -13,7 +13,7 @@
10.4 "-------- fun op #> ----------------------------------------------------------------------------";
10.5 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
10.6 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
10.7 -"-------- fun stacpbls -------------------------------------------------------------------------";
10.8 +"-------- fun stacpbls, fun eval_leaf -----------------------------------";
10.9 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
10.10 "-------- fun subst_typ ------------------------------------------------------------------------";
10.11 "-------- fun subst_typs -----------------------------------------------------------------------";
10.12 @@ -26,36 +26,62 @@
10.13 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
10.14 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
10.15 val rls = assoc_rls "integration";
10.16 -val Seq {scr = Prog auto_script,...} = rls;
10.17 -writeln(term2str auto_script);
10.18 +val thy' = @{theory "Integrate"}
10.19 +val t = @{term "ttt :: real"};
10.20 +
10.21 + Auto_Prog.gen thy' t rls;
10.22 +"~~~~~ fun generate , args:"; val (thy, t, rls) = (thy', t, rls);
10.23 + val prog = case rls of
10.24 + Rule.Rls {rules, ...} => rules2scr_Rls thy rules
10.25 + | Rule.Seq {rules, ...} => rules2scr_Seq thy rules
10.26 + val auto_script = subst_typs prog (type_of t) (TermC.guess_bdv_typ t) (*return from generate*);
10.27 +
10.28 +if term2str auto_script =
10.29 + "auto_generated_inst t_t v =\n" ^
10.30 + "(Try (Rewrite_Set_Inst [(''bdv'', v)] ''integration_rules'') #>\n" ^
10.31 + " Try (Rewrite_Set_Inst [(''bdv'', v)] ''add_new_c'') #>\n" ^
10.32 + " Try (Rewrite_Set_Inst [(''bdv'', v)] ''simplify_Integral''))\n" ^
10.33 + " ??.empty"
10.34 +then () else error "Auto_Prog.gen integration CHANGED";
10.35
10.36 if contain_bdv (get_rules rls) then ()
10.37 else error "scrtools.sml: contain_bdv doesnt work for 'integration'";
10.38
10.39 if terms2str (formal_args auto_script) = "[\"t_t\",\"v\"]"
10.40 then () else error "formal_args of auto-gen.script changed";
10.41 -init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules"))
10.42 - (str2term "someTermWithBdv");
10.43 +
10.44 + init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules"))
10.45 + (str2term "someTermWithBdv");
10.46 +"~~~~~ fun init_istate , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)
10.47 + = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), str2term "someTermWithBdv");
10.48 + val v = case Selem.subs2subst (Celem.assoc_thy "Isac_Knowledge") subs of
10.49 + (_, v) :: _ => v;
10.50 + (*case*) assoc_rls rls (*of*);
10.51 +
10.52
10.53 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
10.54 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
10.55 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
10.56 -val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
10.57 -writeln(term2str auto_script);
10.58 -(*Program Stepwise t_t =
10.59 - (Try (Rewrite_Set discard_minus) #>
10.60 - Try (Rewrite_Set expand_poly_) #>
10.61 - Try (Repeat (Calculate TIMES)) #>
10.62 - Try (Rewrite_Set order_mult_rls_) #>
10.63 - Try (Rewrite_Set simplify_power_) #>
10.64 - Try (Rewrite_Set calc_add_mult_pow_) #>
10.65 - Try (Rewrite_Set reduce_012_mult_) #>
10.66 - Try (Rewrite_Set order_add_rls_) #>
10.67 - Try (Rewrite_Set collect_numerals_) #>
10.68 - Try (Rewrite_Set reduce_012_) #>
10.69 - Try (Rewrite_Set discard_parentheses1))
10.70 - ??.empty ..WORKS, NEVERTHELESS *)
10.71 -atomty auto_script;
10.72 +val rls = assoc_rls "norm_Poly";
10.73 +val thy' = @{theory "Poly"}
10.74 +val t = @{term "ttt :: real"}
10.75 +val auto_script = Auto_Prog.gen thy' t rls;
10.76 +
10.77 +if term2str auto_script =
10.78 + "auto_generated t_t =\n" ^
10.79 + "(Try (Rewrite_Set ''discard_minus'') #>\n" ^
10.80 + " Try (Rewrite_Set ''expand_poly_'') #>\n" ^
10.81 + " Try (Repeat (Calculate ''TIMES'')) #>\n" ^
10.82 + " Try (Rewrite_Set ''order_mult_rls_'') #>\n" ^
10.83 + " Try (Rewrite_Set ''simplify_power_'') #>\n" ^
10.84 + " Try (Rewrite_Set ''calc_add_mult_pow_'') #>\n" ^
10.85 + " Try (Rewrite_Set ''reduce_012_mult_'') #>\n" ^
10.86 + " Try (Rewrite_Set ''order_add_rls_'') #>\n" ^
10.87 + " Try (Rewrite_Set ''collect_numerals_'') #>\n" ^
10.88 + " Try (Rewrite_Set ''reduce_012_'') #>\n" ^
10.89 + " Try (Rewrite_Set ''discard_parentheses1''))\n" ^
10.90 + " ??.empty" (* ..WORKS, NEVERTHELESS*)
10.91 +then () else error "Auto_Prog.gen norm_Poly CHANGED";
10.92
10.93 reset_states (); (*<-- evaluate, if ML-blocks are edited below*)
10.94 CalcTree
10.95 @@ -116,10 +142,12 @@
10.96 if existpt' ([1,4], Res) pt then ()
10.97 else error "auto-generated norm_Poly doesnt work";
10.98
10.99 +
10.100 "-------- test the same called by interSteps norm_Rational -------------------------------------";
10.101 "-------- test the same called by interSteps norm_Rational -------------------------------------";
10.102 "-------- test the same called by interSteps norm_Rational -------------------------------------";
10.103 -val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Rational";
10.104 +val auto_script =
10.105 + Auto_Prog.gen @{theory "Poly"} @{term "ttt :: real"} (assoc_rls "norm_Rational");
10.106 writeln(term2str auto_script);
10.107 atomty auto_script;
10.108 (***
10.109 @@ -174,6 +202,7 @@
10.110 ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
10.111 | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
10.112
10.113 +
10.114 "-------- fun op #> ----------------------------------------------------------------------------";
10.115 "-------- fun op #> ----------------------------------------------------------------------------";
10.116 "-------- fun op #> ----------------------------------------------------------------------------";
10.117 @@ -188,6 +217,7 @@
10.118 "Try (Repeat (Rewrite ''risolate_root_div''))"
10.119 then () else error "fun #> changed"
10.120
10.121 +
10.122 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
10.123 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
10.124 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
10.125 @@ -208,6 +238,7 @@
10.126 " ??.empty)"
10.127 then () else error "rules2scr_Rls auto_generated changed";
10.128
10.129 +
10.130 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
10.131 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
10.132 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
10.133 @@ -241,9 +272,10 @@
10.134 else error "rule2stac_inst changed 1")
10.135 | _ => error "rule2stac_inst changed 2";
10.136
10.137 -"-------- fun stacpbls -------------------------------------------------------------------------";
10.138 -"-------- fun stacpbls -------------------------------------------------------------------------";
10.139 -"-------- fun stacpbls -------------------------------------------------------------------------";
10.140 +
10.141 +"-------- fun stacpbls, fun eval_leaf -----------------------------------";
10.142 +"-------- fun stacpbls, fun eval_leaf -----------------------------------";
10.143 +"-------- fun stacpbls, fun eval_leaf -----------------------------------";
10.144 val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
10.145 case stacpbls sc of
10.146 [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
10.147 @@ -271,11 +303,12 @@
10.148 @{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
10.149 case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
10.150
10.151 +
10.152 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
10.153 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
10.154 "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
10.155 val rls = prep_rls @{theory} Test_simplify; (* adds the Program *)
10.156 -val Prog sc = (#scr o rep_rls) rls;
10.157 +val sc = Auto_Prog.gen thy' t rls;
10.158 val stacs = stacpbls sc;
10.159
10.160 val calcs = filter is_calc stacs;
10.161 @@ -291,10 +324,11 @@
10.162 ("DIVIDE", ("Rings.divide_class.divide", _)), ("POWER", ("Prog_Expr.pow", _))] => ()
10.163 | _ => error "get_calcs changed"
10.164
10.165 +
10.166 "-------- fun subst_typ ------------------------------------------------------------------------";
10.167 "-------- fun subst_typ ------------------------------------------------------------------------";
10.168 "-------- fun subst_typ ------------------------------------------------------------------------";
10.169 -val Rule.Rls {scr = Prog prog, ...} = assoc_rls "isolate_bdv";
10.170 +val prog = Auto_Prog.gen @{theory Isac_Knowledge} t (assoc_rls "isolate_bdv");
10.171 (* term2str prog |> writeln
10.172 auto_generated_inst t_t v =
10.173 Repeat
10.174 @@ -307,8 +341,9 @@
10.175 ??.empty)
10.176 *)
10.177
10.178 -val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real"), Free ("v", "'a")]*)
10.179 -if length frees = 3 then () else error "test setup Auto_Prog.subst_typ changed 1";
10.180 +val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
10.181 +if length frees = 2 then () else error "test setup Auto_Prog.subst_typ changed 1";
10.182 +
10.183 val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
10.184 if length args = 2 then () else error "test setup Auto_Prog.subst_typ changed 2";
10.185
10.186 @@ -320,15 +355,17 @@
10.187 val typs_v = (* = ["real", "'a"]*)
10.188 map (fn t => (t |> dest_Free |> snd)) vars_v;
10.189
10.190 -val subst_ty = subst_typ "v" HOLogic.realT frees; (* = [("real", "real"), ("'a", "real")*)
10.191 -if length subst_ty = 2 then () else error "Auto_Prog.subst_typ changed";
10.192 +val subst_ty = subst_typ "v" HOLogic.realT frees; (* = [("real", "real")]*)
10.193 +if length subst_ty = 1 then () else error "Auto_Prog.subst_typ changed";
10.194 +
10.195
10.196 "-------- fun subst_typs -----------------------------------------------------------------------";
10.197 "-------- fun subst_typs -----------------------------------------------------------------------";
10.198 "-------- fun subst_typs -----------------------------------------------------------------------";
10.199 -val Rule.Rls {scr = Prog prog, ...} = assoc_rls "isolate_bdv";
10.200 +val prog = Auto_Prog.gen thy' t (assoc_rls "isolate_bdv");
10.201 val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real"), Free ("v", "'a")]*)
10.202 -if length frees = 3 then () else error "test setup Auto_Prog.subst_typs changed 1";
10.203 +if length frees = 2 then () else error "test setup Auto_Prog.subst_typs changed 1";
10.204 +
10.205 val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
10.206 if length args = 2 then () else error "test setup Auto_Prog.subst_typs changed 2";
10.207
11.1 --- a/test/Tools/isac/ProgLang/prog-tools.sml Sun Feb 09 16:55:41 2020 +0100
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,343 +0,0 @@
11.4 -(* Title: "ProgLang/scrtools.sml"
11.5 - tests on tools for scripts
11.6 - Author: Walther Neuper 060605
11.7 - (c) due to copyright terms
11.8 -*)
11.9 -"-----------------------------------------------------------------";
11.10 -"table of contents -----------------------------------------------";
11.11 -"-----------------------------------------------------------------";
11.12 -"-------- test the same called by interSteps norm_Poly -----------";
11.13 -"-------- test the same called by interSteps norm_Rational -------";
11.14 -"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
11.15 -"-------- distinguish input to Model -----------------------------------------";
11.16 -"-------- fun subpbl, fun pblterm --------------------------------------------";
11.17 -"-------- fun stacpbls, fun eval_leaf -----------------------------------";
11.18 -"-------- fun is_calc, fun op_of_calc ----------------------------------------";
11.19 -"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
11.20 -"-------- fun op #> ----------------------------------------------------------";
11.21 -"-------- fun get_fun_id -----------------------------------------------------";
11.22 -"-------- fun rules2scr_Rls --------------------------------------------------";
11.23 -"-----------------------------------------------------------------------------";
11.24 -"-----------------------------------------------------------------------------";
11.25 -"-----------------------------------------------------------------------------";
11.26 -
11.27 -"-------- test the same called by interSteps norm_Poly -----------";
11.28 -"-------- test the same called by interSteps norm_Poly -----------";
11.29 -"-------- test the same called by interSteps norm_Poly -----------";
11.30 -val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
11.31 -writeln(term2str auto_script);
11.32 -(*Program Stepwise t_t =
11.33 - (Try (Rewrite_Set discard_minus) #>
11.34 - Try (Rewrite_Set expand_poly_) #>
11.35 - Try (Repeat (Calculate TIMES)) #>
11.36 - Try (Rewrite_Set order_mult_rls_) #>
11.37 - Try (Rewrite_Set simplify_power_) #>
11.38 - Try (Rewrite_Set calc_add_mult_pow_) #>
11.39 - Try (Rewrite_Set reduce_012_mult_) #>
11.40 - Try (Rewrite_Set order_add_rls_) #>
11.41 - Try (Rewrite_Set collect_numerals_) #>
11.42 - Try (Rewrite_Set reduce_012_) #>
11.43 - Try (Rewrite_Set discard_parentheses1))
11.44 - ??.empty ..WORKS, NEVERTHELESS *)
11.45 -atomty auto_script;
11.46 -
11.47 -reset_states (); (*<-- evaluate, if ML-blocks are edited below*)
11.48 -CalcTree
11.49 -[(["Term (b + a - b)", "normalform N"],
11.50 - ("Poly",["polynomial","simplification"],
11.51 - ["simplification","for_polynomials"]))];
11.52 -Iterator 1;
11.53 -moveActiveRoot 1;
11.54 -
11.55 -autoCalculate 1 CompleteCalc;
11.56 -val ((pt,p),_) = get_calc 1;
11.57 -show_pt pt;
11.58 -(* isabisac17 = 15 [
11.59 -(([], Frm), Simplify (b + a - b)),
11.60 -(([1], Frm), b + a - b),
11.61 -(([1], Res), a),
11.62 -(([], Res), a)] *)
11.63 -
11.64 -interSteps 1 ([], Res);
11.65 -val ((pt,p),_) = get_calc 1; show_pt pt;
11.66 -show_pt pt;
11.67 -(* isabisac17 = 15 [
11.68 -(([], Frm), Simplify (b + a - b)),
11.69 -(([1], Frm), b + a - b),
11.70 -(([1], Res), a),
11.71 -(([], Res), a)] *)
11.72 -
11.73 -interSteps 1 ([1], Res);(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
11.74 -"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
11.75 - val ((pt, p), tacis) = get_calc cI;
11.76 -(*if*) (not o is_interpos) ip = false;
11.77 -val ip' = lev_pred' pt ip;
11.78 -
11.79 -(*Math_Engine.detailstep pt ip ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)
11.80 -val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Math_Engine.detailstep pt ip;
11.81 -"~~~~~ fun detailstep, args:"; val (pt, (pos as (p, _))) = (pt, ip);
11.82 - val nd = Ctree.get_nd pt p
11.83 - val cn = Ctree.children nd;
11.84 -(*if*) null cn = false;
11.85 -
11.86 -"~~~~~ to detailrls return val:";
11.87 -(*else*)
11.88 -val return_val = ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Pos.Res));
11.89 -if p @ [length (Ctree.children (Ctree.get_nd pt p))] = [1, 4]
11.90 -then () else error "detailrls: auto-generated norm_Poly doesnt work";
11.91 -
11.92 -val ((pt,p),_) = get_calc 1; show_pt pt;
11.93 -show_pt pt; (*[
11.94 -(([], Frm), Simplify (b + a - b)),
11.95 -(([1], Frm), b + a - b),
11.96 -(([1,1], Frm), b + a - b),
11.97 -(([1,1], Res), b + a + -1 * b),
11.98 -(([1,2], Res), a + b + -1 * b),
11.99 -(([1,3], Res), a + 0 * b),
11.100 -(([1,4], Res), a),
11.101 -(([1], Res), a),
11.102 -(([], Res), a)] *)
11.103 -if existpt' ([1,4], Res) pt then ()
11.104 -else error "auto-generated norm_Poly doesnt work";
11.105 -
11.106 -
11.107 -"-------- test the same called by interSteps norm_Rational -------";
11.108 -"-------- test the same called by interSteps norm_Rational -------";
11.109 -"-------- test the same called by interSteps norm_Rational -------";
11.110 -
11.111 -val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Rational";
11.112 -writeln(term2str auto_script);
11.113 -atomty auto_script;
11.114 -(***
11.115 -*** Const (Program.Stepwise, 'z => 'z => 'z)
11.116 -*** . Free (t_t, 'z)
11.117 -*** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
11.118 -*** . . Const (Program.Try, ('a => 'a) => 'a => 'a)
11.119 -*** . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
11.120 -*** . . . . Free (discard_minus, ID)
11.121 -*** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
11.122 -*** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
11.123 -*** . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
11.124 -*** . . . . . Free (rat_mult_poly, ID)
11.125 -*** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
11.126 -*** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
11.127 -*** . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
11.128 -*** . . . . . . Free (make_rat_poly_with_parentheses, ID)
11.129 -*** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
11.130 -*** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
11.131 -*** . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
11.132 -*** . . . . . . . Free (cancel_p_rls, ID)
11.133 -*** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
11.134 -*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
11.135 -*** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
11.136 -*** . . . . . . . . Free (norm_Rational_rls, ID)
11.137 -*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
11.138 -*** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
11.139 -*** . . . . . . . . Free (discard_parentheses1, ID)
11.140 -*** . . Const (empty, 'a)
11.141 -***)
11.142 -reset_states ();
11.143 -CalcTree
11.144 -[(["Term (b + a - b)", "normalform N"],
11.145 - ("Poly",["polynomial","simplification"],
11.146 - ["simplification","of_rationals"]))];
11.147 -Iterator 1;
11.148 -moveActiveRoot 1;
11.149 -autoCalculate 1 CompleteCalc;
11.150 -
11.151 -interSteps 1 ([], Res);
11.152 -val ((pt,p),_) = get_calc 1; show_pt pt;
11.153 -
11.154 -interSteps 1 ([1], Res);
11.155 -val ((pt,p),_) = get_calc 1; show_pt pt;
11.156 -
11.157 -(*with "Program SimplifyScript (t_::real) = \
11.158 - \ ((Rewrite_Set norm_Rational) t_)"
11.159 -val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
11.160 -*)
11.161 -val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
11.162 -case (term2str form, tac, terms2strs asm) of
11.163 - ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
11.164 - | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
11.165 -
11.166 -"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
11.167 -"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
11.168 -"-------- check auto-gen.script for Rewrite_Set_Inst -------------";
11.169 -val rls = assoc_rls "integration";
11.170 -val Seq {scr = Prog auto_script,...} = rls;
11.171 -writeln(term2str auto_script);
11.172 -
11.173 -if contain_bdv (get_rules rls) then ()
11.174 -else error "scrtools.sml: contain_bdv doesnt work for 'integration'";
11.175 -
11.176 -if terms2str (formal_args auto_script) = "[\"t_t\",\"v\"]"
11.177 -then () else error "formal_args of auto-gen.script changed";
11.178 -init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules"))
11.179 - (str2term "someTermWithBdv");
11.180 -
11.181 -"-------- fun stacpbls, fun eval_leaf -----------------------------------";
11.182 -"-------- fun stacpbls, fun eval_leaf -----------------------------------";
11.183 -"-------- fun stacpbls, fun eval_leaf -----------------------------------";
11.184 -val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
11.185 -case stacpbls sc of
11.186 - [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
11.187 - Const ("Prog_Tac.Rewrite'_Set", _) $ Test_simplify,
11.188 - Const ("Prog_Tac.Rewrite'_Set", _) $ rearrange_assoc,
11.189 - Const ("Prog_Tac.Rewrite'_Set", _) $ isolate_root,
11.190 - Const ("Prog_Tac.Rewrite'_Set", _) $ norm_equation,
11.191 - Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $
11.192 - (Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ bdv $ Free ("v_v", _)) $
11.193 - Const ("List.list.Nil", _))] =>
11.194 - if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
11.195 - HOLogic.dest_string Test_simplify = "Test_simplify" andalso
11.196 - HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso
11.197 - HOLogic.dest_string isolate_root = "isolate_root" andalso
11.198 - HOLogic.dest_string norm_equation = "norm_equation" andalso
11.199 - HOLogic.dest_string bdv = "bdv" andalso
11.200 - HOLogic.dest_string isolate_bdv = "isolate_bdv"
11.201 - then () else error "stacpbls (Test.Solve_root_equation) changed 2"
11.202 -| _ => error "stacpbls (Test.Solve_root_equation) changed 1";
11.203 -
11.204 -(* inappropriate input is skipped *)
11.205 -val t = @{term "(a::real) = (rhs (NTH 1 sol_a))"};
11.206 -case stacpbls t of [] => () | _ => error "stacpbls rhs (NTH 1 sol_a) changed";
11.207 -
11.208 -@{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
11.209 -case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
11.210 -
11.211 -(* --- fun eval_leaf *)
11.212 -case eval_leaf [] NONE e_term sc of
11.213 -(Expr (Const ("HOL.eq", _) $
11.214 - (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $
11.215 - (Const ("HOL.Let", _) $
11.216 - (Const ("Tactical.Chain", _) $
11.217 - (Const ("Tactical.While", _) $ _ $
11.218 - _ ) $
11.219 - (_) $
11.220 - Free ("e_e", _)) $
11.221 - Abs ("e_e", _, Const ("List.list.Cons", _) $ Free ("e_e", _) $ Const ("List.list.Nil", _)) )
11.222 -), NONE) => ()
11.223 -| _ => error "eval_leaf [] NONE e_term";
11.224 -
11.225 -"-------- fun is_calc, fun op_of_calc ----------------------------------------";
11.226 -"-------- fun is_calc, fun op_of_calc ----------------------------------------";
11.227 -"-------- fun is_calc, fun op_of_calc ----------------------------------------";
11.228 -val rls = prep_rls @{theory} Test_simplify; (* adds the Program *)
11.229 -val Prog sc = (#scr o rep_rls) rls;
11.230 -val stacs = stacpbls sc;
11.231 -
11.232 -val calcs = filter is_calc stacs;
11.233 -val ids = map op_of_calc calcs;
11.234 -case ids of
11.235 - ["PLUS", "TIMES", "DIVIDE", "POWER"] => ()
11.236 -| _ => error "op_of_calc";
11.237 -
11.238 -val calcs = ((assoc_calc' @{theory} |> map) o (map LTool.op_of_calc) o
11.239 - (filter LTool.is_calc) o LTool.stacpbls) sc;
11.240 -case calcs of
11.241 - [("PLUS", ("Groups.plus_class.plus", _)), ("TIMES", ("Groups.times_class.times", _)),
11.242 - ("DIVIDE", ("Rings.divide_class.divide", _)), ("POWER", ("Prog_Expr.pow", _))] => ()
11.243 -| _ => error "get_calcs changed"
11.244 -
11.245 -"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
11.246 -"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
11.247 -"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
11.248 -val t = rule2stac @{theory} (Thm ("real_diff_minus", num_str @{thm real_diff_minus}));
11.249 -if term2str t = "Try (Repeat (Rewrite ''real_diff_minus''))" then ()
11.250 -else error "rule2stac Thm.. changed";
11.251 -
11.252 -val t = rule2stac @{theory} (Num_Calc ("Groups.plus_class.plus", eval_binop "#add_"));
11.253 -if term2str t = "Try (Repeat (Calculate ''PLUS''))" then ()
11.254 -else error "rule2stac Num_Calc.. changed";
11.255 -
11.256 -val t = rule2stac @{theory} (Rls_ rearrange_assoc);
11.257 -if term2str t = "Try (Rewrite_Set ''rearrange_assoc'')" then ()
11.258 -else error "rule2stac Rls_.. changed";
11.259 -
11.260 -val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", num_str @{thm risolate_bdv_add}));
11.261 -if term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then ()
11.262 -else error "rule2stac_inst Thm.. changed";
11.263 -case t of
11.264 - (Const ("Tactical.Try", _) $
11.265 - (Const ("Tactical.Repeat", _) $
11.266 - (Const ("Prog_Tac.Rewrite'_Inst", _) $
11.267 - (Const ("List.list.Cons", _) $
11.268 - (Const ("Product_Type.Pair", _) $
11.269 - bdv $
11.270 - Free ("v", _)) $
11.271 - Const ("List.list.Nil", _)) $
11.272 - risolate_bdv_add))) =>
11.273 - (if HOLogic.dest_string bdv = "bdv" andalso
11.274 - HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
11.275 - else error "rule2stac_inst changed 1")
11.276 -| _ => error "rule2stac_inst changed 2"
11.277 -
11.278 -"-------- fun op #> ----------------------------------------------------------";
11.279 -"-------- fun op #> ----------------------------------------------------------";
11.280 -"-------- fun op #> ----------------------------------------------------------";
11.281 - val rules = (#rules o rep_rls) isolate_root;
11.282 - val rs = map (rule2stac @{theory}) rules;
11.283 - val t = #> rs;
11.284 -if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) #>\n" ^
11.285 - "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) #>\n" ^
11.286 - "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) #>\n" ^
11.287 - "Try (Repeat (Rewrite ''risolate_root_add'')) #>\n" ^
11.288 - "Try (Repeat (Rewrite ''risolate_root_mult'')) #>\n" ^
11.289 - "Try (Repeat (Rewrite ''risolate_root_div''))"
11.290 -then () else error "fun #> changed"
11.291 -
11.292 -"-------- fun get_fun_id -----------------------------------------------------";
11.293 -"-------- fun get_fun_id -----------------------------------------------------";
11.294 -"-------- fun get_fun_id -----------------------------------------------------";
11.295 -(* fun_id is nested into arguments, compare ... *)
11.296 -val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
11.297 - (((((((Const (const_id, const_typ) $ _) $ _) $ _) $ _) $ _) $ _) $ _) $ _) =
11.298 - Thm.prop_of @{thm biegelinie.simps};
11.299 -(* ... to: *)
11.300 -val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
11.301 - (Const (const_id, const_typ) $ _) $ _) =
11.302 - Thm.prop_of @{thm simplify.simps};
11.303 -
11.304 -(* get fun_id out of nesting *)
11.305 -val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
11.306 - nested $ _) =
11.307 - Thm.prop_of @{thm biegelinie.simps};
11.308 -val (Const ("Biegelinie.biegelinie", _) $
11.309 - Var (("l", 0), _) $
11.310 - Var (("q", 0), _) $
11.311 - Var (("v", 0), _) $
11.312 - Var (("b", 0), _) $
11.313 - Var (("s", 0), _) $
11.314 - Var (("vs", 0), _) $
11.315 - Var (("id_abl", 0), _)) = nested;
11.316 -strip_comb nested;
11.317 -(*val it =
11.318 - (Const ("Biegelinie.biegelinie", "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool")
11.319 - ,
11.320 - [Var (("l", 0), "real"), Var (("q", 0), "real"), Var (("v", 0), "real"),
11.321 - Var (("b", 0), "real \<Rightarrow> real"), Var (("s", 0), "bool list")]):
11.322 - term * term list*)
11.323 -
11.324 -case get_fun_id (prep_program @{thm biegelinie.simps}) of
11.325 - ("Biegelinie.biegelinie", _) => ()
11.326 -| _ => error "get_fun_id changed";
11.327 -case get_fun_id (prep_program @{thm simplify.simps}) of
11.328 - ("PolyMinus.simplify", _) => ()
11.329 -| _ => error "get_fun_id changed";
11.330 -
11.331 -"-------- fun rules2scr_Rls --------------------------------------------------";
11.332 -"-------- fun rules2scr_Rls --------------------------------------------------";
11.333 -"-------- fun rules2scr_Rls --------------------------------------------------";
11.334 -(*compare Prog_Expr.*)
11.335 -val prog = LTool.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})]
11.336 -;
11.337 -writeln (t2str @{theory} prog);
11.338 -(*auto_generated t_t =
11.339 -Repeat
11.340 - ((Try (Repeat (Rewrite ''thm111'')) #>
11.341 - Try (Repeat (Rewrite ''refl'')))
11.342 - ??.empty)*)
11.343 -;
11.344 -if t2str @{theory} prog =
11.345 -"auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''thm111'')) #>\n Try (Repeat (Rewrite ''refl'')))\n ??.empty)"
11.346 -then () else error "rules2scr_Rls auto_generated changed"