theory Test_VSCode_Example

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

 (*keywords "Example" :: thy_decl  -- the active definition is in Calculation.thy*)

 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\<close> as test

   --- build Outer_Syntax Example 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\<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> (** 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;

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

 \<close> ML \<open> (*for building code copy here

          calculation.sml --- build Outer_Syntax Example 3 ff*)

 \<close> ML \<open>

 \<close> ML \<open>

 (*/--------------------- the active definition is in Calculation.thy -------------------------\* )

 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

                   CTbasic.EmptyPtree => Preliminary.init_ctree thy example_id

                 | state =>

                   let

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

                       CTbasic.get_obj I state [(*Pos todo*)] |> CTbasic.rep_specify_data

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

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

 (*reminder for Template.show ----------------------------------------------------------------\*)

                     val ((_, _, _), (_, pbl_id as ["univariate_calculus", "Optimisation"], _)) =

                       References.for_eval_model (thy_id, probl_id, meth_id) spec_ref o_ref

                     val {model = model_patt, where_ = where_ctree, where_rls, ...} =

                       Problem.from_store ctxt pbl_id;

 (*/----- ERROR: mk_env not reasonable for "Inc Constants [] [__=__, __=__]"-------------\

   ------------------------------------------------vvvvvvvvvvvvvvvvvvvvv-----------------------* )

                     val (_, env_eval) = Pre_Conds.sep_variants_envs_OLD model_patt probl

                     (*------------------- must be completed first -----------------^^^^^*)

                     val _ =

                       case I_Model.is_complete_OLD ctxt model_patt where_rls where_ctree probl of

                         NONE => writeln "I_Model.is_complete_OLD --> NONE"

                       | SOME variants =>

                         writeln ("I_Model.is_complete_OLD --> SOME " ^ LibraryC.ints2str' variants)

 ( *\----- ERROR: mk_env not reasonable for "Inc Constants [] [__=__, __=__]"-------------/*)

 (*reminder for Template.show ----------------------------------------------------------------/*)

 (*reminder for Pre_Conds.check ---------------------------------------------------------\* )

 val (true, [(true, (Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $

   Free ("r", _), _))]) = Pre_Conds.check ctxt where_rls where_ env_eval;

 ( *reminder for Pre_Conds.check ---------------------------------------------------------/*)

 (**)

                     val ((_, _, _), (_, pbl_id as ["univariate_calculus", "Optimisation"], _)) =

                         References.for_eval_model (thy_id, probl_id, meth_id) spec_ref o_ref

                     val _ = re_eval References.empty References.empty

 (**)

                   in

                     Preliminary.update_state thy

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

                   end

           in set_data state thy end)));

 ( *\--------------------- the active definition is in Calculation.thy -------------------------/*)

 \<close> ML \<open>

 \<close> ML \<open> (*Example 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

 \<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, thus OK.

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

 *)

 (** )Example

 ( **)Example(**) "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>

  (*all empty*)

 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")

   )

 ) CTbasic.EmptyPtree;

 val ptp = (pt, p);

 \<close>

 Example "Diff_App-No.123a" (*all empty step 0*)

   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 *)

 (*/---Step.specify_do_next still works with Ctree, not Ctree-------------------* )

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

   = Step.specify_do_next ptp;

 ( *\---Step.specify_do_next still works with Ctree, not Ctree-------------------*)

 \<close>

 Example "Diff_App-No.123a" (*step 1: <Constants [r = 7]>*)

   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 *)

 (*/---Step.specify_do_next still works with Ctree, not Ctree-------------------* )

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

   = Step.specify_do_next ptp;

 ( *\---Step.specify_do_next still works with Ctree, not Ctree-------------------*)

 \<close>

 Example "Diff_App-No.123a" (*step 2: AdditionalValues [u]*)

   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 *)

 (*/---Step.specify_do_next still works with Ctree, not Ctree-------------------* )

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

   = Step.specify_do_next ptp;

 ( *\---Step.specify_do_next still works with Ctree, not Ctree-------------------*)

 \<close>

 Example "Diff_App-No.123a" (*step 3: A.Values [u, v]*)

   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" (*step 4: (wrong) Problem_Ref input*)

   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: "univariate_calculus/Optimisation" (*"Biegelinien/einfache" not in teststore*)

   (*\<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" (*step 5: Method_Ref updated*)

   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: user inputs value of Method_Ref, which shows the respective Model *)

 \<close>

 subsubsection \<open>Specification with Model for the Method_Ref\<close>

 text \<open>

   Observe the (still outcommented) toggles \<Odot>\<Otimes> changed according to the Reference

 \<close>

 Example "Diff_App-No.123a" (*Specification of the Method_Ref*)

   Specification:

     Model:        

       Given: \<open>Constants [r = 7]\<close> \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close>

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

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

         \<open>FunctionVariable u\<close> \<open>Domain {0 <..< r}\<close> \<open>ErrorBound (\<epsilon> = 0)\<close> 

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

       Find: \<open>Results (A, u, v)\<close>

       Relate:

     References:

       Theory_Ref: "Diff_App"

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

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

 (*Solution:*)

 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