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