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

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

keywords

  "Example" :: thy_load (*(isac_example)~(spark_vcg) ..would involve registering in Isabelle/Scala*)

  and(**)"Problem" :: thy_decl (*r oot-problem + recursively in Solution *)

  and "Specification" "Model" "References" :: diag (* structure only *)

  and "Solution" :: thy_decl (* structure only *)

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

(*and "Where" (* only output, preliminarily *)*)

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

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

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

begin

(** )declare [[ML_print_depth = 99999]]( **)

ML_file parseC.sml

ML_file preliminary.sml

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

text \<open>

  code for Example, Problem shifted into structure Preliminary.

\<close>

subsubsection \<open>cp from Pure.thy\<close>

ML \<open>

\<close> ML \<open> (* for "from" ~~ "Given:" *)

(* original *)

val facts = Parse.and_list1 Parse.thms1;

facts: (Facts.ref * Token.src list) list list parser;

\<close> ML \<open>

val facts =

  (writeln "####-## from parser";

    Parse.$$$ ":" |-- Parse.and_list1 Parse.thms1)(** ) --| Parse.$$$ "Where"( **);

facts: (Facts.ref * Token.src list) list list parser;

\<close> ML \<open>

\<close> ML \<open>

\<close>

subsubsection \<open>tools to analyse parsing in Outer_Syntax >> \<close>

ML \<open>

\<close> text \<open> (*original basics.ML*)

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

fun (x, y) |>> f = (f x, y);

\<close> text \<open> (*original scan.ML*)

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

fun (scan >> f) xs = scan xs |>> f;

\<close> ML \<open>

\<close> ML \<open> (*cp.from originals*)

infix 3 @>>;

fun (scan @>> f) xs = scan xs |>> f;

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

\<close> ML \<open> (*appl.to parser*)

op @>> : (Token.src -> 'b * Token.src) * ('b -> 'd) -> Token.src -> 'd * Token.src; (*---^^^*)

\<close> ML \<open>

\<close> ML \<open> (*add analysis*)

\<close> text \<open>

datatype T = Pos of (int * int * int) * Properties.T;

fun s_to_string (Pos ((line, offset, end_offset), _)) = ("Pos ((" ^

  string_of_int line ^ ", " ^ string_of_int offset ^ ", " ^ string_of_int end_offset ^ "), [_])")

s_to_string: src -> string

\<close> text \<open>

datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot

\<close> ML \<open>

Token.pos_of;        (*^^^^^^^^^^^^^^^*)

Token.end_pos_of;                      (*^^^^^^^^^^^^^*)

Token.unparse;                                            (*^^^^^^^^^^^^^*)

\<close> ML \<open>

fun string_of_tok tok = ("\nToken ((" ^

  Position.to_string (Token.pos_of tok) ^ ", " ^ 

  Position.to_string (Token.end_pos_of tok) ^ "), " ^

  Token.unparse tok ^ ", _)")

\<close> ML \<open>

fun string_of_toks toks = fold (curry op ^) (map string_of_tok toks |> rev |> separate ", ") "";

string_of_toks:    Token.src -> string;

\<close> ML \<open>

Token.s_to_string: Token.src -> string; (*<-- string_of_toks WN*)

\<close> ML \<open>

fun (scan @>> f) xs = (@{print}{a = "_ >> ", toks = xs(*GIVES\<rightarrow>"?"*)}; scan xs) |>> f;

fun (scan @>> f) xs = (writeln ("toks= " ^ Token.s_to_string xs);      scan xs) |>> f;

op @>> : (Token.src -> 'b * Token.src) * ('b -> 'd) -> Token.src -> 'd * Token.src; (*---^^^*)

\<close> ML \<open>

op @>> : (Token.T list -> 'a * 'b) * ('a -> 'c) -> Token.T list -> 'c * 'b

\<close> ML \<open>

\<close> ML \<open> (*Scan < Token in bootstrap, thus we take Token.s_to_string as argument of >> *)

infix 3 @@>>;

\<close> ML \<open>

fun ((write, scan) @@>> f) xs = (write xs;                             scan xs) |>> f;

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

\<close> ML \<open>

\<close>

subsubsection \<open>TODO\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

section \<open>setup command_keyword + preliminary test\<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_file -- Parse.parname

      >> (Toplevel.theory o           (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*)

        (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)) );

\<close> ML \<open>

val _ =

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

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

    ((writeln o Token.s_to_string, ParseC.problem_headline)

       @@>> (Toplevel.theory o Preliminary.init_specify));

\<close> ML \<open>

Preliminary.init_specify: ParseC.problem_headline -> theory -> theory;

(Toplevel.theory o Preliminary.init_specify)

  : ParseC.problem_headline -> Toplevel.transition -> Toplevel.transition;

\<close> ML \<open>

(**)                   Preliminary.init_specify: ParseC.problem_headline -> theory -> theory;(**)

(*                                                                          ^^^^^^    ^^^^^^*)

(**)(Toplevel.theory o Preliminary.init_specify):

      ParseC.problem_headline -> Toplevel.transition -> Toplevel.transition;(**)

(*                               ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^*)

\<close> ML \<open>

fun dummy (_(*":"*): string) thy =

  let

    val refs' = Refs_Data.get thy

    val o_model = OMod_Data.get thy

    val i_model = IMod_Data.get thy

    val _ =

      @{print} {a = "### dummy Specification", refs = refs', o_model = o_model, i_model = i_model}

  in thy end;

\<close> ML \<open>

val _ =

  Outer_Syntax.command \<^command_keyword>\<open>Specification\<close> "Specification dummy"

    ((writeln o Token.s_to_string, Parse.$$$ ":") @@>> (Toplevel.theory o dummy))

\<close> ML \<open>

fun dummy2 _ (thy: theory) = thy

\<close> ML \<open> (*or*)

fun dummy2 _ (ctxt: Proof.context) = ctxt

\<close> ML \<open>

val _ =

  Outer_Syntax.command \<^command_keyword>\<open>Model\<close> "Model dummy"

    ((writeln o Token.s_to_string, Parse.$$$ ":") @@>> (Toplevel.theory o dummy))

\<close> ML \<open>

val _ =

  Outer_Syntax.command \<^command_keyword>\<open>Given\<close> "input Given items to the Model of a Specification"

(*                                (facts    >> (Toplevel.proof o Proof.from_thmss_cmd));*)

    ((writeln o Token.s_to_string, facts) @@>> (Toplevel.proof o Proof.from_thmss_cmd));

val _ =

  Outer_Syntax.command \<^command_keyword>\<open>Where\<close> "input Find items to the Model of a Specification"

    (facts @>> (Toplevel.proof o Proof.from_thmss_cmd));

val _ =

  Outer_Syntax.command \<^command_keyword>\<open>Find\<close> "input Find items to the Model of a Specification"

    (facts @>> (Toplevel.proof o Proof.from_thmss_cmd));

val _ =

  Outer_Syntax.command \<^command_keyword>\<open>Relate\<close> "input Relate items to the Model of a Specification"

    (facts @>> (Toplevel.proof o Proof.from_thmss_cmd));

\<close> ML \<open>

(Toplevel.proof o Proof.from_thmss_cmd)

:

  (Facts.ref * Token.src list) list list -> Toplevel.transition -> Toplevel.transition

(*                                          ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^*)

\<close> ML \<open>

val _ =

  Outer_Syntax.command @{command_keyword References} "References dummy"

    (Parse.$$$ ":" >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));

val _ =

  Outer_Syntax.command @{command_keyword RTheory} "RTheory dummy"

    (Parse.$$$ ":" -- Parse.string 

      >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));

val _ =

  Outer_Syntax.command @{command_keyword RProblem} "RProblem dummy"

   (Parse.$$$ ":" -- (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]")

    >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));

val _ =

  Outer_Syntax.command @{command_keyword RMethod} "RMethod dummy"

   (Parse.$$$ ":" -- (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]")

    >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));

val _ =

  Outer_Syntax.command @{command_keyword Solution} "Solution dummy"

    (Parse.$$$ ":" >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));

\<close> ML \<open>

\<close> ML \<open>

\<close>

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

(**)

Example \<open>../Examples/exp_Statics_Biegel_Timischl_7-70.str\<close>

(**)

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

(*1 collapse* )

  Specification:

  (*2 collapse*)

    Model:

      Given: "Traegerlaenge " "Streckenlast " (*Bad context for command "Given"\<^here> -- using reset state*)

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

      Find: "Biegelinie "

      Relate: "Randbedingungen "

    References:

      (*3 collapse*)

      RTheory: ""                           (*Bad context for command "RTheory"\<^here> -- using reset state*)

      RProblem: ["", ""]

      RMethod: ["", ""]

      (*3 collapse*)

  (*2 collapse*)

  Solution:

( * 1 collapse*)

(*

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

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

*)

end