1.1 --- a/TODO.md Sun May 29 12:17:09 2022 +0200
1.2 +++ b/TODO.md Sun May 29 19:00:35 2022 +0200
1.3 @@ -65,3 +65,7 @@
1.4 ML \<open>
1.5 val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
1.6 \<close>
1.7 +
1.8 +* WN: for calculation by use of Makarius' "problem" as boilerplate clarify
1.9 + - reasons to have some parsers local (initially parse_cas, parse_methods, ml in Outer_Syntax.command..problem)
1.10 + -
2.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Sun May 29 12:17:09 2022 +0200
2.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Sun May 29 19:00:35 2022 +0200
2.3 @@ -6,17 +6,71 @@
2.4 *)
2.5
2.6 theory Calculation
2.7 -imports
2.8 -(**)"$ISABELLE_ISAC/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*)
2.9 -(**)"$ISABELLE_ISAC/MathEngine/MathEngine"
2.10 -(** )"SPARK_FDL" ( * remove after devel.of BridgeJEdit*)
2.11 + imports
2.12 + (**)"$ISABELLE_ISAC/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*)
2.13 + (**)"$ISABELLE_ISAC/MathEngine/MathEngine"
2.14 + (** )"SPARK_FDL" ( * remove after devel.of BridgeJEdit*)
2.15 + keywords "Example" :: thy_decl
2.16
2.17 begin
2.18
2.19 ML_file "parseC.sml"
2.20 ML_file "preliminary.sml"
2.21
2.22 -section \<open>new code for Outer_Syntax Example, Problem, ...\<close>
2.23 +section \<open>new code for Outer_Syntax Example ...\<close>
2.24 +text \<open> UPDATE:
2.25 +1. The code re-uses Makarius' \<open>Outer_Syntax.command..problem ..\<close> to a maximal extent.
2.26 +2. GOON
2.27 +\<close>
2.28
2.29 +ML \<open>
2.30 +\<close> ML \<open>
2.31 +\<close> ML \<open>
2.32 +structure Data = Theory_Data
2.33 +(
2.34 + type T = Rule_Set.T option;
2.35 + val empty = NONE;
2.36 + val extend = I;
2.37 + fun merge _ = NONE;
2.38 +);
2.39
2.40 -end
2.41 \ No newline at end of file
2.42 +val set_data = Data.put o SOME;
2.43 +val the_data = the o Data.get;
2.44 +
2.45 +\<close> ML \<open>
2.46 +\<close> ML \<open>
2.47 +\<close> ML \<open>
2.48 +
2.49 +\<close> ML \<open>
2.50 +local
2.51 +
2.52 +(*this assigns code to the keyword ---vvvvvvvvv, without error message here but
2.53 + with error message in Demo_Example ?!? *)
2.54 +val _ =
2.55 + Outer_Syntax.command \<^command_keyword>\<open>Example\<close>
2.56 + "prepare ISAC problem type and register it to Knowledge Store"
2.57 + (Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name --
2.58 + Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Problem.parse_authors --
2.59 + Problem.parse_methods -- Problem.parse_cas -- Problem.parse_model_input)) >>
2.60 + (fn (name, (id, ((((source, maa), mets), cas), model_input))) =>
2.61 + Toplevel.theory (fn thy =>
2.62 + let
2.63 + val pblID = References_Def.explode_id id;
2.64 + val metIDs = map References_Def.explode_id mets;
2.65 + val set_data =
2.66 + ML_Context.expression (Input.pos_of source)
2.67 + (Problem.ml "Theory.setup (Problem.set_data ("
2.68 + @ ML_Lex.read_source source @ Problem.ml "))")
2.69 + |> Context.theory_map;
2.70 + val input = the_data (set_data thy);
2.71 + val arg = Problem.prep_input thy name maa Problem.id_empty (pblID, model_input, input, cas, metIDs);
2.72 + in KEStore_Elems.add_pbts [arg] thy end)))
2.73 +
2.74 +in end;
2.75 +\<close> ML \<open>
2.76 +\<close> ML \<open>
2.77 +\<close> ML \<open>
2.78 +\<close>
2.79 +
2.80 +
2.81 +end
3.1 --- a/src/Tools/isac/BridgeJEdit/Calculation_OLD.thy Sun May 29 12:17:09 2022 +0200
3.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation_OLD.thy Sun May 29 19:00:35 2022 +0200
3.3 @@ -12,8 +12,8 @@
3.4 (**)"$ISABELLE_ISAC/MathEngine/MathEngine"
3.5 (**)"SPARK_FDL" (*remove after devel.of BridgeJEdit*)
3.6 keywords
3.7 - "Example" :: thy_load (*(isac_example)~(spark_vcg) ..would involve registering in Isabelle/Scala*)
3.8 - and(**)"Problem" :: thy_decl (*r oot-problem + recursively in Solution *)
3.9 + "ExampleSPARK" :: thy_load (*(isac_example)~(spark_vcg) ..would involve registering in Isabelle/Scala*)
3.10 + and(**)"Problem" :: thy_decl (*root-problem + recursively in Solution *)
3.11 and "Specification" "Model" "References" :: diag (* structure only *)
3.12 and "Solution" :: thy_decl (* structure only *)
3.13 and "Where" "Given" "Find" "Relate" :: prf_decl (* await input of term *)
3.14 @@ -28,9 +28,9 @@
3.15 ML_file "preliminary-OLD.sml"
3.16
3.17
3.18 -section \<open>new code for Outer_Syntax Example, Problem, ...\<close>
3.19 +section \<open>new code for Outer_Syntax ExampleSPARK, Problem, ...\<close>
3.20 text \<open>
3.21 - code for Example, Problem shifted into structure Preliminary.
3.22 + code for ExampleSPARK, Problem shifted into structure Preliminary.
3.23 \<close>
3.24
3.25 subsubsection \<open>cp from Pure.thy\<close>
3.26 @@ -109,7 +109,7 @@
3.27 ML \<open>
3.28 \<close> ML \<open>
3.29 val _ =
3.30 - Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"
3.31 + Outer_Syntax.command \<^command_keyword>\<open>ExampleSPARK\<close> "start a Calculation from a Formalise-file"
3.32 (Resources.provide_parse_file -- Parse.parname
3.33 >> (Toplevel.theory o (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*)
3.34 (Preliminary_OLD.load_formalisation @{theory Biegelinie} ParseC_OLD.formalisation)) );
3.35 @@ -194,7 +194,7 @@
3.36
3.37 subsection \<open>runs with test-Example\<close>
3.38 (**)
3.39 -Example \<open>../Examples/exp_Statics_Biegel_Timischl_7-70.str\<close>
3.40 +ExampleSPARK \<open>../Examples/exp_Statics_Biegel_Timischl_7-70.str\<close>
3.41 (**)
3.42 Problem ("Biegelinie", ["Biegelinien"])
3.43 (*1 collapse* )
4.1 --- a/src/Tools/isac/BridgeJEdit/Demo_Example.thy Sun May 29 12:17:09 2022 +0200
4.2 +++ b/src/Tools/isac/BridgeJEdit/Demo_Example.thy Sun May 29 19:00:35 2022 +0200
4.3 @@ -9,30 +9,32 @@
4.4 imports Calculation
4.5 begin
4.6
4.7 -section \<open>Boilerplate \<close>
4.8 +section \<open>Boilerplate, the example from Isabelle Workshop 2022\<close>
4.9
4.10 subsection \<open>Specification Phase\<close>
4.11 text \<open>Goal for Isabelle Workshop 2022: this part of the example should be ready for demonstration:
4.12 - 1. The keyword "Example" inserts the template underneath
4.13 + 1. The keyword \<open>Example\<close> inserts the template underneath
4.14 2. The template is filled from a (hidden) formalisation with the following items in the
4.15 - 2.1. Model:
4.16 + 2.1. \<open>Model\<close>:
4.17 * Constants _ ("_" indicates some kind of place holder for input)
4.18 * the complete Where-field (the pre-condition), items marked as True | False
4.19 * Maximum _, AdditionalValues _
4.20 * Extremum _, SideCondition _
4.21 - 2.2 References:
4.22 + 2.2 \<open>References\<close>:
4.23 * place holders "_" for input
4.24 - * The toggle switch before RProblem | RMethod is set to RProblem
4.25 + * The toggle switch before \<open>RProblem\<close> | \<open>RMethod\<close> is set to \<open>RProblem\<close>
4.26 This might be postponed after the Isabelle Workshop.
4.27 3. Input to 2.1 is
4.28 * type checked and marked as Type-Error
4.29 * marked as Correct | Superfluous | Incomplete | Unknown (compare Specify/p-model.sml)
4.30 4. Input to 2.2 by selection from a list / tree
4.31 + 5. On update of \<open>RProblem\<close> (in the root problem) also \<open>Problem\<close> is updated;
4.32 + The argument of \<open>Problem\<close> comes with the template and is read-only.
4.33 \<close>
4.34
4.35 subsubsection \<open>Complete Specification\<close>
4.36 text \<open>
4.37 -Example <No.123 a>
4.38 +Example \<open>No.123 a\<close>
4.39 Problem ''univariate_calculus/Optimisation''
4.40 Specification:
4.41 Model:
4.42 @@ -49,7 +51,7 @@
4.43
4.44 subsubsection \<open>Empty Specification\<close>
4.45 text \<open>
4.46 -Example <No.123 a>
4.47 +Example \<open>No.123 a\<close>
4.48 Problem ''univariate_calculus/Optimisation''
4.49 Specification:
4.50 Model:
4.51 @@ -65,8 +67,33 @@
4.52 \<close>
4.53
4.54 section \<open>Stepwise Development\<close>
4.55 +
4.56 subsection \<open>Specification Phase\<close>
4.57 +text \<open> UPDATE:
4.58 +1. The \<open>Example\<close> below is a minimal adaptation of \<open>problem pbl_bieg : "Biegelinien" ..\<close>
4.59 + in Knowledge/Biegelinie.thy.
4.60 +2. GOON
4.61 +\<close>
4.62
4.63 +(*
4.64 +vvvvvvv why raises \<open>Example\<close> exception Option raised (line 82 of "General/basics.ML")? Although
4.65 + * code (Outer_Syntax.command..Example..) and
4.66 + * application (Example pbl_bieg : "Biegelinien".) are exact copies from Makarius?
4.67 + * Although the application below with \<open>problem\<close> works?
4.68 + * Although \<open>ExampleSPARK\<close> is disambiguated in Calculation_OLD.thy ?!?
4.69 + HOW CAN SUCH AN ERROR BE INVESTIGATED ? debugger ? .. ?
4.70 + *)
4.71 +Example pbl_bieg : "Biegelinien" =
4.72 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
4.73 + Method: "IntegrierenUndKonstanteBestimmen2"
4.74 + Given: "Traegerlaenge l_l" "Streckenlast q_q"
4.75 + (* Where: "0 < l_l" ...wait for < and handling Arbfix*)
4.76 + Find: "Biegelinie b_b"
4.77 + Relate: "Randbedingungen r_b"
4.78
4.79 +ML \<open>
4.80 +\<close> ML \<open>
4.81 +\<close> ML \<open>
4.82 +\<close>
4.83
4.84 end
4.85 \ No newline at end of file
5.1 --- a/src/Tools/isac/BridgeJEdit/parseC.sml Sun May 29 12:17:09 2022 +0200
5.2 +++ b/src/Tools/isac/BridgeJEdit/parseC.sml Sun May 29 19:00:35 2022 +0200
5.3 @@ -2,4 +2,24 @@
5.4 Author: Walther Neuper, JKU Linz
5.5
5.6 Outer token syntax for Isabelle/Isac.
5.7 +This file shall be evaluated earlier such that its definitions are available
5.8 +for Outer_Syntax.command Example, problem, method, etc.
5.9 +Be aware, that keywords need to be defined before using in fun-definitions!
5.10 *)
5.11 +
5.12 +signature PARSE_C =
5.13 +sig
5.14 +
5.15 +end
5.16 +
5.17 +(**)
5.18 +structure Parse_C(**): PARSE_C(**) =
5.19 +struct
5.20 +(**)
5.21 +
5.22 +(* auxiliary parsers *)
5.23 +(*-cp from MathEngBasic/problem.sml-*)
5.24 +
5.25 +end
5.26 +
5.27 +
6.1 --- a/src/Tools/isac/BridgeJEdit/preliminary-OLD.sml Sun May 29 12:17:09 2022 +0200
6.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary-OLD.sml Sun May 29 19:00:35 2022 +0200
6.3 @@ -8,7 +8,7 @@
6.4
6.5 signature PRELIMINARY_OLD =
6.6 sig
6.7 - (* for keyword Example *)
6.8 + (* for keyword ExampleSPARK *)
6.9 val store_and_show: theory -> Formalise.T list -> theory -> theory;
6.10 val load_formalisation: theory -> (Fdl_Lexer.T list -> ParseC_OLD.form_model_refs * 'a) ->
6.11 (theory -> Token.file * theory) * string -> theory -> theory
6.12 @@ -18,7 +18,7 @@
6.13 (** )val init_specify: ParseC_OLD.problem -> theory -> theory( **)
6.14 end
6.15
6.16 -(** code for keyword Example **)
6.17 +(** code for keyword ExampleSPARK **)
6.18
6.19 structure Refs_Data = Theory_Data
6.20 (
7.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Sun May 29 12:17:09 2022 +0200
7.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Sun May 29 19:00:35 2022 +0200
7.3 @@ -26,6 +26,9 @@
7.4 val parse_item_names: string parser -> string list parser
7.5 val parse_model_input: model_input parser
7.6 val parse_authors: string list parser
7.7 + val parse_cas: Token.T list -> string option * Token.T list
7.8 + val parse_methods: string list parser
7.9 + val ml: string -> ML_Lex.token Antiquote.antiquote list
7.10
7.11 val from_store: id -> T
7.12 end
7.13 @@ -158,17 +161,15 @@
7.14 parse_tagged_terms \<^keyword>\<open>Relate\<close> "#Relate";
7.15
7.16 val parse_authors = parse_item_names \<^keyword>\<open>Author\<close>;
7.17 +val parse_cas = Scan.option (parse_item \<^keyword>\<open>CAS\<close> Parse.term);
7.18 +val parse_methods = parse_item_names \<^keyword>\<open>Method\<close>;
7.19 +val ml = ML_Lex.read;
7.20
7.21
7.22 (* command definition *)
7.23
7.24 local
7.25
7.26 -val parse_methods = parse_item_names \<^keyword>\<open>Method\<close>;
7.27 -val parse_cas = Scan.option (parse_item \<^keyword>\<open>CAS\<close> Parse.term);
7.28 -
7.29 -val ml = ML_Lex.read;
7.30 -
7.31 val _ =
7.32 Outer_Syntax.command \<^command_keyword>\<open>problem\<close>
7.33 "prepare ISAC problem type and register it to Knowledge Store"