Fixing amazing loop when using eta-expansion in pattern-matching for

printing notations. Since notation printing is not typed, printing "F G"
using a notation for "f (fun x => g)" recursively eta-expands G, then
x, then a new x and so on forever.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14796 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 24 insertions, 1 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 839a90da05..b484d175b6 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -620,6 +620,18 @@ let match_alist match_fun metas sigma rest x iter termin lassoc =
   let l,sigma = aux sigma [] rest in
   (pi1 sigma, (x,if lassoc then l else List.rev l)::pi2 sigma, pi3 sigma)
 
+let does_not_come_from_already_eta_expanded_var =
+  (* This is hack to avoid looping on a rule with rhs of the form *)
+  (* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *)
+  (* "F (fun x => H x)" and "H x" is recursively matched against the same *)
+  (* rule, giving "H (fun x' => x x')" and so on. *)
+  (* Ideally, we would need the type of the expression to know which of *)
+  (* the arguments applied to it can be eta-expanded without looping. *)
+  (* The following test is then an approximation of what can be done *)
+  (* optimally (whether other looping situations can occur remains to be *)
+  (* checked). *)
+  function GVar _ -> false | _ -> true
+
 let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
   match (a1,a2) with
 
@@ -663,7 +675,8 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
 	else if n1 > n2 then
 	  let l11,l12 = list_chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2
 	else f1,l1, f2, l2 in
-      List.fold_left2 (match_in u alp metas)
+      let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
+      List.fold_left2 (match_ may_use_eta u alp metas)
         (match_in u alp metas sigma f1 f2) l1 l2
   | GLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) ->
      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
diff --git a/test-suite/complexity/Notations.v b/test-suite/complexity/Notations.v
new file mode 100644
index 0000000000..d36d77d574
--- /dev/null
+++ b/test-suite/complexity/Notations.v
@@ -0,0 +1,10 @@
+(* Last line should not loop, even in the presence of eta-expansion in the *)
+(* printing mechanism *)
+(* Expected time < 1.00s *)
+
+Notation "'bind' x <- y ; z" :=(y (fun x => z)) (at level 99, x at
+  level 0, y at level 0,format "'[hv' 'bind'  x  <-  y ;  '/' z ']'").
+
+Definition f (g : (nat -> nat) -> nat) := g (fun x => 0).
+
+Check (fun g => f g).