evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structures

Canonical Structure inference works on named terms only: i.e.
the projection and the value must be named (with few exceptions).

The set of named (head) terms is:
  (Var _|Construct _|Ind _|Const _|Prod _|Sort _)

The set of unnamed is thus:
  (Case _|Fix _|CoFix _|Evar _|Meta _|Rel _)

The MaybeFlex/MaybeFlex case, when no CS inference takes place,
unfolds the rhs only if it exposes a named term. If it exposes
an unnamed term, it tries to unfold on the lhs first. Note that
unnamed terms are whd normal terms, since iota and zeta are
performed by evar_apprec. So the algorithm behaves as before,
but stops unfolding the rhs 1 delta step before it exposes an
unnamed term. Then it starts unfolding the lhs. If the lhs
exposes a rigid term the rhs is naturally unfolded, going back
to same situation in which the algorithm was ending before.
But while it unfolds on the left, the rhs is still named, and
canonical structure inference can succeed.

Ex failing before, the "canon_" prefix marks projections/values
declared as canonical.

  Record test := K { canon_proj : nat }
  (* canon_proj x := math x with K y => y end *)
  canon_val x := match x with 0 => 0 | S m => m end
  Canonical Structure canon_struct x := K (canon_val x)
  (* aliases *)
  proj := canon_proj
  val := canon_val

Old alg:

  proj ?       ===?===       val x
  proj ?       ===?=== canon_val x
  proj ?       ===?=== match x with ... end
  canon_proj ? ===?=== match x with ... end   (* no inference *)
  match ? with K x...end ===?=== match x with 0 ...end (* FAIL *)

New alg:

  proj ?       ===?===       val x
  proj ?       ===?=== canon_val x
  canon_proj ? ===?=== canon_val x (* inference works: ? := canon_struct *)

In case canon_struct is not declared for canon_proj and canon_val
it continues like that:

  canon_proj ? ===?=== canon_val x
  match ? with K x...end ===?=== canon_val x
  match ? with K x...end ===?=== match x with 0 ...end (* FAIL *)

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

2 files changed, 84 insertions, 12 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index bfc2a18db..dc7d10b47 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -196,7 +196,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
           evar_eqappr_x ts env evd pbty
             (decompose_app term1) (decompose_app term2)
 
-and evar_eqappr_x ?(rhs_is_stuck_proj = false)
+and evar_eqappr_x ?(rhs_is_already_stuck = false)
   ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have flushed evars *)
   match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
@@ -325,13 +325,25 @@ and evar_eqappr_x ?(rhs_is_stuck_proj = false)
           (* heuristic: unfold second argument first, exception made
              if the first argument is a beta-redex (expand a constant
              only if necessary) or the second argument is potentially
-             usable as a canonical projection *)
-          let rhs_is_stuck_proj =
-            rhs_is_stuck_proj || is_open_canonical_projection env i appr2 in
-	  if isLambda flex1 || rhs_is_stuck_proj then
+             usable as a canonical projection or canonical value *)
+          let rec is_unnamed (hd, args) = match kind_of_term hd with
+            | (Var _|Construct _|Ind _|Const _|Prod _|Sort _) -> false
+            | (Case _|Fix _|CoFix _|Meta _|Rel _)-> true
+            | Evar _ -> false (* immediate solution without Canon Struct *)
+            | Lambda _ -> assert(args = []); true
+            | LetIn (_,b,_,c) -> 
+                is_unnamed (evar_apprec ts env i args (subst1 b c))
+            | App _| Cast _ -> assert false in
+          let rhs_is_stuck_and_unnamed () =
+            match eval_flexible_term ts env flex2 with
+            | None -> false
+            | Some v2 -> is_unnamed (evar_apprec ts env i l2 v2) in
+          let rhs_is_already_stuck =
+            rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
+	  if isLambda flex1 || rhs_is_already_stuck then
 	    match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
-		evar_eqappr_x ~rhs_is_stuck_proj 
+		evar_eqappr_x ~rhs_is_already_stuck 
                   ts env i pbty (evar_apprec ts env i l1 v1) appr2
 	    | None ->
 		match eval_flexible_term ts env flex2 with
@@ -545,7 +557,7 @@ and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2))
     (fun i -> evar_conv_x trs env i CONV c1 (applist (c,(List.rev ks))));
     (fun i -> ise_list2 i (fun i -> evar_conv_x trs env i CONV) ts ts1)]
 
-(* getting rid of the optional argument rhs_is_stuck_proj *)
+(* getting rid of the optional argument rhs_is_already_stuck *)
 let evar_eqappr_x ts env evd pbty appr1 appr2 =
   evar_eqappr_x ts env evd pbty appr1 appr2
 
diff --git a/test-suite/success/telescope_canonical.v b/test-suite/success/telescope_canonical.v
index 8a607c936..73df5ca99 100644
--- a/test-suite/success/telescope_canonical.v
+++ b/test-suite/success/telescope_canonical.v
@@ -1,12 +1,72 @@
 Structure Inner := mkI { is :> Type }.
 Structure Outer := mkO { os :> Inner }.
-
 Canonical Structure natInner := mkI nat.
 Canonical Structure natOuter := mkO natInner.
-
 Definition hidden_nat := nat.
-
 Axiom P : forall S : Outer, is (os S) -> Prop.
-
-Lemma foo (n : hidden_nat) : P _ n.
+Lemma test1 (n : hidden_nat) : P _ n.
 Admitted.
+
+Structure Pnat := mkP { getp : nat }.
+Definition my_getp := getp.
+Axiom W : nat -> Prop.
+
+(* Fix *)
+Canonical Structure add1Pnat n := mkP (plus n 1).
+Definition test_fix n := (refl_equal _ : W (my_getp _)  = W (n + 1)).
+
+(* Case *)
+Definition pred n := match n with 0 => 0 | S m => m end.
+Canonical Structure predSS n := mkP (pred n).
+Definition test_case x := (refl_equal _ : W (my_getp _)  = W (pred x)).
+Fail Definition test_case' := (refl_equal _ : W (my_getp _)  = W (pred 0)).
+
+Canonical Structure letPnat' := mkP 0.
+Definition letin := (let n := 0 in n).
+Definition test4 := (refl_equal _ : W (getp _)  = W letin).
+Definition test41 := (refl_equal _ : W (my_getp _)  = W letin).
+Definition letin2 (x : nat) := (let n := x in n).
+Canonical Structure letPnat'' x := mkP (letin2 x).
+Definition test42 x := (refl_equal _ : W (my_getp _)  = W (letin2 x)).
+Fail Definition test42' x := (refl_equal _ : W (my_getp _)  = W x).
+
+Structure Morph := mkM { f :> nat -> nat }.
+Definition my_f := f.
+Axiom Q : (nat -> nat) -> Prop.
+
+(* Lambda *)
+Canonical Structure addMorh x := mkM (plus x).
+Definition test_lam x := (refl_equal _ : Q (my_f _) = Q (plus x)).
+Definition test_lam' := (refl_equal _ : Q (my_f _) = Q (plus 0)).
+
+(* Simple tests to justify Sort and Prod as "named". 
+   They are already normal, so they cannot loose their names, 
+   but still... *)
+Structure Sot := mkS { T : Type }.
+Axiom R : Type -> Prop.
+Canonical Structure tsot := mkS (Type).
+Definition test_sort := (refl_equal _ : R (T _) = R Type).
+Canonical Structure tsot2 := mkS (nat -> nat).
+Definition test_prod := (refl_equal _ : R (T _) = R (nat -> nat)).
+
+(* Var *)
+Section Foo.
+Variable v : nat.
+Definition my_v := v.
+Canonical Structure vP := mkP my_v.
+Definition test_var := (refl_equal _ : W (getp _)  = W my_v).
+Canonical Structure vP' := mkP v.
+Definition test_var' := (refl_equal _ : W (my_getp _)  = W my_v).
+End Foo.
+
+(* Rel *)
+Definition test_rel v := (refl_equal _ : W (my_getp _)  = W (my_v v)).
+Goal True.
+pose (x := test_rel 2).
+match goal with x := _ : W (my_getp (vP 2)) = _ |- _ => idtac end.
+apply I.
+Qed.
+
+
+
+