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.Proxy
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import Text.Show (Show(..))
  13 import qualified Language.Symantic.Typing as Sym
  14
  15 import Language.Symantic
  16
  17 import Hcompta.LCC.Amount
  18
  19 -- * Class 'Sym_Unit'
  20 type instance Sym (Proxy Unit) = Sym_Unit
  21 class Sym_Unit term where
  22         unit :: Unit -> term Unit
  23         default unit :: Sym_Unit (UnT term) => Trans term => Unit -> term Unit
  24         unit = trans . unit
  25
  26 instance Sym_Unit Eval where
  27         unit = Eval
  28 instance Sym_Unit View where
  29         unit (Unit u) = View $ \_p _v -> u
  30 instance (Sym_Unit r1, Sym_Unit r2) => Sym_Unit (Dup r1 r2) where
  31         unit x = unit x `Dup` unit x
  32 instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)
  33
  34 instance ClassInstancesFor Unit where
  35         proveConstraintFor _c (TyApp _ (TyConst _ _ q) c)
  36          | Just HRefl <- proj_ConstKiTy @(K Unit) @Unit c
  37          = case () of
  38                  _ | Just Refl <- proj_Const @Eq   q -> Just Dict
  39                    | Just Refl <- proj_Const @Ord  q -> Just Dict
  40                    | Just Refl <- proj_Const @Show q -> Just Dict
  41                  _ -> Nothing
  42         proveConstraintFor _c _q = Nothing
  43 instance TypeInstancesFor Unit
  44 instance Gram_Term_AtomsFor src ss g Unit
  45 instance (Source src, Inj_Sym ss Unit) => ModuleFor src ss Unit where
  46         moduleFor = ["Unit"] `moduleWhere`
  47          [
  48          ]
  49
  50 tyUnit :: Source src => Inj_Len vs => Type src vs Unit
  51 tyUnit = tyConst @(K Unit) @Unit
  52
  53 teUnit :: Source src => Inj_Sym ss Unit => Unit -> Term src ss ts '[] (() #> Unit)
  54 teUnit a = Term noConstraint tyUnit $ teSym @Unit $ unit a