From 9bfa04921a90e2c6a70ea8fafa2a1487ca5fcb19 Mon Sep 17 00:00:00 2001 From: Robert Wright Date: Fri, 5 May 2023 13:34:48 +0100 Subject: [PATCH] Add symmetric and transitive closure relations --- libs/base/Control/Relation.idr | 56 ++++++++++++++++++++++++++++++++++ libs/base/Data/List.idr | 4 +-- tests/idris2/basic044/expected | 26 +++++++++++----- tests/idris2/with003/expected | 1 + 4 files changed, 77 insertions(+), 10 deletions(-) diff --git a/libs/base/Control/Relation.idr b/libs/base/Control/Relation.idr index 91971db13..37971f672 100644 --- a/libs/base/Control/Relation.idr +++ b/libs/base/Control/Relation.idr @@ -127,3 +127,59 @@ PartialEquivalence ty Equal where public export Equivalence ty Equal where + +---------------------------------------- + +public export +data SymClosure : Rel ty -> ty -> ty -> Type where + Fwd : {0 x, y : ty} -> rel x y -> SymClosure rel x y + Bwd : {0 x, y : ty} -> rel y x -> SymClosure rel x y + +public export +Reflexive ty rel => Reflexive ty (SymClosure rel) where + reflexive = Fwd reflexive + +public export +Symmetric ty (SymClosure rel) where + symmetric (Fwd xy) = Bwd xy + symmetric (Bwd yx) = Fwd yx + +---------------------------------------- + +public export +data TransClosure : Rel ty -> ty -> ty -> Type where + Nil : TransClosure rel x x + (::) : {y : ty} -> rel x y -> TransClosure rel y z -> TransClosure rel x z + +public export +Reflexive ty (TransClosure rel) where + reflexive = [] + +public export +Symmetric ty rel => Symmetric ty (TransClosure rel) where + symmetric {x} {y} xy = reverseOnto [] xy + where + reverseOnto : {z : ty} -> + TransClosure rel z x -> + TransClosure rel z y -> + TransClosure rel y x + reverseOnto zx [] = zx + reverseOnto zx (zw :: wy) = reverseOnto (symmetric zw :: zx) wy + +public export +Transitive ty (TransClosure rel) where + transitive [] yz = yz + transitive (xw :: wy) yz = xw :: transitive wy yz + +public export +Symmetric ty rel => Euclidean ty (TransClosure rel) where + euclidean = euclidean @{TSE} + +public export +Symmetric ty rel => Tolerance ty (TransClosure rel) where + +public export +Symmetric ty rel => PartialEquivalence ty (TransClosure rel) where + +public export +Symmetric ty rel => Equivalence ty (TransClosure rel) where diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr index 3f71e7c56..40c24c289 100644 --- a/libs/base/Data/List.idr +++ b/libs/base/Data/List.idr @@ -906,12 +906,12 @@ groupAllWith f = groupWith f . sortBy (comparing f) -- Nil is not Cons export -Uninhabited ([] = x :: xs) where +{0 xs : List a} -> Uninhabited ([] = x :: xs) where uninhabited Refl impossible -- Cons is not Nil export -Uninhabited (x :: xs = []) where +{0 xs : List a} -> Uninhabited (x :: xs = []) where uninhabited Refl impossible -- If the heads or the tails of two lists are provably non-equal, then the diff --git a/tests/idris2/basic044/expected b/tests/idris2/basic044/expected index 7231cc02f..a7fe9fdd8 100644 --- a/tests/idris2/basic044/expected +++ b/tests/idris2/basic044/expected @@ -109,21 +109,25 @@ LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C: ($resolvedN 2) ($resolvedN 2) With default. Target type : Prelude.Types.Nat -LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C: +LOG elab.ambiguous:5: Ambiguous elaboration (kept 4 out of 4 candidates) (not delayed) at Vec:L:C--L:C: +(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil)) (($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil)) (($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil)) (($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil)) Target type : ({arg:N} : (Data.Fin.Fin (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))) -> (Prelude.Basics.List Prelude.Types.Nat) -LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C: +LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C: +$resolvedN $resolvedN $resolvedN Target type : ?Vec.{a:N}_[] -LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C: +LOG elab.ambiguous:5: Ambiguous elaboration (kept 4 out of 4 candidates) (not delayed) at Vec:L:C--L:C: +(($resolvedN ((:: (fromInteger 0)) Nil)) Nil) (($resolvedN ((:: (fromInteger 0)) Nil)) Nil) (($resolvedN ((:: (fromInteger 0)) Nil)) Nil) (($resolvedN ((:: (fromInteger 0)) Nil)) Nil) Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[]) -LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C: +LOG elab.ambiguous:5: Ambiguous elaboration (kept 4 out of 4 candidates) (not delayed) at Vec:L:C--L:C: +(($resolvedN (fromInteger 0)) Nil) (($resolvedN (fromInteger 0)) Nil) (($resolvedN (fromInteger 0)) Nil) (($resolvedN (fromInteger 0)) Nil) @@ -132,26 +136,32 @@ LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C: ($resolvedN 0) ($resolvedN 0) With default. Target type : ?Vec.{a:N}_[] -LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C: +LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C: +$resolvedN $resolvedN $resolvedN Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[]) +LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C: + ($resolvedN 0) + ($resolvedN 0) +With default. Target type : (?Vec.{rel:N}_[] ?Vec.{x:N}_[] ?Vec.{y:N}_[]) LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C: ($resolvedN 0) ($resolvedN 0) With default. Target type : ?Vec.{a:N}_[] -LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C: +LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C: +$resolvedN $resolvedN $resolvedN Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[]) -LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:L:C--L:C: +LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 4 candidates) (delayed) at Vec:L:C--L:C: (($resolvedN (fromInteger 0)) Nil) Target type : (Prelude.Basics.List Prelude.Types.Nat) LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C: ($resolvedN 0) ($resolvedN 0) With default. Target type : Prelude.Types.Nat -LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 2 candidates) (delayed) at Vec:L:C--L:C: +LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:L:C--L:C: $resolvedN Target type : (Prelude.Basics.List Prelude.Types.Nat) LOG declare.def:2: Case tree for Vec.test: [0] (Vec.:: (Prelude.Types.S Prelude.Types.Z) (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.Nil Prelude.Types.Nat) (Vec.:: Prelude.Types.Z (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.:: Prelude.Types.Nat Prelude.Types.Z (Prelude.Basics.Nil Prelude.Types.Nat)) (Vec.Nil (Prelude.Basics.List Prelude.Types.Nat)))) diff --git a/tests/idris2/with003/expected b/tests/idris2/with003/expected index 48db416b2..7ab825b4b 100644 --- a/tests/idris2/with003/expected +++ b/tests/idris2/with003/expected @@ -14,6 +14,7 @@ Main> Error: Can't find an implementation for Num (). ^^^^ Main> Error: Ambiguous elaboration. Possible results: + Control.Relation.Nil Prelude.Nil Data.Vect.Nil