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

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

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

-------------------------------------------------------------------------------
-- Type substitutions
-------------------------------------------------------------------------------

data TypeSubst = TypeSubst (Map TypeVar Type) (Map Type (Maybe Type))

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

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

-------------------------------------------------------------------------------
-- Equality
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- Primitive type substitutions
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- General type 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 an updated type cache
  --
  basicSubst :: a -> TypeSubst -> (Maybe a, TypeSubst)

  --
  -- These substitution functions return Nothing if unchanged
  --
  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

  --
  -- These substitution functions return their argument if unchanged
  --
  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

-------------------------------------------------------------------------------
-- Composing type substitutions, should satisfy
--
-- |- subst (compose s1 s2) t == subst s2 (subst s1 t)
-------------------------------------------------------------------------------

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