1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Mon Sep 02 15:17:34 2013 +0200
1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Mon Sep 02 16:16:08 2013 +0200
1.3 @@ -9,6 +9,11 @@
1.4 exception NO_REWRITE;
1.5 exception STOP_REW_SUB; (*WN050820 quick and dirty*)
1.6
1.7 +fun trace i str =
1.8 + if ! trace_rewrite andalso i < ! depth then tracing (idt "#" i ^ str) else ()
1.9 +fun trace1 i str =
1.10 + if ! trace_rewrite andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
1.11 +
1.12 (*
1.13 Synopsis rewriting (prep for reference manual):
1.14 ----------------------------------------------
1.15 @@ -114,12 +119,11 @@
1.16 and eval__true thy i asms bdv rls =
1.17 if asms = [@{term True}] orelse asms = [] then ([], true)
1.18 (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
1.19 - else if asms = [@{term False}] then ([], false)
1.20 - else
1.21 + else if asms = [@{term False}] then ([], false) else
1.22 let
1.23 fun chk indets [] = (indets, true)(*return asms<>True until false*)
1.24 | chk indets (a::asms) =
1.25 - (case rewrite__set_ thy (i+1) false bdv rls a of
1.26 + (case rewrite__set_ thy (i + 1) false bdv rls a of
1.27 NONE => (chk (indets @ [a]) asms)
1.28 | SOME (t, a') =>
1.29 if t = @{term True} then (chk (indets @ a') asms)
1.30 @@ -129,91 +133,67 @@
1.31 in chk [] asms end
1.32 (* rewrite with a rule set, which must not be the empty Erls *)
1.33 and rewrite__set_ _ _ __ Erls t =
1.34 - error("rewrite__set_ called with 'Erls' for '"^term2str t^"'")
1.35 + error ("rewrite__set_ called with 'Erls' for '" ^ term2str t ^ "'")
1.36 (* rewrite with a 'reverse rule set' implemented by ML code *)
1.37 | rewrite__set_ thy i _ _ (rrls as Rrls _) t =
1.38 - let val _= if ! trace_rewrite andalso i < ! depth
1.39 - then tracing ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^
1.40 - (term2str t)) else ()
1.41 - val (t', asm, rew) = app_rev thy (i+1) rrls t
1.42 - in if rew then SOME (t', distinct asm)
1.43 - else NONE end
1.44 + let
1.45 + val _= trace i (" rls: " ^ id_rls rrls ^ " on: " ^ term2str t)
1.46 + val (t', asm, rew) = app_rev thy (i + 1) rrls t
1.47 + in if rew then SOME (t', distinct asm) else NONE end
1.48 (* rewrite with a rule set containing Thms or Calculations *)
1.49 | rewrite__set_ thy i put_asm bdv rls ct =
1.50 -(* val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
1.51 - *)
1.52 - let
1.53 - datatype switch = Appl | Noap;
1.54 - fun rew_once ruls asm ct Noap [] = (ct,asm)
1.55 - | rew_once ruls asm ct Appl [] =
1.56 - (case rls of Rls _ => rew_once ruls asm ct Noap ruls
1.57 - | Seq _ => (ct,asm))
1.58 - | rew_once ruls asm ct apno (rul::thms) =
1.59 -(* val (ruls, asm, ct, apno, (rul::thms)) = (ruls, [], ct, Noap, ruls);
1.60 - val Thm (thmid, thm) = rul;
1.61 - *)
1.62 - case rul of
1.63 - Thm (thmid, thm) =>
1.64 - (if !trace_rewrite andalso i < ! depth
1.65 - then tracing((idt"#"(i+1))^" try thm: "^thmid) else ();
1.66 - case rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
1.67 - ((#erls o rep_rls) rls) put_asm thm ct of
1.68 - NONE => rew_once ruls asm ct apno thms
1.69 - | SOME (ct',asm') => (if ! trace_rewrite andalso i < ! depth
1.70 - then tracing((idt"="(i+1))^" rewrites to: "^
1.71 - (term2str ct')) else ();
1.72 - rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
1.73 - | Calc (cc as (op_,_)) =>
1.74 - (let val _= if !trace_rewrite andalso i < ! depth then
1.75 - tracing((idt"#"(i+1))^" try calc: "^op_^"'") else ();
1.76 - val ct = uminus_to_string ct
1.77 - in case get_calculation_ thy cc ct of
1.78 - NONE => rew_once ruls asm ct apno thms
1.79 - | SOME (thmid, thm') =>
1.80 - let
1.81 - val pairopt =
1.82 - rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
1.83 - ((#erls o rep_rls) rls) put_asm thm' ct;
1.84 - val _ = if pairopt <> NONE then ()
1.85 - else error("rewrite_set_, rewrite_ \""^
1.86 - (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
1.87 - val _ = if ! trace_rewrite andalso i < ! depth
1.88 - then tracing((idt"="(i+1))^" calc. to: "^
1.89 - (term2str ((fst o the) pairopt)))
1.90 - else()
1.91 - in rew_once ruls asm ((fst o the) pairopt) Appl (rul::thms) end
1.92 - end)
1.93 - | Cal1 (cc as (op_,_)) =>
1.94 - (let val _= if !trace_rewrite andalso i < ! depth then
1.95 - tracing((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
1.96 - val ct = uminus_to_string ct
1.97 - in case get_calculation1_ thy cc ct of
1.98 - NONE => (ct, asm)
1.99 - | SOME (thmid, thm') =>
1.100 - let
1.101 - val pairopt =
1.102 - rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
1.103 - ((#erls o rep_rls) rls) put_asm thm' ct;
1.104 - val _ = if pairopt <> NONE then ()
1.105 - else error("rewrite_set_, rewrite_ \""^
1.106 - (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
1.107 - val _ = if ! trace_rewrite andalso i < ! depth
1.108 - then tracing((idt"="(i+1))^" cal1. to: "^
1.109 - (term2str ((fst o the) pairopt)))
1.110 - else()
1.111 - in the pairopt end
1.112 - end)
1.113 - | Rls_ rls' =>
1.114 - (case rewrite__set_ thy (i+1) put_asm bdv rls' ct of
1.115 - SOME (t',asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
1.116 - | NONE => rew_once ruls asm ct apno thms);
1.117 -
1.118 - val ruls = (#rules o rep_rls) rls;
1.119 - val _= if ! trace_rewrite andalso i < ! depth
1.120 - then tracing ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^
1.121 - (term2str ct)) else ()
1.122 - val (ct',asm') = rew_once ruls [] ct Noap ruls;
1.123 - in if ct = ct' then NONE else SOME (ct', distinct asm') end
1.124 + let
1.125 + datatype switch = Appl | Noap;
1.126 + fun rew_once ruls asm ct Noap [] = (ct, asm)
1.127 + | rew_once ruls asm ct Appl [] =
1.128 + (case rls of Rls _ => rew_once ruls asm ct Noap ruls
1.129 + | Seq _ => (ct, asm))
1.130 + | rew_once ruls asm ct apno (rul::thms) =
1.131 + case rul of
1.132 + Thm (thmid, thm) =>
1.133 + (trace1 i (" try thm: " ^ thmid);
1.134 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
1.135 + ((#erls o rep_rls) rls) put_asm thm ct of
1.136 + NONE => rew_once ruls asm ct apno thms
1.137 + | SOME (ct',asm') =>
1.138 + (trace1 i (" rewrites to: " ^ term2str ct');
1.139 + rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
1.140 + | Calc (cc as (op_, _)) =>
1.141 + let val _= trace1 i (" try calc: " ^ op_ ^ "'")
1.142 + val ct = uminus_to_string ct
1.143 + in case get_calculation_ thy cc ct of
1.144 + NONE => rew_once ruls asm ct apno thms
1.145 + | SOME (thmid, thm') =>
1.146 + let
1.147 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
1.148 + ((#erls o rep_rls) rls) put_asm thm' ct;
1.149 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.150 + string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE")
1.151 + val _ = trace1 i (" calc. to: " ^ term2str ((fst o the) pairopt))
1.152 + in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
1.153 + end
1.154 + | Cal1 (cc as (op_, _)) =>
1.155 + let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
1.156 + val ct = uminus_to_string ct
1.157 + in case get_calculation1_ thy cc ct of
1.158 + NONE => (ct, asm)
1.159 + | SOME (thmid, thm') =>
1.160 + let
1.161 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
1.162 + ((#erls o rep_rls) rls) put_asm thm' ct;
1.163 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
1.164 + string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE")
1.165 + val _ = trace1 i (" cal1. to: " ^ term2str ((fst o the) pairopt))
1.166 + in the pairopt end
1.167 + end
1.168 + | Rls_ rls' =>
1.169 + (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
1.170 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
1.171 + | NONE => rew_once ruls asm ct apno thms);
1.172 + val ruls = (#rules o rep_rls) rls;
1.173 + val _= trace i (" rls: " ^ id_rls rls ^ " on: " ^ term2str ct)
1.174 + val (ct', asm') = rew_once ruls [] ct Noap ruls;
1.175 + in if ct = ct' then NONE else SOME (ct', distinct asm') end
1.176
1.177 (* apply an Rrls; if not applicable proceed with subterms *)
1.178 and app_rev thy i rrls t =
1.179 @@ -233,7 +213,7 @@
1.180 if f pp then true else scan_ f pps;
1.181 in scan_ chk prepat end;
1.182 (* apply the normal_form of a rev-set *)
1.183 - fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
1.184 + fun app_rev' thy (Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...}) t =
1.185 if chk_prepat thy erls prepat t
1.186 then ((*tracing("### app_rev': t = "^(term2str t));*) normal_form t)
1.187 else NONE;
1.188 @@ -272,20 +252,9 @@
1.189 (*WN.11.6.03: shouldnt asm<>[] lead to false ????*)
1.190 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
1.191
1.192 -
1.193 -(*.rewriting without internal argument [] for rew_ord.*)
1.194 -(* val (thy, rew_ord, erls, bool, thm, term) =
1.195 - (thy, (assoc_rew_ord ro), rls', false, (assoc_thm' thy thm'), f);
1.196 - val (thy, rew_ord, erls, bool, thm, term) =
1.197 - (thy, rew_ord, erls, false, thm, t'');
1.198 - *)
1.199 -fun rewrite_ thy rew_ord erls bool thm term =
1.200 - rewrite__ thy 1 [] rew_ord erls bool thm term;
1.201 -fun rewrite_set_ thy bool rls term =
1.202 -(* val (thy, bool, rls, term) = (thy, false, srls, t);
1.203 - *)
1.204 - rewrite__set_ thy 1 bool [] rls term;
1.205 -
1.206 +(* rewriting without internal argument [] *)
1.207 +fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
1.208 +fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
1.209
1.210 fun subs'2subst thy (s:subs') =
1.211 (((map (apfst (term_of o the o (parse thy))))