{-# LANGUAGE ExistentialQuantification, Rank2Types #-}
module Language.Haskell.FreeTheorems.Frontend.TypeExpressions (
freeTypeVariables
, allTypeVariables
, createNewTypeVariableNotIn
, alphaConversion
, substituteTypeVariables
, replaceAllTypeSynonyms
, closeTypeExpressions
, closureFor
) where
import Data.Generics
( Typeable, Data, synthesize, mkQ, everywhere, mkT, gmapT, GenericQ
, GenericT )
import Data.List (find)
import Data.Set as Set
( Set, empty, union, insert, delete, fold, unions, difference, singleton
, member )
import Data.Map as Map (Map, empty, lookup, delete, insert)
import Data.Maybe (maybe, fromJust)
import Language.Haskell.FreeTheorems.Syntax
import Language.Haskell.FreeTheorems.NameStores (typeNameStore)
allTypeVariables :: TypeExpression -> Set.Set TypeVariable
allTypeVariables :: TypeExpression -> Set TypeVariable
allTypeVariables = forall s t. s -> (t -> s -> s) -> GenericQ (s -> t) -> GenericQ t
synthesize forall a. Set a
Set.empty forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall a. a -> a
id forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
`mkQ` TypeExpression -> Set TypeVariable -> Set TypeVariable
update)
where
update :: TypeExpression -> Set TypeVariable -> Set TypeVariable
update TypeExpression
t Set TypeVariable
s = case TypeExpression
t of
TypeVar TypeVariable
v -> forall a. Ord a => a -> Set a -> Set a
Set.insert TypeVariable
v Set TypeVariable
s
TypeAbs TypeVariable
v [TypeClass]
_ TypeExpression
_ -> forall a. Ord a => a -> Set a -> Set a
Set.insert TypeVariable
v Set TypeVariable
s
TypeAbsLab TypeVariable
v [TypeClass]
_ TypeExpression
_ -> forall a. Ord a => a -> Set a -> Set a
Set.insert TypeVariable
v Set TypeVariable
s
TypeExpression
otherwise -> Set TypeVariable
s
freeTypeVariables :: TypeExpression -> Set.Set TypeVariable
freeTypeVariables :: TypeExpression -> Set TypeVariable
freeTypeVariables = forall s t. s -> (t -> s -> s) -> GenericQ (s -> t) -> GenericQ t
synthesize forall a. Set a
Set.empty forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall a. a -> a
id forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
`mkQ` TypeExpression -> Set TypeVariable -> Set TypeVariable
update)
where
update :: TypeExpression -> Set TypeVariable -> Set TypeVariable
update TypeExpression
t Set TypeVariable
s = case TypeExpression
t of
TypeVar TypeVariable
v -> forall a. Ord a => a -> Set a -> Set a
Set.insert TypeVariable
v Set TypeVariable
s
TypeAbs TypeVariable
v [TypeClass]
_ TypeExpression
_ -> forall a. Ord a => a -> Set a -> Set a
Set.delete TypeVariable
v Set TypeVariable
s
TypeAbsLab TypeVariable
v [TypeClass]
_ TypeExpression
_ -> forall a. Ord a => a -> Set a -> Set a
Set.delete TypeVariable
v Set TypeVariable
s
TypeExpression
otherwise -> Set TypeVariable
s
substituteTypeVariables ::
Map.Map TypeVariable TypeExpression
-> TypeExpression
-> TypeExpression
substituteTypeVariables :: Map TypeVariable TypeExpression -> TypeExpression -> TypeExpression
substituteTypeVariables Map TypeVariable TypeExpression
env TypeExpression
t =
forall u. GenericQ (u -> u) -> GenericTw u -> u -> GenericT
everywhereWith (forall a. a -> a
id forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
`mkQ` forall {a}.
TypeExpression -> Map TypeVariable a -> Map TypeVariable a
update) (forall a b u.
(Typeable a, Typeable b) =>
(u -> a -> a) -> u -> b -> b
mkTw Map TypeVariable TypeExpression -> TypeExpression -> TypeExpression
substitute) Map TypeVariable TypeExpression
env TypeExpression
t
where
update :: TypeExpression -> Map TypeVariable a -> Map TypeVariable a
update TypeExpression
t Map TypeVariable a
env = case TypeExpression
t of
TypeAbs TypeVariable
v [TypeClass]
_ TypeExpression
_ -> forall k a. Ord k => k -> Map k a -> Map k a
Map.delete TypeVariable
v Map TypeVariable a
env
TypeAbsLab TypeVariable
v [TypeClass]
_ TypeExpression
_ -> forall k a. Ord k => k -> Map k a -> Map k a
Map.delete TypeVariable
v Map TypeVariable a
env
TypeExpression
otherwise -> Map TypeVariable a
env
substitute :: Map TypeVariable TypeExpression -> TypeExpression -> TypeExpression
substitute Map TypeVariable TypeExpression
env TypeExpression
t = case TypeExpression
t of
TypeVar TypeVariable
v -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe TypeExpression
t forall a. a -> a
id (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TypeVariable
v Map TypeVariable TypeExpression
env)
TypeExpression
otherwise -> TypeExpression
t
createNewTypeVariableNotIn :: Set.Set TypeVariable -> TypeVariable
createNewTypeVariableNotIn :: Set TypeVariable -> TypeVariable
createNewTypeVariableNotIn Set TypeVariable
forbiddenVars =
let vars :: [TypeVariable]
vars = forall a b. (a -> b) -> [a] -> [b]
map (Identifier -> TypeVariable
TV forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Identifier
Ident) [String]
typeNameStore
in forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\TypeVariable
v -> Bool -> Bool
not (TypeVariable
v forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TypeVariable
forbiddenVars)) [TypeVariable]
vars
alphaConversion :: TypeVariable -> TypeExpression -> TypeExpression
alphaConversion :: TypeVariable -> TypeExpression -> TypeExpression
alphaConversion TypeVariable
old TypeExpression
t =
forall u. GenericQ (u -> u) -> GenericTw u -> u -> GenericT
everywhereWith (forall a. a -> a
id forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
`mkQ` TypeExpression
-> (TypeVariable -> TypeVariable) -> TypeVariable -> TypeVariable
change) (forall a b u.
(Typeable a, Typeable b) =>
(u -> a -> a) -> u -> b -> b
mkTw (TypeVariable -> TypeVariable) -> TypeExpression -> TypeExpression
replace) forall a. a -> a
id TypeExpression
t
where
new :: TypeVariable
new = Set TypeVariable -> TypeVariable
createNewTypeVariableNotIn (TypeExpression -> Set TypeVariable
allTypeVariables TypeExpression
t)
rep :: TypeVariable -> TypeVariable
rep TypeVariable
v = if (TypeVariable
v forall a. Eq a => a -> a -> Bool
== TypeVariable
old) then TypeVariable
new else TypeVariable
v
change :: TypeExpression
-> (TypeVariable -> TypeVariable) -> TypeVariable -> TypeVariable
change TypeExpression
t TypeVariable -> TypeVariable
f = case TypeExpression
t of
TypeAbs TypeVariable
v [TypeClass]
_ TypeExpression
_ -> if (TypeVariable
v forall a. Eq a => a -> a -> Bool
== TypeVariable
old) then TypeVariable -> TypeVariable
rep else TypeVariable -> TypeVariable
f
TypeAbsLab TypeVariable
v [TypeClass]
_ TypeExpression
_ -> if (TypeVariable
v forall a. Eq a => a -> a -> Bool
== TypeVariable
old) then TypeVariable -> TypeVariable
rep else TypeVariable -> TypeVariable
f
TypeExpression
otherwise -> TypeVariable -> TypeVariable
f
replace :: (TypeVariable -> TypeVariable) -> TypeExpression -> TypeExpression
replace TypeVariable -> TypeVariable
r TypeExpression
t = case TypeExpression
t of
TypeVar TypeVariable
v -> TypeVariable -> TypeExpression
TypeVar (TypeVariable -> TypeVariable
r TypeVariable
v)
TypeAbs TypeVariable
v [TypeClass]
cs TypeExpression
t' -> TypeVariable -> [TypeClass] -> TypeExpression -> TypeExpression
TypeAbs (TypeVariable -> TypeVariable
rep TypeVariable
v) [TypeClass]
cs TypeExpression
t'
TypeAbsLab TypeVariable
v [TypeClass]
cs TypeExpression
t' -> TypeVariable -> [TypeClass] -> TypeExpression -> TypeExpression
TypeAbsLab (TypeVariable -> TypeVariable
rep TypeVariable
v) [TypeClass]
cs TypeExpression
t'
TypeExpression
otherwise -> TypeExpression
t
type GenericTw u = forall a . Data a => u -> a -> a
mkTw :: (Typeable a, Typeable b) => (u -> a -> a) -> u -> b -> b
mkTw :: forall a b u.
(Typeable a, Typeable b) =>
(u -> a -> a) -> u -> b -> b
mkTw u -> a -> a
f u
u = forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT forall a b. (a -> b) -> a -> b
$ u -> a -> a
f u
u
everywhereWith :: GenericQ (u -> u) -> GenericTw u -> u -> GenericT
everywhereWith :: forall u. GenericQ (u -> u) -> GenericTw u -> u -> GenericT
everywhereWith GenericQ (u -> u)
k GenericTw u
f u
u a
x = (GenericTw u
f u
u) forall a b. (a -> b) -> a -> b
$ forall a. Data a => GenericT -> a -> a
gmapT (forall u. GenericQ (u -> u) -> GenericTw u -> u -> GenericT
everywhereWith GenericQ (u -> u)
k GenericTw u
f (GenericQ (u -> u)
k a
x u
u)) a
x
replaceAllTypeSynonyms :: (Typeable a, Data a) => [TypeDeclaration] -> a -> a
replaceAllTypeSynonyms :: forall a. (Typeable a, Data a) => [TypeDeclaration] -> a -> a
replaceAllTypeSynonyms [TypeDeclaration]
knownTypes = GenericT -> GenericT
everywhere (forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT TypeExpression -> TypeExpression
replace)
where
replace :: TypeExpression -> TypeExpression
replace TypeExpression
t = case TypeExpression
t of
TypeCon TypeConstructor
c [TypeExpression]
ts -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe TypeExpression
t ([TypeExpression] -> TypeDeclaration -> TypeExpression
applyTypeSynonym [TypeExpression]
ts) ([TypeDeclaration] -> TypeConstructor -> Maybe TypeDeclaration
findTypeDecl [TypeDeclaration]
knownTypes TypeConstructor
c)
TypeExpression
otherwise -> TypeExpression
t
applyTypeSynonym :: [TypeExpression] -> TypeDeclaration -> TypeExpression
applyTypeSynonym [TypeExpression]
ts (Type Identifier
_ [TypeVariable]
vs TypeExpression
t) =
let
t1 :: TypeExpression
t1 = forall a. (Typeable a, Data a) => [TypeDeclaration] -> a -> a
replaceAllTypeSynonyms [TypeDeclaration]
knownTypes TypeExpression
t
env :: Map TypeVariable TypeExpression
env = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert) forall k a. Map k a
Map.empty (forall a b. [a] -> [b] -> [(a, b)]
zip [TypeVariable]
vs [TypeExpression]
ts)
allFreeVariables :: Set TypeVariable
allFreeVariables = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map TypeExpression -> Set TypeVariable
freeTypeVariables [TypeExpression]
ts
t2 :: TypeExpression
t2 = forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold TypeVariable -> TypeExpression -> TypeExpression
alphaConversion TypeExpression
t1 Set TypeVariable
allFreeVariables
in Map TypeVariable TypeExpression -> TypeExpression -> TypeExpression
substituteTypeVariables Map TypeVariable TypeExpression
env TypeExpression
t2
findTypeDecl :: [TypeDeclaration] -> TypeConstructor -> Maybe TypeDeclaration
findTypeDecl :: [TypeDeclaration] -> TypeConstructor -> Maybe TypeDeclaration
findTypeDecl [TypeDeclaration]
decls TypeConstructor
con = case TypeConstructor
con of
Con Identifier
name -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\TypeDeclaration
d -> TypeDeclaration -> Identifier
typeName TypeDeclaration
d forall a. Eq a => a -> a -> Bool
== Identifier
name) [TypeDeclaration]
decls
TypeConstructor
otherwise -> forall a. Maybe a
Nothing
closeTypeExpressions :: [Declaration] -> [Declaration]
closeTypeExpressions :: [Declaration] -> [Declaration]
closeTypeExpressions = forall a b. (a -> b) -> [a] -> [b]
map Declaration -> Declaration
closeDecl
where
closeDecl :: Declaration -> Declaration
closeDecl Declaration
d = case Declaration
d of
ClassDecl ClassDeclaration
d -> ClassDeclaration -> Declaration
ClassDecl (ClassDeclaration -> ClassDeclaration
closeClassDecl ClassDeclaration
d)
TypeSig Signature
sig -> Signature -> Declaration
TypeSig (Signature -> Signature
closeSignature Signature
sig)
Declaration
otherwise -> Declaration
d
closeClassDecl :: ClassDeclaration -> ClassDeclaration
closeClassDecl :: ClassDeclaration -> ClassDeclaration
closeClassDecl ClassDeclaration
d =
ClassDeclaration
d { classFuns :: [Signature]
classFuns = forall a b. (a -> b) -> [a] -> [b]
map (TypeVariable -> Signature -> Signature
closureWithout (ClassDeclaration -> TypeVariable
classVar ClassDeclaration
d)) (ClassDeclaration -> [Signature]
classFuns ClassDeclaration
d) }
where
closureWithout :: TypeVariable -> Signature -> Signature
closureWithout TypeVariable
v Signature
s =
let t :: TypeExpression
t = Signature -> TypeExpression
signatureType Signature
s
freeVars :: Set TypeVariable
freeVars = TypeExpression -> Set TypeVariable
freeTypeVariables TypeExpression
t forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` forall a. a -> Set a
Set.singleton TypeVariable
v
in Signature
s { signatureType :: TypeExpression
signatureType = Set TypeVariable -> TypeExpression -> TypeExpression
closureFor Set TypeVariable
freeVars TypeExpression
t }
closeSignature :: Signature -> Signature
closeSignature :: Signature -> Signature
closeSignature Signature
s =
let t :: TypeExpression
t = Signature -> TypeExpression
signatureType Signature
s
in Signature
s { signatureType :: TypeExpression
signatureType = Set TypeVariable -> TypeExpression -> TypeExpression
closureFor (TypeExpression -> Set TypeVariable
freeTypeVariables TypeExpression
t) TypeExpression
t }
closureFor :: Set.Set TypeVariable -> TypeExpression -> TypeExpression
closureFor :: Set TypeVariable -> TypeExpression -> TypeExpression
closureFor Set TypeVariable
vs TypeExpression
t = forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\TypeVariable
v -> TypeVariable -> [TypeClass] -> TypeExpression -> TypeExpression
TypeAbs TypeVariable
v []) TypeExpression
t Set TypeVariable
vs