]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Int.hs
Add TyApp pattern synonyms (:$) and (:@).
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Int.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Int'.
4 module Language.Symantic.Lib.Int where
5
6 import qualified Data.Text as Text
7
8 import Language.Symantic
9
10 -- * Class 'Sym_Int'
11 type instance Sym Int = Sym_Int
12 class Sym_Int term where
13 int :: Int -> term Int
14 default int :: Sym_Int (UnT term) => Trans term => Int -> term Int
15 int = trans . int
16
17 -- Interpreting
18 instance Sym_Int Eval where
19 int = Eval
20 instance Sym_Int View where
21 int a = View $ \_p _v ->
22 Text.pack (show a)
23 instance (Sym_Int r1, Sym_Int r2) => Sym_Int (Dup r1 r2) where
24 int x = int x `Dup` int x
25
26 -- Transforming
27 instance (Sym_Int term, Sym_Lambda term) => Sym_Int (BetaT term)
28
29 -- Typing
30 instance NameTyOf Int where
31 nameTyOf _c = ["Int"] `Mod` "Int"
32 instance ClassInstancesFor Int where
33 proveConstraintFor _c (TyConst _ _ q :$ z)
34 | Just HRefl <- proj_ConstKiTy @_ @Int z
35 = case () of
36 _ | Just Refl <- proj_Const @Bounded q -> Just Dict
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 Int
47
48 -- Compiling
49 instance Gram_Term_AtomsFor src ss g Int
50 instance ModuleFor src ss Int
51
52 -- ** 'Type's
53 tyInt :: Source src => LenInj vs => Type src vs Int
54 tyInt = tyConst @(K Int) @Int
55
56 -- ** 'Term's
57 teInt :: Source src => SymInj ss Int => Int -> Term src ss ts '[] (() #> Int)
58 teInt i = Term noConstraint tyInt $ teSym @Int $ int i