neuper@37906: (* isac's rewriter neuper@37906: (c) Walther Neuper 2000 neuper@37906: *) neuper@37906: wneuper@59380: signature REWRITE = wneuper@59380: sig wneuper@59405: val assoc_thm': theory -> Celem.thm' -> thm wneuper@59405: val assoc_thm'': theory -> Celem.thmID -> thm wneuper@59416: val calculate_: theory -> string * Rule.eval_fn -> term -> (term * (string * thm)) option wneuper@59416: val eval__true: theory -> int -> term list -> (term * term) list -> Rule.rls -> term list * bool wneuper@59416: val eval_listexpr_: theory -> Rule.rls -> term -> term wneuper@59416: val eval_true: theory -> term list -> Rule.rls -> bool wneuper@59416: val eval_true_: Rule.theory' -> Rule.rls -> term -> bool wneuper@59405: val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) wneuper@59416: -> Rule.rls -> bool -> Celem.lrd list -> term -> term -> term * term list * Celem.lrd list * bool wneuper@59416: val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule.rls -> bool -> thm -> wneuper@59405: term -> (term * term list) option wneuper@59416: val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule.rls -> bool wneuper@59405: -> (term * term) list -> thm -> term -> (term * term list) option wneuper@59416: val rewrite_set_: theory -> bool -> Rule.rls -> term -> (term * term list) option wneuper@59416: val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule.rls -> term -> (term * term list) option wneuper@59416: val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule.rls -> term list wneuper@59405: -> term -> (term * term list) option wneuper@59380: (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) wneuper@59380: (* NONE *) wneuper@59380: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) wneuper@59409: val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) -> wneuper@59416: Rule.rls -> bool -> thm -> term -> (term * term list) option wneuper@59416: val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule.rls -> term -> (term * term list) option wneuper@59416: val app_rev: theory -> int -> Rule.rls -> term -> term * term list * bool wneuper@59416: val app_sub: theory -> int -> Rule.rls -> term -> term * term list * bool wneuper@59380: val mk_thm: theory -> string -> thm wneuper@59398: val trace1: int -> string -> unit wneuper@59380: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) wneuper@59380: end wneuper@59380: wneuper@59380: (**) wneuper@59380: structure Rewrite(**): REWRITE(**) = wneuper@59380: struct wneuper@59380: (**) neuper@37906: neuper@37906: exception NO_REWRITE; neuper@37906: exception STOP_REW_SUB; (*WN050820 quick and dirty*) neuper@37906: neuper@52101: fun trace i str = wneuper@59405: if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" i ^ str) else () neuper@52101: fun trace1 i str = wneuper@59405: if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" (i + 1) ^ str) else () neuper@52101: neuper@37906: fun rewrite__ thy i bdv tless rls put_asm thm ct = wneuper@59381: let wneuper@59405: val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: Celem.lrd list) wneuper@59389: (((TermC.inst_bdv bdv) o Calc.norm o #prop o Thm.rep_thm) thm) ct wneuper@59381: in if rew then SOME (t', distinct asms) else NONE end wneuper@59383: (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *) wneuper@59381: and rew_sub thy i bdv tless rls put_asm lrd r t = neuper@38022: (let wneuper@59381: val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r wneuper@59381: (*?alternative Unify.matchers: wneuper@59381: http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML*) wneuper@59381: val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r wneuper@59381: val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r')) wneuper@59381: val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r' wneuper@59405: val _ = if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> [] wneuper@59416: then tracing (idt "#" (i + 1) ^ " eval asms: " ^ Rule.t2str thy r') else () wneuper@59381: val (t'', p'') = (*conditional rewriting*) wneuper@59381: let wneuper@59381: val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls wneuper@59381: in wneuper@59381: if nofalse wneuper@59381: then wneuper@59405: (if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> [] wneuper@59416: then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ Rule.ts2str thy p' ^ wneuper@59416: " stored: " ^ Rule.ts2str thy simpl_p') wneuper@59381: else(); wneuper@59381: (t',simpl_p')) (* uncond.rew. from above*) wneuper@59381: else wneuper@59405: (if ! Celem.trace_rewrite andalso i < ! Celem.depth wneuper@59416: then tracing (idt "#" (i + 1) ^ " asms false: " ^ Rule.ts2str thy p') wneuper@59381: else(); wneuper@59381: raise STOP_REW_SUB (* don't go into subterms of cond *)) wneuper@59381: end wneuper@59381: in wneuper@59389: if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*) wneuper@59405: then (if ! Celem.trace_rewrite andalso i < ! Celem.depth wneuper@59416: then tracing (idt"#"i ^ " not: \"" ^ Rule.t2str thy t ^ "\" > \"" ^ Rule.t2str thy t' ^ "\"") wneuper@59381: else (); wneuper@59381: raise NO_REWRITE) wneuper@59381: else (t'', p'', [], true) wneuper@59381: end wneuper@59383: ) handle _ (*TODO Pattern.MATCH when tests are ready: ERROR 364ce4699452 *) => wneuper@59381: (case t of wneuper@59381: Const(s,T) => (Const(s,T),[],lrd,false) neuper@37906: | Free(s,T) => (Free(s,T),[],lrd,false) neuper@37906: | Var(n,T) => (Var(n,T),[],lrd,false) neuper@37906: | Bound i => (Bound i,[],lrd,false) neuper@37906: | Abs(s,T,body) => wneuper@59405: let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [Celem.D]) r body wneuper@59381: in (Abs(s, T, t'), asms, [], rew) end neuper@37906: | t1 $ t2 => wneuper@59405: let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [Celem.R]) r t2 wneuper@59381: in wneuper@59381: if rew2 then (t1 $ t2', asm2, lrd, true) wneuper@59381: else wneuper@59405: let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [Celem.L]) r t1 wneuper@59381: in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end wneuper@59381: end) wneuper@59381: and eval__true thy i asms bdv rls = (* simplify asumptions until one evaluates to false *) neuper@48760: if asms = [@{term True}] orelse asms = [] then ([], true) wneuper@59381: else (* this allows to check Rrls with prepat = ([@{term True}], pat) *) wneuper@59381: if asms = [@{term False}] then ([], false) wneuper@59381: else wneuper@59381: let wneuper@59381: fun chk indets [] = (indets, true) (*return asms<>True until false*) wneuper@59381: | chk indets (a :: asms) = wneuper@59381: (case rewrite__set_ thy (i + 1) false bdv rls a of wneuper@59381: NONE => (chk (indets @ [a]) asms) wneuper@59381: | SOME (t, a') => wneuper@59381: if t = @{term True} then (chk (indets @ a') asms) wneuper@59381: else if t = @{term False} then ([], false) wneuper@59381: (*asm false .. thm not applied ^^^; continue until False vvv*) wneuper@59381: else chk (indets @ [t] @ a') asms); wneuper@59381: in chk [] asms end wneuper@59416: and rewrite__set_ thy _ __ Rule.Erls t = (* rewrite with a rule set *) wneuper@59416: error ("rewrite__set_ called with 'Erls' for '" ^ Rule.t2str thy t ^ "'") wneuper@59416: | rewrite__set_ thy i _ _ (rrls as Rule.Rrls _) t = (* rewrite with a 'reverse rule set' *) neuper@52101: let wneuper@59416: val _= trace i (" rls: " ^ Rule.id_rls rrls ^ " on: " ^ Rule.t2str thy t) wneuper@59382: val (t', asm, rew) = app_rev thy (i + 1) rrls t neuper@52101: in if rew then SOME (t', distinct asm) else NONE end wneuper@59382: | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Calc, Cal1 *) neuper@52101: let wneuper@59398: (* attention with cp to test/..: unbound thy, i, bdv, rls TODO1803? pull out to rewrite__*) neuper@52101: datatype switch = Appl | Noap; wneuper@59399: fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Tools.rew_once? *) neuper@52101: | rew_once ruls asm ct Appl [] = wneuper@59416: (case rls of Rule.Rls _ => rew_once ruls asm ct Noap ruls wneuper@59416: | Rule.Seq _ => (ct, asm) wneuper@59416: | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule.rls2str rls ^ "\"")) wneuper@59381: | rew_once ruls asm ct apno (rul :: thms) = neuper@52101: case rul of wneuper@59416: Rule.Thm (thmid, thm) => neuper@52101: (trace1 i (" try thm: " ^ thmid); wneuper@59416: case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls) wneuper@59416: ((#erls o Rule.rep_rls) rls) put_asm thm ct of neuper@52101: NONE => rew_once ruls asm ct apno thms wneuper@59381: | SOME (ct', asm') => wneuper@59416: (trace1 i (" rewrites to: " ^ Rule.t2str thy ct'); wneuper@59399: rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms))) wneuper@59399: (* once again try the same rule, e.g. associativity against "()"*) wneuper@59416: | Rule.Calc (cc as (op_, _)) => neuper@52101: let val _= trace1 i (" try calc: " ^ op_ ^ "'") wneuper@59389: val ct = TermC.uminus_to_string ct wneuper@59386: in case Calc.adhoc_thm thy cc ct of neuper@52101: NONE => rew_once ruls asm ct apno thms wneuper@59381: | SOME (_, thm') => neuper@52101: let wneuper@59416: val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls) wneuper@59416: ((#erls o Rule.rep_rls) rls) put_asm thm' ct; neuper@52101: val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ wneuper@59416: Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE") wneuper@59416: val _ = trace1 i (" calc. to: " ^ Rule.t2str thy ((fst o the) pairopt)) neuper@52101: in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end neuper@52101: end wneuper@59416: | Rule.Cal1 (cc as (op_, _)) => neuper@52101: let val _= trace1 i (" try cal1: " ^ op_ ^ "'"); wneuper@59389: val ct = TermC.uminus_to_string ct wneuper@59386: in case Calc.adhoc_thm1_ thy cc ct of neuper@52101: NONE => (ct, asm) wneuper@59381: | SOME (_, thm') => neuper@52101: let wneuper@59416: val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls) wneuper@59416: ((#erls o Rule.rep_rls) rls) put_asm thm' ct; neuper@52101: val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ wneuper@59416: Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE") wneuper@59416: val _ = trace1 i (" cal1. to: " ^ Rule.t2str thy ((fst o the) pairopt)) neuper@52101: in the pairopt end neuper@52101: end wneuper@59416: | Rule.Rls_ rls' => neuper@52101: (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of neuper@52101: SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms wneuper@59381: | NONE => rew_once ruls asm ct apno thms) wneuper@59416: | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\""); wneuper@59416: val ruls = (#rules o Rule.rep_rls) rls; wneuper@59416: val _ = trace i (" rls: " ^ Rule.id_rls rls ^ " on: " ^ Rule.t2str thy ct) neuper@52101: val (ct', asm') = rew_once ruls [] ct Noap ruls; neuper@52101: in if ct = ct' then NONE else SOME (ct', distinct asm') end wneuper@59405: (*------------------------ wneuper@59405: -------------------------------------*) wneuper@59381: and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms *) neuper@52085: let (* check a (precond, pattern) of a rev-set; stops with 1st true *) wneuper@59381: fun chk_prepat _ _ [] _ = true neuper@52085: | chk_prepat thy erls prepat t = neuper@52085: let neuper@52085: fun chk (pres, pat) = neuper@52085: (let neuper@52085: val subst: Type.tyenv * Envir.tenv = neuper@52085: Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty) neuper@52085: in neuper@52085: snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls) wneuper@59381: end) handle _ (*TODO Pattern.MATCH*) => false wneuper@59381: fun scan_ _ [] = false wneuper@59398: | scan_ f (pp :: pps) = neuper@52085: if f pp then true else scan_ f pps; neuper@52085: in scan_ chk prepat end; neuper@52085: (* apply the normal_form of a rev-set *) wneuper@59416: fun app_rev' thy (Rule.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t = wneuper@59381: if chk_prepat thy erls prepat t then normal_form t else NONE wneuper@59416: | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule.rls2str r ^ "\""); neuper@52085: val opt = app_rev' thy rrls t neuper@52085: in neuper@52085: case opt of neuper@52085: SOME (t', asm) => (t', asm, true) neuper@52085: | NONE => app_sub thy i rrls t neuper@52085: end wneuper@59381: and app_sub thy i rrls t = (* apply an Rrls to subterms *) neuper@52085: case t of neuper@52085: Const (s, T) => (Const(s, T), [], false) neuper@52085: | Free (s, T) => (Free(s, T), [], false) neuper@52085: | Var (n, T) => (Var(n, T), [], false) neuper@52085: | Bound i => (Bound i, [], false) neuper@52085: | Abs (s, T, body) => neuper@37906: let val (t', asm, rew) = app_rev thy i rrls body neuper@37906: in (Abs(s, T, t'), asm, rew) end neuper@52085: | t1 $ t2 => neuper@52085: let val (t2', asm2, rew2) = app_rev thy i rrls t2 neuper@52085: in neuper@52085: if rew2 then (t1 $ t2', asm2, true) neuper@52085: else neuper@52085: let val (t1', asm1, rew1) = app_rev thy i rrls t1 neuper@52085: in if rew1 then (t1' $ t2, asm1, true) neuper@52085: else (t1 $ t2, [], false) neuper@52085: end wneuper@59381: end; neuper@37906: wneuper@59381: (* rewriting without argument [] for rew_ord; WN110603: shouldnt asm<>[] lead to false? *) neuper@37906: fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls; neuper@37906: neuper@52101: (* rewriting without internal argument [] *) neuper@52101: fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term; neuper@52101: fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term; neuper@37906: wneuper@59381: (* variants of rewrite; TODO del. put_asm *) wneuper@59381: fun rewrite_inst_ thy rew_ord rls put_asm subst thm ct = wneuper@59381: rewrite__ thy 1 subst rew_ord rls put_asm thm ct; wneuper@59381: fun rewrite_set_inst_ thy put_asm subst rls ct = rewrite__set_ thy 1 put_asm subst rls ct; neuper@37906: neuper@38025: (* given a list of equalities (lhs = rhs) and a term, neuper@38025: replace all occurrences of lhs in the term with rhs; neuper@38025: thus the order or equalities matters: put variables in lhs first. *) neuper@38025: fun rewrite_terms_ thy ord erls equs t = neuper@42359: let neuper@42359: fun rew_ (t', asm') [] _ = (t', asm') neuper@42359: | rew_ (t', asm') (rules as r::rs) t = neuper@42359: let wneuper@59390: val (t'', asm'', _(*lrd*), rew) = rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t neuper@42359: in neuper@42359: if rew neuper@42359: then rew_ (t'', asm' @ asm'') rules t'' neuper@42359: else rew_ (t', asm') rs t' neuper@42359: end wneuper@59416: val (t'', asm'') = rew_ (Rule.e_term, []) equs t wneuper@59416: in if t'' = Rule.e_term then NONE else SOME (t'', asm'') neuper@42359: end; neuper@37906: wneuper@59381: (* search ct for adjacent numerals and calculate them by operator isa_fn *) neuper@37906: fun calculate_ thy isa_fn ct = wneuper@59389: let val ct = TermC.uminus_to_string ct wneuper@59386: in case Calc.adhoc_thm thy isa_fn ct of neuper@37906: NONE => NONE wneuper@59381: | SOME (thmID, thm) => wneuper@59416: (let val rew = case rewrite_ thy Rule.dummy_ord Rule.e_rls false thm ct of wneuper@59381: SOME (rew, _) => rew wneuper@59381: | NONE => raise ERROR "" wneuper@59381: in SOME (rew, (thmID, thm)) end) wneuper@59381: handle _ (*TODO Pattern.MATCH ?del?*)=> error ("calculate_: " ^ thmID ^ " does not rewrite") neuper@37906: end; neuper@37906: wneuper@59381: (* Thm.make_thm added to Pure/thm.ML *) neuper@37906: fun mk_thm thy str = wneuper@59385: let wneuper@59389: val t = (Thm.term_of o the o (TermC.parse thy)) str wneuper@59385: val t' = case t of wneuper@59385: Const ("Pure.imp", _) $ _ $ _ => t wneuper@59390: | _ => HOLogic.Trueprop $ t wneuper@59385: in Thm.make_thm (Thm.global_cterm_of thy t') end; neuper@37906: wneuper@59108: (* "metaview" as seen from programs and from user input (both are parsed like terms presently) *) wneuper@59108: fun convert_metaview_to_thmid thy thmid = wneuper@59108: let val thmid' = case thmid of wneuper@59108: "add_commute" => "add.commute" wneuper@59108: | "mult_commute" => "mult.commute" wneuper@59108: | "add_left_commute" => "add.left_commute" wneuper@59108: | "mult_left_commute" => "mult.left_commute" wneuper@59108: | "add_assoc" => "add.assoc" wneuper@59108: | "mult_assoc" => "mult.assoc" wneuper@59108: | _ => thmid wneuper@59108: in (Global_Theory.get_thm thy) thmid' end; wneuper@59108: wneuper@59381: (* get the theorem associated with the xstring-identifier; neuper@37906: if the identifier starts with "sym_" then swap lhs = rhs around = neuper@37906: (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI); neuper@37906: identifiers starting with "#" come from Calc and wneuper@59381: get a hand-made theorem (containing numerals only) *) wneuper@59381: fun assoc_thm'' thy thmid = wneuper@59253: case Symbol.explode thmid of wneuper@59253: "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid) wneuper@59389: | "s"::"y"::"m"::"_"::id => ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym wneuper@59253: | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid) wneuper@59389: | _ => thmid |> convert_metaview_to_thmid thy |> TermC.num_str wneuper@59381: fun assoc_thm' thy (thmid, ct') = neuper@55487: (case Symbol.explode thmid of neuper@55487: "s"::"y"::"m"::"_"::id => neuper@55487: if hd id = "#" neuper@55487: then mk_thm thy ct' wneuper@59389: else ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym wneuper@59109: | id => neuper@55487: if hd id = "#" neuper@55487: then mk_thm thy ct' wneuper@59389: else thmid |> convert_metaview_to_thmid thy |> TermC.num_str wneuper@59381: ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) => wneuper@59416: error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ Rule.theory2domID thy ^ "\" (and parents)") neuper@37906: neuper@37906: fun eval_listexpr_ thy srls t = neuper@52139: let val rew = rewrite_set_ thy false srls t; neuper@52139: in case rew of SOME (res,_) => res | NONE => t end; neuper@37906: neuper@41928: fun eval_true_ _ _ (Const ("HOL.True",_)) = true wneuper@59405: | eval_true_ thy' rls t = wneuper@59405: case rewrite_set_ (Celem.assoc_thy thy') false rls t of neuper@41928: SOME (Const ("HOL.True",_),_) => true neuper@37906: | _ => false; neuper@37906: wneuper@59380: end