# 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;
-