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
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)
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)
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
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
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]))
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
infixTable :: [(Name, Int, Assoc, Maybe a)]
infixTable =
[
(Name
TypeOp.funName, Int
1, Assoc
RightAssoc, Maybe a
forall a. Maybe a
Nothing),
(Name
TypeOp.productName, Int
3, Assoc
RightAssoc, Maybe a
forall a. Maybe a
Nothing),
(Name
TypeOp.sumName, Int
2, Assoc
RightAssoc, Maybe a
forall a. Maybe a
Nothing)]
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
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
infixTable :: [(Name, Prec, Assoc, Maybe String)]
infixTable :: [(Name, Int, Assoc, Maybe String)]
infixTable =
[
(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),
(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),
(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),
(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),
(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),
(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)]
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)
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
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
(<+>)
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 :: 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)
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]
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)
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
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"]
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
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
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
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)
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
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