1.1 --- a/TODO.md Thu Apr 29 14:13:11 2021 +0200
1.2 +++ b/TODO.md Thu Apr 29 17:02:10 2021 +0200
1.3 @@ -1,8 +1,3 @@
1.4 -* WN: eliminate "handle _ => ..." (essential for PIDE interaction):
1.5 - - either use \<^try>CARTOUCHE / \<^can>CARTOUCHE antiquotation
1.6 - - or more basic try/can combinators;
1.7 - - or more direct ML of intention;
1.8 -
1.9 * reconsider use of Thy_Info.get_theory: only works with batch-build, not within PIDE session;
1.10 + consider in Build_Thydata: Thy_Hierarchy.insert_errpatIDs
1.11 + consider in Biegelinie.thy: KEStore_Elems.add_thes,
2.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Apr 29 14:13:11 2021 +0200
2.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Apr 29 17:02:10 2021 +0200
2.3 @@ -438,13 +438,12 @@
2.4 eval_factors_from_solution ""))*)
2.5
2.6 fun eval_factors_from_solution (thmid:string) _
2.7 - (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol)
2.8 - thy = ((let val prod = factors_from_solution sol
2.9 - in SOME (mk_thmid thmid "" (UnparseC.term_in_thy thy prod) "",
2.10 - Trueprop $ (mk_equality (t, prod)))
2.11 - end)
2.12 - handle _ => NONE)
2.13 - | eval_factors_from_solution _ _ _ _ = NONE;
2.14 + (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
2.15 + let val prod = factors_from_solution sol
2.16 + in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "",
2.17 + HOLogic.Trueprop $ (TermC.mk_equality (t, prod)))
2.18 + end
2.19 + | eval_factors_from_solution _ _ _ _ = NONE;
2.20 \<close>
2.21
2.22 text \<open>\noindent The tracing output of the calc tree after applying this
3.1 --- a/test/Tools/isac/BaseDefinitions/calcelems.sml Thu Apr 29 14:13:11 2021 +0200
3.2 +++ b/test/Tools/isac/BaseDefinitions/calcelems.sml Thu Apr 29 17:02:10 2021 +0200
3.3 @@ -78,14 +78,6 @@
3.4 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
3.5 (*default_print_depth 3;*)
3.6 *)
3.7 -"===== extend TermC.parse to string with markup===";
3.8 -(*
3.9 -fun TermC.parse thy str =
3.10 - (let val t = (TermC.typ_a2real o ThmC_Def.num_to_Free)
3.11 - (Syntax.read_term_global thy str)
3.12 - in SOME (Thm.global_cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)
3.13 - handle _ => NONE;
3.14 -*)
3.15
3.16 "-------- fun ThmC.cut_id 000---------------";
3.17 "-------- fun ThmC.cut_id 000---------------";
4.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Thu Apr 29 14:13:11 2021 +0200
4.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Thu Apr 29 17:02:10 2021 +0200
4.3 @@ -370,23 +370,15 @@
4.4 val t = ThmC_Def.num_to_Free (Syntax.read_term_global thy str);
4.5 val t = (TermC.typ_a2real o ThmC_Def.num_to_Free) (Syntax.read_term_global thy str);
4.6 Thm.global_cterm_of thy t;
4.7 - val t = (the (TermC.parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";
4.8 + case TermC.parse thy str of
4.9 + SOME t' => t'
4.10 + | NONE => error "termC.sml parsing 'x + 2*z' failed";
4.11
4.12 "===== fun TermC.parse_patt caused error in fun T_a2real ===";
4.13 val thy = @{theory "Poly"};
4.14 TermC.parse_patt thy "?p is_addUnordered";
4.15 TermC.parse_patt thy "?p :: real";
4.16
4.17 - val str = "x + z";
4.18 - TermC.parse thy str;
4.19 -"---------------";
4.20 - val str = "x + 2*z";
4.21 - val t = (Syntax.read_term_global thy str);
4.22 - val t = ThmC_Def.num_to_Free (Syntax.read_term_global thy str);
4.23 - val t = (TermC.typ_a2real o ThmC_Def.num_to_Free) (Syntax.read_term_global thy str);
4.24 - Thm.global_cterm_of thy t;
4.25 - val t = (the (TermC.parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";
4.26 -
4.27 "===== fun TermC.parse_patt caused error in fun T_a2real ===";
4.28 val thy = @{theory "Poly"};
4.29 TermC.parse_patt thy "?p is_addUnordered";
5.1 --- a/test/Tools/isac/Knowledge/rational.sml Thu Apr 29 14:13:11 2021 +0200
5.2 +++ b/test/Tools/isac/Knowledge/rational.sml Thu Apr 29 17:02:10 2021 +0200
5.3 @@ -220,7 +220,7 @@
5.4 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
5.5 in
5.6 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
5.7 - end) handle _ => false
5.8 + end) handle Pattern.MATCH => false
5.9 fun scan_ f [] = false (*scan_ NEVER called by []*)
5.10 | scan_ f (pp::pps) =
5.11 if f pp then true else scan_ f pps;
5.12 @@ -242,7 +242,7 @@
5.13 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
5.14 in
5.15 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
5.16 - end) handle _ => false
5.17 + end) handle Pattern.MATCH => false
5.18 fun scan_ f [] = false (*scan_ NEVER called by []*)
5.19 | scan_ f (pp::pps) =
5.20 if f pp then true else scan_ f pps;
5.21 @@ -391,7 +391,7 @@
5.22 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
5.23 in
5.24 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
5.25 - end) handle _ => false
5.26 + end) handle Pattern.MATCH => false
5.27 fun scan_ f [] = false (*scan_ NEVER called by []*)
5.28 | scan_ f (pp::pps) =
5.29 if f pp then true else scan_ f pps;
6.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Thu Apr 29 14:13:11 2021 +0200
6.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Thu Apr 29 17:02:10 2021 +0200
6.3 @@ -19,7 +19,7 @@
6.4 (2) correction ''make_rooteq'' led further to "check_elementwise: no set 1 + sqrt x = 3"
6.5 Since the changeset seems have nothing todo with these errors, this indicates that
6.6 (a) either method ["RootEq", "solve_sq_root_equation"] & Co are somewhat indeterministic
6.7 -(b) of this is a case of indeterminism due to "handle _" or something similar elementary.
6.8 +(b) of this is a case of indeterminism due to something elementary.
6.9
6.10 *)
6.11 val thy = @{theory "RootRatEq"};
7.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Thu Apr 29 14:13:11 2021 +0200
7.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Thu Apr 29 17:02:10 2021 +0200
7.3 @@ -59,11 +59,13 @@
7.4 ("Test", ["sqroot-test", "univariate", "equation", "test"],
7.5 ["Test", "squ-equ-test-subpbl1"]);
7.6 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.7 -(get_ctxt pt p)
7.8 - handle _ => error "--- fun get_ctxt not even some ctxt found in PblObj";
7.9 +case \<^try>\<open> (get_ctxt pt p)\<close> of
7.10 + SOME x => x
7.11 +| NONE => error "--- fun get_ctxt not even some ctxt found in PblObj";
7.12 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.13 -(get_ctxt pt p)
7.14 - handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";
7.15 +case \<^try>\<open> (get_ctxt pt p)\<close> of
7.16 + SOME x => x
7.17 +| NONE => error "--- fun get_ctxt not even some ctxt found in PrfObj";
7.18
7.19 val pt = EmptyPtree;
7.20 val pt = append_problem [] (Istate.empty, ContextC.empty) Formalise.empty ([(*oris*)], References.empty, TermC.empty, ContextC.empty) pt;
8.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Thu Apr 29 14:13:11 2021 +0200
8.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Thu Apr 29 17:02:10 2021 +0200
8.3 @@ -402,7 +402,7 @@
8.4 (map (Envir.subst_term subst) pres)
8.5 [] erls)
8.6 end)
8.7 - handle _ => false
8.8 + handle Pattern.MATCH => false
8.9 fun scan_ f [] = false (*scan_ NEVER called by []*)
8.10 | scan_ f (pp::pps) = if f pp then true
8.11 else scan_ f pps;
8.12 @@ -428,8 +428,8 @@
8.13 (map (Envir.subst_term subst) pres)
8.14 [] erls)
8.15 end)
8.16 - handle _ => false;
8.17 - fun scan_ f [] = false (*scan_ NEVER called by []*)
8.18 + handle Pattern.MATCH => false;
8.19 + fun scan_ _ [] = false (*scan_ NEVER called by []*)
8.20 | scan_ f (pp::pps) = if f pp then true
8.21 else scan_ f pps;
8.22 tracing "=== poly.sml: scan_ chk prepat begin";
9.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Thu Apr 29 14:13:11 2021 +0200
9.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Thu Apr 29 17:02:10 2021 +0200
9.3 @@ -425,7 +425,9 @@
9.4 if power 2 3 = 8 then () else error "power 2 3 = 8";
9.5 if power ~2 3 = ~8 then () else error "power ~2 3 = ~8";
9.6 if power ~3 2 = 9 then () else error "power ~3 2 = 9";
9.7 -(power 3 ~2; error "power 3 ~2: should raise an exn") handle _ => 000;
9.8 +case \<^try>\<open> power 3 ~2 \<close> of
9.9 + SOME _ => raise error "power 3 ~2: should raise an exn 1"
9.10 +| NONE => ()
9.11
9.12 "----------- fun divisors ----------------------------------------------------------------------";
9.13 "----------- fun divisors ----------------------------------------------------------------------";