# HG changeset patch # User wenzelm # Date 1728735375 -7200 # Node ID 0d728eadad86dbbc169ac104c95a441c65ad64e3 # Parent 3dd8035578b84c7f72d986e90ae7811c4eace38a misc tuning and clarification; diff -r 3dd8035578b8 -r 0d728eadad86 src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Fri Oct 11 15:17:37 2024 +0200 +++ b/src/Pure/Syntax/ast.ML Sat Oct 12 14:16:15 2024 +0200 @@ -161,33 +161,30 @@ (* match *) -fun match ast pat = - let - exception NO_MATCH; +local exception NO_MATCH in - fun mtch (Constant a) (Constant b) env = - if a = b then env else raise NO_MATCH - | mtch (Variable a) (Constant b) env = - if a = b then env else raise NO_MATCH - | mtch ast (Variable x) env = Symtab.update (x, ast) env - | mtch (Appl asts) (Appl pats) env = mtch_lst asts pats env - | mtch _ _ _ = raise NO_MATCH - and mtch_lst (ast :: asts) (pat :: pats) env = - mtch_lst asts pats (mtch ast pat env) - | mtch_lst [] [] env = env - | mtch_lst _ _ _ = raise NO_MATCH; +fun match obj pat = + let + fun match1 (Constant a) (Constant b) env = if a = b then env else raise NO_MATCH + | match1 (Variable a) (Constant b) env = if a = b then env else raise NO_MATCH + | match1 ast (Variable x) env = Symtab.update (x, ast) env + | match1 (Appl asts) (Appl pats) env = match2 asts pats env + | match1 _ _ _ = raise NO_MATCH + and match2 (ast :: asts) (pat :: pats) env = match1 ast pat env |> match2 asts pats + | match2 [] [] env = env + | match2 _ _ _ = raise NO_MATCH; val (head, args) = - (case (ast, pat) of + (case (obj, pat) of (Appl asts, Appl pats) => let val a = length asts and p = length pats in if a > p then (Appl (take p asts), drop p asts) - else (ast, []) + else (obj, []) end - | _ => (ast, [])); - in - SOME (Symtab.build (mtch head pat), args) handle NO_MATCH => NONE - end; + | _ => (obj, [])); + in SOME (Symtab.build (match1 head pat), args) handle NO_MATCH => NONE end; + +end; (* normalize *) @@ -195,9 +192,23 @@ val trace = Config.declare_bool ("syntax_ast_trace", \<^here>) (K false); val stats = Config.declare_bool ("syntax_ast_stats", \<^here>) (K false); +local + +fun subst _ (ast as Constant _) = ast + | subst env (Variable x) = the (Symtab.lookup env x) + | subst env (Appl asts) = Appl (map (subst env) asts); + +fun head_name (Constant a) = SOME a + | head_name (Variable a) = SOME a + | head_name (Appl (Constant a :: _)) = SOME a + | head_name (Appl (Variable a :: _)) = SOME a + | head_name _ = NONE; + fun message head body = Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]); +in + (*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*) fun normalize ctxt get_rules pre_ast = let @@ -208,61 +219,53 @@ val failed_matches = Unsynchronized.ref 0; val changes = Unsynchronized.ref 0; - fun subst _ (ast as Constant _) = ast - | subst env (Variable x) = the (Symtab.lookup env x) - | subst env (Appl asts) = Appl (map (subst env) asts); - - fun try_rules ((lhs, rhs) :: pats) ast = + fun rewrite1 ((lhs, rhs) :: pats) ast = (case match ast lhs of SOME (env, args) => (Unsynchronized.inc changes; SOME (mk_appl (subst env rhs) args)) - | NONE => (Unsynchronized.inc failed_matches; try_rules pats ast)) - | try_rules [] _ = NONE; - val try_headless_rules = try_rules (get_rules ""); + | NONE => (Unsynchronized.inc failed_matches; rewrite1 pats ast)) + | rewrite1 [] _ = NONE; - fun try ast a = - (case try_rules (get_rules a) ast of - NONE => try_headless_rules ast - | some => some); + fun rewrite2 (SOME a) ast = + (case rewrite1 (get_rules a) ast of + NONE => rewrite2 NONE ast + | some => some) + | rewrite2 NONE ast = rewrite1 (get_rules "") ast; - fun rewrite (ast as Constant a) = try ast a - | rewrite (ast as Variable a) = try ast a - | rewrite (ast as Appl (Constant a :: _)) = try ast a - | rewrite (ast as Appl (Variable a :: _)) = try ast a - | rewrite ast = try_headless_rules ast; + fun rewrite ast = rewrite2 (head_name ast) ast; fun rewrote old_ast new_ast = if trace then tracing (message "rewrote:" (pretty_rule (old_ast, new_ast))) else (); - fun norm_root ast = + fun norm1 ast = (case rewrite ast of - SOME new_ast => (rewrote ast new_ast; norm_root new_ast) + SOME new_ast => (rewrote ast new_ast; norm1 new_ast) | NONE => ast); - fun norm ast = - (case norm_root ast of + fun norm2 ast = + (case norm1 ast of Appl sub_asts => let val old_changes = ! changes; - val new_ast = Appl (map norm sub_asts); + val new_ast = Appl (map norm2 sub_asts); in - if old_changes = ! changes then new_ast else norm_root new_ast + if old_changes = ! changes then new_ast else norm1 new_ast end | atomic_ast => atomic_ast); - fun normal ast = + fun norm ast = let val old_changes = ! changes; - val new_ast = norm ast; + val new_ast = norm2 ast; in Unsynchronized.inc passes; - if old_changes = ! changes then new_ast else normal new_ast + if old_changes = ! changes then new_ast else norm new_ast end; val _ = if trace then tracing (message "pre:" (pretty_ast pre_ast)) else (); - val post_ast = normal pre_ast; + val post_ast = norm pre_ast; val _ = if trace orelse stats then tracing (message "post:" (pretty_ast post_ast) ^ "\nnormalize: " ^ @@ -273,3 +276,5 @@ in post_ast end; end; + +end;