Signatures.hs

{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}

module Control.Monad.IMSOS.Signatures where

import Data.Kind (Type)
import Data.Comp.Multi.Term (Term)
import Data.Comp.Multi ( (:<:), (:+:), HFunctor )
import Data.Comp.Multi.Sum (project)

-- | A 'language' l captures the abstract syntax of a language 
-- by specifying a signature 

type Lang = Type

-- | A language consists of several sorts 
type Sort = Type

-- | The kind of signatures according to compdata (multi) library
type Signature = (Sort -> Type) -> Sort -> Type

class Language (l :: Lang) where
    type Sorts l :: [Sort]

-- | Subsignatures enable defining transition relations specific to 
-- parts of the signature, as represented by a sort 
class (Language l, HFunctor (SubSig l i), SubSig l i :<: Sig l) =>
  HasSubSig (l :: Lang) (i :: Sort) where
    type SubSig l i :: Signature

-- | Fold a type-level list of signatures into a nested coproduct
type family SumSigs (fs :: [Signature]) :: Signature where
    SumSigs '[f]      = f
    SumSigs (f ': fs) = f :+: SumSigs fs

type family MapSubSig (l :: Lang) (sorts :: [Sort]) :: [Signature] where
    MapSubSig l '[]       = '[]
    MapSubSig l (i ': is) = SubSig l i ': MapSubSig l is

-- | The signature of a language is automatically derived from the sorts
type Sig l = SumSigs (MapSubSig l (Sorts l))

-- | TermL is a convenience for referring to the type of terms of a language
type TermL l = Term (Sig l)

-- | Custom version of unTerm that ensures top-level operator is in relevant SubSig
-- Its usage is unsafe only in the case when an operator is of sort `i`
-- but is included in the signature for some other sort `j`
-- and either there is no semantics associated with the language or
-- there happens to be a semantics (instance of StepDefined) that yields
-- a result of sort j
-- unTerm :: forall l i. (SubSig l i :<: Sig l) => TermL l i -> SubSig l i (TermL l) i
-- unTerm t | Just t' <- project @(SubSig l i) t = t'
--          | otherwise = error "unTerm assertion failed: (Term (Sig l) i) not constructed by (SubSig l i)"