module HERMIT.External
(
External
, ExternalName
, ExternalHelp
, externName
, externDyn
, externHelp
, externTypeString
, externTypeArgResString
, splitFunTyArgs
, toHelp
, external
, Extern(..)
, matchingExternals
, CmdTag(..)
, TagE
, Tag((.+),remTag,tagMatch)
, (.&)
, (.||)
, notT
, externTags
, dictionaryOfTags
, CoreString(..)
, CrumbBox(..)
, IntBox(..)
, IntListBox(..)
, PathBox(..)
, StringBox(..)
, StringListBox(..)
, TagBox(..)
, TransformLCoreStringBox(..)
, TransformLCoreUnitBox(..)
, TransformLCorePathBox(..)
, RewriteLCoreBox(..)
, BiRewriteLCoreBox(..)
, RewriteLCoreListBox(..)
, 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
type ExternalName = String
type ExternalHelp = [String]
data CmdTag = Shell
| Eval
| KURE
| Loop
| Deep
| Shallow
| Navigation
| Query
| Predicate
| Introduce
| Commute
| PreCondition
| Strictness
| Debug
| VersionControl
| Context
| Unsafe
| Safe
| Proof
| TODO
| Experiment
| Deprecated
deriving (Eq, Show, Read, Bounded, Enum)
dictionaryOfTags :: [(CmdTag,String)]
dictionaryOfTags = notes ++ [ (tag,"(unknown purpose)")
| tag <- [minBound..maxBound]
, tag `notElem` map fst notes
]
where notes =
[ (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.")
]
infixl 3 .+
infixr 4 .||
infixr 5 .&
data TagE :: * where
Tag :: Tag a => a -> TagE
NotTag :: TagE -> TagE
AndTag :: TagE -> TagE -> TagE
OrTag :: TagE -> TagE -> TagE
class Tag a where
toTagE :: a -> TagE
(.+) :: External -> a -> External
remTag :: a -> External -> External
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
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)
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
(.&) :: (Tag a, Tag b) => a -> b -> TagE
t1 .& t2 = AndTag (toTagE t1) (toTagE t2)
(.||) :: (Tag a, Tag b) => a -> b -> TagE
t1 .|| t2 = OrTag (toTagE t1) (toTagE t2)
notT :: Tag a => a -> TagE
notT = NotTag . toTagE
data External = External
{ externName :: ExternalName
, externDyn :: Dynamic
, externHelp :: ExternalHelp
, externTags :: [CmdTag]
}
external :: Extern a => ExternalName -> a -> ExternalHelp -> External
external nm fn help = External
{ externName = nm
, externDyn = toDyn (box fn)
, externHelp = map (" " ++) help
, externTags = []
}
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] ]
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
externTypeString :: External -> String
externTypeString = deBoxify . show . dynTypeRep . externDyn
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)
splitFunTyMaybe (TypeRep _ tc [a,r]) | tc == funTc = Just (a,r)
splitFunTyMaybe _ = Nothing
class Typeable (Box a) => Extern a where
type Box a
box :: a -> Box a
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
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