]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/List.hs
Rename inj_* -> *Inj.
[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 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 , SymInj ss []
106 ) => Gram_Term_AtomsFor src ss g [] where
107 g_term_atomsFor =
108 [ rule "teList_list" $
109 between (symbol "[") (symbol "]") listG
110 , rule "teList_empty" $
111 G.source $
112 (\src -> BinTree0 $ Token_Term $ TermAVT teList_empty `setSource` src)
113 <$ symbol "["
114 <* symbol "]"
115 ]
116 where
117 listG :: CF g (AST_Term src ss)
118 listG = rule "list" $
119 G.source $
120 (\a mb src ->
121 case mb of
122 Just b -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a) b
123 Nothing ->
124 BinTree2
125 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a)
126 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_empty))
127 <$> g_term
128 <*> option Nothing (Just <$ symbol "," <*> listG)
129 instance (Source src, SymInj ss []) => ModuleFor src ss [] where
130 moduleFor = ["List"] `moduleWhere`
131 [ "[]" := teList_empty
132 , "zipWith" := teList_zipWith
133 , ":" `withInfixR` 5 := teList_cons
134 ]
135
136 -- ** 'Type's
137 tyList :: Source src => LenInj vs => Type src vs a -> Type src vs [a]
138 tyList = (tyConst @(K []) @[] `tyApp`)
139
140 -- ** 'Term's
141 teList_empty :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> [a])
142 teList_empty = Term noConstraint (tyList a0) $ teSym @[] $ list_empty
143
144 teList_cons :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> (a -> [a] -> [a]))
145 teList_cons = Term noConstraint (a0 ~> tyList a0 ~> tyList a0) $ teSym @[] $ lam2 list_cons
146
147 teList_zipWith :: Source src => SymInj ss [] => Term src ss ts '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> [a] -> [b] -> [c]))
148 teList_zipWith = Term noConstraint ((a0 ~> b1 ~> c2) ~> tyList a0 ~> tyList b1 ~> tyList c2) $ teSym @[] $ lam3 zipWith