# HG changeset patch # User wneuper # Date 1653843635 -7200 # Node ID d780a93d21b32d0f53e49d30c65b85fdf299a974 # Parent 9d98791b4080c3334b238f159d671c7922de6b54 Calculation 1: minimal changes in code + application diff -r 9d98791b4080 -r d780a93d21b3 TODO.md --- a/TODO.md Sun May 29 12:17:09 2022 +0200 +++ b/TODO.md Sun May 29 19:00:35 2022 +0200 @@ -65,3 +65,7 @@ ML \ val rewrite_trace = Attrib.setup_config_bool \<^binding>\rewrite_trace\ (K false); \ + +* WN: for calculation by use of Makarius' "problem" as boilerplate clarify + - reasons to have some parsers local (initially parse_cas, parse_methods, ml in Outer_Syntax.command..problem) + - diff -r 9d98791b4080 -r d780a93d21b3 src/Tools/isac/BridgeJEdit/Calculation.thy --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Sun May 29 12:17:09 2022 +0200 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Sun May 29 19:00:35 2022 +0200 @@ -6,17 +6,71 @@ *) theory Calculation -imports -(**)"$ISABELLE_ISAC/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*) -(**)"$ISABELLE_ISAC/MathEngine/MathEngine" -(** )"SPARK_FDL" ( * remove after devel.of BridgeJEdit*) + imports + (**)"$ISABELLE_ISAC/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*) + (**)"$ISABELLE_ISAC/MathEngine/MathEngine" + (** )"SPARK_FDL" ( * remove after devel.of BridgeJEdit*) + keywords "Example" :: thy_decl begin ML_file "parseC.sml" ML_file "preliminary.sml" -section \new code for Outer_Syntax Example, Problem, ...\ +section \new code for Outer_Syntax Example ...\ +text \ UPDATE: +1. The code re-uses Makarius' \Outer_Syntax.command..problem ..\ to a maximal extent. +2. GOON +\ +ML \ +\ ML \ +\ ML \ +structure Data = Theory_Data +( + type T = Rule_Set.T option; + val empty = NONE; + val extend = I; + fun merge _ = NONE; +); -end \ No newline at end of file +val set_data = Data.put o SOME; +val the_data = the o Data.get; + +\ ML \ +\ ML \ +\ ML \ + +\ ML \ +local + +(*this assigns code to the keyword ---vvvvvvvvv, without error message here but + with error message in Demo_Example ?!? *) +val _ = + Outer_Syntax.command \<^command_keyword>\Example\ + "prepare ISAC problem type and register it to Knowledge Store" + (Parse.name -- Parse.!!! (\<^keyword>\:\ |-- Parse.name -- + Parse.!!! (\<^keyword>\=\ |-- Parse.ML_source -- Problem.parse_authors -- + Problem.parse_methods -- Problem.parse_cas -- Problem.parse_model_input)) >> + (fn (name, (id, ((((source, maa), mets), cas), model_input))) => + Toplevel.theory (fn thy => + let + val pblID = References_Def.explode_id id; + val metIDs = map References_Def.explode_id mets; + val set_data = + ML_Context.expression (Input.pos_of source) + (Problem.ml "Theory.setup (Problem.set_data (" + @ ML_Lex.read_source source @ Problem.ml "))") + |> Context.theory_map; + val input = the_data (set_data thy); + val arg = Problem.prep_input thy name maa Problem.id_empty (pblID, model_input, input, cas, metIDs); + in KEStore_Elems.add_pbts [arg] thy end))) + +in end; +\ ML \ +\ ML \ +\ ML \ +\ + + +end diff -r 9d98791b4080 -r d780a93d21b3 src/Tools/isac/BridgeJEdit/Calculation_OLD.thy --- a/src/Tools/isac/BridgeJEdit/Calculation_OLD.thy Sun May 29 12:17:09 2022 +0200 +++ b/src/Tools/isac/BridgeJEdit/Calculation_OLD.thy Sun May 29 19:00:35 2022 +0200 @@ -12,8 +12,8 @@ (**)"$ISABELLE_ISAC/MathEngine/MathEngine" (**)"SPARK_FDL" (*remove after devel.of BridgeJEdit*) keywords - "Example" :: thy_load (*(isac_example)~(spark_vcg) ..would involve registering in Isabelle/Scala*) - and(**)"Problem" :: thy_decl (*r oot-problem + recursively in Solution *) + "ExampleSPARK" :: thy_load (*(isac_example)~(spark_vcg) ..would involve registering in Isabelle/Scala*) + and(**)"Problem" :: thy_decl (*root-problem + recursively in Solution *) and "Specification" "Model" "References" :: diag (* structure only *) and "Solution" :: thy_decl (* structure only *) and "Where" "Given" "Find" "Relate" :: prf_decl (* await input of term *) @@ -28,9 +28,9 @@ ML_file "preliminary-OLD.sml" -section \new code for Outer_Syntax Example, Problem, ...\ +section \new code for Outer_Syntax ExampleSPARK, Problem, ...\ text \ - code for Example, Problem shifted into structure Preliminary. + code for ExampleSPARK, Problem shifted into structure Preliminary. \ subsubsection \cp from Pure.thy\ @@ -109,7 +109,7 @@ ML \ \ ML \ val _ = - Outer_Syntax.command \<^command_keyword>\Example\ "start a Calculation from a Formalise-file" + Outer_Syntax.command \<^command_keyword>\ExampleSPARK\ "start a Calculation from a Formalise-file" (Resources.provide_parse_file -- Parse.parname >> (Toplevel.theory o (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*) (Preliminary_OLD.load_formalisation @{theory Biegelinie} ParseC_OLD.formalisation)) ); @@ -194,7 +194,7 @@ subsection \runs with test-Example\ (**) -Example \../Examples/exp_Statics_Biegel_Timischl_7-70.str\ +ExampleSPARK \../Examples/exp_Statics_Biegel_Timischl_7-70.str\ (**) Problem ("Biegelinie", ["Biegelinien"]) (*1 collapse* ) diff -r 9d98791b4080 -r d780a93d21b3 src/Tools/isac/BridgeJEdit/Demo_Example.thy --- a/src/Tools/isac/BridgeJEdit/Demo_Example.thy Sun May 29 12:17:09 2022 +0200 +++ b/src/Tools/isac/BridgeJEdit/Demo_Example.thy Sun May 29 19:00:35 2022 +0200 @@ -9,30 +9,32 @@ imports Calculation begin -section \Boilerplate \ +section \Boilerplate, the example from Isabelle Workshop 2022\ subsection \Specification Phase\ text \Goal for Isabelle Workshop 2022: this part of the example should be ready for demonstration: - 1. The keyword "Example" inserts the template underneath + 1. The keyword \Example\ inserts the template underneath 2. The template is filled from a (hidden) formalisation with the following items in the - 2.1. Model: + 2.1. \Model\: * Constants _ ("_" indicates some kind of place holder for input) * the complete Where-field (the pre-condition), items marked as True | False * Maximum _, AdditionalValues _ * Extremum _, SideCondition _ - 2.2 References: + 2.2 \References\: * place holders "_" for input - * The toggle switch before RProblem | RMethod is set to RProblem + * The toggle switch before \RProblem\ | \RMethod\ is set to \RProblem\ This might be postponed after the Isabelle Workshop. 3. Input to 2.1 is * type checked and marked as Type-Error * marked as Correct | Superfluous | Incomplete | Unknown (compare Specify/p-model.sml) 4. Input to 2.2 by selection from a list / tree + 5. On update of \RProblem\ (in the root problem) also \Problem\ is updated; + The argument of \Problem\ comes with the template and is read-only. \ subsubsection \Complete Specification\ text \ -Example +Example \No.123 a\ Problem ''univariate_calculus/Optimisation'' Specification: Model: @@ -49,7 +51,7 @@ subsubsection \Empty Specification\ text \ -Example +Example \No.123 a\ Problem ''univariate_calculus/Optimisation'' Specification: Model: @@ -65,8 +67,33 @@ \ section \Stepwise Development\ + subsection \Specification Phase\ +text \ UPDATE: +1. The \Example\ below is a minimal adaptation of \problem pbl_bieg : "Biegelinien" ..\ + in Knowledge/Biegelinie.thy. +2. GOON +\ +(* +vvvvvvv why raises \Example\ exception Option raised (line 82 of "General/basics.ML")? Although + * code (Outer_Syntax.command..Example..) and + * application (Example pbl_bieg : "Biegelinien".) are exact copies from Makarius? + * Although the application below with \problem\ works? + * Although \ExampleSPARK\ is disambiguated in Calculation_OLD.thy ?!? + HOW CAN SUCH AN ERROR BE INVESTIGATED ? debugger ? .. ? + *) +Example pbl_bieg : "Biegelinien" = + \Rule_Set.append_rules "empty" Rule_Set.empty []\ + Method: "IntegrierenUndKonstanteBestimmen2" + Given: "Traegerlaenge l_l" "Streckenlast q_q" + (* Where: "0 < l_l" ...wait for < and handling Arbfix*) + Find: "Biegelinie b_b" + Relate: "Randbedingungen r_b" +ML \ +\ ML \ +\ ML \ +\ end \ No newline at end of file diff -r 9d98791b4080 -r d780a93d21b3 src/Tools/isac/BridgeJEdit/parseC.sml --- a/src/Tools/isac/BridgeJEdit/parseC.sml Sun May 29 12:17:09 2022 +0200 +++ b/src/Tools/isac/BridgeJEdit/parseC.sml Sun May 29 19:00:35 2022 +0200 @@ -2,4 +2,24 @@ Author: Walther Neuper, JKU Linz Outer token syntax for Isabelle/Isac. +This file shall be evaluated earlier such that its definitions are available +for Outer_Syntax.command Example, problem, method, etc. +Be aware, that keywords need to be defined before using in fun-definitions! *) + +signature PARSE_C = +sig + +end + +(**) +structure Parse_C(**): PARSE_C(**) = +struct +(**) + +(* auxiliary parsers *) +(*-cp from MathEngBasic/problem.sml-*) + +end + + diff -r 9d98791b4080 -r d780a93d21b3 src/Tools/isac/BridgeJEdit/preliminary-OLD.sml --- a/src/Tools/isac/BridgeJEdit/preliminary-OLD.sml Sun May 29 12:17:09 2022 +0200 +++ b/src/Tools/isac/BridgeJEdit/preliminary-OLD.sml Sun May 29 19:00:35 2022 +0200 @@ -8,7 +8,7 @@ signature PRELIMINARY_OLD = sig - (* for keyword Example *) + (* for keyword ExampleSPARK *) val store_and_show: theory -> Formalise.T list -> theory -> theory; val load_formalisation: theory -> (Fdl_Lexer.T list -> ParseC_OLD.form_model_refs * 'a) -> (theory -> Token.file * theory) * string -> theory -> theory @@ -18,7 +18,7 @@ (** )val init_specify: ParseC_OLD.problem -> theory -> theory( **) end -(** code for keyword Example **) +(** code for keyword ExampleSPARK **) structure Refs_Data = Theory_Data ( diff -r 9d98791b4080 -r d780a93d21b3 src/Tools/isac/MathEngBasic/problem.sml --- a/src/Tools/isac/MathEngBasic/problem.sml Sun May 29 12:17:09 2022 +0200 +++ b/src/Tools/isac/MathEngBasic/problem.sml Sun May 29 19:00:35 2022 +0200 @@ -26,6 +26,9 @@ val parse_item_names: string parser -> string list parser val parse_model_input: model_input parser val parse_authors: string list parser + val parse_cas: Token.T list -> string option * Token.T list + val parse_methods: string list parser + val ml: string -> ML_Lex.token Antiquote.antiquote list val from_store: id -> T end @@ -158,17 +161,15 @@ parse_tagged_terms \<^keyword>\Relate\ "#Relate"; val parse_authors = parse_item_names \<^keyword>\Author\; +val parse_cas = Scan.option (parse_item \<^keyword>\CAS\ Parse.term); +val parse_methods = parse_item_names \<^keyword>\Method\; +val ml = ML_Lex.read; (* command definition *) local -val parse_methods = parse_item_names \<^keyword>\Method\; -val parse_cas = Scan.option (parse_item \<^keyword>\CAS\ Parse.term); - -val ml = ML_Lex.read; - val _ = Outer_Syntax.command \<^command_keyword>\problem\ "prepare ISAC problem type and register it to Knowledge Store"