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

     Author:     Walther Neuper, JKU Linz

     (c) due to copyright terms

 Outer syntax for Isabelle/Isac. Compare src/Pure/Pure.thy

 *)

 theory Calculation

   imports "~~/src/Tools/isac/MathEngine/MathEngine" (** )"HOL-SPARK.SPARK"( **HIDE for Test_Isac*)

 keywords

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

   "Problem" and (* root-problem + recursively in Solution *)

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

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

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

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

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

 begin

 ML_file parseC.sml

 section \<open>derive Outer_Syntax.command..Example from ..spark_open\<close>

 subsection \<open>trials 1\<close>

 ML \<open>

 val form_single_str = (

   "(                                                                             " ^

   "  [\"Traegerlaenge L\", \"Streckenlast q_0\", \"Biegelinie y\",               " ^

 	"    \"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]\",     " ^

 	"    \"FunktionsVariable x\", \"GleichungsVariablen [c, c_2, c_3, c_4]\",      " ^

   "    \"AbleitungBiegelinie dy\"],                                              " ^

   "  (\"Biegelinie\", [\"Biegelinien\"], [\"IntegrierenUndKonstanteBestimmen2\"])" ^

   ")")

 \<close> ML \<open>

 \<close> text \<open> (*/------------------------ def. Fdl_Lexer.$$$ ----------------------------------\*)

 val form_single =

   Fdl_Lexer.$$$ "(" --

     Fdl_Lexer.$$$ "[" (* |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Formalise.model *) --*)

 \<close> text \<open>

 form_single: (string * Position.T) list ->

   ((string * Position.T) list * (string * Position.T) list) * (string * Position.T) list

 \<close> text \<open> (*\------------------------ def. Fdl_Lexer.$$$ ----------------------------------*)

 \<close> text \<open>

 form_single [("(", Position.none), ("[", Position.none)](* = (([("(", {})], [("[", {})]), [])*)

 (*          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^   ...........................OK: ^^ *)

 \<close> text \<open>

                       (* |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Formalise.model *) --*)

   ..would need to understand Fdl_Lexer + Fdl_Parser ?!?

 \<close> ML \<open>

 \<close> ML \<open> (*/------------------------ Resources.parse_files -------------------------------\*)

 Resources.provide_parse_files "spark_open"

 \<close> ML \<open>

 Resources.parse_files "spark_open":                 (theory -> Token.file list) parser;

 Resources.parse_files "spark_open": Token.T list -> (theory -> Token.file list) * Token.T list;

 \<close> ML \<open>

 val toks = ParseC.tokenize form_single_str;

 \<close> text \<open>

              (Resources.parse_files "Example") toks;

 ParseC.parse (Resources.parse_files "Example") toks;

 (*exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")*)

 \<close> ML \<open> (*\------------------------ Resources.parse_files -------------------------------/*)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (*/------------------------ Parse.path ------------------------------------------\*)

 Parse.path: string parser;

 \<close> ML \<open>

 val toks = ParseC.tokenize

   "/usr/local/isabisac/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv"

 \<close> text \<open>

 (Scan.ahead Parse.not_eof -- Parse.path) toks

 (*exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")*)

 \<close> ML \<open> (*\------------------------ Parse.path ------------------------------------------/*)

 \<close> ML \<open>

 \<close> 

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

 text \<open>

   We minimally change code for Example, until all works.

   The code is separated from Calculation.thy into files cp_spark_vcs.ML and cp_spark_commands.ML, 

   because text\<open>...\<close> and (*...*) for const_name>\<open>...\<close> etc and @ {thms ...} causes errors.

   Thus for Test_Isac (**)ML_file "cp_spark_vcs.ML", ""(*cp_spark_commands.ML*) must be outcommented.

 \<close>

 (*HIDE for Test_Isac** )

 ML_file "cp_spark_vcs.ML"

 ML_file "cp_spark_commands.ML"

 ( **HIDE for Test_Isac*)

 subsubsection \<open>cp. HOL/SPARK/Tools/spark_vcs.ML\<close>

  ML \<open>

 \<close> ML \<open>

 (*/--------------------------------- cp_spark_vcs.ML -----------------------------------------\*)

 (*\--------------------------------- cp_spark_vcs.ML -----------------------------------------/*)

 \<close> ML \<open>

 \<close>

 subsubsection \<open>cp. HOL/SPARK/Tools/spark_commands.ML\<close>

 ML \<open>

 \<close> ML \<open>

 (*/--------------------------------- cp_spark_commands.ML ------------------------------------\*)

 (*\--------------------------------- cp_spark_commands.ML ------------------------------------/*)

 \<close> ML \<open>

 \<close>

 section \<open>setup command_keyword \<close>

 subsection \<open>hide for development, use for Test_Isac\<close>

 ML \<open>

 type chars = (string * Position.T) list;

 val e_chars = []: (string * Position.T) list;

 fun spark_open (_: ((*Fdl_Lexer.*)chars -> 'a * (*Fdl_Lexer.*)chars)) 

     (_: ('b -> Token.file list * theory) * string) (_: 'b) = @{theory}

 type banner = string * string * string;               val e_banner = ("b1", "b2", "b3")

 type date = string * string * string;                 val e_date = ("d1", "d2", "d3")

 type time = string * string * string * string option; val e_time = ("t1", "t2", "t3", SOME "t4")

 fun siv_header (_: chars) = 

   ((e_banner, (e_date, e_time), (e_date, e_time), ("", "")), e_chars);

 \<close> ML \<open>

 \<close> 

 subsection \<open>def.for Build_Isac; for Test_Isac outcomment SPARK_Commands, Fdl_Lexer below\<close>

 ML \<open>

 \<close> ML \<open>

 val _ =                                                  

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

     (*preliminary from spark_open*)

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

 (** )  >> (Toplevel.theory o ((*SPARK_Commands.*)spark_open Fdl_Lexer.siv_header)));( **)

 (**)  >> (Toplevel.theory o ((*SPARK_Commands.*)spark_open (*Fdl_Lexer.*)siv_header)));(**)

 \<close> ML \<open>

 \<close>

 section \<open>Test: compare Example .. spark_open\<close>

 (** )

 Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close> ( *.str*)

 (*Output + ERROR:

 {a = "//--- ##1# spark_open", files = fn, header = fn, prfx = ""} (line 14 of "/usr/local/isabisac/src/HOL/SPARK/Tools/spark_commands.ML") 

 {a = "##1# spark_open: before call <files thy>, files = siv_header !"} (line 18 of "/usr/local/isabisac/src/HOL/SPARK/Tools/spark_commands.ML") 

 {a = "### provide_parse_files", fs =

  [{digest = "b34ac56c90f483e9cdd0f14dc45d5f703e40aa26", lines =

    ["[", "  (", "    [\"Traegerlaenge L\", \"Streckenlast q_0\", \"Biegelinie y\",", "\t    \"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]\",",

     "\t    \"FunktionsVariable x\", \"GleichungsVariablen [c, c_2, c_3, c_4]\",", "      \"AbleitungBiegelinie dy\"],", "    (\"Biegelinie\", [\"Biegelinien\"], [\"IntegrierenUndKonstanteBestimmen2\"])", "  )",

     "]"],

    pos = {line=1, offset=1, file=~~/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70.str, id=-1818}, src_path =

    "/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70.str"}]} (line 241 of "PIDE/resources.ML") 

 exception Bind raised (line 15 of "/usr/local/isabisac/src/HOL/SPARK/Tools/spark_commands.ML")*)

 (*set theory imports "HOL-SPARK.SPARK"..* )

 spark_open \<open>/usr/local/isabisac/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>

 ( *Output + ERROR:

 {a = "//--- ##1# spark_open", files = fn, header = fn, prfx = ""} (line 14 of "/usr/local/isabisac/src/HOL/SPARK/Tools/spark_commands.ML") 

 {a = "##1# spark_open: before call \"files thy\", files = siv_header"} (line 18 of "/usr/local/isabisac/src/HOL/SPARK/Tools/spark_commands.ML") 

 No such file: "/usr/local/isabisac/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.str"\<^here>

 *)

 end