{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} module HERMIT.External ( -- * Externals External , ExternalName , ExternalHelp , externName , externDyn , externHelp , externTypeString , externTypeArgResString , splitFunTyArgs , toHelp , external , Extern(..) , matchingExternals -- * Tags , CmdTag(..) , TagE , Tag((.+),remTag,tagMatch) , (.&) , (.||) , notT , externTags , dictionaryOfTags -- * Boxes -- | Boxes are used by the 'Extern' class. , CoreString(..) , CrumbBox(..) , IntBox(..) , IntListBox(..) , PathBox(..) , StringBox(..) , StringListBox(..) , TagBox(..) -- ** LCore Boxes , TransformLCoreStringBox(..) , TransformLCoreUnitBox(..) , TransformLCorePathBox(..) , RewriteLCoreBox(..) , BiRewriteLCoreBox(..) , RewriteLCoreListBox(..) -- ** LCoreTC Boxes , TransformLCoreTCStringBox(..) , TransformLCoreTCUnitBox(..) , TransformLCoreTCLCoreBox(..) , TransformLCoreTCPathBox(..) , RewriteLCoreTCBox(..) , BiRewriteLCoreTCBox(..) , RewriteLCoreTCListBox(..) ) where import Data.Map hiding (map) import Data.Dynamic import Data.List import Data.Typeable.Internal (TypeRep(..), funTc) import HERMIT.Core import HERMIT.Context (LocalPathH) import HERMIT.Kure import HERMIT.Lemma ----------------------------------------------------------------- -- | 'External' names are just strings. type ExternalName = String -- | Help information for 'External's is stored as a list of strings, designed for multi-line displaying. type ExternalHelp = [String] -- Tags -------------------------------------------------------- -- | Requirement: commands cannot have the same name as any 'CmdTag' -- (or the help function will not find it). -- These should be /user facing/, because they give the user -- a way of sub-dividing our confusing array of commands. data CmdTag = Shell -- ^ Shell-specific command. | Eval -- ^ The arrow of evaluation (reduces a term). | KURE -- ^ 'Language.KURE' command. | Loop -- ^ Command may operate multiple times. | Deep -- ^ Command may make a deep change, can be O(n). | Shallow -- ^ Command operates on local nodes only, O(1). | Navigation -- ^ Uses 'Path' or 'Lens' to focus onto something. | Query -- ^ Extract information from an expression. | Predicate -- ^ Something that passes or fails. | Introduce -- ^ Introduce something, like a new name. | Commute -- ^ Commute is when you swap nested terms. | PreCondition -- ^ Operation has a (perhaps undocumented) precondition. | Strictness -- ^ Alters the strictness of the expression. | Debug -- ^ Commands specifically to help debugging. | VersionControl -- ^ Version control for Core syntax. | Context -- ^ A command that uses its context, such as inlining. | Unsafe -- ^ Commands that are not type safe (may cause Core Lint to fail), -- or may otherwise change the semantics of the program. -- Only available in unsafe mode! | Safe -- ^ Include in Strict Safety mode (currently unused) | Proof -- ^ Commands related to proving lemmas. | TODO -- ^ An incomplete or potentially buggy command. | Experiment -- ^ Things we are trying out. | Deprecated -- ^ A command that will be removed in a future release; -- it has probably been renamed or subsumed by another command. deriving (Eq, Show, Read, Bounded, Enum) -- | Lists all the tags paired with a short description of what they're about. dictionaryOfTags :: [(CmdTag,String)] dictionaryOfTags = notes ++ [ (tag,"(unknown purpose)") | tag <- [minBound..maxBound] , tag `notElem` map fst notes ] where notes = -- These should give the user a clue about what the sub-commands might do [ (Shell, "Shell-specific command.") , (Eval, "The arrow of evaluation (reduces a term).") , (KURE, "Direct reflection of a combinator from the KURE DSL.") , (Loop, "Command may operate multiple times.") , (Deep, "Command may make a deep change, can be O(n).") , (Shallow, "Command operates on local nodes only, O(1).") , (Navigation, "Navigate via focus, or directional command.") , (Query, "Extract information from an expression.") , (Predicate, "Something that passes or fails.") , (Introduce, "Introduce something, like a new name.") , (Commute, "Commute is when you swap nested terms.") , (PreCondition, "Operation has a (perhaps undocumented) precondition.") , (Strictness, "Alters the strictness of an expression.") , (Debug, "A command specifically to help debugging.") , (VersionControl, "Version control for Core syntax.") , (Context, "A command that uses its context, such as inlining.") , (Unsafe, "Commands that are not type safe (may cause Core Lint to fail), or may otherwise change the semantics of the program.") , (Proof, "Commands related to proving lemmas.") , (TODO, "An incomplete or potentially buggy command.") , (Experiment, "Things we are trying out, use at your own risk.") , (Deprecated, "A command that will be removed in a future release; it has probably been renamed or subsumed by another command.") ] -- Unfortunately, record update syntax seems to associate to the right. -- These operators save us some parentheses. infixl 3 .+ infixr 4 .|| infixr 5 .& -- | A data type of logical operations on tags. data TagE :: * where Tag :: Tag a => a -> TagE NotTag :: TagE -> TagE AndTag :: TagE -> TagE -> TagE OrTag :: TagE -> TagE -> TagE -- | Tags are meta-data that we add to 'External's to make them sortable and searchable. class Tag a where toTagE :: a -> TagE -- | Add a 'Tag' to an 'External'. (.+) :: External -> a -> External -- | Remove a 'Tag' from an 'External'. remTag :: a -> External -> External -- | Check if an 'External' has the specified 'Tag'. tagMatch :: a -> External -> Bool instance Tag TagE where toTagE = id e .+ (Tag t) = e .+ t e .+ (NotTag t) = remTag t e e .+ (AndTag t1 t2) = e .+ t1 .+ t2 e .+ (OrTag t1 t2) = e .+ t1 .+ t2 -- not sure what else to do remTag (Tag t) e = remTag t e remTag (NotTag t) e = e .+ t remTag (AndTag t1 t2) e = remTag t1 (remTag t2 e) remTag (OrTag t1 t2) e = remTag t1 (remTag t2 e) -- again tagMatch (Tag t) e = tagMatch t e tagMatch (NotTag t) e = not (tagMatch t e) tagMatch (AndTag t1 t2) e = tagMatch t1 e && tagMatch t2 e tagMatch (OrTag t1 t2) e = tagMatch t1 e || tagMatch t2 e instance Tag CmdTag where toTagE = Tag ex@(External {externTags = ts}) .+ t = ex {externTags = t:ts} remTag t ex@(External {externTags = ts}) = ex { externTags = [ t' | t' <- ts, t' /= t ] } tagMatch t (External {externTags = ts}) = t `elem` ts -- | An \"and\" on 'Tag's. (.&) :: (Tag a, Tag b) => a -> b -> TagE t1 .& t2 = AndTag (toTagE t1) (toTagE t2) -- | An \"or\" on 'Tag's. (.||) :: (Tag a, Tag b) => a -> b -> TagE t1 .|| t2 = OrTag (toTagE t1) (toTagE t2) -- how to make a unary operator? -- | A \"not\" on 'Tag's. notT :: Tag a => a -> TagE notT = NotTag . toTagE ----------------------------------------------------------------- -- | An 'External' is a 'Dynamic' value with some associated meta-data (name, help string and tags). data External = External { externName :: ExternalName -- ^ Get the name of an 'External'. , externDyn :: Dynamic -- ^ Get the 'Dynamic' value stored in an 'External'. , externHelp :: ExternalHelp -- ^ Get the list of help 'String's for an 'External'. , externTags :: [CmdTag] -- ^ List all the 'CmdTag's associated with an 'External' } -- | The primitive way to build an 'External'. external :: Extern a => ExternalName -> a -> ExternalHelp -> External external nm fn help = External { externName = nm , externDyn = toDyn (box fn) , externHelp = map (" " ++) help , externTags = [] } -- | Get all the 'External's which match a given tag predicate -- and box a Transform of the appropriate type. matchingExternals :: (Extern tr, Tag t) => t -> [External] -> [(External, tr)] matchingExternals tag exts = [ (e,tr) | e <- exts, tagMatch tag e , Just tr <- [fmap unbox $ fromDynamic $ externDyn e] ] -- | Build a 'Data.Map' from names to help information. toHelp :: [External] -> Map ExternalName ExternalHelp toHelp = fromListWith (++) . map toH where toH :: External -> (ExternalName,ExternalHelp) toH e = (externName e, spaceout (externName e ++ " :: " ++ externTypeString e) (show (externTags e)) : externHelp e) spaceout xs ys = xs ++ replicate (width - (length xs + length ys)) ' ' ++ ys width = 78 -- | Get a string representation of the (monomorphic) type of an 'External' externTypeString :: External -> String externTypeString = deBoxify . show . dynTypeRep . externDyn -- | Remove the word 'Box' from a string. deBoxify :: String -> String deBoxify s | "CLSBox -> " `isPrefixOf` s = go (drop 10 s) | "PrettyPrinter -> " `isPrefixOf` s = go (drop 17 s) | otherwise = go s where go xs | "Box" `isPrefixOf` xs = go (drop 3 xs) go (x:xs) = x : go xs go [] = [] externTypeArgResString :: External -> ([String], String) externTypeArgResString e = (map (deBoxify . show) aTys, deBoxify (show rTy)) where (aTys, rTy) = splitExternFunType e splitExternFunType :: External -> ([TypeRep], TypeRep) splitExternFunType = splitFunTyArgs . dynTypeRep . externDyn splitFunTyArgs :: TypeRep -> ([TypeRep], TypeRep) splitFunTyArgs tr = case splitFunTyMaybe tr of Nothing -> ([], tr) Just (a, r) -> let (as, r') = splitFunTyArgs r in (a:as, r') splitFunTyMaybe :: TypeRep -> Maybe (TypeRep, TypeRep) #if __GLASGOW_HASKELL__ < 710 splitFunTyMaybe (TypeRep _ tc [a,r]) | tc == funTc = Just (a,r) #else splitFunTyMaybe (TypeRep _ tc _krs [a,r]) | tc == funTc = Just (a,r) #endif splitFunTyMaybe _ = Nothing ----------------------------------------------------------------- -- | The class of things that can be made into 'External's. -- To be an 'Extern' there must exist an isomorphic 'Box' type that is an instance of 'Typeable'. class Typeable (Box a) => Extern a where -- | An isomorphic wrapper. type Box a -- | Wrap a value in a 'Box'. box :: a -> Box a -- | Unwrap a value from a 'Box'. unbox :: Box a -> a ----------------------------------------------------------------- instance (Extern a, Extern b) => Extern (a -> b) where type Box (a -> b) = Box a -> Box b box f = box . f . unbox unbox f = unbox . f . box ----------------------------------------------------------------- data TagBox = TagBox TagE deriving Typeable instance Extern TagE where type Box TagE = TagBox box = TagBox unbox (TagBox t) = t ----------------------------------------------------------------- data IntBox = IntBox Int deriving Typeable instance Extern Int where type Box Int = IntBox box = IntBox unbox (IntBox i) = i ----------------------------------------------------------------- -- TODO: Considering unifying CrumbBox and PathBox under TransformLCoreTCPathBox. data CrumbBox = CrumbBox Crumb deriving Typeable instance Extern Crumb where type Box Crumb = CrumbBox box = CrumbBox unbox (CrumbBox cr) = cr ----------------------------------------------------------------- data PathBox = PathBox LocalPathH deriving Typeable instance Extern LocalPathH where type Box LocalPathH = PathBox box = PathBox unbox (PathBox p) = p ----------------------------------------------------------------- newtype CoreString = CoreString { unCoreString :: String } deriving Typeable instance Extern CoreString where type Box CoreString = CoreString box = id unbox = id ----------------------------------------------------------------- data StringBox = StringBox String deriving Typeable instance Extern String where type Box String = StringBox box = StringBox unbox (StringBox s) = s ----------------------------------------------------------------- data StringListBox = StringListBox [String] deriving Typeable instance Extern [String] where type Box [String] = StringListBox box = StringListBox unbox (StringListBox l) = l ----------------------------------------------------------------- data IntListBox = IntListBox [Int] deriving Typeable instance Extern [Int] where type Box [Int] = IntListBox box = IntListBox unbox (IntListBox l) = l ----------------------------------------------------------------- instance Extern LemmaName where type Box LemmaName = LemmaName box = id unbox = id ----------------------------------------------------------------- data RewriteLCoreBox = RewriteLCoreBox (RewriteH LCore) deriving Typeable instance Extern (RewriteH LCore) where type Box (RewriteH LCore) = RewriteLCoreBox box = RewriteLCoreBox unbox (RewriteLCoreBox r) = r ----------------------------------------------------------------- data TransformLCoreStringBox = TransformLCoreStringBox (TransformH LCore String) deriving Typeable instance Extern (TransformH LCore String) where type Box (TransformH LCore String) = TransformLCoreStringBox box = TransformLCoreStringBox unbox (TransformLCoreStringBox t) = t ----------------------------------------------------------------- data TransformLCoreUnitBox = TransformLCoreUnitBox (TransformH LCore ()) deriving Typeable instance Extern (TransformH LCore ()) where type Box (TransformH LCore ()) = TransformLCoreUnitBox box = TransformLCoreUnitBox unbox (TransformLCoreUnitBox t) = t ----------------------------------------------------------------- data TransformLCorePathBox = TransformLCorePathBox (TransformH LCore LocalPathH) deriving Typeable instance Extern (TransformH LCore LocalPathH) where type Box (TransformH LCore LocalPathH) = TransformLCorePathBox box = TransformLCorePathBox unbox (TransformLCorePathBox t) = t ----------------------------------------------------------------- data BiRewriteLCoreBox = BiRewriteLCoreBox (BiRewriteH LCore) deriving Typeable instance Extern (BiRewriteH LCore) where type Box (BiRewriteH LCore) = BiRewriteLCoreBox box = BiRewriteLCoreBox unbox (BiRewriteLCoreBox b) = b ----------------------------------------------------------------- data RewriteLCoreListBox = RewriteLCoreListBox [RewriteH LCore] deriving Typeable instance Extern [RewriteH LCore] where type Box [RewriteH LCore] = RewriteLCoreListBox box = RewriteLCoreListBox unbox (RewriteLCoreListBox l) = l ----------------------------------------------------------------- data RewriteLCoreTCBox = RewriteLCoreTCBox (RewriteH LCoreTC) deriving Typeable instance Extern (RewriteH LCoreTC) where type Box (RewriteH LCoreTC) = RewriteLCoreTCBox box = RewriteLCoreTCBox unbox (RewriteLCoreTCBox r) = r ----------------------------------------------------------------- data TransformLCoreTCStringBox = TransformLCoreTCStringBox (TransformH LCoreTC String) deriving Typeable instance Extern (TransformH LCoreTC String) where type Box (TransformH LCoreTC String) = TransformLCoreTCStringBox box = TransformLCoreTCStringBox unbox (TransformLCoreTCStringBox t) = t ----------------------------------------------------------------- data TransformLCoreTCUnitBox = TransformLCoreTCUnitBox (TransformH LCoreTC ()) deriving Typeable instance Extern (TransformH LCoreTC ()) where type Box (TransformH LCoreTC ()) = TransformLCoreTCUnitBox box = TransformLCoreTCUnitBox unbox (TransformLCoreTCUnitBox t) = t ----------------------------------------------------------------- data TransformLCoreTCLCoreBox = TransformLCoreTCLCoreBox (TransformH LCoreTC LCore) deriving Typeable instance Extern (TransformH LCoreTC LCore) where type Box (TransformH LCoreTC LCore) = TransformLCoreTCLCoreBox box = TransformLCoreTCLCoreBox unbox (TransformLCoreTCLCoreBox t) = t ----------------------------------------------------------------- data TransformLCoreTCPathBox = TransformLCoreTCPathBox (TransformH LCoreTC LocalPathH) deriving Typeable instance Extern (TransformH LCoreTC LocalPathH) where type Box (TransformH LCoreTC LocalPathH) = TransformLCoreTCPathBox box = TransformLCoreTCPathBox unbox (TransformLCoreTCPathBox t) = t ----------------------------------------------------------------- data BiRewriteLCoreTCBox = BiRewriteLCoreTCBox (BiRewriteH LCoreTC) deriving Typeable instance Extern (BiRewriteH LCoreTC) where type Box (BiRewriteH LCoreTC) = BiRewriteLCoreTCBox box = BiRewriteLCoreTCBox unbox (BiRewriteLCoreTCBox b) = b ----------------------------------------------------------------- data RewriteLCoreTCListBox = RewriteLCoreTCListBox [RewriteH LCoreTC] deriving Typeable instance Extern [RewriteH LCoreTC] where type Box [RewriteH LCoreTC] = RewriteLCoreTCListBox box = RewriteLCoreTCListBox unbox (RewriteLCoreTCListBox l) = l -----------------------------------------------------------------