1.1 --- a/TODO.md Thu Nov 10 14:25:38 2022 +0100
1.2 +++ b/TODO.md Wed Nov 16 10:29:52 2022 +0100
1.3 @@ -51,6 +51,7 @@
1.4 ***** priority of WN items is top down, most urgent/simple on top
1.5
1.6 * WN?: improve Problem/MethodC..prep_input after meeting MW: why parse twice?
1.7 +* WN: eliminate multiple get_ctxt in Solve_Step, Ctree
1.8 * WN: Know_Store.get_thes, add_thes still required for Error_Patterns, we want to eliminate thes:
1.9 (1) Error_Pattern.T are already stored by MethodC -- place them in respective thys
1.10 (2) Error_Pattern.fill_in stored with thm (in thes): instead introduce new Thy_Data for them.
2.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Thu Nov 10 14:25:38 2022 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Wed Nov 16 10:29:52 2022 +0100
2.3 @@ -22,6 +22,7 @@
2.4 val id_from_rule: Rule.rule -> string
2.5 val contains: Rule.rule -> T -> bool
2.6
2.7 +(*type for_know_store*)
2.8 type for_kestore
2.9 val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
2.10 val to_kestore: for_kestore list * for_kestore list -> for_kestore list
3.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml Thu Nov 10 14:25:38 2022 +0100
3.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml Wed Nov 16 10:29:52 2022 +0100
3.3 @@ -13,6 +13,9 @@
3.4
3.5 val string_of_thm: thm -> string
3.6 val string_of_thms: thm list -> string
3.7 +(*stepwise replace ^^^ by vvv and finally rename by eliminating "_PIDE"*)
3.8 + val string_of_thm_PIDE: Proof.context -> thm -> string
3.9 + val string_of_thms_PIDE: Proof.context -> thm list -> string
3.10
3.11 (* required in ProgLang BEFORE definition in ---------------vvv *)
3.12 val int_opt_of_string: string -> int option (* belongs to TermC *)
3.13 @@ -33,7 +36,15 @@
3.14 val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
3.15 val ctxt' = Config.put show_markup false ctxt
3.16 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
3.17 -fun string_of_thms thms = (strs2str o (map string_of_thm)) thms
3.18 +fun string_of_thms thms = (strs2str o (map (string_of_thm))) thms
3.19 +
3.20 +fun string_of_thm_PIDE ctxt thm =
3.21 + let
3.22 + val t = Thm.prop_of thm
3.23 + (*val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))*)
3.24 + val ctxt' = Config.put show_markup false ctxt
3.25 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
3.26 +fun string_of_thms_PIDE ctxt thms = (strs2str o (map (string_of_thm_PIDE ctxt))) thms
3.27
3.28 fun int_opt_of_string str =
3.29 let
4.1 --- a/src/Tools/isac/Build_Isac.thy Thu Nov 10 14:25:38 2022 +0100
4.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Nov 16 10:29:52 2022 +0100
4.3 @@ -184,6 +184,7 @@
4.4
4.5 open Rewrite;
4.6 open Pos;
4.7 +open TermC;
4.8
4.9 "----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
4.10 "----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
4.11 @@ -293,36 +294,411 @@
4.12 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
4.13 \<close> ML \<open>
4.14 (*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
4.15 -\<close> text \<open>
4.16 -(*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
4.17 +\<close> ML \<open>
4.18 +(*[1], Res*)val (_, ([(tac''', _, _)], _, (pt''', p'''))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
4.19 \<close> ML \<open> (*//----------- step into Apply_Method ----------------------------------------------\\*)
4.20 (*//------------------ step into Apply_Method ----------------------------------------------\\*)
4.21 \<close> ML \<open>
4.22 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
4.23 = (p ,((pt, e_pos'), []));
4.24 \<close> ML \<open>
4.25 + (*if*) Pos.on_calc_end ip (*else*);
4.26 \<close> ML \<open>
4.27 + val (_, probl_id, _) = Calc.references (pt, p);
4.28 \<close> ML \<open>
4.29 -
4.30 +val _ =
4.31 + (*case*) tacis (*of*);
4.32 \<close> ML \<open>
4.33 + (*if*) probl_id = Problem.id_empty (*else*);
4.34 \<close> ML \<open>
4.35 + Step.switch_specify_solve p_ (pt, ip)
4.36 \<close> ML \<open>
4.37 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))
4.38 + = (p_, (pt, ip));
4.39 \<close> ML \<open>
4.40 + (*if*) Pos.on_specification ([], state_pos) (*else*);
4.41 \<close> ML \<open>
4.42 + LI.do_next (pt, input_pos)
4.43 \<close> ML \<open>
4.44 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
4.45 \<close> ML \<open>
4.46 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
4.47 \<close> ML \<open>
4.48 -(*keep for continuing Apply_Method*)
4.49 -\<close> ML \<open> (*------------- continuing Apply_Method -----------------------------------------------*)
4.50 -(*-------------------- continuing Apply_Method -----------------------------------------------*)
4.51 -(*kept for continuing Apply_Method*)
4.52 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
4.53 +\<close> ML \<open>
4.54 +val LI.Next_Step (ist, ctxt, tac) =
4.55 + (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
4.56 +\<close> ML \<open>
4.57 + LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp
4.58 +\<close> ML \<open>
4.59 +"~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos))
4.60 + = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
4.61 +\<close> ML \<open>
4.62 + val pos = next_in_prog' pos
4.63 +\<close> ML \<open>
4.64 + val (pos', c, _, pt) =
4.65 +Solve_Step.add_general tac_ ic (pt, pos);
4.66 +\<close> ML \<open>
4.67 +"~~~~~ fun add_general , args:"; val (tac, ic, cs)
4.68 + = (tac_, ic, (pt, pos));
4.69 +\<close> ML \<open>
4.70 + (*if*) Tactic.for_specify' tac (*else*);
4.71 +\<close> ML \<open>
4.72 +Solve_Step.add tac ic cs
4.73 +\<close> ML \<open>
4.74 +"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
4.75 + = (tac, ic, cs);
4.76 +\<close> ML \<open>
4.77 + val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
4.78 + (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
4.79 +\<close> ML \<open>
4.80 + val pt = Ctree.update_branch pt p Ctree.TransitiveB
4.81 +\<close> ML \<open>
4.82 +val return =
4.83 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
4.84 (*-------------------- stop step into Apply_Method -------------------------------------------*)
4.85 \<close> ML \<open> (*------------- stop step into Apply_Method -------------------------------------------*)
4.86 (*\\------------------ step into Apply_Method ----------------------------------------------//*)
4.87 \<close> ML \<open> (*\\----------- step into Apply_Method ----------------------------------------------//*)
4.88 \<close> ML \<open>
4.89 -\<close> text \<open> (* error consecutively*)
4.90 -(*[2], Res*)val (_, ([(tac, _, _)], _, (pt''''', p'''''))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
4.91 +\<close> text \<open>
4.92 +(*[2], Res*)val (_, ([(tac, _, _)], _, (pt''''', p'''''))) = Step.do_next p''' ((pt''', e_pos'), []);(*Rewrite_Set "Test_simplify"*)
4.93 +\<close> ML \<open> (*//----------- step into Rewrite_Set -----------------------------------------------\\*)
4.94 +(*//------------------ step into Rewrite_Set -----------------------------------------------\\*)
4.95 +\<close> ML \<open>
4.96 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
4.97 + = (p''', ((pt''', e_pos'), []));
4.98 +\<close> ML \<open>
4.99 + (*if*) Pos.on_calc_end ip (*else*);
4.100 +\<close> ML \<open>
4.101 + val (_, probl_id, _) = Calc.references (pt, p);
4.102 +\<close> ML \<open>
4.103 +val _ =
4.104 + (*case*) tacis (*of*);
4.105 +\<close> ML \<open>
4.106 + (*if*) probl_id = Problem.id_empty (*else*);
4.107 +\<close> text \<open>
4.108 + Step.switch_specify_solve p_ (pt, ip);
4.109 +\<close> ML \<open>
4.110 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))
4.111 + = (p_, (pt, ip));
4.112 +\<close> ML \<open>
4.113 + (*if*) Pos.on_specification ([], state_pos) (*else*);
4.114 +\<close> text \<open>
4.115 + LI.do_next (pt, input_pos)
4.116 +\<close> ML \<open>
4.117 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
4.118 +\<close> ML \<open>
4.119 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
4.120 +\<close> ML \<open>
4.121 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
4.122 +\<close> text \<open>
4.123 + (*case*)
4.124 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
4.125 +\<close> ML \<open>
4.126 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Istate.Pstate ist), ctxt)
4.127 + = (sc, (pt, pos), ist, ctxt);
4.128 +\<close> text \<open>
4.129 + (*case*)
4.130 + LI.scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
4.131 +\<close> ML \<open>
4.132 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Istate.Pstate (ist as {path, ...})))
4.133 + = ((prog, (ptp, ctxt)), (Istate.Pstate ist) );
4.134 +\<close> ML \<open>
4.135 + (*if*) path = [] (*else*);
4.136 +\<close> text \<open>
4.137 + LI.go_scan_up (prog, cc) (Istate.trans_scan_up ist);
4.138 +\<close> ML \<open>
4.139 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
4.140 + = ((prog, cc), (Istate.trans_scan_up ist));
4.141 +\<close> ML \<open>
4.142 + (*if*) path = [R] (*root of the program body*) (*else*);
4.143 +\<close> text \<open>
4.144 + LI.scan_up pcc (ist |> Istate.path_up) (go_up path sc);
4.145 +\<close> ML \<open>
4.146 +"~~~~~ fun scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ _))
4.147 += (pcc, (ist |> Istate.path_up), (go_up path sc));
4.148 +\<close> text \<open>
4.149 + LI.go_scan_up pcc ist
4.150 +\<close> ML \<open>
4.151 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
4.152 + = (pcc, ist);
4.153 +\<close> ML \<open>
4.154 + (*if*) path = [R] (*root of the program body*) (*else*);
4.155 +\<close> text \<open>
4.156 + LI.scan_up pcc (ist |> Istate.path_up) (go_up path sc);
4.157 +\<close> ML \<open>
4.158 +"~~~~~ fun scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _))
4.159 + = (pcc, (ist |> Istate.path_up), (go_up path sc));
4.160 +\<close> ML \<open>
4.161 + val e2 = LI.check_Seq_up ist sc
4.162 +\<close> text \<open>
4.163 + (*case*)
4.164 + LI.scan_dn cc (ist |> Istate.path_up_down [R]) e2 (*of*);
4.165 +\<close> ML \<open>
4.166 +"~~~~~ fun scan_dn , args:"; val (cc, (ist as {act_arg, ...}), (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ e))
4.167 + = (cc, (ist |> Istate.path_up_down [R]), e2 );
4.168 +\<close> text \<open>
4.169 + (*case*)
4.170 + LI.scan_dn cc (ist |> Istate.path_down [R]) e (*of*);
4.171 +\<close> ML \<open>
4.172 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t (*fall-through*))
4.173 + = (cc, (ist |> Istate.path_down [R]), e);
4.174 +\<close> ML \<open>
4.175 + (*if*) Tactical.contained_in t (*else*);
4.176 +\<close> ML \<open>
4.177 +val (Program.Tac prog_tac, form_arg) =
4.178 + (*case*) LItool.check_leaf "next " ctxt eval (Istate.get_subst ist) t (*of*);
4.179 +\<close> text \<open>
4.180 + LI.check_tac cc ist (prog_tac, form_arg);
4.181 +\<close> ML \<open>
4.182 +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
4.183 + = (cc, ist, (prog_tac, form_arg));
4.184 +\<close> ML \<open>
4.185 + val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
4.186 +\<close> ML \<open>
4.187 +val _ =
4.188 + (*case*) m (*of*);
4.189 +\<close> text \<open>
4.190 + (*case*)
4.191 +Solve_Step.check m (pt, p) (*of*);
4.192 +\<close> ML \<open>
4.193 +"~~~~~ fun check , args:"; val ((Tactic.Rewrite_Set rls), (cs as (pt, pos)) )
4.194 + = (m, (pt, p));
4.195 +\<close> ML \<open>
4.196 + val ctxt = Ctree.get_loc pt pos |> snd
4.197 + val thy' = ctxt |> Proof_Context.theory_of |> Context.theory_name
4.198 + val f = Calc.current_formula cs;
4.199 +\<close> text \<open>
4.200 + (*case*)
4.201 + Rewrite.rewrite_set_ ctxt false (get_rls ctxt rls) f (*of*);
4.202 +\<close> ML \<open>
4.203 +"~~~~~ fun rewrite_set_ , args:"; val (ctxt, bool, rls, term)
4.204 + = (ctxt, false, (get_rls ctxt rls), f);
4.205 +\<close> text \<open>
4.206 + Rewrite.rewrite__set_ ctxt 1 bool [] rls term
4.207 +\<close> ML \<open>
4.208 +"~~~~~ and rewrite__set_ , args:"; val ((*3*)ctxt, i, put_asm, bdv, rls, ct)
4.209 + = (ctxt, 1, bool, [], rls, term);
4.210 +\<close> ML \<open>
4.211 +val rewrite_trace_depth = Attrib.setup_config_int \<^binding>\<open>rewrite_trace_depth\<close> (K 99999);
4.212 +
4.213 +fun trace1 ctxt i str =
4.214 + if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth
4.215 + then tracing (idt "#" (i + 1) ^ str) else ()
4.216 +fun trace_in1 ctxt i str thmid =
4.217 + trace1 ctxt i (" " ^ str ^ ": \"" ^ thmid ^ "\"")
4.218 +fun trace_in2 ctxt i str t =
4.219 + trace1 ctxt i (" " ^ str ^ ": \"" ^ UnparseC.term_in_ctxt ctxt t ^ "\"");
4.220 +fun trace_in3 ctxt i str pairopt =
4.221 + trace1 ctxt i (" " ^ str ^ ": " ^ UnparseC.term_in_ctxt ctxt ((fst o the) pairopt));
4.222 +fun msg call ctxt op_ thmC t =
4.223 + call ^ ": \n" ^
4.224 + "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm_PIDE ctxt thmC) ^ ")\n" ^
4.225 + "but rewrite__ on " ^ quote (UnparseC.term_in_ctxt ctxt t) ^ " \<longrightarrow> NONE";
4.226 +
4.227 + datatype switch = Appl | Noap;
4.228 + fun rew_once (*1*)_ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
4.229 + | rew_once (*2*)ruls asm ct Appl [] =
4.230 + (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
4.231 + | Rule_Set.Sequence _ => (ct, asm)
4.232 + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
4.233 + | rew_once (*3*)ruls asm ct apno (rul :: thms) =
4.234 + case rul of
4.235 + Rule.Thm (thmid, thm) =>
4.236 + (trace_in1 ctxt i "try thm" thmid;
4.237 + case Rewrite.rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.238 + ((#asm_rls o Rule_Set.rep) rls) put_asm thm ct of
4.239 + NONE => rew_once ruls asm ct apno thms
4.240 + | SOME (ct', asm') =>
4.241 + (trace_in2 ctxt i "rewrites to" ct';
4.242 + rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
4.243 + (* once again try the same rule, e.g. associativity against "()"*)
4.244 + | Rule.Eval (cc as (op_, _)) =>
4.245 + let val _ = trace_in1 ctxt i "try calc" op_;
4.246 + in case Eval.adhoc_thm ctxt cc ct of
4.247 + NONE => rew_once ruls asm ct apno thms
4.248 + | SOME (_, thm') =>
4.249 + let
4.250 + val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.251 + ((#asm_rls o Rule_Set.rep) rls) put_asm thm' ct;
4.252 + val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" ctxt op_ thm' ct)
4.253 + val _ = trace_in3 ctxt i "calc. to" pairopt;
4.254 + in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
4.255 + end
4.256 + | Rule.Cal1 (cc as (op_, _)) =>
4.257 + let val _ = trace_in1 ctxt i "try cal1" op_;
4.258 + in case Eval.adhoc_thm1_ ctxt cc ct of
4.259 + NONE => (ct, asm)
4.260 + | SOME (_, thm') =>
4.261 + let
4.262 + val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.263 + ((#asm_rls o Rule_Set.rep) rls) put_asm thm' ct;
4.264 + val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
4.265 + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_ctxt ctxt ct ^ " = NONE")
4.266 + val _ = trace_in3 ctxt i "cal1. to" pairopt;
4.267 + in the pairopt end
4.268 + end
4.269 + | Rule.Rls_ rls' =>
4.270 + (case rewrite__set_ ctxt (i + 1) put_asm bdv rls' ct of
4.271 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
4.272 + | NONE => rew_once ruls asm ct apno thms)
4.273 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
4.274 +
4.275 +\<close> ML \<open>
4.276 + val ruls = (#rules o Rule_Set.rep) rls;
4.277 +\<close> ML \<open>
4.278 + val _ = trace_eq1 ctxt i "rls" rls ct
4.279 +\<close> text \<open>
4.280 + val (ct', asm') =
4.281 + rew_once ruls [] ct Noap ruls;
4.282 +\<close> ML \<open>
4.283 +"~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms))
4.284 + = (ruls, [], ct, Noap, ruls);
4.285 +\<close> ML \<open>
4.286 +val Rule.Thm (thmid, thm) =
4.287 + (*case*) rul (*of*);
4.288 +\<close> ML \<open>
4.289 +val NONE =
4.290 + (*case*) rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.291 + ((#asm_rls o Rule_Set.rep) rls) put_asm thm ct (*of*);
4.292 +\<close> text \<open>
4.293 + rew_once ruls asm ct apno thms;
4.294 +\<close> ML \<open>
4.295 +"~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms))
4.296 + = (ruls, asm, ct, apno, thms);
4.297 +\<close> ML \<open>
4.298 +(*+*) val Rule.Thm (thmid, thm)= nth 5 thms; (*fst thm rewriting to SOME*)
4.299 +\<close> text \<open>
4.300 + (*case*)
4.301 + rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
4.302 + ((#asm_rls o Rule_Set.rep) rls) put_asm thm ct (*of*);
4.303 +\<close> ML \<open>
4.304 +"~~~~~ fun rewrite__ , args:"; val (ctxt, i, bdv, tless, rls, put_asm, thm, ct)
4.305 + = (ctxt, (i + 1), bdv:Subst.T, ((snd o #rew_ord o Rule_Set.rep) rls),
4.306 + ((#asm_rls o Rule_Set.rep) rls), put_asm, thm, ct);
4.307 +\<close> ML \<open>
4.308 +(* ------------------------------------------^^^.., id = "tval_rls" (*o*)
4.309 +rls =
4.310 + Repeat
4.311 + {asm_rls =
4.312 + Repeat
4.313 + {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 =
4.314 + "testerls", preconds = [], prog_rls = Empty, program = Empty_Prog, rew_ord = ("termlessI", fn), rules =
4.315 + [Thm ("refl", "?t = ?t"), Thm ("order_refl", "?x \<le> ?x"), Thm ("radd_left_cancel_le", "(?k + ?m \<le> ?k + ?n) = (?m \<le> ?n)"), Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"),
4.316 + Thm ("and_true", "(?a \<and> True) = ?a"), Thm ("and_false", "(?a \<and> False) = False"), Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a"),
4.317 + Thm ("and_commute", "(?a \<and> ?b) = (?b \<and> ?a)"), Thm ("or_commute", "(?a \<or> ?b) = (?b \<or> ?a)"), Eval ("Prog_Expr.is_num", fn), Eval ("Prog_Expr.matches", fn), Eval ("Groups.plus_class.plus", fn),
4.318 + 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)]},
4.319 + calc = [], errpatts = [], id = "tval_rls", preconds = [], prog_rls =
4.320 + 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 =
4.321 + ("sqrt_right", fn), rules =
4.322 + [Thm ("refl", "?t = ?t"), Thm ("order_refl", "?x \<le> ?x"), Thm ("radd_left_cancel_le", "(?k + ?m \<le> ?k + ?n) = (?m \<le> ?n)"), Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True"),
4.323 + Thm ("and_true", "(?a \<and> True) = ?a"), Thm ("and_false", "(?a \<and> False) = False"), Thm ("or_true", "(?a \<or> True) = True"), Thm ("or_false", "(?a \<or> False) = ?a"), Thm ("and_commute", "(?a \<and> ?b) = (?b \<and> ?a)"),
4.324 + Thm ("or_commute", "(?a \<or> ?b) = (?b \<or> ?a)"), Thm ("real_diff_minus", "?a - ?b = ?a + - 1 * ?b"), Thm ("root_ge0", "0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True"),
4.325 + Thm ("root_add_ge0", "0 \<le> ?a \<Longrightarrow> 0 \<le> ?b \<Longrightarrow> (0 \<le> sqrt ?a + sqrt ?b) = True"), Thm ("root_ge0_1", "0 \<le> ?a \<Longrightarrow> 0 \<le> ?b \<Longrightarrow> 0 \<le> ?c \<Longrightarrow> (0 \<le> ?a * sqrt ?b + sqrt ?c) = True"),
4.326 + Thm ("root_ge0_2", "0 \<le> ?a \<Longrightarrow> 0 \<le> ?b \<Longrightarrow> 0 \<le> ?c \<Longrightarrow> (0 \<le> sqrt ?a + ?b * sqrt ?c) = True"), Eval ("Prog_Expr.is_num", fn), Eval ("Test.contains_root", fn), Eval ("Prog_Expr.matches", fn),
4.327 + 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),
4.328 + Eval ("Orderings.ord_class.less", fn), Eval ("Orderings.ord_class.less_eq", fn), Eval ("Prog_Expr.ident", fn)]}
4.329 +*)
4.330 +\<close> ML \<open>
4.331 +\<close> text \<open>
4.332 + val (t', asms, _(*lrd*), rew) =
4.333 + Rewrite.rew_sub ctxt i bdv tless rls put_asm ([]: TermC.path)
4.334 + (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct
4.335 +\<close> ML \<open>
4.336 +"~~~~~ and rew_sub , args:"; val (ctxt, i, bdv, tless, rls, put_asm, lrd, r, t)
4.337 + = (ctxt, i, bdv, tless, rls, put_asm, ([]: TermC.path),
4.338 + (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct);
4.339 +\<close> ML \<open>
4.340 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
4.341 +\<close> ML \<open>
4.342 +(* inhibit exn NO_REWRITE
4.343 + val r' = (Envir.subst_term (Pattern.match (Proof_Context.theory_of ctxt)
4.344 + (lhs, t) (Vartab.empty, Vartab.empty)) r)
4.345 + handle Pattern.MATCH => raise NO_REWRITE
4.346 +*)
4.347 +(*+*) UnparseC.term_in_ctxt ctxt t = "x + 1 + - 1 * 2 = 0";
4.348 +\<close> ML \<open>
4.349 +val t1 $ t2 =
4.350 + (*case*) t (*of*);
4.351 +\<close> ML \<open>
4.352 +val (t2', asm2, lrd, rew2) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
4.353 +\<close> ML \<open>
4.354 + (*if*) rew2 (*else*);
4.355 +\<close> text \<open>
4.356 +val (t1', asm1, lrd, rew1) =
4.357 + rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
4.358 +\<close> ML \<open>
4.359 +"~~~~~ fun rew_sub , args:"; val (ctxt, i, bdv, tless, rls, put_asm, lrd, r, t)
4.360 + = (ctxt, i, bdv, tless, rls, put_asm, (lrd @ [TermC.L]), r, t1);
4.361 +\<close> ML \<open>
4.362 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
4.363 +\<close> ML \<open>
4.364 +(* inhibit exn NO_REWRITE
4.365 + val r' = (Envir.subst_term (Pattern.match (Proof_Context.theory_of ctxt)
4.366 + (lhs, t) (Vartab.empty, Vartab.empty)) r)
4.367 + handle Pattern.MATCH => raise NO_REWRITE
4.368 +*)
4.369 +(*+*) UnparseC.term_in_ctxt ctxt t = "(=) (x + 1 + - 1 * 2)";
4.370 +\<close> ML \<open>
4.371 +val t1 $ t2 =
4.372 + (*case*) t (*of*);
4.373 +\<close> text \<open>
4.374 +val (t2', asm2, lrd, rew2) =
4.375 + rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
4.376 +\<close> ML \<open>
4.377 +"~~~~~ fun rew_sub , args:"; val (ctxt, i, bdv, tless, rls, put_asm, lrd, r, t)
4.378 + = (ctxt, i, bdv, tless, rls, put_asm, (lrd @ [TermC.R]), r, t2);
4.379 +\<close> ML \<open>
4.380 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
4.381 +\<close> ML \<open>
4.382 + val r' = (Envir.subst_term (Pattern.match (Proof_Context.theory_of ctxt)
4.383 + (lhs, t) (Vartab.empty, Vartab.empty)) r)
4.384 + handle Pattern.MATCH => raise NO_REWRITE
4.385 +\<close> ML \<open>
4.386 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
4.387 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
4.388 +\<close> ML \<open>
4.389 +(*+*) UnparseC.term_in_ctxt ctxt t' = "- 1 * 2 + (x + 1)";
4.390 +\<close> ML \<open>
4.391 + val (simpl_p', nofalse) = eval__true ctxt (i + 1) p' bdv rls
4.392 +\<close> ML \<open>
4.393 + (*if*) nofalse (*then*);
4.394 +\<close> ML \<open>
4.395 + val (t'', p'') = (t', simpl_p')
4.396 +\<close> text \<open>
4.397 + (*if*) TermC.perm lhs rhs andalso not (tless bdv (t', t));
4.398 +\<close> text \<open>
4.399 + (tless bdv (t', t))
4.400 +\<close> ML \<open>
4.401 +(*+*)tless; (*vvv--- found (*o*) tval_rls*)
4.402 +(*+*) val sqrt_right = tval_rls |> (snd o #rew_ord o Rule_Set.rep);
4.403 +\<close> ML \<open>
4.404 +"~~~~~ fun sqrt_right , args:"; val ((pr:bool), thy, (_: subst), (ts, us))
4.405 + = (false, @{theory}(*?!*), bdv, (t', t));
4.406 +\<close> text \<open> -- hidden by "local" -- delete
4.407 + (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );
4.408 +\<close> ML \<open>
4.409 +\<close> ML \<open>
4.410 +\<close> ML \<open>
4.411 +\<close> ML \<open>
4.412 +\<close> ML \<open>
4.413 +\<close> ML \<open>
4.414 +\<close> ML \<open>
4.415 +\<close> ML \<open>
4.416 +\<close> ML \<open>
4.417 +\<close> ML \<open>
4.418 +\<close> ML \<open>
4.419 +\<close> ML \<open>
4.420 +\<close> ML \<open>
4.421 +(*keep for continuing Rewrite_Set*)
4.422 +\<close> ML \<open> (*------------- continuing Rewrite_Set ------------------------------------------------*)
4.423 +(*-------------------- continuing Rewrite_Set ------------------------------------------------*)
4.424 +(*kept for continuing XXXXX*)
4.425 +(*-------------------- stop step into Rewrite_Set --------------------------------------------*)
4.426 +\<close> ML \<open> (*------------- stop step into Rewrite_Set --------------------------------------------*)
4.427 +(*\\------------------ step into Rewrite_Set -----------------------------------------------//*)
4.428 +\<close> ML \<open> (*\\----------- step into Rewrite_Set -----------------------------------------------//*)
4.429
4.430 \<close> text \<open>
4.431 (*/--------- investigate Rewrite_Set "Test_simplify" -----------------------------------------\*)
5.1 --- a/src/Tools/isac/Interpret/derive.sml Thu Nov 10 14:25:38 2022 +0100
5.2 +++ b/src/Tools/isac/Interpret/derive.sml Wed Nov 16 10:29:52 2022 +0100
5.3 @@ -53,11 +53,11 @@
5.4 fun msg_2 ctxt thmid =
5.5 if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
5.6 fun msg_3 ctxt t' =
5.7 - if Config.get ctxt rewrite_trace then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
5.8 + if Config.get ctxt rewrite_trace then tracing ("=== rewrites to: " ^ UnparseC.term_in_ctxt ctxt t') else ();
5.9 fun msg_4 ctxt op_ =
5.10 if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying calc. \"" ^ op_^"\"");
5.11 fun msg_5 ctxt t' =
5.12 - if not (Config.get ctxt rewrite_trace) then () else tracing("=== calc. to: " ^ UnparseC.term t')
5.13 + if not (Config.get ctxt rewrite_trace) then () else tracing("=== calc. to: " ^ UnparseC.term_in_ctxt ctxt t')
5.14
5.15
5.16 fun do_one ctxt asm_rls rs ro goal tt =
5.17 @@ -65,7 +65,7 @@
5.18 datatype switch = Appl | Noap (* TODO: unify with version in Rewrite *)
5.19 fun rew_once _ rts t Noap [] =
5.20 (case goal of NONE => rts | SOME _ =>
5.21 - raise ERROR ("Derive.do_one: no derivation for " ^ UnparseC.term t))
5.22 + raise ERROR ("Derive.do_one: no derivation for " ^ UnparseC.term_in_ctxt ctxt t))
5.23 | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs
5.24 | rew_once lim rts t apno rs' =
5.25 (case goal of
6.1 --- a/src/Tools/isac/Interpret/li-tool.sml Thu Nov 10 14:25:38 2022 +0100
6.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Nov 16 10:29:52 2022 +0100
6.3 @@ -85,7 +85,7 @@
6.4 in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end
6.5 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>, _) $ op_ $ _) =
6.6 (Tactic.Calculate (HOLogic.dest_string op_))
6.7 - | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ t) = (Tactic.Take (UnparseC.term t))
6.8 + | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ t) = (Tactic.Take (UnparseC.term_in_thy thy t))
6.9 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ isasub $ _) =
6.10 Tactic.Substitute (Prog_Tac.Substitute_adapt_to_type thy isasub)
6.11 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Check_elementwise\<close>, _) $ _ $
6.12 @@ -338,11 +338,13 @@
6.13
6.14 fun trace_msg_1 ctxt call t stac =
6.15 if Config.get ctxt LI_trace then
6.16 - tracing ("@@@ " ^ call ^ " leaf \"" ^ UnparseC.term t ^ "\" \<longrightarrow> Tac \"" ^ UnparseC.term stac ^ "\"")
6.17 + tracing ("@@@ " ^ call ^ " leaf \"" ^ UnparseC.term_in_ctxt ctxt t ^ "\" \<longrightarrow> Tac \"" ^
6.18 + UnparseC.term_in_ctxt ctxt stac ^ "\"")
6.19 else ();
6.20 fun trace_msg_2 ctxt call t lexpr' =
6.21 if Config.get ctxt LI_trace then
6.22 - tracing("@@@ " ^ call ^ " leaf '" ^ UnparseC.term t ^ "' \<longrightarrow> Expr \"" ^ UnparseC.term lexpr' ^ "\"")
6.23 + tracing("@@@ " ^ call ^ " leaf '" ^ UnparseC.term_in_ctxt ctxt t ^ "' \<longrightarrow> Expr \"" ^
6.24 + UnparseC.term_in_ctxt ctxt lexpr' ^ "\"")
6.25 else ();
6.26 (*
6.27 check a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr.
7.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Nov 10 14:25:38 2022 +0100
7.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Nov 16 10:29:52 2022 +0100
7.3 @@ -255,7 +255,8 @@
7.4
7.5 | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.If\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
7.6
7.7 - | scan_up _ _ t = raise ERROR ("scan_up not impl for " ^ UnparseC.term t)
7.8 + | scan_up (pcc as (_, (_, ctxt))) _ t = raise ERROR ("scan_up not impl for " ^
7.9 + UnparseC.term_in_ctxt ctxt t)
7.10
7.11 (* scan program until an applicable tactic is found *)
7.12 fun scan_to_tactic (prog, cc) (Pstate (ist as {path, ...})) =
7.13 @@ -471,7 +472,8 @@
7.14
7.15 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.If\<close>,_) $ _ $ _ $ _) = go_scan_up1 pcct ist
7.16
7.17 - | scan_up1 _ _ t = raise ERROR ("scan_up1 not impl for t= " ^ UnparseC.term t)
7.18 + | scan_up1 (_, (_, ctxt, _)) _ t =
7.19 + raise ERROR ("scan_up1 not impl for t= " ^ UnparseC.term_in_ctxt ctxt t)
7.20
7.21 fun scan_to_tactic1 (prog, (cctt as ((_, p), _, _))) (Pstate (ist as {path, ...})) =
7.22 if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH find_next_step IN solve*)p
8.1 --- a/src/Tools/isac/Interpret/solve-step.sml Thu Nov 10 14:25:38 2022 +0100
8.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Wed Nov 16 10:29:52 2022 +0100
8.3 @@ -21,7 +21,6 @@
8.4 val get_eval: string -> Pos.pos' -> Ctree.ctree -> string * ThyC.id * Eval.ml
8.5
8.6 \<^isac_test>\<open>
8.7 - val get_ctxt: Ctree.ctree -> Pos.pos' -> Proof.context
8.8 val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Eval.ml_from_prog list
8.9 \<close>
8.10 end
8.11 @@ -239,10 +238,12 @@
8.12 end
8.13 | check (Tactic.Tac id) (cs as (pt, pos)) =
8.14 let
8.15 - val thy = (Ctree.get_loc pt pos |> snd) |> Proof_Context.theory_of
8.16 + val ctxt = Ctree.get_ctxt pt pos
8.17 + val thy = ctxt |> Proof_Context.theory_of
8.18 val f = Calc.current_formula cs;
8.19 + val f' = UnparseC.term_in_ctxt ctxt f
8.20 in
8.21 - Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
8.22 + Applicable.Yes (Tactic.Tac_ (thy, f', id, f'))
8.23 end
8.24 | check (Tactic.Take str) (pt, pos) =
8.25 let
8.26 @@ -267,16 +268,16 @@
8.27 let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t
8.28 in (pos, c, Test_Out.EmptyMout, pt) end
8.29 | NONE => (pos, [], Test_Out.EmptyMout, pt))
8.30 - | add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
8.31 + | add (Tactic.Take' t) (l as (_, ctxt)) (pt, (p, _)) = (* val (Take' t) = m; *)
8.32 let
8.33 val p =
8.34 let val (ps, p') = split_last p (* no connex to prev.ppobj *)
8.35 in if p' = 0 then ps @ [1] else p end
8.36 val (pt, c) = Ctree.cappend_form pt p l t
8.37 in
8.38 - ((p, Pos.Frm), c, Test_Out.FormKF (UnparseC.term t), pt)
8.39 + ((p, Pos.Frm), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt t), pt)
8.40 end
8.41 - | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Frm)) =
8.42 + | add (Tactic.Begin_Trans' t) (l as (_, ctxt)) (pt, (p, Pos.Frm)) =
8.43 let
8.44 val (pt, c) = Ctree.cappend_form pt p l t
8.45 val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*)
8.46 @@ -284,17 +285,17 @@
8.47 val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
8.48 val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*)
8.49 in
8.50 - ((p, Pos.Frm), c @ c', Test_Out.FormKF (UnparseC.term t), pt)
8.51 + ((p, Pos.Frm), c @ c', Test_Out.FormKF (UnparseC.term_in_ctxt ctxt t), pt)
8.52 end
8.53 | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Res)) =
8.54 (*append after existing PrfObj vvvvvvvvvvvvv*)
8.55 add (Tactic.Begin_Trans' t) l (pt, (Pos.lev_on p, Pos.Frm))
8.56 - | add (Tactic.End_Trans' tasm) l (pt, (p, _)) =
8.57 + | add (Tactic.End_Trans' tasm) (l as (_, ctxt)) (pt, (p, _)) =
8.58 let
8.59 val p' = Pos.lev_up p
8.60 val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
8.61 in
8.62 - ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
8.63 + ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*UnparseC.term_in_ctxt ctxt t*), pt)
8.64 end
8.65 | add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
8.66 let
8.67 @@ -302,14 +303,14 @@
8.68 (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete;
8.69 val pt = Ctree.update_branch pt p Ctree.TransitiveB
8.70 in
8.71 - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
8.72 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
8.73 end
8.74 | add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
8.75 let
8.76 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete
8.77 val pt = Ctree.update_branch pt p Ctree.TransitiveB
8.78 in
8.79 - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
8.80 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
8.81 end
8.82 | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
8.83 let
8.84 @@ -317,7 +318,7 @@
8.85 (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete
8.86 val pt = Ctree.update_branch pt p Ctree.TransitiveB
8.87 in
8.88 - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
8.89 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
8.90 end
8.91 | add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
8.92 let
8.93 @@ -325,37 +326,37 @@
8.94 (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
8.95 val pt = Ctree.update_branch pt p Ctree.TransitiveB
8.96 in
8.97 - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
8.98 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
8.99 end
8.100 - | add (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) =
8.101 + | add (Tactic.Check_Postcond' (_, scval)) (l as (_, ctxt)) (pt, (p, _)) =
8.102 let
8.103 val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete
8.104 in
8.105 - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term scval), pt)
8.106 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt scval), pt)
8.107 end
8.108 - | add (Tactic.Calculate' (_, op_, f, (f', _))) l (pt, (p, _)) =
8.109 + | add (Tactic.Calculate' (_, op_, f, (f', _))) (l as (_, ctxt)) (pt, (p, _)) =
8.110 let
8.111 val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete
8.112 in
8.113 - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
8.114 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
8.115 end
8.116 - | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (pt, (p, _)) =
8.117 + | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) (l as (_, ctxt)) (pt, (p, _)) =
8.118 let
8.119 val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete
8.120 in
8.121 - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
8.122 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
8.123 end
8.124 - | add (Tactic.Or_to_List' (ors, list)) l (pt, (p, _)) =
8.125 + | add (Tactic.Or_to_List' (ors, list)) (l as (_, ctxt)) (pt, (p, _)) =
8.126 let
8.127 val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete
8.128 in
8.129 - ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term list), pt)
8.130 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt list), pt)
8.131 end
8.132 - | add (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) =
8.133 + | add (Tactic.Substitute' (_, _, subte, t, t')) (l as (_, ctxt)) (pt, (p, _)) =
8.134 let
8.135 val (pt,c) =
8.136 Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete
8.137 - in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term t'), pt)
8.138 + in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt t'), pt)
8.139 end
8.140 | add (Tactic.Tac_ (_, f, id, f')) l (pt, pos as (p, _)) =
8.141 let
9.1 --- a/src/Tools/isac/Knowledge/Root.thy Thu Nov 10 14:25:38 2022 +0100
9.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Nov 16 10:29:52 2022 +0100
9.3 @@ -104,14 +104,14 @@
9.4 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
9.5 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
9.6 | ord => ord)
9.7 - | term_ord' pr _(*thy*) (t, u) =
9.8 + | term_ord' pr thy (t, u) =
9.9 (if pr then
9.10 let
9.11 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
9.12 - val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^"\" @ \"[" ^
9.13 - commas (map UnparseC.term ts) ^ "]\"");
9.14 + val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_ctxt (Proof_Context.init_global thy) f ^"\" @ \"[" ^
9.15 + commas (map (UnparseC.term_in_ctxt (Proof_Context.init_global thy)) ts) ^ "]\"");
9.16 val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^
9.17 - commas (map UnparseC.term us) ^ "]\"");
9.18 + commas (map (UnparseC.term_in_ctxt (Proof_Context.init_global thy)) us) ^ "]\"");
9.19 val _ = tracing ("size_of_term(t,u)= (" ^
9.20 string_of_int(size_of_term' t) ^", " ^
9.21 string_of_int(size_of_term' u) ^")");
10.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Thu Nov 10 14:25:38 2022 +0100
10.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Wed Nov 16 10:29:52 2022 +0100
10.3 @@ -20,15 +20,16 @@
10.4 val rewrite_set_inst_: Proof.context -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
10.5 val rewrite_terms_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> term list
10.6 -> term -> (term * term list) option
10.7 -
10.8 -\<^isac_test>\<open>
10.9 +(*from isac_test for Minisubpbl*)
10.10 val rewrite__: Proof.context -> int -> Subst.T -> Rewrite_Ord.function ->
10.11 Rule_Set.T -> bool -> thm -> term -> (term * term list) option
10.12 val rewrite__set_: Proof.context -> int -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
10.13 + val trace_eq1 : Proof.context -> int -> string -> Rule_Def.rule_set -> term -> unit;
10.14 +
10.15 +\<^isac_test>\<open>
10.16 val app_rev: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool
10.17 val app_sub: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool
10.18 val trace1: Proof.context -> int -> string -> unit
10.19 - val trace_eq1 : Proof.context -> int -> string -> Rule_Def.rule_set -> term -> unit;
10.20 val trace_eq2 : Proof.context -> int -> string -> term -> term -> unit;
10.21 val trace_in1 : Proof.context -> int -> string -> string -> unit;
10.22 val trace_in2 : Proof.context -> int -> string -> term -> unit;
10.23 @@ -87,7 +88,7 @@
10.24 else();
10.25 fun msg call ctxt op_ thmC t =
10.26 call ^ ": \n" ^
10.27 - "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^
10.28 + "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm_PIDE ctxt thmC) ^ ")\n" ^
10.29 "but rewrite__ on " ^ quote (UnparseC.term_in_ctxt ctxt t) ^ " \<longrightarrow> NONE";
10.30
10.31 fun rewrite__ ctxt i bdv tless rls put_asm thm ct =
10.32 @@ -198,7 +199,7 @@
10.33 val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
10.34 ((#asm_rls o Rule_Set.rep) rls) put_asm thm' ct;
10.35 val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
10.36 - ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_ctxt ctxt ct ^ " = NONE")
10.37 + ThmC.string_of_thm_PIDE ctxt thm' ^ "\" " ^ UnparseC.term_in_ctxt ctxt ct ^ " = NONE")
10.38 val _ = trace_in3 ctxt i "cal1. to" pairopt;
10.39 in the pairopt end
10.40 end
10.41 @@ -261,8 +262,8 @@
10.42 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
10.43
10.44 (* rewriting without internal arguments 1, [] *)
10.45 -fun rewrite_ thy rew_ord asm_rls bool thm term = rewrite__ thy 1 [] rew_ord asm_rls bool thm term;
10.46 -fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
10.47 +fun rewrite_ ctxt rew_ord asm_rls bool thm term = rewrite__ ctxt 1 [] rew_ord asm_rls bool thm term;
10.48 +fun rewrite_set_ ctxt bool rls term = rewrite__set_ ctxt 1 bool [] rls term;
10.49
10.50 (* variants of rewrite; TODO del. put_asm *)
10.51 fun rewrite_inst_ thy rew_ord rls put_asm subst thm ct =
11.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Thu Nov 10 14:25:38 2022 +0100
11.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Wed Nov 16 10:29:52 2022 +0100
11.3 @@ -13,8 +13,14 @@
11.4
11.5 val cut_id: string -> id
11.6 val long_id: T -> long_id
11.7 +
11.8 val string_of_thm: thm -> string
11.9 val string_of_thms: thm list -> string
11.10 +(*stepwise replace ^^^ by vvv and finally rename by eliminating "_PIDE"*)
11.11 +(*val string_of:*)
11.12 + val string_of_thm_PIDE: Proof.context -> thm -> string
11.13 + val string_of_thms_PIDE: Proof.context -> thm list -> string
11.14 +
11.15 val id_of_thm: thm -> id
11.16 val of_thm: thm -> T
11.17 val from_rule : Rule.rule -> T
11.18 @@ -53,6 +59,8 @@
11.19
11.20 val string_of_thm = ThmC_Def.string_of_thm;
11.21 val string_of_thms = ThmC_Def.string_of_thms;
11.22 +val string_of_thm_PIDE = ThmC_Def.string_of_thm_PIDE;
11.23 +val string_of_thms_PIDE = ThmC_Def.string_of_thms_PIDE;
11.24
11.25 fun id_of_thm thm = thm |> Thm.get_name_hint |> cut_id;
11.26 fun of_thm thm = (id_of_thm thm, thm);
12.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Nov 10 14:25:38 2022 +0100
12.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Nov 16 10:29:52 2022 +0100
12.3 @@ -117,7 +117,7 @@
12.4 Step_Specify.nxt_specify_init_calc ctxt (fmz, sp);
12.5 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
12.6 (*val (_, hdl, (dI, pI, mI), pors, pctxt) =*)
12.7 - initialise ctxt (fmz, (dI, pI, mI));
12.8 +Step_Specify.initialise ctxt (fmz, (dI, pI, mI));
12.9 "~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, (dI, pI, mI));
12.10 val thy = ThyC.get_theory dI
12.11 val ctxt = Proof_Context.init_global thy;
13.1 --- a/test/Tools/isac/Test_Isac.thy Thu Nov 10 14:25:38 2022 +0100
13.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Nov 16 10:29:52 2022 +0100
13.3 @@ -235,7 +235,7 @@
13.4 ML_file "Minisubpbl/000-comments.sml"
13.5 ML_file "Minisubpbl/100-init-rootpbl.sml"
13.6 ML_file "Minisubpbl/150a-add-given-Maximum.sml"
13.7 - ML_file "Minisubpbl/150b-add-given-Equation.sml"
13.8 + ML_file "Minisubpbl/150-add-given-Equation.sml"
13.9 ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"
13.10 ML_file "Minisubpbl/200-start-method.sml"
13.11 ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
14.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Nov 10 14:25:38 2022 +0100
14.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Nov 16 10:29:52 2022 +0100
14.3 @@ -204,7 +204,7 @@
14.4 ML_file "BaseDefinitions/libraryC.sml"
14.5 ML_file "BaseDefinitions/rule-def.sml"
14.6 ML_file "BaseDefinitions/eval-def.sml"
14.7 - ML_file "BaseDefinitions/rewrite-order.sml"
14.8 + ML_file "BaseDefinitions/rewrite-order.sml"
14.9 ML_file "BaseDefinitions/theoryC.sml"
14.10 ML_file "BaseDefinitions/rule.sml"
14.11 ML_file "BaseDefinitions/thmC-def.sml"