]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/List.hs
Massive rewrite to better support rank-1 polymorphic types.
[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
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 (Proxy []) = 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 FixityOf [] where
66 instance ClassInstancesFor [] where
67 proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
68 | Just HRefl <- proj_ConstKiTy @_ @[] z
69 = case () of
70 _ | Just Refl <- proj_Const @Applicative q -> Just Dict
71 | Just Refl <- proj_Const @Foldable q -> Just Dict
72 | Just Refl <- proj_Const @Functor q -> Just Dict
73 | Just Refl <- proj_Const @Monad q -> Just Dict
74 | Just Refl <- proj_Const @Traversable q -> Just Dict
75 _ -> Nothing
76 proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ z a))
77 | Just HRefl <- proj_ConstKiTy @_ @[] z
78 = case () of
79 _ | Just Refl <- proj_Const @Eq q
80 , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
81 | Just Refl <- proj_Const @Monoid q -> Just Dict
82 | Just Refl <- proj_Const @Show q
83 , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
84 | Just Refl <- proj_Const @Ord q
85 , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
86 | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict
87 | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
88 | Just Refl <- proj_Const @Seqs.IsSequence q -> Just Dict
89 | Just Refl <- proj_Const @Seqs.SemiSequence q -> Just Dict
90 _ -> Nothing
91 proveConstraintFor _c _q = Nothing
92 instance TypeInstancesFor [] where
93 expandFamFor _c _len f ((TyApp _ z a) `TypesS` TypesZ)
94 | Just HRefl <- proj_ConstKi @_ @Element f
95 , Just HRefl <- proj_ConstKiTy @_ @[] z
96 = Just a
97 expandFamFor _c _len _fam _as = Nothing
98
99 -- Compiling
100 instance
101 ( Gram_App g
102 , Gram_Rule g
103 , Gram_Comment g
104 , Gram_Term src ss g
105 , Inj_Sym ss []
106 ) => Gram_Term_AtomsFor src ss g [] where
107 g_term_atomsFor _t =
108 [ rule "teList_list" $
109 between (symbol "[") (symbol "]") listG
110 , rule "teList_empty" $
111 withMeta $
112 (\src -> BinTree0 $ Token_Term $ TermVT_CF teList_empty `setSource` src)
113 <$ symbol "["
114 <* symbol "]"
115 ]
116 where
117 listG :: CF g (AST_Term src ss)
118 listG = rule "list" $
119 withMeta $
120 (\a mb src ->
121 case mb of
122 Just b_ -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teList_cons) a) b_
123 Nothing ->
124 BinTree2
125 (BinTree2 (BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teList_cons) a)
126 (BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teList_empty))
127 <$> g_term
128 <*> option Nothing (Just <$ symbol "," <*> listG)
129 instance (Source src, Inj_Sym ss []) => Module src ss [] where
130 module_ _s = [] `moduleWhere`
131 [ "[]" := teList_empty
132 , "zipWith" := teList_zipWith
133 , ":" `withInfixR` 5 := teList_cons
134 ]
135
136 -- ** 'Type's
137 tyList :: Source src => Inj_Len vs => Type src vs a -> Type src vs [a]
138 tyList = (tyConst @(K []) @[] `tyApp`)
139
140 -- ** 'Term's
141 teList_empty ::
142 Source src => Inj_Sym ss [] =>
143 Term src ss ts '[Proxy a] [a]
144 teList_empty = Term noConstraint (tyList a0) $ teSym @[] $ list_empty
145
146 teList_cons ::
147 Source src => Inj_Sym ss [] =>
148 Term src ss ts '[Proxy a] (a -> [a] -> [a])
149 teList_cons =
150 Term noConstraint (a0 ~> tyList a0 ~> tyList a0) $
151 teSym @[] $ lam2 list_cons
152
153 teList_zipWith ::
154 Source src => Inj_Sym ss [] =>
155 Term src ss ts '[Proxy a, Proxy b, Proxy c]
156 ((a -> b -> c) -> [a] -> [b] -> [c])
157 teList_zipWith =
158 Term noConstraint ((a0 ~> b1 ~> c2) ~> tyList a0 ~> tyList b1 ~> tyList c2) $
159 teSym @[] $ lam3 zipWith