hermit-0.3.1.0: Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone

HERMIT.External

Contents

Synopsis

Externals

data External Source

An External is a Dynamic value with some associated meta-data (name, help string and tags).

type ExternalName = StringSource

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.

externDyn :: External -> DynamicSource

Get the Dynamic value stored in an External.

externHelp :: External -> ExternalHelpSource

Get the list of help Strings for an External.

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] -> DictionarySource

Build a Map from names to Dynamic values.

toHelp :: [External] -> Map ExternalName ExternalHelpSource

Build a Map from names to help information.

external :: Extern a => ExternalName -> a -> ExternalHelp -> ExternalSource

The primitive way to build an External.

class Typeable (Box a) => Extern a whereSource

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.

Associated Types

type Box a Source

An isomorphic wrapper.

Methods

box :: a -> Box aSource

Wrap a value in a Box.

unbox :: Box a -> aSource

Unwrap a value from a Box.

matchingExternals :: (Extern tr, Tag t) => t -> [External] -> [(External, tr)]Source

Get all the Externals which match a given tag predicate and box a Translate of the appropriate type.

Tags

data CmdTag Source

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

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

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.

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.

data TagE Source

A data type of logical operations on tags.

Instances

class Tag a whereSource

Tags are meta-data that we add to Externals to make them sortable and searchable.

Methods

(.+) :: External -> a -> ExternalSource

Add a Tag to an External.

remTag :: a -> External -> ExternalSource

Remove a Tag from an External.

tagMatch :: a -> External -> BoolSource

Check if an External has the specified Tag.

Instances

(.&) :: (Tag a, Tag b) => a -> b -> TagESource

An "and" on Tags.

(.||) :: (Tag a, Tag b) => a -> b -> TagESource

An "or" on Tags.

notT :: Tag a => a -> TagESource

A "not" on Tags.

externTags :: External -> [CmdTag]Source

List all the CmdTags associated with an External

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 TagBox Source

Constructors

TagBox TagE 

Instances

data IntBox Source

Constructors

IntBox Int 

Instances

data NameBox Source

Constructors

NameBox Name 

Instances

newtype CoreString Source

Constructors

CoreString 

Fields

unCoreString :: String
 

Instances

data CoreBox Source

Constructors

CoreBox CoreString 

Instances

data CrumbBox Source

Constructors

CrumbBox Crumb 

Instances

data PathBox Source

Constructors

PathBox LocalPathH 

Instances

data StringBox Source

Constructors

StringBox String 

Instances

data NameListBox Source

Constructors

NameListBox [Name] 

data IntListBox Source

Constructors

IntListBox [Int] 

Instances