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