1.1 --- a/test/Tools/isac/Test_Some.thy	Thu Dec 17 11:22:53 2020 +0100
     1.2 +++ b/test/Tools/isac/Test_Some.thy	Thu Dec 17 11:42:18 2020 +0100
     1.3 @@ -103,6 +103,17 @@
     1.4  spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
     1.5  (*..Problem adds to spark..*)
     1.6  Problem (*procedure_g_c_d_4*)("Biegelinie", ["Biegelinien"])
     1.7 +  Specification:
     1.8 +    Model:
     1.9 +      Given: "Traegerlaenge ", "Streckenlast "
    1.10 +      Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"
    1.11 +      Find: "Biegelinie "
    1.12 +      Relate: "Randbedingungen "
    1.13 +    References:
    1.14 +      RTheory: ""
    1.15 +      RProblem: ["", ""]
    1.16 +      RMethod: ["", ""]
    1.17 +  Solution:
    1.18  
    1.19  ML \<open>
    1.20    (*
    1.21 @@ -112,7 +123,6 @@
    1.22    BUT spark_open + Problem  ABOVE SHOWS NO ERROR -- THAT IS WHAT WE WANT DURING ADAPTATION!
    1.23    *)
    1.24  \<close>
    1.25 -
    1.26  (*//--------- SPARK keywords do work IF THERE IS NO spark_open ABOVE.. ----------------------\\* )
    1.27  (** )
    1.28  spark_proof_functions gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
    1.29 @@ -138,7 +148,9 @@
    1.30  
    1.31  subsection \<open>result Problem 1: got data from Example\<close>
    1.32  text \<open>
    1.33 -{a = "prove_vc", o_model =
    1.34 +trace:
    1.35 +
    1.36 +{a = "//--- Spark_Commands.prove_vc", o_model =
    1.37   [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]), (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),
    1.38    (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]),
    1.39    (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),
    1.40 @@ -161,8 +173,71 @@
    1.41  *)
    1.42  \<close> 
    1.43  
    1.44 -subsection \<open>\<close>
    1.45 -text \<open>\<close>
    1.46 +subsection \<open>result Problem 2: initial Specification parsed\<close>
    1.47 +text \<open>
    1.48 +  Note: this kind of parsing is inappropriate with respect to integration:
    1.49 +  the Position.T are dropped, so no feedback can be allocated.
    1.50 +
    1.51 +  trace:
    1.52 +
    1.53 +### Private_Output.report keyword1 
    1.54 +{a = "//--- Spark_Commands.prove_vc", headline =
    1.55 + (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
    1.56 +   ((((("Specification", ":"),
    1.57 +       ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]), "Where"), ":"),
    1.58 +               ["<markup>", "<markup>"]),
    1.59 +              "Find"),
    1.60 +             ":"),
    1.61 +            "<markup>"),
    1.62 +           "Relate"),
    1.63 +          ":"),
    1.64 +         ["<markup>"]),
    1.65 +        (("References", ":"), (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),
    1.66 +      "Solution"),
    1.67 +     ":"),
    1.68 +    [])),
    1.69 +  "")} (line 677 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy") 
    1.70 +{a = "prove_vc", i_model =
    1.71 + [(0, [], false, "#Given", Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
    1.72 +  (0, [], false, "#Given", Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
    1.73 +  (0, [], false, "#Find", Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
    1.74 +  (0, [], false, "#Relate",
    1.75 +   Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []), (Const ("empty", "??.'a"), [])))],
    1.76 + o_model =
    1.77 + [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]),
    1.78 +  (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),
    1.79 +  (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]),
    1.80 +  (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),
    1.81 +   [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
    1.82 +      (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $
    1.83 +      Const ("List.list.Nil", "bool list"),
    1.84 +    Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
    1.85 +      (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $
    1.86 +      Const ("List.list.Nil", "bool list"),
    1.87 +    Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
    1.88 +      (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $
    1.89 +        Free ("0", "real")) $
    1.90 +      Const ("List.list.Nil", "bool list"),
    1.91 +    Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
    1.92 +      (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $
    1.93 +        Free ("0", "real")) $
    1.94 +      Const ("List.list.Nil", "bool list")]),
    1.95 +  (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),
    1.96 +  (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),
    1.97 +   [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $ Const ("List.list.Nil", "real list"),
    1.98 +    Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $ Const ("List.list.Nil", "real list"),
    1.99 +    Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $ Const ("List.list.Nil", "real list"),
   1.100 +    Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $ Const ("List.list.Nil", "real list")]),
   1.101 +  (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("dy", "real \<Rightarrow> real")])],
   1.102 + refs =
   1.103 + ("Biegelinie", ["Biegelinien"],
   1.104 +  ["IntegrierenUndKonstanteBestimmen2"])} (line 690 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy") 
   1.105 +### Private_Output.report  
   1.106 +### Syntax_Phases.check_typs 
   1.107 +:
   1.108 +### Syntax_Phases.check_terms 
   1.109 +:
   1.110 +\<close>
   1.111  
   1.112  section \<open>===================================================================================\<close>
   1.113  ML \<open>