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 FixityOf SemiSequence
  54 instance ClassInstancesFor SemiSequence
  55 instance TypeInstancesFor SemiSequence
  56
  57 -- Compiling
  58 instance Gram_Term_AtomsFor src ss g SemiSequence
  59 instance (Source src, SymInj ss SemiSequence) => ModuleFor src ss SemiSequence where
  60         moduleFor = ["SemiSequence"] `moduleWhere`
  61          [ "intersperse" := teSemiSequence_intersperse
  62          , "cons"        := teSemiSequence_cons
  63          , "snoc"        := teSemiSequence_snoc
  64          , "reverse"     := teSemiSequence_reverse
  65          ]
  66
  67 -- ** 'Type's
  68 tySemiSequence :: Source src => Type src vs a -> Type src vs (SemiSequence a)
  69 tySemiSequence a = tyConstLen @(K SemiSequence) @SemiSequence (lenVars a) `tyApp` a
  70
  71 s0 :: Source src => LenInj vs => KindInj (K s) =>
  72       Type src (Proxy s ': vs) s
  73 s0 = tyVar "s" varZ
  74
  75 -- ** 'Term's
  76 teSemiSequence_reverse :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (s -> s))
  77 teSemiSequence_reverse = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> s0) $ teSym @SemiSequence $ lam1 reverse
  78
  79 teSemiSequence_intersperse, teSemiSequence_cons :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (e -> s -> s))
  80 teSemiSequence_intersperse = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> s0) $ teSym @SemiSequence $ lam2 intersperse
  81 teSemiSequence_cons = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> s0) $ teSym @SemiSequence $ lam2 cons
  82
  83 teSemiSequence_snoc :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (s -> e -> s))
  84 teSemiSequence_snoc = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> e1 ~> s0) $ teSym @SemiSequence $ lam2 snoc
  85
  86 -- * Class 'Sym_IsSequence'
  87 type instance Sym IsSequence = Sym_IsSequence
  88 class Sym_IsSequence term where
  89         filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
  90         default filter :: Sym_IsSequence (UnT term) => Trans term => IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
  91         filter = trans2 filter
  92
  93 -- Interpreting
  94 instance Sym_IsSequence Eval where
  95         filter  = eval2 Seqs.filter
  96 instance Sym_IsSequence View where
  97         filter  = view2 "filter"
  98 instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (Dup r1 r2) where
  99         filter  = dup2 @Sym_IsSequence filter
 100
 101 -- Transforming
 102 instance (Sym_IsSequence term, Sym_Lambda term) => Sym_IsSequence (BetaT term)
 103
 104 -- Typing
 105 instance FixityOf IsSequence
 106 instance ClassInstancesFor IsSequence
 107 instance TypeInstancesFor IsSequence
 108
 109 -- Compiling
 110 instance Gram_Term_AtomsFor src ss g IsSequence
 111 instance (Source src, SymInj ss IsSequence) => ModuleFor src ss IsSequence where
 112         moduleFor = ["IsSequence"] `moduleWhere`
 113          [ "filter" := teIsSequence_filter
 114          ]
 115
 116 -- ** 'Type's
 117 tyIsSequence :: Source src => Type src vs a -> Type src vs (IsSequence a)
 118 tyIsSequence a = tyConstLen @(K IsSequence) @IsSequence (lenVars a) `tyApp` a
 119
 120 -- ** 'Term's
 121 teIsSequence_filter :: TermDef IsSequence '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> ((e -> Bool) -> s -> s))
 122 teIsSequence_filter = Term (tyIsSequence s0 # e1 #~ famElement s0) ((e1 ~> tyBool) ~> s0 ~> s0) $ teSym @IsSequence $ lam2 filter