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