2 imports "Isac.Build_Isac"
5 ML \<open>open ML_System\<close>
7 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
8 (* these vvv test, if funs are intermediately opened in structure
9 in case of errors here consider ~~/xtest-to-coding.sh *)
12 open Test_Code; CalcTreeTEST;
13 open LItool; arguments_from_model;
21 open Error_Pattern_Def;
23 open Ctree; append_problem;
29 open Auto_Prog; rule2stac;
36 open Solve; (* NONE *)
37 open ContextC; transfer_asms_from_to;
38 open Tactic; (* NONE *)
41 open P_Model; (* NONE *)
46 open Rule_Set; Sequence;
53 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
55 ML_file "BridgeJEdit/parseC.sml"
57 section \<open>code for copy & paste ===============================================================\<close>
59 "~~~~~ fun xxx , args:"; val () = ();
60 "~~~~~ and xxx , args:"; val () = ();
61 "~~~~~ fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
62 (*if*) (*then*); (*else*); (*case*) (*of*); (*return from xxx*);
64 ^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**)
65 (*/------------------- step into XXXXX -----------------------------------------------------\*)
66 (*-------------------- stop step into XXXXX -------------------------------------------------*)
67 (*\------------------- step into XXXXX -----------------------------------------------------/*)
68 (*-------------------- contiue step into XXXXX ----------------------------------------------*)
69 (*/------------------- check entry to XXXXX ------------------------------------------------\*)
70 (*\------------------- check entry to XXXXX ------------------------------------------------/*)
71 (*/------------------- check within XXXXX --------------------------------------------------\*)
72 (*\------------------- check within XXXXX --------------------------------------------------/*)
73 (*/------------------- check result of XXXXX -----------------------------------------------\*)
74 (*\------------------- check result of XXXXX -----------------------------------------------/*)
76 (*/------------------- build new fun XXXXX -------------------------------------------------\*)
77 (*\------------------- build new fun XXXXX -------------------------------------------------/*)
85 declare [[show_types]]
86 declare [[show_sorts]]
87 find_theorems "?a <= ?a"
93 ML_command \<open>Pretty.writeln prt\<close>
94 declare [[ML_print_depth = 999]]
95 declare [[ML_exception_trace]]
98 section \<open>=============== test prove_vc for Problem + sprak_vc (KEEP!) ======================\<close>
100 (* requires startup with ./zcoding-to-test.sh ..*)
101 Example \<open>~~/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
103 spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
104 (*..Problem adds to spark..*)
105 Problem (*procedure_g_c_d_4*)("Biegelinie", ["Biegelinien"])
109 Given: "Traegerlaenge ", "Streckenlast "
110 Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"
112 Relate: "Randbedingungen "
122 subsection \<open><Output> BY CLICK ON Problem..Specification\<close>
124 Comparison of the two subsections below:
125 (1) <Output> AFTER session Isac (after ./zcoding-to-test.sh) WITH click on Problem..Specification:
126 ((WHILE click ON Example SHOWS NO ERROR))
127 # headline = ..(1) == (2) ..PARSED + Specification
128 # i_model = Inc ..IN 4 ELEMENTS, (1) == (2) ..?!? FROM PARSED ?!?
129 # o_model = COMPLETE WITH 7 ELEMENTS ..FROM Example
130 # refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])..FROM References
132 (2) <Output> WITHOUT session Isac (after ./ztest-to-coding.sh) WITH click on Problem..Specification:
133 ((WHILE click ON Example SHOWS !!! ERROR))
134 # headline = ..(1) == (2) ..PARSED + Specification
135 # i_model = Inc ..IN 4 ELEMENTS, (1) == (2) ..?!? FROM PARSED ?!?
136 # o_model = [] ..NO Example
137 # refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"]) ..FROM headline ONLY
140 subsubsection \<open>(1) WITH session Isac (AFTER ./zcoding-to-test.sh)\<close>
142 {a = "//--- Spark_Commands.prove_vc", headline =
143 (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
144 ((((("Specification", ":"),
145 ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),
148 ["<markup>", "<markup>"]),
155 (("References", ":"),
156 (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),
160 "")} (line 677 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
161 {a = "prove_vc", i_model =
162 [(0, [], false, "#Given",
163 Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
164 (0, [], false, "#Given",
165 Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
166 (0, [], false, "#Find",
167 Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),
168 (Const ("empty", "??.'a"), []))),
169 (0, [], false, "#Relate",
170 Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),
171 (Const ("empty", "??.'a"), [])))],
173 [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]),
174 (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),
175 (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),
176 [Free ("y", "real \<Rightarrow> real")]),
177 (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),
178 [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
179 (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $
180 Free ("0", "real")) $
181 Const ("List.list.Nil", "bool list"),
182 Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
183 (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $
184 Free ("0", "real")) $
185 Const ("List.list.Nil", "bool list"),
186 Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
187 (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
188 (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $
189 Const ("List.list.Nil", "bool list"),
190 Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
191 (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
192 (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $
193 Const ("List.list.Nil", "bool list")]),
194 (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),
195 (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),
196 [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $
197 Const ("List.list.Nil", "real list"),
198 Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $
199 Const ("List.list.Nil", "real list"),
200 Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $
201 Const ("List.list.Nil", "real list"),
202 Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $
203 Const ("List.list.Nil", "real list")]),
204 (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),
205 [Free ("dy", "real \<Rightarrow> real")])],
207 ("Biegelinie", ["Biegelinien"],
208 ["IntegrierenUndKonstanteBestimmen2"])} (line 690 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
209 ### Proof_Context.gen_fixes
210 ### Proof_Context.gen_fixes
211 ### Proof_Context.gen_fixes
212 ### Syntax_Phases.check_terms
213 ### Syntax_Phases.check_typs
214 ### Syntax_Phases.check_typs
215 ### Syntax_Phases.check_typs
216 ## calling Output.report
217 #### Syntax_Phases.check_props
218 ### Syntax_Phases.check_terms
219 ### Syntax_Phases.check_typs
220 ### Syntax_Phases.check_typs
221 ## calling Output.report
222 #### Syntax_Phases.check_props
223 ### Syntax_Phases.check_terms
224 ### Syntax_Phases.check_typs
225 ### Syntax_Phases.check_typs
226 ## calling Output.report
227 #### Syntax_Phases.check_props
228 ### Syntax_Phases.check_terms
229 ### Syntax_Phases.check_typs
230 ### Syntax_Phases.check_typs
231 ## calling Output.report
232 #### Syntax_Phases.check_props
233 ### Syntax_Phases.check_terms
234 ### Syntax_Phases.check_typs
235 ### Syntax_Phases.check_typs
236 ## calling Output.report
237 #### Syntax_Phases.check_props
238 ### Syntax_Phases.check_terms
239 ### Syntax_Phases.check_typs
240 ### Syntax_Phases.check_typs
241 ## calling Output.report
242 #### Syntax_Phases.check_props
243 ### Syntax_Phases.check_terms
244 ### Syntax_Phases.check_typs
245 ### Syntax_Phases.check_typs
246 ## calling Output.report
247 #### Syntax_Phases.check_props
248 ### Syntax_Phases.check_terms
249 ### Syntax_Phases.check_typs
250 ### Syntax_Phases.check_typs
251 ## calling Output.report
252 #### Syntax_Phases.check_props
253 ### Syntax_Phases.check_terms
254 ### Syntax_Phases.check_typs
255 ### Syntax_Phases.check_typs
256 ## calling Output.report
257 #### Syntax_Phases.check_props
258 ### Syntax_Phases.check_terms
259 ### Syntax_Phases.check_typs
260 ### Syntax_Phases.check_typs
261 ## calling Output.report
262 #### Syntax_Phases.check_props
263 ### Syntax_Phases.check_terms
264 ### Syntax_Phases.check_typs
265 ### Syntax_Phases.check_typs
266 ## calling Output.report
267 #### Syntax_Phases.check_props
268 ### Syntax_Phases.check_terms
269 ### Syntax_Phases.check_typs
270 ### Syntax_Phases.check_typs
271 ## calling Output.report
272 #### Syntax_Phases.check_props
273 ### Syntax_Phases.check_terms
274 ### Syntax_Phases.check_typs
275 ### Syntax_Phases.check_typs
276 ## calling Output.report
277 #### Syntax_Phases.check_props
278 ### Syntax_Phases.check_terms
279 ### Syntax_Phases.check_typs
280 ### Syntax_Phases.check_typs
281 ## calling Output.report
282 #### Syntax_Phases.check_props
283 ### Syntax_Phases.check_terms
284 ### Syntax_Phases.check_typs
285 ### Syntax_Phases.check_typs
286 ## calling Output.report
287 #### Syntax_Phases.check_props
288 ### Syntax_Phases.check_terms
289 ### Syntax_Phases.check_typs
290 ### Syntax_Phases.check_typs
291 ## calling Output.report
292 #### Syntax_Phases.check_props
293 ### Syntax_Phases.check_terms
294 ### Syntax_Phases.check_typs
295 ### Syntax_Phases.check_typs
296 ## calling Output.report
297 #### Syntax_Phases.check_props
298 ### Syntax_Phases.check_terms
299 ### Syntax_Phases.check_typs
300 ### Syntax_Phases.check_typs
301 ## calling Output.report
302 #### Syntax_Phases.check_props
303 ### Syntax_Phases.check_terms
304 ### Syntax_Phases.check_typs
305 ### Syntax_Phases.check_typs
306 ## calling Output.report
307 #### Syntax_Phases.check_props
308 ### Syntax_Phases.check_terms
309 ### Syntax_Phases.check_typs
310 ### Syntax_Phases.check_typs
311 ## calling Output.report
312 #### Syntax_Phases.check_props
313 ### Syntax_Phases.check_terms
314 ### Syntax_Phases.check_typs
315 ### Syntax_Phases.check_typs
316 ## calling Output.report
317 #### Syntax_Phases.check_props
318 ### Syntax_Phases.check_terms
319 ### Syntax_Phases.check_typs
320 ### Syntax_Phases.check_typs
321 ## calling Output.report
322 #### Syntax_Phases.check_props
323 ### Syntax_Phases.check_terms
324 ### Syntax_Phases.check_typs
325 ### Syntax_Phases.check_typs
326 ### Syntax_Phases.check_typs
327 ## calling Output.report
328 #### Syntax_Phases.check_props
329 ### Syntax_Phases.check_terms
330 ### Syntax_Phases.check_typs
331 ### Syntax_Phases.check_typs
332 ### Syntax_Phases.check_typs
333 ## calling Output.report
334 ### Syntax_Phases.check_terms
335 ### Syntax_Phases.check_typs
336 ### Syntax_Phases.check_typs
337 ### Syntax_Phases.check_typs
338 ## calling Output.report
339 ### Syntax_Phases.check_terms
340 ### Syntax_Phases.check_typs
341 ### Syntax_Phases.check_typs
342 ### Syntax_Phases.check_typs
343 ## calling Output.report
344 ### Syntax_Phases.check_terms
345 ### Syntax_Phases.check_typs
346 ### Syntax_Phases.check_typs
347 ### Syntax_Phases.check_typs
348 ## calling Output.report
349 ### Syntax_Phases.check_terms
350 ### Syntax_Phases.check_typs
351 ### Syntax_Phases.check_typs
352 ### Syntax_Phases.check_typs
353 ## calling Output.report
354 ### Syntax_Phases.check_terms
355 ### Syntax_Phases.check_typs
356 ### Syntax_Phases.check_typs
357 ### Syntax_Phases.check_typs
358 ## calling Output.report
359 ### Proof_Context.gen_fixes
360 ### Proof_Context.gen_fixes
363 subsubsection \<open>(2) WITHOUT session Isac (AFTER ./ztest-to-coding.sh)\<close>
365 {a = "//--- Spark_Commands.prove_vc", headline =
366 (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
367 ((((("Specification", ":"),
368 ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),
371 ["<markup>", "<markup>"]),
378 (("References", ":"),
379 (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),
384 {a = "prove_vc", i_model =
385 [(0, [], false, "#Given",
386 Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
387 (0, [], false, "#Given",
388 Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
389 (0, [], false, "#Find",
390 Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),
391 (Const ("empty", "??.'a"), []))),
392 (0, [], false, "#Relate",
393 Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),
394 (Const ("empty", "??.'a"), [])))],
395 o_model = [], refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"])}
396 ### Proof_Context.gen_fixes
397 ### Proof_Context.gen_fixes
398 ### Proof_Context.gen_fixes
399 ### Syntax_Phases.check_terms
400 ### Syntax_Phases.check_typs
401 ### Syntax_Phases.check_typs
402 ### Syntax_Phases.check_typs
403 ## calling Output.report
404 #### Syntax_Phases.check_props
405 ### Syntax_Phases.check_terms
406 ### Syntax_Phases.check_typs
407 ### Syntax_Phases.check_typs
408 ## calling Output.report
409 #### Syntax_Phases.check_props
410 ### Syntax_Phases.check_terms
411 ### Syntax_Phases.check_typs
412 ### Syntax_Phases.check_typs
413 ## calling Output.report
414 #### Syntax_Phases.check_props
415 ### Syntax_Phases.check_terms
416 ### Syntax_Phases.check_typs
417 ### Syntax_Phases.check_typs
418 ## calling Output.report
419 #### Syntax_Phases.check_props
420 ### Syntax_Phases.check_terms
421 ### Syntax_Phases.check_typs
422 ### Syntax_Phases.check_typs
423 ## calling Output.report
424 #### Syntax_Phases.check_props
425 ### Syntax_Phases.check_terms
426 ### Syntax_Phases.check_typs
427 ### Syntax_Phases.check_typs
428 ## calling Output.report
429 #### Syntax_Phases.check_props
430 ### Syntax_Phases.check_terms
431 ### Syntax_Phases.check_typs
432 ### Syntax_Phases.check_typs
433 ## calling Output.report
434 #### Syntax_Phases.check_props
435 ### Syntax_Phases.check_terms
436 ### Syntax_Phases.check_typs
437 ### Syntax_Phases.check_typs
438 ## calling Output.report
439 #### Syntax_Phases.check_props
440 ### Syntax_Phases.check_terms
441 ### Syntax_Phases.check_typs
442 ### Syntax_Phases.check_typs
443 ## calling Output.report
444 #### Syntax_Phases.check_props
445 ### Syntax_Phases.check_terms
446 ### Syntax_Phases.check_typs
447 ### Syntax_Phases.check_typs
448 ## calling Output.report
449 #### Syntax_Phases.check_props
450 ### Syntax_Phases.check_terms
451 ### Syntax_Phases.check_typs
452 ### Syntax_Phases.check_typs
453 ## calling Output.report
454 #### Syntax_Phases.check_props
455 ### Syntax_Phases.check_terms
456 ### Syntax_Phases.check_typs
457 ### Syntax_Phases.check_typs
458 ## calling Output.report
459 #### Syntax_Phases.check_props
460 ### Syntax_Phases.check_terms
461 ### Syntax_Phases.check_typs
462 ### Syntax_Phases.check_typs
463 ## calling Output.report
464 #### Syntax_Phases.check_props
465 ### Syntax_Phases.check_terms
466 ### Syntax_Phases.check_typs
467 ### Syntax_Phases.check_typs
468 ## calling Output.report
469 #### Syntax_Phases.check_props
470 ### Syntax_Phases.check_terms
471 ### Syntax_Phases.check_typs
472 ### Syntax_Phases.check_typs
473 ## calling Output.report
474 #### Syntax_Phases.check_props
475 ### Syntax_Phases.check_terms
476 ### Syntax_Phases.check_typs
477 ### Syntax_Phases.check_typs
478 ## calling Output.report
479 #### Syntax_Phases.check_props
480 ### Syntax_Phases.check_terms
481 ### Syntax_Phases.check_typs
482 ### Syntax_Phases.check_typs
483 ## calling Output.report
484 #### Syntax_Phases.check_props
485 ### Syntax_Phases.check_terms
486 ### Syntax_Phases.check_typs
487 ### Syntax_Phases.check_typs
488 ## calling Output.report
489 #### Syntax_Phases.check_props
490 ### Syntax_Phases.check_terms
491 ### Syntax_Phases.check_typs
492 ### Syntax_Phases.check_typs
493 ## calling Output.report
494 #### Syntax_Phases.check_props
495 ### Syntax_Phases.check_terms
496 ### Syntax_Phases.check_typs
497 ### Syntax_Phases.check_typs
498 ## calling Output.report
499 #### Syntax_Phases.check_props
500 ### Syntax_Phases.check_terms
501 ### Syntax_Phases.check_typs
502 ### Syntax_Phases.check_typs
503 ## calling Output.report
504 #### Syntax_Phases.check_props
505 ### Syntax_Phases.check_terms
506 ### Syntax_Phases.check_typs
507 ### Syntax_Phases.check_typs
508 ## calling Output.report
509 #### Syntax_Phases.check_props
510 ### Syntax_Phases.check_terms
511 ### Syntax_Phases.check_typs
512 ### Syntax_Phases.check_typs
513 ### Syntax_Phases.check_typs
514 ## calling Output.report
515 #### Syntax_Phases.check_props
516 ### Syntax_Phases.check_terms
517 ### Syntax_Phases.check_typs
518 ### Syntax_Phases.check_typs
519 ### Syntax_Phases.check_typs
520 ## calling Output.report
521 ### Syntax_Phases.check_terms
522 ### Syntax_Phases.check_typs
523 ### Syntax_Phases.check_typs
524 ### Syntax_Phases.check_typs
525 ## calling Output.report
526 ### Syntax_Phases.check_terms
527 ### Syntax_Phases.check_typs
528 ### Syntax_Phases.check_typs
529 ### Syntax_Phases.check_typs
530 ## calling Output.report
531 ### Syntax_Phases.check_terms
532 ### Syntax_Phases.check_typs
533 ### Syntax_Phases.check_typs
534 ### Syntax_Phases.check_typs
535 ## calling Output.report
536 ### Syntax_Phases.check_terms
537 ### Syntax_Phases.check_typs
538 ### Syntax_Phases.check_typs
539 ### Syntax_Phases.check_typs
540 ## calling Output.report
541 ### Syntax_Phases.check_terms
542 ### Syntax_Phases.check_typs
543 ### Syntax_Phases.check_typs
544 ### Syntax_Phases.check_typs
545 ## calling Output.report
546 ### Proof_Context.gen_fixes
547 ### Proof_Context.gen_fixes
550 subsection \<open>How complete must SPARK's sequence of keywords be?\<close>
553 AT ABOVE "ML" WE HAVE:
554 Bad context for command "ML"\<^here> -- using reset state
555 ..CAUSED BY INSUFFICIENT SEQUENCE OF SPARK keywords here in this test sequence,
556 BUT spark_open + Problem ABOVE SHOWS NO ERROR -- THAT IS WHAT WE WANT DURING ADAPTATION!
559 (*//--------- SPARK keywords do work IF THERE IS NO spark_open ABOVE.. ----------------------\\* )
561 spark_proof_functions gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
565 spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
567 The following verification conditions remain to be proved:
572 spark_vc procedure_g_c_d_4 (*Bad context for command "spark_vc"\<^here> -- using reset state*)
574 spark_vc procedure_g_c_d_11
578 ( *Bad path binding: "$ISABELLE_HOME/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv"*)
580 ( *\\--------- SPARK keywords do work IF THERE IS NO spark_open ABOVE.. ----------------------//*)
582 section \<open>===================================================================================\<close>
589 section \<open>===================================================================================\<close>
596 section \<open>===================================================================================\<close>
603 section \<open>code for copy & paste ===============================================================\<close>
605 "~~~~~ fun xxx , args:"; val () = ();
606 "~~~~~ and xxx , args:"; val () = ();
607 "~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));
608 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);