Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/biegelinie-4.sml
author wneuper <Walther.Neuper@jku.at>
Sun, 27 Aug 2023 11:19:14 +0200
changeset 60739 78a78f428ef8
parent 60736 7297c166991e
child 60752 77958bc6ed7d
permissions -rw-r--r--
followup 1 (to PIDE turn 11a): eliminate penv

Note: this was the buggy predecessor of env_subst and env_eval. 
     1 (* "Knowledge/biegelinie-4.sml"

     2    author: Walther Neuper 190515

     3    (c) due to copyright terms

     4 *)

     5 "table of contents ---------------------------------------------------------------------------";

     6 "---------------------------------------------------------------------------------------------";

     7 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";

     8 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' with ALL subproblems -----------";

     9 "----------- biegel Bsp.7.70. check Problem + MethodC model ----------------------------------";

    10 "---------------------------------------------------------------------------------------------";

    11 "---------------------------------------------------------------------------------------------";

    12 "---------------------------------------------------------------------------------------------";

    13 

    14 

    15 (** -------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ---- **)

    16 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";

    17 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";

    18 (* the error in this test might be independent from introduction of y, dy

    19    as arguments in IntegrierenUndKonstanteBestimmen2,

    20    rather due to so far untested use of "auto"

    21 ----------------------------------------------------------------------------------------------* )

    22 val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

    23 	     "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

    24 	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

    25        "AbleitungBiegelinie dy"];

    26 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);

    27 

    28 States.reset ();

    29 CalcTree @{context} [(fmz, (dI',pI',mI'))];                                     

    30 Iterator 1;

    31 moveActiveRoot 1;

    32 autoCalculate 1 CompleteCalc;

    33 

    34 val ((pt, p),_) = States.get_calc 1;

    35 if p = ([], Pbl) then () else error ""

    36 get_obj I pt (fst p); (*TODO investigate failure*)

    37 

    38 (* NOTE: \<up> \<up> \<up> \<up> \<up> ^^ no progress already in isabisac15, but not noticed \<up> \<up> \<up> \<up> \<up> ^^ * )

    39 (*[], Met*)autoCalculate 1 CompleteCalcHead;

    40 (*[1], Pbl*)autoCalculate 1 (Steps 1); (* into SubProblem *)

    41 (*[1], Res*)autoCalculate 1 CompleteSubpbl; (**)

    42 (*[2], Pbl*)autoCalculate 1 (Steps 1); (* out of SubProblem *)

    43 (*[2], Res*)autoCalculate 1 CompleteSubpbl;

    44 (*[3], Pbl*)autoCalculate 1 (Steps 1); (* out of SubProblem *)

    45 (*[3], Met*)autoCalculate 1 CompleteCalcHead;

    46 (*[3, 1], Frm*)autoCalculate 1 (Steps 1); (* solve SubProblem *)

    47 (*(**)autoCalculate 1 CompleteSubpbl;  error in kernel 4: Step.add: not impl.for Empty_Tac_*)

    48 (*[3, 1], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)

    49 (*[3, 2], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)

    50 (*[3, 3], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)

    51 (*[3, 4], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)

    52 (*[3, 5], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)

    53 (*[3, 6], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)

    54 (*[3, 7], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)

    55 (*[3, 8], Pbl*)autoCalculate 1 (Steps 1); (* solve SubProblem *)

    56 (*[3, 8], Met*)autoCalculate 1 CompleteCalcHead;

    57 (*[3, 8, 1], Frm*)autoCalculate 1 (Steps 1); (* solve SubProblem *)

    58 (*[3, 8, 1], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)

    59 (*(**)autoCalculate 1 (Steps 1); 

    60 *** Step.add: not impl.for Empty_Tac_ 

    61 val it = <AUTOCALC><CALCID>1</CALCID><CALCMESSAGE>helpless</CALCMESSAGE></AUTOCALC>: XML.tree *)

    62 

    63 val ((pt,_),_) = States.get_calc 1;

    64 val ip = States.get_pos 1 1;

    65 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);

    66 

    67 if ip = ([3, 8, 1], Res) andalso 

    68 UnparseC.term @{context} f = "[- 1 * c_4 / - 1 = 0,\n (6 * c_4 * EI + 6 * L * c_3 * EI + -3 * L \<up> 2 * c_2 + - 1 * L \<up> 3 * c) /\n (6 * EI) =\n L \<up> 4 * q_0 / (- 24 * EI),\n c_2 = 0, c_2 + L * c = L \<up> 2 * q_0 / 2]"

    69 then 

    70   case tac of

    71     SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => ()

    72   | _ => error "ERROR biegel.7.70 changed 1"

    73 else error "ERROR biegel.7.70 changed 2";

    74 ( * NOTE: \<up> \<up> \<up> \<up> \<up> ^^ no progress already in isabisac15, but not noticed \<up> \<up> \<up> \<up> \<up> ^^ *)

    75 ----------------------------------------------------------------------------------------------*)

    76 

    77 

    78 (** -------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' with ALL subproblems --------- **)

    79 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' with ALL subproblems -----------";

    80 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' with ALL subproblems -----------";

    81 

    82 val (tac as Model_Problem (*["Biegelinien"]*), (pt, p as ([], Pbl))) =

    83 Test_Code.init_calc' @{context} [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

    84 	    "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

    85 (*

    86   Now follow items for ALL SubProblems,

    87   since ROOT MethodC must provide values for "actuals" of ALL SubProblems.

    88   See Biegelinie.thy subsection \<open>Survey on Methods\<close>.

    89 *)

    90 (*

    91   Items for MethodC "IntegrierenUndKonstanteBestimmen2"

    92 *)

    93 	    "FunktionsVariable x",

    94     (*"Biegelinie y",          ..already input for Problem above*)

    95       "AbleitungBiegelinie dy",

    96       "Biegemoment M_b",

    97       "Querkraft Q",

    98 (*

    99   Item for Problem "LINEAR/system", which by [''no_met''] involves refinement

   100 *)

   101       "GleichungsVariablen [c, c_2, c_3, c_4]"

   102 ],

   103 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]

   104 

   105 (* 

   106   Legend:

   107   the indentation follows subsection \<open>Survey on Methods\<close> in Biegelinie.thy.

   108   The structure of the calculation below is made explicit in the following way:

   109 

   110   |create I_Model of root Problem from Formalise.model

   111   |check 3 Formalise.refs

   112   |create I_Model of root MethodC, ending by Apply_Method 

   113 

   114     |create I_Model of SubProblem from arguments, given values by the Program of the root

   115     |check 3 Formalise.refs

   116     |create I_Model of SubProblem's MethodC, ending either by

   117     |  Apply_Method of respective SubProblem

   118     |  or

   119     |  Check_Postcond of Problem and return to respective parent

   120 

   121   Note: Programs immediately calling a SubProblem, does (not yet) indicate

   122     this SubProblem as separate Step.

   123 *)

   124 

   125   val (tac as Apply_Method ["IntegrierenUndKonstanteBestimmen2"], (pt, p as ([], Met))) =

   126   (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'

   127   (*---broken elementwise input to lists---* ) |> me' ( *---broken elementwise input to lists---*)

   128   |> me' |> me' |> me'

   129 

   130     (*INVISIBLE: tac as SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)

   131     val (tac as Apply_Method ["Biegelinien", "ausBelastung"], (pt, p as ([1], Met))) =

   132     (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' 

   133     |> me'

   134     val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 2], Res))) =

   135     (tac, (pt, p)) |> me' |> me' |> me'

   136 

   137       val (tac as Apply_Method ["diff", "integration", "named"], (pt, p as ([1, 3], Met))) =

   138       (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'

   139       val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p)) =

   140       (tac, (pt, p)) |> me' |> me' |> me'

   141 

   142     val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 4], Res))) =

   143     (tac, (pt, p)) |> me' |> me'

   144 

   145       val (tac as Apply_Method ["diff", "integration", "named"], (pt, p as ([1, 5], Met))) =

   146       (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'

   147       val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 5, 1], Res))) =

   148       (tac, (pt, p)) |> me' |> me'

   149 

   150     val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 7], Res))) =

   151     (tac, (pt, p)) |> me' |> me' |> me'

   152 

   153       val (tac as Apply_Method ["diff", "integration", "named"], (pt, p as ([1, 8], Met))) =

   154       (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'

   155       val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 8, 2], Res))) =

   156       (tac, (pt, p)) |> me' |> me' |> me'

   157 

   158     val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p)) =

   159     (tac, (pt, p)) |> me'

   160 

   161       val (tac as Apply_Method ["diff", "integration", "named"], (pt, p as ([1, 9], Met))) =

   162       (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'

   163       val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p)) =

   164       (tac, (pt, p)) |> me' |> me'

   165 

   166     val (tac as Check_Postcond ["vonBelastungZu", "Biegelinien"], (pt, p as ([1, 9], Res))) =

   167     (tac, (pt, p)) |> me'

   168 

   169   val (tac as Subproblem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"]), (pt, p as ([1], Res))) =

   170   (tac, (pt, p)) |> me'

   171 

   172     val (tac as Apply_Method ["Biegelinien", "setzeRandbedingungenEin"], (pt, p as ([2], Met))) =

   173     (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'

   174 

   175       (*INVISIBLE: tac as SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''])*)

   176       val (tac as Apply_Method ["Equation", "fromFunction"], (pt, p as ([2, 1], Met))) =

   177       (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'

   178       val (tac as Check_Postcond ["makeFunctionTo", "equation"], (pt, p)) =

   179       (tac, (pt, p)) |> me' |> me' |> me' |> me'

   180 

   181     val (tac as Subproblem ("Biegelinie", ["makeFunctionTo", "equation"]), (pt, p as ([2, 1], Res))) =

   182     (tac, (pt, p)) |> me'

   183 val "0 = - 1 * c_4 / - 1" = Calc.current_formula (pt, p) |> UnparseC.term @{context};

   184 (*--^^^^^^^^^^^^^^^^^^^^^ requires improved simplification*)

   185 

   186 (** -------- biegel Bsp.7.70. check Problem + MethodC model -------------------------------- **)

   187 "----------- biegel Bsp.7.70. check Problem + MethodC model ----------------------------------";

   188 "----------- biegel Bsp.7.70. check Problem + MethodC model ----------------------------------";

   189 (*this formalisation contains no variants, as opposed to maximum example*)

   190 val (tac as Model_Problem (*["Biegelinien"]*), ptp as (pt, p as ([], Pbl))) =

   191 Test_Code.init_calc' @{context} [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

   192 	    "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

   193 (*

   194   Now follow items for ALL SubProblems,

   195   since ROOT MethodC must provide values for "actuals" of ALL SubProblems.

   196   See Biegelinie.thy subsection \<open>Survey on Methods\<close>.

   197 *)

   198 (*

   199   Items for MethodC "IntegrierenUndKonstanteBestimmen2"

   200 *)

   201 	    "FunktionsVariable x",

   202     (*"Biegelinie y",          ..already input for Problem above*)

   203       "AbleitungBiegelinie dy",

   204       "Biegemoment M_b",

   205       "Querkraft Q",

   206 (*

   207   Item for Problem "LINEAR/system", which by [''no_met''] involves refinement

   208 *)

   209       "GleichungsVariablen [c, c_2, c_3, c_4]"

   210 ],

   211 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]

   212 

   213 (*** stepwise Specification: Problem model================================================= ***)

   214 val ("ok", ([(Model_Problem, _, _)], _, ptp))

   215   = Step.specify_do_next ptp;

   216 val ("ok", ([(Add_Given "Traegerlaenge L", _, _)], _, ptp))

   217   = Step.specify_do_next ptp;

   218 val ("ok", ([(Add_Given "Streckenlast q_0", _, _)], _, ptp))

   219   = Step.specify_do_next ptp;

   220 val ("ok", ([(Add_Find "Biegelinie y", _, _)], _, ptp))

   221   = Step.specify_do_next ptp;

   222 val ("ok", ([(Add_Relation "Randbedingungen [y 0 = 0]", _, _)], _, ptp))

   223   = Step.specify_do_next ptp;

   224 val ("ok", ([(Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]", _, _)], _, ptp))

   225   = Step.specify_do_next ptp;

   226 

   227 (*** Problem model is complete ============================================================ ***)

   228 val PblObj {probl, ...} = get_obj I (fst ptp) [];

   229 (*WN230827 adaptation too time consuming* )

   230 if I_Model.to_string @{context} probl = "[\n" ^

   231   "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^

   232   "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

   233   "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^

   234   "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]))]"

   235 then () else error "I_Model.to_string probl CHANGED";

   236 ( *WN230827 adaptation too time consuming*)

   237 

   238 (*** Specification of References ========================================================== ***)

   239 val ("ok", ([(Specify_Theory "Biegelinie", _, _)], _, ptp))

   240   = Step.specify_do_next ptp;

   241 val ("ok", ([(Specify_Problem ["Biegelinien"], _, _)], _, ptp))

   242   = Step.specify_do_next ptp;

   243 val ("ok", ([(Specify_Method ["IntegrierenUndKonstanteBestimmen2"], _, _)], _, ptp))

   244   = Step.specify_do_next ptp;

   245 

   246 (*** stepwise Specification: MethodC model ================================================ ***)

   247 val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], _, ptp))

   248   = Step.specify_do_next ptp;

   249 val ("ok", ([(Add_Given "AbleitungBiegelinie dy", _, _)], _, ptp))

   250   = Step.specify_do_next ptp;

   251 val ("ok", ([(Add_Given "Biegemoment M_b", _, _)], _, ptp))

   252   = Step.specify_do_next ptp;

   253 val ("ok", ([(Add_Given "Querkraft Q", _, _)], _, ptp))

   254   = Step.specify_do_next ptp;

   255 val ("ok", ([(Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]", _, _)], _, ptp))

   256   = Step.specify_do_next ptp;

   257 

   258 (*** Specification of Problem and MethodC model is completes ============================== ***)

   259 val PblObj {meth, ...} = get_obj I (fst ptp) [];

   260 if I_Model.to_string @{context} meth = "[\n" ^

   261   "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^

   262   "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^

   263   "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^

   264   "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^

   265   "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x , pen2str), \n" ^

   266   "(6 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy , pen2str), \n" ^

   267   "(7 ,[1] ,true ,#Given ,Cor Biegemoment M_b , pen2str), \n" ^

   268   "(8 ,[1] ,true ,#Given ,Cor Querkraft Q , pen2str), \n" ^

   269   "(9 ,[1] ,true ,#Given ,Cor GleichungsVariablen [c, c_2, c_3, c_4] , pen2str)]"

   270 then () else error "I_Model.to_string meth CHANGED";

   271 

   272 (*** Solution starts ====================================================================== ***)

   273 val ("ok", ([(Apply_Method ["IntegrierenUndKonstanteBestimmen2"], _, _)], _, ptp))

   274   = Step.specify_do_next ptp;
wneuper/isa