module HOL.TypeSubst
where
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import HOL.Data
import qualified HOL.Type as Type
data TypeSubst = TypeSubst (Map TypeVar Type) (Map Type (Maybe Type))
mk :: Map TypeVar Type -> TypeSubst
mk :: Map TypeVar Type -> TypeSubst
mk Map TypeVar Type
m =
Map TypeVar Type -> Map Type (Maybe Type) -> TypeSubst
TypeSubst ((TypeVar -> Type -> Bool) -> Map TypeVar Type -> Map TypeVar Type
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey TypeVar -> Type -> Bool
norm Map TypeVar Type
m) Map Type (Maybe Type)
forall k a. Map k a
Map.empty
where
norm :: TypeVar -> Type -> Bool
norm TypeVar
v Type
ty = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TypeVar -> Type -> Bool
Type.eqVar TypeVar
v Type
ty
dest :: TypeSubst -> Map TypeVar Type
dest :: TypeSubst -> Map TypeVar Type
dest (TypeSubst Map TypeVar Type
m Map Type (Maybe Type)
_) = Map TypeVar Type
m
fromList :: [(TypeVar,Type)] -> TypeSubst
fromList :: [(TypeVar, Type)] -> TypeSubst
fromList = Map TypeVar Type -> TypeSubst
mk (Map TypeVar Type -> TypeSubst)
-> ([(TypeVar, Type)] -> Map TypeVar Type)
-> [(TypeVar, Type)]
-> TypeSubst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(TypeVar, Type)] -> Map TypeVar Type
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
empty :: TypeSubst
empty :: TypeSubst
empty = [(TypeVar, Type)] -> TypeSubst
fromList []
singleton :: TypeVar -> Type -> TypeSubst
singleton :: TypeVar -> Type -> TypeSubst
singleton TypeVar
v Type
ty = [(TypeVar, Type)] -> TypeSubst
fromList [(TypeVar
v,Type
ty)]
null :: TypeSubst -> Bool
null :: TypeSubst -> Bool
null = Map TypeVar Type -> Bool
forall k a. Map k a -> Bool
Map.null (Map TypeVar Type -> Bool)
-> (TypeSubst -> Map TypeVar Type) -> TypeSubst -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubst -> Map TypeVar Type
dest
instance Eq TypeSubst where
TypeSubst
sub1 == :: TypeSubst -> TypeSubst -> Bool
== TypeSubst
sub2 = TypeSubst -> Map TypeVar Type
dest TypeSubst
sub1 Map TypeVar Type -> Map TypeVar Type -> Bool
forall a. Eq a => a -> a -> Bool
== TypeSubst -> Map TypeVar Type
dest TypeSubst
sub2
varSubst :: TypeVar -> TypeSubst -> Maybe Type
varSubst :: TypeVar -> TypeSubst -> Maybe Type
varSubst TypeVar
v (TypeSubst Map TypeVar Type
m Map Type (Maybe Type)
_) = TypeVar -> Map TypeVar Type -> Maybe Type
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TypeVar
v Map TypeVar Type
m
dataSubst :: TypeData -> TypeSubst -> (Maybe Type, TypeSubst)
dataSubst :: TypeData -> TypeSubst -> (Maybe Type, TypeSubst)
dataSubst (VarType TypeVar
v) TypeSubst
s = (TypeVar -> TypeSubst -> Maybe Type
varSubst TypeVar
v TypeSubst
s, TypeSubst
s)
dataSubst (OpType TypeOp
t [Type]
tys) TypeSubst
s =
(([Type] -> Type) -> Maybe [Type] -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TypeOp -> [Type] -> Type
Type.mkOp TypeOp
t) Maybe [Type]
tys', TypeSubst
s')
where
(Maybe [Type]
tys',TypeSubst
s') = [Type] -> TypeSubst -> (Maybe [Type], TypeSubst)
forall a. CanSubst a => a -> TypeSubst -> (Maybe a, TypeSubst)
basicSubst [Type]
tys TypeSubst
s
class CanSubst a where
basicSubst :: a -> TypeSubst -> (Maybe a, TypeSubst)
sharingSubst :: a -> TypeSubst -> (Maybe a, TypeSubst)
sharingSubst a
x TypeSubst
s =
if TypeSubst -> Bool
HOL.TypeSubst.null TypeSubst
s then (Maybe a
forall a. Maybe a
Nothing,TypeSubst
s) else a -> TypeSubst -> (Maybe a, TypeSubst)
forall a. CanSubst a => a -> TypeSubst -> (Maybe a, TypeSubst)
basicSubst a
x TypeSubst
s
subst :: TypeSubst -> a -> Maybe a
subst TypeSubst
s a
x = (Maybe a, TypeSubst) -> Maybe a
forall a b. (a, b) -> a
fst ((Maybe a, TypeSubst) -> Maybe a)
-> (Maybe a, TypeSubst) -> Maybe a
forall a b. (a -> b) -> a -> b
$ a -> TypeSubst -> (Maybe a, TypeSubst)
forall a. CanSubst a => a -> TypeSubst -> (Maybe a, TypeSubst)
sharingSubst a
x TypeSubst
s
trySharingSubst :: a -> TypeSubst -> (a,TypeSubst)
trySharingSubst a
x TypeSubst
s = (a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
x Maybe a
x', TypeSubst
s') where (Maybe a
x',TypeSubst
s') = a -> TypeSubst -> (Maybe a, TypeSubst)
forall a. CanSubst a => a -> TypeSubst -> (Maybe a, TypeSubst)
sharingSubst a
x TypeSubst
s
trySubst :: TypeSubst -> a -> a
trySubst TypeSubst
s 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
subst TypeSubst
s a
x)
instance CanSubst a => CanSubst [a] where
basicSubst :: [a] -> TypeSubst -> (Maybe [a], TypeSubst)
basicSubst [] TypeSubst
s = (Maybe [a]
forall a. Maybe a
Nothing,TypeSubst
s)
basicSubst (a
h : [a]
t) TypeSubst
s =
(Maybe [a]
l',TypeSubst
s'')
where
(Maybe a
h',TypeSubst
s') = a -> TypeSubst -> (Maybe a, TypeSubst)
forall a. CanSubst a => a -> TypeSubst -> (Maybe a, TypeSubst)
basicSubst a
h TypeSubst
s
(Maybe [a]
t',TypeSubst
s'') = [a] -> TypeSubst -> (Maybe [a], TypeSubst)
forall a. CanSubst a => a -> TypeSubst -> (Maybe a, TypeSubst)
basicSubst [a]
t TypeSubst
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 -> TypeSubst -> (Maybe (Set a), TypeSubst)
basicSubst Set a
xs TypeSubst
s =
(Maybe (Set a)
xs',TypeSubst
s')
where
xl :: [a]
xl = Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
xs
(Maybe [a]
xl',TypeSubst
s') = [a] -> TypeSubst -> (Maybe [a], TypeSubst)
forall a. CanSubst a => a -> TypeSubst -> (Maybe a, TypeSubst)
basicSubst [a]
xl TypeSubst
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 -> TypeSubst -> (Maybe Type, TypeSubst)
basicSubst Type
ty TypeSubst
s =
case Type -> Map Type (Maybe Type) -> Maybe (Maybe Type)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Type
ty Map Type (Maybe Type)
c of
Just Maybe Type
ty' -> (Maybe Type
ty',TypeSubst
s)
Maybe (Maybe Type)
Nothing ->
(Maybe Type
ty', Map TypeVar Type -> Map Type (Maybe Type) -> TypeSubst
TypeSubst Map TypeVar Type
m (Type
-> Maybe Type -> Map Type (Maybe Type) -> Map Type (Maybe Type)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Type
ty Maybe Type
ty' Map Type (Maybe Type)
c'))
where
(Maybe Type
ty', TypeSubst Map TypeVar Type
m Map Type (Maybe Type)
c') = TypeData -> TypeSubst -> (Maybe Type, TypeSubst)
dataSubst (Type -> TypeData
Type.dest Type
ty) TypeSubst
s
where
TypeSubst Map TypeVar Type
_ Map Type (Maybe Type)
c = TypeSubst
s
instance CanSubst Var where
basicSubst :: Var -> TypeSubst -> (Maybe Var, TypeSubst)
basicSubst (Var Name
n Type
ty) TypeSubst
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', TypeSubst
s')
where
(Maybe Type
ty',TypeSubst
s') = Type -> TypeSubst -> (Maybe Type, TypeSubst)
forall a. CanSubst a => a -> TypeSubst -> (Maybe a, TypeSubst)
basicSubst Type
ty TypeSubst
s
compose :: TypeSubst -> TypeSubst -> TypeSubst
compose :: TypeSubst -> TypeSubst -> TypeSubst
compose TypeSubst
sub1 TypeSubst
sub2 | TypeSubst -> Bool
HOL.TypeSubst.null TypeSubst
sub2 = TypeSubst
sub1
compose TypeSubst
sub1 TypeSubst
sub2 | TypeSubst -> Bool
HOL.TypeSubst.null TypeSubst
sub1 = TypeSubst
sub2
compose TypeSubst
sub1 TypeSubst
sub2 | Bool
otherwise =
Map TypeVar Type -> TypeSubst
mk (Map TypeVar Type -> TypeSubst) -> Map TypeVar Type -> TypeSubst
forall a b. (a -> b) -> a -> b
$ (Map TypeVar Type, TypeSubst) -> Map TypeVar Type
forall a b. (a, b) -> a
fst ((Map TypeVar Type, TypeSubst) -> Map TypeVar Type)
-> (Map TypeVar Type, TypeSubst) -> Map TypeVar Type
forall a b. (a -> b) -> a -> b
$ (TypeVar
-> Type
-> (Map TypeVar Type, TypeSubst)
-> (Map TypeVar Type, TypeSubst))
-> (Map TypeVar Type, TypeSubst)
-> Map TypeVar Type
-> (Map TypeVar Type, TypeSubst)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey TypeVar
-> Type
-> (Map TypeVar Type, TypeSubst)
-> (Map TypeVar Type, TypeSubst)
forall a k.
(CanSubst a, Ord k) =>
k -> a -> (Map k a, TypeSubst) -> (Map k a, TypeSubst)
inc (TypeSubst -> Map TypeVar Type
dest TypeSubst
sub2, TypeSubst
sub2) (TypeSubst -> Map TypeVar Type
dest TypeSubst
sub1)
where
inc :: k -> a -> (Map k a, TypeSubst) -> (Map k a, TypeSubst)
inc k
v1 a
t1 (Map k a
m2,TypeSubst
s2) = (Map k a
m2',TypeSubst
s2')
where
(a
t1',TypeSubst
s2') = a -> TypeSubst -> (a, TypeSubst)
forall a. CanSubst a => a -> TypeSubst -> (a, TypeSubst)
trySharingSubst a
t1 TypeSubst
s2
m2' :: Map k a
m2' = k -> a -> Map k a -> Map k a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
v1 a
t1' Map k a
m2