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 NameTyOf () where
  31         nameTyOf _c = [] `Mod` ""
  32 instance ClassInstancesFor () where
  33         proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
  34          | Just HRefl <- proj_ConstKiTy @_ @() z
  35          = case () of
  36                  _ | Just Refl <- proj_Const @Bounded q -> Just Dict
  37                    | Just Refl <- proj_Const @Enum    q -> Just Dict
  38                    | Just Refl <- proj_Const @Eq      q -> Just Dict
  39                    | Just Refl <- proj_Const @Monoid  q -> Just Dict
  40                    | Just Refl <- proj_Const @Ord     q -> Just Dict
  41                    | Just Refl <- proj_Const @Show    q -> Just Dict
  42                  _ -> Nothing
  43         proveConstraintFor _c _q = Nothing
  44 instance TypeInstancesFor ()
  45
  46 -- Compiling
  47 instance
  48  ( Gram_Source src g
  49  , Gram_Rule g
  50  , Gram_Comment g
  51  , SymInj ss ()
  52  ) => Gram_Term_AtomsFor src ss g () where
  53         g_term_atomsFor =
  54          [ rule "teUnit" $
  55                 source $
  56                 (\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teUnit)
  57                  <$ symbol "("
  58                  <* symbol ")"
  59          ]
  60 instance ModuleFor src ss ()
  61
  62 -- ** 'Type's
  63 tyUnit :: Source src => LenInj vs => Type src vs ()
  64 tyUnit = tyConst @(K ()) @()
  65
  66 -- ** 'Term's
  67 teUnit :: TermDef () '[] (() #> ())
  68 teUnit = Term noConstraint tyUnit $ teSym @() $ unit