module Hcompta.LCC.Source where

import Data.Eq (Eq)
import Text.Show (Show)

import Language.Symantic hiding (Source(..))
import qualified Language.Symantic as Sym

import Hcompta.LCC.Compta (Compta)

-- * Type 'Source'
-- | A 'Source' usable when using 'readCompta'.
data Source inp ss
 =   Source_Less
 |   Source_Input    (Span inp)
 |   Source_AST_Term (AST_Term (Source inp ss) (Proxy (Compta (Source inp ss) ss) ': ss))
 |   Source_AST_Type (AST_Type (Source inp ss))
 |   Source_Kind     (KindK    (Source inp ss))
 |   Source_Type     (TypeVT   (Source inp ss))
 |   Source_Term
 deriving (Eq, Show)

type instance Source_Input (Source inp ss) = inp

instance Sym.Source (Source inp ss) where
	noSource = Source_Less
instance SourceInj (Span inp) (Source inp ss) where
	sourceInj = Source_Input
instance SourceInj (AST_Term (Source inp ss) (Proxy (Compta (Source inp ss) ss) ': ss)) (Source inp ss) where
	sourceInj = Source_AST_Term
instance SourceInj (AST_Type (Source inp ss)) (Source inp ss) where
	sourceInj = Source_AST_Type
instance SourceInj (KindK (Source inp ss)) (Source inp ss) where
	sourceInj = Source_Kind
instance SourceInj (TypeVT (Source inp ss)) (Source inp ss) where
	sourceInj = Source_Type