1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Sun Jan 17 15:25:27 2021 +0100
1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Fri Jan 22 11:27:47 2021 +0100
1.3 @@ -15,7 +15,7 @@
1.4 and "Problem" :: thy_decl (* root-problem + recursively in Solution;
1.5 "spark_vc" :: thy_goal *)
1.6 and "Specification" "Model" "References" "Solution" (* structure only *)
1.7 - and"Given" "Find" "Relate" "Where" (* await input of term *)
1.8 + and "Given" "Find" "Relate" "Where" (* await input of term *)
1.9 and "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *)
1.10 and "RProblem" "RMethod" (* await input of string list *)
1.11 "Tactic" (* optional for each step 0..end of calculation *)
1.12 @@ -643,8 +643,7 @@
1.13 "start a Specification, either from scratch or from preceding 'Example'"
1.14 (ParseC.problem >> prove_vc);
1.15 \<close> ML \<open>
1.16 -prove_vc: ParseC.problem -> Proof.context -> Proof.state
1.17 -\<close> ML \<open>
1.18 +prove_vc: ParseC.problem -> Proof.context -> Proof.state;
1.19 SPARK_Commands.prove_vc: string -> Proof.context -> Proof.state
1.20 \<close> ML \<open>
1.21 \<close>
2.1 --- a/src/Tools/isac/BridgeJEdit/parseC.sml Sun Jan 17 15:25:27 2021 +0100
2.2 +++ b/src/Tools/isac/BridgeJEdit/parseC.sml Fri Jan 22 11:27:47 2021 +0100
2.3 @@ -61,12 +61,15 @@
2.4
2.5 val tactic: Token.T list -> (string * string) * Token.T list
2.6
2.7 + (*Steps*)
2.8 + val steps: (string * (string * string)) list parser
2.9 + val exec_step_term: string * (string * string) -> string
2.10 + val steps_subpbl: string list parser
2.11 +
2.12 (*Problem*)
2.13 type body
2.14 val body: body parser
2.15 val body_dummy: body
2.16 - val exec_step_term: string * (string * string) -> string
2.17 -
2.18
2.19 val tokenize_string: Fdl_Lexer.chars -> Fdl_Lexer.T * Fdl_Lexer.chars
2.20 val scan: Fdl_Lexer.chars -> Fdl_Lexer.T list * Fdl_Lexer.chars
2.21 @@ -227,9 +230,15 @@
2.22
2.23 (** Step of term + tactic**)
2.24
2.25 +val steps = (Scan.repeat (Parse.term -- (Scan.optional tactic ("", ""))))
2.26 +
2.27 fun exec_step_term (tm, (tac1, tac2)) =
2.28 "EXEC IMMEDIATELY step_term: " ^ (*UnparseC.term*) tm ^ " (" ^ tac1 ^ ", " ^ tac2 ^ ")";
2.29 -
2.30 +val steps_subpbl =
2.31 + Scan.repeat (
2.32 + ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) (** ) ||
2.33 + (problem >> exec_subproblem) ( **)
2.34 + )
2.35
2.36 (** Body **)
2.37
3.1 --- a/src/Tools/isac/BridgeJEdit/preliminary.sml Sun Jan 17 15:25:27 2021 +0100
3.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml Fri Jan 22 11:27:47 2021 +0100
3.3 @@ -85,7 +85,7 @@
3.4 |> fst
3.5 |> ParseC.read_out_formalise
3.6 |> store_and_show
3.7 - val _ = @{print} {a = "### load_formalisation \<rightarrow>", formalise = formalise}
3.8 +(** )val _ = @{print} {a = "### load_formalisation \<rightarrow>", formalise = formalise}( **)
3.9 in
3.10 formalise thy'
3.11 end;
4.1 --- a/test/Pure/Isar/Test_Parse_Isac.thy Sun Jan 17 15:25:27 2021 +0100
4.2 +++ b/test/Pure/Isar/Test_Parse_Isac.thy Fri Jan 22 11:27:47 2021 +0100
4.3 @@ -1,31 +1,23 @@
4.4 subsection \<open>definitions for keywords\<close>
4.5
4.6 theory Test_Parse_Isac
4.7 - imports (**) Pure (** ) Isac.Isac_Knowledge (* required for LibraryC.strs2str *)( **)
4.8 -keywords (*see section \<open>Own trials ..\<close>*)
4.9 - (* this has a type and thus is a "major keyword" *)
4.10 - "ISAC" :: diag and
4.11 - (* the following are without type: "minor keywords" *)
4.12 - "Problem" (* root-problem + recursively in Solution *)
4.13 - "Specification" "Model" "References" "Solution" (* structure only *) and
4.14 - "Given" "Find" "Relate" "Where" (* await input of term *) and
4.15 - "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *) and
4.16 - "RProblem" "RMethod" (* await input of string list *) and
4.17 - "Tactic" (* optionally repeated with each step 0.. end of calculation*)
4.18 +(**)imports Isac.Calculation(**)
4.19 +keywords
4.20 + "OLDProblem" (* :: thy_decl in Calculation.thy; this would break *_WITH_Problem*)
4.21 begin
4.22
4.23 chapter \<open>Tools and Goals\<close>
4.24 section \<open>Tools\<close>
4.25 ML \<open>
4.26 +\<close> ML \<open>
4.27 +open ParseC
4.28 +\<close> ML \<open>
4.29 fun tokenize str =
4.30 filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str)
4.31 -\<close> ML \<open>
4.32 -fun parse parser toks = Scan.finite Token.stopper (Scan.error parser) toks
4.33 +(* here we overwrite Calculation.thy "Problem" :: thy_decl -------^^^^^^^^^^*)
4.34 \<close> ML \<open>
4.35 fun string_of_strs strs = fold (curry op ^) (rev strs) ""
4.36 \<close> ML \<open>
4.37 -fun string_of_toks toks = fold (curry op ^) (map Token.unparse toks |> rev |> separate ", ") "";
4.38 -\<close> ML \<open>
4.39 \<close>
4.40
4.41 section \<open>Goals for parsing\<close>
4.42 @@ -33,13 +25,13 @@
4.43 text \<open>
4.44 Running example for development of parsing:
4.45 # completely collapsed is
4.46 - Problem ("Biegelinie", ["vonBelastungZu", "Biegelinien"])
4.47 + OLDProblem ("Biegelinie", ["vonBelastungZu", "Biegelinien"])
4.48 # partially collapsed is
4.49 - Problem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"])
4.50 + OLDProblem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"])
4.51 # strings are not escaped (like in a cartouche)
4.52 as follows:
4.53
4.54 -Problem ("Biegelinie", ["Biegelinien"])
4.55 +OLDProblem ("Biegelinie", ["Biegelinien"])
4.56 Specification:
4.57 Model :
4.58 Given: "Traegerlaenge L", "Streckenlast q_0"
4.59 @@ -51,9 +43,9 @@
4.60 RProblem: ["Biegelinien"]
4.61 RMethod: ["Integrieren", "KonstanteBestimmen2"]
4.62 Solution:
4.63 - Problem ("Biegelinie", ["vonBelastungZu", "Biegelinien"])
4.64 + OLDProblem ("Biegelinie", ["vonBelastungZu", "Biegelinien"])
4.65 "[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)]"
4.66 - Problem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"])
4.67 + OLDProblem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"])
4.68 Specification:
4.69 Solution:
4.70 "[L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3]"
4.71 @@ -70,66 +62,15 @@
4.72 "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"
4.73 \<close>
4.74 subsection \<open>The goal bypassing cartouches, terms shortened\<close>
4.75 -ML \<open>
4.76 +text \<open>
4.77 + for further goals see test/../parseC.sml
4.78 \<close> ML \<open>
4.79 val problem_headline_str_WITH_Problem =
4.80 - "Problem ( \"Biegelinie\" , [\"Biegelinien\"] )"
4.81 + "OLDProblem ( \"Biegelinie\" , [\"Biegelinien\"] )"
4.82 \<close> ML \<open>
4.83 val problem_headline_str =
4.84 "( \"Biegelinie\" , [\"Biegelinien\"] )"
4.85 \<close> ML \<open>
4.86 -val model_str = (
4.87 - "Model:" ^
4.88 - (*^^^^^^^^^^^^*)
4.89 - "Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^
4.90 - "Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^
4.91 - "Find: \"Biegelinie y\"" ^
4.92 - "Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\""
4.93 -)
4.94 -\<close> ML \<open>
4.95 -val model_empty_str = (
4.96 - "Model:" ^
4.97 - (*^^^^^^^^^^^^*)
4.98 - "Given: \"Traegerlaenge \", \"Streckenlast \"" ^
4.99 - "Where: \"_ ist_integrierbar_auf {| |}\"" ^
4.100 - "Find: \"Biegelinie \"" ^
4.101 - "Relate: \"Randbedingungen [ ]\""
4.102 -)
4.103 -\<close> ML \<open>
4.104 -val model_str_opt = (
4.105 - "Model ( RProblem ):" ^
4.106 - (*^^^^^^^^^^^^*)
4.107 - "Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^
4.108 - "Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^
4.109 - "Find: \"Biegelinie y\"" ^
4.110 - "Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\""
4.111 -)
4.112 -\<close> ML \<open>
4.113 -val references_str = (
4.114 - "References:" ^
4.115 - "RTheory: \"Biegelinie\"" ^
4.116 - "RProblem: [\"Biegelinien\"]" ^
4.117 - "RMethod: [\"Integrieren\", \"KonstanteBestimmen2\"]"
4.118 -)
4.119 -\<close> ML \<open>
4.120 -val references_empty_str = (
4.121 - "References:" ^
4.122 - "RTheory: \"\"" ^
4.123 - "RProblem: [\"\"]" ^
4.124 - "RMethod: [\"\"]"
4.125 -)
4.126 -\<close> ML \<open>
4.127 -val references_collapsed_str = (
4.128 - "References:"
4.129 -)
4.130 -\<close> ML \<open>
4.131 -val problem_str = (
4.132 - problem_headline_str ^
4.133 - "Specification:" ^
4.134 - model_str ^
4.135 - references_str
4.136 -)
4.137 -\<close> ML \<open>
4.138 val tactic_Substitute_str =
4.139 "Tactic Substitute \"c_4 + c_3 * x + 1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\""
4.140 val tactic_Rewrite_Set_Inst_str =
4.141 @@ -150,9 +91,9 @@
4.142 )
4.143 \<close> ML \<open>
4.144 val steps_subproblem_str = (
4.145 - "Problem (\"Biegelinie\", [\"vonBelastungZu\", \"Biegelinien\"])" ^
4.146 + "OLDProblem (\"Biegelinie\", [\"vonBelastungZu\", \"Biegelinien\"])" ^
4.147 "\"[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^ 2\"" ^
4.148 - "Problem (\"Biegelinie\", [\"setzeRandbedingungen\", \"Biegelinien\"])" ^
4.149 + "OLDProblem (\"Biegelinie\", [\"setzeRandbedingungen\", \"Biegelinien\"])" ^
4.150 "Specification:" ^
4.151 "Solution:" ^
4.152 "\"[L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3]\"" ^
4.153 @@ -169,117 +110,26 @@
4.154 final_result_str (**)
4.155 )
4.156 \<close> ML \<open>
4.157 -val solution_str = (
4.158 - "Solution:" ^
4.159 - steps_nonrec_str
4.160 -)
4.161 -\<close> ML \<open>
4.162 -val problem_whole_str_WITH_Problem = (
4.163 - problem_headline_str_WITH_Problem ^
4.164 - "Specification:" ^
4.165 - model_str ^
4.166 - references_str ^
4.167 - "Solution:" ^
4.168 - steps_nonrec_str
4.169 -)
4.170 -\<close> ML \<open>
4.171 -if problem_whole_str_WITH_Problem =
4.172 - "Problem ( \"Biegelinie\" , [\"Biegelinien\"] )" ^
4.173 - "Specification:" ^
4.174 - "Model:" ^
4.175 - "Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^
4.176 - "Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^
4.177 - "Find: \"Biegelinie y\"" ^
4.178 - "Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\"" ^
4.179 - "References:" ^
4.180 - "RTheory: \"Biegelinie\"" ^
4.181 - "RProblem: [\"Biegelinien\"]" ^
4.182 - "RMethod: [\"Integrieren\", \"KonstanteBestimmen2\"]" ^
4.183 - "Solution:" ^
4.184 - "\"[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]\"" ^
4.185 - "\"y x = c_4 + c_3 * x + 1 / (-1 * EI)\"" ^
4.186 - "Tactic Substitute \"c_4 + c_3 * x + 1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\"" ^
4.187 - "\"y x = 0 + 0 * x + 1 / (-1 * EI)\"" ^
4.188 - "Tactic Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\"" ^
4.189 - "\"y x = -6 * q_0 * L ^ 2 / (-24 * EI)\"" ^
4.190 - "Tactic Check_Postcond [\"Biegelinien\", \"xxx\"]" ^
4.191 - "\"y x = -6 * q_0 * L ^ 2 / (-24 * EI)\""
4.192 -then () else error "problem_whole_str CHANGED"
4.193 -\<close> ML \<open>
4.194 -val problem_whole_str = (
4.195 - problem_headline_str ^
4.196 - "Specification:" ^
4.197 - model_str ^
4.198 - references_str ^
4.199 - "Solution:" ^
4.200 - steps_nonrec_str
4.201 -)
4.202 -\<close> ML \<open>
4.203 -if problem_whole_str =
4.204 - "( \"Biegelinie\" , [\"Biegelinien\"] )" ^
4.205 - "Specification:" ^
4.206 - "Model:" ^
4.207 - "Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^
4.208 - "Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^
4.209 - "Find: \"Biegelinie y\"" ^
4.210 - "Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\"" ^
4.211 - "References:" ^
4.212 - "RTheory: \"Biegelinie\"" ^
4.213 - "RProblem: [\"Biegelinien\"]" ^
4.214 - "RMethod: [\"Integrieren\", \"KonstanteBestimmen2\"]" ^
4.215 - "Solution:" ^
4.216 - "\"[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]\"" ^
4.217 - "\"y x = c_4 + c_3 * x + 1 / (-1 * EI)\"" ^
4.218 - "Tactic Substitute \"c_4 + c_3 * x + 1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\"" ^
4.219 - "\"y x = 0 + 0 * x + 1 / (-1 * EI)\"" ^
4.220 - "Tactic Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\"" ^
4.221 - "\"y x = -6 * q_0 * L ^ 2 / (-24 * EI)\"" ^
4.222 - "Tactic Check_Postcond [\"Biegelinien\", \"xxx\"]" ^
4.223 - "\"y x = -6 * q_0 * L ^ 2 / (-24 * EI)\""
4.224 -then () else error "problem_whole_str CHANGED"
4.225 -\<close> ML \<open>
4.226 \<close>
4.227
4.228 -subsection \<open>The goal with Problem recursively\<close>
4.229 -ML \<open>
4.230 -\<close> ML \<open>
4.231 -\<close> ML \<open>
4.232 -\<close> ML \<open>
4.233 -\<close> ML \<open>
4.234 -\<close> ML \<open>
4.235 -\<close>
4.236 -
4.237 -chapter \<open>Stepwise extending parser\<close>
4.238 -section \<open>Problem headline\<close>
4.239 +chapter \<open>OLDProblem\<close>
4.240 +section \<open>headline\<close>
4.241 ML \<open>
4.242 \<close> ML \<open>
4.243 val toks_WITH_Problem = tokenize problem_headline_str_WITH_Problem
4.244 \<close> ML \<open>
4.245 -Thy_Header.get_keywords' @{context}
4.246 -(*
4.247 - Keywords
4.248 - {commands =
4.249 - {(".",
4.250 - {files = [], id = 39558, kind = "qed", pos =
4.251 - {line=71, offset=3218, end_offset=3219, file=~~/src/Pure/Pure.thy}, tags = ["proof"]}),
4.252 -:
4.253 - minor =
4.254 - {"!", "!!", "%", "(", ")", "+", ",", ":", "::", ";", "<", "<=", "=", "==", "=>", "?", "Find",
4.255 - "Given", "Model", "Problem", "RMethod", "RProblem", "RTheory", "References", "Relate",
4.256 -:
4.257 -*)
4.258 \<close> ML \<open>
4.259 -val problem_headline_WITH_Problem = Parse.$$$ "Problem" --
4.260 +val problem_headline_WITH_Problem = Parse.$$$ "OLDProblem" --
4.261 Parse.$$$ "(" --
4.262 Parse.string -- Parse.$$$ "," --
4.263 (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") --
4.264 Parse.$$$ ")"
4.265 \<close> ML \<open>
4.266 case problem_headline_WITH_Problem toks_WITH_Problem of
4.267 - (((((("Problem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"), [])
4.268 + (((((("OLDProblem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"), [])
4.269 => () | _ => error "parse problem_headline CHANGED"
4.270 \<close> ML \<open>
4.271 -val problem_headline = (*Parse.$$$ "Problem" --*)
4.272 +val problem_headline = (*Parse.$$$ "OLDProblem" --*)
4.273 Parse.$$$ "(" --
4.274 Parse.string -- Parse.$$$ "," --
4.275 (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") --
4.276 @@ -293,815 +143,7 @@
4.277 \<close> ML \<open>
4.278 \<close>
4.279
4.280 -section \<open>Specification\<close>
4.281 -subsection \<open>Model\<close>
4.282 -ML \<open>
4.283 -\<close> ML \<open> (* original *)
4.284 -val model = (
4.285 - Parse.$$$ "Model" --
4.286 - (Scan.optional (*.. show, whether the Model refers to RProblem or to RMethod *)
4.287 - (Parse.$$$ "(" -- (Parse.$$$ "RProblem" || Parse.$$$ "RMethod") -- Parse.$$$ ")")
4.288 - (("", ""), "") ) --
4.289 - Parse.$$$ ":" --
4.290 - Parse.$$$ "Given" -- Parse.$$$ ":" -- Parse.list1 Parse.term --
4.291 - Parse.$$$ "Where" -- Parse.$$$ ":" -- Parse.list Parse.term --
4.292 - Parse.$$$ "Find" -- Parse.$$$ ":" -- Parse.term --
4.293 - Parse.$$$ "Relate" -- Parse.$$$ ":" -- Parse.list Parse.term
4.294 -)
4.295 -\<close> ML \<open>
4.296 -val toks = tokenize model_str
4.297 -\<close> ML \<open>
4.298 -case parse model toks of
4.299 -(((((((((((((((
4.300 - "Model", (("", ""), "")), ":"),
4.301 - "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.302 - "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.303 - "Find"), ":"), _(*"<markup>"*)),
4.304 - "Relate"), ":"), [_(*"<markup>"*)]), [])
4.305 -=> () | _ => error "parse model CHANGED"
4.306 -\<close> ML \<open>
4.307 -val toks = tokenize model_empty_str
4.308 -\<close> ML \<open>
4.309 -case parse model toks of
4.310 -(((((((((((((((
4.311 - "Model", (("", ""), "")), ":"),
4.312 - "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.313 - "Where"), ":"), [_(*"<markup>"*) (*//, _(*"<markup>"*) //*)]),
4.314 - "Find"), ":"), _(*"<markup>"*)),
4.315 - "Relate"), ":"), [_(*"<markup>"*)]), [])
4.316 -=> () | _ => error "parse model_empty_str CHANGED"
4.317 -\<close> ML \<open>
4.318 -\<close> ML \<open>
4.319 -\<close>
4.320 -
4.321 -subsection \<open>References\<close>
4.322 -ML \<open>
4.323 -\<close> ML \<open>
4.324 - Parse.$$$ "RTheory" -- Parse.$$$ ":" -- Parse.string (**) --
4.325 - Parse.$$$ "RProblem" -- Parse.$$$ ":" (**) --
4.326 - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (**) --
4.327 - Parse.$$$ "RMethod" -- Parse.$$$ ":" (**) --
4.328 - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (**)
4.329 - :
4.330 -((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list) parser
4.331 -\<close> ML \<open>
4.332 -type refs =
4.333 - ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list)
4.334 -\<close> ML \<open>
4.335 -val refs_dummy =
4.336 - (((((((("", ""), ""), ""), ""), []), ""), ""), [])
4.337 -\<close> ML \<open>
4.338 -val references = (
4.339 - Parse.$$$ "References" -- Parse.$$$ ":" (**) --
4.340 - (Scan.optional
4.341 - (Parse.$$$ "RTheory" -- Parse.$$$ ":" -- Parse.string (**) --
4.342 - Parse.$$$ "RProblem" -- Parse.$$$ ":" (**) --
4.343 - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (**) --
4.344 - Parse.$$$ "RMethod" -- Parse.$$$ ":" (**) --
4.345 - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]")
4.346 - )
4.347 - refs_dummy
4.348 - ))
4.349 -\<close> ML \<open>
4.350 -references: Token.T list -> ((string * string) * ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list)) * Token.T list;
4.351 -(* ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list)*)
4.352 -references: Token.T list -> ((string * string) * refs) * Token.T list;
4.353 -references: ((string * string) * refs) parser
4.354 -\<close> ML \<open>
4.355 -parse references (tokenize references_collapsed_str)
4.356 -\<close> ML \<open>
4.357 -case parse references (tokenize references_collapsed_str) of
4.358 - ((("References", ":"), (((((((("", ""), ""), ""), ""), []), ""), ""), [])), [])
4.359 - => () | _ => error "parse references_collapsed CHANGED"
4.360 -\<close> ML \<open>
4.361 -case parse references (tokenize references_str) of (((
4.362 - "References", ":"),
4.363 - ((((((((
4.364 - "RTheory", ":"), "Biegelinie"),
4.365 - "RProblem"), ":"), ["Biegelinien"]),
4.366 - "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])),
4.367 - [])
4.368 - => () | _ => error "parse references CHANGED"
4.369 -\<close> ML \<open>
4.370 -references (tokenize references_empty_str)
4.371 -\<close> ML \<open>
4.372 -case references (tokenize references_empty_str) of (((
4.373 - "References", ":"), ((((((((
4.374 - "RTheory", ":"), ""),
4.375 - "RProblem"), ":"), [""]),
4.376 - "RMethod"), ":"), [""])),
4.377 - [])
4.378 - => () | _ => error "parse references_empty_str CHANGED"
4.379 -\<close> ML \<open>
4.380 -\<close>
4.381 -
4.382 -subsection \<open>Model -- References\<close>
4.383 -ML \<open>
4.384 -\<close> ML \<open>
4.385 -val toks = tokenize (model_str ^ references_str)
4.386 -\<close> ML \<open>
4.387 -length toks = 35;
4.388 -\<close> ML \<open>
4.389 -(model -- references) toks
4.390 -(* = ((((((((((((((((
4.391 - "Model", (("", ""), "")), ":"),
4.392 - "Given"), ":"), ["<markup>", "<markup>"]),
4.393 - "Where"), ":"), ["<markup>", "<markup>"]),
4.394 - "Find"), ":"), "<markup>"),
4.395 - "Relate"), ":"), ["<markup>"]), ((
4.396 - "References", ":"), ((((((((
4.397 - "RTheory", ":"), "Biegelinie"),
4.398 - "RProblem"), ":"), ["Biegelinien"]),
4.399 - "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"]))),
4.400 -[])*)
4.401 -\<close> ML \<open>
4.402 -\<close>
4.403 -
4.404 -subsection \<open>Specification: Model -- References\<close>
4.405 -ML \<open>
4.406 -\<close> ML \<open>
4.407 -val specification_str = (
4.408 - "Specification:" ^
4.409 - model_str ^
4.410 - references_str
4.411 - )
4.412 -\<close> ML \<open>
4.413 -val toks = tokenize specification_str
4.414 -\<close> ML \<open>
4.415 -length toks = 37;
4.416 -\<close> ML \<open>
4.417 -val specification_whole = (
4.418 - Parse.$$$ "Specification" -- Parse.$$$ ":" (**) --
4.419 - (model -- references) (**)
4.420 -)
4.421 -\<close> ML \<open>
4.422 -parse specification_whole toks
4.423 -(* = (((
4.424 - "Specification", ":"), (((((((((((((((
4.425 - "Model", (("", ""), "")), ":"),
4.426 - "Given"), ":"), ["<markup>", "<markup>"]),
4.427 - "Where"), ":"), ["<markup>", "<markup>"]),
4.428 - "Find"), ":"), "<markup>"),
4.429 - "Relate"), ":"), ["<markup>"]), ((
4.430 - "References", ":"), ((((((((
4.431 - "RTheory", ":"), "Biegelinie"),
4.432 - "RProblem"), ":"), ["Biegelinien"]),
4.433 - "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),
4.434 -[])*)
4.435 -\<close> ML \<open>
4.436 -\<close>
4.437 -
4.438 -subsection \<open>Specification: Scan.optional Model -- References\<close>
4.439 -ML \<open>
4.440 -\<close> ML \<open>
4.441 -(model -- references)
4.442 -: (((((((((((((((string * ((string * string) * string)) * string) * string) * string) *
4.443 - string list) * string) * string) * string list) * string) * string) * string) * string) * string) *
4.444 - string list) *
4.445 - ((string * string) * ((((((((string * string) * string) * string) * string) * string list) *
4.446 - string) * string) * string list))) parser
4.447 -\<close> ML \<open>
4.448 -type model_refs_dummy = (((((((((((((((string * ((string * string) * string)) * string) * string) * string) *
4.449 - string list) * string) * string) * string list) * string) * string) * string) * string) * string) *
4.450 - string list) *
4.451 - ((string * string) * ((((((((string * string) * string) * string) * string) * string list) *
4.452 - string) * string) * string list)))
4.453 -\<close> ML \<open>
4.454 -val string = "";
4.455 -val model_refs_dummy = ((((((((((((((("", (("", ""), "")), ""), ""), ""),
4.456 - []), ""), ""), []), ""), ""), ""), ""), ""),
4.457 - []),
4.458 - (("", ""), (((((((("", ""), ""), ""), ""), []),
4.459 - ""), ""), [])))
4.460 -\<close> ML \<open>
4.461 -model_refs_dummy : model_refs_dummy
4.462 -\<close> ML \<open>
4.463 -val specification = (
4.464 - (Parse.$$$ "Specification" -- Parse.$$$ ":") --
4.465 - (Scan.optional
4.466 - (model -- references)
4.467 - )
4.468 - model_refs_dummy
4.469 -)
4.470 -\<close> ML \<open> (*whole Specification from above -----------------------------------------------------\*)
4.471 -specification (tokenize specification_str)
4.472 -\<close> ML \<open>
4.473 -case specification (tokenize specification_str) of (((
4.474 - "Specification", ":"),
4.475 - (((((((((((((((
4.476 - "Model", (("", ""), "")), ":"),
4.477 - "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.478 - "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.479 - "Find"), ":"), _(*"<markup>"*)),
4.480 - "Relate"), ":"), [_(*"<markup>"*)]),
4.481 - ((
4.482 - "References", ":"), ((((((((
4.483 - "RTheory", ":"), "Biegelinie"),
4.484 - "RProblem"), ":"), ["Biegelinien"]),
4.485 - "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),
4.486 - [])
4.487 - => () | _ => error "parse specification (expanded) changed"
4.488 -\<close> ML \<open>
4.489 -(specification toks) : ((string * string) * model_refs_dummy) * Token.T list
4.490 -\<close> ML \<open>
4.491 -\<close> ML \<open> (*Specification collapsed ------------------------------------------------------------\*)
4.492 -val toks = tokenize (
4.493 -" Specification:" (** ) ^
4.494 -" Model:"^
4.495 -" Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^
4.496 -" Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^
4.497 -" Find: \"Biegelinie y\"" ^
4.498 -" Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\"" ^
4.499 -" References:" (**) ^
4.500 -" RTheory: \"Biegelinie\"" (**) ^
4.501 -" RProblem: [\"Biegelinien\"]" (**) ^
4.502 -" RMethod: [\"Integrieren\", \"KonstanteBestimmen2\"]" ( **)
4.503 -)
4.504 -\<close> ML \<open>
4.505 -parse specification toks
4.506 -\<close> ML \<open>
4.507 -parse specification toks
4.508 -\<close> ML \<open>
4.509 -case parse specification toks of (((
4.510 - "Specification", ":"),
4.511 -(*model*)((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""),
4.512 -(*refs?*)(((((((("", ""), ""), ""), ""), []), ""), ""), [])))),
4.513 - [])
4.514 - => () | _ => error "parse specification (collapsed) changed"
4.515 -\<close> ML \<open>
4.516 -\<close>
4.517 -
4.518 -section \<open>Tactics\<close>
4.519 -ML \<open>
4.520 -val toks1 = tokenize "Substitute \"c_4 + c_3 * x + 1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\""
4.521 -val substitute = Parse.reserved "Substitute" -- Parse.term -- Parse.term;
4.522 -case substitute toks1 of ((("Substitute", _(*<markup>*)), _(*<markup>*)), [])
4.523 -=> () | _ => error "parse Substitute CHANGED";
4.524 -\<close> ML \<open>
4.525 -val toks2 = tokenize "Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\""
4.526 -val rewrite_set_inst = Parse.reserved "Rewrite_Set_Inst" -- Parse.term -- Parse.name;
4.527 -case rewrite_set_inst toks2 of
4.528 - ((("Rewrite_Set_Inst", _(*<markup>*)), "make_ratpoly_in"), [])
4.529 -=> () | _ => error "parse Rewrite_Set_Inst CHANGED";
4.530 -\<close> ML \<open>
4.531 -val toks3 = tokenize "Check_Postcond [\"Biegelinien\", \"xxx\"]"
4.532 -val check_postcond = Parse.reserved "Check_Postcond" --
4.533 - (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]");
4.534 -case check_postcond toks3 of (("Check_Postcond", ["Biegelinien", "xxx"]), [])
4.535 -=> () | _ => error "parse Check_Postcond CHANGED"
4.536 -\<close> ML \<open>
4.537 -\<close> ML \<open>
4.538 -\<close> ML \<open> (* see test/../Test_Parsers.thy \<open>|| requires arguments of equal type; 2 tricks that help:\<close>
4.539 - semantics is NOT YET fully understood *)
4.540 -fun exec_substitute ((str, tm), bdv) =
4.541 - "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*UnparseC.term*) tm ^ " " ^ (*UnparseC.term*) bdv;
4.542 -fun exec_rewrite_set_inst ((str, tm), id) =
4.543 - "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*UnparseC.term*) tm ^ " " ^ (*Problem.id_to_string*) id;
4.544 -fun exec_check_postcond (str, path) =
4.545 - "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*Problem.id_to_string*)fold (curry op ^) path "";
4.546 -\<close> ML \<open>
4.547 -val toks1' = tokenize tactic_Substitute_str
4.548 -val toks2' = tokenize tactic_Rewrite_Set_Inst_str
4.549 -val toks3' = tokenize tactic_Check_Postcond_str
4.550 -\<close> ML \<open>
4.551 -val tactic = ( (* incomplete list of tactics *)
4.552 -Parse.$$$ "Tactic" --
4.553 - (substitute >> exec_substitute (**) ||
4.554 - rewrite_set_inst >> exec_rewrite_set_inst (**)||
4.555 - check_postcond >> exec_check_postcond (**)
4.556 - )
4.557 -)
4.558 -\<close> ML \<open>
4.559 -parse tactic toks1'; (* = (("Tactic", "EXEC IMMEDIATELY: Substitute <markup> <markup>"), [])*)
4.560 -parse tactic toks2'; (* = (("Tactic", "EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in"), [])*)
4.561 -parse tactic toks3'; (* = (("Tactic", "EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien"), [])*)
4.562 -\<close> ML \<open>
4.563 -\<close>
4.564 -
4.565 -section \<open>Solution\<close>
4.566 -text \<open>
4.567 - Problem might occur recursively in Solution.
4.568 - for recursive parsers see p.140 \<section>6.2: parse_tree
4.569 -\<close>
4.570 -subsection \<open>steps\<close>
4.571 -ML \<open>
4.572 -\<close> ML \<open>
4.573 -val steps_1_str = "\"[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]\""
4.574 -val steps_term_tac_str = (
4.575 - final_result_str ^
4.576 - " Tactic Check_Postcond [\"Biegelinien\"]"
4.577 -)
4.578 -\<close> ML \<open>
4.579 -val toks1 = tokenize steps_1_str
4.580 -val toks2 = tokenize steps_term_tac_str
4.581 -val toks3 = tokenize steps_nonrec_str
4.582 -\<close> ML \<open>
4.583 -\<close> ML \<open> (* simple version -----------------------------------------------------------------------*)
4.584 -val steps = (Scan.repeat (Parse.term -- (Scan.optional tactic ("", ""))))
4.585 -:
4.586 -(string * (string * string)) list parser
4.587 -\<close> ML \<open>
4.588 -parse steps []; (* = ([], []): (string * (string * string)) list * Token.T list *)
4.589 -parse steps toks1; (* = ([("<markup>", ("", ""))], [])*)
4.590 -parse steps toks2; (* = ([("<markup>", ("Tactic", "EXEC IMMEDIATELY: Check_Postcond Biegelinien"))], [])*)
4.591 -\<close> ML \<open>
4.592 -parse steps toks3;
4.593 -\<close> ML \<open>
4.594 -case parse steps toks3 of
4.595 - ([(_(*"<markup>"*), ("", "")),
4.596 - (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Substitute <markup> <markup>"*))),
4.597 - (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in"*))),
4.598 - (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Check_Postcond Biegelinien"*))),
4.599 - (_(*"<markup>"*), ("", ""))],
4.600 - [])
4.601 -=> () | _ => error "parse steps, simple version, CHANGED";
4.602 -\<close> ML \<open>
4.603 -\<close> ML \<open> (* version preparing subproblems --------------------------------------------------------*)
4.604 -fun exec_step_term (tm, (tac1, tac2)) =
4.605 - "EXEC IMMEDIATELY step_term: " ^ (*UnparseC.term*) tm ^ " (" ^ tac1 ^ ", " ^ tac2 ^ ")";
4.606 -\<close> ML \<open>
4.607 -val steps =
4.608 - Scan.repeat (
4.609 - ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) (** ) ||
4.610 - (problem >> exec_subproblem) ( **)
4.611 - )
4.612 -\<close> ML \<open>
4.613 -parse steps toks3
4.614 -\<close> ML \<open>
4.615 -case parse steps toks3 of
4.616 - ([_(*"EXEC IMMEDIATELY step_term: <markup> (, )"*),
4.617 - _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Substitute <markup> <markup>)"*),
4.618 - _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in)"*),
4.619 - _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien)"*),
4.620 - _(*"EXEC IMMEDIATELY step_term: <markup> (, )"*)],
4.621 - [])
4.622 -=> () | _ => error "parse steps, with exec_step_term, CHANGED";
4.623 -\<close> ML \<open>
4.624 -\<close>
4.625 -
4.626 -subsection \<open>solution\<close>
4.627 -ML \<open>
4.628 -\<close> ML \<open>
4.629 -val toks = tokenize solution_str
4.630 -\<close> ML \<open> (* not explicit in problem *)
4.631 -val solution = Parse.$$$ "Solution" -- Parse.$$$ ":" -- steps
4.632 -\<close> ML \<open>
4.633 -parse solution toks
4.634 -\<close> ML \<open>
4.635 -parse solution toks
4.636 -\<close> ML \<open>
4.637 -case parse solution toks of
4.638 - ((("Solution", ":"),
4.639 - [_(*"EXEC IMMEDIATELY step_term: <markup> (, )"*),
4.640 - _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Substitute <markup> <markup>)"*),
4.641 - _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in)"*),
4.642 - _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien)"*),
4.643 - _(*"EXEC IMMEDIATELY step_term: <markup> (, )"*)]),
4.644 - [])
4.645 -=> () | _ => error "parse solution CHANGED";
4.646 -\<close> ML \<open>
4.647 -\<close>
4.648 -
4.649 -section \<open>body of Problem\<close>
4.650 -ML \<open>
4.651 -\<close> ML \<open>
4.652 -val body_str = specification_str ^ solution_str
4.653 -\<close> ML \<open>
4.654 -val toks = tokenize body_str
4.655 -\<close> ML \<open>
4.656 -val body =
4.657 - specification --
4.658 - Parse.$$$ "Solution" -- Parse.$$$ ":" --
4.659 - (*/----- this will become "and steps".. *)
4.660 - (Scan.repeat (
4.661 - ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) (** ) ||
4.662 - (problem >> exec_subproblem) ( *exec_* make types equal for both args of ||*)
4.663 - ))
4.664 - (*\----- ..this will become "and steps" *)
4.665 -\<close> ML \<open>
4.666 -\<close> ML \<open>
4.667 -\<close>
4.668 -
4.669 -section \<open>Problem\<close>
4.670 -subsection \<open>type problem\<close>
4.671 -ML \<open>
4.672 -\<close> ML \<open> (*taken from "val problem =" below*)
4.673 -type problem_WITH_Problem =
4.674 - (((((((string * string) * string) * string) * string list) * string) *
4.675 - (((((string * string) *
4.676 - (((((((((((((((string * ((string * string) * string)) * string) * string) * string) *
4.677 - string list) * string) * string) * string list) * string) *
4.678 - string) * string) * string) * string) * string list) *
4.679 - ((string * string) *
4.680 - ((((((((string * string) * string) * string) * string) * string list) * string) *
4.681 - string) * string list)))) *
4.682 - string) * string) * string list)) *
4.683 - string)
4.684 -\<close> ML \<open>
4.685 -(* compare case parse problem toks of *)
4.686 -type problem = ((((((
4.687 - string * string) * string) * string list) * string) * (((((
4.688 - string * string) * (((((((((((((((
4.689 - string * ((string * string) * string)) * string) *
4.690 - string) * string) * string list) *
4.691 - string) * string) * string list) *
4.692 - string) * string) * string) *
4.693 - string) * string) * string list) * ((
4.694 - string * string) * ((((((((
4.695 - string * string) * string) *
4.696 - string) * string) * string list) *
4.697 - string) * string) * string list)))) *
4.698 - string) * string) *
4.699 - string list)) *
4.700 - string)
4.701 -\<close> ML \<open>
4.702 -val problem_dummy_WITH_Problem =
4.703 - ((((((("", ""), ""), ""), []: string list), ""),
4.704 - ((((("", ""),
4.705 - ((((((((((((((("", (("", ""), "")), ""), ""), ""),
4.706 - []: string list), ""), ""), []: string list), ""),
4.707 - ""), ""), ""), ""), []: string list),
4.708 - (("", ""),
4.709 - (((((((("", ""), ""), ""), ""), []: string list), ""),
4.710 - ""), []: string list)))),
4.711 - ""), ""), []: string list)),
4.712 - "");
4.713 -\<close> ML \<open>
4.714 -(* compare case parse problem toks of *)
4.715 -val problem_dummy = ((((((
4.716 - "", ""), ""), []: string list), ""), (((((
4.717 - "", ""), (((((((((((((((
4.718 - "", (("", ""), "")), ""),
4.719 - ""), ""), []: string list),
4.720 - ""), ""), []: string list),
4.721 - ""), ""), ""),
4.722 - ""), ""), []: string list), ((
4.723 - "", ""), ((((((((
4.724 - "", ""), ""),
4.725 - ""), ""), []: string list),
4.726 - ""), ""), []: string list)))),
4.727 - ""), ""),
4.728 - []: string list)),
4.729 - "")
4.730 -\<close> ML \<open>
4.731 -\<close> ML \<open> (*type cartouche_problem*)
4.732 -type cartouche_problem = string * problem_WITH_Problem;
4.733 -\<close> ML \<open>
4.734 -val cartouche_problem_dummy = ("", problem_dummy_WITH_Problem);
4.735 -\<close> ML \<open>
4.736 -\<close>
4.737 -
4.738 -subsection \<open>whole Problem\<close>
4.739 -ML \<open>
4.740 -\<close> ML \<open>
4.741 -val toks_WITH_Problem = tokenize (problem_headline_str_WITH_Problem ^ specification_str ^ solution_str);
4.742 -val toks = tokenize (problem_headline_str ^ specification_str ^ solution_str);
4.743 -\<close>
4.744 -declare [[ML_print_depth = 999]] (* ..for getting complete <Output> *)
4.745 -ML \<open>
4.746 -body
4.747 -\<close> ML \<open>
4.748 -type body = (((((string * string) *
4.749 - (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) *
4.750 - ((string * string) * ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list)))) *
4.751 - string) * string) * string list)
4.752 -\<close> ML \<open>
4.753 -val body_dummy = ((((("", ""),
4.754 - ((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []),
4.755 - (("", ""), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))),
4.756 - ""), ""), [])
4.757 -\<close> ML \<open>
4.758 -val problem_WITH_Problem =
4.759 - problem_headline_WITH_Problem --
4.760 - (Scan.optional body) body_dummy --
4.761 - (Scan.optional Parse.term) ""
4.762 -\<close> ML \<open>
4.763 -problem_WITH_Problem: problem_WITH_Problem parser
4.764 -\<close> ML \<open>
4.765 -val problem =
4.766 - problem_headline --
4.767 - (Scan.optional body) body_dummy --
4.768 - (Scan.optional Parse.term) ""
4.769 -\<close> ML \<open>
4.770 -problem: problem parser
4.771 -\<close> ML \<open>
4.772 -\<close>
4.773 -declare [[ML_print_depth = 999]] (* ..for getting complete <Output> *)
4.774 -ML \<open>
4.775 -\<close> ML \<open>
4.776 -case parse problem_WITH_Problem toks_WITH_Problem of ((((((((
4.777 - "Problem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
4.778 - "Specification", ":"), (((((((((((((((
4.779 - "Model", (("", ""), "")), ":"),
4.780 - "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.781 - "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.782 - "Find"), ":"), _(*"<markup>"*)),
4.783 - "Relate"), ":"), [_(*"<markup>"*)]), ((
4.784 - "References", ":"), ((((((((
4.785 - "RTheory", ":"), "Biegelinie"),
4.786 - "RProblem"), ":"), ["Biegelinien"]),
4.787 - "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),
4.788 - "Solution"), ":"),
4.789 - [_(*"EXEC IMMEDIATELY step_term: <markup> (, )"*),
4.790 - _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Substitute <markup> <markup>)"*),
4.791 - _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in)"*),
4.792 - _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien)"*),
4.793 - _(*"EXEC IMMEDIATELY step_term: <markup> (, )"*)])),
4.794 - ""),
4.795 -[])
4.796 - => () | _ => error "parse problem_WITH_Problem (whole) CHANGED"
4.797 -\<close> ML \<open>
4.798 -case parse problem toks of (((((((
4.799 - "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
4.800 - "Specification", ":"), (((((((((((((((
4.801 - "Model", (("", ""), "")), ":"),
4.802 - "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.803 - "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.804 - "Find"), ":"), _(*"<markup>"*)),
4.805 - "Relate"), ":"), [_(*"<markup>"*)]), ((
4.806 - "References", ":"), ((((((((
4.807 - "RTheory", ":"), "Biegelinie"),
4.808 - "RProblem"), ":"), ["Biegelinien"]),
4.809 - "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),
4.810 - "Solution"), ":"),
4.811 - [_(*"EXEC IMMEDIATELY step_term: <markup> (, )"*),
4.812 - _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Substitute <markup> <markup>)"*),
4.813 - _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in)"*),
4.814 - _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien)"*),
4.815 - _(*"EXEC IMMEDIATELY step_term: <markup> (, )"*)])),
4.816 - ""),
4.817 -[])
4.818 - => () | _ => error "parse problem (whole) CHANGED"
4.819 -\<close> ML \<open>
4.820 -parse problem toks
4.821 -\<close> ML \<open>
4.822 -(* compare case parse problem toks of *)
4.823 -type problem = ((((((
4.824 - string * string) * string) * string list) * string) * (((((
4.825 - string * string) * (((((((((((((((
4.826 - string * ((string * string) * string)) * string) *
4.827 - string) * string) * string list) *
4.828 - string) * string) * string list) *
4.829 - string) * string) * string) *
4.830 - string) * string) * string list) * ((
4.831 - string * string) * ((((((((
4.832 - string * string) * string) *
4.833 - string) * string) * string list) *
4.834 - string) * string) * string list)))) *
4.835 - string) * string) *
4.836 - string list)) *
4.837 - string)
4.838 -\<close> ML \<open>
4.839 -(* compare case parse problem toks of *)
4.840 -val problem_dummy = ((((((
4.841 - "", ""), ""), []: string list), ""), (((((
4.842 - "", ""), (((((((((((((((
4.843 - "", (("", ""), "")), ""),
4.844 - ""), ""), []: string list),
4.845 - ""), ""), []: string list),
4.846 - ""), ""), ""),
4.847 - ""), ""), []: string list), ((
4.848 - "", ""), ((((((((
4.849 - "", ""), ""),
4.850 - ""), ""), []: string list),
4.851 - ""), ""), []: string list)))),
4.852 - ""), ""),
4.853 - []: string list)),
4.854 - "")
4.855 -\<close> ML \<open>
4.856 -\<close>
4.857 -
4.858 -subsection \<open>Problem collapsed in variants\<close>
4.859 -text \<open>
4.860 - The variants of input below should be accepted by the final calc_parser "problem'.
4.861 - An occasion to improve parsers' error messages !"
4.862 -\<close>
4.863 -subsubsection \<open>start calculation: headline only\<close>
4.864 -ML \<open>
4.865 -\<close> ML \<open>
4.866 -val toks = tokenize problem_headline_str_WITH_Problem
4.867 -\<close> ML \<open>
4.868 -case problem_headline_WITH_Problem toks of
4.869 - (((((("Problem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"), [])
4.870 -=> () | _ => error "parse problem_headline_str_WITH_Problem CHANGED"
4.871 -\<close> ML \<open>
4.872 -\<close>
4.873 -
4.874 -subsubsection \<open>enter Specification\<close>
4.875 -text \<open>
4.876 - the Model only has Descriptors and the References are empty
4.877 -\<close> ML \<open>
4.878 -val toks_WITH_Problem = tokenize (
4.879 - problem_headline_str_WITH_Problem ^
4.880 - "Specification:" ^
4.881 - model_empty_str ^ (* <<<----- empty *)
4.882 - "References:" ^ (* <<<----- collapsed *)
4.883 - "Solution:"
4.884 -)
4.885 -\<close> ML \<open>
4.886 -case parse problem_WITH_Problem toks_WITH_Problem of ((((((((
4.887 - "Problem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
4.888 - "Specification", ":"), (((((((((((((((
4.889 - "Model", (("", ""), "")), ":"),
4.890 - "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.891 - "Where"), ":"), [_(*"<markup>"*)]),
4.892 - "Find"), ":"), _(*"<markup>"*)),
4.893 - "Relate"), ":"), [_(*"<markup>"*)]), ((
4.894 - "References", ":"), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))),
4.895 - "Solution"), ":"), [])),
4.896 - ""),
4.897 -[])
4.898 -=> () | _ => error "parse enter Specification WITH_Problem CHANGED"
4.899 -\<close> ML \<open>
4.900 -val toks = tokenize (
4.901 - problem_headline_str ^
4.902 - "Specification:" ^
4.903 - model_empty_str ^ (* <<<----- empty *)
4.904 - "References:" ^ (* <<<----- collapsed *)
4.905 - "Solution:"
4.906 -)
4.907 -\<close> ML \<open>
4.908 -case parse problem toks of (((((((
4.909 - "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
4.910 - "Specification", ":"), (((((((((((((((
4.911 - "Model", (("", ""), "")), ":"),
4.912 - "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.913 - "Where"), ":"), [_(*"<markup>"*)]),
4.914 - "Find"), ":"), _(*"<markup>"*)),
4.915 - "Relate"), ":"), [_(*"<markup>"*)]), ((
4.916 - "References", ":"), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))),
4.917 - "Solution"), ":"), [])),
4.918 - ""),
4.919 -[])
4.920 -=> () | _ => error "parse enter Specification CHANGED"
4.921 -\<close> ML \<open>
4.922 -\<close> ML \<open> (* this also works with Problem-headline only*)
4.923 -val toks = tokenize problem_headline_str;
4.924 -\<close> ML \<open>
4.925 -parse problem toks
4.926 -\<close> ML \<open>
4.927 -case parse problem toks of (((((((
4.928 - "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
4.929 - "", ""), (((((((((((((((
4.930 - "", (("", ""), "")), ""),
4.931 - ""), ""), []),
4.932 - ""), ""), []),
4.933 - ""), ""), ""),
4.934 - ""), ""), []), ((
4.935 - "", ""), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))),
4.936 - ""), ""), [])),
4.937 - ""),
4.938 -[])
4.939 -=> () | _ => error "parse BEFORE enter Specification CHANGED"
4.940 -\<close> ML \<open>
4.941 -\<close>
4.942 -
4.943 -subsubsection \<open>finish Specification\<close>
4.944 -ML \<open>
4.945 -\<close> ML \<open>
4.946 -val toks_WITH_Problem = tokenize (
4.947 - problem_headline_str_WITH_Problem ^
4.948 - "Specification:" ^
4.949 - model_str ^
4.950 - references_str ^
4.951 - "Solution:"
4.952 -)
4.953 -\<close> ML \<open>
4.954 -parse problem_WITH_Problem toks_WITH_Problem
4.955 -\<close> ML \<open>
4.956 -case parse problem_WITH_Problem toks_WITH_Problem of ((((((((
4.957 - "Problem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
4.958 - "Specification", ":"), (((((((((((((((
4.959 - "Model", (("", ""), "")), ":"),
4.960 - "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.961 - "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.962 - "Find"), ":"), _(*"<markup>"*)),
4.963 - "Relate"), ":"), [_(*"<markup>"*)]), ((
4.964 - "References", ":"), ((((((((
4.965 - "RTheory", ":"), "Biegelinie"),
4.966 - "RProblem"), ":"), ["Biegelinien"]),
4.967 - "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),
4.968 - "Solution"), ":"),
4.969 - [])),
4.970 - ""),
4.971 -[])
4.972 - => () | _ => error "parse finish specification CHANGED"
4.973 -\<close> ML \<open>
4.974 -val toks = tokenize (
4.975 - problem_headline_str ^
4.976 - "Specification:" ^
4.977 - model_str ^
4.978 - references_str ^
4.979 - "Solution:"
4.980 -)
4.981 -\<close> ML \<open>
4.982 -case parse problem toks of ( ((((((
4.983 - "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
4.984 - "Specification", ":"), (((((((((((((((
4.985 - "Model", (("", ""), "")), ":"),
4.986 - "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.987 - "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
4.988 - "Find"), ":"), _(*"<markup>"*)),
4.989 - "Relate"), ":"), [_(*"<markup>"*)]), ((
4.990 - "References", ":"), ((((((((
4.991 - "RTheory", ":"), "Biegelinie"),
4.992 - "RProblem"), ":"), ["Biegelinien"]),
4.993 - "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),
4.994 - "Solution"), ":"),
4.995 - [])),
4.996 - ""),
4.997 - [])
4.998 - => () | _ => error "parse finish specification CHANGED"
4.999 -\<close> ML \<open>
4.1000 -(*
4.1001 - val read_out_problem: problem -> P_Spec.record
4.1002 -*)
4.1003 -fun read_out_problem ((((((
4.1004 - "(", thy_id), ","), pbl_id), ")"), (((((
4.1005 - "Specification", ":"), (((((((((((((((
4.1006 - "Model", (("", ""), "")), ":"),
4.1007 - "Given"), ":"), givens),
4.1008 - "Where"), ":"), wheres),
4.1009 - "Find"), ":"), find),
4.1010 - "Relate"), ":"), relates), ((
4.1011 - "References", ":"), ((((((((
4.1012 - "RTheory", ":"), rthy_id),
4.1013 - "RProblem"), ":"), rpbl_id),
4.1014 - "RMethod"), ":"), rmet_id)))),
4.1015 - "Solution"), ":"),
4.1016 - [])),
4.1017 - "") =
4.1018 - {thy_id = thy_id, pbl_id = pbl_id,
4.1019 - givens = givens, wheres = wheres, find = find, relates = relates,
4.1020 - rthy_id = rthy_id, rpbl_id = rpbl_id, rmet_id = rmet_id}
4.1021 - | read_out_problem arg =
4.1022 - (@{print} {a = "read_out_problem called with", arg = arg};
4.1023 - raise ERROR "read_out_problem called with")
4.1024 -\<close> ML \<open>
4.1025 -(*P_Spec.record*)
4.1026 -type record = {thy_id: string, pbl_id: string list, (* headline of Problem *)
4.1027 - givens: string list, wheres: string list, (* Model.T *)
4.1028 - find: string, relates: string list,
4.1029 - rthy_id: string, rpbl_id: string list, rmet_id: string list} (* References.T *)
4.1030 -\<close> ML \<open>
4.1031 -read_out_problem: problem -> record
4.1032 -\<close> ML \<open>
4.1033 -case parse problem toks |> fst |> read_out_problem of
4.1034 - {thy_id = "Biegelinie", pbl_id = ["Biegelinien"],
4.1035 - givens = [_(*"<markup>"*), _(*"<markup>"*)], wheres = [_(*"<markup>"*), _(*"<markup>"*)],
4.1036 - find = _(*"<markup>"*), relates = [_(*"<markup>"*)],
4.1037 - rthy_id = "Biegelinie", rpbl_id = ["Biegelinien"], rmet_id = ["Integrieren", "KonstanteBestimmen2"]
4.1038 - } => ()
4.1039 -| _ => error "read_out_problem CHANGED"
4.1040 -\<close> ML \<open>
4.1041 -\<close>
4.1042 -
4.1043 -subsubsection \<open>enter Solution\<close>
4.1044 -text \<open>
4.1045 - Specification collapsed or expanded
4.1046 -\<close> ML \<open>
4.1047 -\<close> ML \<open> val str = (problem_headline_str_WITH_Problem ^ " Specification: Solution:")
4.1048 -\<close> ML \<open>
4.1049 -if str = "Problem ( \"Biegelinie\" , [\"Biegelinien\"] ) Specification: Solution:"
4.1050 -then () else error "Specification collapsed, Solution CHANGED"
4.1051 -\<close> ML \<open>
4.1052 -val toks1_WITH_Problem = tokenize str
4.1053 -\<close> ML \<open>
4.1054 -parse problem_WITH_Problem toks1_WITH_Problem
4.1055 -\<close> ML \<open>
4.1056 -case parse problem_WITH_Problem toks1_WITH_Problem of ((((((((
4.1057 - "Problem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
4.1058 - "Specification", ":"), ((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))),
4.1059 - "Solution"), ":"), [])),
4.1060 - ""),
4.1061 -[])
4.1062 - => () | _ => error "parse Specification collapsed CHANGED"
4.1063 -\<close> ML \<open>
4.1064 -\<close>
4.1065 -
4.1066 -subsubsection \<open>Problem with final_result, collapsed\<close>
4.1067 -ML \<open>
4.1068 -\<close> ML \<open>
4.1069 -val str = (problem_headline_str_WITH_Problem ^ final_result_str)
4.1070 -\<close> ML \<open>
4.1071 -val toks_WITH_Problem = tokenize str
4.1072 -\<close> ML \<open>
4.1073 -parse problem_WITH_Problem toks_WITH_Problem
4.1074 -\<close> ML \<open>
4.1075 -case parse problem_WITH_Problem toks_WITH_Problem of ((((((((
4.1076 - "Problem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"),
4.1077 - ((((("", ""),
4.1078 - ((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []),
4.1079 - (("", ""), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))),
4.1080 - ""), ""), [])),
4.1081 - _(*"<markup>"*)),
4.1082 -[])
4.1083 - => () | _ => error "parse Problem with final_result, collapsed CHANGED"
4.1084 -\<close> ML \<open>
4.1085 -\<close>
4.1086 -
4.1087 -subsection \<open>Problem .. Solution recursively\<close>
4.1088 -subsubsection \<open>towards recursion\<close>
4.1089 +section \<open>towards recursion\<close>
4.1090 text \<open>
4.1091 we make steps close to recursive version according to subsequent subsubsection.
4.1092 \<close> ML \<open>
4.1093 @@ -1151,10 +193,10 @@
4.1094 problem_nonrec_WITH_Problem parser
4.1095 (* ^^^^^^^*)
4.1096 \<close> ML \<open>
4.1097 -parse problem_nonrec_WITH_Problem toks_WITH_Problem
4.1098 +ParseC.parse problem_nonrec_WITH_Problem toks_WITH_Problem
4.1099 \<close> ML \<open>
4.1100 -case parse problem_nonrec_WITH_Problem toks_WITH_Problem of ((((((((((
4.1101 - "Problem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"),
4.1102 +case ParseC.parse problem_nonrec_WITH_Problem toks_WITH_Problem of ((((((((((
4.1103 + "OLDProblem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"),
4.1104 ((
4.1105 "Specification", ":"),
4.1106 ((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""), (((((((("", ""), ""), ""), ""), []), ""), ""), []))))),
4.1107 @@ -1169,12 +211,12 @@
4.1108 \<close> ML \<open>
4.1109 \<close>
4.1110
4.1111 -subsubsection \<open>problem_mini\<close>
4.1112 +section \<open>problem_mini\<close>
4.1113 text \<open>
4.1114 we make a minimal problem in order to investigate types
4.1115 of the parser's components
4.1116 \<close> ML \<open>
4.1117 -val problem_headline_mini = Parse.$$$ "Problem"
4.1118 +val problem_headline_mini = Parse.$$$ "OLDProblem"
4.1119 \<close> ML \<open>
4.1120 val specification_mini = Parse.$$$ "Specification"
4.1121 \<close> ML \<open>
4.1122 @@ -1191,8 +233,8 @@
4.1123 and steps_mini _ =
4.1124 Parse.name >> exec_name || Parse.int >> exec_int
4.1125 \<close> ML \<open>
4.1126 -(problem_mini "") (tokenize "Problem Specification aaa")
4.1127 -(* = ((("Problem", "Specification"), "EXEC IMMEDIATELY exec_name: aaa"), [])*)
4.1128 +(problem_mini "") (tokenize "OLDProblem Specification aaa")
4.1129 +(* = ((("OLDProblem", "Specification"), "EXEC IMMEDIATELY exec_name: aaa"), [])*)
4.1130 \<close> ML \<open>
4.1131 problem_mini: 'a -> Token.T list -> ((string * string) * string) * Token.T list
4.1132 \<close> ML \<open>
4.1133 @@ -1214,10 +256,10 @@
4.1134 problem_mini: ((string * string) * string list) parser;
4.1135 steps_mini : string list parser;
4.1136 \<close> ML \<open>
4.1137 -problem_mini (tokenize "Problem Specification aaa")
4.1138 -(* = ((("Problem", "Specification"), ["EXEC IMMEDIATELY exec_name: aaa"]), [])*)
4.1139 +problem_mini (tokenize "OLDProblem Specification aaa")
4.1140 +(* = ((("OLDProblem", "Specification"), ["EXEC IMMEDIATELY exec_name: aaa"]), [])*)
4.1141 \<close> text \<open> ERROR ?!?!?
4.1142 -parse problem_mini (tokenize "Problem Specification Problem Specification")
4.1143 +parse problem_mini (tokenize "OLDProblem Specification OLDProblem Specification")
4.1144 exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")
4.1145 \<close> ML \<open>
4.1146 \<close> ML \<open>
4.1147 @@ -1235,18 +277,18 @@
4.1148 ((writeln ("name " ^ string_of_toks toks); Parse.name >> exec_name) (**)||
4.1149 (writeln ("sub-problem " ^ string_of_toks toks); problem_mini >> exec_problem_mini)(**))) toks
4.1150 \<close> text \<open>
4.1151 -problem_mini (tokenize "Problem Specification")
4.1152 +problem_mini (tokenize "OLDProblem Specification")
4.1153 (*
4.1154 -problem_mini Problem, Specification
4.1155 -steps_mini Problem, Specification
4.1156 +problem_mini OLDProblem, Specification
4.1157 +steps_mini OLDProblem, Specification
4.1158 name
4.1159 sub-problem
4.1160 exception MORE () raised (line 159 of "General/scan.ML")*)
4.1161 \<close> text \<open>
4.1162 -problem_mini (tokenize "Problem Specification aaa")
4.1163 +problem_mini (tokenize "OLDProblem Specification aaa")
4.1164 (*
4.1165 -problem_mini Problem, Specification, aaa
4.1166 -steps_mini Problem, Specification, aaa
4.1167 +problem_mini OLDProblem, Specification, aaa
4.1168 +steps_mini OLDProblem, Specification, aaa
4.1169 name aaa
4.1170 sub-problem aaa
4.1171 exception MORE () raised (line 159 of "General/scan.ML")
4.1172 @@ -1260,7 +302,7 @@
4.1173 \<close> ML \<open>
4.1174 \<close>
4.1175
4.1176 -subsubsection \<open>trials on recursion stopped\<close>
4.1177 +section \<open>trials on recursion stopped\<close>
4.1178 text \<open>
4.1179 Trials on recursion have been postponed after parsing from cartouche
4.1180 (or even ?after executing Specification?).
4.1181 @@ -1357,80 +399,4 @@
4.1182 \<close> ML \<open>
4.1183 \<close>
4.1184
4.1185 -chapter \<open>command_keyword ISAC, avoid error at end\<close>
4.1186 -ML \<open> (*original Outer_Syntax.command with trials to adapt with problem parser*)
4.1187 -val _ =
4.1188 - Outer_Syntax.command @{command_keyword ISAC} "embedded ISAC language"
4.1189 - (
4.1190 - (Parse.input ((**)Parse.cartouche (** )-- (** ) ParseC.( **)problem ( **)))
4.1191 - >> (* try variants ^^^^^^^^^^^^^^^ ^^ ^^^^^^^*)
4.1192 - (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input)))
4.1193 - )
4.1194 -\<close>
4.1195 -
4.1196 -chapter \<open>Parser for exp_file.str\<close>
4.1197 -ML \<open>
4.1198 -\<close> ML \<open>
4.1199 -val form_single =
4.1200 - Parse.$$$ "(" --
4.1201 - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Formalise.model *) --
4.1202 - Parse.$$$ "," --
4.1203 - Parse.$$$ "(" (* begin Formalise.spec *) --
4.1204 - Parse.string -- (* ThyC.id, still not qualified *)
4.1205 - Parse.$$$ "," --
4.1206 - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Problem.id *) --
4.1207 - Parse.$$$ "," --
4.1208 - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Method.id *) --
4.1209 - Parse.$$$ ")" (* end Formalise.spec *) --
4.1210 - Parse.$$$ ")"
4.1211 -\<close> ML \<open>
4.1212 -val form_single_str = (
4.1213 - "( " ^
4.1214 - " [\"Traegerlaenge L\", \"Streckenlast q_0\", \"Biegelinie y\", " ^
4.1215 - " \"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]\", " ^
4.1216 - " \"FunktionsVariable x\", \"GleichungsVariablen [c, c_2, c_3, c_4]\", " ^
4.1217 - " \"AbleitungBiegelinie dy\"], " ^
4.1218 - " (\"Biegelinie\", [\"Biegelinien\"], [\"IntegrierenUndKonstanteBestimmen2\"])" ^
4.1219 - ")")
4.1220 -\<close> ML \<open>
4.1221 -val toks = tokenize form_single_str
4.1222 -\<close> ML \<open>
4.1223 -case parse form_single toks of
4.1224 -(((((((((((
4.1225 -"(",
4.1226 - ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
4.1227 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
4.1228 - "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
4.1229 - "AbleitungBiegelinie dy"]),
4.1230 -","),
4.1231 - "("),
4.1232 - "Biegelinie"), ","), ["Biegelinien"]), ","), ["IntegrierenUndKonstanteBestimmen2"]),
4.1233 - ")"),
4.1234 -")"), []) => () | _ => error "parse form_single toks CHANGED"
4.1235 -\<close> ML \<open>
4.1236 -val formalise = (Parse.$$$ "[" |-- Parse.list1 form_single --| Parse.$$$ "]")
4.1237 -\<close> ML \<open>
4.1238 -type formalise =
4.1239 - ((((((((((string * string list) * string) * string) * string) * string) * string list) *
4.1240 - string) * string list) * string) * string) list
4.1241 -\<close> ML \<open>
4.1242 -\<close> ML \<open>
4.1243 -val toks = tokenize ("[" ^ form_single_str ^ "]")
4.1244 -\<close> ML \<open>
4.1245 -parse formalise (tokenize ("[" ^ form_single_str ^ "]"));
4.1246 -\<close> ML \<open>
4.1247 -parse formalise (tokenize ("[" ^ form_single_str ^ "," ^ form_single_str ^ "]"));
4.1248 -\<close> text \<open> exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")..
4.1249 -parse formalise (tokenize ("[" ^ "]"));
4.1250 -\<close> ML \<open>
4.1251 - formalise: formalise parser;
4.1252 - formalise: Token.T list -> formalise * Token.T list
4.1253 -\<close> text \<open> TODO:
4.1254 - formalise: (string * Position.T) list -> formalise * (string * Position.T) list
4.1255 -\<close> ML \<open>
4.1256 -\<close> ML \<open>
4.1257 -\<close>
4.1258 -
4.1259 -
4.1260 -
4.1261 end
5.1 --- a/test/Tools/isac/BridgeJEdit/parseC.sml Sun Jan 17 15:25:27 2021 +0100
5.2 +++ b/test/Tools/isac/BridgeJEdit/parseC.sml Fri Jan 22 11:27:47 2021 +0100
5.3 @@ -6,7 +6,513 @@
5.4 "-----------------------------------------------------------------------------------------------";
5.5 "table of contents -----------------------------------------------------------------------------";
5.6 "-----------------------------------------------------------------------------------------------";
5.7 -"----------- SEE test/Pure/Isar/Test_Parse_Isac.thy --------------------------------------------";
5.8 +"----------- Problem headline ------------------------------------------------------------------";
5.9 +"----------- Model -----------------------------------------------------------------------------";
5.10 +"----------- References ------------------------------------------------------------------------";
5.11 +"----------- Specification: References + Model -------------------------------------------------";
5.12 +"----------- Tactics ---------------------------------------------------------------------------";
5.13 +"----------- steps -----------------------------------------------------------------------------";
5.14 +"----------- body ------------------------------------------------------------------------------";
5.15 +"----------- Problem ---------------------------------------------------------------------------";
5.16 +"----------- fun read_out_problem --------------------------------------------------------------";
5.17 +"----------- THERE ARE TESTS with INCOMPLETE WORK IN Test_Parse_Isac.thy -----------------------";
5.18 +"----------- parser for exp_file.str -----------------------------------------------------------";
5.19 "-----------------------------------------------------------------------------------------------";
5.20 "-----------------------------------------------------------------------------------------------";
5.21 "-----------------------------------------------------------------------------------------------";
5.22 +
5.23 +Thy_Header.get_keywords' @{context};
5.24 +(*
5.25 + Keywords
5.26 + {commands =
5.27 + {(".",
5.28 + {files = [], id = 39558, kind = "qed", pos =
5.29 + {line=71, offset=3218, end_offset=3219, file=~~/src/Pure/Pure.thy}, tags = ["proof"]}),
5.30 +:
5.31 + minor =
5.32 + {"!", "!!", "%", "(", ")", "+", ",", ":", "::", ";", "<", "<=", "=", "==", "=>", "?", "Find",
5.33 + "Given", "Model", "Problem", "RMethod", "RProblem", "RTheory", "References", "Relate",
5.34 +:
5.35 +*)
5.36 +
5.37 +"----------- Problem headline ------------------------------------------------------------------";
5.38 +"----------- Problem headline ------------------------------------------------------------------";
5.39 +"----------- Problem headline ------------------------------------------------------------------";
5.40 +val problem_headline_str =
5.41 + "( \"Biegelinie\" , [\"Biegelinien\"] )";
5.42 +
5.43 +val toks = ParseC.tokenize problem_headline_str;
5.44 +case ParseC.problem_headline toks of
5.45 + ((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"), [])
5.46 + => () | _ => error "parse problem_headline CHANGED"
5.47 +
5.48 +
5.49 +"----------- Model -----------------------------------------------------------------------------";
5.50 +"----------- Model -----------------------------------------------------------------------------";
5.51 +"----------- Model -----------------------------------------------------------------------------";
5.52 +val model_str = (
5.53 + "Model:" ^
5.54 + (*^^^^^^^^^^^^*)
5.55 + "Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^
5.56 + "Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^
5.57 + "Find: \"Biegelinie y\"" ^
5.58 + "Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\""
5.59 + );
5.60 +val model_empty_str = ( (*Model before student's input"*)
5.61 + "Model:" ^
5.62 + (*^^^^^^^^^^^^*)
5.63 + "Given: \"Traegerlaenge \", \"Streckenlast \"" ^
5.64 + "Where: \"_ ist_integrierbar_auf {| |}\"" ^
5.65 + "Find: \"Biegelinie \"" ^
5.66 + "Relate: \"Randbedingungen [ ]\""
5.67 + );
5.68 +val model_str_opt = ( (*Model explicitly referring to RProblem (default), not RMethod*)
5.69 + "Model ( RProblem ):" ^
5.70 + (*^^^^^^^^^^^^*)
5.71 + "Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^
5.72 + "Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^
5.73 + "Find: \"Biegelinie y\"" ^
5.74 + "Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\""
5.75 + );
5.76 +
5.77 +val toks = ParseC.tokenize model_str;
5.78 +case ParseC.parse ParseC.model toks of
5.79 +(((((((((((((((
5.80 + "Model", (("", ""), "")), ":"),
5.81 + "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.82 + "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.83 + "Find"), ":"), _(*"<markup>"*)),
5.84 + "Relate"), ":"), [_(*"<markup>"*)]), [])
5.85 +=> () | _ => error "parse model CHANGED";
5.86 +
5.87 +"----------- Model before student's input";
5.88 +val toks = ParseC.tokenize model_empty_str;
5.89 +case ParseC.parse ParseC.model toks of
5.90 +(((((((((((((((
5.91 + "Model", (("", ""), "")), ":"),
5.92 + "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.93 + "Where"), ":"), [_(*"<markup>"*) (*//, _(*"<markup>"*) //*)]),
5.94 + "Find"), ":"), _(*"<markup>"*)),
5.95 + "Relate"), ":"), [_(*"<markup>"*)]), [])
5.96 +=> () | _ => error "parse model_empty_str CHANGED";
5.97 +
5.98 +"----------- Model explicitly referring to RProblem (default), not RMethod";
5.99 +val toks = ParseC.tokenize model_str_opt;
5.100 +case ParseC.parse ParseC.model toks of
5.101 +(((((((((((((((
5.102 + "Model", (("(", "RProblem"), ")")), ":"),
5.103 + "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.104 + "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.105 + "Find"), ":"), _(*"<markup>"*)),
5.106 + "Relate"), ":"), [_(*"<markup>"*)]), [])
5.107 +=> () | _ => error "parse model_str_opt CHANGED";
5.108 +
5.109 +
5.110 +"----------- References ------------------------------------------------------------------------";
5.111 +"----------- References ------------------------------------------------------------------------";
5.112 +"----------- References ------------------------------------------------------------------------";
5.113 +val references_collapsed_str = (
5.114 + "References:"
5.115 + );
5.116 +val references_str = (
5.117 + "References:" ^
5.118 + "RTheory: \"Biegelinie\"" ^
5.119 + "RProblem: [\"Biegelinien\"]" ^
5.120 + "RMethod: [\"Integrieren\", \"KonstanteBestimmen2\"]"
5.121 + );
5.122 +val references_empty_str = (
5.123 + "References:" ^
5.124 + "RTheory: \"\"" ^
5.125 + "RProblem: [\"\"]" ^
5.126 + "RMethod: [\"\"]"
5.127 + );
5.128 +
5.129 +case ParseC.parse ParseC.references (ParseC.tokenize references_collapsed_str) of
5.130 + ((("References", ":"), (((((((("", ""), ""), ""), ""), []), ""), ""), [])), [])
5.131 + => () | _ => error "parse references_collapsed CHANGED";
5.132 +
5.133 +case ParseC.parse ParseC.references (ParseC.tokenize references_str) of (((
5.134 + "References", ":"),
5.135 + ((((((((
5.136 + "RTheory", ":"), "Biegelinie"),
5.137 + "RProblem"), ":"), ["Biegelinien"]),
5.138 + "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])),
5.139 + [])
5.140 + => () | _ => error "parse references CHANGED";
5.141 +
5.142 +case ParseC.parse ParseC.references (ParseC.tokenize references_empty_str) of (((
5.143 + "References", ":"), ((((((((
5.144 + "RTheory", ":"), ""),
5.145 + "RProblem"), ":"), [""]),
5.146 + "RMethod"), ":"), [""])),
5.147 + [])
5.148 + => () | _ => error "parse references_empty_str CHANGED"
5.149 +
5.150 +
5.151 +"----------- Specification: References + Model -------------------------------------------------";
5.152 +"----------- Specification: References + Model -------------------------------------------------";
5.153 +"----------- Specification: References + Model -------------------------------------------------";
5.154 +val specification_str = (
5.155 + "Specification:" ^
5.156 + model_str ^
5.157 + references_str
5.158 + );
5.159 +val specification_collapsed_str = (
5.160 +" Specification:" (** ) ^
5.161 +" Model:"^
5.162 +" Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^
5.163 +" Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^
5.164 +" Find: \"Biegelinie y\"" ^
5.165 +" Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\"" ^
5.166 +" References:" (**) ^
5.167 +" RTheory: \"Biegelinie\"" (**) ^
5.168 +" RProblem: [\"Biegelinien\"]" (**) ^
5.169 +" RMethod: [\"Integrieren\", \"KonstanteBestimmen2\"]" ( **)
5.170 +);
5.171 +
5.172 +case ParseC.specification (ParseC.tokenize specification_str) of (((
5.173 + "Specification", ":"),
5.174 + (((((((((((((((
5.175 + "Model", (("", ""), "")), ":"),
5.176 + "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.177 + "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.178 + "Find"), ":"), _(*"<markup>"*)),
5.179 + "Relate"), ":"), [_(*"<markup>"*)]),
5.180 + ((
5.181 + "References", ":"), ((((((((
5.182 + "RTheory", ":"), "Biegelinie"),
5.183 + "RProblem"), ":"), ["Biegelinien"]),
5.184 + "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),
5.185 + [])
5.186 + => () | _ => error "parse specification (expanded) changed";
5.187 +
5.188 +"----------- Specification collapsed";
5.189 +case ParseC.parse ParseC.specification (ParseC.tokenize specification_collapsed_str) of (((
5.190 + "Specification", ":"),
5.191 +(*model*)((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""),
5.192 +(*refs?*)(((((((("", ""), ""), ""), ""), []), ""), ""), [])))),
5.193 + [])
5.194 + => () | _ => error "parse specification (collapsed) changed";
5.195 +
5.196 +
5.197 +"----------- Tactics ---------------------------------------------------------------------------";
5.198 +"----------- Tactics ---------------------------------------------------------------------------";
5.199 +"----------- Tactics ---------------------------------------------------------------------------";
5.200 +val tactic_Substitute_str =
5.201 + "Tactic Substitute \"c_4 + c_3 * x + 1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\"";
5.202 +val tactic_Rewrite_Set_Inst_str =
5.203 + "Tactic Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\"";
5.204 +val tactic_Check_Postcond_str =
5.205 + "Tactic Check_Postcond [\"Biegelinien\", \"xxx\"]";
5.206 +val final_result_str = "\"y x = -6 * q_0 * L ^ 2 / (-24 * EI)\"";
5.207 +
5.208 +val toks1 = ParseC.tokenize "Substitute \"c_4 + c_3 * x + 1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\"";
5.209 +case ParseC.substitute toks1 of ((("Substitute", _(*<markup>*)), _(*<markup>*)), [])
5.210 +=> () | _ => error "parse Substitute CHANGED";
5.211 +
5.212 +val toks2 = ParseC.tokenize "Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\"";
5.213 +case ParseC.rewrite_set_inst toks2 of
5.214 + ((("Rewrite_Set_Inst", _(*<markup>*)), "make_ratpoly_in"), [])
5.215 +=> () | _ => error "parse Rewrite_Set_Inst CHANGED";
5.216 +
5.217 +val toks3 = ParseC.tokenize "Check_Postcond [\"Biegelinien\", \"xxx\"]";
5.218 +case ParseC.check_postcond toks3 of (("Check_Postcond", ["Biegelinien", "xxx"]), [])
5.219 +=> () | _ => error "parse Check_Postcond CHANGED";
5.220 +
5.221 +"----------- Tactics collected";
5.222 +val toks1' = ParseC.tokenize tactic_Substitute_str;
5.223 +val toks2' = ParseC.tokenize tactic_Rewrite_Set_Inst_str;
5.224 +val toks3' = ParseC.tokenize tactic_Check_Postcond_str;
5.225 +
5.226 +ParseC.parse ParseC.tactic toks1'; (* = (("Tactic", "EXEC IMMEDIATELY: Substitute <markup> <markup>"), [])*)
5.227 +ParseC.parse ParseC.tactic toks2'; (* = (("Tactic", "EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in"), [])*)
5.228 +ParseC.parse ParseC.tactic toks3'; (* = (("Tactic", "EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien"), [])*)
5.229 +
5.230 +case ParseC.parse ParseC.tactic (ParseC.tokenize tactic_Substitute_str) of
5.231 + (("Tactic", _(*"EXEC IMMEDIATELY: Substitute <markup> <markup>"*)), [])
5.232 +=> () | _ => error "parse Tactic Substitute CHANGED";
5.233 +
5.234 +
5.235 +"----------- steps -----------------------------------------------------------------------------";
5.236 +"----------- steps -----------------------------------------------------------------------------";
5.237 +"----------- steps -----------------------------------------------------------------------------";
5.238 +val steps_1_str = "\"[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]\"";
5.239 +val steps_term_tac_str = (
5.240 + final_result_str ^
5.241 + " Tactic Check_Postcond [\"Biegelinien\"]"
5.242 + );
5.243 +val steps_nonrec_str = (
5.244 + "\"[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]\"" (**) ^
5.245 + "\"y x = c_4 + c_3 * x + 1 / (-1 * EI)\"" (**) ^
5.246 + tactic_Substitute_str ^
5.247 + "\"y x = 0 + 0 * x + 1 / (-1 * EI)\"" (**) ^
5.248 + tactic_Rewrite_Set_Inst_str ^
5.249 + final_result_str (**) ^
5.250 + tactic_Check_Postcond_str ^
5.251 + final_result_str (**)
5.252 +);
5.253 +
5.254 +val toks1 = ParseC.tokenize steps_1_str;
5.255 +val toks2 = ParseC.tokenize steps_term_tac_str;
5.256 +val toks3 = ParseC.tokenize steps_nonrec_str;
5.257 +
5.258 +"----------- simple version";
5.259 +ParseC.parse ParseC.steps []; (* = ([], []): (string * (string * string)) list * Token.T list *)
5.260 +ParseC.parse ParseC.steps toks1; (* = ([("<markup>", ("", ""))], [])*)
5.261 +ParseC.parse ParseC.steps toks2; (* = ([("<markup>", ("Tactic", "EXEC IMMEDIATELY: Check_Postcond Biegelinien"))], [])*)
5.262 +ParseC.parse ParseC.steps toks3;
5.263 +
5.264 +case ParseC.parse ParseC.steps toks3 of
5.265 + ([(_(*"<markup>"*), ("", "")),
5.266 + (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Substitute <markup> <markup>"*))),
5.267 + (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in"*))),
5.268 + (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Check_Postcond Biegelinien"*))),
5.269 + (_(*"<markup>"*), ("", ""))],
5.270 + [])
5.271 +=> () | _ => error "parse steps, simple version, CHANGED";
5.272 +
5.273 +"----------- version preparing subproblems";
5.274 +case ParseC.parse ParseC.steps_subpbl toks3 of
5.275 + ([_(*"EXEC IMMEDIATELY step_term: <markup> (, )"*),
5.276 + _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Substitute <markup> <markup>)"*),
5.277 + _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in)"*),
5.278 + _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien)"*),
5.279 + _(*"EXEC IMMEDIATELY step_term: <markup> (, )"*)],
5.280 + [])
5.281 +=> () | _ => error "parse steps, with exec_step_term, CHANGED";
5.282 +
5.283 +
5.284 +"----------- body ------------------------------------------------------------------------------";
5.285 +"----------- body ------------------------------------------------------------------------------";
5.286 +"----------- body ------------------------------------------------------------------------------";
5.287 +val solution_str = (
5.288 + "Solution:" ^
5.289 + steps_nonrec_str
5.290 + );
5.291 +val body_str = specification_str ^ solution_str;
5.292 +
5.293 +case ParseC.parse ParseC.body (ParseC.tokenize body_str) of ((((((
5.294 + "Specification", ":"), (((((((((((((((
5.295 + "Model", (("", ""), "")), ":"),
5.296 + "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.297 + "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.298 + "Find"), ":"), _(*"<markup>"*)),
5.299 + "Relate"), ":"), [_(*"<markup>"*)]), ((
5.300 + "References", ":"), ((((((((
5.301 + "RTheory", ":"), "Biegelinie"),
5.302 + "RProblem"), ":"), ["Biegelinien"]),
5.303 + "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),
5.304 + "Solution"), ":"),
5.305 + [_(*"EXEC IMMEDIATELY step_term: <markup> (, )"*),
5.306 + _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Substitute <markup> <markup>)"*),
5.307 + _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in)"*),
5.308 + _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien)"*),
5.309 + _(*"EXEC IMMEDIATELY step_term: <markup> (, )"*)]),
5.310 + [])
5.311 +=> () | _ => error "parse body CHANGED";
5.312 +
5.313 +
5.314 +"----------- Problem ---------------------------------------------------------------------------";
5.315 +"----------- Problem ---------------------------------------------------------------------------";
5.316 +"----------- Problem ---------------------------------------------------------------------------";
5.317 +"----------- whole Problem";
5.318 +val toks = ParseC.tokenize (problem_headline_str ^ specification_str ^ solution_str);
5.319 +
5.320 +case ParseC.parse ParseC.problem toks of (((((((
5.321 + "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
5.322 + "Specification", ":"), (((((((((((((((
5.323 + "Model", (("", ""), "")), ":"),
5.324 + "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.325 + "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.326 + "Find"), ":"), _(*"<markup>"*)),
5.327 + "Relate"), ":"), [_(*"<markup>"*)]), ((
5.328 + "References", ":"), ((((((((
5.329 + "RTheory", ":"), "Biegelinie"),
5.330 + "RProblem"), ":"), ["Biegelinien"]),
5.331 + "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),
5.332 + "Solution"), ":"),
5.333 + [_(*"EXEC IMMEDIATELY step_term: <markup> (, )"*),
5.334 + _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Substitute <markup> <markup>)"*),
5.335 + _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in)"*),
5.336 + _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien)"*),
5.337 + _(*"EXEC IMMEDIATELY step_term: <markup> (, )"*)])),
5.338 + ""),
5.339 +[])
5.340 + => () | _ => error "parse problem (whole) CHANGED"
5.341 +
5.342 +"----------- enter Specification";
5.343 +val toks = ParseC.tokenize (
5.344 + problem_headline_str ^
5.345 + "Specification:" ^
5.346 + model_empty_str ^ (* <<<----- empty *)
5.347 + "References:" ^ (* <<<----- collapsed *)
5.348 + "Solution:"
5.349 + );
5.350 +case ParseC.parse ParseC.problem toks of (((((((
5.351 + "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
5.352 + "Specification", ":"), (((((((((((((((
5.353 + "Model", (("", ""), "")), ":"),
5.354 + "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.355 + "Where"), ":"), [_(*"<markup>"*)]),
5.356 + "Find"), ":"), _(*"<markup>"*)),
5.357 + "Relate"), ":"), [_(*"<markup>"*)]), ((
5.358 + "References", ":"), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))),
5.359 + "Solution"), ":"), [])),
5.360 + ""),
5.361 +[])
5.362 +=> () | _ => error "parse enter Specification CHANGED"
5.363 +
5.364 +"----------- Problem-headline only";
5.365 +val toks = ParseC.tokenize problem_headline_str;
5.366 +
5.367 +case ParseC.parse ParseC.problem toks of (((((((
5.368 + "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
5.369 + "", ""), (((((((((((((((
5.370 + "", (("", ""), "")), ""),
5.371 + ""), ""), []),
5.372 + ""), ""), []),
5.373 + ""), ""), ""),
5.374 + ""), ""), []), ((
5.375 + "", ""), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))),
5.376 + ""), ""), [])),
5.377 + ""),
5.378 +[])
5.379 +=> () | _ => error "parse BEFORE enter Specification CHANGED"
5.380 +
5.381 +"----------- finish Specification";
5.382 +val toks = ParseC.tokenize (
5.383 + problem_headline_str ^
5.384 + "Specification:" ^
5.385 + model_str ^
5.386 + references_str ^
5.387 + "Solution:"
5.388 + );
5.389 +case ParseC.parse ParseC.problem toks of ( ((((((
5.390 + "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
5.391 + "Specification", ":"), (((((((((((((((
5.392 + "Model", (("", ""), "")), ":"),
5.393 + "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.394 + "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
5.395 + "Find"), ":"), _(*"<markup>"*)),
5.396 + "Relate"), ":"), [_(*"<markup>"*)]), ((
5.397 + "References", ":"), ((((((((
5.398 + "RTheory", ":"), "Biegelinie"),
5.399 + "RProblem"), ":"), ["Biegelinien"]),
5.400 + "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))),
5.401 + "Solution"), ":"),
5.402 + [])),
5.403 + ""),
5.404 +[])
5.405 +=> () | _ => error "parse finish specification CHANGED"
5.406 +
5.407 +"----------- Specification collapsed";
5.408 +case ParseC.parse ParseC.problem (ParseC.tokenize problem_headline_str) of (((((((
5.409 + "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
5.410 + (*Specification*)"", ""), (((((((((((((((
5.411 + (*Model*)"", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""), ((((((((
5.412 + (*References*)"", ""), ""), ""), ""), []), ""), ""), [])))),
5.413 + (*Solution*)""), ""),
5.414 + [])),
5.415 + ""),
5.416 +[])
5.417 +=> () | _ => error "parse Specification collapsed CHANGED"
5.418 +
5.419 +"----------- Problem with final_result, all collapsed";
5.420 +val toks = ParseC.tokenize (problem_headline_str ^ final_result_str);
5.421 +case ParseC.parse ParseC.problem toks of (((((((
5.422 + "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
5.423 + (*Specification*)"", ""), (((((((((((((((
5.424 + (*Model*)"", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""), ((((((((
5.425 + (*References*)"", ""), ""), ""), ""), []), ""), ""), [])))),
5.426 + (*Solution*)""), ""),
5.427 + [])),
5.428 + _(*"<markup>"*)),
5.429 +[])
5.430 +=> () | _ => error "parse Problem with final_result, all collapsed CHANGED"
5.431 +
5.432 +
5.433 +"----------- fun read_out_problem --------------------------------------------------------------";
5.434 +"----------- fun read_out_problem --------------------------------------------------------------";
5.435 +"----------- fun read_out_problem --------------------------------------------------------------";
5.436 +val toks = ParseC.tokenize (
5.437 + problem_headline_str ^
5.438 + "Specification:" ^
5.439 + model_str ^
5.440 + references_str ^
5.441 + "Solution:"
5.442 + );
5.443 +case ParseC.parse ParseC.problem toks |> fst |> ParseC.read_out_problem of
5.444 + {thy_id = "Biegelinie", pbl_id = ["Biegelinien"],
5.445 + givens = [_(*"<markup>"*), _(*"<markup>"*)], wheres = [_(*"<markup>"*), _(*"<markup>"*)],
5.446 + find = _(*"<markup>"*), relates = [_(*"<markup>"*)],
5.447 + rthy_id = "Biegelinie", rpbl_id = ["Biegelinien"], rmet_id = ["Integrieren", "KonstanteBestimmen2"]
5.448 + } => ()
5.449 +| _ => error "read_out_problem CHANGED"
5.450 +
5.451 +
5.452 +"----------- THERE ARE TESTS with INCOMPLETE WORK IN Test_Parse_Isac.thy -----------------------";
5.453 +"----------- THERE ARE TESTS with INCOMPLETE WORK IN Test_Parse_Isac.thy -----------------------";
5.454 +"----------- THERE ARE TESTS with INCOMPLETE WORK IN Test_Parse_Isac.thy -----------------------";
5.455 +(*TODO after Problem became recursive*)
5.456 +
5.457 +"----------- parser for exp_file.str -----------------------------------------------------------";
5.458 +"----------- parser for exp_file.str -----------------------------------------------------------";
5.459 +"----------- parser for exp_file.str -----------------------------------------------------------";
5.460 +(*
5.461 + For keyword Example SPARK's lexer and parser are used. Respective Isac code was developed
5.462 + alongside existing SPARK code, not by tests. Here are tests for code using Isabelle technologies
5.463 + and preceeding the actual production code.
5.464 +*)
5.465 +val form_single =
5.466 + Parse.$$$ "(" --
5.467 + (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Formalise.model *) --
5.468 + Parse.$$$ "," --
5.469 + Parse.$$$ "(" (* begin Formalise.spec *) --
5.470 + Parse.string -- (* ThyC.id, still not qualified *)
5.471 + Parse.$$$ "," --
5.472 + (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Problem.id *) --
5.473 + Parse.$$$ "," --
5.474 + (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Method.id *) --
5.475 + Parse.$$$ ")" (* end Formalise.spec *) --
5.476 + Parse.$$$ ")";
5.477 +
5.478 +val form_single_str = (
5.479 + "( " ^
5.480 + " [\"Traegerlaenge L\", \"Streckenlast q_0\", \"Biegelinie y\", " ^
5.481 + " \"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]\", " ^
5.482 + " \"FunktionsVariable x\", \"GleichungsVariablen [c, c_2, c_3, c_4]\", " ^
5.483 + " \"AbleitungBiegelinie dy\"], " ^
5.484 + " (\"Biegelinie\", [\"Biegelinien\"], [\"IntegrierenUndKonstanteBestimmen2\"])" ^
5.485 + ")");
5.486 +
5.487 +val toks = ParseC.tokenize form_single_str;
5.488 +case ParseC.parse form_single toks of (((((((((((
5.489 + "(",
5.490 + ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
5.491 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",
5.492 + "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"]),
5.493 + ","),
5.494 + "("), "Biegelinie"), ","), ["Biegelinien"]), ","), ["IntegrierenUndKonstanteBestimmen2"]), ")"),
5.495 + ")"),
5.496 +[])
5.497 +=> () | _ => error "parse form_single toks CHANGED";
5.498 +
5.499 +(* Isac always takes a singleton here *)
5.500 +val formalise = (Parse.$$$ "[" |-- Parse.list1 form_single --| Parse.$$$ "]");
5.501 +type formalise =
5.502 + ((((((((((string * string list) * string) * string) * string) * string) * string list) *
5.503 + string) * string list) * string) * string) list;
5.504 +formalise: formalise parser;
5.505 +
5.506 +val toks = ParseC.tokenize ("[" ^ form_single_str ^ "]");
5.507 +case ParseC.parse formalise (ParseC.tokenize ("[" ^ form_single_str ^ "]")) of ([((((((((((
5.508 + "(",
5.509 + ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
5.510 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",
5.511 + "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"]),
5.512 + ","),
5.513 + "("), "Biegelinie"), ","), ["Biegelinien"]), ","), ["IntegrierenUndKonstanteBestimmen2"]), ")"),
5.514 + ")")],
5.515 +[])
5.516 +=> () | _ => error "parse formalise CHANGED";
5.517 +
6.1 --- a/test/Tools/isac/Test_Some.thy Sun Jan 17 15:25:27 2021 +0100
6.2 +++ b/test/Tools/isac/Test_Some.thy Fri Jan 22 11:27:47 2021 +0100
6.3 @@ -52,7 +52,7 @@
6.4 open UnparseC
6.5 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.6 \<close>
6.7 -ML_file "BaseDefinitions/libraryC.sml"
6.8 +ML_file "BridgeJEdit/parseC.sml"
6.9
6.10 section \<open>code for copy & paste ===============================================================\<close>
6.11 ML \<open>