1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,736 @@
1.4 +(* isac's rewriter
1.5 + (c) Walther Neuper 2000
1.6 +
1.7 +use"ProgLang/rewrite.sml";
1.8 +use"rewrite.sml";
1.9 +*)
1.10 +
1.11 +
1.12 +exception NO_REWRITE;
1.13 +exception STOP_REW_SUB; (*WN050820 quick and dirty*)
1.14 +
1.15 +(*17.6.00: rewrite by going down the term with rew_sub*)
1.16 +(* val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
1.17 + (thy, 1, []:(Term.term * Term.term) list, rew_ord, erls, bool,thm,term);
1.18 + *)
1.19 +fun rewrite__ thy i bdv tless rls put_asm thm ct =
1.20 + ((*writeln ("@@@ r..te__ begin: t = "^(term2str ct));*)
1.21 + let
1.22 + val (t',asms,lrd,rew) =
1.23 + rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
1.24 + (((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct;
1.25 + in if rew then SOME (t', distinct asms)
1.26 + else NONE end)
1.27 +(* val(r,t)=(((inst_bdv bdv) o norm o #prop o rep_thm) thm,ct);
1.28 + val t1 = (#prop o rep_thm) thm;
1.29 + val t2 = norm t1;
1.30 + val t3 = inst_bdv bdv t2;
1.31 +
1.32 + val thm4 = read_instantiate [("bdv","x")] thm;
1.33 + val t4 = (norm o #prop o rep_thm) thm4;
1.34 + *)
1.35 +(* val (thy, i, bdv, tless, rls, put_asm, r, t) =
1.36 + (thy, i,bdv, tless, rls, put_asm,
1.37 + (((inst_bdv bdv) o norm o #prop o rep_thm) thm), ct);
1.38 + val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
1.39 + (thy, 1, [], ord, erls,false, [], r, t);
1.40 + val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
1.41 + (thy, i, bdv, tless, rls, put_asm, [],
1.42 + ((inst_bdv bdv) o norm o #prop o rep_thm) thm, ct);
1.43 + *)
1.44 +and rew_sub thy i bdv tless rls put_asm lrd r t =
1.45 + ((*writeln ("@@@ rew_sub begin: t = "^(term2str t));*)
1.46 + let (* copy from Pure/thm.ML: fun rewritec *)
1.47 + (*val (lhs,rhs) = (dest_equals' o strip_trueprop
1.48 + o Logic.strip_imp_concl) r;
1.49 + val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs,t);
1.50 + val r' = ren_inst (insts, r, lhs, t);
1.51 + val p' = map strip_trueprop (Logic.strip_imp_prems r');
1.52 + val t' = (snd o dest_equals' o strip_trueprop
1.53 + o Logic.strip_imp_concl) r';*)
1.54 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
1.55 + o Logic.strip_imp_concl) r;
1.56 + val r' = Envir.subst_term (Pattern.match thy (lhs, t)
1.57 + (Vartab.empty, Vartab.empty)) r;
1.58 + val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
1.59 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
1.60 + o Logic.strip_imp_concl) r';
1.61 + (*val _= writeln("@@@ rew_sub match: t'= "^(term2str t'));*)
1.62 + val _= if ! trace_rewrite andalso i < ! depth andalso p' <> []
1.63 + then writeln((idt"#"(i+1))^" eval asms: "^(term2str r')) else();
1.64 + val (t'',p'') = (*conditional rewriting*)
1.65 + let val (simpl_p', nofalse) = eval__true thy (i+1) p' bdv rls
1.66 + in if nofalse
1.67 + then (if ! trace_rewrite andalso i < ! depth andalso p' <> []
1.68 + then writeln((idt"#"(i+1))^" asms accepted: "^(terms2str p')^
1.69 + " stored: "^(terms2str simpl_p'))
1.70 + else(); (t',simpl_p')) (* + uncond.rew. *)
1.71 + else
1.72 + (if ! trace_rewrite andalso i < ! depth
1.73 + then writeln((idt"#"(i+1))^" asms false: "^(terms2str p'))
1.74 + else(); raise STOP_REW_SUB (*dont go into subterms of cond*))
1.75 + end
1.76 + in if perm lhs rhs andalso not (tless bdv (t',t)) (*ordered rewriting*)
1.77 + then (if ! trace_rewrite andalso i < ! depth
1.78 + then writeln((idt"#"i)^" not: \""^
1.79 + (term2str t)^"\" > \""^
1.80 + (term2str t')^"\"") else ();
1.81 + raise NO_REWRITE )
1.82 + else ((*writeln("##@ rew_sub: (t''= "^(term2str t'')^
1.83 + ", p'' ="^(terms2str p'')^", true)");*)
1.84 + (t'',p'',[],true))
1.85 + end
1.86 + ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests + MATCH!*) =>
1.87 + ((*writeln ("@@@ rew_sub gosub: t = "^(term2str t));*)
1.88 + case t of
1.89 + Const(s,T) => (Const(s,T),[],lrd,false)
1.90 + | Free(s,T) => (Free(s,T),[],lrd,false)
1.91 + | Var(n,T) => (Var(n,T),[],lrd,false)
1.92 + | Bound i => (Bound i,[],lrd,false)
1.93 + | Abs(s,T,body) =>
1.94 + let val (t', asms, lrd, rew) =
1.95 + rew_sub thy i bdv tless rls put_asm (lrd@[D]) r body
1.96 + in (Abs(s,T,t'), asms, [], rew) end
1.97 + | t1 $ t2 =>
1.98 + let val (t2', asm2, lrd, rew2) =
1.99 + rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2
1.100 + in if rew2 then (t1 $ t2', asm2, lrd, true)
1.101 + else let val (t1', asm1, lrd, rew1) =
1.102 + rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1
1.103 + in if rew1 then (t1' $ t2, asm1, lrd, true)
1.104 + else (t1 $ t2,[], lrd, false) end
1.105 + end)
1.106 +(* val (cprems',rls)=([pre],prls);
1.107 + rewrite__set_ thy i false rls pre;
1.108 + *)
1.109 +and eval__true thy i asms bdv rls =
1.110 +(* val (thy, i, asms, bdv, rls) = (thy, (i+1), p', bdv, rls);
1.111 + *)
1.112 + if asms = [HOLogic.true_const] orelse asms = []
1.113 + then ([], true) else if asms = [HOLogic.false_const] then ([], false)
1.114 + else let
1.115 + fun chk indets [] = (indets, true)(*return asms<>True until false*)
1.116 + | chk indets (a::asms) =
1.117 +(* val (indets, (a::asms)) = ([], asms);
1.118 + *)
1.119 + (case rewrite__set_ thy (i+1) false bdv rls a of
1.120 + NONE => (chk (indets @ [a]) asms)
1.121 + | SOME (t, a') =>
1.122 + if t = HOLogic.true_const
1.123 + then (chk (indets @ a') asms)
1.124 + else if t = HOLogic.false_const then ([], false)
1.125 + (*asm false .. thm not applied ^^^; continue until False vvv*)
1.126 + else (chk (indets @ [t] @ a') asms));
1.127 + in chk [] asms end
1.128 +
1.129 +and rewrite__set_ _ _ __ Erls t =
1.130 + raise error("rewrite__set_ called with 'Erls' for '"^term2str t^"'")
1.131 + | rewrite__set_ thy i _ _ (rrls as Rrls _) t =
1.132 + let val _= if ! trace_rewrite andalso i < ! depth
1.133 + then writeln ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^
1.134 + (term2str t)) else ()
1.135 + val (t', asm, rew) = app_rev thy (i+1) rrls t
1.136 + in if rew then SOME (t', distinct asm)
1.137 + else NONE end
1.138 + | rewrite__set_ thy i put_asm bdv rls ct =
1.139 +(* val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
1.140 + *)
1.141 + let
1.142 + datatype switch = Appl | Noap;
1.143 + fun rew_once ruls asm ct Noap [] = (ct,asm)
1.144 + | rew_once ruls asm ct Appl [] =
1.145 + (case rls of Rls _ => rew_once ruls asm ct Noap ruls
1.146 + | Seq _ => (ct,asm))
1.147 + | rew_once ruls asm ct apno (rul::thms) =
1.148 +(* val (ruls, asm, ct, apno, (rul::thms)) = (ruls, [], ct, Noap, ruls);
1.149 + val Thm (thmid, thm) = rul;
1.150 + *)
1.151 + case rul of
1.152 + Thm (thmid, thm) =>
1.153 + (if !trace_rewrite andalso i < ! depth
1.154 + then writeln((idt"#"(i+1))^" try thm: "^thmid) else ();
1.155 + case rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
1.156 + ((#erls o rep_rls) rls) put_asm thm ct of
1.157 + NONE => rew_once ruls asm ct apno thms
1.158 + | SOME (ct',asm') => (if ! trace_rewrite andalso i < ! depth
1.159 + then writeln((idt"="(i+1))^" rewrites to: "^
1.160 + (term2str ct')) else ();
1.161 + rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
1.162 + | Calc (cc as (op_,_)) =>
1.163 + (let val _= if !trace_rewrite andalso i < ! depth then
1.164 + writeln((idt"#"(i+1))^" try calc: "^op_^"'") else ();
1.165 + val ct = uminus_to_string ct
1.166 + in case get_calculation_ thy cc ct of
1.167 + NONE => ((*writeln "@@@ rewrite__set_: get_calculation_-> NONE";*)
1.168 + rew_once ruls asm ct apno thms)
1.169 + | SOME (thmid, thm') =>
1.170 + let
1.171 + val pairopt =
1.172 + rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
1.173 + ((#erls o rep_rls) rls) put_asm thm' ct;
1.174 + val _ = if pairopt <> NONE then ()
1.175 + else raise error("rewrite_set_, rewrite_ \""^
1.176 + (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
1.177 + val _ = if ! trace_rewrite andalso i < ! depth
1.178 + then writeln((idt"="(i+1))^" calc. to: "^
1.179 + (term2str ((fst o the) pairopt)))
1.180 + else()
1.181 + in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end
1.182 + end)
1.183 +(* use"ProgLang/rewrite.sml";
1.184 + @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.185 + | Cal1 (cc as (op_,_)) =>
1.186 + (let val _= if !trace_rewrite andalso i < ! depth then
1.187 + writeln((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
1.188 + val ct = uminus_to_string ct
1.189 + in case get_calculation1_ thy cc ct of
1.190 + NONE => (ct, asm)
1.191 + | SOME (thmid, thm') =>
1.192 + let
1.193 + val pairopt =
1.194 + rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
1.195 + ((#erls o rep_rls) rls) put_asm thm' ct;
1.196 + val _ = if pairopt <> NONE then ()
1.197 + else raise error("rewrite_set_, rewrite_ \""^
1.198 + (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
1.199 + val _ = if ! trace_rewrite andalso i < ! depth
1.200 + then writeln((idt"="(i+1))^" cal1. to: "^
1.201 + (term2str ((fst o the) pairopt)))
1.202 + else()
1.203 + in the pairopt end
1.204 + end)
1.205 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.206 + | Rls_ rls' =>
1.207 + (case rewrite__set_ thy (i+1) put_asm bdv rls' ct of
1.208 + SOME (t',asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
1.209 + | NONE => rew_once ruls asm ct apno thms);
1.210 +
1.211 + val ruls = (#rules o rep_rls) rls;
1.212 + val _= if ! trace_rewrite andalso i < ! depth
1.213 + then writeln ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^
1.214 + (term2str ct)) else ()
1.215 + val (ct',asm') = rew_once ruls [] ct Noap ruls;
1.216 + in if ct = ct' then NONE else SOME (ct', distinct asm') end
1.217 +
1.218 +and app_rev thy i rrls t =
1.219 + let (*.check a (precond, pattern) of a rev-set; stops with 1st true.*)
1.220 + fun chk_prepat thy erls [] t = true
1.221 + | chk_prepat thy erls prepat t =
1.222 + let fun chk (pres, pat) =
1.223 + (let val subst: Type.tyenv * Envir.tenv =
1.224 + Pattern.match thy (pat, t)
1.225 + (Vartab.empty, Vartab.empty)
1.226 + in snd (eval__true thy (i+1)
1.227 + (map (Envir.subst_term subst) pres)
1.228 + [] erls)
1.229 + end)
1.230 + handle _ => false
1.231 + fun scan_ f [] = false (*scan_ NEVER called by []*)
1.232 + | scan_ f (pp::pps) = if f pp then true
1.233 + else scan_ f pps;
1.234 + in scan_ chk prepat end;
1.235 +
1.236 + (*.apply the normal_form of a rev-set.*)
1.237 + fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
1.238 + if chk_prepat thy erls prepat t
1.239 + then ((*writeln("### app_rev': t = "^(term2str t));*)
1.240 + normal_form t)
1.241 + else NONE;
1.242 +
1.243 + val opt = app_rev' thy rrls t
1.244 + in case opt of
1.245 + SOME (t', asm) => (t', asm, true)
1.246 + | NONE => app_sub thy i rrls t
1.247 + end
1.248 +and app_sub thy i rrls t =
1.249 + ((*writeln("### app_sub: subterm = "^(term2str t));*)
1.250 + case t of
1.251 + Const (s, T) => (Const(s, T), [], false)
1.252 + | Free (s, T) => (Free(s, T), [], false)
1.253 + | Var (n, T) => (Var(n, T), [], false)
1.254 + | Bound i => (Bound i, [], false)
1.255 + | Abs (s, T, body) =>
1.256 + let val (t', asm, rew) = app_rev thy i rrls body
1.257 + in (Abs(s, T, t'), asm, rew) end
1.258 + | t1 $ t2 =>
1.259 + let val (t2', asm2, rew2) = app_rev thy i rrls t2
1.260 + in if rew2 then (t1 $ t2', asm2, true)
1.261 + else let val (t1', asm1, rew1) = app_rev thy i rrls t1
1.262 + in if rew1 then (t1' $ t2, asm1, true)
1.263 + else (t1 $ t2, [], false) end
1.264 + end);
1.265 +
1.266 +
1.267 +
1.268 +(*.rewriting without argument [] for rew_ord.*)
1.269 +(*WN.11.6.03: shouldnt asm<>[] lead to false ????*)
1.270 +fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
1.271 +
1.272 +
1.273 +(*.rewriting without internal argument [] for rew_ord.*)
1.274 +(* val (thy, rew_ord, erls, bool, thm, term) =
1.275 + (thy, (assoc_rew_ord ro), rls', false, (assoc_thm' thy thm'), f);
1.276 + val (thy, rew_ord, erls, bool, thm, term) =
1.277 + (thy, rew_ord, erls, false, thm, t'');
1.278 + *)
1.279 +fun rewrite_ thy rew_ord erls bool thm term =
1.280 + rewrite__ thy 1 [] rew_ord erls bool thm term;
1.281 +fun rewrite_set_ thy bool rls term =
1.282 +(* val (thy, bool, rls, term) = (thy, false, srls, t);
1.283 + *)
1.284 + rewrite__set_ thy 1 bool [] rls term;
1.285 +
1.286 +
1.287 +fun subs'2subst thy (s:subs') =
1.288 + (((map (apfst (term_of o the o (parse thy))))
1.289 + o (map (apsnd (term_of o the o (parse thy))))) s):subst;
1.290 +
1.291 +(*.variants of rewrite.*)
1.292 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst,
1.293 + thus the argument put_asm IS NOT NECESSARY -- FIXME*)
1.294 +(* val (rew_ord,rls,put_asm,thm,ct)=
1.295 + (e_rew_ord,poly_erls,false,num_str d1_isolate_add2,t);
1.296 + *)
1.297 +fun rewrite_inst_ (thy:theory) rew_ord (rls:rls) (put_asm:bool)
1.298 + (subst:(term * term) list) (thm:thm) (ct:term) =
1.299 + rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
1.300 +
1.301 +fun rewrite_set_inst_ (thy:theory)
1.302 + (put_asm:bool) (subst:(term * term) list) (rls:rls) (ct:term) =
1.303 + (*let
1.304 + val subst = subs'2subst thy subs';
1.305 + val subrls = instantiate_rls subs' rls
1.306 + in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct
1.307 + (*end*);
1.308 +
1.309 +(* val (thy, ord, erls, subte, t) = (thy, dummy_ord, Erls, subte, t);
1.310 + *)
1.311 +(*.rewrite using a list of terms.*)
1.312 +fun rewrite_terms_ thy ord erls subte t =
1.313 + let (*val _=writeln("### rewrite_terms_ subte= '"^terms2str subte^"' ..."^
1.314 + term_detail2str (hd subte)^
1.315 + "### rewrite_terms_ t= '"^term2str t^"' ..."^
1.316 + term_detail2str t);*)
1.317 + fun rew_ (t', asm') [] _ = (t', asm')
1.318 + (* 1st val (t', asm', rules as r::rs, t) = (e_term, [], subte, t);
1.319 + 2nd val (t', asm', rules as r::rs, t) = (t'', [], rules, t'');
1.320 + rew_ (t', asm') (r::rs) t;
1.321 + *)
1.322 + | rew_ (t', asm') (rules as r::rs) t =
1.323 + let val _ = writeln("rew_ "^term2str t);
1.324 + val (t'', asm'', lrd, rew) =
1.325 + rew_sub thy 1 [] ord erls false [] r t
1.326 + in if rew
1.327 + then (writeln("true rew_ "^term2str t'');
1.328 + rew_ (t'', asm' @ asm'') rules t'')
1.329 + else (writeln("false rew_ "^term2str t'');
1.330 + rew_ (t', asm') rs t')
1.331 + end
1.332 + val (t'', asm'') = rew_ (e_term, []) subte t
1.333 + in if t'' = e_term
1.334 + then NONE else SOME (t'', asm'')
1.335 + end;
1.336 +
1.337 +
1.338 +(*. search ct for adjacent numerals and calculate them by operator isa_fn .*)
1.339 +fun calculate_ thy isa_fn ct =
1.340 + let val ct = uminus_to_string ct
1.341 + in case get_calculation_ thy isa_fn ct of
1.342 + NONE => NONE
1.343 + | SOME (thmID, thm) =>
1.344 + (let val SOME (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct
1.345 + in SOME (rew,(thmID, thm)) end)
1.346 + handle _ => error ("calculate_: "^thmID^" does not rewrite")
1.347 + end;
1.348 +(*
1.349 +> val thy = InsSort.thy;
1.350 +> val op_ = "le"; (* < *)
1.351 +> val ct = (the o (parse thy))
1.352 + "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])";
1.353 +> calculate_ thy op_ ct;
1.354 + SOME
1.355 + ("foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])",
1.356 + "(#1 < #3) = True") : (cterm * thm) option *)
1.357 +
1.358 +
1.359 +(* for test-printouts:
1.360 +val _ = writeln("in rew_sub : "^( Syntax.string_of_term (thy2ctxt thy) t))
1.361 +val _ = writeln("in eval_true: prems= "^(commas (map (Syntax.string_of_term (thy2ctxt thy)) prems')))
1.362 +*)
1.363 +
1.364 +
1.365 +
1.366 +
1.367 +
1.368 +
1.369 +fun get_rls_scr rs' = ((#scr o rep_rls o #2 o the o assoc') (!ruleset',rs'))
1.370 + handle _ => raise error ("get_rls_scr: no script for "^rs');
1.371 +
1.372 +
1.373 +(*make_thm added to Pure/thm.ML*)
1.374 +fun mk_thm thy str =
1.375 + let val t = (term_of o the o (parse thy)) str
1.376 + val t' = case t of
1.377 + Const ("==>",_) $ _ $ _ => t
1.378 + | _ => Trueprop $ t
1.379 + in make_thm (cterm_of thy t') end;
1.380 +(*
1.381 + val str = "?r ^^^ 2 = ?r * ?r";
1.382 + val thm = realpow_twoI;
1.383 +
1.384 + val t1 = (#prop o rep_thm) (num_str thm);
1.385 + val t2 = Trueprop $ ((term_of o the o (parse thy)) str);
1.386 + t1 = t2;
1.387 +val it = true : bool ... !!!
1.388 + val th1 = (num_str thm);
1.389 + val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
1.390 + th1 = th2;
1.391 +ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
1.392 +
1.393 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.394 + val str = "k ~= 0 ==> m * k / (n * k) = m / n";
1.395 + val thm = real_mult_div_cancel2;
1.396 +
1.397 + val t1 = (#prop o rep_thm) (num_str thm);
1.398 + val t2 = ((term_of o the o (parse thy)) str);
1.399 + t1 = t2;
1.400 +val it = false : bool ... Var .. Free
1.401 + val th1 = (num_str thm);
1.402 + val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
1.403 + th1 = th2;
1.404 +ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
1.405 +*)
1.406 +
1.407 +
1.408 +(*prints subgoal etc.
1.409 +((goal thy);(topthm()) o ) str; *)
1.410 +(*assume rejects scheme variables
1.411 + assume ((cterm_of thy) (Trueprop $
1.412 + (term_of o the o (parse thy)) str)); *)
1.413 +
1.414 +
1.415 +(* outcommented 18.11.xx, xx < 02 -------
1.416 +fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm)
1.417 + | rul2rul' (Calc op_) = Calc' op_;
1.418 +fun rul'2rul thy (Thm'(thmid, ct')) =
1.419 + Thm (thmid, mk_thm thy ct')
1.420 + | rul'2rul thy' (Calc' op_) = Calc op_;
1.421 +
1.422 +
1.423 +fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) =
1.424 + Rls'{preconds'= map string_of_cterm preconds,
1.425 + rew_ord' = fst rew_ord,
1.426 + rules' = map rul2rul' rules}:rlsdat';
1.427 +
1.428 +fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord,
1.429 + rules'=rules}:rlsdat') =
1.430 + let val thy = the (assoc' (theory',thy'))
1.431 + in Rls{preconds = map (the o (parse thy)) preconds,
1.432 + rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))),
1.433 + rules = map (rul'2rul thy) rules}:rls end;
1.434 +------- *)
1.435 +
1.436 +(*.get the theorem associated with the xstring-identifier;
1.437 + if the identifier starts with "sym_" then swap lhs = rhs around =
1.438 + (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
1.439 + identifiers starting with "#" come from Calc and
1.440 + get a hand-made theorem (containing numerals only).*)
1.441 +fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
1.442 + (case explode thmid of
1.443 + "s"::"y"::"m"::"_"::id =>
1.444 + if hd id = "#"
1.445 + then mk_thm thy ct'
1.446 + else ((num_str o (PureThy.get_thm thy)) (implode id)) RS sym
1.447 + | id =>
1.448 + if hd id = "#"
1.449 + then mk_thm thy ct'
1.450 + else (num_str o (PureThy.get_thm thy)) thmid
1.451 + ) handle _ =>
1.452 + raise error ("assoc_thm': '"^thmid^"' not in '"^
1.453 + (theory2domID thy)^"' (and parents)");
1.454 +(*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3");
1.455 +val it = "6 = 2 * 3" : thm
1.456 +
1.457 +> assoc_thm' Isac.thy ("real_add_zero_left","");
1.458 +val it = "0 + ?z = ?z" : thm
1.459 +
1.460 +> assoc_thm' Isac.thy ("sym_real_add_zero_left","");
1.461 +val it = "?t = 0 + ?t" [.] : thm
1.462 +
1.463 +> assoc_thm' HOL.thy ("sym_real_add_zero_left","");
1.464 +*** Unknown theorem(s) "real_add_zero_left"
1.465 +*** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)
1.466 + uncaught exception ERROR*)
1.467 +
1.468 +
1.469 +fun parse' (thy:theory') (ct:cterm') =
1.470 + case parse ((the o assoc')(!theory',thy)) ct of
1.471 + NONE => NONE
1.472 + | SOME ct => SOME ((term2str (term_of ct)):cterm');
1.473 +
1.474 +
1.475 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
1.476 + thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
1.477 +fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls')
1.478 + (put_asm:bool) (thm:thm') (ct:cterm') =
1.479 +(* val (rew_ord, rls, thm, ct) = (rew_ord', id_rls rls', thm', f);
1.480 + *)
1.481 + let val thy = (the o assoc')(!theory',thy');
1.482 + in
1.483 + case rewrite_ thy
1.484 + ((the o assoc')(!rew_ord',rew_ord))((#2 o the o assoc')(!ruleset',rls))
1.485 + put_asm ((assoc_thm' thy) thm)
1.486 + ((term_of o the o (parse thy)) ct) of
1.487 + NONE => NONE
1.488 + | SOME (t, ts) => SOME (term2str t, terms2str ts)
1.489 + end;
1.490 +
1.491 +(*
1.492 +val thy = "RatArith.thy";
1.493 +val rew_ord = "dummy_ord";
1.494 +> val rls = "eval_rls";
1.495 +val put_asm = true;
1.496 +val thm = ("square_equation_left","");
1.497 +val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
1.498 +
1.499 +val Zthy = ((the o assoc')(!theory',thy));
1.500 +val Zrew_ord = ((the o assoc')(!rew_ord',rew_ord));
1.501 +val Zrls = ((the o assoc')(!ruleset',rls));
1.502 +val Zput_asm = put_asm;
1.503 +val Zthm = ((the o (assoc'_thm' thy)) thm);
1.504 +val Zct = ((the o (parse ((the o assoc')(!theory',thy)))) ct);
1.505 +
1.506 +rewrite_ Zthy Zrew_ord Zrls Zput_asm Zthm Zct;
1.507 +
1.508 + use"Isa99/interface_ME_ISA.sml";
1.509 +*)
1.510 +
1.511 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
1.512 + thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
1.513 +fun rewrite_set (thy':theory') (put_asm:bool)
1.514 + (rls:rls') (ct:cterm') =
1.515 + let val thy = (the o assoc')(!theory',thy');
1.516 + in
1.517 + case rewrite_set_ thy put_asm ((#2 o the o assoc')(!ruleset',rls))
1.518 + ((term_of o the o (parse thy)) ct) of
1.519 + NONE => NONE
1.520 + | SOME (t, ts) => SOME (term2str t, terms2str ts)
1.521 + end;
1.522 +
1.523 +(*evaluate list-expressions
1.524 + should work on term, and stand in Isa99/rewrite-parse.sml,
1.525 + but there list_rls <- eval_binop is not yet defined*)
1.526 +(*fun eval_listexpr' ct =
1.527 + let val rew = rewrite_set "ListC.thy" false "list_rls" ct;
1.528 + in case rew of
1.529 + SOME (res,_) => res
1.530 + | NONE => ct end;-----------------30.9.02---*)
1.531 +fun eval_listexpr_ thy srls t =
1.532 +(* val (thy, srls, t) =
1.533 + ((assoc_thy th), sr, (subst_atomic (upd_env_opt E (a,v)) t));
1.534 + *)
1.535 + let val rew = rewrite_set_ thy false srls t;
1.536 + in case rew of
1.537 + SOME (res,_) => res
1.538 + | NONE => t end;
1.539 +
1.540 +
1.541 +fun get_calculation' (thy:theory') op_ (ct:cterm') =
1.542 + case get_calculation_ ((the o assoc')(!theory',thy)) op_
1.543 + ((uminus_to_string o term_of o the o
1.544 + (parse ((the o assoc')(!theory',thy)))) ct) of
1.545 + NONE => NONE
1.546 + | SOME (thmid, thm) =>
1.547 + SOME ((thmid, string_of_thmI thm):thm');
1.548 +
1.549 +fun calculate (thy':theory') op_ (ct:cterm') =
1.550 + let val thy = (the o assoc')(!theory',thy');
1.551 + in
1.552 + case calculate_ thy op_
1.553 + ((term_of o the o (parse thy)) ct) of
1.554 + NONE => NONE
1.555 + | SOME (ct,(thmID,thm)) =>
1.556 + SOME (term2str ct,
1.557 + (thmID, string_of_thmI thm):thm')
1.558 + end;
1.559 +(*
1.560 +fun instantiate'' thy' subs ((thmid,ct'):thm') =
1.561 + let val thmid_ = implode ("#"::(explode thmid)) (*see type thm'*)
1.562 + in (thmid_, (string_of_thmI o (read_instantiate subs))
1.563 + ((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end;
1.564 +
1.565 +fun instantiate_rls' thy' subs (rls:rls') =
1.566 + rls2rls' (instantiate_rls subs ((the o (assoc_rls thy')) rls)):rlsdat';
1.567 +
1.568 +... problem with these functions:
1.569 +> val thm = mk_thm thy "(bdv + a = b) = (bdv = b - a)";
1.570 +val thm = "(bdv + a = b) = (bdv = b - a)" : thm
1.571 +> show_types:=true; thm;
1.572 +val it = "((bdv::'a) + (a::'a) = (b::'a)) = (bdv = b - a)" : thm
1.573 +... and this doesn't match because of too general typing (?!)
1.574 + and read_insitantiate doesn't instantiate the types (?!)
1.575 +=== solutions:
1.576 +(1) hard-coded type-instantiation ("'a", "RatArith.rat")
1.577 +(2) instantiate', instantiate ... no help by isabelle-users@ !!!
1.578 +=== conclusion:
1.579 + rewrite_inst, rewrite_set_inst circumvent the problem,
1.580 + according functions out-commented with 'instantiate''
1.581 +*)
1.582 +
1.583 +(* instantiate''
1.584 +fun instantiate'' thy' subs ((thmid,ct'):thm') =
1.585 + let
1.586 + val thmid_ = implode ("#"::(explode thmid)); (*see type thm'*)
1.587 + val thy = (the o assoc')(!theory',thy');
1.588 + val typs = map (#T o rep_cterm o the o (parse thy))
1.589 + ((snd o split_list) subs);
1.590 + val ctyps = map
1.591 + ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o (parse thy))
1.592 + ((snd o split_list) subs);
1.593 +
1.594 +> val thy' = "RatArith.thy";
1.595 +> val subs = [("bdv","x::rat"),("zzz","z::nat")];
1.596 +> (the o (parse ((the o assoc')(!theory',thy')))) "x::rat";
1.597 +> (#T o rep_cterm o the o (parse ((the o assoc')(!theory',thy'))));
1.598 +
1.599 +> val ctyp = ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o
1.600 + (parse ((the o assoc')(!theory',thy')))) "x::rat";
1.601 +> val bdv = (the o (parse thy)) "bdv";
1.602 +> val x = (the o (parse thy)) "x";
1.603 +> (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
1.604 + handle e => print_exn e;
1.605 +uncaught exception THM
1.606 + raised at: thm.ML:1085.18-1085.69
1.607 + thm.ML:1092.34
1.608 + goals.ML:536.61
1.609 +
1.610 +> val bdv = (the o (parse thy)) "bdv::nat";
1.611 +> val x = (the o (parse thy)) "x::nat";
1.612 +> (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
1.613 + handle e => print_exn e;
1.614 +uncaught exception THM
1.615 + raised at: thm.ML:1085.18-1085.69
1.616 + thm.ML:1092.34
1.617 + goals.ML:536.61
1.618 +
1.619 +> (instantiate' [SOME ctyp] [] isolate_bdv_add)
1.620 + handle e => print_exn e;
1.621 +uncaught exception TYPE
1.622 + raised at: drule.ML:613.13-615.44
1.623 + goals.ML:536.61
1.624 +
1.625 +> val repct = (rep_cterm o the o (parse ((the o assoc')(!theory',thy')))) "x::rat";
1.626 +*)
1.627 +
1.628 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
1.629 + thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
1.630 +fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls')
1.631 + (put_asm:bool) subs (thm:thm') (ct:cterm') =
1.632 + let
1.633 + val thy = (the o assoc')(!theory',thy');
1.634 + val thm = assoc_thm' thy thm; (*28.10.02*)
1.635 + (*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*)
1.636 + in
1.637 + case rewrite_ thy
1.638 + ((the o assoc')(!rew_ord',rew_ord)) ((#2 o the o assoc')(!ruleset',rls))
1.639 + put_asm (*sub*)thm ((term_of o the o (parse thy)) ct) of
1.640 + NONE => NONE
1.641 + | SOME (ctm, ctms) =>
1.642 + SOME ((term2str ctm):cterm', (map term2str ctms):cterm' list)
1.643 + end;
1.644 +
1.645 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
1.646 + thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
1.647 +fun rewrite_set_inst (thy':theory') (put_asm:bool)
1.648 + subs' (rls:rls') (ct:cterm') =
1.649 + let
1.650 + val thy = (the o assoc')(!theory',thy');
1.651 + val rls = assoc_rls rls
1.652 + val subst = subs'2subst thy subs'
1.653 + (*val subrls = instantiate_rls subs ((the o assoc')(!ruleset',rls))*)
1.654 + in case rewrite_set_inst_ thy put_asm subst (*sub*)rls
1.655 + ((term_of o the o (parse thy)) ct) of
1.656 + NONE => NONE
1.657 + | SOME (t, ts) => SOME (term2str t, terms2str ts)
1.658 + end;
1.659 +
1.660 +
1.661 +(*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *)
1.662 +fun eval_true' (thy':theory') (rls':rls') (Const ("True",_)) = true
1.663 +
1.664 + | eval_true' (thy':theory') (rls':rls') (t:term) =
1.665 +(* val thy'="Isac.thy"; val rls'="eval_rls"; val t=hd pres';
1.666 + *)
1.667 + let val ct' = term2str t;
1.668 + in case rewrite_set thy' false rls' ct' of
1.669 + SOME ("True",_) => true
1.670 + | _ => false
1.671 + end;
1.672 +fun eval_true_ _ _ (Const ("True",_)) = true
1.673 + | eval_true_ (thy':theory') rls t =
1.674 + case rewrite_set_ (assoc_thy thy') false rls t of
1.675 + SOME (Const ("True",_),_) => true
1.676 + | _ => false;
1.677 +
1.678 +(*
1.679 +val test_rls =
1.680 + Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right),
1.681 + rules = [Calc ("matches",eval_matches "")
1.682 + ],
1.683 + scr = Script ((term_of o the o (parse thy))
1.684 + "empty_script")
1.685 + }:rls;
1.686 +
1.687 +
1.688 +
1.689 + rewrite_set_ Isac.thy eval_rls false test_rls
1.690 + ((the o (parse thy)) "matches (?a = ?b) (x = #0)");
1.691 + val xxx = (term_of o the o (parse thy))
1.692 + "matches (?a = ?b) (x = #0)";
1.693 + eval_matches """" xxx thy;
1.694 +SOME ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True",
1.695 + Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
1.696 +
1.697 +
1.698 +
1.699 + rewrite_set_ Isac.thy eval_rls false eval_rls
1.700 + ((the o (parse thy)) "contains_root (sqrt #0)");
1.701 +val it = SOME ("True",[]) : (cterm * cterm list) option
1.702 +
1.703 +*)
1.704 +
1.705 +
1.706 +(*----------WN:16.5.03 stuff below considered illdesigned, thus coded from scratch in appl.sml fun check_elementwise
1.707 +datatype det = TRUE | FALSE | INDET;(*FIXXME.WN:16.5.03
1.708 + introduced with quick-and-dirty code*)
1.709 +fun determine dts =
1.710 + let val false_indet =
1.711 + filter_out ((curry op= TRUE) o (#1:det * term -> det)) dts
1.712 + val ts = map (#2: det * term -> term) dts
1.713 + in if nil = false_indet then (TRUE, ts)
1.714 + else if nil = filter ((curry op= FALSE) o (#1:det * term -> det))
1.715 + false_indet
1.716 + then (INDET, ts)
1.717 + else (FALSE, ts) end;
1.718 +(* val dts = [(INDET,e_term), (FALSE,HOLogic.false_const),
1.719 + (INDET,e_term), (TRUE,HOLogic.true_const)];
1.720 + determine dts;
1.721 +val it =
1.722 + (FALSE,
1.723 + [Const ("empty","'a"),Const ("False","bool"),Const ("empty","'a"),
1.724 + Const ("True","bool")]) : det * term list*)
1.725 +
1.726 +fun eval__indet_ thy cs rls = (*FIXXME.WN:16.5.03 pull into eval__true_, update check (check_elementwise), and regard eval_true_ + eval_true*)
1.727 +if cs = [HOLogic.true_const] orelse cs = [] then (TRUE, [])
1.728 + else if cs = [HOLogic.false_const] then (FALSE, cs)
1.729 + else
1.730 + let fun eval t =
1.731 + let val taopt = rewrite__set_ thy 1 false [] rls t
1.732 + in case taopt of
1.733 + SOME (t,_) =>
1.734 + if t = HOLogic.true_const then (TRUE, t)
1.735 + else if t = HOLogic.false_const then (FALSE, t)
1.736 + else (INDET, t)
1.737 + | NONE => (INDET, t) end
1.738 + in (determine o (map eval)) cs end;
1.739 +WN.16.5.0-------------------------------------------------------------*)