lcc/Hcompta/LCC/Sym/Unit.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
   4 -- | Symantic for 'Unit'.
   5 module Hcompta.LCC.Sym.Unit where
   6
   7 -- import Data.Decimal (Decimal)
   8 import Data.Eq (Eq)
   9 import Data.Function (($), (.))
  10 import Data.Maybe (Maybe(..))
  11 import Data.Ord (Ord)
  12 import Data.Proxy
  13 import Data.Type.Equality ((:~:)(Refl))
  14 import Text.Show (Show(..))
  15 import qualified Data.Text as Text
  16 import qualified Language.Symantic.Typing as Sym
  17
  18 import Hcompta.LCC.Amount
  19
  20 import Language.Symantic.Parsing
  21 import Language.Symantic.Typing
  22 import Language.Symantic.Compiling
  23 import Language.Symantic.Interpreting
  24 import Language.Symantic.Transforming.Trans
  25 import qualified Language.Symantic.Lib as Sym
  26
  27 -- * Class 'Sym_Unit'
  28 class Sym_Unit term where
  29         unit :: Unit -> term Unit
  30         default unit :: Trans t term => Unit -> t term Unit
  31         unit = trans_lift . unit
  32
  33 type instance Sym_of_Iface (Proxy Unit) = Sym_Unit
  34 type instance TyConsts_of_Iface (Proxy Unit) = Proxy Unit ': TyConsts_imported_by (Proxy Unit)
  35 type instance TyConsts_imported_by (Proxy Unit) =
  36  [ Proxy Eq
  37  , Proxy Ord
  38  , Proxy Show
  39  ]
  40
  41 instance Sym_Unit HostI where
  42         unit = HostI
  43 instance Sym_Unit TextI where
  44         unit a = TextI $ \_p _v ->
  45                 Text.pack (show a)
  46 instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (DupI r1 r2) where
  47         unit x = unit x `DupI` unit x
  48
  49 instance
  50  ( Read_TyNameR TyName cs rs
  51  , Inj_TyConst cs Unit
  52  ) => Read_TyNameR TyName cs (Proxy Unit ': rs) where
  53         read_TyNameR _cs (TyName "Unit") k = k (ty @Unit)
  54         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  55 instance Show_TyConst cs => Show_TyConst (Proxy Unit ': cs) where
  56         show_TyConst TyConstZ{} = "Unit"
  57         show_TyConst (TyConstS c) = show_TyConst c
  58
  59 instance Proj_TyFamC cs Sym.TyFam_MonoElement Unit
  60
  61 instance -- Proj_TyConC
  62  ( Proj_TyConst cs Unit
  63  , Proj_TyConsts cs (TyConsts_imported_by (Proxy Unit))
  64  ) => Proj_TyConC cs (Proxy Unit) where
  65         proj_TyConC _ (TyConst q :$ TyConst c)
  66          | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
  67          , Just Refl <- proj_TyConst c (Proxy @Unit)
  68          = case () of
  69                  _ | Just Refl <- proj_TyConst q (Proxy @Eq)   -> Just TyCon
  70                    | Just Refl <- proj_TyConst q (Proxy @Ord)  -> Just TyCon
  71                    | Just Refl <- proj_TyConst q (Proxy @Show) -> Just TyCon
  72                  _ -> Nothing
  73         proj_TyConC _c _q = Nothing
  74 data instance TokenT meta (ts::[*]) (Proxy Unit)
  75  = Token_Term_Unit Unit
  76 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Unit))
  77 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Unit))
  78
  79 instance -- CompileI
  80  Inj_TyConst cs Unit =>
  81  CompileI cs is (Proxy Unit) where
  82         compileI tok _ctx k =
  83                 case tok of
  84                  Token_Term_Unit i -> k (ty @Unit) $ TermO $ \_c -> unit i
  85 instance -- TokenizeT
  86  -- Inj_Token meta ts Unit =>
  87  TokenizeT meta ts (Proxy Unit)
  88 instance Gram_Term_AtomsT meta ts (Proxy Unit) g