Commit 341a7b5a authored by Juan Pablo Garcia Garland's avatar Juan Pablo Garcia Garland
Browse files

small cleanup+hide test modules

parent 3028ac80
......@@ -21,7 +21,7 @@ cabal-version: >=1.10
library
exposed-modules: Data.Type.Require
other-modules: Figures, Vector
--other-modules: Figures, Vector
other-extensions: UndecidableInstances
, MultiParamTypeClasses
, FlexibleContexts
......
......@@ -163,8 +163,7 @@ instance (TypeError
type family IsEmptyCtx (ms :: [ErrorMessage]) :: Bool where
IsEmptyCtx '[] = True
IsEmptyCtx (m ': ms) = False -- IsEmptyMsg m && IsEmptyCtx ms
IsEmptyCtx _ = True
IsEmptyCtx (m ': ms) = False
type family IsEmptyMsg (m :: ErrorMessage) :: Bool where
IsEmptyMsg (Text "") = True
......@@ -173,8 +172,8 @@ type family IsEmptyMsg (m :: ErrorMessage) :: Bool where
-- -- | Formatting of context printing.
type family ShowCTX (ctx :: [ErrorMessage]) :: ErrorMessage where
ShowCTX ('[]) = 'Text ""
ShowCTX ((m :: ErrorMessage) ': (ms :: [ErrorMessage])) = m :$$: ShowCTX ms
ShowCTX ((m :: ErrorMessage) ': (ms :: [ErrorMessage]))
= m :$$: ShowCTX ms
ShowCTX (m :: [ErrorMessage]) = Text ""
......@@ -234,12 +233,11 @@ type family RequireEqWithMsg (t :: k) (t' :: k) (msg :: k -> k -> Type)
(ctx :: [ErrorMessage]) :: Constraint
type instance RequireEqWithMsg t t' f ctx =
(AssertEq' t t' f ctx, t ~ t')
--If (t `Equal` t') (()::Constraint) (Require (OpError (Eval (f t t'))) ctx))
type family AssertEq' (t1 :: k)(t2 :: k) (f :: k -> k -> Type) ctx :: Constraint
type family AssertEq' (t1 :: k)(t2 :: k)
(f :: k -> k -> Type) ctx :: Constraint
where
AssertEq' a a f ctx = ()
AssertEq' a b f ctx = Require (OpError (Eval (f a b))
) ctx
AssertEq' a b f ctx = Require (OpError (Eval (f a b))) ctx
-- Exported operators.
......@@ -273,7 +271,6 @@ emptyCtx = Proxy :: Proxy '[ Text ""]
appendCtx :: Proxy ctx -> Proxy ctx' -> Proxy (ctx :++ ctx')
appendCtx Proxy Proxy = Proxy
type family (:++) xs ys where
'[] :++ ys = ys
(x ': xs) :++ ys = x ': (xs :++ ys)
......@@ -118,7 +118,7 @@ combine' (Circle 1 1 1 :: Figure R2 (RGB 1 1 1))
> f1 = (Circle 2 2 2 :: Figure R2 (RGB 1 1 1))
> f2 = (Sphere 2 2 2 2:: Figure R3 (RGB 1 1 1))
> f = CFigure $ \Proxy -> f1
> f = (CFigure $ \Proxy -> f1) :: CFigure 'R2 ('RGB 1 1 1) '[]
> f' = CFigure $ \Proxy -> f2
> f'' = traceFig
......@@ -132,13 +132,13 @@ combine' (Circle 1 1 1 :: Figure R2 (RGB 1 1 1))
> combine''
> :: (Require (OpEqDim' (d == d') d d') (Text "lalo" :ctx),
> Require (OpEqCol' (Equ c c') c c') (Text "lalo" : ctx)) =>
> CFigure d c ctx -> CFigure d' c' ctx -> CFigure d c ctx
> :: (Require (OpEqDim' (d == d') d d') (Text "combine''" :ctx),
> Require (OpEqCol' (Equ c c') c c') (Text "combine''" : ctx)) =>
> CFigure d c ctx -> CFigure d' c' ctx' -> CFigure d c ctx
> combine'' (CFigure f1) (CFigure f2)
> = CFigure $ \(a :: Proxy ctx) ->
> req (Proxy :: Proxy (Text "lalo" : ctx))
> (OpCombine (f1 a) (f2 a))
> req (Proxy :: Proxy (Text "combine''" : ctx))
> (OpCombine (f1 a) (f2 Proxy))
> traceFig :: (Proxy ctx' -> Proxy ctx) -> CFigure d c ctx -> CFigure d c ctx'
......@@ -149,3 +149,17 @@ combine' (Circle 1 1 1 :: Figure R2 (RGB 1 1 1))
Error:
> g = combine'' (tr $ tr f) (tr $ tr f'') -- (tr $ tr $ tr $ combine'' f f) f''
Adding traces:
> addMsg :: Proxy msg -> Proxy (msg ': ctx) -> Proxy ctx
> addMsg Proxy Proxy = Proxy
> f11 = traceFig (addMsg (Proxy @(Text "11"))) f
> f22 = traceFig (addMsg (Proxy @(Text "22"))) f
> fcomb = traceFig (addMsg (Proxy @(Text "comb"))) $ combine'' f11 f22
> ferr = traceFig (addMsg (Proxy @(Text "err"))) $ combine'' fcomb f'
Supports Markdown
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