{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for the Input/Output.
module Hcompta.LCC.Sym.IO where

import System.IO (IO)
import qualified Prelude ()

import Language.Symantic.Grammar
import Language.Symantic
import Language.Symantic.Lib (a0, tyIO)

import Hcompta.LCC.Read ()
import Hcompta.LCC.IO (PathFile(..), FromFile)
import Hcompta.LCC.Sym.FileSystem (tyPathFile)
import qualified Hcompta.LCC.IO as LCC

-- * Class 'Sym_FromFile'
type instance Sym FromFile = Sym_FromFile
class Sym_FromFile term where
	fromFile :: FromFile a => term PathFile -> term (IO a)
	default fromFile :: Sym_FromFile (UnT term) => Trans term => FromFile a => term PathFile -> term (IO a)
	fromFile = trans1 fromFile

instance Sym_FromFile Eval where
	fromFile = eval1 LCC.fromFile
instance Sym_FromFile View where
	fromFile = view1 "fromFile"
instance (Sym_FromFile r1, Sym_FromFile r2) => Sym_FromFile (Dup r1 r2) where
	fromFile = dup1 @Sym_FromFile fromFile
instance (Sym_FromFile term, Sym_Lambda term) => Sym_FromFile (BetaT term)

instance FixityOf FromFile
instance NameTyOf FromFile where
	nameTyOf _c = ["IO"] `Mod` "FromFile"
instance ClassInstancesFor FromFile
instance TypeInstancesFor FromFile
instance Gram_Term_AtomsFor src ss g FromFile
instance (Source src, SymInj ss FromFile) => ModuleFor src ss FromFile where
	moduleFor = ["IO"] `moduleWhere`
	 [ "fromFile" := teIO_fromFile
	 ]

tyFromFile :: Source src => Type src vs a -> Type src vs (FromFile a)
tyFromFile a = tyConstLen @(K FromFile) @FromFile (lenVars a) `tyApp` a

teIO_fromFile :: TermDef FromFile '[Proxy a] (FromFile a #> (PathFile -> IO a))
teIO_fromFile = Term (tyFromFile a0) (tyPathFile ~> tyIO a0) (teSym @FromFile (lam1 fromFile))

{-
-- * Class 'Sym_LoadFile'
type instance Sym ReadFile = Sym_LoadFile
class Sym_LoadFile term where
	loadFile :: (ReadFile a{-, Loadable src ss-}) => term PathFile -> term (IO a)
	default loadFile :: (Sym_LoadFile (UnT term){-, Loadable src ss-}) => Trans term => ReadFile a => term PathFile -> term (IO a)
	loadFile = trans1 loadFile

instance Sym_LoadFile Eval where
	loadFile = eval1 LCC.fromFile
instance Sym_LoadFile View where
	loadFile = view1 "loadFile"
instance (Sym_LoadFile r1, Sym_LoadFile r2) => Sym_LoadFile (Dup r1 r2) where
	loadFile = dup1 @Sym_LoadFile loadFile
instance (Sym_LoadFile term, Sym_Lambda term) => Sym_LoadFile (BetaT term)

instance FixityOf ReadFile
instance NameTyOf ReadFile where
	nameTyOf _c = ["IO"] `Mod` "ReadFile"
instance ClassInstancesFor ReadFile
instance TypeInstancesFor ReadFile
instance Gram_Term_AtomsFor src ss g ReadFile
instance
 ( Source src
 , Typeable ss
 , SymInj ss ReadFile
 ) => ModuleFor src ss ReadFile where
	moduleFor = ["IO"] `moduleWhere`
	 [ "loadFile" := teIO_loadFile
	 ]

tyLoadFile :: Source src => Type src vs a -> Type src vs (ReadFile a)
tyLoadFile a = tyConstLen @(K ReadFile) @ReadFile (lenVars a) `tyApp` a

teIO_loadFile ::
 forall src ss ts a.
 Typeable ss =>
 SymInj ss ReadFile =>
 Source src =>
 Term src ss ts '[Proxy a] ((ReadFile a) #> (PathFile -> IO a))
teIO_loadFile = Term (tyLoadFile a0) (tyPathFile ~> tyIO a0) (teSym @ReadFile (lam1 loadFile))
-}