module Momo.ModTyping
  ( typeModule
  , ModTypingError(..)
  ) where

import Control.Monad (unless, when)
import Control.Monad.Catch (Exception, MonadThrow(throwM))
import Data.Foldable (for_)
import Data.Map.Strict qualified as Map
import Data.Text (Text)

import Momo.CoreTyping qualified as CT
import Momo.CoreSyntax qualified as Core
import Momo.Env (Env)
import Momo.Env qualified as Env
import Momo.Ident (Ident(..))
import Momo.Path (Path)
import Momo.Path qualified as Path
import Momo.ModSyntax qualified as Mod
import Momo.Subst (Subst)

data ModTypingError
  = CircularValue Text
  | CircularType Text
  | CircularModule Text
  | KindMismatch Text
  | UnmatchedSignatureComponent Text
  | ValueComponentsMismatch Text Text
  | TypeComponentsMismatch Text Text
  | ModuleTypeMismatch
  deriving (ModTypingError -> ModTypingError -> Bool
(ModTypingError -> ModTypingError -> Bool)
-> (ModTypingError -> ModTypingError -> Bool) -> Eq ModTypingError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ModTypingError -> ModTypingError -> Bool
$c/= :: ModTypingError -> ModTypingError -> Bool
== :: ModTypingError -> ModTypingError -> Bool
$c== :: ModTypingError -> ModTypingError -> Bool
Eq, Eq ModTypingError
Eq ModTypingError
-> (ModTypingError -> ModTypingError -> Ordering)
-> (ModTypingError -> ModTypingError -> Bool)
-> (ModTypingError -> ModTypingError -> Bool)
-> (ModTypingError -> ModTypingError -> Bool)
-> (ModTypingError -> ModTypingError -> Bool)
-> (ModTypingError -> ModTypingError -> ModTypingError)
-> (ModTypingError -> ModTypingError -> ModTypingError)
-> Ord ModTypingError
ModTypingError -> ModTypingError -> Bool
ModTypingError -> ModTypingError -> Ordering
ModTypingError -> ModTypingError -> ModTypingError
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ModTypingError -> ModTypingError -> ModTypingError
$cmin :: ModTypingError -> ModTypingError -> ModTypingError
max :: ModTypingError -> ModTypingError -> ModTypingError
$cmax :: ModTypingError -> ModTypingError -> ModTypingError
>= :: ModTypingError -> ModTypingError -> Bool
$c>= :: ModTypingError -> ModTypingError -> Bool
> :: ModTypingError -> ModTypingError -> Bool
$c> :: ModTypingError -> ModTypingError -> Bool
<= :: ModTypingError -> ModTypingError -> Bool
$c<= :: ModTypingError -> ModTypingError -> Bool
< :: ModTypingError -> ModTypingError -> Bool
$c< :: ModTypingError -> ModTypingError -> Bool
compare :: ModTypingError -> ModTypingError -> Ordering
$ccompare :: ModTypingError -> ModTypingError -> Ordering
Ord, Int -> ModTypingError -> ShowS
[ModTypingError] -> ShowS
ModTypingError -> String
(Int -> ModTypingError -> ShowS)
-> (ModTypingError -> String)
-> ([ModTypingError] -> ShowS)
-> Show ModTypingError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModTypingError] -> ShowS
$cshowList :: [ModTypingError] -> ShowS
show :: ModTypingError -> String
$cshow :: ModTypingError -> String
showsPrec :: Int -> ModTypingError -> ShowS
$cshowsPrec :: Int -> ModTypingError -> ShowS
Show)

instance Exception ModTypingError

typeModule
  :: forall term m
  .  ( CT.CoreTyping term
     , MonadThrow m
     )
  => Env term
  -> Mod.ModTerm term
  -> m (Mod.ModType term)
typeModule :: forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModTerm term -> m (ModType term)
typeModule Env term
env = \case
  Mod.LongIdent Path
path ->
    Path -> Env term -> m (ModType term)
forall {k} (term :: k) (m :: * -> *).
(CoreSyntax term, MonadThrow m) =>
Path -> Env term -> m (ModType term)
Env.findModule Path
path Env term
env m (ModType term)
-> (ModType term -> m (ModType term)) -> m (ModType term)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
      Path -> ModType term -> m (ModType term)
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Path -> ModType term -> m (ModType term)
strengthenModType Path
path

  Mod.Structure [Definition term]
struct ->
    ([Specification term] -> ModType term)
-> m [Specification term] -> m (ModType term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Specification term] -> ModType term
forall {k} (term :: k). [Specification term] -> ModType term
Mod.Signature (m [Specification term] -> m (ModType term))
-> m [Specification term] -> m (ModType term)
forall a b. (a -> b) -> a -> b
$
      Env term -> [Text] -> [Definition term] -> m [Specification term]
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> [Text] -> [Definition term] -> m [Specification term]
typeStructure Env term
env [] [Definition term]
struct

  Mod.Functor Ident
param ModType term
mty ModTerm term
body -> do
    Env term -> ModType term -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModType term -> m ()
checkModType Env term
env ModType term
mty
    (ModType term -> ModType term)
-> m (ModType term) -> m (ModType term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ident -> ModType term -> ModType term -> ModType term
forall {k} (term :: k).
Ident -> ModType term -> ModType term -> ModType term
Mod.FunctorType Ident
param ModType term
mty) (m (ModType term) -> m (ModType term))
-> m (ModType term) -> m (ModType term)
forall a b. (a -> b) -> a -> b
$
      Env term -> ModTerm term -> m (ModType term)
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModTerm term -> m (ModType term)
typeModule
        (Ident -> ModType term -> Env term -> Env term
forall {k} (term :: k).
Ident -> ModType term -> Env term -> Env term
Env.addModule Ident
param ModType term
mty Env term
env)
        ModTerm term
body

  Mod.Apply ModTerm term
funct ModTerm term
arg ->
    case ModTerm term
arg of
      Mod.LongIdent Path
path ->
        Env term -> ModTerm term -> m (ModType term)
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModTerm term -> m (ModType term)
typeModule Env term
env ModTerm term
funct m (ModType term)
-> (ModType term -> m (ModType term)) -> m (ModType term)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Mod.FunctorType Ident
param ModType term
mty_param ModType term
mty_res -> do
            ModType term
mty_arg <- Env term -> ModTerm term -> m (ModType term)
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModTerm term -> m (ModType term)
typeModule Env term
env ModTerm term
arg
            Env term -> ModType term -> ModType term -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModType term -> ModType term -> m ()
modTypeMatch Env term
env ModType term
mty_arg ModType term
mty_param
            ModType term -> m (ModType term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModType term -> m (ModType term))
-> ModType term -> m (ModType term)
forall a b. (a -> b) -> a -> b
$ ModType term -> Subst -> ModType term
forall {k} (term :: k).
CoreSyntax term =>
ModType term -> Subst -> ModType term
Mod.substModType ModType term
mty_res (Ident -> Path -> Subst
forall k a. k -> a -> Map k a
Map.singleton Ident
param Path
path)
          ModType term
_nonFunctor ->
            String -> m (ModType term)
forall a. HasCallStack => String -> a
error String
"application of a non-functor"
      ModTerm term
_nonPath ->
        String -> m (ModType term)
forall a. HasCallStack => String -> a
error String
"application of a functor to a non-path"

  Mod.Constraint ModTerm term
modl ModType term
mty -> do
    Env term -> ModType term -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModType term -> m ()
checkModType Env term
env ModType term
mty

    ModType term
sig <- Env term -> ModTerm term -> m (ModType term)
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModTerm term -> m (ModType term)
typeModule Env term
env ModTerm term
modl
    Env term -> ModType term -> ModType term -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModType term -> ModType term -> m ()
modTypeMatch Env term
env ModType term
sig ModType term
mty

    ModType term -> m (ModType term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModType term
mty

typeStructure
  :: ( CT.CoreTyping term
     , MonadThrow m
     )
  => Env term
  -> [Text]
  -> [Mod.Definition term]
  -> m [Mod.Specification term]
typeStructure :: forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> [Text] -> [Definition term] -> m [Specification term]
typeStructure Env term
env [Text]
seen = \case
  [] ->
    [Specification term] -> m [Specification term]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  Definition term
structItem : [Definition term]
remaining -> do
    ([Text]
seen', Specification term
sigItem) <- Env term
-> [Text] -> Definition term -> m ([Text], Specification term)
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term
-> [Text] -> Definition term -> m ([Text], Specification term)
typeDefinition Env term
env [Text]
seen Definition term
structItem
    [Specification term]
next <- Env term -> [Text] -> [Definition term] -> m [Specification term]
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> [Text] -> [Definition term] -> m [Specification term]
typeStructure (Specification term -> Env term -> Env term
forall {k} (term :: k). Specification term -> Env term -> Env term
Env.addSpec Specification term
sigItem Env term
env) [Text]
seen' [Definition term]
remaining
    [Specification term] -> m [Specification term]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification term
sigItem Specification term -> [Specification term] -> [Specification term]
forall a. a -> [a] -> [a]
: [Specification term]
next)

typeDefinition
  :: ( CT.CoreTyping term
     , MonadThrow m
     )
  => Env term
  -> [Text]
  -> Mod.Definition term
  -> m ([Text], Mod.Specification term)
typeDefinition :: forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term
-> [Text] -> Definition term -> m ([Text], Specification term)
typeDefinition Env term
env [Text]
seen = \case
  Mod.ValueStr Ident
ident term
term -> do
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Ident
ident.name Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
seen) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      ModTypingError -> m ()
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM (ModTypingError -> m ()) -> ModTypingError -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> ModTypingError
CircularValue Ident
ident.name
    Val term
typ <- Env term -> term -> m (Val term)
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> term -> m (Val term)
CT.typeTerm Env term
env term
term
    ([Text], Specification term) -> m ([Text], Specification term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( Ident
ident.name Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
seen
      , Ident -> Val term -> Specification term
forall {k} (term :: k). Ident -> Val term -> Specification term
Mod.ValueSig Ident
ident Val term
typ
      )

  Mod.ModuleStr Ident
ident ModTerm term
modl -> do
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Ident
ident.name Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
seen) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      ModTypingError -> m ()
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM (ModTypingError -> m ()) -> ModTypingError -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> ModTypingError
CircularModule Ident
ident.name
    ModType term
sig <- Env term -> ModTerm term -> m (ModType term)
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModTerm term -> m (ModType term)
typeModule Env term
env ModTerm term
modl
    ([Text], Specification term) -> m ([Text], Specification term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( Ident
ident.name Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
seen
      , Ident -> ModType term -> Specification term
forall {k} (term :: k). Ident -> ModType term -> Specification term
Mod.ModuleSig Ident
ident ModType term
sig
      )

  Mod.TypeStr Ident
ident Kind term
kind Def term
typ -> do
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Ident
ident.name Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
seen) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      ModTypingError -> m ()
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM (ModTypingError -> m ()) -> ModTypingError -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> ModTypingError
CircularType Ident
ident.name
    Env term -> Kind term -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> Kind term -> m ()
CT.checkKind Env term
env Kind term
kind
    Kind term
kind' <- Env term -> Def term -> m (Kind term)
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> Def term -> m (Kind term)
CT.kindDefType Env term
env Def term
typ
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Env term -> Kind term -> Kind term -> Bool
forall term.
CoreTyping term =>
Env term -> Kind term -> Kind term -> Bool
CT.kindMatch Env term
env Kind term
kind' Kind term
kind) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      ModTypingError -> m ()
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM (ModTypingError -> m ()) -> ModTypingError -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> ModTypingError
KindMismatch Ident
ident.name
    ([Text], Specification term) -> m ([Text], Specification term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( Ident
ident.name Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
seen
      , Ident -> TypeDecl term -> Specification term
forall {k} (term :: k).
Ident -> TypeDecl term -> Specification term
Mod.TypeSig Ident
ident Mod.TypeDecl
          { kind :: Kind term
kind = Kind term
kind
          , manifest :: Maybe (Def term)
manifest = Def term -> Maybe (Def term)
forall a. a -> Maybe a
Just Def term
typ
          }
      )

checkModType
  :: ( CT.CoreTyping term
     , MonadThrow m
     )
  => Env term
  -> Mod.ModType term
  -> m ()
checkModType :: forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModType term -> m ()
checkModType Env term
env = \case
  Mod.Signature [Specification term]
sg ->
    Env term -> [Text] -> [Specification term] -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> [Text] -> [Specification term] -> m ()
checkSignature Env term
env [Text]
forall a. Monoid a => a
mempty [Specification term]
sg
  Mod.FunctorType Ident
param ModType term
arg ModType term
res -> do
    Env term -> ModType term -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModType term -> m ()
checkModType Env term
env ModType term
arg
    Env term -> ModType term -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModType term -> m ()
checkModType (Ident -> ModType term -> Env term -> Env term
forall {k} (term :: k).
Ident -> ModType term -> Env term -> Env term
Env.addModule Ident
param ModType term
arg Env term
env) ModType term
res

checkSignature
  :: ( CT.CoreTyping term
     , MonadThrow m
     )
  => Env term
  -> [Text]
  -> [Mod.Specification term]
  -> m ()
checkSignature :: forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> [Text] -> [Specification term] -> m ()
checkSignature Env term
env [Text]
seen = \case
  [] ->
    () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  Mod.ValueSig Ident
ident Val term
vty : [Specification term]
remaining -> do
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Ident
ident.name Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
seen) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      ModTypingError -> m ()
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM (ModTypingError -> m ()) -> ModTypingError -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> ModTypingError
CircularValue Ident
ident.name
    Env term -> Val term -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> Val term -> m ()
CT.checkValType Env term
env Val term
vty
    Env term -> [Text] -> [Specification term] -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> [Text] -> [Specification term] -> m ()
checkSignature Env term
env (Ident
ident.name Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
seen) [Specification term]
remaining

  Mod.TypeSig Ident
ident TypeDecl term
decl : [Specification term]
remaining -> do
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Ident
ident.name Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
seen) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      ModTypingError -> m ()
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM (ModTypingError -> m ()) -> ModTypingError -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> ModTypingError
CircularType Ident
ident.name
    Env term -> Kind term -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> Kind term -> m ()
CT.checkKind Env term
env TypeDecl term
decl.kind
    Maybe (Def term) -> (Def term -> m ()) -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ TypeDecl term
decl.manifest \Def term
typ -> do
      Kind term
kind' <- Env term -> Def term -> m (Kind term)
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> Def term -> m (Kind term)
CT.kindDefType Env term
env Def term
typ
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Env term -> Kind term -> Kind term -> Bool
forall term.
CoreTyping term =>
Env term -> Kind term -> Kind term -> Bool
CT.kindMatch Env term
env Kind term
kind' TypeDecl term
decl.kind) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        ModTypingError -> m ()
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM (ModTypingError -> m ()) -> ModTypingError -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> ModTypingError
KindMismatch Ident
ident.name
    Env term -> [Text] -> [Specification term] -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> [Text] -> [Specification term] -> m ()
checkSignature
      (Ident -> TypeDecl term -> Env term -> Env term
forall {k} (term :: k).
Ident -> TypeDecl term -> Env term -> Env term
Env.addType Ident
ident TypeDecl term
decl Env term
env)
      (Ident
ident.name Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
seen)
      [Specification term]
remaining

  Mod.ModuleSig Ident
ident ModType term
mty : [Specification term]
remaining -> do
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Ident
ident.name Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Text]
seen) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      ModTypingError -> m ()
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM (ModTypingError -> m ()) -> ModTypingError -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> ModTypingError
CircularModule Ident
ident.name
    Env term -> ModType term -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModType term -> m ()
checkModType Env term
env ModType term
mty
    Env term -> [Text] -> [Specification term] -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> [Text] -> [Specification term] -> m ()
checkSignature
      (Ident -> ModType term -> Env term -> Env term
forall {k} (term :: k).
Ident -> ModType term -> Env term -> Env term
Env.addModule Ident
ident ModType term
mty Env term
env)
      (Ident
ident.name Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
seen)
      [Specification term]
remaining

modTypeMatch
  :: forall term m
  . ( CT.CoreTyping term
    , MonadThrow m
    )
  => Env term
  -> Mod.ModType term
  -> Mod.ModType term
  -> m ()
modTypeMatch :: forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModType term -> ModType term -> m ()
modTypeMatch Env term
env ModType term
mty1 ModType term
mty2 =
  case (ModType term
mty1, ModType term
mty2) of
    (Mod.Signature [Specification term]
sig1, Mod.Signature [Specification term]
sig2) -> do
      ([(Specification term, Specification term)]
pairedComponents, Subst
subst) <- [Specification term]
-> [Specification term]
-> m ([(Specification term, Specification term)], Subst)
forall {k} (term :: k) (m :: * -> *).
(CoreSyntax term, MonadThrow m) =>
[Specification term]
-> [Specification term]
-> m ([(Specification term, Specification term)], Subst)
pairSignatureComponents [Specification term]
sig1 [Specification term]
sig2
      let extEnv :: Env term
extEnv = [Specification term] -> Env term -> Env term
forall {k} (term :: k).
[Specification term] -> Env term -> Env term
Env.addSignature [Specification term]
sig1 Env term
env
      [(Specification term, Specification term)]
-> ((Specification term, Specification term) -> m ()) -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Specification term, Specification term)]
pairedComponents (((Specification term, Specification term) -> m ()) -> m ())
-> ((Specification term, Specification term) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$
        forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term
-> Subst -> (Specification term, Specification term) -> m ()
specificationMatch @term Env term
extEnv Subst
subst

    (Mod.FunctorType Ident
param1 ModType term
arg1 ModType term
res1, Mod.FunctorType Ident
param2 ModType term
arg2 ModType term
res2) -> do
      let subst :: Subst
subst = Ident -> Path -> Subst
forall k a. k -> a -> Map k a
Map.singleton Ident
param1 (Ident -> Path
Path.Ident Ident
param2)
      let res1' :: ModType term
res1' = ModType term -> Subst -> ModType term
forall {k} (term :: k).
CoreSyntax term =>
ModType term -> Subst -> ModType term
Mod.substModType ModType term
res1 Subst
subst
      Env term -> ModType term -> ModType term -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModType term -> ModType term -> m ()
modTypeMatch Env term
env ModType term
arg2 ModType term
arg1
      Env term -> ModType term -> ModType term -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModType term -> ModType term -> m ()
modTypeMatch (Ident -> ModType term -> Env term -> Env term
forall {k} (term :: k).
Ident -> ModType term -> Env term -> Env term
Env.addModule Ident
param2 ModType term
arg2 Env term
env) ModType term
res1' ModType term
res2

    (ModType term, ModType term)
_ ->
      ModTypingError -> m ()
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM ModTypingError
ModuleTypeMismatch

pairSignatureComponents
  :: (Core.CoreSyntax term, MonadThrow m)
  => [Mod.Specification term]
  -> [Mod.Specification term]
  -> m
    ( [ (Mod.Specification term, Mod.Specification term) ]
    , Subst
    )
pairSignatureComponents :: forall {k} (term :: k) (m :: * -> *).
(CoreSyntax term, MonadThrow m) =>
[Specification term]
-> [Specification term]
-> m ([(Specification term, Specification term)], Subst)
pairSignatureComponents [Specification term]
sig1 [Specification term]
sig2 =
  case [Specification term]
sig2 of
    [] ->
      ([(Specification term, Specification term)], Subst)
-> m ([(Specification term, Specification term)], Subst)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], Subst
forall a. Monoid a => a
mempty)
    Specification term
item2 : [Specification term]
remaining2 -> do
      let
        findMatchingComponent :: [Specification term] -> m (Ident, Ident, Specification term)
findMatchingComponent = \case
          [] ->
            ModTypingError -> m (Ident, Ident, Specification term)
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM (ModTypingError -> m (Ident, Ident, Specification term))
-> ModTypingError -> m (Ident, Ident, Specification term)
forall a b. (a -> b) -> a -> b
$ Text -> ModTypingError
UnmatchedSignatureComponent (Text -> ModTypingError) -> Text -> ModTypingError
forall a b. (a -> b) -> a -> b
$
              case Specification term
item2 of
                Mod.ValueSig Ident
ident2 Val term
_ ->
                  Ident
ident2.name
                Mod.TypeSig Ident
ident2 TypeDecl term
_ ->
                  Ident
ident2.name
                Mod.ModuleSig Ident
ident2 ModType term
_ ->
                  Ident
ident2.name

          Specification term
item1 : [Specification term]
remaining1 ->
            case (Specification term
item1, Specification term
item2) of
              (Mod.ValueSig Ident
ident1 Val term
_, Mod.ValueSig Ident
ident2 Val term
_)
                | Ident
ident1.name Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
ident2.name ->
                    (Ident, Ident, Specification term)
-> m (Ident, Ident, Specification term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ident
ident1, Ident
ident2, Specification term
item1)

              (Mod.TypeSig Ident
ident1 TypeDecl term
_, Mod.TypeSig Ident
ident2 TypeDecl term
_)
                | Ident
ident1.name Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
ident2.name ->
                    (Ident, Ident, Specification term)
-> m (Ident, Ident, Specification term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ident
ident1, Ident
ident2, Specification term
item1)

              (Mod.ModuleSig Ident
ident1 ModType term
_, Mod.ModuleSig Ident
ident2 ModType term
_)
                | Ident
ident1.name Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
ident2.name ->
                    (Ident, Ident, Specification term)
-> m (Ident, Ident, Specification term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ident
ident1, Ident
ident2, Specification term
item1)

              (Specification term, Specification term)
_ ->
                [Specification term] -> m (Ident, Ident, Specification term)
findMatchingComponent [Specification term]
remaining1

      (Ident
ident1, Ident
ident2, Specification term
item1) <- [Specification term] -> m (Ident, Ident, Specification term)
findMatchingComponent [Specification term]
sig1
      ([(Specification term, Specification term)]
pairs, Subst
subst) <- [Specification term]
-> [Specification term]
-> m ([(Specification term, Specification term)], Subst)
forall {k} (term :: k) (m :: * -> *).
(CoreSyntax term, MonadThrow m) =>
[Specification term]
-> [Specification term]
-> m ([(Specification term, Specification term)], Subst)
pairSignatureComponents [Specification term]
sig1 [Specification term]
remaining2

      ([(Specification term, Specification term)], Subst)
-> m ([(Specification term, Specification term)], Subst)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Specification term
item1, Specification term
item2) (Specification term, Specification term)
-> [(Specification term, Specification term)]
-> [(Specification term, Specification term)]
forall a. a -> [a] -> [a]
: [(Specification term, Specification term)]
pairs
        , Ident -> Path -> Subst -> Subst
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
ident2 (Ident -> Path
Path.Ident Ident
ident1) Subst
subst
        )

specificationMatch
  :: forall term m
  .  ( CT.CoreTyping term
     , MonadThrow m
     )
  => Env term
  -> Subst
  -> (Mod.Specification term, Mod.Specification term)
  -> m ()
specificationMatch :: forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term
-> Subst -> (Specification term, Specification term) -> m ()
specificationMatch Env term
env Subst
subst = \case
  (Mod.ValueSig Ident
ident1 Val term
vty1, Mod.ValueSig Ident
ident2 Val term
vty2) ->
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Env term -> Val term -> Val term -> Bool
forall term.
CoreTyping term =>
Env term -> Val term -> Val term -> Bool
CT.valTypeMatch Env term
env Val term
vty1 (forall term. CoreSyntax term => Val term -> Subst -> Val term
forall {k} (term :: k).
CoreSyntax term =>
Val term -> Subst -> Val term
Core.substVal @term Val term
vty2 Subst
subst)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      ModTypingError -> m ()
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM (ModTypingError -> m ()) -> ModTypingError -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> Text -> ModTypingError
ValueComponentsMismatch Ident
ident1.name Ident
ident2.name

  (Mod.TypeSig Ident
ident1 TypeDecl term
decl1, Mod.TypeSig Ident
ident2 TypeDecl term
decl2) -> do
    let decl2' :: TypeDecl term
decl2' = forall term.
CoreSyntax term =>
TypeDecl term -> Subst -> TypeDecl term
forall {k} (term :: k).
CoreSyntax term =>
TypeDecl term -> Subst -> TypeDecl term
Mod.substTypeDecl @term TypeDecl term
decl2 Subst
subst :: Mod.TypeDecl term
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall term.
CoreTyping term =>
Env term -> Ident -> TypeDecl term -> TypeDecl term -> Bool
typeDeclMatch @term Env term
env Ident
ident1 TypeDecl term
decl1 TypeDecl term
decl2') (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      ModTypingError -> m ()
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM (ModTypingError -> m ()) -> ModTypingError -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> Text -> ModTypingError
TypeComponentsMismatch Ident
ident1.name Ident
ident2.name

  (Mod.ModuleSig Ident
_ ModType term
mty1, Mod.ModuleSig Ident
_ ModType term
mty2) ->
    Env term -> ModType term -> ModType term -> m ()
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Env term -> ModType term -> ModType term -> m ()
modTypeMatch Env term
env ModType term
mty1 (ModType term -> Subst -> ModType term
forall {k} (term :: k).
CoreSyntax term =>
ModType term -> Subst -> ModType term
Mod.substModType ModType term
mty2 Subst
subst)

  (Specification term, Specification term)
_brokenPairing ->
    String -> m ()
forall a. HasCallStack => String -> a
error String
"Invalid signature component pair"

typeDeclMatch
  :: forall term
  . CT.CoreTyping term
  => Env term
  -> Ident
  -> Mod.TypeDecl term
  -> Mod.TypeDecl term
  -> Bool
typeDeclMatch :: forall term.
CoreTyping term =>
Env term -> Ident -> TypeDecl term -> TypeDecl term -> Bool
typeDeclMatch Env term
env Ident
ident TypeDecl term
decl1 TypeDecl term
decl2 = Bool
kindMatches Bool -> Bool -> Bool
&& Bool
manifestMatches
  where
    kindMatches :: Bool
kindMatches =
      Env term -> Kind term -> Kind term -> Bool
forall term.
CoreTyping term =>
Env term -> Kind term -> Kind term -> Bool
CT.kindMatch Env term
env TypeDecl term
decl1.kind TypeDecl term
decl2.kind

    manifestMatches :: Bool
manifestMatches =
      case (TypeDecl term
decl1.manifest, TypeDecl term
decl2.manifest) of
        (Maybe (Def term)
_, Maybe (Def term)
Nothing) ->
          Bool
True

        (Just Def term
typ1, Just Def term
typ2) ->
          Env term -> Kind term -> Def term -> Def term -> Bool
forall term.
CoreTyping term =>
Env term -> Kind term -> Def term -> Def term -> Bool
CT.defTypeEquiv Env term
env TypeDecl term
decl2.kind Def term
typ1 Def term
typ2

        (Maybe (Def term)
Nothing, Just Def term
typ2) ->
          Env term -> Kind term -> Def term -> Def term -> Bool
forall term.
CoreTyping term =>
Env term -> Kind term -> Def term -> Def term -> Bool
CT.defTypeEquiv
            Env term
env
            TypeDecl term
decl2.kind
            ( forall term. CoreTyping term => Path -> Kind term -> Def term
CT.deftypeOfPath
                @term
                (Ident -> Path
Path.Ident Ident
ident)
                TypeDecl term
decl1.kind
            )
            Def term
typ2

strengthenModType
  :: ( CT.CoreTyping term
     , MonadThrow m
     )
  => Path
  -> Mod.ModType term
  -> m (Mod.ModType term)
strengthenModType :: forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Path -> ModType term -> m (ModType term)
strengthenModType Path
path = \case
  Mod.Signature [Specification term]
sg ->
    ([Specification term] -> ModType term)
-> m [Specification term] -> m (ModType term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Specification term] -> ModType term
forall {k} (term :: k). [Specification term] -> ModType term
Mod.Signature (m [Specification term] -> m (ModType term))
-> m [Specification term] -> m (ModType term)
forall a b. (a -> b) -> a -> b
$
      (Specification term -> m (Specification term))
-> [Specification term] -> m [Specification term]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Path -> Specification term -> m (Specification term)
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Path -> Specification term -> m (Specification term)
strengthenSpec Path
path) [Specification term]
sg

  mty :: ModType term
mty@Mod.FunctorType{} ->
    ModType term -> m (ModType term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModType term
mty

strengthenSpec
  :: forall term m
  .  ( CT.CoreTyping term
     , MonadThrow m
     )
  => Path
  -> Mod.Specification term
  -> m (Mod.Specification term)
strengthenSpec :: forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Path -> Specification term -> m (Specification term)
strengthenSpec Path
path = \case
  item :: Specification term
item@Mod.ValueSig{} ->
    Specification term -> m (Specification term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Specification term
item

  Mod.TypeSig Ident
ident TypeDecl term
decl -> do
    let
      manifest' :: Def term
manifest' =
        case TypeDecl term
decl.manifest of
          Just Def term
ty ->
            Def term
ty
          Maybe (Def term)
Nothing ->
            forall term. CoreTyping term => Path -> Kind term -> Def term
CT.deftypeOfPath
              @term
              (Path -> Text -> Path
Path.Dot Path
path Ident
ident.name)
              TypeDecl term
decl.kind
    Specification term -> m (Specification term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification term -> m (Specification term))
-> Specification term -> m (Specification term)
forall a b. (a -> b) -> a -> b
$
      Ident -> TypeDecl term -> Specification term
forall {k} (term :: k).
Ident -> TypeDecl term -> Specification term
Mod.TypeSig Ident
ident Mod.TypeDecl
        { kind :: Kind term
kind     = TypeDecl term
decl.kind
        , manifest :: Maybe (Def term)
manifest = Def term -> Maybe (Def term)
forall a. a -> Maybe a
Just Def term
manifest'
        }

  Mod.ModuleSig Ident
ident ModType term
mty ->
    (ModType term -> Specification term)
-> m (ModType term) -> m (Specification term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ident -> ModType term -> Specification term
forall {k} (term :: k). Ident -> ModType term -> Specification term
Mod.ModuleSig Ident
ident) (m (ModType term) -> m (Specification term))
-> m (ModType term) -> m (Specification term)
forall a b. (a -> b) -> a -> b
$
      Path -> ModType term -> m (ModType term)
forall term (m :: * -> *).
(CoreTyping term, MonadThrow m) =>
Path -> ModType term -> m (ModType term)
strengthenModType
        (Path -> Text -> Path
Path.Dot Path
path Ident
ident.name)
        ModType term
mty