Add tar GNUmakefile target.

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

diff --git a/symantic-lib/Language/Symantic/Lib/Eq.hs b/symantic-lib/Language/Symantic/Lib/Eq.hs
index 2aa873062b1178289008fde8aad25183cf97c032..0aba6defda4b55a709c72d149d3560d8e5cae66c 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Eq.hs
+++ b/symantic-lib/Language/Symantic/Lib/Eq.hs
@@ -3,83 +3,59 @@
 -- | Symantic for 'Eq'.
 module Language.Symantic.Lib.Eq where
 
-import Control.Monad
-import qualified Data.Eq as Eq
-import Data.Proxy (Proxy(..))
 import Prelude hiding ((==), (/=))
+import qualified Data.Eq as Eq
 
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Lambda
+import Language.Symantic
+import Language.Symantic.Lib.Bool (tyBool)
+import Language.Symantic.Lib.Function (a0)
 
 -- * Class 'Sym_Eq'
+type instance Sym Eq = Sym_Eq
 class Sym_Eq term where
        (==) :: Eq a => term a -> term a -> term Bool; infix 4 ==
        (/=) :: Eq a => term a -> term a -> term Bool; infix 4 /=
        
-       default (==) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
-       default (/=) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
+       default (==) :: Sym_Eq (UnT term) => Trans term => Eq a => term a -> term a -> term Bool
+       default (/=) :: Sym_Eq (UnT term) => Trans term => Eq a => term a -> term a -> term Bool
        
-       (==) = trans_map2 (==)
-       (/=) = trans_map2 (/=)
+       (==) = trans2 (==)
+       (/=) = trans2 (/=)
+
+-- Interpreting
+instance Sym_Eq Eval where
+       (==) = eval2 (Eq.==)
+       (/=) = eval2 (Eq./=)
+instance Sym_Eq View where
+       (==) = viewInfix "==" (infixN 4)
+       (/=) = viewInfix "/=" (infixN 4)
+instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (Dup r1 r2) where
+       (==) = dup2 @Sym_Eq (==)
+       (/=) = dup2 @Sym_Eq (/=)
+
+-- Transforming
+instance (Sym_Eq term, Sym_Lambda term) => Sym_Eq (BetaT term)
 
-type instance Sym_of_Iface (Proxy Eq) = Sym_Eq
-type instance TyConsts_of_Iface (Proxy Eq) = Proxy Eq ': TyConsts_imported_by Eq
-type instance TyConsts_imported_by Eq = '[]
+-- Typing
+instance NameTyOf Eq where
+       nameTyOf _c = ["Eq"] `Mod` "Eq"
+instance FixityOf Eq
+instance ClassInstancesFor Eq
+instance TypeInstancesFor Eq
 
-instance Sym_Eq HostI where
-       (==) = liftM2 (Eq.==)
-       (/=) = liftM2 (Eq./=)
-instance Sym_Eq TextI where
-       (==) = textI_infix "==" (infixN 4)
-       (/=) = textI_infix "/=" (infixN 4)
-instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (DupI r1 r2) where
-       (==) = dupI2 (Proxy @Sym_Eq) (==)
-       (/=) = dupI2 (Proxy @Sym_Eq) (/=)
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Eq
+instance (Source src, SymInj ss Eq) => ModuleFor src ss Eq where
+       moduleFor = ["Eq"] `moduleWhere`
+        [ "==" `withInfixN` 4 := teEq_eq
+        , "/=" `withInfixN` 4 := teEq_ne
+        ]
 
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Eq
- ) => Read_TyNameR TyName cs (Proxy Eq ': rs) where
-       read_TyNameR _cs (TyName "Eq") k = k (ty @Eq)
-       read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Eq ': cs) where
-       show_TyConst TyConstZ{} = "Eq"
-       show_TyConst (TyConstS c) = show_TyConst c
+-- ** 'Type's
+tyEq :: Source src => Type src vs a -> Type src vs (Eq a)
+tyEq a = tyConstLen @(K Eq) @Eq (lenVars a) `tyApp` a
 
-instance Proj_TyConC cs (Proxy Eq)
-data instance TokenT meta (ts::[*]) (Proxy Eq)
- = Token_Term_Eq_eq (EToken meta ts)
- | Token_Term_Eq_ne (EToken meta ts)
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Eq))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Eq))
-instance -- CompileI
- ( Inj_TyConst (TyConsts_of_Ifaces is) Bool
- , Inj_TyConst (TyConsts_of_Ifaces is) (->)
- , Inj_TyConst (TyConsts_of_Ifaces is) Eq
- , Proj_TyCon (TyConsts_of_Ifaces is)
- , Compile is
- ) => CompileI is (Proxy Eq) where
-       compileI tok ctx k =
-               case tok of
-                Token_Term_Eq_eq tok_a -> from_op (==) tok_a
-                Token_Term_Eq_ne tok_a -> from_op (/=) tok_a
-               where
-               from_op (op::forall term a. (Sym_Eq term, Eq a) => term a -> term a -> term Bool) tok_a =
-                       compileO tok_a ctx $ \ty_a (TermO a) ->
-                       check_TyCon (At (Just tok_a) (ty @Eq :$ ty_a)) $ \TyCon ->
-                       k (ty_a ~> ty @Bool) $ TermO $
-                        \c -> lam $ op (a c)
-instance -- TokenizeT
- Inj_Token meta ts Eq =>
- TokenizeT meta ts (Proxy Eq) where
-       tokenizeT _t = mempty
-        { tokenizers_infix = tokenizeTMod []
-                [ tokenize1 "==" (infixN 4) Token_Term_Eq_eq
-                , tokenize1 "/=" (infixN 4) Token_Term_Eq_ne
-                ]
-        }
-instance Gram_Term_AtomsT meta ts (Proxy Eq) g
+-- ** 'Term's
+teEq_eq, teEq_ne :: TermDef Eq '[Proxy a] (Eq a #> (a -> a -> Bool))
+teEq_eq = Term (tyEq a0) (a0 ~> a0 ~> tyBool) $ teSym @Eq $ lam2 (==)
+teEq_ne = Term (tyEq a0) (a0 ~> a0 ~> tyBool) $ teSym @Eq $ lam2 (/=)