test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml
changeset 60739 78a78f428ef8
parent 60733 4097c1317986
child 60741 22586d7fedb0
     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