-- | This module is internal to QuickSpec.
--
-- Typed terms and operations on them.
{-# LANGUAGE PatternSynonyms, ViewPatterns, TypeSynonymInstances, FlexibleInstances, TypeFamilies, ConstraintKinds, DeriveGeneric, DeriveAnyClass, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, TypeOperators, DeriveFunctor, FlexibleContexts, DeriveTraversable #-}
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
module QuickSpec.Internal.Term(module QuickSpec.Internal.Term, module Twee.Base, module Twee.Pretty) where

import QuickSpec.Internal.Type
import QuickSpec.Internal.Utils
import Control.Monad
import GHC.Generics(Generic)
import Test.QuickCheck(CoArbitrary(..))
import Data.DList(DList)
import qualified Data.DList as DList
import Twee.Base(Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint)
import Twee.Pretty
import qualified Data.Map.Strict as Map
import Data.Map(Map)
import Data.List
import Data.Ord
import Data.Maybe

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

-- | A variable, which has a type and a number.
data Var = V { Var -> Type
var_ty :: !Type, Var -> Int
var_id :: {-# UNPACK #-} !Int }
  deriving (Var -> Var -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Eq Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
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 :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
Ord, Int -> Var -> ShowS
[Var] -> ShowS
Var -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> String
$cshow :: Var -> String
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> Var -> ShowS
Show, forall x. Rep Var x -> Var
forall x. Var -> Rep Var x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Var x -> Var
$cfrom :: forall x. Var -> Rep Var x
Generic)

instance CoArbitrary Var where
  coarbitrary :: forall b. Var -> Gen b -> Gen b
coarbitrary = forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Int
var_id

instance Typed Var where
  typ :: Var -> Type
typ Var
x = Var -> Type
var_ty Var
x
  otherTypesDL :: Var -> DList Type
otherTypesDL Var
_ = forall (m :: * -> *) a. MonadPlus m => m a
mzero
  typeSubst_ :: (Var -> Builder TyCon) -> Var -> Var
typeSubst_ Var -> Builder TyCon
sub (V Type
ty Int
x) = Type -> Int -> Var
V (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub Type
ty) Int
x

match :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
match :: forall f. Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
match (Var Var
x) Term f
t = forall a. a -> Maybe a
Just (forall k a. k -> a -> Map k a
Map.singleton Var
x Term f
t)
match (Fun f
f) (Fun f
g)
  | f
f forall a. Eq a => a -> a -> Bool
== f
g = forall a. a -> Maybe a
Just forall k a. Map k a
Map.empty
  | Bool
otherwise = forall a. Maybe a
Nothing
match (Term f
f :$: Term f
x) (Term f
g :$: Term f
y) = do
  Map Var (Term f)
m1 <- forall f. Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
match Term f
f Term f
g
  Map Var (Term f)
m2 <- forall f. Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
match Term f
x Term f
y
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Term f
t forall a. Eq a => a -> a -> Bool
== Term f
u | (Term f
t, Term f
u) <- forall k a. Map k a -> [a]
Map.elems (forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith (,) Map Var (Term f)
m1 Map Var (Term f)
m2)])
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Var (Term f)
m1 Map Var (Term f)
m2)

unify :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
unify :: forall f. Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
unify Term f
t Term f
u = forall {f}.
Eq f =>
Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop forall k a. Map k a
Map.empty [(Term f
t, Term f
u)]
  where
    loop :: Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop Map Var (Term f)
sub [] = forall a. a -> Maybe a
Just Map Var (Term f)
sub
    loop Map Var (Term f)
sub ((Fun f
f, Fun f
g):[(Term f, Term f)]
xs)
      | f
f forall a. Eq a => a -> a -> Bool
== f
g = Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop Map Var (Term f)
sub [(Term f, Term f)]
xs
    loop Map Var (Term f)
sub ((Term f
f :$: Term f
x, Term f
g :$: Term f
y):[(Term f, Term f)]
xs) =
      Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop Map Var (Term f)
sub ((Term f
f, Term f
g)forall a. a -> [a] -> [a]
:(Term f
x, Term f
y)forall a. a -> [a] -> [a]
:[(Term f, Term f)]
xs)
    loop Map Var (Term f)
sub ((Var Var
x, Term f
t):[(Term f, Term f)]
xs)
      | Term f
t forall a. Eq a => a -> a -> Bool
== forall f. Var -> Term f
Var Var
x = Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop Map Var (Term f)
sub [(Term f, Term f)]
xs
      | Var
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall f a. Symbolic f a => a -> [Var]
vars Term f
t = forall a. Maybe a
Nothing
      | Bool
otherwise =
        Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop
          (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
x Term f
t (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall {f}. Var -> Term f -> Term f -> Term f
replace Var
x Term f
t) Map Var (Term f)
sub))
          [(forall {f}. Var -> Term f -> Term f -> Term f
replace Var
x Term f
t Term f
u, forall {f}. Var -> Term f -> Term f -> Term f
replace Var
x Term f
t Term f
v) | (Term f
u, Term f
v) <- [(Term f, Term f)]
xs]
    loop Map Var (Term f)
sub ((Term f
t, Var Var
x):[(Term f, Term f)]
xs) = Map Var (Term f) -> [(Term f, Term f)] -> Maybe (Map Var (Term f))
loop Map Var (Term f)
sub ((forall f. Var -> Term f
Var Var
x, Term f
t)forall a. a -> [a] -> [a]
:[(Term f, Term f)]
xs)

    replace :: Var -> Term f -> Term f -> Term f
replace Var
x Term f
t (Var Var
y) | Var
x forall a. Eq a => a -> a -> Bool
== Var
y = Term f
t
    replace Var
_ Term f
_ Term f
t = Term f
t

-- | A class for things that contain terms.
class Symbolic f a | a -> f where
  -- | A different list of all terms contained in the thing.
  termsDL :: a -> DList (Term f)
  -- | Apply a substitution to all terms in the thing.
  subst :: (Var -> Term f) -> a -> a

instance Symbolic f (Term f) where
  termsDL :: Term f -> DList (Term f)
termsDL = forall (m :: * -> *) a. Monad m => a -> m a
return
  subst :: (Var -> Term f) -> Term f -> Term f
subst Var -> Term f
sub (Var Var
x) = Var -> Term f
sub Var
x
  subst Var -> Term f
_ (Fun f
x) = forall f. f -> Term f
Fun f
x
  subst Var -> Term f
sub (Term f
t :$: Term f
u) = forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst Var -> Term f
sub Term f
t forall f. Term f -> Term f -> Term f
:$: forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst Var -> Term f
sub Term f
u

instance Symbolic f a => Symbolic f [a] where
  termsDL :: [a] -> DList (Term f)
termsDL = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall f a. Symbolic f a => a -> DList (Term f)
termsDL
  subst :: (Var -> Term f) -> [a] -> [a]
subst Var -> Term f
sub = forall a b. (a -> b) -> [a] -> [b]
map (forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst Var -> Term f
sub)

class Sized a where
  size :: a -> Int

instance Sized f => Sized (Term f) where
  size :: Term f -> Int
size (Var Var
_) = Int
1
  size (Fun f
f) = forall a. Sized a => a -> Int
size f
f
  size (Term f
t :$: Term f
u) =
    forall a. Sized a => a -> Int
size Term f
t forall a. Num a => a -> a -> a
+ forall a. Sized a => a -> Int
size Term f
u forall a. Num a => a -> a -> a
+
    -- Penalise applied function variables, because they can be used
    -- to build many many terms without any constants at all
    case Term f
t of
      Var Var
_ -> Int
1
      Term f
_ -> Int
0

instance Pretty Var where
  pPrint :: Var -> Doc
pPrint Var
x = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"X" Doc -> Doc -> Doc
<#> forall a. Pretty a => a -> Doc
pPrint (Var -> Int
var_id Var
xforall a. Num a => a -> a -> a
+Int
1) Doc -> Doc -> Doc
<+> String -> Doc
text String
"::" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint (Var -> Type
var_ty Var
x)
  --pPrint x = text "X" <#> pPrint (var_id x+1)

instance PrettyTerm f => Pretty (Term f) where
  pPrintPrec :: PrettyLevel -> Rational -> Term f -> Doc
pPrintPrec PrettyLevel
l Rational
p (Var Var
x :@: [Term f]
ts) =
    TermStyle
-> forall a.
   Pretty a =>
   PrettyLevel -> Rational -> Doc -> [a] -> Doc
pPrintTerm TermStyle
curried PrettyLevel
l Rational
p (forall a. Pretty a => a -> Doc
pPrint Var
x) [Term f]
ts
  pPrintPrec PrettyLevel
l Rational
p (Fun f
f :@: [Term f]
ts) =
    TermStyle
-> forall a.
   Pretty a =>
   PrettyLevel -> Rational -> Doc -> [a] -> Doc
pPrintTerm (forall f. PrettyTerm f => f -> TermStyle
termStyle f
f) PrettyLevel
l Rational
p (forall a. Pretty a => a -> Doc
pPrint f
f) [Term f]
ts

-- | All terms contained in a `Symbolic`.
terms :: Symbolic f a => a -> [Term f]
terms :: forall f a. Symbolic f a => a -> [Term f]
terms = forall a. DList a -> [a]
DList.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f a. Symbolic f a => a -> DList (Term f)
termsDL

-- | All function symbols appearing in a `Symbolic`, in order of appearance,
-- with duplicates included.
funs :: Symbolic f a => a -> [f]
funs :: forall f a. Symbolic f a => a -> [f]
funs a
x = [ f
f | Term f
t <- forall f a. Symbolic f a => a -> [Term f]
terms a
x, Fun f
f <- forall f. Term f -> [Term f]
subterms Term f
t ]

-- | All variables appearing in a `Symbolic`, in order of appearance,
-- with duplicates included.
vars :: Symbolic f a => a -> [Var]
vars :: forall f a. Symbolic f a => a -> [Var]
vars a
x = [ Var
v | Term f
t <- forall f a. Symbolic f a => a -> [Term f]
terms a
x, Var Var
v <- forall f. Term f -> [Term f]
subterms Term f
t ]

-- | Decompose a term into a head and a list of arguments.
pattern f $b:@: :: forall {f}. Term f -> [Term f] -> Term f
$m:@: :: forall {r} {f}.
Term f -> (Term f -> [Term f] -> r) -> ((# #) -> r) -> r
:@: ts <- (getApp -> (f, ts)) where
  Term f
f :@: [Term f]
ts = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall f. Term f -> Term f -> Term f
(:$:) Term f
f [Term f]
ts

getApp :: Term f -> (Term f, [Term f])
getApp :: forall f. Term f -> (Term f, [Term f])
getApp (Term f
t :$: Term f
u) = (Term f
f, [Term f]
ts forall a. [a] -> [a] -> [a]
++ [Term f
u])
  where
    (Term f
f, [Term f]
ts) = forall f. Term f -> (Term f, [Term f])
getApp Term f
t
getApp Term f
t = (Term f
t, [])

-- | Compute the number of a variable which does /not/ appear in the `Symbolic`.
freeVar :: Symbolic f a => a -> Int
freeVar :: forall f a. Symbolic f a => a -> Int
freeVar a
x = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0forall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map (forall a. Enum a => a -> a
succ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Int
var_id) (forall f a. Symbolic f a => a -> [Var]
vars a
x))

-- | Count how many times a given function symbol occurs.
occ :: (Eq f, Symbolic f a) => f -> a -> Int
occ :: forall f a. (Eq f, Symbolic f a) => f -> a -> Int
occ f
x a
t = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
== f
x) (forall f a. Symbolic f a => a -> [f]
funs a
t))

-- | Count how many times a given variable occurs.
occVar :: Symbolic f a => Var -> a -> Int
occVar :: forall f a. Symbolic f a => Var -> a -> Int
occVar Var
x a
t = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
== Var
x) (forall f a. Symbolic f a => a -> [Var]
vars a
t))

-- | Map a function over variables.
mapVar :: (Var -> Var) -> Term f -> Term f
mapVar :: forall f. (Var -> Var) -> Term f -> Term f
mapVar Var -> Var
f (Var Var
x) = forall f. Var -> Term f
Var (Var -> Var
f Var
x)
mapVar Var -> Var
_ (Fun f
x) = forall f. f -> Term f
Fun f
x
mapVar Var -> Var
f (Term f
t :$: Term f
u) = forall f. (Var -> Var) -> Term f -> Term f
mapVar Var -> Var
f Term f
t forall f. Term f -> Term f -> Term f
:$: forall f. (Var -> Var) -> Term f -> Term f
mapVar Var -> Var
f Term f
u

-- | Map a function over function symbols.
mapFun :: (f -> g) -> Term f -> Term g
mapFun :: forall a b. (a -> b) -> Term a -> Term b
mapFun f -> g
_ (Var Var
x) = forall f. Var -> Term f
Var Var
x
mapFun f -> g
f (Fun f
x) = forall f. f -> Term f
Fun (f -> g
f f
x)
mapFun f -> g
f (Term f
t :$: Term f
u) = forall a b. (a -> b) -> Term a -> Term b
mapFun f -> g
f Term f
t forall f. Term f -> Term f -> Term f
:$: forall a b. (a -> b) -> Term a -> Term b
mapFun f -> g
f Term f
u

-- | Map a function over function symbols.
flatMapFun :: (f -> Term g) -> Term f -> Term g
flatMapFun :: forall f g. (f -> Term g) -> Term f -> Term g
flatMapFun f -> Term g
_ (Var Var
x) = forall f. Var -> Term f
Var Var
x
flatMapFun f -> Term g
f (Fun f
x) = f -> Term g
f f
x
flatMapFun f -> Term g
f (Term f
t :$: Term f
u) =
  forall f g. (f -> Term g) -> Term f -> Term g
flatMapFun f -> Term g
f Term f
t forall f. Term f -> Term f -> Term f
:$: forall f g. (f -> Term g) -> Term f -> Term g
flatMapFun f -> Term g
f Term f
u

-- | A type representing functions which may be the identity.
data OrId f = Id | NotId f

-- | Eliminate the identity function from a term.
eliminateId :: Term (OrId f) -> Maybe (Term f)
eliminateId :: forall f. Term (OrId f) -> Maybe (Term f)
eliminateId Term (OrId f)
t = do
  OrId (Term f)
t <- forall f. Term (OrId f) -> Maybe (OrId (Term f))
elim Term (OrId f)
t
  case OrId (Term f)
t of
    OrId (Term f)
Id -> forall a. Maybe a
Nothing
    NotId Term f
t -> forall a. a -> Maybe a
Just Term f
t
  where
    elim :: Term (OrId f) -> Maybe (OrId (Term f))
    elim :: forall f. Term (OrId f) -> Maybe (OrId (Term f))
elim (Var Var
x) = forall a. a -> Maybe a
Just (forall f. f -> OrId f
NotId (forall f. Var -> Term f
Var Var
x))
    elim (Fun (NotId f
f)) = forall a. a -> Maybe a
Just (forall f. f -> OrId f
NotId (forall f. f -> Term f
Fun f
f))
    elim (Fun OrId f
Id) = forall a. a -> Maybe a
Just forall f. OrId f
Id
    elim (Term (OrId f)
t :$: Term (OrId f)
u) = do
      OrId (Term f)
t <- forall f. Term (OrId f) -> Maybe (OrId (Term f))
elim Term (OrId f)
t
      OrId (Term f)
u <- forall f. Term (OrId f) -> Maybe (OrId (Term f))
elim Term (OrId f)
u
      case (OrId (Term f)
t, OrId (Term f)
u) of
        (OrId (Term f)
Id, OrId (Term f)
_) -> forall a. a -> Maybe a
Just OrId (Term f)
u
        (NotId Term f
_, OrId (Term f)
Id) -> forall a. Maybe a
Nothing
        (NotId Term f
t, NotId Term f
u) -> forall a. a -> Maybe a
Just (forall f. f -> OrId f
NotId (Term f
t forall f. Term f -> Term f -> Term f
:$: Term f
u))

-- | Find all subterms of a term. Includes the term itself.
subterms :: Term f -> [Term f]
subterms :: forall f. Term f -> [Term f]
subterms Term f
t = Term f
tforall a. a -> [a] -> [a]
:forall f. Term f -> [Term f]
properSubterms Term f
t

-- | Find all subterms of a term. Does not include the term itself.
properSubterms :: Term f -> [Term f]
properSubterms :: forall f. Term f -> [Term f]
properSubterms (Term f
t :$: Term f
u) = forall f. Term f -> [Term f]
subterms Term f
t forall a. [a] -> [a] -> [a]
++ forall f. Term f -> [Term f]
subterms Term f
u
properSubterms Term f
_ = []

subtermsFO :: Term f -> [Term f]
subtermsFO :: forall f. Term f -> [Term f]
subtermsFO Term f
t = Term f
tforall a. a -> [a] -> [a]
:forall f. Term f -> [Term f]
properSubtermsFO Term f
t

properSubtermsFO :: Term f -> [Term f]
properSubtermsFO :: forall f. Term f -> [Term f]
properSubtermsFO (Term f
_f :@: [Term f]
ts) = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall f. Term f -> [Term f]
subtermsFO [Term f]
ts
properSubtermsFO Term f
_ = []

-- | Renames variables so that they appear in a canonical order.
-- Also makes sure that variables of different types have different numbers.
canonicalise :: Symbolic fun a => a -> a
canonicalise :: forall fun a. Symbolic fun a => a -> a
canonicalise a
t = forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst (\Var
x -> forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. HasCallStack => a
undefined Var
x Map Var (Term fun)
sub) a
t
  where
    sub :: Map Var (Term fun)
sub =
      forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
        [(Var
x, forall f. Var -> Term f
Var (Type -> Int -> Var
V Type
ty Int
n))
        | (x :: Var
x@(V Type
ty Int
_), Int
n) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Eq a => [a] -> [a]
nub (forall f a. Symbolic f a => a -> [Var]
vars a
t)) [Int
0..]]

-- | Evaluate a term, given a valuation for variables and function symbols.
evalTerm :: (Typed fun, Apply a, Monad m) => (Var -> m a) -> (fun -> m a) -> Term fun -> m a
evalTerm :: forall fun a (m :: * -> *).
(Typed fun, Apply a, Monad m) =>
(Var -> m a) -> (fun -> m a) -> Term fun -> m a
evalTerm Var -> m a
var fun -> m a
fun = Term fun -> m a
eval
  where
    eval :: Term fun -> m a
eval (Var Var
x) = Var -> m a
var Var
x
    eval (Fun fun
f) = fun -> m a
fun fun
f
    eval (Term fun
t :$: Term fun
u) = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall a. Apply a => a -> a -> a
apply (Term fun -> m a
eval Term fun
t) (Term fun -> m a
eval Term fun
u)

instance Typed f => Typed (Term f) where
  typ :: Term f -> Type
typ (Var Var
x) = forall a. Typed a => a -> Type
typ Var
x
  typ (Fun f
f) = forall a. Typed a => a -> Type
typ f
f
  typ (Term f
t :$: Term f
_) = Int -> Type -> Type
typeDrop Int
1 (forall a. Typed a => a -> Type
typ Term f
t)

  otherTypesDL :: Term f -> DList Type
otherTypesDL (Var Var
_) = forall a. Monoid a => a
mempty
  otherTypesDL (Fun f
f) = forall a. Typed a => a -> DList Type
typesDL f
f
  otherTypesDL (Term f
t :$: Term f
u) = forall a. Typed a => a -> DList Type
typesDL Term f
t forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Typed a => a -> DList Type
typesDL Term f
u

  typeSubst_ :: (Var -> Builder TyCon) -> Term f -> Term f
typeSubst_ Var -> Builder TyCon
sub = Term f -> Term f
tsub
    where
      tsub :: Term f -> Term f
tsub (Var Var
x) = forall f. Var -> Term f
Var (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub Var
x)
      tsub (Fun f
f) = forall f. f -> Term f
Fun (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub f
f)
      tsub (Term f
t :$: Term f
u) =
        forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub Term f
t forall f. Term f -> Term f -> Term f
:$: forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub Term f
u

instance (PrettyTerm f, Typed f) => Apply (Term f) where
  tryApply :: Term f -> Term f -> Maybe (Term f)
tryApply Term f
t Term f
u = do
    forall a. Apply a => a -> a -> Maybe a
tryApply (forall a. Typed a => a -> Type
typ Term f
t) (forall a. Typed a => a -> Type
typ Term f
u)
    forall (m :: * -> *) a. Monad m => a -> m a
return (Term f
t forall f. Term f -> Term f -> Term f
:$: Term f
u)

depth :: Term f -> Int
depth :: forall a. Term a -> Int
depth Var{} = Int
1
depth Fun{} = Int
1
depth (Term f
t :$: Term f
u) = forall a. Term a -> Int
depth Term f
t forall a. Ord a => a -> a -> a
`max` (Int
1forall a. Num a => a -> a -> a
+forall a. Term a -> Int
depth Term f
u)

-- | A standard term ordering - size, skeleton, generality.
-- Satisfies the property:
-- if measure (schema t) < measure (schema u) then t < u.
type Measure f = (Int, Int, Int, Int, MeasureFuns f, Int, [Var])
-- | Compute the term ordering for a term.
measure :: (Sized f, Typed f) => Term f -> Measure f
measure :: forall f. (Sized f, Typed f) => Term f -> Measure f
measure Term f
t =
  (forall a. Term a -> Int
depth Term f
t, forall a. Sized a => a -> Int
size Term f
t, forall {a}. Typed a => Term a -> Int
missing Term f
t, -forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall f a. Symbolic f a => a -> [Var]
vars Term f
t), forall f. Term f -> MeasureFuns f
MeasureFuns (forall {f}. Term f -> Term f
skel Term f
t),
   -forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Ord a => [a] -> [a]
usort (forall f a. Symbolic f a => a -> [Var]
vars Term f
t)), forall f a. Symbolic f a => a -> [Var]
vars Term f
t)
  where
    skel :: Term f -> Term f
skel (Var (V Type
ty Int
_)) = forall f. Var -> Term f
Var (Type -> Int -> Var
V Type
ty Int
0)
    skel (Fun f
f) = forall f. f -> Term f
Fun f
f
    skel (Term f
t :$: Term f
u) = Term f -> Term f
skel Term f
t forall f. Term f -> Term f -> Term f
:$: Term f -> Term f
skel Term f
u
    -- Prefer fully-applied terms to partially-applied ones.
    -- This function counts how many unsaturated function applications
    -- occur in a term.
    missing :: Term a -> Int
missing (Fun a
f :@: [Term a]
ts) =
      Type -> Int
typeArity (forall a. Typed a => a -> Type
typ a
f) forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term a]
ts forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (forall a b. (a -> b) -> [a] -> [b]
map Term a -> Int
missing [Term a]
ts)
    missing (Var Var
_ :@: [Term a]
ts) =
      forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (forall a b. (a -> b) -> [a] -> [b]
map Term a -> Int
missing [Term a]
ts)

-- | A helper for `Measure`.
newtype MeasureFuns f = MeasureFuns (Term f)
instance Ord f => Eq (MeasureFuns f) where
  MeasureFuns f
t == :: MeasureFuns f -> MeasureFuns f -> Bool
== MeasureFuns f
u = forall a. Ord a => a -> a -> Ordering
compare MeasureFuns f
t MeasureFuns f
u forall a. Eq a => a -> a -> Bool
== Ordering
EQ
instance Ord f => Ord (MeasureFuns f) where
  compare :: MeasureFuns f -> MeasureFuns f -> Ordering
compare (MeasureFuns Term f
t) (MeasureFuns Term f
u) = forall f. Ord f => Term f -> Term f -> Ordering
compareFuns Term f
t Term f
u

-- | A helper for `Measure`.
compareFuns :: Ord f => Term f -> Term f -> Ordering
compareFuns :: forall f. Ord f => Term f -> Term f -> Ordering
compareFuns (Term f
f :@: [Term f]
ts) (Term f
g :@: [Term f]
us) =
  forall f. Ord f => Term f -> Term f -> Ordering
compareHead Term f
f Term f
g forall a. Monoid a => a -> a -> a
`mappend` forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (forall a b. (a -> b) -> [a] -> [b]
map forall f. Term f -> MeasureFuns f
MeasureFuns) [Term f]
ts [Term f]
us
  where
    compareHead :: Term a -> Term a -> Ordering
compareHead (Var Var
x) (Var Var
y) = forall a. Ord a => a -> a -> Ordering
compare Var
x Var
y
    compareHead (Var Var
_) Term a
_ = Ordering
LT
    compareHead Term a
_ (Var Var
_) = Ordering
GT
    compareHead (Fun a
f) (Fun a
g) = forall a. Ord a => a -> a -> Ordering
compare a
f a
g
    compareHead Term a
_ Term a
_ = forall a. HasCallStack => String -> a
error String
"viewApp"

----------------------------------------------------------------------
-- * Data types a la carte-ish.
----------------------------------------------------------------------

-- | A sum type. Intended to be used to build the type of function
-- symbols. Comes with instances that are useful for QuickSpec.
data a :+: b = Inl a | Inr b deriving ((a :+: b) -> (a :+: b) -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => (a :+: b) -> (a :+: b) -> Bool
/= :: (a :+: b) -> (a :+: b) -> Bool
$c/= :: forall a b. (Eq a, Eq b) => (a :+: b) -> (a :+: b) -> Bool
== :: (a :+: b) -> (a :+: b) -> Bool
$c== :: forall a b. (Eq a, Eq b) => (a :+: b) -> (a :+: b) -> Bool
Eq, (a :+: b) -> (a :+: b) -> Bool
(a :+: b) -> (a :+: b) -> Ordering
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} {b}. (Ord a, Ord b) => Eq (a :+: b)
forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Bool
forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Ordering
forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> a :+: b
min :: (a :+: b) -> (a :+: b) -> a :+: b
$cmin :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> a :+: b
max :: (a :+: b) -> (a :+: b) -> a :+: b
$cmax :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> a :+: b
>= :: (a :+: b) -> (a :+: b) -> Bool
$c>= :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Bool
> :: (a :+: b) -> (a :+: b) -> Bool
$c> :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Bool
<= :: (a :+: b) -> (a :+: b) -> Bool
$c<= :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Bool
< :: (a :+: b) -> (a :+: b) -> Bool
$c< :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Bool
compare :: (a :+: b) -> (a :+: b) -> Ordering
$ccompare :: forall a b. (Ord a, Ord b) => (a :+: b) -> (a :+: b) -> Ordering
Ord)

instance (Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) where
  size :: (fun1 :+: fun2) -> Int
size (Inl fun1
x) = forall a. Sized a => a -> Int
size fun1
x
  size (Inr fun2
x) = forall a. Sized a => a -> Int
size fun2
x

instance (Typed fun1, Typed fun2) => Typed (fun1 :+: fun2) where
  typ :: (fun1 :+: fun2) -> Type
typ (Inl fun1
x) = forall a. Typed a => a -> Type
typ fun1
x
  typ (Inr fun2
x) = forall a. Typed a => a -> Type
typ fun2
x
  otherTypesDL :: (fun1 :+: fun2) -> DList Type
otherTypesDL (Inl fun1
x) = forall a. Typed a => a -> DList Type
otherTypesDL fun1
x
  otherTypesDL (Inr fun2
x) = forall a. Typed a => a -> DList Type
otherTypesDL fun2
x
  typeSubst_ :: (Var -> Builder TyCon) -> (fun1 :+: fun2) -> fun1 :+: fun2
typeSubst_ Var -> Builder TyCon
sub (Inl fun1
x) = forall a b. a -> a :+: b
Inl (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub fun1
x)
  typeSubst_ Var -> Builder TyCon
sub (Inr fun2
x) = forall a b. b -> a :+: b
Inr (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub fun2
x)

instance (Pretty fun1, Pretty fun2) => Pretty (fun1 :+: fun2) where
  pPrintPrec :: PrettyLevel -> Rational -> (fun1 :+: fun2) -> Doc
pPrintPrec PrettyLevel
l Rational
p (Inl fun1
x) = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
p fun1
x
  pPrintPrec PrettyLevel
l Rational
p (Inr fun2
x) = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
p fun2
x

instance (PrettyTerm fun1, PrettyTerm fun2) => PrettyTerm (fun1 :+: fun2) where
  termStyle :: (fun1 :+: fun2) -> TermStyle
termStyle (Inl fun1
x) = forall f. PrettyTerm f => f -> TermStyle
termStyle fun1
x
  termStyle (Inr fun2
x) = forall f. PrettyTerm f => f -> TermStyle
termStyle fun2
x