haskhol-core-1.1.0: src/HaskHOL/Core/Parser/TermParser.hs
{-# LANGUAGE OverloadedStrings #-}
{-|
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
| match PRETERM with CLAUSES
| function CLAUSES
| identifier
CLAUSES :: PATTERN -> PRETERM | .. | PATTERN -> PRETERM
PATTERN :: PRETERM when PRETERM
| PRETERM
@
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
import HaskHOL.Core.Parser.Lib
import HaskHOL.Core.Parser.TypeParser
-- | Parser for HOL terms.
pterm :: MyParser thry PreTerm
pterm =
(do mywhiteSpace
(ctxt, _, _) <- getState
expressionParser (infixes ctxt) ptyped)
<|> (do s <- myidentifier <|> myoperator
return $! PVar s dpty)
ptyped :: MyParser thry PreTerm
ptyped = pas =<< pappl
pappl :: MyParser thry PreTerm
pappl =
(do p <- pprefix
tm <- pappl
return $! PComb (PVar p dpty) tm)
<|> do (tm:tms) <- mymany1 pbinder
return $! foldr (flip PComb) tm (reverse tms)
pprefix :: MyParser thry Text
pprefix =
do (ctxt, _, _) <- getState
choiceId $ prefixes ctxt
pbinder :: MyParser thry PreTerm
pbinder =
(do myreserved "let"
tms <- pterm `mysepBy1` 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 <- choiceId $ binders ctxt
(do vars <- mymany1 pvar
myreservedOp "."
bod <- pterm
return $! mkBinders bind vars bod)
<|> (return $! PVar bind dpty))
<|> (do (ctxt, _, _) <- getState
bind <- choiceId $ tyBinders ctxt
(do vars <- mymany1 psmall
myreservedOp "."
bod <- pterm
return $! mkTyBinders bind vars bod)
<|> (return $! PVar bind dpty))
<|> pinst
where
pinst :: MyParser thry PreTerm
pinst =
(do myreserved "TYINST"
vars <- mymany1 pinst'
tm <- patomic
return $! PInst vars tm)
<|> patomic
where pinst' :: MyParser thry (PreType, Text)
pinst' = myparens $ do myreservedOp "_"
x <- myidentifier
myreservedOp ":"
ty <- ptype
return (ty, x)
pvar :: MyParser thry PreTerm
pvar = pas =<< patomic
pas :: PreTerm -> MyParser thry PreTerm
pas tm =
(do myreservedOp ":"
ty <- ptype
return $! PAs tm ty) <|> return tm
patomic :: MyParser thry PreTerm
patomic =
myparens ((do myreservedOp ":"
ty <- ptype
return $! PAs (PVar "UNIV" dpty)
(PTyComb (PTyCon "fun")
[ty, PTyComb (PTyCon "bool") []]))
<|> mytry pterm
<|> (do s <- myidentifier <|> myoperator
return (PVar s dpty)))
<|> (do myreserved "if"
c <- pterm
myreserved "then"
t <- pterm
myreserved "else"
e <- pterm
return $! PComb (PComb (PComb (PVar "COND" dpty) c) t) e)
<|> mybrackets
((do myreservedOp ":"
ty <- ptype
return $! PApp ty)
<|> (do tms <- mysemiSep pterm
return (foldr (\ x y -> PVar "CONS" dpty `PComb`
x `PComb` y)
(PVar "NIL" dpty) tms)))
{-
<|> mybraces
((do tms <- mycommaSep pterm
return $! foldr (\ x y -> PComb (PComb (PVar "INSERT" dpty) x) y)
(PVar "EMPTY" dpty) tms)
<|> (do tms <- pterm `sepBy1` myreservedOp "|"
case tms of
(l:r:[]) -> pmkSetAbs l r
(f:v:b:[]) -> pmkSetCompr f (pfrees vs []) b
_ -> fail "patomic: bad set construction."))
-}
<|> (do myreserved "match"
e <- pterm
myreserved "with"
c <- pclauses
return $! PComb (PComb (PVar "_MATCH" dpty) e) c)
<|> (do myreserved "function"
c <- pclauses
return $! PComb (PVar "_FUNCTION" dpty) c)
<|> mytry (do x <- myidentifier <|> myoperator
(ctxt, _, _) <- getState
if x `notElem` prefixes ctxt &&
x `notElem` map fst (infixes ctxt) &&
x `notElem` binders ctxt
then return $! PVar x dpty
else fail "patomic")
pclauses :: MyParser thry PreTerm
pclauses =
do c <- pclause `mysepBy1` myreservedOp "|"
return $! foldr1 (\ s t -> PComb (PComb (PVar "_SEQPATTERN" dpty) s) t) c
where pclause :: MyParser thry PreTerm
pclause = do (pat:guards) <- pterm `mysepBy1` myreserved "when"
myreservedOp "->"
res <- pterm
mkPattern pat guards res
-- helper functions
pgenVar :: MyParser thry PreTerm
pgenVar =
do (ctxt, ops, n) <- getState
setState (ctxt, ops, succ n)
return $! PVar (pack $ "_GENPVAR_" ++ show n) dpty
pfrees :: PreTerm -> [PreTerm] -> MyParser thry [PreTerm]
pfrees ptm@(PVar v pty) acc
| textNull v && pty == dpty = return acc
| otherwise =
do (ctxt, _, _) <- getState
case getTypeArityCtxt ctxt v of
Just _ -> return acc
Nothing ->
case numOfString (unpack v) :: (Maybe Integer) of
Just _ -> return acc
Nothing ->
case lookup v $ getInterfaceCtxt ctxt of
Just _ -> return acc
Nothing -> return $! ptm `insert` acc
pfrees PConst{} acc = return acc
pfrees (PComb p1 p2) acc = pfrees p1 =<< pfrees p2 acc
pfrees (PAbs p1 p2) acc =
do p1s <- pfrees p1 []
p2s <- pfrees p2 acc
return $! p2s \\ p1s
pfrees (PAs p _) acc = pfrees p acc
pfrees (PInst _ p) acc = pfrees p acc
pfrees PApp{} acc = return acc
pfrees (TyPAbs _ p) acc = pfrees p acc
pfrees (TyPComb p _ _) acc = pfrees p acc
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 :: Text -> PreTerm -> PreTerm -> PreTerm
mkBinder "\\" v bod = PAbs v bod
mkBinder n v bod = PComb (PVar n dpty) $ PAbs v bod
mkBinders :: Text -> [PreTerm] -> PreTerm -> PreTerm
mkBinders bind vars bod = foldr (mkBinder bind) bod vars
mkTyBinder :: Text -> PreType -> PreTerm -> PreTerm
mkTyBinder "\\\\" v bod = TyPAbs v bod
mkTyBinder n v bod = PComb (PVar n dpty) $ TyPAbs v bod
mkTyBinders :: Text -> [PreType] -> PreTerm -> PreTerm
mkTyBinders bind vars bod = foldr (mkTyBinder bind) bod vars
mkPattern :: PreTerm -> [PreTerm] -> PreTerm -> MyParser thry PreTerm
mkPattern pat guards res =
do x <- pgenVar
y <- pgenVar
vs <- pfrees pat []
let bod = if null guards
then PComb (PComb (PVar "_UNGUARDED_PATTERN" dpty) $
mkGEQ pat x) $ mkGEQ res y
else PComb (PComb (PComb (PVar "_GUARDED_PATTERN" dpty) $
mkGEQ pat x) $ head guards) $ mkGEQ res y
return . PAbs x . PAbs y $ foldr mkExists bod vs
where mkGEQ :: PreTerm -> PreTerm -> PreTerm
mkGEQ l = PComb (PComb (PVar "GEQ" dpty) l)
mkExists :: PreTerm -> PreTerm -> PreTerm
mkExists v ptm = PComb (PVar "?" dpty) $ PAbs v ptm
-- build expression parser from infix operators in context
expressionParser :: [(Text, (Int, Text))] -> MyParser thry PreTerm
-> MyParser thry PreTerm
expressionParser [] prs = prs
expressionParser infxs@((_, (p, at)):_) prs =
let (topins, rest) = partition (\ (_, pat') -> pat' == (p, at)) infxs
parse' = if at == "right" then pRightBinary else pLeftBinary in
parse' (expressionParser rest prs)
(choiceId (map fst topins))
(\ op x y -> PComb (PComb (PVar op dpty) x) y)
sepPair :: MyParser thry Text -> MyParser thry PreTerm
-> MyParser thry [(Text, PreTerm)]
sepPair sep prs =
mymany (do l <- sep
r <- prs
return (l, r))
pRightBinary :: MyParser thry PreTerm -> MyParser thry Text
-> (Text -> PreTerm -> PreTerm -> PreTerm)
-> MyParser thry PreTerm
pRightBinary prs sep cns =
do x <- prs
opxs <- sepPair sep prs
if null opxs
then return x
else let (ops, xs) = unzip opxs in
case foldr2 cns (last xs) ops (x:init xs) of
Just res -> return res
_ -> fail "pRightBinary"
pLeftBinary :: MyParser thry PreTerm -> MyParser thry Text
-> (Text -> PreTerm -> PreTerm -> PreTerm)
-> MyParser thry PreTerm
pLeftBinary prs sep cns =
do x <- prs
opxs <- sepPair sep prs
let (ops, xs) = unzip opxs in
case foldr2 (\ op l r -> cns op r l) x (reverse ops) (reverse xs) of
Just res -> return res
_ -> fail "pLeftBinary"