(* Title:  "BridgeJEdit/vscode-example.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- VSCode example with Step.specify_do_next ------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

(**** VSCode example with Step.specify_do_next ########################################### ****)

"----------- VSCode example with Step.specify_do_next ------------------------------------------";

"----------- VSCode example with Step.specify_do_next ------------------------------------------";

val c = []:cid;

val fmz = [

(*Problem model:*)

  "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",

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

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

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

  "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]",

(*MethodC model:*)

  "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>",

  "Domain {0 <..< r}",

  "Domain {0 <..< r}",

  "Domain {0 <..< \<pi> / 2}",

  "ErrorBound (\<epsilon> = (0::real))"

]: TermC.as_string list;

if (fmz |> map (TermC.parseNEW @{context}) |> filter is_some |> length) = 14

then () else error "Formalise.model not parsed completely";

val refs =

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

(*/------- start example as usual in tests ---------------------------------------------------* )

val (p,_,f, nxt,_,pt) = CalcTreeTEST [(fmz, refs)];

val ptp = (pt, p);

( *-------- outcomment EITHER above OR below --------------------------------------------------*)

case Store.get (KEStore_Elems.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"] of

  (_, ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: _, 

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

    => ()

| _ => error "intermed. example_store CHANGED";

val p = ([], Pbl);

val pt = update_state (*here we have Ctree.EmptyPtree and thus call init_ctree*)

("Diff_App-No.123a", 

    (* Problem.parse_model_input results in markup, which is accepted by \<open>fun update_state\<close>, too:

                 Constants [r = 7] *)

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

     ("#Where", ["0 < r"]), 

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

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

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

    ],

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

    (*References_Def.explode_id ^^^^^^^^^^^^^^^^^^^^^^, ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

  )

) Ctree.EmptyPtree;

val ptp = (pt, p);

(*\------- start example as required in VSCode_Example.thy -----------------------------------*)

(*** stepwise Specification: Problem model================================================= ***)

(** ) we drop this step, because the user shall be presented a (empty) Model ... ( ** )

val ("ok", ([(Model_Problem, Model_Problem' (["univariate_calculus", "Optimisation"], _, _), _)], _, ptp))

  = Step.specify_do_next ptp;

( **)

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

  = Step.specify_do_next ptp;

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

  = Step.specify_do_next ptp;

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

  = Step.specify_do_next ptp;

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

  = Step.specify_do_next ptp;

val ("ok", ([(Tactic.Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)", _, _)], _, ptp))

  = Step.specify_do_next ptp;

val ("ok", ([(Tactic.Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", _, _)], _, ptp))

  = Step.specify_do_next ptp;

(*** Problem model is complete ============================================================ ***)

val PblObj {probl, ...} = get_obj I (fst ptp) [];

if I_Model.to_string @{context} probl = "[\n" ^

  "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n" ^

  "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n" ^

  "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n" ^

  "(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n" ^

  "(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]]))]"

then () else error "I_Model.to_string probl CHANGED";

(*//---------------- adhoc inserted ------------------------------------------------\\*)

(*with update_state*)

(* already been input -------vvvvvvvvvvvvvvvvvvv: code in check_input is missing*)

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

  = (**) Step.specify_do_next ptp;

(*with update_state*)

(*+*)val ("ERROR I_Model.check_single: \"Maximum A\"\" not for field \"#Find\"", ([], [], ptp))

  = (**) Step.specify_do_next ptp;

(*\\---------------- adhoc inserted ------------------------------------------------//*)

(*** Specification of References ========================================================== *** )

val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp))

  = Step.specify_do_next ptp;

val ("ok", ([(Specify_Problem ["univariate_calculus", "Optimisation"], _, _)], _, ptp))

  = Step.specify_do_next ptp;

val ("ok", ([(Specify_Method ["Optimisation", "by_univariate_calculus"], _, _)], _, ptp))

  = Step.specify_do_next ptp;

---------------------------------------------------------------------- trace from CalcTreeTEST*)

(*** stepwise Specification: MethodC model ================================================ ***

)

val ("ok", ([(Add_Given "FunctionVariable a", _, _)], _, ptp))

  = Step.specify_do_next ptp;

val ("ok", ([(Add_Given "Input_Descript.Domain {0<..<r}", _, _)], _, ptp))

  = Step.specify_do_next ptp;

val ("ok", ([(Add_Given "ErrorBound (\<epsilon> = 0)", _, _)], _, ptp))

  = Step.specify_do_next ptp;

---------------------------------------------------------------------- trace from CalcTreeTEST*)

(*** Specification of Problem and MethodC model is complete =============================== ***)

val PblObj {meth, ...} = get_obj I (fst ptp) [];

(*with update_state*)

if I_Model.to_string @{context} meth = ("[\n" ^

  "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]]))]"

) then () else error "ERROR output CHANGED";

(*with CalcTreeTEST* )

if I_Model.to_string @ {context} meth = "[\n" ^

  "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n" ^

  "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n" ^

  "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n" ^

  "(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n" ^

  "(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]])), \n" ^

  "(7 ,[1] ,true ,#Given ,Cor FunctionVariable a ,(funvar, [a])), \n" ^

  "(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} ,(doma, [{0<..<r}])), \n" ^

  "(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) ,(err, [\<epsilon> = 0]))]"

then () else error "I_Model.to_string meth CHANGED";

---------------------------------------------------------------------- trace from CalcTreeTEST*)

(*** Solution starts ====================================================================== ***)

(*---

Step.specify_do_next ptp;

(*ERinROR in creating the environment from formal args. of partial_function "Diff_App.univar_optimisation"

and the actual args., ie. items of the guard of "["Optimisation", "by_univariate_calculus"]" by "assoc_by_type":

formal arg "err" of type "bool" doesn't mach an actual arg.

with:

7 formal args: ["fixes", "maxx", "extr", "sideconds", "funvar", "doma", "err"]

7 actual args: ["[r = 7]", "A", "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", "a", "{0<..<r}", "\<epsilon> = 0", "[u, v]"]

   with types: ["bool list", "real", "bool list", "real", "real set", "bool", "real list"]*)

---*)