1.1 --- a/src/Tools/isac/BaseDefinitions/model-pattern.sml Thu Jul 13 10:51:16 2023 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/model-pattern.sml Thu Jul 13 17:53:58 2023 +0200
1.3 @@ -71,7 +71,7 @@
1.4 type empty_input = string
1.5 fun empty_for (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) = "[__=__, __=__]"
1.6 | empty_for (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) = "[__, __]"
1.7 - | empty_for (Type ("HOL.bool", [])) = "(__=__)"
1.8 + | empty_for (Type ("fun", [Type ("HOL.bool", []), _])) = "(__=__)"
1.9 | empty_for _ = "__"
1.10 type pre_model_single = (m_field * (descriptor * term) * Position.T)
1.11 datatype pre_model_single' =
2.1 --- a/src/Tools/isac/Build_Isac.thy Thu Jul 13 10:51:16 2023 +0200
2.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Jul 13 17:53:58 2023 +0200
2.3 @@ -220,6 +220,7 @@
2.4 \<close> ML \<open>
2.5 \<close> ML \<open>
2.6 \<close> ML \<open>
2.7 +\<close> ML \<open>
2.8 \<close>
2.9
2.10 section \<open>check presence of definitions from directories\<close>
3.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Thu Jul 13 10:51:16 2023 +0200
3.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Thu Jul 13 17:53:58 2023 +0200
3.3 @@ -172,7 +172,7 @@
3.4 Given: \<open>Constants [__=__, __=__]\<close>
3.5 Where: \<open>0 < r\<close>
3.6 Find: \<open>Maximum __\<close> \<open>AdditionalValues [__, __]\<close>
3.7 - Relate: \<open>Extremum __\<close>
3.8 + Relate: \<open>Extremum (__=__)\<close>
3.9 \<open>SideConditions [__=__, __=__]\<close>
3.10 References:
3.11 Theory_Ref: "__"
3.12 @@ -276,7 +276,7 @@
3.13 Given: \<open>Constants [__=__, __=__]\<close>
3.14 Where: \<open>0 < r\<close>
3.15 Find: \<open>Maximum __\<close> \<open>AdditionalValues [__, __]\<close>
3.16 - Relate: \<open>Extremum __\<close>
3.17 + Relate: \<open>Extremum (__=__)\<close>
3.18 \<open>SideConditions [__=__, __=__]\<close>
3.19 References:
3.20 Theory_Ref: "__"
3.21 @@ -301,7 +301,7 @@
3.22 Given: \<open>Constants [r = 7]\<close>
3.23 Where: \<open>0 < r\<close>
3.24 Find: \<open>Maximum __\<close> \<open>AdditionalValues [__, __]\<close>
3.25 - Relate: \<open>Extremum __\<close> \<open>SideConditions [__=__, __=__]\<close>
3.26 + Relate: \<open>Extremum (__=__)\<close> \<open>SideConditions [__=__, __=__]\<close>
3.27 References:
3.28 Theory_Ref: "__"
3.29 (*\<Odot>*) Problem_Ref: "__/__"
3.30 @@ -324,7 +324,7 @@
3.31 Given: \<open>Constants [r = 7]\<close>
3.32 Where: \<open>0 < r\<close>
3.33 Find: \<open>Maximum __\<close> \<open>AdditionalValues [u]\<close>
3.34 - Relate: \<open>Extremum __\<close> \<open>SideConditions [__=__, __=__]\<close>
3.35 + Relate: \<open>Extremum (__=__)\<close> \<open>SideConditions [__=__, __=__]\<close>
3.36 References:
3.37 Theory_Ref: "__"
3.38 (*\<Odot>*) Problem_Ref: "__/__"
3.39 @@ -347,7 +347,7 @@
3.40 Given: \<open>Constants [r = 7]\<close>
3.41 Where: \<open>0 < r\<close>
3.42 Find: \<open>Maximum __\<close> \<open>AdditionalValues [u, v]\<close>
3.43 - Relate: \<open>Extremum __\<close> \<open>SideConditions [__=__, __=__]\<close>
3.44 + Relate: \<open>Extremum (__=__)\<close> \<open>SideConditions [__=__, __=__]\<close>
3.45 References:
3.46 Theory_Ref: "__"
3.47 (*\<Odot>*) Problem_Ref: "__/__"
3.48 @@ -365,7 +365,7 @@
3.49 Given: \<open>Constants [r = 7]\<close>
3.50 Where: \<open>0 < r\<close>
3.51 Find: \<open>Maximum __\<close> \<open>AdditionalValues [u, v]\<close>
3.52 - Relate: \<open>Extremum __\<close> \<open>SideConditions [__=__, __=__]\<close>
3.53 + Relate: \<open>Extremum (__=__)\<close> \<open>SideConditions [__=__, __=__]\<close>
3.54 References:
3.55 Theory_Ref: "__"
3.56 (*\<Odot>*) Problem_Ref: "univariate_calculus/Optimisation" (*"Biegelinien/einfache" not in teststore*)
3.57 @@ -385,7 +385,7 @@
3.58 Given: \<open>Constants [r = 7]\<close>
3.59 Where: \<open>0 < r\<close>
3.60 Find: \<open>Maximum __\<close> \<open>AdditionalValues [u, v]\<close>
3.61 - Relate: \<open>Extremum __\<close> \<open>SideConditions [__]\<close>
3.62 + Relate: \<open>Extremum (__=__)\<close> \<open>SideConditions [__]\<close>
3.63 References:
3.64 Theory_Ref: "__"
3.65 (*\<Odot>*) Problem_Ref: "univariate_calculus/Optimisation"
4.1 --- a/test/Tools/isac/BridgeJEdit/template.sml Thu Jul 13 10:51:16 2023 +0200
4.2 +++ b/test/Tools/isac/BridgeJEdit/template.sml Thu Jul 13 17:53:58 2023 +0200
4.3 @@ -57,7 +57,7 @@
4.4 (*+*) "(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n" ^
4.5 (*+*) "(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n" ^
4.6 (*+*) "(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n" ^
4.7 -(*+*) "(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum __, Position.T)), \n" ^
4.8 +(*+*) "(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n" ^
4.9 (*+*) "(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
4.10 (*+*)then () else error "final test of build I_Model.init_TEST FAILED";
4.11
4.12 @@ -67,7 +67,7 @@
4.13 show ctxt preconds empty_i_model in_refs;
4.14 "~~~~~ fun show , args:"; val (ctxt, preconds, i_model, in_refs) =
4.15 (ctxt, preconds, empty_i_model, in_refs);
4.16 -(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum __, Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
4.17 +(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
4.18 (*+*) = i_model |> I_Model.to_string_TEST @{context}
4.19 (*let*)
4.20 val model_out =
4.21 @@ -96,7 +96,7 @@
4.22 " #Where: \n" ^
4.23 " #Find: \"Maximum __\" (Incomplete)\n" ^
4.24 " \"AdditionalValues [__, __]\" (Incomplete)\n" ^
4.25 - " #Relate: \"Extremum __\" (Incomplete)\n" ^
4.26 + " #Relate: \"Extremum (__=__)\" (Incomplete)\n" ^
4.27 " \"SideConditions [__=__, __=__]\" (Incomplete)\n" ^
4.28 " References:\n Theory_Ref: \"__\"\n" ^
4.29 " Problem_Ref: \"__/__\"\n" ^
5.1 --- a/test/Tools/isac/Specify/i-model.sml Thu Jul 13 10:51:16 2023 +0200
5.2 +++ b/test/Tools/isac/Specify/i-model.sml Thu Jul 13 17:53:58 2023 +0200
5.3 @@ -166,7 +166,7 @@
5.4 I_Model.init_TEST o_model model_patt;
5.5 "~~~~~ fun init_TEST , args:"; val (ctxt, model_patt) = (ctxt, model_patt);
5.6 ;
5.7 -(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum __, Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
5.8 +(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
5.9 (*+*) = I_Model.to_string_TEST @{context} empty_i_model;
5.10
5.11
5.12 @@ -246,7 +246,7 @@
5.13 (*[(1, [1, 2, 3], false, "#Given", (Inp_TEST (Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam"), "[__=__, __=__]"), {})),
5.14 (2, [1, 2, 3], false, "#Find", (Inp_TEST (Const ("Input_Descript.Maximum", "real \<Rightarrow> toreal"), "__"), {})),
5.15 (3, [1, 2, 3], false, "#Find", (Inp_TEST (Const ("Input_Descript.AdditionalValues", "real list \<Rightarrow> toreall"), "[__, __]"), {})),
5.16 - (4, [1, 2, 3], false, "#Relate", (Inp_TEST (Const ("Input_Descript.Extremum", "bool \<Rightarrow> toreal"), "__"), {})),
5.17 + (4, [1, 2, 3], false, "#Relate", (Inp_TEST (Const ("Input_Descript.Extremum", "bool \<Rightarrow> toreal"), "(__=__)"), {})),
5.18 (5, [1, 2], false, "#Relate", (Inp_TEST (Const ("Input_Descript.SideConditions", "bool list \<Rightarrow> una"), "[__=__, __=__]"), {}))]*)
5.19 ;
5.20 val probl_POS = (*from above, #1 and #5,6 replaced by complete items for building code.test*)
5.21 @@ -294,7 +294,7 @@
5.22 "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] ,(fixes, [[r = 7]]), Position.T)), \n" ^
5.23 "(2, [1, 2, 3], false ,#Find, (Inp_TEST Maximum __, Position.T)), \n" ^
5.24 "(3, [1, 2, 3], false ,#Find, (Inp_TEST AdditionalValues [__, __], Position.T)), \n" ^
5.25 - "(4, [1, 2, 3], false ,#Relate, (Inp_TEST Extremum __, Position.T)), \n" ^
5.26 + "(4, [1, 2, 3], false ,#Relate, (Inp_TEST Extremum (__=__), Position.T)), \n" ^
5.27 "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [??.empty]), Position.T)), \n" ^
5.28 "(6, [3], true ,#Relate, (Cor_TEST SideConditions\n [(2::'a) * u = r * sin \<alpha>, (2::'a) * v = r * cos \<alpha>] ,(sideconds, [??.empty]), Position.T))]"
5.29 then () else raise error "I_Model.to_string_TEST i_model CHANGED";
6.1 --- a/test/Tools/isac/Specify/pre-conditions.sml Thu Jul 13 10:51:16 2023 +0200
6.2 +++ b/test/Tools/isac/Specify/pre-conditions.sml Thu Jul 13 17:53:58 2023 +0200
6.3 @@ -32,7 +32,7 @@
6.4 (*[(1, [1, 2, 3], false, "#Given", (Inp_TEST (Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam"), "[__=__, __=__]"), {})),
6.5 (2, [1, 2, 3], false, "#Find", (Inp_TEST (Const ("Input_Descript.Maximum", "real \<Rightarrow> toreal"), "__"), {})),
6.6 (3, [1, 2, 3], false, "#Find", (Inp_TEST (Const ("Input_Descript.AdditionalValues", "real list \<Rightarrow> toreall"), "[__, __]"), {})),
6.7 - (4, [1, 2, 3], false, "#Relate", (Inp_TEST (Const ("Input_Descript.Extremum", "bool \<Rightarrow> toreal"), "__"), {})),
6.8 + (4, [1, 2, 3], false, "#Relate", (Inp_TEST (Const ("Input_Descript.Extremum", "bool \<Rightarrow> toreal"), "(__=__)"), {})),
6.9 (5, [1, 2], false, "#Relate", (Inp_TEST (Const ("Input_Descript.SideConditions", "bool list \<Rightarrow> una"), "[__=__, __=__]"), {}))]*)
6.10 ;
6.11 val probl_POS = (*from above, #1 and #2 replaced by complete items*)
7.1 --- a/test/Tools/isac/Test_Theory.thy Thu Jul 13 10:51:16 2023 +0200
7.2 +++ b/test/Tools/isac/Test_Theory.thy Thu Jul 13 17:53:58 2023 +0200
7.3 @@ -335,10 +335,10 @@
7.4 (model_patt, i_model);
7.5
7.6 \<close> ML \<open> (*with NEW code*)
7.7 -(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum __, Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
7.8 +(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
7.9 = i_model |> I_Model.to_string_TEST @{context}
7.10 \<close> text \<open> (*with OLD code*)
7.11 -(*+*)val "[\n(0, [], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(0, [], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(0, [], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(0, [], false ,#Relate, (Inc_TEST Extremum __, Position.T)), \n(0, [], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
7.12 +(*+*)val "[\n(0, [], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(0, [], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(0, [], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(0, [], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(0, [], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
7.13 = i_model |> I_Model.to_string_TEST @ {context}
7.14 \<close> ML \<open>
7.15