wneuper/isa: comparison src/Tools/isac/ProgLang/rewrite.sml

equal deleted inserted replaced

-:0831a4a6ec8a
+:c3f399ce32af
 *)
 exception NO_REWRITE;
 exception STOP_REW_SUB; (*WN050820 quick and dirty*)
+fun trace i str =
+if ! trace_rewrite andalso i < ! depth then tracing (idt "#" i ^ str) else ()
+fun trace1 i str =
+if ! trace_rewrite andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
 (*
 Synopsis rewriting (prep for reference manual):
 ----------------------------------------------
 Rewriting uses theorems for transforming terms. However, not all kinds
 	  end)
 (* simplify asumptions until one evaluates to false, store intermined's (x~=0)*)
 and eval__true thy i asms bdv rls =
 if asms = [@{term True}] orelse asms = [] then ([], true)
 (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
-else if asms = [@{term False}] then ([], false)
+else if asms = [@{term False}] then ([], false) else
-else
 let
 fun chk indets [] = (indets, true)(*return asms<>True until false*)
 | chk indets (a::asms) =
-(case rewrite__set_ thy (i+1) false bdv rls a of
+(case rewrite__set_ thy (i + 1) false bdv rls a of
 NONE => (chk (indets @ [a]) asms)
 | SOME (t, a') =>
 if t = @{term True} then (chk (indets @ a') asms)
 else if t = @{term False} then ([], false)
 (*asm false .. thm not applied ^^^; continue until False vvv*)
 else chk (indets @ [t] @ a') asms);
 in chk [] asms end
 (* rewrite with a rule set, which must not be the empty Erls *)
 and rewrite__set_ _ _ __ Erls t =
-error("rewrite__set_ called with 'Erls' for '"^term2str t^"'")
+error ("rewrite__set_ called with 'Erls' for '" ^ term2str t ^ "'")
 (* rewrite with a 'reverse rule set' implemented by ML code *)
 | rewrite__set_ thy i _ _ (rrls as Rrls _) t =
-let val _= if ! trace_rewrite andalso i < ! depth
+let
-	       then tracing ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^
+val _= trace i (" rls: " ^ id_rls rrls ^ " on: " ^ term2str t)
-			     (term2str t)) else ()
+	    val (t', asm, rew) = app_rev thy (i + 1) rrls t
-	val (t', asm, rew) = app_rev thy (i+1) rrls t
+in if rew then SOME (t', distinct asm) else NONE end
-in if rew then SOME (t', distinct asm)
-else NONE end
 (* rewrite with a rule set containing Thms or Calculations *)
 | rewrite__set_ thy i put_asm bdv rls ct =
-(* val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
+let
-*)
+datatype switch = Appl | Noap;
-let
+fun rew_once ruls asm ct Noap [] = (ct, asm)
-datatype switch = Appl | Noap;
+| rew_once ruls asm ct Appl [] =
-fun rew_once ruls asm ct Noap [] = (ct,asm)
+(case rls of Rls _ => rew_once ruls asm ct Noap ruls
-| rew_once ruls asm ct Appl [] =
+| Seq _ => (ct, asm))
-	(case rls of Rls _ => rew_once ruls asm ct Noap ruls
+| rew_once ruls asm ct apno (rul::thms) =
-		   | Seq _ => (ct,asm))
+case rul of
-| rew_once ruls asm ct apno (rul::thms) =
+Thm (thmid, thm) =>
-(* val (ruls, asm, ct, apno, (rul::thms)) = (ruls, [], ct, Noap, ruls);
+(trace1 i (" try thm: " ^ thmid);
-val Thm (thmid, thm) = rul;
+case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
-*)
+((#erls o rep_rls) rls) put_asm thm ct of
-case rul of
+NONE => rew_once ruls asm ct apno thms
-	Thm (thmid, thm) =>
+| SOME (ct',asm') =>
-	  (if !trace_rewrite andalso i < ! depth
+(trace1 i (" rewrites to: " ^ term2str ct');
-	   then tracing((idt"#"(i+1))^" try thm: "^thmid) else ();
+rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
-	   case rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
+| Calc (cc as (op_, _)) =>
-	     ((#erls o rep_rls) rls) put_asm thm ct of
+let val _= trace1 i (" try calc: " ^ op_ ^ "'")
-	     NONE => rew_once ruls asm ct apno thms
+val ct = uminus_to_string ct
-	   | SOME (ct',asm') => (if ! trace_rewrite andalso i < ! depth
+in case get_calculation_ thy cc ct of
-	     then tracing((idt"="(i+1))^" rewrites to: "^
+NONE => rew_once ruls asm ct apno thms
-			  (term2str ct')) else ();
+| SOME (thmid, thm') =>
-	       rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
+let
-| Calc (cc as (op_,_)) =>
+val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
-	  (let val _= if !trace_rewrite andalso i < ! depth then
+((#erls o rep_rls) rls) put_asm thm' ct;
-		      tracing((idt"#"(i+1))^" try calc: "^op_^"'") else ();
+val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
-	     val ct = uminus_to_string ct
+string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE")
-	   in case get_calculation_ thy cc ct of
+val _ = trace1 i (" calc. to: " ^ term2str ((fst o the) pairopt))
-	     NONE => rew_once ruls asm ct apno thms
+in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
-	   | SOME (thmid, thm') =>
+end
-	       let
+| Cal1 (cc as (op_, _)) =>
-		 val pairopt =
+let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
-		   rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
+val ct = uminus_to_string ct
-		   ((#erls o rep_rls) rls) put_asm thm' ct;
+in case get_calculation1_ thy cc ct of
-		 val _ = if pairopt <> NONE then ()
+NONE => (ct, asm)
-			 else error("rewrite_set_, rewrite_ \""^
+| SOME (thmid, thm') =>
-			 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
+let
-		 val _ = if ! trace_rewrite andalso i < ! depth
+val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
-			   then tracing((idt"="(i+1))^" calc. to: "^
+((#erls o rep_rls) rls) put_asm thm' ct;
-					(term2str ((fst o the) pairopt)))
+val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
-			 else()
+string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE")
-	       in rew_once ruls asm ((fst o the) pairopt) Appl (rul::thms) end
+val _ = trace1 i (" cal1. to: " ^ term2str ((fst o the) pairopt))
-	   end)
+in the pairopt end
-| Cal1 (cc as (op_,_)) =>
+end
-	  (let val _= if !trace_rewrite andalso i < ! depth then
+| Rls_ rls' =>
-		      tracing((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
+(case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
-	     val ct = uminus_to_string ct
+SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
-	   in case get_calculation1_ thy cc ct of
+| NONE => rew_once ruls asm ct apno thms);
-	     NONE => (ct, asm)
+val ruls = (#rules o rep_rls) rls;
-	   | SOME (thmid, thm') =>
+val _= trace i (" rls: " ^ id_rls rls ^ " on: " ^ term2str ct)
-	       let
+val (ct', asm') = rew_once ruls [] ct Noap ruls;
-		 val pairopt =
+	  in if ct = ct' then NONE else SOME (ct', distinct asm') end
-		   rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
-		   ((#erls o rep_rls) rls) put_asm thm' ct;
-		 val _ = if pairopt <> NONE then ()
-			 else error("rewrite_set_, rewrite_ \""^
-			 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
-		 val _ = if ! trace_rewrite andalso i < ! depth
-			   then tracing((idt"="(i+1))^" cal1. to: "^
-					(term2str ((fst o the) pairopt)))
-			 else()
-	       in the pairopt end
-	   end)
-| Rls_ rls' =>
-	(case rewrite__set_ thy (i+1) put_asm bdv rls' ct of
-	     SOME (t',asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
-	   | NONE => rew_once ruls asm ct apno thms);
-val ruls = (#rules o rep_rls) rls;
-val _= if ! trace_rewrite andalso i < ! depth
-	   then tracing ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^
-			 (term2str ct)) else ()
-val (ct',asm') = rew_once ruls [] ct Noap ruls;
-in if ct = ct' then NONE else SOME (ct', distinct asm') end
 (* apply an Rrls; if not applicable proceed with subterms *)
 and app_rev thy i rrls t =
 let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
 fun chk_prepat thy erls [] t = true
 fun scan_ f [] = false (*scan_ NEVER called by []*)
 | scan_ f (pp::pps) =
 if f pp then true else scan_ f pps;
 in scan_ chk prepat end;
 (* apply the normal_form of a rev-set *)
-fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
+fun app_rev' thy (Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...}) t =
 if chk_prepat thy erls prepat t
 then ((*tracing("### app_rev': t = "^(term2str t));*) normal_form t)
 else NONE;
 val opt = app_rev' thy rrls t
 in
 (*.rewriting without argument [] for rew_ord.*)
 (*WN.11.6.03: shouldnt asm<>[] lead to false ????*)
 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
+(* rewriting without internal argument [] *)
-(*.rewriting without internal argument [] for rew_ord.*)
+fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
-(* val (thy, rew_ord, erls, bool, thm, term) =
+fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
-(thy, (assoc_rew_ord ro), rls', false, (assoc_thm' thy thm'), f);
-val (thy, rew_ord, erls, bool, thm, term) =
-(thy, rew_ord, erls, false, thm, t'');
-*)
-fun rewrite_ thy rew_ord erls bool thm term =
-rewrite__ thy 1 [] rew_ord erls bool thm term;
-fun rewrite_set_ thy bool rls term =
-(* val (thy, bool, rls, term) = (thy, false, srls, t);
-*)
-rewrite__set_ thy 1 bool [] rls term;
 fun subs'2subst thy (s:subs') =
 (((map (apfst (term_of o the o (parse thy))))
 o (map (apsnd (term_of o the o (parse thy))))) s):subst;

changeset 52101	c3f399ce32af
parent 52085	39f0a7b9b054
child 52105	2786cc9704c8