diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/relaxed_ambiguous_paths.out | 50 | ||||
| -rw-r--r-- | test-suite/output/relaxed_ambiguous_paths.v | 72 |
2 files changed, 86 insertions, 36 deletions
diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out index 48368c7ede..6bf03d30d3 100644 --- a/test-suite/output/relaxed_ambiguous_paths.out +++ b/test-suite/output/relaxed_ambiguous_paths.out @@ -1,13 +1,24 @@ -File "stdin", line 10, characters 0-28: +File "stdin", line 13, characters 0-29: Warning: -New coercion path [ac; cd] : A >-> D is ambiguous with existing -[ab; bd] : A >-> D. [ambiguous-paths,typechecker] -[ab] : A >-> B -[ac] : A >-> C -[ab; bd] : A >-> D -[bd] : B >-> D -[cd] : C >-> D -File "stdin", line 26, characters 0-28: +New coercion path [g1; f2] : A >-> B' is ambiguous with existing +[f1; g2] : A >-> B'. [ambiguous-paths,typechecker] +File "stdin", line 14, characters 0-29: +Warning: +New coercion path [h1; f3] : B >-> C' is ambiguous with existing +[f2; h2] : B >-> C'. [ambiguous-paths,typechecker] +[f1] : A >-> A' +[g1] : A >-> B +[f1; g2] : A >-> B' +[g1; h1] : A >-> C +[f1; g2; h2] : A >-> C' +[g2] : A' >-> B' +[g2; h2] : A' >-> C' +[f2] : B >-> B' +[h1] : B >-> C +[f2; h2] : B >-> C' +[h2] : B' >-> C' +[f3] : C >-> C' +File "stdin", line 33, characters 0-28: Warning: New coercion path [ab; bc] : A >-> C is ambiguous with existing [ac] : A >-> C. [ambiguous-paths,typechecker] @@ -17,6 +28,19 @@ New coercion path [ab; bc] : A >-> C is ambiguous with existing [bc] : B >-> C [bc; cd] : B >-> D [cd] : C >-> D +File "stdin", line 50, characters 0-28: +Warning: +New coercion path [ab; bc] : A >-> C is ambiguous with existing +[ac] : A >-> C. [ambiguous-paths,typechecker] +File "stdin", line 51, characters 0-28: +Warning: +New coercion path [ba; ab] : B >-> B is not definitionally an identity function. +New coercion path [ab; ba] : A >-> A is not definitionally an identity function. +[ambiguous-paths,typechecker] +[ab] : A >-> B +[ac] : A >-> C +[ba] : B >-> A +[bc] : B >-> C [B_A] : B >-> A [C_A] : C >-> A [D_A] : D >-> A @@ -31,7 +55,7 @@ New coercion path [ab; bc] : A >-> C is ambiguous with existing [D_B; B_A'] : D >-> A' [D_B] : D >-> B [D_C] : D >-> C -File "stdin", line 121, characters 0-86: +File "stdin", line 147, characters 0-86: Warning: New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing [D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker] @@ -44,15 +68,15 @@ New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing [D_B; B_A'] : D >-> A' [D_B] : D >-> B [D_C] : D >-> C -File "stdin", line 130, characters 0-47: +File "stdin", line 156, characters 0-47: Warning: New coercion path [unwrap_nat; wrap_nat] : NAT >-> NAT is not definitionally an identity function. [ambiguous-paths,typechecker] -File "stdin", line 131, characters 0-64: +File "stdin", line 157, characters 0-64: Warning: New coercion path [unwrap_list; wrap_list] : LIST >-> LIST is not definitionally an identity function. [ambiguous-paths,typechecker] -File "stdin", line 132, characters 0-51: +File "stdin", line 158, characters 0-51: Warning: New coercion path [unwrap_Type; wrap_Type] : TYPE >-> TYPE is not definitionally an identity function. [ambiguous-paths,typechecker] diff --git a/test-suite/output/relaxed_ambiguous_paths.v b/test-suite/output/relaxed_ambiguous_paths.v index 41322045f2..182e155273 100644 --- a/test-suite/output/relaxed_ambiguous_paths.v +++ b/test-suite/output/relaxed_ambiguous_paths.v @@ -1,13 +1,20 @@ Module test1. Section test1. -Variable (A B C D : Type). -Variable (ab : A -> B) (bd : B -> D) (ac : A -> C) (cd : C -> D). - -Local Coercion ab : A >-> B. -Local Coercion bd : B >-> D. -Local Coercion ac : A >-> C. -Local Coercion cd : C >-> D. +Variable (A B C A' B' C' : Type). +Variable (f1 : A -> A') (f2 : B -> B') (f3 : C -> C'). +Variable (g1 : A -> B) (g2 : A' -> B') (h1 : B -> C) (h2 : B' -> C'). + +Local Coercion g1 : A >-> B. +Local Coercion g2 : A' >-> B'. +Local Coercion h1 : B >-> C. +Local Coercion h2 : B' >-> C'. +Local Coercion f1 : A >-> A'. +Local Coercion f2 : B >-> B'. +Local Coercion f3 : C >-> C'. +(* [g1; h1; f3], [f1; g2; h2] : A >-> C' should not be reported as ambiguous *) +(* paths because they are redundant with `[g1; f2], [f1; g2] : A >-> B'` and *) +(* `[h1; f3], [f2; h2] : B >-> C'`. *) Print Graph. @@ -24,8 +31,8 @@ Local Coercion ac : A >-> C. Local Coercion cd : C >-> D. Local Coercion ab : A >-> B. Local Coercion bc : B >-> C. -(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be shown as ambiguous paths *) -(* here because they are redundant with `[ab; bc], [ac] : A >-> C`. *) +(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be reported as ambiguous *) +(* paths because they are redundant with `[ab; bc], [ac] : A >-> C`. *) Print Graph. @@ -34,6 +41,25 @@ End test2. Module test3. Section test3. + +Variable (A B C : Type). +Variable (ab : A -> B) (ba : B -> A) (ac : A -> C) (bc : B -> C). + +Local Coercion ac : A >-> C. +Local Coercion bc : B >-> C. +Local Coercion ab : A >-> B. +Local Coercion ba : B >-> A. +(* `[ba; ac], [bc] : B >-> C` should not be reported as ambiguous paths *) +(* because they are redundant with `[ab; bc], [ac] : A >-> C` and *) +(* `[ba; ab] : B >-> B`. *) + +Print Graph. + +End test3. +End test3. + +Module test4. +Section test4. Variable (A : Type) (P Q : A -> Prop). Record B := { @@ -57,11 +83,11 @@ Local Coercion D_C (d : D) : C := Build_C (D_A d) (D_Q d). Print Graph. -End test3. -End test3. +End test4. +End test4. -Module test4. -Section test4. +Module test5. +Section test5. Variable (A : Type) (P Q : A -> Prop). @@ -89,11 +115,11 @@ Local Coercion D_C (d : D) : C true := Build_C true (D_A d) (D_Q d). Print Graph. -End test4. -End test4. +End test5. +End test5. -Module test5. -Section test5. +Module test6. +Section test6. Variable (A : Type) (P Q : A -> Prop). @@ -123,18 +149,18 @@ Local Coercion D_C (d : D) : C true := Print Graph. -End test5. -End test5. +End test6. +End test6. -Module test6. +Module test7. Record > NAT := wrap_nat { unwrap_nat :> nat }. Record > LIST (T : Type) := wrap_list { unwrap_list :> list T }. Record > TYPE := wrap_Type { unwrap_Type :> Type }. -End test6. +End test7. -Module test7. +Module test8. Set Primitive Projections. Record > NAT_prim := wrap_nat { unwrap_nat :> nat }. Record > LIST_prim (T : Type) := wrap_list { unwrap_list :> list T }. Record > TYPE_prim := wrap_Type { unwrap_Type :> Type }. -End test7. +End test8. |