theory Test_VSCode_Example

   imports "Isac.Build_Isac" (*"Isac.Calculation"*)

   keywords "Example_TEST" :: thy_decl

 begin

 text \<open>

   Tests here in BridgePIDE are already based on Build_Isac.thy bypassing $ISABELLE_ISAC_TEST.

   TODO: eliminate "Isac." above on eliminating session in $ISABELLE_ISAC_TEST.

 \<close>

 subsection \<open>Development\<close>

 text \<open>

   Here we develop the semantics of \<open>Example_TEST\<close> as test

   --- build Outer_Syntax Example_TEST n:

   and save intermediate states as separate tests in test/../preliminary.sml

   as soon as some stable state is achieved.

   This way we make all \<open>Example\<close> to \<open>Example_TEST\<close> step by step 

   and finally rename all again to \<open>Example\<close>.

 \<close> ML \<open>

 val ((in_thy, thy_id_pos), (in_pbl, probl_id_pos), (in_met, meth_id_pos)) =

   (("__", Position.none), ( "__/__", Position.none), ("__/__", Position.none))

 val in_ = (in_thy, in_pbl, in_met)

 val spec_ as (spec_thy, spec_pbl, spec_met) = References.empty

 val o_ as (o_thy, o_pbl, o_met) =

   ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"])

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (** preliminary handling of References **)

 \<close> ML \<open> (* assumption:  we read the Specfication as a whole *)

 (*/-------------------- state of src/../preliminary.sml at that time  -------------------------\*)

 fun re_eval_all ((*dummyarg*)) = ("re_eval_all if new_thy"; ((*dummyarg*)))

 fun re_eval_pbl ((*dummyarg*)) = ("re_eval_pbl"; ((*dummyarg*)))

 fun re_eval_met ((*dummyarg*)) = ("re_eval_met"; ((*dummyarg*)))

 ;

 re_eval_all: unit -> unit;

 (*

   switch_pbl_met IS MISSING! Greater changes are to expect with respective introduction.

   In the meanwhile we just \<open>re_eval\<close> the \<open>I_Model\<close> of \<open>Problem\<close>;

   in case this is complete, we automatically complete the \<open>I_Model\<close> of \<open>MethodC\<close>

   without displaying the respective \<open>P_Model\<close> and immediately start solve-phase by \<open>Apply_Method\<close>;

 *)

 fun re_eval (input_thy, input_pbl, input_met) (spec_thy, spec_pbl, spec_met) =

   if spec_thy <> input_thy

     then re_eval_all ()

     else if spec_pbl <> input_pbl

       then re_eval_pbl ()

       else if spec_met <> input_met

         then re_eval_met ()

         else ("nothing to re-evaluate"; ((*dummyarg*)))

 ;

 re_eval: References.T -> References.T -> unit

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 (*\-------------------- state of src/../preliminary.sml at that time  -------------------------/*)

 \<close> ML \<open> (*\<longrightarrow> test/../calculation.sml*)

 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------";

 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------";

 "----------- build Outer_Syntax Example_TEST ---------------------------------------------------";

 "----------- build Outer_Syntax Example_TEST: stepwise input, References empty -----------------";

 "----------- build Outer_Syntax Example_TEST: stepwise input, References empty -----------------";

 "----------- build Outer_Syntax Example_TEST: stepwise input, References empty -----------------";

 (*/---------------------------------------- mimic input from PIDE -----------------------------\*)

 (* Example_TEST "Diff_App-No.123a" (*complete Model, empty References*) *)

 val thy = @{theory}

 val model_input = (*type Position.T is hidden, thus redefinition*)

  [("#Given", [("Constants [r = 7]", Position.none)]),

   ("#Where", [("0 < r", Position.none)]),

   ("#Find",

    [("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]),

   ("#Relate",

    [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),

     ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]

 : (Model_Pattern.m_field * (string * Position.T) list) list

 (**)

 val ((thy_id, thy_id_pos), (probl_id, probl_id_pos), (meth_id, meth_id_pos)) =

   (("__", Position.none), ( "__/__", Position.none), ("__/__", Position.none))

 (**)

 val example_id = "Diff_App-No.123a";

 (*\---------------------------------------- mimic input from PIDE -----------------------------/*)

 \<close> ML \<open>

             val state =

               case the_data thy of

                   Ctree.EmptyPtree => Preliminary.init_ctree_TEST thy example_id

                 | _ => the_data thy

 \<close> ML \<open>

                   (*let*)

                     val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =

                       Ctree.get_obj I state [(*Pos will become variable*)] |> Ctree.rep_specify_data

                     val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)

                     val (model, where_) = Model_Pattern.parse_pos_TEST ctxt model_input (*+check syntax*)

 \<close> ML \<open>

 (model, where_) (*GOON*)

 \<close> ML \<open>

 (**)

                     val _ = re_eval References.empty References.empty;

 (**)

 \<close> ML \<open>

             (*in*) Preliminary.update_state_TEST thy

                       (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy)

             (*end*)

 \<close> ML \<open>

 (*POSTPONED Specify.check_input \<longrightarrow> specify.sml*)

 fun check_input _ = 123

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 val _ =

   Outer_Syntax.command \<^command_keyword>\<open>Example_TEST\<close>

     "prepare ISAC problem type and register it to Knowledge Store"

     (Parse.name -- Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --

          \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close>  |-- Problem.parse_pos_model_input --

            (\<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- Parse.!!! References.parse_input_pos

              (** )-- ( \<^keyword>\<open>Solution\<close> -- keyword>\<open>:\<close>)( ** )WHAT IS WRONG HEREWITH?( **)) ) >>

       (fn (example_id, (model_input,

           ((thy_id, thy_id_pos), ((probl_id, probl_id_pos), (meth_id, meth_id_pos)) ) )) =>

         Toplevel.theory (fn thy =>

           let

             val state =

               case the_data thy of

                   Ctree.EmptyPtree => Preliminary.init_ctree_TEST thy example_id

                 | _ =>

                   let

                     val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =

                       Ctree.get_obj I state [] |> Ctree.rep_specify_data

                     val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)

                     val (model, where_) = Model_Pattern.parse_pos_TEST ctxt model_input

 (**)

                     val _ = re_eval References.empty References.empty

 (**)

                   in

                     Preliminary.update_state_TEST thy

                       (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy)

                   end

           in set_data state thy end)));

 \<close> ML \<open>

 \<close> ML \<open> (*Example_TEST below*)

 \<close>

 subsection \<open>Mirror from src/../VSCode_Example.thy for testing purposes\<close>

 subsubsection \<open>Complete Specification at once\<close>

 text \<open>

   Just a test, that this works also in $ISABELLE_ISAC_TEST

 \<close>

 Example "Diff_App-No.123a" (*complete Specification*)

   Specification:

     Model:

       Given: \<open>Constants [r = 7]\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close>

       Relate: \<open>Extremum A = 2 * u * v - u \<up> 2\<close> 

         \<open>SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\<close>

     References:

       Theory_Ref: "Diff_App"

   (*\<Otimes>*) Problem_Ref: "univariate_calculus/Optimisation"

   (*\<Odot>*) Method_Ref: "Optimisation/by_univariate_calculus"

 (*Solution:*)

 text \<open>

   Check complete \<open>Model\<close>, infer empty \<open>References\<close> from data hidden in "Diff_App-No.123a"

 \<close>

 (*

 Example: no syntax check of terms, OK.

 Example_TEST: proper syntax check of terms with Model_Pattern.parse_pos,

   but with parse_pos_TEST ERROR Malformed YXML: unbalanced element "input"

 *)

 (**)Example

 (** )Example_TEST( **) "Diff_App-No.123a" (*complete Model, empty References*)

   Specification:

     Model:

       Given: \<open>Constants [r = 7]\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close>

       Relate: \<open>Extremum (A = 2 * u * v - u \<up> 2)\<close> 

         \<open>SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\<close>

     References: 

       Theory_Ref: "__"

   (*\<Odot>*) Problem_Ref: "__/__"

   (*\<Otimes>*) Method_Ref: "__/__"

 (*Solution:*)

 subsubsection \<open>Empty Specification ready for input by students\<close>

 text \<open>

   In order to help the student (similar to a personal instructur helping a beginner)

   the \<open>Specification\<close> is given as a template,

   where so-called \<open>descriptor\<close>s give hints about the input requested

   (in native language!) and delimiters are (partially) given.

   For the same reason \<open>Where\<close> is already filled; most beginners are 

   not aware of "where_-conditions", i.e. of preconditions.

 \<close>

 Example "Diff_App-No.123a"

   Specification:

     Model:

       Given: \<open>Constants [__=__, __=__]\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum __\<close> \<open>AdditionalValues [__, __]\<close>

       Relate: \<open>Extremum __\<close> 

         \<open>SideConditions [__=__, __=__]\<close>

     References: 

       Theory_Ref: "__"

   (*\<Odot>*) Problem_Ref: "__/__"

   (*\<Otimes>*) Method_Ref: "__/__"

 (*Solution:*)

 subsubsection \<open>Start Example with a CAS_Cmd\<close>

 text \<open>

   The student wants to use Isabelle/Isac like an Algebra System and issues a CAS_Cmd.

   The CAS_Cmd triggers implicit Specification (which usually is not requested 

   in case of CAS_Cmd).

   This user-requirement is not reflected so far. Three possible solutions are sketched below.

 \<close>

 (*----------------------------------------*  )

 Example ""

   Specification (\<open>Simplify (2*a + 3*a)\<close>):

   Solution:

     \<open>2*a + 3*a\<close>

     :

 (  *-----------------------------------------*)

 (*----------------------------------------*  )

 Example \<open>Simplify (2*a + 3*a)\<close>

   Specification:

   Solution:

     \<open>2*a + 3*a\<close>

     :

 (  *----------------------------------------*)

 (*----------------------------------------*  )

 \<open>Simplify (2*a + 3*a)\<close>

   Specification:

   Solution:

     \<open>2*a + 3*a\<close>

     :

 (  *----------------------------------------*)

 subsubsection \<open>Specification step by step\<close>

 text \<open>

   In an electronic textbook there shall be references to examples given, for instance,

   by \<open>Example "Diff_App-No.123a"\<close>. Such a reference shall be easily "activated" 

   to start a Specification + Solution at the spot ?and?or? to open a separate window.

   Activating the reference \<open>Example "Diff_App-No.123a"\<close> shall result in a threefold alternative,

   where (2)=(3) holds for the parsers:

   (1) the Example presents a "normal problem" with a Specification (preferred by engineers),

     see above subsubsection \<open>Empty Specification\<close>,

   (2) the Example presents a "normal problem" without a Specification (preferred in high-school):

     |Example "Diff_App-No.123a"

     |  Specification:

     |  Solution:

     |    ..first formula as given by the specifid Method..

   (3) the Example presents a "CAS_Cmd":

     |Example \<open>Simplify (2*a + 3*a)\<close>

     |  Specification:

     |  Solution:

     |    solve (x + 1 = 2, x)

   \<open>Specification\<close> is always visible in order to remind of the existence.

   \<open>Outer_Syntax.command \<^command_keyword>\<open>Example\<close>\<close> shall be able to parse all three cases

   (while still skipping considerations about \<open>Specification\<close> and sub-problems).

   Below is the Example with case (1):

   * The lines \<open>text --- remove this line and make content Isar input---\\<close>

     and      ---------- remove this line and make content Isar input---/

     will be deleted after correct implementation

   * The \<open>ML \<open>blocks\<close>\<close> in between show, that ISAC is able of "next step guidance"; 

     these can be deleted as well.

   * This Example also shows the toggle between \<open>\<Otimes>\<close> and \<open>\<Odot>\<close>.

 \<close> 

 text \<open>

   # 1: ISAC starts the Example by presenting an "empty" Specification.

   "Presenting" should mean: by "activation" of Example the system presents

   the empty Specification as a template, where the items give hints on the input format.

   The field \<open>Where\<close> is already filled, but editable and shows missing input by \<open>False\<close>.

 \<close>

 ML \<open>

 \<close> ML \<open> (* # 1: At the first call of \<open>Example\<close> ISAC initialises a calculation *)

 val p = ([], Pos.Pbl);

 val pt = Preliminary.update_state @{theory} (*here we have Ctree.EmptyPtree and thus call init_ctree*)

   ("Diff_App-No.123a", 

   ( [("#Given", [("Constants [r = 7]", Position.none)]),

      ("#Where", [("0 < r", Position.none)]), 

      ("#Find", [("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]), 

      ("#Relate", [("Extremum A = 2 * u * v - u \<up> 2", Position.none), 

         ("SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])

     ],

     ("Diff_App", "univariate_calculus/Optimisation", "Optimisation/by_univariate_calculus")

   )

 ) Ctree.EmptyPtree;

 val ptp = (pt, p);

 \<close>

 Example "Diff_App-No.123a"

   Specification:

     Model:

       Given: \<open>Constants [__=__, __=__]\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum __\<close> \<open>AdditionalValues [__, __]\<close>

       Relate: \<open>Extremum __\<close> 

         \<open>SideConditions [__=__, __=__]\<close>

     References: 

       Theory_Ref: "__"

   (*\<Odot>*) Problem_Ref: "__/__"

   (*\<Otimes>*) Method_Ref: "__/__"

 (*Solution:*)

 text \<open>

   # 2: Somewhere in the Model, the user inputs a next item, which is marked "correct" by ISAC.

   By this input Where: \<open>0 < r\<close> is not rendered \<open>False\<close> anymore.

 \<close> 

 ML \<open> (* # 2: Somewhere in the Model, the user inputs a next item *)

 val ("ok", ([(Tactic.Add_Given "Constants [r = 7]", _, _)], _, ptp))

   = Step.specify_do_next ptp;

 \<close>

 Example "Diff_App-No.123a"

   Specification:

     Model:

       Given: \<open>Constants [r = 7]\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum _\<close> \<open>AdditionalValues [__, __]\<close>

       Relate: \<open>Extremum _\<close> \<open>SideConditions [__=__, __=__]\<close>

     References:

       Theory_Ref: "__"

   (*\<Odot>*) Problem_Ref: "__/__"

   (*\<Otimes>*) Method_Ref: "__/__"

 (*Solution:*)

 text \<open>

   # 3: The user inputs a next item somewhere in the \<open>Specification\<close>;

        Since this item requests for a list, \<open>AdditionalValues\<close> is marked "incomplete":

 \<close> 

 ML \<open> (* 3: ISAC suggests a next item within a term list *)

 val ("ok", ([(Tactic.Add_Find "Maximum A", _, _)], _, ptp))

   = Step.specify_do_next ptp;

 \<close>

 Example "Diff_App-No.123a"

   Specification:

     Model:

       Given: \<open>Constants r = 7\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum _\<close> \<open>AdditionalValues [u]\<close>

       Relate: \<open>Extremum _\<close> \<open>SideConditions [__=__, __=__]\<close>

     References:

       Theory_Ref: "__"

   (*\<Odot>*) Problem_Ref: "__/__"

   (*\<Otimes>*) Method_Ref: "__/__"

 (*Solution:*)

 text \<open>

   # 4: The user inputs a next item, and the item \<open>AdditionalValues\<close> is marked "correct":

 \<close> 

 ML \<open> (* # 4: ISAC suggests a next step on request, even a next element within a list *)

 val ("ok", ([(Tactic.Add_Find "AdditionalValues [u]", _, _)], _, ptp))

   = Step.specify_do_next ptp;

 \<close>

 Example "Diff_App-No.123a"

   Specification:

     Model:

       Given: \<open>Constants r = 7\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close>

       Relate: \<open>Extremum _\<close> \<open>SideConditions [__=__, __=__]\<close>

     References:

       Theory_Ref: "__"

   (*\<Odot>*) Problem_Ref: "__/__"

   (*\<Otimes>*) Method_Ref: "__/__"

 (*Solution:*)

 text \<open>

   # 5: Input to \<open>Problem_Ref\<close> is according to the (hidden) formalisation:

 \<close> 

 ML \<open> (* # 5: Input to \<open>Problem_Ref\<close> might change the \<open>Model\<close> *)

 \<close>

 Example "Diff_App-No.123a"

   Specification:

     Model:

       Given: \<open>Constants r = 7\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close>

       Relate: \<open>Extremum _\<close> \<open>SideConditions [__=__, __=__]\<close>

     References:

       Theory_Ref: "__"

   (*\<Odot>*) Problem_Ref: "__/__"

   (*\<Otimes>*) Method_Ref: "__/__"

 (*Solution:*)

 text \<open>

   # 6: Input to \<open>Method_Ref\<close> changes the \<open>Model\<close> to the respective \<open>Method\<close>;

        There is also a feature to change the \<open>Model\<close> according to 

        direct manipulation of \<open>\<Otimes>\<close> and \<open>\<Odot>\<close>.

 \<close> 

 ML \<open> (* # 6: Input to \<open>Method_Ref\<close> changes the \<open>Model\<close> to the respective \<open>Method\<close> *)

 \<close>

 Example "Diff_App-No.123a"

   Specification:

     Model:      (* FIXME: lookup model of method *)

       Given: \<open>Constants r = 7\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close>

       Relate: \<open>Extremum _\<close> \<open>SideConditions [_]\<close>

     References:

       Theory_Ref: "__"

   (*\<Odot>*) Problem_Ref: "univariate_calculus/Optimisation"

   (*\<Otimes>*) Method_Ref: "Optimisation/by_univariate_calculus"

 (*Solution:*)

 text \<open>

   # 7: xxxxx:

 \<close> 

 ML \<open> (* # 7: ISAC suggests a next step on request *)

 \<close>

 text \<open> --- remove this line and make content Isar input---\

 ---------- remove this line and make content Isar input---/

 \<close>

 text \<open>

   # 8: xxxxx:

 \<close> 

 ML \<open> (* # 8: ISAC suggests a next step on request *)

 \<close>

 text \<open> --- remove this line and make content Isar input---\

 ---------- remove this line and make content Isar input---/

 \<close>

 text \<open>

   # 9: xxxxx:

 \<close> 

 ML \<open> (* # 9: ISAC suggests a next step on request *)

 \<close>

 text \<open> --- remove this line and make content Isar input---\

 ---------- remove this line and make content Isar input---/

 \<close>

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end