Lib.hs

{-# LANGUAGE FlexibleContexts, PatternSynonyms, TypeFamilies #-}
{-|
  Module:    HaskHOL.Core.Parser.Lib
  Copyright: (c) The University of Kansas 2013
  LICENSE:   BSD3

  Maintainer:  ecaustin@ittc.ku.edu
  Stability:   unstable
  Portability: unknown

  This module defines or re-exports common utility functions, type classes, 
  and auxilliary data types used in HaskHOL's parsers.  These primarily fall
  three classes of objects:

  * Types and functions used by the parsers.

  * Benign flag and state extensions used by the parsers.

  * Predicates and modifiers for state extensions used by the parsers.

  Note that, because these state extensions were designed to be used with the
  parser, the accessor and predicate functions are written to use 'getExtCtxt' 
  rather than 'getExt' for convenience.

  To see what is actually exported to the user, see the module 
  "HaskHOL.Core.Parser".
-}

module HaskHOL.Core.Parser.Lib
    ( -- * Parser Utilities and Types
      PreType(..)
    , PreTerm(..)
    , dpty
    , pretypeOfType
    , MyParser
    , ParseError -- | A re-export of 'ParseError'.
    , runParser -- |A re-export of 'runParser'.
    , langDef
    , lexer
    , mysymbol
    , myparens
    , mybraces
    , mybrackets
    , mycommaSep1
    , mysemiSep
    , mysemiSep1
    , myreserved
    , myidentifier
    , myinteger
    , myoperator
    , myreservedOp
    , choiceSym
    , choiceId
    , mywhiteSpace
    , mymany
    , mymany1
    , mysepBy1
    , mytry
      -- * Type Elaboration Flags
    , FlagIgnoreConstVarstruct(..)
    , FlagTyInvWarning(..)
    , FlagTyOpInvWarning(..)
    , FlagAddTyAppsAuto(..)
      -- * Pretty Printer Flags
    , FlagRevInterface(..)
    , FlagPrintAllThm(..)
      -- * Extensible Parser Operators
    , HOLContext(..)
    , prepHOLContext
    , getTypeArityCtxt
    , parseAsBinder
    , parseAsTyBinder
    , parseAsPrefix
    , parseAsInfix
    , unparseAsBinder
    , unparseAsTyBinder
    , unparseAsPrefix
    , unparseAsInfix
    , parsesAsBinder
    , parsesAsTyBinder
    , isPrefix
    , getInfixStatus
      -- * Overloading and Interface Mapping
    , makeOverloadable
    , removeInterface
    , reduceInterface
    , overrideInterface
    , overloadInterface
    , prioritizeOverload
    , getInterface
    , getOverloads
      -- * Type Abbreviations
    , newTypeAbbrev
    , removeTypeAbbrev
    , typeAbbrevs
      -- * Hidden Constant Mapping 
    , hideConstant
    , unhideConstant
    , getHidden
      -- * Extensible Printer Operators
    , addUnspacedBinop 
    , addPrebrokenBinop
    , removeUnspacedBinop
    , removePrebrokenBinop
    , getUnspacedBinops
    , getPrebrokenBinops
      -- * Parser state manipulations
    , getState
    , setState
    , updateState
    ) where

import HaskHOL.Core.Lib hiding ((<?>))
import HaskHOL.Core.Kernel
import HaskHOL.Core.State
import HaskHOL.Core.Basics
import HaskHOL.Core.Parser.Prims

import Text.Parsec hiding (runParser, setState, getState, updateState
                          ,ParseError, (<|>))
import qualified Text.Parsec as P
import Text.Parsec.Language
import Text.Parsec.Text
import Text.Parsec.Token

import Control.Monad.Identity

import {-# SOURCE #-} HaskHOL.Core.Parser.Rep

-- new flags and extensions
{-| 
  Flag to say whether to treat a constant varstruct, i.e.  @\\ const . bod@, as
  variable.
-}
newFlag "FlagIgnoreConstVarstruct" True

{-|
  Flag indicating that the user should be warned if a type variable was invented
  during parsing.
-}
newFlag "FlagTyInvWarning" False

{-|
  Flag indicating that the user should be warned if a type operator variable was
  invented during parsing.
-}
newFlag "FlagTyOpInvWarning" False

{-|
  Flag to say whether implicit type applications are to be added during parsing.
-}
newFlag "FlagAddTyAppsAuto" True

-- | Flag to indicate whether the interface should be reversed on printing.
newFlag "FlagRevInterface" True

{-| 
  Flag to indicate if the entirety of a theorem should be printed, as opposed
  to just the conclusion term.
-}
newFlag "FlagPrintAllThm" True

data BinderOps = BinderOps ![Text] deriving Typeable

deriveSafeCopy 0 'base ''BinderOps

initBinderOps :: [Text]
initBinderOps = ["\\"]

insertBinder :: Text -> Update BinderOps ()
insertBinder op =
    do (BinderOps ops) <- get
       put (BinderOps (op:ops))

removeBinder :: Text -> Update BinderOps ()
removeBinder op =
    do (BinderOps ops) <- get
       put (BinderOps (op `delete` ops))

getBinders :: Query BinderOps [Text]
getBinders =
    do (BinderOps ops) <- ask
       return ops

makeAcidic ''BinderOps ['insertBinder, 'removeBinder, 'getBinders]


data TyBinderOps = TyBinderOps ![Text] deriving Typeable

deriveSafeCopy 0 'base ''TyBinderOps

initTyBinderOps :: [Text]
initTyBinderOps = ["\\\\"]

insertTyBinder :: Text -> Update TyBinderOps ()
insertTyBinder op =
    do (TyBinderOps ops) <- get
       put (TyBinderOps (op:ops))

removeTyBinder :: Text -> Update TyBinderOps ()
removeTyBinder op =
    do (TyBinderOps ops) <- get
       put (TyBinderOps (op `delete` ops))

getTyBinders :: Query TyBinderOps [Text]
getTyBinders =
    do (TyBinderOps ops) <- ask
       return ops

makeAcidic ''TyBinderOps ['insertTyBinder, 'removeTyBinder, 'getTyBinders]

data PrefixOps = PrefixOps ![Text] deriving Typeable

deriveSafeCopy 0 'base ''PrefixOps

insertPrefix :: Text -> Update PrefixOps ()
insertPrefix op =
    do (PrefixOps ops) <- get
       put (PrefixOps (op:ops))

removePrefix :: Text -> Update PrefixOps ()
removePrefix op =
    do (PrefixOps ops) <- get
       put (PrefixOps (op `delete` ops))

getPrefixes :: Query PrefixOps [Text]
getPrefixes =
    do (PrefixOps ops) <- ask
       return ops

makeAcidic ''PrefixOps ['insertPrefix, 'removePrefix, 'getPrefixes]

data InfixOps = InfixOps ![(Text, (Int, Text))] deriving Typeable

deriveSafeCopy 0 'base ''InfixOps

initInfixOps :: [(Text, (Int, Text))]
initInfixOps = [("=", (12, "right"))]

insertInfix :: (Text, (Int, Text)) -> Update InfixOps ()
insertInfix i@(n, _) =
    do (InfixOps is) <- get 
       let is' = case find (\ (n', _) -> n == n') is of
                   Just _ -> is
                   _ -> 
                       sort (\ (s, (x, a)) (t, (y, b)) ->
                         x < y || x == y && a > b || x == y && a == b && s < t)
                         (i:is)
       put (InfixOps is')

removeInfix :: Text -> Update InfixOps ()
removeInfix op =
    do (InfixOps ops) <- get
       put (InfixOps (filter (\ (x, _) -> x /= op) ops))

getInfixes :: Query InfixOps [(Text, (Int, Text))]
getInfixes =
    do (InfixOps ops) <- ask
       return ops

makeAcidic ''InfixOps ['insertInfix, 'removeInfix, 'getInfixes]


data Interface = Interface ![(Text, (Text, HOLType))] deriving Typeable

deriveSafeCopy 0 'base ''Interface

insertInterface :: (Text, (Text, HOLType)) -> Update Interface ()
insertInterface x =
    do (Interface xs) <- get
       put (Interface (x:xs))

deleteInterface :: (Text, (Text, HOLType)) -> Update Interface ()
deleteInterface x =
    do (Interface xs) <- get
       put (Interface (x `delete` xs))

filterInterface :: Text -> Update Interface ()
filterInterface s =
    do (Interface xs) <- get
       put (Interface (filter (\ (x, _) -> x /= s) xs))

getInterfaces :: Query Interface [(Text, (Text, HOLType))]
getInterfaces =
    do (Interface xs) <- ask
       return xs

makeAcidic ''Interface 
    ['insertInterface, 'deleteInterface, 'filterInterface, 'getInterfaces]


data Overload = Overload !(Map Text HOLType) deriving Typeable

deriveSafeCopy 0 'base ''Overload

insertOverload :: Text -> HOLType -> Update Overload ()
insertOverload s ty =
    do (Overload xs) <- get
       put (Overload (mapInsert s ty xs))

getOverload :: Query Overload (Map Text HOLType)
getOverload =
    do (Overload xs) <- ask
       return xs

makeAcidic ''Overload ['insertOverload, 'getOverload]


data TypeAbbreviations = TypeAbbreviations !(Map Text HOLType) 
    deriving Typeable

deriveSafeCopy 0 'base ''TypeAbbreviations

insertTypeAbbreviation :: Text -> HOLType -> Update TypeAbbreviations ()
insertTypeAbbreviation x ty =
    do (TypeAbbreviations xs) <- get
       put (TypeAbbreviations (mapInsert x ty xs))

removeTypeAbbreviation :: Text -> Update TypeAbbreviations ()
removeTypeAbbreviation x =
    do (TypeAbbreviations xs) <- get
       put (TypeAbbreviations (x `mapDelete` xs))

getTypeAbbreviations :: Query TypeAbbreviations (Map Text HOLType)
getTypeAbbreviations =
    do (TypeAbbreviations xs) <- ask
       return xs

makeAcidic ''TypeAbbreviations 
    ['insertTypeAbbreviation, 'removeTypeAbbreviation, 'getTypeAbbreviations]


data Hidden = Hidden [Text] deriving Typeable

deriveSafeCopy 0 'base ''Hidden

insertHidden :: Text -> Update Hidden ()
insertHidden x =
    do (Hidden xs) <- get
       put (Hidden (x `insert` xs))

removeHidden :: Text -> Update Hidden ()
removeHidden x =
    do (Hidden xs) <- get
       put (Hidden (x `delete` xs))

getHiddens :: Query Hidden [Text]
getHiddens =
    do (Hidden xs) <- ask
       return xs

makeAcidic ''Hidden ['insertHidden, 'removeHidden, 'getHiddens]


data UnspacedBinops = UnspacedBinops ![Text] deriving Typeable

deriveSafeCopy 0 'base ''UnspacedBinops

initUnspaced :: [Text]
initUnspaced = [",", "..", "$"]

insertUnspaced :: Text -> Update UnspacedBinops ()
insertUnspaced op =
    do (UnspacedBinops ops) <- get
       put (UnspacedBinops (op:ops))

removeUnspaced :: Text -> Update UnspacedBinops ()
removeUnspaced op =
    do (UnspacedBinops ops) <- get
       put (UnspacedBinops (ops \\ [op]))

getUnspaced :: Query UnspacedBinops [Text]
getUnspaced =
    do (UnspacedBinops ops) <- ask
       return ops

makeAcidic ''UnspacedBinops ['insertUnspaced, 'removeUnspaced, 'getUnspaced]


data PrebrokenBinops = PrebrokenBinops ![Text] deriving Typeable

deriveSafeCopy 0 'base ''PrebrokenBinops

initPrebroken :: [Text]
initPrebroken = ["==>"]

insertPrebroken :: Text -> Update PrebrokenBinops ()
insertPrebroken op =
    do (PrebrokenBinops ops) <- get
       put (PrebrokenBinops (op:ops))

removePrebroken :: Text -> Update PrebrokenBinops ()
removePrebroken op =
    do (PrebrokenBinops ops) <- get
       put (PrebrokenBinops (ops \\ [op]))

getPrebroken :: Query PrebrokenBinops [Text]
getPrebroken =
    do (PrebrokenBinops ops) <- ask
       return ops

makeAcidic ''PrebrokenBinops ['insertPrebroken, 'removePrebroken, 'getPrebroken]

-- | The default 'PreType' to be used as a blank for the type inference engine.
dpty :: PreType
dpty = PTyComb (PTyCon textEmpty) []

-- | Converts a 'HOLType' to 'PreType'
pretypeOfType :: HOLType -> PreType
pretypeOfType (TyVar f v) = UTyVar f v 0
pretypeOfType (TyApp tyop args) =
    let (s, n) = destTypeOp tyop
        tyop' = if n == -1 then UTyVar False s (length args) else PTyCon s in
      PTyComb tyop' $ map pretypeOfType args
pretypeOfType (UType tv tb) = 
    PUTy (pretypeOfType tv) $ pretypeOfType tb
pretypeOfType _ = error "pretypeOfType: exhaustive warning."

{-| 
  An alias to a stateful 'GenParser' that carries a 'HOLContext', a list of
  known type operator variables with their arity, and a counter  The list of
  operators is used to guarantee that all instances of a type operator variable
  in a term have the same arity.  The counter is used to generate fresh names
  in a term.
-}
type MyParser thry = GenParser (HOLContext thry, [(Text, Int)], Int)

-- | The Parsec 'LanguageDef' for HaskHOL.
langDef :: GenLanguageDef Text st Identity
langDef = LanguageDef
    { commentStart = ""
    , commentEnd = ""
    , commentLine = ""
    , nestedComments = True
    , identStart = alphaNum <|> char '_'
    , identLetter = alphaNum <|> oneOf "_'"
    , opStart = oneOf ",:!#$%&*+./<=>?@\\^|-~"
    , opLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
    , reservedNames = [ "TYINST", "let", "and", "in", "if", "then", "else"
                      , "match", "when", "function" ]
    , reservedOpNames = ["(", ")", "[", "]", "{", "}"
                        , "%", "_", "'", "->", ".", ":", ";", "|"]
    , caseSensitive = True
    }

-- | The Parsec token parser for HaskHOL.
lexer :: GenTokenParser Text (HOLContext thry, [(Text, Int)], Int) Identity
lexer = makeTokenParser langDef

-- | A version of 'symbol' for our language.
mysymbol :: String -> MyParser thry Text
mysymbol = liftM pack . symbol lexer

-- | A version of 'parens' for our language.
myparens :: MyParser thry a -> MyParser thry a
myparens = parens lexer

-- | A version of 'braces' for our language.
mybraces :: MyParser thry a -> MyParser thry a
mybraces = braces lexer

-- | A version of 'brackets' for our language.
mybrackets :: MyParser thry a -> MyParser thry a
mybrackets = brackets lexer

-- | A version of 'commaSep1' for our language.
mycommaSep1 :: MyParser thry a -> MyParser thry [a]
mycommaSep1 = commaSep1 lexer

-- | A version of 'semiSep' for our language.
mysemiSep :: MyParser thry a -> MyParser thry [a]
mysemiSep = semiSep lexer

-- | A version of 'semiSep1' for our language.
mysemiSep1 :: MyParser thry a -> MyParser thry [a]
mysemiSep1 = semiSep1 lexer

-- | A version of 'reserved' for our language.
myreserved :: String -> MyParser thry ()
myreserved = reserved lexer

-- | A version of 'identifier' for our language.
myidentifier :: MyParser thry Text
myidentifier = liftM pack $ identifier lexer

-- | A version of 'integer' for our language.
myinteger :: MyParser thry Integer
myinteger = integer lexer

-- | A version of 'operator' for our language.
myoperator :: MyParser thry Text
myoperator = liftM pack $ operator lexer

-- | A version of 'reservedOp' for our language.
myreservedOp :: String -> MyParser thry ()
myreservedOp = reservedOp lexer

-- | Selects the first matching symbol.
choiceSym :: [String] -> MyParser thry Text
choiceSym ops = choice $ map mysymbol ops

-- | Selects the first matching reserved operator.
choiceId :: [Text] -> MyParser thry Text
choiceId ops = choice $ map 
               (\ s -> try $ do s' <- myidentifier <|> myoperator
                                if s' == s
                                   then return s
                                   else fail "choiceId") ops

-- | A version of 'whiteSpace' for our language.
mywhiteSpace :: MyParser thry ()
mywhiteSpace = whiteSpace lexer

-- | A re-export of 'P.many'.
mymany :: MyParser thry a -> MyParser thry [a]
mymany = P.many

-- | A re-export of 'P.many1'.
mymany1 :: MyParser thry a -> MyParser thry [a]
mymany1 = P.many1

-- | A re-export of 'P.sepBy1'.
mysepBy1 :: MyParser thry a -> MyParser thry b -> MyParser thry [a]
mysepBy1 = P.sepBy1

-- | A re-export of 'P.try'.
mytry :: MyParser thry a -> MyParser thry a
mytry = P.try

-- State Extensions
prepHOLContext :: HOL cls thry (HOLContext thry)
prepHOLContext =
    do acid1 <- openLocalStateHOL (InfixOps initInfixOps)
       is <- queryHOL acid1 GetInfixes
       closeAcidStateHOL acid1
       acid2 <- openLocalStateHOL (PrefixOps [])
       ps <- queryHOL acid2 GetPrefixes
       closeAcidStateHOL acid2
       acid3 <- openLocalStateHOL (BinderOps initBinderOps)
       bs <- queryHOL acid3 GetBinders
       closeAcidStateHOL acid3
       acid4 <- openLocalStateHOL (TyBinderOps initTyBinderOps)
       tbs <- queryHOL acid4 GetTyBinders
       closeAcidStateHOL acid4
       ts <- types
       tas <- typeAbbrevs
       iface <- getInterface
       cond1 <- getBenignFlag FlagPrintAllThm
       cond2 <- getBenignFlag FlagRevInterface
       us <- getUnspacedBinops
       pbs <- getPrebrokenBinops
       return $! HOLContext is ps bs tbs ts tas iface cond1 cond2 us pbs


-- Operators
-- A version of 'getTypeArity' for parser contexts.
getTypeArityCtxt :: HOLContext thry -> Text -> Maybe Int
getTypeArityCtxt ctxt name =
    liftM (snd . destTypeOp) . mapLookup name $ typesCtxt ctxt

-- | Specifies a 'Text' to be recognized as a term binder by the parser.
parseAsBinder :: Text -> HOL Theory thry ()
parseAsBinder op =
    do acid <- openLocalStateHOL (BinderOps initBinderOps)
       updateHOL acid (InsertBinder op)
       createCheckpointAndCloseHOL acid

-- | Specifies a 'Text' to be recognized as a type binder by the parser.
parseAsTyBinder :: Text -> HOL Theory thry ()
parseAsTyBinder op =
    do acid <- openLocalStateHOL (TyBinderOps initTyBinderOps)
       updateHOL acid (InsertTyBinder op)
       createCheckpointAndCloseHOL acid

-- | Specifies a 'Text' to be recognized as a prefix operator by the parser.
parseAsPrefix :: Text -> HOL Theory thry ()
parseAsPrefix op =
    do acid <- openLocalStateHOL (PrefixOps [])
       updateHOL acid (InsertPrefix op)
       createCheckpointAndCloseHOL acid

{-| 
  Specifies a 'Text' to be recognized as an infix operator by the parser with
  a given precedence level and associativity.
-}
parseAsInfix :: (Text, (Int, Text)) -> HOL Theory thry ()
parseAsInfix op =
    do acid <- openLocalStateHOL (InfixOps initInfixOps)
       updateHOL acid (InsertInfix op)
       createCheckpointAndCloseHOL acid

-- | Specifies a 'Text' for the parser to stop recognizing as a term binder.
unparseAsBinder :: Text -> HOL Theory thry ()
unparseAsBinder op =
    do acid <- openLocalStateHOL (BinderOps initBinderOps)
       updateHOL acid (RemoveBinder op)
       createCheckpointAndCloseHOL acid

-- | Specifies a 'Text' for the parser to stop recognizing as a type binder.
unparseAsTyBinder :: Text -> HOL Theory thry ()
unparseAsTyBinder op =
    do acid <- openLocalStateHOL (TyBinderOps initTyBinderOps)
       updateHOL acid (RemoveTyBinder op)
       createCheckpointAndCloseHOL acid

{-| 
  Specifies a 'Text' for the parser to stop recognizing as a prefix operator.
-}
unparseAsPrefix :: Text -> HOL Theory thry ()
unparseAsPrefix op =
    do acid <- openLocalStateHOL (PrefixOps [])
       updateHOL acid (RemovePrefix op)
       createCheckpointAndCloseHOL acid

{-| 
  Specifies a 'Text' for the parser to stop recognizing as an infix operator.
-}
unparseAsInfix :: Text -> HOL Theory thry ()
unparseAsInfix op =
    do acid <- openLocalStateHOL (InfixOps initInfixOps)
       updateHOL acid (RemoveInfix op)
       createCheckpointAndCloseHOL acid

-- | Predicate for 'Text's recognized as term binders by the parser.
parsesAsBinder :: Text -> HOLContext thry -> Bool
parsesAsBinder op = elem op . binders

-- | Predicate for 'Text's recognized as term binders by the parser.
parsesAsTyBinder :: Text -> HOLContext thry -> Bool
parsesAsTyBinder op = elem op . tyBinders

-- | Predicate for 'Text's recognized as prefix operators by the parser.
isPrefix :: Text -> HOLContext thry -> Bool
isPrefix op = elem op . prefixes

{-| 
  Predicate for 'Text's recognized as infix operators by the parser.  Returns
  a precidence and associativity pair guarded by 'Maybe'.
-}
getInfixStatus :: Text -> HOLContext thry -> Maybe (Int, Text)
getInfixStatus op = lookup op . infixes

-- Interface
{-|
  Specifies a 'Text' 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.
-}
makeOverloadable :: Text -> HOLType -> HOL Theory thry ()
makeOverloadable s gty =
    do overs <- getOverloads
       case mapLookup s overs of
         Just ty
             | gty == ty -> return ()
             | otherwise -> 
                 fail "makeOverloadable: differs from existing skeleton"
         _ -> do acid1 <- openLocalStateHOL (Overload mapEmpty)
                 updateHOL acid1 (InsertOverload s gty)
                 createCheckpointAndCloseHOL acid1
                 acid2 <- openLocalStateHOL (Interface [])
                 updateHOL acid2 (FilterInterface s)
                 createCheckpointAndCloseHOL acid2

-- | Removes all instances of an overloaded symbol from the interface.
removeInterface :: Text -> HOL Theory thry ()
removeInterface sym =
    do acid <- openLocalStateHOL (Interface [])
       updateHOL acid (FilterInterface sym)
       createCheckpointAndCloseHOL acid

{-| 
  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.
-}
reduceInterface :: Text -> HOLTerm -> HOL Theory thry ()
reduceInterface sym tm =
    do namty <- liftMaybe "reduceInterface: term not a constant or variable" $ 
                  destConst tm <|> destVar tm
       acid <- openLocalStateHOL (Interface [])
       updateHOL acid (DeleteInterface (sym, namty))
       createCheckpointAndCloseHOL acid

{-|
  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.
-}
overrideInterface :: Text -> HOLTerm -> HOL Theory thry ()
overrideInterface sym tm =
    do namty <- liftMaybe "overrideInterface: term not a constant or variable" $
                  destConst tm <|> destVar tm
       let m = do acid <- openLocalStateHOL (Interface [])
                  updateHOL acid (FilterInterface sym)
                  updateHOL acid (InsertInterface (sym, namty))
                  createCheckpointAndCloseHOL acid
       overs <- getOverloads
       case sym `mapLookup` overs of
         Just gty -> if isNothing $ typeMatch gty (snd namty) ([], [], [])
                     then fail $ "overrideInterface: " ++
                                 "not an instance of type skeleton"
                     else m
         _ -> m

{-|
  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'.
-}
overloadInterface :: Text -> HOLTerm -> HOL Theory thry ()
overloadInterface sym tm =
    do overs <- getOverloads
       gty <- liftMaybe ("overloadInstace: symbol " ++ show sym ++ 
                         " is not overloadable.") $ mapLookup sym overs
       namty <- liftMaybe "overloadInstance: term not a constant or variable" $ 
                  destConst tm <|> destVar tm
       if isNothing $ typeMatch gty (snd namty) ([], [], [])
          then fail "overloadInstance: not an instance of type skeleton"
          else do acid <- openLocalStateHOL (Interface [])
                  let i = (sym, namty)
                  updateHOL acid (DeleteInterface i)
                  updateHOL acid (InsertInterface i)
                  createCheckpointAndCloseHOL acid

{-|
  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'.
-}
prioritizeOverload :: HOLType -> HOL Theory thry ()
prioritizeOverload ty =
    do overs <- getOverloads
       mapM_ (\ (s, gty) -> 
              (do iface <- getInterface
                  let (n, t') = fromJust $ 
                                tryFind (\ (s', x@(_, t)) ->
                                         if s' /= s then Nothing
                                         else do (ts, _, _) <- typeMatch gty t
                                                                 ([], [], [])
                                                 _ <- ty `revLookup` ts
                                                 return x) iface
                  overloadInterface s $ mkVar n t')
              <|> return ()) $ mapToList overs

-- | Returns the list of all currently defined interface overloads.
getInterface :: HOL cls thry [(Text, (Text, HOLType))]
getInterface =
    do acid <- openLocalStateHOL (Interface [])
       iface <- queryHOL acid GetInterfaces
       closeAcidStateHOL acid
       return iface

{-| 
  Returns the list of all overloadable symbols paired with their most generic 
  types.
-}
getOverloads :: HOL cls thry (Map Text HOLType)
getOverloads =
    do acid <- openLocalStateHOL (Overload mapEmpty)
       ovrlds <- queryHOL acid GetOverload
       closeAcidStateHOL acid
       return ovrlds

-- Type Abbreviations
{-| 
  Specifies a 'Text' 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.
-}
newTypeAbbrev :: HOLTypeRep ty Theory thry => Text -> ty -> HOL Theory thry ()
newTypeAbbrev s pty =
    do ty <- toHTy pty
       acid <- openLocalStateHOL (TypeAbbreviations mapEmpty)
       updateHOL acid (InsertTypeAbbreviation s ty)
       createCheckpointAndCloseHOL acid

{-| 
  Specifies a 'Text' for the parser to stop recognizing as a type 
  abbreviation.
-}
removeTypeAbbrev :: Text -> HOL Theory thry ()
removeTypeAbbrev s =
    do acid <- openLocalStateHOL (TypeAbbreviations mapEmpty)
       updateHOL acid (RemoveTypeAbbreviation s)
       createCheckpointAndCloseHOL acid

{-| 
  Returns all 'Text's currently acting as type abbreviations in the parser
  paired with their associated types.
-}
typeAbbrevs :: HOL cls thry (Map Text HOLType)
typeAbbrevs =
    do acid <- openLocalStateHOL (TypeAbbreviations mapEmpty)
       abvs <- queryHOL acid GetTypeAbbreviations
       closeAcidStateHOL acid
       return abvs

-- Hidden Constant Mapping
-- | Specifies a 'Text' for the parser to stop recognizing as a constant.
hideConstant :: Text -> HOL Theory thry ()
hideConstant c =
    do acid <- openLocalStateHOL (Hidden [])
       updateHOL acid (InsertHidden c)
       createCheckpointAndCloseHOL acid

-- | Specifies a 'Text' for the parser to resume recognizing as a constant.
unhideConstant :: Text -> HOL Theory thry ()
unhideConstant c =
    do acid <- openLocalStateHOL (Hidden [])
       updateHOL acid (RemoveHidden c)
       createCheckpointAndCloseHOL acid

-- | Returns all 'Text's currently acting as constants hidden from the parser.
getHidden :: HOL cls thry [Text]
getHidden =
    do acid <- openLocalStateHOL (Hidden [])
       hids <- queryHOL acid GetHiddens
       closeAcidStateHOL acid
       return hids

{-| 
  Specifies a symbol to be recognized as an unspaced, binary operator by the
  printer.  Applications involving these operators will be built with the '<>'
  combinator as opposed to '<+>'.

  Note that technically this method should be considered benign, however, for
  simplicity of implementation it is defined using 'modifyExt' and thus must be
  tagged a 'Theory' computation.
-}
addUnspacedBinop :: Text -> HOL Theory thry ()
addUnspacedBinop op =
    do acid <- openLocalStateHOL (UnspacedBinops initUnspaced)
       updateHOL acid (InsertUnspaced op)
       createCheckpointAndCloseHOL acid

{-| 
  Specifies a symbol to be recognized as a prebroken, binary operator by the
  printer.  Applications involving these operators will have their right-hand
  side argument printed on the next line using the 'hang' combinator.

  Note that technically this method should be considered benign, however, for
  simplicity of implementation it is defined using 'modifyExt' and thus must be
  tagged a 'Theory' computation.
-}
addPrebrokenBinop :: Text -> HOL Theory thry ()
addPrebrokenBinop op =
    do acid <- openLocalStateHOL (PrebrokenBinops initPrebroken)
       updateHOL acid (InsertPrebroken op)
       createCheckpointAndCloseHOL acid

{-| 
  Specifies a symbol to stop being recognized as an unspaced, binary operator 
  by the printer.

  Note that technically this method should be considered benign, however, for
  simplicity of implementation it is defined using 'modifyExt' and thus must be
  tagged a 'Theory' computation.
-}
removeUnspacedBinop :: Text -> HOL Theory thry ()
removeUnspacedBinop op =
    do acid <- openLocalStateHOL (UnspacedBinops initUnspaced)
       updateHOL acid (RemoveUnspaced op)
       createCheckpointAndCloseHOL acid

{-| 
  Specifies a symbol to stop being recognized as an prebroken, binary operator 
  by the printer.

  Note that technically this method should be considered benign, however, for
  simplicity of implementation it is defined using 'modifyExt' and thus must be
  tagged a 'Theory' computation.
-}
removePrebrokenBinop :: Text -> HOL Theory thry ()
removePrebrokenBinop op =
    do acid <- openLocalStateHOL (PrebrokenBinops initPrebroken)
       updateHOL acid (RemovePrebroken op)
       createCheckpointAndCloseHOL acid

{-| 
  Returns the list of all symbols current recognized as unspaced, binary
  operators by the printer.
-}
getUnspacedBinops :: HOL cls thry [Text]
getUnspacedBinops =
    do acid <- openLocalStateHOL (UnspacedBinops initUnspaced)
       ops <- queryHOL acid GetUnspaced
       closeAcidStateHOL acid
       return ops

{-| 
  Returns the list of all symbols current recognized as prebroken, binary
  operators by the printer.
-}
getPrebrokenBinops :: HOL cls thry [Text]
getPrebrokenBinops =
    do acid <- openLocalStateHOL (PrebrokenBinops initUnspaced)
       ops <- queryHOL acid GetPrebroken
       closeAcidStateHOL acid
       return ops

-- Re-exports
-- | A re-export of 'P.runParser'.
runParser :: GenParser st a -> st -> P.SourceName -> Text 
          -> Either ParseError a
runParser = P.runParser

-- | A re-export of 'P.getState'.
getState :: Monad m => P.ParsecT s u m u
getState = P.getState

-- | A re-export of 'P.setState'.
setState :: Monad m => u -> P.ParsecT s u m ()
setState = P.setState

-- | A re-export of 'P.updateState'.
updateState :: Monad m => (u -> u) -> P.ParsecT s u m ()
updateState = P.updateState