aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/telescope_canonical.v
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-22 10:54:14 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-22 10:54:14 +0000
commit4a0fc5c294cf0f6db842bab26df80a3ce7cdf07b (patch)
tree78aa5054da2fc2744cafaae8210d2eb040db0f94 /test-suite/success/telescope_canonical.v
parentc7d396319a1d07bd517b69024ccc6de0a90feaf9 (diff)
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
Diffstat (limited to 'test-suite/success/telescope_canonical.v')
-rw-r--r--test-suite/success/telescope_canonical.v70
1 files changed, 65 insertions, 5 deletions
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.
+
+
+
+