Archive old attempt to remove proto tokens without polymorphic types.

[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Functor.hs

diff --git a/symantic-lib/Language/Symantic/Lib/Functor.hs b/symantic-lib/Language/Symantic/Lib/Functor.hs
index 7efe890fb44c3e2c1d644faf5b106b8c4778660b..dcb7c3db8408f0491e5d242e14f765c4a2bf8c32 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Functor.hs
+++ b/symantic-lib/Language/Symantic/Lib/Functor.hs
@@ -4,12 +4,12 @@
 module Language.Symantic.Lib.Functor where
 
 import Control.Monad (liftM2)
-import qualified Data.Function as Fun
 import Data.Functor (Functor)
-import qualified Data.Functor as Functor
 import Data.Proxy (Proxy(..))
 import Data.Type.Equality
 import Prelude hiding (Functor(..))
+import qualified Data.Function as Fun
+import qualified Data.Functor as Functor
 
 import Language.Symantic.Parsing
 import Language.Symantic.Typing
@@ -33,8 +33,8 @@ class Sym_Lambda term => Sym_Functor term where
 
 
 type instance Sym_of_Iface (Proxy Functor) = Sym_Functor
-type instance TyConsts_of_Iface (Proxy Functor) = Proxy Functor ': TyConsts_imported_by Functor
-type instance TyConsts_imported_by Functor = '[]
+type instance TyConsts_of_Iface (Proxy Functor) = Proxy Functor ': TyConsts_imported_by (Proxy Functor)
+type instance TyConsts_imported_by (Proxy Functor) = '[]
 
 instance Sym_Functor HostI where
        fmap = liftM2 Functor.fmap
@@ -43,8 +43,8 @@ instance Sym_Functor TextI where
        fmap = textI2 "fmap"
        (<$) = textI_infix "<$" (infixL 4)
 instance (Sym_Functor r1, Sym_Functor r2) => Sym_Functor (DupI r1 r2) where
-       fmap = dupI2 (Proxy @Sym_Functor) fmap
-       (<$) = dupI2 (Proxy @Sym_Functor) (<$)
+       fmap = dupI2 @Sym_Functor fmap
+       (<$) = dupI2 @Sym_Functor (<$)
 
 -- | 'fmap' alias.
 (<$>) :: (Sym_Functor term, Functor f)
@@ -68,18 +68,19 @@ data instance TokenT meta (ts::[*]) (Proxy Functor)
  | Token_Term_Functor_const (EToken meta ts) (EToken meta ts)
 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Functor))
 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Functor))
+
 instance -- CompileI
- ( Inj_TyConst  (TyConsts_of_Ifaces is) Functor
- , Inj_TyConst  (TyConsts_of_Ifaces is) (->)
- , Proj_TyCon   (TyConsts_of_Ifaces is)
- , Compile is
- ) => CompileI is (Proxy Functor) where
+ ( Inj_TyConst cs Functor
+ , Inj_TyConst cs (->)
+ , Proj_TyCon  cs
+ , Compile cs is
+ ) => CompileI cs is (Proxy Functor) where
        compileI tok ctx k =
                case tok of
                 Token_Term_Functor_fmap tok_a2b tok_fa ->
                        -- fmap :: Functor f => (a -> b) -> f a -> f b
-                       compileO tok_a2b ctx $ \ty_a2b (TermO a2b) ->
-                       compileO tok_fa  ctx $ \ty_fa  (TermO fa) ->
+                       compile tok_a2b ctx $ \ty_a2b (Term a2b) ->
+                       compile tok_fa  ctx $ \ty_fa  (Term fa) ->
                        check_TyEq2 (ty @(->))
                         (At (Just tok_a2b) ty_a2b) $ \Refl ty_a2b_a ty_a2b_b ->
                        check_TyCon1 (ty @Functor)
@@ -87,15 +88,15 @@ instance -- CompileI
                        check_TyEq
                         (At (Just tok_a2b) ty_a2b_a)
                         (At (Just tok_fa) ty_fa_a) $ \Refl ->
-                       k (ty_fa_f :$ ty_a2b_b) $ TermO $
+                       k (ty_fa_f :$ ty_a2b_b) $ Term $
                         \c -> fmap (a2b c) (fa c)
                 Token_Term_Functor_const tok_a tok_fb ->
                        -- (<$) :: Functor f => a -> f b -> f a
-                       compileO tok_a  ctx $ \ty_a  (TermO a) ->
-                       compileO tok_fb ctx $ \ty_fb (TermO fb) ->
+                       compile tok_a  ctx $ \ty_a  (Term a) ->
+                       compile tok_fb ctx $ \ty_fb (Term fb) ->
                        check_TyCon1 (ty @Functor)
                         (At (Just tok_fb) ty_fb) $ \Refl TyCon ty_fb_f _ty_fb_b ->
-                       k (ty_fb_f :$ ty_a) $ TermO $
+                       k (ty_fb_f :$ ty_a) $ Term $
                         \c -> (<$) (a c) (fb c)
 instance -- TokenizeT
  Inj_Token meta ts Functor =>