# HG changeset patch # User wneuper # Date 1668590992 -3600 # Node ID 777d05447375a4c9dd56058ea73632342cef896a # Parent 35846e25713ec732ef9500f7ab315bf54cfd290c make Minisubplb/200-start-method independent #2: Tactic.Rewrite_Set partially diff -r 35846e25713e -r 777d05447375 TODO.md --- a/TODO.md Thu Nov 10 14:25:38 2022 +0100 +++ b/TODO.md Wed Nov 16 10:29:52 2022 +0100 @@ -51,6 +51,7 @@ ***** priority of WN items is top down, most urgent/simple on top * WN?: improve Problem/MethodC..prep_input after meeting MW: why parse twice? +* WN: eliminate multiple get_ctxt in Solve_Step, Ctree * WN: Know_Store.get_thes, add_thes still required for Error_Patterns, we want to eliminate thes: (1) Error_Pattern.T are already stored by MethodC -- place them in respective thys (2) Error_Pattern.fill_in stored with thm (in thes): instead introduce new Thy_Data for them. diff -r 35846e25713e -r 777d05447375 src/Tools/isac/BaseDefinitions/rule-set.sml --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Thu Nov 10 14:25:38 2022 +0100 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Wed Nov 16 10:29:52 2022 +0100 @@ -22,6 +22,7 @@ val id_from_rule: Rule.rule -> string val contains: Rule.rule -> T -> bool +(*type for_know_store*) type for_kestore val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool val to_kestore: for_kestore list * for_kestore list -> for_kestore list diff -r 35846e25713e -r 777d05447375 src/Tools/isac/BaseDefinitions/thmC-def.sml --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml Thu Nov 10 14:25:38 2022 +0100 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml Wed Nov 16 10:29:52 2022 +0100 @@ -13,6 +13,9 @@ val string_of_thm: thm -> string val string_of_thms: thm list -> string +(*stepwise replace ^^^ by vvv and finally rename by eliminating "_PIDE"*) + val string_of_thm_PIDE: Proof.context -> thm -> string + val string_of_thms_PIDE: Proof.context -> thm list -> string (* required in ProgLang BEFORE definition in ---------------vvv *) val int_opt_of_string: string -> int option (* belongs to TermC *) @@ -33,7 +36,15 @@ val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge")) val ctxt' = Config.put show_markup false ctxt in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; -fun string_of_thms thms = (strs2str o (map string_of_thm)) thms +fun string_of_thms thms = (strs2str o (map (string_of_thm))) thms + +fun string_of_thm_PIDE ctxt thm = + let + val t = Thm.prop_of thm + (*val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))*) + val ctxt' = Config.put show_markup false ctxt + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; +fun string_of_thms_PIDE ctxt thms = (strs2str o (map (string_of_thm_PIDE ctxt))) thms fun int_opt_of_string str = let diff -r 35846e25713e -r 777d05447375 src/Tools/isac/Build_Isac.thy --- a/src/Tools/isac/Build_Isac.thy Thu Nov 10 14:25:38 2022 +0100 +++ b/src/Tools/isac/Build_Isac.thy Wed Nov 16 10:29:52 2022 +0100 @@ -184,6 +184,7 @@ open Rewrite; open Pos; +open TermC; "----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------"; "----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------"; @@ -293,36 +294,411 @@ (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*) \ ML \ (*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*) -\ text \ -(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*) +\ ML \ +(*[1], Res*)val (_, ([(tac''', _, _)], _, (pt''', p'''))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*) \ ML \ (*//----------- step into Apply_Method ----------------------------------------------\\*) (*//------------------ step into Apply_Method ----------------------------------------------\\*) \ ML \ "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p ,((pt, e_pos'), [])); \ ML \ + (*if*) Pos.on_calc_end ip (*else*); \ ML \ + val (_, probl_id, _) = Calc.references (pt, p); \ ML \ - +val _ = + (*case*) tacis (*of*); \ ML \ + (*if*) probl_id = Problem.id_empty (*else*); \ ML \ + Step.switch_specify_solve p_ (pt, ip) \ ML \ +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) + = (p_, (pt, ip)); \ ML \ + (*if*) Pos.on_specification ([], state_pos) (*else*); \ ML \ + LI.do_next (pt, input_pos) \ ML \ +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos); \ ML \ + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); \ ML \ -(*keep for continuing Apply_Method*) -\ ML \ (*------------- continuing Apply_Method -----------------------------------------------*) -(*-------------------- continuing Apply_Method -----------------------------------------------*) -(*kept for continuing Apply_Method*) + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt; +\ ML \ +val LI.Next_Step (ist, ctxt, tac) = + (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*); +\ ML \ + LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp +\ ML \ +"~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos)) + = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp); +\ ML \ + val pos = next_in_prog' pos +\ ML \ + val (pos', c, _, pt) = +Solve_Step.add_general tac_ ic (pt, pos); +\ ML \ +"~~~~~ fun add_general , args:"; val (tac, ic, cs) + = (tac_, ic, (pt, pos)); +\ ML \ + (*if*) Tactic.for_specify' tac (*else*); +\ ML \ +Solve_Step.add tac ic cs +\ ML \ +"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _))) + = (tac, ic, cs); +\ ML \ + val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f + (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete +\ ML \ + val pt = Ctree.update_branch pt p Ctree.TransitiveB +\ ML \ +val return = + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt) (*-------------------- stop step into Apply_Method -------------------------------------------*) \ ML \ (*------------- stop step into Apply_Method -------------------------------------------*) (*\\------------------ step into Apply_Method ----------------------------------------------//*) \ ML \ (*\\----------- step into Apply_Method ----------------------------------------------//*) \ ML \ -\ text \ (* error consecutively*) -(*[2], Res*)val (_, ([(tac, _, _)], _, (pt''''', p'''''))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*) +\ text \ +(*[2], Res*)val (_, ([(tac, _, _)], _, (pt''''', p'''''))) = Step.do_next p''' ((pt''', e_pos'), []);(*Rewrite_Set "Test_simplify"*) +\ ML \ (*//----------- step into Rewrite_Set -----------------------------------------------\\*) +(*//------------------ step into Rewrite_Set -----------------------------------------------\\*) +\ ML \ +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) + = (p''', ((pt''', e_pos'), [])); +\ ML \ + (*if*) Pos.on_calc_end ip (*else*); +\ ML \ + val (_, probl_id, _) = Calc.references (pt, p); +\ ML \ +val _ = + (*case*) tacis (*of*); +\ ML \ + (*if*) probl_id = Problem.id_empty (*else*); +\ text \ + Step.switch_specify_solve p_ (pt, ip); +\ ML \ +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) + = (p_, (pt, ip)); +\ ML \ + (*if*) Pos.on_specification ([], state_pos) (*else*); +\ text \ + LI.do_next (pt, input_pos) +\ ML \ +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos); +\ ML \ + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); +\ ML \ + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt; +\ text \ + (*case*) + LI.find_next_step sc (pt, pos) ist ctxt (*of*); +\ ML \ +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Istate.Pstate ist), ctxt) + = (sc, (pt, pos), ist, ctxt); +\ text \ + (*case*) + LI.scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*); +\ ML \ +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Istate.Pstate (ist as {path, ...}))) + = ((prog, (ptp, ctxt)), (Istate.Pstate ist) ); +\ ML \ + (*if*) path = [] (*else*); +\ text \ + LI.go_scan_up (prog, cc) (Istate.trans_scan_up ist); +\ ML \ +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) + = ((prog, cc), (Istate.trans_scan_up ist)); +\ ML \ + (*if*) path = [R] (*root of the program body*) (*else*); +\ text \ + LI.scan_up pcc (ist |> Istate.path_up) (go_up path sc); +\ ML \ +"~~~~~ fun scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\Tactical.Try\(*2*), _) $ _)) += (pcc, (ist |> Istate.path_up), (go_up path sc)); +\ text \ + LI.go_scan_up pcc ist +\ ML \ +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) + = (pcc, ist); +\ ML \ + (*if*) path = [R] (*root of the program body*) (*else*); +\ text \ + LI.scan_up pcc (ist |> Istate.path_up) (go_up path sc); +\ ML \ +"~~~~~ fun scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\Tactical.Chain\(*3*), _) $ _)) + = (pcc, (ist |> Istate.path_up), (go_up path sc)); +\ ML \ + val e2 = LI.check_Seq_up ist sc +\ text \ + (*case*) + LI.scan_dn cc (ist |> Istate.path_up_down [R]) e2 (*of*); +\ ML \ +"~~~~~ fun scan_dn , args:"; val (cc, (ist as {act_arg, ...}), (Const (\<^const_name>\Tactical.Try\(*2*), _) $ e)) + = (cc, (ist |> Istate.path_up_down [R]), e2 ); +\ text \ + (*case*) + LI.scan_dn cc (ist |> Istate.path_down [R]) e (*of*); +\ ML \ +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t (*fall-through*)) + = (cc, (ist |> Istate.path_down [R]), e); +\ ML \ + (*if*) Tactical.contained_in t (*else*); +\ ML \ +val (Program.Tac prog_tac, form_arg) = + (*case*) LItool.check_leaf "next " ctxt eval (Istate.get_subst ist) t (*of*); +\ text \ + LI.check_tac cc ist (prog_tac, form_arg); +\ ML \ +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) + = (cc, ist, (prog_tac, form_arg)); +\ ML \ + val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac +\ ML \ +val _ = + (*case*) m (*of*); +\ text \ + (*case*) +Solve_Step.check m (pt, p) (*of*); +\ ML \ +"~~~~~ fun check , args:"; val ((Tactic.Rewrite_Set rls), (cs as (pt, pos)) ) + = (m, (pt, p)); +\ ML \ + val ctxt = Ctree.get_loc pt pos |> snd + val thy' = ctxt |> Proof_Context.theory_of |> Context.theory_name + val f = Calc.current_formula cs; +\ text \ + (*case*) + Rewrite.rewrite_set_ ctxt false (get_rls ctxt rls) f (*of*); +\ ML \ +"~~~~~ fun rewrite_set_ , args:"; val (ctxt, bool, rls, term) + = (ctxt, false, (get_rls ctxt rls), f); +\ text \ + Rewrite.rewrite__set_ ctxt 1 bool [] rls term +\ ML \ +"~~~~~ and rewrite__set_ , args:"; val ((*3*)ctxt, i, put_asm, bdv, rls, ct) + = (ctxt, 1, bool, [], rls, term); +\ ML \ +val rewrite_trace_depth = Attrib.setup_config_int \<^binding>\rewrite_trace_depth\ (K 99999); + +fun trace1 ctxt i str = + if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth + then tracing (idt "#" (i + 1) ^ str) else () +fun trace_in1 ctxt i str thmid = + trace1 ctxt i (" " ^ str ^ ": \"" ^ thmid ^ "\"") +fun trace_in2 ctxt i str t = + trace1 ctxt i (" " ^ str ^ ": \"" ^ UnparseC.term_in_ctxt ctxt t ^ "\""); +fun trace_in3 ctxt i str pairopt = + trace1 ctxt i (" " ^ str ^ ": " ^ UnparseC.term_in_ctxt ctxt ((fst o the) pairopt)); +fun msg call ctxt op_ thmC t = + call ^ ": \n" ^ + "Eval.get_pair for " ^ quote op_ ^ " \ SOME (_, " ^ quote (ThmC.string_of_thm_PIDE ctxt thmC) ^ ")\n" ^ + "but rewrite__ on " ^ quote (UnparseC.term_in_ctxt ctxt t) ^ " \ NONE"; + + datatype switch = Appl | Noap; + fun rew_once (*1*)_ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *) + | rew_once (*2*)ruls asm ct Appl [] = + (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls + | Rule_Set.Sequence _ => (ct, asm) + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\"")) + | rew_once (*3*)ruls asm ct apno (rul :: thms) = + case rul of + Rule.Thm (thmid, thm) => + (trace_in1 ctxt i "try thm" thmid; + case Rewrite.rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) + ((#asm_rls o Rule_Set.rep) rls) put_asm thm ct of + NONE => rew_once ruls asm ct apno thms + | SOME (ct', asm') => + (trace_in2 ctxt i "rewrites to" ct'; + rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms))) + (* once again try the same rule, e.g. associativity against "()"*) + | Rule.Eval (cc as (op_, _)) => + let val _ = trace_in1 ctxt i "try calc" op_; + in case Eval.adhoc_thm ctxt cc ct of + NONE => rew_once ruls asm ct apno thms + | SOME (_, thm') => + let + val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) + ((#asm_rls o Rule_Set.rep) rls) put_asm thm' ct; + val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" ctxt op_ thm' ct) + val _ = trace_in3 ctxt i "calc. to" pairopt; + in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end + end + | Rule.Cal1 (cc as (op_, _)) => + let val _ = trace_in1 ctxt i "try cal1" op_; + in case Eval.adhoc_thm1_ ctxt cc ct of + NONE => (ct, asm) + | SOME (_, thm') => + let + val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) + ((#asm_rls o Rule_Set.rep) rls) put_asm thm' ct; + val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^ + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_ctxt ctxt ct ^ " = NONE") + val _ = trace_in3 ctxt i "cal1. to" pairopt; + in the pairopt end + end + | Rule.Rls_ rls' => + (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 r ^ "\""); + +\ ML \ + val ruls = (#rules o Rule_Set.rep) rls; +\ ML \ + val _ = trace_eq1 ctxt i "rls" rls ct +\ text \ + val (ct', asm') = + rew_once ruls [] ct Noap ruls; +\ ML \ +"~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms)) + = (ruls, [], ct, Noap, ruls); +\ ML \ +val Rule.Thm (thmid, thm) = + (*case*) rul (*of*); +\ ML \ +val NONE = + (*case*) rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) + ((#asm_rls o Rule_Set.rep) rls) put_asm thm ct (*of*); +\ text \ + rew_once ruls asm ct apno thms; +\ ML \ +"~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms)) + = (ruls, asm, ct, apno, thms); +\ ML \ +(*+*) val Rule.Thm (thmid, thm)= nth 5 thms; (*fst thm rewriting to SOME*) +\ text \ + (*case*) + rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) + ((#asm_rls o Rule_Set.rep) rls) put_asm thm ct (*of*); +\ ML \ +"~~~~~ fun rewrite__ , args:"; val (ctxt, i, bdv, tless, rls, put_asm, thm, ct) + = (ctxt, (i + 1), bdv:Subst.T, ((snd o #rew_ord o Rule_Set.rep) rls), + ((#asm_rls o Rule_Set.rep) rls), put_asm, thm, ct); +\ ML \ +(* ------------------------------------------^^^.., id = "tval_rls" (*o*) +rls = + Repeat + {asm_rls = + Repeat + {asm_rls = Repeat {asm_rls = Empty, calc = [], errpatts = [], id = "empty", preconds = [], prog_rls = Empty, program = Empty_Prog, rew_ord = ("dummy_ord", fn), rules = []}, calc = [], errpatts = [], id = + "testerls", preconds = [], prog_rls = Empty, program = Empty_Prog, rew_ord = ("termlessI", fn), rules = + [Thm ("refl", "?t = ?t"), Thm ("order_refl", "?x \ ?x"), Thm ("radd_left_cancel_le", "(?k + ?m \ ?k + ?n) = (?m \ ?n)"), Thm ("not_true", "(\ True) = False"), Thm ("not_false", "(\ False) = True"), + Thm ("and_true", "(?a \ True) = ?a"), Thm ("and_false", "(?a \ False) = False"), Thm ("or_true", "(?a \ True) = True"), Thm ("or_false", "(?a \ False) = ?a"), + Thm ("and_commute", "(?a \ ?b) = (?b \ ?a)"), Thm ("or_commute", "(?a \ ?b) = (?b \ ?a)"), Eval ("Prog_Expr.is_num", fn), Eval ("Prog_Expr.matches", fn), Eval ("Groups.plus_class.plus", fn), + Eval ("Groups.times_class.times", fn), Eval ("BaseDefinitions.realpow", fn), Eval ("Orderings.ord_class.less", fn), Eval ("Orderings.ord_class.less_eq", fn), Eval ("Prog_Expr.ident", fn)]}, + calc = [], errpatts = [], id = "tval_rls", preconds = [], prog_rls = + Repeat {asm_rls = Empty, calc = [], errpatts = [], id = "empty", preconds = [], prog_rls = Empty, program = Empty_Prog, rew_ord = ("dummy_ord", fn), rules = []}, program = Empty_Prog, rew_ord = + ("sqrt_right", fn), rules = + [Thm ("refl", "?t = ?t"), Thm ("order_refl", "?x \ ?x"), Thm ("radd_left_cancel_le", "(?k + ?m \ ?k + ?n) = (?m \ ?n)"), Thm ("not_true", "(\ True) = False"), Thm ("not_false", "(\ False) = True"), + Thm ("and_true", "(?a \ True) = ?a"), Thm ("and_false", "(?a \ False) = False"), Thm ("or_true", "(?a \ True) = True"), Thm ("or_false", "(?a \ False) = ?a"), Thm ("and_commute", "(?a \ ?b) = (?b \ ?a)"), + Thm ("or_commute", "(?a \ ?b) = (?b \ ?a)"), Thm ("real_diff_minus", "?a - ?b = ?a + - 1 * ?b"), Thm ("root_ge0", "0 \ ?a \ (0 \ sqrt ?a) = True"), + Thm ("root_add_ge0", "0 \ ?a \ 0 \ ?b \ (0 \ sqrt ?a + sqrt ?b) = True"), Thm ("root_ge0_1", "0 \ ?a \ 0 \ ?b \ 0 \ ?c \ (0 \ ?a * sqrt ?b + sqrt ?c) = True"), + Thm ("root_ge0_2", "0 \ ?a \ 0 \ ?b \ 0 \ ?c \ (0 \ sqrt ?a + ?b * sqrt ?c) = True"), Eval ("Prog_Expr.is_num", fn), Eval ("Test.contains_root", fn), Eval ("Prog_Expr.matches", fn), + Eval ("Test.contains_root", fn), Eval ("Groups.plus_class.plus", fn), Eval ("Groups.times_class.times", fn), Eval ("NthRoot.sqrt", fn), Eval ("BaseDefinitions.realpow", fn), + Eval ("Orderings.ord_class.less", fn), Eval ("Orderings.ord_class.less_eq", fn), Eval ("Prog_Expr.ident", fn)]} +*) +\ ML \ +\ text \ + val (t', asms, _(*lrd*), rew) = + Rewrite.rew_sub ctxt i bdv tless rls put_asm ([]: TermC.path) + (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct +\ ML \ +"~~~~~ and rew_sub , args:"; val (ctxt, i, bdv, tless, rls, put_asm, lrd, r, t) + = (ctxt, i, bdv, tless, rls, put_asm, ([]: TermC.path), + (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct); +\ ML \ + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r +\ ML \ +(* inhibit exn NO_REWRITE + val r' = (Envir.subst_term (Pattern.match (Proof_Context.theory_of ctxt) + (lhs, t) (Vartab.empty, Vartab.empty)) r) + handle Pattern.MATCH => raise NO_REWRITE +*) +(*+*) UnparseC.term_in_ctxt ctxt t = "x + 1 + - 1 * 2 = 0"; +\ ML \ +val t1 $ t2 = + (*case*) t (*of*); +\ ML \ +val (t2', asm2, lrd, rew2) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.R]) r t2 +\ ML \ + (*if*) rew2 (*else*); +\ text \ +val (t1', asm1, lrd, rew1) = + rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.L]) r t1 +\ ML \ +"~~~~~ fun rew_sub , args:"; val (ctxt, i, bdv, tless, rls, put_asm, lrd, r, t) + = (ctxt, i, bdv, tless, rls, put_asm, (lrd @ [TermC.L]), r, t1); +\ ML \ + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r +\ ML \ +(* inhibit exn NO_REWRITE + val r' = (Envir.subst_term (Pattern.match (Proof_Context.theory_of ctxt) + (lhs, t) (Vartab.empty, Vartab.empty)) r) + handle Pattern.MATCH => raise NO_REWRITE +*) +(*+*) UnparseC.term_in_ctxt ctxt t = "(=) (x + 1 + - 1 * 2)"; +\ ML \ +val t1 $ t2 = + (*case*) t (*of*); +\ text \ +val (t2', asm2, lrd, rew2) = + rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.R]) r t2 +\ ML \ +"~~~~~ fun rew_sub , args:"; val (ctxt, i, bdv, tless, rls, put_asm, lrd, r, t) + = (ctxt, i, bdv, tless, rls, put_asm, (lrd @ [TermC.R]), r, t2); +\ ML \ + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r +\ ML \ + val r' = (Envir.subst_term (Pattern.match (Proof_Context.theory_of ctxt) + (lhs, t) (Vartab.empty, Vartab.empty)) r) + handle Pattern.MATCH => raise NO_REWRITE +\ ML \ + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r')) + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r' +\ ML \ +(*+*) UnparseC.term_in_ctxt ctxt t' = "- 1 * 2 + (x + 1)"; +\ ML \ + val (simpl_p', nofalse) = eval__true ctxt (i + 1) p' bdv rls +\ ML \ + (*if*) nofalse (*then*); +\ ML \ + val (t'', p'') = (t', simpl_p') +\ text \ + (*if*) TermC.perm lhs rhs andalso not (tless bdv (t', t)); +\ text \ + (tless bdv (t', t)) +\ ML \ +(*+*)tless; (*vvv--- found (*o*) tval_rls*) +(*+*) val sqrt_right = tval_rls |> (snd o #rew_ord o Rule_Set.rep); +\ ML \ +"~~~~~ fun sqrt_right , args:"; val ((pr:bool), thy, (_: subst), (ts, us)) + = (false, @{theory}(*?!*), bdv, (t', t)); +\ text \ -- hidden by "local" -- delete + (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS ); +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +(*keep for continuing Rewrite_Set*) +\ ML \ (*------------- continuing Rewrite_Set ------------------------------------------------*) +(*-------------------- continuing Rewrite_Set ------------------------------------------------*) +(*kept for continuing XXXXX*) +(*-------------------- stop step into Rewrite_Set --------------------------------------------*) +\ ML \ (*------------- stop step into Rewrite_Set --------------------------------------------*) +(*\\------------------ step into Rewrite_Set -----------------------------------------------//*) +\ ML \ (*\\----------- step into Rewrite_Set -----------------------------------------------//*) \ text \ (*/--------- investigate Rewrite_Set "Test_simplify" -----------------------------------------\*) diff -r 35846e25713e -r 777d05447375 src/Tools/isac/Interpret/derive.sml --- a/src/Tools/isac/Interpret/derive.sml Thu Nov 10 14:25:38 2022 +0100 +++ b/src/Tools/isac/Interpret/derive.sml Wed Nov 16 10:29:52 2022 +0100 @@ -53,11 +53,11 @@ fun msg_2 ctxt thmid = if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying thm \"" ^ thmid ^ "\""); fun msg_3 ctxt t' = - if Config.get ctxt rewrite_trace then tracing ("=== rewrites to: " ^ UnparseC.term t') else (); + if Config.get ctxt rewrite_trace then tracing ("=== rewrites to: " ^ UnparseC.term_in_ctxt ctxt t') else (); fun msg_4 ctxt op_ = if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying calc. \"" ^ op_^"\""); fun msg_5 ctxt t' = - if not (Config.get ctxt rewrite_trace) then () else tracing("=== calc. to: " ^ UnparseC.term t') + if not (Config.get ctxt rewrite_trace) then () else tracing("=== calc. to: " ^ UnparseC.term_in_ctxt ctxt t') fun do_one ctxt asm_rls rs ro goal tt = @@ -65,7 +65,7 @@ datatype switch = Appl | Noap (* TODO: unify with version in Rewrite *) fun rew_once _ rts t Noap [] = (case goal of NONE => rts | SOME _ => - raise ERROR ("Derive.do_one: no derivation for " ^ UnparseC.term t)) + raise ERROR ("Derive.do_one: no derivation for " ^ UnparseC.term_in_ctxt ctxt t)) | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs | rew_once lim rts t apno rs' = (case goal of diff -r 35846e25713e -r 777d05447375 src/Tools/isac/Interpret/li-tool.sml --- a/src/Tools/isac/Interpret/li-tool.sml Thu Nov 10 14:25:38 2022 +0100 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Nov 16 10:29:52 2022 +0100 @@ -85,7 +85,7 @@ in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end | tac_from_prog _ _ (Const (\<^const_name>\Prog_Tac.Calculate\, _) $ op_ $ _) = (Tactic.Calculate (HOLogic.dest_string op_)) - | tac_from_prog _ _ (Const (\<^const_name>\Prog_Tac.Take\, _) $ t) = (Tactic.Take (UnparseC.term t)) + | tac_from_prog _ thy (Const (\<^const_name>\Prog_Tac.Take\, _) $ t) = (Tactic.Take (UnparseC.term_in_thy thy t)) | tac_from_prog _ thy (Const (\<^const_name>\Prog_Tac.Substitute\, _) $ isasub $ _) = Tactic.Substitute (Prog_Tac.Substitute_adapt_to_type thy isasub) | tac_from_prog _ thy (Const (\<^const_name>\Prog_Tac.Check_elementwise\, _) $ _ $ @@ -338,11 +338,13 @@ fun trace_msg_1 ctxt call t stac = if Config.get ctxt LI_trace then - tracing ("@@@ " ^ call ^ " leaf \"" ^ UnparseC.term t ^ "\" \ Tac \"" ^ UnparseC.term stac ^ "\"") + tracing ("@@@ " ^ call ^ " leaf \"" ^ UnparseC.term_in_ctxt ctxt t ^ "\" \ Tac \"" ^ + UnparseC.term_in_ctxt ctxt stac ^ "\"") else (); fun trace_msg_2 ctxt call t lexpr' = if Config.get ctxt LI_trace then - tracing("@@@ " ^ call ^ " leaf '" ^ UnparseC.term t ^ "' \ Expr \"" ^ UnparseC.term lexpr' ^ "\"") + tracing("@@@ " ^ call ^ " leaf '" ^ UnparseC.term_in_ctxt ctxt t ^ "' \ Expr \"" ^ + UnparseC.term_in_ctxt ctxt lexpr' ^ "\"") else (); (* check a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr. diff -r 35846e25713e -r 777d05447375 src/Tools/isac/Interpret/lucas-interpreter.sml --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Nov 10 14:25:38 2022 +0100 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 16 10:29:52 2022 +0100 @@ -255,7 +255,8 @@ | scan_up pcc ist (Const (\<^const_name>\Tactical.If\(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist - | scan_up _ _ t = raise ERROR ("scan_up not impl for " ^ UnparseC.term t) + | scan_up (pcc as (_, (_, ctxt))) _ t = raise ERROR ("scan_up not impl for " ^ + UnparseC.term_in_ctxt ctxt t) (* scan program until an applicable tactic is found *) fun scan_to_tactic (prog, cc) (Pstate (ist as {path, ...})) = @@ -471,7 +472,8 @@ | scan_up1 pcct ist (Const (\<^const_name>\Tactical.If\,_) $ _ $ _ $ _) = go_scan_up1 pcct ist - | scan_up1 _ _ t = raise ERROR ("scan_up1 not impl for t= " ^ UnparseC.term t) + | scan_up1 (_, (_, ctxt, _)) _ t = + raise ERROR ("scan_up1 not impl for t= " ^ UnparseC.term_in_ctxt ctxt t) fun scan_to_tactic1 (prog, (cctt as ((_, p), _, _))) (Pstate (ist as {path, ...})) = if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH find_next_step IN solve*)p diff -r 35846e25713e -r 777d05447375 src/Tools/isac/Interpret/solve-step.sml --- a/src/Tools/isac/Interpret/solve-step.sml Thu Nov 10 14:25:38 2022 +0100 +++ b/src/Tools/isac/Interpret/solve-step.sml Wed Nov 16 10:29:52 2022 +0100 @@ -21,7 +21,6 @@ val get_eval: string -> Pos.pos' -> Ctree.ctree -> string * ThyC.id * Eval.ml \<^isac_test>\ - val get_ctxt: Ctree.ctree -> Pos.pos' -> Proof.context val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Eval.ml_from_prog list \ end @@ -239,10 +238,12 @@ end | check (Tactic.Tac id) (cs as (pt, pos)) = let - val thy = (Ctree.get_loc pt pos |> snd) |> Proof_Context.theory_of + val ctxt = Ctree.get_ctxt pt pos + val thy = ctxt |> Proof_Context.theory_of val f = Calc.current_formula cs; + val f' = UnparseC.term_in_ctxt ctxt f in - Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f)) + Applicable.Yes (Tactic.Tac_ (thy, f', id, f')) end | check (Tactic.Take str) (pt, pos) = let @@ -267,16 +268,16 @@ let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t in (pos, c, Test_Out.EmptyMout, pt) end | NONE => (pos, [], Test_Out.EmptyMout, pt)) - | add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *) + | add (Tactic.Take' t) (l as (_, ctxt)) (pt, (p, _)) = (* val (Take' t) = m; *) let val p = let val (ps, p') = split_last p (* no connex to prev.ppobj *) in if p' = 0 then ps @ [1] else p end val (pt, c) = Ctree.cappend_form pt p l t in - ((p, Pos.Frm), c, Test_Out.FormKF (UnparseC.term t), pt) + ((p, Pos.Frm), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt t), pt) end - | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Frm)) = + | add (Tactic.Begin_Trans' t) (l as (_, ctxt)) (pt, (p, Pos.Frm)) = let val (pt, c) = Ctree.cappend_form pt p l t val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*) @@ -284,17 +285,17 @@ val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*) in - ((p, Pos.Frm), c @ c', Test_Out.FormKF (UnparseC.term t), pt) + ((p, Pos.Frm), c @ c', Test_Out.FormKF (UnparseC.term_in_ctxt ctxt t), pt) end | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Res)) = (*append after existing PrfObj vvvvvvvvvvvvv*) add (Tactic.Begin_Trans' t) l (pt, (Pos.lev_on p, Pos.Frm)) - | add (Tactic.End_Trans' tasm) l (pt, (p, _)) = + | add (Tactic.End_Trans' tasm) (l as (_, ctxt)) (pt, (p, _)) = let val p' = Pos.lev_up p val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete in - ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt) + ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*UnparseC.term_in_ctxt ctxt t*), pt) end | add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) = let @@ -302,14 +303,14 @@ (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete; val pt = Ctree.update_branch pt p Ctree.TransitiveB in - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt) + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt) end | add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) = let val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete val pt = Ctree.update_branch pt p Ctree.TransitiveB in - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt) + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt) end | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) = let @@ -317,7 +318,7 @@ (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete val pt = Ctree.update_branch pt p Ctree.TransitiveB in - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt) + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt) end | add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) = let @@ -325,37 +326,37 @@ (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete val pt = Ctree.update_branch pt p Ctree.TransitiveB in - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt) + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt) end - | add (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) = + | add (Tactic.Check_Postcond' (_, scval)) (l as (_, ctxt)) (pt, (p, _)) = let val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete in - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term scval), pt) + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt scval), pt) end - | add (Tactic.Calculate' (_, op_, f, (f', _))) l (pt, (p, _)) = + | add (Tactic.Calculate' (_, op_, f, (f', _))) (l as (_, ctxt)) (pt, (p, _)) = let val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete in - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt) + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt) end - | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (pt, (p, _)) = + | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) (l as (_, ctxt)) (pt, (p, _)) = let val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete in - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt) + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt) end - | add (Tactic.Or_to_List' (ors, list)) l (pt, (p, _)) = + | add (Tactic.Or_to_List' (ors, list)) (l as (_, ctxt)) (pt, (p, _)) = let val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete in - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term list), pt) + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt list), pt) end - | add (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) = + | add (Tactic.Substitute' (_, _, subte, t, t')) (l as (_, ctxt)) (pt, (p, _)) = let val (pt,c) = Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete - in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term t'), pt) + in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt t'), pt) end | add (Tactic.Tac_ (_, f, id, f')) l (pt, pos as (p, _)) = let diff -r 35846e25713e -r 777d05447375 src/Tools/isac/Knowledge/Root.thy --- a/src/Tools/isac/Knowledge/Root.thy Thu Nov 10 14:25:38 2022 +0100 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Nov 16 10:29:52 2022 +0100 @@ -104,14 +104,14 @@ fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord) - | term_ord' pr _(*thy*) (t, u) = + | term_ord' pr thy (t, u) = (if pr then let val (f, ts) = strip_comb t and (g, us) = strip_comb u; - val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^"\" @ \"[" ^ - commas (map UnparseC.term ts) ^ "]\""); + val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_ctxt (Proof_Context.init_global thy) f ^"\" @ \"[" ^ + commas (map (UnparseC.term_in_ctxt (Proof_Context.init_global thy)) ts) ^ "]\""); val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^ - commas (map UnparseC.term us) ^ "]\""); + commas (map (UnparseC.term_in_ctxt (Proof_Context.init_global thy)) us) ^ "]\""); val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int(size_of_term' t) ^", " ^ string_of_int(size_of_term' u) ^")"); diff -r 35846e25713e -r 777d05447375 src/Tools/isac/MathEngBasic/rewrite.sml --- a/src/Tools/isac/MathEngBasic/rewrite.sml Thu Nov 10 14:25:38 2022 +0100 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Wed Nov 16 10:29:52 2022 +0100 @@ -20,15 +20,16 @@ val rewrite_set_inst_: Proof.context -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option val rewrite_terms_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> term list -> term -> (term * term list) option - -\<^isac_test>\ +(*from isac_test for Minisubpbl*) val rewrite__: Proof.context -> int -> Subst.T -> Rewrite_Ord.function -> Rule_Set.T -> bool -> thm -> term -> (term * term list) option val rewrite__set_: Proof.context -> int -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option + val trace_eq1 : Proof.context -> int -> string -> Rule_Def.rule_set -> term -> unit; + +\<^isac_test>\ val app_rev: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool val app_sub: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool val trace1: Proof.context -> int -> string -> unit - val trace_eq1 : Proof.context -> int -> string -> Rule_Def.rule_set -> term -> unit; val trace_eq2 : Proof.context -> int -> string -> term -> term -> unit; val trace_in1 : Proof.context -> int -> string -> string -> unit; val trace_in2 : Proof.context -> int -> string -> term -> unit; @@ -87,7 +88,7 @@ else(); fun msg call ctxt op_ thmC t = call ^ ": \n" ^ - "Eval.get_pair for " ^ quote op_ ^ " \ SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^ + "Eval.get_pair for " ^ quote op_ ^ " \ SOME (_, " ^ quote (ThmC.string_of_thm_PIDE ctxt thmC) ^ ")\n" ^ "but rewrite__ on " ^ quote (UnparseC.term_in_ctxt ctxt t) ^ " \ NONE"; fun rewrite__ ctxt i bdv tless rls put_asm thm ct = @@ -198,7 +199,7 @@ val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) ((#asm_rls o Rule_Set.rep) rls) put_asm thm' ct; val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^ - ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_ctxt ctxt ct ^ " = NONE") + ThmC.string_of_thm_PIDE ctxt thm' ^ "\" " ^ UnparseC.term_in_ctxt ctxt ct ^ " = NONE") val _ = trace_in3 ctxt i "cal1. to" pairopt; in the pairopt end end @@ -261,8 +262,8 @@ fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls; (* rewriting without internal arguments 1, [] *) -fun rewrite_ thy rew_ord asm_rls bool thm term = rewrite__ thy 1 [] rew_ord asm_rls bool thm term; -fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term; +fun rewrite_ ctxt rew_ord asm_rls bool thm term = rewrite__ ctxt 1 [] rew_ord asm_rls bool thm term; +fun rewrite_set_ ctxt bool rls term = rewrite__set_ ctxt 1 bool [] rls term; (* variants of rewrite; TODO del. put_asm *) fun rewrite_inst_ thy rew_ord rls put_asm subst thm ct = diff -r 35846e25713e -r 777d05447375 src/Tools/isac/MathEngBasic/thmC.sml --- a/src/Tools/isac/MathEngBasic/thmC.sml Thu Nov 10 14:25:38 2022 +0100 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Wed Nov 16 10:29:52 2022 +0100 @@ -13,8 +13,14 @@ val cut_id: string -> id val long_id: T -> long_id + val string_of_thm: thm -> string val string_of_thms: thm list -> string +(*stepwise replace ^^^ by vvv and finally rename by eliminating "_PIDE"*) +(*val string_of:*) + val string_of_thm_PIDE: Proof.context -> thm -> string + val string_of_thms_PIDE: Proof.context -> thm list -> string + val id_of_thm: thm -> id val of_thm: thm -> T val from_rule : Rule.rule -> T @@ -53,6 +59,8 @@ val string_of_thm = ThmC_Def.string_of_thm; val string_of_thms = ThmC_Def.string_of_thms; +val string_of_thm_PIDE = ThmC_Def.string_of_thm_PIDE; +val string_of_thms_PIDE = ThmC_Def.string_of_thms_PIDE; fun id_of_thm thm = thm |> Thm.get_name_hint |> cut_id; fun of_thm thm = (id_of_thm thm, thm); diff -r 35846e25713e -r 777d05447375 test/Tools/isac/MathEngine/mathengine-stateless.sml --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Nov 10 14:25:38 2022 +0100 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Nov 16 10:29:52 2022 +0100 @@ -117,7 +117,7 @@ Step_Specify.nxt_specify_init_calc ctxt (fmz, sp); "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp); (*val (_, hdl, (dI, pI, mI), pors, pctxt) =*) - initialise ctxt (fmz, (dI, pI, mI)); +Step_Specify.initialise ctxt (fmz, (dI, pI, mI)); "~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, (dI, pI, mI)); val thy = ThyC.get_theory dI val ctxt = Proof_Context.init_global thy; diff -r 35846e25713e -r 777d05447375 test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Thu Nov 10 14:25:38 2022 +0100 +++ b/test/Tools/isac/Test_Isac.thy Wed Nov 16 10:29:52 2022 +0100 @@ -235,7 +235,7 @@ ML_file "Minisubpbl/000-comments.sml" ML_file "Minisubpbl/100-init-rootpbl.sml" ML_file "Minisubpbl/150a-add-given-Maximum.sml" - ML_file "Minisubpbl/150b-add-given-Equation.sml" + ML_file "Minisubpbl/150-add-given-Equation.sml" ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml" ML_file "Minisubpbl/200-start-method.sml" ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml" diff -r 35846e25713e -r 777d05447375 test/Tools/isac/Test_Isac_Short.thy --- a/test/Tools/isac/Test_Isac_Short.thy Thu Nov 10 14:25:38 2022 +0100 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Nov 16 10:29:52 2022 +0100 @@ -204,7 +204,7 @@ ML_file "BaseDefinitions/libraryC.sml" ML_file "BaseDefinitions/rule-def.sml" ML_file "BaseDefinitions/eval-def.sml" - ML_file "BaseDefinitions/rewrite-order.sml" + ML_file "BaseDefinitions/rewrite-order.sml" ML_file "BaseDefinitions/theoryC.sml" ML_file "BaseDefinitions/rule.sml" ML_file "BaseDefinitions/thmC-def.sml"