Commit 3028ac80 authored by Juan Pablo Garcia Garland's avatar Juan Pablo Garcia Garland
Browse files

update 0702

parent d8f604e1
......@@ -2,7 +2,7 @@
-- documentation, see http://haskell.org/cabal/users-guide/
name: requirements
version: 0.7.0.1
version: 0.7.0.2
synopsis: Abstraction to manage user defined Type Errors
description: requirements is a framework to build user-defined type errors.
Users condense the arguments of functions that can raise a
......@@ -22,7 +22,20 @@ cabal-version: >=1.10
library
exposed-modules: Data.Type.Require
other-modules: Figures, Vector
-- other-extensions:
other-extensions: UndecidableInstances
, MultiParamTypeClasses
, FlexibleContexts
, ConstraintKinds
, FlexibleInstances
, TypeOperators
, TypeFamilies
, DataKinds
, PolyKinds
, KindSignatures
, GADTs
, TypeApplications
, ScopedTypeVariables
build-depends: base >=4.12 && <4.18
hs-source-dirs: src
default-language: Haskell2010
......@@ -172,8 +172,8 @@ type family IsEmptyMsg (m :: ErrorMessage) :: Bool where
IsEmptyMsg other = False
-- -- | Formatting of context printing.
type family ShowCTX (ctx :: k) :: ErrorMessage where
ShowCTX ('[] :: [ErrorMessage]) = Text ""
type family ShowCTX (ctx :: [ErrorMessage]) :: ErrorMessage where
ShowCTX ('[]) = 'Text ""
ShowCTX ((m :: ErrorMessage) ': (ms :: [ErrorMessage])) = m :$$: ShowCTX ms
ShowCTX (m :: [ErrorMessage]) = Text ""
......@@ -216,15 +216,15 @@ type family AssertEq (t1 :: k)(t2 :: k) ctx :: Constraint where
data Exp (a :: k) where Exp :: a -> Exp a
data Exp (a :: Type) where Exp :: a -> Exp a
type family Eval (exp :: Type) :: k
data CondEq (a ::k) (b :: k) where
data CondEq (a ::Type) (b :: Type) where
CondEq :: a -> b -> CondEq a b
data RequireEqResF (a ::k) (b :: k) where
data RequireEqResF (a :: Type) (b :: Type) where
RequireEqResF :: a -> b -> RequireEqResF a b
data EqMsg (a::k)(b::k) where EqMsg :: a -> b -> EqMsg a b
data EqMsg (a::Type)(b::Type) where EqMsg :: a -> b -> EqMsg a b
type instance Eval (EqMsg t1 t2) =
(Text "\nEQMSG" :<>: ShowTE t1
:<>: Text "\n/= " :<>: ShowTE t2)
......@@ -261,7 +261,7 @@ type family RequireEqRes (t1 :: k) (t2 :: k)
(Require (OpError (Text "\n " :<>: ShowTE t1
:<>: Text "\n/= " :<>: ShowTE t2)) ctx)
type family Equal (a :: k) (b :: k') :: Bool where
type family Equal (a :: k) (b :: k) :: Bool where
Equal a a = True
Equal a b = False
......
......@@ -97,7 +97,7 @@ Then, the wrapper instance:
> type ReqR (OpGet n k a) =
> ReqR (OpGet' (Lt n k) n k a)
> req proxy (OpGet (n :: SNat n) (v :: Vec k a)) =
> req proxy (OpGet' (Proxy @ (Lt n k)) n v)
> req proxy (OpGet' (Proxy @(Lt n k)) n v)
Now we program the good cases:
......@@ -134,7 +134,7 @@ infraestructure.
> type ReqR (OpGet' False n k a) = OpError (Text "lala")
> req = error "unreachable"
> get n v = req (Proxy @ '[Text "getting"]) (OpGet n v)
> get n v = req (Proxy @( '[ 'Text "getting"])) (OpGet n v)
> vecEx = 'a' :< 'b' :< 'c' :< 'd' :< VNil
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment