1.1 --- a/test/Pure/Isar/Keywords_Diag.thy Thu Jul 02 09:57:58 2020 +0200
1.2 +++ b/test/Pure/Isar/Keywords_Diag.thy Fri Jul 17 11:42:20 2020 +0200
1.3 @@ -10,16 +10,16 @@
1.4 subsection \<open>definitions for keywords\<close>
1.5
1.6 theory Keywords_Diag
1.7 -imports Pure
1.8 +imports Isac.Isac_Knowledge (*Pure: not for Problem Biegelinie*)
1.9 keywords
1.10 (* this has a type and thus is a "major keyword" *)
1.11 "ISAC" :: diag and
1.12 (* the following are without type: "minor keywords" *)
1.13 - "Problem" (* await input of (string * string list) *)and
1.14 + "Problem" (* root-problem + recursively in Solution *)
1.15 "Specification" "Model" "References" "Solution" (* structure only *) and
1.16 "Given" "Find" "Relate" "Where" (* await input of term *) and
1.17 - "Theory" (* await input of string *) and
1.18 - "Problem" "Method" (* await input of string list *) and
1.19 + "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *) and
1.20 + "RProblem" "RMethod" (* await input of string list *) and
1.21 "Tactic" (* optionally repeated with each step 0.. end of calculation *)
1.22 begin
1.23
1.24 @@ -34,6 +34,10 @@
1.25 : Token.T list -> (Toplevel.transition -> Toplevel.transition) * Token.T list;
1.26 (*---------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ value of >> *)
1.27 \<close> ML \<open>
1.28 +op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c (* args -------vvv-- 1st -- 2nd*)
1.29 +(* ('a parser : T list -> 'a * T list
1.30 + * (Input.source -> (Toplevel.transition -> Toplevel.transition))*)
1.31 +\<close> ML \<open>
1.32 (Parse.input Parse.cartouche) : Input.source parser;
1.33 (*-----------------------------^^^^^^^^^^^^^^^^^^^^^----------------------------- 1st arg of >> *)
1.34 \<close> ML \<open>
1.35 @@ -44,7 +48,7 @@
1.36 \<close> ML \<open> (*decompose and investigate 1st arg..------------------------------------------------- *)
1.37 Parse.input : 'a parser -> Input.source parser;
1.38 Parse.cartouche : string parser
1.39 -;
1.40 +\<close> ML \<open>
1.41 val input = Input.string "123"
1.42 (* = Source {delimited = true, range = ({}, {}), text = "123"}*)
1.43 : Input.source;
1.44 @@ -95,9 +99,30 @@
1.45 (*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 1st arg of >> *)
1.46 \<close> ML \<open>
1.47 Parse.input : 'a parser -> Input.source parser;
1.48 -\<close> ML \<open>
1.49 Parse.cartouche : string parser
1.50 (*\\------------------------------------------------------------------------------------------//*)
1.51 +\<close> ML \<open>
1.52 +\<close>
1.53 +
1.54 +subsubsection \<open>tokenise input"\<close>
1.55 +ML \<open>
1.56 +\<close> ML \<open>
1.57 + Outer_Syntax.command @{command_keyword TEST_SIGNAT} "investigate signatures involveD"
1.58 + ((Parse.input Parse.cartouche) >> (fn input =>
1.59 + Toplevel.keep (fn _ => ignore (ML_Lex.read_source input) ) ) ) : unit
1.60 +\<close> ML \<open>
1.61 +ML_Lex.read_source: Input.source -> (ML_Lex.token Antiquote.antiquote) list
1.62 +\<close> ML \<open>
1.63 +Source.source:
1.64 + 'a Scan.stopper ->
1.65 + ('a list -> 'b list * 'a list) ->
1.66 + ('a, 'c) Source.source -> ('b, ('a, 'c) Source.source) Source.source
1.67 +\<close> ML \<open>
1.68 +\<close> ML \<open>
1.69 +\<close> ML \<open>
1.70 +K
1.71 +\<close> ML \<open>
1.72 +\<close> ML \<open>
1.73 \<close>
1.74
1.75 subsection \<open>stepwise incrementing the parser\<close>
1.76 @@ -107,23 +132,7 @@
1.77 "Outer_Syntax.command @ {command_keyword xxx}" is allowed only once in a theory,
1.78 so outcomment accordingly !
1.79 \<close>
1.80 -subsubsection \<open>step 0: provide functions such that \<close>
1.81 -ML \<open>
1.82 -val ISAC_parser = Parse.cartouche
1.83 -\<close> ML \<open>
1.84 -val check_ISAC : (Token.T list -> Input.source * Token.T list) = fn input =>
1.85 - let
1.86 - val toks = Parse.input ISAC_parser input
1.87 - val _ (*just check if input is according to ..*) = ISAC_parser
1.88 - in toks end
1.89 -\<close> ML \<open>
1.90 -val _ =
1.91 - Outer_Syntax.command @{command_keyword ISAC}
1.92 - "parsing stepwise incremented by check_ISAC"
1.93 - (check_ISAC >> (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))
1.94 -\<close> ML \<open>
1.95 -\<close>
1.96 -subsubsection \<open>step 1: "Problem Specification Model -- STOPPED HERE"\<close>
1.97 +subsubsection \<open>step -1: investigate signatures "Problem Specification Model -- STOPPED HERE"\<close>
1.98 ML \<open>
1.99 \<close> ML \<open>
1.100 Parse.input : 'a parser -> Input.source parser;
1.101 @@ -154,39 +163,142 @@
1.102 *)
1.103 \<close> ML \<open>
1.104 \<close>
1.105 +subsubsection \<open>step 0: provide a structure for steps\<close>
1.106 +ML \<open>
1.107 +val ISAC_parser = Parse.cartouche;
1.108 +ISAC_parser: string parser
1.109 +\<close> ML \<open>
1.110 +val check_ISAC : (Token.T list -> Input.source * Token.T list) = fn input =>
1.111 + let
1.112 + val toks = Parse.input ISAC_parser input
1.113 + val _ (*just check if input is according to ..*) = ISAC_parser
1.114 + in toks end
1.115 +\<close> text \<open> (*ML -> Duplicate outer syntax command "ISAC" *)
1.116 +val _ = (*-------------v--------------------*)
1.117 + Outer_Syntax.command @ {command_keyword ISAC} "parsing stepwise incremented by check_ISAC"
1.118 + (check_ISAC >> (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))
1.119 +\<close> ML \<open>
1.120 +\<close>
1.121
1.122 -subsection \<open>Makarius' hint on rendering ISAC calculation\<close>
1.123 -subsubsection \<open>ISAC command definition, original by Makarius\<close>
1.124 -(*//------- outcommented during stepwise incrementing the parser ----------------------------* )
1.125 +subsubsection \<open>step 1: Problem ("Biegelinie", ["Biegelinien"]) etc\<close>
1.126 +text \<open>
1.127 + we have {term "Problem (''Biegelinie'', [''Biegelinien''])"} !!!
1.128 + !!! as formula + as Tactic
1.129 +\<close>
1.130 ML \<open>
1.131 -val _ =
1.132 - Outer_Syntax.command @{command_keyword ISAC}
1.133 - "embedded ISAC language" (* an initial hint by Makarius *)
1.134 - (Parse.input Parse.cartouche >>
1.135 - (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))
1.136 -\<close>
1.137 -( *--------- outcommented during stepwise incrementing the parser --------------------------//*)
1.138 +val str = "Problem (''Biegelinie'', [''Biegelinien''])"
1.139 +val t = @{term "Problem (''Biegelinie'', [''Biegelinien''])"}
1.140 +\<close> ML \<open>
1.141 +val input = Input.string str
1.142 +\<close> ML \<open>
1.143 +val toks = ML_Lex.read_source input;
1.144 +\<close> ML \<open>
1.145 +toks: ML_Lex.token Antiquote.antiquote list
1.146 +\<close> ML \<open>
1.147 +length toks = 11;
1.148 +nth 1 toks (* = Text (Token (({}, {}), (Ident, "Problem"))) <--------- (Keyword, "Problem") *);
1.149 +nth 2 toks (* = Text (Token (({}, {}), (Space, " ")))*);
1.150 +nth 3 toks (* = Text (Token (({}, {}), (Keyword, "(")))*);
1.151 +nth 4 toks (*Text (Token (({}, {}), (Type_Var, "''Biegelinie''"))) <---------- Type_Var !?!?*);
1.152 +nth 10 toks (* = Text (Token (({}, {}), (Keyword, ")")))*);
1.153 +\<close> ML \<open>
1.154 +ignore (ML_Lex.read_source input) : unit;
1.155 +\<close> ML \<open>
1.156 +\<close> ML \<open>
1.157 +\<close> ML \<open>
1.158 +val str = "a=b";
1.159 +val input = Input.string str
1.160 +val toks = ML_Lex.read_source (*true*) input;
1.161 +nth 2 toks (* = Text (Token (({}, {}), (Keyword, "="))) ----------^^^ (Keyword, "Problem") *);
1.162 +\<close> ML \<open>
1.163 +\<close>
1.164
1.165 -subsubsection \<open>complete ISAC calculation\<close>
1.166 -ISAC \<open>
1.167 -Problem ("Biegelinie", ["Biegelinien"])
1.168 - Specification:
1.169 - Model:
1.170 +subsubsection \<open>step 2: Model\<close>
1.171 +ML \<open>
1.172 +\<close> ML \<open>
1.173 +val ISAC_parser = Parse.cartouche;
1.174 +ISAC_parser: string parser
1.175 +\<close> ML \<open>
1.176 +val parse_Model = Parse.reserved "Model" --
1.177 + Parse.reserved "Given" -- Parse.list (Parse.term) --
1.178 + Parse.reserved "Where" -- Parse.list (Parse.term) --
1.179 + Parse.reserved "Find" -- Parse.term --
1.180 + Parse.reserved "Relate" -- Parse.list (Parse.term)
1.181 +\<close> ML \<open>
1.182 +parse_Model: Token.T list ->
1.183 + ((((((((string * string) * string list) * string) * string list) * string) * string) * string) * string list) * Token.T list
1.184 +\<close> ML \<open> (*/---------- -> ERROR text cartouche was found ----------\*)
1.185 +val ISAC_parser = (*a* ) parse_Model -- Parse.cartouche ( *a*)
1.186 + (*b*) Parse.cartouche -- parse_Model (*b*)
1.187 +\<close> ML \<open>
1.188 +val check_ISAC : (Token.T list -> Input.source * Token.T list) = fn input =>
1.189 + let
1.190 + val toks = Parse.input ISAC_parser input
1.191 + val _ (*just check if input is according to ..*) = ISAC_parser
1.192 + in toks end
1.193 +\<close> ML \<open> (*ML -> Duplicate outer syntax command "ISAC" *)
1.194 +val _ = (*-------------v--------------------*)
1.195 + Outer_Syntax.command @{command_keyword ISAC} "parsing stepwise incremented by check_ISAC"
1.196 + (check_ISAC >> (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))
1.197 +\<close> ML \<open>
1.198 +\<close>
1.199 +(*/----- with above check_ISAC + ISAC_parser (*a*) | (*b*)*)
1.200 +ISAC \<open>Model:
1.201 Given: "Traegerlaenge L", "Streckenlast q_0"
1.202 Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"
1.203 Find: "Biegelinie y"
1.204 Relate: "Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]"
1.205 +\<close>
1.206 +(* ----- ERROR (*a*) | (*b*): * )
1.207 +(*a*) Outer syntax error: reserved identifier "Model" expected,
1.208 +but text cartouche was found:
1.209 +\<open>Model: ...
1.210 +
1.211 +(*b*) Outer syntax error\<^here>: reserved identifier "Model" expected,
1.212 +but end-of-input\<^here> was found
1.213 +( *\---------- -> ERROR text cartouche was found ----------/*)
1.214 +
1.215 +
1.216 +subsection \<open>Makarius' hint on rendering ISAC calculation\<close>
1.217 +text \<open>
1.218 + ISAC command definition, original by Makarius
1.219 +/--- outcommented during stepwise incrementing the parser ----------------------------\
1.220 +
1.221 +keywords "ISAC" :: diag
1.222 +
1.223 +ML \<open>
1.224 +val _ =
1.225 + Outer_Syntax.command @ {command_keyword ISAC}
1.226 + "embedded ISAC language" (* an initial hint by Makarius *)
1.227 + (Parse.input Parse.cartouche >>
1.228 + (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))
1.229 +\<close>
1.230 +\--- outcommented during stepwise incrementing the parser ----------------------------/
1.231 +\<close>
1.232 +subsection \<open>complete ISAC calculation\<close>
1.233 +(*/--- outcomment during stepwise incrementing the parser ----------------------------\*)
1.234 +ISAC \<open>
1.235 +"Problem ("Biegelinie", ["Biegelinien"])"
1.236 + Specification:
1.237 + Model:
1.238 + Given: ["Traegerlaenge L", "Streckenlast q_0"]
1.239 + Where: ["q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"]
1.240 + Find: "Biegelinie y"
1.241 + Relate: ["Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]"]
1.242 References:
1.243 - Theory: "Biegelinie"
1.244 - Problem: ["Biegelinien"]
1.245 - Method: ["Integrieren", "KonstanteBestimmen2"]
1.246 + RTheory: "Biegelinie"
1.247 + RProblem: ["Biegelinien"]
1.248 + RMethod: ["Integrieren", "KonstanteBestimmen2"]
1.249 Solution:
1.250 - Problem ("Biegelinie", ["vonBelastungZu", "Biegelinien"])
1.251 + "Problem ("Biegelinie", ["vonBelastungZu", "Biegelinien"])"
1.252 "[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)]"
1.253 - Problem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"])
1.254 +
1.255 + "Problem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"])"
1.256 "[L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3]"
1.257 +
1.258 "solveSystem [L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3] [c, c_1, c_2, c_4]"
1.259 "[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
1.260 +
1.261 "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)"
1.262 Tactic Substitute "c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)" "[c, c_1, c_2, c_4]"
1.263 "y x = 0 + 0 * x + 1 / (-1 * EI) * (-1 * L ^ 2 * q_0 / 2 / 2 * x ^ 2 + -1 * L * q_0 / -1 / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)"
1.264 @@ -195,4 +307,6 @@
1.265 Tactic Check_Postcond ["Biegelinien"]
1.266 "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"
1.267 \<close>
1.268 +(*\--- outcomment during stepwise incrementing the parser ----------------------------/*)
1.269 +
1.270 end
1.271 \ No newline at end of file