rhi/quox
rhi
/
quox
1
0
Fork 0
Code Issues 16 Pull Requests 1 Releases Wiki Activity

bikeshedding again

This commit is contained in:
rhiannon morris 2021-12-23 16:05:55 +01:00
parent 1924250fcd
commit acfa1b96be
1 changed files with 28 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

54
src/Quox/Error.idr
View File

@ -12,8 +12,8 @@ import Control.Monad.RWS
%default total
||| a representation of a list's length. this is used in the `Ord` instance to
||| transform the `Ord` constraints into `Eq`s
||| a representation of a list's length. this is used in `implyAll` to transform
||| the constraints one by one
public export
data Spine : List a -> Type where
NIL : Spine []
@ -37,13 +37,12 @@ Uninhabited (OneOf []) where uninhabited x = uninhabited x.elem
export %inline
inj : ty `Elem` tys => ty -> OneOf tys
inj value = One %search value
inj @{elem} value = One {elem, value}
||| `All p types` computes a constraint for `p a` for each `a` in `types`
public export
All : (Type -> Type) -> List Type -> Type
All p [] = ()
All p (x::xs) = (p x, All p xs)
All p = foldr (,) () . map p
private
@ -51,24 +50,28 @@ eq : All Eq types => OneOf types -> OneOf types -> Bool
eq (One Here x) (One Here y) = x == y
eq (One (There p) x) (One (There q) y) = eq (One p x) (One q y)
eq (One Here _) (One (There _) _) = False
eq (One (There z) x) (One Here y) = False
eq (One (There _) _) (One Here _) = False
export %inline
All Eq types => Eq (OneOf types) where (==) = eq
private
ordsToEqs : Spine types => All Ord types => All Eq types
ordsToEqs @{NIL} = ()
ordsToEqs @{CONS tl} = (%search, ordsToEqs @{tl})
export
implyAll : (0 c, d : Type -> Type) ->
(forall a. c a -> d a) => Spine types => All c types => All d types
implyAll c d @{q} @{spine} @{ps} = go spine ps where
go : forall types. Spine types -> All c types -> All d types
go NIL _ = ()
go (CONS tl) (p, ps) = (q p, go tl ps)
private %inline
[eqOrds] (Spine types, All Ord types) => Eq (OneOf types) where
(==) = eq @{ordsToEqs}
(==) = eq @{implyAll Ord Eq}
private
cmp : All Ord types => OneOf types -> OneOf types -> Ordering
cmp : All Ord types => (x, y : OneOf types) -> Ordering
cmp (One Here x) (One Here y) = compare x y
cmp (One Here _) (One (There _) _) = LT
cmp (One (There _) _) (One Here _) = GT
@ -79,11 +82,12 @@ export %inline
compare = cmp
private shw : All Show types => Prec -> OneOf types -> String
shw d (One Here value) = showPrec d value
shw d (One (There p) value) = shw d $ One p value
export %inline All Show types => Show (OneOf types) where showPrec = shw
export %inline
All Show types => Show (OneOf types) where
showPrec d = go where
go : forall types. All Show types => OneOf types -> String
go (One Here value) = showPrec d value
go (One (There p) value) = go $ One p value
public export
@ -122,7 +126,7 @@ without' (y :: xs) (There p) = y :: without' xs p
infix 9 `without`
export %inline
without : (xs : List a) -> (x : a) -> x `Elem` xs => List a
xs `without` x = without' {x} xs %search
(xs `without` x) @{e} = without' xs e
private
@ -135,7 +139,7 @@ get' (There y) (One (There p) x) = mapSnd {elem $= There} $ get' y (One p x)
export %inline
get : (0 err : Type) -> err `Elem` errs =>
OneOf errs -> Either err (OneOf (errs `without` err))
get _ = get' %search
get _ @{e} = get' e
export %inline
@ -153,14 +157,12 @@ data Embed : List a -> List a -> Type where
(::) : x `Elem` ys -> Embed xs ys -> Embed (x::xs) ys
private
embedElem' : Embed xs ys -> x `Elem` xs -> x `Elem` ys
embedElem' (e :: _) Here = e
embedElem' (_ :: es) (There p) = embedElem' es p
export %inline
embedElem : Embed xs ys => x `Elem` xs -> x `Elem` ys
embedElem = embedElem' %search
embedElem @{emb} = go emb where
go : forall xs. Embed xs ys -> x `Elem` xs -> x `Elem` ys
go (e :: _) Here = e
go (_ :: es) (There p) = go es p
export %inline
@ -205,7 +207,7 @@ implementation
(Monad m, Embed errs1 errs2) =>
MonadEmbed (ErrorT errs1 m) (ErrorT errs2 m)
where
embed (MkErrorT act) = MkErrorT $ mapFst {elem $= embedElem} <$> act
embed (MkErrorT act) = MkErrorT $ act <&> mapFst {elem $= embedElem}
export %inline