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

import qualified Language.Symantic.Document as Doc
import Language.Symantic

import Hcompta.LCC.Write (Writeable, Context_Write)
import qualified Hcompta.LCC.Write as LCC

-- * 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 LCC.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))

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

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