mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 12:42:02 +03:00
[ cleanup ] now that we can assert_total on data
This commit is contained in:
parent
7c66d10eae
commit
b173267f50
@ -5,7 +5,7 @@
|
||||
|
||||
module Data.Description.Indexed
|
||||
|
||||
%default covering
|
||||
%default total
|
||||
|
||||
public export
|
||||
data IDesc : (p : Type -> Type) -> (i : Type) -> Type where
|
||||
@ -16,7 +16,7 @@ data IDesc : (p : Type -> Type) -> (i : Type) -> Type where
|
||||
(+) : (d1, d2 : IDesc p i) -> IDesc p i
|
||||
Sig : (s : Type) -> p s -> (s -> IDesc p i) -> IDesc p i
|
||||
|
||||
total public export
|
||||
public export
|
||||
Elem : IDesc p i -> (i -> Type) -> Type
|
||||
Elem Zero x = Void
|
||||
Elem One x = ()
|
||||
@ -27,7 +27,7 @@ Elem (Sig s prop d) x = (v : s ** Elem (d v) x)
|
||||
|
||||
public export
|
||||
data Fix : (i -> IDesc p i) -> i -> Type where
|
||||
MkFix : Elem (d i) (Fix d) -> Fix d i
|
||||
MkFix : assert_total (Elem (d i) (Fix d)) -> Fix d i
|
||||
|
||||
namespace Example
|
||||
|
||||
@ -35,7 +35,7 @@ namespace Example
|
||||
VecD a 0 = One
|
||||
VecD a (S n) = Sig a () (const (Id n))
|
||||
|
||||
export total
|
||||
export
|
||||
map : (d : IDesc p i) -> ((v : i) -> x v -> y v) -> Elem d x -> Elem d y
|
||||
map Zero f v = v
|
||||
map One f v = v
|
||||
@ -45,8 +45,8 @@ map (d1 + d2) f (Left v) = Left (map d1 f v)
|
||||
map (d1 + d2) f (Right v) = Right (map d2 f v)
|
||||
map (Sig s _ d) f (x ** v) = (x ** map (d x) f v)
|
||||
|
||||
export covering
|
||||
export
|
||||
ifold : {d : i -> IDesc p i} ->
|
||||
((v : i) -> Elem (d v) x -> x v) ->
|
||||
{v : i} -> Fix d v -> x v
|
||||
ifold alg (MkFix t) = alg v (Indexed.map (d v) (\ _ => ifold alg) t)
|
||||
ifold alg (MkFix t) = alg v (assert_total $ Indexed.map (d v) (\ _ => ifold alg) t)
|
||||
|
@ -5,7 +5,7 @@
|
||||
|
||||
module Data.Description.Regular
|
||||
|
||||
%default covering
|
||||
%default total
|
||||
|
||||
||| Description of regular functors
|
||||
||| @ p stores additional data for constant types
|
||||
@ -55,7 +55,7 @@ map d f = go d where
|
||||
||| is total because we do not track positivity in function arguments
|
||||
public export
|
||||
data Fix : Desc p -> Type where
|
||||
MkFix : Elem d (Fix d) -> Fix d
|
||||
MkFix : assert_total (Elem d (Fix d)) -> Fix d
|
||||
|
||||
namespace Example
|
||||
|
||||
@ -94,7 +94,7 @@ infixr 0 ~>
|
||||
export
|
||||
record (~>) {p : Type -> Type} (d : Desc p) (b : Fix d -> Type) where
|
||||
constructor MkMemo
|
||||
getMemo : Memo d (\ x => Inf (d ~> x)) (b . MkFix)
|
||||
getMemo : assert_total (Memo d (\ x => Inf (d ~> x)) (b . MkFix))
|
||||
|
||||
export
|
||||
trie : {d : Desc p} -> {0 b : Fix d -> Type} -> ((x : Fix d) -> b x) -> d ~> b
|
||||
@ -106,7 +106,7 @@ trie f = MkMemo (go d (\ t => f (MkFix t))) where
|
||||
Memo e (\ x => Inf (d ~> x)) b'
|
||||
go Zero f = ()
|
||||
go One f = f ()
|
||||
go Id f = trie f
|
||||
go Id f = assert_total trie f
|
||||
go (Const s prop) f = f
|
||||
go (d1 * d2) f = go d1 $ \ v1 => go d2 $ \ v2 => f (v1, v2)
|
||||
go (d1 + d2) f = (go d1 (\ v => f (Left v)), go d2 (\ v => f (Right v)))
|
||||
|
@ -103,7 +103,7 @@ stream (MkEnumerator enum) = iterate enum []
|
||||
-- Defining generic enumerators for regular types
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
covering export
|
||||
export
|
||||
regular : (d : Desc List) -> Enumerator (Fix d) (Fix d)
|
||||
regular d = MkFix <$> go d where
|
||||
|
||||
@ -123,11 +123,9 @@ namespace Example
|
||||
lists : (xs : List a) -> Nat -> List (Fix (ListD xs))
|
||||
lists xs = sized (regular (ListD xs))
|
||||
|
||||
covering
|
||||
encode : {0 xs : List a} -> List a -> Fix (ListD xs)
|
||||
encode = foldr (\x, xs => MkFix (Right (x, xs))) (MkFix (Left ()))
|
||||
|
||||
covering
|
||||
decode : {xs : List a} -> Fix (ListD xs) -> List a
|
||||
decode = fold (either (const []) (uncurry (::)))
|
||||
|
||||
|
@ -86,7 +86,7 @@ isized f (S n) v = runIEnumerator (f v) (isized f n)
|
||||
-- Defining generic enumerators for indexed datatypes
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
covering export
|
||||
export
|
||||
indexed : (d : i -> IDesc List i) -> (v : i) -> IEnumerator (Fix d) (Fix d v)
|
||||
indexed d v = MkFix <$> go (d v) where
|
||||
|
||||
@ -98,11 +98,11 @@ indexed d v = MkFix <$> go (d v) where
|
||||
go (d1 + d2) = Left <$> go d1 <|> Right <$> go d2
|
||||
go (Sig s vs f) = sig (const vs) (\ x => go (f x))
|
||||
|
||||
export covering
|
||||
export
|
||||
0 Memorator : (d : Desc p) -> (Fix d -> Type) -> Type -> Type
|
||||
Memorator d a b = (d ~> (List . a)) -> List b
|
||||
|
||||
export covering
|
||||
export
|
||||
memorate : {d : Desc p} ->
|
||||
{0 b : Fix d -> Type} ->
|
||||
((x : Fix d) -> Memorator d b (b x)) ->
|
||||
|
Loading…
Reference in New Issue
Block a user