lcc/Hcompta/LCC/Sym/IO.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for the Input/Output.
   4 module Hcompta.LCC.Sym.IO where
   5
   6 import System.IO (IO)
   7 import qualified Prelude ()
   8
   9 import Language.Symantic.Grammar
  10 import Language.Symantic
  11 import Language.Symantic.Lib (a0, tyIO)
  12
  13 import Hcompta.LCC.Read ()
  14 import Hcompta.LCC.IO (PathFile(..), FromFile)
  15 import Hcompta.LCC.Sym.FileSystem (tyPathFile)
  16 import qualified Hcompta.LCC.IO as LCC
  17
  18 -- * Class 'Sym_FromFile'
  19 type instance Sym FromFile = Sym_FromFile
  20 class Sym_FromFile term where
  21         fromFile :: FromFile a => term PathFile -> term (IO a)
  22         default fromFile :: Sym_FromFile (UnT term) => Trans term => FromFile a => term PathFile -> term (IO a)
  23         fromFile = trans1 fromFile
  24
  25 instance Sym_FromFile Eval where
  26         fromFile = eval1 LCC.fromFile
  27 instance Sym_FromFile View where
  28         fromFile = view1 "fromFile"
  29 instance (Sym_FromFile r1, Sym_FromFile r2) => Sym_FromFile (Dup r1 r2) where
  30         fromFile = dup1 @Sym_FromFile fromFile
  31 instance (Sym_FromFile term, Sym_Lambda term) => Sym_FromFile (BetaT term)
  32
  33 instance FixityOf FromFile
  34 instance NameTyOf FromFile where
  35         nameTyOf _c = ["IO"] `Mod` "FromFile"
  36 instance ClassInstancesFor FromFile
  37 instance TypeInstancesFor FromFile
  38 instance Gram_Term_AtomsFor src ss g FromFile
  39 instance (Source src, SymInj ss FromFile) => ModuleFor src ss FromFile where
  40         moduleFor = ["IO"] `moduleWhere`
  41          [ "fromFile" := teIO_fromFile
  42          ]
  43
  44 tyFromFile :: Source src => Type src vs a -> Type src vs (FromFile a)
  45 tyFromFile a = tyConstLen @(K FromFile) @FromFile (lenVars a) `tyApp` a
  46
  47 teIO_fromFile :: TermDef FromFile '[Proxy a] (FromFile a #> (PathFile -> IO a))
  48 teIO_fromFile = Term (tyFromFile a0) (tyPathFile ~> tyIO a0) (teSym @FromFile (lam1 fromFile))
  49
  50 {-
  51 -- * Class 'Sym_LoadFile'
  52 type instance Sym ReadFile = Sym_LoadFile
  53 class Sym_LoadFile term where
  54         loadFile :: (ReadFile a{-, Loadable src ss-}) => term PathFile -> term (IO a)
  55         default loadFile :: (Sym_LoadFile (UnT term){-, Loadable src ss-}) => Trans term => ReadFile a => term PathFile -> term (IO a)
  56         loadFile = trans1 loadFile
  57
  58 instance Sym_LoadFile Eval where
  59         loadFile = eval1 LCC.fromFile
  60 instance Sym_LoadFile View where
  61         loadFile = view1 "loadFile"
  62 instance (Sym_LoadFile r1, Sym_LoadFile r2) => Sym_LoadFile (Dup r1 r2) where
  63         loadFile = dup1 @Sym_LoadFile loadFile
  64 instance (Sym_LoadFile term, Sym_Lambda term) => Sym_LoadFile (BetaT term)
  65
  66 instance FixityOf ReadFile
  67 instance NameTyOf ReadFile where
  68         nameTyOf _c = ["IO"] `Mod` "ReadFile"
  69 instance ClassInstancesFor ReadFile
  70 instance TypeInstancesFor ReadFile
  71 instance Gram_Term_AtomsFor src ss g ReadFile
  72 instance
  73  ( Source src
  74  , Typeable ss
  75  , SymInj ss ReadFile
  76  ) => ModuleFor src ss ReadFile where
  77         moduleFor = ["IO"] `moduleWhere`
  78          [ "loadFile" := teIO_loadFile
  79          ]
  80
  81 tyLoadFile :: Source src => Type src vs a -> Type src vs (ReadFile a)
  82 tyLoadFile a = tyConstLen @(K ReadFile) @ReadFile (lenVars a) `tyApp` a
  83
  84 teIO_loadFile ::
  85  forall src ss ts a.
  86  Typeable ss =>
  87  SymInj ss ReadFile =>
  88  Source src =>
  89  Term src ss ts '[Proxy a] ((ReadFile a) #> (PathFile -> IO a))
  90 teIO_loadFile = Term (tyLoadFile a0) (tyPathFile ~> tyIO a0) (teSym @ReadFile (lam1 loadFile))
  91 -}