| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
HERMIT.External
- data External
- type ExternalName = String
- type ExternalHelp = [String]
- externName :: External -> ExternalName
- externDyn :: External -> Dynamic
- externHelp :: External -> ExternalHelp
- externTypeString :: External -> String
- externTypeArgResString :: External -> ([String], String)
- type Dictionary = Map ExternalName [Dynamic]
- toDictionary :: [External] -> Dictionary
- addToDictionary :: External -> Dictionary -> Dictionary
- toHelp :: [External] -> Map ExternalName ExternalHelp
- external :: Extern a => ExternalName -> a -> ExternalHelp -> External
- class Typeable (Box a) => Extern a where
- matchingExternals :: (Extern tr, Tag t) => t -> [External] -> [(External, tr)]
- data CmdTag
- = Shell
- | Eval
- | KURE
- | Loop
- | Deep
- | Shallow
- | Navigation
- | Query
- | Predicate
- | Introduce
- | Commute
- | PreCondition
- | Debug
- | VersionControl
- | Context
- | Unsafe
- | Proof
- | TODO
- | Experiment
- | Deprecated
- data TagE :: *
- class Tag a where
- (.&) :: (Tag a, Tag b) => a -> b -> TagE
- (.||) :: (Tag a, Tag b) => a -> b -> TagE
- notT :: Tag a => a -> TagE
- externTags :: External -> [CmdTag]
- dictionaryOfTags :: [(CmdTag, String)]
- data TagBox = TagBox TagE
- data IntBox = IntBox Int
- data RewriteCoreBox = RewriteCoreBox (RewriteH Core)
- data RewriteCoreTCBox = RewriteCoreTCBox (RewriteH CoreTC)
- data BiRewriteCoreBox = BiRewriteCoreBox (BiRewriteH Core)
- data TransformCoreStringBox = TransformCoreStringBox (TransformH Core String)
- data TransformCoreTCStringBox = TransformCoreTCStringBox (TransformH CoreTC String)
- data TransformCoreCheckBox = TransformCoreCheckBox (TransformH Core ())
- data TransformCoreTCCheckBox = TransformCoreTCCheckBox (TransformH CoreTC ())
- data TransformCorePathBox = TransformCorePathBox (TransformH Core LocalPathH)
- data TransformCoreTCPathBox = TransformCoreTCPathBox (TransformH CoreTC LocalPathH)
- newtype CoreString = CoreString {}
- data CoreBox = CoreBox CoreString
- data CrumbBox = CrumbBox Crumb
- data PathBox = PathBox LocalPathH
- data StringBox = StringBox String
- data StringListBox = StringListBox [String]
- data IntListBox = IntListBox [Int]
- data RewriteCoreListBox = RewriteCoreListBox [RewriteH Core]
Externals
type ExternalName = String Source
External names are just strings.
type ExternalHelp = [String] Source
Help information for Externals is stored as a list of strings, designed for multi-line displaying.
externName :: External -> ExternalName Source
Get the name of an External.
externHelp :: External -> ExternalHelp Source
externTypeString :: External -> String Source
Get a string representation of the (monomorphic) type of an External
externTypeArgResString :: External -> ([String], String) Source
type Dictionary = Map ExternalName [Dynamic] Source
A Dictionary is a collection of Dynamics.
Looking up a Dynamic (via an ExternalName key) returns a list, as there can be multiple Dynamics with the same name.
toDictionary :: [External] -> Dictionary Source
addToDictionary :: External -> Dictionary -> Dictionary Source
toHelp :: [External] -> Map ExternalName ExternalHelp Source
Build a Map from names to help information.
external :: Extern a => ExternalName -> a -> ExternalHelp -> External Source
The primitive way to build an External.
class Typeable (Box a) => Extern a where Source
The class of things that can be made into Externals.
To be an Extern there must exist an isomorphic Box type that is an instance of Typeable.
Instances
matchingExternals :: (Extern tr, Tag t) => t -> [External] -> [(External, tr)] Source
Get all the Externals which match a given tag predicate
and box a Transform of the appropriate type.
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.
Constructors
| Shell | Shell-specific command. |
| Eval | The arrow of evaluation (reduces a term). |
| KURE |
|
| 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 | |
| Query | A question we ask. |
| 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. |
| 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. |
| 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. |
A data type of logical operations on tags.
Tags are meta-data that we add to Externals to make them sortable and searchable.
dictionaryOfTags :: [(CmdTag, String)] Source
Lists all the tags paired with a short description of what they're about.
Boxes
Boxes are used by the Extern class.
data TransformCoreStringBox Source
Constructors
| TransformCoreStringBox (TransformH Core String) |
Instances
data TransformCoreTCStringBox Source
Constructors
| TransformCoreTCStringBox (TransformH CoreTC String) |
Instances
data TransformCoreTCCheckBox Source
Constructors
| TransformCoreTCCheckBox (TransformH CoreTC ()) |
Instances
data TransformCorePathBox Source
Constructors
| TransformCorePathBox (TransformH Core LocalPathH) |
Instances
data TransformCoreTCPathBox Source
Constructors
| TransformCoreTCPathBox (TransformH CoreTC LocalPathH) |
Instances
newtype CoreString Source
Constructors
| CoreString | |
Fields | |
Instances
| Extern CoreString | |
| type Box CoreString = CoreBox |