]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Tuple2.hs
Clarify a few names in Grammar.Fixity.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Tuple2.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for @(,)@.
4 module Language.Symantic.Lib.Tuple2 where
5
6 import Data.Semigroup ((<>))
7 import Prelude hiding (fst, snd)
8 import qualified Data.Tuple as Tuple
9 import qualified Data.MonoTraversable as MT
10
11 import Language.Symantic
12 import Language.Symantic.Grammar
13 import Language.Symantic.Lib.Function (a0, b1)
14 import Language.Symantic.Lib.MonoFunctor (Element)
15 import Language.Symantic.Lib.Monoid (tyMonoid)
16
17 -- * Class 'Sym_Tuple2'
18 type instance Sym (,) = Sym_Tuple2
19 class Sym_Tuple2 term where
20 tuple2 :: term a -> term b -> term (a, b)
21 fst :: term (a, b) -> term a
22 snd :: term (a, b) -> term b
23
24 default tuple2 :: Sym_Tuple2 (UnT term) => Trans term => term a -> term b -> term (a, b)
25 default fst :: Sym_Tuple2 (UnT term) => Trans term => term (a, b) -> term a
26 default snd :: Sym_Tuple2 (UnT term) => Trans term => term (a, b) -> term b
27
28 tuple2 = trans2 tuple2
29 fst = trans1 fst
30 snd = trans1 snd
31
32 -- Interpreting
33 instance Sym_Tuple2 Eval where
34 tuple2 = eval2 (,)
35 fst = eval1 Tuple.fst
36 snd = eval1 Tuple.snd
37 instance Sym_Tuple2 View where
38 tuple2 (View a) (View b) =
39 View $ \_po v ->
40 "(" <> a (op, SideL) v <> ", " <> b (op, SideR) v <> ")"
41 where op = infixN 0
42 fst = view1 "fst"
43 snd = view1 "snd"
44 instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (Dup r1 r2) where
45 tuple2 = dup2 @Sym_Tuple2 tuple2
46 fst = dup1 @Sym_Tuple2 fst
47 snd = dup1 @Sym_Tuple2 snd
48
49 -- Transforming
50 instance (Sym_Tuple2 term, Sym_Lambda term) => Sym_Tuple2 (BetaT term)
51
52 -- Typing
53 instance NameTyOf (,) where
54 nameTyOf _c = ["Tuple2"] `Mod` ","
55 instance FixityOf (,) where
56 fixityOf _c = Just $ Fixity2 $ infixN (-1)
57 instance ClassInstancesFor (,) where
58 proveConstraintFor _ (TyConst _ _ q :$ t:@a)
59 | Just HRefl <- proj_ConstKiTy @_ @(,) t
60 = case () of
61 _ | Just Refl <- proj_Const @Applicative q
62 , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
63 | Just Refl <- proj_Const @Functor q -> Just Dict
64 | Just Refl <- proj_Const @Foldable q -> Just Dict
65 | Just Refl <- proj_Const @Monad q
66 , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict
67 | Just Refl <- proj_Const @Traversable q -> Just Dict
68 _ -> Nothing
69 proveConstraintFor _ (tq@(TyConst _ _ q) :$ t:@a:@b)
70 | Just HRefl <- proj_ConstKiTy @_ @(,) t
71 = case () of
72 _ | Just Refl <- proj_Const @Bounded q
73 , Just Dict <- proveConstraint (tq`tyApp`a)
74 , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
75 | Just Refl <- proj_Const @Eq q
76 , Just Dict <- proveConstraint (tq`tyApp`a)
77 , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
78 | Just Refl <- proj_Const @Monoid q
79 , Just Dict <- proveConstraint (tq`tyApp`a)
80 , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
81 | Just Refl <- proj_Const @Ord q
82 , Just Dict <- proveConstraint (tq`tyApp`a)
83 , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
84 | Just Refl <- proj_Const @Show q
85 , Just Dict <- proveConstraint (tq`tyApp`a)
86 , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
87 | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
88 | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
89 _ -> Nothing
90 proveConstraintFor _c _q = Nothing
91 instance TypeInstancesFor (,) where
92 expandFamFor _c _len f (t:@_a:@b `TypesS` TypesZ)
93 | Just HRefl <- proj_ConstKi @_ @Element f
94 , Just HRefl <- proj_ConstKiTy @_ @(,) t
95 = Just b
96 expandFamFor _c _len _fam _as = Nothing
97
98 -- Compiling
99 instance
100 ( Gram_Source src g
101 , Gram_Alt g
102 , Gram_Rule g
103 , Gram_Comment g
104 , Gram_Term src ss g
105 , SymInj ss (,)
106 ) => Gram_Term_AtomsFor src ss g (,) where
107 g_term_atomsFor =
108 -- TODO: proper TupleSections
109 [ rule "teTuple2_2" $
110 source $ parens $
111 (\a b src ->
112 BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2) a) b)
113 <$> g_term
114 <* symbol ","
115 <*> g_term
116 , rule "teTuple2" $
117 source $
118 (\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2)
119 <$ symbol "(,)"
120 ]
121 instance (Source src, SymInj ss (,)) => ModuleFor src ss (,) where
122 moduleFor = ["Tuple2"] `moduleWhere`
123 [ "fst" := teTuple2_fst
124 , "snd" := teTuple2_snd
125 ]
126
127 -- ** 'Term's
128 tyTuple2 :: Source src => LenInj vs => Type src vs a -> Type src vs b -> Type src vs (a, b)
129 tyTuple2 a b = tyConst @(K (,)) @(,) `tyApp` a `tyApp` b
130
131 teTuple2 :: TermDef (,) '[Proxy a, Proxy b] (() #> (a -> b -> (a, b)))
132 teTuple2 = Term noConstraint (a0 ~> b1 ~> tyTuple2 a0 b1) $ teSym @(,) $ lam2 tuple2
133 teTuple2_fst :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> a))
134 teTuple2_fst = Term noConstraint (tyTuple2 a0 b1 ~> a0) $ teSym @(,) $ lam1 fst
135 teTuple2_snd :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> b))
136 teTuple2_snd = Term noConstraint (tyTuple2 a0 b1 ~> b1) $ teSym @(,) $ lam1 snd