HaskHOL.Core.Parser

This module defines the parsers for HOLTypes and HOLTerms.

It also re-exports the related benign flags, theory extension mechanisms, and type/term elaborators.

For examples of the parsers and elaborators in use see the HaskHOL.Core.TermRep module.

Parser Data Types

data PreTerm

Parsed, but pre-elaborated HOL terms.

Instances

Show PreTerm

HOLTermRep PreTerm a

data PreType

Parsed, but pre-elaborated HOL types.

Instances

Eq PreType

Show PreType

HOLTypeRep PreType a

Type Elaboration Flags

data FlagIgnoreConstVarstruct

Flag to say whether to treat a constant varstruct, i.e. \ const . bod, as variable.

Constructors

FlagIgnoreConstVarstruct

Instances

Typeable FlagIgnoreConstVarstruct

BenignFlag FlagIgnoreConstVarstruct

data FlagTyInvWarning

Flag indicating that the user should be warned if a type variable was invented during parsing.

Constructors

FlagTyInvWarning

Instances

Typeable FlagTyInvWarning

BenignFlag FlagTyInvWarning

data FlagTyOpInvWarning

Flag indicating that the user should be warned if a type operator variable was invented during parsing.

Constructors

FlagTyOpInvWarning

Instances

Typeable FlagTyOpInvWarning

BenignFlag FlagTyOpInvWarning

data FlagAddTyAppsAuto

Flag to say whether implicit type applications are to be added during parsing.

Constructors

FlagAddTyAppsAuto

Instances

Typeable FlagAddTyAppsAuto

BenignFlag FlagAddTyAppsAuto

Extensible Parser Operators

parseAsBinder :: String -> HOL Theory thry ()

Specifies a String to be recognized as a term binder by the parser.

parseAsTyBinder :: String -> HOL Theory thry ()

Specifies a String to be recognized as a type binder by the parser.

parseAsPrefix :: String -> HOL Theory thry ()

Specifies a String to be recognized as a prefix operator by the parser.

parseAsInfix :: (String, (Int, Assoc)) -> HOL Theory thry ()

Specifies a String to be recognized as an infix operator by the parser with a given precedence level and associativity.

unparseAsBinder :: String -> HOL Theory thry ()

Specifies a String for the parser to stop recognizing as a term binder.

unparseAsTyBinder :: String -> HOL Theory thry ()

Specifies a String for the parser to stop recognizing as a type binder.

unparseAsPrefix :: String -> HOL Theory thry ()

Specifies a String for the parser to stop recognizing as a prefix operator.

unparseAsInfix :: String -> HOL Theory thry ()

Specifies a String for the parser to stop recognizing as an infix operator.

binders :: HOLContext thry -> [String]

Returns all Strings recognized as term binders by the parser.

tyBinders :: HOLContext thry -> [String]

Returns all Strings recognized as type binders by the parser.

prefixes :: HOLContext thry -> [String]

Returns all Strings recognized as prefix operators by the parser.

infixes :: HOLContext thry -> [(String, (Int, Assoc))]

Returns all Strings recognized as infix operators by the parser along with their precedence and associativity pairs.

parsesAsBinder :: String -> HOLContext thry -> Bool

Predicate for Strings recognized as term binders by the parser.

parsesAsTyBinder :: String -> HOLContext thry -> Bool

Predicate for Strings recognized as term binders by the parser.

isPrefix :: String -> HOLContext thry -> Bool

Predicate for Strings recognized as prefix operators by the parser.

getInfixStatus :: String -> HOLContext thry -> Maybe (Int, Assoc)

Predicate for Strings recognized as infix operators by the parser. Returns a precidence and associativity pair guarded by Maybe.

Overloading and Interface Mapping

makeOverloadable :: String -> HOLType -> HOL Theory thry ()

Specifies a String that can act as an overloadable identifier within the parser. The provided type is the most general type that instances of this symbol may have. Throws a HOLException if the given symbol has already been declared as overloadable with a different type.

Note that defining a symbol as overloadable will erase any interface overloads that were previously introduced via overrideInterface in order to guarantee that all overloads are matchable with their most general type.

removeInterface :: String -> HOL Theory thry ()

Removes all instances of an overloaded symbol from the interface.

reduceInterface :: String -> HOLTerm -> HOL Theory thry ()

Removes a specific instance of an overloaded symbol from the interface. Throws a HOLException if the provided term is not a constant or varible term representing an instance of the overloaded symbol.

overrideInterface :: String -> HOLTerm -> HOL Theory thry ()

Removes all existing overloads for a given symbol and replaces them with a single, specific instance. Throws a HOLException if the provided term is not a constant or variable term representing an instance of the overloaded symbol.

Note that because overrideInterface can introduce at most one overload for a symbol it does not have to be previously defined as overloadable via makeOverloadable. However, if the symbol is defined as overloadable then the provided term must have a type that is matchable with the symbol's most general type.

overloadInterface :: String -> HOLTerm -> HOL Theory thry ()

Introduces a new overload for a given symbol. Throws a HOLException in the following cases:

• The symbol has not previously been defined as overloadable via makeOverloadable.
• The provided term is not a constant or variable term representing a specific instance of the overloaded symbol.
• The provided term does not have a type that is matchable with the overloadable symbol's specified most general type.

Note that specifying an overload that already exists will move it to the front of the interface list, effectively prioritizing it. This behavior is utilized by prioritizeOverload.

prioritizeOverload :: HOLType -> HOL Theory thry ()

Specifies a type to prioritize when the interface is used to overload a symbol. Note that this applies to all overloads in the system whose match with the specified most general type involves the provided type. Prioritization is done by redefining overloads via overloadInterface.

getInterface :: HOLContext thry -> [(String, (String, HOLType))]

Returns the list of all currently defined interface overloads.

getOverloads :: HOLContext thry -> [(String, HOLType)]

Returns the list of all overloadable symbols paired with their most generic types.

Type Abbreviations

newTypeAbbrev :: String -> HOLType -> HOL Theory thry ()

Specifies a String to act as an abbreviation for a given type in the parser. Upon recognizing the abbreviation the parser will replace it with the PreType value for it's associated HOLType such that the elaborator can infer the correct type for polymorphic abbreviations.

removeTypeAbbrev :: String -> HOL Theory thry ()

Specifies a String for the parser to stop recognizing as a type abbreviation.

typeAbbrevs :: HOLContext thry -> [(String, HOLType)]

Returns all Strings currently acting as type abbreviations in the parser paired with their associated types.

Hidden Constant Mapping

hideConstant :: String -> HOL Theory thry ()

Specifies a String for the parser to stop recognizing as a constant.

unhideConstant :: String -> HOL Theory thry ()

Specifies a String for the parser to resume recognizing as a constant.

getHidden :: HOLContext thry -> [String]

Returns all Strings currently acting as constants hidden from the parser.

Elaboration Functions

tyElab :: PreType -> HOL cls thry HOLType

Elaborator for PreTypes.

elab :: PreTerm -> HOL cls thry HOLTerm

Elaborator and type inference for PreTerms.

Parsing Functions

holTypeParser :: String -> HOLContext thry -> Either ParseError PreType

Parser for HOLTypes.

holTermParser :: String -> HOLContext thry -> Either ParseError PreTerm

Parser for HOLTerms.

Type/Term Representation Conversions

class HOLTypeRep a thry | a -> thry where

The HOLTypeRep class provides a conversion from an alternative representation of types to HOLType within the HOL monad.

The first parameter is the type of the alternative representation.

The second parameter is the tag for the last checkpoint of the current working theory. This enables us to have a conversion from representations that are theory dependent without running into type matchability issues.

Methods

toHTy :: a -> HOL cls thry HOLType

Conversion from alternative type a to HOLType.

Instances

HOLTypeRep String a

HOLTypeRep HOLType a

HOLTypeRep PreType a

HOLTypeRep (PType thry) thry

class HOLTermRep a thry | a -> thry where

The HOLTermRep class provides a conversion from an alternative representation of terms to HOLTerm within the HOL monad.

The first parameter is the type of the alternative representation.

The second parameter is the tag for the last checkpoint of the current working theory. This enables us to have a conversion from representations that are theory dependent, i.e. PTerm, without running into type matchability issues.

Methods

toHTm :: a -> HOL cls thry HOLTerm

Conversion from alternative type a to HOLTerm.

Instances

HOLTermRep String a

HOLTermRep HOLTerm a

HOLTermRep PreTerm a

HOLTermRep (PTerm thry) thry