(* Title:  "BridgeJEdit/parseC.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- Problem headline ------------------------------------------------------------------";

"----------- Model -----------------------------------------------------------------------------";

"----------- References ------------------------------------------------------------------------";

"----------- Specification: References + Model -------------------------------------------------";

"----------- Tactics ---------------------------------------------------------------------------";

"----------- steps -----------------------------------------------------------------------------";

"----------- body ------------------------------------------------------------------------------";

"----------- Problem ---------------------------------------------------------------------------";

"----------- fun read_out_problem --------------------------------------------------------------";

"----------- THERE ARE TESTS with INCOMPLETE WORK IN Test_Parse_Isac.thy -----------------------";

"----------- parser for exp_file.str -----------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

Thy_Header.get_keywords' @{context};

(*

   Keywords

    {commands =

     {(".",

        {files = [], id = 39558, kind = "qed", pos =

         {line=71, offset=3218, end_offset=3219, file=~~/src/Pure/Pure.thy}, tags = ["proof"]}),

:

     minor =

     {"!", "!!", "%", "(", ")", "+", ",", ":", "::", ";", "<", "<=", "=", "==", "=>", "?", "Find",

       "Given", "Model", "Problem", "RMethod", "RProblem", "RTheory", "References", "Relate",

:

*)

"----------- Problem headline ------------------------------------------------------------------";

"----------- Problem headline ------------------------------------------------------------------";

"----------- Problem headline ------------------------------------------------------------------";

val problem_headline_str =

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

val toks = ParseC.tokenize problem_headline_str;

case ParseC.problem_headline toks of

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

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

"----------- Model -----------------------------------------------------------------------------";

"----------- Model -----------------------------------------------------------------------------";

"----------- Model -----------------------------------------------------------------------------";

val model_str = (

  "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 ]\""

    );

val model_empty_str = ( (*Model before student's input"*)

  "Model:" ^

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

    "Given: \"Traegerlaenge \", \"Streckenlast \"" ^

    "Where: \"_ ist_integrierbar_auf {| |}\"" ^

    "Find: \"Biegelinie \"" ^

    "Relate: \"Randbedingungen [ ]\""

    );

val model_str_opt = ( (*Model explicitly referring to RProblem (default), not RMethod*)

  "Model ( RProblem ):" ^

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

    "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 ]\""

    );

val toks = ParseC.tokenize model_str;

case ParseC.parse ParseC.model toks of

(((((((((((((((

  "Model", (("", ""), "")), ":"),

    "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),

    "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),

    "Find"), ":"), _(*"<markup>"*)),

    "Relate"), ":"), [_(*"<markup>"*)]), [])

=> () | _ => error "parse model CHANGED";

"----------- Model before student's input";

val toks = ParseC.tokenize model_empty_str;

case ParseC.parse ParseC.model toks of

(((((((((((((((

  "Model", (("", ""), "")), ":"),

    "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),

    "Where"), ":"), [_(*"<markup>"*) (*//, _(*"<markup>"*) //*)]),

    "Find"), ":"), _(*"<markup>"*)),

    "Relate"), ":"), [_(*"<markup>"*)]), [])

=> () | _ => error "parse model_empty_str CHANGED";

"----------- Model explicitly referring to RProblem (default), not RMethod";

val toks = ParseC.tokenize model_str_opt;

case ParseC.parse ParseC.model toks of

(((((((((((((((

  "Model", (("(", "RProblem"), ")")), ":"),

    "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),

    "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),

    "Find"), ":"), _(*"<markup>"*)),

    "Relate"), ":"), [_(*"<markup>"*)]), [])

=> () | _ => error "parse model_str_opt CHANGED";

"----------- References ------------------------------------------------------------------------";

"----------- References ------------------------------------------------------------------------";

"----------- References ------------------------------------------------------------------------";

val references_collapsed_str = (

  "References:"

  );

val references_str = (

  "References:"  ^

    "RTheory: \"Biegelinie\"" ^

    "RProblem: [\"Biegelinien\"]" ^

    "RMethod: [\"Integrieren\", \"KonstanteBestimmen2\"]"

    );

val references_empty_str = (

  "References:"  ^

    "RTheory: \"\"" ^

    "RProblem: [\"\"]" ^

    "RMethod: [\"\"]"

    );

case ParseC.parse ParseC.references (ParseC.tokenize references_collapsed_str) of

  ((("References", ":"), (((((((("", ""), ""), ""), ""), []), ""), ""), [])), [])

  => () | _ => error "parse references_collapsed CHANGED";

case ParseC.parse ParseC.references (ParseC.tokenize references_str) of (((

  "References", ":"),

     ((((((((

    "RTheory", ":"), "Biegelinie"),

    "RProblem"), ":"), ["Biegelinien"]),

    "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])),

   [])

  => () | _ => error "parse references CHANGED";

case ParseC.parse ParseC.references (ParseC.tokenize references_empty_str) of (((

  "References", ":"), ((((((((

    "RTheory", ":"), ""),

    "RProblem"), ":"), [""]),

    "RMethod"), ":"), [""])),

   [])

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

"----------- Specification: References + Model -------------------------------------------------";

"----------- Specification: References + Model -------------------------------------------------";

"----------- Specification: References + Model -------------------------------------------------";

val specification_str = (

    "Specification:" ^

       model_str ^

       references_str

       );

val specification_collapsed_str = (

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

);

case ParseC.specification (ParseC.tokenize specification_str) of (((

  "Specification", ":"),

     (((((((((((((((

    "Model", (("", ""), "")), ":"),

      "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),

      "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),

      "Find"), ":"), _(*"<markup>"*)),

      "Relate"), ":"), [_(*"<markup>"*)]),

      ((

    "References", ":"), ((((((((

      "RTheory", ":"), "Biegelinie"),

      "RProblem"), ":"), ["Biegelinien"]),

      "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),

   [])

  => () | _ => error "parse specification (expanded) changed";

"----------- Specification collapsed";

case ParseC.parse ParseC.specification (ParseC.tokenize specification_collapsed_str) of (((

  "Specification", ":"),

(*model*)((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""),

(*refs?*)(((((((("", ""), ""), ""), ""), []), ""), ""), [])))),

   [])

  => () | _ => error "parse specification (collapsed) changed";

"----------- Tactics ---------------------------------------------------------------------------";

"----------- Tactics ---------------------------------------------------------------------------";

"----------- Tactics ---------------------------------------------------------------------------";

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)\"";

val toks1 = ParseC.tokenize "Substitute \"c_4 + c_3 * x +  1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\"";

case ParseC.substitute toks1 of ((("Substitute", _(*<markup>*)), _(*<markup>*)), [])

=> () | _ => error "parse Substitute CHANGED";

val toks2 = ParseC.tokenize "Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\"";

case ParseC.rewrite_set_inst toks2 of

  ((("Rewrite_Set_Inst", _(*<markup>*)), "make_ratpoly_in"), [])

=> () | _ => error "parse Rewrite_Set_Inst CHANGED";

val toks3 = ParseC.tokenize "Check_Postcond [\"Biegelinien\", \"xxx\"]";

case ParseC.check_postcond toks3 of (("Check_Postcond", ["Biegelinien", "xxx"]), [])

=> () | _ => error "parse Check_Postcond CHANGED";

"----------- Tactics collected";

val toks1' = ParseC.tokenize tactic_Substitute_str;

val toks2' = ParseC.tokenize tactic_Rewrite_Set_Inst_str;

val toks3' = ParseC.tokenize tactic_Check_Postcond_str;

ParseC.parse ParseC.tactic toks1'; (* = (("Tactic", "EXEC IMMEDIATELY: Substitute <markup> <markup>"), [])*)

ParseC.parse ParseC.tactic toks2'; (* = (("Tactic", "EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in"), [])*)

ParseC.parse ParseC.tactic toks3'; (* = (("Tactic", "EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien"), [])*)

case ParseC.parse ParseC.tactic (ParseC.tokenize tactic_Substitute_str) of

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

=> () | _ => error "parse Tactic Substitute CHANGED";

"----------- steps -----------------------------------------------------------------------------";

"----------- steps -----------------------------------------------------------------------------";

"----------- steps -----------------------------------------------------------------------------";

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

val steps_term_tac_str = (

  final_result_str ^

  "  Tactic Check_Postcond [\"Biegelinien\"]"

  );

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

);

val toks1 = ParseC.tokenize steps_1_str;

val toks2 = ParseC.tokenize steps_term_tac_str;

val toks3 = ParseC.tokenize steps_nonrec_str;

"----------- simple version";

ParseC.parse ParseC.steps []; (* = ([], []): (string * (string * string)) list * Token.T list *)

ParseC.parse ParseC.steps toks1; (* = ([("<markup>", ("", ""))], [])*) 

ParseC.parse ParseC.steps toks2; (* = ([("<markup>", ("Tactic", "EXEC IMMEDIATELY: Check_Postcond Biegelinien"))], [])*)

ParseC.parse ParseC.steps toks3;

case ParseC.parse ParseC.steps toks3 of

  ([(_(*"<markup>"*), ("", "")), 

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

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

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

    (_(*"<markup>"*), ("", ""))],

  [])

=> () | _ => error "parse steps, simple version, CHANGED";

"----------- version preparing subproblems";

case ParseC.parse ParseC.steps_subpbl toks3 of

   ([_(*"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 steps, with exec_step_term, CHANGED";

"----------- body ------------------------------------------------------------------------------";

"----------- body ------------------------------------------------------------------------------";

"----------- body ------------------------------------------------------------------------------";

val solution_str = (

  "Solution:" ^

    steps_nonrec_str

  );

val body_str = specification_str ^ solution_str;

case ParseC.parse ParseC.body (ParseC.tokenize body_str) of ((((((

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

    "Model", (("", ""), "")), ":"),

      "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),

      "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]), 

      "Find"), ":"), _(*"<markup>"*)),

      "Relate"), ":"), [_(*"<markup>"*)]), ((

    "References", ":"), ((((((((

      "RTheory", ":"), "Biegelinie"),

      "RProblem"), ":"), ["Biegelinien"]),

      "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),

  "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 body CHANGED";

"----------- Problem ---------------------------------------------------------------------------";

"----------- Problem ---------------------------------------------------------------------------";

"----------- Problem ---------------------------------------------------------------------------";

"----------- whole Problem";

val toks = ParseC.tokenize (problem_headline_str ^ specification_str ^ solution_str);

case ParseC.parse ParseC.problem toks of (((((((

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

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

      "Model", (("", ""), "")), ":"),

        "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),

        "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),

        "Find"), ":"), _(*"<markup>"*)),

        "Relate"), ":"), [_(*"<markup>"*)]), ((

      "References", ":"), ((((((((

        "RTheory", ":"), "Biegelinie"),

        "RProblem"), ":"), ["Biegelinien"]),

        "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),

      "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 (whole) CHANGED"

"----------- enter Specification";

val toks = ParseC.tokenize (

  problem_headline_str ^

    "Specification:" ^

      model_empty_str ^ (* <<<----- empty *)

      "References:" ^   (* <<<----- collapsed *)

    "Solution:"

  );

case ParseC.parse ParseC.problem toks of (((((((

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

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

      "Model", (("", ""), "")), ":"),

        "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),

        "Where"), ":"), [_(*"<markup>"*)]),

        "Find"), ":"), _(*"<markup>"*)),

        "Relate"), ":"), [_(*"<markup>"*)]), ((

      "References", ":"), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))),

    "Solution"), ":"), [])),

  ""),

[])

=> () | _ => error "parse enter Specification CHANGED"

"----------- Problem-headline only";

val toks = ParseC.tokenize problem_headline_str;

case ParseC.parse ParseC.problem toks of (((((((

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

    "", ""), (((((((((((((((

      "", (("", ""), "")), ""),

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

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

        ""), ""), ""),

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

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

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

  ""),

[]) 

=> () | _ => error "parse BEFORE enter Specification CHANGED"

"----------- finish Specification";

val toks = ParseC.tokenize (

  problem_headline_str ^

    "Specification:" ^

      model_str ^

      references_str ^

    "Solution:"

  );

case ParseC.parse ParseC.problem toks of ( ((((((

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

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

      "Model", (("", ""), "")), ":"),

        "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),

        "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),

        "Find"), ":"), _(*"<markup>"*)),

        "Relate"), ":"), [_(*"<markup>"*)]), ((

      "References", ":"), ((((((((

        "RTheory", ":"), "Biegelinie"),

        "RProblem"), ":"), ["Biegelinien"]),

        "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),

      "Solution"), ":"),

        [])),

  ""),

[])

=> () | _ => error "parse finish specification CHANGED"

"----------- Specification collapsed";

case ParseC.parse ParseC.problem (ParseC.tokenize problem_headline_str) of (((((((

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

    (*Specification*)"", ""), (((((((((((((((

      (*Model*)"", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""), ((((((((

      (*References*)"", ""), ""), ""), ""), []), ""), ""), [])))),

    (*Solution*)""), ""),

      [])),

  ""),

[])

=> () | _ => error "parse Specification collapsed CHANGED"

"----------- Problem with final_result, all collapsed";

val toks = ParseC.tokenize (problem_headline_str ^ final_result_str);

case ParseC.parse ParseC.problem toks of (((((((

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

    (*Specification*)"", ""), (((((((((((((((

      (*Model*)"", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""), ((((((((

      (*References*)"", ""), ""), ""), ""), []), ""), ""), [])))),

    (*Solution*)""), ""),

      [])),

  _(*"<markup>"*)),

[])

=> () | _ => error "parse Problem with final_result, all collapsed CHANGED"

"----------- fun read_out_problem --------------------------------------------------------------";

"----------- fun read_out_problem --------------------------------------------------------------";

"----------- fun read_out_problem --------------------------------------------------------------";

val toks = ParseC.tokenize (

  problem_headline_str ^

    "Specification:" ^

      model_str ^

      references_str ^

    "Solution:"

  );

case ParseC.parse ParseC.problem toks |> fst |> ParseC.read_out_problem of

  {thy_id = "Biegelinie", pbl_id = ["Biegelinien"],

   givens = [_(*"<markup>"*), _(*"<markup>"*)], wheres = [_(*"<markup>"*), _(*"<markup>"*)],

     find = _(*"<markup>"*), relates = [_(*"<markup>"*)],

   rthy_id = "Biegelinie", rpbl_id = ["Biegelinien"], rmet_id = ["Integrieren", "KonstanteBestimmen2"]

   } => ()

| _ => error "read_out_problem CHANGED"

"----------- THERE ARE TESTS with INCOMPLETE WORK IN Test_Parse_Isac.thy -----------------------";

"----------- THERE ARE TESTS with INCOMPLETE WORK IN Test_Parse_Isac.thy -----------------------";

"----------- THERE ARE TESTS with INCOMPLETE WORK IN Test_Parse_Isac.thy -----------------------";

(*TODO after Problem became recursive*)

"----------- parser for exp_file.str -----------------------------------------------------------";

"----------- parser for exp_file.str -----------------------------------------------------------";

"----------- parser for exp_file.str -----------------------------------------------------------";

(*

  For keyword Example SPARK's lexer and parser are used. Respective Isac code was developed 

  alongside existing SPARK code, not by tests. Here are tests for code using Isabelle technologies

  and preceeding the actual production code.

*)

val form_single =

  Parse.$$$ "(" --

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

  Parse.$$$ "," --

    Parse.$$$ "(" (* begin Formalise.spec *) --

      Parse.string -- (* ThyC.id, still not qualified *)

    Parse.$$$ "," --

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

    Parse.$$$ "," --

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

    Parse.$$$ ")" (* end Formalise.spec *) --

  Parse.$$$ ")";

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\"])" ^

  ")");

val toks = ParseC.tokenize form_single_str;

case ParseC.parse form_single toks of (((((((((((

  "(",

     ["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"]), ")"),

  ")"),

[])

=> () | _ => error "parse form_single toks CHANGED";

(* Isac always takes a singleton here *)

val formalise = (Parse.$$$ "[" |-- Parse.list1 form_single --| Parse.$$$ "]");

type formalise =

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

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

formalise: formalise parser;

val toks = ParseC.tokenize ("[" ^ form_single_str ^ "]");

case ParseC.parse formalise (ParseC.tokenize ("[" ^ form_single_str ^ "]")) of ([((((((((((

  "(",

    ["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"]), ")"),

  ")")],

[])

=> () | _ => error "parse formalise CHANGED";