lcc/Hcompta/LCC/Sym/Unit.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Unit'.
   4 module Hcompta.LCC.Sym.Unit where
   5
   6 import Data.Eq (Eq)
   7 import Data.Function (($), (.))
   8 import Data.Maybe (Maybe(..))
   9 import Data.Ord (Ord)
  10 import Data.Type.Equality ((:~:)(Refl))
  11 import Text.Show (Show(..))
  12 import qualified Language.Symantic.Typing as Sym
  13
  14 import Language.Symantic
  15
  16 import Hcompta.LCC.Amount
  17
  18 -- * Class 'Sym_Unit'
  19 type instance Sym Unit = Sym_Unit
  20 class Sym_Unit term where
  21         unit :: Unit -> term Unit
  22         default unit :: Sym_Unit (UnT term) => Trans term => Unit -> term Unit
  23         unit = trans . unit
  24
  25 instance Sym_Unit Eval where
  26         unit = Eval
  27 instance Sym_Unit View where
  28         unit (Unit u) = View $ \_p _v -> u
  29 instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where
  30         unit x = unit x `Dup` unit x
  31 instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)
  32
  33 instance NameTyOf Unit where
  34         nameTyOf _c = ["Unit"] `Mod` "Unit"
  35 instance ClassInstancesFor Unit where
  36         proveConstraintFor _c (TyApp _ (TyConst _ _ q) c)
  37          | Just HRefl <- proj_ConstKiTy @(K Unit) @Unit c
  38          = case () of
  39                  _ | Just Refl <- proj_Const @Eq   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 Unit
  45 instance Gram_Term_AtomsFor src ss g Unit
  46 instance (Source src, SymInj ss Unit) => ModuleFor src ss Unit where
  47         moduleFor = ["Unit"] `moduleWhere`
  48          [
  49          ]
  50
  51 tyUnit :: Source src => LenInj vs => Type src vs Unit
  52 tyUnit = tyConst @(K Unit) @Unit
  53
  54 teUnit :: Source src => SymInj ss Unit => Unit -> Term src ss ts '[] (() #> Unit)
  55 teUnit a = Term noConstraint tyUnit $ teSym @Unit $ unit a