Language/Symantic/Compiling/Char.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 -- | Symantic for 'Char'.
  14 module Language.Symantic.Compiling.Char where
  15
  16 import Control.Monad (liftM)
  17 import qualified Data.Char as Char
  18 import qualified Data.Function as Fun
  19 import Data.Proxy
  20 import Data.String (IsString)
  21 import Data.Text (Text)
  22 import qualified Data.Text as Text
  23 import Data.Type.Equality ((:~:)(Refl))
  24
  25 import Language.Symantic.Typing
  26 import Language.Symantic.Compiling.Term
  27 import Language.Symantic.Interpreting
  28 import Language.Symantic.Transforming.Trans
  29
  30 -- * Class 'Sym_Char'
  31 class Sym_Char term where
  32         char :: Char -> term Char
  33         char_toUpper :: term Char -> term Char
  34
  35         default char :: Trans t term => Char -> t term Char
  36         default char_toUpper :: Trans t term => t term Char -> t term Char
  37
  38         char = trans_lift . char
  39         char_toUpper = trans_map1 char_toUpper
  40
  41 type instance Sym_of_Iface (Proxy Char) = Sym_Char
  42 type instance Consts_of_Iface (Proxy Char) = Proxy Char ': Consts_imported_by Char
  43 type instance Consts_imported_by Char =
  44  [ Proxy Bounded
  45  , Proxy Enum
  46  , Proxy Eq
  47  , Proxy Ord
  48  ]
  49
  50 instance Sym_Char HostI where
  51         char = HostI
  52         char_toUpper = liftM Char.toUpper
  53 instance Sym_Char TextI where
  54         char a = TextI $ \_p _v ->
  55                 Text.pack (show a)
  56         char_toUpper = textI_app1 "char_toUpper"
  57 instance (Sym_Char r1, Sym_Char r2) => Sym_Char (DupI r1 r2) where
  58         char x = char x `DupI` char x
  59         char_toUpper = dupI1 sym_Char char_toUpper
  60
  61 instance Const_from Text cs => Const_from Text (Proxy Char ': cs) where
  62         const_from "Char" k = k (ConstZ kind)
  63         const_from s k = const_from s $ k . ConstS
  64 instance Show_Const cs => Show_Const (Proxy Char ': cs) where
  65         show_const ConstZ{} = "Char"
  66         show_const (ConstS c) = show_const c
  67
  68 instance -- Proj_ConC
  69  ( Proj_Const cs Char
  70  , Proj_Consts cs (Consts_imported_by Char)
  71  ) => Proj_ConC cs (Proxy Char) where
  72         proj_conC _ (TyConst q :$ TyConst c)
  73          | Just Refl <- eq_skind (kind_of_const c) SKiType
  74          , Just Refl <- proj_const c (Proxy::Proxy Char)
  75          = Just $ case () of
  76                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded) -> Just Con
  77                    | Just Refl <- proj_const q (Proxy::Proxy Enum)    -> Just Con
  78                    | Just Refl <- proj_const q (Proxy::Proxy Eq)      -> Just Con
  79                    | Just Refl <- proj_const q (Proxy::Proxy Ord)     -> Just Con
  80                  _ -> Nothing
  81         proj_conC _c _q = Nothing
  82 instance -- Term_fromI
  83  ( AST ast
  84  , Lexem ast ~ LamVarName
  85  , Inj_Const (Consts_of_Ifaces is) Char
  86  , Inj_Const (Consts_of_Ifaces is) (->)
  87  , Show_Const (Consts_of_Ifaces is)
  88  , Term_from is ast
  89  ) => Term_fromI is (Proxy Char) ast where
  90         term_fromI ast ctx k =
  91                 case ast_lexem ast of
  92                  "char" -> char_from
  93                  "char_toUpper" -> char_toUpper_from
  94                  _ -> Left $ Error_Term_unsupported
  95                 where
  96                 char_from =
  97                         let ty = tyChar in
  98                         from_lex (Text.pack $ show_type ty) ast $ \(i::Char) ->
  99                         k ty $ TermLC $ Fun.const $ char i
 100                 char_toUpper_from =
 101                         case ast_nodes ast of
 102                          [] ->
 103                                 k (tyChar ~> tyChar) $ TermLC $
 104                                 Fun.const $ lam char_toUpper
 105                          [ast_c] ->
 106                                 term_from ast_c ctx $ \ty_c (TermLC c) ->
 107                                 check_type (At Nothing tyChar) (At (Just ast_c) ty_c) $ \Refl ->
 108                                 k tyChar $ TermLC $ char_toUpper . c
 109                          _ -> Left $ Error_Term_Syntax $
 110                                 Error_Syntax_too_many_arguments $ At (Just ast) 3
 111
 112 -- | The 'Char' 'Type'
 113 tyChar :: Inj_Const cs Char => Type cs Char
 114 tyChar = TyConst inj_const
 115
 116 sym_Char :: Proxy Sym_Char
 117 sym_Char = Proxy
 118
 119 syChar :: IsString a => Syntax a
 120 syChar = Syntax "Char" []