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

Safe HaskellNone
LanguageHaskell2010

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 = 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.

externDyn :: External -> Dynamic Source

Get the Dynamic value stored in an External.

externHelp :: External -> ExternalHelp Source

Get the list of help Strings for an External.

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

Wrap a value in a Box.

unbox :: Box a -> a Source

Unwrap a value from a Box.

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

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

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.

Instances

data TagE :: * Source

A data type of logical operations on tags.

Instances

class Tag a where Source

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

Minimal complete definition

toTagE, (.+), remTag, tagMatch

Methods

(.+) :: External -> a -> External infixl 3 Source

Add a Tag to an External.

remTag :: a -> External -> External Source

Remove a Tag from an External.

tagMatch :: a -> External -> Bool Source

Check if an External has the specified Tag.

Instances

(.&) :: (Tag a, Tag b) => a -> b -> TagE infixr 5 Source

An "and" on Tags.

(.||) :: (Tag a, Tag b) => a -> b -> TagE infixr 4 Source

An "or" on Tags.

notT :: Tag a => a -> TagE Source

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.

newtype CoreString Source

Constructors

CoreString 

Fields

unCoreString :: String
 

Instances

data CrumbBox Source

Constructors

CrumbBox Crumb 

Instances

data IntBox Source

Constructors

IntBox Int 

Instances

data IntListBox Source

Constructors

IntListBox [Int] 

Instances

data PathBox Source

Constructors

PathBox LocalPathH 

Instances

data StringBox Source

Constructors

StringBox String 

Instances

data StringListBox Source

Constructors

StringListBox [String] 

Instances

data TagBox Source

Constructors

TagBox TagE 

Instances

LCore Boxes

data TransformLCoreStringBox Source

Constructors

TransformLCoreStringBox (TransformH LCore String) 

Instances

data TransformLCoreUnitBox Source

Constructors

TransformLCoreUnitBox (TransformH LCore ()) 

Instances

data TransformLCorePathBox Source

Constructors

TransformLCorePathBox (TransformH LCore LocalPathH) 

Instances

data RewriteLCoreBox Source

Constructors

RewriteLCoreBox (RewriteH LCore) 

Instances

data BiRewriteLCoreBox Source

Constructors

BiRewriteLCoreBox (BiRewriteH LCore) 

Instances

data RewriteLCoreListBox Source

Constructors

RewriteLCoreListBox [RewriteH LCore] 

Instances

LCoreTC Boxes

data TransformLCoreTCStringBox Source

Constructors

TransformLCoreTCStringBox (TransformH LCoreTC String) 

Instances

data TransformLCoreTCUnitBox Source

Constructors

TransformLCoreTCUnitBox (TransformH LCoreTC ()) 

Instances

data TransformLCoreTCLCoreBox Source

Constructors

TransformLCoreTCLCoreBox (TransformH LCoreTC LCore) 

Instances

data TransformLCoreTCPathBox Source

Constructors

TransformLCoreTCPathBox (TransformH LCoreTC LocalPathH) 

Instances

data RewriteLCoreTCBox Source

Constructors

RewriteLCoreTCBox (RewriteH LCoreTC) 

Instances

data BiRewriteLCoreTCBox Source

Constructors

BiRewriteLCoreTCBox (BiRewriteH LCoreTC) 

Instances

data RewriteLCoreTCListBox Source

Constructors

RewriteLCoreTCListBox [RewriteH LCoreTC] 

Instances