1.1 --- a/TODO.md Thu Aug 04 14:18:35 2022 +0200
1.2 +++ b/TODO.md Thu Aug 04 15:24:58 2022 +0200
1.3 @@ -1,22 +1,3 @@
1.4 -* MW: make Outer_Syntax.command \<^command_keyword>\<open>problem\<close> a model for ..\<open>Example\<close>
1.5 - An ML syntax error should be indicated in place (in the string after \<^keyword>\<open>Given\<close> etc)
1.6 - and not on the definition as a whole.
1.7 - - in MathEngBasic/problem "Outer_Syntax.command \<^command_keyword>\<open>problem\<close>" there are writeln
1.8 - and comments with testdata from "problem pbl_bieg : "Biegelinien"" in Biegelinie.thy
1.9 - - in MathEngBasic/problem there is guesswork ("TODO") how to reorganise "fun prep_input_PIDE"
1.10 - such that errors in "Given" etc are indicated WITHIN the term.
1.11 -
1.12 -* ?MW?: In Outer_Syntax.command \<^command_keyword>\<open>Example\<close> is there a quick fix
1.13 - for successfully replacing hacked Problem.parse_cas by parse_references_input?
1.14 - (a) In addition to replacing Problem.parse_cas: How implement the optional parser:
1.15 - - Example "Diff_App/No.123 a" + NONE
1.16 - - Example "Diff_App/No.123 a" + SOME (probl_id, model_input, refs_input)
1.17 - i.e. we expect ISAC to present an empty template "Problem..Solution", but as a whole, to the user;
1.18 - see VSCode_Example.thy subsubsection \<open>Specification step by step\<close>
1.19 - How get Token.src for testing purposes?
1.20 - How can Scan.* be traced?
1.21 - (Tracing should help understanding Problem.parse_cas, Problem.parse_model_input which involve Scan.*)
1.22 -
1.23 * MW: clarify/eliminate Isabelle/Scala add-ons (presently unused)
1.24
1.25 diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/build-jars ./src/Pure/build-jars
1.26 @@ -27,58 +8,67 @@
1.27 76a77
1.28 > "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
1.29
1.30 -* Eliminate Thy_Info.get_theory eventually: should take theory from ancestory
1.31 - within current context.
1.32 - cf. e587c45cae0f note in Build_Thydata.thy
1.33 +
1.34 +***** some items for discussion
1.35 +
1.36 +* What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
1.37 + https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf distinguishes
1.38 + several kinds of ISAC users, in particular "math author (Mathematik-Autor)" and
1.39 + "course designer (Kurs-Designer)". The latter just adds examples which re-use existing
1.40 + knowledge designed by the former. KEStore_Elems.add_thes is an interface for the latter.
1.41 + KEStore_Elems.get_thes and KEStore_Elems.add_thes are ONLY required for the Lucas-Interpreter
1.42 + retrieving Thm and Rls from string-identifiers (which do NOT indicate the theory of) --
1.43 + -- get_thes and add_thes are the main reason for (b)
1.44 + So: How can KEStore_Elems.get_thes and KEStore_Elems.add_thes be replaced in current Isabelle?
1.45
1.46 * Clarify symmetric rule: Thm.apply_attribute Calculation.symmetric thm context (!?);
1.47 ??
1.48
1.49 +* "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
1.50 + takes only static arguments ----------------^^^^^^^^^^^^^^, not value of "hd_ord (f, g)"
1.51 + ? are there better approximations to old output of (*1*) than with (*2*)
1.52 + (*1*)val _ = tracing ("hd_ord (f, g) = " ^ ((pr_ord o hd_ord) (f, g)) );
1.53 + (*2*)val _ = @{print tracing}{a = "hd_ord (f, g) = ", z = hd_ord (f, g)}(**)
1.54 +
1.55 * KEStore_Elems: Should we eliminate union_overwrite and use standard namespace merge?
1.56 (Exception: rlss with its special cross-theory merge.)
1.57 ? how adapt the different signatures ?
1.58 union_overwrite: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
1.59 merge : ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
1.60
1.61 -* What is the purpose of "#numeral" instead of plain numeral?
1.62 - ??
1.63
1.64 -* Check/clarify Context.theory_name vs. Context.theory_long_name.
1.65 - present ISAC assumes 2 sessions in the MathEngine, Specify and Interpret,
1.66 - and all Isac_Knowledge is in session Isac.
1.67 - So Context.theory_name suffices
1.68 +***** for the few items below WN asks MW for help
1.69
1.70 -* Eliminate mutable Rewrite_Ord.id (!?);
1.71 - shall be done in connection with cf. e587c45cae0f note in Build_Thydata.thy
1.72 +* MW: make Outer_Syntax.command \<^command_keyword>\<open>problem\<close> a model for ..\<open>Example\<close>
1.73 + The model should demonstrate, how an ML syntax error is indicated in place
1.74 + (in the string after \<^keyword>\<open>Given\<close> etc) and not on the definition as a whole.
1.75 + - in MathEngBasic/problem "Outer_Syntax.command \<^command_keyword>\<open>problem\<close>" there are writeln
1.76 + and comments with testdata from "problem pbl_bieg : "Biegelinien"" in Biegelinie.thy
1.77 + - in MathEngBasic/problem there is guesswork ("TODO") how to reorganise "fun prep_input_PIDE"
1.78 + such that errors in "Given" etc are indicated WITHIN the term.
1.79
1.80 -* What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
1.81 - https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf distinguishes
1.82 - several kinds of ISAC users, in particular "math author (Mathematik-Autor)" and
1.83 - "course designer (Kurs-Designer)". The latter just adds examples which re-use existing
1.84 - knowledge designed by the former. KEStore_Elems.add_thes is an interface for the latter.
1.85 +* MW: In Outer_Syntax.command \<^command_keyword>\<open>Example\<close> is there a quick fix
1.86 + for successfully replacing hacked Problem.parse_cas by parse_references_input?
1.87 + (a) In addition to replacing Problem.parse_cas: How implement the optional parser:
1.88 + - Example "Diff_App/No.123 a" + NONE
1.89 + - Example "Diff_App/No.123 a" + SOME (probl_id, model_input, refs_input)
1.90 + i.e. we expect ISAC to present an empty template "Problem..Solution", but as a whole, to the user;
1.91 + see VSCode_Example.thy subsubsection \<open>Specification step by step\<close>
1.92 + How get Token.src for testing purposes?
1.93 + How can Scan.* be traced?
1.94 + (Tracing should help understanding Problem.parse_cas, Problem.parse_model_input which involve Scan.* )
1.95
1.96 -* WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
1.97 - e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";
1.98 +* ?How represent items, which have not yet been input?
1.99 + Note: For the purpose of user-guidance the format of requested input should be indicated!
1.100 + - proposal for how to indicate requested input: in VSCode_Example.thy subsubsection \<open>Empty Specification>
1.101 + - the trial with <fun is_empty> in Calculation.thy makes the question more precise:
1.102 + better hack parsers or better work on ML_Syntax?
1.103
1.104 -* WN: Avoid Thm.get_name_hint and use Global_Theory.get_thm instead, get theory from References.T
1.105 - and push theory through as argument of respective functions.
1.106
1.107 -* WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations
1.108 - - quite often "axiomatization ..." can be turned into "lemma ... by auto"
1.109 - without further ado;
1.110 - - sometimes this requires to use more specific types / type classes;
1.111 - - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
1.112 - - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
1.113 +***** priority of WN items is top down, most urgent/simple on top
1.114
1.115 -* WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
1.116 - takes only static arguments ----------------^^^^^^^^^^^^^^, not value of "hd_ord (f, g)"
1.117 - ? are there better approximations to old output of (*1*) than with (*2*)
1.118 - (*1*)val _ = tracing ("hd_ord (f, g) = " ^ ((pr_ord o hd_ord) (f, g)) );
1.119 - (*2*)val _ = @{print tracing}{a = "hd_ord (f, g) = ", z = hd_ord (f, g)}(**)
1.120 -
1.121 -
1.122 -* WN: Calculate.thy: add structure Calculate
1.123 -* WN: cleanup method-def.sml, problem-def.sml, "eval-def.sml", "rewrite-order.sml"
1.124 +* WN: cleanup method-def.sml, problem-def.sml,
1.125 +* WN: Calculate.thy: add structure Calculate, also signature EXAMPLE
1.126 * WN: MethodC.from_store throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument
1.127
1.128 * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
1.129 @@ -90,21 +80,32 @@
1.130 - Eval.adhoc_thm, adhoc_thm1_
1.131 - ? LIST IS NOT COMPLETE
1.132
1.133 +* WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
1.134 + e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";
1.135 +
1.136 * WN: ? Rational.Cancel_p; extend use of \<^theory> to \<^theory_context>
1.137
1.138 +* WN: Avoid Thm.get_name_hint and use Global_Theory.get_thm instead, get theory from References.T
1.139 + and push theory through as argument of respective functions.
1.140 +
1.141 +* WN: Eliminate Thy_Info.get_theory eventually: should take theory from ancestory
1.142 + within current context.
1.143 + cf. e587c45cae0f note in Build_Thydata.thy
1.144 +
1.145 +* WN: Check/clarify Context.theory_name vs. Context.theory_long_name.
1.146 + present ISAC assumes 2 sessions in the MathEngine, Specify and Interpret,
1.147 + and all Isac_Knowledge is in session Isac.
1.148 + So Context.theory_name suffices
1.149 +
1.150 +* WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations
1.151 + - quite often "axiomatization ..." can be turned into "lemma ... by auto"
1.152 + without further ado;
1.153 + - sometimes this requires to use more specific types / type classes;
1.154 + - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
1.155 + - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
1.156 +
1.157 * WN: redesign transition from Specification to Solution: how relate
1.158 - Formalise.model with variants (e.g. VSCode_Example)
1.159 reconsider separation of variants F_I, F_II, see MAWEN paper
1.160 - !?! I_Model of MethodC (fairly free sequence, dependent on Formalise.model)
1.161 - !?! formal arguments of program (fixed sequence)
1.162 -
1.163 -* WN: ?How represent items, which have not yet been input?
1.164 - Note: For the purpose of user-guidance the format of requested input should be indicated!
1.165 - - proposal for how to indicate requested input: in VSCode_Example.thy subsubsection \<open>Empty Specification>
1.166 - - the trial with <fun is_empty> in Calculation.thy makes the question more precise:
1.167 - better hack parsers or better work on ML_Syntax?
1.168 -
1.169 -* WN: as soon as parsing in Outer_Syntax.command..‹Example› works, implement in Calculation
1.170 - - init_ctree, update_status, check_input
1.171 -
1.172 -