hermit-0.6.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.

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.

data BiRewriteCoreBox Source

Constructors

BiRewriteCoreBox (BiRewriteH Core) 

Instances

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

Constructors

RewriteCoreBox (RewriteH Core) 

Instances

data RewriteCoreListBox Source

Constructors

RewriteCoreListBox [RewriteH Core] 

Instances

data RewriteCoreTCBox Source

Constructors

RewriteCoreTCBox (RewriteH CoreTC) 

Instances

data RewriteEqualityBox Source

Constructors

RewriteEqualityBox (RewriteH Equality) 

Instances

data StringBox Source

Constructors

StringBox String 

Instances

data StringListBox Source

Constructors

StringListBox [String] 

Instances

data TagBox Source

Constructors

TagBox TagE 

Instances

data TransformCoreCheckBox Source

Constructors

TransformCoreCheckBox (TransformH Core ()) 

Instances

data TransformCorePathBox Source

Constructors

TransformCorePathBox (TransformH Core LocalPathH) 

Instances

data TransformCoreStringBox Source

Constructors

TransformCoreStringBox (TransformH Core String) 

Instances

data TransformCoreTCCheckBox Source

Constructors

TransformCoreTCCheckBox (TransformH CoreTC ()) 

Instances

data TransformCoreTCPathBox Source

Constructors

TransformCoreTCPathBox (TransformH CoreTC LocalPathH) 

Instances

data TransformCoreTCStringBox Source

Constructors

TransformCoreTCStringBox (TransformH CoreTC String) 

Instances

data TransformEqualityStringBox Source

Constructors

TransformEqualityStringBox (TransformH Equality String) 

Instances