(*  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/Knowledge/Build_Thydata"   (*remove after devel.of BridgeJEdit*)

(** )"~~/src/Tools/isac/MathEngine/MathEngine"  ( *activate after devel.of BridgeJEdit*)

(**) "HOL-SPARK.SPARK"                             (*remove after devel.of BridgeJEdit*)

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

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           (*vvvvvvvvvvvvvvvvvvvv--- HACK: test independent from session Isac*)

        (Preliminary.load_formalisation @{theory Biegelinie} 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>

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

(*vvvvvvvv--- makes Outer_Syntax..Problem run; Isac code is just added*)

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

(*..Problem adds to SPARK..*)

Problem (*procedure_g_c_d_4*)("Biegelinie", ["Biegelinien"])

  Specification:

(*1*)

    Model:

      Given: "Traegerlaenge ", "Streckenlast "

      Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"

      Find: "Biegelinie "

      Relate: "Randbedingungen "

    References:

  (*2*)

      RTheory: ""

      RProblem: ["", ""]

      RMethod: ["", ""]

  (*2*)

(*1*)

  Solution:

(*

  compare click on above Given: "Traegerlaenge ", "Streckenlast " 

  with click on from \<open>0 < d\<close> in SPARK/../Greatest_Common_Divisorthy

*)

subsection \<open><Output> BY CLICK ON Problem..Solution\<close>

text \<open>

  Comparison of the two subsections below:

(1) <Output> AFTER session Isac (after ./zcoding-to-test.sh) WITH click on Problem..Specification:

  ((WHILE click ON Example SHOWS NO ERROR))

# headline =  ..(1) == (2)                                                     ..PARSED + Specification

# i_model = Inc  ..IN 4 ELEMENTS, (1) == (2)                                   ..?!? FROM PARSED ?!?

# o_model = COMPLETE WITH 7 ELEMENTS                                           ..FROM Example

# refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])..FROM References

(2) <Output> WITHOUT session Isac (after ./ztest-to-coding.sh) WITH click on Problem..Specification:

  ((WHILE click ON Example SHOWS !!! ERROR))

# headline =  ..(1) == (2)                                                     ..PARSED + Specification

# i_model = Inc  ..IN 4 ELEMENTS, (1) == (2)                                   ..?!? FROM PARSED ?!?

# o_model = []                                                                 ..NO Example

# refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"])                    ..FROM headline ONLY

\<close>

subsubsection \<open>(1) WITH session Isac (AFTER ./zcoding-to-test.sh)\<close>

text \<open>

{a = "//--- Spark_Commands.prove_vc", headline =

 (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),

   ((((("Specification", ":"),

       ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),

                 "Where"),

                ":"),

               ["<markup>", "<markup>"]),

              "Find"),

             ":"),

            "<markup>"),

           "Relate"),

          ":"),

         ["<markup>"]),

        (("References", ":"),

         (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),

      "Solution"),

     ":"),

    [])),

  "")} (line 677 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy") 

{a = "prove_vc", i_model =

 [(0, [], false, "#Given",

   Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),

  (0, [], false, "#Given",

   Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),

  (0, [], false, "#Find",

   Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),

        (Const ("empty", "??.'a"), []))),

  (0, [], false, "#Relate",

   Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),

        (Const ("empty", "??.'a"), [])))],

 o_model =

 [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]),

  (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),

  (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),

   [Free ("y", "real \<Rightarrow> real")]),

  (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),

   [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $

      (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $

        Free ("0", "real")) $

      Const ("List.list.Nil", "bool list"),

    Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $

      (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $

        Free ("0", "real")) $

      Const ("List.list.Nil", "bool list"),

    Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $

      (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $

        (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $

      Const ("List.list.Nil", "bool list"),

    Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $

      (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $

        (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $

      Const ("List.list.Nil", "bool list")]),

  (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),

  (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),

   [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $

      Const ("List.list.Nil", "real list"),

    Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $

      Const ("List.list.Nil", "real list"),

    Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $

      Const ("List.list.Nil", "real list"),

    Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $

      Const ("List.list.Nil", "real list")]),

  (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),

   [Free ("dy", "real \<Rightarrow> real")])],

 refs =

 ("Biegelinie", ["Biegelinien"],

  ["IntegrierenUndKonstanteBestimmen2"])} (line 690 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy") 

### Proof_Context.gen_fixes 

### Proof_Context.gen_fixes 

### Proof_Context.gen_fixes 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Proof_Context.gen_fixes 

### Proof_Context.gen_fixes

\<close>

subsubsection \<open>(2) WITHOUT session Isac (AFTER ./ztest-to-coding.sh)\<close>

text \<open>

{a = "//--- Spark_Commands.prove_vc", headline =

 (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),

   ((((("Specification", ":"),

       ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),

                 "Where"),

                ":"),

               ["<markup>", "<markup>"]),

              "Find"),

             ":"),

            "<markup>"),

           "Relate"),

          ":"),

         ["<markup>"]),

        (("References", ":"),

         (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),

      "Solution"),

     ":"),

    [])),

  "")}

{a = "prove_vc", i_model =

 [(0, [], false, "#Given",

   Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),

  (0, [], false, "#Given",

   Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),

  (0, [], false, "#Find",

   Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),

        (Const ("empty", "??.'a"), []))),

  (0, [], false, "#Relate",

   Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),

        (Const ("empty", "??.'a"), [])))],

 o_model = [], refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"])}

### Proof_Context.gen_fixes 

### Proof_Context.gen_fixes 

### Proof_Context.gen_fixes 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Proof_Context.gen_fixes 

### Proof_Context.gen_fixes

\<close>

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 - ...

*)