Make stack flags customizable in GNUmakefile.

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

diff --git a/symantic-lib/Language/Symantic/Lib/Int.hs b/symantic-lib/Language/Symantic/Lib/Int.hs
index d9734e5fe7ba494d50066a7a0e63b2b227abc142..d1b2b29ce92571433dac50be1893f6f5461db3db 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Int.hs
+++ b/symantic-lib/Language/Symantic/Lib/Int.hs
@@ -1,87 +1,58 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
 -- | Symantic for 'Int'.
 module Language.Symantic.Lib.Int where
 
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
 import qualified Data.Text as Text
 
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
+import Language.Symantic
 
 -- * Class 'Sym_Int'
+type instance Sym Int = Sym_Int
 class Sym_Int term where
        int :: Int -> term Int
-       default int :: Trans t term => Int -> t term Int
-       int = trans_lift . int
-
-type instance Sym_of_Iface (Proxy Int) = Sym_Int
-type instance TyConsts_of_Iface (Proxy Int) = Proxy Int ': TyConsts_imported_by (Proxy Int)
-type instance TyConsts_imported_by (Proxy Int) =
- [ Proxy Bounded
- , Proxy Enum
- , Proxy Eq
- , Proxy Integral
- , Proxy Num
- , Proxy Ord
- , Proxy Real
- , Proxy Show
- ]
-
-instance Sym_Int HostI where
-       int = HostI
-instance Sym_Int TextI where
-       int a = TextI $ \_p _v ->
+       default int :: Sym_Int (UnT term) => Trans term => Int -> term Int
+       int = trans . int
+
+-- Interpreting
+instance Sym_Int Eval where
+       int = Eval
+instance Sym_Int View where
+       int a = View $ \_p _v ->
                Text.pack (show a)
-instance (Sym_Int r1, Sym_Int r2) => Sym_Int (DupI r1 r2) where
-       int x = int x `DupI` int x
-
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Int
- ) => Read_TyNameR TyName cs (Proxy Int ': rs) where
-       read_TyNameR _cs (TyName "Int") k = k (ty @Int)
-       read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Int ': cs) where
-       show_TyConst TyConstZ{} = "Int"
-       show_TyConst (TyConstS c) = show_TyConst c
-
-instance Proj_TyFamC cs TyFam_MonoElement Int
-
-instance -- Proj_TyConC
- ( Proj_TyConst cs Int
- , Proj_TyConsts cs (TyConsts_imported_by (Proxy Int))
- ) => Proj_TyConC cs (Proxy Int) where
-       proj_TyConC _ (TyConst q :$ TyConst c)
-        | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
-        , Just Refl <- proj_TyConst c (Proxy @Int)
+instance (Sym_Int r1, Sym_Int r2) => Sym_Int (Dup r1 r2) where
+       int x = int x `Dup` int x
+
+-- Transforming
+instance (Sym_Int term, Sym_Lambda term) => Sym_Int (BetaT term)
+
+-- Typing
+instance NameTyOf Int where
+       nameTyOf _c = ["Int"] `Mod` "Int"
+instance ClassInstancesFor Int where
+       proveConstraintFor _c (TyApp _ (TyConst _ _ q) z)
+        | Just HRefl <- proj_ConstKiTy @_ @Int z
         = case () of
-                _ | Just Refl <- proj_TyConst q (Proxy @Bounded)  -> Just TyCon
-                  | Just Refl <- proj_TyConst q (Proxy @Enum)     -> Just TyCon
-                  | Just Refl <- proj_TyConst q (Proxy @Eq)       -> Just TyCon
-                  | Just Refl <- proj_TyConst q (Proxy @Integral) -> Just TyCon
-                  | Just Refl <- proj_TyConst q (Proxy @Num)      -> Just TyCon
-                  | Just Refl <- proj_TyConst q (Proxy @Ord)      -> Just TyCon
-                  | Just Refl <- proj_TyConst q (Proxy @Real)     -> Just TyCon
-                  | Just Refl <- proj_TyConst q (Proxy @Show)     -> Just TyCon
+                _ | Just Refl <- proj_Const @Bounded  q -> Just Dict
+                  | Just Refl <- proj_Const @Enum     q -> Just Dict
+                  | Just Refl <- proj_Const @Eq       q -> Just Dict
+                  | Just Refl <- proj_Const @Integral q -> Just Dict
+                  | Just Refl <- proj_Const @Num      q -> Just Dict
+                  | Just Refl <- proj_Const @Ord      q -> Just Dict
+                  | Just Refl <- proj_Const @Real     q -> Just Dict
+                  | Just Refl <- proj_Const @Show     q -> Just Dict
                 _ -> Nothing
-       proj_TyConC _c _q = Nothing
-data instance TokenT meta (ts::[*]) (Proxy Int)
- = Token_Term_Int Int
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Int))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Int))
+       proveConstraintFor _c _q = Nothing
+instance TypeInstancesFor Int
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Int
+instance ModuleFor src ss Int
+
+-- ** 'Type's
+tyInt :: Source src => LenInj vs => Type src vs Int
+tyInt = tyConst @(K Int) @Int
 
-instance -- CompileI
- Inj_TyConst cs Int =>
- CompileI cs is (Proxy Int) where
-       compileI tok _ctx k =
-               case tok of
-                Token_Term_Int i -> k (ty @Int) $ Term $ \_c -> int i
-instance TokenizeT meta ts (Proxy Int)
-instance Gram_Term_AtomsT meta ts (Proxy Int) g
+-- ** 'Term's
+teInt :: Source src => SymInj ss Int => Int -> Term src ss ts '[] (() #> Int)
+teInt i = Term noConstraint tyInt $ teSym @Int $ int i