{- |
module: $Header$
description: Higher order logic substitutions
license: MIT

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

module HOL.Subst
where

import Control.Monad (guard)
import Control.Monad.Trans.State (State,get,put,evalState)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe,isNothing)
import Data.Set (Set)
import qualified Data.Set as Set

import HOL.Data
import qualified HOL.Term as Term
import HOL.TypeSubst (TypeSubst)
import qualified HOL.TypeSubst as TypeSubst
import HOL.Util (mkUnsafe2)
import qualified HOL.Var as Var

-------------------------------------------------------------------------------
-- Capture-avoiding substitutions
-------------------------------------------------------------------------------

data Subst = Subst TypeSubst (Map Var Term) (Map Term (Maybe Term))

-------------------------------------------------------------------------------
-- Constructors and destructors
-------------------------------------------------------------------------------

mk :: TypeSubst -> Map Var Term -> Maybe Subst
mk :: TypeSubst -> Map Var Term -> Maybe Subst
mk TypeSubst
ts Map Var Term
m = do
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (((Var, Term) -> Bool) -> [(Var, Term)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Var -> Term -> Bool) -> (Var, Term) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Var -> Term -> Bool
Term.sameTypeVar) ([(Var, Term)] -> Bool) -> [(Var, Term)] -> Bool
forall a b. (a -> b) -> a -> b
$ Map Var Term -> [(Var, Term)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Var Term
m)
    Subst -> Maybe Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Maybe Subst) -> Subst -> Maybe Subst
forall a b. (a -> b) -> a -> b
$ TypeSubst -> Map Var Term -> Map Term (Maybe Term) -> Subst
Subst TypeSubst
ts ((Var -> Term -> Bool) -> Map Var Term -> Map Var Term
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey Var -> Term -> Bool
norm Map Var Term
m) Map Term (Maybe Term)
forall k a. Map k a
Map.empty
  where
    norm :: Var -> Term -> Bool
norm Var
v Term
tm = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Var -> Term -> Bool
Term.eqVar Var
v Term
tm

mkUnsafe :: TypeSubst -> Map Var Term -> Subst
mkUnsafe :: TypeSubst -> Map Var Term -> Subst
mkUnsafe = String
-> (TypeSubst -> Map Var Term -> Maybe Subst)
-> TypeSubst
-> Map Var Term
-> Subst
forall a b c. String -> (a -> b -> Maybe c) -> a -> b -> c
mkUnsafe2 String
"HOL.Subst.mk" TypeSubst -> Map Var Term -> Maybe Subst
mk

dest :: Subst -> (TypeSubst, Map Var Term)
dest :: Subst -> (TypeSubst, Map Var Term)
dest (Subst TypeSubst
ts Map Var Term
m Map Term (Maybe Term)
_) = (TypeSubst
ts,Map Var Term
m)

fromList :: [(TypeVar,Type)] -> [(Var,Term)] -> Maybe Subst
fromList :: [(TypeVar, Type)] -> [(Var, Term)] -> Maybe Subst
fromList [(TypeVar, Type)]
ts = TypeSubst -> Map Var Term -> Maybe Subst
mk ([(TypeVar, Type)] -> TypeSubst
TypeSubst.fromList [(TypeVar, Type)]
ts) (Map Var Term -> Maybe Subst)
-> ([(Var, Term)] -> Map Var Term) -> [(Var, Term)] -> Maybe Subst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Var, Term)] -> Map Var Term
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList

fromListUnsafe :: [(TypeVar,Type)] -> [(Var,Term)] -> Subst
fromListUnsafe :: [(TypeVar, Type)] -> [(Var, Term)] -> Subst
fromListUnsafe = String
-> ([(TypeVar, Type)] -> [(Var, Term)] -> Maybe Subst)
-> [(TypeVar, Type)]
-> [(Var, Term)]
-> Subst
forall a b c. String -> (a -> b -> Maybe c) -> a -> b -> c
mkUnsafe2 String
"HOL.Subst.fromList" [(TypeVar, Type)] -> [(Var, Term)] -> Maybe Subst
fromList

empty :: Subst
empty :: Subst
empty = TypeSubst -> Map Var Term -> Map Term (Maybe Term) -> Subst
Subst TypeSubst
TypeSubst.empty Map Var Term
forall k a. Map k a
Map.empty Map Term (Maybe Term)
forall k a. Map k a
Map.empty

singleton :: Var -> Term -> Maybe Subst
singleton :: Var -> Term -> Maybe Subst
singleton Var
v Term
tm = [(TypeVar, Type)] -> [(Var, Term)] -> Maybe Subst
fromList [] [(Var
v,Term
tm)]

singletonUnsafe :: Var -> Term -> Subst
singletonUnsafe :: Var -> Term -> Subst
singletonUnsafe = String -> (Var -> Term -> Maybe Subst) -> Var -> Term -> Subst
forall a b c. String -> (a -> b -> Maybe c) -> a -> b -> c
mkUnsafe2 String
"HOL.Subst.singleton" Var -> Term -> Maybe Subst
singleton

null :: Subst -> Bool
null :: Subst -> Bool
null (Subst TypeSubst
ts Map Var Term
m Map Term (Maybe Term)
_) = TypeSubst -> Bool
TypeSubst.null TypeSubst
ts Bool -> Bool -> Bool
&& Map Var Term -> Bool
forall k a. Map k a -> Bool
Map.null Map Var Term
m

-------------------------------------------------------------------------------
-- Avoiding capture
-------------------------------------------------------------------------------

capturableVars :: Var -> Term -> Term -> Set Var
capturableVars :: Var -> Term -> Term -> Set Var
capturableVars Var
v =
    \Term
tm Term
tm' -> State (Set (Term, Term)) (Set Var) -> Set (Term, Term) -> Set Var
forall s a. State s a -> s -> a
evalState (Term -> Term -> State (Set (Term, Term)) (Set Var)
termVars Term
tm Term
tm') Set (Term, Term)
forall a. Set a
Set.empty
  where
    noVars :: Set Var
    noVars :: Set Var
noVars = Set Var
forall a. Set a
Set.empty

    termVars :: Term -> Term -> State (Set (Term,Term)) (Set Var)
    termVars :: Term -> Term -> State (Set (Term, Term)) (Set Var)
termVars Term
tm Term
tm' =
        if Var -> Term -> Bool
forall a. HasFree a => Var -> a -> Bool
Var.notFreeIn Var
v Term
tm then Set Var -> State (Set (Term, Term)) (Set Var)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Var -> State (Set (Term, Term)) (Set Var))
-> Set Var -> State (Set (Term, Term)) (Set Var)
forall a b. (a -> b) -> a -> b
$ Term -> Set Var
forall a. HasFree a => a -> Set Var
Var.free Term
tm'
        else ((Term, Term) -> State (Set (Term, Term)) (Set Var))
-> Set Var -> (Term, Term) -> State (Set (Term, Term)) (Set Var)
forall a b.
Ord a =>
(a -> State (Set a) b) -> b -> a -> State (Set a) b
cachedIdem (Term, Term) -> State (Set (Term, Term)) (Set Var)
subVars Set Var
noVars (Term
tm,Term
tm')

    subVars :: (Term,Term) -> State (Set (Term,Term)) (Set Var)
    subVars :: (Term, Term) -> State (Set (Term, Term)) (Set Var)
subVars (Term
tm,Term
tm') = TermData -> TermData -> State (Set (Term, Term)) (Set Var)
dataVars (Term -> TermData
Term.dest Term
tm) (Term -> TermData
Term.dest Term
tm')

    dataVars :: TermData -> TermData -> State (Set (Term,Term)) (Set Var)
    dataVars :: TermData -> TermData -> State (Set (Term, Term)) (Set Var)
dataVars (VarTerm Var
_) TermData
_ = Set Var -> State (Set (Term, Term)) (Set Var)
forall (m :: * -> *) a. Monad m => a -> m a
return Set Var
noVars  -- must be variable v
    dataVars (AppTerm Term
f Term
x) (AppTerm Term
f' Term
x') = do
        Set Var
fv <- Term -> Term -> State (Set (Term, Term)) (Set Var)
termVars Term
f Term
f'
        Set Var
xv <- Term -> Term -> State (Set (Term, Term)) (Set Var)
termVars Term
x Term
x'
        Set Var -> State (Set (Term, Term)) (Set Var)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Var -> State (Set (Term, Term)) (Set Var))
-> Set Var -> State (Set (Term, Term)) (Set Var)
forall a b. (a -> b) -> a -> b
$ Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Var
fv Set Var
xv
    dataVars (AbsTerm Var
_ Term
b) (AbsTerm Var
v' Term
b') = do  -- cannot be variable v
        Set Var
bv <- Term -> Term -> State (Set (Term, Term)) (Set Var)
termVars Term
b Term
b'
        Set Var -> State (Set (Term, Term)) (Set Var)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Var -> State (Set (Term, Term)) (Set Var))
-> Set Var -> State (Set (Term, Term)) (Set Var)
forall a b. (a -> b) -> a -> b
$ Var -> Set Var -> Set Var
forall a. Ord a => a -> Set a -> Set a
Set.insert Var
v' Set Var
bv
    dataVars TermData
_ TermData
_ = String -> State (Set (Term, Term)) (Set Var)
forall a. HasCallStack => String -> a
error String
"HOL.Subst.capturableVars.dataVars"

    cachedIdem :: Ord a => (a -> State (Set a) b) -> b ->
                  a -> State (Set a) b
    cachedIdem :: (a -> State (Set a) b) -> b -> a -> State (Set a) b
cachedIdem a -> State (Set a) b
f b
i a
a = do
      Set a
s <- StateT (Set a) Identity (Set a)
forall (m :: * -> *) s. Monad m => StateT s m s
get
      case a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member a
a Set a
s of
        Bool
True -> b -> State (Set a) b
forall (m :: * -> *) a. Monad m => a -> m a
return b
i
        Bool
False -> do
          b
b <- a -> State (Set a) b
f a
a
          Set a
s' <- StateT (Set a) Identity (Set a)
forall (m :: * -> *) s. Monad m => StateT s m s
get
          Set a -> StateT (Set a) Identity ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
a Set a
s')
          b -> State (Set a) b
forall (m :: * -> *) a. Monad m => a -> m a
return b
b

renameBoundVar :: Var -> Term -> Term -> Term -> Term
renameBoundVar :: Var -> Term -> Term -> Term -> Term
renameBoundVar Var
v Term
v' =
    \Term
tm Term
tm' -> State (Map (Term, Term) Term) Term -> Map (Term, Term) Term -> Term
forall s a. State s a -> s -> a
evalState (Term -> Term -> State (Map (Term, Term) Term) Term
termRename Term
tm Term
tm') Map (Term, Term) Term
forall k a. Map k a
Map.empty
  where
    termRename :: Term -> Term -> State (Map (Term,Term) Term) Term
    termRename :: Term -> Term -> State (Map (Term, Term) Term) Term
termRename Term
tm Term
tm' =
        if Var -> Term -> Bool
forall a. HasFree a => Var -> a -> Bool
Var.notFreeIn Var
v Term
tm then Term -> State (Map (Term, Term) Term) Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm'
        else ((Term, Term) -> State (Map (Term, Term) Term) Term)
-> (Term, Term) -> State (Map (Term, Term) Term) Term
forall a b.
Ord a =>
(a -> State (Map a b) b) -> a -> State (Map a b) b
cached (Term, Term) -> State (Map (Term, Term) Term) Term
subRename (Term
tm,Term
tm')

    subRename :: (Term,Term) -> State (Map (Term,Term) Term) Term
    subRename :: (Term, Term) -> State (Map (Term, Term) Term) Term
subRename (Term
tm,Term
tm') = TermData -> TermData -> State (Map (Term, Term) Term) Term
dataRename (Term -> TermData
Term.dest Term
tm) (Term -> TermData
Term.dest Term
tm')

    dataRename :: TermData -> TermData -> State (Map (Term,Term) Term) Term
    dataRename :: TermData -> TermData -> State (Map (Term, Term) Term) Term
dataRename (VarTerm Var
_) TermData
_ = Term -> State (Map (Term, Term) Term) Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v' -- must be variable v
    dataRename (AppTerm Term
f Term
x) (AppTerm Term
f' Term
x') = do
        Term
f'' <- Term -> Term -> State (Map (Term, Term) Term) Term
termRename Term
f Term
f'
        Term
x'' <- Term -> Term -> State (Map (Term, Term) Term) Term
termRename Term
x Term
x'
        Term -> State (Map (Term, Term) Term) Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> State (Map (Term, Term) Term) Term)
-> Term -> State (Map (Term, Term) Term) Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
Term.mkAppUnsafe Term
f'' Term
x''
    dataRename (AbsTerm Var
_ Term
b) (AbsTerm Var
w' Term
b') = do  -- cannot be variable v
        Term
b'' <- Term -> Term -> State (Map (Term, Term) Term) Term
termRename Term
b Term
b'
        Term -> State (Map (Term, Term) Term) Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> State (Map (Term, Term) Term) Term)
-> Term -> State (Map (Term, Term) Term) Term
forall a b. (a -> b) -> a -> b
$ Var -> Term -> Term
Term.mkAbs Var
w' Term
b''
    dataRename TermData
_ TermData
_ = String -> State (Map (Term, Term) Term) Term
forall a. HasCallStack => String -> a
error String
"HOL.Subst.renameBoundVar.dataRename"

    cached :: Ord a => (a -> State (Map a b) b) -> a -> State (Map a b) b
    cached :: (a -> State (Map a b) b) -> a -> State (Map a b) b
cached a -> State (Map a b) b
f a
a = do
      Map a b
c <- StateT (Map a b) Identity (Map a b)
forall (m :: * -> *) s. Monad m => StateT s m s
get
      case a -> Map a b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
a Map a b
c of
        Just b
b -> b -> State (Map a b) b
forall (m :: * -> *) a. Monad m => a -> m a
return b
b
        Maybe b
Nothing -> do
          b
b <- a -> State (Map a b) b
f a
a
          Map a b
c' <- StateT (Map a b) Identity (Map a b)
forall (m :: * -> *) s. Monad m => StateT s m s
get
          Map a b -> StateT (Map a b) Identity ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (a -> b -> Map a b -> Map a b
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
a b
b Map a b
c')
          b -> State (Map a b) b
forall (m :: * -> *) a. Monad m => a -> m a
return b
b

avoidCapture :: Bool -> Var -> Var -> Term -> Term -> (Var,Term)
avoidCapture :: Bool -> Var -> Var -> Term -> Term -> (Var, Term)
avoidCapture Bool
vSub' Var
v Var
v' Term
b Term
b' =
    (Var
v'',Term
b'')
  where
    avoid :: Set Name
avoid = (Var -> Name) -> Set Var -> Set Name
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Var -> Name
Var.name (Set Var -> Set Name) -> Set Var -> Set Name
forall a b. (a -> b) -> a -> b
$ Var -> Term -> Term -> Set Var
capturableVars Var
v Term
b Term
b'
    v'' :: Var
v'' = Set Name -> Var -> Var
Var.renameAvoiding Set Name
avoid Var
v'
    b'' :: Term
b'' = if Bool -> Bool
not Bool
vSub' Bool -> Bool -> Bool
&& Var
v'' Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v' then Term
b'
          else Var -> Term -> Term -> Term -> Term
renameBoundVar Var
v (Var -> Term
Term.mkVar Var
v'') Term
b Term
b'

-------------------------------------------------------------------------------
-- Primitive substitutions
-------------------------------------------------------------------------------

varSubst :: Var -> Subst -> (Maybe Term, Subst)
varSubst :: Var -> Subst -> (Maybe Term, Subst)
varSubst Var
v Subst
s =
    (Maybe Term
tm,Subst
s')
  where
    -- first apply the type substitution
    (Maybe Var
v',Subst
s') = Var -> Subst -> (Maybe Var, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
basicSubst Var
v Subst
s
    -- then apply the term substitution
    tm :: Maybe Term
tm = case Maybe Var
v' of
           Maybe Var
Nothing -> Var -> Map Var Term -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Var
v Map Var Term
m
           Just Var
w -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe (Var -> Term
Term.mkVar Var
w) (Var -> Map Var Term -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Var
w Map Var Term
m)
    Subst TypeSubst
_ Map Var Term
m Map Term (Maybe Term)
_ = Subst
s'

dataSubst :: TermData -> Subst -> (Maybe Term, Subst)
dataSubst :: TermData -> Subst -> (Maybe Term, Subst)
dataSubst (ConstTerm Const
c Type
ty) Subst
s =
    ((Type -> Term) -> Maybe Type -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Const -> Type -> Term
Term.mkConst Const
c) Maybe Type
ty', Subst
s')
  where
    (Maybe Type
ty',Subst
s') = Type -> Subst -> (Maybe Type, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
basicSubst Type
ty Subst
s
dataSubst (VarTerm Var
v) Subst
s = Var -> Subst -> (Maybe Term, Subst)
varSubst Var
v Subst
s
dataSubst (AppTerm Term
f Term
x) Subst
s =
    (Maybe Term
tm',Subst
s'')
  where
    (Maybe Term
f',Subst
s') = Term -> Subst -> (Maybe Term, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
basicSubst Term
f Subst
s
    (Maybe Term
x',Subst
s'') = Term -> Subst -> (Maybe Term, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
basicSubst Term
x Subst
s'
    tm' :: Maybe Term
tm' = case Maybe Term
f' of
            Maybe Term
Nothing -> (Term -> Term) -> Maybe Term -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term -> Term -> Term
Term.mkAppUnsafe Term
f) Maybe Term
x'
            Just Term
g -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Term -> Term
Term.mkAppUnsafe Term
g (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
x Maybe Term
x')
dataSubst (AbsTerm Var
v Term
b) Subst
s =
    (Maybe Term
tm',Subst
s'')
  where
    (Maybe Var
v',Subst
s') = Var -> Subst -> (Maybe Var, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
basicSubst Var
v Subst
s
    (Maybe Term
b',Subst
s'') = Term -> Subst -> (Maybe Term, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
basicSubst Term
b Subst
s'
    tm' :: Maybe Term
tm' = if Maybe Var -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Var
v' Bool -> Bool -> Bool
&& Maybe Term -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Term
b' then Maybe Term
forall a. Maybe a
Nothing
          else Term -> Maybe Term
forall a. a -> Maybe a
Just (Var -> Term -> Term
Term.mkAbs Var
v'' Term
b'')
    (Var
v'',Term
b'') = Bool -> Var -> Var -> Term -> Term -> (Var, Term)
avoidCapture Bool
wSub Var
v Var
w Term
b (Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
b Maybe Term
b')
    wSub :: Bool
wSub = Var -> Map Var Term -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Var
w Map Var Term
m where Subst TypeSubst
_ Map Var Term
m Map Term (Maybe Term)
_ = Subst
s''
    w :: Var
w = Var -> Maybe Var -> Var
forall a. a -> Maybe a -> a
fromMaybe Var
v Maybe Var
v'

-------------------------------------------------------------------------------
-- General substitutions
-------------------------------------------------------------------------------

class CanSubst a where
  --
  -- This is the primitive substitution function for types to implement,
  -- which has the following properties:
  --  1. Can assume the substitution is not null
  --  2. Returns Nothing if the argument is unchanged by the substitution
  --  3. Returns the substitution with updated type and term caches
  --
  basicSubst :: a -> Subst -> (Maybe a, Subst)

  --
  -- These substitution functions return Nothing if unchanged
  --
  sharingSubst :: a -> Subst -> (Maybe a, Subst)
  sharingSubst a
x Subst
s = if Subst -> Bool
HOL.Subst.null Subst
s then (Maybe a
forall a. Maybe a
Nothing,Subst
s) else a -> Subst -> (Maybe a, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
basicSubst a
x Subst
s

  subst :: Subst -> a -> Maybe a
  subst Subst
s a
x = (Maybe a, Subst) -> Maybe a
forall a b. (a, b) -> a
fst ((Maybe a, Subst) -> Maybe a) -> (Maybe a, Subst) -> Maybe a
forall a b. (a -> b) -> a -> b
$ a -> Subst -> (Maybe a, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
sharingSubst a
x Subst
s

  typeSubst :: TypeSubst -> a -> Maybe a
  typeSubst TypeSubst
ts = Subst -> a -> Maybe a
forall a. CanSubst a => Subst -> a -> Maybe a
subst (Subst -> a -> Maybe a) -> Subst -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ TypeSubst -> Map Var Term -> Subst
mkUnsafe TypeSubst
ts Map Var Term
forall k a. Map k a
Map.empty

  --
  -- These substitution functions return their argument if unchanged
  --
  trySharingSubst :: a -> Subst -> (a,Subst)
  trySharingSubst a
x Subst
s = (a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
x Maybe a
x', Subst
s') where (Maybe a
x',Subst
s') = a -> Subst -> (Maybe a, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
sharingSubst a
x Subst
s

  trySubst :: Subst -> a -> a
  trySubst Subst
s a
x = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
x (Subst -> a -> Maybe a
forall a. CanSubst a => Subst -> a -> Maybe a
subst Subst
s a
x)

  tryTypeSubst :: TypeSubst -> a -> a
  tryTypeSubst TypeSubst
ts a
x = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
x (TypeSubst -> a -> Maybe a
forall a. CanSubst a => TypeSubst -> a -> Maybe a
typeSubst TypeSubst
ts a
x)

instance CanSubst a => CanSubst [a] where
  basicSubst :: [a] -> Subst -> (Maybe [a], Subst)
basicSubst [] Subst
s = (Maybe [a]
forall a. Maybe a
Nothing,Subst
s)
  basicSubst (a
h : [a]
t) Subst
s =
      (Maybe [a]
l',Subst
s'')
    where
      (Maybe a
h',Subst
s') = a -> Subst -> (Maybe a, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
basicSubst a
h Subst
s
      (Maybe [a]
t',Subst
s'') = [a] -> Subst -> (Maybe [a], Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
basicSubst [a]
t Subst
s'
      l' :: Maybe [a]
l' = case Maybe a
h' of
             Maybe a
Nothing -> ([a] -> [a]) -> Maybe [a] -> Maybe [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((:) a
h) Maybe [a]
t'
             Just a
x -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> Maybe [a] -> [a]
forall a. a -> Maybe a -> a
fromMaybe [a]
t Maybe [a]
t')

instance (Ord a, CanSubst a) => CanSubst (Set a) where
  basicSubst :: Set a -> Subst -> (Maybe (Set a), Subst)
basicSubst Set a
xs Subst
s =
      (Maybe (Set a)
xs',Subst
s')
    where
      xl :: [a]
xl = Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
xs
      (Maybe [a]
xl',Subst
s') = [a] -> Subst -> (Maybe [a], Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
basicSubst [a]
xl Subst
s
      xs' :: Maybe (Set a)
xs' = ([a] -> Set a) -> Maybe [a] -> Maybe (Set a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList Maybe [a]
xl'

instance CanSubst Type where
  basicSubst :: Type -> Subst -> (Maybe Type, Subst)
basicSubst Type
ty Subst
s =
      (Maybe Type
ty', TypeSubst -> Map Var Term -> Map Term (Maybe Term) -> Subst
Subst TypeSubst
ts' Map Var Term
m Map Term (Maybe Term)
c)
    where
      Subst TypeSubst
ts Map Var Term
m Map Term (Maybe Term)
c = Subst
s
      (Maybe Type
ty',TypeSubst
ts') = Type -> TypeSubst -> (Maybe Type, TypeSubst)
forall a. CanSubst a => a -> TypeSubst -> (Maybe a, TypeSubst)
TypeSubst.sharingSubst Type
ty TypeSubst
ts

-- This only applies the type substitution
instance CanSubst Var where
  basicSubst :: Var -> Subst -> (Maybe Var, Subst)
basicSubst (Var Name
n Type
ty) Subst
s =
      ((Type -> Var) -> Maybe Type -> Maybe Var
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> Type -> Var
Var Name
n) Maybe Type
ty', Subst
s')
    where
      (Maybe Type
ty',Subst
s') = Type -> Subst -> (Maybe Type, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
basicSubst Type
ty Subst
s

instance CanSubst Term where
  basicSubst :: Term -> Subst -> (Maybe Term, Subst)
basicSubst Term
tm Subst
s =
      case Term -> Map Term (Maybe Term) -> Maybe (Maybe Term)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Term
tm Map Term (Maybe Term)
c of
        Just Maybe Term
tm' -> (Maybe Term
tm',Subst
s)
        Maybe (Maybe Term)
Nothing ->
            (Maybe Term
tm', TypeSubst -> Map Var Term -> Map Term (Maybe Term) -> Subst
Subst TypeSubst
ts Map Var Term
m (Term
-> Maybe Term -> Map Term (Maybe Term) -> Map Term (Maybe Term)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Term
tm Maybe Term
tm' Map Term (Maybe Term)
c'))
          where
            (Maybe Term
tm', Subst TypeSubst
ts Map Var Term
m Map Term (Maybe Term)
c') = TermData -> Subst -> (Maybe Term, Subst)
dataSubst (Term -> TermData
Term.dest Term
tm) Subst
s
    where
      Subst TypeSubst
_ Map Var Term
_ Map Term (Maybe Term)
c = Subst
s