1.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Mon Feb 27 09:45:29 2023 +0100
1.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Sat Mar 04 19:02:39 2023 +0100
1.3 @@ -63,12 +63,9 @@
1.4 \<close> ML \<open>
1.5 (*\-------------------- state of src/../preliminary.sml at that time -------------------------/*)
1.6 \<close> ML \<open> (*\<longrightarrow> test/../calculation.sml*)
1.7 -"----------- build Outer_Syntax Example_TEST ---------------------------------------------------";
1.8 -"----------- build Outer_Syntax Example_TEST ---------------------------------------------------";
1.9 -"----------- build Outer_Syntax Example_TEST ---------------------------------------------------";
1.10 -"----------- build Outer_Syntax Example_TEST: stepwise input, References empty -----------------";
1.11 -"----------- build Outer_Syntax Example_TEST: stepwise input, References empty -----------------";
1.12 -"----------- build Outer_Syntax Example_TEST: stepwise input, References empty -----------------";
1.13 +"----------- build Outer_Syntax Example_TEST 2: stepwise input, References empty ---------------";
1.14 +"----------- build Outer_Syntax Example_TEST 2: stepwise input, References empty ---------------";
1.15 +"----------- build Outer_Syntax Example_TEST 2: stepwise input, References empty ---------------";
1.16 (*/---------------------------------------- mimic input from PIDE -----------------------------\*)
1.17 (* Example_TEST "Diff_App-No.123a" (*complete Model, empty References*) *)
1.18 val thy = @{theory}
1.19 @@ -96,7 +93,53 @@
1.20 (*let*)
1.21 val {origin = (_, o_ref, _), spec = spec_ref, ctxt, ...} =
1.22 Ctree.get_obj I state [(*Pos will become variable*)] |> Ctree.rep_specify_data
1.23 +\<close> ML \<open>
1.24 +open Model_Pattern
1.25 +\<close> ML \<open> (*knows variables from origin + notation (input) undefined ^^^^^ from BaseDefinitions.thy*)
1.26 +(*test*)val Const ("Input_Descript.Constants", _) $
1.27 + (Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ Const ("HOL.undefined", _) $ Const ("HOL.undefined", _)) $
1.28 + (Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ Const ("HOL.undefined", _) $ Const ("HOL.undefined", _)) $
1.29 + Const ("List.list.Nil", _))) = Syntax.read_term ctxt "Constants [__=__, __=__]"
1.30 +\<close> ML \<open>
1.31 val thy_id' = References.for_parse thy_id (#1 spec_ref) (#1 o_ref)
1.32 +\<close> ML \<open>
1.33 +val "Diff_App" = thy_id'
1.34 +\<close> ML \<open>
1.35 + val (model, where_) =
1.36 +Model_Pattern.parse_pos_TEST ctxt model_input;
1.37 +\<close> ML \<open>
1.38 +"~~~~~ fun parse_pos_TEST , args:"; val (ctxt, model_input) = (ctxt, model_input);
1.39 +\<close> ML \<open>
1.40 + val items = model_input |> map (fn (m_field, items) => map (pair m_field) items) |> flat;
1.41 +\<close> ML \<open>
1.42 + val model = items
1.43 + |> filter_out ((fn f => (fn (f', _) => f = f')) "#Where")
1.44 +(* |> map (parse_term ctxt) *)
1.45 +(*val model =
1.46 + [("#Given", ("Constants [r = 7]", {})), ("#Find", ("Maximum A", {})), ("#Find", ("AdditionalValues [u, v]", {})), ("#Relate", ("Extremum (A = 2 * u * v - u \<up> 2)", {})),
1.47 + ("#Relate", ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", {}))]:
1.48 + (string * (string * Position.T)) list*)
1.49 +\<close> ML \<open>
1.50 +"~~~~~ fun parse_term_TEST , args:"; val (ctxt, (m_field, (str, pos))) = (ctxt, hd model);
1.51 +\<close> ML \<open>
1.52 + val (m_field, term, pos) = parse_term ctxt (m_field, (str, pos))
1.53 +\<close> ML \<open>
1.54 +\<close> ML \<open>
1.55 +(*test*)if is_undefined @{term "Constants [__=__, __=__]"}
1.56 +(*test*) then () else error "is_undefined 1 CHANGED";
1.57 +(*test*)if is_undefined @{term "Maximum __"}
1.58 +(*test*) then () else error "is_undefined 2 CHANGED";
1.59 +(*test*)if is_undefined @{term "AdditionalValues [__, __]"}
1.60 +(*test*) then () else error "is_undefined 3 CHANGED";
1.61 +(*test*)if is_undefined @{term "Constants [r = 7]"}
1.62 +(*test*) then error "is_undefined 4 CHANGED" else ();
1.63 +\<close> ML \<open>
1.64 + val (m_field, (descr, arg), pos) = split_descriptor ctxt (m_field, term, pos)
1.65 +\<close> ML \<open>
1.66 + if is_undefined arg
1.67 + then Empty (m_field, (descr, descr |> type_of |> empty_for), pos)
1.68 + else Proper (m_field, (descr, arg), pos)
1.69 +\<close> ML \<open>
1.70 val (model, where_) = Model_Pattern.parse_pos_TEST ctxt model_input (*+check syntax*)
1.71 \<close> ML \<open>
1.72 (model, where_) (*GOON*)
1.73 @@ -160,13 +203,13 @@
1.74 text \<open>
1.75 Just a test, that this works also in $ISABELLE_ISAC_TEST
1.76 \<close>
1.77 -Example "Diff_App-No.123a" (*complete Specification*)
1.78 +Example_TEST "Diff_App-No.123a" (*complete Specification*)
1.79 Specification:
1.80 Model:
1.81 Given: \<open>Constants [r = 7]\<close>
1.82 Where: \<open>0 < r\<close>
1.83 Find: \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close>
1.84 - Relate: \<open>Extremum A = 2 * u * v - u \<up> 2\<close>
1.85 + Relate: \<open>Extremum (A = 2 * u * v - u \<up> 2)\<close>
1.86 \<open>SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\<close>
1.87 References:
1.88 Theory_Ref: "Diff_App"
1.89 @@ -178,12 +221,11 @@
1.90 Check complete \<open>Model\<close>, infer empty \<open>References\<close> from data hidden in "Diff_App-No.123a"
1.91 \<close>
1.92 (*
1.93 -Example: no syntax check of terms, OK.
1.94 +Example: no syntax check of terms, thus OK.
1.95 Example_TEST: proper syntax check of terms with Model_Pattern.parse_pos,
1.96 - but with parse_pos_TEST ERROR Malformed YXML: unbalanced element "input"
1.97 *)
1.98 -(**)Example
1.99 -(** )Example_TEST( **) "Diff_App-No.123a" (*complete Model, empty References*)
1.100 +(** )Example
1.101 +( **)Example_TEST(**) "Diff_App-No.123a" (*complete Model, empty References*)
1.102 Specification:
1.103 Model:
1.104 Given: \<open>Constants [r = 7]\<close>
1.105 @@ -208,7 +250,7 @@
1.106 not aware of "where_-conditions", i.e. of preconditions.
1.107 \<close>
1.108
1.109 -Example "Diff_App-No.123a"
1.110 +Example_TEST "Diff_App-No.123a" (*all empty*)
1.111 Specification:
1.112 Model:
1.113 Given: \<open>Constants [__=__, __=__]\<close>
1.114 @@ -312,7 +354,7 @@
1.115 ) Ctree.EmptyPtree;
1.116 val ptp = (pt, p);
1.117 \<close>
1.118 -Example "Diff_App-No.123a"
1.119 +Example_TEST "Diff_App-No.123a" (*all empty step 0*)
1.120 Specification:
1.121 Model:
1.122 Given: \<open>Constants [__=__, __=__]\<close>
1.123 @@ -335,13 +377,13 @@
1.124 val ("ok", ([(Tactic.Add_Given "Constants [r = 7]", _, _)], _, ptp))
1.125 = Step.specify_do_next ptp;
1.126 \<close>
1.127 -Example "Diff_App-No.123a"
1.128 +Example_TEST "Diff_App-No.123a" (*step 1: <Constants [r = 7]>*)
1.129 Specification:
1.130 Model:
1.131 Given: \<open>Constants [r = 7]\<close>
1.132 Where: \<open>0 < r\<close>
1.133 - Find: \<open>Maximum _\<close> \<open>AdditionalValues [__, __]\<close>
1.134 - Relate: \<open>Extremum _\<close> \<open>SideConditions [__=__, __=__]\<close>
1.135 + Find: \<open>Maximum __\<close> \<open>AdditionalValues [__, __]\<close>
1.136 + Relate: \<open>Extremum __\<close> \<open>SideConditions [__=__, __=__]\<close>
1.137 References:
1.138 Theory_Ref: "__"
1.139 (*\<Odot>*) Problem_Ref: "__/__"
1.140 @@ -356,13 +398,13 @@
1.141 val ("ok", ([(Tactic.Add_Find "Maximum A", _, _)], _, ptp))
1.142 = Step.specify_do_next ptp;
1.143 \<close>
1.144 -Example "Diff_App-No.123a"
1.145 +Example_TEST "Diff_App-No.123a" (*step 2: AdditionalValues [u]*)
1.146 Specification:
1.147 Model:
1.148 - Given: \<open>Constants r = 7\<close>
1.149 + Given: \<open>Constants [r = 7]\<close>
1.150 Where: \<open>0 < r\<close>
1.151 - Find: \<open>Maximum _\<close> \<open>AdditionalValues [u]\<close>
1.152 - Relate: \<open>Extremum _\<close> \<open>SideConditions [__=__, __=__]\<close>
1.153 + Find: \<open>Maximum __\<close> \<open>AdditionalValues [u]\<close>
1.154 + Relate: \<open>Extremum __\<close> \<open>SideConditions [__=__, __=__]\<close>
1.155 References:
1.156 Theory_Ref: "__"
1.157 (*\<Odot>*) Problem_Ref: "__/__"
1.158 @@ -377,13 +419,13 @@
1.159 = Step.specify_do_next ptp;
1.160 \<close>
1.161
1.162 -Example "Diff_App-No.123a"
1.163 +Example_TEST "Diff_App-No.123a" (*step 3: A.Values [u, v]*)
1.164 Specification:
1.165 Model:
1.166 - Given: \<open>Constants r = 7\<close>
1.167 + Given: \<open>Constants [r = 7]\<close>
1.168 Where: \<open>0 < r\<close>
1.169 - Find: \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close>
1.170 - Relate: \<open>Extremum _\<close> \<open>SideConditions [__=__, __=__]\<close>
1.171 + Find: \<open>Maximum __\<close> \<open>AdditionalValues [u, v]\<close>
1.172 + Relate: \<open>Extremum __\<close> \<open>SideConditions [__=__, __=__]\<close>
1.173 References:
1.174 Theory_Ref: "__"
1.175 (*\<Odot>*) Problem_Ref: "__/__"
1.176 @@ -395,16 +437,16 @@
1.177 \<close>
1.178 ML \<open> (* # 5: Input to \<open>Problem_Ref\<close> might change the \<open>Model\<close> *)
1.179 \<close>
1.180 -Example "Diff_App-No.123a"
1.181 +Example_TEST "Diff_App-No.123a" (*step 4: (wrong) Problem_Ref input*)
1.182 Specification:
1.183 Model:
1.184 - Given: \<open>Constants r = 7\<close>
1.185 + Given: \<open>Constants [r = 7]\<close>
1.186 Where: \<open>0 < r\<close>
1.187 - Find: \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close>
1.188 - Relate: \<open>Extremum _\<close> \<open>SideConditions [__=__, __=__]\<close>
1.189 + Find: \<open>Maximum __\<close> \<open>AdditionalValues [u, v]\<close>
1.190 + Relate: \<open>Extremum __\<close> \<open>SideConditions [__=__, __=__]\<close>
1.191 References:
1.192 Theory_Ref: "__"
1.193 - (*\<Odot>*) Problem_Ref: "__/__"
1.194 + (*\<Odot>*) Problem_Ref: "univariate_calculus/Optimisation" (*"Biegelinien/einfache" not in teststore*)
1.195 (*\<Otimes>*) Method_Ref: "__/__"
1.196 (*Solution:*)
1.197
1.198 @@ -415,13 +457,13 @@
1.199 \<close>
1.200 ML \<open> (* # 6: Input to \<open>Method_Ref\<close> changes the \<open>Model\<close> to the respective \<open>Method\<close> *)
1.201 \<close>
1.202 -Example "Diff_App-No.123a"
1.203 +Example_TEST "Diff_App-No.123a" (*step 5: Method_Ref updated*)
1.204 Specification:
1.205 Model: (* FIXME: lookup model of method *)
1.206 - Given: \<open>Constants r = 7\<close>
1.207 + Given: \<open>Constants [r = 7]\<close>
1.208 Where: \<open>0 < r\<close>
1.209 - Find: \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close>
1.210 - Relate: \<open>Extremum _\<close> \<open>SideConditions [_]\<close>
1.211 + Find: \<open>Maximum __\<close> \<open>AdditionalValues [u, v]\<close>
1.212 + Relate: \<open>Extremum __\<close> \<open>SideConditions [__]\<close>
1.213 References:
1.214 Theory_Ref: "__"
1.215 (*\<Odot>*) Problem_Ref: "univariate_calculus/Optimisation"