{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Writeable'.
module Hcompta.LCC.Sym.Writeable where

import qualified Language.Symantic.Document as Doc
import qualified Language.Symantic.Document.Term.IO as DocIO
import Language.Symantic

import Hcompta.LCC.Write (Writeable)
import qualified Hcompta.LCC.Write as W

-- * Class 'Sym_Writeable'
type instance Sym Writeable = Sym_Writeable
class Sym_Writeable term where
	write :: Writeable d a => term a -> term d
	default write :: Sym_Writeable (UnT term) => Trans term => Writeable d a => term a -> term d
	write = trans1 write

instance Sym_Writeable Eval where
	write = eval1 W.write
instance Sym_Writeable View where
	write = view1 "write"
instance (Sym_Writeable r1, Sym_Writeable r2) => Sym_Writeable (Dup r1 r2) where
	write = dup1 @Sym_Writeable write
instance (Sym_Writeable term, Sym_Lambda term) => Sym_Writeable (BetaT term)

instance NameTyOf Writeable where
	nameTyOf _c = ["Write"] `Mod` "Writeable"
instance FixityOf Writeable
instance ClassInstancesFor Writeable
instance TypeInstancesFor Writeable
instance Gram_Term_AtomsFor src ss g Writeable
instance (Source src, SymInj ss Writeable) => ModuleFor src ss Writeable where
	moduleFor = ["Writeable"] `moduleWhere`
	 [ "write" := teWriteable_write
	 ]

tyWriteable :: Source src => Type src vs d -> Type src vs a -> Type src vs (Writeable d a)
tyWriteable d a = tyConstLen @(K Writeable) @Writeable (lenVars d) `tyApp` d `tyApp` a

d0 :: Source src => LenInj vs => KindInj (K d) => Type src (Proxy d ': vs) d
d0 = tyVar "d" varZ
a1 :: Source src => LenInj vs => KindInj (K a) => Type src (d ': Proxy a ': vs) a
a1 = tyVar "a" (VarS varZ)

teWriteable_write :: TermDef Writeable '[Proxy d, Proxy a] (Writeable d a #> (a -> d))
teWriteable_write = Term (tyWriteable d0 a1) (a1 ~> d0) (teSym @Writeable (lam1 write))

-- 'W.Reader'
instance NameTyOf W.Reader where
	nameTyOf _c = ["Write"] `Mod` "W.Reader"
instance ClassInstancesFor W.Reader
instance TypeInstancesFor W.Reader
tyContext_Write :: Source src => LenInj vs => Type src vs W.Reader
tyContext_Write = tyConst @(K W.Reader) @W.Reader

-- 'Doc.TermIO'
instance NameTyOf DocIO.TermIO where
	nameTyOf _c = ["Doc"] `Mod` "TermIO"
instance ClassInstancesFor DocIO.TermIO
instance TypeInstancesFor DocIO.TermIO
tyANSI_IO :: Source src => LenInj vs => Type src vs DocIO.TermIO
tyANSI_IO = tyConst @(K DocIO.TermIO) @DocIO.TermIO