]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/List.hs
Integrate types to the module system.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / List.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for '[]'.
4 module Language.Symantic.Lib.List where
5
6 import Data.Semigroup ((<>))
7 import Prelude hiding (zipWith)
8 import qualified Data.Functor as Functor
9 import qualified Data.List as List
10 import qualified Data.MonoTraversable as MT
11 import qualified Data.Sequences as Seqs
12 import qualified Data.Text as Text
13 import qualified Data.Traversable as Traversable
14
15 import Language.Symantic
16 import Language.Symantic.Grammar as G
17 import Language.Symantic.Lib.Function (a0, b1, c2)
18 import Language.Symantic.Lib.MonoFunctor (Element)
19
20 -- * Class 'Sym_List'
21 type instance Sym [] = Sym_List
22 class Sym_List term where
23 list_empty :: term [a]
24 list_cons :: term a -> term [a] -> term [a]; infixr 5 `list_cons`
25 list :: [term a] -> term [a]
26 zipWith :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
27
28 default list_empty :: Sym_List (UnT term) => Trans term => term [a]
29 default list_cons :: Sym_List (UnT term) => Trans term => term a -> term [a] -> term [a]
30 default list :: Sym_List (UnT term) => Trans term => [term a] -> term [a]
31 default zipWith :: Sym_List (UnT term) => Trans term => term (a -> b -> c) -> term [a] -> term [b] -> term [c]
32
33 list_empty = trans list_empty
34 list_cons = trans2 list_cons
35 list l = trans (list (unTrans Functor.<$> l))
36 zipWith = trans3 zipWith
37
38 -- Interpreting
39 instance Sym_List Eval where
40 list_empty = return []
41 list_cons = eval2 (:)
42 list = Traversable.sequence
43 zipWith = eval3 List.zipWith
44 instance Sym_List View where
45 list_empty = View $ \_p _v -> "[]"
46 list_cons = viewInfix ":" (infixR 5)
47 list l = View $ \_po v ->
48 "[" <> Text.intercalate ", " ((\(View a) -> a op v) Functor.<$> l) <> "]"
49 where op = (infixN0, SideL)
50 zipWith = view3 "zipWith"
51 instance (Sym_List r1, Sym_List r2) => Sym_List (Dup r1 r2) where
52 list_empty = dup0 @Sym_List list_empty
53 list_cons = dup2 @Sym_List list_cons
54 list l =
55 let (l1, l2) =
56 foldr (\(x1 `Dup` x2) (xs1, xs2) ->
57 (x1:xs1, x2:xs2)) ([], []) l in
58 list l1 `Dup` list l2
59 zipWith = dup3 @Sym_List zipWith
60
61 -- Transforming
62 instance (Sym_List term, Sym_Lambda term) => Sym_List (BetaT term)
63
64 -- Typing
65 instance NameTyOf [] where
66 nameTyOf _c = [] `Mod` "[]"
67 instance FixityOf []
68 instance ClassInstancesFor [] where
69 proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
70 | Just HRefl <- proj_ConstKiTy @_ @[] z
71 = case () of
72 _ | Just Refl <- proj_Const @Applicative q -> Just Dict
73 | Just Refl <- proj_Const @Foldable q -> Just Dict
74 | Just Refl <- proj_Const @Functor q -> Just Dict
75 | Just Refl <- proj_Const @Monad q -> Just Dict
76 | Just Refl <- proj_Const @Traversable q -> Just Dict
77 _ -> Nothing
78 proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ z a))
79 | Just HRefl <- proj_ConstKiTy @_ @[] z
80 = case () of
81 _ | Just Refl <- proj_Const @Eq q
82 , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
83 | Just Refl <- proj_Const @Monoid q -> Just Dict
84 | Just Refl <- proj_Const @Show q
85 , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
86 | Just Refl <- proj_Const @Ord q
87 , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
88 | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
89 | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
90 | Just Refl <- proj_Const @Seqs.IsSequence q -> Just Dict
91 | Just Refl <- proj_Const @Seqs.SemiSequence q -> Just Dict
92 _ -> Nothing
93 proveConstraintFor _c _q = Nothing
94 instance TypeInstancesFor [] where
95 expandFamFor _c _len f ((TyApp _ z a) `TypesS` TypesZ)
96 | Just HRefl <- proj_ConstKi @_ @Element f
97 , Just HRefl <- proj_ConstKiTy @_ @[] z
98 = Just a
99 expandFamFor _c _len _fam _as = Nothing
100
101 -- Compiling
102 instance
103 ( Gram_App g
104 , Gram_Rule g
105 , Gram_Comment g
106 , Gram_Term src ss g
107 , SymInj ss []
108 ) => Gram_Term_AtomsFor src ss g [] where
109 g_term_atomsFor =
110 [ rule "teList_list" $
111 between (symbol "[") (symbol "]") listG
112 , rule "teList_empty" $
113 G.source $
114 (\src -> BinTree0 $ Token_Term $ TermAVT teList_empty `setSource` src)
115 <$ symbol "["
116 <* symbol "]"
117 ]
118 where
119 listG :: CF g (AST_Term src ss)
120 listG = rule "list" $
121 G.source $
122 (\a mb src ->
123 case mb of
124 Just b -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a) b
125 Nothing ->
126 BinTree2
127 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a)
128 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_empty))
129 <$> g_term
130 <*> option Nothing (Just <$ symbol "," <*> listG)
131 instance (Source src, SymInj ss []) => ModuleFor src ss [] where
132 moduleFor = ["List"] `moduleWhere`
133 [ "[]" := teList_empty
134 , "zipWith" := teList_zipWith
135 , ":" `withInfixR` 5 := teList_cons
136 ]
137
138 -- ** 'Type's
139 tyList :: Source src => LenInj vs => Type src vs a -> Type src vs [a]
140 tyList = (tyConst @(K []) @[] `tyApp`)
141
142 -- ** 'Term's
143 teList_empty :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> [a])
144 teList_empty = Term noConstraint (tyList a0) $ teSym @[] $ list_empty
145
146 teList_cons :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> (a -> [a] -> [a]))
147 teList_cons = Term noConstraint (a0 ~> tyList a0 ~> tyList a0) $ teSym @[] $ lam2 list_cons
148
149 teList_zipWith :: Source src => SymInj ss [] => Term src ss ts '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> [a] -> [b] -> [c]))
150 teList_zipWith = Term noConstraint ((a0 ~> b1 ~> c2) ~> tyList a0 ~> tyList b1 ~> tyList c2) $ teSym @[] $ lam3 zipWith