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