Add symantic-document.

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

diff --git a/symantic-lib/Language/Symantic/Lib/Real.hs b/symantic-lib/Language/Symantic/Lib/Real.hs
index 1c46b43038ba2bd9697836ab8eb51ab9128be864..853fde5641cac7193b95a3d28982513095a0da7b 100644 (file)
--- a/symantic-lib/Language/Symantic/Lib/Real.hs
+++ b/symantic-lib/Language/Symantic/Lib/Real.hs
@@ -1,79 +1,54 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
 -- | Symantic for 'Real'.
 module Language.Symantic.Lib.Real where
 
-import Control.Monad (liftM)
-import Data.Proxy
-import Data.Ratio (Ratio)
 import Prelude (Real)
 import Prelude hiding (Real(..))
 import qualified Prelude
 
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
+import Language.Symantic
+import Language.Symantic.Lib.Function (a0)
+import Language.Symantic.Lib.Integer (tyInteger)
+import Language.Symantic.Lib.Ratio (tyRatio)
 
 -- * Class 'Sym_Real'
+type instance Sym (Proxy Real) = Sym_Real
 class Sym_Real term where
        toRational :: Real a => term a -> term Rational
-       default toRational :: (Trans t term, Real a) => t term a -> t term Rational
-       toRational = trans_map1 toRational
-
-type instance Sym_of_Iface (Proxy Real) = Sym_Real
-type instance TyConsts_of_Iface (Proxy Real) = Proxy Real ': TyConsts_imported_by (Proxy Real)
-type instance TyConsts_imported_by (Proxy Real) =
- [ Proxy Ratio
- , Proxy Integer
- ]
-
-instance Sym_Real HostI where
-       toRational = liftM  Prelude.toRational
-instance Sym_Real TextI where
-       toRational = textI1 "toRational"
-instance (Sym_Real r1, Sym_Real r2) => Sym_Real (DupI r1 r2) where
-       toRational = dupI1 @Sym_Real toRational
-
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Real
- ) => Read_TyNameR TyName cs (Proxy Real ': rs) where
-       read_TyNameR _cs (TyName "Real") k = k (ty @Real)
-       read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Real ': cs) where
-       show_TyConst TyConstZ{} = "Real"
-       show_TyConst (TyConstS c) = show_TyConst c
-
-instance Proj_TyConC cs (Proxy Real)
-data instance TokenT meta (ts::[*]) (Proxy Real)
- =  Token_Term_Real (EToken meta ts)
-deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Real))
-deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Real))
-
-instance -- CompileI
- ( Read_TyName TyName cs
- , Inj_TyConst cs Real
- , Inj_TyConsts cs (TyConsts_imported_by (Proxy Real))
- , Proj_TyCon cs
- , Compile cs is
- ) => CompileI cs is (Proxy Real) where
-       compileI tok ctx k =
-               case tok of
-                Token_Term_Real tok_a ->
-                       -- toRational :: a -> Rational
-                       compileO tok_a ctx $ \ty_a (TermO a) ->
-                       check_TyCon (At (Just tok_a) (ty @Real :$ ty_a)) $ \TyCon ->
-                       k (ty @Ratio :$ ty @Integer) $ TermO $
-                        \c -> toRational (a c)
-instance -- TokenizeT
- Inj_Token meta ts Real =>
- TokenizeT meta ts (Proxy Real) where
-       tokenizeT _t = mempty
-        { tokenizers_infix = tokenizeTMod []
-                [ tokenize1 "toRational" infixN5 Token_Term_Real
-                ]
-        }
-instance Gram_Term_AtomsT meta ts (Proxy Real) g
+       default toRational :: Sym_Real (UnT term) => Trans term => Real a => term a -> term Rational
+       toRational = trans1 toRational
+
+-- Interpreting
+instance Sym_Real Eval where
+       toRational = eval1 Prelude.toRational
+instance Sym_Real View where
+       toRational = view1 "toRational"
+instance (Sym_Real r1, Sym_Real r2) => Sym_Real (Dup r1 r2) where
+       toRational = dup1 @Sym_Real toRational
+
+-- Transforming
+instance (Sym_Real term, Sym_Lambda term) => Sym_Real (BetaT term)
+
+-- Typing
+instance FixityOf Real
+instance ClassInstancesFor Real
+instance TypeInstancesFor Real
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Real
+instance (Source src, Inj_Sym ss Real) => ModuleFor src ss Real where
+       moduleFor _s = ["Real"] `moduleWhere`
+        [ "toRational" := teReal_toRational
+        ]
+
+-- ** 'Type's
+tyReal :: Source src => Type src vs a -> Type src vs (Real a)
+tyReal a = tyConstLen @(K Real) @Real (lenVars a) `tyApp` a
+
+tyRational :: Source src => Inj_Len vs => Type src vs Rational
+tyRational = tyRatio tyInteger
+
+-- ** 'Term's
+teReal_toRational :: TermDef Real '[Proxy a] (Real a #> (a -> Rational))
+teReal_toRational = Term (tyReal a0) (a0 ~> tyRational) $ teSym @Real $ lam1 toRational