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 Control.Applicative ((<*))
   7 import Data.Eq (Eq)
   8 import Data.Function (($))
   9 import Data.Functor ((<$))
  10 import Data.Maybe (Maybe(..))
  11 import Data.Monoid (Monoid)
  12 import Data.Ord (Ord)
  13 import Prelude (Bounded, Enum)
  14 import Text.Show (Show)
  15
  16 import Language.Symantic
  17 import Language.Symantic.Grammar
  18
  19 -- * Class 'Sym_Unit'
  20 type instance Sym () = Sym_Unit
  21 class Sym_Unit term where
  22         unit :: term ()
  23         default unit :: Sym_Unit (UnT term) => Trans term => term ()
  24         unit = trans unit
  25
  26 -- Interpreting
  27 instance Sym_Unit Eval where
  28         unit = Eval ()
  29 instance Sym_Unit View where
  30         unit = View $ \_p _v -> "()"
  31 instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where
  32         unit = unit `Dup` unit
  33
  34 -- Transforming
  35 instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)
  36
  37 -- Typing
  38 instance NameTyOf () where
  39         nameTyOf _c = [] `Mod` ""
  40 instance ClassInstancesFor () where
  41         proveConstraintFor _ (TyConst _ _ q :$ z)
  42          | Just HRefl <- proj_ConstKiTy @_ @() z
  43          = case () of
  44                  _ | Just Refl <- proj_Const @Bounded q -> Just Dict
  45                    | Just Refl <- proj_Const @Enum    q -> Just Dict
  46                    | Just Refl <- proj_Const @Eq      q -> Just Dict
  47                    | Just Refl <- proj_Const @Monoid  q -> Just Dict
  48                    | Just Refl <- proj_Const @Ord     q -> Just Dict
  49                    | Just Refl <- proj_Const @Show    q -> Just Dict
  50                  _ -> Nothing
  51         proveConstraintFor _c _q = Nothing
  52 instance TypeInstancesFor ()
  53
  54 -- Compiling
  55 instance
  56  ( Gram_Source src g
  57  , Gram_Rule g
  58  , Gram_Comment g
  59  , SymInj ss ()
  60  ) => Gram_Term_AtomsFor src ss g () where
  61         g_term_atomsFor =
  62          [ rule "teUnit" $
  63                 source $
  64                 (\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teUnit)
  65                  <$ symbol "("
  66                  <* symbol ")"
  67          ]
  68 instance ModuleFor src ss ()
  69
  70 -- ** 'Type's
  71 tyUnit :: Source src => LenInj vs => Type src vs ()
  72 tyUnit = tyConst @(K ()) @()
  73
  74 -- ** 'Term's
  75 teUnit :: TermDef () '[] (() #> ())
  76 teUnit = Term noConstraint tyUnit $ teSym @() $ unit