# HG changeset patch # User wenzelm # Date 801480008 -7200 # Node ID 42ec82147d838fba2da6c7b3e940d1cc93065af3 # Parent 50ac36140e21801f4a2230623c9f2c9a4fe0f4e6 changed macro expander such that patterns also match prefixes of appls; diff -r 50ac36140e21 -r 42ec82147d83 src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Mon May 22 16:00:26 1995 +0200 +++ b/src/Pure/Syntax/ast.ML Fri May 26 11:20:08 1995 +0200 @@ -187,19 +187,28 @@ let exception NO_MATCH; - fun mtch (Constant a, Constant b, env) = + fun mtch (Constant a) (Constant b) env = if a = b then env else raise NO_MATCH - | mtch (Variable a, Constant b, env) = + | mtch (Variable a) (Constant b) env = if a = b then env else raise NO_MATCH - | mtch (ast, Variable x, env) = Env.add ((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; + | mtch ast (Variable x) env = Env.add ((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; + + val (head, args) = + (case (ast, 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, []) + end + | _ => (ast, [])); in - Some (mtch (ast, pat, Env.empty)) handle NO_MATCH => None + Some (mtch head pat Env.empty, args) handle NO_MATCH => None end; @@ -220,7 +229,8 @@ fun try_rules ast ((lhs, rhs) :: pats) = (case match ast lhs of - Some env => (inc changes; Some (subst env rhs)) + Some (env, args) => + (inc changes; Some (mk_appl (subst env rhs) args)) | None => (inc failed_matches; try_rules ast pats)) | try_rules _ [] = None; @@ -285,4 +295,3 @@ end; -