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

0 files changed, 0 insertions, 0 deletions