module HaskHOL.Core.Printer
(
FlagRevInterface(..)
, FlagPrintAllThm(..)
, addUnspacedBinop
, addPrebrokenBinop
, removeUnspacedBinop
, removePrebrokenBinop
, getUnspacedBinops
, getPrebrokenBinops
, ppType
, ppTerm
, ppThm
, ShowHOL(..)
, printHOL
) where
import HaskHOL.Core.Lib hiding (empty, lefts, rights)
import HaskHOL.Core.Kernel
import HaskHOL.Core.State
import HaskHOL.Core.Basics
import HaskHOL.Core.Parser
import Text.PrettyPrint
newFlag "FlagRevInterface" True
newFlag "FlagPrintAllThm" True
newExtension "UnspacedBinops" [| [",", "..", "$"] :: [String] |]
newExtension "PrebrokenBinops" [| ["==>"] :: [String] |]
addUnspacedBinop :: String -> HOL Theory thry ()
addUnspacedBinop op =
modifyExt (\ (UnspacedBinops ops) -> UnspacedBinops $ op `insert` ops)
addPrebrokenBinop :: String -> HOL Theory thry ()
addPrebrokenBinop op =
modifyExt (\ (PrebrokenBinops ops) -> PrebrokenBinops $ op `insert` ops)
removeUnspacedBinop :: String -> HOL Theory thry ()
removeUnspacedBinop op =
modifyExt (\ (UnspacedBinops ops) -> UnspacedBinops $ ops \\ [op])
removePrebrokenBinop :: String -> HOL Theory thry ()
removePrebrokenBinop op =
modifyExt (\ (PrebrokenBinops ops) -> PrebrokenBinops $ ops \\ [op])
getUnspacedBinops :: HOLContext thry -> [String]
getUnspacedBinops ctxt =
let (UnspacedBinops ops) = getExtCtxt ctxt in ops
getPrebrokenBinops :: HOLContext thry -> [String]
getPrebrokenBinops ctxt =
let (PrebrokenBinops ops) = getExtCtxt ctxt in ops
ppType :: HOLType -> String
ppType = render . ppTypeRec 0
where ppTypeRec :: Int -> HOLType -> Doc
ppTypeRec _ (view -> TyVar False x) = text x
ppTypeRec _ (view -> TyVar True x) = text $ '\'' : x
ppTypeRec prec ty =
case destUTypes ty of
Just (tvs, bod) ->
let tvs' = foldr (\ x acc -> ppTypeRec prec x <+> acc)
empty tvs in
parens $ char '%' <+> tvs' <+> char '.' <+>
ppTypeRec prec bod
Nothing ->
case do (op, tys) <- destType ty
let (name, ar) = destTypeOp op
name' = if ar < 0 then '_':name else name
return (name', tys) of
Just (op, []) -> text op
Just ("fun", ty1:ty2:[]) ->
ppTypeApp "->" (prec > 0) [ ppTypeRec 1 ty1
, ppTypeRec 0 ty2]
Just ("sum", ty1:ty2:[]) ->
ppTypeApp "+" (prec > 2) [ ppTypeRec 3 ty1
, ppTypeRec 2 ty2]
Just ("prod", ty1:ty2:[]) ->
ppTypeApp "#" (prec > 4) [ ppTypeRec 5 ty1
, ppTypeRec 4 ty2]
Just ("cart", ty1:ty2:[]) ->
ppTypeApp "^" (prec > 6) [ ppTypeRec 6 ty1
, ppTypeRec 7 ty2]
Just (bin, args) ->
ppTypeApp "," True (map (ppTypeRec 0) args) <+> text bin
_ -> text "ppType: printer error - unrecognized type"
ppTypeApp :: String -> Bool -> [Doc] -> Doc
ppTypeApp sepr flag ds =
case tryFoldr1 (\ x y -> x <+> text sepr <+> y) ds of
Nothing -> empty
Just bod -> if flag then parens bod else bod
ppTerm :: HOLContext thry -> HOLTerm -> String
ppTerm ctxt = render . ppTermRec 0
where ppTermRec :: Int -> HOLTerm -> Doc
ppTermRec prec tm =
case destList tm of
Just tms -> brackets $ ppTermSeq ";" 0 tms
Nothing ->
case destTyComb tm of
Just (t, ty) ->
let base = ppTermRec 999 t <+>
brackets (char ':' <> text (ppType ty)) in
if prec == 1000 then parens base else base
Nothing ->
case destLet tm of
Just (eq:eqs, bod) ->
let ppLet x = case uncurry primMkEq x of
Right x' -> ppTermRec 0 x'
_ -> text "<*bad let binding*>"
base = hang
(text "let" <+>
foldr (\ eq' acc -> acc <+> text "and" <+>
ppLet eq') (ppLet eq) eqs <+>
text "in") 2 $ ppTermRec 0 bod in
if prec == 0 then base else parens base
_ ->
let (hop, args) = stripComb tm in
if isAbs hop && null args
then ppBinder prec "\\" False hop
else
if isTyAbs hop && null args
then ppBinder prec "\\\\" True hop
else let s0 = case view hop of
Var x _ -> x
Const x _ _ -> x
_ -> ""
ty0 = typeOf hop
s = reverseInterface s0 ty0 in
if s == "GABS"
then case destGAbs tm of
Nothing -> text "ppTerm: printer error - GAbs case"
Just (vs, bod) ->
let base = char '\\' <+> ppTermRec 999 vs <+>
char '.' <+> ppTermRec 0 bod in
if prec == 0 then base else parens base
else
if s == "COND" && length args == 3
then let (c:t:e:_) = args
base = text "if" <+> ppTermRec 0 c <+>
text "then" <+> ppTermRec 0 t <+>
text "else" <+> ppTermRec 0 e in
if prec == 0 then base else parens base
else
if s `elem` prefix &&
length args == 1
then let base = text s <+> ppTermRec 999 (head args) in
if prec == 1000 then parens base else base
else
if s `elem` binds &&
length args == 1 &&
isGAbs (head args)
then ppBinder prec s False tm
else
if s `elem` tybinds &&
length args == 1 &&
isTyAbs (head args)
then ppBinder prec s True tm
else
let getRight = s `lookup` rights
getLeft = s `lookup` lefts in
if (isJust getRight || isJust getLeft) &&
length args == 2
then let (barg:bargs) =
if isJust getRight
then let (tms, tmt) =
splitList (destBinaryTm hop) tm in
tms ++ [tmt]
else let (tmt, tms) =
revSplitList (destBinaryTm hop) tm in
tmt:tms
newprec = fromMaybe 0 (getRight <|> getLeft)
wrapper = if newprec <= prec then parens else id
sepr =
if s `elem` getUnspacedBinops ctxt
then (\ x y -> cat [x, y])
else (\ x y -> sep [x, y])
hanger =
if s `elem` getPrebrokenBinops ctxt
then (\ x y -> x `sepr` (text s <+> y))
else (\ x y -> (x <+> text s) `sepr` y) in
wrapper $
foldr (\ x acc -> acc `hanger`
ppTermRec newprec x)
(ppTermRec newprec barg) $ reverse bargs
else
if null args && (isConst hop || isVar hop)
then if s `elem` binds ||
s `elem` tybinds ||
isJust (s `lookup` rights) ||
isJust (s `lookup` lefts) ||
s `elem` prefix
then parens $ text s
else text s
else case destComb tm of
Just (l, r) ->
let base = ppTermRec 999 l <+> ppTermRec 1000 r in
if prec == 1000 then parens base else base
_ -> text "ppTerm: printer error - unrecognized term"
grabInfix :: Assoc -> [(String, (Int, Assoc))] -> [(String, Int)]
grabInfix a =
mapMaybe (\ (x, (n, a')) -> if a == a'
then Just (x, n)
else Nothing)
binds :: [String]
binds = binders ctxt
tybinds :: [String]
tybinds = tyBinders ctxt
prefix :: [String]
prefix = prefixes ctxt
lefts :: [(String, Int)]
lefts = grabInfix AssocLeft $ infixes ctxt
rights :: [(String, Int)]
rights = grabInfix AssocRight $ infixes ctxt
ppTermSeq :: String -> Int -> [HOLTerm] -> Doc
ppTermSeq sepr prec = ppTermSeqRec
where ppTermSeqRec [] = empty
ppTermSeqRec (x:[]) = ppTermRec prec x
ppTermSeqRec (x:xs) =
ppTermRec prec x <+> text sepr <+> ppTermSeqRec xs
ppBinder :: Int -> String -> Bool -> HOLTerm -> Doc
ppBinder prec prep f tm =
let (vs, bod) = if f then stripTy ([], tm) else stripTm ([], tm)
base = let bvs = text prep <>
foldr (\ x acc -> acc <+> text x) empty vs <>
char '.'
indent = min (1 + length (render bvs)) 5 in
cat [ bvs
, nest indent $ ppTermRec prec bod
] in
if prec == 0 then base else parens base
where stripTm :: ([String], HOLTerm) -> ([String], HOLTerm)
stripTm (acc, view -> Abs (view -> Var bv _) bod) =
stripTm (bv:acc, bod)
stripTm pat@(acc, view -> Comb (view -> Const s _ _)
(view -> Abs (view -> Var bv _) bod))
| s == prep = stripTm (bv:acc, bod)
| otherwise = pat
stripTm pat = pat
stripTy :: ([String], HOLTerm) -> ([String], HOLTerm)
stripTy (acc, view -> TyAbs (view -> TyVar _ bv) bod) =
stripTy (('\'':bv):acc, bod)
stripTy pat@(acc, view -> Comb (view -> Const s _ _)
(view -> TyAbs (view -> TyVar _ bv) bod))
| s == prep = stripTy (('\'':bv):acc, bod)
| otherwise = pat
stripTy pat = pat
destBinaryTm :: HOLTerm -> HOLTerm -> Maybe (HOLTerm, HOLTerm)
destBinaryTm c tm =
do (il, r) <- destComb tm
(i, l) <- destComb il
if i == c
then do i' <- destConst i
c' <- destConst c
if uncurry reverseInterface i' ==
uncurry reverseInterface c'
then Just (l, r)
else Nothing
else Nothing
reverseInterface :: String -> HOLType -> String
reverseInterface s0 ty0
| not (getBenignFlagCtxt FlagRevInterface ctxt) = s0
| otherwise = fromMaybe s0 . liftM fst .
find (\ (_, (s', ty)) -> s' == s0 &&
isJust (typeMatch ty ty0 ([], [], []))) $
getInterface ctxt
ppThm :: HOLContext thry -> HOLThm -> String
ppThm ctxt (view -> Thm asl c) = render ppThmRec
where ppThmRec :: Doc
ppThmRec =
let c' = text $ ppTerm ctxt c
asl'
| null asl = [empty]
| not (getBenignFlagCtxt FlagPrintAllThm ctxt) = [text "..."]
| otherwise = showHOLListRec comma $ map (ppTerm ctxt) asl in
sep (asl' ++ [text "|-" <+> c'])
class ShowHOL a thry where
showHOL :: a -> HOL cls thry String
instance ShowHOL String thry where
showHOL = return
instance ShowHOL a thry => ShowHOL [a] thry where
showHOL = liftM (showHOLList brackets comma) . mapM showHOL
instance (ShowHOL a thry, ShowHOL b thry) => ShowHOL (a, b) thry where
showHOL (a, b) = liftM (showHOLList parens comma) . sequence $
[showHOL a, showHOL b]
instance (ShowHOL a thry, ShowHOL b thry, ShowHOL c thry) =>
ShowHOL (a, b, c) thry where
showHOL (a, b, c) = liftM (showHOLList parens comma) . sequence $
[showHOL a, showHOL b, showHOL c]
instance (ShowHOL a thry, ShowHOL b thry, ShowHOL c thry, ShowHOL d thry) =>
ShowHOL (a, b, c, d) thry where
showHOL (a, b, c, d) = liftM (showHOLList parens comma) . sequence $
[showHOL a, showHOL b, showHOL c, showHOL d]
showHOLList :: (Doc -> Doc) -> Doc -> [String] -> String
showHOLList wrap sepr = render . wrap . sep . showHOLListRec sepr
showHOLListRec :: Doc -> [String] -> [Doc]
showHOLListRec _ [] = [empty]
showHOLListRec _ (x:[]) = [text x]
showHOLListRec sepr (x:xs) = (text x <> sepr <> space) : showHOLListRec sepr xs
instance ShowHOL Assoc thry where
showHOL (AssocNone) = return "None"
showHOL (AssocLeft) = return "Left"
showHOL (AssocRight) = return "Right"
instance ShowHOL TypeOp thry where
showHOL = return . show
instance ShowHOL HOLType thry where
showHOL ty = return $ ':' : ppType ty
instance ShowHOL HOLTerm thry where
showHOL tm = do ctxt <- get
return $! ppTerm ctxt tm
instance ShowHOL HOLThm thry where
showHOL thm = do ctxt <- get
return $! ppThm ctxt thm
printHOL :: ShowHOL a thry => a -> HOL cls thry ()
printHOL = putStrLnHOL <=< showHOL
deriveLiftMany [''UnspacedBinops, ''PrebrokenBinops]