Language/Symantic/Compiling/Int.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=6 #-}
  14 -- | Symantic for 'Int'.
  15 module Language.Symantic.Compiling.Int 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_Int'
  30 class Sym_Int term where
  31         int :: Int -> term Int
  32         default int :: Trans t term => Int -> t term Int
  33         int = trans_lift . int
  34
  35 type instance Sym_of_Iface (Proxy Int) = Sym_Int
  36 type instance Consts_of_Iface (Proxy Int) = Proxy Int ': Consts_imported_by Int
  37 type instance Consts_imported_by Int =
  38  [ Proxy Bounded
  39  , Proxy Enum
  40  , Proxy Eq
  41  , Proxy Integral
  42  , Proxy Num
  43  , Proxy Ord
  44  , Proxy Real
  45  ]
  46
  47 instance Sym_Int HostI where
  48         int = HostI
  49 instance Sym_Int TextI where
  50         int a = TextI $ \_p _v ->
  51                 Text.pack (show a)
  52 instance (Sym_Int r1, Sym_Int r2) => Sym_Int (DupI r1 r2) where
  53         int x = int x `DupI` int x
  54
  55 instance Const_from Text cs => Const_from Text (Proxy Int ': cs) where
  56         const_from "Int" k = k (ConstZ kind)
  57         const_from s k = const_from s $ k . ConstS
  58 instance Show_Const cs => Show_Const (Proxy Int ': cs) where
  59         show_const ConstZ{} = "Int"
  60         show_const (ConstS c) = show_const c
  61
  62 instance -- Proj_ConC
  63  ( Proj_Const cs Int
  64  , Proj_Consts cs (Consts_imported_by Int)
  65  ) => Proj_ConC cs (Proxy Int) where
  66         proj_conC _ (TyConst q :$ TyConst c)
  67          | Just Refl <- eq_skind (kind_of_const c) SKiType
  68          , Just Refl <- proj_const c (Proxy::Proxy Int)
  69          = Just $ case () of
  70                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded)  -> Just Con
  71                    | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Con
  72                    | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Con
  73                    | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Con
  74                    | Just Refl <- proj_const q (Proxy::Proxy Num)      -> Just Con
  75                    | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Con
  76                    | Just Refl <- proj_const q (Proxy::Proxy Real)     -> Just Con
  77                  _ -> Nothing
  78         proj_conC _c _q = Nothing
  79 instance -- Term_fromI
  80  ( AST ast
  81  , Lexem ast ~ LamVarName
  82  , Inj_Const (Consts_of_Ifaces is) Int
  83  , Show_Const (Consts_of_Ifaces is)
  84  ) => Term_fromI is (Proxy Int) ast where
  85         term_fromI ast _ctx k =
  86                 case ast_lexem ast of
  87                  "int" -> int_from
  88                  _ -> Left $ Error_Term_unsupported
  89                 where
  90                 int_from =
  91                         let ty = tyInt in
  92                         from_ast1 ast $ \ast_lit as ->
  93                         from_lex (Text.pack $ show_type ty) ast_lit $ \(lit::Int) ->
  94                         k as ty $ TermLC $ Fun.const $ int lit
  95
  96 -- | The 'Int' 'Type'
  97 tyInt :: Inj_Const cs Int => Type cs Int
  98 tyInt = TyConst inj_const
  99
 100 sym_Int :: Proxy Sym_Int
 101 sym_Int = Proxy
 102
 103 syInt :: IsString a => Syntax a
 104 syInt = Syntax "Int" []