Remove dependency on ghc-prim.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Sequences.hs
index 41fbf96af91a165f374386a2b2b07533bae853a4..7257d18dcf5d9b96a89a50b73019d2d789b0b2bf 100644 (file)
@@ -14,7 +14,7 @@ import Language.Symantic.Lib.Bool (tyBool)
 import Language.Symantic.Lib.MonoFunctor (e1, famElement)
 
 -- * Class 'Sym_SemiSequence'
-type instance Sym (Proxy SemiSequence) = Sym_SemiSequence
+type instance Sym SemiSequence = Sym_SemiSequence
 class Sym_SemiSequence term where
        intersperse :: SemiSequence s => term (MT.Element s) -> term s -> term s
        cons        :: SemiSequence s => term (MT.Element s) -> term s -> term s
@@ -50,14 +50,16 @@ instance (Sym_SemiSequence r1, Sym_SemiSequence r2) => Sym_SemiSequence (Dup r1
 instance (Sym_SemiSequence term, Sym_Lambda term) => Sym_SemiSequence (BetaT term)
 
 -- Typing
+instance NameTyOf SemiSequence where
+       nameTyOf _c = ["SemiSequence"] `Mod` "SemiSequence"
 instance FixityOf SemiSequence
 instance ClassInstancesFor SemiSequence
 instance TypeInstancesFor SemiSequence
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g SemiSequence
-instance (Source src, Inj_Sym ss SemiSequence) => ModuleFor src ss SemiSequence where
-       moduleFor _s = ["SemiSequence"] `moduleWhere`
+instance (Source src, SymInj ss SemiSequence) => ModuleFor src ss SemiSequence where
+       moduleFor = ["SemiSequence"] `moduleWhere`
         [ "intersperse" := teSemiSequence_intersperse
         , "cons"        := teSemiSequence_cons
         , "snoc"        := teSemiSequence_snoc
@@ -68,7 +70,7 @@ instance (Source src, Inj_Sym ss SemiSequence) => ModuleFor src ss SemiSequence
 tySemiSequence :: Source src => Type src vs a -> Type src vs (SemiSequence a)
 tySemiSequence a = tyConstLen @(K SemiSequence) @SemiSequence (lenVars a) `tyApp` a
 
-s0 :: Source src => Inj_Len vs => Inj_Kind (K s) =>
+s0 :: Source src => LenInj vs => KindInj (K s) =>
       Type src (Proxy s ': vs) s
 s0 = tyVar "s" varZ
 
@@ -84,7 +86,7 @@ teSemiSequence_snoc :: TermDef SemiSequence '[Proxy s, Proxy e] (SemiSequence s
 teSemiSequence_snoc = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> e1 ~> s0) $ teSym @SemiSequence $ lam2 snoc
 
 -- * Class 'Sym_IsSequence'
-type instance Sym (Proxy IsSequence) = Sym_IsSequence
+type instance Sym IsSequence = Sym_IsSequence
 class Sym_IsSequence term where
        filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
        default filter :: Sym_IsSequence (UnT term) => Trans term => IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
@@ -102,14 +104,16 @@ instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (Dup r1 r2) wh
 instance (Sym_IsSequence term, Sym_Lambda term) => Sym_IsSequence (BetaT term)
 
 -- Typing
+instance NameTyOf IsSequence where
+       nameTyOf _c = ["IsSequence"] `Mod` "IsSequence"
 instance FixityOf IsSequence
 instance ClassInstancesFor IsSequence
 instance TypeInstancesFor IsSequence
 
 -- Compiling
 instance Gram_Term_AtomsFor src ss g IsSequence
-instance (Source src, Inj_Sym ss IsSequence) => ModuleFor src ss IsSequence where
-       moduleFor _s = ["IsSequence"] `moduleWhere`
+instance (Source src, SymInj ss IsSequence) => ModuleFor src ss IsSequence where
+       moduleFor = ["IsSequence"] `moduleWhere`
         [ "filter" := teIsSequence_filter
         ]