1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Fri Apr 10 14:46:55 2020 +0200
1.3 @@ -0,0 +1,342 @@
1.4 +(* isac's rewriter
1.5 + (c) Walther Neuper 2000
1.6 +*)
1.7 +
1.8 +signature REWRITE =
1.9 + sig
1.10 +(*/------- to ThmC_Def -------\*)
1.11 + val assoc_thm': theory -> ThmC_Def.thm' -> thm
1.12 + val assoc_thm'': theory -> ThmC_Def.thmID -> thm
1.13 +(*\------- to ThmC_Def -------/*)
1.14 + val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
1.15 + val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
1.16 + val eval_prog_expr: theory -> Rule_Set.T -> term -> term
1.17 + val eval_true_: theory -> Rule_Set.T -> term -> bool
1.18 + val eval_true: theory -> term list -> Rule_Set.T -> bool
1.19 + val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
1.20 + -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
1.21 + val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
1.22 + term -> (term * term list) option
1.23 + val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
1.24 + -> (term * term) list -> thm -> term -> (term * term list) option
1.25 + val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
1.26 + val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
1.27 + val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
1.28 + -> term -> (term * term list) option
1.29 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.30 + (* NONE *)
1.31 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.32 + val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
1.33 + Rule_Set.T -> bool -> thm -> term -> (term * term list) option
1.34 + val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
1.35 + val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
1.36 + val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
1.37 + val mk_thm: theory -> string -> thm
1.38 + val trace1: int -> string -> unit
1.39 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.40 + end
1.41 +
1.42 +(**)
1.43 +structure Rewrite(**): REWRITE(**) =
1.44 +struct
1.45 +(**)
1.46 +
1.47 +exception NO_REWRITE;
1.48 +exception STOP_REW_SUB; (*WN050820 quick and dirty*)
1.49 +
1.50 +fun trace i str =
1.51 + if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" i ^ str) else ()
1.52 +fun trace1 i str =
1.53 + if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" (i + 1) ^ str) else ()
1.54 +
1.55 +fun rewrite__ thy i bdv tless rls put_asm thm ct =
1.56 + let
1.57 + val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
1.58 + (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm) ct
1.59 + in if rew then SOME (t', distinct asms) else NONE end
1.60 + (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
1.61 +and rew_sub thy i bdv tless rls put_asm lrd r t =
1.62 + (let
1.63 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
1.64 + (*?alternative Unify.matchers:
1.65 + http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML*)
1.66 + val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
1.67 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
1.68 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
1.69 + val _ = if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
1.70 + then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.t2str thy r') else ()
1.71 + val (t'', p'') = (*conditional rewriting*)
1.72 + let
1.73 + val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
1.74 + in
1.75 + if nofalse
1.76 + then
1.77 + (if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
1.78 + then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.ts2str thy p' ^
1.79 + " stored: " ^ UnparseC.ts2str thy simpl_p')
1.80 + else();
1.81 + (t',simpl_p')) (* uncond.rew. from above*)
1.82 + else
1.83 + (if ! Celem.trace_rewrite andalso i < ! Celem.depth
1.84 + then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.ts2str thy p')
1.85 + else();
1.86 + raise STOP_REW_SUB (* don't go into subterms of cond *))
1.87 + end
1.88 + in
1.89 + if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
1.90 + then (if ! Celem.trace_rewrite andalso i < ! Celem.depth
1.91 + then tracing (idt"#"i ^ " not: \"" ^ UnparseC.t2str thy t ^ "\" > \"" ^ UnparseC.t2str thy t' ^ "\"")
1.92 + else ();
1.93 + raise NO_REWRITE)
1.94 + else (t'', p'', [], true)
1.95 + end
1.96 + ) handle _ (*TODO Pattern.MATCH when tests are ready: ERROR 364ce4699452 *) =>
1.97 + (case t of
1.98 + Const(s,T) => (Const(s,T),[],lrd,false)
1.99 + | Free(s,T) => (Free(s,T),[],lrd,false)
1.100 + | Var(n,T) => (Var(n,T),[],lrd,false)
1.101 + | Bound i => (Bound i,[],lrd,false)
1.102 + | Abs(s,T,body) =>
1.103 + let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.D]) r body
1.104 + in (Abs(s, T, t'), asms, [], rew) end
1.105 + | t1 $ t2 =>
1.106 + let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
1.107 + in
1.108 + if rew2 then (t1 $ t2', asm2, lrd, true)
1.109 + else
1.110 + let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
1.111 + in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
1.112 + end)
1.113 +and eval__true thy i asms bdv rls = (* simplify asumptions until one evaluates to false *)
1.114 + if asms = [@{term True}] orelse asms = [] then ([], true)
1.115 + else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
1.116 + if asms = [@{term False}] then ([], false)
1.117 + else
1.118 + let
1.119 + fun chk indets [] = (indets, true) (*return asms<>True until false*)
1.120 + | chk indets (a :: asms) =
1.121 + (case rewrite__set_ thy (i + 1) false bdv rls a of
1.122 + NONE => (chk (indets @ [a]) asms)
1.123 + | SOME (t, a') =>
1.124 + if t = @{term True} then (chk (indets @ a') asms)
1.125 + else if t = @{term False} then ([], false)
1.126 + (*asm false .. thm not applied ^^^; continue until False vvv*)
1.127 + else chk (indets @ [t] @ a') asms);
1.128 + in chk [] asms end
1.129 +and rewrite__set_ thy _ __ Rule_Set.Empty t = (* rewrite with a rule set *)
1.130 + error ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.t2str thy t ^ "'")
1.131 + | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set' *)
1.132 + let
1.133 + val _= trace i (" rls: " ^ Rule_Set.rls2str rrls ^ " on: " ^ UnparseC.t2str thy t)
1.134 + val (t', asm, rew) = app_rev thy (i + 1) rrls t
1.135 + in if rew then SOME (t', distinct asm) else NONE end
1.136 + | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Num_Calc, Cal1 *)
1.137 + let
1.138 + (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
1.139 + datatype switch = Appl | Noap;
1.140 + fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
1.141 + | rew_once ruls asm ct Appl [] =
1.142 + (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
1.143 + | Rule_Set.Seqence _ => (ct, asm)
1.144 + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.rls2str rls ^ "\""))
1.145 + | rew_once ruls asm ct apno (rul :: thms) =
1.146 + case rul of
1.147 + Rule.Thm (thmid, thm) =>
1.148 + (trace1 i (" try thm: \"" ^ thmid ^ "\"");
1.149 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.150 + ((#erls o Rule_Set.rep) rls) put_asm thm ct of
1.151 + NONE => rew_once ruls asm ct apno thms
1.152 + | SOME (ct', asm') =>
1.153 + (trace1 i (" rewrites to: \"" ^ UnparseC.t2str thy ct' ^ "\"");
1.154 + rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
1.155 + (* once again try the same rule, e.g. associativity against "()"*)
1.156 + | Rule.Num_Calc (cc as (op_, _)) =>
1.157 + let val _= trace1 i (" try calc: \"" ^ op_ ^ "\"")
1.158 + val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
1.159 + in case Num_Calc.adhoc_thm thy cc ct of
1.160 + NONE => rew_once ruls asm ct apno thms
1.161 + | SOME (_, thm') =>
1.162 + let
1.163 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.164 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
1.165 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.166 + ThmC_Def.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
1.167 + val _ = trace1 i (" calc. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
1.168 + in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
1.169 + end
1.170 + | Rule.Cal1 (cc as (op_, _)) =>
1.171 + let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
1.172 + val ct = TermC.uminus_to_string ct
1.173 + in case Num_Calc.adhoc_thm1_ thy cc ct of
1.174 + NONE => (ct, asm)
1.175 + | SOME (_, thm') =>
1.176 + let
1.177 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
1.178 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
1.179 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.180 + ThmC_Def.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
1.181 + val _ = trace1 i (" cal1. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
1.182 + in the pairopt end
1.183 + end
1.184 + | Rule.Rls_ rls' =>
1.185 + (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
1.186 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
1.187 + | NONE => rew_once ruls asm ct apno thms)
1.188 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
1.189 + val ruls = (#rules o Rule_Set.rep) rls;
1.190 + val _ = trace i (" rls: " ^ Rule_Set.rls2str rls ^ " on: " ^ UnparseC.t2str thy ct)
1.191 + val (ct', asm') = rew_once ruls [] ct Noap ruls;
1.192 + in if ct = ct' then NONE else SOME (ct', distinct asm') end
1.193 +(*-------------------------------------------------------------*)
1.194 +and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms *)
1.195 + let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
1.196 + fun chk_prepat _ _ [] _ = true
1.197 + | chk_prepat thy erls prepat t =
1.198 + let
1.199 + fun chk (pres, pat) =
1.200 + (let
1.201 + val subst: Type.tyenv * Envir.tenv =
1.202 + Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
1.203 + in
1.204 + snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
1.205 + end) handle _ (*TODO Pattern.MATCH*) => false
1.206 + fun scan_ _ [] = false
1.207 + | scan_ f (pp :: pps) =
1.208 + if f pp then true else scan_ f pps;
1.209 + in scan_ chk prepat end;
1.210 + (* apply the normal_form of a rev-set *)
1.211 + fun app_rev' thy (Rule_Set.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t =
1.212 + if chk_prepat thy erls prepat t then normal_form t else NONE
1.213 + | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule_Set.rls2str r ^ "\"");
1.214 + val opt = app_rev' thy rrls t
1.215 + in
1.216 + case opt of
1.217 + SOME (t', asm) => (t', asm, true)
1.218 + | NONE => app_sub thy i rrls t
1.219 + end
1.220 +and app_sub thy i rrls t = (* apply an Rrls to subterms *)
1.221 + case t of
1.222 + Const (s, T) => (Const(s, T), [], false)
1.223 + | Free (s, T) => (Free(s, T), [], false)
1.224 + | Var (n, T) => (Var(n, T), [], false)
1.225 + | Bound i => (Bound i, [], false)
1.226 + | Abs (s, T, body) =>
1.227 + let val (t', asm, rew) = app_rev thy i rrls body
1.228 + in (Abs(s, T, t'), asm, rew) end
1.229 + | t1 $ t2 =>
1.230 + let val (t2', asm2, rew2) = app_rev thy i rrls t2
1.231 + in
1.232 + if rew2 then (t1 $ t2', asm2, true)
1.233 + else
1.234 + let val (t1', asm1, rew1) = app_rev thy i rrls t1
1.235 + in if rew1 then (t1' $ t2, asm1, true)
1.236 + else (t1 $ t2, [], false)
1.237 + end
1.238 + end;
1.239 +
1.240 +(* rewriting without argument [] for rew_ord; WN110603: shouldnt asm<>[] lead to false? *)
1.241 +fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
1.242 +
1.243 +(* rewriting without internal argument [] *)
1.244 +fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
1.245 +fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
1.246 +
1.247 +(* variants of rewrite; TODO del. put_asm *)
1.248 +fun rewrite_inst_ thy rew_ord rls put_asm subst thm ct =
1.249 + rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
1.250 +fun rewrite_set_inst_ thy put_asm subst rls ct = rewrite__set_ thy 1 put_asm subst rls ct;
1.251 +
1.252 +(* given a list of equalities (lhs = rhs) and a term,
1.253 + replace all occurrences of lhs in the term with rhs;
1.254 + thus the order or equalities matters: put variables in lhs first. *)
1.255 +fun rewrite_terms_ thy ord erls equs t =
1.256 + let
1.257 + fun rew_ (t', asm') [] _ = (t', asm')
1.258 + | rew_ (t', asm') (rules as r::rs) t =
1.259 + let
1.260 + val (t'', asm'', _(*lrd*), rew) = rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t
1.261 + in
1.262 + if rew
1.263 + then rew_ (t'', asm' @ asm'') rules t''
1.264 + else rew_ (t', asm') rs t'
1.265 + end
1.266 + val (t'', asm'') = rew_ (TermC.empty, []) equs t
1.267 + in if t'' = TermC.empty then NONE else SOME (t'', asm'')
1.268 + end;
1.269 +
1.270 +(* search ct for adjacent numerals and calculate them by operator isa_fn *)
1.271 +fun calculate_ thy isa_fn ct =
1.272 + let val ct = TermC.uminus_to_string ct
1.273 + in case Num_Calc.adhoc_thm thy isa_fn ct of
1.274 + NONE => NONE
1.275 + | SOME (thmID, thm) =>
1.276 + (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
1.277 + SOME (rew, _) => rew
1.278 + | NONE => raise ERROR ""
1.279 + in SOME (rew, (thmID, thm)) end)
1.280 + handle _ (*TODO Pattern.MATCH ?del?*)=> error ("calculate_: " ^ thmID ^ " does not rewrite")
1.281 + end;
1.282 +
1.283 +(* Thm.make_thm added to Pure/thm.ML *)
1.284 +fun mk_thm thy str =
1.285 + let
1.286 + val t = (Thm.term_of o the o (TermC.parse thy)) str
1.287 + val t' = case t of
1.288 + Const ("Pure.imp", _) $ _ $ _ => t
1.289 + | _ => HOLogic.Trueprop $ t
1.290 + in Thm.make_thm (Thm.global_cterm_of thy t') end;
1.291 +
1.292 +(*/------- to ThmC_Def -------\*)
1.293 +(*
1.294 + "metaview" as seen from programs and from user input;
1.295 + both are parsed as terms by the function package.
1.296 +*)
1.297 +fun convert_metaview_to_thmid thy thmid =
1.298 + let val thmid' = case thmid of
1.299 + "add_commute" => "add.commute"
1.300 + | "mult_commute" => "mult.commute"
1.301 + | "add_left_commute" => "add.left_commute"
1.302 + | "mult_left_commute" => "mult.left_commute"
1.303 + | "add_assoc" => "add.assoc"
1.304 + | "mult_assoc" => "mult.assoc"
1.305 + | _ => thmid
1.306 + in (Global_Theory.get_thm thy) thmid' end;
1.307 +
1.308 +(* get the theorem associated with the xstring-identifier;
1.309 + if the identifier starts with "sym_" then swap lhs = rhs around =
1.310 + (ATTENTION: "RS sym" attaches a [.] -- remove it with ThmC_Def.string_of_thmI);
1.311 + identifiers starting with "#" come from Num_Calc and
1.312 + get a hand-made theorem (containing numerals only) *)
1.313 +fun assoc_thm'' thy thmid =
1.314 + case Symbol.explode thmid of
1.315 + "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
1.316 + | "s"::"y"::"m"::"_"::id => ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
1.317 + | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
1.318 + | _ => thmid |> convert_metaview_to_thmid thy |> TermC.num_str
1.319 +fun assoc_thm' thy (thmid, ct') =
1.320 + (case Symbol.explode thmid of
1.321 + "s"::"y"::"m"::"_"::id =>
1.322 + if hd id = "#"
1.323 + then mk_thm thy ct'
1.324 + else ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
1.325 + | id =>
1.326 + if hd id = "#"
1.327 + then mk_thm thy ct'
1.328 + else thmid |> convert_metaview_to_thmid thy |> TermC.num_str
1.329 + ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) =>
1.330 + raise ERROR
1.331 + ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ ThyC.theory2domID thy ^ "\" (and parents)")
1.332 +(*\------- to ThmC_Def -------/*)
1.333 +
1.334 +
1.335 +fun eval_prog_expr thy srls t =
1.336 + let val rew = rewrite_set_ thy false srls t;
1.337 + in case rew of SOME (res,_) => res | NONE => t end;
1.338 +
1.339 +fun eval_true_ _ _ (Const ("HOL.True",_)) = true
1.340 + | eval_true_ thy rls t =
1.341 + case rewrite_set_ thy false rls t of
1.342 + SOME (Const ("HOL.True",_),_) => true
1.343 + | _ => false;
1.344 +
1.345 +end
1.346 \ No newline at end of file