haskhol-core-1.0.0: src/HaskHOL/Core/Parser/TermParser.hs
{-|
Module: HaskHOL.Core.Parser.TermParser
Copyright: (c) The University of Kansas 2013
LICENSE: BSD3
Maintainer: ecaustin@ittc.ku.edu
Stability: unstable
Portability: unknown
This module defines the parser for 'HOLTerm's that satisfies the following BNF
grammar:
@
PRETERM :: APPL_PRETERM binop APPL_PRETERM
| APPL_PRETERM
APPL_PRETERM :: BINDER_PRETERM+
| BINDER_PRETERM : type
BINDER_PRETERM :: tybinder small-type-variables . PRETERM
| binder VARSTRUCT_PRETERM+ . PRETERM
| let PRETERM and ... and PRETERM in PRETERM
| TYPED_PRETERM
TYPED_PRETERM :: TYINST (tyop-var : PRETYPE)+ ATOMIC_PRETERM
| ATOMIC_PRETERM
VARSTRUCT_PRETERM :: ATOMIC_PRETERM : type
| ATOMIC_PRETERM
ATOMIC_PRETERM :: ( PRETERM )
| [: type]
| [ PRETERM; .. ; PRETERM ]
| if PRETERM then PRETERM else PRETERM
| identifier
@
Note that arbitrary atomic preterms, typed or untyped, are allowed as
varstructs in order to simplify parsing. We do not make the same
simplification for @TYINST@ terms in order to avoid the mixing of terms,
types, and type operators.
Also note that a number of advanced HOL term features, mostly relating to sets
and patterns, are not currently supported by the parser. These will be added
in as the relevant logic libraries are added to the system.
As a heads up, the error messages thrown by this parser leave much to be
desired.
-}
module HaskHOL.Core.Parser.TermParser
( pterm
) where
import HaskHOL.Core.Lib hiding (many)
import HaskHOL.Core.State
import HaskHOL.Core.Parser.Lib
import HaskHOL.Core.Parser.TypeParser
-- | Parser for HOL terms.
pterm :: MyParser thry PreTerm
pterm =
do mywhiteSpace
ctxt <- getState
buildExpressionParser (partitionOps ctxt) pappl
pappl :: MyParser thry PreTerm
pappl =
try (do prefs <- pprefixes
if null prefs
then fail "pappl: no prefix found"
else do bod <- pappl
return $! foldr PComb bod prefs)
<|> (do tms <- many1 pbinder
let tm = mkPComb tms
pas tm <|> return tm)
pbinder :: MyParser thry PreTerm
pbinder =
(do myreserved "let"
tms <- pterm `sepBy1` myreserved "and"
myreserved "in"
bod <- pterm
case mkLet tms bod of
Nothing -> fail "pterm: invalid let construction"
Just tm -> return tm)
<|> do (ctxt, _) <- getState
bind <- choiceOp $ binders ctxt
(do vars <- many1 pvar
myreservedOp "."
bod <- pterm
return $! mkBinders bind vars bod)
<|> (return $! PVar bind dpty)
<|> do (ctxt, _) <- getState
bind <- choiceOp $ tyBinders ctxt
(do vars <- many1 psmall
myreservedOp "."
bod <- pterm
return $! mkTyBinders bind vars bod)
<|> (return $! PVar bind dpty)
<|> ptyped
where
ptyped :: MyParser thry PreTerm
ptyped =
(do myreserved "TYINST"
vars <- many1 pinst
tm <- patomic
return $! PInst vars tm)
<|> patomic
where pinst :: MyParser thry (PreType, String)
pinst = myparens $ do myreservedOp "_"
x <- myidentifier
myreservedOp ":"
ty <- ptype
return (ty, x)
pvar :: MyParser thry PreTerm
pvar =
do tm <- patomic
pas tm <|> return tm
pas :: PreTerm -> MyParser thry PreTerm
pas ptm =
do myreservedOp ":"
ty <- ptype
return $! PAs ptm ty
patomic :: MyParser thry PreTerm
patomic =
myparens (pterm <|> (do x <- myoperator
return $! PVar x dpty))
<|> mybrackets
((do myreservedOp ":"
ty <- ptype
return $! PApp ty)
<|> (do tms <- mysemiSep pterm
return (foldr (\ x y -> PVar "CONS" dpty `PComb`
x `PComb` y)
(PVar "NILS" dpty) tms)))
{- <|> mybraces
((do tms <- mycommaSep pterm
return $! foldr (\ x y -> PComb (PComb (PVar "INSERT" dpty) x) y)
(PVar "EMPTY" dpty) tms)
<|> (do tms <- mypipeSep pterm
if length tms == 2
then -- setabs
else if length tms == 3
then -- setcompr))
-}
<|> (do myreserved "if"
c <- pterm
myreserved "then"
t <- pterm
myreserved "else"
e <- pterm
return $! PComb (PComb (PComb (PVar "COND" dpty) c) t) e)
<|> (do x <- myidentifier
return $! PVar x dpty)
pprefixes :: MyParser thry [PreTerm]
pprefixes =
do (ctxt, _) <- getState
pref <- myoperator
let prefOps = sortBy (\ x y -> compare (length y) (length x)) $
prefixes ctxt
return $! splitPref pref prefOps []
where splitPref :: String -> [String] -> [PreTerm] -> [PreTerm]
splitPref _ [] acc = acc
splitPref ops prefs@(p:ps) acc =
case stripPrefix p ops of
Nothing -> splitPref ops ps acc
Just ops' ->
let acc' = acc ++ [PVar p dpty] in
if null ops' then acc'
else splitPref ops' prefs acc'
-- helper functions
mkPComb :: [PreTerm] -> PreTerm
mkPComb (tm:[]) = tm
mkPComb (tm:tms) = foldr (flip PComb) tm (reverse tms)
mkPComb _ = error "parser: mkPComb used without many1 parser combinator"
pdestEq :: PreTerm -> Maybe (PreTerm, PreTerm)
pdestEq (PComb (PComb (PVar "=" _) l) r) = Just (l, r)
pdestEq (PComb (PComb (PVar "<=>" _) l) r) = Just (l, r)
pdestEq _ = Nothing
mkLet :: [PreTerm] -> PreTerm -> Maybe PreTerm
mkLet binds bod = case length tms of
0 -> Nothing
_ -> Just $ foldl PComb letstart tms
where (vars, tms) = unzip $ mapMaybe pdestEq binds
letend = PComb (PVar "LET_END" dpty) bod
ab = foldr PAbs letend vars
letstart = PComb (PVar "LET" dpty) ab
mkBinder :: String -> PreTerm -> PreTerm -> PreTerm
mkBinder "\\" v bod = PAbs v bod
mkBinder n v bod = PComb (PVar n dpty) $ PAbs v bod
mkBinders :: String -> [PreTerm] -> PreTerm -> PreTerm
mkBinders bind vars bod = foldr (mkBinder bind) bod vars
mkTyBinder :: String -> PreType -> PreTerm -> PreTerm
mkTyBinder "\\\\" v bod = TyPAbs v bod
mkTyBinder n v bod = PComb (PVar n dpty) $ TyPAbs v bod
mkTyBinders :: String -> [PreType] -> PreTerm -> PreTerm
mkTyBinders bind vars bod = foldr (mkTyBinder bind) bod vars
-- build op table for expression parser from context
-- Note: prefix operators are handled separately in pprefixes
partitionOps :: (HOLContext thry, [(String, Int)]) ->
OperatorTable Char (HOLContext thry, [(String, Int)]) PreTerm
partitionOps (ctxt, _) = map (map mkOp) .
group' (\ (_, (x, _)) (_, (y, _)) -> x == y) $
infixes ctxt
where mkOp :: (String, (Int, Assoc)) ->
Operator Char (HOLContext thry, [(String, Int)]) PreTerm
mkOp (name, (_, a)) =
Infix (do myreservedOp name
return (\ x y -> PComb (PComb (PVar name dpty) x) y)) a