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

 theory Test_Parse_Isac

 (**)imports Isac.Calculation(**)

 keywords

   "OLDProblem" (* :: thy_decl  in Calculation.thy; this would break *_WITH_Problem*)

 begin

 chapter \<open>Tools and Goals\<close>

 section \<open>Tools\<close>

 ML \<open>

 \<close> ML \<open>

 open ParseC

 \<close> ML \<open>

 fun tokenize str =

   filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str)

 (* here we overwrite Calculation.thy "Problem" :: thy_decl -------^^^^^^^^^^*)

 \<close> ML \<open>

 fun string_of_strs strs = fold (curry op ^) (rev strs) ""

 \<close> ML \<open>

 \<close>

 section \<open>Goals for parsing\<close>

 subsection \<open>The final goal for parsing from a cartouche\<close>

 text \<open>

   Running example for development of parsing:

   # completely collapsed is

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

   # partially collapsed is

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

   # strings are not escaped (like in a cartouche)

   as follows:

 OLDProblem ("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:

     OLDProblem ("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)]"

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

       Specification:

       Solution:

     "[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 = -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>

 subsection \<open>The goal bypassing cartouches, terms shortened\<close>

 text \<open>

   for further goals see test/../parseC.sml

 \<close> ML \<open>

 val problem_headline_str_WITH_Problem =

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

 \<close> ML \<open>

 val problem_headline_str =

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

 \<close> ML \<open>

 val tactic_Substitute_str =

         "Tactic Substitute \"c_4 + c_3 * x +  1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\""

 val tactic_Rewrite_Set_Inst_str =

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

 val tactic_Check_Postcond_str =

         "Tactic Check_Postcond [\"Biegelinien\", \"xxx\"]"

 val final_result_str = "\"y x = -6 * q_0 * L ^ 2 / (-24 * EI)\""

 \<close> ML \<open>

 val steps_nonrec_str = (

      "\"[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)\"" (**) ^

         tactic_Substitute_str ^

      "\"y x = 0 + 0 * x + 1 / (-1 * EI)\"" (**) ^

         tactic_Rewrite_Set_Inst_str ^

      final_result_str (**) ^

         tactic_Check_Postcond_str ^

   final_result_str (**)

 )

 \<close> ML \<open>

 val steps_subproblem_str = (

      "OLDProblem (\"Biegelinie\", [\"vonBelastungZu\", \"Biegelinien\"])" ^

      "\"[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^ 2\"" ^

      "OLDProblem (\"Biegelinie\", [\"setzeRandbedingungen\", \"Biegelinien\"])" ^

        "Specification:" ^

        "Solution:" ^

      "\"[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)\"" (**) ^

         tactic_Substitute_str ^

      "\"y x = 0 + 0 * x + 1 / (-1 * EI)\"" (**) ^

         tactic_Rewrite_Set_Inst_str ^

      final_result_str (**) ^

         tactic_Check_Postcond_str ^

   final_result_str (**)

 )

 \<close> ML \<open>

 \<close>

 chapter \<open>OLDProblem\<close>

 section \<open>headline\<close>

 ML \<open>

 \<close> ML \<open>

 val toks_WITH_Problem = tokenize problem_headline_str_WITH_Problem

 \<close> ML \<open>

 \<close> ML \<open>

 val problem_headline_WITH_Problem = Parse.$$$ "OLDProblem" --

   Parse.$$$ "(" --

     Parse.string -- Parse.$$$ "," --

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

   Parse.$$$ ")"

 \<close> ML \<open>

 case problem_headline_WITH_Problem toks_WITH_Problem of

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

   => () | _ => error "parse problem_headline CHANGED"

 \<close> ML \<open>

 val problem_headline = (*Parse.$$$ "OLDProblem" --*)

   Parse.$$$ "(" --

     Parse.string -- Parse.$$$ "," --

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

   Parse.$$$ ")"

 \<close> ML \<open>

 val toks = tokenize problem_headline_str

 \<close> ML \<open>

 case problem_headline toks of

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

   => () | _ => error "parse problem_headline CHANGED"

 \<close> ML \<open>

 \<close>

 section \<open>towards recursion\<close>

 text \<open>

   we make steps close to recursive version according to subsequent subsubsection.

 \<close> ML \<open>

 val toks_WITH_Problem = tokenize (

   problem_headline_str_WITH_Problem ^

     "Specification:" ^

     "Solution:" ^

       steps_nonrec_str

 )

 \<close> ML \<open>

 val steps_nonrec =

   Scan.repeat (

     ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) (** ) ||

     (problem >> exec_subproblem) ( **)

   )

 : Token.T list -> string list * Token.T list

 \<close> ML \<open>

 steps_nonrec :    string list  parser

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

 \<close> ML \<open>

 \<close>

 declare [[ML_print_depth = 999]] (* ..for finding the type of steps_nonrec, exec_step_subproblem *)

 ML \<open>

 \<close> ML \<open> (* copy <Output> from val problem_nonrec = ..*)

 type problem_nonrec_WITH_Problem =

   (((((((((string * string) * string) * string) * string list) * string) *

          ((string * string) *

           (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) *

                 string) * string) * string) * string) * string list) *

            ((string * string) * ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list)))))

         * string) * string) * string list)

 (*                  ? repeat ^^^^^^^^^^^^*)

 \<close> ML \<open>

 val empty_problem_nonrec_WITH_Problem = 

   ((((((((("", ""), ""), ""), []), ""),

          (("", ""),

           ((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""),

                 ""), ""), ""), ""), []),

            (("", ""), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))))

        , ""), ""), [])

 \<close> ML \<open>

 val problem_nonrec_WITH_Problem =

   problem_headline_WITH_Problem --

     specification --

     Parse.$$$ "Solution" -- Parse.$$$ ":" -- steps_nonrec

   :

   problem_nonrec_WITH_Problem  parser

 (*               ^^^^^^^*)

 \<close> ML \<open>

 ParseC.parse problem_nonrec_WITH_Problem toks_WITH_Problem

 \<close> ML \<open>

 case ParseC.parse problem_nonrec_WITH_Problem toks_WITH_Problem of ((((((((((

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

         ((

     "Specification", ":"),

          ((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""), (((((((("", ""), ""), ""), ""), []), ""), ""), []))))),

     "Solution"), ":"),

       [_(*"EXEC IMMEDIATELY step_term: <markup> (, )"*),

        _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Substitute <markup> <markup>)"*),

        _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in)"*),

        _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien)"*),

        _(*"EXEC IMMEDIATELY step_term: <markup> (, )"*)]),

    [])

   => () | _ => error "parse problem_nonrec CHANGED"

 \<close> ML \<open>

 \<close>

 section \<open>problem_mini\<close>

 text \<open>

   we make a minimal problem in order to investigate types

   of the parser's components

 \<close> ML \<open>

 val problem_headline_mini = Parse.$$$ "OLDProblem" 

 \<close> ML \<open>

 val specification_mini = Parse.$$$ "Specification"

 \<close> ML \<open>

 fun exec_name str = "EXEC IMMEDIATELY exec_name: " ^ str;

 fun exec_int int = "EXEC IMMEDIATELY exec_int: " ^ string_of_int int;

 \<close> ML \<open>

 Parse.name >> exec_name: string parser;

 Parse.int >> exec_int  : string parser

 \<close> ML \<open>

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

 fun problem_mini toks =

   problem_headline_mini --

   specification_mini -- steps_mini toks

 and steps_mini _ =

   Parse.name >> exec_name || Parse.int >> exec_int

 \<close> ML \<open>

 (problem_mini "") (tokenize "OLDProblem Specification aaa")

 (* = ((("OLDProblem", "Specification"), "EXEC IMMEDIATELY exec_name: aaa"), [])*)

 \<close> ML \<open>

 problem_mini: 'a -> Token.T list -> ((string * string) * string) * Token.T list

 \<close> ML \<open>

 fun exec_problem_mini ((headl, spec), steps) =

   ["EXEC IMMEDIATELY exec_int: ((" ^ headl ^ ", " ^ spec ^ "0, " ^ string_of_strs steps];

 \<close> ML \<open>

 fun exec_name str = ["EXEC IMMEDIATELY exec_name: " ^ str];

 \<close> ML \<open>

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

 fun problem_mini toks =

   (problem_headline_mini --

   specification_mini -- steps_mini) toks

 and steps_mini toks =

   (Parse.name >> exec_name || problem_mini >> exec_problem_mini) toks

 \<close> ML \<open>

 problem_mini: Token.T list -> ((string * string) * string list) * Token.T list ;

 steps_mini  : Token.T list -> string list * Token.T list ;

 \<close> ML \<open>

 problem_mini: ((string * string) * string list) parser;

 steps_mini  : string list parser;

 \<close> ML \<open>

 problem_mini (tokenize "OLDProblem Specification aaa")

 (* = ((("OLDProblem", "Specification"), ["EXEC IMMEDIATELY exec_name: aaa"]), [])*)

 \<close> text \<open> ERROR ?!?!?

 parse problem_mini (tokenize "OLDProblem Specification   OLDProblem Specification")

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

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open> (* recursive + repeat *)

 fun exec_name str = "EXEC IMMEDIATELY exec_name: " ^ str;

 \<close> ML \<open>

 fun exec_problem_mini ((headl, spec), steps) =

   "EXEC IMMEDIATELY exec_int: ((" ^ headl ^ ", " ^ spec ^ "0, " ^ string_of_strs steps;

 \<close> ML \<open>

 fun problem_mini toks =

   (writeln ("problem_mini " ^ string_of_toks toks); problem_headline_mini --

   specification_mini -- (writeln ("steps_mini   " ^ string_of_toks toks); steps_mini)) toks

 and steps_mini toks =

   (Scan.repeat

     ((writeln ("name         " ^ string_of_toks toks); Parse.name >> exec_name) (**)||

      (writeln ("sub-problem  " ^ string_of_toks toks); problem_mini >> exec_problem_mini)(**))) toks

 \<close> text \<open>

 problem_mini (tokenize "OLDProblem Specification")

 (*

 problem_mini OLDProblem, Specification 

 steps_mini   OLDProblem, Specification 

 name          

 sub-problem   

 exception MORE () raised (line 159 of "General/scan.ML")*)

 \<close> text \<open>

 problem_mini (tokenize "OLDProblem Specification aaa")

 (*

 problem_mini OLDProblem, Specification, aaa 

 steps_mini   OLDProblem, Specification, aaa 

 name         aaa 

 sub-problem  aaa 

 exception MORE () raised (line 159 of "General/scan.ML")

 NOTE: this error persists in case outcommented (** )||

      (writeln ("sub-problem  " ^ string_of_toks toks); problem_mini >> exec_problem_mini)( **)

 THUS THERE IS SOMETHING NOT UNDERSTOOD, see !2! arguments in Test_Parsers_Cookbook.thy

 see Test_Parsers_Cookbook (* recursive parser p.140 \<section>6.1 adapted to tokens: *)

 *)

 \<close> ML \<open>

 \<close>

 section \<open>trials on recursion stopped\<close>

 text \<open>

   Trials on recursion have been postponed after parsing from cartouche

   (or even ?after executing Specification?).

 \<close> ML \<open>

 val toks_WITH_Problem = tokenize (

   problem_headline_str_WITH_Problem ^

     "Specification:" ^

     "Solution:" ^

       steps_subproblem_str

 )

 \<close> ML \<open> (* finding the type of exec_subproblem: *)

 fun problem_WITH_Problem xxx =

   problem_headline_WITH_Problem --

     specification --

     Parse.$$$ "Solution" -- Parse.$$$ ":" -- (steps xxx)

 and steps xxx =

       Scan.repeat (

         (Parse.term -- (Scan.optional tactic ("", "")) >> exec_step_term) ||

         (problem_WITH_Problem xxx >> xxx)

       )

 \<close> ML \<open>

 problem_WITH_Problem

 \<close> ML \<open> (* copy from <Output> abstracted ..*)

 problem_WITH_Problem : (problem_nonrec_WITH_Problem -> string) -> Token.T list -> problem_nonrec_WITH_Problem * Token.T list;

 (*  xxx : ^^^^^^^^^^^^^^^^^^^^^^^^^^                   vvvvvv*)

 problem_WITH_Problem : (problem_nonrec_WITH_Problem -> string) -> problem_nonrec_WITH_Problem parser

 \<close> ML \<open> (* compose arguments from empty_problem_nonrec ..*)

 fun subproblem_msg_WITH_Problem

   (((((((((s1, s2), s3), s4), strs0), s5),

          ((s6, s7),

           (((((((((((((((s11, ((s12, s13), s14)), s15), s16), s17), strs18), s19), s20), strs21), s22),

                 s23), s24), s25), s26), strs27),

            ((s31, s32), ((((((((s30, s33), s34), s35), s36), strs37), s38), s39), strs40)))))

        , s51), s61), strs71) = "EXEC IMMEDIATELY step_subproblem:\n" ^

 "  (((((((((" ^ s1 ^ ", " ^ s2 ^ "), " ^ s3 ^ "), " ^ s4 ^ "), " ^ string_of_strs strs0 ^ "), " ^ s5 ^ "),\n" ^

 "         ((" ^ s6 ^ ", " ^ s7 ^ "),\n" ^

 "          (((((((((((((((" ^ s11 ^ ", ((" ^ s12 ^ ", " ^ s13 ^ "), " ^ s14 ^ ")), " ^ s15 ^ "), " ^ s16 ^ "), " ^ s17 ^ "), " ^ string_of_strs strs18 ^ "), " ^ s19 ^ "), " ^ s20 ^ "), " ^ string_of_strs strs21 ^ "), " ^ s22 ^ "),\n" ^

                  s23 ^ "), " ^ s24 ^ "), " ^ s25 ^ "), " ^ s26 ^ "), " ^ string_of_strs strs27 ^ "),\n" ^

 "           ((" ^ s31 ^ ", " ^ s32 ^ "), ((((((((" ^ s30 ^ ", " ^ s33 ^ "), " ^ s34 ^ "), " ^ s35 ^ "), " ^ s36 ^ "), " ^ string_of_strs strs37 ^ "), " ^ s38 ^ "), " ^ s39 ^ "), " ^ string_of_strs strs40 ^ ")))))\n" ^

 "       , " ^ s51 ^ "), " ^ s61 ^ "), " ^ string_of_strs strs71 ^ ")"

 \<close> ML \<open>

 fun exec_subproblem_WITH_Problem

   (((((((((s1, s2), s3), s4), strs0), s5),

          ((s6, s7),

           (((((((((((((((s11, ((s12, s13), s14)), s15), s16), s17), strs18), s19), s20), strs21), s22),

                 s23), s24), s25), s26), strs27),

            ((s31, s32), ((((((((s30, s33), s34), s35), s36), strs37), s38), s39), strs40)))))

        , s51), s61), strs71) = subproblem_msg_WITH_Problem

   (((((((((s1, s2), s3), s4), strs0), s5),

          ((s6, s7),

           (((((((((((((((s11, ((s12, s13), s14)), s15), s16), s17), strs18), s19), s20), strs21), s22),

                 s23), s24), s25), s26), strs27),

            ((s31, s32), ((((((((s30, s33), s34), s35), s36), strs37), s38), s39), strs40)))))

        , s51), s61), strs71)

 \<close> ML \<open>

 exec_subproblem_WITH_Problem : problem_nonrec_WITH_Problem -> string

 \<close> ML \<open>

 \<close> ML \<open> (* exec_subproblem has right? type in problem *)

 fun problem_WITH_Problem _ =

   problem_headline_WITH_Problem --

     specification --

     Parse.$$$ "Solution" -- Parse.$$$ ":" -- (steps 1)

 and steps _ =

       Scan.repeat (

         (

           ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) ||

           (problem_WITH_Problem 1 >> exec_subproblem_WITH_Problem)

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

         )

       )

 \<close> ML \<open>

 problem_WITH_Problem : int -> problem_nonrec_WITH_Problem parser

 \<close> ML \<open>

 steps   : int -> string list    parser

 \<close> ML \<open> (* BUT: omitting the parsers' arguments does NOT work:

  *)

 \<close> ML \<open> (* here is the first attempt towards finalisation:

   THIS REQUIRES 1-2 ARGUMENTS, see Test_Parsers_Cookbook subsection "recursive parsers" * )

 val problem =

   problem_headline --

     specification --

     Parse.$$$ "Solution" -- Parse.$$$ ":" -- steps

 and steps =

       Scan.repeat (

         (

           ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) ||

           (problem >> exec_subproblem)

         )

       )

 *)

 \<close> ML \<open>

 \<close>

 end