packages feed

dedukti-1.0.0: Dedukti/Module.hs

-- |
-- Copyright : © 2009 CNRS - École Polytechnique - INRIA
-- License   : GPL
--
-- A representation of module names and associated functions to map module
-- names to source files and vice-versa. Qualified names, as required in the
-- presence of modules, are also defined here.
module Dedukti.Module
    ( -- * Data types
      Hierarchy(..), MName
    -- * Exceptions
    , InvalidModuleName(..)
    -- * Functions
    , hierarchy, toList
    , pathFromModule, moduleFromPath
    , srcPathFromModule, objPathFromModule, ifacePathFromModule
    -- * Qualified names.
    , Qid(..), qid, (.$), provenance, unqualify
    ) where

import Dedukti.DkM
import System.FilePath
import Data.Char (isAlpha, isAlphaNum)
import qualified Data.Text.Lazy as T
import Text.PrettyPrint.Leijen


data Hierarchy = !Hierarchy :. !T.Text | Root
                 deriving (Eq, Ord, Show)

type MName = Hierarchy

newtype InvalidModuleName = InvalidModuleName String
    deriving (Eq, Ord, Typeable)

instance Show InvalidModuleName where
    show (InvalidModuleName name) = "invalid character in " ++ name

instance Exception InvalidModuleName

instance Pretty MName where
    pretty (Root :. x) = text (T.unpack x)
    pretty (xs :. x) = pretty xs <> char '.' <> text (T.unpack x)

hierarchy :: [T.Text] -> Hierarchy
hierarchy =  f . reverse where
    f [] = Root
    f (x:xs) = f xs :. x

toList :: Hierarchy -> [T.Text]
toList = reverse . f where
    f Root = []
    f (xs :. x) = x : f xs

-- | Raise an exception if module name component is a valid identifier.
check :: String -> String
check cmpt@(x:xs) | isAlpha x, and (map isAlphaNum xs) = cmpt
                  | otherwise = throw $ InvalidModuleName cmpt

pathFromModule :: String -> MName -> FilePath
pathFromModule ext mod =
    addExtension (joinPath $ map T.unpack $ toList mod) ext

moduleFromPath :: FilePath -> MName
moduleFromPath =
    hierarchy . map (T.pack . check) . splitDirectories . dropExtension

srcPathFromModule :: MName -> FilePath
srcPathFromModule = pathFromModule ".eu"

objPathFromModule :: MName -> FilePath
objPathFromModule = pathFromModule ".euo"

ifacePathFromModule :: MName -> FilePath
ifacePathFromModule = pathFromModule ".eui"

-- | The datatype of qualified names.
data Qid = Qid { qid_qualifier :: !Hierarchy
               , qid_stem      :: !T.Text
               , qid_suffix    :: !Hierarchy }
           deriving (Eq, Ord, Show)

-- | Shorthand qid introduction.
qid :: T.Text -> Qid
qid x = Qid Root x Root

-- | Append suffix.
(.$) :: Qid -> T.Text -> Qid
(Qid qual x sufs) .$ suf = Qid qual x (sufs :. suf)

-- | Get the module where the qid is defined, based on its qualifier.
provenance :: Qid -> Maybe MName
provenance (Qid Root _ _) = Nothing
provenance (Qid qual _ _) = Just qual

-- | Remove any qualifier.
unqualify :: Qid -> Qid
unqualify qid = qid{qid_qualifier = Root}