{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for the file system.
module Hcompta.LCC.Sym.FileSystem where

import Control.Applicative (Applicative(..))
import Data.Eq (Eq)
import Data.Foldable (concat)
import Data.Function (($), (.))
import Data.Functor (Functor(..), (<$>))
import Data.Maybe (Maybe(..))
import Data.Type.Equality ((:~:)(Refl))
import System.IO (FilePath)
import Text.Show (Show(..))
import qualified Data.Text as Text
import qualified Prelude ()

import Language.Symantic.Grammar
import Language.Symantic

import Hcompta.LCC.IO (PathFile(..))

-- * Class 'Sym_PathFile'
type instance Sym PathFile = Sym_PathFile
class Sym_PathFile term where
	pathfile :: PathFile -> term PathFile
	default pathfile :: Sym_PathFile (UnT term) => Trans term => PathFile -> term PathFile
	pathfile = trans . pathfile

instance Sym_PathFile Eval where
	pathfile = Eval
instance Sym_PathFile View where
	pathfile a = View $ \_p _v -> Text.pack (show a)
instance (Sym_PathFile r1, Sym_PathFile r2) => Sym_PathFile (Dup r1 r2) where
	pathfile x = pathfile x `Dup` pathfile x
instance (Sym_PathFile term, Sym_Lambda term) => Sym_PathFile (BetaT term)

instance NameTyOf PathFile where
	nameTyOf _c = ["LCC"] `Mod` "PathFile"
instance ClassInstancesFor PathFile where
	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
	 | Just HRefl <- proj_ConstKiTy @(K PathFile) @PathFile c
	 = case () of
		 _ | Just Refl <- proj_Const @Eq q   -> Just Dict
		   | Just Refl <- proj_Const @Show q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor PathFile

instance -- Gram_Term_AtomsFor
 ( Gram_Rule g
 , Gram_Alt g
 , Gram_Comment g
 , Gram_Source src g
 , SymInj ss PathFile
 ) => Gram_Term_AtomsFor src ss g PathFile where
	g_term_atomsFor =
	 [ rule "tePathFile" $
		lexeme $ source $
		(\a src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ tePathFile a)
		 <$> g_pathfile
	 ]
		where
		g_pathfile :: CF g PathFile
		g_pathfile =
			fmap PathFile $
			(:)
			 <$> char '.'
			 <*> (concat <$> some ((:) <$> char '/' <*> g_pathfile_section))
		g_pathfile_section :: CF g FilePath
		g_pathfile_section = some (choice $ char '.' : (unicat <$> [Unicat_Letter, Unicat_Number]))
instance (Source src, SymInj ss PathFile) => ModuleFor src ss PathFile where
	moduleFor = ["LCC", "PathFile"] `moduleWhere`
	 [
	 ]

tyPathFile :: Source src => LenInj vs => Type src vs PathFile
tyPathFile = tyConst @(K PathFile) @PathFile

tePathFile :: Source src => SymInj ss PathFile => PathFile -> Term src ss ts '[] (() #> PathFile)
tePathFile a = Term noConstraint tyPathFile $ teSym @PathFile $ pathfile a