module Hydra.Types.Substitution where

import Hydra.All
import Hydra.Impl.Haskell.Dsl.Types as Types

import qualified Data.List as L
import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.Maybe as Y

import Hydra.Util.Debug


type Subst m = M.Map VariableType (Type m)

composeSubst :: Subst m -> Subst m -> Subst m
composeSubst :: forall m. Subst m -> Subst m -> Subst m
composeSubst Subst m
s1 Subst m
s2 = forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Subst m
s1 forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall m. Map VariableType (Type m) -> Type m -> Type m
substituteInType Subst m
s1) Subst m
s2

normalVariables :: [VariableType]
normalVariables :: [VariableType]
normalVariables = (\Integer
n -> String -> VariableType
VariableType forall a b. (a -> b) -> a -> b
$ String
"v" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
1..]

normalizeScheme :: Show m => TypeScheme m -> TypeScheme m
normalizeScheme :: forall m. Show m => TypeScheme m -> TypeScheme m
normalizeScheme ts :: TypeScheme m
ts@(TypeScheme [VariableType]
_ Type m
body) = forall m. [VariableType] -> Type m -> TypeScheme m
TypeScheme (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd [(VariableType, VariableType)]
ord) (forall {m}. Type m -> Type m
normalizeType Type m
body)
  where
    ord :: [(VariableType, VariableType)]
ord = forall a b. [a] -> [b] -> [(a, b)]
L.zip (forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ forall m. Type m -> Set VariableType
freeVariablesInType Type m
body) [VariableType]
normalVariables

    normalizeFieldType :: FieldType m -> FieldType m
normalizeFieldType (FieldType FieldName
fname Type m
typ) = forall m. FieldName -> Type m -> FieldType m
FieldType FieldName
fname forall a b. (a -> b) -> a -> b
$ Type m -> Type m
normalizeType Type m
typ

    normalizeType :: Type m -> Type m
normalizeType Type m
typ = case Type m
typ of
      TypeApplication (ApplicationType Type m
lhs Type m
rhs) -> forall m. ApplicationType m -> Type m
TypeApplication (forall m. Type m -> Type m -> ApplicationType m
ApplicationType (Type m -> Type m
normalizeType Type m
lhs) (Type m -> Type m
normalizeType Type m
rhs))
      TypeAnnotated (Annotated Type m
t m
ann) -> forall m. Annotated (Type m) m -> Type m
TypeAnnotated (forall a m. a -> m -> Annotated a m
Annotated (Type m -> Type m
normalizeType Type m
t) m
ann)
      TypeElement Type m
t -> forall {m}. Type m -> Type m
element forall a b. (a -> b) -> a -> b
$ Type m -> Type m
normalizeType Type m
t
      TypeFunction (FunctionType Type m
dom Type m
cod) -> forall m. Type m -> Type m -> Type m
function (Type m -> Type m
normalizeType Type m
dom) (Type m -> Type m
normalizeType Type m
cod)
      TypeList Type m
t -> forall {m}. Type m -> Type m
list forall a b. (a -> b) -> a -> b
$ Type m -> Type m
normalizeType Type m
t
      TypeLiteral LiteralType
_ -> Type m
typ
      TypeMap (MapType Type m
kt Type m
vt) -> forall m. Type m -> Type m -> Type m
Types.map (Type m -> Type m
normalizeType Type m
kt) (Type m -> Type m
normalizeType Type m
vt)
      TypeNominal Name
_ -> Type m
typ
      TypeOptional Type m
t -> forall {m}. Type m -> Type m
optional forall a b. (a -> b) -> a -> b
$ Type m -> Type m
normalizeType Type m
t
      TypeProduct [Type m]
types -> forall m. [Type m] -> Type m
TypeProduct (Type m -> Type m
normalizeType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type m]
types)
      TypeRecord (RowType Name
n Maybe Name
e [FieldType m]
fields) -> forall m. RowType m -> Type m
TypeRecord forall a b. (a -> b) -> a -> b
$ forall m. Name -> Maybe Name -> [FieldType m] -> RowType m
RowType Name
n Maybe Name
e (FieldType m -> FieldType m
normalizeFieldType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldType m]
fields)
      TypeSet Type m
t -> forall {m}. Type m -> Type m
set forall a b. (a -> b) -> a -> b
$ Type m -> Type m
normalizeType Type m
t
      TypeSum [Type m]
types -> forall m. [Type m] -> Type m
TypeSum (Type m -> Type m
normalizeType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type m]
types)
      TypeUnion (RowType Name
n Maybe Name
e [FieldType m]
fields) -> forall m. RowType m -> Type m
TypeUnion forall a b. (a -> b) -> a -> b
$ forall m. Name -> Maybe Name -> [FieldType m] -> RowType m
RowType Name
n Maybe Name
e (FieldType m -> FieldType m
normalizeFieldType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldType m]
fields)
      TypeLambda (LambdaType (VariableType String
v) Type m
t) -> forall m. LambdaType m -> Type m
TypeLambda (forall m. VariableType -> Type m -> LambdaType m
LambdaType (String -> VariableType
VariableType String
v) forall a b. (a -> b) -> a -> b
$ Type m -> Type m
normalizeType Type m
t)
      TypeVariable VariableType
v -> case forall a b. Eq a => a -> [(a, b)] -> Maybe b
Prelude.lookup VariableType
v [(VariableType, VariableType)]
ord of
        Just (VariableType String
v1) -> forall m. String -> Type m
variable String
v1
        Maybe VariableType
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"type variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show VariableType
v forall a. [a] -> [a] -> [a]
++ String
" not in signature of type scheme: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeScheme m
ts

substituteInScheme :: M.Map VariableType (Type m) -> TypeScheme m -> TypeScheme m
substituteInScheme :: forall m. Map VariableType (Type m) -> TypeScheme m -> TypeScheme m
substituteInScheme Map VariableType (Type m)
s (TypeScheme [VariableType]
as Type m
t) = forall m. [VariableType] -> Type m -> TypeScheme m
TypeScheme [VariableType]
as forall a b. (a -> b) -> a -> b
$ forall m. Map VariableType (Type m) -> Type m -> Type m
substituteInType Map VariableType (Type m)
s' Type m
t
  where
    s' :: Map VariableType (Type m)
s' = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr forall k a. Ord k => k -> Map k a -> Map k a
M.delete Map VariableType (Type m)
s [VariableType]
as

substituteInType :: M.Map VariableType (Type m) -> Type m -> Type m
substituteInType :: forall m. Map VariableType (Type m) -> Type m -> Type m
substituteInType Map VariableType (Type m)
s Type m
typ = case Type m
typ of
    TypeApplication (ApplicationType Type m
lhs Type m
rhs) -> forall m. ApplicationType m -> Type m
TypeApplication (forall m. Type m -> Type m -> ApplicationType m
ApplicationType (Type m -> Type m
subst Type m
lhs) (Type m -> Type m
subst Type m
rhs))
    TypeAnnotated (Annotated Type m
t m
ann) -> forall m. Annotated (Type m) m -> Type m
TypeAnnotated (forall a m. a -> m -> Annotated a m
Annotated (Type m -> Type m
subst Type m
t) m
ann)
    TypeElement Type m
t -> forall {m}. Type m -> Type m
element forall a b. (a -> b) -> a -> b
$ Type m -> Type m
subst Type m
t
    TypeFunction (FunctionType Type m
dom Type m
cod) -> forall m. Type m -> Type m -> Type m
function (Type m -> Type m
subst Type m
dom) (Type m -> Type m
subst Type m
cod)
    TypeList Type m
t -> forall {m}. Type m -> Type m
list forall a b. (a -> b) -> a -> b
$ Type m -> Type m
subst Type m
t
    TypeLiteral LiteralType
_ -> Type m
typ
    TypeMap (MapType Type m
kt Type m
vt) -> forall m. Type m -> Type m -> Type m
Types.map (Type m -> Type m
subst Type m
kt) (Type m -> Type m
subst Type m
vt)
    TypeNominal Name
_ -> Type m
typ -- because we do not allow names to be bound to types with free variables
    TypeOptional Type m
t -> forall {m}. Type m -> Type m
optional forall a b. (a -> b) -> a -> b
$ Type m -> Type m
subst Type m
t
    TypeProduct [Type m]
types -> forall m. [Type m] -> Type m
TypeProduct (Type m -> Type m
subst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type m]
types)
    TypeRecord (RowType Name
n Maybe Name
e [FieldType m]
fields) -> forall m. RowType m -> Type m
TypeRecord forall a b. (a -> b) -> a -> b
$ forall m. Name -> Maybe Name -> [FieldType m] -> RowType m
RowType Name
n Maybe Name
e (FieldType m -> FieldType m
substField forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldType m]
fields)
    TypeSet Type m
t -> forall {m}. Type m -> Type m
set forall a b. (a -> b) -> a -> b
$ Type m -> Type m
subst Type m
t
    TypeSum [Type m]
types -> forall m. [Type m] -> Type m
TypeSum (Type m -> Type m
subst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type m]
types)
    TypeUnion (RowType Name
n Maybe Name
e [FieldType m]
fields) -> forall m. RowType m -> Type m
TypeUnion forall a b. (a -> b) -> a -> b
$ forall m. Name -> Maybe Name -> [FieldType m] -> RowType m
RowType Name
n Maybe Name
e (FieldType m -> FieldType m
substField forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldType m]
fields)
    TypeLambda (LambdaType var :: VariableType
var@(VariableType String
v) Type m
body) -> if forall a. Maybe a -> Bool
Y.isNothing (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VariableType
var Map VariableType (Type m)
s)
      then forall m. LambdaType m -> Type m
TypeLambda (forall m. VariableType -> Type m -> LambdaType m
LambdaType (String -> VariableType
VariableType String
v) (Type m -> Type m
subst Type m
body))
      else Type m
typ
    TypeVariable VariableType
a -> forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault Type m
typ VariableType
a Map VariableType (Type m)
s
  where
    subst :: Type m -> Type m
subst = forall m. Map VariableType (Type m) -> Type m -> Type m
substituteInType Map VariableType (Type m)
s
    substField :: FieldType m -> FieldType m
substField (FieldType FieldName
fname Type m
t) = forall m. FieldName -> Type m -> FieldType m
FieldType FieldName
fname forall a b. (a -> b) -> a -> b
$ Type m -> Type m
subst Type m
t