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

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

     2    Author: Walther Neuper

     3    (c) due to copyright terms

     4 *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    20 "-----------------------------------------------------------------------------------------------";

    21 "-----------------------------------------------------------------------------------------------";

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

    24 Thy_Header.get_keywords' @{context};

    25 (*

    26    Keywords

    27     {commands =

    28      {(".",

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

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

    31 :

    32      minor =

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

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

    35 :

    36 *)

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

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

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

    41 val problem_headline_str =

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

    44 val toks = ParseC.tokenize problem_headline_str;

    45 case ParseC.problem_headline toks of

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

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

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

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

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

    53 val model_str = (

    54   "Model:" ^

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

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

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

    58     "Find: \"Biegelinie y\"" ^

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

    60     );

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

    62   "Model:" ^

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

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

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

    66     "Find: \"Biegelinie \"" ^

    67     "Relate: \"Randbedingungen [ ]\""

    68     );

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

    70   "Model ( RProblem ):" ^

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

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

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

    74     "Find: \"Biegelinie y\"" ^

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

    76     );

    78 val toks = ParseC.tokenize model_str;

    79 case ParseC.parse ParseC.model toks of

    80 (((((((((((((((

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

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

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

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

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

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

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

    89 val toks = ParseC.tokenize model_empty_str;

    90 case ParseC.parse ParseC.model toks of

    91 (((((((((((((((

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

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

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

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

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

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

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

   100 val toks = ParseC.tokenize model_str_opt;

   101 case ParseC.parse ParseC.model toks of

   102 (((((((((((((((

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

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

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

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

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

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

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

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

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

   114 val references_collapsed_str = (

   115   "References:"

   116   );

   117 val references_str = (

   118   "References:"  ^

   119     "RTheory: \"Biegelinie\"" ^

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

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

   122     );

   123 val references_empty_str = (

   124   "References:"  ^

   125     "RTheory: \"\"" ^

   126     "RProblem: [\"\"]" ^

   127     "RMethod: [\"\"]"

   128     );

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

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

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

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

   135   "References", ":"),

   136      ((((((((

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

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

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

   140    [])

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

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

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

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

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

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

   148    [])

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

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

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

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

   155 val specification_str = (

   156     "Specification:" ^

   157        model_str ^

   158        references_str

   159        );

   160 val specification_collapsed_str = (

   161 "  Specification:" (** ) ^

   162 "    Model:"^

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

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

   165 "      Find: \"Biegelinie y\"" ^

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

   167 "    References:" (**) ^

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

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

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

   171 );

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

   174   "Specification", ":"),

   175      (((((((((((((((

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

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

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

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

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

   181       ((

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

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

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

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

   186    [])

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

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

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

   191   "Specification", ":"),

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

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

   194    [])

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

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

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

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

   201 val tactic_Substitute_str =

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

   203 val tactic_Rewrite_Set_Inst_str =

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

   205 val tactic_Check_Postcond_str =

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

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

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

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

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

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

   214 case ParseC.rewrite_set_inst toks2 of

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

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

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

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

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

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

   223 val toks1' = ParseC.tokenize tactic_Substitute_str;

   224 val toks2' = ParseC.tokenize tactic_Rewrite_Set_Inst_str;

   225 val toks3' = ParseC.tokenize tactic_Check_Postcond_str;

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

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

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

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

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

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

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

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

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

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

   240 val steps_term_tac_str = (

   241   final_result_str ^

   242   "  Tactic Check_Postcond [\"Biegelinien\"]"

   243   );

   244 val steps_nonrec_str = (

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

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

   247         tactic_Substitute_str ^

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

   249         tactic_Rewrite_Set_Inst_str ^

   250      final_result_str (**) ^

   251         tactic_Check_Postcond_str ^

   252   final_result_str (**)

   253 );

   255 val toks1 = ParseC.tokenize steps_1_str;

   256 val toks2 = ParseC.tokenize steps_term_tac_str;

   257 val toks3 = ParseC.tokenize steps_nonrec_str;

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

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

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

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

   263 ParseC.parse ParseC.steps toks3;

   265 case ParseC.parse ParseC.steps toks3 of

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

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

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

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

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

   271   [])

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

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

   275 case ParseC.parse ParseC.steps_subpbl toks3 of

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

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

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

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

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

   281     [])

   282 => () | _ => error "parse steps, with exec_step_term, CHANGED";

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

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

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

   288 val solution_str = (

   289   "Solution:" ^

   290     steps_nonrec_str

   291   );

   292 val body_str = specification_str ^ solution_str;

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

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

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

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

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

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

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

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

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

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

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

   305   "Solution"), ":"),

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

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

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

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

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

   311     [])

   312 => () | _ => error "parse body CHANGED";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   333       "Solution"), ":"),

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

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

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

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

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

   339   ""),

   340 [])

   341   => () | _ => error "parse problem (whole) CHANGED"

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

   344 val toks = ParseC.tokenize (

   345   problem_headline_str ^

   346     "Specification:" ^

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

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

   349     "Solution:"

   350   );

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

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

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

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

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

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

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

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

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

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

   361   ""),

   362 [])

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

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

   366 val toks = ParseC.tokenize problem_headline_str;

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

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

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

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

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

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

   374         ""), ""), ""),

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

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

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

   378   ""),

   379 [])

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

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

   383 val toks = ParseC.tokenize (

   384   problem_headline_str ^

   385     "Specification:" ^

   386       model_str ^

   387       references_str ^

   388     "Solution:"

   389   );

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

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

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

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

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

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

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

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

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

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

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

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

   402       "Solution"), ":"),

   403         [])),

   404   ""),

   405 [])

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

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

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

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

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

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

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

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

   415       [])),

   416   ""),

   417 [])

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

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

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

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

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

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

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

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

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

   428       [])),

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

   430 [])

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

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

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

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

   437 val toks = ParseC.tokenize (

   438   problem_headline_str ^

   439     "Specification:" ^

   440       model_str ^

   441       references_str ^

   442     "Solution:"

   443   );

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

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

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

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

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

   449    } => ()

   450 | _ => error "read_out_problem CHANGED"

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

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

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

   456 (*TODO after Problem became recursive*)

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

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

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

   461 (*

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

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

   464   and preceeding the actual production code.

   465 *)

   466 val form_single =

   467   Parse.$$$ "(" --

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

   469   Parse.$$$ "," --

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

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

   472     Parse.$$$ "," --

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

   474     Parse.$$$ "," --

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

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

   477   Parse.$$$ ")";

   479 val form_single_str = (

   480   "(                                                                             " ^

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

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

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

   484   "    \"AbleitungBiegelinie dy\"],                                              " ^

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

   486   ")");

   488 val toks = ParseC.tokenize form_single_str;

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

   490   "(",

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

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

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

   494   ","),

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

   496   ")"),

   497 [])

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

   500 (* Isac always takes a singleton here *)

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

   502 type formalise =

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

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

   505 formalise: formalise parser;

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

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

   509   "(",

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

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

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

   513   ","),

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

   515   ")")],

   516 [])

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

author	Walther Neuper <walther.neuper@jku.at>
	Fri, 22 Jan 2021 11:27:47 +0100
changeset 60147	d3cb5af53d3d
parent 60044	004bbb5d4417
child 60152	77a9287c56a3
permissions	-rw-r--r--