lcc/Hcompta/LCC/Sym/Negable.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Negable'.
   4 module Hcompta.LCC.Sym.Negable where
   5
   6 import Control.Monad (liftM)
   7 import Data.Eq (Eq)
   8 import Data.Function (($))
   9 import Data.Maybe (Maybe(..))
  10 import Data.Monoid (Monoid(..))
  11 import Data.Proxy
  12 import Hcompta.Quantity
  13 import Text.Show (Show)
  14 import qualified Prelude ()
  15
  16 import Language.Symantic
  17
  18 -- * Class 'Sym_Negable'
  19 class Sym_Negable term where
  20         neg :: Negable n => term n -> term n
  21         default neg :: (Trans t term, Negable n) => t term n -> t term n
  22         neg = trans_map1 neg
  23
  24 type instance Sym_of_Iface (Proxy Negable) = Sym_Negable
  25 type instance TyConsts_of_Iface (Proxy Negable) = Proxy Negable ': TyConsts_imported_by (Proxy Negable)
  26 type instance TyConsts_imported_by (Proxy Negable) = '[]
  27
  28 instance Sym_Negable HostI where
  29         neg = liftM quantity_neg
  30 instance Sym_Negable TextI where
  31         neg = textI1 "-"
  32 instance (Sym_Negable r1, Sym_Negable r2) => Sym_Negable (DupI r1 r2) where
  33         neg = dupI1 @Sym_Negable neg
  34
  35 instance
  36  ( Read_TyNameR TyName cs rs
  37  , Inj_TyConst cs Negable
  38  ) => Read_TyNameR TyName cs (Proxy Negable ': rs) where
  39         read_TyNameR _cs (TyName "Negable") k = k (ty @Negable)
  40         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  41 instance Show_TyConst cs => Show_TyConst (Proxy Negable ': cs) where
  42         show_TyConst TyConstZ{} = "Negable"
  43         show_TyConst (TyConstS c) = show_TyConst c
  44
  45 instance Proj_TyConC cs (Proxy Negable)
  46 data instance TokenT meta (ts::[*]) (Proxy Negable)
  47  = Token_Term_Negable_neg (EToken meta ts)
  48 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Negable))
  49 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Negable))
  50
  51 instance -- CompileI
  52  ( Inj_TyConst cs Negable
  53  , Proj_TyCon  cs
  54  , Compile cs is
  55  ) => CompileI cs is (Proxy Negable) where
  56         compileI tok ctx k =
  57                 case tok of
  58                  Token_Term_Negable_neg tok_a -> op1_from tok_a neg
  59                 where
  60                 op1_from tok_a
  61                  (op::forall term a. (Sym_Negable term, Negable a)
  62                          => term a -> term a) =
  63                  -- neg :: Negable a => a -> a
  64                         compileO tok_a ctx $ \ty_a (TermO x) ->
  65                         check_TyCon (At (Just tok_a) (ty @Negable :$ ty_a)) $ \TyCon ->
  66                         k ty_a $ TermO $
  67                          \c -> op (x c)
  68 instance -- TokenizeT
  69  Inj_Token meta ts Negable =>
  70  TokenizeT meta ts (Proxy Negable) where
  71         tokenizeT _t = mempty
  72          { tokenizers_prefix = tokenizeTMod []
  73                  [ tokenize1 "-" (Prefix 10) Token_Term_Negable_neg
  74                  ]
  75          }
  76 instance Gram_Term_AtomsT meta ts (Proxy Negable) g