1.1 --- a/TODO.md Wed Aug 03 13:22:36 2022 +0200
1.2 +++ b/TODO.md Wed Aug 03 17:18:47 2022 +0200
1.3 @@ -86,7 +86,7 @@
1.4 \<close>
1.5
1.6 * WN: Calculate.thy: add structure Calculate
1.7 -* WN: cleanup method-def.sml problem-def.sml
1.8 +* WN: cleanup method-def.sml, problem-def.sml, "eval-def.sml", "rewrite-order.sml"
1.9 * WN: MethodC.from_store throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument
1.10
1.11 * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
2.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Aug 03 13:22:36 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Aug 03 17:18:47 2022 +0200
2.3 @@ -68,6 +68,8 @@
2.4 *)
2.5 signature KESTORE_ELEMS =
2.6 sig
2.7 + val get_rew_ord: theory -> Rewrite_Ord.rew_ord list
2.8 + val add_rew_ord: Rewrite_Ord.rew_ord list -> theory -> theory
2.9 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
2.10 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
2.11 val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
2.12 @@ -87,11 +89,20 @@
2.13 val set_ref_thy: theory -> unit
2.14 end;
2.15
2.16 -structure KEStore_Elems: KESTORE_ELEMS =
2.17 +structure KEStore_Elems(**): KESTORE_ELEMS(**) =
2.18 struct
2.19 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
2.20
2.21 structure Data = Theory_Data (
2.22 + type T = (string * (LibraryC.subst -> term * term -> bool)) list;
2.23 + val empty = [];
2.24 + val extend = I;
2.25 + val merge = merge Rewrite_Ord.equal;
2.26 + );
2.27 + fun get_rew_ord thy = Data.get thy
2.28 + fun add_rew_ord rlss = Data.map (union_overwrite Rewrite_Ord.equal rlss)
2.29 +
2.30 + structure Data = Theory_Data (
2.31 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
2.32 val empty = [];
2.33 val extend = I;
2.34 @@ -183,7 +194,7 @@
2.35 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
2.36 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
2.37 fun get_ref_thy () = Synchronized.value cur_thy;
2.38 -end;
2.39 +(**)end(**);
2.40 \<close>
2.41
2.42
2.43 @@ -242,6 +253,12 @@
2.44 ML \<open>
2.45 val get_ref_thy = KEStore_Elems.get_ref_thy;
2.46
2.47 +fun assoc' ([], key) = raise ERROR ("ME_Isa: rew_ord \"" ^ key ^ "\" not in system 2")
2.48 + | assoc' ((keyi, xi) :: pairs, key) =
2.49 + if key = keyi then SOME xi else assoc' (pairs, key);
2.50 +fun assoc_rew_ord thy ro = ((the o assoc') (KEStore_Elems.get_rew_ord thy, ro))
2.51 + handle ERROR _ => raise ERROR ("ME_Isa: rew_ord \"" ^ ro ^ "\" not in system 1");
2.52 +
2.53 fun assoc_rls (rls' : Rule_Set.id) =
2.54 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
2.55 SOME (_, rls) => rls
3.1 --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml Wed Aug 03 13:22:36 2022 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml Wed Aug 03 17:18:47 2022 +0200
3.3 @@ -13,8 +13,7 @@
3.4 val to_string: rew_ord -> string
3.5
3.6 type rew_ord' = Rule_Def.rew_ord'
3.7 - val rew_ord': (rew_ord' * (LibraryC.subst -> term * term -> bool)) list Unsynchronized.ref
3.8 - val assoc_rew_ord: string -> LibraryC.subst -> term * term -> bool
3.9 + val equal: rew_ord * rew_ord -> bool
3.10 end
3.11
3.12 (**)
3.13 @@ -42,10 +41,7 @@
3.14 -> (term * term) (* (t1, t2) to be compared *)
3.15 -> bool)) (* if t1 <= t2 then true else false *)
3.16 list); (* association list *)
3.17 -fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
3.18 - | assoc' ((keyi, xi) :: pairs, key) =
3.19 - if key = keyi then SOME xi else assoc' (pairs, key);
3.20 -fun assoc_rew_ord ro = ((the o assoc') (! rew_ord', ro))
3.21 - handle ERROR _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
3.22
3.23 -end
3.24 \ No newline at end of file
3.25 +fun equal ((id1, _), (id2, _)) = id1 = id2
3.26 +
3.27 +end
4.1 --- a/src/Tools/isac/Interpret/solve-step.sml Wed Aug 03 13:22:36 2022 +0200
4.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Wed Aug 03 17:18:47 2022 +0200
4.3 @@ -136,12 +136,13 @@
4.4 | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) =
4.5 let
4.6 val (msg, thy', ro, rls', _) = get_ruleset thm p pt;
4.7 - val thy = ThyC.id_to_ctxt thy';
4.8 + val thy = ThyC.get_theory thy';
4.9 + val ctxt = Proof_Context.init_global thy;
4.10 val f = Calc.current_formula cs;
4.11 in
4.12 if msg = "OK"
4.13 then
4.14 - case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm) f of
4.15 + case Rewrite.rewrite_ ctxt (assoc_rew_ord thy ro) rls' false (snd thm) f of
4.16 SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm)))
4.17 | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable")
4.18 else Applicable.No msg
4.19 @@ -156,7 +157,7 @@
4.20 val f = Calc.current_formula cs;
4.21 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
4.22 in
4.23 - case Rewrite.rewrite_inst_ ctxt (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm) f of
4.24 + case Rewrite.rewrite_inst_ ctxt (assoc_rew_ord thy ro') erls false subst (snd thm) f of
4.25 SOME (f', asm) =>
4.26 Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
4.27 | NONE => Applicable.No (fst thm ^ " not applicable")
4.28 @@ -198,7 +199,7 @@
4.29 val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp)
4.30 val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
4.31 val subst = Subst.T_from_string_eqs thy sube
4.32 - val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
4.33 + val ro = assoc_rew_ord thy rew_ord'
4.34 in
4.35 if foldl and_ (true, map TermC.contains_Var subte)
4.36 then (*1*)
5.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Wed Aug 03 13:22:36 2022 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Wed Aug 03 17:18:47 2022 +0200
5.3 @@ -52,11 +52,13 @@
5.4 \<close> ML \<open>
5.5 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)
5.6 val tless_true = Rewrite_Ord.dummy_ord;
5.7 -Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx here, too*)
5.8 - [("tless_true", tless_true),
5.9 - ("e_rew_ord'", tless_true),
5.10 - ("dummy_ord", Rewrite_Ord.dummy_ord)]);
5.11 -\<close>
5.12 +\<close> ML \<open>
5.13 +\<close>
5.14 +setup \<open>KEStore_Elems.add_rew_ord [
5.15 + ("tless_true", tless_true),
5.16 + ("e_rew_ord", tless_true),
5.17 + ("e_rew_ord'", tless_true),
5.18 + ("dummy_ord", Rewrite_Ord.dummy_ord)]\<close>
5.19
5.20 subsection \<open>rule-sets\<close>
5.21 ML \<open>
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Aug 03 13:22:36 2022 +0200
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Aug 03 17:18:47 2022 +0200
6.3 @@ -159,13 +159,13 @@
6.4 (*for the rls's*)
6.5 fun ord_simplify_System (pr:bool) thy _(*subst*) (ts, us) =
6.6 (term_ord' pr thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS);
6.7 -(**)
6.8 -end;
6.9 -(**)
6.10 -Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
6.11 -[("ord_simplify_System", ord_simplify_System false \<^theory>)
6.12 - ]);
6.13 +
6.14 +(**)end;(**)
6.15 +\<close> ML \<open>
6.16 \<close>
6.17 +setup \<open>KEStore_Elems.add_rew_ord [
6.18 + ("ord_simplify_System", ord_simplify_System false \<^theory>)]\<close>
6.19 +
6.20 ML \<open>
6.21 (** rulesets **)
6.22
7.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Aug 03 13:22:36 2022 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Aug 03 17:18:47 2022 +0200
7.3 @@ -549,10 +549,10 @@
7.4 (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );
7.5
7.6 end;(*local*)
7.7 -
7.8 -Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (* TODO: make analogous to KEStore_Elems.add_mets *)
7.9 -[("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false \<^theory>)]);
7.10 -\<close>
7.11 +\<close>
7.12 +setup \<open>KEStore_Elems.add_rew_ord [
7.13 + ("termlessI", termlessI),
7.14 + ("ord_make_polynomial", ord_make_polynomial false \<^theory>)]\<close>
7.15
7.16 subsection \<open>predicates\<close>
7.17 subsubsection \<open>in specifications\<close>
8.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Aug 03 13:22:36 2022 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Aug 03 17:18:47 2022 +0200
8.3 @@ -513,7 +513,7 @@
8.4
8.5 val cancel_p =
8.6 Rule_Set.Rrls {id = "cancel_p", prepat = [],
8.7 - rew_ord=("ord_make_polynomial", ord_make_polynomial false \<^theory>),
8.8 + rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
8.9 erls = rational_erls,
8.10 calc =
8.11 [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
9.1 --- a/src/Tools/isac/Knowledge/Root.thy Wed Aug 03 13:22:36 2022 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Aug 03 17:18:47 2022 +0200
9.3 @@ -149,13 +149,14 @@
9.4 fun sqrt_right (pr:bool) thy (_: subst) (ts, us) =
9.5 (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );
9.6 end;
9.7 +\<close> ML \<open>
9.8 +\<close>
9.9 +setup \<open>KEStore_Elems.add_rew_ord [
9.10 + ("termlessI", termlessI),
9.11 + ("sqrt_right", sqrt_right false @{theory "Pure"})]\<close>
9.12
9.13 -Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
9.14 -[("termlessI", termlessI),
9.15 - ("sqrt_right", sqrt_right false @{theory "Pure"})
9.16 - ]);
9.17 -
9.18 -(*-------------------------rulse-------------------------*)
9.19 +ML \<open>
9.20 +(*------------------------- rules -------------------------*)
9.21 val Root_crls =
9.22 Rule_Set.append_rules "Root_crls" Atools_erls [
9.23 \<^rule_thm>\<open>real_unari_minus\<close>,
10.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Aug 03 13:22:36 2022 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Aug 03 17:18:47 2022 +0200
10.3 @@ -589,12 +589,11 @@
10.4 (matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e)"
10.5 Find: "solutions v_v'i'"
10.6
10.7 +setup \<open>KEStore_Elems.add_rew_ord [
10.8 + ("termlessI", termlessI),
10.9 + ("ord_make_polytest", ord_make_polytest false \<^theory>)]\<close>
10.10 +
10.11 ML \<open>
10.12 -Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
10.13 -[("termlessI", termlessI),
10.14 - ("ord_make_polytest", ord_make_polytest false \<^theory>)
10.15 - ]);
10.16 -
10.17 val make_polytest =
10.18 Rule_Def.Repeat{id = "make_polytest", preconds = []:term list,
10.19 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
11.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Aug 03 13:22:36 2022 +0200
11.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Aug 03 17:18:47 2022 +0200
11.3 @@ -271,9 +271,10 @@
11.4 try_rew ctxt Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f
11.5 (Rule.Eval (assoc_calc' (Proof_Context.theory_of ctxt) scrID |> snd))
11.6 | applicable ctxt ro erls f (Rewrite thm'') =
11.7 - try_rew ctxt (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
11.8 + try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls [] f (Rule.Thm thm'')
11.9 | applicable ctxt ro erls f (Rewrite_Inst (subs, thm'')) =
11.10 - try_rew ctxt (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input ctxt subs) f (Rule.Thm thm'')
11.11 + try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls
11.12 + (Subst.T_from_input ctxt subs) f (Rule.Thm thm'')
11.13
11.14 | applicable thy _ _ f (Rewrite_Set rls') =
11.15 filter_appl_rews thy [] f (assoc_rls rls')
12.1 --- a/src/Tools/isac/ROOT Wed Aug 03 13:22:36 2022 +0200
12.2 +++ b/src/Tools/isac/ROOT Wed Aug 03 17:18:47 2022 +0200
12.3 @@ -6,9 +6,15 @@
12.4 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
12.5 before out-outcommenting (*, browser_info = true*) below and ...
12.6 $ ./bin/isabelle build -o browser_info -v -c HOL
12.7 +$ ./bin/isabelle build -o browser_info -v -b Specify
12.8 +$ ./bin/isabelle build -o browser_info -v -b Interpret
12.9 $ ./bin/isabelle build -o browser_info -v -b Isac
12.10 # this creates, among others:
12.11 -# file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
12.12 +# file:///home/walthern/.isabelle/isabisac/browser_info/HOL/index.html
12.13 +# file:///home/walthern/.isabelle/isabisac/browser_info/Unsorted/index.html
12.14 +# file:///home/walthern/.isabelle/isabisac/browser_info/Unsorted/Specify/session_graph.pdf
12.15 +# file:///home/walthern/.isabelle/isabisac/browser_info/Unsorted/Interpret/session_graph.pdf
12.16 +# file:///home/walthern/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
12.17 *)
12.18
12.19 (* run "./bin/isabelle build -v -b Specify" *)
13.1 --- a/test/Tools/isac/BridgeJEdit/vscode-example.sml Wed Aug 03 13:22:36 2022 +0200
13.2 +++ b/test/Tools/isac/BridgeJEdit/vscode-example.sml Wed Aug 03 17:18:47 2022 +0200
13.3 @@ -23,7 +23,7 @@
13.4 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
13.5 "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
13.6 "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]",
13.7 -(*MethodC model:*)
13.8 +(*MethodC model:*)
13.9 "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>",
13.10 "Domain {0 <..< r}",
13.11 "Domain {0 <..< r}",
13.12 @@ -40,14 +40,14 @@
13.13 val (p,_,f, nxt,_,pt) = CalcTreeTEST [(fmz, refs)];
13.14 val ptp = (pt, p);
13.15 ( *-------- outcomment EITHER above OR below --------------------------------------------------*)
13.16 -case get_example "Diff_App/No.123 a" of
13.17 +case Store.get (KEStore_Elems.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"] of
13.18 (_, ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: _,
13.19 ("Diff_App", ["univariate_calculus", "Optimisation"] ,["Optimisation", "by_univariate_calculus"])))
13.20 => ()
13.21 | _ => error "intermed. example_store CHANGED";
13.22 val p = ([], Pbl);
13.23 val pt = update_state (*here we have Ctree.EmptyPtree and thus call init_ctree*)
13.24 -("Diff_App/No.123 a",
13.25 +("Diff_App-No.123a",
13.26 (* Problem.parse_model_input results in markup, which is accepted by \<open>fun update_state\<close>, too:
13.27 Constants [r = 7] *)
13.28 ( [("#Given", ["Constants [r = 7]"]),
14.1 --- a/test/Tools/isac/Test_Isac.thy Wed Aug 03 13:22:36 2022 +0200
14.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Aug 03 17:18:47 2022 +0200
14.3 @@ -150,12 +150,6 @@
14.4 \<close> ML \<open>
14.5 \<close> ML \<open>
14.6 \<close> ML \<open>
14.7 -\<close> ML \<open>
14.8 -\<close> ML \<open>
14.9 -\<close> ML \<open>
14.10 -\<close> ML \<open>
14.11 -\<close> ML \<open>
14.12 -\<close> ML \<open>
14.13 \<close>
14.14
14.15 ML \<open>
14.16 @@ -329,12 +323,6 @@
14.17 \<close> ML \<open>
14.18 \<close> ML \<open>
14.19 \<close> ML \<open>
14.20 -\<close> ML \<open>
14.21 -\<close> ML \<open>
14.22 -\<close> ML \<open>
14.23 -\<close> ML \<open>
14.24 -\<close> ML \<open>
14.25 -\<close> ML \<open>
14.26 \<close>
14.27
14.28 section \<open>history of tests\<close>