{-# LANGUAGE UndecidableInstances #-} -- Eq/Ord/Show deriving

module Momo.ModSyntax
  ( Specification(..)
  , ModType(..)
  , TypeDecl(..)

  , Definition(..)
  , ModTerm(..)

  , substTypeDecl
  , substModType
  ) where

import Momo.CoreSyntax qualified as Core
import Momo.Ident (Ident)
import Momo.Path (Path)
import Momo.Subst (Subst)

data TypeDecl term = TypeDecl
  { forall {k} (term :: k). TypeDecl term -> Kind term
kind     :: Core.Kind term
  , forall {k} (term :: k). TypeDecl term -> Maybe (Def term)
manifest :: Maybe (Core.Def term)
  }

deriving instance Core.EqTerm term => Eq (TypeDecl term)
deriving instance Core.OrdTerm term => Ord (TypeDecl term)
deriving instance Core.ShowTerm term => Show (TypeDecl term)

data ModType term
  = Signature [Specification term]
  | FunctorType Ident (ModType term) (ModType term)

deriving instance Core.EqTerm term => Eq (ModType term)
deriving instance Core.OrdTerm term => Ord (ModType term)
deriving instance Core.ShowTerm term => Show (ModType term)

data Specification term
  = ValueSig Ident (Core.Val term)
  | TypeSig Ident (TypeDecl term)
  | ModuleSig Ident (ModType term)

deriving instance Core.EqTerm term => Eq (Specification term)
deriving instance Core.OrdTerm term => Ord (Specification term)
deriving instance Core.ShowTerm term => Show (Specification term)

data ModTerm term
  = LongIdent Path
  | Structure [Definition term]
  | Functor Ident (ModType term) (ModTerm term)
  | Apply (ModTerm term) (ModTerm term)
  | Constraint (ModTerm term) (ModType term)

deriving instance Core.EqTerm term => Eq (ModTerm term)
deriving instance Core.OrdTerm term => Ord (ModTerm term)
deriving instance Core.ShowTerm term => Show (ModTerm term)

data Definition term
  = ValueStr Ident term
  | TypeStr Ident (Core.Kind term) (Core.Def term)
  | ModuleStr Ident (ModTerm term)

deriving instance Core.EqTerm term => Eq (Definition term)
deriving instance Core.OrdTerm term => Ord (Definition term)
deriving instance Core.ShowTerm term => Show (Definition term)

substTypeDecl
  :: forall term
  .  Core.CoreSyntax term
  => TypeDecl term
  -> Subst
  -> TypeDecl term
substTypeDecl :: forall {k} (term :: k).
CoreSyntax term =>
TypeDecl term -> Subst -> TypeDecl term
substTypeDecl TypeDecl term
decl Subst
sub =
  TypeDecl
    { kind :: Kind term
kind =
        forall (term :: k).
CoreSyntax term =>
Kind term -> Subst -> Kind term
forall {k} (term :: k).
CoreSyntax term =>
Kind term -> Subst -> Kind term
Core.substKind @term TypeDecl term
decl.kind Subst
sub
    , manifest :: Maybe (Def term)
manifest =
        (Def term -> Def term) -> Maybe (Def term) -> Maybe (Def term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
          ( \Def term
dty ->
              forall (term :: k).
CoreSyntax term =>
Def term -> Subst -> Def term
forall {k} (term :: k).
CoreSyntax term =>
Def term -> Subst -> Def term
Core.substDef @term Def term
dty Subst
sub
          )
          TypeDecl term
decl.manifest
    }

substModType
  :: forall term
  .  Core.CoreSyntax term
  => ModType term
  -> Subst
  -> ModType term
substModType :: forall {k} (term :: k).
CoreSyntax term =>
ModType term -> Subst -> ModType term
substModType ModType term
mty Subst
sub =
  case ModType term
mty of
    Signature [Specification term]
sg ->
      [Specification term] -> ModType term
forall {k} (term :: k). [Specification term] -> ModType term
Signature ([Specification term] -> ModType term)
-> [Specification term] -> ModType term
forall a b. (a -> b) -> a -> b
$
        (Specification term -> Specification term)
-> [Specification term] -> [Specification term]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Specification term -> Specification term
forall {k} (term :: k).
CoreSyntax term =>
Subst -> Specification term -> Specification term
substSigItem Subst
sub) [Specification term]
sg
    FunctorType Ident
ident ModType term
mty1 ModType term
mty2 ->
      Ident -> ModType term -> ModType term -> ModType term
forall {k} (term :: k).
Ident -> ModType term -> ModType term -> ModType term
FunctorType
        Ident
ident
        (ModType term -> Subst -> ModType term
forall {k} (term :: k).
CoreSyntax term =>
ModType term -> Subst -> ModType term
substModType ModType term
mty1 Subst
sub)
        (ModType term -> Subst -> ModType term
forall {k} (term :: k).
CoreSyntax term =>
ModType term -> Subst -> ModType term
substModType ModType term
mty2 Subst
sub)

substSigItem
  :: forall term
  .  Core.CoreSyntax term
  => Subst
  -> Specification term
  -> Specification term
substSigItem :: forall {k} (term :: k).
CoreSyntax term =>
Subst -> Specification term -> Specification term
substSigItem Subst
sub = \case
  ValueSig Ident
ident Val term
vty ->
    Ident -> Val term -> Specification term
forall {k} (term :: k). Ident -> Val term -> Specification term
ValueSig Ident
ident (forall (term :: k).
CoreSyntax term =>
Val term -> Subst -> Val term
forall {k} (term :: k).
CoreSyntax term =>
Val term -> Subst -> Val term
Core.substVal @term Val term
vty Subst
sub)
  TypeSig Ident
ident TypeDecl term
decl ->
    Ident -> TypeDecl term -> Specification term
forall {k} (term :: k).
Ident -> TypeDecl term -> Specification term
TypeSig Ident
ident (TypeDecl term -> Subst -> TypeDecl term
forall {k} (term :: k).
CoreSyntax term =>
TypeDecl term -> Subst -> TypeDecl term
substTypeDecl TypeDecl term
decl Subst
sub)
  ModuleSig Ident
ident ModType term
mty ->
    Ident -> ModType term -> Specification term
forall {k} (term :: k). Ident -> ModType term -> Specification term
ModuleSig Ident
ident (ModType term -> Subst -> ModType term
forall {k} (term :: k).
CoreSyntax term =>
ModType term -> Subst -> ModType term
substModType ModType term
mty Subst
sub)