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> (** 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_TEST 3 ff*)

\<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

                  CTbasic_TEST.EmptyPtree => Preliminary.init_ctree thy example_id

                | state =>

                  let

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

                      CTbasic_TEST.get_obj I state [(*Pos todo*)] |> CTbasic_TEST.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 (_, env_eval) = Pre_Conds.sep_variants_envs_OLD model_patt probl

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

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

                      Problem.from_store ctxt pbl_id;

                    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)

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

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

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

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

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

(**)

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

\<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_TEST "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_TEST: proper syntax check of terms with Model_Pattern.parse_pos,

*)

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

 (*all empty*)

Example_TEST "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_TEST.EmptyPtree;

val ptp = (pt, p);

\<close>

Example_TEST "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_TEST-------------------* )

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

  = Step.specify_do_next ptp;

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

\<close>

Example_TEST "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_TEST-------------------* )

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

  = Step.specify_do_next ptp;

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

\<close>

Example_TEST "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_TEST-------------------* )

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

  = Step.specify_do_next ptp;

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

\<close>

Example_TEST "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_TEST "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_TEST "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_TEST "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