{- |
module: $Header$
description: Pretty-printing
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}

module HOL.Print
where

import Control.Monad (guard)
import qualified Data.Char as Char
import qualified Data.List as List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (isJust)
import Data.Set (Set)
import qualified Data.Set as Set
import Prelude hiding ((<>))
import Text.PrettyPrint ((<>),(<+>))
import qualified Text.PrettyPrint as PP

import qualified HOL.Const as Const
import HOL.Data
import HOL.Name
import HOL.Sequent (Sequent)
import qualified HOL.Sequent as Sequent
import qualified HOL.Term as Term
import HOL.TermAlpha (TermAlpha)
import qualified HOL.TermAlpha as TermAlpha
import HOL.Thm (Thm)
import qualified HOL.Thm as Thm
import qualified HOL.Type as Type
import qualified HOL.TypeOp as TypeOp
import HOL.TypeSubst (TypeSubst)
import qualified HOL.TypeSubst as TypeSubst
import qualified HOL.TypeVar as TypeVar
import qualified HOL.Var as Var

-------------------------------------------------------------------------------
-- Printing symbol names
-------------------------------------------------------------------------------

isSymbolChar :: Char -> Bool
isSymbolChar :: Char -> Bool
isSymbolChar = Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
Char.isAlphaNum

isSymbolString :: String -> Bool
isSymbolString :: String -> Bool
isSymbolString [] = Bool
True
isSymbolString [Char
'o'] = Bool
True
isSymbolString [Char
'(',Char
')'] = Bool
False
isSymbolString [Char
'[',Char
']'] = Bool
False
isSymbolString [Char
'{',Char
'}'] = Bool
False
isSymbolString (Char
c : String
_) = Char -> Bool
isSymbolChar Char
c

ppSymbolName :: Name -> PP.Doc
ppSymbolName :: Name -> Doc
ppSymbolName =
    Name -> Doc
parenSymbol (Name -> Doc) -> (Name -> Name) -> Name -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
showName
  where
    showName :: Name -> Name
showName (Name Namespace
ns String
s) = Namespace -> String -> Name
Name (Namespace -> Namespace
showNamespace Namespace
ns) String
s
    showNamespace :: Namespace -> Namespace
showNamespace (Namespace [String]
ns) = [String] -> Namespace
Namespace ((String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
List.dropWhile String -> Bool
isUpper [String]
ns)
    isUpper :: String -> Bool
isUpper [] = Bool
False
    isUpper (Char
c : String
_) = Char -> Bool
Char.isUpper Char
c

    parenSymbol :: Name -> Doc
parenSymbol Name
n = (if Name -> Bool
isSymbol Name
n then Doc -> Doc
PP.parens else Doc -> Doc
forall a. a -> a
id) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Name -> Doc
forall a. Printable a => a -> Doc
toDoc Name
n
    isSymbol :: Name -> Bool
isSymbol (Name (Namespace [String]
ns) String
s) = String -> Bool
isSymbolString ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String]
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s)

-------------------------------------------------------------------------------
-- Printing prefix operators
-------------------------------------------------------------------------------

type PrefixOp = PP.Doc -> PP.Doc

ppPrefixOps :: [PrefixOp] -> PP.Doc -> PP.Doc
ppPrefixOps :: [Doc -> Doc] -> Doc -> Doc
ppPrefixOps = (Doc -> [Doc -> Doc] -> Doc) -> [Doc -> Doc] -> Doc -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Doc -> [Doc -> Doc] -> Doc) -> [Doc -> Doc] -> Doc -> Doc)
-> (Doc -> [Doc -> Doc] -> Doc) -> [Doc -> Doc] -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ((Doc -> Doc) -> Doc -> Doc) -> Doc -> [Doc -> Doc] -> Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Doc -> Doc
p Doc
d -> Doc -> Doc
p Doc
d)

-------------------------------------------------------------------------------
-- Printing infix operators
-------------------------------------------------------------------------------

type Prec = Int

data Assoc =
    LeftAssoc
  | RightAssoc
  | NonAssoc
  deriving (Assoc -> Assoc -> Bool
(Assoc -> Assoc -> Bool) -> (Assoc -> Assoc -> Bool) -> Eq Assoc
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Assoc -> Assoc -> Bool
$c/= :: Assoc -> Assoc -> Bool
== :: Assoc -> Assoc -> Bool
$c== :: Assoc -> Assoc -> Bool
Eq,Eq Assoc
Eq Assoc
-> (Assoc -> Assoc -> Ordering)
-> (Assoc -> Assoc -> Bool)
-> (Assoc -> Assoc -> Bool)
-> (Assoc -> Assoc -> Bool)
-> (Assoc -> Assoc -> Bool)
-> (Assoc -> Assoc -> Assoc)
-> (Assoc -> Assoc -> Assoc)
-> Ord Assoc
Assoc -> Assoc -> Bool
Assoc -> Assoc -> Ordering
Assoc -> Assoc -> Assoc
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 :: Assoc -> Assoc -> Assoc
$cmin :: Assoc -> Assoc -> Assoc
max :: Assoc -> Assoc -> Assoc
$cmax :: Assoc -> Assoc -> Assoc
>= :: Assoc -> Assoc -> Bool
$c>= :: Assoc -> Assoc -> Bool
> :: Assoc -> Assoc -> Bool
$c> :: Assoc -> Assoc -> Bool
<= :: Assoc -> Assoc -> Bool
$c<= :: Assoc -> Assoc -> Bool
< :: Assoc -> Assoc -> Bool
$c< :: Assoc -> Assoc -> Bool
compare :: Assoc -> Assoc -> Ordering
$ccompare :: Assoc -> Assoc -> Ordering
$cp1Ord :: Eq Assoc
Ord,Int -> Assoc -> String -> String
[Assoc] -> String -> String
Assoc -> String
(Int -> Assoc -> String -> String)
-> (Assoc -> String) -> ([Assoc] -> String -> String) -> Show Assoc
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Assoc] -> String -> String
$cshowList :: [Assoc] -> String -> String
show :: Assoc -> String
$cshow :: Assoc -> String
showsPrec :: Int -> Assoc -> String -> String
$cshowsPrec :: Int -> Assoc -> String -> String
Show)

type InfixOp = (Prec, Assoc, PP.Doc -> PP.Doc)

ppInfixOps :: (a -> Maybe (InfixOp,a,a)) -> (Bool -> a -> PP.Doc) ->
              Bool -> a -> PP.Doc
ppInfixOps :: (a -> Maybe (InfixOp, a, a))
-> (Bool -> a -> Doc) -> Bool -> a -> Doc
ppInfixOps a -> Maybe (InfixOp, a, a)
dest Bool -> a -> Doc
pp =
    Maybe Int -> Bool -> a -> Doc
go Maybe Int
forall a. Maybe a
Nothing
  where
    go :: Maybe Int -> Bool -> a -> Doc
go Maybe Int
mprec Bool
rightmost a
a =
        case a -> Maybe (InfixOp, a, a)
dest a
a of
          Maybe (InfixOp, a, a)
Nothing -> Doc
base
          Just ((Int
prec,Assoc
assoc,Doc -> Doc
op),a
x,a
y) ->
              if Bool -> Bool
not (Int -> Maybe Int -> Bool
forall a. Ord a => a -> Maybe a -> Bool
tightEnough Int
prec Maybe Int
mprec) then Doc
base
              else [Doc] -> Doc
PP.fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Assoc -> Bool -> a -> a -> (Doc -> Doc) -> [Doc]
goList Int
prec Assoc
assoc Bool
rightmost a
x a
y Doc -> Doc
op
      where
        base :: Doc
base = Bool -> a -> Doc
pp Bool
rightmost a
a

    goList :: Int -> Assoc -> Bool -> a -> a -> (Doc -> Doc) -> [Doc]
goList Int
prec Assoc
LeftAssoc Bool
rightmost a
x a
y Doc -> Doc
op =
        Int -> a -> (Doc -> Doc) -> [Doc] -> [Doc]
goLeft Int
prec a
x Doc -> Doc
op [Int -> Bool -> a -> Doc
goNext Int
prec Bool
rightmost a
y]
    goList Int
prec Assoc
RightAssoc Bool
rightmost a
x a
y Doc -> Doc
op =
        Doc -> Doc
op (Int -> Bool -> a -> Doc
goNext Int
prec Bool
False a
x) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: Int -> Bool -> a -> [Doc]
goRight Int
prec Bool
rightmost a
y
    goList Int
prec Assoc
NonAssoc Bool
rightmost a
x a
y Doc -> Doc
op =
        [Doc -> Doc
op (Int -> Bool -> a -> Doc
goNext Int
prec Bool
False a
x), Int -> Bool -> a -> Doc
goNext Int
prec Bool
rightmost a
y]

    goLeft :: Int -> a -> (Doc -> Doc) -> [Doc] -> [Doc]
goLeft Int
prec a
a Doc -> Doc
rop [Doc]
ds =
        case a -> Maybe (InfixOp, a, a)
dest a
a of
          Maybe (InfixOp, a, a)
Nothing -> [Doc]
base
          Just ((Int
prec',Assoc
assoc,Doc -> Doc
op),a
x,a
y) ->
              if Int
prec' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
prec then [Doc]
base
              else if Assoc
assoc Assoc -> Assoc -> Bool
forall a. Eq a => a -> a -> Bool
/= Assoc
LeftAssoc then String -> [Doc]
forall a. HasCallStack => String -> a
error String
"mixed associativity"
              else Int -> a -> (Doc -> Doc) -> [Doc] -> [Doc]
goLeft Int
prec a
x Doc -> Doc
op (Doc -> Doc
rop (Int -> Bool -> a -> Doc
goNext Int
prec Bool
False a
y) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
ds)
      where
        base :: [Doc]
base = Doc -> Doc
rop (Int -> Bool -> a -> Doc
goNext Int
prec Bool
False a
a) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
ds

    goRight :: Int -> Bool -> a -> [Doc]
goRight Int
prec Bool
rightmost a
a =
        case a -> Maybe (InfixOp, a, a)
dest a
a of
          Maybe (InfixOp, a, a)
Nothing -> [Doc]
base
          Just ((Int
prec',Assoc
assoc,Doc -> Doc
op),a
x,a
y) ->
              if Int
prec' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
prec then [Doc]
base
              else if Assoc
assoc Assoc -> Assoc -> Bool
forall a. Eq a => a -> a -> Bool
/= Assoc
RightAssoc then String -> [Doc]
forall a. HasCallStack => String -> a
error String
"mixed associativity"
              else Doc -> Doc
op (Int -> Bool -> a -> Doc
goNext Int
prec Bool
False a
x) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: Int -> Bool -> a -> [Doc]
goRight Int
prec Bool
rightmost a
y
      where
        base :: [Doc]
base = [Int -> Bool -> a -> Doc
goNext Int
prec Bool
rightmost a
a]

    goNext :: Int -> Bool -> a -> Doc
goNext Int
prec Bool
rightmost a
a = Maybe Int -> Bool -> a -> Doc
go (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int
prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) Bool
rightmost a
a

    tightEnough :: a -> Maybe a -> Bool
tightEnough a
_ Maybe a
Nothing = Bool
True
    tightEnough a
prec (Just a
mprec) = a
mprec a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
prec

-------------------------------------------------------------------------------
-- Printable types
-------------------------------------------------------------------------------

class Printable a where
  toDoc :: a -> PP.Doc

  toStringWith :: PP.Style -> a -> String
  toStringWith Style
style = Style -> Doc -> String
PP.renderStyle Style
style (Doc -> String) -> (a -> Doc) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Printable a => a -> Doc
toDoc

  toString :: a -> String
  toString = Style -> a -> String
forall a. Printable a => Style -> a -> String
toStringWith Style
style
    where
      style :: Style
style = Style
PP.style {lineLength :: Int
PP.lineLength = Int
80, ribbonsPerLine :: Float
PP.ribbonsPerLine = Float
1.0}

instance Printable PP.Doc where
  toDoc :: Doc -> Doc
toDoc = Doc -> Doc
forall a. a -> a
id

instance Printable Integer where
  toDoc :: Integer -> Doc
toDoc = Integer -> Doc
PP.integer

instance (Printable a, Printable b) => Printable (a,b) where
  toDoc :: (a, b) -> Doc
toDoc (a
x,b
y) = Doc -> Doc
PP.parens (a -> Doc
forall a. Printable a => a -> Doc
toDoc a
x Doc -> Doc -> Doc
<> Doc
PP.comma Doc -> Doc -> Doc
<+> b -> Doc
forall a. Printable a => a -> Doc
toDoc b
y)

instance Printable a => Printable [a] where
  toDoc :: [a] -> Doc
toDoc = Doc -> Doc
PP.brackets (Doc -> Doc) -> ([a] -> Doc) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
PP.fsep ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
PP.punctuate Doc
PP.comma ([Doc] -> [Doc]) -> ([a] -> [Doc]) -> [a] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Printable a => a -> Doc
toDoc

instance Printable a => Printable (Set a) where
  toDoc :: Set a -> Doc
toDoc = Doc -> Doc
PP.braces (Doc -> Doc) -> (Set a -> Doc) -> Set a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
PP.sep ([Doc] -> Doc) -> (Set a -> [Doc]) -> Set a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
PP.punctuate Doc
PP.comma ([Doc] -> [Doc]) -> (Set a -> [Doc]) -> Set a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Printable a => a -> Doc
toDoc ([a] -> [Doc]) -> (Set a -> [a]) -> Set a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> [a]
forall a. Set a -> [a]
Set.toAscList

-------------------------------------------------------------------------------
-- Names
-------------------------------------------------------------------------------

instance Printable Namespace where
  toDoc :: Namespace -> Doc
toDoc =
      Namespace -> Doc
go
    where
      go :: Namespace -> Doc
go (Namespace []) = Doc
pr0
      go (Namespace [String]
l) = [String] -> Doc
pr1 [String]
l

      pr0 :: Doc
pr0 = String -> Doc
PP.text String
"<empty>"
      pr1 :: [String] -> Doc
pr1 = [Doc] -> Doc
PP.hcat ([Doc] -> Doc) -> ([String] -> [Doc]) -> [String] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
PP.punctuate (String -> Doc
PP.text String
".") ([Doc] -> [Doc]) -> ([String] -> [Doc]) -> [String] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
PP.text

instance Printable Name where
  toDoc :: Name -> Doc
toDoc (Name (Namespace [String]
l) String
s) = Namespace -> Doc
forall a. Printable a => a -> Doc
toDoc ([String] -> Namespace
Namespace ([String]
l [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
s]))

quoteNamespace :: Namespace -> PP.Doc
quoteNamespace :: Namespace -> Doc
quoteNamespace (Namespace [String]
l) =
    Doc -> Doc
PP.doubleQuotes (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
PP.hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
PP.punctuate Doc
sep ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
escape [String]
l
  where
    escape :: String -> Doc
escape = [Doc] -> Doc
PP.hcat ([Doc] -> Doc) -> (String -> [Doc]) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Doc) -> String -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Doc
mk
    mk :: Char -> Doc
mk Char
c = let d :: Doc
d = Char -> Doc
PP.char Char
c in if Char -> Bool
escapable Char
c then Doc
esc Doc -> Doc -> Doc
<> Doc
d else Doc
d
    escapable :: Char -> Bool
escapable = (Char -> String -> Bool) -> String -> Char -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
"\"\\."

    sep :: Doc
sep = String -> Doc
PP.text String
"."
    esc :: Doc
esc = Char -> Doc
PP.char Char
'\\'

quoteName :: Name -> PP.Doc
quoteName :: Name -> Doc
quoteName (Name (Namespace [String]
l) String
s) = Namespace -> Doc
quoteNamespace ([String] -> Namespace
Namespace ([String]
l [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
s]))

-------------------------------------------------------------------------------
-- Types
-------------------------------------------------------------------------------

instance Printable TypeVar where
  toDoc :: TypeVar -> Doc
toDoc = Name -> Doc
forall a. Printable a => a -> Doc
toDoc (Name -> Doc) -> (TypeVar -> Name) -> TypeVar -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeVar -> Name
TypeVar.dest

instance Printable TypeOp where
  toDoc :: TypeOp -> Doc
toDoc = Name -> Doc
ppSymbolName (Name -> Doc) -> (TypeOp -> Name) -> TypeOp -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeOp -> Name
TypeOp.name

instance Printable Type where
  toDoc :: Type -> Doc
toDoc =
      Type -> Doc
normal
    where
      basic :: Bool -> Type -> Doc
basic Bool
_ Type
ty =
          if Type -> Bool
isInfix Type
ty then Type -> Doc
parens Type
ty
          else case Type -> TypeData
Type.dest Type
ty of
                 VarType TypeVar
v -> TypeVar -> Doc
forall a. Printable a => a -> Doc
toDoc TypeVar
v
                 OpType TypeOp
t [] -> TypeOp -> Doc
forall a. Printable a => a -> Doc
toDoc TypeOp
t
                 OpType TypeOp
t [Type
x] -> Bool -> Type -> Doc
basic Bool
False Type
x Doc -> Doc -> Doc
<+> TypeOp -> Doc
forall a. Printable a => a -> Doc
toDoc TypeOp
t
                 OpType TypeOp
t [Type]
xs -> [Type] -> Doc
normals [Type]
xs Doc -> Doc -> Doc
<+> TypeOp -> Doc
forall a. Printable a => a -> Doc
toDoc TypeOp
t

      normal :: Type -> Doc
normal = (Type -> Maybe (InfixOp, Type, Type))
-> (Bool -> Type -> Doc) -> Bool -> Type -> Doc
forall a.
(a -> Maybe (InfixOp, a, a))
-> (Bool -> a -> Doc) -> Bool -> a -> Doc
ppInfixOps Type -> Maybe (InfixOp, Type, Type)
destInfix Bool -> Type -> Doc
basic Bool
True

      normals :: [Type] -> Doc
normals = Doc -> Doc
PP.parens (Doc -> Doc) -> ([Type] -> Doc) -> [Type] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
PP.fsep ([Doc] -> Doc) -> ([Type] -> [Doc]) -> [Type] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
PP.punctuate Doc
PP.comma ([Doc] -> [Doc]) -> ([Type] -> [Doc]) -> [Type] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Doc) -> [Type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Doc
normal

      parens :: Type -> Doc
parens = Doc -> Doc
PP.parens (Doc -> Doc) -> (Type -> Doc) -> Type -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Doc
normal

      -------------------------------------------------------------------------
      -- These grammar tables control type printing
      -------------------------------------------------------------------------

      infixTable :: [(Name, Int, Assoc, Maybe a)]
infixTable =
          [--
           -- Primitives
           (Name
TypeOp.funName, Int
1, Assoc
RightAssoc, Maybe a
forall a. Maybe a
Nothing),
           --
           -- Pairs
           (Name
TypeOp.productName, Int
3, Assoc
RightAssoc, Maybe a
forall a. Maybe a
Nothing),
           --
           -- Sums
           (Name
TypeOp.sumName, Int
2, Assoc
RightAssoc, Maybe a
forall a. Maybe a
Nothing)]

      -------------------------------------------------------------------------
      -- Infix type operators
      -------------------------------------------------------------------------

      mkInfixOp :: (Name, a, b, Maybe String) -> (Name, (a, b, Doc -> Doc))
mkInfixOp (Name
n,a
p,b
a,Maybe String
x) =
          (Name
n, (a
p, b
a, (Doc -> Doc -> Doc) -> Doc -> Doc -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Doc -> Doc -> Doc
(<+>) (Doc -> Doc -> Doc) -> Doc -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
PP.text String
s))
        where
          s :: String
s = case Maybe String
x of
                Just y -> String
y
                Maybe String
Nothing -> let Name Namespace
_ String
y = Name
n in String
y

      infixOps :: Map Name InfixOp
      infixOps :: Map Name InfixOp
infixOps = [(Name, InfixOp)] -> Map Name InfixOp
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, InfixOp)] -> Map Name InfixOp)
-> [(Name, InfixOp)] -> Map Name InfixOp
forall a b. (a -> b) -> a -> b
$ ((Name, Int, Assoc, Maybe String) -> (Name, InfixOp))
-> [(Name, Int, Assoc, Maybe String)] -> [(Name, InfixOp)]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Int, Assoc, Maybe String) -> (Name, InfixOp)
forall a b.
(Name, a, b, Maybe String) -> (Name, (a, b, Doc -> Doc))
mkInfixOp [(Name, Int, Assoc, Maybe String)]
forall a. [(Name, Int, Assoc, Maybe a)]
infixTable

      destBinary :: Type -> Maybe (TypeOp, Type, Type)
destBinary Type
ty =
          case Type -> TypeData
Type.dest Type
ty of
            OpType TypeOp
t [Type
x,Type
y] -> (TypeOp, Type, Type) -> Maybe (TypeOp, Type, Type)
forall a. a -> Maybe a
Just (TypeOp
t,Type
x,Type
y)
            TypeData
_ -> Maybe (TypeOp, Type, Type)
forall a. Maybe a
Nothing

      destInfix :: Type -> Maybe (InfixOp,Type,Type)
      destInfix :: Type -> Maybe (InfixOp, Type, Type)
destInfix Type
ty = do
          (TypeOp
t,Type
x,Type
y) <- Type -> Maybe (TypeOp, Type, Type)
destBinary Type
ty
          InfixOp
i <- Name -> Maybe InfixOp
lookupOp (TypeOp -> Name
TypeOp.name TypeOp
t)
          (InfixOp, Type, Type) -> Maybe (InfixOp, Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (InfixOp
i,Type
x,Type
y)
        where
          lookupOp :: Name -> Maybe InfixOp
lookupOp Name
n = Name -> Map Name InfixOp -> Maybe InfixOp
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name InfixOp
infixOps

      isInfix :: Type -> Bool
isInfix = Maybe (InfixOp, Type, Type) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (InfixOp, Type, Type) -> Bool)
-> (Type -> Maybe (InfixOp, Type, Type)) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (InfixOp, Type, Type)
destInfix

instance Printable TypeSubst where
  toDoc :: TypeSubst -> Doc
toDoc = [Doc] -> Doc
forall a. Printable a => a -> Doc
toDoc ([Doc] -> Doc) -> (TypeSubst -> [Doc]) -> TypeSubst -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TypeVar, Type) -> Doc) -> [(TypeVar, Type)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (TypeVar, Type) -> Doc
forall a b. (Printable a, Printable b) => (a, b) -> Doc
mk ([(TypeVar, Type)] -> [Doc])
-> (TypeSubst -> [(TypeVar, Type)]) -> TypeSubst -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map TypeVar Type -> [(TypeVar, Type)]
forall k a. Map k a -> [(k, a)]
Map.toAscList (Map TypeVar Type -> [(TypeVar, Type)])
-> (TypeSubst -> Map TypeVar Type)
-> TypeSubst
-> [(TypeVar, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubst -> Map TypeVar Type
TypeSubst.dest
    where
      mk :: (a, a) -> Doc
mk (a
v,a
ty) = a -> Doc
forall a. Printable a => a -> Doc
toDoc a
v Doc -> Doc -> Doc
<+> String -> Doc
PP.text String
"|->" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Printable a => a -> Doc
toDoc a
ty

-------------------------------------------------------------------------------
-- Terms
-------------------------------------------------------------------------------

instance Printable Const where
  toDoc :: Const -> Doc
toDoc = Name -> Doc
ppSymbolName (Name -> Doc) -> (Const -> Name) -> Const -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> Name
Const.name

instance Printable Var where
  toDoc :: Var -> Doc
toDoc = Name -> Doc
forall a. Printable a => a -> Doc
toDoc (Name -> Doc) -> (Var -> Name) -> Var -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Name
Var.name

instance Printable Term where
  toDoc :: Term -> Doc
toDoc =
      Term -> Doc
normal
    where
      atom :: Term -> Doc
atom Term
tm =
          case Term -> TermData
Term.dest Term
tm of
            VarTerm Var
v -> Var -> Doc
forall a. Printable a => a -> Doc
toDoc Var
v
            ConstTerm Const
c Type
_ -> Const -> Doc
forall a. Printable a => a -> Doc
toDoc Const
c
            TermData
_ -> Term -> Doc
parens Term
tm

      comprehension :: Term -> Doc
comprehension Term
tm =
          case Term -> Maybe ([Var], Term, Term)
destComprehension Term
tm of
            Just ([Var]
v,Term
pat,Term
prd) ->
                [Doc] -> Doc -> Doc -> Doc
ppComprehension ((Var -> Doc) -> [Var] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Doc
forall a. Printable a => a -> Doc
toDoc [Var]
v) (Term -> Doc
normal Term
pat) (Term -> Doc
normal Term
prd)
            Maybe ([Var], Term, Term)
Nothing -> Term -> Doc
atom Term
tm

      pair :: Term -> Doc
pair Term
tm =
          case Term -> ([Term], Term)
stripPair Term
tm of
            ([],Term
_) -> Term -> Doc
comprehension Term
tm
            ([Term]
xs,Term
y) -> [Doc] -> Doc
ppPair ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Term -> Doc
negation Bool
False) [Term]
xs [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Bool -> Term -> Doc
negation Bool
True Term
y])

      basic :: Term -> Doc
basic Term
tm =
          case Term -> Maybe Integer
destNumeral Term
tm of
            Just Integer
i -> Integer -> Doc
PP.integer Integer
i
            Maybe Integer
Nothing -> Term -> Doc
pair Term
tm

      application :: Term -> Doc
application Term
tm =
          case Term -> (Term, [Term])
stripGenApp Term
tm of
            (Term
_,[]) -> Term -> Doc
basic Term
tm
            (Term
f,[Term]
xs) -> Term -> Doc
basic Term
f Doc -> Doc -> Doc
<+> [Doc] -> Doc
PP.sep ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
basic [Term]
xs)

      binder :: Bool -> Term -> Doc
binder Bool
rightmost Term
tm =
          case Term -> Maybe (Doc -> Doc, [Term], Term)
destBinder Term
tm of
            Just (Doc -> Doc
b,[Term]
v,Term
t) ->
                if Bool
rightmost then (Doc -> Doc) -> [Doc] -> Doc -> Doc
ppBinder Doc -> Doc
b ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
basic [Term]
v) (Term -> Doc
normal Term
t)
                else Term -> Doc
parens Term
tm
            Maybe (Doc -> Doc, [Term], Term)
Nothing -> Term -> Doc
application Term
tm

      negation :: Bool -> Term -> Doc
negation Bool
rightmost Term
tm =
          case Term -> ([Doc -> Doc], Term)
stripNegation Term
tm of
            ([],Term
_) -> Bool -> Term -> Doc
binder Bool
rightmost Term
tm
            ([Doc -> Doc]
ns,Term
t) -> [Doc -> Doc] -> Doc -> Doc
ppPrefixOps [Doc -> Doc]
ns (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Bool -> Term -> Doc
binder Bool
rightmost Term
t

      infixTerm :: Bool -> Term -> Doc
infixTerm = (Term -> Maybe (InfixOp, Term, Term))
-> (Bool -> Term -> Doc) -> Bool -> Term -> Doc
forall a.
(a -> Maybe (InfixOp, a, a))
-> (Bool -> a -> Doc) -> Bool -> a -> Doc
ppInfixOps Term -> Maybe (InfixOp, Term, Term)
destInfix Bool -> Term -> Doc
negation

      conditional :: Bool -> Term -> Doc
conditional Bool
rightmost Term
tm =
          case Term -> ([(Term, Term)], Term)
stripCond Term
tm of
            ([],Term
_) -> Bool -> Term -> Doc
infixTerm Bool
rightmost Term
tm
            ((Term
c,Term
t) : [(Term, Term)]
cts, Term
e) -> (Term -> Doc)
-> (Term -> Doc) -> Term -> Term -> [(Term, Term)] -> Term -> Doc
ppCond (Bool -> Term -> Doc
infixTerm Bool
False)
                                  (Bool -> Term -> Doc
infixTerm Bool
rightmost) Term
c Term
t [(Term, Term)]
cts Term
e

      letTerm :: Bool -> Term -> Doc
letTerm Bool
rightmost Term
tm =
          case Term -> ([(Term, Term)], Term)
stripLet Term
tm of
            ([],Term
_) -> Bool -> Term -> Doc
conditional Bool
rightmost Term
tm
            ([(Term, Term)]
ves,Term
t) -> (Term -> Doc)
-> (Term -> Doc) -> (Term -> Doc) -> [(Term, Term)] -> Term -> Doc
ppLet Term -> Doc
application (Bool -> Term -> Doc
conditional Bool
False)
                         (Bool -> Term -> Doc
conditional Bool
rightmost) [(Term, Term)]
ves Term
t

      normal :: Term -> Doc
normal = Bool -> Term -> Doc
letTerm Bool
True

      parens :: Term -> Doc
parens = Doc -> Doc
PP.parens (Doc -> Doc) -> (Term -> Doc) -> Term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Doc
normal

      -------------------------------------------------------------------------
      -- These grammar tables control term printing
      -------------------------------------------------------------------------

      infixTable :: [(Name, Prec, Assoc, Maybe String)]
      infixTable :: [(Name, Int, Assoc, Maybe String)]
infixTable =
          [--
           -- Booleans
           (Name
Const.conjName, -Int
1, Assoc
RightAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.disjName, -Int
2, Assoc
RightAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.impName, -Int
3, Assoc
RightAssoc, Maybe String
forall a. Maybe a
Nothing),
           --
           -- Functions
           (Name
Const.composeName, Int
4, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.funpowName, Int
9, Assoc
RightAssoc, Maybe String
forall a. Maybe a
Nothing),
           --
           -- Natural numbers
           (Name
Const.powerName, Int
9, Assoc
RightAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.multName, Int
8, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.divName, Int
7, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.modName, Int
7, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.addName, Int
6, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.subName, Int
6, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.leName, Int
3, Assoc
NonAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.ltName, Int
3, Assoc
NonAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.geName, Int
3, Assoc
NonAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.gtName, Int
3, Assoc
NonAssoc, Maybe String
forall a. Maybe a
Nothing),
           --
           -- Set theory
           (Name
Const.crossName, Int
7, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.intersectName, Int
7, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.differenceName, Int
6, Assoc
LeftAssoc, String -> Maybe String
forall a. a -> Maybe a
Just String
"-"),
           (Name
Const.unionName, Int
6, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.insertName, Int
6, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.deleteName, Int
6, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.memberName, Int
3, Assoc
NonAssoc, String -> Maybe String
forall a. a -> Maybe a
Just String
"in"),
           (Name
Const.subsetName, Int
3, Assoc
NonAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.properSubsetName, Int
3, Assoc
NonAssoc, Maybe String
forall a. Maybe a
Nothing),
           --
           --  List theory
           (Name
Const.appendName, Int
5, Assoc
RightAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.consName, Int
5, Assoc
RightAssoc, Maybe String
forall a. Maybe a
Nothing),
           --
           -- Real numbers
           (Name
Const.powerRealName, Int
9, Assoc
RightAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.multRealName, Int
8, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.divRealName, Int
8, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.addRealName, Int
6, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.subRealName, Int
6, Assoc
LeftAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.leRealName, Int
3, Assoc
NonAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.ltRealName, Int
3, Assoc
NonAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.geRealName, Int
3, Assoc
NonAssoc, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.gtRealName, Int
3, Assoc
NonAssoc, Maybe String
forall a. Maybe a
Nothing)]

      quantifierTable :: [(Name, Maybe String)]
      quantifierTable :: [(Name, Maybe String)]
quantifierTable =
          [(Name
Const.selectName, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.forallName, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.existsName, Maybe String
forall a. Maybe a
Nothing),
           (Name
Const.existsUniqueName, Maybe String
forall a. Maybe a
Nothing)]

      negationTable :: [(Name, Maybe String)]
      negationTable :: [(Name, Maybe String)]
negationTable =
          [(Name
Const.negName, Maybe String
forall a. Maybe a
Nothing)]

      -------------------------------------------------------------------------
      -- Operators of a given arity
      -------------------------------------------------------------------------

      destUnaryOp :: Term -> Maybe (Const,Term)
      destUnaryOp :: Term -> Maybe (Const, Term)
destUnaryOp Term
tm = do
          (Term
t,Term
x) <- Term -> Maybe (Term, Term)
Term.destApp Term
tm
          (Const
c,Type
_) <- Term -> Maybe (Const, Type)
Term.destConst Term
t
          (Const, Term) -> Maybe (Const, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Const
c,Term
x)

      destBinaryOp :: Term -> Maybe (Const,Term,Term)
      destBinaryOp :: Term -> Maybe (Const, Term, Term)
destBinaryOp Term
tm = do
          (Term
t,Term
y) <- Term -> Maybe (Term, Term)
Term.destApp Term
tm
          (Const
c,Term
x) <- Term -> Maybe (Const, Term)
destUnaryOp Term
t
          (Const, Term, Term) -> Maybe (Const, Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Const
c,Term
x,Term
y)

      destTernaryOp :: Term -> Maybe (Const,Term,Term,Term)
      destTernaryOp :: Term -> Maybe (Const, Term, Term, Term)
destTernaryOp Term
tm = do
          (Term
t,Term
z) <- Term -> Maybe (Term, Term)
Term.destApp Term
tm
          (Const
c,Term
x,Term
y) <- Term -> Maybe (Const, Term, Term)
destBinaryOp Term
t
          (Const, Term, Term, Term) -> Maybe (Const, Term, Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Const
c,Term
x,Term
y,Term
z)

      -------------------------------------------------------------------------
      -- Infix operators
      -------------------------------------------------------------------------

      nameOp :: Name -> Maybe String -> String
      nameOp :: Name -> Maybe String -> String
nameOp Name
n Maybe String
x =
          case Maybe String
x of
            Just String
y -> String
y
            Maybe String
Nothing -> let Name Namespace
_ String
y = Name
n in String
y

      mkInfixOp :: (Name, Prec, Assoc, Maybe String) -> (Name,InfixOp)
      mkInfixOp :: (Name, Int, Assoc, Maybe String) -> (Name, InfixOp)
mkInfixOp (Name
n,Int
p,Assoc
a,Maybe String
x) =
          (Name
n, (Int
p, Assoc
a, (Doc -> Doc -> Doc) -> Doc -> Doc -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Doc -> Doc -> Doc
(<+>) Doc
d))
        where
          s :: String
s = Name -> Maybe String -> String
nameOp Name
n Maybe String
x
          t :: Doc
t = String -> Doc
PP.text String
s
          d :: Doc
d = if String -> Bool
isSymbolString String
s then Doc
t else Char -> Doc
PP.char Char
'`' Doc -> Doc -> Doc
<> Doc
t Doc -> Doc -> Doc
<> Char -> Doc
PP.char Char
'`'

      eqInfixOp :: InfixOp
      eqInfixOp :: InfixOp
eqInfixOp = (Name, InfixOp) -> InfixOp
forall a b. (a, b) -> b
snd ((Name, InfixOp) -> InfixOp) -> (Name, InfixOp) -> InfixOp
forall a b. (a -> b) -> a -> b
$ (Name, Int, Assoc, Maybe String) -> (Name, InfixOp)
mkInfixOp (Name
Const.eqName, Int
3, Assoc
NonAssoc, Maybe String
forall a. Maybe a
Nothing)

      iffInfixOp :: InfixOp
      iffInfixOp :: InfixOp
iffInfixOp = (Name, InfixOp) -> InfixOp
forall a b. (a, b) -> b
snd ((Name, InfixOp) -> InfixOp) -> (Name, InfixOp) -> InfixOp
forall a b. (a -> b) -> a -> b
$ (Name, Int, Assoc, Maybe String) -> (Name, InfixOp)
mkInfixOp (Name
Const.eqName, -Int
4, Assoc
NonAssoc, String -> Maybe String
forall a. a -> Maybe a
Just String
"<=>")

      infixOps :: Map Name InfixOp
      infixOps :: Map Name InfixOp
infixOps = [(Name, InfixOp)] -> Map Name InfixOp
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, InfixOp)] -> Map Name InfixOp)
-> [(Name, InfixOp)] -> Map Name InfixOp
forall a b. (a -> b) -> a -> b
$ ((Name, Int, Assoc, Maybe String) -> (Name, InfixOp))
-> [(Name, Int, Assoc, Maybe String)] -> [(Name, InfixOp)]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Int, Assoc, Maybe String) -> (Name, InfixOp)
mkInfixOp [(Name, Int, Assoc, Maybe String)]
infixTable

      destInfix :: Term -> Maybe (InfixOp,Term,Term)
      destInfix :: Term -> Maybe (InfixOp, Term, Term)
destInfix Term
tm = do
          (Const
c,Term
x,Term
y) <- Term -> Maybe (Const, Term, Term)
destBinaryOp Term
tm
          InfixOp
i <- Type -> Name -> Maybe InfixOp
lookupOp (Term -> Type
Term.typeOf Term
x) (Const -> Name
Const.name Const
c)
          (InfixOp, Term, Term) -> Maybe (InfixOp, Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (InfixOp
i,Term
x,Term
y)
        where
          lookupOp :: Type -> Name -> Maybe InfixOp
lookupOp Type
ty Name
n =
              if Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
Const.eqName then Name -> Map Name InfixOp -> Maybe InfixOp
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name InfixOp
infixOps
              else if Type -> Bool
Type.isBool Type
ty then InfixOp -> Maybe InfixOp
forall a. a -> Maybe a
Just InfixOp
iffInfixOp
              else InfixOp -> Maybe InfixOp
forall a. a -> Maybe a
Just InfixOp
eqInfixOp

      isInfix :: Term -> Bool
      isInfix :: Term -> Bool
isInfix = Maybe (InfixOp, Term, Term) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (InfixOp, Term, Term) -> Bool)
-> (Term -> Maybe (InfixOp, Term, Term)) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe (InfixOp, Term, Term)
destInfix

      -------------------------------------------------------------------------
      -- Prefix operators
      -------------------------------------------------------------------------

      mkPrefixOp :: (Name, Maybe String) -> (Name,PrefixOp)
      mkPrefixOp :: (Name, Maybe String) -> (Name, Doc -> Doc)
mkPrefixOp (Name
n,Maybe String
x) =
          (Name
n, Doc -> Doc -> Doc
attach (Doc -> Doc -> Doc) -> Doc -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
PP.text String
s)
        where
          s :: String
s = Name -> Maybe String -> String
nameOp Name
n Maybe String
x
          attach :: Doc -> Doc -> Doc
attach = case String -> String
forall a. [a] -> [a]
reverse String
s of
                     Char
c : String
_ | Char -> Bool
isSymbolChar Char
c -> Doc -> Doc -> Doc
(<>)
                     String
_ -> Doc -> Doc -> Doc
(<+>)

      -------------------------------------------------------------------------
      -- Generalized lambda abstractions
      -------------------------------------------------------------------------

      destForall :: Term -> Maybe (Var,Term)
      destForall :: Term -> Maybe (Var, Term)
destForall Term
tm = do
          (Const
c,Term
t) <- Term -> Maybe (Const, Term)
destUnaryOp Term
tm
          (Var
v,Term
b) <- Term -> Maybe (Var, Term)
Term.destAbs Term
t
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Const -> Name
Const.name Const
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
Const.forallName)
          (Var, Term) -> Maybe (Var, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
v,Term
b)

      stripForall :: Term -> ([Var],Term)
      stripForall :: Term -> ([Var], Term)
stripForall Term
tm =
          case Term -> Maybe (Var, Term)
destForall Term
tm of
            Just (Var
v,Term
t) -> (Var
v Var -> [Var] -> [Var]
forall a. a -> [a] -> [a]
: [Var]
vs, Term
b) where ([Var]
vs,Term
b) = Term -> ([Var], Term)
stripForall Term
t
            Maybe (Var, Term)
Nothing -> ([],Term
tm)

      destAbs :: Term -> Maybe (Term,Term)
      destAbs :: Term -> Maybe (Term, Term)
destAbs Term
tm =
          case Term -> Maybe (Var, Term)
Term.destAbs Term
tm of
            Just (Var
v,Term
t) -> (Term, Term) -> Maybe (Term, Term)
forall a. a -> Maybe a
Just (Var -> Term
Term.mkVar Var
v, Term
t)
            Maybe (Var, Term)
Nothing -> do
              (Var
f,Term
t0) <- Term -> Maybe (Var, Term)
Term.destSelect Term
tm
              let ([Var]
vl,Term
t1) = Term -> ([Var], Term)
stripForall Term
t0
              Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Var -> [Var] -> Bool
forall a. HasFree a => Var -> a -> Bool
Var.notFreeIn Var
f [Var]
vl)
              (Term
t2,Term
body) <- Term -> Maybe (Term, Term)
Term.destEq Term
t1
              (Term
f',Term
pat) <- Term -> Maybe (Term, Term)
Term.destApp Term
t2
              Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Var -> Term -> Bool
Term.eqVar Var
f Term
f')
              Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Set Var -> [Var]
forall a. Set a -> [a]
Set.toAscList (Term -> Set Var
forall a. HasFree a => a -> Set Var
Var.free Term
pat) [Var] -> [Var] -> Bool
forall a. Eq a => a -> a -> Bool
== [Var]
vl)
              Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Var -> Term -> Bool
forall a. HasFree a => Var -> a -> Bool
Var.notFreeIn Var
f Term
body)
              (Term, Term) -> Maybe (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
pat,Term
body)

      lambda :: PrefixOp
      lambda :: Doc -> Doc
lambda = (Name, Doc -> Doc) -> Doc -> Doc
forall a b. (a, b) -> b
snd ((Name, Doc -> Doc) -> Doc -> Doc)
-> (Name, Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Name, Maybe String) -> (Name, Doc -> Doc)
mkPrefixOp (Name
forall a. HasCallStack => a
undefined, String -> Maybe String
forall a. a -> Maybe a
Just String
"\\")

      stripLambda :: Term -> Maybe (PrefixOp,[Term],Term)
      stripLambda :: Term -> Maybe (Doc -> Doc, [Term], Term)
stripLambda Term
tm = do
          (Term
v,Term
t) <- Term -> Maybe (Term, Term)
destAbs Term
tm
          let ([Term]
vs,Term
b) = Term -> ([Term], Term)
strip Term
t
          (Doc -> Doc, [Term], Term) -> Maybe (Doc -> Doc, [Term], Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Doc
lambda, Term
v Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
vs, Term
b)
        where
          strip :: Term -> ([Term], Term)
strip Term
t =
              case Term -> Maybe (Term, Term)
destAbs Term
t of
                Just (Term
v,Term
u) -> (Term
v Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
vs, Term
b) where ([Term]
vs,Term
b) = Term -> ([Term], Term)
strip Term
u
                Maybe (Term, Term)
Nothing -> ([],Term
t)

      -------------------------------------------------------------------------
      -- Quantifiers
      -------------------------------------------------------------------------

      quantifiers :: Map Name PrefixOp
      quantifiers :: Map Name (Doc -> Doc)
quantifiers = [(Name, Doc -> Doc)] -> Map Name (Doc -> Doc)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, Doc -> Doc)] -> Map Name (Doc -> Doc))
-> [(Name, Doc -> Doc)] -> Map Name (Doc -> Doc)
forall a b. (a -> b) -> a -> b
$ ((Name, Maybe String) -> (Name, Doc -> Doc))
-> [(Name, Maybe String)] -> [(Name, Doc -> Doc)]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Maybe String) -> (Name, Doc -> Doc)
mkPrefixOp [(Name, Maybe String)]
quantifierTable

      destQuantifier :: Term -> Maybe (Const,Term,Term)
      destQuantifier :: Term -> Maybe (Const, Term, Term)
destQuantifier Term
tm = do
          (Const
c,Term
vb) <- Term -> Maybe (Const, Term)
destUnaryOp Term
tm
          (Term
v,Term
b) <- Term -> Maybe (Term, Term)
destAbs Term
vb
          (Const, Term, Term) -> Maybe (Const, Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Const
c,Term
v,Term
b)

      stripQuantifier :: Term -> Maybe (PrefixOp,[Term],Term)
      stripQuantifier :: Term -> Maybe (Doc -> Doc, [Term], Term)
stripQuantifier Term
tm = do
          (Const
c,Term
v,Term
t) <- Term -> Maybe (Const, Term, Term)
destQuantifier Term
tm
          Doc -> Doc
q <- Name -> Map Name (Doc -> Doc) -> Maybe (Doc -> Doc)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Const -> Name
Const.name Const
c) Map Name (Doc -> Doc)
quantifiers
          let ([Term]
vs,Term
b) = Const -> Term -> ([Term], Term)
strip Const
c Term
t
          (Doc -> Doc, [Term], Term) -> Maybe (Doc -> Doc, [Term], Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Doc
q, Term
v Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
vs, Term
b)
        where
          strip :: Const -> Term -> ([Term], Term)
strip Const
c Term
t =
              case Term -> Maybe (Const, Term, Term)
destQuantifier Term
t of
                Just (Const
c',Term
v,Term
u) | Const
c' Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
c -> (Term
v Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
vs, Term
b) where ([Term]
vs,Term
b) = Const -> Term -> ([Term], Term)
strip Const
c Term
u
                Maybe (Const, Term, Term)
_ -> ([],Term
t)

      -------------------------------------------------------------------------
      -- Binders
      -------------------------------------------------------------------------

      destBinder :: Term -> Maybe (PrefixOp,[Term],Term)
      destBinder :: Term -> Maybe (Doc -> Doc, [Term], Term)
destBinder Term
tm =
          case Term -> Maybe (Doc -> Doc, [Term], Term)
stripLambda Term
tm of
            Just (Doc -> Doc, [Term], Term)
b -> (Doc -> Doc, [Term], Term) -> Maybe (Doc -> Doc, [Term], Term)
forall a. a -> Maybe a
Just (Doc -> Doc, [Term], Term)
b
            Maybe (Doc -> Doc, [Term], Term)
Nothing -> Term -> Maybe (Doc -> Doc, [Term], Term)
stripQuantifier Term
tm

      isBinder :: Term -> Bool
      isBinder :: Term -> Bool
isBinder = Maybe (Doc -> Doc, [Term], Term) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Doc -> Doc, [Term], Term) -> Bool)
-> (Term -> Maybe (Doc -> Doc, [Term], Term)) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe (Doc -> Doc, [Term], Term)
destBinder

      ppBoundVars :: [PP.Doc] -> PP.Doc
      ppBoundVars :: [Doc] -> Doc
ppBoundVars =
          \[Doc]
v -> [Doc] -> Doc
PP.fsep [Doc]
v Doc -> Doc -> Doc
<> Doc
dot
        where
          dot :: Doc
dot = Char -> Doc
PP.char Char
'.'

      ppBinder :: PrefixOp -> [PP.Doc] -> PP.Doc -> PP.Doc
      ppBinder :: (Doc -> Doc) -> [Doc] -> Doc -> Doc
ppBinder Doc -> Doc
b [Doc]
v Doc
t = Doc -> Doc
b (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
PP.sep [[Doc] -> Doc
ppBoundVars [Doc]
v, Doc
t]

      -------------------------------------------------------------------------
      -- Negation operators
      -------------------------------------------------------------------------

      negations :: Map Name PrefixOp
      negations :: Map Name (Doc -> Doc)
negations = [(Name, Doc -> Doc)] -> Map Name (Doc -> Doc)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, Doc -> Doc)] -> Map Name (Doc -> Doc))
-> [(Name, Doc -> Doc)] -> Map Name (Doc -> Doc)
forall a b. (a -> b) -> a -> b
$ ((Name, Maybe String) -> (Name, Doc -> Doc))
-> [(Name, Maybe String)] -> [(Name, Doc -> Doc)]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Maybe String) -> (Name, Doc -> Doc)
mkPrefixOp [(Name, Maybe String)]
negationTable

      destNegation :: Term -> Maybe (PrefixOp,Term)
      destNegation :: Term -> Maybe (Doc -> Doc, Term)
destNegation Term
tm = do
          (Const
c,Term
t) <- Term -> Maybe (Const, Term)
destUnaryOp Term
tm
          Doc -> Doc
p <- Name -> Map Name (Doc -> Doc) -> Maybe (Doc -> Doc)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Const -> Name
Const.name Const
c) Map Name (Doc -> Doc)
negations
          (Doc -> Doc, Term) -> Maybe (Doc -> Doc, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> Doc
p,Term
t)

      isNegation :: Term -> Bool
      isNegation :: Term -> Bool
isNegation = Maybe (Doc -> Doc, Term) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Doc -> Doc, Term) -> Bool)
-> (Term -> Maybe (Doc -> Doc, Term)) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe (Doc -> Doc, Term)
destNegation

      stripNegation :: Term -> ([PrefixOp],Term)
      stripNegation :: Term -> ([Doc -> Doc], Term)
stripNegation Term
tm =
          case Term -> Maybe (Doc -> Doc, Term)
destNegation Term
tm of
            Just (Doc -> Doc
n,Term
t) -> (Doc -> Doc
n (Doc -> Doc) -> [Doc -> Doc] -> [Doc -> Doc]
forall a. a -> [a] -> [a]
: [Doc -> Doc]
ns, Term
b) where ([Doc -> Doc]
ns,Term
b) = Term -> ([Doc -> Doc], Term)
stripNegation Term
t
            Maybe (Doc -> Doc, Term)
Nothing -> ([],Term
tm)

      -------------------------------------------------------------------------
      -- Conditionals
      -------------------------------------------------------------------------

      destCond :: Term -> Maybe (Term,Term,Term)
      destCond :: Term -> Maybe (Term, Term, Term)
destCond Term
tm = do
          (Const
c,Term
x,Term
y,Term
z) <- Term -> Maybe (Const, Term, Term, Term)
destTernaryOp Term
tm
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Const -> Name
Const.name Const
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
Const.condName)
          (Term, Term, Term) -> Maybe (Term, Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
x,Term
y,Term
z)

      isCond :: Term -> Bool
      isCond :: Term -> Bool
isCond = Maybe (Term, Term, Term) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Term, Term, Term) -> Bool)
-> (Term -> Maybe (Term, Term, Term)) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe (Term, Term, Term)
destCond

      stripCond :: Term -> ([(Term,Term)],Term)
      stripCond :: Term -> ([(Term, Term)], Term)
stripCond Term
tm =
          case Term -> Maybe (Term, Term, Term)
destCond Term
tm of
            Just (Term
c,Term
t,Term
u) -> ((Term
c,Term
t) (Term, Term) -> [(Term, Term)] -> [(Term, Term)]
forall a. a -> [a] -> [a]
: [(Term, Term)]
cts, Term
e) where ([(Term, Term)]
cts,Term
e) = Term -> ([(Term, Term)], Term)
stripCond Term
u
            Maybe (Term, Term, Term)
Nothing -> ([],Term
tm)

      ppCond :: (Term -> PP.Doc) -> (Term -> PP.Doc) ->
                Term -> Term -> [(Term,Term)] -> Term -> PP.Doc
      ppCond :: (Term -> Doc)
-> (Term -> Doc) -> Term -> Term -> [(Term, Term)] -> Term -> Doc
ppCond Term -> Doc
pp Term -> Doc
ppe =
          \Term
c Term
t [(Term, Term)]
cts Term
e ->
            [Doc] -> Doc
PP.sep (Term -> Term -> Doc
ifThen Term
c Term
t Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: ((Term, Term) -> Doc) -> [(Term, Term)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term, Term) -> Doc
elseIfThen [(Term, Term)]
cts [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> Doc
elseBranch Term
e])
        where
          ifThen :: Term -> Term -> Doc
ifThen Term
c Term
t =
              String -> Doc
PP.text String
"if" Doc -> Doc -> Doc
<+> [Doc] -> Doc
PP.sep [Term -> Doc
pp Term
c, String -> Doc
PP.text String
"then" Doc -> Doc -> Doc
<+> Term -> Doc
pp Term
t]

          elseIfThen :: (Term, Term) -> Doc
elseIfThen (Term
c,Term
t) =
              String -> Doc
PP.text String
"else" Doc -> Doc -> Doc
<+> [Doc] -> Doc
PP.sep [String -> Doc
PP.text String
"if" Doc -> Doc -> Doc
<+> Term -> Doc
pp Term
c,
                                         String -> Doc
PP.text String
"then" Doc -> Doc -> Doc
<+> Term -> Doc
pp Term
t]

          elseBranch :: Term -> Doc
elseBranch Term
e = String -> Doc
PP.text String
"else" Doc -> Doc -> Doc
<+> Term -> Doc
ppe Term
e

      -------------------------------------------------------------------------
      -- Lets
      -------------------------------------------------------------------------

      destLet :: Term -> Maybe (Term,Term,Term)
      destLet :: Term -> Maybe (Term, Term, Term)
destLet Term
tm = do
          (Term
vt,Term
e) <- Term -> Maybe (Term, Term)
Term.destApp Term
tm
          (Term
v,Term
t) <- Term -> Maybe (Term, Term)
destAbs Term
vt
          (Term, Term, Term) -> Maybe (Term, Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v,Term
e,Term
t)

      isLet :: Term -> Bool
      isLet :: Term -> Bool
isLet = Maybe (Term, Term, Term) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Term, Term, Term) -> Bool)
-> (Term -> Maybe (Term, Term, Term)) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe (Term, Term, Term)
destLet

      stripLet :: Term -> ([(Term,Term)],Term)
      stripLet :: Term -> ([(Term, Term)], Term)
stripLet Term
tm =
          case Term -> Maybe (Term, Term, Term)
destLet Term
tm of
            Just (Term
v,Term
e,Term
u) -> ((Term
v,Term
e) (Term, Term) -> [(Term, Term)] -> [(Term, Term)]
forall a. a -> [a] -> [a]
: [(Term, Term)]
ves, Term
t) where ([(Term, Term)]
ves,Term
t) = Term -> ([(Term, Term)], Term)
stripLet Term
u
            Maybe (Term, Term, Term)
Nothing -> ([],Term
tm)

      ppLet :: (Term -> PP.Doc) -> (Term -> PP.Doc) -> (Term -> PP.Doc) ->
               [(Term,Term)] -> Term -> PP.Doc
      ppLet :: (Term -> Doc)
-> (Term -> Doc) -> (Term -> Doc) -> [(Term, Term)] -> Term -> Doc
ppLet Term -> Doc
ppv Term -> Doc
ppe Term -> Doc
pp =
          \[(Term, Term)]
ves Term
t ->
            [Doc] -> Doc
PP.sep (((Term, Term) -> Doc) -> [(Term, Term)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term, Term) -> Doc
letBind [(Term, Term)]
ves [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> Doc
pp Term
t])
        where
          letBind :: (Term, Term) -> Doc
letBind (Term
v,Term
e) =
              String -> Doc
PP.text String
"let" Doc -> Doc -> Doc
<+> [Doc] -> Doc
PP.sep [Term -> Doc
ppv Term
v Doc -> Doc -> Doc
<+> String -> Doc
PP.text String
"<-",
                                        Term -> Doc
ppe Term
e Doc -> Doc -> Doc
<+> String -> Doc
PP.text String
"in"]

      -------------------------------------------------------------------------
      -- Numerals
      -------------------------------------------------------------------------

      fromNaturals :: Set Name
      fromNaturals :: Set Name
fromNaturals = [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList
          [Name
Const.fromNaturalRealName]

      destFromNatural :: Term -> Maybe Term
      destFromNatural :: Term -> Maybe Term
destFromNatural Term
tm = do
          (Const
c,Term
t) <- Term -> Maybe (Const, Term)
destUnaryOp Term
tm
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Const -> Name
Const.name Const
c) Set Name
fromNaturals)
          Term -> Maybe Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

      destMaybeFromNatural :: Term -> Term
      destMaybeFromNatural :: Term -> Term
destMaybeFromNatural Term
tm =
          case Term -> Maybe Term
destFromNatural Term
tm of
            Just Term
t -> Term
t
            Maybe Term
Nothing -> Term
tm

      isZero :: Term -> Bool
      isZero :: Term -> Bool
isZero Term
tm =
          case Term -> Maybe (Const, Type)
Term.destConst Term
tm of
            Just (Const
c,Type
_) -> Const -> Name
Const.name Const
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
Const.zeroName
            Maybe (Const, Type)
Nothing -> Bool
False

      destBit :: Term -> Maybe (Bool,Term)
      destBit :: Term -> Maybe (Bool, Term)
destBit Term
tm = do
          (Const
c,Term
t) <- Term -> Maybe (Const, Term)
destUnaryOp Term
tm
          (Bool -> (Bool, Term)) -> Maybe Bool -> Maybe (Bool, Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bool -> Term -> (Bool, Term)) -> Term -> Bool -> (Bool, Term)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) Term
t) (Maybe Bool -> Maybe (Bool, Term))
-> Maybe Bool -> Maybe (Bool, Term)
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Bool
bit (Const -> Name
Const.name Const
c)
        where
          bit :: Name -> Maybe Bool
bit Name
n = if Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
Const.bit0Name then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                  else if Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
Const.bit1Name then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
                  else Maybe Bool
forall a. Maybe a
Nothing

      destBits :: Term -> Maybe Integer
      destBits :: Term -> Maybe Integer
destBits Term
tm =
          if Term -> Bool
isZero Term
tm then Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
          else do
            (Bool
b,Term
t) <- Term -> Maybe (Bool, Term)
destBit Term
tm
            Integer
i <- Term -> Maybe Integer
destNumeral Term
t
            Bool -> Integer -> Maybe Integer
forall a. (Eq a, Num a) => Bool -> a -> Maybe a
bit Bool
b Integer
i
        where
          bit :: Bool -> a -> Maybe a
bit Bool
False a
0 = Maybe a
forall a. Maybe a
Nothing
          bit Bool
b a
i = a -> Maybe a
forall a. a -> Maybe a
Just (a
2 a -> a -> a
forall a. Num a => a -> a -> a
* a
i a -> a -> a
forall a. Num a => a -> a -> a
+ (if Bool
b then a
1 else a
0))

      destNumeral :: Term -> Maybe Integer
      destNumeral :: Term -> Maybe Integer
destNumeral = Term -> Maybe Integer
destBits (Term -> Maybe Integer) -> (Term -> Term) -> Term -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
destMaybeFromNatural

      isNumeral :: Term -> Bool
      isNumeral :: Term -> Bool
isNumeral = Maybe Integer -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Integer -> Bool) -> (Term -> Maybe Integer) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe Integer
destNumeral

      -------------------------------------------------------------------------
      -- Pairs
      -------------------------------------------------------------------------

      destPair :: Term -> Maybe (Term,Term)
      destPair :: Term -> Maybe (Term, Term)
destPair Term
tm = do
          (Const
c,Term
x,Term
y) <- Term -> Maybe (Const, Term, Term)
destBinaryOp Term
tm
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Const -> Name
Const.name Const
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
Const.pairName)
          (Term, Term) -> Maybe (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
x,Term
y)

      isPair :: Term -> Bool
      isPair :: Term -> Bool
isPair = Maybe (Term, Term) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Term, Term) -> Bool)
-> (Term -> Maybe (Term, Term)) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe (Term, Term)
destPair

      stripPair :: Term -> ([Term],Term)
      stripPair :: Term -> ([Term], Term)
stripPair Term
tm =
          case Term -> Maybe (Term, Term)
destPair Term
tm of
            Just (Term
x,Term
t) -> (Term
x Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
xs, Term
y) where ([Term]
xs,Term
y) = Term -> ([Term], Term)
stripPair Term
t
            Maybe (Term, Term)
Nothing -> ([],Term
tm)

      ppPair :: [PP.Doc] -> PP.Doc
      ppPair :: [Doc] -> Doc
ppPair = Doc -> Doc
PP.parens (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
PP.fsep ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
PP.punctuate Doc
PP.comma

      -------------------------------------------------------------------------
      -- Set comprehensions
      -------------------------------------------------------------------------

      destFromPredicate :: Term -> Maybe Term
      destFromPredicate :: Term -> Maybe Term
destFromPredicate Term
tm = do
          (Const
c,Term
t) <- Term -> Maybe (Const, Term)
destUnaryOp Term
tm
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Const -> Name
Const.name Const
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
Const.fromPredicateName)
          Term -> Maybe Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

      destConj :: Term -> Maybe (Term,Term)
      destConj :: Term -> Maybe (Term, Term)
destConj Term
tm = do
          (Const
c,Term
x,Term
y) <- Term -> Maybe (Const, Term, Term)
destBinaryOp Term
tm
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Const -> Name
Const.name Const
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
Const.conjName)
          (Term, Term) -> Maybe (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
x,Term
y)

      destExists :: Term -> Maybe (Var,Term)
      destExists :: Term -> Maybe (Var, Term)
destExists Term
tm = do
          (Const
c,Term
t) <- Term -> Maybe (Const, Term)
destUnaryOp Term
tm
          (Var
v,Term
b) <- Term -> Maybe (Var, Term)
Term.destAbs Term
t
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Const -> Name
Const.name Const
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
Const.existsName)
          (Var, Term) -> Maybe (Var, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
v,Term
b)

      stripExists :: Term -> ([Var],Term)
      stripExists :: Term -> ([Var], Term)
stripExists Term
tm =
          case Term -> Maybe (Var, Term)
destExists Term
tm of
            Just (Var
v,Term
t) -> (Var
v Var -> [Var] -> [Var]
forall a. a -> [a] -> [a]
: [Var]
vs, Term
b) where ([Var]
vs,Term
b) = Term -> ([Var], Term)
stripExists Term
t
            Maybe (Var, Term)
Nothing -> ([],Term
tm)

      destComprehension :: Term -> Maybe ([Var],Term,Term)
      destComprehension :: Term -> Maybe ([Var], Term, Term)
destComprehension Term
tm = do
          Term
t0 <- Term -> Maybe Term
destFromPredicate Term
tm
          (Var
v,Term
t1) <- Term -> Maybe (Var, Term)
Term.destAbs Term
t0
          let ([Var]
vl,Term
t2) = Term -> ([Var], Term)
stripExists Term
t1
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not ([Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
vl))
          let vs :: Set Var
vs = [Var] -> Set Var
forall a. Ord a => [a] -> Set a
Set.fromList [Var]
vl
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([Var] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
vl Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Set Var -> Int
forall a. Set a -> Int
Set.size Set Var
vs)
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Var
v Set Var
vs)
          (Term
t3,Term
prd) <- Term -> Maybe (Term, Term)
destConj Term
t2
          (Term
v',Term
pat) <- Term -> Maybe (Term, Term)
Term.destEq Term
t3
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Var -> Term -> Bool
Term.eqVar Var
v Term
v')
          let fvs :: Set Var
fvs = Term -> Set Var
forall a. HasFree a => a -> Set Var
Var.free Term
pat
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Var
v Set Var
fvs)
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Var -> Term -> Bool
forall a. HasFree a => Var -> a -> Bool
Var.notFreeIn Var
v Term
prd)
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Set Var -> Set Var -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set Var
vs Set Var
fvs)
          ([Var], Term, Term) -> Maybe ([Var], Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Var]
vl,Term
pat,Term
prd)

      isComprehension :: Term -> Bool
      isComprehension :: Term -> Bool
isComprehension = Maybe ([Var], Term, Term) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe ([Var], Term, Term) -> Bool)
-> (Term -> Maybe ([Var], Term, Term)) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe ([Var], Term, Term)
destComprehension

      ppComprehension :: [PP.Doc] -> PP.Doc -> PP.Doc -> PP.Doc
      ppComprehension :: [Doc] -> Doc -> Doc -> Doc
ppComprehension [Doc]
v Doc
pat Doc
prd =
          Doc
PP.lbrace Doc -> Doc -> Doc
<+>
          [Doc] -> Doc
PP.sep [[Doc] -> Doc
PP.sep [[Doc] -> Doc
ppBoundVars [Doc]
v, Doc
pat Doc -> Doc -> Doc
<+> String -> Doc
PP.text String
"|"], Doc
prd] Doc -> Doc -> Doc
<+>
          Doc
PP.rbrace

      -------------------------------------------------------------------------
      -- Function application
      -------------------------------------------------------------------------

      destGenApp :: Term -> Maybe (Term,Term)
      destGenApp :: Term -> Maybe (Term, Term)
destGenApp Term
tm = do
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Term -> Bool
isNumeral Term
tm)
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Term -> Bool
isCond Term
tm)
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Term -> Bool
isPair Term
tm)
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Term -> Bool
isLet Term
tm)
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Term -> Bool
isComprehension Term
tm)
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Term -> Bool
isInfix Term
tm)
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Term -> Bool
isNegation Term
tm)
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Term -> Bool
isBinder Term
tm)
          --guard (not $ isCase tm)
          Term -> Maybe (Term, Term)
Term.destApp Term
tm

      stripGenApp :: Term -> (Term,[Term])
      stripGenApp :: Term -> (Term, [Term])
stripGenApp =
          [Term] -> Term -> (Term, [Term])
go []
        where
          go :: [Term] -> Term -> (Term, [Term])
go [Term]
xs Term
tm =
              case Term -> Maybe (Term, Term)
destGenApp Term
tm of
                Maybe (Term, Term)
Nothing -> (Term
tm,[Term]
xs)
                Just (Term
f,Term
x) -> [Term] -> Term -> (Term, [Term])
go (Term
x Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
xs) Term
f

instance Printable TermAlpha where
  toDoc :: TermAlpha -> Doc
toDoc = Term -> Doc
forall a. Printable a => a -> Doc
toDoc (Term -> Doc) -> (TermAlpha -> Term) -> TermAlpha -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermAlpha -> Term
TermAlpha.dest

-------------------------------------------------------------------------------
-- Theorems
-------------------------------------------------------------------------------

instance Printable Sequent where
  toDoc :: Sequent -> Doc
toDoc Sequent
sq =
      [Doc] -> Doc
PP.sep [Doc
hd, String -> Doc
PP.text String
"|-" Doc -> Doc -> Doc
<+> TermAlpha -> Doc
forall a. Printable a => a -> Doc
toDoc TermAlpha
c]
    where
      (Set TermAlpha
h,TermAlpha
c) = Sequent -> (Set TermAlpha, TermAlpha)
Sequent.dest Sequent
sq
      hd :: Doc
hd = if Set TermAlpha -> Bool
forall a. Set a -> Bool
Set.null Set TermAlpha
h then Doc
PP.empty else Set TermAlpha -> Doc
forall a. Printable a => a -> Doc
toDoc Set TermAlpha
h

instance Printable Thm where
  toDoc :: Thm -> Doc
toDoc = Sequent -> Doc
forall a. Printable a => a -> Doc
toDoc (Sequent -> Doc) -> (Thm -> Sequent) -> Thm -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thm -> Sequent
Thm.dest