]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Integer.hs
Integrate types to the module system.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Integer.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Integer'.
4 module Language.Symantic.Lib.Integer where
5
6 import qualified Data.Text as Text
7
8 import Language.Symantic
9 import Language.Symantic.Grammar
10
11 -- * Class 'Sym_Integer'
12 type instance Sym Integer = Sym_Integer
13 class Sym_Integer term where
14 integer :: Integer -> term Integer
15 default integer :: Sym_Integer (UnT term) => Trans term => Integer -> term Integer
16 integer = trans . integer
17
18 -- Interpreting
19 instance Sym_Integer Eval where
20 integer = Eval
21 instance Sym_Integer View where
22 integer a = View $ \_p _v ->
23 Text.pack (show a)
24 instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (Dup r1 r2) where
25 integer x = integer x `Dup` integer x
26
27 -- Transforming
28 instance (Sym_Integer term, Sym_Lambda term) => Sym_Integer (BetaT term)
29
30 -- Typing
31 instance NameTyOf Integer where
32 nameTyOf _c = ["Integer"] `Mod` "Integer"
33 instance ClassInstancesFor Integer where
34 proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
35 | Just HRefl <- proj_ConstKiTy @_ @Integer z
36 = case () of
37 _ | Just Refl <- proj_Const @Enum q -> Just Dict
38 | Just Refl <- proj_Const @Eq q -> Just Dict
39 | Just Refl <- proj_Const @Integral q -> Just Dict
40 | Just Refl <- proj_Const @Num q -> Just Dict
41 | Just Refl <- proj_Const @Ord q -> Just Dict
42 | Just Refl <- proj_Const @Real q -> Just Dict
43 | Just Refl <- proj_Const @Show q -> Just Dict
44 _ -> Nothing
45 proveConstraintFor _c _q = Nothing
46 instance TypeInstancesFor Integer
47
48 -- Compiling
49 instance
50 ( Gram_Source src g
51 , Gram_Alt g
52 , Gram_AltApp g
53 , Gram_Rule g
54 , Gram_Comment g
55 , SymInj ss Integer
56 ) => Gram_Term_AtomsFor src ss g Integer where
57 g_term_atomsFor =
58 [ rule "teinteger" $
59 lexeme $ source $
60 (\i src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teInteger $ read i)
61 <$> some (choice $ char <$> ['0'..'9'])
62 ]
63 instance ModuleFor src ss Integer
64
65 -- ** 'Term's
66 tyInteger :: Source src => LenInj vs => Type src vs Integer
67 tyInteger = tyConst @(K Integer) @Integer
68
69 teInteger :: Source src => SymInj ss Integer => Integer -> Term src ss ts '[] (() #> Integer)
70 teInteger i = Term noConstraint tyInteger $ teSym @Integer $ integer i