1.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Sat Aug 26 15:14:24 2023 +0200
1.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Sun Aug 27 11:19:14 2023 +0200
1.3 @@ -309,10 +309,10 @@
1.4 val icl = filter false_and_not_Sup vits; (* incomplete *)
1.5
1.6 (*if*) icl = [] (*else*);
1.7 -(*+*)val "[\n(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] ,(Constants, [])), \n(2 ,[1, 2, 3] ,false ,#Find ,Inc Maximum ,(Maximum, [])), \n(3 ,[1, 2, 3] ,false ,#Find ,Inc AdditionalValues [] ,(AdditionalValues, [])), \n(4 ,[1, 2, 3] ,false ,#Relate ,Inc Extremum ,(Extremum, [])), \n(5 ,[1, 2] ,false ,#Relate ,Inc SideConditions [] ,(SideConditions, []))]"
1.8 -(*+*) = icl |> I_Model.to_string @{context}
1.9 -(*+*)val "(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] ,(Constants, []))"
1.10 -(*+*) = hd icl |> I_Model.single_to_string @{context}
1.11 +(*+*)val "[\n(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str), \n(2 ,[1, 2, 3] ,false ,#Find ,Inc Maximum , pen2str), \n(3 ,[1, 2, 3] ,false ,#Find ,Inc AdditionalValues [] , pen2str), \n(4 ,[1, 2, 3] ,false ,#Relate ,Inc Extremum , pen2str), \n(5 ,[1, 2] ,false ,#Relate ,Inc SideConditions [] , pen2str)]"
1.12 + = icl |> I_Model.to_string @{context}
1.13 +(*+*)val "(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str)"
1.14 + = hd icl |> I_Model.single_to_string @{context}
1.15
1.16 (*++*)val feedback = (fn (_, _, _, _, feedback) => feedback) (hd icl)
1.17 (*++*)val Const ("Input_Descript.Constants", _) = I_Model.descriptor feedback
1.18 @@ -404,7 +404,7 @@
1.19 val pval = [Input_Descript.join'''' (d, ts')]
1.20 val complete = if eq_set op = (ts', all) then true else false
1.21
1.22 -(*+*)val "Inc Constants [] ,(Constants, [])" = itm_ |> I_Model.feedback_to_string @{context}
1.23 +(*+*)val "Inc Constants [] , pen2str" = itm_ |> I_Model.feedback_to_string @{context}
1.24 (*\\\----------------- step into specify_do_next -------------------------------------------//*)
1.25 (*\\------------------ step into do_next ---------------------------------------------------//*)
1.26 val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next
1.27 @@ -921,7 +921,7 @@
1.28 (*if*) itms <> [] (*then*);
1.29 val itms = I_Model.complete oris probl [] model
1.30
1.31 -(*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]])), \n(7 ,[1] ,true ,#Given ,Cor FunctionVariable a ,(funvar, [a])), \n(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} ,(doma, [{0<..<r}])), \n(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) ,(err, [\<epsilon> = 0]))]"
1.32 +(*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,true ,#Given ,Cor FunctionVariable a , pen2str), \n(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} , pen2str), \n(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) , pen2str)]"
1.33 = itms |> I_Model.to_string @{context}
1.34 (*+*)val 8 = length itms
1.35 (*+*)val 8 = length model