equal
deleted
inserted
replaced
43 solvers: solver list * solver list} |
43 solvers: solver list * solver list} |
44 val print_ss: simpset -> unit |
44 val print_ss: simpset -> unit |
45 val empty_ss: simpset |
45 val empty_ss: simpset |
46 val merge_ss: simpset * simpset -> simpset |
46 val merge_ss: simpset * simpset -> simpset |
47 type simproc |
47 type simproc |
48 val mk_simproc: string -> cterm list -> |
48 val mk_simproc': string -> cterm list -> (simpset -> cterm -> thm option) -> simproc |
49 (theory -> simpset -> term -> thm option) -> simproc |
49 val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc |
50 val add_prems: thm list -> simpset -> simpset |
50 val add_prems: thm list -> simpset -> simpset |
51 val prems_of_ss: simpset -> thm list |
51 val prems_of_ss: simpset -> thm list |
52 val addsimps: simpset * thm list -> simpset |
52 val addsimps: simpset * thm list -> simpset |
53 val delsimps: simpset * thm list -> simpset |
53 val delsimps: simpset * thm list -> simpset |
54 val addeqcongs: simpset * thm list -> simpset |
54 val addeqcongs: simpset * thm list -> simpset |
196 solvers: solver list * solver list} |
196 solvers: solver list * solver list} |
197 and proc = |
197 and proc = |
198 Proc of |
198 Proc of |
199 {name: string, |
199 {name: string, |
200 lhs: cterm, |
200 lhs: cterm, |
201 proc: theory -> simpset -> term -> thm option, |
201 proc: simpset -> cterm -> thm option, |
202 id: stamp} |
202 id: stamp} |
203 and solver = |
203 and solver = |
204 Solver of |
204 Solver of |
205 {name: string, |
205 {name: string, |
206 solver: simpset -> int -> tactic, |
206 solver: simpset -> int -> tactic, |
334 Pretty.strs ("safe solvers:" :: map (quote o solver_name) (#2 solvers))] |
334 Pretty.strs ("safe solvers:" :: map (quote o solver_name) (#2 solvers))] |
335 |> Pretty.chunks |> Pretty.writeln |
335 |> Pretty.chunks |> Pretty.writeln |
336 end; |
336 end; |
337 |
337 |
338 |
338 |
339 (* simprocs *) |
|
340 |
|
341 exception SIMPROC_FAIL of string * exn; |
|
342 |
|
343 datatype simproc = Simproc of proc list; |
|
344 |
|
345 fun mk_simproc name lhss proc = |
|
346 let val id = stamp () in |
|
347 Simproc (lhss |> map (fn lhs => |
|
348 Proc {name = name, lhs = lhs, proc = proc, id = id})) |
|
349 end; |
|
350 |
|
351 (* FIXME avoid global thy and Logic.varify *) |
|
352 fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify); |
|
353 fun simproc thy name = simproc_i thy name o map (Sign.read_term thy); |
|
354 |
|
355 |
|
356 |
339 |
357 (** simpset operations **) |
340 (** simpset operations **) |
358 |
341 |
359 (* context *) |
342 (* context *) |
360 |
343 |
375 fun context ctxt = |
358 fun context ctxt = |
376 map_simpset1 (fn (rules, prems, bounds, _) => (rules, prems, bounds, SOME ctxt)); |
359 map_simpset1 (fn (rules, prems, bounds, _) => (rules, prems, bounds, SOME ctxt)); |
377 |
360 |
378 val theory_context = context o ProofContext.init; |
361 val theory_context = context o ProofContext.init; |
379 |
362 |
380 fun fallback_context _ (ss as Simpset ({context = SOME _, ...}, _)) = ss |
363 fun activate_context thy (ss as Simpset ({context = SOME ctxt, ...}, _)) = |
381 | fallback_context thy ss = |
364 context (Context.transfer_proof (Theory.merge (thy, ProofContext.theory_of ctxt)) ctxt) ss |
|
365 | activate_context thy ss = |
382 (warning "Simplifier: no proof context in simpset -- fallback to theory context!"; |
366 (warning "Simplifier: no proof context in simpset -- fallback to theory context!"; |
383 theory_context thy ss); |
367 theory_context thy ss); |
384 |
368 |
385 |
369 |
386 (* maintain simp rules *) |
370 (* maintain simp rules *) |
614 |
598 |
615 end; |
599 end; |
616 |
600 |
617 |
601 |
618 (* simprocs *) |
602 (* simprocs *) |
|
603 |
|
604 exception SIMPROC_FAIL of string * exn; |
|
605 |
|
606 datatype simproc = Simproc of proc list; |
|
607 |
|
608 fun mk_simproc' name lhss proc = |
|
609 let val id = stamp () |
|
610 in Simproc (lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = proc, id = id})) end; |
|
611 |
|
612 fun mk_simproc name lhss proc = |
|
613 mk_simproc' name lhss (fn ss => fn ct => |
|
614 proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct)); |
|
615 |
|
616 (* FIXME avoid global thy and Logic.varify *) |
|
617 fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify); |
|
618 fun simproc thy name = simproc_i thy name o map (Sign.read_term thy); |
|
619 |
619 |
620 |
620 local |
621 local |
621 |
622 |
622 fun add_proc (proc as Proc {name, lhs, ...}) ss = |
623 fun add_proc (proc as Proc {name, lhs, ...}) ss = |
623 (trace_cterm false ("Adding simplification procedure " ^ quote name ^ " for") ss lhs; |
624 (trace_cterm false ("Adding simplification procedure " ^ quote name ^ " for") ss lhs; |
913 fun proc_rews [] = NONE |
914 fun proc_rews [] = NONE |
914 | proc_rews (Proc {name, proc, lhs, ...} :: ps) = |
915 | proc_rews (Proc {name, proc, lhs, ...} :: ps) = |
915 if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then |
916 if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then |
916 (debug_term false ("Trying procedure " ^ quote name ^ " on:") ss thyt eta_t; |
917 (debug_term false ("Trying procedure " ^ quote name ^ " on:") ss thyt eta_t; |
917 case transform_failure (curry SIMPROC_FAIL name) |
918 case transform_failure (curry SIMPROC_FAIL name) |
918 (fn () => proc thyt ss eta_t) () of |
919 (fn () => proc ss eta_t') () of |
919 NONE => (debug false "FAILED"; proc_rews ps) |
920 NONE => (debug false "FAILED"; proc_rews ps) |
920 | SOME raw_thm => |
921 | SOME raw_thm => |
921 (trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") ss raw_thm; |
922 (trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") ss raw_thm; |
922 (case rews (mk_procrule ss raw_thm) of |
923 (case rews (mk_procrule ss raw_thm) of |
923 NONE => (trace_cterm true ("IGNORED result of simproc " ^ quote name ^ |
924 NONE => (trace_cterm true ("IGNORED result of simproc " ^ quote name ^ |
1190 |
1191 |
1191 fun rewrite_cterm mode prover raw_ss raw_ct = |
1192 fun rewrite_cterm mode prover raw_ss raw_ct = |
1192 let |
1193 let |
1193 val ct = Thm.adjust_maxidx_cterm ~1 raw_ct; |
1194 val ct = Thm.adjust_maxidx_cterm ~1 raw_ct; |
1194 val {thy, t, maxidx, ...} = Thm.rep_cterm ct; |
1195 val {thy, t, maxidx, ...} = Thm.rep_cterm ct; |
1195 val ss = fallback_context thy raw_ss; |
1196 val ss = activate_context thy raw_ss; |
1196 val _ = inc simp_depth; |
1197 val _ = inc simp_depth; |
1197 val _ = |
1198 val _ = |
1198 if ! simp_depth mod 20 = 0 then |
1199 if ! simp_depth mod 20 = 0 then |
1199 warning ("Simplification depth " ^ string_of_int (! simp_depth)) |
1200 warning ("Simplification depth " ^ string_of_int (! simp_depth)) |
1200 else (); |
1201 else (); |