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

\<close> ML \<open>

val demo_example = ("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", 

   ([

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

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

      ["Optimisation", "by_univariate_calculus"]): References.T)): Example.T

\<close> 

setup \<open>KEStore_Elems.add_expls [(demo_example, ["Diff_App-No.123a"])]\<close>

ML \<open>

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

\<close> ML \<open>

\<close> ML \<open>

(*

  Implementation reasonable, as soo as

 * clarified, how "empty" items in Model are represented

 * parse_references_input works

 * switching \<Odot>\<Otimes> i_model for probl and meth works.

*)

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

\<close> ML \<open>

\<close> ML \<open>

(* at the first encounter of an Example create the following data and transfer them to ctree:

    origin: eventually used by sub-problems, too

    O_Model: for check of missing items

    I_Model: for efficient check of user input

*)

\<close> ML \<open>

fun init_ctree example_id =

    let

      (* TODO     vvvvvvvvvvvvvvv works only within Isac_Test_Base *)

      val thy = (*ThyC.get_theory thy_id*)@{theory Diff_App}

      val example_id' = References_Def.explode_id example_id

      val (_, (fmz as (model, refs as (_(*thy_id*), probl_id, _)))) =

        Store.get (KEStore_Elems.get_expls @{theory}) example_id' example_id' 

      val ctxt = ContextC.initialise' thy model;

      val o_model = Problem.from_store probl_id |> #ppc |> O_Model.init thy model

    in

      Ctree.Nd (Ctree.PblObj {

        fmz = fmz, origin = (o_model, refs, TermC.empty (*TODO handle CAS_Cmd*)),

        spec = References.empty, probl = I_Model.empty, meth = I_Model.empty,

        ctxt = ctxt, loc = (NONE, NONE), 

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

    end

\<close> ML \<open>

(* 

At the first call 

* initialise ctree with origin from example_id

* add items already input ..TODO..TODO..TODO..TODO..TODO..TODO..TODO..TODO..TODO

*)

\<close> ML \<open>

fun update_state (example_id, (model, refs)) Ctree.EmptyPtree = 

    init_ctree example_id |>  update_state (example_id, (model, refs))

  | update_state (_, (model, (thy_id, probl_id, meth_id)))

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

      children)) =

      let 

        val _ = if thy_id <> othy then "re-parse all i_model" else "do nothing"

        val _ = if probl_id <> opbl then "switch from meth? check_input of probl" else "do nothing"

        val _ = if meth_id <> omet then "switch from probl check_input of meth" else "do nothing"

      in

        Ctree.Nd (Ctree.PblObj {

          fmz = fmz, origin = origin, spec = References.select_input spec (thy_id, probl_id, meth_id), 

          probl = check_input model, meth = meth, (*TODO +switch Problem_Ref | Method_Ref*)

          ctxt = ctxt, loc = loc, 

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

      end

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

\<close> ML \<open>

\<close> ML \<open>

update_state: string * (Problem.model_input * References.T) -> 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>

fun is_empty str = 

  let

    val strl = Symbol.explode str |> rev

  in

    take (2, strl) = ["_", " "] orelse take (3, strl) = ["]", "_", "["]

  end

\<close> ML \<open>

val m2 = "0 < r";                val m2' = Symbol.explode m2 |> rev;

val m3 = "Maximum _";            val m3' = Symbol.explode m3 |> rev;

val m4 = "AdditionalValues [_]"; val m4' = Symbol.explode m4 |> rev;

\<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>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 (example_id, (model_input, _(*references_input*))) =>

        Toplevel.theory (fn thy =>

          let

(** )

val _ = writeln ("#Example model_input: " ^ @{make_string} model_input)

(*                #Example model_input:

    [("#Given", ["<markup>"]), ("#Where", ["<markup>"]), ("#Find", ["<markup>", "<markup>"]), ("#Relate", ["<markup>", "<markup>"])]*)

val [("#Given", [m1]), ("#Where", [m2]), ("#Find", [m3, m4]), ("#Relate", [m5, m6])] = 

  model_input : Problem.model_input

val _ = writeln ("#Example m.: " ^ m1 ^ " " ^ m2 ^ " " ^ m3 ^ " " ^ m4 ^ " " ^ m4 ^ " " ^ m5 ^ " " ^ m6)

val m2' = Symbol.explode m2;

val _ = writeln ("#Example Symbol.explode m2: " ^ @{make_string} m2')

val _ = if (is_empty m2) then writeln "true" else writeln "false";

val _ = if (is_empty m3) then writeln "true" else writeln "false";

val _ = if (is_empty m4) then writeln "true" else writeln "false";

(*                #Example m.: Constants [r = 7] 0 < r Maximum _ AdditionalValues [_] AdditionalValues [_] Extremum _ SideCondition [_]*)

( **)

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

            val input = update_state (example_id, (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>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 * (Problem.model_input * references_input)) parser*)

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

: Token.T list ->

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

    (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> text \<open>

  INVESTIGATE Problem.Outer_Syntax.command \ <^command_keyword>\<open>problem\<close>

  on Biegelinie.problem pbl_bieg : "Biegelinien"

  ML-source shows error-positions already perfectly: what types are involved?..

\<close> ML \<open>

Rule_Set.append_rules "empty" Rule_Set.empty [] (* ORIGINAL source = ARGUMENT IN fn *)

(* (1a)

  Ouptut from Biegelinie.problem pbl_bieg : "Biegelinien":

  #problem source: Source {delimited = true, range = ({offset=38, end_offset=87, id=-1652}, {offset=87, id=-1652}), 

    text = "\127Rule_Set.append_rules \"empty\" Rule_Set.empty []\127"}

*)

\<close> ML \<open>

val source = Input.empty;

val ml = ML_Lex.read;

\<close> ML \<open>

  (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")

(*= 

   [Text (Token (({}, {}), (Long_Ident, "Theory.setup"))), Text (Token (({}, {}), (Space, " "))), Text (Token (({}, {}), (Keyword, "("))), Text (Token (({}, {}), (Long_Ident, "Problem.set_data"))),

    Text (Token (({}, {}), (Space, " "))), Text (Token (({}, {}), (Keyword, "("))), Text (Token (({}, {}), (Space, " "))), Text (Token (({}, {}), (Keyword, ")"))), Text (Token (({}, {}), (Keyword, ")"))),

    Text (Token (({}, {}), (Space, " ")))]

   : ML_Lex.token Antiquote.antiquote list

   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ type of (1a)

*)

\<close> ML \<open>

ML_Context.expression (Input.pos_of source)

  (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")

  : Context.generic -> Context.generic

\<close> ML \<open>

ML_Context.expression (Input.pos_of source)

  (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")

  |> Context.theory_map

  : theory -> theory

\<close> ML \<open>

Outer_Syntax.command: Outer_Syntax.command_keyword -> string -> 

  (Toplevel.transition -> Toplevel.transition) parser -> unit

\<close> ML \<open>

\<close> text \<open>

  ML-source shows error-positions already perfectly: types involved are above.

  Input at Given does NOT show error-position, 

    but ISAC msg \<open>ME_Isa: thy "Isac_Knowledge" not in system\<close>

  Thus compare ML-source/input with model_input ...

\<close> ML \<open>

Problem.parse_model_input:                 Problem.model_input parser;

Problem.parse_model_input: Token.src ->    Problem.model_input * Token.src;

Problem.parse_model_input: Token.T list -> Problem.model_input * (Token.T list)

\<close> ML \<open>

[]: Position.range list;

[]: Position.T list;

\<close> ML \<open>

\<close> ML \<open>

(* Given: "Traegerlaenge l_l" "Streckenlast q_q" *)

(* (1b)

  Ouptut from Biegelinie.problem pbl_bieg : "Biegelinien":

  #problem model_input: [("#Given", ["<markup>", "<markup>"]), ("#Find", ["<markup>"]), ("#Relate", ["<markup>"])] 

                        : Problem.model_input

  type of  (1b) --------^^^^^^^^^^^^^^^^^^^^^^> contains ? Markup.T ?..

  #problem m1: Traegerlaenge l_l

  #problem m2: Streckenlast q_q 

  I this -----^^^______________^^^ Markup.T ?

*)

\<close> ML \<open> (** investigate parse_model_input **)

\<close> ML \<open> (* how get a Token.T list without Outer_Syntax.command ? *)

\<close> ML \<open>

Parse.term:                 string parser;

Parse.term: Token.T list -> string * Token.T list;

\<close> ML \<open>

\<close> ML \<open> (* relation Token.T -- Markup.T ??? *)

\<close> ML \<open>

val ctxt = Proof_Context.init_global @{theory};

val given_1 = Syntax.read_term ctxt "Traegerlaenge l_l" (* as in parse_tagged_terms *)

(*  ^^^^^^^ : term  -- why then evaluates parse_model_input to markup ? *)

\<close> ML \<open>

\<close> ML \<open>

Markup.literal_fact "Traegerlaenge l_l" = ("literal_fact", [("name", "Traegerlaenge l_l")])

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

end