# HG changeset patch # User wneuper # Date 1628511620 -7200 # Node ID 600952fb4724be79301b754ca3cb9deab0cde0d4 # Parent a14022b99b92052535f9ca4b78e1be79e225d260 eliminate ThyC.to_ctxt done except 1 error diff -r a14022b99b92 -r 600952fb4724 TODO.md --- a/TODO.md Mon Aug 09 11:19:25 2021 +0200 +++ b/TODO.md Mon Aug 09 14:20:20 2021 +0200 @@ -63,10 +63,10 @@ - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun'); - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation); -* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation, DONE partially; - + TOODOO are exclusive for this changeset; most follow from TOODOO.1 - + TOODOO.1: exception TYPE raised by Skip_Proof.make_thm - + ? how to do algebraic operations on numerals ? Presburger ? simplifier ? +* WN: eliminate ThmC.numerals_to_Free, done except 1 error: + + exception TYPE raised by Skip_Proof.make_thm, several inherited errors in tests marked TOODOO.1 + + ? how do algebraic operations on numerals ? Presburger ? simplifier ? hack see + https://hg.risc.uni-linz.ac.at/wneuper/isa/file/a14022b99b92/src/Tools/isac/ProgLang/evaluate.sml#l210 * WN: DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art), partially; Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too) diff -r a14022b99b92 -r 600952fb4724 test/Tools/isac/Knowledge/integrate.sml --- a/test/Tools/isac/Knowledge/integrate.sml Mon Aug 09 11:19:25 2021 +0200 +++ b/test/Tools/isac/Knowledge/integrate.sml Mon Aug 09 14:20:20 2021 +0200 @@ -172,6 +172,7 @@ "----------- simplify by ruleset reducing make_ratpoly_in"; "----------- simplify by ruleset reducing make_ratpoly_in"; val thy = @{theory "Isac_Knowledge"}; +val subst = [(TermC.str2term "bdv ::real", TermC.str2term "x ::real")]; (*DOESN'T HELP*) "===== test 1"; val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \ 2 / 2)"; @@ -183,23 +184,15 @@ "===== test 2"; val rls = order_add_mult_in; -(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\ - assume flawed test setup hidden by "handle _ => ..." - ERROR ord_make_polynomial_in called with subst = [] -val SOME (t,[]) = rewrite_set_ thy true rls t; +val SOME (t, []) = rewrite_set_inst_ thy true subst rls t; if UnparseC.term t = "1 / EI * (L * (q_0 * x) / 2 + - 1 * (q_0 * x \ 2) / 2)" then() else error "integrate.sml simplify by ruleset order_add_mult_in #2"; - \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----//*) "===== test 3"; val rls = discard_parentheses; -(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\ - assume flawed test setup hidden by "handle _ => ..." - ERROR ord_make_polynomial_in called with subst = [] -val SOME (t,[]) = rewrite_set_ thy true rls t; +val SOME (t, []) = rewrite_set_ thy true rls t; if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \ 2 / 2)" then () else error "integrate.sml simplify by ruleset discard_parenth.. #3"; - \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO//*) "===== test 4"; val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")]; diff -r a14022b99b92 -r 600952fb4724 test/Tools/isac/ProgLang/evaluate.sml --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Aug 09 11:19:25 2021 +0200 +++ b/test/Tools/isac/ProgLang/evaluate.sml Mon Aug 09 14:20:20 2021 +0200 @@ -22,6 +22,7 @@ "----------- calculate (2 * x is_const) -----------------"; "----------- fun get_pair: examples ------------------------------------------------------------"; "----------- fun adhoc_thm: examples -----------------------------------------------------------"; +"----------- fun adhoc_thm \ exception TYPE --------------------------------------------------"; "----------- fun power -------------------------------------------------------------------------"; "----------- fun divisors ----------------------------------------------------------------------"; "----------- fun doubles, fun squfact ----------------------------------------------------------"; @@ -459,8 +460,8 @@ "----------- fun adhoc_thm \ exception TYPE --------------------------------------------------"; val t = TermC.str2term "sqrt 4"; -(* TOODOO.1: exception TYPE raised by Skip_Proof.make_thm * ) - exception TYPE raised (line 169 of "consts.ML"): Illegal type +(* error-from-Skip_Proof.make_thm: inherited errors are marked TOODOO.1 in test/* + exception TYPE raised (line 169 of "consts.ML"): Illegal type for constant "HOL.eq" :: real \ (num \ real) \ bool (**) Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t ( **) diff -r a14022b99b92 -r 600952fb4724 test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Mon Aug 09 11:19:25 2021 +0200 +++ b/test/Tools/isac/Test_Some.thy Mon Aug 09 14:20:20 2021 +0200 @@ -111,498 +111,9 @@ \ ML \ \ -section \========== check integrate.sml ====================================================\ +section \===================================================================================\ ML \ \ ML \ -(* Title: test/Tools/isac/Knowledge/integrate.sml - Author: Walther Neuper 050826 - (c) due to copyright terms -*) -"--------------------------------------------------------"; -"table of contents --------------------------------------"; -"--------------------------------------------------------"; -"----------- parsing ------------------------------------"; -"----------- integrate by rewriting ---------------------"; -"----------- test add_new_c, TermC.is_f_x ---------------------"; -"----------- simplify by ruleset reducing make_ratpoly_in"; -"----------- integrate by ruleset -----------------------"; -"----------- rewrite 3rd integration in 7.27 ------------"; -"----------- check probem type --------------------------"; -"----------- me method [diff,integration] ---------------"; -"----------- autoCalculate [diff,integration] -----------"; -"----------- me method [diff,integration,named] ---------"; -"----------- me met [diff,integration,named] Biegelinie.Q"; -"----------- method analog to rls 'integration' ---------"; -"--------------------------------------------------------"; -"--------------------------------------------------------"; -"--------------------------------------------------------"; - -(*these val/fun provide for exact parsing in Integrate.thy, not Isac.thy; -they are used several times below; TODO remove duplicates*) -val thy = @{theory "Integrate"}; -val ctxt = ThyC.to_ctxt thy; - -fun str2t str = parseNEW ctxt str |> the; -fun term2s t = UnparseC.term_in_ctxt ctxt t; - -val conditions_in_integration_rules = - Rule_Set.Repeat {id="conditions_in_integration_rules", - preconds = [], - rew_ord = ("termlessI",termlessI), - erls = Rule_Set.Empty, - srls = Rule_Set.Empty, calc = [], errpatts = [], - rules = [(*for rewriting conditions in Thm's*) - Eval ("Prog_Expr.occurs_in", - eval_occurs_in "#occurs_in_"), - Thm ("not_true", @{thm not_true}), - Thm ("not_false", @{thm not_false})], - scr = Empty_Prog}; -val subs = [(str2t "bdv::real", str2t "x::real")]; -fun rewrit thm str = - fst (the (rewrite_inst_ thy tless_true - conditions_in_integration_rules - true subs thm str)); - - -"----------- parsing ------------------------------------"; -"----------- parsing ------------------------------------"; -"----------- parsing ------------------------------------"; -val t = TermC.str2term "Integral x D x"; -val t = TermC.str2term "Integral x \ 2 D x"; -case t of - Const (\<^const_name>\Integral\, _) $ - (Const (\<^const_name>\powr\, _) $ Free _ $ _) $ Free ("x", _) => () - | _ => error "integrate.sml: parsing: Integral x \ 2 D x"; - -val t = TermC.str2term "ff x is_f_x"; -case t of Const (\<^const_name>\is_f_x\, _) $ _ => () - | _ => error "integrate.sml: parsing: ff x is_f_x"; - - -"----------- integrate by rewriting ---------------------"; -"----------- integrate by rewriting ---------------------"; -"----------- integrate by rewriting ---------------------"; -val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral 1 D x"); -if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x"; - -val str = rewrit @{thm "integral_const"} (TermC.str2term "Integral M'/EJ D x"); -if term2s str = "M' / EJ * x" then () -else error "Integral M'/EJ D x BY integral_const"; - -val str = rewrit @{thm "integral_var"} (TermC.str2term "Integral x D x"); -if term2s str = "x \ 2 / 2" then () -else error "Integral x D x BY integral_var"; - -val str = rewrit @{thm "integral_add"} (TermC.str2term "Integral x + 1 D x"); -if term2s str = "Integral x D x + Integral 1 D x" then () -else error "Integral x + 1 D x BY integral_add"; - -val str = rewrit @{thm "integral_mult"} (TermC.str2term "Integral M'/EJ * x \ 3 D x"); -if term2s str = "M' / EJ * Integral x \ 3 D x" then () -else error "Integral M'/EJ * x \ 3 D x BY integral_mult"; - -val str = rewrit @{thm "integral_pow"} (TermC.str2term "Integral x \ 3 D x"); -if term2s str = "x \ (3 + 1) / (3 + 1)" then () -else error "integrate.sml Integral x \ 3 D x"; - - -"----------- test add_new_c, TermC.is_f_x ---------------------"; -"----------- test add_new_c, TermC.is_f_x ---------------------"; -"----------- test add_new_c, TermC.is_f_x ---------------------"; -val term = TermC.str2term "x \ 2 * c + c_2"; -val cc = new_c term; -if UnparseC.term cc = "c_3" then () else error "integrate.sml: new_c ???"; - -val SOME (id,t') = eval_add_new_c "" "Integrate.add_new_c" term thy; -if UnparseC.term t' = "x \ 2 * c + c_2 = x \ 2 * c + c_2 + c_3" then () -else error "intergrate.sml: diff. eval_add_new_c"; - -val cc = ("Integrate.add_new_c", eval_add_new_c "add_new_c_"); -val SOME (thmstr, thm) = adhoc_thm1_ thy cc term; - -val SOME (t',_) = rewrite_set_ thy true add_new_c term; -if UnparseC.term t' = "x \ 2 * c + c_2 + c_3" then () -else error "intergrate.sml: diff. rewrite_set add_new_c 1"; - -val term = TermC.str2term "ff x = x \ 2*c + c_2"; -val SOME (t',_) = rewrite_set_ thy true add_new_c term; -if UnparseC.term t' = "ff x = x \ 2 * c + c_2 + c_3" then () -else error "intergrate.sml: diff. rewrite_set add_new_c 2"; - - -(*WN080222 replace call_new_c with add_new_c---------------------- -val term = str2t "new_c (c * x \ 2 + c_2)"; -val SOME (_,t') = eval_new_c 0 0 term 0; -if term2s t' = "new_c c * x \ 2 + c_2 = c_3" then () -else error "integrate.sml: eval_new_c ???"; - -val t = str2t "matches (?u + new_c ?v) (x \ 2 / 2)"; -val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t'; -if term2s t' = "matches (?u + new_c ?v) (x \ 2 / 2) = False" then () -else error "integrate.sml: matches new_c = False"; - -val t = str2t "matches (?u + new_c ?v) (x \ 2 / 2 + new_c x \ 2 / 2)"; -val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t'; -if term2s t'="matches (?u + new_c ?v) (x \ 2 / 2 + new_c x \ 2 / 2) = True" -then () else error "integrate.sml: matches new_c = True"; - -val t = str2t "ff x TermC.is_f_x"; -val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t'; -if term2s t' = "(ff x TermC.is_f_x) = True" then () -else error "integrate.sml: eval_is_f_x --> true"; - -val t = str2t "q_0/2 * L * x TermC.is_f_x"; -val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t'; -if term2s t' = "(q_0 / 2 * L * x TermC.is_f_x) = False" then () -else error "integrate.sml: eval_is_f_x --> false"; - -val conditions_in_integration = -Rule_Set.Repeat {id="conditions_in_integration", - preconds = [], - rew_ord = ("termlessI",termlessI), - erls = Rule_Set.Empty, - srls = Rule_Set.Empty, calc = [], errpatts = [], - rules = [Eval ("Prog_Expr.matches",eval_matches ""), - Eval ("Integrate.is_f_x", - eval_is_f_x "is_f_x_"), - Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}), - Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}) - ], - scr = Empty_Prog}; -fun rewrit thm t = - fst (the (rewrite_inst_ thy tless_true - conditions_in_integration true subs thm t)); -val t = rewrit call_for_new_c (str2t "x \ 2 / 2"); term2s t; -val t = (rewrit call_for_new_c t) - handle OPTION => str2t "no_rewrite"; - -val t = rewrit call_for_new_c - (str2t "ff x = q_0/2 *L*x"); term2s t; -val t = (rewrit call_for_new_c - (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x")) - handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite"; ---------------------------------------------------------------------*) - - -"----------- simplify by ruleset reducing make_ratpoly_in"; -"----------- simplify by ruleset reducing make_ratpoly_in"; -"----------- simplify by ruleset reducing make_ratpoly_in"; -\ ML \ -val subst = [(TermC.str2term "bdv ::real", TermC.str2term "x ::real")] -\ ML \ -val thy = @{theory "Isac_Knowledge"}; -"===== test 1"; -val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \ 2 / 2)"; - -"----- stepwise from the rulesets in simplify_Integral and below-----"; -val rls = norm_Rational_noadd_fractions; -case rewrite_set_inst_ thy true subs rls t of - SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2" - | NONE => (); - -"===== test 2"; -\ ML \ -val rls = order_add_mult_in; -\ text \ (*GOON*) -(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\*) - assume flawed test setup hidden by "handle _ => ..." - ERROR ord_make_polynomial_in called with subst = [] -\ text \ -val SOME (t, []) = rewrite_set_ thy true rls t; - -UnparseC.term t - -if UnparseC.term t = "1 / EI * (L * (q_0 * x) / 2 + - 1 * (q_0 * x \ 2) / 2)" then() -else error "integrate.sml simplify by ruleset order_add_mult_in #2"; -(*\\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----//*) - -"===== test 3"; -\ ML \ -val rls = discard_parentheses; -(*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\ - assume flawed test setup hidden by "handle _ => ..." - ERROR ord_make_polynomial_in called with subst = [] -val SOME (t,[]) = rewrite_set_ thy true rls t; -if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \ 2 / 2)" then () -else error "integrate.sml simplify by ruleset discard_parenth.. #3"; - \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO//*) - -"===== test 4"; -val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")]; -val rls = - (Rule_Set.append_rules "separate_bdv" collect_bdv - [Thm ("separate_bdv", @{thm separate_bdv}), - (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) - Thm ("separate_bdv_n", @{thm separate_bdv_n}), - (*"?a * ?bdv \ ?n / ?b = ?a / ?b * ?bdv \ ?n"*) - Thm ("separate_1_bdv", @{thm separate_1_bdv}), - (*"?bdv / ?b = (1 / ?b) * ?bdv"*) - Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n}) - (*"?bdv \ ?n / ?b = 1 / ?b * ?bdv \ ?n"*) - ]); -(*show_types := true; --- do we need type-constraint in thms? *) -@{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*) -@{thm separate_bdv_n}; (*::real ..because of \ , rewrites*) -@{thm separate_1_bdv}; (*::?'a*) -val xxx = @{thm separate_1_bdv}; (*::?'a*) -@{thm separate_1_bdv_n}; (*::real ..because of \ *) -(*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*) - -val SOME (t, []) = rewrite_set_inst_ thy true subs rls t; -if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \ 2)" then () -else error "integrate.sml simplify by ruleset separate_bdv.. #4"; - -"===== test 5"; -val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \ 2 / 2)"; -val rls = simplify_Integral; -val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t; -(* given was: "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \ 2 / 2)" *) -if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \ 2)" then () -else error "integrate.sml, simplify_Integral #99"; - -"........... 2nd integral ........................................"; -"........... 2nd integral ........................................"; -"........... 2nd integral ........................................"; -val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")]; - -val thy = @{theory Biegelinie}; -val t = TermC.str2term - "Integral 1 / EI * (L * q_0 / 2 * (x \ 2 / 2) + - 1 * q_0 / 2 * (x \ 3 / 3)) D x"; - -val rls = simplify_Integral; -val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t; -if UnparseC.term t = "Integral 1 / EI * (L * q_0 / 4 * x \ 2 + - 1 * q_0 / 6 * x \ 3) D x" -then () else raise error "integrate.sml, simplify_Integral #198"; - -val rls = integration_rules; -val SOME (t, []) = rewrite_set_ thy true rls t; -if UnparseC.term t = "1 / EI * (L * q_0 / 4 * (x \ 3 / 3) + - 1 * q_0 / 6 * (x \ 4 / 4))" -then () else error "integrate.sml, simplify_Integral #199"; - - -"----------- integrate by ruleset -----------------------"; -"----------- integrate by ruleset -----------------------"; -"----------- integrate by ruleset -----------------------"; -val thy = @{theory "Integrate"}; -val rls = integration_rules; -val subs = [(@{term "bdv::real"}, @{term "x::real"})]; -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*) - -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral x D x"; -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; -if UnparseC.term res = "x \ 2 / 2" then () else error "Integral x D x changed"; - -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \ 2 + c_2 D x"; -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; -if UnparseC.term res = "c * (x \ 3 / 3) + c_2 * x" then () else error "Integral c * x \ 2 + c_2 D x"; - -val rls = add_new_c; -val t = (Thm.term_of o the o (TermC.parse thy)) "c * (x \ 3 / 3) + c_2 * x"; -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; -if UnparseC.term res = "c * (x \ 3 / 3) + c_2 * x + c_3" then () -else error "integrate.sml: diff.behav. in add_new_c simpl."; - -val t = (Thm.term_of o the o (TermC.parse thy)) "F x = x \ 3 / 3 + x"; -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; -if UnparseC.term res = "F x = x \ 3 / 3 + x + c"(*not "F x + c =..."*) then () -else error "integrate.sml: diff.behav. in add_new_c equation"; - -val rls = simplify_Integral; -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*) -val t = (Thm.term_of o the o (TermC.parse thy)) "ff x = c * x + - 1 * q_0 * (x \ 2 / 2) + c_2"; -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; -if UnparseC.term res = "ff x = c_2 + c * x + - 1 * q_0 / 2 * x \ 2" -then () else error "integrate.sml: diff.behav. in simplify_I #1"; - -val rls = integration; -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*) -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \ 2 + c_2 D x"; -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; -if UnparseC.term res = "c_3 + c_2 * x + c / 3 * x \ 3" -then () else error "integrate.sml: diff.behav. in integration #1"; - -val t = (Thm.term_of o the o (TermC.parse thy)) "Integral 3*x \ 2 + 2*x + 1 D x"; -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; -if UnparseC.term res = "c + x + x \ 2 + x \ 3" then () -else error "integrate.sml: diff.behav. in integration #2"; - -val t = (Thm.term_of o the o (TermC.parse thy)) - "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \ 2) D x"; -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; -"Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \ 2) D x"; -if UnparseC.term res = "c + 1 / EI * (L * q_0 / 4 * x \ 2 + - 1 * q_0 / 6 * x \ 3)" -then () else error "integrate.sml: diff.behav. in integration #3"; - -val t = (Thm.term_of o the o (TermC.parse thy)) ("Integral " ^ UnparseC.term res ^ " D x"); -val SOME (res, _) = rewrite_set_inst_ thy true subs rls t; -if UnparseC.term res = "c_2 + c * x +\n1 / EI * (L * q_0 / 12 * x \ 3 + - 1 * q_0 / 24 * x \ 4)" -then () else error "integrate.sml: diff.behav. in integration #4"; - -"----------- rewrite 3rd integration in 7.27 ------------"; -"----------- rewrite 3rd integration in 7.27 ------------"; -"----------- rewrite 3rd integration in 7.27 ------------"; -val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*); -val t = TermC.str2term "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \ 2) / 2) D x"; -val SOME(t, _)= rewrite_set_inst_ thy true subs simplify_Integral t; -if UnparseC.term t = - "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \ 2) D x" -then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral"; - -val SOME(t, _) = rewrite_set_inst_ thy true subs integration t; -if UnparseC.term t = - "c + 1 / EI * (L * q_0 / 4 * x \ 2 + - 1 * q_0 / 6 * x \ 3)" -then () else error "integrate.sml 3rd integration in 7.27, integration"; - - -"----------- check probem type --------------------------"; -"----------- check probem type --------------------------"; -"----------- check probem type --------------------------"; -val thy = @{theory Integrate}; -val model = {Given =["functionTerm f_f", "integrateBy v_v"], - Where =[], - Find =["antiDerivative F_F"], - With =[], - Relate=[]}:string ppc; -val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model; -val t1 = (Thm.term_of o hd) chkmodel; -val t2 = (Thm.term_of o hd o tl) chkmodel; -val t3 = (Thm.term_of o hd o tl o tl) chkmodel; -case t3 of Const (\<^const_name>\antiDerivative\, _) $ _ => () - | _ => error "integrate.sml: Integrate.antiDerivative ???"; - -val model = {Given =["functionTerm f_f", "integrateBy v_v"], - Where =[], - Find =["antiDerivativeName F_F"], - With =[], - Relate=[]}:string ppc; -val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model; -val t1 = (Thm.term_of o hd) chkmodel; -val t2 = (Thm.term_of o hd o tl) chkmodel; -val t3 = (Thm.term_of o hd o tl o tl) chkmodel; -case t3 of Const (\<^const_name>\antiDerivativeName\, _) $ _ => () - | _ => error "integrate.sml: Integrate.antiDerivativeName"; - -"----- compare 'Find's from problem, script, formalization -------"; -val {ppc,...} = Problem.from_store ["named", "integrate", "function"]; -val ("#Find", (Const (\<^const_name>\antiDerivativeName\, _), - F1_ as Free ("F_F", F1_type))) = last_elem ppc; -val {scr = Prog sc,... } = MethodC.from_store ["diff", "integration", "named"]; -val [_,_, F2_] = formal_args sc; -if F1_ = F2_ then () else error "integrate.sml: unequal find's"; - -val ((dsc as Const (\<^const_name>\antiDerivativeName\, _)) - $ Free ("ff", F3_type)) = TermC.str2term "antiDerivativeName ff"; -if Input_Descript.is_a dsc then () else error "integrate.sml: no description"; -if F1_type = F3_type then () -else error "integrate.sml: unequal types in find's"; - -Test_Tool.show_ptyps(); -val pbl = Problem.from_store ["integrate", "function"]; -case #cas pbl of SOME (Const (\<^const_name>\Integrate\, _) $ _) => () - | _ => error "integrate.sml: Integrate.Integrate ???"; - - -"----------- me method [diff,integration] ---------------"; -"----------- me method [diff,integration] ---------------"; -"----------- me method [diff,integration] ---------------"; -(*exp_CalcInt_No- 1.xml*) -val p = e_pos'; val c = []; -"----- step 0: returns nxt = Model_Problem ---"; -val (p,_,f,nxt,_,pt) = - CalcTreeTEST - [(["functionTerm (x \ 2 + 1)", "integrateBy x", "antiDerivative FF"], - ("Integrate", ["integrate", "function"], ["diff", "integration"]))]; -"----- step 1: returns nxt = Add_Given \"functionTerm (x \ 2 + 1)\" ---"; -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*) -"----- step 2: returns nxt = Add_Given \"integrateBy x\" ---"; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---"; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"----- step 4: returns nxt = Specify_Theory \"Integrate\" ---"; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---"; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---"; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -"----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---"; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -case nxt of (Apply_Method ["diff", "integration"]) => () - | _ => error "integrate.sml -- me method [diff,integration] -- spec"; -"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")"; -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; -if f2str f = "c + x + 1 / 3 * x \ 3" then () -else error "integrate.sml -- me method [diff,integration] -- end"; - - -"----------- autoCalculate [diff,integration] -----------"; -"----------- autoCalculate [diff,integration] -----------"; -"----------- autoCalculate [diff,integration] -----------"; -reset_states (); -CalcTree - [(["functionTerm (x \ 2 + 1)", "integrateBy x", "antiDerivative FF"], - ("Integrate", ["integrate", "function"], ["diff", "integration"]))]; -Iterator 1; -moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; @{make_string} p; Test_Tool.show_pt pt; -val (Form t,_,_) = ME_Misc.pt_extract (pt, p); -if UnparseC.term t = "c + x + 1 / 3 * x \ 3" then () -else error "integrate.sml -- interSteps [diff,integration] -- result"; - - -"----------- me method [diff,integration,named] ---------"; -"----------- me method [diff,integration,named] ---------"; -"----------- me method [diff,integration,named] ---------"; -(*exp_CalcInt_No- 2.xml*) -val fmz = ["functionTerm (x \ 2 + (1::real))", - "integrateBy x", "antiDerivativeName F"]; -val (dI',pI',mI') = - ("Integrate",["named", "integrate", "function"], - ["diff", "integration", "named"]); -val p = e_pos'; val c = []; -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *); -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*); -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; -if f2str f = "F x = c + x + 1 / 3 * x \ 3" then() -else error "integrate.sml: method [diff,integration,named]"; - - -"----------- me met [diff,integration,named] Biegelinie.Q"; -"----------- me met [diff,integration,named] Biegelinie.Q"; -"----------- me met [diff,integration,named] Biegelinie.Q"; -(*exp_CalcInt_No-3.xml*) -val fmz = ["functionTerm (- q_0)", - "integrateBy x", "antiDerivativeName Q"]; -val (dI',pI',mI') = - ("Biegelinie",["named", "integrate", "function"], - ["diff", "integration", "named"]); -val p = e_pos'; val c = []; -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -(*Error Tac Q not in ...*) -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *); -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*); -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; -if f2str f = "Q x = c + - 1 * q_0 * x" then() -else error "integrate.sml: method [diff,integration,named] .Q"; - - \ ML \ \ ML \ \