symantic-lib/Language/Symantic/Lib/Sequences.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Sequences'.
   4 module Language.Symantic.Lib.Sequences where
   5
   6 import Data.Sequences (SemiSequence, IsSequence)
   7 import Prelude hiding (filter, reverse)
   8 import qualified Data.MonoTraversable as MT
   9 import qualified Data.Sequences as Seqs
  10
  11 import Language.Symantic
  12 import Language.Symantic.Lib.Function ()
  13 import Language.Symantic.Lib.Bool (tyBool)
  14 import Language.Symantic.Lib.MonoFunctor (e1, famElement)
  15
  16 -- * Class 'Sym_SemiSequence'
  17 type instance Sym SemiSequence = Sym_SemiSequence
  18 class Sym_SemiSequence term where
  19         intersperse :: SemiSequence s => term (MT.Element s) -> term s -> term s
  20         cons        :: SemiSequence s => term (MT.Element s) -> term s -> term s
  21         snoc        :: SemiSequence s => term s -> term (MT.Element s) -> term s
  22         reverse     :: SemiSequence s => term s -> term s
  23         default intersperse :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term s
  24         default cons        :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term s
  25         default snoc        :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term s -> term (MT.Element s) -> term s
  26         default reverse     :: Sym_SemiSequence (UnT term) => Trans term => SemiSequence s => term s -> term s
  27         intersperse = trans2 cons
  28         cons        = trans2 cons
  29         snoc        = trans2 snoc
  30         reverse     = trans1 reverse
  31
  32 -- Interpreting
  33 instance Sym_SemiSequence Eval where
  34         intersperse = eval2 Seqs.intersperse
  35         cons        = eval2 Seqs.cons
  36         snoc        = eval2 Seqs.snoc
  37         reverse     = eval1 Seqs.reverse
  38 instance Sym_SemiSequence View where
  39         intersperse = view2 "intersperse"
  40         cons        = view2 "cons"
  41         snoc        = view2 "snoc"
  42         reverse     = view1 "reverse"
  43 instance (Sym_SemiSequence r1, Sym_SemiSequence r2) => Sym_SemiSequence (Dup r1 r2) where
  44         intersperse = dup2 @Sym_SemiSequence intersperse
  45         cons        = dup2 @Sym_SemiSequence cons
  46         snoc        = dup2 @Sym_SemiSequence snoc
  47         reverse     = dup1 @Sym_SemiSequence reverse
  48
  49 -- Transforming
  50 instance (Sym_SemiSequence term, Sym_Lambda term) => Sym_SemiSequence (BetaT term)
  51
  52 -- Typing
  53 instance NameTyOf SemiSequence where
  54         nameTyOf _c = ["SemiSequence"] `Mod` "SemiSequence"
  55 instance FixityOf SemiSequence
  56 instance ClassInstancesFor SemiSequence
  57 instance TypeInstancesFor SemiSequence
  58
  59 -- Compiling
  60 instance Gram_Term_AtomsFor src ss g SemiSequence
  61 instance (Source src, SymInj ss SemiSequence) => ModuleFor src ss SemiSequence where
  62         moduleFor = ["SemiSequence"] `moduleWhere`
  63          [ "intersperse" := teSemiSequence_intersperse
  64          , "cons"        := teSemiSequence_cons
  65          , "snoc"        := teSemiSequence_snoc
  66          , "reverse"     := teSemiSequence_reverse
  67          ]
  68
  69 -- ** 'Type's
  70 tySemiSequence :: Source src => Type src vs a -> Type src vs (SemiSequence a)
  71 tySemiSequence a = tyConstLen @(K SemiSequence) @SemiSequence (lenVars a) `tyApp` a
  72
  73 s0 :: Source src => LenInj vs => KindInj (K s) =>
  74       Type src (Proxy s ': vs) s
  75 s0 = tyVar "s" varZ
  76
  77 -- ** 'Term's
  78 teSemiSequence_reverse :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (s -> s))
  79 teSemiSequence_reverse = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> s0) $ teSym @SemiSequence $ lam1 reverse
  80
  81 teSemiSequence_intersperse, teSemiSequence_cons :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (e -> s -> s))
  82 teSemiSequence_intersperse = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> s0) $ teSym @SemiSequence $ lam2 intersperse
  83 teSemiSequence_cons = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> s0) $ teSym @SemiSequence $ lam2 cons
  84
  85 teSemiSequence_snoc :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (s -> e -> s))
  86 teSemiSequence_snoc = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> e1 ~> s0) $ teSym @SemiSequence $ lam2 snoc
  87
  88 -- * Class 'Sym_IsSequence'
  89 type instance Sym IsSequence = Sym_IsSequence
  90 class Sym_IsSequence term where
  91         filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
  92         default filter :: Sym_IsSequence (UnT term) => Trans term => IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
  93         filter = trans2 filter
  94
  95 -- Interpreting
  96 instance Sym_IsSequence Eval where
  97         filter  = eval2 Seqs.filter
  98 instance Sym_IsSequence View where
  99         filter  = view2 "filter"
 100 instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (Dup r1 r2) where
 101         filter  = dup2 @Sym_IsSequence filter
 102
 103 -- Transforming
 104 instance (Sym_IsSequence term, Sym_Lambda term) => Sym_IsSequence (BetaT term)
 105
 106 -- Typing
 107 instance NameTyOf IsSequence where
 108         nameTyOf _c = ["IsSequence"] `Mod` "IsSequence"
 109 instance FixityOf IsSequence
 110 instance ClassInstancesFor IsSequence
 111 instance TypeInstancesFor IsSequence
 112
 113 -- Compiling
 114 instance Gram_Term_AtomsFor src ss g IsSequence
 115 instance (Source src, SymInj ss IsSequence) => ModuleFor src ss IsSequence where
 116         moduleFor = ["IsSequence"] `moduleWhere`
 117          [ "filter" := teIsSequence_filter
 118          ]
 119
 120 -- ** 'Type's
 121 tyIsSequence :: Source src => Type src vs a -> Type src vs (IsSequence a)
 122 tyIsSequence a = tyConstLen @(K IsSequence) @IsSequence (lenVars a) `tyApp` a
 123
 124 -- ** 'Term's
 125 teIsSequence_filter :: TermDef IsSequence '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> ((e -> Bool) -> s -> s))
 126 teIsSequence_filter = Term (tyIsSequence s0 # e1 #~ famElement s0) ((e1 ~> tyBool) ~> s0 ~> s0) $ teSym @IsSequence $ lam2 filter