1.1 --- a/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Thu Jan 26 19:02:41 2023 +0100
1.2 +++ b/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Sat Jan 28 13:21:39 2023 +0100
1.3 @@ -1427,7 +1427,7 @@
1.4 {\footnotesize
1.5 \begin{verbatim}
1.6 01 ML {*
1.7 -02 val SOME t = parseNEW ctxt "argument_in (X (z::real))";
1.8 +02 val t = parse ctxt "argument_in (X (z::real))";
1.9 03 val SOME (str, t') = eval_argument_in ""
1.10 04 "Build_Inverse_Z_Transform.argument'_in" t 0;
1.11 05 term2str t';
2.1 --- a/doc-isac/mlehnfeld/bacc/presentation.tex Thu Jan 26 19:02:41 2023 +0100
2.2 +++ b/doc-isac/mlehnfeld/bacc/presentation.tex Sat Jan 28 13:21:39 2023 +0100
2.3 @@ -174,7 +174,7 @@
2.4 \item provide data for Isabelle's automated provers
2.5 \end{itemize}
2.6 %\item e.g. theories have no direct functions for type inference
2.7 -%\item replace function \texttt{parseNEW}
2.8 +%\item replace function \texttt{parse}
2.9 %\item assumptions \& environment $\rightarrow$ context
2.10 \item allow to conform with scopes for subprograms.
2.11 \end{itemize}
2.12 @@ -244,8 +244,8 @@
2.13 \>\>in SOME (cterm\_of thy t) end)\\
2.14 \>\>\>handle \_ => NONE;\\
2.15 \\
2.16 -fun parseNEW ctxt str = \\
2.17 -\>\>\>SOME (\alert{Syntax.read\_term ctxt} str |> numbers\_to\_string)\\
2.18 +fun parse ctxt str = \\
2.19 +\>\>\>(\alert{Syntax.read\_term ctxt} str |> numbers\_to\_string)\\
2.20 \>\>\>handle \_ => NONE;
2.21 \end{tabbing}
2.22 }}
2.23 @@ -368,7 +368,7 @@
2.24 \>\>\>\>val ctxt = ProofContext.init\_global thy \\
2.25 \>\>\>\>\> |> fold declare\_constraints fmz\\
2.26 \>\>\>\>val ori = \\
2.27 -\>\>\>\>\> map (add\_field thy pbt o split\_dts o the o parseNEW ctxt) fmz\\
2.28 +\>\>\>\>\> map (add\_field thy pbt o split\_dts o (parse ctxt)) fmz\\
2.29 \>\>\>\>\>\> |> add\_variants\\
2.30 \>\>\>\>val maxv = map fst ori |> max\\
2.31 \>\>\>\>val maxv = if maxv = 0 then 1 else maxv\\
3.1 --- a/doc-isac/mlehnfeld/bacc/projektbericht.tex Thu Jan 26 19:02:41 2023 +0100
3.2 +++ b/doc-isac/mlehnfeld/bacc/projektbericht.tex Sat Jan 28 13:21:39 2023 +0100
3.3 @@ -123,8 +123,8 @@
3.4 {\tt
3.5 \begin{tabbing}
3.6 xx\=xx\=xx\=xx\=xx\=\kill
3.7 -fun parseNEW ctxt str = \\
3.8 -\>\>\>SOME ({Syntax.read\_term ctxt} str |> numbers\_to\_string)\\
3.9 +fun parse ctxt str = \\
3.10 +\>\>\>({Syntax.read\_term ctxt} str |> numbers\_to\_string)\\
3.11 \>\>\>handle \_ => NONE;
3.12 \end{tabbing}
3.13 }
3.14 @@ -243,8 +243,8 @@
3.15 \textit{CalcTreeTEST} erzeugt schlie\3lich die grundlegenden Datenstrukturen für die folgenden Berechnungen. Beispielsweise wird ein ``context'' erzeugt, der nun im Baum \textit{pt} an der Position \textit{p} steht.
3.16 \begin{verbatim}
3.17 val ctxt = get_ctxt pt p;
3.18 -val SOME known_x = parseNEW ctxt "x + y + z";
3.19 -val SOME unknown = parseNEW ctxt "a + b + c";
3.20 +val known_x = parse ctxt "x + y + z";
3.21 +val unknown = parse ctxt "a + b + c";
3.22 \end{verbatim}
3.23 Dies erzeugt folgenden Output:
3.24 \begin{verbatim}
3.25 @@ -394,8 +394,8 @@
3.26
3.27 ML {*
3.28 val ctxt = get_ctxt pt p;
3.29 - val SOME known_x = parseNEW ctxt "x + y + z";
3.30 - val SOME unknown = parseNEW ctxt "a + b + c";
3.31 + val known_x = parseparse ctxt "x + y + z";
3.32 + val unknown = parse ctxt "a + b + c";
3.33 *}
3.34
3.35 ML {*
3.36 @@ -431,8 +431,8 @@
3.37
3.38 ML {*
3.39 val ctxt = get_ctxt pt p;
3.40 - val SOME known_x = parseNEW ctxt "x+y+z";
3.41 - val SOME unknown = parseNEW ctxt "a+b+c";
3.42 + val known_x = parse ctxt "x+y+z";
3.43 + val unknown = parse ctxt "a+b+c";
3.44 *}
3.45
3.46 ML {*
3.47 @@ -537,9 +537,9 @@
3.48 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
3.49 02.03.2011 & 1:30 & vorbereitendes Übungsbeispiel \\
3.50 03.03.2011 & 1:00 & ... \\
3.51 - 04.03.2011 & 5:00 & Funktion {\tt parseNEW} schreiben \\
3.52 + 04.03.2011 & 5:00 & Funktion {\tt parse} schreiben \\
3.53 05.03.2011 & 3:00 & Funktion {\tt vars} anpassen, {\tt declare\_constraints} neu \\
3.54 - 07.03.2011 & 8:45 & {\tt parseNEW}, Spezifikationen studieren \\
3.55 + 07.03.2011 & 8:45 & {\tt parse}, Spezifikationen studieren \\
3.56 08.03.2011 & 6:00 & {\it context} in zentrale Datenstrukturen einbauen \\
3.57 09.03.2011 & 2:00 & Fehlersuche {\it context}-Integration \\
3.58 \end{tabular}
4.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Thu Jan 26 19:02:41 2023 +0100
4.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Sat Jan 28 13:21:39 2023 +0100
4.3 @@ -72,11 +72,12 @@
4.4
4.5 val matches: theory -> term -> term -> bool
4.6
4.7 - val parseNEW: Proof.context -> string -> term option(*old version to be eliminated*)
4.8 + val parse: Proof.context -> string -> term
4.9 + val parse_patt: theory -> string -> term
4.10 +(*val parse_opt: Proof.context -> string -> term option (*kept while developing Specify*)*)
4.11 + val parseNEW: Proof.context -> string -> term option
4.12 val parseNEW': Proof.context -> string -> term (*old version to be eliminated*)
4.13 val parseNEW'': theory -> string -> term (*old version to be eliminated*)
4.14 -(*goal*)val parse: Proof.context -> string -> term
4.15 -(*goal*)val parse_patt: theory -> string -> term
4.16 (*for test/* *)
4.17 (*goal*)val parse_test: Proof.context -> string -> term
4.18 (*goal*)val parse_patt_test: theory -> string -> term
4.19 @@ -539,7 +540,7 @@
4.20 (** parse in test/* **)
4.21 (*
4.22 This bypasses building ctxt at the begin of a calculation
4.23 - and thus borrows adapt_to_type (used for where_-parsed terms from Know_Store).
4.24 + and thus borrows adapt_to_type (used for adapting pre-parsed terms from Know_Store).
4.25 *)
4.26 fun parse_test ctxt str = str
4.27 |> Syntax.read_term_global (Proof_Context.theory_of ctxt)
5.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Thu Jan 26 19:02:41 2023 +0100
5.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Sat Jan 28 13:21:39 2023 +0100
5.3 @@ -153,33 +153,29 @@
5.4 check if input is exactly equal to the rewrite from a rule
5.5 which is stored at the pos where the input is stored of "ok".
5.6 *)
5.7 -fun filled_exactly (pt, pos as (p, _)) istr =
5.8 - (* input from Isabelle/PIDE: TODO handle Position *)
5.9 +(*will come directly from PIDE --------vvvvvvvvvvv*)
5.10 +fun filled_exactly (pt, pos as (p, _)) (istr(*, pp*)) =
5.11 let
5.12 - val ctxt = Ctree.get_ctxt pt pos
5.13 - in
5.14 - case TermC.parseNEW (Ctree.get_ctxt pt pos) istr of
5.15 - NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
5.16 - | SOME ifo =>
5.17 + val ctxt = (Ctree.get_ctxt pt pos)
5.18 + val ifo = Syntax.read_term ctxt istr
5.19 + handle ERROR msg => error (msg (*^ Position.here pp*))
5.20 + val p' = Pos.lev_on p;
5.21 + val tac = Ctree.get_obj Ctree.g_tac pt p';
5.22 + in
5.23 + case Solve_Step.check tac (pt, pos) of
5.24 + Applicable.No msg => (msg, Tactic.Tac "")
5.25 + | Applicable.Yes rew =>
5.26 let
5.27 - val p' = Pos.lev_on p;
5.28 - val tac = Ctree.get_obj Ctree.g_tac pt p';
5.29 + val res = case rew of
5.30 + Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
5.31 + |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
5.32 + | t => raise ERROR ("filled_exactly: uncovered case for " ^ Tactic.string_of ctxt t)
5.33 in
5.34 - case Solve_Step.check tac (pt, pos) of
5.35 - Applicable.No msg => (msg, Tactic.Tac "")
5.36 - | Applicable.Yes rew =>
5.37 - let
5.38 - val res = case rew of
5.39 - Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
5.40 - | Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
5.41 - | t => raise ERROR ("filled_exactly: uncovered case for " ^ Tactic.string_of ctxt t)
5.42 - in
5.43 - if not (ifo = res) then
5.44 - ("input does not exactly fill the gaps", Tactic.Tac "")
5.45 - else ("ok", tac)
5.46 - end
5.47 + if not (ifo = res) then
5.48 + ("input does not exactly fill the gaps", Tactic.Tac "")
5.49 + else ("ok", tac)
5.50 end
5.51 - end
5.52 + end
5.53
5.54 (* fetch errpatIDs from an arbitrary tactic *)
5.55 fun from_store ctxt tac =
6.1 --- a/src/Tools/isac/Interpret/step-solve.sml Thu Jan 26 19:02:41 2023 +0100
6.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Sat Jan 28 13:21:39 2023 +0100
6.3 @@ -87,38 +87,39 @@
6.4 (Error_Pattern.check_for *within* compare_step seems too expensive)
6.5 *)
6.6 (*fun by_term (next_cs as (_, _, (pt, pos as (p, _))): Calc.state_post) istr =*)
6.7 -fun by_term (pt, pos as (p, _)) istr =
6.8 - case TermC.parseNEW (get_ctxt pt pos) istr of
6.9 - NONE => ("syntax error in '" ^ istr ^ "'", Calc.state_empty_post)
6.10 - | SOME f_in =>
6.11 - let
6.12 - val pos_pred = lev_back(*'*) pos
6.13 - val f_pred = Ctree.get_curr_formula (pt, pos_pred);
6.14 - val f_succ = Ctree.get_curr_formula (pt, pos);
6.15 - in
6.16 - if f_succ = f_in
6.17 - then ("same-formula", ([], [], (pt, pos))) (* ctree not cut with replaceFormula *)
6.18 - else
6.19 - case CAS_Cmd.input f_in of
6.20 - SOME (pt, _) => ("ok", ([], [], (pt, (p, Pos.Met))))
6.21 - | NONE =>
6.22 - case LI.locate_input_term (pt, pos) f_in of
6.23 - LI.Found_Step cstate =>
6.24 - ("ok" , ([], [], cstate (* already contains istate, ctxt *)))
6.25 - | LI.Not_Derivable =>
6.26 - let
6.27 - val ctxt = Ctree.get_ctxt pt pos
6.28 - val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)
6.29 - val (errpats, rew_rls, prog) = (* after shift to Diff --vvvvvvvvvvvvvvv ctxt should be sufficient*)
6.30 - case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of
6.31 - {errpats, rew_rls, program = Rule.Prog prog, ...} => (errpats, rew_rls, prog)
6.32 - | _ => raise ERROR "inform: uncovered case of get_met"
6.33 - val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
6.34 - in
6.35 - case Error_Pattern.check_for (Ctree.get_ctxt pt pos) (f_pred, f_in) (prog, env) (errpats, rew_rls) of
6.36 - SOME errpatID => ("error pattern #" ^ errpatID ^ "#", Calc.state_empty_post)
6.37 - | NONE => ("no derivation found", Calc.state_empty_post)
6.38 - end
6.39 - end
6.40 +(*will come directly from PIDE--vvvvvvvvvvv*)
6.41 +fun by_term (pt, pos as (p, _)) (istr(*, pp*)) =
6.42 + let
6.43 + val f_in = Syntax.read_term (Ctree.get_ctxt pt pos) istr
6.44 + handle ERROR msg => error (msg (*^ Position.here pp*))
6.45 + val pos_pred = lev_back(*'*) pos
6.46 + val f_pred = Ctree.get_curr_formula (pt, pos_pred);
6.47 + val f_succ = Ctree.get_curr_formula (pt, pos);
6.48 + in
6.49 + if f_succ = f_in
6.50 + then ("same-formula", ([], [], (pt, pos))) (* ctree not cut with replaceFormula *)
6.51 + else
6.52 + case CAS_Cmd.input f_in of
6.53 + SOME (pt, _) => ("ok", ([], [], (pt, (p, Pos.Met))))
6.54 + | NONE =>
6.55 + case LI.locate_input_term (pt, pos) f_in of
6.56 + LI.Found_Step cstate =>
6.57 + ("ok" , ([], [], cstate (* already contains istate, ctxt *)))
6.58 + | LI.Not_Derivable =>
6.59 + let
6.60 + val ctxt = Ctree.get_ctxt pt pos
6.61 + val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)
6.62 + val (errpats, rew_rls, prog) = (* after shift to Diff --vvvvvvvvvvvvvvv ctxt should be sufficient*)
6.63 + case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of
6.64 + {errpats, rew_rls, program = Rule.Prog prog, ...} => (errpats, rew_rls, prog)
6.65 + | _ => raise ERROR "inform: uncovered case of get_met"
6.66 + val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
6.67 + in
6.68 + case Error_Pattern.check_for (Ctree.get_ctxt pt pos) (f_pred, f_in) (prog, env) (errpats, rew_rls) of
6.69 + SOME errpatID => ("error pattern #" ^ errpatID ^ "#", Calc.state_empty_post)
6.70 + | NONE => ("no derivation found", Calc.state_empty_post)
6.71 + end
6.72 + end
6.73 +
6.74
6.75 end
7.1 --- a/src/Tools/isac/Knowledge/Equation.thy Thu Jan 26 19:02:41 2023 +0100
7.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Sat Jan 28 13:21:39 2023 +0100
7.3 @@ -58,10 +58,10 @@
7.4 (* function for handling the cas-input "solve (x+1=2, x)":
7.5 make a model which is already in ctree-internal format *)
7.6 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ eq $ bdv] =
7.7 - [((the o (TermC.parseNEW \<^context>)) "equality", [eq]),
7.8 - ((the o (TermC.parseNEW \<^context>)) "solveFor", [bdv]),
7.9 - ((the o (TermC.parseNEW \<^context>)) "solutions",
7.10 - [(the o (TermC.parseNEW \<^context>)) "L"])
7.11 + [((TermC.parse \<^context>) "equality", [eq]),
7.12 + ((TermC.parse \<^context>) "solveFor", [bdv]),
7.13 + ((TermC.parse \<^context>) "solutions",
7.14 + [(TermC.parse \<^context>) "L"])
7.15 ]
7.16 | argl2dtss _ = raise ERROR "Equation.ML: wrong argument for argl2dtss";
7.17 \<close>
8.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml Thu Jan 26 19:02:41 2023 +0100
8.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Sat Jan 28 13:21:39 2023 +0100
8.3 @@ -20,7 +20,7 @@
8.4
8.5 type o_model
8.6 type o_model_single
8.7 - val o_model_to_string : Proof.context -> o_model -> string
8.8 + val o_model_to_string : Proof.context -> o_model -> string
8.9 val o_model_single_to_string : Proof.context -> o_model_single -> string
8.10 val o_model_empty : o_model_single
8.11
9.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Thu Jan 26 19:02:41 2023 +0100
9.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Sat Jan 28 13:21:39 2023 +0100
9.3 @@ -196,17 +196,17 @@
9.4
9.5 (* check if a term is a Prog_Tac *)
9.6
9.7 -val SOME Calculate = TermC.parseNEW @{context} "Calculate";
9.8 -val SOME Rewrite = TermC.parseNEW @{context} "Rewrite";
9.9 -val SOME Rewrite_Inst = TermC.parseNEW @{context} "Rewrite'_Inst";
9.10 -val SOME Rewrite_Set = TermC.parseNEW @{context} "Rewrite'_Set";
9.11 -val SOME Rewrite_Set_Inst = TermC.parseNEW @{context} "Rewrite'_Set'_Inst";
9.12 -val SOME Or_to_List = TermC.parseNEW @{context} "Or'_to'_List";
9.13 -val SOME SubProblem = TermC.parseNEW @{context} "SubProblem";
9.14 -val SOME Substitute = TermC.parseNEW @{context} "Substitute";
9.15 -val SOME Take = TermC.parseNEW @{context} "Take";
9.16 -val SOME Check_elementwise = TermC.parseNEW @{context} "Check'_elementwise";
9.17 -val SOME Assumptions = TermC.parseNEW @{context} "Assumptions";
9.18 +val Calculate = TermC.parse @{context} "Calculate";
9.19 +val Rewrite = TermC.parse @{context} "Rewrite";
9.20 +val Rewrite_Inst = TermC.parse @{context} "Rewrite'_Inst";
9.21 +val Rewrite_Set = TermC.parse @{context} "Rewrite'_Set";
9.22 +val Rewrite_Set_Inst = TermC.parse @{context} "Rewrite'_Set'_Inst";
9.23 +val Or_to_List = TermC.parse @{context} "Or'_to'_List";
9.24 +val SubProblem = TermC.parse @{context} "SubProblem";
9.25 +val Substitute = TermC.parse @{context} "Substitute";
9.26 +val Take = TermC.parse @{context} "Take";
9.27 +val Check_elementwise = TermC.parse @{context} "Check'_elementwise";
9.28 +val Assumptions = TermC.parse @{context} "Assumptions";
9.29
9.30 val all_Consts = [Calculate, Rewrite, Rewrite_Inst, Rewrite_Set, Rewrite_Set_Inst, Or_to_List,
9.31 SubProblem, Substitute, Take, Check_elementwise, Assumptions]
10.1 --- a/src/Tools/isac/ProgLang/Tactical.thy Thu Jan 26 19:02:41 2023 +0100
10.2 +++ b/src/Tools/isac/ProgLang/Tactical.thy Sat Jan 28 13:21:39 2023 +0100
10.3 @@ -33,13 +33,13 @@
10.4 struct
10.5 (**)
10.6
10.7 -val SOME (Let $ _ $ _) = TermC.parseNEW @{context} "let aaa = 1 in aaa"
10.8 -val SOME (Chain) = TermC.parseNEW @{context} "Chain";
10.9 -val SOME (Try) = TermC.parseNEW @{context} "Try";
10.10 -val SOME (Repeat) = TermC.parseNEW @{context} "Repeat";
10.11 -val SOME (Or $ _ $ _) = TermC.parseNEW @{context} "aaa Or bbb";
10.12 -val SOME (While $ _ $ _) = TermC.parseNEW @{context} "While aaa Do bbb";
10.13 -val SOME (If $ _ $ _ $ _) = TermC.parseNEW @{context} "If aaa Then bbb Else ccc";
10.14 +val (Let $ _ $ _) = TermC.parse @{context} "let aaa = 1 in aaa"
10.15 +val (Chain) = TermC.parse @{context} "Chain";
10.16 +val (Try) = TermC.parse @{context} "Try";
10.17 +val (Repeat) = TermC.parse @{context} "Repeat";
10.18 +val (Or $ _ $ _) = TermC.parse @{context} "aaa Or bbb";
10.19 +val (While $ _ $ _) = TermC.parse @{context} "While aaa Do bbb";
10.20 +val (If $ _ $ _ $ _) = TermC.parse @{context} "If aaa Then bbb Else ccc";
10.21
10.22 val all_Consts = [Let, Chain, Try, Repeat, Or, While, If]
10.23
11.1 --- a/src/Tools/isac/Specify/Input_Descript.thy Thu Jan 26 19:02:41 2023 +0100
11.2 +++ b/src/Tools/isac/Specify/Input_Descript.thy Sat Jan 28 13:21:39 2023 +0100
11.3 @@ -174,7 +174,7 @@
11.4 let val elems = (flat o (map TermC.isalist2list)) ts;
11.5 in TermC.list2isalist (type_of (hd elems)) elems end;
11.6
11.7 -val script_parse = the o (@{theory BaseDefinitions} |> Proof_Context.init_global |> TermC.parseNEW);
11.8 +val script_parse = @{theory BaseDefinitions} |> Proof_Context.init_global |> TermC.parse;
11.9 val e_listReal = script_parse "[]::(real list)";
11.10 val e_listBool = script_parse "[]::(bool list)";
11.11
12.1 --- a/src/Tools/isac/Specify/i-model.sml Thu Jan 26 19:02:41 2023 +0100
12.2 +++ b/src/Tools/isac/Specify/i-model.sml Sat Jan 28 13:21:39 2023 +0100
12.3 @@ -247,6 +247,7 @@
12.4 In case of O_Model.T = [] (i.e. no data for user-guidance in Formalise.T)
12.5 check_single is extremely permissive.
12.6 *)
12.7 +(*old version ----------------------------------------------------------------------\*)
12.8 fun check_single ctxt m_field [] i_model m_patt ct =
12.9 let
12.10 val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)
12.11 @@ -300,7 +301,68 @@
12.12 | (msg, _, _) => Err ("ERROR I_Model.check_single: contains: " ^ msg))
12.13 | SOME t => Err ("ERROR I_Model.check_single: impossible for input \"" ^
12.14 UnparseC.term_in_ctxt ctxt t ^ "\"");
12.15 -
12.16 +(*old version ----------------------------------------------------------------------/*)
12.17 +(*new version ----------------------------------------------------------------------\* )
12.18 +(*will come directly from PIDE -----------------vvvvvvvvvvv
12.19 + in case t comes from Step.specify_do_next -----------vvv = Position.none*)
12.20 +fun check_single ctxt m_field [] i_model m_patt (ct(*, pos*)) =
12.21 + let
12.22 + val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)
12.23 + val t = TermC.parse ctxt ct
12.24 + handle ERROR msg => error (msg (*^ Position.here pos*))
12.25 + (*NONE => Add (i, [], false, m_field, Syn ct)*)
12.26 + val (d, ts) = Input_Descript.split t
12.27 + in
12.28 + if d = TermC.empty then
12.29 + Add (i, [], false, m_field, Mis (unknown_descriptor, hd ts))
12.30 + else
12.31 + (case find_first (eq1 d) m_patt of
12.32 + NONE => Add (i, [], true, m_field, Sup (d,ts))
12.33 + | SOME (f, (_, id)) =>
12.34 + let
12.35 + fun eq2 d (i, _, _, _, itm_) = d = (descriptor itm_) andalso i <> 0
12.36 + in
12.37 + case find_first (eq2 d) i_model of
12.38 + NONE => Add (i, [], true, f,Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
12.39 + | SOME (i', _, _, _, itm_) =>
12.40 + if Input_Descript.for_list d then
12.41 + let
12.42 + val in_itm = o_model_values itm_
12.43 + val ts' = union op = ts in_itm
12.44 + val i'' = if in_itm = [] then i else i'
12.45 + in Add (i'', [], true, f, Cor ((d, ts'), (id, [Input_Descript.join'''' (d, ts')])))end
12.46 + else Add (i', [], true, f, Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
12.47 + end)
12.48 + end
12.49 + (* for MethodC: #undef completed vvvvv vvvvvv term_as_string *)
12.50 + (*will come directly from PIDE ----------------------vvvvvvvvvvv*)
12.51 + | check_single ctxt m_field o_model i_model m_patt (str(*, pos*)) =
12.52 + let
12.53 + val (t as (descriptor $ _)) = TermC.parse ctxt str
12.54 + handle ERROR msg => error (msg (*^ Position.here pp*))
12.55 + (*NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")*)
12.56 + in
12.57 + case Model_Pattern.get_field descriptor m_patt of
12.58 + NONE => Err ("ERROR I_Model.check_single: unknown descriptor \"" ^
12.59 + UnparseC.term_in_ctxt ctxt descriptor ^ "\"")
12.60 + | SOME m_field' =>
12.61 + if m_field <> m_field' then
12.62 + Err ("ERROR I_Model.check_single: \"" ^ UnparseC.term_in_ctxt ctxt t ^ "\"" ^
12.63 + "\" not for field \"" ^ m_field ^ "\"")
12.64 + else
12.65 + case O_Model.contains ctxt m_field o_model t of
12.66 + ("", ori', all) =>
12.67 + (case is_notyet_input ctxt i_model all ori' m_patt of
12.68 + ("", itm) => Add itm
12.69 + | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
12.70 + | (msg, _, _) => Err ("ERROR I_Model.check_single: contains: " ^ msg)
12.71 +(* case parseNEW of ..kept for understanding code..
12.72 + | SOME t => Err ("ERROR I_Model.check_single: impossible for input \"" ^
12.73 + UnparseC.term_in_ctxt ctxt t ^ "\"")
12.74 +*)
12.75 + end
12.76 +( *new version ----------------------------------------------------------------------*)
12.77 +
12.78
12.79 (** add input **)
12.80
13.1 --- a/src/Tools/isac/Specify/refine.sml Thu Jan 26 19:02:41 2023 +0100
13.2 +++ b/src/Tools/isac/Specify/refine.sml Sat Jan 28 13:21:39 2023 +0100
13.3 @@ -5,10 +5,12 @@
13.4 Refine a problem by a search for a \<open>ML_structure Model_Pattern\<close>
13.5 better fitting the respective where_-condition.
13.6
13.7 -The search on the tree got by @{term Know_Store.get_pbls} is costly such that
13.8 -\<open>ML_structure Know_Store\<close> holds terms in \<open>ML_structure Model_Pattern\<close>, where_-condition (and cas).
13.9 -The terms are where_-compiled with the most general \<open>ML_type "'a"\<close> and the type is adapted
13.10 -according to the type suggested by the current \<open>ML_structure Context\<close>.
13.11 +The search on the tree given by @{term Know_Store.get_pbls} is costly such that
13.12 +\<open>ML_structure Know_Store\<close> holds terms pre-parsed with a most generally type.
13.13 +
13.14 +On transfer to a calculation these terms are strongly typed by Model_Pattern.adapt_to_type
13.15 +(and users of this function in \<open>ML_structure Error_Pattern, MethodC, Problem\<close>)
13.16 +according to the current context.
13.17
13.18 Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term TermC.typ_a2real\<close> etc)
13.19 are adapted for "adapt_to_type on the fly" until further clarification.
14.1 --- a/test/Pure/Syntax/Syntax.thy Thu Jan 26 19:02:41 2023 +0100
14.2 +++ b/test/Pure/Syntax/Syntax.thy Sat Jan 28 13:21:39 2023 +0100
14.3 @@ -26,7 +26,7 @@
14.4
14.5 fun update trm = Syntax_Data.map (fn trms => trm::trms);
14.6 val ctxt =
14.7 - ProofContext.init_global @{theory} |>
14.8 + Proof_Context.init_global @{theory} |>
14.9 Syntax_Data.map (fn trms => @{term "x::int"}::trms);
14.10
14.11 fun parseNEW ctxt str =
15.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Thu Jan 26 19:02:41 2023 +0100
15.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Sat Jan 28 13:21:39 2023 +0100
15.3 @@ -35,8 +35,8 @@
15.4 (*must NOT check ThyC.id_empty in specify_data.spec, .. is still empty in this case
15.5 but for References_Def.T in specify_data.origin. .. is already assigned in this case
15.6 and in case of CAS-cmd *)
15.7 - val SOME known_x = TermC.parseNEW ctxt "x + y + z";
15.8 - val SOME unknown = TermC.parseNEW ctxt "a + b + c";
15.9 + val known_x = TermC.parse ctxt "x + y + z";
15.10 + val unknown = TermC.parse ctxt "a + b + c";
15.11 if type_of known_x = HOLogic.realT andalso
15.12 type_of unknown = TFree ("'a",["Groups.plus"])
15.13 then () else error "All_Ctx: type constraints beginning specification of root-problem ";
15.14 @@ -74,8 +74,8 @@
15.15
15.16 ML \<open>(*not significant in this example*)
15.17 val ctxt = Ctree.get_ctxt pt p;
15.18 - val SOME known_x = TermC.parseNEW ctxt "x+y+z";
15.19 - val SOME unknown = TermC.parseNEW ctxt "a+b+c";
15.20 + val known_x = TermC.parse ctxt "x+y+z";
15.21 + val unknown = TermC.parseparse ctxt "a+b+c";
15.22 if type_of known_x = HOLogic.realT andalso
15.23 type_of unknown = TFree ("'a",["Groups.plus"])
15.24 then () else error "All_Ctx: type constraints beginning specification of SubProblem ";
16.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Jan 26 19:02:41 2023 +0100
16.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Jan 28 13:21:39 2023 +0100
16.3 @@ -133,10 +133,10 @@
16.4 val ctxt = Proof_Context.init_global @{theory};
16.5 (*val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt;*)
16.6
16.7 - val SOME fun1 =
16.8 - TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z \<up> -1)"; UnparseC.term fun1;
16.9 - val SOME fun1' =
16.10 - TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term fun1';
16.11 + val fun1 =
16.12 + TermC.parse ctxt "X z = 3 / (z - 1/4 + -1/8 * z \<up> -1)"; UnparseC.term_in_ctxt ctxt fun1;
16.13 + val fun1' =
16.14 + TermC.parse ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; UnparseC.term_in_ctxt ctxt fun1';
16.15 \<close>
16.16
16.17 subsubsection \<open>Prepare Numerator and Denominator\<close>
16.18 @@ -262,7 +262,7 @@
16.19 for this equation type. Later on {\sisac} should determine the type
16.20 of the given equation self.\<close>
16.21 ML \<open>
16.22 - val denominator = TermC.parseNEW ctxt "z \<up> 2 - 1/4*z - 1/8 = 0";
16.23 + val denominator = TermC.parse ctxt "z \<up> 2 - 1/4*z - 1/8 = 0";
16.24 val fmz = ["equality (z \<up> 2 - 1/4*z - 1/8 = (0::real))",
16.25 "solveFor z",
16.26 "solutions L"];
17.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Thu Jan 26 19:02:41 2023 +0100
17.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Sat Jan 28 13:21:39 2023 +0100
17.3 @@ -2,7 +2,7 @@
17.4 Author: Walther Neuper 060225,
17.5 (c) due to copyright terms
17.6
17.7 -Strange ERROR "Undefined fact: "all_left""
17.8 +Strange ERROR "Undefined fact: "all_left""
17.9 *)
17.10
17.11 "-----------------------------------------------------------------";
17.12 @@ -459,7 +459,8 @@
17.13 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
17.14 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
17.15
17.16 - appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
17.17 +(*appendFormula 1 " x - "; ..ERROR Inner syntax error: unexpected end of input
17.18 + Failed to parse term *)
17.19 val ((pt,_),_) = States.get_calc 1;
17.20 val str = pr_ctree ctxt pr_short pt;
17.21 writeln str;
18.1 --- a/test/Tools/isac/MathEngine/step.sml Thu Jan 26 19:02:41 2023 +0100
18.2 +++ b/test/Tools/isac/MathEngine/step.sml Sat Jan 28 13:21:39 2023 +0100
18.3 @@ -182,7 +182,22 @@
18.4 autoCalculate 1 CompleteCalcHead;
18.5 autoCalculate 1 (Steps 1);
18.6 autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
18.7 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);
18.8 +;
18.9 + @{term "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" }
18.10 +;
18.11 +appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)";
18.12 + (*WAS ERROR: Inner syntax error \n Failed to parse term: "d_d x (x ^ 2) + cos (4 * x ^ 3)"
18.13 + -----------------------------------------------------------------\<up>-----------------\<up>*)
18.14 +(*/------------------- locate ERROR within appendFormula more precisely ---------------------\*)
18.15 +"~~~~~ fun appendFormula , args:"; val (cI, ifo) = (1, "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
18.16 + val cs = States.get_calc cI
18.17 + val pos = States.get_pos cI 1
18.18 +val ("ok", (_, _, ptp)) =
18.19 + (*case*) Step.do_next pos cs (*of*);
18.20 +
18.21 + (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*WAS ERROR: Inner syntax error \n Failed to parse term*)
18.22 +(*\------------------- locate ERROR within appendFormula more precisely ---------------------/*)
18.23 +
18.24 (* the check for errpat is maximally liberal (whole term modulo "rew_rls" from "type met"),
18.25 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
18.26 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
19.1 --- a/test/Tools/isac/Test_Some.thy Thu Jan 26 19:02:41 2023 +0100
19.2 +++ b/test/Tools/isac/Test_Some.thy Sat Jan 28 13:21:39 2023 +0100
19.3 @@ -38,7 +38,7 @@
19.4 open P_Model; (* NONE *)
19.5 open Rewrite;
19.6 open Eval; get_pair;
19.7 - open TermC; atomt;
19.8 + open TermC;
19.9 open Rule;
19.10 open Rule_Set; Sequence;
19.11 open Eval_Def
19.12 @@ -62,7 +62,7 @@
19.13 "xx"
19.14 ^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
19.15 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
19.16 - (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
19.17 +(*//------------------ adhoc inserted n ----------------------------------------------------\\*)
19.18 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)
19.19 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
19.20
19.21 @@ -71,7 +71,7 @@
19.22 (*keep for continuing YYYYY*)
19.23 \<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)
19.24 (*-------------------- continuing XXXXX ------------------------------------------------------*)
19.25 -(*kept for continuing XXXXX*)
19.26 +(*kept for continuing YYYYY*)
19.27 (*-------------------- stop step into XXXXX --------------------------------------------------*)
19.28 \<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)
19.29 (*\\------------------ step into XXXXX -----------------------------------------------------//*)
19.30 @@ -120,11 +120,471 @@
19.31 \<close> ML \<open>
19.32 \<close>
19.33
19.34 -section \<open>===================================================================================\<close>
19.35 +section \<open>=========="Minisubpbl/150a-add-given-Maximum.sml"==================================\<close>
19.36 ML \<open>
19.37 \<close> ML \<open>
19.38 \<close> ML \<open>
19.39 \<close> ML \<open>
19.40 +(* Title: "Minisubpbl/150a-add-given-Maximum.sml"
19.41 + Author: Walther Neuper 1105
19.42 + (c) copyright due to lincense terms.
19.43 +
19.44 +Note: This test --- steps into me --- more than once;
19.45 + in order not to get lost while working in Test_Some etc,
19.46 + re-introduce ML (*--- step into XXXXX ---*) and Co.
19.47 + and use Sidekick for orientation.
19.48 +*)
19.49 +
19.50 +open Test_Code
19.51 +open Pos
19.52 +open Ctree
19.53 +open Tactic
19.54 +
19.55 +val (_(*example text*),
19.56 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
19.57 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
19.58 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
19.59 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
19.60 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
19.61 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
19.62 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
19.63 + "ErrorBound (\<epsilon> = (0::real))" :: []),
19.64 + refs as ("Diff_App",
19.65 + ["univariate_calculus", "Optimisation"],
19.66 + ["Optimisation", "by_univariate_calculus"])))
19.67 + = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
19.68 +
19.69 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
19.70 +val c = [];
19.71 +
19.72 +\<close> ML \<open>
19.73 +val (p''', _, f''', nxt''', _, pt''') = me nxt p c pt; val Add_Given "Constants [r = 7]" = nxt''';
19.74 +
19.75 +\<close> ML \<open>
19.76 +(*+*)val PblObj {ctxt, ...} = get_obj I pt''' [];
19.77 +(*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*)
19.78 +\<close> ML \<open>
19.79 +(*+*)val "r = (7::'a)" = parse ctxt "r = 7" |> UnparseC.term_in_ctxt ctxt
19.80 + (* ^^^^^ ctxt SHOULD KNOW r::real FROM Formalise.model *)
19.81 +\<close> ML \<open>
19.82 +\<close> ML \<open>(*//------------ step into me Model_Problem ------------------------------------------\\*)
19.83 +(*//------------------ step into me Model_Problem ------------------------------------------\\*)
19.84 +"~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);
19.85 + val (pt, p) =
19.86 + (*ERROR Specify.item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt ... see 100-init-rootpbl.sml*)
19.87 + case Step.by_tactic tac (pt,p) of
19.88 + ("ok", (_, _, ptp)) => ptp;
19.89 +
19.90 +\<close> ML \<open>
19.91 +val ("ok", (ts as (_, _, _) :: _, _, _)) =
19.92 + (*case*)
19.93 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
19.94 +\<close> ML \<open>(*///----------- step into do_next ---------------------------------------------------\\ERROR*)
19.95 +(*//------------------ step into do_next ---------------------------------------------------\\*)
19.96 +\<close> ML \<open>
19.97 +val (ts'''', (pt'''', p'''')) = (ts, (pt, p)); (* keep for continuing me Model_Problem *)
19.98 +\<close> ML \<open>
19.99 +
19.100 +"~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
19.101 + (p, ((pt, e_pos'),[]));
19.102 + val pIopt = get_pblID (pt,ip);
19.103 + (*if*) ip = ([],Res); (* = false*)
19.104 + val _ = (*case*) tacis (*of*);
19.105 + val SOME _ = (*case*) pIopt (*of*);
19.106 +
19.107 +\<close> ML \<open>(*||||Step.switch_specify_solve ERROR*)
19.108 +\<close> ML \<open>
19.109 + val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
19.110 + Step.switch_specify_solve p_ (pt, ip);
19.111 +\<close> ML \<open>
19.112 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
19.113 + (*if*) Pos.on_specification ([], state_pos) (*then*);
19.114 +
19.115 +\<close> ML \<open>(*|||||Step.specify_do_next ERROR*)
19.116 +\<close> text \<open> (*isa*)
19.117 + val ("ERROR I_Model.check_single: contains: associate_input: input ('Constants [r = (7::'a)]') not found in oris (typed)", ([], [], _)) =
19.118 + Step.specify_do_next (pt, input_pos);
19.119 +\<close> ML \<open> (*isa2*)
19.120 + val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
19.121 + Step.specify_do_next (pt, input_pos);
19.122 +\<close> ML \<open>
19.123 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
19.124 +
19.125 +\<close> ML \<open>(*||||||Specify.find_next_step OK*)
19.126 +(* val (_, (p_', tac)) =*)
19.127 +\<close> ML \<open>val return_find_next_step = (*keep for continuing specify_do_next*)
19.128 + Specify.find_next_step ptp;
19.129 +"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
19.130 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
19.131 + spec = refs, ...} = Calc.specify_data (pt, pos);
19.132 + val ctxt = Ctree.get_ctxt pt pos;
19.133 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
19.134 + (*if*) p_ = Pos.Pbl (*then*);
19.135 +
19.136 +\<close> ML \<open>(*|||||||Specify.for_problem OK*)
19.137 + Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
19.138 +"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
19.139 + = (ctxt, oris, (o_refs, refs), (pbl, met));
19.140 + val cdI = if dI = ThyC.id_empty then dI' else dI;
19.141 + val cpI = if pI = Problem.id_empty then pI' else pI;
19.142 + val cmI = if mI = MethodC.id_empty then mI' else mI;
19.143 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
19.144 + val {model = mpc, ...} = MethodC.from_store ctxt cmI
19.145 + val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
19.146 + (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
19.147 + (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
19.148 + (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
19.149 +
19.150 +\<close> ML \<open>(*||||||||Specify.item_to_add OK*)
19.151 + (*case*)
19.152 + Specify.item_to_add (ThyC.get_theory_PIDE ctxt
19.153 + (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
19.154 +"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
19.155 + = ((ThyC.get_theory_PIDE ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
19.156 + fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
19.157 + fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
19.158 + fun test_id ids r = member op= ids (#1 (r : O_Model.single))
19.159 + fun test_subset itm (_, _, _, d, ts) =
19.160 + (I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#5 itm), ts)
19.161 + fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
19.162 + | false_and_not_Sup (_, _, false, _, _) = true
19.163 + | false_and_not_Sup _ = false
19.164 + val v = if itms = [] then 1 else I_Model.max_variant itms
19.165 + val vors = if v = 0 then oris else filter (testr_vt v) oris
19.166 + val vits =
19.167 + if v = 0
19.168 + then itms (* because of dsc without dat *)
19.169 + else filter (testi_vt v) itms; (* itms..vat *)
19.170 + val icl = filter false_and_not_Sup vits; (* incomplete *)
19.171 + (*if*) icl = [] (*else*);
19.172 +val SOME ori =
19.173 + (*case*) find_first (test_subset (hd icl)) vors (*of*);
19.174 +\<close> ML \<open> (*|||||-------- continuing specify_do_next --------------------------------------------*)
19.175 +(*|||||--------------- continuing specify_do_next --------------------------------------------*)
19.176 +val (_, (p_', tac)) = return_find_next_step (*kept for continuing specify_do_next*)
19.177 +\<close> ML \<open>
19.178 + val ist_ctxt = Ctree.get_loc pt (p, p_)
19.179 +\<close> ML \<open>
19.180 +(*+*)val Add_Given str = tac
19.181 +(*+*)val "Constants [r = 7]" = str
19.182 +\<close> ML \<open>
19.183 +\<close> ML \<open>
19.184 +val _ =
19.185 + (*case*) tac (*of*);
19.186 +\<close> ML \<open>
19.187 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
19.188 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
19.189 + (tac, (pt, (p, p_')));
19.190 +\<close> ML \<open>
19.191 + Specify.by_Add_ "#Given" ct ptp;
19.192 +"~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) =
19.193 + ("#Given", ct, ptp);
19.194 +\<close> ML \<open>
19.195 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
19.196 +\<close> ML \<open>
19.197 + val (i_model, m_patt) =
19.198 + if p_ = Pos.Met then
19.199 + (met,
19.200 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
19.201 + else
19.202 + (pbl,
19.203 + (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
19.204 +\<close> ML \<open>
19.205 + (*case*)
19.206 + I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
19.207 +"~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) =
19.208 + (ctxt, m_field, oris, i_model, m_patt, ct);
19.209 +\<close> ML \<open>
19.210 +(*new*) val (t as (descriptor $ _)) = TermC.parse ctxt str
19.211 +\<close> ML \<open>
19.212 +(*+*)val "Constants [r = (7::'a)]" = UnparseC.term_in_ctxt @{context} t;
19.213 +(*+*)Proof_Context.theory_of ctxt (* = Pure, .., Isac.Diff_App}: theory*); (*??? WHY DOES ctxt NOT KNOW ABOUT r;
19.214 + ^^^^ SHOULD KNOW r::real SINCE Formalise.model HAS BEEN PARSED ???*)
19.215 +\<close> ML \<open>
19.216 +\<close> ML \<open>
19.217 +(*new*)val SOME m_field' =
19.218 +(*new*) (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
19.219 +\<close> ML \<open>
19.220 +(*new*) (*if*) m_field <> m_field' (*else*);
19.221 +\<close> ML \<open>
19.222 +(*+*)val "#Given" = m_field
19.223 +(*+*)val "#Given" = m_field'
19.224 +\<close> ML \<open>
19.225 +(*new*)val (msg, _, _) =
19.226 +(*new*) (*case*) O_Model.contains ctxt m_field o_model t (*of*);
19.227 +\<close> ML \<open>
19.228 +(*+*)val "associate_input: input ('Constants [r = (7::'a)]') not found in oris (typed)" = msg;
19.229 +(*---------------------------------------------------^^^^*)
19.230 +\<close> ML \<open>
19.231 +(*+*)val "Constants [r = (7::'a)]" = UnparseC.term_in_ctxt @{context} t;
19.232 +\<close> ML \<open>
19.233 +(*+*)val (_, _, _, _, vals) = hd o_model;
19.234 +(*+*)val "Constants [r = 7]" = UnparseC.term_in_ctxt @{context} (@{term Constants} $ (hd vals));
19.235 +(*+*) if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^
19.236 +(*+*) "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^
19.237 +(*+*) "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^
19.238 +(*+*) "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^
19.239 +(*+*) "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^
19.240 +(*+*) "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^
19.241 +(*+*) "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^
19.242 +(*+*) "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^
19.243 +(*+*) "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^
19.244 +(*+*) "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^
19.245 +(*+*) "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
19.246 +(*+*) = O_Model.to_string_PIDE @{context} o_model then () else error "o_model CHANGED";
19.247 +\<close> ML \<open>
19.248 +\<close> ML \<open>
19.249 +\<close> ML \<open>
19.250 +\<close> ML \<open>
19.251 +\<close> ML \<open>
19.252 +\<close> ML \<open>
19.253 +\<close> ML \<open>
19.254 +\<close> ML \<open>
19.255 +\<close> ML \<open>
19.256 +\<close> ML \<open>
19.257 +\<close> ML \<open>
19.258 +\<close> ML \<open>
19.259 +\<close> ML \<open>
19.260 +(*-------------------- stop step into do_next ------------------------------------------------*)
19.261 +\<close> ML \<open>(*|||----------- stop step into do_next ------------------------------------------------*)
19.262 +(*\\------------------ step into into do_next ----------------------------------------------//*)
19.263 +\<close> ML \<open>(*\\\----------- step into into do_next ----------------------------------------------//*)
19.264 +
19.265 +\<close> ML \<open>
19.266 +(*||------------------ continue with me Model_Problem ----------------------------------------*)
19.267 +\<close> ML \<open>(*||------------ continue with me Model_Problem ----------------------------------------*)
19.268 +\<close> ML \<open>
19.269 +"~~~~~ continue fun me Model_Problem"; val (ts, (p, pt)) = (ts'''', (p'''', pt''''));
19.270 +\<close> ML \<open>
19.271 +val tacis as (_::_) =
19.272 + (*case*) ts (*of*);
19.273 + val (tac, _, _) = last_elem tacis
19.274 +\<close> ML \<open>
19.275 +
19.276 +val return = (p, [] : NEW,
19.277 + TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
19.278 +"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
19.279 + val (form, _, _) = ME_Misc.pt_extract ctxt ptp
19.280 +val Ctree.ModSpec (_, p_, _, gfr, where_, _) =
19.281 + (*case*) form (*of*);
19.282 +
19.283 +(*+*)val Pos.Pbl = p_;
19.284 + Test_Out.PpcKF ( (Test_Out.Problem [],
19.285 + P_Model.from (Proof_Context.theory_of ctxt) gfr where_));
19.286 +
19.287 + P_Model.from (Proof_Context.theory_of ctxt) gfr where_;
19.288 +"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
19.289 + fun coll model [] = model
19.290 + | coll model ((_, _, _, field, itm_) :: itms) =
19.291 + coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
19.292 +
19.293 + val gfr = coll P_Model.empty itms;
19.294 +"~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))
19.295 + = (P_Model.empty, itms);
19.296 +
19.297 +(*+*)val 4 = length itms;
19.298 +(*+*)val itm = nth 1 itms;
19.299 +
19.300 + coll P_Model.empty [itm];
19.301 +"~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: []))
19.302 + = (P_Model.empty, [itm]);
19.303 +
19.304 + (add_sel_ppc thy field model (item_from_feedback thy itm_));
19.305 +"~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )
19.306 + = (thy, field, model, (item_from_feedback thy itm_));
19.307 +
19.308 + P_Model.item_from_feedback thy itm_;
19.309 +"~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);
19.310 + P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
19.311 +(*-------------------- stop step into me Model_Problem ---------------------------------------*)
19.312 +\<close> ML \<open>(*\\------------ stop step into me Model_Problem ---------------------------------------*)
19.313 +(*\\------------------ step into into me Model_Problem -------------------------------------//*)
19.314 +\<close> ML \<open>(*\\------------ step into into me Model_Problem -------------------------------------//*)
19.315 +
19.316 +\<close> ML \<open>
19.317 +val (p,_,f,nxt,_,pt) = me nxt''' p''' c pt'''; val Add_Find "Maximum A" = nxt;
19.318 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt;
19.319 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt;
19.320 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;
19.321 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" = nxt;
19.322 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Diff_App" = nxt;
19.323 +
19.324 +val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = nxt''';
19.325 +
19.326 +(*//------------------ step into me Specify_Theory -----------------------------------------\\*)
19.327 +\<close> ML \<open>(*//------------ step into me Specify_Theory -----------------------------------------\\*)
19.328 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
19.329 + val ctxt = Ctree.get_ctxt pt p
19.330 + val (pt, p) =
19.331 + case Step.by_tactic tac (pt, p) of
19.332 + ("ok", (_, _, ptp)) => ptp
19.333 +
19.334 +val ("ok", (ts as (_, _, _) :: _, _, _)) =
19.335 + (*case*)
19.336 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
19.337 +(*//------------------ step into do_next ---------------------------------------------------\\*)
19.338 +\<close> ML \<open>(*///----------- step into do_next ---------------------------------------------------\\*)
19.339 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
19.340 + = (p, ((pt, Pos.e_pos'), [])) (*of*);
19.341 + (*if*) Pos.on_calc_end ip (*else*);
19.342 + val (_, probl_id, _) = Calc.references (pt, p);
19.343 +val _ =
19.344 + (*case*) tacis (*of*);
19.345 + (*if*) probl_id = Problem.id_empty (*else*);
19.346 +
19.347 + Step.switch_specify_solve p_ (pt, ip);
19.348 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
19.349 + (*if*) Pos.on_specification ([], state_pos) (*then*);
19.350 +
19.351 + Step.specify_do_next (pt, input_pos);
19.352 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
19.353 + val (_, (p_', tac)) = Specify.find_next_step ptp
19.354 + val ist_ctxt = Ctree.get_loc pt (p, p_);
19.355 + (*case*) tac (*of*);
19.356 +
19.357 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
19.358 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Problem pI), (pt, pos as (p, _)))
19.359 + = (tac, (pt, (p, p_')));
19.360 + val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
19.361 + PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
19.362 + (oris, dI, dI', pI', probl, ctxt)
19.363 + val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
19.364 + val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
19.365 +(*-------------------- stop step into me Specify_Theory --------------------------------------*)
19.366 +\<close> ML \<open>(*-------------- stop step into me Specify_Theory --------------------------------------*)
19.367 +(*\\------------------ step into me Specify_Theory -----------------------------------------//*)
19.368 +\<close> ML \<open>(*\\------------ step into me Specify_Theory -----------------------------------------//*)
19.369 +\<close> ML \<open>
19.370 +val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt''' p''' c pt'''; val Specify_Method ["Optimisation", "by_univariate_calculus"] = nxt'''';
19.371 +
19.372 +\<close> ML \<open>
19.373 +(*//------------------ step into me Specify_Problem ----------------------------------------\\*)
19.374 +\<close> ML \<open>(*//------------------ step into me Specify_Problem ----------------------------------------\\*)
19.375 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');
19.376 + val ctxt = Ctree.get_ctxt pt p
19.377 +
19.378 + val ("ok", (_, _, ptp as (pt''''', p'''''))) =
19.379 + (*case*)
19.380 + Step.by_tactic tac (pt, p) (*of*);
19.381 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
19.382 +
19.383 + (*case*)
19.384 + Step.check tac (pt, p) (*of*);
19.385 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
19.386 + (*if*) Tactic.for_specify tac (*then*);
19.387 +
19.388 +Specify_Step.check tac (ctree, pos);
19.389 +"~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))
19.390 + = (tac, (ctree, pos));
19.391 + val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
19.392 + Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
19.393 + => (oris, dI, pI, dI', pI', itms)
19.394 + val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
19.395 +(*-------------------- stop step into Step.do_next -------------------------------------------*)
19.396 +(*-------------------- stop step into me Specify_Problem -------------------------------------*)
19.397 +
19.398 +val (p, pt, nxt) = (p''''', pt''''', nxt'''); (* kept for continuing me *)
19.399 +
19.400 + (*case*)
19.401 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
19.402 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
19.403 + (*if*) Pos.on_calc_end ip (*else*);
19.404 + val (_, probl_id, _) = Calc.references (pt, p);
19.405 +val _ =
19.406 + (*case*) tacis (*of*);
19.407 + (*if*) probl_id = Problem.id_empty (*else*);
19.408 +
19.409 + Step.switch_specify_solve p_ (pt, ip);
19.410 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
19.411 + (*if*) Pos.on_specification ([], state_pos) (*then*);
19.412 +
19.413 + Step.specify_do_next (pt, input_pos);
19.414 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
19.415 + val (_, (p_', tac)) = Specify.find_next_step ptp
19.416 + val ist_ctxt = Ctree.get_loc pt (p, p_)
19.417 +val _ =
19.418 + (*case*) tac (*of*);
19.419 +
19.420 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
19.421 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
19.422 + = (tac, (pt, (p, p_')));
19.423 +
19.424 + val (o_model, ctxt, i_model) =
19.425 +Specify_Step.complete_for id (pt, pos);
19.426 +"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
19.427 + val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
19.428 + ...} = Calc.specify_data (ctree, pos);
19.429 + val ctxt = Ctree.get_ctxt ctree pos
19.430 + val (dI, _, _) = References.select_input o_refs refs;
19.431 + val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
19.432 + val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
19.433 + val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
19.434 + val thy = ThyC.get_theory_PIDE ctxt dI
19.435 + val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
19.436 +(*-------------------- stop step into me Specify_Problem -------------------------------------*)
19.437 +(*\\------------------ step into me Specify_Problem ----------------------------------------//*)
19.438 +
19.439 +val (p''',_,f,nxt''',_,pt''') = me nxt'''' p'''' c pt''''; val Add_Given "FunctionVariable a" = nxt''';
19.440 +(*//------------------ step into me Specify_Method -----------------------------------------\\*)
19.441 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt'''', p'''', c, pt'''');
19.442 + val ctxt = Ctree.get_ctxt pt p
19.443 + val (pt, p) =
19.444 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
19.445 + case Step.by_tactic tac (pt, p) of
19.446 + ("ok", (_, _, ptp)) => ptp;
19.447 +
19.448 + (*case*)
19.449 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
19.450 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
19.451 + (*if*) Pos.on_calc_end ip (*else*);
19.452 + val (_, probl_id, _) = Calc.references (pt, p);
19.453 +val _ =
19.454 + (*case*) tacis (*of*);
19.455 + (*if*) probl_id = Problem.id_empty (*else*);
19.456 +
19.457 + Step.switch_specify_solve p_ (pt, ip);
19.458 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
19.459 + (*if*) Pos.on_specification ([], state_pos) (*then*);
19.460 +
19.461 + Step.specify_do_next (pt, input_pos);
19.462 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
19.463 +
19.464 + val (_, (p_', tac)) =
19.465 + Specify.find_next_step ptp;
19.466 +"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
19.467 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
19.468 + spec = refs, ...} = Calc.specify_data (pt, pos);
19.469 + val ctxt = Ctree.get_ctxt pt pos;
19.470 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
19.471 + (*if*) p_ = Pos.Pbl (*else*);
19.472 +
19.473 + Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
19.474 +"~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
19.475 + = (ctxt, oris, (o_refs, refs), (pbl, met));
19.476 + val cmI = if mI = MethodC.id_empty then mI' else mI;
19.477 + val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
19.478 + val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
19.479 +val NONE =
19.480 + (*case*) find_first (I_Model.is_error o #5) met (*of*);
19.481 +
19.482 + (*case*)
19.483 + Specify.item_to_add (ThyC.get_theory_PIDE ctxt
19.484 + (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
19.485 +"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
19.486 + = ((ThyC.get_theory_PIDE ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
19.487 +(*-------------------- stop step into me Specify_Method --------------------------------------*)
19.488 +(*\\------------------ step into me Specify_Method -----------------------------------------//*)
19.489 +
19.490 +val (p,_,f,nxt,_,pt) = me nxt''' p''' c pt'''; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;
19.491 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
19.492 +(*
19.493 + nxt would be Tactic.Apply_Method, which tries to determine a next step in the ***Program***,
19.494 + but the Program is not yet perfectly implemented.
19.495 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.496 +*)
19.497 +\<close> ML \<open>
19.498 +\<close> ML \<open>
19.499 +\<close> ML \<open>
19.500 \<close>
19.501
19.502 section \<open>===================================================================================\<close>
20.1 --- a/test/Tools/isac/Test_Theory.thy Thu Jan 26 19:02:41 2023 +0100
20.2 +++ b/test/Tools/isac/Test_Theory.thy Sat Jan 28 13:21:39 2023 +0100
20.3 @@ -47,7 +47,6 @@
20.4 (*//------------------ build new fun XXXXX -------------------------------------------------\\*)
20.5 (*\\------------------ build new fun XXXXX -------------------------------------------------//*)
20.6 \<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)
20.7 -\<close> ML \<open>
20.8 \<close>
20.9 ML \<open>
20.10 \<close> ML \<open>
20.11 @@ -67,45 +66,25 @@
20.12 declare [[ML_exception_trace]]
20.13 \<close>
20.14
20.15 -section \<open>=================================================================\<close>
20.16 +section \<open>===================================================================================\<close>
20.17 ML \<open>
20.18 \<close> ML \<open>
20.19 \<close> ML \<open>
20.20 \<close> ML \<open>
20.21 -\<close> ML \<open>
20.22 -\<close> ML \<open>
20.23 -\<close> ML \<open>
20.24 \<close>
20.25
20.26 -section \<open>=========="Minisubpbl/100-init-rootpbl.sml"========================================\<close>
20.27 +section \<open>===================================================================================\<close>
20.28 ML \<open>
20.29 \<close> ML \<open>
20.30 \<close> ML \<open>
20.31 \<close> ML \<open>
20.32 -\<close> ML \<open>
20.33 -\<close> ML \<open>
20.34 -\<close> ML \<open>
20.35 \<close>
20.36
20.37 -section \<open>=================================================================\<close>
20.38 +section \<open>===================================================================================\<close>
20.39 ML \<open>
20.40 \<close> ML \<open>
20.41 \<close> ML \<open>
20.42 \<close> ML \<open>
20.43 -\<close> ML \<open>
20.44 -\<close> ML \<open>
20.45 -\<close> ML \<open>
20.46 -\<close>
20.47 -
20.48 -section \<open>=================================================================\<close>
20.49 -ML \<open>
20.50 -\<close> ML \<open>
20.51 -\<close> ML \<open>
20.52 -\<close> ML \<open>
20.53 -\<close> ML \<open>
20.54 -\<close> ML \<open>
20.55 -\<close> ML \<open>
20.56 -\<close> ML \<open>
20.57 \<close>
20.58
20.59 section \<open>code for copy & paste ===============================================================\<close>