lcc/Hcompta/LCC/Sym/Writeable.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Writeable'.
   4 module Hcompta.LCC.Sym.Writeable where
   5
   6 import qualified Language.Symantic.Document as Doc
   7 import Language.Symantic
   8
   9 import Hcompta.LCC.Write (Writeable, Context_Write)
  10 import qualified Hcompta.LCC.Write as LCC
  11
  12 -- * Class 'Sym_Writeable'
  13 type instance Sym Writeable = Sym_Writeable
  14 class Sym_Writeable term where
  15         write :: Writeable d a => term a -> term d
  16         default write :: Sym_Writeable (UnT term) => Trans term => Writeable d a => term a -> term d
  17         write = trans1 write
  18
  19 instance Sym_Writeable Eval where
  20         write = eval1 LCC.write
  21 instance Sym_Writeable View where
  22         write = view1 "write"
  23 instance (Sym_Writeable r1, Sym_Writeable r2) => Sym_Writeable (Dup r1 r2) where
  24         write = dup1 @Sym_Writeable write
  25 instance (Sym_Writeable term, Sym_Lambda term) => Sym_Writeable (BetaT term)
  26
  27 instance NameTyOf Writeable where
  28         nameTyOf _c = ["Write"] `Mod` "Writeable"
  29 instance FixityOf Writeable
  30 instance ClassInstancesFor Writeable
  31 instance TypeInstancesFor Writeable
  32 instance Gram_Term_AtomsFor src ss g Writeable
  33 instance (Source src, SymInj ss Writeable) => ModuleFor src ss Writeable where
  34         moduleFor = ["Writeable"] `moduleWhere`
  35          [ "write" := teWriteable_write
  36          ]
  37
  38 tyWriteable :: Source src => Type src vs d -> Type src vs a -> Type src vs (Writeable d a)
  39 tyWriteable d a = tyConstLen @(K Writeable) @Writeable (lenVars d) `tyApp` d `tyApp` a
  40
  41 d0 :: Source src => LenInj vs => KindInj (K d) => Type src (Proxy d ': vs) d
  42 d0 = tyVar "d" varZ
  43 a1 :: Source src => LenInj vs => KindInj (K a) => Type src (d ': Proxy a ': vs) a
  44 a1 = tyVar "a" (VarS varZ)
  45
  46 teWriteable_write :: TermDef Writeable '[Proxy d, Proxy a] (Writeable d a #> (a -> d))
  47 teWriteable_write = Term (tyWriteable d0 a1) (a1 ~> d0) (teSym @Writeable (lam1 write))
  48
  49 -- 'Context_Write'
  50 instance NameTyOf Context_Write where
  51         nameTyOf _c = ["Write"] `Mod` "Context_Write"
  52 instance ClassInstancesFor Context_Write
  53 instance TypeInstancesFor Context_Write
  54 tyContext_Write :: Source src => LenInj vs => Type src vs Context_Write
  55 tyContext_Write = tyConst @(K Context_Write) @Context_Write
  56
  57 -- 'Doc.ANSI_IO'
  58 instance NameTyOf Doc.ANSI_IO where
  59         nameTyOf _c = ["Doc"] `Mod` "ANSI_IO"
  60 instance ClassInstancesFor Doc.ANSI_IO
  61 instance TypeInstancesFor Doc.ANSI_IO
  62 tyANSI_IO :: Source src => LenInj vs => Type src vs Doc.ANSI_IO
  63 tyANSI_IO = tyConst @(K Doc.ANSI_IO) @Doc.ANSI_IO