# HG changeset patch # User wneuper # Date 1673366873 -3600 # Node ID ea7db4f4f837784d18f1ea8378a0dc63bcc0d050 # Parent 52e8e77920b9de919650fe6ef346ddf2342f12d1 eliminate use of Thy_Info 10: arg. ctxt for Rule.to_string finished diff -r 52e8e77920b9 -r ea7db4f4f837 src/Tools/isac/BaseDefinitions/rule-set.sml --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Tue Jan 10 10:01:05 2023 +0100 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Tue Jan 10 17:07:53 2023 +0100 @@ -184,7 +184,7 @@ fun id_from_rule _ (Rule.Rls_ rls) = id rls | id_from_rule ctxt r = - raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string_PIDE ctxt r); + raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string ctxt r); (* check if a rule is contained in a rule-set (recursivley down in Rls_); this rule can even be a rule-set itself *) diff -r 52e8e77920b9 -r ea7db4f4f837 src/Tools/isac/BaseDefinitions/rule.sml --- a/src/Tools/isac/BaseDefinitions/rule.sml Tue Jan 10 10:01:05 2023 +0100 +++ b/src/Tools/isac/BaseDefinitions/rule.sml Tue Jan 10 17:07:53 2023 +0100 @@ -14,17 +14,16 @@ val set_id: Rule_Def.rule_set -> string val id: rule -> string val equal: rule * rule -> bool - val to_string: rule -> string - val to_string_PIDE: Proof.context -> rule -> string + val to_string: Proof.context -> rule -> string val to_string_short: rule -> string val s_to_string: rule list -> string - val thm: rule -> thm + val thm: Proof.context -> rule -> thm val distinct' : rule list -> rule list val thm_id: rule -> string - val eval: rule -> string * Rule_Def.eval_fn - val rls: rule -> Rule_Def.rule_set + val eval: Proof.context -> rule -> string * Rule_Def.eval_fn + val rls: Proof.context -> rule -> Rule_Def.rule_set val make_eval: string -> Rule_Def.eval_fn -> rule end @@ -58,17 +57,12 @@ | equal _ = false; fun distinct' rs = distinct equal rs -fun to_string_PIDE _ Rule_Def.Erule = "Erule" - | to_string_PIDE ctxt (Rule_Def.Thm (str, thm)) = +fun to_string _ Rule_Def.Erule = "Erule" + | to_string ctxt (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm_PIDE ctxt thm ^ ")" - | to_string_PIDE _ (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)" - | to_string_PIDE _ (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" - | to_string_PIDE _ (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")"; -fun to_string Rule_Def.Erule = "Erule" - | to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm thm ^ ")" - | to_string (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)" - | to_string (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" - | to_string (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")"; + | to_string _ (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)" + | to_string _ (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" + | to_string _ (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")"; fun to_string_short Rule_Def.Erule = "Erule" | to_string_short (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")" | to_string_short (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)" @@ -78,13 +72,13 @@ fun thm_id (Rule_Def.Thm (id, _)) = id | thm_id _ = raise ERROR ("Rule.thm_id: uncovered case " (* ^ to_string r *)) -fun thm (Rule_Def.Thm (_, thm)) = thm - | thm r = raise ERROR ("Rule.thm: uncovered case " ^ to_string r) +fun thm _ (Rule_Def.Thm (_, thm)) = thm + | thm ctxt r = raise ERROR ("Rule.thm: uncovered case " ^ to_string ctxt r) -fun eval (Eval e) = e - | eval r = raise ERROR ("Rule.eval NOT FOR " ^ to_string r) -fun rls (Rls_ rls) = rls - | rls r = raise ERROR ("Rule.rls NOT FOR " ^ to_string r) +fun eval _ (Eval e) = e + | eval ctxt r = raise ERROR ("Rule.eval NOT FOR " ^ to_string ctxt r) +fun rls _ (Rls_ rls) = rls + | rls ctxt r = raise ERROR ("Rule.rls NOT FOR " ^ to_string ctxt r) (* ML antiquotations *) diff -r 52e8e77920b9 -r ea7db4f4f837 src/Tools/isac/Interpret/derive.sml --- a/src/Tools/isac/Interpret/derive.sml Tue Jan 10 10:01:05 2023 +0100 +++ b/src/Tools/isac/Interpret/derive.sml Tue Jan 10 17:07:53 2023 +0100 @@ -100,7 +100,7 @@ (case Rewrite.rewrite_set_ ctxt true rls t of NONE => rew_once lim rts t apno rs' | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs') - | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string_PIDE ctxt rule)) + | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string ctxt rule)) | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []" in rew_once (Config.get ctxt rewrite_limit) [] tt Noap rs end diff -r 52e8e77920b9 -r ea7db4f4f837 src/Tools/isac/Knowledge/Rational.thy --- a/src/Tools/isac/Knowledge/Rational.thy Tue Jan 10 10:01:05 2023 +0100 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Jan 10 17:07:53 2023 +0100 @@ -491,7 +491,9 @@ fun locate_rule thy eval_rls ro [rs] t r = if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r) then - let val ropt = Rewrite.rewrite_ (Proof_Context.init_global thy) ro eval_rls true (Rule.thm r) t; + let + val ctxt = Proof_Context.init_global thy + val ropt = Rewrite.rewrite_ ctxt ro eval_rls true (Rule.thm ctxt r) t; in case ropt of SOME ta => [(r, ta)] | NONE => ((*tracing @@ -552,7 +554,9 @@ fun locate_rule thy eval_rls ro [rs] t r = if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r) then - let val ropt = Rewrite.rewrite_ (Proof_Context.init_global thy) ro eval_rls true (Rule.thm r) t; + let + val ctxt = Proof_Context.init_global thy + val ropt = Rewrite.rewrite_ ctxt ro eval_rls true (Rule.thm ctxt r) t; in case ropt of SOME ta => [(r, ta)] diff -r 52e8e77920b9 -r ea7db4f4f837 src/Tools/isac/MathEngBasic/istate-def.sml --- a/src/Tools/isac/MathEngBasic/istate-def.sml Tue Jan 10 10:01:05 2023 +0100 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml Tue Jan 10 17:07:53 2023 +0100 @@ -86,14 +86,14 @@ val empty = Pstate e_pstate; fun rta2str ctxt (r, (t, a)) = - "\n(" ^ Rule.to_string_PIDE ctxt r ^ ", (" ^ UnparseC.term_in_ctxt ctxt t ^ ", " ^ + "\n(" ^ Rule.to_string ctxt r ^ ", (" ^ UnparseC.term_in_ctxt ctxt t ^ ", " ^ UnparseC.terms_in_ctxt ctxt a ^ "))"; fun string_of _ Uistate = "Uistate" | string_of _ (Pstate pst) = "Pstate " ^ pstate2str pst | string_of ctxt (RrlsState (t, t1, rss, rtas)) = "RrlsState (" ^ UnparseC.term t ^ ", " ^ UnparseC.term_in_ctxt ctxt t1 ^ ", " ^ - (strs2str o (map (strs2str o (map (Rule.to_string_PIDE ctxt))))) rss ^ ", " ^ + (strs2str o (map (strs2str o (map (Rule.to_string ctxt))))) rss ^ ", " ^ (strs2str o (map (rta2str ctxt))) rtas ^ ")"; fun string_of' Uistate = "Uistate" | string_of' (Pstate pst) = diff -r 52e8e77920b9 -r ea7db4f4f837 src/Tools/isac/MathEngBasic/rewrite.sml --- a/src/Tools/isac/MathEngBasic/rewrite.sml Tue Jan 10 10:01:05 2023 +0100 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Tue Jan 10 17:07:53 2023 +0100 @@ -207,7 +207,7 @@ (case rewrite__set_ ctxt (i + 1) put_asm bdv rls' ct of SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms | NONE => rew_once ruls asm ct apno thms) - | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string_PIDE ctxt r ^ "\""); + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string ctxt r ^ "\""); val ruls = (#rules o Rule_Set.rep) rls; val _ = trace_eq1 ctxt i "rls" rls ct val (ct', asm') = rew_once ruls [] ct Noap ruls; diff -r 52e8e77920b9 -r ea7db4f4f837 src/Tools/isac/MathEngBasic/state-steps.sml --- a/src/Tools/isac/MathEngBasic/state-steps.sml Tue Jan 10 10:01:05 2023 +0100 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml Tue Jan 10 17:07:53 2023 +0100 @@ -57,7 +57,7 @@ Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)), (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty))) | make_single ctxt _ _ (t, r, _) = raise ERROR ("State_Steps.make_single: not impl. for " ^ - Rule.to_string_PIDE ctxt r ^ " at " ^ UnparseC.term_in_ctxt ctxt t) + Rule.to_string ctxt r ^ " at " ^ UnparseC.term_in_ctxt ctxt t) (* update pos in tacis for embedding by generate *) fun insert_pos (_: Pos.pos) [] = [] diff -r 52e8e77920b9 -r ea7db4f4f837 src/Tools/isac/MathEngBasic/tactic.sml --- a/src/Tools/isac/MathEngBasic/tactic.sml Tue Jan 10 10:01:05 2023 +0100 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Tue Jan 10 17:07:53 2023 +0100 @@ -260,7 +260,7 @@ | rule2tac ctxt subst (Rule.Rls_ rls) = Rewrite_Set_Inst (Subst.T_to_input ctxt subst, (Rule_Set.id rls)) | rule2tac ctxt _ rule = - raise ERROR ("rule2tac: called with \"" ^ Rule.to_string_PIDE ctxt rule ^ "\""); + raise ERROR ("rule2tac: called with \"" ^ Rule.to_string ctxt rule ^ "\""); (* try if a rewrite-rule is applicable to a given formula; in case of rule-sets (recursivley) collect all _atomic_ rewrites *) diff -r 52e8e77920b9 -r ea7db4f4f837 src/Tools/isac/MathEngBasic/thmC.sml --- a/src/Tools/isac/MathEngBasic/thmC.sml Tue Jan 10 10:01:05 2023 +0100 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Tue Jan 10 17:07:53 2023 +0100 @@ -65,7 +65,7 @@ fun of_thm thm = (id_of_thm thm, thm); fun from_rule _ (Rule.Thm (id, thm)) = (id, thm) | from_rule ctxt r = - raise ERROR ("ThmC.from_rule: not defined for " ^ Rule.to_string_PIDE ctxt r); + raise ERROR ("ThmC.from_rule: not defined for " ^ Rule.to_string ctxt r); \<^isac_test>\ fun string_of_thm_in_thy thy thm = @@ -151,7 +151,7 @@ | _ => "sym_" ^ thmID in Rule.Thm (thmID', thm') end | make_sym_rule _ (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls) - | make_sym_rule ctxt r = raise ERROR ("ThmC.make_sym_rule: not for " ^ Rule.to_string_PIDE ctxt r) + | make_sym_rule ctxt r = raise ERROR ("ThmC.make_sym_rule: not for " ^ Rule.to_string ctxt r) \<^isac_test>\ (* revert a thm RS @{thm sym} back to original thm, in case it ML\is_sym\ *) @@ -167,7 +167,7 @@ else Rule.Thm (Thm.get_name_hint thm, thm) (*recover the thy the thm comes from*) | revert_sym_rule thy rule = raise ERROR ("ThmC.revert_sym_rule: NOT for " ^ - Rule.to_string_PIDE (Proof_Context.init_global thy) rule) + Rule.to_string (Proof_Context.init_global thy) rule) \ diff -r 52e8e77920b9 -r ea7db4f4f837 src/Tools/isac/ProgLang/Auto_Prog.thy --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Tue Jan 10 10:01:05 2023 +0100 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Tue Jan 10 17:07:53 2023 +0100 @@ -132,7 +132,8 @@ | rule2stac thy (Rule.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ HOLogic.mk_string (get_calc_prog_id (Proof_Context.init_global thy) c))) | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule_Set.id rls)) - | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule.to_string r ^ "\""); + | rule2stac thy r = raise ERROR ("rule2stac: not applicable to \"" ^ + Rule.to_string (Proof_Context.init_global thy) r ^ "\""); fun rule2stac_inst _ (Rule.Thm (thmID, _)) = Try $ (Repeat $ (Rew_Inst $ Subs $ HOLogic.mk_string thmID)) | rule2stac_inst thy (Rule.Eval (c, _)) = @@ -141,7 +142,8 @@ Try $ (Repeat $ (Cal $ HOLogic.mk_string (get_calc_prog_id (Proof_Context.init_global thy) c))) | rule2stac_inst _ (Rule.Rls_ rls) = Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule_Set.id rls)) - | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule.to_string r ^ "\""); + | rule2stac_inst thy r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ + Rule.to_string (Proof_Context.init_global thy) r ^ "\""); (*for appropriate nesting take stacs in _reverse_ order*) fun op #>@ sts [s] = SEq $ s $ sts diff -r 52e8e77920b9 -r ea7db4f4f837 test/Tools/isac/Knowledge/rational-2.sml --- a/test/Tools/isac/Knowledge/rational-2.sml Tue Jan 10 10:01:05 2023 +0100 +++ b/test/Tools/isac/Knowledge/rational-2.sml Tue Jan 10 17:07:53 2023 +0100 @@ -718,15 +718,15 @@ (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id) then () else error "first element of revset changed"; if -(revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\", ?r1 \ 2 = ?r1 * ?r1)" andalso -(revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 \ 2\", 9 = 3 \ 2)" andalso -(revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\", 6 * x = 2 * (3 * x))" +(revsets |> nth 1 |> nth 1 |> Rule.to_string ctxt) = "Thm (\"realpow_twoI\", ?r1 \ 2 = ?r1 * ?r1)" andalso +(revsets |> nth 1 |> nth 2 |> Rule.to_string ctxt) = "Thm (\"#: 9 = 3 \ 2\", 9 = 3 \ 2)" andalso +(revsets |> nth 1 |> nth 3 |> Rule.to_string ctxt) = "Thm (\"#: 6 * x = 2 * (3 * x)\", 6 * x = 2 * (3 * x))" andalso -(revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: - 3 * x = - 1 * (3 * x)\", - 3 * x = - 1 * (3 * x))" +(revsets |> nth 1 |> nth 4 |> Rule.to_string ctxt) = "Thm (\"#: - 3 * x = - 1 * (3 * x)\", - 3 * x = - 1 * (3 * x))" andalso -(revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\", 9 = 3 * 3)" andalso -(revsets |> nth 1 |> nth 6 |> Rule.to_string) = "Rls_ (\"sym_order_mult_rls_\")" andalso -(revsets |> nth 1 |> nth 7 |> Rule.to_string) = +(revsets |> nth 1 |> nth 5 |> Rule.to_string ctxt) = "Thm (\"#: 9 = 3 * 3\", 9 = 3 * 3)" andalso +(revsets |> nth 1 |> nth 6 |> Rule.to_string ctxt) = "Rls_ (\"sym_order_mult_rls_\")" andalso +(revsets |> nth 1 |> nth 7 |> Rule.to_string ctxt) = "Thm (\"sym_mult.assoc\", ?a * (?b * ?c) = ?a * ?b * ?c)" then () else error "first 7 elements in revset changed" @@ -1581,7 +1581,7 @@ (*default_print_depth 99;*) map ((UnparseC.term_in_ctxt ctxt) o #1) der; (*default_print_depth 3;*) "...,(- 1 * b \ 2 + a \ 2) / (- 2 * (a * b) + a \ 2 + (- 1 * b) \ 2) ]"; -(*default_print_depth 99;*) map (Rule.to_string o #2) der; (*default_print_depth 3;*) +(*default_print_depth 99;*) map ((Rule.to_string ctxt) o #2) der; (*default_print_depth 3;*) (*default_print_depth 99;*) map ((UnparseC.term_in_ctxt ctxt) o #1 o #3) der; (*default_print_depth 3;*) val der = Derive.do_one ctxt Atools_erls rules ro NONE