Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data External
- type ExternalName = String
- type ExternalHelp = [String]
- externName :: External -> ExternalName
- externDyn :: External -> Dynamic
- externHelp :: External -> ExternalHelp
- externTypeString :: External -> String
- externTypeArgResString :: External -> ([String], String)
- splitFunTyArgs :: TypeRep -> ([TypeRep], TypeRep)
- 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
- | Strictness
- | Debug
- | VersionControl
- | Context
- | Unsafe
- | Safe
- | 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)]
- newtype CoreString = CoreString {}
- data CrumbBox = CrumbBox Crumb
- data IntBox = IntBox Int
- data IntListBox = IntListBox [Int]
- data PathBox = PathBox LocalPathH
- data StringBox = StringBox String
- data StringListBox = StringListBox [String]
- data TagBox = TagBox TagE
- data TransformLCoreStringBox = TransformLCoreStringBox (TransformH LCore String)
- data TransformLCoreUnitBox = TransformLCoreUnitBox (TransformH LCore ())
- data TransformLCorePathBox = TransformLCorePathBox (TransformH LCore LocalPathH)
- data RewriteLCoreBox = RewriteLCoreBox (RewriteH LCore)
- data BiRewriteLCoreBox = BiRewriteLCoreBox (BiRewriteH LCore)
- data RewriteLCoreListBox = RewriteLCoreListBox [RewriteH LCore]
- data TransformLCoreTCStringBox = TransformLCoreTCStringBox (TransformH LCoreTC String)
- data TransformLCoreTCUnitBox = TransformLCoreTCUnitBox (TransformH LCoreTC ())
- data TransformLCoreTCLCoreBox = TransformLCoreTCLCoreBox (TransformH LCoreTC LCore)
- data TransformLCoreTCPathBox = TransformLCoreTCPathBox (TransformH LCoreTC LocalPathH)
- data RewriteLCoreTCBox = RewriteLCoreTCBox (RewriteH LCoreTC)
- data BiRewriteLCoreTCBox = BiRewriteLCoreTCBox (BiRewriteH LCoreTC)
- data RewriteLCoreTCListBox = RewriteLCoreTCListBox [RewriteH LCoreTC]
Externals
type ExternalName = String Source
External
names are just strings.
type ExternalHelp = [String] Source
Help information for External
s 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
splitFunTyArgs :: TypeRep -> ([TypeRep], TypeRep) 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 External
s.
To be an Extern
there must exist an isomorphic Box
type that is an instance of Typeable
.
matchingExternals :: (Extern tr, Tag t) => t -> [External] -> [(External, tr)] Source
Get all the External
s 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.
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 | 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. |
A data type of logical operations on tags.
Tags are meta-data that we add to External
s 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.
newtype CoreString Source
Extern CoreString | |
Typeable * CoreString | |
type Box CoreString = CoreString |