mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-11 14:57:30 +03:00
5b73dcbde1
Instead of checking there's exactly one result, they must check that one of the (possibly many) results is the exact name they were looking for, since some things may be unqualified and will be returned anyway. Fixes #2271 (again; test for disambig001 and disambig002 added)
90 lines
2.4 KiB
Idris
90 lines
2.4 KiB
Idris
import Data.Vect
|
|
import Data.Fin
|
|
import Control.Isomorphism
|
|
|
|
Dec0 : Type -> Type
|
|
Dec0 = Dec
|
|
|
|
Dec1 : {A : Type} -> (P : A -> Type) -> Type
|
|
Dec1 {A} P = (a : A) -> Dec0 (P a)
|
|
|
|
Unique : Type -> Type
|
|
Unique t = (p : t) -> (q : t) -> p = q
|
|
|
|
Unique0 : Type -> Type
|
|
Unique0 = Unique
|
|
|
|
Unique1 : (t0 -> Type) -> Type
|
|
Unique1 {t0} t1 = (v : t0) -> Unique0 (t1 v)
|
|
|
|
namespace Iso
|
|
|
|
from : {A, B : Type} -> Iso A B -> (B -> A)
|
|
from (MkIso to from toFrom fromTo) = from
|
|
|
|
namespace Fin
|
|
|
|
||| 'Tail' of a finite function
|
|
tail : {A : Type} -> {n : Nat} ->
|
|
(Fin (S n) -> A) -> (Fin n -> A)
|
|
tail f k = f (FS k)
|
|
|
|
||| Maps a finite function to a vector
|
|
toVect : {A : Type} -> {n : Nat} ->
|
|
(Fin n -> A) -> Vect n A
|
|
toVect {n = Z} _ = Nil
|
|
toVect {n = S m} f = (f FZ) :: (toVect (tail f))
|
|
|
|
namespace Finite
|
|
|
|
||| Notion of finiteness for types
|
|
Finite : Type -> Type
|
|
Finite A = Exists (\ n => Iso A (Fin n))
|
|
|
|
||| Cardinality of finite types
|
|
card : {A : Type} -> (fA : Finite A) -> Nat
|
|
card = getWitness
|
|
|
|
||| Maps a finite type |A| of cardinality |n| to a vector of |A|-values of length |n|
|
|
toVect : {A : Type} -> (fA : Finite A) -> Vect (card fA) A
|
|
toVect (Evidence n iso) = toVect (from iso)
|
|
|
|
||| Filters a vector on a decidable property and pairs elements with proofs
|
|
filterTag : {A : Type} ->
|
|
{P : A -> Type} ->
|
|
Dec1 P ->
|
|
Vect n A ->
|
|
Sigma Nat (\ m => Vect m (Sigma A P))
|
|
filterTag d1P Nil = (_ ** Nil)
|
|
filterTag d1P (a :: as) with (filterTag d1P as)
|
|
| (_ ** tail) with (d1P a)
|
|
| (Yes p) = (_ ** (a ** p) :: tail)
|
|
| (No _) = (_ ** tail)
|
|
|
|
||| Maps a finite type |A| and a decidable predicate |P| to a vector |Sigma A P| values
|
|
toVect : {A : Type} ->
|
|
{P : A -> Type} ->
|
|
Finite A ->
|
|
Dec1 P ->
|
|
(n : Nat ** Vect n (Sigma A P))
|
|
toVect fA d1P = filterTag d1P (toVect fA)
|
|
|
|
sigmaUniqueLemma1 : {A : Type} ->
|
|
{P : A -> Type} ->
|
|
Unique1 {t0 = A} P ->
|
|
(a : A) ->
|
|
(p : P a) ->
|
|
(ss : Vect n (Sigma A P)) ->
|
|
Elem a (map getWitness ss) ->
|
|
Elem (a ** p) ss
|
|
|
|
toVectComplete : {A : Type} ->
|
|
{P : A -> Type} ->
|
|
(fA : Finite A) ->
|
|
(d1P : Dec1 P) ->
|
|
Unique1 {t0 = A} P ->
|
|
(s : Sigma A P) ->
|
|
Elem s (getProof (toVect fA d1P))
|
|
|
|
|