# HG changeset patch # User wneuper # Date 1619545949 -7200 # Node ID b987b05f1ca88ce9ab6f62c6e34f54d8f3d925bd # Parent 95bae6eeccfa158e72e50978657bbfea2f5ef596 eliminate "handle _ => ..." by more direct ML diff -r 95bae6eeccfa -r b987b05f1ca8 src/Tools/isac/BaseDefinitions/rewrite-order.sml --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml Tue Apr 27 18:14:02 2021 +0200 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml Tue Apr 27 19:52:29 2021 +0200 @@ -47,7 +47,7 @@ fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known") | assoc' ((keyi, xi) :: pairs, key) = if key = keyi then SOME xi else assoc' (pairs, key); -fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro)) - handle _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system"); +fun assoc_rew_ord ro = ((the o assoc') (! rew_ord', ro)) + handle ERROR _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system"); end \ No newline at end of file diff -r 95bae6eeccfa -r b987b05f1ca8 src/Tools/isac/BaseDefinitions/theoryC.sml --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Tue Apr 27 18:14:02 2021 +0200 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Tue Apr 27 19:52:29 2021 +0200 @@ -48,7 +48,7 @@ fun get_theory thy = if thy = "empty_thy_id" then (get_thy "Base_Tools") (*lower bound of Knowledge*) - else (get_thy thy) handle _ => raise ERROR ("ME_Isa: thy \"" ^ thy ^ "\" not in system"); + else (get_thy thy) handle ERROR _ => raise ERROR ("ME_Isa: thy \"" ^ thy ^ "\" not in system"); fun id_to_ctxt thy' = Proof_Context.init_global (get_theory thy'); fun to_ctxt thy = Proof_Context.init_global thy; diff -r 95bae6eeccfa -r b987b05f1ca8 src/Tools/isac/BridgeLibisabelle/present-tool.sml --- a/src/Tools/isac/BridgeLibisabelle/present-tool.sml Tue Apr 27 18:14:02 2021 +0200 +++ b/src/Tools/isac/BridgeLibisabelle/present-tool.sml Tue Apr 27 19:52:29 2021 +0200 @@ -75,9 +75,9 @@ (* make a guh from a reference to an element in the kestore; EXCEPT theory hierarchy ... compare 'fun keref2xml' *) fun pblID2guh pblID = (((#guh o Problem.from_store) pblID) - handle _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\"")); + handle ERROR _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\"")); fun metID2guh metID = (((#guh o MethodC.from_store) metID) - handle _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\"")); + handle ERROR _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\"")); fun kestoreID2guh Pbl_ kestoreID = pblID2guh kestoreID | kestoreID2guh Met_ kestoreID = metID2guh kestoreID | kestoreID2guh ketyp kestoreID = diff -r 95bae6eeccfa -r b987b05f1ca8 src/Tools/isac/Interpret/Interpret.thy --- a/src/Tools/isac/Interpret/Interpret.thy Tue Apr 27 18:14:02 2021 +0200 +++ b/src/Tools/isac/Interpret/Interpret.thy Tue Apr 27 19:52:29 2021 +0200 @@ -8,7 +8,6 @@ theory Interpret imports Specify.Specify begin -(* removed all warnings here, only "handle _" remains *) ML_file istate.sml ML_file "sub-problem.sml" ML_file "thy-read.sml" diff -r 95bae6eeccfa -r b987b05f1ca8 src/Tools/isac/Interpret/derive.sml --- a/src/Tools/isac/Interpret/derive.sml Tue Apr 27 18:14:02 2021 +0200 +++ b/src/Tools/isac/Interpret/derive.sml Tue Apr 27 19:52:29 2021 +0200 @@ -94,7 +94,7 @@ val _ = msg_5 t' val r' = Rule.Thm (thmid, tm) in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end) - handle _ => raise ERROR "derive_norm, Eval: no rewrite") + handle NO_REWRITE => raise ERROR "derive_norm, Eval: no rewrite") | Rule.Rls_ rls => (case Rewrite.rewrite_set_ thy true rls t of NONE => rew_once lim rts t apno rs' diff -r 95bae6eeccfa -r b987b05f1ca8 src/Tools/isac/Knowledge/Partial_Fractions.thy --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Tue Apr 27 18:14:02 2021 +0200 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Tue Apr 27 19:52:29 2021 +0200 @@ -56,15 +56,15 @@ in mk_prod TermC.empty (map fac_from_sol ts) end; (*("factors_from_solution", ("Partial_Fractions.factors_from_solution", - eval_factors_from_solution ""))*) + eval_factors_from_solution "")) + this code is limited (max 3 solutions) AND has too little checks *) fun eval_factors_from_solution (thmid:string) _ - (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy = - ((let val prod = factors_from_solution sol - in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "", - HOLogic.Trueprop $ (TermC.mk_equality (t, prod))) - end) - handle _ => NONE) - | eval_factors_from_solution _ _ _ _ = NONE; + (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy = + let val prod = factors_from_solution sol + in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "", + HOLogic.Trueprop $ (TermC.mk_equality (t, prod))) + end + | eval_factors_from_solution _ _ _ _ = NONE; \ subsection \'ansatz' for partial fractions\ diff -r 95bae6eeccfa -r b987b05f1ca8 src/Tools/isac/Knowledge/Rational-WN.sml --- a/src/Tools/isac/Knowledge/Rational-WN.sml Tue Apr 27 18:14:02 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,257 +0,0 @@ -(*Stefan K.*) - -(*protokoll 14.3.02 -------------------------------------------------- -val ct = parse thy "(a + #1)//(#2*a^^^#2 - #2)"; -val t = (Thm.term_of o the) ct; -atomt t; -val ct = parse thy "not (#1+a)"; (*HOL.thy ?*) -val t = (Thm.term_of o the) ct; -atomt t; -val ct = parse thy "x"; (*momentan ist alles 'real'*) -val t = (Thm.term_of o the) ct; -atomty t; -val ct = parse thy "(x::int)"; (* !!! *) -val t = (Thm.term_of o the) ct; -atomty t; - -val ct = parse thy "(x::int)*(y::real)"; (*momentan ist alles 'real'*) - -val Const ("RatArith.cancel",_) $ zaehler $ nenner = t; ----------------------------------------------------------------------*) - - -(*diese vvv funktionen kommen nach src/Isa99/termC.sml -------------*) -fun UnparseC.term t = - let fun ato (Const(a,T)) n = - "\n"^indent n^"Const ( "^a^")" - | ato (Free (a,T)) n = - "\n"^indent n^"Free ( "^a^", "^")" - | ato (Var ((a,ix),T)) n = - "\n"^indent n^"Var (("^a^", "^string_of_int ix^"), "^")" - | ato (Bound ix) n = - "\n"^indent n^"Bound "^string_of_int ix - | ato (Abs(a,T,body)) n = - "\n"^indent n^"Abs( "^a^",.."^ato body (n+1) - | ato (f$t') n = ato f n^ato t' (n+1) - in "\n-------------"^ato t 0^"\n" end; -fun free2int (t as Free (s, _)) = (((the o int_of_str) s) - handle _ => raise ERROR ("free2int: "^UnparseC.term t)) - | free2int t = raise ERROR ("free2int: "^UnparseC.term t); -(*diese ^^^ funktionen kommen nach src/Isa99/termC.sml -------------*) - - -(* remark on exceptions: 'error' is implemented by Isabelle - as the typical system error *) - - -type poly = int list; - -(* transform a Isabelle-term t into internal polynomial format - preconditions for t: - a-b -> a+(-b) - x^1 -> x - term ordered ascending - parentheses right side (caused by 'ordered rewriting') - variable as power (not as product) *) - -fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g = - if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly - else raise ERROR ("term2poly.1 "^UnparseC.term t1) - | mono (t as Const ("Groups.times_class.times",_) $ t1 $ - (Const ("RatArith.pow",_) $ t2 $ t3)) v g = - if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1] - else raise ERROR ("term2poly.2 "^UnparseC.term t) - | mono t _ _ = raise ERROR ("term2poly.3 "^UnparseC.term t); - -fun poly (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v g = - let val l = mono t1 v g - in (l @ (poly t2 v ((length l) + g))) end - | poly t v g = mono t v g; - -fun term2poly (t as Free (s, _)) v = - if t = v then SOME ([0,1] : poly) else (SOME [(the o int_of_str) s] - handle _ => NONE) - | term2poly (Const ("Groups.times_class.times",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v = - if t = v then SOME [0, (the o int_of_str) s1] else NONE - | term2poly (Const ("Groups.plus_class.plus",_) $ (Free (s1,_)) $ t) v = - SOME ([(the o int_of_str) s1] @ (poly t v 1)) - | term2poly t v = - SOME (poly t v 0) handle _ => NONE; - -(*tests*) -val v = (Thm.term_of o the o (parse thy)) "x::real"; -val t = (Thm.term_of o the o (parse thy)) "#-1::real"; -term2poly t v; -val t = (Thm.term_of o the o (parse thy)) "x::real"; -term2poly t v; -val t = (Thm.term_of o the o (parse thy)) "#1 * x::real"; (*FIXME: drop it*) -term2poly t v; -val t = (Thm.term_of o the o (parse thy)) "x \ #1"; (*FIXME: drop it*) -term2poly t v; -val t = (Thm.term_of o the o (parse thy)) "x \ #3"; -term2poly t v; -val t = (Thm.term_of o the o (parse thy)) "#3 * x \ #3"; -term2poly t v; -val t = (Thm.term_of o the o (parse thy)) "#-1 + #3 * x \ #3"; -term2poly t v; -val t = (Thm.term_of o the o (parse thy)) "#-1 + (#3 * x \ #3 + #5 * x \ #5)"; -term2poly t v; -val t = (Thm.term_of o the o (parse thy)) - "#-1 + (#3 * x \ #3 + (#5 * x \ #5 + #7 * x \ #7))"; -term2poly t v; -val t = (Thm.term_of o the o (parse thy)) - "#3 * x \ #3 + (#5 * x \ #5 + #7 * x \ #7)"; -term2poly t v; - - -fun is_polynomial_in t v = - case term2poly t v of SOME _ => true | NONE => false; - -(* transform the internal polynomial p into an Isabelle term t - where t meets the preconditions of term2poly -val mk_mono = - fn : typ -> of the coefficients - typ -> of the unknown - typ -> of the monomial and polynomial - typ -> of the exponent of the unknown - int -> the coefficient <> 0 - string -> the unknown - int -> the degree, i.e. the value of the exponent - term -remark: all the typs above are "RealDef.real" due to the typs of * + ^ -which may change in the future -*) -fun mk_mono cT vT pT eT c v g = - case g of - 0 => Free (str_of_int c, cT) (*will cause problems with diff.typs*) - | 1 => if c = 1 then Free (v, vT) - else Const ("Groups.times_class.times", [cT, vT]--->pT) $ - Free (str_of_int c, cT) $ Free (v, vT) - | n => if c = 1 then (Const ("RatArith.pow", [vT, eT]--->pT) $ - Free (v, vT) $ Free (str_of_int g, eT)) - else Const ("Groups.times_class.times", [cT, vT]--->pT) $ - Free (str_of_int c, cT) $ - (Const ("RatArith.pow", [vT, eT]--->pT) $ - Free (v, vT) $ Free (str_of_int g, eT)); -(*tests*) -val cT = HOLogic.realT; val vT = HOLogic.realT; val pT = HOLogic.realT; -val eT = HOLogic.realT; -val t = mk_mono cT vT pT eT ~5 "x" 5; -(Thm.global_cterm_of thy) t; -val t = mk_mono cT vT pT eT ~1 "x" 0; -(Thm.global_cterm_of thy) t; -val t = mk_mono cT vT pT eT 1 "x" 1; -(Thm.global_cterm_of thy) t; - - -fun mk_sum pT t1 t2 = Const ("Groups.plus_class.plus", [pT, pT]--->pT) $ t1 $ t2; - - -fun poly2term cT vT pT eT ([p]:poly) v = mk_mono cT vT pT eT p v 0 - | poly2term cT vT pT eT (p:poly) v = - let - fun mk_poly cT vT pT eT [] t v g = t - | mk_poly cT vT pT eT [p] t v g = - if p = 0 then t - else mk_sum pT (mk_mono cT vT pT eT p v g) t - | mk_poly cT vT pT eT (p::ps) t v g = - if p = 0 then mk_poly cT vT pT eT ps t v (g-1) - else mk_poly cT vT pT eT ps - (mk_sum pT (mk_mono cT vT pT eT p v g) t) v (g-1) - val (p'::ps') = rev p - val g = (length p) - 1 - in mk_poly cT vT pT eT ps' (mk_mono cT vT pT eT p' v g) v (g-1) end; - -(*tests*) -val t = poly2term cT vT pT eT [~1] "x"; -(Thm.global_cterm_of thy) t; -val t = poly2term cT vT pT eT [0,1] "x"; -(Thm.global_cterm_of thy) t; -val t = poly2term cT vT pT eT [0,0,0,1] "x"; -(Thm.global_cterm_of thy) t; -val t = poly2term cT vT pT eT [0,0,0,3] "x"; -(Thm.global_cterm_of thy) t; -val t = poly2term cT vT pT eT [~1,0,0,3] "x"; -(Thm.global_cterm_of thy) t; -val t = poly2term cT vT pT eT [~1,0,0,3,0,5] "x"; -(Thm.global_cterm_of thy) t; -val t = poly2term cT vT pT eT [~1,0,0,3,0,5,0,7] "x"; -(Thm.global_cterm_of thy) t; -val t = poly2term cT vT pT eT [0,0,0,3,0,5,0,7] "x"; -(Thm.global_cterm_of thy) t; - -"***************************************************************************"; -"* reverse-rewriting 12.8.02 *"; -"***************************************************************************"; -fun rewrite_set_' thy rls put_asm ruless ct = - case ruless of - Rule_Set.Rrls _ => raise ERROR "rewrite_set_' not for Rule_Set.Rrls" - | Rule_Def.Repeat _ => - let - datatype switch = Appl | Noap; - fun rew_once ruls asm ct Noap [] = (ct,asm) - | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls - | rew_once ruls asm ct apno (rul::thms) = - case rul of - Rule.Thm (thmid, thm) => - (case rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless) - rls put_asm (Rule.thm rul) ct of - NONE => rew_once ruls asm ct apno thms - | SOME (ct',asm') => - rew_once ruls (asm union asm') ct' Appl (rul::thms)) - | Rule.Eval (cc as (op_,_)) => - (case adhoc_thm thy cc ct of - NONE => rew_once ruls asm ct apno thms - | SOME (thmid, thm') => - let - val pairopt = - rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless) - rls put_asm thm' ct; - val _ = if pairopt <> NONE then () - else raise ERROR("rewrite_set_, rewrite_ \""^ - (ThmC.string_of_thm thm')^"\" \""^ - (Syntax.string_of_term (ThyC.to_ctxt thy) ct)^"\" = NONE") - in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); - val ruls = (#rules o Rule_Set.rep) ruless; - val (ct',asm') = rew_once ruls [] ct Noap ruls; - in if ct = ct' then NONE else SOME (ct',asm') end; - -(* -fun reverse_rewrite t1 t2 rls = -*) -fun rewrite_set_' thy rls put_asm ruless ct = - case ruless of - Rule_Set.Rrls _ => raise ERROR "rewrite_set_' not for Rule_Set.Rrls" - | Rule_Def.Repeat _ => - let - datatype switch = Appl | Noap; - fun rew_once ruls asm ct Noap [] = (ct,asm) - | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls - | rew_once ruls asm ct apno (rul::thms) = - case rul of - Rule.Thm (thmid, thm) => - (case rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless) - rls put_asm (Rule.thm rul) ct of - NONE => rew_once ruls asm ct apno thms - | SOME (ct',asm') => - rew_once ruls (asm union asm') ct' Appl (rul::thms)) - | Rule.Eval (cc as (op_,_)) => - (case adhoc_thm thy cc ct of - NONE => rew_once ruls asm ct apno thms - | SOME (thmid, thm') => - let - val pairopt = - rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless) - rls put_asm thm' ct; - val _ = if pairopt <> NONE then () - else raise ERROR("rewrite_set_, rewrite_ \""^ - (ThmC.string_of_thm thm')^"\" \""^ - (Syntax.string_of_term (ThyC.to_ctxt thy) ct)^"\" = NONE") - in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); - val ruls = (#rules o Rule_Set.rep) ruless; - val (ct',asm') = rew_once ruls [] ct Noap ruls; - in if ct = ct' then NONE else SOME (ct',asm') end; - - realpow_two; - real_mult_div_cancel1; -