{-# 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.

  <http://www.cl.cam.ac.uk/~jrh13/hol-light/>

-}
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 {
  Sentence -> Term
term :: Term,
  Sentence -> Maybe HolProof
proof :: Maybe HolProof
  } deriving (Sentence -> Sentence -> Bool
(Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Bool) -> Eq Sentence
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sentence -> Sentence -> Bool
$c/= :: Sentence -> Sentence -> Bool
== :: Sentence -> Sentence -> Bool
$c== :: Sentence -> Sentence -> Bool
Eq, Eq Sentence
Eq Sentence =>
(Sentence -> Sentence -> Ordering)
-> (Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Sentence)
-> (Sentence -> Sentence -> Sentence)
-> Ord Sentence
Sentence -> Sentence -> Bool
Sentence -> Sentence -> Ordering
Sentence -> Sentence -> Sentence
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Sentence -> Sentence -> Sentence
$cmin :: Sentence -> Sentence -> Sentence
max :: Sentence -> Sentence -> Sentence
$cmax :: Sentence -> Sentence -> Sentence
>= :: Sentence -> Sentence -> Bool
$c>= :: Sentence -> Sentence -> Bool
> :: Sentence -> Sentence -> Bool
$c> :: Sentence -> Sentence -> Bool
<= :: Sentence -> Sentence -> Bool
$c<= :: Sentence -> Sentence -> Bool
< :: Sentence -> Sentence -> Bool
$c< :: Sentence -> Sentence -> Bool
compare :: Sentence -> Sentence -> Ordering
$ccompare :: Sentence -> Sentence -> Ordering
$cp1Ord :: Eq Sentence
Ord, Int -> Sentence -> ShowS
[Sentence] -> ShowS
Sentence -> String
(Int -> Sentence -> ShowS)
-> (Sentence -> String) -> ([Sentence] -> ShowS) -> Show Sentence
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sentence] -> ShowS
$cshowList :: [Sentence] -> ShowS
show :: Sentence -> String
$cshow :: Sentence -> String
showsPrec :: Int -> Sentence -> ShowS
$cshowsPrec :: Int -> Sentence -> ShowS
Show, Typeable, Typeable Sentence
Constr
DataType
Typeable Sentence =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Sentence -> c Sentence)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Sentence)
-> (Sentence -> Constr)
-> (Sentence -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Sentence))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence))
-> ((forall b. Data b => b -> b) -> Sentence -> Sentence)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Sentence -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Sentence -> r)
-> (forall u. (forall d. Data d => d -> u) -> Sentence -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Sentence -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Sentence -> m Sentence)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sentence -> m Sentence)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sentence -> m Sentence)
-> Data Sentence
Sentence -> Constr
Sentence -> DataType
(forall b. Data b => b -> b) -> Sentence -> Sentence
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sentence -> c Sentence
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sentence
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Sentence -> u
forall u. (forall d. Data d => d -> u) -> Sentence -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sentence
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sentence -> c Sentence
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sentence)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence)
$cSentence :: Constr
$tSentence :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Sentence -> m Sentence
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
gmapMp :: (forall d. Data d => d -> m d) -> Sentence -> m Sentence
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
gmapM :: (forall d. Data d => d -> m d) -> Sentence -> m Sentence
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
gmapQi :: Int -> (forall d. Data d => d -> u) -> Sentence -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sentence -> u
gmapQ :: (forall d. Data d => d -> u) -> Sentence -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sentence -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
gmapT :: (forall b. Data b => b -> b) -> Sentence -> Sentence
$cgmapT :: (forall b. Data b => b -> b) -> Sentence -> Sentence
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Sentence)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sentence)
dataTypeOf :: Sentence -> DataType
$cdataTypeOf :: Sentence -> DataType
toConstr :: Sentence -> Constr
$ctoConstr :: Sentence -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sentence
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sentence
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sentence -> c Sentence
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sentence -> c Sentence
$cp1Data :: Typeable Sentence
Data)

instance Pretty Sentence where
  pretty :: Sentence -> Doc
pretty = Term -> Doc
ppPrintTerm (Term -> Doc) -> (Sentence -> Term) -> Sentence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sentence -> Term
term

ppPrintTerm :: Term -> Doc
ppPrintTerm :: Term -> Doc
ppPrintTerm = Int -> Term -> Doc
printTerm 0

precParens :: Int -> Doc -> Doc
precParens :: Int -> Doc -> Doc
precParens prec :: Int
prec = if Int
prec Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= 0 then Doc -> Doc
parens else Doc -> Doc
forall a. a -> a
id

replacePt :: Term -> HolParseType -> Term
replacePt :: Term -> HolParseType -> Term
replacePt tm :: Term
tm pt :: HolParseType
pt = case Term
tm of
  Var s :: String
s t :: HolType
t _ -> String -> HolType -> HolTermInfo -> Term
Var String
s HolType
t ((HolParseType, Maybe (String, HolParseType)) -> HolTermInfo
HolTermInfo (HolParseType
pt, Maybe (String, HolParseType)
forall a. Maybe a
Nothing))
  Const s :: String
s t :: HolType
t _ -> String -> HolType -> HolTermInfo -> Term
Const String
s HolType
t ((HolParseType, Maybe (String, HolParseType)) -> HolTermInfo
HolTermInfo (HolParseType
pt, Maybe (String, HolParseType)
forall a. Maybe a
Nothing))
  _ -> Term
tm

printTerm :: Int -> Term -> Doc
printTerm :: Int -> Term -> Doc
printTerm prec :: Int
prec tm :: Term
tm =
 let _1 :: Maybe Doc
_1 = case Term -> Maybe Integer
destNumeral Term
tm of
         Just i :: Integer
i -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (String -> Doc
text (Integer -> String
forall a. Show a => a -> String
show Integer
i))
         _ -> Maybe Doc
forall a. Maybe a
Nothing in
  let _2 :: Maybe Doc
_2 = case Term -> Maybe [Term]
destList Term
tm of
         Just tms :: [Term]
tms -> case Term -> Maybe HolType
Helper.typeOf Term
tm of
           Just t :: HolType
t -> case HolType -> Maybe (String, [HolType])
destType HolType
t of
             Just (_, x :: HolType
x : _) -> case HolType -> Maybe (String, [HolType])
destType HolType
x of
               Just ("char", _) -> let cs :: [Maybe Int]
cs = (Term -> Maybe Int) -> [Term] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Maybe Int
forall b. Num b => Term -> Maybe b
codeOfTerm [Term]
tms
                 in if (Maybe Int -> Bool) -> [Maybe Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe Int -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe Int]
cs then Maybe Doc
forall a. Maybe a
Nothing
                    else Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Doc
quotes (String -> Doc
text ((Int -> ShowS) -> String -> [Int] -> String
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) (Char -> ShowS) -> (Int -> Char) -> Int -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Char
Char.chr) []
                                              ([Maybe Int] -> [Int]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Int]
cs))))
               _ -> Maybe Doc
forall a. Maybe a
Nothing
             _ -> Maybe Doc
forall a. Maybe a
Nothing
           _ -> Maybe Doc
forall a. Maybe a
Nothing
         _ -> Maybe Doc
forall a. Maybe a
Nothing in
 let _3 :: Maybe Doc
_3 = if Maybe Doc -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Doc
_2 then case Term -> Maybe [Term]
destList Term
tm of
            Just tms :: [Term]
tms -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Doc
brackets (String -> Int -> [Term] -> Doc
printTermSequence "; " 0 [Term]
tms))
            _ -> Maybe Doc
forall a. Maybe a
Nothing
       else Maybe Doc
forall a. Maybe a
Nothing in
 let _4 :: Maybe Doc
_4 = if Term -> Bool
isGabs Term
tm then Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Int -> Term -> Doc
printBinder Int
prec Term
tm)
       else Maybe Doc
forall a. Maybe a
Nothing in
 let (s :: String
s, _, args :: [Term]
args, hop :: Term
hop) = case Term -> (Term, [Term])
stripComb Term
tm of
               (hop' :: Term
hop', args' :: [Term]
args') -> case Maybe HolType -> HolType
forall a. HasCallStack => Maybe a -> a
fromJust (Term -> Maybe HolType
Helper.typeOf Term
hop') of
               {- not really sure in which cases (typeOf hop) == Nothing,
               but shouldn't happen if i understand the original
               ocaml code correctly -}
                  ty0' :: HolType
ty0' ->
                    let s0 :: String
s0 = Term -> String
nameOf Term
hop' in
                    case (String, Term) -> (String, Maybe HolParseType)
reverseInterface (String
s0, Term
hop') of
                      (s' :: String
s', Just pt :: HolParseType
pt) -> (String
s', HolType
ty0', [Term]
args', Term -> HolParseType -> Term
replacePt Term
hop' HolParseType
pt)
                      _ -> (String
s0, HolType
ty0', [Term]
args', Term
hop') in
 let _5 :: Maybe Doc
_5 = case (String
s, Term -> Bool
isConst Term
tm, [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
args) of
         ("EMPTY", True, True) -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Doc
braces Doc
empty)
         ("UNIV", True, True) -> case Term -> Maybe HolType
Helper.typeOf Term
tm of
            Just t :: HolType
t -> case HolType -> Maybe (HolType, HolType)
destFunTy HolType
t of
              Just (ty :: HolType
ty, _) -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Doc
parens ([Doc] -> Doc
hcat [String -> Doc
text ":", HolType -> Doc
ppPrintType HolType
ty]))
              _ -> Maybe Doc
forall a. Maybe a
Nothing
            _ -> Maybe Doc
forall a. Maybe a
Nothing
         ("INSERT", _, _) ->
            let (mems :: [Term]
mems, oth :: Term
oth) = (Term -> Maybe (Term, Term)) -> Term -> ([Term], Term)
forall t a. (t -> Maybe (a, t)) -> t -> ([a], t)
splitlist (String -> Term -> Maybe (Term, Term)
destBinary' "INSERT") Term
tm
            in case (Term -> Bool
isConst Term
oth, Term -> Maybe (String, HolType)
destConst Term
oth) of
                 (True, Just ("EMPTY", _)) -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Doc
braces (String -> Int -> [Term] -> Doc
printTermSequence
                                                     ", " 14 [Term]
mems))
                 _ -> Maybe Doc
forall a. Maybe a
Nothing
         ("GSPEC", _, _) -> case Term -> Maybe Term
rand Term
tm of
            Just rtm :: Term
rtm -> case Term -> Maybe Term
body Term
rtm of
              Just b :: Term
b -> let (evs :: [Term]
evs, bod :: Term
bod) = Term -> ([Term], Term)
stripExists Term
b
                        in case Term -> Maybe (Term, Term)
destComb Term
bod of
                             Nothing -> Maybe Doc
forall a. Maybe a
Nothing
                             Just (bod1 :: Term
bod1, fabs :: Term
fabs) ->
                               case Term -> Maybe (Term, Term)
destComb Term
bod1 of
                                 Nothing -> Maybe Doc
forall a. Maybe a
Nothing
                                 Just (bod2 :: Term
bod2, babs :: Term
babs) ->
                                   case Term -> Maybe Term
rator Term
bod2 of
                                     Nothing -> Maybe Doc
forall a. Maybe a
Nothing
                                     Just c :: Term
c ->
                                       case Term -> Maybe (String, HolType)
destConst Term
c of
                                         Just ("SETSPEC", _) ->
                                          Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Doc
braces ([Doc] -> Doc
hcat [
                                           Int -> Term -> Doc
printTerm 0 Term
fabs,
                                           String -> Doc
text " | ",
                                           String -> Int -> [Term] -> Doc
printTermSequence "," 14 [Term]
evs,
                                           String -> Doc
text " | ",
                                           Int -> Term -> Doc
printTerm 0 Term
babs
                                          ]))
                                         _ -> Maybe Doc
forall a. Maybe a
Nothing
              _ -> Maybe Doc
forall a. Maybe a
Nothing
            _ -> Maybe Doc
forall a. Maybe a
Nothing
         _ -> Maybe Doc
forall a. Maybe a
Nothing in
 let _6 :: Maybe Doc
_6 = case Term -> Maybe ([(Term, Term)], Term)
destLet Term
tm of
         Just (e :: (Term, Term)
e : eqs :: [(Term, Term)]
eqs, _) -> case (Term, Term) -> Maybe Term
mkEq (Term, Term)
e of
           Just e' :: Term
e' -> let eqs' :: [Maybe Term]
eqs' = ((Term, Term) -> Maybe Term) -> [(Term, Term)] -> [Maybe Term]
forall a b. (a -> b) -> [a] -> [b]
map (\ (v :: Term
v, t :: Term
t) -> (Term, Term) -> Maybe Term
mkEq (Term
v, Term
t)) [(Term, Term)]
eqs
             in if Maybe Term -> [Maybe Term] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Maybe Term
forall a. Maybe a
Nothing [Maybe Term]
eqs' then Maybe Doc
forall a. Maybe a
Nothing else
                Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Int -> Doc -> Doc
precParens Int
prec
                        ([Doc] -> Doc
hcat [
                          String -> Doc
text "let ",
                          Int -> Term -> Doc
printTerm 0 Term
e',
                          [Doc] -> Doc
vcat ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ eq :: Term
eq -> [Doc] -> Doc
hcat [
                               String -> Doc
text "and ",
                               Int -> Term -> Doc
printTerm 0 Term
eq]) ([Maybe Term] -> [Term]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Term]
eqs')
                                [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Doc
text " in", String -> Doc
text ""])
                        ]))
           _ -> Maybe Doc
forall a. Maybe a
Nothing
         _ -> Maybe Doc
forall a. Maybe a
Nothing in
 let _7 :: Maybe Doc
_7 = if String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "DECIMAL" Bool -> Bool -> Bool
&& [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 2 then
         case (Term -> Maybe Integer
destNumeral ([Term] -> Term
forall a. [a] -> a
head [Term]
args), Term -> Maybe Integer
destNumeral ([Term]
args [Term] -> Int -> Term
forall a. [a] -> Int -> a
!! 1)) of
           (Just n_num :: Integer
n_num, Just n_den :: Integer
n_den) -> if Bool -> Bool
not (Integer -> Bool
powerof10 Integer
n_den) then Maybe Doc
forall a. Maybe a
Nothing
             else let s_num :: Doc
s_num = String -> Doc
text (Integer -> String
forall a. Show a => a -> String
show (Integer
n_num Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
n_den)) in
                  let s_den :: Doc
s_den = String -> Doc
text ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> [String]
forall a. [a] -> [a]
tail ((Char -> String) -> String -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> ShowS
forall a. a -> [a] -> [a]
: [])
                                    (Integer -> String
forall a. Show a => a -> String
show (Integer
n_den Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (Integer
n_num Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
n_den)))
                                   )))
                   in Doc -> Maybe Doc
forall a. a -> Maybe a
Just ([Doc] -> Doc
hcat [String -> Doc
text "#", Doc
s_num, if Integer
n_den Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then Doc
empty
                                            else String -> Doc
text ".",
                            Doc
s_den])
           _ -> Maybe Doc
forall a. Maybe a
Nothing
       else Maybe Doc
forall a. Maybe a
Nothing in
 let _8 :: Maybe Doc
_8 = if String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "_MATCH" Bool -> Bool -> Bool
&& [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 2 then
         case Term -> Maybe [[Term]]
destClauses ([Term]
args [Term] -> Int -> Term
forall a. [a] -> Int -> a
!! 1) of
           Just cls :: [[Term]]
cls -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Int -> Doc -> Doc
precParens Int
prec ([Doc] -> Doc
vcat [
             [Doc] -> Doc
hcat [String -> Doc
text "match ",
              Int -> Term -> Doc
printTerm 0 ([Term] -> Term
forall a. [a] -> a
head [Term]
args),
              String -> Doc
text " with"],
             [[Term]] -> Doc
printClauses [[Term]]
cls]))
           _ -> Maybe Doc
forall a. Maybe a
Nothing
       else Maybe Doc
forall a. Maybe a
Nothing in
 let _9 :: Maybe Doc
_9 = if String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "_FUNCTION" Bool -> Bool -> Bool
&& [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then
            case Term -> Maybe [[Term]]
destClauses ([Term] -> Term
forall a. [a] -> a
head [Term]
args) of
              Just cls :: [[Term]]
cls -> Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Int -> Doc -> Doc
precParens Int
prec ([Doc] -> Doc
vcat [
                  String -> Doc
text "function",
                  [[Term]] -> Doc
printClauses [[Term]]
cls
                ]))
              _ -> Maybe Doc
forall a. Maybe a
Nothing
          else Maybe Doc
forall a. Maybe a
Nothing in
 let _10 :: Maybe Doc
_10 = if String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "COND" Bool -> Bool -> Bool
&& [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 3 then
         Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Int -> Doc -> Doc
precParens Int
prec ([Doc] -> Doc
vcat [
          [Doc] -> Doc
hcat [String -> Doc
text "if ", Int -> Term -> Doc
printTerm 0 ([Term] -> Term
forall a. [a] -> a
head [Term]
args)],
          [Doc] -> Doc
hcat [String -> Doc
text " then ", Int -> Term -> Doc
printTerm 0 ([Term]
args [Term] -> Int -> Term
forall a. [a] -> Int -> a
!! 1)],
          [Doc] -> Doc
hcat [String -> Doc
text " else ", Int -> Term -> Doc
printTerm 0 ([Term]
args [Term] -> Int -> Term
forall a. [a] -> Int -> a
!! 2)]
         ]))
       else Maybe Doc
forall a. Maybe a
Nothing in
 let _11 :: Maybe Doc
_11 = if Term -> Bool
isPrefix Term
hop Bool -> Bool -> Bool
&& [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then
          Doc -> Maybe Doc
forall a. a -> Maybe a
Just ((if Int
prec Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1000 then Doc -> Doc
parens else Doc -> Doc
forall a. a -> a
id)
                ([Doc] -> Doc
hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
Char.isAlphaNum String
s Bool -> Bool -> Bool
|| String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "--"
                    Bool -> Bool -> Bool
|| (
                        case Term -> Maybe (Term, Term)
destComb ([Term] -> Term
forall a. [a] -> a
head [Term]
args) of
                          Just (l :: Term
l, _) -> let (s0 :: String
s0, _) = (Term -> String
nameOf Term
l, Term -> Maybe HolType
Helper.typeOf Term
l)
                            in (String, Maybe HolParseType) -> String
forall a b. (a, b) -> a
fst ((String, Term) -> (String, Maybe HolParseType)
reverseInterface (String
s0, Term
hop)) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "--"
                               Bool -> Bool -> Bool
|| (case Term -> Maybe (String, HolType)
destConst Term
l of
                                    Just (f :: String
f, _) -> String
f String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ["real_of_num",
                                                          "int_of_num"]
                                    _ -> Bool
False)
                          _ -> Bool
False)
                    Bool -> Bool -> Bool
|| String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "~" then
                        [String -> Doc
text String
s, Int -> Term -> Doc
printTerm 999 ([Term] -> Term
forall a. [a] -> a
head [Term]
args), String -> Doc
text " "]
                 else [String -> Doc
text String
s, Int -> Term -> Doc
printTerm 999 ([Term] -> Term
forall a. [a] -> a
head [Term]
args)]))
        else Maybe Doc
forall a. Maybe a
Nothing in
 let _12 :: Maybe Doc
_12 = if Term -> Bool
parsesAsBinder Term
hop Bool -> Bool -> Bool
&& [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 Bool -> Bool -> Bool
&& Term -> Bool
isGabs ([Term] -> Term
forall a. [a] -> a
head [Term]
args)
           then Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Int -> Term -> Doc
printBinder Int
prec Term
tm)
           else Maybe Doc
forall a. Maybe a
Nothing in
 let _13 :: Maybe Doc
_13 = if Term -> Bool
canGetInfixStatus Term
hop Bool -> Bool -> Bool
&& [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 2 then
          let bargs :: [Term]
bargs = if Term -> Bool
aright Term
hop then
                        let (tms :: [Term]
tms, tmt :: Term
tmt) = (Term -> Maybe (Term, Term)) -> Term -> ([Term], Term)
forall t a. (t -> Maybe (a, t)) -> t -> ([a], t)
splitlist (Term -> Term -> Maybe (Term, Term)
destBinary Term
hop) Term
tm
                                         in [Term]
tms [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term
tmt]
                      else
                        let (tmt :: Term
tmt, tms :: [Term]
tms) = (Term -> Maybe (Term, Term)) -> Term -> (Term, [Term])
forall t t1. (t -> Maybe (t, t1)) -> t -> (t, [t1])
revSplitlist (Term -> Term -> Maybe (Term, Term)
destBinary Term
hop) Term
tm
                                         in Term
tmt Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
tms in
          let (newprec :: Int
newprec, unspaced_binops :: [String]
unspaced_binops) = (Term -> Int
getPrec Term
hop, [",", "..", "$"])
          in Doc -> Maybe Doc
forall a. a -> Maybe a
Just ((if Int
newprec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
prec then Doc -> Doc
parens else Doc -> Doc
forall a. a -> a
id) ([Doc] -> Doc
hcat
                    (Int -> Term -> Doc
printTerm Int
newprec ([Term] -> Term
forall a. [a] -> a
head [Term]
bargs) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
                     (Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: Term
x -> [Doc] -> Doc
hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
                      if String
s String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
unspaced_binops then [String -> Doc
text String
s,
                                                        Int -> Term -> Doc
printTerm Int
newprec Term
x]
                      else
                       [String -> Doc
text " ", String -> Doc
text String
s, String -> Doc
text " ", Int -> Term -> Doc
printTerm Int
newprec Term
x]
                     ) ([Term] -> [Term]
forall a. [a] -> [a]
tail [Term]
bargs)
                  )))
        else Maybe Doc
forall a. Maybe a
Nothing in
 let _14 :: Maybe Doc
_14 = if (Term -> Bool
isConst Term
hop Bool -> Bool -> Bool
|| Term -> Bool
isVar Term
hop) Bool -> Bool -> Bool
&& [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
args then
             let s' :: Doc
s' = if Term -> Bool
parsesAsBinder Term
hop Bool -> Bool -> Bool
|| Term -> Bool
canGetInfixStatus Term
hop
                         Bool -> Bool -> Bool
|| Term -> Bool
isPrefix Term
tm then Doc -> Doc
parens (String -> Doc
text String
s) else String -> Doc
text String
s
             in Doc -> Maybe Doc
forall a. a -> Maybe a
Just Doc
s'
           else Maybe Doc
forall a. Maybe a
Nothing in
 let _15 :: Maybe Doc
_15 = case Term -> Maybe (Term, Term)
destComb Term
tm of
              Just (l :: Term
l, r :: Term
r) -> let mem :: Bool
mem = case Term -> Maybe (String, HolType)
destConst Term
l of
                                        Just (s' :: String
s', _) -> String
s' String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`
                                          ["real_of_num", "int_of_num"]
                                        _ -> Bool
False
                            in Doc -> Maybe Doc
forall a. a -> Maybe a
Just ((if Int
prec Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1000 then Doc -> Doc
parens else Doc -> Doc
forall a. a -> a
id)
                                         ([Doc] -> Doc
hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ if Bool -> Bool
not Bool
mem
                                          then [Int -> Term -> Doc
printTerm 999 Term
l, String -> Doc
text " ",
                                                Int -> Term -> Doc
printTerm 1000 Term
r]
                                          else [Int -> Term -> Doc
printTerm 999 Term
l,
                                                Int -> Term -> Doc
printTerm 1000 Term
r]))
              _ -> Maybe Doc
forall a. Maybe a
Nothing
 in [Doc] -> Doc
forall a. [a] -> a
head ([Maybe Doc] -> [Doc]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Doc
_1, Maybe Doc
_2, Maybe Doc
_3, Maybe Doc
_4, Maybe Doc
_5, Maybe Doc
_6, Maybe Doc
_7, Maybe Doc
_8, Maybe Doc
_9,
                     Maybe Doc
_10, Maybe Doc
_11, Maybe Doc
_12, Maybe Doc
_13, Maybe Doc
_14, Maybe Doc
_15, Doc -> Maybe Doc
forall a. a -> Maybe a
Just Doc
empty])

printTermSequence :: String -> Int -> [Term] -> Doc
printTermSequence :: String -> Int -> [Term] -> Doc
printTermSequence sep' :: String
sep' prec :: Int
prec tms :: [Term]
tms =
  if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
tms then Doc
empty
  else [Doc] -> Doc
hcat (Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text String
sep') ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Term -> Doc
printTerm Int
prec) [Term]
tms))

printBinder :: Int -> Term -> Doc
printBinder :: Int -> Term -> Doc
printBinder prec :: Int
prec tm :: Term
tm =
    let absf :: Bool
absf = Term -> Bool
isGabs Term
tm in
    let s' :: Maybe String
s' = if Bool
absf then String -> Maybe String
forall a. a -> Maybe a
Just "\\"
             else case Term -> Maybe Term
rator Term
tm of
                   Just r :: Term
r -> String -> Maybe String
forall a. a -> Maybe a
Just (Term -> String
nameOf Term
r)
                   Nothing -> Maybe String
forall a. Maybe a
Nothing in
    case Maybe String
s' of
     Just s :: String
s -> let collectvs :: Term -> ([(Bool, Term)], Term)
collectvs tm' :: Term
tm'
                    | Bool
absf =
                       if Term -> Bool
isAbs Term
tm' then
                        case Term -> Maybe (Term, Term)
destAbs Term
tm' of
                         Just (v :: Term
v, t :: Term
t) -> let (vs :: [(Bool, Term)]
vs, bod :: Term
bod) = Term -> ([(Bool, Term)], Term)
collectvs Term
t
                                        in ((Bool
False, Term
v) (Bool, Term) -> [(Bool, Term)] -> [(Bool, Term)]
forall a. a -> [a] -> [a]
: [(Bool, Term)]
vs, Term
bod)
                         _ -> ([], Term
tm')
                       else if Term -> Bool
isGabs Term
tm' then
                        case Term -> Maybe (Term, Term)
destGabs Term
tm' of
                         Just (v :: Term
v, t :: Term
t) -> let (vs :: [(Bool, Term)]
vs, bod :: Term
bod) = Term -> ([(Bool, Term)], Term)
collectvs Term
t
                                        in ((Bool
True, Term
v) (Bool, Term) -> [(Bool, Term)] -> [(Bool, Term)]
forall a. a -> [a] -> [a]
: [(Bool, Term)]
vs, Term
bod)
                         _ -> ([], Term
tm')
                       else ([], Term
tm')
                    | Term -> Bool
isComb Term
tm' =
                       case Term -> Maybe Term
rator Term
tm' of
                        Just r'' :: Term
r'' -> if Term -> String
nameOf Term
r'' String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s then
                         case Term -> Maybe Term
rand Term
tm' of
                          Just r' :: Term
r'
                           | Term -> Bool
isAbs Term
r' ->
                              case Term -> Maybe (Term, Term)
destAbs Term
r' of
                               Just (v :: Term
v, t :: Term
t) -> let (vs :: [(Bool, Term)]
vs, bod :: Term
bod) = Term -> ([(Bool, Term)], Term)
collectvs Term
t
                                              in ((Bool
False, Term
v) (Bool, Term) -> [(Bool, Term)] -> [(Bool, Term)]
forall a. a -> [a] -> [a]
: [(Bool, Term)]
vs, Term
bod)
                               _ -> ([], Term
tm')
                           | Term -> Bool
isGabs Term
r' ->
                              case Term -> Maybe (Term, Term)
destGabs Term
r' of
                               Just (v :: Term
v, t :: Term
t) -> let (vs :: [(Bool, Term)]
vs, bod :: Term
bod) = Term -> ([(Bool, Term)], Term)
collectvs Term
t
                                              in ((Bool
True, Term
v) (Bool, Term) -> [(Bool, Term)] -> [(Bool, Term)]
forall a. a -> [a] -> [a]
: [(Bool, Term)]
vs, Term
bod)
                               _ -> ([], Term
tm')
                           | Bool
otherwise -> ([], Term
tm')
                          _ -> ([], Term
tm')
                         else ([], Term
tm')
                        _ -> ([], Term
tm')
                    | Bool
otherwise = ([], Term
tm') in
       let (vs :: [(Bool, Term)]
vs, bod :: Term
bod) = Term -> ([(Bool, Term)], Term)
collectvs Term
tm in
         Int -> Doc -> Doc
precParens Int
prec ([Doc] -> Doc
hcat ([
           String -> Doc
text String
s,
           if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
Char.isAlphaNum String
s then String -> Doc
text " " else Doc
empty]
           [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ ((Bool, Term) -> Doc) -> [(Bool, Term)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (b :: Bool
b, x :: Term
x) -> [Doc] -> Doc
hcat [
                 (if Bool
b then Doc -> Doc
parens else Doc -> Doc
forall a. a -> a
id) (Int -> Term -> Doc
printTerm 0 Term
x),
                 String -> Doc
text " "] )
               ([(Bool, Term)] -> [(Bool, Term)]
forall a. [a] -> [a]
init [(Bool, Term)]
vs)
           [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [
            if (Bool, Term) -> Bool
forall a b. (a, b) -> a
fst ([(Bool, Term)] -> (Bool, Term)
forall a. [a] -> a
last [(Bool, Term)]
vs) then String -> Doc
text "(" else Doc
empty,
            Int -> Term -> Doc
printTerm 0 ((Bool, Term) -> Term
forall a b. (a, b) -> b
snd ([(Bool, Term)] -> (Bool, Term)
forall a. [a] -> a
last [(Bool, Term)]
vs)),
            if (Bool, Term) -> Bool
forall a b. (a, b) -> a
fst ([(Bool, Term)] -> (Bool, Term)
forall a. [a] -> a
last [(Bool, Term)]
vs) then String -> Doc
text ")" else Doc
empty,
            String -> Doc
text ".",
            if [(Bool, Term)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Bool, Term)]
vs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then String -> Doc
text " " else Doc
empty,
            Int -> Term -> Doc
printTerm 0 Term
bod
           ]
          ))
     _ -> Doc
empty

printClauses :: [[Term]] -> Doc
printClauses :: [[Term]] -> Doc
printClauses cls :: [[Term]]
cls = case [[Term]]
cls of
  [] -> Doc
empty
  c :: [Term]
c : cls' :: [[Term]]
cls' -> [Doc] -> Doc
vcat ([Term] -> Doc
printClause [Term]
c Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
   ([Term] -> Doc) -> [[Term]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ cl :: [Term]
cl -> [Doc] -> Doc
hcat [String -> Doc
text "| ", [Term] -> Doc
printClause [Term]
cl]) [[Term]]
cls')

printClause :: [Term] -> Doc
printClause :: [Term] -> Doc
printClause cl :: [Term]
cl = case [Term]
cl of
  [p :: Term
p, g :: Term
g, r :: Term
r] -> [Doc] -> Doc
hcat [Int -> Term -> Doc
printTerm 1 Term
p,
                   String -> Doc
text " when ",
                   Int -> Term -> Doc
printTerm 1 Term
g,
                   String -> Doc
text " -> ",
                   Int -> Term -> Doc
printTerm 1 Term
r]
  [p :: Term
p, r :: Term
r] -> [Doc] -> Doc
hcat [Int -> Term -> Doc
printTerm 1 Term
p,
                 String -> Doc
text " -> ",
                 Int -> Term -> Doc
printTerm 1 Term
r]
  _ -> Doc
empty