symantic-lib/Language/Symantic/Lib/Unit.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for '()'.
   4 module Language.Symantic.Lib.Unit where
   5
   6 import Prelude hiding ((&&), not, (||))
   7
   8 import Language.Symantic
   9 import Language.Symantic.Grammar
  10
  11 -- * Class 'Sym_Unit'
  12 type instance Sym (Proxy ()) = Sym_Unit
  13 class Sym_Unit term where
  14         unit :: term ()
  15         default unit :: Sym_Unit (UnT term) => Trans term => term ()
  16         unit = trans unit
  17
  18 -- Interpreting
  19 instance Sym_Unit Eval where
  20         unit = Eval ()
  21 instance Sym_Unit View where
  22         unit = View $ \_p _v -> "()"
  23 instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where
  24         unit = unit `Dup` unit
  25
  26 -- Transforming
  27 instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)
  28
  29 -- Typing
  30 instance ClassInstancesFor () where
  31         proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
  32          | Just HRefl <- proj_ConstKiTy @_ @() z
  33          = case () of
  34                  _ | Just Refl <- proj_Const @Bounded q -> Just Dict
  35                    | Just Refl <- proj_Const @Enum    q -> Just Dict
  36                    | Just Refl <- proj_Const @Eq      q -> Just Dict
  37                    | Just Refl <- proj_Const @Monoid  q -> Just Dict
  38                    | Just Refl <- proj_Const @Ord     q -> Just Dict
  39                    | Just Refl <- proj_Const @Show    q -> Just Dict
  40                  _ -> Nothing
  41         proveConstraintFor _c _q = Nothing
  42 instance TypeInstancesFor ()
  43
  44 -- Compiling
  45 instance
  46  ( Gram_Rule g
  47  , Gram_Comment g
  48  , Gram_Meta src g
  49  , Inj_Sym ss ()
  50  , Source src
  51  ) => Gram_Term_AtomsFor src ss g () where
  52         g_term_atomsFor _t =
  53          [ rule "teUnit" $
  54                 withMeta $
  55                 (\src -> BinTree0 $ Token_Term $ TermVT_CF $ (`setSource` src) $ teUnit)
  56                  <$ symbol "("
  57                  <* symbol ")"
  58          ]
  59 instance Module src ss ()
  60
  61 -- ** 'Type's
  62 tyUnit :: Source src => Inj_Len vs => Type src vs ()
  63 tyUnit = tyConst @(K ()) @()
  64
  65 -- ** 'Term's
  66 teUnit ::
  67  Source src => Inj_Sym ss () =>
  68  Term src ss ts '[] ()
  69 teUnit = Term noConstraint tyUnit $ teSym @() $ unit