-- Formulae, inputs, terms and so on.
--
-- "Show" instances for several of these types are found in TPTP.Print.

{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, Rank2Types, GADTs, TypeOperators, ScopedTypeVariables, BangPatterns, PatternGuards, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
module Jukebox.Form where

import Prelude hiding (sequence, mapM)
import qualified Data.Set as Set
import Data.Set(Set)
import qualified Data.Map.Strict as Map
import Data.Map(Map)
import Data.Ord
import Jukebox.Name
import Control.Monad
import Control.Monad.Trans.Class
import Control.Monad.Trans.State.Strict
import Data.List
import Jukebox.Utils
import Data.Typeable(Typeable)
import Data.Monoid
import qualified Data.DList as DList
import Data.DList(DList)
import Data.MemoUgly

-- Set to True to switch on some sanity checks
debugging :: Bool
debugging :: Bool
debugging = Bool
False

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

data Type =
    O
  | Type { Type -> Name
tname :: !Name }
  deriving Typeable

indType, intType, ratType, realType :: Type
indType :: Type
indType = Name -> Type
Type ([Char] -> Name
forall a. Named a => a -> Name
name [Char]
"$i")
intType :: Type
intType = Name -> Type
Type ([Char] -> Name
forall a. Named a => a -> Name
name [Char]
"$int")
ratType :: Type
ratType = Name -> Type
Type ([Char] -> Name
forall a. Named a => a -> Name
name [Char]
"$rat")
realType :: Type
realType = Name -> Type
Type ([Char] -> Name
forall a. Named a => a -> Name
name [Char]
"$real")

data FunType = FunType { FunType -> [Type]
args :: [Type], FunType -> Type
res :: Type } deriving (FunType -> FunType -> Bool
(FunType -> FunType -> Bool)
-> (FunType -> FunType -> Bool) -> Eq FunType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FunType -> FunType -> Bool
$c/= :: FunType -> FunType -> Bool
== :: FunType -> FunType -> Bool
$c== :: FunType -> FunType -> Bool
Eq, Eq FunType
Eq FunType
-> (FunType -> FunType -> Ordering)
-> (FunType -> FunType -> Bool)
-> (FunType -> FunType -> Bool)
-> (FunType -> FunType -> Bool)
-> (FunType -> FunType -> Bool)
-> (FunType -> FunType -> FunType)
-> (FunType -> FunType -> FunType)
-> Ord FunType
FunType -> FunType -> Bool
FunType -> FunType -> Ordering
FunType -> FunType -> FunType
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 :: FunType -> FunType -> FunType
$cmin :: FunType -> FunType -> FunType
max :: FunType -> FunType -> FunType
$cmax :: FunType -> FunType -> FunType
>= :: FunType -> FunType -> Bool
$c>= :: FunType -> FunType -> Bool
> :: FunType -> FunType -> Bool
$c> :: FunType -> FunType -> Bool
<= :: FunType -> FunType -> Bool
$c<= :: FunType -> FunType -> Bool
< :: FunType -> FunType -> Bool
$c< :: FunType -> FunType -> Bool
compare :: FunType -> FunType -> Ordering
$ccompare :: FunType -> FunType -> Ordering
$cp1Ord :: Eq FunType
Ord, Typeable)

-- Helper function for defining (Eq, Ord) instances
typeMaybeName :: Type -> Maybe Name
typeMaybeName :: Type -> Maybe Name
typeMaybeName Type
O = Maybe Name
forall a. Maybe a
Nothing
typeMaybeName Type{tname :: Type -> Name
tname = Name
t} = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
t

instance Eq Type where
  Type
t1 == :: Type -> Type -> Bool
== Type
t2 = Type -> Maybe Name
typeMaybeName Type
t1 Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== Type -> Maybe Name
typeMaybeName Type
t2

instance Ord Type where
  compare :: Type -> Type -> Ordering
compare = (Type -> Maybe Name) -> Type -> Type -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Type -> Maybe Name
typeMaybeName

instance Named Type where
  name :: Type -> Name
name Type
O = [Char] -> Name
forall a. Named a => a -> Name
name [Char]
"$o"
  name Type{tname :: Type -> Name
tname = Name
t} = Name
t

-- Typeclass of "things that have a type"
class Typed a where
  typ :: a -> Type

instance Typed Type where
  typ :: Type -> Type
typ = Type -> Type
forall a. a -> a
id

instance Typed FunType where
  typ :: FunType -> Type
typ = FunType -> Type
res

instance Typed b => Typed (a ::: b) where
  typ :: (a ::: b) -> Type
typ (a
_ ::: b
t) = b -> Type
forall a. Typed a => a -> Type
typ b
t

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

type Variable = Name ::: Type
type Function = Name ::: FunType
data Term = Var Variable | Function :@: [Term] deriving (Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq, Eq Term
Eq Term
-> (Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
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 :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
$cp1Ord :: Eq Term
Ord)

instance Named Term where
  name :: Term -> Name
name (Var Variable
x) = Variable -> Name
forall a. Named a => a -> Name
name Variable
x
  name (Function
f :@: [Term]
_) = Function -> Name
forall a. Named a => a -> Name
name Function
f

instance Typed Term where
  typ :: Term -> Type
typ (Var Variable
x) = Variable -> Type
forall a. Typed a => a -> Type
typ Variable
x
  typ (Function
f :@: [Term]
_) = Function -> Type
forall a. Typed a => a -> Type
typ Function
f

newSymbol :: Named a => a -> b -> NameM (Name ::: b)
newSymbol :: a -> b -> NameM (Name ::: b)
newSymbol a
x b
ty = (Name -> Name ::: b) -> NameM Name -> NameM (Name ::: b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> b -> Name ::: b
forall a b. a -> b -> a ::: b
::: b
ty) (a -> NameM Name
forall a. Named a => a -> NameM Name
newName a
x)

newFunction :: Named a => a -> [Type] -> Type -> NameM Function
newFunction :: a -> [Type] -> Type -> NameM Function
newFunction a
x [Type]
args Type
res = a -> FunType -> NameM Function
forall a b. Named a => a -> b -> NameM (Name ::: b)
newSymbol a
x ([Type] -> Type -> FunType
FunType [Type]
args Type
res)

newType :: Named a => a -> NameM Type
newType :: a -> NameM Type
newType a
x = Name -> Type
Type (Name -> Type) -> NameM Name -> NameM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> NameM Name
forall a. Named a => a -> NameM Name
newName a
x

funArgs :: Function -> [Type]
funArgs :: Function -> [Type]
funArgs (Name
_ ::: FunType
ty) = FunType -> [Type]
args FunType
ty

arity :: Function -> Int
arity :: Function -> Int
arity = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Type] -> Int) -> (Function -> [Type]) -> Function -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Function -> [Type]
funArgs

size :: Term -> Int
size :: Term -> Int
size Var{} = Int
1
size (Function
_f :@: [Term]
xs) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Term -> Int) -> [Term] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Int
size [Term]
xs)

subterms :: Term -> [Term]
subterms :: Term -> [Term]
subterms Term
t =
  Term
tTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:
  case Term
t of
    Var Variable
_ -> []
    Function
_f :@: [Term]
ts -> (Term -> [Term]) -> [Term] -> [Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Term -> [Term]
subterms [Term]
ts

contexts :: Term -> [(Term, Term -> Term)]
contexts :: Term -> [(Term, Term -> Term)]
contexts Term
t = Term -> (Term -> Term) -> [(Term, Term -> Term)]
ctxs Term
t Term -> Term
forall a. a -> a
id
  where
    ctxs :: Term -> (Term -> Term) -> [(Term, Term -> Term)]
    ctxs :: Term -> (Term -> Term) -> [(Term, Term -> Term)]
ctxs Term
t Term -> Term
k =
      (Term
t, Term -> Term
k)(Term, Term -> Term)
-> [(Term, Term -> Term)] -> [(Term, Term -> Term)]
forall a. a -> [a] -> [a]
:
      case Term
t of
        Var Variable
_ -> []
        Function
f :@: [Term]
ts ->
          [[(Term, Term -> Term)]] -> [(Term, Term -> Term)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ Term -> (Term -> Term) -> [(Term, Term -> Term)]
ctxs ([Term]
ts [Term] -> Int -> Term
forall a. [a] -> Int -> a
!! Int
i) (\Term
u -> Term -> Term
k (Function
f Function -> [Term] -> Term
:@: (Int -> [Term] -> [Term]
forall a. Int -> [a] -> [a]
take Int
i [Term]
ts [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term
u] [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ Int -> [Term] -> [Term]
forall a. Int -> [a] -> [a]
drop (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [Term]
ts)))
          | Int
i <- [Int
0..[Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
tsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ]

----------------------------------------------------------------------
-- Literals

infix 8 :=:
data Atomic = Term :=: Term | Tru Term

-- Helper for (Eq Atomic, Ord Atomic) instances
normAtomic :: Atomic -> Either (Term, Term) Term
normAtomic :: Atomic -> Either (Term, Term) Term
normAtomic (Term
t1 :=: Term
t2) | Term
t1 Term -> Term -> Bool
forall a. Ord a => a -> a -> Bool
> Term
t2 = (Term, Term) -> Either (Term, Term) Term
forall a b. a -> Either a b
Left (Term
t2, Term
t1)
                       | Bool
otherwise = (Term, Term) -> Either (Term, Term) Term
forall a b. a -> Either a b
Left (Term
t1, Term
t2)
normAtomic (Tru Term
p) = Term -> Either (Term, Term) Term
forall a b. b -> Either a b
Right Term
p

instance Eq Atomic where
  Atomic
t1 == :: Atomic -> Atomic -> Bool
== Atomic
t2 = Atomic -> Either (Term, Term) Term
normAtomic Atomic
t1 Either (Term, Term) Term -> Either (Term, Term) Term -> Bool
forall a. Eq a => a -> a -> Bool
== Atomic -> Either (Term, Term) Term
normAtomic Atomic
t2

instance Ord Atomic where
  compare :: Atomic -> Atomic -> Ordering
compare = (Atomic -> Either (Term, Term) Term)
-> Atomic -> Atomic -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Atomic -> Either (Term, Term) Term
normAtomic

data Signed a = Pos a | Neg a
  deriving (Int -> Signed a -> ShowS
[Signed a] -> ShowS
Signed a -> [Char]
(Int -> Signed a -> ShowS)
-> (Signed a -> [Char]) -> ([Signed a] -> ShowS) -> Show (Signed a)
forall a. Show a => Int -> Signed a -> ShowS
forall a. Show a => [Signed a] -> ShowS
forall a. Show a => Signed a -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Signed a] -> ShowS
$cshowList :: forall a. Show a => [Signed a] -> ShowS
show :: Signed a -> [Char]
$cshow :: forall a. Show a => Signed a -> [Char]
showsPrec :: Int -> Signed a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Signed a -> ShowS
Show, Signed a -> Signed a -> Bool
(Signed a -> Signed a -> Bool)
-> (Signed a -> Signed a -> Bool) -> Eq (Signed a)
forall a. Eq a => Signed a -> Signed a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Signed a -> Signed a -> Bool
$c/= :: forall a. Eq a => Signed a -> Signed a -> Bool
== :: Signed a -> Signed a -> Bool
$c== :: forall a. Eq a => Signed a -> Signed a -> Bool
Eq, Eq (Signed a)
Eq (Signed a)
-> (Signed a -> Signed a -> Ordering)
-> (Signed a -> Signed a -> Bool)
-> (Signed a -> Signed a -> Bool)
-> (Signed a -> Signed a -> Bool)
-> (Signed a -> Signed a -> Bool)
-> (Signed a -> Signed a -> Signed a)
-> (Signed a -> Signed a -> Signed a)
-> Ord (Signed a)
Signed a -> Signed a -> Bool
Signed a -> Signed a -> Ordering
Signed a -> Signed a -> Signed a
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
forall a. Ord a => Eq (Signed a)
forall a. Ord a => Signed a -> Signed a -> Bool
forall a. Ord a => Signed a -> Signed a -> Ordering
forall a. Ord a => Signed a -> Signed a -> Signed a
min :: Signed a -> Signed a -> Signed a
$cmin :: forall a. Ord a => Signed a -> Signed a -> Signed a
max :: Signed a -> Signed a -> Signed a
$cmax :: forall a. Ord a => Signed a -> Signed a -> Signed a
>= :: Signed a -> Signed a -> Bool
$c>= :: forall a. Ord a => Signed a -> Signed a -> Bool
> :: Signed a -> Signed a -> Bool
$c> :: forall a. Ord a => Signed a -> Signed a -> Bool
<= :: Signed a -> Signed a -> Bool
$c<= :: forall a. Ord a => Signed a -> Signed a -> Bool
< :: Signed a -> Signed a -> Bool
$c< :: forall a. Ord a => Signed a -> Signed a -> Bool
compare :: Signed a -> Signed a -> Ordering
$ccompare :: forall a. Ord a => Signed a -> Signed a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Signed a)
Ord, a -> Signed b -> Signed a
(a -> b) -> Signed a -> Signed b
(forall a b. (a -> b) -> Signed a -> Signed b)
-> (forall a b. a -> Signed b -> Signed a) -> Functor Signed
forall a b. a -> Signed b -> Signed a
forall a b. (a -> b) -> Signed a -> Signed b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Signed b -> Signed a
$c<$ :: forall a b. a -> Signed b -> Signed a
fmap :: (a -> b) -> Signed a -> Signed b
$cfmap :: forall a b. (a -> b) -> Signed a -> Signed b
Functor, Signed a -> Bool
(a -> m) -> Signed a -> m
(a -> b -> b) -> b -> Signed a -> b
(forall m. Monoid m => Signed m -> m)
-> (forall m a. Monoid m => (a -> m) -> Signed a -> m)
-> (forall m a. Monoid m => (a -> m) -> Signed a -> m)
-> (forall a b. (a -> b -> b) -> b -> Signed a -> b)
-> (forall a b. (a -> b -> b) -> b -> Signed a -> b)
-> (forall b a. (b -> a -> b) -> b -> Signed a -> b)
-> (forall b a. (b -> a -> b) -> b -> Signed a -> b)
-> (forall a. (a -> a -> a) -> Signed a -> a)
-> (forall a. (a -> a -> a) -> Signed a -> a)
-> (forall a. Signed a -> [a])
-> (forall a. Signed a -> Bool)
-> (forall a. Signed a -> Int)
-> (forall a. Eq a => a -> Signed a -> Bool)
-> (forall a. Ord a => Signed a -> a)
-> (forall a. Ord a => Signed a -> a)
-> (forall a. Num a => Signed a -> a)
-> (forall a. Num a => Signed a -> a)
-> Foldable Signed
forall a. Eq a => a -> Signed a -> Bool
forall a. Num a => Signed a -> a
forall a. Ord a => Signed a -> a
forall m. Monoid m => Signed m -> m
forall a. Signed a -> Bool
forall a. Signed a -> Int
forall a. Signed a -> [a]
forall a. (a -> a -> a) -> Signed a -> a
forall m a. Monoid m => (a -> m) -> Signed a -> m
forall b a. (b -> a -> b) -> b -> Signed a -> b
forall a b. (a -> b -> b) -> b -> Signed a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Signed a -> a
$cproduct :: forall a. Num a => Signed a -> a
sum :: Signed a -> a
$csum :: forall a. Num a => Signed a -> a
minimum :: Signed a -> a
$cminimum :: forall a. Ord a => Signed a -> a
maximum :: Signed a -> a
$cmaximum :: forall a. Ord a => Signed a -> a
elem :: a -> Signed a -> Bool
$celem :: forall a. Eq a => a -> Signed a -> Bool
length :: Signed a -> Int
$clength :: forall a. Signed a -> Int
null :: Signed a -> Bool
$cnull :: forall a. Signed a -> Bool
toList :: Signed a -> [a]
$ctoList :: forall a. Signed a -> [a]
foldl1 :: (a -> a -> a) -> Signed a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Signed a -> a
foldr1 :: (a -> a -> a) -> Signed a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Signed a -> a
foldl' :: (b -> a -> b) -> b -> Signed a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Signed a -> b
foldl :: (b -> a -> b) -> b -> Signed a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Signed a -> b
foldr' :: (a -> b -> b) -> b -> Signed a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Signed a -> b
foldr :: (a -> b -> b) -> b -> Signed a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Signed a -> b
foldMap' :: (a -> m) -> Signed a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Signed a -> m
foldMap :: (a -> m) -> Signed a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Signed a -> m
fold :: Signed m -> m
$cfold :: forall m. Monoid m => Signed m -> m
Foldable, Functor Signed
Foldable Signed
Functor Signed
-> Foldable Signed
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Signed a -> f (Signed b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Signed (f a) -> f (Signed a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Signed a -> m (Signed b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Signed (m a) -> m (Signed a))
-> Traversable Signed
(a -> f b) -> Signed a -> f (Signed b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Signed (m a) -> m (Signed a)
forall (f :: * -> *) a.
Applicative f =>
Signed (f a) -> f (Signed a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Signed a -> m (Signed b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Signed a -> f (Signed b)
sequence :: Signed (m a) -> m (Signed a)
$csequence :: forall (m :: * -> *) a. Monad m => Signed (m a) -> m (Signed a)
mapM :: (a -> m b) -> Signed a -> m (Signed b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Signed a -> m (Signed b)
sequenceA :: Signed (f a) -> f (Signed a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Signed (f a) -> f (Signed a)
traverse :: (a -> f b) -> Signed a -> f (Signed b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Signed a -> f (Signed b)
$cp2Traversable :: Foldable Signed
$cp1Traversable :: Functor Signed
Traversable)

type Literal = Signed Atomic

neg :: Signed a -> Signed a
neg :: Signed a -> Signed a
neg (Pos a
x) = a -> Signed a
forall a. a -> Signed a
Neg a
x
neg (Neg a
x) = a -> Signed a
forall a. a -> Signed a
Pos a
x

the :: Signed a -> a
the :: Signed a -> a
the (Pos a
x) = a
x
the (Neg a
x) = a
x

pos :: Signed a -> Bool
pos :: Signed a -> Bool
pos (Pos a
_) = Bool
True
pos (Neg a
_) = Bool
False

signForm :: Signed a -> Form -> Form
signForm :: Signed a -> Form -> Form
signForm (Pos a
_) Form
f = Form
f
signForm (Neg a
_) Form
f = Form -> Form
Not Form
f

----------------------------------------------------------------------
-- Formulae

-- Invariant: each name is bound only once on each path
-- i.e. nested quantification of the same variable twice is not allowed
-- Not OK: ![X]: (... ![X]: ...)
-- OK:     (![X]: ...) & (![X]: ...)
-- Free variables must also not be bound inside subformulae
data Form
  = Literal Literal
  | Not Form
  | And [Form]
  | Or [Form]
  | Equiv Form Form
  | ForAll {-# UNPACK #-} !(Bind Form)
  | Exists {-# UNPACK #-} !(Bind Form)
    -- Just exists so that parsing followed by pretty-printing is
    -- somewhat lossless; the simplify function will get rid of it
  | Connective Connective Form Form
  deriving (Form -> Form -> Bool
(Form -> Form -> Bool) -> (Form -> Form -> Bool) -> Eq Form
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Form -> Form -> Bool
$c/= :: Form -> Form -> Bool
== :: Form -> Form -> Bool
$c== :: Form -> Form -> Bool
Eq, Eq Form
Eq Form
-> (Form -> Form -> Ordering)
-> (Form -> Form -> Bool)
-> (Form -> Form -> Bool)
-> (Form -> Form -> Bool)
-> (Form -> Form -> Bool)
-> (Form -> Form -> Form)
-> (Form -> Form -> Form)
-> Ord Form
Form -> Form -> Bool
Form -> Form -> Ordering
Form -> Form -> Form
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 :: Form -> Form -> Form
$cmin :: Form -> Form -> Form
max :: Form -> Form -> Form
$cmax :: Form -> Form -> Form
>= :: Form -> Form -> Bool
$c>= :: Form -> Form -> Bool
> :: Form -> Form -> Bool
$c> :: Form -> Form -> Bool
<= :: Form -> Form -> Bool
$c<= :: Form -> Form -> Bool
< :: Form -> Form -> Bool
$c< :: Form -> Form -> Bool
compare :: Form -> Form -> Ordering
$ccompare :: Form -> Form -> Ordering
$cp1Ord :: Eq Form
Ord)

-- Miscellaneous connectives that exist in TPTP
data Connective = Implies | Follows | Xor | Nor | Nand
  deriving (Connective -> Connective -> Bool
(Connective -> Connective -> Bool)
-> (Connective -> Connective -> Bool) -> Eq Connective
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Connective -> Connective -> Bool
$c/= :: Connective -> Connective -> Bool
== :: Connective -> Connective -> Bool
$c== :: Connective -> Connective -> Bool
Eq, Eq Connective
Eq Connective
-> (Connective -> Connective -> Ordering)
-> (Connective -> Connective -> Bool)
-> (Connective -> Connective -> Bool)
-> (Connective -> Connective -> Bool)
-> (Connective -> Connective -> Bool)
-> (Connective -> Connective -> Connective)
-> (Connective -> Connective -> Connective)
-> Ord Connective
Connective -> Connective -> Bool
Connective -> Connective -> Ordering
Connective -> Connective -> Connective
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 :: Connective -> Connective -> Connective
$cmin :: Connective -> Connective -> Connective
max :: Connective -> Connective -> Connective
$cmax :: Connective -> Connective -> Connective
>= :: Connective -> Connective -> Bool
$c>= :: Connective -> Connective -> Bool
> :: Connective -> Connective -> Bool
$c> :: Connective -> Connective -> Bool
<= :: Connective -> Connective -> Bool
$c<= :: Connective -> Connective -> Bool
< :: Connective -> Connective -> Bool
$c< :: Connective -> Connective -> Bool
compare :: Connective -> Connective -> Ordering
$ccompare :: Connective -> Connective -> Ordering
$cp1Ord :: Eq Connective
Ord)

connective :: Connective -> Form -> Form -> Form
connective :: Connective -> Form -> Form -> Form
connective Connective
Implies Form
t Form
u = Form -> Form
nt Form
t Form -> Form -> Form
\/ Form
u
connective Connective
Follows Form
t Form
u = Form
t Form -> Form -> Form
\/ Form -> Form
nt Form
u
connective Connective
Xor Form
t Form
u = Form -> Form
nt (Form
t Form -> Form -> Form
`Equiv` Form
u)
connective Connective
Nor Form
t Form
u = Form -> Form
nt (Form
t Form -> Form -> Form
\/ Form
u)
connective Connective
Nand Form
t Form
u = Form -> Form
nt (Form
t Form -> Form -> Form
/\ Form
u)

data Bind a = Bind (Set Variable) a
  deriving (Bind a -> Bind a -> Bool
(Bind a -> Bind a -> Bool)
-> (Bind a -> Bind a -> Bool) -> Eq (Bind a)
forall a. Eq a => Bind a -> Bind a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Bind a -> Bind a -> Bool
$c/= :: forall a. Eq a => Bind a -> Bind a -> Bool
== :: Bind a -> Bind a -> Bool
$c== :: forall a. Eq a => Bind a -> Bind a -> Bool
Eq, Eq (Bind a)
Eq (Bind a)
-> (Bind a -> Bind a -> Ordering)
-> (Bind a -> Bind a -> Bool)
-> (Bind a -> Bind a -> Bool)
-> (Bind a -> Bind a -> Bool)
-> (Bind a -> Bind a -> Bool)
-> (Bind a -> Bind a -> Bind a)
-> (Bind a -> Bind a -> Bind a)
-> Ord (Bind a)
Bind a -> Bind a -> Bool
Bind a -> Bind a -> Ordering
Bind a -> Bind a -> Bind a
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
forall a. Ord a => Eq (Bind a)
forall a. Ord a => Bind a -> Bind a -> Bool
forall a. Ord a => Bind a -> Bind a -> Ordering
forall a. Ord a => Bind a -> Bind a -> Bind a
min :: Bind a -> Bind a -> Bind a
$cmin :: forall a. Ord a => Bind a -> Bind a -> Bind a
max :: Bind a -> Bind a -> Bind a
$cmax :: forall a. Ord a => Bind a -> Bind a -> Bind a
>= :: Bind a -> Bind a -> Bool
$c>= :: forall a. Ord a => Bind a -> Bind a -> Bool
> :: Bind a -> Bind a -> Bool
$c> :: forall a. Ord a => Bind a -> Bind a -> Bool
<= :: Bind a -> Bind a -> Bool
$c<= :: forall a. Ord a => Bind a -> Bind a -> Bool
< :: Bind a -> Bind a -> Bool
$c< :: forall a. Ord a => Bind a -> Bind a -> Bool
compare :: Bind a -> Bind a -> Ordering
$ccompare :: forall a. Ord a => Bind a -> Bind a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Bind a)
Ord)

true, false :: Form
true :: Form
true = [Form] -> Form
And []
false :: Form
false = [Form] -> Form
Or []

isTrue, isFalse :: Form -> Bool
isTrue :: Form -> Bool
isTrue (And []) = Bool
True
isTrue Form
_ = Bool
False
isFalse :: Form -> Bool
isFalse (Or []) = Bool
True
isFalse Form
_ = Bool
False

nt :: Form -> Form
nt :: Form -> Form
nt (Not Form
a) = Form
a
nt Form
a       = Form -> Form
Not Form
a

(.=>.) :: Form -> Form -> Form
.=>. :: Form -> Form -> Form
(.=>.) = Connective -> Form -> Form -> Form
connective Connective
Implies

(.=.) :: Term -> Term -> Form
Term
t .=. :: Term -> Term -> Form
.=. Term
u | Term -> Type
forall a. Typed a => a -> Type
typ Term
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
O = Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Pos (Term -> Atomic
Tru Term
t)) Form -> Form -> Form
`Equiv` Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Pos (Term -> Atomic
Tru Term
u))
        | Bool
otherwise = Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Pos (Term
t Term -> Term -> Atomic
:=: Term
u))

(/\), (\/) :: Form -> Form -> Form
And [Form]
as /\ :: Form -> Form -> Form
/\ And [Form]
bs = [Form] -> Form
And ([Form]
as [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [Form]
bs)
Form
a      /\ Form
b | Form -> Bool
isFalse Form
a Bool -> Bool -> Bool
|| Form -> Bool
isFalse Form
b = Form
false
And [Form]
as /\ Form
b      = [Form] -> Form
And (Form
bForm -> [Form] -> [Form]
forall a. a -> [a] -> [a]
:[Form]
as)
Form
a      /\ And [Form]
bs = [Form] -> Form
And (Form
aForm -> [Form] -> [Form]
forall a. a -> [a] -> [a]
:[Form]
bs)
Form
a      /\ Form
b      = [Form] -> Form
And [Form
a, Form
b]

Or [Form]
as \/ :: Form -> Form -> Form
\/ Or [Form]
bs = [Form] -> Form
Or ([Form]
as [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [Form]
bs)
Form
a     \/ Form
b | Form -> Bool
isTrue Form
a Bool -> Bool -> Bool
|| Form -> Bool
isTrue Form
b = Form
true
Or [Form]
as \/ Form
b     = [Form] -> Form
Or (Form
bForm -> [Form] -> [Form]
forall a. a -> [a] -> [a]
:[Form]
as)
Form
a     \/ Or [Form]
bs = [Form] -> Form
Or (Form
aForm -> [Form] -> [Form]
forall a. a -> [a] -> [a]
:[Form]
bs)
Form
a     \/ Form
b     = [Form] -> Form
Or [Form
a, Form
b]

closeForm :: Form -> Form
closeForm :: Form -> Form
closeForm Form
f | Set Variable -> Bool
forall a. Set a -> Bool
Set.null Set Variable
vars = Form
f
            | Bool
otherwise = Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vars Form
f)
  where vars :: Set Variable
vars = Form -> Set Variable
forall a. Symbolic a => a -> Set Variable
free Form
f

-- remove Not from the root of a problem
positive :: Form -> Form
positive :: Form -> Form
positive (Not Form
f) = Form -> Form
notInwards Form
f
-- Some connectives are fairly not-ish
positive (Connective Connective
c Form
t Form
u)         = Form -> Form
positive (Connective -> Form -> Form -> Form
connective Connective
c Form
t Form
u)
positive Form
f = Form
f

notInwards :: Form -> Form
notInwards :: Form -> Form
notInwards (And [Form]
as)             = [Form] -> Form
Or ((Form -> Form) -> [Form] -> [Form]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Form -> Form
notInwards [Form]
as)
notInwards (Or [Form]
as)              = [Form] -> Form
And ((Form -> Form) -> [Form] -> [Form]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Form -> Form
notInwards [Form]
as)
notInwards (Form
a `Equiv` Form
b)        = Form -> Form
notInwards Form
a Form -> Form -> Form
`Equiv` Form
b
notInwards (Not Form
a)              = Form -> Form
positive Form
a
notInwards (ForAll (Bind Set Variable
vs Form
a)) = Bind Form -> Form
Exists (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs (Form -> Form
notInwards Form
a))
notInwards (Exists (Bind Set Variable
vs Form
a)) = Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs (Form -> Form
notInwards Form
a))
notInwards (Literal Literal
l)          = Literal -> Form
Literal (Literal -> Literal
forall a. Signed a -> Signed a
neg Literal
l)
notInwards (Connective Connective
c Form
t Form
u)   = Form -> Form
notInwards (Connective -> Form -> Form -> Form
connective Connective
c Form
t Form
u)

-- remove Exists and Or from the top level of a formula
simple :: Form -> Form
simple :: Form -> Form
simple (Or [Form]
as)              = Form -> Form
Not ([Form] -> Form
And ((Form -> Form) -> [Form] -> [Form]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Form -> Form
nt [Form]
as))
simple (Exists (Bind Set Variable
vs Form
a)) = Form -> Form
Not (Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs (Form -> Form
nt Form
a)))
simple (Connective Connective
c Form
t Form
u)   = Form -> Form
simple (Connective -> Form -> Form -> Form
connective Connective
c Form
t Form
u)
simple Form
a                    = Form
a

-- perform some easy algebraic simplifications
simplify :: Form -> Form
simplify t :: Form
t@Literal{} = Form
t
simplify (Connective Connective
c Form
t Form
u) = Form -> Form
simplify (Connective -> Form -> Form -> Form
connective Connective
c Form
t Form
u)
simplify (Not Form
t) = Form -> Form
simplify (Form -> Form
notInwards Form
t)
simplify (And [Form]
ts) = (Form -> Form -> Form) -> Form -> [Form] -> Form
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
(/\) Form
true ((Form -> Form) -> [Form] -> [Form]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Form -> Form
simplify [Form]
ts)
simplify (Or [Form]
ts) = (Form -> Form -> Form) -> Form -> [Form] -> Form
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
(\/) Form
false ((Form -> Form) -> [Form] -> [Form]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Form -> Form
simplify [Form]
ts)
simplify (Equiv Form
t Form
u) = Form -> Form -> Form
equiv (Form -> Form
simplify Form
t) (Form -> Form
simplify Form
u)
  where equiv :: Form -> Form -> Form
equiv Form
t Form
u | Form -> Bool
isTrue Form
t = Form
u
                  | Form -> Bool
isTrue Form
u = Form
t
                  | Form -> Bool
isFalse Form
t = Form -> Form
nt Form
u
                  | Form -> Bool
isFalse Form
u = Form -> Form
nt Form
t
                  | Bool
otherwise = Form -> Form -> Form
Equiv Form
t Form
u
simplify (ForAll (Bind Set Variable
vs Form
t)) = Set Variable -> Form -> Form
forAll Set Variable
vs (Form -> Form
simplify Form
t)
  where forAll :: Set Variable -> Form -> Form
forAll Set Variable
vs Form
t | Set Variable -> Bool
forall a. Set a -> Bool
Set.null Set Variable
vs = Form
t
        forAll Set Variable
vs (ForAll (Bind Set Variable
vs' Form
t)) = Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind (Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Variable
vs Set Variable
vs') Form
t)
        forAll Set Variable
vs Form
t = Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs Form
t)
simplify (Exists (Bind Set Variable
vs Form
t)) = Set Variable -> Form -> Form
exists Set Variable
vs (Form -> Form
simplify Form
t)
  where exists :: Set Variable -> Form -> Form
exists Set Variable
vs Form
t | Set Variable -> Bool
forall a. Set a -> Bool
Set.null Set Variable
vs = Form
t
        exists Set Variable
vs (Exists (Bind Set Variable
vs' Form
t)) = Bind Form -> Form
Exists (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind (Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Variable
vs Set Variable
vs') Form
t)
        exists Set Variable
vs Form
t = Bind Form -> Form
Exists (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs Form
t)

----------------------------------------------------------------------
-- Clauses

data CNF =
  CNF {
    CNF -> [Input Clause]
axioms :: [Input Clause],
    CNF -> [[Input Clause]]
conjectures :: [[Input Clause]],
    CNF -> Maybe Model -> Answer
satisfiable :: Maybe Model -> Answer,
    CNF -> Maybe Model -> Answer
unsatisfiable :: Maybe CNFRefutation -> Answer }

toCNF :: [Input Clause] -> [[Input Clause]] -> CNF
toCNF :: [Input Clause] -> [[Input Clause]] -> CNF
toCNF [Input Clause]
axioms [] = [Input Clause]
-> [[Input Clause]]
-> (Maybe Model -> Answer)
-> (Maybe Model -> Answer)
-> CNF
CNF [Input Clause]
axioms [[]] (SatReason -> Maybe Model -> Answer
Sat SatReason
Satisfiable) (UnsatReason -> Maybe Model -> Answer
Unsat UnsatReason
Unsatisfiable)
toCNF [Input Clause]
axioms [[Input Clause]
conjecture] = [Input Clause]
-> [[Input Clause]]
-> (Maybe Model -> Answer)
-> (Maybe Model -> Answer)
-> CNF
CNF [Input Clause]
axioms [[Input Clause]
conjecture] (SatReason -> Maybe Model -> Answer
Sat SatReason
CounterSatisfiable) (UnsatReason -> Maybe Model -> Answer
Unsat UnsatReason
Theorem)
toCNF [Input Clause]
axioms [[Input Clause]]
conjectures = [Input Clause]
-> [[Input Clause]]
-> (Maybe Model -> Answer)
-> (Maybe Model -> Answer)
-> CNF
CNF [Input Clause]
axioms [[Input Clause]]
conjectures (\Maybe Model
_ -> NoAnswerReason -> Answer
NoAnswer NoAnswerReason
GaveUp) (UnsatReason -> Maybe Model -> Answer
Unsat UnsatReason
Theorem)

newtype Clause = Clause (Bind [Literal])

clause :: [Literal] -> Clause
clause :: [Literal] -> Clause
clause [Literal]
xs = Bind [Literal] -> Clause
Clause ([Literal] -> Bind [Literal]
forall a. Symbolic a => a -> Bind a
bind [Literal]
xs)

toForm :: Clause -> Form
toForm :: Clause -> Form
toForm (Clause (Bind Set Variable
vs [Literal]
ls))
  | Set Variable -> Bool
forall a. Set a -> Bool
Set.null Set Variable
vs = [Form] -> Form
Or ((Literal -> Form) -> [Literal] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Literal -> Form
Literal [Literal]
ls)
  | Bool
otherwise = Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs ([Form] -> Form
Or ((Literal -> Form) -> [Literal] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Literal -> Form
Literal [Literal]
ls)))

toLiterals :: Clause -> [Literal]
toLiterals :: Clause -> [Literal]
toLiterals (Clause (Bind Set Variable
_ [Literal]
ls)) = [Literal]
ls

toClause :: Form -> Maybe Clause
toClause :: Form -> Maybe Clause
toClause (ForAll (Bind Set Variable
_ Form
f)) = Form -> Maybe Clause
toClause Form
f
toClause Form
f = [Literal] -> Clause
clause ([Literal] -> Clause) -> Maybe [Literal] -> Maybe Clause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Form -> Maybe [Literal]
cl Form
f
  where
    cl :: Form -> Maybe [Literal]
cl (Or [Form]
fs) = [[Literal]] -> [Literal]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Literal]] -> [Literal]) -> Maybe [[Literal]] -> Maybe [Literal]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Form -> Maybe [Literal]) -> [Form] -> Maybe [[Literal]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Form -> Maybe [Literal]
cl [Form]
fs
    cl (Literal Literal
l) = [Literal] -> Maybe [Literal]
forall a. a -> Maybe a
Just [Literal
l]
    cl (Not (Literal Literal
l)) = [Literal] -> Maybe [Literal]
forall a. a -> Maybe a
Just [Literal -> Literal
forall a. Signed a -> Signed a
neg Literal
l]
    cl Form
_ = Maybe [Literal]
forall a. Maybe a
Nothing

----------------------------------------------------------------------
-- Problems

type Tag = String

data Kind = Ax AxKind | Conj ConjKind deriving (Kind -> Kind -> Bool
(Kind -> Kind -> Bool) -> (Kind -> Kind -> Bool) -> Eq Kind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Kind -> Kind -> Bool
$c/= :: Kind -> Kind -> Bool
== :: Kind -> Kind -> Bool
$c== :: Kind -> Kind -> Bool
Eq, Eq Kind
Eq Kind
-> (Kind -> Kind -> Ordering)
-> (Kind -> Kind -> Bool)
-> (Kind -> Kind -> Bool)
-> (Kind -> Kind -> Bool)
-> (Kind -> Kind -> Bool)
-> (Kind -> Kind -> Kind)
-> (Kind -> Kind -> Kind)
-> Ord Kind
Kind -> Kind -> Bool
Kind -> Kind -> Ordering
Kind -> Kind -> Kind
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 :: Kind -> Kind -> Kind
$cmin :: Kind -> Kind -> Kind
max :: Kind -> Kind -> Kind
$cmax :: Kind -> Kind -> Kind
>= :: Kind -> Kind -> Bool
$c>= :: Kind -> Kind -> Bool
> :: Kind -> Kind -> Bool
$c> :: Kind -> Kind -> Bool
<= :: Kind -> Kind -> Bool
$c<= :: Kind -> Kind -> Bool
< :: Kind -> Kind -> Bool
$c< :: Kind -> Kind -> Bool
compare :: Kind -> Kind -> Ordering
$ccompare :: Kind -> Kind -> Ordering
$cp1Ord :: Eq Kind
Ord)
data AxKind =
  Axiom | Hypothesis | Definition | Assumption | Lemma | TheoremKind |
  NegatedConjecture deriving (AxKind -> AxKind -> Bool
(AxKind -> AxKind -> Bool)
-> (AxKind -> AxKind -> Bool) -> Eq AxKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AxKind -> AxKind -> Bool
$c/= :: AxKind -> AxKind -> Bool
== :: AxKind -> AxKind -> Bool
$c== :: AxKind -> AxKind -> Bool
Eq, Eq AxKind
Eq AxKind
-> (AxKind -> AxKind -> Ordering)
-> (AxKind -> AxKind -> Bool)
-> (AxKind -> AxKind -> Bool)
-> (AxKind -> AxKind -> Bool)
-> (AxKind -> AxKind -> Bool)
-> (AxKind -> AxKind -> AxKind)
-> (AxKind -> AxKind -> AxKind)
-> Ord AxKind
AxKind -> AxKind -> Bool
AxKind -> AxKind -> Ordering
AxKind -> AxKind -> AxKind
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 :: AxKind -> AxKind -> AxKind
$cmin :: AxKind -> AxKind -> AxKind
max :: AxKind -> AxKind -> AxKind
$cmax :: AxKind -> AxKind -> AxKind
>= :: AxKind -> AxKind -> Bool
$c>= :: AxKind -> AxKind -> Bool
> :: AxKind -> AxKind -> Bool
$c> :: AxKind -> AxKind -> Bool
<= :: AxKind -> AxKind -> Bool
$c<= :: AxKind -> AxKind -> Bool
< :: AxKind -> AxKind -> Bool
$c< :: AxKind -> AxKind -> Bool
compare :: AxKind -> AxKind -> Ordering
$ccompare :: AxKind -> AxKind -> Ordering
$cp1Ord :: Eq AxKind
Ord)
data ConjKind = Conjecture | Question deriving (ConjKind -> ConjKind -> Bool
(ConjKind -> ConjKind -> Bool)
-> (ConjKind -> ConjKind -> Bool) -> Eq ConjKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConjKind -> ConjKind -> Bool
$c/= :: ConjKind -> ConjKind -> Bool
== :: ConjKind -> ConjKind -> Bool
$c== :: ConjKind -> ConjKind -> Bool
Eq, Eq ConjKind
Eq ConjKind
-> (ConjKind -> ConjKind -> Ordering)
-> (ConjKind -> ConjKind -> Bool)
-> (ConjKind -> ConjKind -> Bool)
-> (ConjKind -> ConjKind -> Bool)
-> (ConjKind -> ConjKind -> Bool)
-> (ConjKind -> ConjKind -> ConjKind)
-> (ConjKind -> ConjKind -> ConjKind)
-> Ord ConjKind
ConjKind -> ConjKind -> Bool
ConjKind -> ConjKind -> Ordering
ConjKind -> ConjKind -> ConjKind
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 :: ConjKind -> ConjKind -> ConjKind
$cmin :: ConjKind -> ConjKind -> ConjKind
max :: ConjKind -> ConjKind -> ConjKind
$cmax :: ConjKind -> ConjKind -> ConjKind
>= :: ConjKind -> ConjKind -> Bool
$c>= :: ConjKind -> ConjKind -> Bool
> :: ConjKind -> ConjKind -> Bool
$c> :: ConjKind -> ConjKind -> Bool
<= :: ConjKind -> ConjKind -> Bool
$c<= :: ConjKind -> ConjKind -> Bool
< :: ConjKind -> ConjKind -> Bool
$c< :: ConjKind -> ConjKind -> Bool
compare :: ConjKind -> ConjKind -> Ordering
$ccompare :: ConjKind -> ConjKind -> Ordering
$cp1Ord :: Eq ConjKind
Ord)

data Answer = Sat SatReason (Maybe Model) | Unsat UnsatReason (Maybe CNFRefutation) | NoAnswer NoAnswerReason
  deriving (Answer -> Answer -> Bool
(Answer -> Answer -> Bool)
-> (Answer -> Answer -> Bool) -> Eq Answer
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Answer -> Answer -> Bool
$c/= :: Answer -> Answer -> Bool
== :: Answer -> Answer -> Bool
$c== :: Answer -> Answer -> Bool
Eq, Eq Answer
Eq Answer
-> (Answer -> Answer -> Ordering)
-> (Answer -> Answer -> Bool)
-> (Answer -> Answer -> Bool)
-> (Answer -> Answer -> Bool)
-> (Answer -> Answer -> Bool)
-> (Answer -> Answer -> Answer)
-> (Answer -> Answer -> Answer)
-> Ord Answer
Answer -> Answer -> Bool
Answer -> Answer -> Ordering
Answer -> Answer -> Answer
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 :: Answer -> Answer -> Answer
$cmin :: Answer -> Answer -> Answer
max :: Answer -> Answer -> Answer
$cmax :: Answer -> Answer -> Answer
>= :: Answer -> Answer -> Bool
$c>= :: Answer -> Answer -> Bool
> :: Answer -> Answer -> Bool
$c> :: Answer -> Answer -> Bool
<= :: Answer -> Answer -> Bool
$c<= :: Answer -> Answer -> Bool
< :: Answer -> Answer -> Bool
$c< :: Answer -> Answer -> Bool
compare :: Answer -> Answer -> Ordering
$ccompare :: Answer -> Answer -> Ordering
$cp1Ord :: Eq Answer
Ord)

data NoAnswerReason = GaveUp | Timeout deriving (NoAnswerReason -> NoAnswerReason -> Bool
(NoAnswerReason -> NoAnswerReason -> Bool)
-> (NoAnswerReason -> NoAnswerReason -> Bool) -> Eq NoAnswerReason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NoAnswerReason -> NoAnswerReason -> Bool
$c/= :: NoAnswerReason -> NoAnswerReason -> Bool
== :: NoAnswerReason -> NoAnswerReason -> Bool
$c== :: NoAnswerReason -> NoAnswerReason -> Bool
Eq, Eq NoAnswerReason
Eq NoAnswerReason
-> (NoAnswerReason -> NoAnswerReason -> Ordering)
-> (NoAnswerReason -> NoAnswerReason -> Bool)
-> (NoAnswerReason -> NoAnswerReason -> Bool)
-> (NoAnswerReason -> NoAnswerReason -> Bool)
-> (NoAnswerReason -> NoAnswerReason -> Bool)
-> (NoAnswerReason -> NoAnswerReason -> NoAnswerReason)
-> (NoAnswerReason -> NoAnswerReason -> NoAnswerReason)
-> Ord NoAnswerReason
NoAnswerReason -> NoAnswerReason -> Bool
NoAnswerReason -> NoAnswerReason -> Ordering
NoAnswerReason -> NoAnswerReason -> NoAnswerReason
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 :: NoAnswerReason -> NoAnswerReason -> NoAnswerReason
$cmin :: NoAnswerReason -> NoAnswerReason -> NoAnswerReason
max :: NoAnswerReason -> NoAnswerReason -> NoAnswerReason
$cmax :: NoAnswerReason -> NoAnswerReason -> NoAnswerReason
>= :: NoAnswerReason -> NoAnswerReason -> Bool
$c>= :: NoAnswerReason -> NoAnswerReason -> Bool
> :: NoAnswerReason -> NoAnswerReason -> Bool
$c> :: NoAnswerReason -> NoAnswerReason -> Bool
<= :: NoAnswerReason -> NoAnswerReason -> Bool
$c<= :: NoAnswerReason -> NoAnswerReason -> Bool
< :: NoAnswerReason -> NoAnswerReason -> Bool
$c< :: NoAnswerReason -> NoAnswerReason -> Bool
compare :: NoAnswerReason -> NoAnswerReason -> Ordering
$ccompare :: NoAnswerReason -> NoAnswerReason -> Ordering
$cp1Ord :: Eq NoAnswerReason
Ord, Int -> NoAnswerReason -> ShowS
[NoAnswerReason] -> ShowS
NoAnswerReason -> [Char]
(Int -> NoAnswerReason -> ShowS)
-> (NoAnswerReason -> [Char])
-> ([NoAnswerReason] -> ShowS)
-> Show NoAnswerReason
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [NoAnswerReason] -> ShowS
$cshowList :: [NoAnswerReason] -> ShowS
show :: NoAnswerReason -> [Char]
$cshow :: NoAnswerReason -> [Char]
showsPrec :: Int -> NoAnswerReason -> ShowS
$cshowsPrec :: Int -> NoAnswerReason -> ShowS
Show)
data SatReason = Satisfiable | CounterSatisfiable deriving (SatReason -> SatReason -> Bool
(SatReason -> SatReason -> Bool)
-> (SatReason -> SatReason -> Bool) -> Eq SatReason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SatReason -> SatReason -> Bool
$c/= :: SatReason -> SatReason -> Bool
== :: SatReason -> SatReason -> Bool
$c== :: SatReason -> SatReason -> Bool
Eq, Eq SatReason
Eq SatReason
-> (SatReason -> SatReason -> Ordering)
-> (SatReason -> SatReason -> Bool)
-> (SatReason -> SatReason -> Bool)
-> (SatReason -> SatReason -> Bool)
-> (SatReason -> SatReason -> Bool)
-> (SatReason -> SatReason -> SatReason)
-> (SatReason -> SatReason -> SatReason)
-> Ord SatReason
SatReason -> SatReason -> Bool
SatReason -> SatReason -> Ordering
SatReason -> SatReason -> SatReason
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 :: SatReason -> SatReason -> SatReason
$cmin :: SatReason -> SatReason -> SatReason
max :: SatReason -> SatReason -> SatReason
$cmax :: SatReason -> SatReason -> SatReason
>= :: SatReason -> SatReason -> Bool
$c>= :: SatReason -> SatReason -> Bool
> :: SatReason -> SatReason -> Bool
$c> :: SatReason -> SatReason -> Bool
<= :: SatReason -> SatReason -> Bool
$c<= :: SatReason -> SatReason -> Bool
< :: SatReason -> SatReason -> Bool
$c< :: SatReason -> SatReason -> Bool
compare :: SatReason -> SatReason -> Ordering
$ccompare :: SatReason -> SatReason -> Ordering
$cp1Ord :: Eq SatReason
Ord, Int -> SatReason -> ShowS
[SatReason] -> ShowS
SatReason -> [Char]
(Int -> SatReason -> ShowS)
-> (SatReason -> [Char])
-> ([SatReason] -> ShowS)
-> Show SatReason
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SatReason] -> ShowS
$cshowList :: [SatReason] -> ShowS
show :: SatReason -> [Char]
$cshow :: SatReason -> [Char]
showsPrec :: Int -> SatReason -> ShowS
$cshowsPrec :: Int -> SatReason -> ShowS
Show)
data UnsatReason = Unsatisfiable | Theorem deriving (UnsatReason -> UnsatReason -> Bool
(UnsatReason -> UnsatReason -> Bool)
-> (UnsatReason -> UnsatReason -> Bool) -> Eq UnsatReason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UnsatReason -> UnsatReason -> Bool
$c/= :: UnsatReason -> UnsatReason -> Bool
== :: UnsatReason -> UnsatReason -> Bool
$c== :: UnsatReason -> UnsatReason -> Bool
Eq, Eq UnsatReason
Eq UnsatReason
-> (UnsatReason -> UnsatReason -> Ordering)
-> (UnsatReason -> UnsatReason -> Bool)
-> (UnsatReason -> UnsatReason -> Bool)
-> (UnsatReason -> UnsatReason -> Bool)
-> (UnsatReason -> UnsatReason -> Bool)
-> (UnsatReason -> UnsatReason -> UnsatReason)
-> (UnsatReason -> UnsatReason -> UnsatReason)
-> Ord UnsatReason
UnsatReason -> UnsatReason -> Bool
UnsatReason -> UnsatReason -> Ordering
UnsatReason -> UnsatReason -> UnsatReason
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 :: UnsatReason -> UnsatReason -> UnsatReason
$cmin :: UnsatReason -> UnsatReason -> UnsatReason
max :: UnsatReason -> UnsatReason -> UnsatReason
$cmax :: UnsatReason -> UnsatReason -> UnsatReason
>= :: UnsatReason -> UnsatReason -> Bool
$c>= :: UnsatReason -> UnsatReason -> Bool
> :: UnsatReason -> UnsatReason -> Bool
$c> :: UnsatReason -> UnsatReason -> Bool
<= :: UnsatReason -> UnsatReason -> Bool
$c<= :: UnsatReason -> UnsatReason -> Bool
< :: UnsatReason -> UnsatReason -> Bool
$c< :: UnsatReason -> UnsatReason -> Bool
compare :: UnsatReason -> UnsatReason -> Ordering
$ccompare :: UnsatReason -> UnsatReason -> Ordering
$cp1Ord :: Eq UnsatReason
Ord, Int -> UnsatReason -> ShowS
[UnsatReason] -> ShowS
UnsatReason -> [Char]
(Int -> UnsatReason -> ShowS)
-> (UnsatReason -> [Char])
-> ([UnsatReason] -> ShowS)
-> Show UnsatReason
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [UnsatReason] -> ShowS
$cshowList :: [UnsatReason] -> ShowS
show :: UnsatReason -> [Char]
$cshow :: UnsatReason -> [Char]
showsPrec :: Int -> UnsatReason -> ShowS
$cshowsPrec :: Int -> UnsatReason -> ShowS
Show)
type Model = [String]
type CNFRefutation = [String]

instance Show Answer where
  show :: Answer -> [Char]
show (Sat SatReason
reason Maybe Model
_) = SatReason -> [Char]
forall a. Show a => a -> [Char]
show SatReason
reason
  show (Unsat UnsatReason
reason Maybe Model
_) = UnsatReason -> [Char]
forall a. Show a => a -> [Char]
show UnsatReason
reason
  show (NoAnswer NoAnswerReason
x) = NoAnswerReason -> [Char]
forall a. Show a => a -> [Char]
show NoAnswerReason
x

explainAnswer :: Answer -> String
explainAnswer :: Answer -> [Char]
explainAnswer (Sat SatReason
Satisfiable Maybe Model
_) = [Char]
"the axioms are consistent"
explainAnswer (Sat SatReason
CounterSatisfiable Maybe Model
_) = [Char]
"the conjecture is false"
explainAnswer (Unsat UnsatReason
Unsatisfiable Maybe Model
_) = [Char]
"the axioms are contradictory"
explainAnswer (Unsat UnsatReason
Theorem Maybe Model
_) = [Char]
"the conjecture is true"
explainAnswer (NoAnswer NoAnswerReason
GaveUp) = [Char]
"couldn't solve the problem"
explainAnswer (NoAnswer NoAnswerReason
Timeout) = [Char]
"ran out of time while solving the problem"

answerSZS :: Answer -> [String]
answerSZS :: Answer -> Model
answerSZS Answer
answer =
  [[Char]
"% SZS status " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Answer -> [Char]
forall a. Show a => a -> [Char]
show Answer
answer] Model -> Model -> Model
forall a. [a] -> [a] -> [a]
++
  case Answer -> Maybe Model
answerJustification Answer
answer of
    Maybe Model
Nothing -> []
    Just Model
strs -> [[Char]
""] Model -> Model -> Model
forall a. [a] -> [a] -> [a]
++ Model
strs

answerJustification :: Answer -> Maybe [String]
answerJustification :: Answer -> Maybe Model
answerJustification (Sat SatReason
_ (Just Model
model)) =
  Model -> Maybe Model
forall a. a -> Maybe a
Just (Model -> Maybe Model) -> Model -> Maybe Model
forall a b. (a -> b) -> a -> b
$
    [[Char]
"% SZS output start Model"] Model -> Model -> Model
forall a. [a] -> [a] -> [a]
++
    Model
model Model -> Model -> Model
forall a. [a] -> [a] -> [a]
++
    [[Char]
"% SZS output end Model"]
answerJustification (Unsat UnsatReason
_ (Just Model
refutation)) =
  Model -> Maybe Model
forall a. a -> Maybe a
Just (Model -> Maybe Model) -> Model -> Maybe Model
forall a b. (a -> b) -> a -> b
$
    [[Char]
"% SZS output start CNFRefutation"] Model -> Model -> Model
forall a. [a] -> [a] -> [a]
++
    Model
refutation Model -> Model -> Model
forall a. [a] -> [a] -> [a]
++
    [[Char]
"% SZS output end CNFRefutation"]
answerJustification Answer
_ = Maybe Model
forall a. Maybe a
Nothing

data Input a = Input
  { Input a -> [Char]
tag    :: Tag,
    Input a -> Kind
kind   :: Kind,
    Input a -> InputSource
source :: InputSource,
    Input a -> a
what   :: a }
  deriving (a -> Input b -> Input a
(a -> b) -> Input a -> Input b
(forall a b. (a -> b) -> Input a -> Input b)
-> (forall a b. a -> Input b -> Input a) -> Functor Input
forall a b. a -> Input b -> Input a
forall a b. (a -> b) -> Input a -> Input b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Input b -> Input a
$c<$ :: forall a b. a -> Input b -> Input a
fmap :: (a -> b) -> Input a -> Input b
$cfmap :: forall a b. (a -> b) -> Input a -> Input b
Functor, Input a -> Bool
(a -> m) -> Input a -> m
(a -> b -> b) -> b -> Input a -> b
(forall m. Monoid m => Input m -> m)
-> (forall m a. Monoid m => (a -> m) -> Input a -> m)
-> (forall m a. Monoid m => (a -> m) -> Input a -> m)
-> (forall a b. (a -> b -> b) -> b -> Input a -> b)
-> (forall a b. (a -> b -> b) -> b -> Input a -> b)
-> (forall b a. (b -> a -> b) -> b -> Input a -> b)
-> (forall b a. (b -> a -> b) -> b -> Input a -> b)
-> (forall a. (a -> a -> a) -> Input a -> a)
-> (forall a. (a -> a -> a) -> Input a -> a)
-> (forall a. Input a -> [a])
-> (forall a. Input a -> Bool)
-> (forall a. Input a -> Int)
-> (forall a. Eq a => a -> Input a -> Bool)
-> (forall a. Ord a => Input a -> a)
-> (forall a. Ord a => Input a -> a)
-> (forall a. Num a => Input a -> a)
-> (forall a. Num a => Input a -> a)
-> Foldable Input
forall a. Eq a => a -> Input a -> Bool
forall a. Num a => Input a -> a
forall a. Ord a => Input a -> a
forall m. Monoid m => Input m -> m
forall a. Input a -> Bool
forall a. Input a -> Int
forall a. Input a -> [a]
forall a. (a -> a -> a) -> Input a -> a
forall m a. Monoid m => (a -> m) -> Input a -> m
forall b a. (b -> a -> b) -> b -> Input a -> b
forall a b. (a -> b -> b) -> b -> Input a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Input a -> a
$cproduct :: forall a. Num a => Input a -> a
sum :: Input a -> a
$csum :: forall a. Num a => Input a -> a
minimum :: Input a -> a
$cminimum :: forall a. Ord a => Input a -> a
maximum :: Input a -> a
$cmaximum :: forall a. Ord a => Input a -> a
elem :: a -> Input a -> Bool
$celem :: forall a. Eq a => a -> Input a -> Bool
length :: Input a -> Int
$clength :: forall a. Input a -> Int
null :: Input a -> Bool
$cnull :: forall a. Input a -> Bool
toList :: Input a -> [a]
$ctoList :: forall a. Input a -> [a]
foldl1 :: (a -> a -> a) -> Input a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Input a -> a
foldr1 :: (a -> a -> a) -> Input a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Input a -> a
foldl' :: (b -> a -> b) -> b -> Input a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Input a -> b
foldl :: (b -> a -> b) -> b -> Input a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Input a -> b
foldr' :: (a -> b -> b) -> b -> Input a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Input a -> b
foldr :: (a -> b -> b) -> b -> Input a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Input a -> b
foldMap' :: (a -> m) -> Input a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Input a -> m
foldMap :: (a -> m) -> Input a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Input a -> m
fold :: Input m -> m
$cfold :: forall m. Monoid m => Input m -> m
Foldable, Functor Input
Foldable Input
Functor Input
-> Foldable Input
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Input a -> f (Input b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Input (f a) -> f (Input a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Input a -> m (Input b))
-> (forall (m :: * -> *) a. Monad m => Input (m a) -> m (Input a))
-> Traversable Input
(a -> f b) -> Input a -> f (Input b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Input (m a) -> m (Input a)
forall (f :: * -> *) a. Applicative f => Input (f a) -> f (Input a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Input a -> m (Input b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Input a -> f (Input b)
sequence :: Input (m a) -> m (Input a)
$csequence :: forall (m :: * -> *) a. Monad m => Input (m a) -> m (Input a)
mapM :: (a -> m b) -> Input a -> m (Input b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Input a -> m (Input b)
sequenceA :: Input (f a) -> f (Input a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Input (f a) -> f (Input a)
traverse :: (a -> f b) -> Input a -> f (Input b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Input a -> f (Input b)
$cp2Traversable :: Foldable Input
$cp1Traversable :: Functor Input
Traversable)

data InputSource =
    Unknown
  | FromFile String Int
  | Inference String String [Input Form]

type Problem a = [Input a]

----------------------------------------------------------------------
-- Symbolic stuff

-- A universe of types with typecase
data TypeOf a where
  Form :: TypeOf Form
  Clause_ :: TypeOf Clause
  Term :: TypeOf Term
  Atomic :: TypeOf Atomic
  Signed :: (Symbolic a, Symbolic (Signed a)) => TypeOf (Signed a)
  Bind_ :: (Symbolic a, Symbolic (Bind a)) => TypeOf (Bind a)
  List :: (Symbolic a, Symbolic [a]) => TypeOf [a]
  Input_ :: (Symbolic a, Symbolic (Input a)) => TypeOf (Input a)
  CNF_ :: TypeOf CNF

class Symbolic a where
  typeOf :: a -> TypeOf a

instance Symbolic Form where typeOf :: Form -> TypeOf Form
typeOf Form
_ = TypeOf Form
Form
instance Symbolic Clause where typeOf :: Clause -> TypeOf Clause
typeOf Clause
_ = TypeOf Clause
Clause_
instance Symbolic Term where typeOf :: Term -> TypeOf Term
typeOf Term
_ = TypeOf Term
Term
instance Symbolic Atomic where typeOf :: Atomic -> TypeOf Atomic
typeOf Atomic
_ = TypeOf Atomic
Atomic
instance Symbolic a => Symbolic (Signed a) where typeOf :: Signed a -> TypeOf (Signed a)
typeOf Signed a
_ = TypeOf (Signed a)
forall a. (Symbolic a, Symbolic (Signed a)) => TypeOf (Signed a)
Signed
instance Symbolic a => Symbolic (Bind a) where typeOf :: Bind a -> TypeOf (Bind a)
typeOf Bind a
_ = TypeOf (Bind a)
forall a. (Symbolic a, Symbolic (Bind a)) => TypeOf (Bind a)
Bind_
instance Symbolic a => Symbolic [a] where typeOf :: [a] -> TypeOf [a]
typeOf [a]
_ = TypeOf [a]
forall a. (Symbolic a, Symbolic [a]) => TypeOf [a]
List
instance Symbolic a => Symbolic (Input a) where typeOf :: Input a -> TypeOf (Input a)
typeOf Input a
_ = TypeOf (Input a)
forall a. (Symbolic a, Symbolic (Input a)) => TypeOf (Input a)
Input_
instance Symbolic CNF where typeOf :: CNF -> TypeOf CNF
typeOf CNF
_ = TypeOf CNF
CNF_

-- Generic representations of values.
data Rep a where
  Const :: !a -> Rep a
  Unary :: Symbolic a => (a -> b) -> a -> Rep b
  Binary :: (Symbolic a, Symbolic b) => (a -> b -> c) -> a -> b -> Rep c

-- This inline declaration is crucial so that
-- pattern-matching on a rep degenerates into typecase.
{-# INLINE rep #-}
rep :: Symbolic a => a -> Rep a
rep :: a -> Rep a
rep a
x =
  case a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
x of
    TypeOf a
Form -> a -> Rep a
forall a. Unpack a => a -> Rep a
rep' a
x
    TypeOf a
Clause_ -> a -> Rep a
forall a. Unpack a => a -> Rep a
rep' a
x
    TypeOf a
Term -> a -> Rep a
forall a. Unpack a => a -> Rep a
rep' a
x
    TypeOf a
Atomic -> a -> Rep a
forall a. Unpack a => a -> Rep a
rep' a
x
    TypeOf a
Signed -> a -> Rep a
forall a. Unpack a => a -> Rep a
rep' a
x
    TypeOf a
Bind_ -> a -> Rep a
forall a. Unpack a => a -> Rep a
rep' a
x
    TypeOf a
List -> a -> Rep a
forall a. Unpack a => a -> Rep a
rep' a
x
    TypeOf a
Input_ -> a -> Rep a
forall a. Unpack a => a -> Rep a
rep' a
x
    TypeOf a
CNF_ -> a -> Rep a
forall a. Unpack a => a -> Rep a
rep' a
x

-- Implementation of rep for all types
class Unpack a where
  rep' :: a -> Rep a

instance Unpack Form where
  rep' :: Form -> Rep Form
rep' (Literal Literal
l) = (Literal -> Form) -> Literal -> Rep Form
forall a b. Symbolic a => (a -> b) -> a -> Rep b
Unary Literal -> Form
Literal Literal
l
  rep' (Not Form
t) = (Form -> Form) -> Form -> Rep Form
forall a b. Symbolic a => (a -> b) -> a -> Rep b
Unary Form -> Form
Not Form
t
  rep' (And [Form]
ts) = ([Form] -> Form) -> [Form] -> Rep Form
forall a b. Symbolic a => (a -> b) -> a -> Rep b
Unary [Form] -> Form
And [Form]
ts
  rep' (Or [Form]
ts) = ([Form] -> Form) -> [Form] -> Rep Form
forall a b. Symbolic a => (a -> b) -> a -> Rep b
Unary [Form] -> Form
Or [Form]
ts
  rep' (Equiv Form
t Form
u) = (Form -> Form -> Form) -> Form -> Form -> Rep Form
forall a b c.
(Symbolic a, Symbolic b) =>
(a -> b -> c) -> a -> b -> Rep c
Binary Form -> Form -> Form
Equiv Form
t Form
u
  rep' (ForAll Bind Form
b) = (Bind Form -> Form) -> Bind Form -> Rep Form
forall a b. Symbolic a => (a -> b) -> a -> Rep b
Unary Bind Form -> Form
ForAll Bind Form
b
  rep' (Exists Bind Form
b) = (Bind Form -> Form) -> Bind Form -> Rep Form
forall a b. Symbolic a => (a -> b) -> a -> Rep b
Unary Bind Form -> Form
Exists Bind Form
b
  rep' (Connective Connective
c Form
t Form
u) = (Form -> Form -> Form) -> Form -> Form -> Rep Form
forall a b c.
(Symbolic a, Symbolic b) =>
(a -> b -> c) -> a -> b -> Rep c
Binary (Connective -> Form -> Form -> Form
Connective Connective
c) Form
t Form
u

instance Unpack Clause where
  rep' :: Clause -> Rep Clause
rep' (Clause Bind [Literal]
ls) = (Bind [Literal] -> Clause) -> Bind [Literal] -> Rep Clause
forall a b. Symbolic a => (a -> b) -> a -> Rep b
Unary Bind [Literal] -> Clause
Clause Bind [Literal]
ls

instance Unpack Term where
  rep' :: Term -> Rep Term
rep' t :: Term
t@Var{} = Term -> Rep Term
forall a. a -> Rep a
Const Term
t
  rep' (Function
f :@: [Term]
ts) = ([Term] -> Term) -> [Term] -> Rep Term
forall a b. Symbolic a => (a -> b) -> a -> Rep b
Unary (Function
f Function -> [Term] -> Term
:@:) [Term]
ts

instance Unpack Atomic where
  rep' :: Atomic -> Rep Atomic
rep' (Term
t :=: Term
u) = (Term -> Term -> Atomic) -> Term -> Term -> Rep Atomic
forall a b c.
(Symbolic a, Symbolic b) =>
(a -> b -> c) -> a -> b -> Rep c
Binary Term -> Term -> Atomic
(:=:) Term
t Term
u
  rep' (Tru Term
p) = (Term -> Atomic) -> Term -> Rep Atomic
forall a b. Symbolic a => (a -> b) -> a -> Rep b
Unary Term -> Atomic
Tru Term
p

instance Symbolic a => Unpack (Signed a) where
  rep' :: Signed a -> Rep (Signed a)
rep' (Pos a
x) = (a -> Signed a) -> a -> Rep (Signed a)
forall a b. Symbolic a => (a -> b) -> a -> Rep b
Unary a -> Signed a
forall a. a -> Signed a
Pos a
x
  rep' (Neg a
x) = (a -> Signed a) -> a -> Rep (Signed a)
forall a b. Symbolic a => (a -> b) -> a -> Rep b
Unary a -> Signed a
forall a. a -> Signed a
Neg a
x

instance Symbolic a => Unpack (Bind a) where
  rep' :: Bind a -> Rep (Bind a)
rep' (Bind Set Variable
vs a
x) = (a -> Bind a) -> a -> Rep (Bind a)
forall a b. Symbolic a => (a -> b) -> a -> Rep b
Unary (Set Variable -> a -> Bind a
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs) a
x

instance Symbolic a => Unpack [a] where
  rep' :: [a] -> Rep [a]
rep' [] = [a] -> Rep [a]
forall a. a -> Rep a
Const []
  rep' (a
x:[a]
xs) = (a -> [a] -> [a]) -> a -> [a] -> Rep [a]
forall a b c.
(Symbolic a, Symbolic b) =>
(a -> b -> c) -> a -> b -> Rep c
Binary (:) a
x [a]
xs

instance Symbolic a => Unpack (Input a) where
  rep' :: Input a -> Rep (Input a)
rep' (Input [Char]
tag Kind
kind InputSource
info a
what) = (a -> Input a) -> a -> Rep (Input a)
forall a b. Symbolic a => (a -> b) -> a -> Rep b
Unary ([Char] -> Kind -> InputSource -> a -> Input a
forall a. [Char] -> Kind -> InputSource -> a -> Input a
Input [Char]
tag Kind
kind InputSource
info) a
what

instance Unpack CNF where
  rep' :: CNF -> Rep CNF
rep' (CNF [Input Clause]
ax [[Input Clause]]
conj Maybe Model -> Answer
s1 Maybe Model -> Answer
s2) =
    ([Input Clause] -> [[Input Clause]] -> CNF)
-> [Input Clause] -> [[Input Clause]] -> Rep CNF
forall a b c.
(Symbolic a, Symbolic b) =>
(a -> b -> c) -> a -> b -> Rep c
Binary (\[Input Clause]
ax' [[Input Clause]]
conj' -> [Input Clause]
-> [[Input Clause]]
-> (Maybe Model -> Answer)
-> (Maybe Model -> Answer)
-> CNF
CNF [Input Clause]
ax' [[Input Clause]]
conj' Maybe Model -> Answer
s1 Maybe Model -> Answer
s2) [Input Clause]
ax [[Input Clause]]
conj

-- Little generic strategies

{-# INLINE recursively #-}
recursively :: Symbolic a => (forall a. Symbolic a => a -> a) -> a -> a
recursively :: (forall a. Symbolic a => a -> a) -> a -> a
recursively forall a. Symbolic a => a -> a
h a
t =
  case a -> Rep a
forall a. Symbolic a => a -> Rep a
rep a
t of
    Const a
x -> a
x
    Unary a -> a
f a
x -> a -> a
f (a -> a
forall a. Symbolic a => a -> a
h a
x)
    Binary a -> b -> a
f a
x b
y -> a -> b -> a
f (a -> a
forall a. Symbolic a => a -> a
h a
x) (b -> b
forall a. Symbolic a => a -> a
h b
y)

{-# INLINE recursivelyM #-}
recursivelyM :: (Monad m, Symbolic a) => (forall a. Symbolic a => a -> m a) -> a -> m a
recursivelyM :: (forall a. Symbolic a => a -> m a) -> a -> m a
recursivelyM forall a. Symbolic a => a -> m a
h a
t =
  case a -> Rep a
forall a. Symbolic a => a -> Rep a
rep a
t of
    Const a
x -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
    Unary a -> a
f a
x -> (a -> a) -> m a -> m a
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM a -> a
f (a -> m a
forall a. Symbolic a => a -> m a
h a
x)
    Binary a -> b -> a
f a
x b
y -> (a -> b -> a) -> m a -> m b -> m a
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 a -> b -> a
f (a -> m a
forall a. Symbolic a => a -> m a
h a
x) (b -> m b
forall a. Symbolic a => a -> m a
h b
y)

{-# INLINE collect #-}
collect :: (Symbolic a, Monoid b) => (forall a. Symbolic a => a -> b) -> a -> b
collect :: (forall a. Symbolic a => a -> b) -> a -> b
collect forall a. Symbolic a => a -> b
h a
t =
  case a -> Rep a
forall a. Symbolic a => a -> Rep a
rep a
t of
    Const a
_x -> b
forall a. Monoid a => a
mempty
    Unary a -> a
_f a
x -> a -> b
forall a. Symbolic a => a -> b
h a
x
    Binary a -> b -> a
_f a
x b
y -> a -> b
forall a. Symbolic a => a -> b
h a
x b -> b -> b
forall a. Monoid a => a -> a -> a
`mappend` b -> b
forall a. Symbolic a => a -> b
h b
y

----------------------------------------------------------------------
-- Substitutions

type Subst = Map Variable Term

ids :: Subst
ids :: Subst
ids = Subst
forall k a. Map k a
Map.empty

(|=>) :: Variable -> Term -> Subst
Variable
v |=> :: Variable -> Term -> Subst
|=> Term
x = Variable -> Term -> Subst
forall k a. k -> a -> Map k a
Map.singleton Variable
v Term
x

(|+|) :: Subst -> Subst -> Subst
|+| :: Subst -> Subst -> Subst
(|+|) = Subst -> Subst -> Subst
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union

subst :: Symbolic a => Subst -> a -> a
subst :: Subst -> a -> a
subst Subst
s a
t =
  case a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
t of
    TypeOf a
Term -> Term -> Term
term a
Term
t
    TypeOf a
Bind_ -> Bind a -> Bind a
forall a. Symbolic a => Bind a -> Bind a
bind a
Bind a
t
    TypeOf a
_ -> a -> a
forall a. Symbolic a => a -> a
generic a
t
  where
    term :: Term -> Term
term (Var Variable
x)
      | Just Term
u <- Variable -> Subst -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Variable
x Subst
s = Term
u
    term Term
t = Term -> Term
forall a. Symbolic a => a -> a
generic Term
t

    bind :: Symbolic a => Bind a -> Bind a
    bind :: Bind a -> Bind a
bind (Bind Set Variable
vs a
t) =
      Set Variable -> a -> Bind a
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs (Subst -> a -> a
forall a. Symbolic a => Subst -> a -> a
subst (Set Variable -> Subst -> Subst
checkBinder Set Variable
vs (Subst
s Subst -> Map Variable () -> Subst
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.\\ Map Variable ()
vs')) a
t)
      where
        vs' :: Map Variable ()
vs' = (Variable -> ()) -> Set Variable -> Map Variable ()
forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (() -> Variable -> ()
forall a b. a -> b -> a
const ()) Set Variable
vs

    generic :: Symbolic a => a -> a
    generic :: a -> a
generic a
t = (forall a. Symbolic a => a -> a) -> a -> a
forall a. Symbolic a => (forall a. Symbolic a => a -> a) -> a -> a
recursively (Subst -> a -> a
forall a. Symbolic a => Subst -> a -> a
subst Subst
s) a
t

match :: Term -> Term -> Maybe Subst
match :: Term -> Term -> Maybe Subst
match Term
pat Term
t = StateT Subst Maybe () -> Subst -> Maybe Subst
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Term -> Term -> StateT Subst Maybe ()
forall (m :: * -> *).
MonadPlus m =>
Term -> Term -> StateT Subst m ()
matchM Term
pat Term
t) Subst
ids
  where
    matchM :: Term -> Term -> StateT Subst m ()
matchM (Var Variable
x) Term
t = do
      Subst
sub <- StateT Subst m Subst
forall (m :: * -> *) s. Monad m => StateT s m s
get
      case Variable -> Subst -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Variable
x Subst
sub of
        Maybe Term
Nothing -> Subst -> StateT Subst m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Subst
sub Subst -> Subst -> Subst
|+| (Variable
x Variable -> Term -> Subst
|=> Term
t))
        Just Term
u | Term
u Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
t -> () -> StateT Subst m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Maybe Term
_ -> StateT Subst m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    matchM (Function
f :@: [Term]
ts) (Function
g :@: [Term]
us) | Function
f Function -> Function -> Bool
forall a. Eq a => a -> a -> Bool
== Function
g =
      (Term -> Term -> StateT Subst m ())
-> [Term] -> [Term] -> StateT Subst m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ Term -> Term -> StateT Subst m ()
matchM [Term]
ts [Term]
us
    matchM Term
_ Term
_ = StateT Subst m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero

----------------------------------------------------------------------
-- Functions operating on symbolic terms

free :: Symbolic a => a -> Set Variable
free :: a -> Set Variable
free a
t
  | TypeOf a
Term <- a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
t,
    Var x <- a
t        = Variable -> Set Variable
var Variable
x
  | TypeOf a
Bind_ <- a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
t = Bind a -> Set Variable
forall a. Symbolic a => Bind a -> Set Variable
bind a
Bind a
t
  | Bool
otherwise         = (forall a. Symbolic a => a -> Set Variable) -> a -> Set Variable
forall a b.
(Symbolic a, Monoid b) =>
(forall a. Symbolic a => a -> b) -> a -> b
collect forall a. Symbolic a => a -> Set Variable
free a
t
  where
    var :: Variable -> Set Variable
    var :: Variable -> Set Variable
var Variable
x = Variable -> Set Variable
forall a. a -> Set a
Set.singleton Variable
x

    bind :: Symbolic a => Bind a -> Set Variable
    bind :: Bind a -> Set Variable
bind (Bind Set Variable
vs a
t) = a -> Set Variable
forall a. Symbolic a => a -> Set Variable
free a
t Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Variable
vs

ground :: Symbolic a => a -> Bool
ground :: a -> Bool
ground = Set Variable -> Bool
forall a. Set a -> Bool
Set.null (Set Variable -> Bool) -> (a -> Set Variable) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set Variable
forall a. Symbolic a => a -> Set Variable
free

bind :: Symbolic a => a -> Bind a
bind :: a -> Bind a
bind a
x = Set Variable -> a -> Bind a
forall a. Set Variable -> a -> Bind a
Bind (a -> Set Variable
forall a. Symbolic a => a -> Set Variable
free a
x) a
x

-- Helper function for collecting information from terms and binders.
termsAndBinders :: forall a b.
                   Symbolic a =>
                   (Term -> DList b) ->
                   (forall a. Symbolic a => Bind a -> [b]) ->
                   a -> [b]
termsAndBinders :: (Term -> DList b)
-> (forall a. Symbolic a => Bind a -> [b]) -> a -> [b]
termsAndBinders Term -> DList b
term forall a. Symbolic a => Bind a -> [b]
bind = DList b -> [b]
forall a. DList a -> [a]
DList.toList (DList b -> [b]) -> (a -> DList b) -> a -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> DList b
forall c. Symbolic c => c -> DList b
aux where
  aux :: Symbolic c => c -> DList b
  aux :: c -> DList b
aux c
t =
    (forall c. Symbolic c => c -> DList b) -> c -> DList b
forall a b.
(Symbolic a, Monoid b) =>
(forall a. Symbolic a => a -> b) -> a -> b
collect forall c. Symbolic c => c -> DList b
aux c
t DList b -> DList b -> DList b
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
    case c -> TypeOf c
forall a. Symbolic a => a -> TypeOf a
typeOf c
t of
      TypeOf c
Term -> Term -> DList b
term c
Term
t
      TypeOf c
Bind_ -> [b] -> DList b
forall a. [a] -> DList a
DList.fromList (Bind a -> [b]
forall a. Symbolic a => Bind a -> [b]
bind c
Bind a
t)
      TypeOf c
_ -> DList b
forall (m :: * -> *) a. MonadPlus m => m a
mzero

names :: Symbolic a => a -> [Name]
names :: a -> [Name]
names = [Name] -> [Name]
forall a. Ord a => [a] -> [a]
usort ([Name] -> [Name]) -> (a -> [Name]) -> a -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> DList Name)
-> (forall a. Symbolic a => Bind a -> [Name]) -> a -> [Name]
forall a b.
Symbolic a =>
(Term -> DList b)
-> (forall a. Symbolic a => Bind a -> [b]) -> a -> [b]
termsAndBinders Term -> DList Name
forall a. (Named a, Typed a) => a -> DList Name
term forall a. Symbolic a => Bind a -> [Name]
bind where
  term :: a -> DList Name
term a
t = [Name] -> DList Name
forall a. [a] -> DList a
DList.fromList (a -> [Name]
forall a. Named a => a -> [Name]
allNames a
t) DList Name -> DList Name -> DList Name
forall a. Monoid a => a -> a -> a
`mappend` [Name] -> DList Name
forall a. [a] -> DList a
DList.fromList (Type -> [Name]
forall a. Named a => a -> [Name]
allNames (a -> Type
forall a. Typed a => a -> Type
typ a
t))

  bind :: Symbolic a => Bind a -> [Name]
  bind :: Bind a -> [Name]
bind (Bind Set Variable
vs a
_) = (Variable -> Name) -> [Variable] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Name
forall a. Named a => a -> Name
name (Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList Set Variable
vs)

run :: Symbolic a => a -> (a -> NameM b) -> b
run :: a -> (a -> NameM b) -> b
run a
x a -> NameM b
f = [Name] -> NameM b -> b
forall a. [Name] -> NameM a -> a
runNameM (a -> [Name]
forall a. Symbolic a => a -> [Name]
names a
x) (a -> NameM b
f a
x)

run_ :: Symbolic a => a -> NameM b -> b
run_ :: a -> NameM b -> b
run_ a
x NameM b
mx = a -> (a -> NameM b) -> b
forall a b. Symbolic a => a -> (a -> NameM b) -> b
run a
x (NameM b -> a -> NameM b
forall a b. a -> b -> a
const NameM b
mx)

types :: Symbolic a => a -> [Type]
types :: a -> [Type]
types = [Type] -> [Type]
forall a. Ord a => [a] -> [a]
usort ([Type] -> [Type]) -> (a -> [Type]) -> a -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> DList Type)
-> (forall a. Symbolic a => Bind a -> [Type]) -> a -> [Type]
forall a b.
Symbolic a =>
(Term -> DList b)
-> (forall a. Symbolic a => Bind a -> [b]) -> a -> [b]
termsAndBinders Term -> DList Type
forall (m :: * -> *) a. (Monad m, Typed a) => a -> m Type
term forall a. Symbolic a => Bind a -> [Type]
bind where
  term :: a -> m Type
term a
t = Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Type
forall a. Typed a => a -> Type
typ a
t)

  bind :: Symbolic a => Bind a -> [Type]
  bind :: Bind a -> [Type]
bind (Bind Set Variable
vs a
_) = (Variable -> Type) -> [Variable] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Type
forall a. Typed a => a -> Type
typ (Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList Set Variable
vs)

types' :: Symbolic a => a -> [Type]
types' :: a -> [Type]
types' = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter (Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
O) ([Type] -> [Type]) -> (a -> [Type]) -> a -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [Type]
forall a. Symbolic a => a -> [Type]
types

terms :: Symbolic a => a -> [Term]
terms :: a -> [Term]
terms = [Term] -> [Term]
forall a. Ord a => [a] -> [a]
usort ([Term] -> [Term]) -> (a -> [Term]) -> a -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> DList Term)
-> (forall a. Symbolic a => Bind a -> [Term]) -> a -> [Term]
forall a b.
Symbolic a =>
(Term -> DList b)
-> (forall a. Symbolic a => Bind a -> [b]) -> a -> [b]
termsAndBinders Term -> DList Term
forall (m :: * -> *) a. Monad m => a -> m a
term forall a. Monoid a => a
forall a. Symbolic a => Bind a -> [Term]
mempty where
  term :: a -> m a
term a
t = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
t

vars :: Symbolic a => a -> [Variable]
vars :: a -> [Variable]
vars = [Variable] -> [Variable]
forall a. Ord a => [a] -> [a]
usort ([Variable] -> [Variable]) -> (a -> [Variable]) -> a -> [Variable]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> DList Variable)
-> (forall a. Symbolic a => Bind a -> [Variable])
-> a
-> [Variable]
forall a b.
Symbolic a =>
(Term -> DList b)
-> (forall a. Symbolic a => Bind a -> [b]) -> a -> [b]
termsAndBinders Term -> DList Variable
forall (m :: * -> *).
(Monad m, Monoid (m Variable)) =>
Term -> m Variable
term forall a. Symbolic a => Bind a -> [Variable]
bind where
  term :: Term -> m Variable
term (Var Variable
x) = Variable -> m Variable
forall (m :: * -> *) a. Monad m => a -> m a
return Variable
x
  term Term
_ = m Variable
forall a. Monoid a => a
mempty

  bind :: Symbolic a => Bind a -> [Variable]
  bind :: Bind a -> [Variable]
bind (Bind Set Variable
vs a
_) = Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList Set Variable
vs

functions :: Symbolic a => a -> [Function]
functions :: a -> [Function]
functions = [Function] -> [Function]
forall a. Ord a => [a] -> [a]
usort ([Function] -> [Function]) -> (a -> [Function]) -> a -> [Function]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> DList Function)
-> (forall a. Symbolic a => Bind a -> [Function])
-> a
-> [Function]
forall a b.
Symbolic a =>
(Term -> DList b)
-> (forall a. Symbolic a => Bind a -> [b]) -> a -> [b]
termsAndBinders Term -> DList Function
forall (m :: * -> *).
(Monad m, Monoid (m Function)) =>
Term -> m Function
term forall a. Monoid a => a
forall a. Symbolic a => Bind a -> [Function]
mempty where
  term :: Term -> m Function
term (Function
f :@: [Term]
_) = Function -> m Function
forall (m :: * -> *) a. Monad m => a -> m a
return Function
f
  term Term
_ = m Function
forall a. Monoid a => a
mempty

funOcc :: Symbolic a => Function -> a -> Int
funOcc :: Function -> a -> Int
funOcc Function
f a
x = Sum Int -> Int
forall a. Sum a -> a
getSum (a -> Sum Int
forall a. Symbolic a => a -> Sum Int
occ a
x)
  where
    occ :: Symbolic a => a -> Sum Int
    occ :: a -> Sum Int
occ a
x = (forall a. Symbolic a => a -> Sum Int) -> a -> Sum Int
forall a b.
(Symbolic a, Monoid b) =>
(forall a. Symbolic a => a -> b) -> a -> b
collect forall a. Symbolic a => a -> Sum Int
occ a
x Sum Int -> Sum Int -> Sum Int
forall a. Monoid a => a -> a -> a
`mappend` a -> Sum Int
forall a. Symbolic a => a -> Sum Int
occ1 a
x

    occ1 :: Symbolic a => a -> Sum Int
    occ1 :: a -> Sum Int
occ1 a
x
      | TypeOf a
Term <- a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
x,
        g :@: _ <- a
x,
        Function
f Function -> Function -> Bool
forall a. Eq a => a -> a -> Bool
== Function
g = Int -> Sum Int
forall a. a -> Sum a
Sum Int
1
      | Bool
otherwise = Sum Int
forall a. Monoid a => a
mempty

funsOcc :: Symbolic a => a -> Map Function Int
funsOcc :: a -> Map Function Int
funsOcc =
  [(Function, Int)] -> Map Function Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Function, Int)] -> Map Function Int)
-> (a -> [(Function, Int)]) -> a -> Map Function Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Function] -> (Function, Int))
-> [[Function]] -> [(Function, Int)]
forall a b. (a -> b) -> [a] -> [b]
map [Function] -> (Function, Int)
forall a. [a] -> (a, Int)
f ([[Function]] -> [(Function, Int)])
-> (a -> [[Function]]) -> a -> [(Function, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Function] -> [[Function]]
forall a. Eq a => [a] -> [[a]]
group ([Function] -> [[Function]])
-> (a -> [Function]) -> a -> [[Function]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Function] -> [Function]
forall a. Ord a => [a] -> [a]
sort ([Function] -> [Function]) -> (a -> [Function]) -> a -> [Function]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> DList Function)
-> (forall a. Symbolic a => Bind a -> [Function])
-> a
-> [Function]
forall a b.
Symbolic a =>
(Term -> DList b)
-> (forall a. Symbolic a => Bind a -> [b]) -> a -> [b]
termsAndBinders Term -> DList Function
forall (m :: * -> *).
(Monad m, Monoid (m Function)) =>
Term -> m Function
term forall a. Monoid a => a
forall a. Symbolic a => Bind a -> [Function]
mempty
  where
    term :: Term -> m Function
term (Function
f :@: [Term]
_) = Function -> m Function
forall (m :: * -> *) a. Monad m => a -> m a
return Function
f
    term Term
_ = m Function
forall a. Monoid a => a
mempty

    f :: [a] -> (a, Int)
f xs :: [a]
xs@(a
x:[a]
_) = (a
x, [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs)

isFof :: Symbolic a => a -> Bool
isFof :: a -> Bool
isFof a
f = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (a -> [Type]
forall a. Symbolic a => a -> [Type]
types' a
f) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1

eraseTypes :: Symbolic a => a -> a
eraseTypes :: a -> a
eraseTypes a
x =
  (Type -> Type) -> a -> a
forall a. Symbolic a => (Type -> Type) -> a -> a
mapType (\Type
ty -> if Type
ty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
O then Type
ty else Type
indType) a
x

uniqueNames :: Symbolic a => a -> NameM a
uniqueNames :: a -> NameM a
uniqueNames a
t = StateT (Map Name Type) NameM a -> Map Name Type -> NameM a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Subst -> a -> StateT (Map Name Type) NameM a
forall a.
Symbolic a =>
Subst -> a -> StateT (Map Name Type) NameM a
aux Subst
forall k a. Map k a
Map.empty a
t) ([(Name, Type)] -> Map Name Type
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Name
x, Type
t) | Name
x ::: Type
t <- Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList (a -> Set Variable
forall a. Symbolic a => a -> Set Variable
free a
t)])
  where aux :: Symbolic a => Subst -> a -> StateT (Map Name Type) NameM a
        aux :: Subst -> a -> StateT (Map Name Type) NameM a
aux Subst
s a
t =
          case a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
t of
            TypeOf a
Term -> Subst -> Term -> StateT (Map Name Type) NameM Term
term Subst
s a
Term
t
            TypeOf a
Bind_ -> Subst -> Bind a -> StateT (Map Name Type) NameM (Bind a)
forall a.
Symbolic a =>
Subst -> Bind a -> StateT (Map Name Type) NameM (Bind a)
bind Subst
s a
Bind a
t
            TypeOf a
_ -> Subst -> a -> StateT (Map Name Type) NameM a
forall a.
Symbolic a =>
Subst -> a -> StateT (Map Name Type) NameM a
generic Subst
s a
t

        term :: Subst -> Term -> StateT (Map Name Type) NameM Term
        term :: Subst -> Term -> StateT (Map Name Type) NameM Term
term Subst
s t :: Term
t@(Var Variable
x) = do
          case Variable -> Subst -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Variable
x Subst
s of
            Maybe Term
Nothing -> Term -> StateT (Map Name Type) NameM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
            Just Term
u -> Term -> StateT (Map Name Type) NameM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
        term Subst
s Term
t = Subst -> Term -> StateT (Map Name Type) NameM Term
forall a.
Symbolic a =>
Subst -> a -> StateT (Map Name Type) NameM a
generic Subst
s Term
t

        bind :: Symbolic a => Subst -> Bind a -> StateT (Map Name Type) NameM (Bind a)
        bind :: Subst -> Bind a -> StateT (Map Name Type) NameM (Bind a)
bind Subst
s (Bind Set Variable
vs a
x) = do
          Map Name Type
used <- StateT (Map Name Type) NameM (Map Name Type)
forall (m :: * -> *) s. Monad m => StateT s m s
get
          let ([Variable]
stale, [Variable]
fresh) = (Variable -> Bool) -> [Variable] -> ([Variable], [Variable])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((Name -> Map Name Type -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map Name Type
used) (Name -> Bool) -> (Variable -> Name) -> Variable -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable -> Name
forall a b. (a ::: b) -> a
lhs) (Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList Set Variable
vs)
              tuple :: (a ::: b) -> (a, b)
tuple (a
x ::: b
y) = (a
x, b
y)
          [Variable]
stale' <- [StateT (Map Name Type) NameM Variable]
-> StateT (Map Name Type) NameM [Variable]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ NameM Variable -> StateT (Map Name Type) NameM Variable
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Name -> Type -> NameM Variable
forall a b. Named a => a -> b -> NameM (Name ::: b)
newSymbol Name
x Type
t) | Name
x ::: Type
t <- [Variable]
stale ]
          Map Name Type -> StateT (Map Name Type) NameM ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Map Name Type
used Map Name Type -> Map Name Type -> Map Name Type
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` [(Name, Type)] -> Map Name Type
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ((Variable -> (Name, Type)) -> [Variable] -> [(Name, Type)]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> (Name, Type)
forall a b. (a ::: b) -> (a, b)
tuple ([Variable]
fresh [Variable] -> [Variable] -> [Variable]
forall a. [a] -> [a] -> [a]
++ [Variable]
stale')))
          case [Variable]
stale of
            [] -> (a -> Bind a)
-> StateT (Map Name Type) NameM a
-> StateT (Map Name Type) NameM (Bind a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Set Variable -> a -> Bind a
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs) (Subst -> a -> StateT (Map Name Type) NameM a
forall a.
Symbolic a =>
Subst -> a -> StateT (Map Name Type) NameM a
aux Subst
s a
x)
            [Variable]
_ ->
              do
                let s' :: Subst
s' = [(Variable, Term)] -> Subst
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Variable
x, Variable -> Term
Var Variable
y) | (Variable
x, Variable
y) <- [Variable]
stale [Variable] -> [Variable] -> [(Variable, Variable)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Variable]
stale'] Subst -> Subst -> Subst
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Subst
s
                    vs' :: Set Variable
vs' = [Variable] -> Set Variable
forall a. Ord a => [a] -> Set a
Set.fromList ([Variable]
stale' [Variable] -> [Variable] -> [Variable]
forall a. [a] -> [a] -> [a]
++ [Variable]
fresh)
                (a -> Bind a)
-> StateT (Map Name Type) NameM a
-> StateT (Map Name Type) NameM (Bind a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Set Variable -> a -> Bind a
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs') (Subst -> a -> StateT (Map Name Type) NameM a
forall a.
Symbolic a =>
Subst -> a -> StateT (Map Name Type) NameM a
aux Subst
s' a
x)

        generic :: Symbolic a => Subst -> a -> StateT (Map Name Type) NameM a
        generic :: Subst -> a -> StateT (Map Name Type) NameM a
generic Subst
s a
t = (forall a. Symbolic a => a -> StateT (Map Name Type) NameM a)
-> a -> StateT (Map Name Type) NameM a
forall (m :: * -> *) a.
(Monad m, Symbolic a) =>
(forall a. Symbolic a => a -> m a) -> a -> m a
recursivelyM (Subst -> a -> StateT (Map Name Type) NameM a
forall a.
Symbolic a =>
Subst -> a -> StateT (Map Name Type) NameM a
aux Subst
s) a
t

-- Force a value.
force :: Symbolic a => a -> a
force :: a -> a
force a
x = a -> ()
forall a. Symbolic a => a -> ()
rnf a
x () -> a -> a
`seq` a
x
  where rnf :: Symbolic a => a -> ()
        rnf :: a -> ()
rnf a
x =
          case a -> Rep a
forall a. Symbolic a => a -> Rep a
rep a
x of
            Const !a
_ -> ()
            Unary a -> a
_ a
x -> a -> ()
forall a. Symbolic a => a -> ()
rnf a
x
            Binary a -> b -> a
_ a
x b
y -> a -> ()
forall a. Symbolic a => a -> ()
rnf a
x () -> () -> ()
`seq` b -> ()
forall a. Symbolic a => a -> ()
rnf b
y

-- Check that there aren't two nested binders binding the same variable
check :: Symbolic a => a -> a
check :: a -> a
check a
x | Bool -> Bool
not Bool
debugging = a
x
        | Set Variable -> a -> Bool
forall a. Symbolic a => Set Variable -> a -> Bool
check' (a -> Set Variable
forall a. Symbolic a => a -> Set Variable
free a
x) a
x = a
x
        | Bool
otherwise = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Form.check: invariant broken"
  where check' :: Symbolic a => Set Variable -> a -> Bool
        check' :: Set Variable -> a -> Bool
check' Set Variable
vars a
t =
          case a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
t of
            TypeOf a
Term -> Set Variable -> Term -> Bool
term Set Variable
vars a
Term
t
            TypeOf a
Bind_ -> Set Variable -> Bind a -> Bool
forall a. Symbolic a => Set Variable -> Bind a -> Bool
bind Set Variable
vars a
Bind a
t
            TypeOf a
_ -> Set Variable -> a -> Bool
forall a. Symbolic a => Set Variable -> a -> Bool
generic Set Variable
vars a
t

        term :: Set Variable -> Term -> Bool
        term :: Set Variable -> Term -> Bool
term Set Variable
vars (Var Variable
x) = Variable
x Variable -> Set Variable -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Variable
vars
        term Set Variable
vars Term
t = Set Variable -> Term -> Bool
forall a. Symbolic a => Set Variable -> a -> Bool
generic Set Variable
vars Term
t

        bind :: Symbolic a => Set Variable -> Bind a -> Bool
        bind :: Set Variable -> Bind a -> Bool
bind Set Variable
vars (Bind Set Variable
vs a
t) =
          Set Variable -> Bool
forall a. Set a -> Bool
Set.null (Set Variable
vs Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set Variable
vars) Bool -> Bool -> Bool
&&
          Set Variable -> a -> Bool
forall a. Symbolic a => Set Variable -> a -> Bool
check' (Set Variable
vs Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Variable
vars) a
t

        generic :: Symbolic a => Set Variable -> a -> Bool
        generic :: Set Variable -> a -> Bool
generic Set Variable
vars = All -> Bool
getAll (All -> Bool) -> (a -> All) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Symbolic a => a -> All) -> a -> All
forall a b.
(Symbolic a, Monoid b) =>
(forall a. Symbolic a => a -> b) -> a -> b
collect (Bool -> All
All (Bool -> All) -> (a -> Bool) -> a -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Variable -> a -> Bool
forall a. Symbolic a => Set Variable -> a -> Bool
check' Set Variable
vars)

-- Check that a binder doesn't capture variables from a substitution.
checkBinder :: Set Variable -> Subst -> Subst
checkBinder :: Set Variable -> Subst -> Subst
checkBinder Set Variable
vs Subst
s | Bool -> Bool
not Bool
debugging = Subst
s
                 | Set Variable -> Bool
forall a. Set a -> Bool
Set.null ([Term] -> Set Variable
forall a. Symbolic a => a -> Set Variable
free (Subst -> [Term]
forall k a. Map k a -> [a]
Map.elems Subst
s) Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set Variable
vs) = Subst
s
                 | Bool
otherwise = [Char] -> Subst
forall a. HasCallStack => [Char] -> a
error [Char]
"Form.checkBinder: capturing substitution"

-- Apply a function to each name, while preserving sharing.
mapName :: Symbolic a => (Name -> Name) -> a -> a
mapName :: (Name -> Name) -> a -> a
mapName Name -> Name
f0 = a -> a
forall a. Symbolic a => a -> a
rename
  where
    rename :: Symbolic a => a -> a
    rename :: a -> a
rename a
t =
      case a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
t of
        TypeOf a
Term -> Term -> Term
term a
Term
t
        TypeOf a
Bind_ -> Bind a -> Bind a
forall a. Symbolic a => Bind a -> Bind a
bind a
Bind a
t
        TypeOf a
_ -> (forall a. Symbolic a => a -> a) -> a -> a
forall a. Symbolic a => (forall a. Symbolic a => a -> a) -> a -> a
recursively forall a. Symbolic a => a -> a
rename a
t

    bind :: Symbolic a => Bind a -> Bind a
    bind :: Bind a -> Bind a
bind (Bind Set Variable
vs a
t) =  Set Variable -> a -> Bind a
forall a. Set Variable -> a -> Bind a
Bind ((Variable -> Variable) -> Set Variable -> Set Variable
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Variable -> Variable
var Set Variable
vs) (a -> a
forall a. Symbolic a => a -> a
rename a
t)
    term :: Term -> Term
term (Function
f :@: [Term]
ts) = Function -> Function
fun Function
f Function -> [Term] -> Term
:@: (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
term [Term]
ts
    term (Var Variable
x) = Variable -> Term
Var (Variable -> Variable
var Variable
x)

    var :: Variable -> Variable
var = (Variable -> Variable) -> Variable -> Variable
forall a b. Ord a => (a -> b) -> a -> b
memo ((Variable -> Variable) -> Variable -> Variable)
-> (Variable -> Variable) -> Variable -> Variable
forall a b. (a -> b) -> a -> b
$ \(Name
x ::: Type
ty) -> Name -> Name
f Name
x Name -> Type -> Variable
forall a b. a -> b -> a ::: b
::: Type -> Type
type_ Type
ty
    fun :: Function -> Function
fun = (Function -> Function) -> Function -> Function
forall a b. Ord a => (a -> b) -> a -> b
memo ((Function -> Function) -> Function -> Function)
-> (Function -> Function) -> Function -> Function
forall a b. (a -> b) -> a -> b
$ \(Name
x ::: FunType [Type]
args Type
res) ->
                   Name -> Name
f Name
x Name -> FunType -> Function
forall a b. a -> b -> a ::: b
::: [Type] -> Type -> FunType
FunType ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
type_ [Type]
args) (Type -> Type
type_ Type
res)
    type_ :: Type -> Type
type_ =
      (Type -> Type) -> Type -> Type
forall a b. Ord a => (a -> b) -> a -> b
memo ((Type -> Type) -> Type -> Type) -> (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ \Type
ty ->
        case Type
ty of
          Type
O -> Type
O
          Type Name
name -> Name -> Type
Type (Name -> Name
f Name
name)

    f :: Name -> Name
f = (Name -> Name) -> Name -> Name
forall a b. Ord a => (a -> b) -> a -> b
memo Name -> Name
f0

-- Apply a function to each type, while preserving sharing.
mapType :: Symbolic a => (Type -> Type) -> a -> a
mapType :: (Type -> Type) -> a -> a
mapType Type -> Type
f0 = a -> a
forall a. Symbolic a => a -> a
mapType'
  where mapType' :: Symbolic a => a -> a
        mapType' :: a -> a
mapType' a
t =
          case a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
t of
            TypeOf a
Term -> Term -> Term
term a
Term
t
            TypeOf a
Bind_ -> Bind a -> Bind a
forall a. Symbolic a => Bind a -> Bind a
bind a
Bind a
t
            TypeOf a
_ -> (forall a. Symbolic a => a -> a) -> a -> a
forall a. Symbolic a => (forall a. Symbolic a => a -> a) -> a -> a
recursively forall a. Symbolic a => a -> a
mapType' a
t

        bind :: Symbolic a => Bind a -> Bind a
        bind :: Bind a -> Bind a
bind (Bind Set Variable
vs a
t) = Set Variable -> a -> Bind a
forall a. Set Variable -> a -> Bind a
Bind ((Variable -> Variable) -> Set Variable -> Set Variable
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Variable -> Variable
var Set Variable
vs) (a -> a
forall a. Symbolic a => a -> a
mapType' a
t)

        term :: Term -> Term
term (Function
f :@: [Term]
ts) = Function -> Function
fun Function
f Function -> [Term] -> Term
:@: (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Term
term [Term]
ts
        term (Var Variable
x) = Variable -> Term
Var (Variable -> Variable
var Variable
x)

        var :: Variable -> Variable
var = (Variable -> Variable) -> Variable -> Variable
forall a b. Ord a => (a -> b) -> a -> b
memo ((Variable -> Variable) -> Variable -> Variable)
-> (Variable -> Variable) -> Variable -> Variable
forall a b. (a -> b) -> a -> b
$ \(Name
x ::: Type
ty) -> Name
x Name -> Type -> Variable
forall a b. a -> b -> a ::: b
::: Type -> Type
f Type
ty
        fun :: Function -> Function
fun = (Function -> Function) -> Function -> Function
forall a b. Ord a => (a -> b) -> a -> b
memo ((Function -> Function) -> Function -> Function)
-> (Function -> Function) -> Function -> Function
forall a b. (a -> b) -> a -> b
$ \(Name
x ::: FunType [Type]
args Type
res) ->
                       Name
x Name -> FunType -> Function
forall a b. a -> b -> a ::: b
::: [Type] -> Type -> FunType
FunType ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
f [Type]
args) (Type -> Type
f Type
res)

        f :: Type -> Type
f = (Type -> Type) -> Type -> Type
forall a b. Ord a => (a -> b) -> a -> b
memo Type -> Type
f0