diff options
| -rw-r--r-- | pretyping/evarconv.ml | 26 | ||||
| -rw-r--r-- | test-suite/success/telescope_canonical.v | 70 |
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. + + + + |