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

     Author:     Walther Neuper, JKU Linz

     (c) due to copyright terms

 Outer syntax for Isabelle/Isac's Calculation.

 *)

 theory Calculation

 imports

   "~~/src/Tools/isac/MathEngine/MathEngine"

 (**)"HOL-SPARK.SPARK" (** ) preliminarily for parsing Example files *)

 (** )"HOL-Word.Word"( ** ) trial on ERROR in definition sdiv below *)

 keywords

     "Example" :: thy_load ("str") (* "spark_vc" :: thy_goal *)

   and "Problem" :: thy_decl (* root-problem + recursively in Solution;

                                "spark_vc" :: thy_goal *)

   and "Specification" "Model" "References" "Solution" (* structure only *)

   and "Given" "Find" "Relate" "Where" (* await input of term *)

   and "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *)

   and "RProblem" "RMethod" (* await input of string list *)

     "Tactic" (* optional for each step 0..end of calculation *)

 begin

 (**)ML_file parseC.sml(**)

 (**)ML_file preliminary.sml(**)

 (**)ML_file "~~/test/Tools/isac/BridgeJEdit/preliminary.sml"(*remove with next step*)

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

 subsection \<open>code for Problem\<close>

 text \<open>

   Again, we copy code from spark_vc into Calculation.thy and

   add functionality for Problem

   such that the code keeps running during adaption from spark_vc to Problem.

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> 

 subsubsection \<open>TODO\<close>

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 subsubsection \<open>TODO\<close>

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 subsubsection \<open>TODO\<close>

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 section \<open>setup command_keyword \<close>

 ML \<open>

 \<close> ML \<open>

 val _ =                                                  

   Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"

     (Resources.provide_parse_files "Example" -- Parse.parname

       >> (Toplevel.theory o (Preliminary.load_formalisation ParseC.formalisation)));

 \<close> ML \<open>

 val _ =

   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>Problem\<close>

     "start a Specification, either from scratch or from preceding 'Example'"

     (ParseC.problem >> Preliminary.prove_vc);

 \<close> ML \<open>

 Preliminary.prove_vc: ParseC.problem -> Proof.context -> Proof.state;

 SPARK_Commands.prove_vc: string -> Proof.context -> Proof.state

 \<close> ML \<open>

 \<close>

 subsection \<open>test runs with Example\<close>

 subsubsection \<open>with new code\<close>

 text \<open>

   Starting the Calculation for the Example requires session Isac with Isac.Biegelinie etc.

   So, do ~~$ ./zcoding-to-test.sh and use Test_Some.thy to evaluate

     Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>

   This now gives no error, but also no <Output>. See child of 3ea616c84845.

 \<close>

 subsubsection \<open>with original SPARK code\<close>

 text \<open>

   The sequence of code below is copied from SPARK/Examples/Gcd/Greatest_Common_Divisor.thy.

   But here the code works only partially (see ERROR at end).

   Thus it is advisable to run tests in Test_Some.thy, where "Example" has "Biegelinie".

   spark_proof_functions is required for proof below..

 \<close>

 (*//------------------- outcomment before creating session Isac ----------------------------\\* )

 (**)

   spark_proof_functions gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"

 (**)

 spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>

 (*Output..* )

 The following verification conditions remain to be proved:

   procedure_g_c_d_4

   procedure_g_c_d_11

 ( **)

 spark_vc procedure_g_c_d_4

 proof -

   from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)

   with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1

     by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])

 (** )

 proof -

   from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)

   with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1

     by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])

 next

   from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2

     by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)

 qed

 ( **)oops(**)

 (** )sorry( **)

 spark_vc procedure_g_c_d_11

   sorry

 (** )

 spark_end

 ( *Bad path binding: "$ISABELLE_HOME/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv"*)

 ( *\\------------------- outcomment before creating session Isac ----------------------------//*)

 section \<open>Notes: adapt spark_vc to Problem using Naproche as model\<close>

 subsection \<open>survey on steps of investigation\<close>

 text \<open>

   We stopped step 3.4 going down from Outer_Syntax.local_theory_to_proof into proof.

   Now we go the other way: Naproche checks the input via the Isabelle/server

   and outputs highlighting, semantic annotations and errors via PIDE ---

   and we investigate the output.

   Investigation of Naproche showed, that annotations are ONLY sent bY

   Output.report: string list -> unit, where string holds markup.

   For Output.report @ {print} is NOT available, so we trace all respective CALLS.

   However, NO @ {print} available in src/Pure is reached by "spark_vc procedure_g_c_d_4",

   so tracing is done by writeln (which breaks build between Main and Complex_Main

   by writing longer strings, see Pure/General/output.ML).

   Tracing is implemented in (1) Isabelle_Naproche and in (2) isabisac in parallel;

   (1) requires only Pure, thus is built quicker, but does NOT handle proofs within ML

   (2) requires HOL.SPARK, there is full proof handling, but this is complex.

   Tracing the calls of Output.report shows some properties of handling proofs,

   see text in SPARK/Examples/Gcd/Greatest_Common_Divisor.thy.

 \<close>

 end(* SEE "outcomment before creating session Isac" ABOVE !!! OTHERWISE YOU HAVE..

   ERROR: Found the end of the theory, but the last SPARK environment is still open.

   ..is acceptable for testing spark_vc .. proof - ...

 *)