(*  Title:      src/Tools/isac/BridgeJEdit/Calculation.thy

     Author:     Walther Neuper, JKU Linz

 Outer syntax for Isabelle/Isac's Calculation interactive via Isabelle/PIDE.

 Second trial following Makarius' definition of "problem" already existing in this repository.

 *)

 theory Calculation

   imports

   (**)"$ISABELLE_ISAC/Knowledge/Build_Thydata"   (*remove after devel.of BridgeJEdit*)

   (**)"$ISABELLE_ISAC/MathEngine/MathEngine"

   (** )"SPARK_FDL"                             ( * remove after devel.of BridgeJEdit*)

 keywords "Example" :: thy_decl

 and "Problem" "Specification" "Model" "References" "Solution" 

 begin

 ML_file "parseC.sml"

 ML_file "preliminary.sml"

 section \<open>new code for Outer_Syntax Example  ...\<close>

 text \<open> 

   stepwise development starts at changeset

   https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080

   and can be inspected following the subsequent changesets..

 \<close>

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 structure Data = Theory_Data

 (

   type T = Ctree.ctree option;

   val empty = NONE;

   val extend = I;

   fun merge _ = NONE;

 );

 val set_data = Data.put o SOME;

 fun the_data thy = 

   case Data.get thy of NONE => Ctree.EmptyPtree

   | SOME ctree => ctree;

 \<close> ML \<open>

 \<close> text \<open>

 A provisional Example collection.

 For notes from ISAC's discontinued Java front-end see

 https://isac.miraheze.org/wiki/Extend_ISAC_Knowledge#Add_an_example_in_XML_format

 \<close> ML \<open>

 type description = string

 type example = (description * Formalise.T)

 val example_store = []: (string * example) list

 \<close> ML \<open>

 val example_store = AList.update op= ("Diff_App/No.123 a", 

  ("The efficiency of an electrical coil depends on the mass of the kernel." ^

   "Given is a kernel with cross-sectional area determined by two rectangles" ^

   "of same shape as shown in the figure." ^

   "Given a radius r = 7, determine the length u and width v of the rectangles" ^

   "such that the cross-sectional area A (and thus the mass of the kernel) is a" ^

   "maximum. + Figure", 

    (["[r = 7]", "[A, [u, v]]", "[A = 2 \<sqdot> u \<sqdot> v - u 2 , ( 2 u ) 2 + ( 2 v ) 2 = r 2 ]", 

       "{0 < .. < r}"]: TermC.as_string list,

       (*TODO: compare paper + test/../Diff_App: more than one list of Model_Def.form_model? *)

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

       ["Optimisation", "by_univariate_calculus"]): References.T)): example) example_store

 \<close> ML \<open>

 case AList.lookup op= example_store "Diff_App/No.123 a" of

   SOME (_, (["[r = 7]", "[A, [u, v]]", "[A = 2 \<sqdot> u \<sqdot> v - u 2 , ( 2 u ) 2 + ( 2 v ) 2 = r 2 ]", "{0 < .. < r}"], 

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

     => ()

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

 \<close> ML \<open>

 \<close> ML \<open>

 (*? I_Model.* or Problem.* ?*)

 fun check_input (*ctxt o-model ??*) (_: Problem.model_input) = []: I_Model.T

 \<close> ML \<open>

 fun update_state (model, (thy_id, probl_id, meth_id)) (*at the first encounter of an Example*)

     Ctree.EmptyPtree =

     Ctree.Nd (Ctree.PblObj {

       fmz = Formalise.empty, origin = (O_Model.empty, References.empty, TermC.empty),

       spec = (thy_id, probl_id, meth_id), probl = check_input model, meth = []: Model_Def.i_model,

       ctxt = ContextC.empty, loc = (NONE, NONE), 

       branch = Ctree.NoBranch, ostate = Ctree.Incomplete, result = (TermC.empty, [])}, [])

   | update_state (model, (thy_id, probl_id, meth_id)) (*TODO +switch RProblem | RMethod*)

     (Ctree.Nd (Ctree.PblObj {fmz, origin, spec = _, probl = _, meth, ctxt, loc, branch, ostate, result}, 

       children)) =

     Ctree.Nd (Ctree.PblObj {

       fmz = fmz, origin = origin,

       spec = (thy_id, probl_id, meth_id), probl = check_input model, meth = meth,

       ctxt = ctxt, loc = loc, 

       branch = branch, ostate = ostate, result = result}, children)

   | update_state _ _ = raise ERROR "update_state: uncovered case in fun.def."

 \<close> ML \<open>

 update_state: Problem.model_input * (ThyC.id * Problem.id * MethodC.id) 

   -> Ctree.ctree -> Ctree.ctree

 \<close> ML \<open>

 type references_input = (string * (string * string))

 \<close> ML \<open>

 val parse_references_input =

   Parse.!!! ( \<^keyword>\<open>Theory_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name --

   Parse.!!! ( \<^keyword>\<open>Problem_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name --

   Parse.!!! ( \<^keyword>\<open>Method_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name)))

 \<close> ML \<open>

 parse_references_input: references_input parser (*TODO: dpes not yet work,

   thus in Outer_Syntax.command \<^command_keyword>\<open>Example\<close> replacced by Problem.parse_cas*)

 \<close> ML \<open>

 op --  : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e;

 op |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 val _ =

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

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

     (Parse.name -- Parse.!!! (  \<^keyword>\<open>Problem\<close> |-- Parse.name -- 

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

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

          Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- (*parse_references_input*)Problem.parse_cas))) >>

       (fn (_(*exp_id*), (_(*probl_id'*), (model_input, _(*references_input*)))) =>

         Toplevel.theory (fn thy =>

           let

             val (thy_id, (probl_id, meth_id)) = (*references_input*)("Diff_App", ("univariate_calculus/Optimisation", "Optimisation/by_univariate_calculus"))

             val input = update_state (model_input, 

               (thy_id, References_Def.explode_id probl_id, References_Def.explode_id meth_id)) 

                 Ctree.EmptyPtree;

           in set_data input thy end)));

 \<close> ML \<open>

 \<close> ML \<open>

 (*/----------------------------------------------------------------------------\*)

      Parse.name -- Parse.!!! (  \<^keyword>\<open>Problem\<close> |-- Parse.name -- 

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

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

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

 : (string * (string * (Problem.model_input * references_input))) parser

 (*\----------------------------------------------------------------------------/*) 

 : Token.T list ->

 (*/----------------------------------------------------------------------------\*)

     (string * (string * (Problem.model_input * references_input)))

 (*\----------------------------------------------------------------------------/*)

 * Token.T list

 (*/----------------------------------------------------------------------------\* )

    the type above is the type of the argument of \<open>(fn (_(*name*),..\<close> 

 ( *\----------------------------------------------------------------------------/*)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> 

 end