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