wneuper/isa: test/Tools/isac/BridgeJEdit/parseC.sml@e534316f9e07

     1 (* Title:  "BridgeJEdit/parseC.sml"

     2    Author: Walther Neuper

     3    (c) due to copyright terms

     4 *)

     6 "-----------------------------------------------------------------------------------------------";

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

     8 "-----------------------------------------------------------------------------------------------";

     9 "----------- complete Problem ------------------------------------------------------------------";

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

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

    12 "----------- Model-items -----------------------------------------------------------------------";

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

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

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

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

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

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

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

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

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

    22 "-----------------------------------------------------------------------------------------------";

    23 "-----------------------------------------------------------------------------------------------";

    24 "-----------------------------------------------------------------------------------------------";

    26 Thy_Header.get_keywords' @{context};

    27 (*

    28    Keywords

    29     {commands =

    30      {(".",

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

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

    33 :

    34      minor =

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

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

    37 :

    38 *)

    40 "----------- complete Problem ------------------------------------------------------------------";

    41 "----------- complete Problem ------------------------------------------------------------------";

    42 "----------- complete Problem ------------------------------------------------------------------";

    43 (* copy fromIsac's Java-Frontend:

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

    46   Specification:

    47     Model:

    48       Given: "Traegerlaenge L", "Streckenlast q_0"

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

    50       Find: "Biegelinie y"

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

    52     References:

    53       RTheory: "Biegelinie"

    54       RProblem: ["Biegelinien"]

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

    56   Solution:

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

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

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

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

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

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

    63     "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)"

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

    65     "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)"

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

    67     "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"

    68       Tactic Check_Postcond ["Biegelinien"]

    69 "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"

    70 *)

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

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

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

    75 val problem_headline_str =

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

    78 val toks = ParseC.tokenize problem_headline_str;

    79 case ParseC.problem_headline toks of

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

    81   => () | _ => error "TermC.parse problem_headline CHANGED"

    84 "----------- Model-items -----------------------------------------------------------------------";

    85 "----------- Model-items -----------------------------------------------------------------------";

    86 "----------- Model-items -----------------------------------------------------------------------";

    87 val given_comma_str = "Given: \"Traegerlaenge L\", \"Streckenlast q_0\"";

    88 val given_str = "Given: \"Traegerlaenge L\"(*,*) \"Streckenlast q_0\"";

    90 val toks = ParseC.tokenize given_str;

    91 (*

    92 (*given_comma_str\<rightarrow>*)val toks =

    93    [Token (("Given", ({}, {})), (Command, "Given"), Slot), Token ((":", ({}, {})), (Keyword, ":"), Slot), Token (("Traegerlaenge L", ({}, {})), (String, "Traegerlaenge L"), Slot),

    94     Token ((",", ({}, {})), (Keyword, ","), Slot), Token (("Streckenlast q_0", ({}, {})), (String, "Streckenlast q_0"), Slot)]

    95 (*given_str\<rightarrow>*)val toks =

    96    [Token (("Given", ({}, {})), (Command, "Given"), Slot), Token ((":", ({}, {})), (Keyword, ":"), Slot), Token (("Traegerlaenge L", ({}, {})), (String, "Traegerlaenge L"), Slot),

    97     Token (("Streckenlast q_0", ({}, {})), (String, "Streckenlast q_0"), Slot)]:

    98 *)

    99 val given_comma = Parse.command_name "Given" -- Parse.$$$ ":" -- Parse.list1 Parse.term;

   100 val given = Parse.command_name "Given" -- Parse.$$$ ":" -- Parse.list1 Parse.term;

   102 case ParseC.parse given_comma (ParseC.tokenize given_comma_str) of

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

   104     []) => ()

   105   (*^^^^--------------------------------- is empty:     parsing OK*)

   106 | _ => error "TermC.parse given_comma CHANGED";

   108 "----------- Parse.list1 DOES expect <,> between elements";

   109 case ParseC.parse given (ParseC.tokenize given_str) of

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

   111     [_(*Token (("Streckenlast q_0", ({}, {})), (String, "Streckenlast q_0"), Slot)*)]) => ()

   112   (*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ is NOT empty: parsing NOT ok*)

   113 | _ => error "TermC.parse given CHANGED";

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

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

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

   119 val model_str = (

   120   "Model:" ^

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

   122     "Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^

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

   124     "Find: \"Biegelinie y\"" ^

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

   126     );

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

   128   "Model:" ^

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

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

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

   132     "Find: \"Biegelinie \"" ^

   133     "Relate: \"Randbedingungen [ ]\""

   134     );

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

   136   "Model ( RProblem ):" ^

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

   138     "Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^

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

   140     "Find: \"Biegelinie y\"" ^

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

   142     );

   144 val toks = ParseC.tokenize model_str;

   145 case ParseC.parse ParseC.model toks of

   146 (((((((((((((((

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

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

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

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

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

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

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

   155 val toks = ParseC.tokenize model_empty_str;

   156 case ParseC.parse ParseC.model toks of

   157 (((((((((((((((

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

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

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

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

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

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

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

   166 val toks = ParseC.tokenize model_str_opt;

   167 case ParseC.parse ParseC.model toks of

   168 (((((((((((((((

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

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

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

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

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

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

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

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

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

   180 val references_collapsed_str = (

   181   "References:"

   182   );

   183 val references_str = (

   184   "References:"  ^

   185     "RTheory: \"Biegelinie\"" ^

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

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

   188     );

   189 val references_empty_str = (

   190   "References:"  ^

   191     "RTheory: \"\"" ^

   192     "RProblem: [\"\"]" ^

   193     "RMethod: [\"\"]"

   194     );

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

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

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

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

   201   "References", ":"),

   202      ((((((((

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

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

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

   206    [])

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

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

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

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

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

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

   214    [])

   215   => () | _ => error "TermC.parse references_empty_str CHANGED"

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

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

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

   221 val specification_str = (

   222     "Specification:" ^

   223        model_str ^

   224        references_str

   225        );

   226 val specification_collapsed_str = (

   227 "  Specification:" (** ) ^

   228 "    Model:"^

   229 "      Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^

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

   231 "      Find: \"Biegelinie y\"" ^

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

   233 "    References:" (**) ^

   234 "      RTheory: \"Biegelinie\"" (**) ^

   235 "      RProblem: [\"Biegelinien\"]" (**) ^

   236 "      RMethod: [\"Integrieren\", \"KonstanteBestimmen2\"]" ( **)

   237 );

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

   240   "Specification", ":"),

   241      (((((((((((((((

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

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

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

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

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

   247       ((

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

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

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

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

   252    [])

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

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

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

   257   "Specification", ":"),

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

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

   260    [])

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

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

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

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

   267 val tactic_Substitute_str =

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

   269 val tactic_Rewrite_Set_Inst_str =

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

   271 val tactic_Check_Postcond_str =

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

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

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

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

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

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

   280 case ParseC.rewrite_set_inst toks2 of

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

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

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

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

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

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

   289 val toks1' = ParseC.tokenize tactic_Substitute_str;

   290 val toks2' = ParseC.tokenize tactic_Rewrite_Set_Inst_str;

   291 val toks3' = ParseC.tokenize tactic_Check_Postcond_str;

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

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

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

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

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

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

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

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

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

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

   306 val steps_term_tac_str = (

   307   final_result_str ^

   308   "  Tactic Check_Postcond [\"Biegelinien\"]"

   309   );

   310 val steps_nonrec_str = (

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

   312      "\"y x = c_4 + c_3 * x + 1 / (-1 * EI)\"" (**) ^

   313         tactic_Substitute_str ^

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

   315         tactic_Rewrite_Set_Inst_str ^

   316      final_result_str (**) ^

   317         tactic_Check_Postcond_str ^

   318   final_result_str (**)

   319 );

   321 val toks1 = ParseC.tokenize steps_1_str;

   322 val toks2 = ParseC.tokenize steps_term_tac_str;

   323 val toks3 = ParseC.tokenize steps_nonrec_str;

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

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

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

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

   329 ParseC.parse ParseC.steps toks3;

   331 case ParseC.parse ParseC.steps toks3 of

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

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

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

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

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

   337   [])

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

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

   341 case ParseC.parse ParseC.steps_subpbl toks3 of

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

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

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

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

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

   347     [])

   348 => () | _ => error "TermC.parse steps, with exec_step_term, CHANGED";

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

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

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

   354 val solution_str = (

   355   "Solution:" ^

   356     steps_nonrec_str

   357   );

   358 val body_str = specification_str ^ solution_str;

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

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

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

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

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

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

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

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

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

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

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

   371   "Solution"), ":"),

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

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

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

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

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

   377     [])

   378 => () | _ => error "TermC.parse body CHANGED";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   399       "Solution"), ":"),

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

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

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

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

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

   405   ""),

   406 [])

   407   => () | _ => error "TermC.parse problem (whole) CHANGED"

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

   410 val toks = ParseC.tokenize (

   411   problem_headline_str ^

   412     "Specification:" ^

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

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

   415     "Solution:"

   416   );

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

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

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

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

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

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

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

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

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

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

   427   ""),

   428 [])

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

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

   432 val toks = ParseC.tokenize problem_headline_str;

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

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

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

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

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

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

   440         ""), ""), ""),

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

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

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

   444   ""),

   445 [])

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

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

   449 val toks = ParseC.tokenize (

   450   problem_headline_str ^

   451     "Specification:" ^

   452       model_str ^

   453       references_str ^

   454     "Solution:"

   455   );

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

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

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

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

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

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

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

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

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

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

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

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

   468       "Solution"), ":"),

   469         [])),

   470   ""),

   471 [])

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

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

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

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

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

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

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

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

   481       [])),

   482   ""),

   483 [])

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

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

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

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

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

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

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

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

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

   494       [])),

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

   496 [])

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

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

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

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

   503 val toks = ParseC.tokenize (

   504   problem_headline_str ^

   505     "Specification:" ^

   506       model_str ^

   507       references_str ^

   508     "Solution:"

   509   );

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

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

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

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

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

   515    } => ()

   516 | _ => error "read_out_problem CHANGED"

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

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

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

   522 (*TODO after Problem became recursive*)

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

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

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

   527 (*

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

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

   530   and preceeding the actual production code.

   531 *)

   532 val form_single =

   533   Parse.$$$ "(" --

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

   535   Parse.$$$ "," --

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

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

   538     Parse.$$$ "," --

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

   540     Parse.$$$ "," --

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

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

   543   Parse.$$$ ")";

   545 val form_single_str = (

   546   "(                                                                             " ^

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

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

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

   550   "    \"AbleitungBiegelinie dy\"],                                              " ^

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

   552   ")");

   554 val toks = ParseC.tokenize form_single_str;

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

   556   "(",

   557      ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

   558        "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",

   559        "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"]),

   560   ","),

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

   562   ")"),

   563 [])

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

   566 (* Isac always takes a singleton here *)

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

   568 type formalise =

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

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

   571 formalise: formalise parser;

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

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

   575   "(",

   576     ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

   577       "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",

   578       "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"]),

   579   ","),

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

   581   ")")],

   582 [])

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

author	wenzelm
	Mon, 19 Apr 2021 20:12:53 +0200
changeset 60237	e534316f9e07
parent 60230	0ca0f9363ad3
child 60242	73ee61385493
permissions	-rw-r--r--