(* Preparations for Isabelle/jEdit as Isac front-end.

   Walther Neuper 2018

*)

text \<open>These are first trials on introducing Isabelle/jEdit as Isac front-end with hints by Makarius.

  This file cannot be contained in Test_Isac as soon as "xxx" (within

  "Outer_Syntax.command @ {command_keyword xxx"}) is also known to Build_Isac.thy .

  Stepwise incrementing the parser requires outcommenting for the same reason.

\<close>

subsection \<open>definitions for keywords\<close>

theory Keywords_Diag

imports Isac.Isac_Knowledge (*Pure: not for Problem Biegelinie*)

keywords

  (* this has a type and thus is a "major keyword" *)

  "ISAC" :: diag and

  (* the following are without type: "minor keywords" *)

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

  "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 *) and

  "Tactic" (* optionally repeated with each step 0.. end of calculation *)

begin

subsection \<open>analyse functions' signatures in the command definition\<close>

subsubsection \<open>get args' types from command definition\<close>

ML \<open>

(*val _ =

  Outer_Syntax.command @{command_keyword ISAC}

    "embedded ISAC language" (* an initial hint by Makarius ...*)*)

    (Parse.input Parse.cartouche) >> (fn input =>

      Toplevel.keep (fn _ => ignore (ML_Lex.read_source input)))

  : Token.T list -> (Toplevel.transition -> Toplevel.transition) * Token.T list;

(*---------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ value of >>    *)

\<close> ML \<open>

op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c (* args -------vvv-- 1st -- 2nd*)

(*      ('a parser : T list -> 'a * T list

                        * (Input.source -> (Toplevel.transition -> Toplevel.transition))*)

\<close> ML \<open>

(Parse.input Parse.cartouche) : Input.source parser;

(*-----------------------------^^^^^^^^^^^^^^^^^^^^^----------------------------- 1st arg of >> *)

\<close> ML \<open>

(fn input =>

      Toplevel.keep (fn _ => ignore (ML_Lex.read_source input)))

  : Input.source -> (Toplevel.transition -> Toplevel.transition)

(*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 2nd arg of >> *)

\<close> ML \<open> (*decompose and investigate 1st arg..-------------------------------------------------  *)

Parse.input : 'a parser -> Input.source parser;

Parse.cartouche : string parser

\<close> ML \<open>

val input = Input.string "123"

(* = Source {delimited = true, range = ({}, {}), text = "123"}*)

: Input.source;

ML_Lex.read_source  (*true*) input

(* = [Text (Token (({}, {}), (Int, "123"))), Text (Token (({}, {}), (Space, " ")))]*)

  : ML_Lex.token Antiquote.antiquote list

\<close> ML \<open>

val input = Input.string "abc"

(* = Source {delimited = true, range = ({}, {}), text = "abc"}*)

: Input.source;

(*  ------decompose and investigate 2nd arg..-------------------------------------------------  *)

\<close> ML \<open>

ML_Lex.read_source  (*true*) input

(* = [Text (Token (({}, {}), (Ident, "abc"))), Text (Token (({}, {}), (Space, " ")))]*)

  : ML_Lex.token Antiquote.antiquote list

;

ignore (ML_Lex.read_source input) : unit

\<close> ML \<open>

Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))

  : Toplevel.transition -> Toplevel.transition

;

Toplevel.keep

  : (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition

\<close> 

subsubsection \<open>infer args' types of >> in command definition from types above\<close>

ML \<open>

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

(*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ signature of >>*)

(* analysis of types in "Outer_Syntax.command @{command_keyword ISAC}.." starts from value of >> :

                                     -> 'a -> 'd * 'c

value                                  \-------------/ *)

(*                                      'a : Token.T list

                                           -> 'd : Toplevel.transition -> Toplevel.transition

                                                 * 'c : Token.T list

2nd arg                   \--------/

                           'b : Input.source

                              -> 'd : Toplevel.transition -> Toplevel.transition    ((from value))

1st arg \-------------/

         'a : Token.T list                                     ((from value, initialised with []))

            -> 'b : Input.source                               ((from 2nd arg                   ))

                  * 'c : Token.T list                          ((from value, tail still unparsed))

         ^^^^^^^^^^^^^^^^^^^^^^^^^^ = Input.source parser : type 'a parser = T list -> 'a * T list

*)

\<close> ML \<open>

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

Parse.input Parse.cartouche : Input.source parser;

(*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 1st arg of >>  *)

\<close> ML \<open>

Parse.input : 'a parser -> Input.source parser;

Parse.cartouche : string parser

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

\<close> ML \<open>

\<close>

subsubsection \<open>tokenise input"\<close>

ML \<open>

\<close> ML \<open>

  Outer_Syntax.command @{command_keyword TEST_SIGNAT} "investigate signatures involveD"

    ((Parse.input Parse.cartouche) >> (fn input =>

      Toplevel.keep (fn _ => ignore (ML_Lex.read_source input) ) ) ) : unit

\<close> ML \<open>

ML_Lex.read_source: Input.source -> (ML_Lex.token Antiquote.antiquote) list

\<close> ML \<open>

Source.source:

   'a Scan.stopper ->

     ('a list -> 'b list * 'a list) ->

       ('a, 'c) Source.source -> ('b, ('a, 'c) Source.source) Source.source

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

K

\<close> ML \<open>

\<close> ML \<open>

\<close>

subsection \<open>stepwise incrementing the parser\<close>

text \<open>goal of this subsection is to extend ISAC_parser such, that the "complete ISAC calculation"

  at the bottom of this file is is parsed finally.

  "Outer_Syntax.command @ {command_keyword xxx}" is allowed only once in a theory,

  so outcomment accordingly !

\<close>

subsubsection \<open>step -1: investigate signatures "Problem Specification Model -- STOPPED HERE"\<close>

ML \<open>

\<close> ML \<open>

Parse.input : 'a parser -> Input.source parser;

Parse.cartouche : string parser; (* ... how build such parser <<<<<<<<<<<<<<---------------?(2)*)

Parse.input Parse.cartouche : Input.source parser;

\<close> ML \<open>

val input = Input.string "Problem Specification Model": Input.source

\<close> ML \<open>

(* build a dummy parser according to "?(2)": *)

Parse.$$$ : string -> string parser;

Parse.$$$ "Problem Specification Model" : string parser

\<close> ML \<open>

val xxx = Parse.input (Parse.$$$ "Problem Specification Model") : Input.source parser;

xxx : Input.source parser;

\<close> ML \<open>

val xxx : Input.source parser = fn (args : Token.T list) => (input, args);

(*                    where from get ------^^^^^^^^^^^^^            <<<<<<<<<<<<<<----------?(1)*)

(* ================== STOPPED WITH THIS QUESTION ===============================================*)

\<close> ML \<open>

ML_Lex.read_source : (*bool ->*) Input.source -> ML_Lex.token Antiquote.antiquote list

(* we don't need                                          ^^^^^^^^^^^^^^^^^^^ here *)

\<close> ML \<open>

ML_Lex.read_source  (*true*) input (* =

   [Text (Token (({}, {}), (Ident, "Problem"))), Text (Token (({}, {}), (Space, " "))),

    Text (Token (({}, {}), (Ident, "Specification"))), Text (Token (({}, {}), (Space, " "))),

    Text (Token (({}, {}), (Ident, "Model"))), Text (Token (({}, {}), (Space, " ")))]:

   ML_Lex.token Antiquote.antiquote list

*)

\<close> ML \<open>

\<close> 

subsubsection \<open>step 0: provide a structure for steps\<close>

ML \<open>

val ISAC_parser = Parse.cartouche;

ISAC_parser: string parser

\<close> ML \<open>

val check_ISAC : (Token.T list -> Input.source * Token.T list) = fn input => 

  let

    val toks = Parse.input ISAC_parser input

    val _ (*just check if input is according to ..*) = ISAC_parser

  in toks end

\<close> text \<open> (*ML -> Duplicate outer syntax command "ISAC" *)

val _ =  (*-------------v--------------------*)

  Outer_Syntax.command @ {command_keyword ISAC} "parsing stepwise incremented by check_ISAC"

    (check_ISAC >> (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))

\<close> ML \<open>

\<close>

subsubsection \<open>step 1: Problem ("Biegelinie", ["Biegelinien"]) etc\<close>

text \<open>

  we have {term "Problem (''Biegelinie'', [''Biegelinien''])"} !!!

  !!! as formula + as Tactic

\<close>

ML \<open>

val str =      "Problem (''Biegelinie'', [''Biegelinien''])"

val t = @{term "Problem (''Biegelinie'', [''Biegelinien''])"}

\<close> ML \<open>

val input = Input.string str

\<close> ML \<open>

val toks = ML_Lex.read_source input;

\<close> ML \<open>

toks: ML_Lex.token Antiquote.antiquote list

\<close> ML \<open>

length toks = 11;

nth 1 toks (* = Text (Token (({}, {}), (Ident, "Problem")))   <--------- (Keyword, "Problem") *);

nth 2 toks (* = Text (Token (({}, {}), (Space, " ")))*);

nth 3 toks (* = Text (Token (({}, {}), (Keyword, "(")))*);

nth 4 toks (*Text (Token (({}, {}), (Type_Var, "''Biegelinie''")))   <---------- Type_Var !?!?*);

nth 10 toks (* = Text (Token (({}, {}), (Keyword, ")")))*);

\<close> ML \<open>

ignore (ML_Lex.read_source input) : unit;

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

val str = "a=b";

val input = Input.string str

val toks = ML_Lex.read_source  (*true*) input;

nth 2 toks (* = Text (Token (({}, {}), (Keyword, "=")))    ----------^^^ (Keyword, "Problem") *);

\<close> ML \<open>

\<close>

subsubsection \<open>step 2: Model\<close>

ML \<open>

\<close> ML \<open>

val ISAC_parser = Parse.cartouche;

ISAC_parser: string parser

\<close> ML \<open>

val parse_Model = Parse.reserved "Model" --

  Parse.reserved "Given" -- Parse.list (Parse.term) --

  Parse.reserved "Where" -- Parse.list (Parse.term) --

  Parse.reserved "Find" -- Parse.term --

  Parse.reserved "Relate" -- Parse.list (Parse.term)

\<close> ML \<open>

parse_Model: Token.T list ->

  ((((((((string * string) * string list) * string) * string list) * string) * string) * string) * string list) * Token.T list

\<close> ML \<open> (*/---------- -> ERROR text cartouche was found ----------\*)

val ISAC_parser = (*a* ) parse_Model -- Parse.cartouche ( *a*)

                  (*b*) Parse.cartouche -- parse_Model (*b*)

\<close> ML \<open>

val check_ISAC : (Token.T list -> Input.source * Token.T list) = fn input => 

  let

    val toks = Parse.input ISAC_parser input

    val _ (*just check if input is according to ..*) = ISAC_parser

  in toks end

\<close> ML \<open> (*ML -> Duplicate outer syntax command "ISAC" *)

val _ =  (*-------------v--------------------*)

  Outer_Syntax.command @{command_keyword ISAC} "parsing stepwise incremented by check_ISAC"

    (check_ISAC >> (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))

\<close> ML \<open>

\<close>

(*/----- with above check_ISAC + ISAC_parser (*a*) | (*b*)*)

ISAC \<open>Model:

      Given: "Traegerlaenge L", "Streckenlast q_0"

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

      Find: "Biegelinie y"

      Relate: "Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]"

\<close>

(* ----- ERROR (*a*) | (*b*): * )

(*a*) Outer syntax error: reserved identifier "Model" expected,

but text cartouche was found:

\<open>Model: ...

(*b*) Outer syntax error\<^here>: reserved identifier "Model" expected,

but end-of-input\<^here> was found

( *\---------- -> ERROR text cartouche was found ----------/*)

subsection \<open>Makarius' hint on rendering ISAC calculation\<close>

text \<open>

  ISAC command definition, original by Makarius

/--- outcommented during stepwise incrementing the parser ----------------------------\

keywords "ISAC" :: diag

ML \<open>

val _ =

  Outer_Syntax.command @ {command_keyword ISAC}

    "embedded ISAC language" (* an initial hint by Makarius *)

    (Parse.input Parse.cartouche >> 

      (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))

\<close>

\--- outcommented during stepwise incrementing the parser ----------------------------/

\<close>

subsection \<open>complete ISAC calculation\<close>

(*/--- outcomment during stepwise incrementing the parser ----------------------------\*)

ISAC \<open>

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

  Specification:

    Model:

      Given: ["Traegerlaenge L", "Streckenlast q_0"] 

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

      Find: "Biegelinie y"

      Relate: ["Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]"]

    References:

      RTheory: "Biegelinie"

      RProblem: ["Biegelinien"]

      RMethod: ["Integrieren", "KonstanteBestimmen2"]

  Solution:

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

    "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^ 2,  y' x =  c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^ 2 + -1 * q_0 / 6 * x ^ 3),  y x =  c_4 + c_3 * x +  1 / (-1 * EI) *  (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)]"

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

    "[L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4,  0 = c_3]"

    "solveSystem [L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4,  0 = c_3] [c, c_1, c_2, c_4]"

    "[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"

    "y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)"

      Tactic Substitute "c_4 + c_3 * x +  1 / (-1 * EI) *  (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)" "[c, c_1, c_2, c_4]"

    "y x = 0 + 0 * x + 1 / (-1 * EI) * (-1 * L ^ 2 * q_0 / 2 / 2 * x ^ 2 + -1 * L * q_0 / -1 / 6 * x ^ 3 +  -1 * q_0 / 24 * x ^ 4)"

      Tactic Rewrite_Set_Inst "[(bdv, x)]" "make_ratpoly_in" "y x"

    "y x = -6 * q_0 * L ^ 2 / (-24 * EI) * x ^ 2 + 4 * L * q_0 / (-24 * EI) * x ^ 3 + -1 * q_0 / (-24 * EI) * x ^ 4"

      Tactic Check_Postcond ["Biegelinien"]

"y x = -6 * q_0 * L ^ 2 / (-24 * EI) * x ^ 2 + 4 * L * q_0 / (-24 * EI) * x ^ 3 + -1 * q_0 / (-24 * EI) * x ^ 4"

\<close>

(*\--- outcomment during stepwise incrementing the parser ----------------------------/*)

end