module HaskHOL.Core.Parser.Lib
(
PreType(..)
, PreTerm(..)
, dpty
, pretypeOfType
, MyParser
, myparens
, mybraces
, mybrackets
, mycommaSep1
, mysemiSep
, myreserved
, myidentifier
, myinteger
, myoperator
, myreservedOp
, choiceOp
, mywhiteSpace
, FlagIgnoreConstVarstruct(..)
, FlagTyInvWarning(..)
, FlagTyOpInvWarning(..)
, FlagAddTyAppsAuto(..)
, parseAsBinder
, parseAsTyBinder
, parseAsPrefix
, parseAsInfix
, unparseAsBinder
, unparseAsTyBinder
, unparseAsPrefix
, unparseAsInfix
, binders
, tyBinders
, prefixes
, infixes
, parsesAsBinder
, parsesAsTyBinder
, isPrefix
, getInfixStatus
, makeOverloadable
, removeInterface
, reduceInterface
, overrideInterface
, overloadInterface
, prioritizeOverload
, getInterface
, getOverloads
, newTypeAbbrev
, removeTypeAbbrev
, typeAbbrevs
, hideConstant
, unhideConstant
, getHidden
, module Text.ParserCombinators.Parsec
) where
import HaskHOL.Core.Lib
import HaskHOL.Core.Kernel
import HaskHOL.Core.State
import HaskHOL.Core.Basics
import Text.ParserCombinators.Parsec hiding ((<|>))
import Text.ParserCombinators.Parsec.Token
import Text.ParserCombinators.Parsec.Language (emptyDef)
newFlag "FlagIgnoreConstVarstruct" True
newFlag "FlagTyInvWarning" True
newFlag "FlagTyOpInvWarning" True
newFlag "FlagAddTyAppsAuto" True
newExtension "BinderOps" [| ["\\"] :: [String] |]
newExtension "TyBinderOps" [| ["\\\\"] :: [String] |]
newExtension "PrefixOps" [| [] :: [String] |]
newExtension "InfixOps"
[| [("=", (12, AssocRight))] :: [(String, (Int, Assoc))] |]
newExtension "Interface" [| [] :: [(String, (String, HOLType))] |]
newExtension "Overload" [| [] :: [(String, HOLType)] |]
newExtension "TypeAbbreviations" [| [] :: [(String, HOLType)] |]
newExtension "Hidden" [| [] :: [String] |]
data PreType
= PTyCon String
| UTyVar Bool String Int
| STyVar Int
| PTyComb PreType [PreType]
| PUTy PreType PreType
deriving (Eq, Show)
data PreTerm
= PVar String PreType
| PConst String PreType
| PComb PreTerm PreTerm
| PAbs PreTerm PreTerm
| PAs PreTerm PreType
| PInst [(PreType, String)] PreTerm
| PApp PreType
| TyPAbs PreType PreTerm
| TyPComb PreTerm PreType PreType
deriving Show
dpty :: PreType
dpty = PTyComb (PTyCon "") []
pretypeOfType :: HOLType -> PreType
pretypeOfType (view -> TyVar f v) = UTyVar f v 0
pretypeOfType (view -> 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 (view -> UType tv tb) =
PUTy (pretypeOfType tv) $ pretypeOfType tb
pretypeOfType _ = error "pretypeOfType: incomplete view pattern"
type MyParser thry a = CharParser (HOLContext thry, [(String, Int)]) a
lexer :: TokenParser (HOLContext thry, [(String, Int)])
lexer = makeTokenParser
(emptyDef
{ reservedNames = ["TYINST", "let", "and", "in", "if", "then", "else"]
, reservedOpNames = ["%", "_", "'", "->", "+", "#", "^", ":", ";"]
})
myparens :: MyParser thry a -> MyParser thry a
myparens = parens lexer
mybraces :: MyParser thry a -> MyParser thry a
mybraces = braces lexer
mybrackets :: MyParser thry a -> MyParser thry a
mybrackets = brackets lexer
mycommaSep1 :: MyParser thry a -> MyParser thry [a]
mycommaSep1 = commaSep1 lexer
mysemiSep :: MyParser thry a -> MyParser thry [a]
mysemiSep = semiSep lexer
myreserved :: String -> MyParser thry ()
myreserved = reserved lexer
myidentifier :: MyParser thry String
myidentifier = identifier lexer
myinteger :: MyParser thry Integer
myinteger = integer lexer
myoperator :: MyParser thry String
myoperator = operator lexer
myreservedOp :: String -> MyParser thry ()
myreservedOp = reservedOp lexer
choiceOp :: [String] -> MyParser thry String
choiceOp ops =
choice $ map (\ name -> do myreservedOp name
return name) ops
mywhiteSpace :: MyParser thry ()
mywhiteSpace = whiteSpace lexer
parseAsBinder :: String -> HOL Theory thry ()
parseAsBinder op =
modifyExt (\ (BinderOps ops) -> BinderOps $ op `insert` ops)
parseAsTyBinder :: String -> HOL Theory thry ()
parseAsTyBinder op =
modifyExt (\ (TyBinderOps ops) -> TyBinderOps $ op `insert` ops)
parseAsPrefix :: String -> HOL Theory thry ()
parseAsPrefix op =
modifyExt (\ (PrefixOps ops) -> PrefixOps $ op `insert` ops)
parseAsInfix :: (String, (Int, Assoc)) -> HOL Theory thry ()
parseAsInfix op =
modifyExt (\ (InfixOps ops) -> InfixOps $ op `insertInfix` ops)
where insertInfix :: (String, (Int, Assoc)) -> [(String, (Int, Assoc))] ->
[(String, (Int, Assoc))]
insertInfix i@(n, _) is =
case find (\ (n', _) -> n == n') is of
Just _ -> is
_ -> sortBy (\ (_, (x, _)) (_, (y, _)) -> y `compare` x) $ i:is
unparseAsBinder :: String -> HOL Theory thry ()
unparseAsBinder op =
modifyExt (\ (BinderOps ops) -> BinderOps $ op `delete` ops)
unparseAsTyBinder :: String -> HOL Theory thry ()
unparseAsTyBinder op =
modifyExt (\ (TyBinderOps ops) -> TyBinderOps $ op `delete` ops)
unparseAsPrefix :: String -> HOL Theory thry ()
unparseAsPrefix op =
modifyExt (\ (PrefixOps ops) -> PrefixOps $ op `delete` ops)
unparseAsInfix :: String -> HOL Theory thry ()
unparseAsInfix op =
modifyExt (\ (InfixOps ops) ->
InfixOps $ filter (\ (x, _) -> x == op) ops)
binders :: HOLContext thry -> [String]
binders ctxt =
let (BinderOps ops) = getExtCtxt ctxt in
ops
tyBinders :: HOLContext thry -> [String]
tyBinders ctxt =
let (TyBinderOps ops) = getExtCtxt ctxt in
ops
prefixes :: HOLContext thry -> [String]
prefixes ctxt =
let (PrefixOps ops) = getExtCtxt ctxt in
ops
infixes :: HOLContext thry -> [(String, (Int, Assoc))]
infixes ctxt =
let (InfixOps ops) = getExtCtxt ctxt in
ops
parsesAsBinder :: String -> HOLContext thry -> Bool
parsesAsBinder op = elem op . binders
parsesAsTyBinder :: String -> HOLContext thry -> Bool
parsesAsTyBinder op = elem op . tyBinders
isPrefix :: String -> HOLContext thry -> Bool
isPrefix op = elem op . prefixes
getInfixStatus :: String -> HOLContext thry -> Maybe (Int, Assoc)
getInfixStatus op = lookup op . infixes
makeOverloadable :: String -> HOLType -> HOL Theory thry ()
makeOverloadable s gty =
do (Overload overs) <- getExt
case lookup s overs of
Just ty
| gty == ty -> return ()
| otherwise ->
fail "makeOverloadable: differs from existing skeleton"
_ -> do putExt $ Overload ((s, gty):overs)
modifyExt (\ (Interface iface) ->
Interface $ filter (\ (x, _) -> x /= s) iface)
removeInterface :: String -> HOL Theory thry ()
removeInterface sym =
modifyExt (\ (Interface iface) -> Interface $
filter (\ (x, _) -> x /= sym) iface)
reduceInterface :: String -> HOLTerm -> HOL Theory thry ()
reduceInterface sym tm =
do namty <- liftMaybe "reduceInterface: term not a constant or variable" $
destConst tm <|> destVar tm
modifyExt (\ (Interface iface) -> Interface $
(sym, namty) `delete` iface)
overrideInterface :: String -> HOLTerm -> HOL Theory thry ()
overrideInterface sym tm =
do namty <- liftMaybe "overrideInterface: term not a constant or variable" $
destConst tm <|> destVar tm
let m = modifyExt (\ (Interface iface) ->
let iface' = filter (\ (x, _) -> x /= sym) iface in
Interface $ (sym, namty) : iface')
(Overload overs) <- getExt
case sym `lookup` overs of
Just gty -> if isNothing $ typeMatch gty (snd namty) ([], [], [])
then fail $ "overrideInterface: " ++
"not an instance of type skeleton"
else m
_ -> m
overloadInterface :: String -> HOLTerm -> HOL Theory thry ()
overloadInterface sym tm =
do (Overload overs) <- getExt
gty <- liftMaybe ("overloadInstace: symbol " ++ sym ++
" is not overloadable.") $ lookup 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 modifyExt (\ (Interface iface) ->
let iface' = (sym, namty) `delete` iface in
Interface $ (sym, namty) : iface')
prioritizeOverload :: HOLType -> HOL Theory thry ()
prioritizeOverload ty =
do (Overload overs) <- getExt
mapM_ (\ (s, gty) ->
(do (Interface iface) <- getExt
let (n, t') = fromJust $
tryFind (\ (s', x@(_, t)) ->
if s' /= s then Nothing
else do (tys, _, _) <- typeMatch gty t
([], [], [])
_ <- ty `revLookup` tys
return x) iface
overloadInterface s $ mkVar n t')
<|> return ()) overs
getInterface :: HOLContext thry -> [(String, (String, HOLType))]
getInterface ctxt =
let (Interface iface) = getExtCtxt ctxt in iface
getOverloads :: HOLContext thry -> [(String, HOLType)]
getOverloads ctxt =
let (Overload overs) = getExtCtxt ctxt in overs
newTypeAbbrev :: String -> HOLType -> HOL Theory thry ()
newTypeAbbrev s ty =
modifyExt (\ (TypeAbbreviations abvs) ->
TypeAbbreviations $ insertMap s ty abvs)
removeTypeAbbrev :: String -> HOL Theory thry ()
removeTypeAbbrev s =
modifyExt (\ (TypeAbbreviations abvs) ->
TypeAbbreviations $ filter (\ (s', _) -> s' /= s) abvs)
typeAbbrevs :: HOLContext thry -> [(String, HOLType)]
typeAbbrevs ctxt =
let (TypeAbbreviations abvs) = getExtCtxt ctxt in abvs
hideConstant :: String -> HOL Theory thry ()
hideConstant c = modifyExt (\ (Hidden hcs) -> Hidden $ c `insert` hcs)
unhideConstant :: String -> HOL Theory thry ()
unhideConstant c = modifyExt (\ (Hidden hcs) -> Hidden $ c `delete` hcs)
getHidden :: HOLContext thry -> [String]
getHidden ctxt =
let (Hidden hidden) = getExtCtxt ctxt in hidden
deriveLiftMany [ ''BinderOps, ''TyBinderOps
, ''PrefixOps, ''InfixOps
, ''Interface, ''Overload
, ''TypeAbbreviations, ''Hidden ]