1 {-# LANGUAGE EmptyDataDecls #-}
2 {-# LANGUAGE UndecidableInstances #-}
3 {-# OPTIONS_GHC -fno-warn-orphans #-}
4 -- | Symantic for the file system.
5 module Hcompta.LCC.Sym.FileSystem where
7 import Control.Applicative (Applicative(..))
9 import Data.Foldable (concat)
10 import Data.Function (($), (.))
11 import Data.Functor (Functor(..), (<$>))
12 import Data.Maybe (Maybe(..))
14 import Data.Type.Equality ((:~:)(Refl))
15 import System.IO (FilePath)
16 import Text.Show (Show(..))
17 import qualified Data.Text as Text
18 import qualified Prelude ()
20 import Language.Symantic.Grammar
21 import Language.Symantic
23 import Hcompta.LCC.Journal (PathFile(..))
25 -- * Class 'Sym_PathFile'
26 type instance Sym (Proxy PathFile) = Sym_PathFile
27 class Sym_PathFile term where
28 pathfile :: PathFile -> term PathFile
29 default pathfile :: Sym_PathFile (UnT term) => Trans term => PathFile -> term PathFile
30 pathfile = trans . pathfile
32 instance Sym_PathFile Eval where
34 instance Sym_PathFile View where
35 pathfile a = View $ \_p _v -> Text.pack (show a)
36 instance (Sym_PathFile r1, Sym_PathFile r2) => Sym_PathFile (Dup r1 r2) where
37 pathfile x = pathfile x `Dup` pathfile x
38 instance (Sym_PathFile term, Sym_Lambda term) => Sym_PathFile (BetaT term)
40 instance ClassInstancesFor PathFile where
41 proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
42 | Just HRefl <- proj_ConstKiTy @(K PathFile) @PathFile c
44 _ | Just Refl <- proj_Const @Eq q -> Just Dict
45 | Just Refl <- proj_Const @Show q -> Just Dict
47 proveConstraintFor _c _q = Nothing
48 instance TypeInstancesFor PathFile
50 instance -- Gram_Term_AtomsFor
56 ) => Gram_Term_AtomsFor src ss g PathFile where
60 (\a src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ tePathFile a)
64 g_pathfile :: CF g PathFile
69 <*> (concat <$> some ((:) <$> char '/' <*> g_pathfile_section))
70 g_pathfile_section :: CF g FilePath
71 g_pathfile_section = some (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
72 instance (Source src, Inj_Sym ss PathFile) => ModuleFor src ss PathFile where
73 moduleFor = ["PathFile"] `moduleWhere`
77 tyPathFile :: Source src => Inj_Len vs => Type src vs PathFile
78 tyPathFile = tyConst @(K PathFile) @PathFile
80 tePathFile :: Source src => Inj_Sym ss PathFile => PathFile -> Term src ss ts '[] (() #> PathFile)
81 tePathFile a = Term noConstraint tyPathFile $ teSym @PathFile $ pathfile a