]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Either.hs
Separate tests into test/.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Either.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Either'.
4 module Language.Symantic.Lib.Either where
5
6 import Prelude hiding (either)
7 import qualified Data.Either as Either
8 import qualified Data.MonoTraversable as MT
9
10 import Language.Symantic
11 import Language.Symantic.Lib.MonoFunctor (Element)
12 import Language.Symantic.Lib.Function (a0, b1, c2)
13
14 -- * Class 'Sym_Either'
15 type instance Sym Either = Sym_Either
16 class Sym_Either term where
17 _Left :: term l -> term (Either l r)
18 _Right :: term r -> term (Either l r)
19 either :: term (l -> a) -> term (r -> a) -> term (Either l r) -> term a
20
21 default _Left :: Sym_Either (UnT term) => Trans term => term l -> term (Either l r)
22 default _Right :: Sym_Either (UnT term) => Trans term => term r -> term (Either l r)
23 default either :: Sym_Either (UnT term) => Trans term => term (l -> a) -> term (r -> a) -> term (Either l r) -> term a
24
25 _Left = trans1 _Left
26 _Right = trans1 _Right
27 either = trans3 either
28
29 -- Interpreting
30 instance Sym_Either Eval where
31 _Right = eval1 Right
32 _Left = eval1 Left
33 either = eval3 Either.either
34 instance Sym_Either View where
35 _Right = view1 "Right"
36 _Left = view1 "Left"
37 either = view3 "either"
38 instance (Sym_Either r1, Sym_Either r2) => Sym_Either (Dup r1 r2) where
39 _Left = dup1 @Sym_Either _Left
40 _Right = dup1 @Sym_Either _Right
41 either = dup3 @Sym_Either either
42
43 -- Transforming
44 instance (Sym_Either term, Sym_Lambda term) => Sym_Either (BetaT term)
45
46 -- Typing
47 instance NameTyOf Either where
48 nameTyOf _c = ["Either"] `Mod` "Either"
49 instance FixityOf Either
50 instance ClassInstancesFor Either where
51 proveConstraintFor _ (TyConst _ _ q :$ e:@_l)
52 | Just HRefl <- proj_ConstKiTy @_ @Either e
53 = case () of
54 _ | Just Refl <- proj_Const @Functor q -> Just Dict
55 | Just Refl <- proj_Const @Applicative q -> Just Dict
56 | Just Refl <- proj_Const @Monad q -> Just Dict
57 | Just Refl <- proj_Const @Foldable q -> Just Dict
58 | Just Refl <- proj_Const @Traversable q -> Just Dict
59 _ -> Nothing
60 proveConstraintFor _ (tq@(TyConst _ _ q) :$ e:@l:@r)
61 | Just HRefl <- proj_ConstKiTy @_ @Either e
62 = case () of
63 _ | Just Refl <- proj_Const @Eq q
64 , Just Dict <- proveConstraint (tq`tyApp`l)
65 , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict
66 | Just Refl <- proj_Const @Ord q
67 , Just Dict <- proveConstraint (tq`tyApp`l)
68 , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict
69 | Just Refl <- proj_Const @Show q
70 , Just Dict <- proveConstraint (tq`tyApp`l)
71 , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict
72 | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
73 | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
74 _ -> Nothing
75 proveConstraintFor _c _q = Nothing
76 instance TypeInstancesFor Either where
77 expandFamFor _c _len f (e:@_ty_l:@r `TypesS` TypesZ)
78 | Just HRefl <- proj_ConstKi @_ @Element f
79 , Just HRefl <- proj_ConstKiTy @_ @Either e
80 = Just r
81 expandFamFor _c _len _fam _as = Nothing
82
83 -- Compiling
84 instance Gram_Term_AtomsFor src ss g Either
85 instance (Source src, SymInj ss Either) => ModuleFor src ss Either where
86 moduleFor = ["Either"] `moduleWhere`
87 [ "Left" := teEither_Left
88 , "Right" := teEither_Right
89 , "either" := teEither_either
90 ]
91
92 -- ** 'Type's
93 tyEither :: Source src => Type src vs l -> Type src vs r -> Type src vs (Either l r)
94 tyEither l r = tyConstLen @(K Either) @Either (lenVars l) `tyApp` l `tyApp` r
95
96 -- ** 'Term's
97 teEither_Left :: TermDef Either '[Proxy a, Proxy b] (() #> (a -> Either a b))
98 teEither_Left = Term noConstraint (a0 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Left
99 teEither_Right :: TermDef Either '[Proxy a, Proxy b] (() #> (b -> Either a b))
100 teEither_Right = Term noConstraint (b1 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Right
101 teEither_either :: TermDef Either '[Proxy a, Proxy b, Proxy c] (() #> ((a -> c) -> (b -> c) -> Either a b -> c))
102 teEither_either = Term noConstraint ((a0 ~> c2) ~> (b1 ~> c2) ~> tyEither a0 b1 ~> c2) $ teSym @Either $ lam3 either