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 () = 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_Source src g
  47  , Gram_Rule g
  48  , Gram_Comment g
  49  , SymInj ss ()
  50  ) => Gram_Term_AtomsFor src ss g () where
  51         g_term_atomsFor =
  52          [ rule "teUnit" $
  53                 source $
  54                 (\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teUnit)
  55                  <$ symbol "("
  56                  <* symbol ")"
  57          ]
  58 instance ModuleFor src ss ()
  59
  60 -- ** 'Type's
  61 tyUnit :: Source src => LenInj vs => Type src vs ()
  62 tyUnit = tyConst @(K ()) @()
  63
  64 -- ** 'Term's
  65 teUnit :: TermDef () '[] (() #> ())
  66 teUnit = Term noConstraint tyUnit $ teSym @() $ unit