{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module : ./HolLight/Sentence.hs
Description : Sentence for HolLight logic
Copyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
License : GPLv2 or higher, see LICENSE.txt
Maintainer : jonathan.von_schroeder@dfki.de
Stability : experimental
Portability : portable
Definition of sentences for HolLight logic
Ref.
-}
module HolLight.Sentence where
import Common.DocUtils
import Common.Doc
import HolLight.Helper as Helper
import HolLight.Term
import Data.Data
import Data.Maybe (fromJust, catMaybes, isNothing)
import qualified Data.Char as Char
data Sentence = Sentence {
term :: Term,
proof :: Maybe HolProof
} deriving (Eq, Ord, Show, Typeable, Data)
instance Pretty Sentence where
pretty = ppPrintTerm . term
ppPrintTerm :: Term -> Doc
ppPrintTerm = printTerm 0
precParens :: Int -> Doc -> Doc
precParens prec = if prec /= 0 then parens else id
replacePt :: Term -> HolParseType -> Term
replacePt tm pt = case tm of
Var s t _ -> Var s t (HolTermInfo (pt, Nothing))
Const s t _ -> Const s t (HolTermInfo (pt, Nothing))
_ -> tm
printTerm :: Int -> Term -> Doc
printTerm prec tm =
let _1 = case destNumeral tm of
Just i -> Just (text (show i))
_ -> Nothing in
let _2 = case destList tm of
Just tms -> case Helper.typeOf tm of
Just t -> case destType t of
Just (_, x : _) -> case destType x of
Just ("char", _) -> let cs = map codeOfTerm tms
in if any isNothing cs then Nothing
else Just (quotes (text (foldr ((:) . Char.chr) []
(catMaybes cs))))
_ -> Nothing
_ -> Nothing
_ -> Nothing
_ -> Nothing in
let _3 = if isNothing _2 then case destList tm of
Just tms -> Just (brackets (printTermSequence "; " 0 tms))
_ -> Nothing
else Nothing in
let _4 = if isGabs tm then Just (printBinder prec tm)
else Nothing in
let (s, _, args, hop) = case stripComb tm of
(hop', args') -> case fromJust (Helper.typeOf hop') of
{- not really sure in which cases (typeOf hop) == Nothing,
but shouldn't happen if i understand the original
ocaml code correctly -}
ty0' ->
let s0 = nameOf hop' in
case reverseInterface (s0, hop') of
(s', Just pt) -> (s', ty0', args', replacePt hop' pt)
_ -> (s0, ty0', args', hop') in
let _5 = case (s, isConst tm, null args) of
("EMPTY", True, True) -> Just (braces empty)
("UNIV", True, True) -> case Helper.typeOf tm of
Just t -> case destFunTy t of
Just (ty, _) -> Just (parens (hcat [text ":", ppPrintType ty]))
_ -> Nothing
_ -> Nothing
("INSERT", _, _) ->
let (mems, oth) = splitlist (destBinary' "INSERT") tm
in case (isConst oth, destConst oth) of
(True, Just ("EMPTY", _)) -> Just (braces (printTermSequence
", " 14 mems))
_ -> Nothing
("GSPEC", _, _) -> case rand tm of
Just rtm -> case body rtm of
Just b -> let (evs, bod) = stripExists b
in case destComb bod of
Nothing -> Nothing
Just (bod1, fabs) ->
case destComb bod1 of
Nothing -> Nothing
Just (bod2, babs) ->
case rator bod2 of
Nothing -> Nothing
Just c ->
case destConst c of
Just ("SETSPEC", _) ->
Just (braces (hcat [
printTerm 0 fabs,
text " | ",
printTermSequence "," 14 evs,
text " | ",
printTerm 0 babs
]))
_ -> Nothing
_ -> Nothing
_ -> Nothing
_ -> Nothing in
let _6 = case destLet tm of
Just (e : eqs, _) -> case mkEq e of
Just e' -> let eqs' = map (\ (v, t) -> mkEq (v, t)) eqs
in if elem Nothing eqs' then Nothing else
Just (precParens prec
(hcat [
text "let ",
printTerm 0 e',
vcat (map (\ eq -> hcat [
text "and ",
printTerm 0 eq]) (catMaybes eqs')
++ [text " in", text ""])
]))
_ -> Nothing
_ -> Nothing in
let _7 = if s == "DECIMAL" && length args > 2 then
case (destNumeral (head args), destNumeral (args !! 1)) of
(Just n_num, Just n_den) -> if not (powerof10 n_den) then Nothing
else let s_num = text (show (n_num `quot` n_den)) in
let s_den = text (concat (tail (map (: [])
(show (n_den + (n_num `mod` n_den)))
)))
in Just (hcat [text "#", s_num, if n_den == 1 then empty
else text ".",
s_den])
_ -> Nothing
else Nothing in
let _8 = if s == "_MATCH" && length args == 2 then
case destClauses (args !! 1) of
Just cls -> Just (precParens prec (vcat [
hcat [text "match ",
printTerm 0 (head args),
text " with"],
printClauses cls]))
_ -> Nothing
else Nothing in
let _9 = if s == "_FUNCTION" && length args == 1 then
case destClauses (head args) of
Just cls -> Just (precParens prec (vcat [
text "function",
printClauses cls
]))
_ -> Nothing
else Nothing in
let _10 = if s == "COND" && length args == 3 then
Just (precParens prec (vcat [
hcat [text "if ", printTerm 0 (head args)],
hcat [text " then ", printTerm 0 (args !! 1)],
hcat [text " else ", printTerm 0 (args !! 2)]
]))
else Nothing in
let _11 = if isPrefix hop && length args == 1 then
Just ((if prec == 1000 then parens else id)
(hcat $ if all Char.isAlphaNum s || s == "--"
|| (
case destComb (head args) of
Just (l, _) -> let (s0, _) = (nameOf l, Helper.typeOf l)
in fst (reverseInterface (s0, hop)) == "--"
|| (case destConst l of
Just (f, _) -> f `elem` ["real_of_num",
"int_of_num"]
_ -> False)
_ -> False)
|| s == "~" then
[text s, printTerm 999 (head args), text " "]
else [text s, printTerm 999 (head args)]))
else Nothing in
let _12 = if parsesAsBinder hop && length args == 1 && isGabs (head args)
then Just (printBinder prec tm)
else Nothing in
let _13 = if canGetInfixStatus hop && length args == 2 then
let bargs = if aright hop then
let (tms, tmt) = splitlist (destBinary hop) tm
in tms ++ [tmt]
else
let (tmt, tms) = revSplitlist (destBinary hop) tm
in tmt : tms in
let (newprec, unspaced_binops) = (getPrec hop, [",", "..", "$"])
in Just ((if newprec <= prec then parens else id) (hcat
(printTerm newprec (head bargs) :
map (\ x -> hcat $
if s `elem` unspaced_binops then [text s,
printTerm newprec x]
else
[text " ", text s, text " ", printTerm newprec x]
) (tail bargs)
)))
else Nothing in
let _14 = if (isConst hop || isVar hop) && null args then
let s' = if parsesAsBinder hop || canGetInfixStatus hop
|| isPrefix tm then parens (text s) else text s
in Just s'
else Nothing in
let _15 = case destComb tm of
Just (l, r) -> let mem = case destConst l of
Just (s', _) -> s' `elem`
["real_of_num", "int_of_num"]
_ -> False
in Just ((if prec == 1000 then parens else id)
(hcat $ if not mem
then [printTerm 999 l, text " ",
printTerm 1000 r]
else [printTerm 999 l,
printTerm 1000 r]))
_ -> Nothing
in head (catMaybes [_1, _2, _3, _4, _5, _6, _7, _8, _9,
_10, _11, _12, _13, _14, _15, Just empty])
printTermSequence :: String -> Int -> [Term] -> Doc
printTermSequence sep' prec tms =
if null tms then empty
else hcat (punctuate (text sep') (map (printTerm prec) tms))
printBinder :: Int -> Term -> Doc
printBinder prec tm =
let absf = isGabs tm in
let s' = if absf then Just "\\"
else case rator tm of
Just r -> Just (nameOf r)
Nothing -> Nothing in
case s' of
Just s -> let collectvs tm'
| absf =
if isAbs tm' then
case destAbs tm' of
Just (v, t) -> let (vs, bod) = collectvs t
in ((False, v) : vs, bod)
_ -> ([], tm')
else if isGabs tm' then
case destGabs tm' of
Just (v, t) -> let (vs, bod) = collectvs t
in ((True, v) : vs, bod)
_ -> ([], tm')
else ([], tm')
| isComb tm' =
case rator tm' of
Just r'' -> if nameOf r'' == s then
case rand tm' of
Just r'
| isAbs r' ->
case destAbs r' of
Just (v, t) -> let (vs, bod) = collectvs t
in ((False, v) : vs, bod)
_ -> ([], tm')
| isGabs r' ->
case destGabs r' of
Just (v, t) -> let (vs, bod) = collectvs t
in ((True, v) : vs, bod)
_ -> ([], tm')
| otherwise -> ([], tm')
_ -> ([], tm')
else ([], tm')
_ -> ([], tm')
| otherwise = ([], tm') in
let (vs, bod) = collectvs tm in
precParens prec (hcat ([
text s,
if all Char.isAlphaNum s then text " " else empty]
++ map (\ (b, x) -> hcat [
(if b then parens else id) (printTerm 0 x),
text " "] )
(init vs)
++ [
if fst (last vs) then text "(" else empty,
printTerm 0 (snd (last vs)),
if fst (last vs) then text ")" else empty,
text ".",
if length vs == 1 then text " " else empty,
printTerm 0 bod
]
))
_ -> empty
printClauses :: [[Term]] -> Doc
printClauses cls = case cls of
[] -> empty
c : cls' -> vcat (printClause c :
map (\ cl -> hcat [text "| ", printClause cl]) cls')
printClause :: [Term] -> Doc
printClause cl = case cl of
[p, g, r] -> hcat [printTerm 1 p,
text " when ",
printTerm 1 g,
text " -> ",
printTerm 1 r]
[p, r] -> hcat [printTerm 1 p,
text " -> ",
printTerm 1 r]
_ -> empty