]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Integer.hs
Add tests for Compiling.
[haskell/symantic.git] / Language / Symantic / Compiling / Integer.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE DefaultSignatures #-}
3 {-# LANGUAGE FlexibleContexts #-}
4 {-# LANGUAGE FlexibleInstances #-}
5 {-# LANGUAGE MultiParamTypeClasses #-}
6 {-# LANGUAGE OverloadedStrings #-}
7 {-# LANGUAGE Rank2Types #-}
8 {-# LANGUAGE ScopedTypeVariables #-}
9 {-# LANGUAGE TypeFamilies #-}
10 {-# LANGUAGE TypeOperators #-}
11 {-# LANGUAGE UndecidableInstances #-}
12 {-# OPTIONS_GHC -fno-warn-orphans #-}
13 {-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
14 -- | Symantic for 'Integer'.
15 module Language.Symantic.Compiling.Integer where
16
17 import qualified Data.Function as Fun
18 import Data.Proxy
19 import Data.String (IsString)
20 import Data.Text (Text)
21 import qualified Data.Text as Text
22 import Data.Type.Equality ((:~:)(Refl))
23
24 import Language.Symantic.Typing
25 import Language.Symantic.Compiling.Term
26 import Language.Symantic.Interpreting
27 import Language.Symantic.Transforming.Trans
28
29 -- * Class 'Sym_Integer'
30 class Sym_Integer term where
31 integer :: Integer -> term Integer
32 default integer :: Trans t term => Integer -> t term Integer
33 integer = trans_lift . integer
34
35 type instance Sym_of_Iface (Proxy Integer) = Sym_Integer
36 type instance Consts_of_Iface (Proxy Integer) = Proxy Integer ': Consts_imported_by Integer
37 type instance Consts_imported_by Integer =
38 [ Proxy Enum
39 , Proxy Eq
40 , Proxy Integral
41 , Proxy Num
42 , Proxy Ord
43 , Proxy Real
44 ]
45
46 instance Sym_Integer HostI where
47 integer = HostI
48 instance Sym_Integer TextI where
49 integer a = TextI $ \_p _v ->
50 Text.pack (show a)
51 instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (DupI r1 r2) where
52 integer x = integer x `DupI` integer x
53
54 instance Const_from Text cs => Const_from Text (Proxy Integer ': cs) where
55 const_from "Integer" k = k (ConstZ kind)
56 const_from s k = const_from s $ k . ConstS
57 instance Show_Const cs => Show_Const (Proxy Integer ': cs) where
58 show_const ConstZ{} = "Integer"
59 show_const (ConstS c) = show_const c
60
61 instance -- Proj_ConC
62 ( Proj_Const cs Integer
63 , Proj_Consts cs (Consts_imported_by Integer)
64 ) => Proj_ConC cs (Proxy Integer) where
65 proj_conC _ (TyConst q :$ TyConst c)
66 | Just Refl <- eq_skind (kind_of_const c) SKiType
67 , Just Refl <- proj_const c (Proxy::Proxy Integer)
68 = Just $ case () of
69 _ | Just Refl <- proj_const q (Proxy::Proxy Enum) -> Just Con
70 | Just Refl <- proj_const q (Proxy::Proxy Eq) -> Just Con
71 | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Con
72 | Just Refl <- proj_const q (Proxy::Proxy Num) -> Just Con
73 | Just Refl <- proj_const q (Proxy::Proxy Ord) -> Just Con
74 | Just Refl <- proj_const q (Proxy::Proxy Real) -> Just Con
75 _ -> Nothing
76 proj_conC _c _q = Nothing
77 instance -- Term_fromI
78 ( AST ast
79 , Lexem ast ~ LamVarName
80 , Inj_Const (Consts_of_Ifaces is) Integer
81 , Show_Const (Consts_of_Ifaces is)
82 ) => Term_fromI is (Proxy Integer) ast where
83 term_fromI ast _ctx k =
84 case ast_lexem ast of
85 "integer" -> integer_from
86 _ -> Left $ Error_Term_unsupported
87 where
88 integer_from =
89 let ty = tyInteger in
90 from_ast1 ast $ \ast_lit as ->
91 from_lex (Text.pack $ show_type ty) ast_lit $ \(lit::Integer) ->
92 k as ty $ TermLC $ Fun.const $ integer lit
93
94 -- | The 'Integer' 'Type'
95 tyInteger :: Inj_Const cs Integer => Type cs Integer
96 tyInteger = TyConst inj_const
97
98 sym_Integer :: Proxy Sym_Integer
99 sym_Integer = Proxy
100
101 syInteger :: IsString a => Syntax a
102 syInteger = Syntax "Integer" []