removed lookups count;
authorwenzelm
Fri Oct 12 12:10:07 2001 +0200 (2001-10-12)
changeset 117339dd88f3aa8e0
parent 11732 139aaced13f4
child 11734 7a21bf539412
removed lookups count;
always try headless rules;
src/Pure/Syntax/ast.ML
     1.1 --- a/src/Pure/Syntax/ast.ML	Fri Oct 12 12:09:38 2001 +0200
     1.2 +++ b/src/Pure/Syntax/ast.ML	Fri Oct 12 12:10:07 2001 +0200
     1.3 @@ -201,7 +201,6 @@
     1.4  fun normalize trace stat get_rules pre_ast =
     1.5    let
     1.6      val passes = ref 0;
     1.7 -    val lookups = ref 0;
     1.8      val failed_matches = ref 0;
     1.9      val changes = ref 0;
    1.10  
    1.11 @@ -209,20 +208,24 @@
    1.12        | subst env (Variable x) = the (Symtab.lookup (env, x))
    1.13        | subst env (Appl asts) = Appl (map (subst env) asts);
    1.14  
    1.15 -    fun try_rules ast ((lhs, rhs) :: pats) =
    1.16 +    fun try_rules ((lhs, rhs) :: pats) ast =
    1.17            (case match ast lhs of
    1.18              Some (env, args) =>
    1.19                (inc changes; Some (mk_appl (subst env rhs) args))
    1.20 -          | None => (inc failed_matches; try_rules ast pats))
    1.21 -      | try_rules _ [] = None;
    1.22 +          | None => (inc failed_matches; try_rules pats ast))
    1.23 +      | try_rules [] _ = None;
    1.24 +    val try_headless_rules = try_rules (get_rules "");
    1.25  
    1.26 -    fun try ast a = (inc lookups; try_rules ast (get_rules a));
    1.27 +    fun try ast a =
    1.28 +      (case try_rules (get_rules a) ast of
    1.29 +        None => try_headless_rules ast
    1.30 +      | some => some);
    1.31  
    1.32      fun rewrite (ast as Constant a) = try ast a
    1.33        | rewrite (ast as Variable a) = try ast a
    1.34        | rewrite (ast as Appl (Constant a :: _)) = try ast a
    1.35        | rewrite (ast as Appl (Variable a :: _)) = try ast a
    1.36 -      | rewrite ast = try ast "";
    1.37 +      | rewrite ast = try_headless_rules ast;
    1.38  
    1.39      fun rewrote old_ast new_ast =
    1.40        if trace then
    1.41 @@ -262,7 +265,6 @@
    1.42      if trace orelse stat then
    1.43        writeln ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
    1.44          string_of_int (! passes) ^ " passes, " ^
    1.45 -        string_of_int (! lookups) ^ " lookups, " ^
    1.46          string_of_int (! changes) ^ " changes, " ^
    1.47          string_of_int (! failed_matches) ^ " matches failed")
    1.48      else ();