Archive old attempt to remove proto tokens without polymorphic types.

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

diff --git a/symantic-lib/Language/Symantic/Lib/Monoid.hs b/symantic-lib/Language/Symantic/Lib/Monoid.hs
index 41e878a669fc9aeadbd6636f636e2d7a418e6a52..211ca42309a103b4481337a84c0347c0264f3047 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Monoid.hs
+++ b/symantic-lib/Language/Symantic/Lib/Monoid.hs
@@ -4,12 +4,12 @@
 module Language.Symantic.Lib.Monoid where
 
 import Control.Monad
-import qualified Data.Function as Fun
 import Data.Monoid (Monoid)
-import qualified Data.Monoid as Monoid
 import Data.Proxy
 import Data.Type.Equality ((:~:)(Refl))
 import Prelude hiding (Monoid(..))
+import qualified Data.Function as Fun
+import qualified Data.Monoid as Monoid
 
 import Language.Symantic.Parsing
 import Language.Symantic.Typing
@@ -28,8 +28,8 @@ class Sym_Monoid term where
        mappend = trans_map2 mappend
 
 type instance Sym_of_Iface (Proxy Monoid) = Sym_Monoid
-type instance TyConsts_of_Iface (Proxy Monoid) = Proxy Monoid ': TyConsts_imported_by Monoid
-type instance TyConsts_imported_by Monoid = '[]
+type instance TyConsts_of_Iface (Proxy Monoid) = Proxy Monoid ': TyConsts_imported_by (Proxy Monoid)
+type instance TyConsts_imported_by (Proxy Monoid) = '[]
 
 instance Sym_Monoid HostI where
        mempty  = HostI Monoid.mempty
@@ -57,38 +57,39 @@ data instance TokenT meta (ts::[*]) (Proxy Monoid)
  | Token_Term_Monoid_mappend (EToken meta ts)
 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monoid))
 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monoid))
+
 instance -- CompileI
- ( Read_TyName TyName (TyConsts_of_Ifaces is)
- , Inj_TyConst (TyConsts_of_Ifaces is) Monoid
- , Inj_TyConst (TyConsts_of_Ifaces is) (->)
- , Proj_TyCon  (TyConsts_of_Ifaces is)
- , Compile is
- ) => CompileI is (Proxy Monoid) where
+ ( Read_TyName TyName cs
+ , Inj_TyConst        cs Monoid
+ , Inj_TyConst        cs (->)
+ , Proj_TyCon         cs
+ , Compile cs is
+ ) => CompileI cs is (Proxy Monoid) where
        compileI tok ctx k =
                case tok of
                 Token_Term_Monoid_mempty tok_ty_a ->
                        -- mempty :: Monoid a => a
-                       compile_Type tok_ty_a $ \(ty_a::Type (TyConsts_of_Ifaces is) a) ->
+                       compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
                        check_Kind
                         (At Nothing SKiType)
                         (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
                        check_TyCon (At (Just tok_ty_a) (ty @Monoid :$ ty_a)) $ \TyCon ->
-                       k ty_a $ TermO $ Fun.const mempty
+                       k ty_a $ Term $ Fun.const mempty
                 Token_Term_Monoid_mappend tok_a ->
                        -- mappend :: Monoid a => a -> a -> a
-                       compileO tok_a ctx $ \ty_a (TermO x) ->
+                       compile tok_a ctx $ \ty_a (Term x) ->
                        check_TyCon (At (Just tok_a) (ty @Monoid :$ ty_a)) $ \TyCon ->
-                       k (ty_a ~> ty_a) $ TermO $
+                       k (ty_a ~> ty_a) $ Term $
                         \c -> lam $ \y -> mappend (x c) y
 instance -- TokenizeT
  Inj_Token meta ts Monoid =>
  TokenizeT meta ts (Proxy Monoid) where
        tokenizeT _t = Monoid.mempty
         { tokenizers_infix = tokenizeTMod []
-                [ (Term_Name "mempty",) Term_ProTok
-                        { term_protok = \meta -> ProTokPi $ \a ->
-                               ProTok $ inj_EToken meta $ Token_Term_Monoid_mempty a
-                        , term_fixity = infixN5
+                [ (TeName "mempty",) ProTok_Term
+                        { protok_term = \meta -> ProTokPi $ \a ->
+                               ProTokTe $ inj_EToken meta $ Token_Term_Monoid_mempty a
+                        , protok_fixity = infixN5
                         }
                 , tokenize1 "mappend" infixN5 Token_Term_Monoid_mappend
                 ]