neuper@37906: (* isac's rewriter neuper@37906: (c) Walther Neuper 2000 neuper@37906: *) neuper@37906: wneuper@59380: signature REWRITE = walther@59901: sig walther@60269: exception NO_REWRITE Walther@60500: val calculate_: Proof.context -> string * Eval_Def.eval_fn -> term -> (term * (string * thm)) option Walther@60500: val eval__true: Proof.context -> int -> term list -> Subst.T -> Rule_Set.T -> term list * bool Walther@60500: val eval_prog_expr: Proof.context -> Rule_Set.T -> term -> term Walther@60500: val eval_true_: Proof.context -> Rule_Set.T -> term -> bool Walther@60500: val eval_true: Proof.context -> term list -> Rule_Set.T -> bool Walther@60509: val rew_sub: Proof.context -> int -> Subst.T -> Rewrite_Ord.function walther@59901: -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool Walther@60509: val rewrite_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool -> thm -> walther@59901: term -> (term * term list) option Walther@60509: val rewrite_inst_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool Walther@60477: -> Subst.T -> thm -> term -> (term * term list) option Walther@60500: val rewrite_set_: Proof.context -> bool -> Rule_Set.T -> term -> (term * term list) option Walther@60500: val rewrite_set_inst_: Proof.context -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option Walther@60509: val rewrite_terms_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> term list walther@59901: -> term -> (term * term list) option walther@59901: wenzelm@60223: \<^isac_test>\ Walther@60509: val rewrite__: Proof.context -> int -> Subst.T -> Rewrite_Ord.function -> walther@59901: Rule_Set.T -> bool -> thm -> term -> (term * term list) option Walther@60500: val rewrite__set_: Proof.context -> int -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option Walther@60500: val app_rev: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool Walther@60500: val app_sub: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool Walther@60500: val trace1: Proof.context -> int -> string -> unit Walther@60500: val trace_eq1 : Proof.context -> int -> string -> Rule_Def.rule_set -> term -> unit; Walther@60500: val trace_eq2 : Proof.context -> int -> string -> term -> term -> unit; Walther@60500: val trace_in1 : Proof.context -> int -> string -> string -> unit; Walther@60500: val trace_in2 : Proof.context -> int -> string -> term -> unit; Walther@60500: val trace_in3 : Proof.context -> int -> string -> (term * 'a) option -> unit; Walther@60500: val trace_in4 : Proof.context -> int -> string -> term list -> term list -> unit; Walther@60500: val trace_in5 : Proof.context -> int -> string -> term list -> unit; wenzelm@60223: \ walther@59901: end wneuper@59380: Walther@60500: (* must be global for re-use in other structs *) Walther@60500: val rewrite_trace = Attrib.setup_config_bool \<^binding>\rewrite_trace\ (K false); Walther@60501: (* no of rewrites exceeding this int -> NO_REWRITE *) Walther@60501: val rewrite_limit = Attrib.setup_config_int \<^binding>\rewrite_limit\ (K 100); Walther@60501: wneuper@59380: (**) wneuper@59380: structure Rewrite(**): REWRITE(**) = wneuper@59380: struct wneuper@59380: (**) neuper@37906: neuper@37906: exception NO_REWRITE; neuper@37906: Walther@60507: (* depth of recursion in traces of the rewriter, if trace_on = true *) Walther@60501: val rewrite_trace_depth = Attrib.setup_config_int \<^binding>\rewrite_trace_depth\ (K 99999); walther@59901: Walther@60500: fun trace ctxt i str = Walther@60501: if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth Walther@60501: then tracing (idt "#" i ^ str) else () Walther@60500: fun trace_eq1 ctxt i str rrls t = Walther@60500: trace ctxt i (" " ^ str ^ ": " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_ctxt ctxt t) Walther@60500: fun trace_eq2 ctxt i str t t' = Walther@60500: trace ctxt i (" " ^ str ^ ": \"" ^ Walther@60500: UnparseC.term_in_ctxt ctxt t ^ "\" > \"" ^ UnparseC.term_in_ctxt ctxt t' ^ "\""); Walther@60500: fun trace1 ctxt i str = Walther@60501: if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth Walther@60501: then tracing (idt "#" (i + 1) ^ str) else () Walther@60500: fun trace_in1 ctxt i str thmid = Walther@60500: trace1 ctxt i (" " ^ str ^ ": \"" ^ thmid ^ "\"") Walther@60500: fun trace_in2 ctxt i str t = Walther@60500: trace1 ctxt i (" " ^ str ^ ": \"" ^ UnparseC.term_in_ctxt ctxt t ^ "\""); Walther@60500: fun trace_in3 ctxt i str pairopt = Walther@60500: trace1 ctxt i (" " ^ str ^ ": " ^ UnparseC.term_in_ctxt ctxt ((fst o the) pairopt)); Walther@60500: fun trace_in4 ctxt i str ts ts' = Walther@60501: if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth andalso ts <> [] Walther@60500: then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_ctxt ctxt ts ^ Walther@60500: " stored: " ^ UnparseC.terms_in_ctxt ctxt ts') walther@60262: else (); Walther@60500: fun trace_in5 ctxt i str p' = Walther@60501: if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth Walther@60500: then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_ctxt ctxt p') walther@60262: else(); Walther@60500: fun msg call ctxt op_ thmC t = walther@60390: call ^ ": \n" ^ walther@60390: "Eval.get_pair for " ^ quote op_ ^ " \ SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^ Walther@60500: "but rewrite__ on " ^ quote (UnparseC.term_in_ctxt ctxt t) ^ " \ NONE"; neuper@52101: Walther@60500: fun rewrite__ ctxt i bdv tless rls put_asm thm ct = wneuper@59381: let Walther@60500: val (t', asms, _(*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path) wenzelm@60203: (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct walther@60017: in if rew then SOME (t', distinct op = asms) else NONE end walther@60262: (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *) Walther@60500: and rew_sub ctxt 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 Walther@60500: val r' = (Envir.subst_term (Pattern.match (Proof_Context.theory_of ctxt) Walther@60500: (lhs, t) (Vartab.empty, Vartab.empty)) r) walther@60262: handle Pattern.MATCH => raise NO_REWRITE 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' Walther@60500: val _ = trace_in2 ctxt i "eval asms" r'; walther@60262: val (t'', p'') = (*conditional rewriting*) Walther@60500: let val (simpl_p', nofalse) = eval__true ctxt (i + 1) p' bdv rls wneuper@59381: in wneuper@59381: if nofalse Walther@60500: then (trace_in4 ctxt i "asms accepted" p' simpl_p'; (t', simpl_p'))(*uncond.rew.from above*) Walther@60500: else (trace_in5 ctxt i "asms false" p'; raise NO_REWRITE) (* don't go into subtm.of cond*) walther@60324: end walther@60262: in walther@60262: if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*) Walther@60500: then (trace_eq2 ctxt i "not >" t t'; raise NO_REWRITE) walther@60262: else (t'', p'', [], true) walther@60262: end walther@60262: ) handle NO_REWRITE => walther@60262: (case t of walther@60262: Const(s, T) => (Const(s, T), [], lrd, false) walther@60262: | Free(s, T) => (Free(s, T), [], lrd, false) walther@60262: | Var(n, T) => (Var(n, T), [], lrd, false) walther@60262: | Bound i => (Bound i, [], lrd, false) walther@60262: | Abs(s, T, body) => Walther@60500: let val (t', asms, _ (*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.D]) r body walther@60262: in (Abs(s, T, t'), asms, [], rew) end walther@60262: | t1 $ t2 => Walther@60500: let val (t2', asm2, lrd, rew2) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.R]) r t2 walther@60262: in walther@60262: if rew2 then (t1 $ t2', asm2, lrd, true) walther@60262: else Walther@60500: let val (t1', asm1, lrd, rew1) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.L]) r t1 walther@60262: in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end walther@60262: end) Walther@60500: and eval__true ctxt i asms bdv rls = (* rewrite 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) = Walther@60500: (case rewrite__set_ ctxt (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 Walther@60500: and rewrite__set_ ctxt (*1*)_ _ _ Rule_Set.Empty t = (* rewrite with a rule set*) Walther@60500: raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_ctxt ctxt t ^ "'") Walther@60500: | rewrite__set_ (*2*)ctxt i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set'*) neuper@52101: let Walther@60500: val _= trace_eq1 ctxt i "rls" rrls t; Walther@60500: val (t', asm, rew) = app_rev ctxt (i + 1) rrls t walther@60017: in if rew then SOME (t', distinct op = asm) else NONE end Walther@60500: | rewrite__set_ (*3*)ctxt i put_asm bdv rls ct = (* Rls, Seq containing Thms or Eval, Cal1 *) neuper@52101: let Walther@60500: (* attention with cp to test/..: unbound ctxt, i, bdv, rls; TODO1803? pull out to rewrite__*) neuper@52101: datatype switch = Appl | Noap; walther@60389: fun rew_once (*1*)_ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *) walther@60389: | rew_once (*2*)ruls asm ct Appl [] = walther@59851: (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls walther@59878: | Rule_Set.Sequence _ => (ct, asm) walther@59867: | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\"")) walther@60389: | rew_once (*3*)ruls asm ct apno (rul :: thms) = neuper@52101: case rul of wneuper@59416: Rule.Thm (thmid, thm) => Walther@60500: (trace_in1 ctxt i "try thm" thmid; Walther@60500: case rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) walther@59852: ((#erls o Rule_Set.rep) rls) put_asm thm ct of neuper@52101: NONE => rew_once ruls asm ct apno thms wneuper@59381: | SOME (ct', asm') => Walther@60500: (trace_in2 ctxt i "rewrites to" 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 "()"*) Walther@60500: | Rule.Eval (cc as (op_, _)) => Walther@60500: let val _ = trace_in1 ctxt i "try calc" op_; Walther@60500: in case Eval.adhoc_thm (Proof_Context.theory_of ctxt) cc ct of neuper@52101: NONE => rew_once ruls asm ct apno thms wneuper@59381: | SOME (_, thm') => neuper@52101: let Walther@60500: val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) walther@59852: ((#erls o Rule_Set.rep) rls) put_asm thm' ct; Walther@60500: val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" ctxt op_ thm' ct) Walther@60500: val _ = trace_in3 ctxt i "calc. to" 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_, _)) => Walther@60500: let val _ = trace_in1 ctxt i "try cal1" op_; Walther@60500: in case Eval.adhoc_thm1_ (Proof_Context.theory_of ctxt) cc ct of neuper@52101: NONE => (ct, asm) wneuper@59381: | SOME (_, thm') => neuper@52101: let Walther@60500: val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) walther@59852: ((#erls o Rule_Set.rep) rls) put_asm thm' ct; walther@59962: val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^ Walther@60500: ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_ctxt ctxt ct ^ " = NONE") Walther@60500: val _ = trace_in3 ctxt i "cal1. to" pairopt; neuper@52101: in the pairopt end neuper@52101: end wneuper@59416: | Rule.Rls_ rls' => Walther@60500: (case rewrite__set_ ctxt (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) walther@59867: | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\""); walther@59852: val ruls = (#rules o Rule_Set.rep) rls; Walther@60500: val _ = trace_eq1 ctxt i "rls" rls ct neuper@52101: val (ct', asm') = rew_once ruls [] ct Noap ruls; walther@60017: in if ct = ct' then NONE else SOME (ct', distinct op = asm') end Walther@60500: (*--vvv and app_sub are type correct-----------------------------------------------------------*) Walther@60500: and app_rev ctxt 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 Walther@60500: | chk_prepat ctxt erls prepat t = neuper@52085: let neuper@52085: fun chk (pres, pat) = neuper@52085: (let neuper@52085: val subst: Type.tyenv * Envir.tenv = Walther@60500: Pattern.match (Proof_Context.theory_of ctxt) (pat, t) (Vartab.empty, Vartab.empty) neuper@52085: in Walther@60500: snd (eval__true ctxt (i + 1) (map (Envir.subst_term subst) pres) [] erls) walther@60267: end) handle 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 *) Walther@60500: fun app_rev' ctxt (Rule_Set.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t = Walther@60500: if chk_prepat ctxt erls prepat t then normal_form t else NONE walther@59867: | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule_Set.id r ^ "\""); Walther@60500: val opt = app_rev' ctxt rrls t neuper@52085: in neuper@52085: case opt of neuper@52085: SOME (t', asm) => (t', asm, true) Walther@60500: | NONE => app_sub ctxt i rrls t neuper@52085: end Walther@60500: and app_sub ctxt 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) => Walther@60500: let val (t', asm, rew) = app_rev ctxt i rrls body neuper@37906: in (Abs(s, T, t'), asm, rew) end neuper@52085: | t1 $ t2 => Walther@60500: let val (t2', asm2, rew2) = app_rev ctxt i rrls t2 neuper@52085: in neuper@52085: if rew2 then (t1 $ t2', asm2, true) neuper@52085: else Walther@60500: let val (t1', asm1, rew1) = app_rev ctxt 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: walther@60324: (* rewriting without argument [] for rew_ord *) neuper@37906: fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls; neuper@37906: walther@60324: (* rewriting without internal arguments 1, [] *) 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 walther@59861: val (t'', asm'') = rew_ (TermC.empty, []) equs t walther@59861: in if t'' = TermC.empty 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 *) Walther@60500: fun calculate_ ctxt (isa_fn as (id, eval_fn)) t = Walther@60500: case Eval.adhoc_thm (Proof_Context.theory_of ctxt) isa_fn t of walther@60337: NONE => NONE walther@60337: | SOME (thmID, thm) => Walther@60509: (let val rew = case rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm t of walther@60337: SOME (rew, _) => rew Walther@60500: | NONE => raise ERROR (msg "calculate_" ctxt id thm t) walther@60337: in SOME (rew, (thmID, thm)) end) walther@60337: handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite"); neuper@37906: walther@59718: fun eval_prog_expr 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: wenzelm@60309: fun eval_true_ _ _ (Const (\<^const_name>\True\,_)) = true walther@59722: | eval_true_ thy rls t = walther@59722: case rewrite_set_ thy false rls t of wenzelm@60309: SOME (Const (\<^const_name>\True\,_),_) => true neuper@37906: | _ => false; neuper@37906: walther@60262: end