1.1 --- a/src/sml/ROOT.ML Sat Aug 20 15:15:41 2005 +0200
1.2 +++ b/src/sml/ROOT.ML Sat Aug 20 18:04:54 2005 +0200
1.3 @@ -124,9 +124,9 @@
1.4 cd"smltest/ME";
1.5 use"modspec.sml";
1.6 cd "../..";
1.7 -cd"smltest/xmlsrc";
1.8 - (*use".sml";*)
1.9 - cd "../..";
1.10 +(*cd"smltest/xmlsrc";
1.11 + use".sml";
1.12 + cd "../.."; *)
1.13 cd"smltest/FE-interface";
1.14 use"interface.sml";
1.15 cd "../..";
2.1 --- a/src/sml/Scripts/rewrite.sml Sat Aug 20 15:15:41 2005 +0200
2.2 +++ b/src/sml/Scripts/rewrite.sml Sat Aug 20 18:04:54 2005 +0200
2.3 @@ -1,11 +1,12 @@
2.4 (* isac's rewriter
2.5 - (c) Walther Neuper 1999
2.6 + (c) Walther Neuper 2000
2.7
2.8 use"~/proto2/isac/src/sml/Scripts/rewrite.sml";
2.9 *)
2.10
2.11
2.12 exception NO_REWRITE;
2.13 +exception STOP_REW_SUB; (*WN050820 quick and dirty*)
2.14
2.15 (*17.6.00: rewrite by going down the term with rew_sub*)
2.16 (* val (bdv,tless)=(subst,rew_ord);
2.17 @@ -25,11 +26,11 @@
2.18 val t4 = (norm o #prop o rep_thm) thm4;
2.19 *)
2.20 and rew_sub thy i bdv tless rls put_asm r t =
2.21 - (let (* from Pure/thm.ML: fun rewritec *)
2.22 + ((let (* copy from Pure/thm.ML: fun rewritec *)
2.23 val (lhs,rhs) = (dest_equals' o strip_trueprop
2.24 o Logic.strip_imp_concl) r;
2.25 - (*val _=writeln("@@@ rew_sub: t= "^(term2str t));
2.26 - val _=writeln("@@@ rew_sub: lhs= "^(term2str lhs));*)
2.27 + (*val _=writeln("1.. rew_sub: t= "^(term2str t));
2.28 + val _=writeln("2.. rew_sub: lhs= "^(term2str lhs));*)
2.29 val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs,t);
2.30 (*TODOtest: (-"-) handle _ => raise NO_REWRITE; 12.8.02 ???*)
2.31 (*val _=writeln("@@@ rew_sub: Pattern.match (lhs,t) ");*)
2.32 @@ -41,8 +42,8 @@
2.33 val _= if ! trace_rewrite andalso i < ! depth andalso p' <> []
2.34 then writeln((idt"#"(i+1))^" eval asms: "^(term2str r')) else();
2.35 val (t'',p'') =
2.36 - let val (simpl_p', bool) = eval__true thy (i+1) p' bdv rls
2.37 - in if bool
2.38 + let val (simpl_p', nofalse) = eval__true thy (i+1) p' bdv rls
2.39 + in if nofalse
2.40 then (if ! trace_rewrite andalso i < ! depth andalso p' <> []
2.41 then writeln((idt"#"(i+1))^" asms accepted: "^(terms2str p')^
2.42 " stored: "^(terms2str simpl_p'))
2.43 @@ -50,7 +51,7 @@
2.44 else
2.45 (if ! trace_rewrite andalso i < ! depth
2.46 then writeln((idt"#"(i+1))^" asms false: "^(terms2str p'))
2.47 - else(); raise NO_REWRITE)
2.48 + else(); raise STOP_REW_SUB)
2.49 end
2.50 in if perm lhs rhs andalso not (tless bdv (t',t))
2.51 then (if ! trace_rewrite andalso i < ! depth
2.52 @@ -61,7 +62,8 @@
2.53 else ((*writeln("##@ rew_sub: (t''= "^(term2str t'')^
2.54 ", p'' ="^(terms2str p'')^", true)");*)
2.55 (t'',p'',true))
2.56 - end) handle _ (*TODOtest: NO_REWRITE *) =>
2.57 + end) handle STOP_REW_SUB => (t,[],false)
2.58 + ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests*) =>
2.59 (case t of
2.60 Const(s,T) => (Const(s,T),[],false)
2.61 | Free(s,T) => (Free(s,T),[],false)
2.62 @@ -87,13 +89,14 @@
2.63 else let
2.64 fun chk indets [] = (indets, true)(*return asms<>True until false*)
2.65 | chk indets (a::asms) =
2.66 - case rewrite__set_ thy (i+1) false bdv rls a of
2.67 - None => chk (indets @ [a]) asms
2.68 + (case rewrite__set_ thy (i+1) false bdv rls a of
2.69 + None => (chk (indets @ [a]) asms)
2.70 | Some (t, a') =>
2.71 - if t = HOLogic.true_const then chk (indets @ a') asms
2.72 + if t = HOLogic.true_const
2.73 + then (chk (indets @ a') asms)
2.74 else if t = HOLogic.false_const then ([], false)
2.75 - (*asm false .. thm not applied*)
2.76 - else chk (indets @ [t]) asms;
2.77 + (*asm false .. thm not applied ^^^; continue until False vvv*)
2.78 + else (chk (indets @ [t] @ a') asms));
2.79 in chk [] asms end
2.80
2.81 and rewrite__set_ thy i _ _ (rrls as Rrls _) t =