1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Tue Sep 28 13:30:29 2010 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Fri Oct 01 10:23:38 2010 +0200
     1.3 @@ -79,7 +79,8 @@
     1.4  	  end)
     1.5  (* simplify asumptions until one evaluates to false, store intermined's (x~=0)*)
     1.6  and eval__true thy i asms bdv rls =
     1.7 -  if asms = [HOLogic.true_const] orelse asms = [] then ([], true) 
     1.8 +  if asms = [HOLogic.true_const] orelse asms = [] then ([], true)
     1.9 +  (* this allows to check Rrls with prepat = ([HOLogic.true_const], pat) *)
    1.10    else if asms = [HOLogic.false_const] then ([], false)
    1.11    else let                            
    1.12        fun chk indets [] = (indets, true)(*return asms<>True until false*)
    1.13 @@ -96,7 +97,7 @@
    1.14  (* rewrite with a rule set, which must not be the empty Erls *)
    1.15  and rewrite__set_ _ _ __ Erls t = 
    1.16      error("rewrite__set_ called with 'Erls' for '"^term2str t^"'")
    1.17 -  (* rewrite with a 'reverse rule set' based on ML code *)
    1.18 +  (* rewrite with a 'reverse rule set' implemented by ML code *)
    1.19    | rewrite__set_ thy i _ _ (rrls as Rrls _) t =
    1.20      let val _= if ! trace_rewrite andalso i < ! depth 
    1.21  	       then tracing ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^
    1.22 @@ -182,13 +183,17 @@
    1.23    in if ct = ct' then NONE else SOME (ct', distinct asm') end
    1.24  
    1.25  and app_rev thy i rrls t = 
    1.26 -    let (*.check a (precond, pattern) of a rev-set; stops with 1st true.*)
    1.27 +    let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
    1.28  	fun chk_prepat thy erls [] t = true
    1.29  	  | chk_prepat thy erls prepat t =
    1.30  	    let fun chk (pres, pat) =
    1.31  		    (let val subst: Type.tyenv * Envir.tenv = 
    1.32  			     Pattern.match thy (pat, t)
    1.33  					    (Vartab.empty, Vartab.empty)
    1.34 +			 val _ = tracing ("app_rev: pres=------------------");
    1.35 +			 val _ = tracing ("app_rev: pres=" ^ terms2str pres);
    1.36 +			 val _ = tracing ("app_rev: pat =" ^ term2str pat);
    1.37 +			 val _ = tracing ("app_rev: t   =" ^ term2str t);
    1.38  		     in snd (eval__true thy (i+1) 
    1.39  					(map (Envir.subst_term subst) pres)
    1.40  					[] erls)
    1.41 @@ -199,7 +204,7 @@
    1.42  					else scan_ f pps;
    1.43  	    in scan_ chk prepat end;
    1.44  
    1.45 -	(*.apply the normal_form of a rev-set.*)
    1.46 +	(* apply the normal_form of a rev-set *)
    1.47  	fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
    1.48  	    if chk_prepat thy erls prepat t
    1.49  	    then ((*tracing("### app_rev': t = "^(term2str t));*)