1.1 --- a/TODO.md Tue Feb 07 18:32:58 2023 +0100
1.2 +++ b/TODO.md Wed Feb 08 07:51:39 2023 +0100
1.3 @@ -44,24 +44,12 @@
1.4
1.5 * WN: eliminate multiple get_ctxt in Solve_Step, Ctree
1.6 * WN: shift code from libraryC.sml to designated destination (ThyC, etc)
1.7 -* WN: Know_Store.get_thes, add_thes still required for Error_Patterns, we want to eliminate thes:
1.8 - (1) Error_Pattern.T are already stored by MethodC -- place them in respective thys
1.9 - (2) Error_Pattern.fill_in stored with thm (in thes): instead introduce new Thy_Data for them.
1.10 - adapt Know_Store.insert_fillpats for that purpose.
1.11 - cf. e587c45cae0f note in Build_Thydata.thy
1.12 * WN: rename type Rule.rule -> Rule.T
1.13 -* WN: Sub_Problem.tac_from_prog: use ctxt from pt
1.14 -* WN: in subst_adapt_to_type should ''bdv''(string) handled by Varialbe.declare_constraints
1.15 - ?why is "x" not already typed correctly (by reading strings from Formalise)?)
1.16 -* WN: replace tools derived from get_thes/add_thes by tools derived from current ctxt
1.17 * WN: improve naming in refine.sml, m-match.sml
1.18 -* WN: all UnparseC with Proof.context, cleanup unparseC.sml and calls
1.19 -* WN: all Subst with Proof.context, cleanup unparseC.sml and calls
1.20 * WN: review Prog_Tac:
1.21 (*+isa==isa2*)@{term "Substitution []"}; (*Free ("Subproblem",.. ALSO Subproblem, ?!*)
1.22 (*+isa==isa2*)@{term "Rewrite_Set ''norm_Rational''"}; (*Const ("Prog_Tac.Rewrite_Set",..*)
1.23
1.24 -* WN: Specify/formalise.sml is in BaseDefinitions/ AND Specify/ DELETE ONE VERSION
1.25 * WN: Step_Specify.initialise: remove hdl in return-value, replace Step_Specify.initialise'
1.26 ? which uses initialise !?
1.27 * WN: ? unify "no_met" with "empty_meth_id" from References.empty ?
2.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Tue Feb 07 18:32:58 2023 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Feb 08 07:51:39 2023 +0100
2.3 @@ -89,9 +89,7 @@
2.4 val get_via_last_thy: ThyC.id -> theory (*only used for * (Sub-)problem retrieving respective thy
2.5 * problem refinement
2.6 * CAS_Cmd, to be redesigned anyway
2.7 - * Ctree.get_ctxt
2.8 - * ThmC.long_id
2.9 - * in fun UnparseC.term_ERROR
2.10 + * Ctree.get_ctxt, ThmC.long_id
2.11 * in ContextC.for_ERROR *)
2.12 end;
2.13
3.1 --- a/src/Tools/isac/Specify/formalise.sml Tue Feb 07 18:32:58 2023 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,40 +0,0 @@
3.4 -(* Title: Specify/formalise.sml
3.5 - Author: Walther Neuper 191026
3.6 - (c) due to copyright terms
3.7 -
3.8 -A formalisation, \<open>Formalise\<close>, contains all items required to automatically solve a calculation
3.9 -(and thus assist students in in all phases of problem solving):
3.10 -(1) the \<open>values\<close> of \<open>Formalise.model\<close> for instantiating a \<open>Problem.model_input\<close>,
3.11 - accompanied with \<open>descriptor\<close>s for students, and
3.12 -(2) \<open>Formalise.refs\<close> as defautlt \<open>References\<close> into Isac's 3-dimensional Know_Store,
3.13 - which can interactively be changed during problem solving.
3.14 -
3.15 -\<open>Formalise\<close> of the root of a calculation might contain items,
3.16 -which are required by \<open>Subproblem\<close>s (e.g. "errorBound" in case an equation
3.17 -cannot be solved symbolically and thus is solved numerically).
3.18 -*)
3.19 -signature FORMALISE =
3.20 -sig
3.21 - type T
3.22 - val empty: T
3.23 -
3.24 - type model(*TODO revise: model list together with ERROR in
3.25 -https://hg.risc.uni-linz.ac.at/wneuper/isa/file/51f6113384db/test/Tools/isac/BridgeJEdit/vscode-example.sml#l98*)
3.26 - type spec (*TODO: rename -> refs*)
3.27 -end
3.28 -
3.29 -(**)
3.30 -structure Formalise(**): FORMALISE(**) =
3.31 -struct
3.32 -(**)
3.33 -
3.34 -type model = Model_Def.form_model;
3.35 -type spec = Model_Def.form_refs;
3.36 -
3.37 -(* a formalization of an example contains data
3.38 - sufficient for mechanically finding the solution for the example.
3.39 - FIXME.WN051014: dont store form_T = (_,form_refs) in the PblObj, this is done in origin *)
3.40 -type T = Model_Def.form_T;
3.41 -val empty = Model_Def.form_empty;
3.42 -
3.43 -(**)end(**);
4.1 --- a/test/Tools/isac/ADDTESTS/session-get_theory/Bar.thy Tue Feb 07 18:32:58 2023 +0100
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,9 +0,0 @@
4.4 -theory Bar imports Pure begin
4.5 -ML \<open>
4.6 - val bar_data = "bar_data"
4.7 -\<close>
4.8 -(*
4.9 - in case we started with "./bin/isabelle jedit -l Bar"
4.10 - we see the error "Cannot update finished theory "Bar.Bar""
4.11 -*)
4.12 -end
5.1 --- a/test/Tools/isac/ADDTESTS/session-get_theory/Foo.thy Tue Feb 07 18:32:58 2023 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,9 +0,0 @@
5.4 -theory Foo imports Bar begin
5.5 -ML \<open>
5.6 - @{theory Bar}; (*OK *)
5.7 -(*Thy_Info.get_theory "Bar"; ERROR 'Theory loader: undefined theory entry for "Bar"'*)
5.8 - case Thy_Info.lookup_theory "Bar.Bar" of
5.9 - NONE => writeln "Expected, if Foo.thy is loaded directly. "
5.10 - | SOME _ => writeln "Expected, if Foo.thy is loaded from: ./bin/isabelle jedit -l Bar"
5.11 -\<close>
5.12 -end
6.1 --- a/test/Tools/isac/ADDTESTS/session-get_theory/ROOT Tue Feb 07 18:32:58 2023 +0100
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,9 +0,0 @@
6.4 -session Bar = Pure +
6.5 - description "
6.6 - Trial to make the theory loader able to 'Thy_Info.get_theory Bar' in Foo.thy.
6.7 - This only works if ~~/ROOTS is extended by a session created with
6.8 - ./bin/isabelle build -v -b Bar
6.9 - See https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-September/msg00060.html.
6.10 - "
6.11 - options [document = false]
6.12 - theories Bar