packages feed

imsos-monad 0.1.0.0 → 0.2.4.0

raw patch · 15 files changed

+1723/−93 lines, 15 filesdep +compdatadep +containersdep +random

Dependencies added: compdata, containers, random, template-haskell

Files

imsos-monad.cabal view
@@ -20,7 +20,7 @@ -- PVP summary:     +-+------- breaking API changes --                  | | +----- non-breaking API additions --                  | | | +--- code changes with no API change-version:            0.1.0.0+version:            0.2.4.0  -- A short (one-line) description of the package. synopsis:@@ -64,17 +64,38 @@     import:           warnings      -- Modules exported by the library.-    exposed-modules:  Control.Monad.IMSOS +    exposed-modules:  Control.Monad.IMSOS+                     ,Control.Monad.IMSOS.Fixed+                     ,Control.Monad.IMSOS.Layered      -- Modules included in this library but not exported.-    -- other-modules:+    other-modules:   +                     ,Control.Monad.IMSOS.Monad+                     ,Control.Monad.IMSOS.Signatures+                     ,Control.Monad.IMSOS.Rules.Relations+                     ,Control.Monad.IMSOS.Algebras+                     ,Control.Monad.IMSOS.LayeredAlgebras+                     ,Control.Monad.IMSOS.Rules.Step+                     ,Control.Monad.IMSOS.Rules.LayeredStep+                     ,Control.Monad.IMSOS.LayeredTerms +                     ,Data.Comp.SubsumeCommon+                     ,Data.Comp.ProjectionExt+                     ,Control.Monad.IMSOS.LayeredDeriving++--                     ,Control.Monad.IMSOS.Cases.WhileFixed+--                     ,Control.Monad.IMSOS.Cases.WhileLayered+     -- LANGUAGE extensions used by modules in this package.     -- other-extensions:      -- Other library packages from which modules are imported.     build-depends:    base ^>=4.18.3.0+                     ,containers ^>= 0.6                      ,mtl ^>= 2.3.1+                     ,random ^>= 1.3+                     ,template-haskell ^>= 2.20+                     ,compdata ^>= 0.13      -- Directories containing source files.     hs-source-dirs:   src
src/Control/Monad/IMSOS.hs view
@@ -1,92 +1,4 @@-{-# LANGUAGE UndecidableInstances-  , FlexibleInstances-  , FlexibleContexts-  , MultiParamTypeClasses-#-}- module Control.Monad.IMSOS -  (MonadIMSOS(..), runIMSOS, yieldIMSOS-  ,tell-  ,local, reader-  ,get, put, state-  ,fail, throwError, catchError-  ) where--import Control.Applicative (Alternative(..))-import Control.Monad.Error.Class-import Control.Monad.Reader (MonadReader(..))-import Control.Monad.State  (MonadState(..))-import Control.Monad.Writer (MonadWriter(..))-import Control.Monad (ap)--newtype MonadIMSOS r s w me e a = MonadIMSOS (r -> s -> me e (a, s, w))--instance Functor (me e) => Functor (MonadIMSOS r s w me e) where-  fmap f (MonadIMSOS m) = MonadIMSOS m'-    where m' r s = modify <$> m r s-           where modify (a, s', w) = (f a, s', w)--instance (MonadError e (me e), Monad (me e), Monoid w)-    => Monad (MonadIMSOS r s w me e) where-  (MonadIMSOS p) >>= m = MonadIMSOS $ \r1 s1  -> do-     (a, s2, w2) <- p r1 s1-     let MonadIMSOS q = m a-     (b, s3, w3) <- q r1 s2-     return (b, s3, w2 <> w3)--instance (MonadError e (me e), Monad (me e), Monoid w)-    => Applicative (MonadIMSOS r s w me e) where-  pure a = MonadIMSOS m-    where m _ s = pure (a, s, mempty)-  (<*>) = ap--instance (MonadError e (me e), Monad (me e), Alternative (me e), Monoid w)-    => Alternative (MonadIMSOS r s w me e) where-  empty = MonadIMSOS (\_ _ -> empty)-  (MonadIMSOS p) <|> (MonadIMSOS q) = MonadIMSOS m-    where m r s = p r s `catchError` \_ -> q r s- ---instance (MonadError e (me e), Monad (me e), Monoid w)---    => MonadPlus (MonadIMSOS r s w me e)--instance (MonadError String (me String), Monad (me String), Monoid w)-    => MonadFail (MonadIMSOS r s w me String) where-  fail = throwError--instance (MonadError e (me e), Monad (me e), Monoid w)-    => MonadReader r (MonadIMSOS r s w me e) where-  ask = MonadIMSOS m -    where m r s = pure (r, s, mempty)-  local f (MonadIMSOS p) = MonadIMSOS m-    where m r s = p (f r) s--instance (MonadError e (me e), Monad (me e), Monoid w)-    => MonadState s (MonadIMSOS r s w me e) where-  state act = MonadIMSOS m-    where m _ s = pure (a, s', mempty)-           where (a, s') = act s--instance (MonadError e (me e), Monad (me e), Monoid w)-    => MonadWriter w (MonadIMSOS r s w me e) where-  tell w = MonadIMSOS m-    where m _ s = pure ((), s, w)-  listen (MonadIMSOS p) = MonadIMSOS m-    where m r s = p r s >>= \(a, s', w) -> pure ((a,w), s', w)-  pass (MonadIMSOS p) = MonadIMSOS m-    where m r s = p r s >>= \((a,f), s', w) -> pure (a, s', f w)--instance (MonadError e (me e), Monad (me e), Monoid w)-    => MonadError e (MonadIMSOS r s w me e) where-  throwError e = MonadIMSOS m-    where m _ _ = throwError e-  catchError (MonadIMSOS p) h = MonadIMSOS m-    where m r s = p r s `catchError` \e -> -                  let MonadIMSOS q = h e-                  in q r s -- continues with a state as if p not executed--runIMSOS :: r -> s -> MonadIMSOS r s w me e a -> me e (a, s, w)-runIMSOS r s (MonadIMSOS f) = f r s+  (module Control.Monad.IMSOS.Layered) where -yieldIMSOS :: Functor (me e) => -  r -> s -> ((a, s, w) -> y) -> MonadIMSOS r s w me e a -> me e y-yieldIMSOS r s toyield m = toyield <$> runIMSOS r s m +import Control.Monad.IMSOS.Layered
+ src/Control/Monad/IMSOS/Algebras.hs view
@@ -0,0 +1,41 @@++{-# LANGUAGE GADTs #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+++module Control.Monad.IMSOS.Algebras where++import Data.Comp.Multi.Ops ( (:+:)(..))+import Data.Comp.Multi ( Term, Alg, HFunctor (..), (:->) )+import Data.Comp.Multi.Algebra (cata)+import Data.Kind (Type)+import Control.Monad.IMSOS.Signatures (Sort, HasSubSig (SubSig))++class HasAlg f e where+  sem :: Alg f (GetCarrier e)++-- TODO can I get rid of this?+newtype GetCarrier e i = GetCarrier { getCarrier :: CarrierOf e i i }++class HasCarrier e s where+  type CarrierOf e s :: Sort -> Type++instance (HasAlg f e, HasAlg g e)+  => HasAlg (f :+: g) e where+    sem (Inl f) = sem @f f+    sem (Inr g) = sem @g g++eval :: forall eval sig sort.+  (HFunctor sig, HasAlg sig eval)+  => Term sig sort -> GetCarrier eval sort+eval = cata (sem @sig @eval)
+ src/Control/Monad/IMSOS/Fixed.hs view
@@ -0,0 +1,49 @@+module Control.Monad.IMSOS.Fixed+  (+  -- from IMSOS.Monad+   MonadIMSOS(..), SemMonad, runIMSOS, yieldIMSOS+  ,Control.Monad.IMSOS.Monad.tell, Control.Monad.IMSOS.Monad.listen, Control.Monad.IMSOS.Monad.censor+  ,Control.Monad.IMSOS.Monad.local, Control.Monad.IMSOS.Monad.reader, Control.Monad.IMSOS.Monad.ask+  ,Control.Monad.IMSOS.Monad.get, Control.Monad.IMSOS.Monad.put, Control.Monad.IMSOS.Monad.modify+  ,fail, MonadError(..)+  ,guard, Alternative(..)+  -- from IMSOS.Rules.Relations+  ,RelID(..), HasRulesErrors(..), SemEntities(..), HasDefaults(..), runSem, Rel+  , GivesSemanticsTo, SharedSemEntities+  -- from IMSOS.Signature +  ,Signature, HasSubSig(..)+  --,IsSubSortWitness(..), Share, IsSubSort, HasSubSort, liftTerm, lowerTerm+  -- from IMSOS.Rules.Step +  ,HasTaggedRel(..)+  ,isValue, toValue, HasValOps(..), IsLangOp, IsValOp, ValOp, TermL, Language(..), Lang, Sort+  ,StepDefined(..), StepRes(..), steps, stepsOrHalt, stepsOrHaltWhen, StepAvailable, StepsAvailable, StepsTo+  -- to simplify writing rules+  ,premise, premiseE, trans, notrans+  -- from IMSOS.Rules.Trans+  --,TransAvailable, TransDefined(..), (:~>:)(..), EvaluatesTo(..), EvalTag, Direct, Via+  -- from ProjectionExt +  ,(:*:)(..), (:<~), (:<|), pr, uncons, recons+  -- from Control.Monad.IMSOS.Algebras +  ,HasAlg(..), GetCarrier(..), HasCarrier(..), eval+  ,Term, inject, project, unTerm+  ,(:+:), (:<:), caseH+  -- deriving hfunctors+  ,HFunctor, makeHFunctor, smartConstructors, derive, K(..)+  -- related to Show, Ord and Eq+  ,ShowHF(), makeShowHF+  ) where++import Control.Monad.IMSOS.Signatures+import Control.Monad.IMSOS.Monad+import Control.Monad.IMSOS.Rules.Relations+import Control.Monad.IMSOS.Algebras+import Control.Monad.IMSOS.Rules.Step+import Control.Monad.Error.Class (MonadError(..))+import Control.Applicative (Alternative(..))+import Data.Comp.ProjectionExt+import Data.Comp.Multi.Ops  ((:+:), (:<:), caseH)+import Data.Comp.Multi.Derive (makeHFunctor, HFunctor, smartConstructors, derive, makeShowHF, ShowHF)+import Data.Comp.Multi.Sum (inject)+import Data.Comp.Multi ( project, unTerm )+import Data.Comp.Multi.Term ( Term )+import Data.Comp.Multi.HFunctor (K(..))
+ src/Control/Monad/IMSOS/Layered.hs view
@@ -0,0 +1,56 @@+module Control.Monad.IMSOS.Layered+  (+  -- alternative definitions related to 'sort-polymorphic, layered terms'+   Term(..), inject, project, unTerm, fixL+  ,Alg, HasAlg(..), cata, eval+  ,StepDefined(..), steps, stepsOrHalt, stepsOrHaltWhen, premise, premiseE, trans, notrans+  ,isValue, toValue, HasValOps(..), StepsAvailable, StepsTo, SharedSemEntities, IsValOp, ValOp, IsLangOp+  ,HasRulesErrors(..)+  -- deriving +  ,smartConstructors++  -- as in IMSOS.Fixed ++  -- from IMSOS.Monad+  ,MonadIMSOS(..), SemMonad, runIMSOS, yieldIMSOS+  ,Control.Monad.IMSOS.Monad.tell, Control.Monad.IMSOS.Monad.listen, Control.Monad.IMSOS.Monad.censor+  ,Control.Monad.IMSOS.Monad.local, Control.Monad.IMSOS.Monad.reader, Control.Monad.IMSOS.Monad.ask+  ,Control.Monad.IMSOS.Monad.get, Control.Monad.IMSOS.Monad.put, Control.Monad.IMSOS.Monad.modify+  ,fail, MonadError(..)+  ,guard, Alternative(..)+  -- from IMSOS.Rules.Relations+  ,RelID(..), SemEntities(..), HasDefaults(..), runSem, Rel+  , GivesSemanticsTo+  -- from IMSOS.Signature +  ,Signature, HasSubSig(..)+  --,IsSubSortWitness(..), Share, IsSubSort, HasSubSort, liftTerm, lowerTerm+  -- from IMSOS.Rules.Step +  ,HasTaggedRel(..)+  ,TermL, Language(..), Lang, Sort+  -- to simplify writing rules+  -- from IMSOS.Rules.Trans+  --,TransAvailable, TransDefined(..), (:~>:)(..), EvaluatesTo(..), EvalTag, Direct, Via+  -- from ProjectionExt +  ,(:*:)(..), (:<~), (:<|), pr, uncons, recons+  -- from Control.Monad.IMSOS.Algebras +  ,(:+:), (:<:), caseH+  -- deriving hfunctors+  ,HFunctor, makeHFunctor, derive, K(..)+  -- related to Show, Ord and Eq+  ,ShowHF(), makeShowHF++  ) where++import Control.Monad.IMSOS.Monad+import Control.Monad.IMSOS.LayeredAlgebras+import Control.Monad.IMSOS.LayeredTerms+import Control.Monad.IMSOS.LayeredDeriving (smartConstructors)+import Control.Monad.IMSOS.Rules.LayeredStep+import Control.Monad.IMSOS.Rules.Relations+import Control.Monad.Except+import Control.Applicative+import Control.Monad.IMSOS.Signatures+import Data.Comp.ProjectionExt+import Data.Comp.Multi hiding (Alg, cata, unTerm, project, inject, Term)+import Data.Comp.Multi.Derive hiding (smartConstructors)+
+ src/Control/Monad/IMSOS/LayeredAlgebras.hs view
@@ -0,0 +1,49 @@++{-# LANGUAGE GADTs #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+++module Control.Monad.IMSOS.LayeredAlgebras where++import Data.Comp.Multi ( HFunctor (..), (:->) )+import Data.Kind (Type)+import Control.Monad.IMSOS.Signatures (Sort, Sig)+import Control.Monad.IMSOS.LayeredTerms (Term (..))+import qualified Data.Comp.Multi as Multi+import Data.Comp.Multi.Ops++type Alg l c = Multi.Alg (Sig l) c++class HasAlg f e where+  sem :: Multi.Alg f (GetCarrier e)++-- TODO can I get rid of this?+newtype GetCarrier e i = GetCarrier { getCarrier :: CarrierOf e i i }++class HasCarrier e s where+  type CarrierOf e s :: Sort -> Type++instance (HasAlg f e, HasAlg g e)+  => HasAlg (f :+: g) e where+    sem (Inl f) = sem @f f+    sem (Inr g) = sem @g g++cata :: forall l c. Alg l c -> Term l :-> c+cata f = go +  where go :: forall j. Term l j -> c j+        go (Term layer) = f (inj (hfmap go layer))++eval :: forall eval l sort. +  (HasAlg (Sig l) eval)+  => Term l sort -> GetCarrier eval sort +eval = cata (sem @(Sig l) @eval)
+ src/Control/Monad/IMSOS/LayeredDeriving.hs view
@@ -0,0 +1,212 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Control.Monad.IMSOS.Derive.SmartConstructors+-- Description :  Derive smart constructors for the indexed LTerm representation.+--+-- This is adapted from Data.Comp.Multi.Derive.SmartConstructors in+-- compdata-0.13.1.  Unlike compdata's version, the generated constructors+-- build an LTerm layer:+--+--   LTerm (inj (Constructor ...))+--+-- rather than a compdata Cxt layer:+--+--   inject (Constructor ...)+--+-- Usage, assuming the corresponding names are in scope:+--+--   $(smartConstructorsLTerm ''LTerm ''HasSubSig ''SubSig ''Add)+--+-- For+--+--   data Add a i where+--     Add :: a Expr -> a Expr -> Add a Expr+--+-- this generates, up to alpha-renaming:+--+--   iAdd+--     :: ( HasSubSig l Expr+--        , Add :<: SubSig l Expr+--        )+--     => LTerm l Expr -> LTerm l Expr -> LTerm l Expr+--   iAdd x y = LTerm (inj (Add x y))+--+-- For non-nullary constructors the signature is deliberately inferred, as in+-- compdata's original implementation.  This preserves the argument sorts of+-- GADT constructors (for example, Expr -> Bool operators).+--------------------------------------------------------------------------------+module Control.Monad.IMSOS.LayeredDeriving+  ( smartConstructorsLTerm+  , smartConstructors+  ) where++import Control.Arrow ((&&&))+import Control.Monad (liftM)+import Data.Comp.Derive.Utils+  ( DataInfo (..)+  , abstractConType+  , abstractNewtypeQ+  , isEqualP+  , newNames+  , tyVarBndrName+  )+import Data.Comp.Multi.Ops ((:<:), inj)+import Language.Haskell.TH hiding (Cxt)+import Control.Monad.IMSOS.LayeredTerms (Term(..))+import Control.Monad.IMSOS.Signatures (HasSubSig(..))++smartConstructors = smartConstructorsLTerm ''Term 'Term ''HasSubSig ''SubSig ++-- | Generate smart constructors for one signature functor, targeting a custom+-- sort-dependent layered term type.+--+-- The first three arguments identify the custom API:+--+-- * the GADT constructor/type name @LTerm@;+-- * the class name @HasSubSig@;+-- * the associated type-family name @SubSig@.+--+-- The last argument is the signature functor to inspect, for example @''Add@.+--+-- Passing names rather than importing the IMSOS modules makes this derivation+-- module independent of a particular LTerm implementation.++-- | Generate smart constructors for one signature functor, targeting a custom+-- sort-dependent LTerm.+--+-- Example:+--+--   $(smartConstructorsLTerm ''LTerm ''HasSubSig ''SubSig ''Add)+smartConstructorsLTerm+  :: Name  -- ^ LTerm type+  -> Name  -- ^ LTerm constructor+  -> Name  -- ^ HasSubSig class+  -> Name  -- ^ SubSig associated type family+  -> Name  -- ^ signature functor, for example Add+  -> Q [Dec]+smartConstructorsLTerm ltermName ltermCons hasSubSigName subSigName fname = do+  -- `abstractNewtypeQ` already takes a `Q Info`; do not fmap it over+  -- `reify fname`.+  Just (DataInfo _cxt tname targs constrs _deriving) <-+    abstractNewtypeQ (reify fname)++  let iVar = tyVarBndrName (last targs)+      cons = map (abstractConType &&& resultSort iVar) constrs++  liftM concat $+    mapM (genSmartConstr (map tyVarBndrName targs) tname) cons+  where+    -- GHC reifies a GADT result such as+    --+    --   Done :: Done r Commands+    --+    -- as a `GadtC` result type.  Older reification styles can instead expose+    -- the refinement as an equality predicate, so support both forms.+    resultSort :: Name -> Con -> Maybe Type+    resultSort iVar (ForallC _ cxt con) =+      case [ y | Just (x, y) <- map isEqualP cxt, x == VarT iVar ] of+        tp : _ -> Just tp+        []     -> resultSort iVar con+    resultSort _ (GadtC _ _ resultType) = finalArgument resultType+    resultSort _ (RecGadtC _ _ resultType) = finalArgument resultType+    resultSort _ _ = Nothing++    finalArgument :: Type -> Maybe Type+    finalArgument (AppT _ x) = Just x+    finalArgument (SigT t _) = finalArgument t+    finalArgument (ParensT t) = finalArgument t+    finalArgument _ = Nothing++    genSmartConstr+      :: [Name]+      -> Name+      -> ((Name, Int), Maybe Type)+      -> Q [Dec]+    genSmartConstr targs' tname ((conName, arity), resultIndex) =+      genSmartConstr'+        targs'+        tname+        (mkName ('i' : nameBase conName))+        conName+        arity+        resultIndex++    genSmartConstr'+      :: [Name]+      -> Name+      -> Name+      -> Name+      -> Int+      -> Maybe Type+      -> Q [Dec]+    genSmartConstr' targs' tname smartName conName arity resultIndex = do+      varNs <- newNames arity "x"++      let pats = map varP varNs+          vars = map varE varNs+          layer = foldl appE (conE conName) vars+          body =+            appE (conE ltermCons)+              (appE (varE 'inj) layer)+          function =+            [ funD smartName+                [ clause pats (normalB body) []+                ]+            ]+          sig+            | arity == 0 =+                genNullarySig targs' tname smartName resultIndex+            | otherwise =+                []++      sequence (sig ++ function)++    -- For constructors with fields, leave the signature inferred.  This+    -- preserves their actual GADT argument sorts.  A nullary constructor+    -- needs an explicit signature to avoid monomorphism-restriction issues.+    genNullarySig+      :: [Name]+      -> Name+      -> Name+      -> Maybe Type+      -> [Q Dec]+    genNullarySig _ _ _ Nothing = []+    genNullarySig targs' tname smartName (Just indexType) =+      [ do+          lVar <- newName "l"++          let signatureParameters = init (init targs')++              atomicSignature =+                foldl appT (conT tname) (map varT signatureParameters)++              targetSubSig =+                conT subSigName+                  `appT` varT lVar+                  `appT` pure indexType++              output =+                conT ltermName+                  `appT` varT lVar+                  `appT` pure indexType++              hasSubSigConstraint =+                conT hasSubSigName+                  `appT` varT lVar+                  `appT` pure indexType++              embedsInSubSig =+                conT ''(:<:)+                  `appT` atomicSignature+                  `appT` targetSubSig++              quantified =+                PlainTV lVar SpecifiedSpec+                  : map (`PlainTV` SpecifiedSpec) signatureParameters++          sigD smartName $+            forallT quantified+              (sequence [hasSubSigConstraint, embedsInSubSig])+              output+      ]
+ src/Control/Monad/IMSOS/LayeredTerms.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Module defining 'layered terms'.+-- At each layer, an operator from `SubSig l i` is applied+module Control.Monad.IMSOS.LayeredTerms where+import Control.Monad.IMSOS.Signatures (HasSubSig(..), TermL, Sig)+import Data.Comp.Multi ((:<:), inj, proj, HFunctor (hfmap), inject)+import qualified Data.Comp.Multi as Multi++data Term l i where +  Term ::+   ( HasSubSig l i ) => +      SubSig l i (Term l) i -> Term l i++unTerm :: Term l i -> SubSig l i (Term l) i+unTerm (Term l) = l++inject :: (f :<: SubSig l i, HasSubSig l i) +  => f (Term l) i -> Term l i+inject = Term . inj++project :: (f :<: SubSig l i) => Term l i -> Maybe (f (Term l) i)+project = proj . unTerm++fixL :: forall l i. Term l i -> TermL l i+fixL = go+  where+    go :: forall j. Term l j -> TermL l j+    go (Term layer) =+      Data.Comp.Multi.inject (hfmap go layer)++-- TODO: instances below might cause significant overhead due to fixing+instance +  (Show (Multi.Term (Sig l) i)) +  => Show (Term l i) where +  show = show . fixL++instance +  (Ord (Multi.Term (Sig l) i))+  => Ord (Term l i) where +    compare l r = compare (fixL l) (fixL r)++instance +  (Eq (Multi.Term (Sig l) i))+  => Eq (Term l i) where +    l == r = fixL l == fixL r
+ src/Control/Monad/IMSOS/Monad.hs view
@@ -0,0 +1,163 @@+{-# LANGUAGE UndecidableInstances+  , FlexibleInstances+  , FlexibleContexts+  , MultiParamTypeClasses+  , TypeOperators+  , LambdaCase+  , ScopedTypeVariables+  , TypeApplications+  , TupleSections+  , AllowAmbiguousTypes+#-}++module Control.Monad.IMSOS.Monad+  (MonadIMSOS(..), runIMSOS, yieldIMSOS+  ,Control.Monad.IMSOS.Monad.tell, Control.Monad.IMSOS.Monad.listen, Control.Monad.IMSOS.Monad.censor+  ,Control.Monad.IMSOS.Monad.local, Control.Monad.IMSOS.Monad.reader, Control.Monad.IMSOS.Monad.ask+  ,Control.Monad.IMSOS.Monad.get, Control.Monad.IMSOS.Monad.put, Control.Monad.IMSOS.Monad.modify+  ,fail, throwError, catchError+  ,guard, (<|>)+  ) where++import Control.Applicative (Alternative(..))+import Control.Monad.Error.Class+import Control.Monad.Reader (MonadReader(..))+import Control.Monad.State  (MonadState(..), modify)+import Control.Monad.Writer (MonadWriter(..), censor)+import Control.Monad (ap, join, guard)++import Data.Foldable (toList)+import Data.Comp.ProjectionExt ((:*:)(..), (:<~), (:<|), pr, uncons, recons, modify)++newtype MonadIMSOS r s w me e fl a = MonadIMSOS {+    unwrap :: r -> s -> me e (fl (a, s, w))+  }++instance (Functor (me e), Functor fl) => Functor (MonadIMSOS r s w me e fl) where+  fmap f (MonadIMSOS m) = MonadIMSOS m'+    where m' r s = fmap modify' <$> m r s+           where modify' (a, s', w) = (f a, s', w)++instance (Monad (me e), Monoid w, Traversable fl, Monad fl)+    => Monad (MonadIMSOS r s w me e fl) where+  (MonadIMSOS p) >>= m = MonadIMSOS $ \r1 s1  -> do+     p_res <- p r1 s1+     let modify' (a, s2, w2) = fmap (,w2) <$> q r1 s2+          where MonadIMSOS q = m a+     q_ress <- mapM modify' p_res+     let mod2 :: ((b, s, w), w) -> (b, s, w)+         mod2 ((b, s3, w3), w2) = (b, s3, w2 <> w3)+     return (fmap mod2 (join q_ress))++instance (Monad (me e), Monoid w, Monad fl, Traversable fl)+    => Applicative (MonadIMSOS r s w me e fl) where+  pure a = MonadIMSOS m+    where m _ s = pure (pure (a, s, mempty))+  (<*>) = ap++instance (Monad (me e), MonadError e (me e), Monoid w+         ,Alternative fl, Monad fl, Traversable fl)+    => Alternative (MonadIMSOS r s w me e fl) where+  empty = MonadIMSOS (\_ _ -> return empty)+  (MonadIMSOS p) <|> (MonadIMSOS q) = MonadIMSOS m+    where m r s = tryError (p r s) >>= \case+                      Left _      -> q r s+                      Right p_res -> tryError (q r s) >>= \case+                          Left _ -> return empty+                          Right q_res -> return (p_res <|> q_res)++instance {-# INCOHERENT #-}+  (MonadError String (me String), Monad (me String), Monoid w, Traversable fl, Monad fl)+    => MonadFail (MonadIMSOS r s w me String fl) where+  fail = throwError++instance (MonadError e (me e), Monad (me e), Monoid w, Monad fl, Traversable fl)+    => MonadReader r (MonadIMSOS r s w me e fl) where+  ask = MonadIMSOS m+    where m r s = pure $ pure (r, s, mempty)+  local f (MonadIMSOS p) = MonadIMSOS m+    where m r s = p (f r) s++instance (MonadError e (me e), Monad (me e), Monoid w, Monad fl, Traversable fl)+    => MonadState s (MonadIMSOS r s w me e fl) where+  state act = MonadIMSOS m+    where m _ s = pure $ pure (a, s', mempty)+           where (a, s') = act s++instance (MonadError e (me e), Monad (me e), Monoid w, Monad fl, Traversable fl)+    => MonadWriter w (MonadIMSOS r s w me e fl) where+  tell w = MonadIMSOS m+    where m _ s = pure $ pure ((), s, w)+  listen (MonadIMSOS p) = MonadIMSOS m+    where m r s = p r s >>= \as -> pure (fmap modify' as)+            where modify' (a, s', w) = ((a, w), s', w)+  pass (MonadIMSOS p) = MonadIMSOS m+    where m r s = p r s >>= \as -> pure (fmap modify' as)+            where modify' ((a,f), s', w) = (a, s', f w)++instance (MonadError e (me e), Monad (me e), Monoid w, Traversable fl, Monad fl)+    => MonadError e (MonadIMSOS r s w me e fl) where+  throwError e = MonadIMSOS m+    where m _ _ = throwError e+  catchError (MonadIMSOS p) h = MonadIMSOS m+    where m r s = p r s `catchError` \e ->+                  let MonadIMSOS q = h e+                  in q r s -- continues with a state as if p not executed++class Unifies a where+    unify :: [a] -> a++search :: (Unifies s, Unifies w, Monad (me e), Applicative fl, Foldable fl)+  => MonadIMSOS r s w me e fl a -> MonadIMSOS r s w me e fl [a]+search (MonadIMSOS p) = MonadIMSOS $ \r s -> do+  (as, ss, ws) <- unzip3 . toList <$> p r s+  return $ pure (as, unify ss, unify ws)++runIMSOS :: (MonadError e (me e))+  => r -> s -> MonadIMSOS r s w me e fl a -> me e (fl (a, s, w))+runIMSOS r s (MonadIMSOS f) = f r s++yieldIMSOS :: (Functor (me e), Functor fl, MonadFail (me e), MonadError e (me e)) =>+  r -> s -> ((a, s, w) -> y) -> MonadIMSOS r s w me e fl a -> me e (fl y)+yieldIMSOS r s toyield m = fmap toyield <$> runIMSOS r s m++-- ------------------------------+-- --- Auxiliary entities +-- ------------------------------++instance (Semigroup f, Semigroup g)+  => Semigroup (f :*: g) where+  (l1 :*: r1) <> (l2 :*: r2) = (l1 <> l2) :*: (r1 <> r2)++instance (Monoid f, Monoid g)+  => Monoid (f :*: g) where+    mempty = mempty :*: mempty++tell :: forall f w m. (f :<| w, MonadWriter w m) => f -> m ()+tell f = Control.Monad.Writer.tell (recons rem_ f)+  where (_, rem_) = uncons @f (mempty @w)++listen :: forall f w m a. (f :<~ w, MonadWriter w m) => m a -> m (a, f)+listen m = fmap (pr @f) <$> Control.Monad.Writer.listen m++censor :: forall f w m a. (f :<| w, MonadWriter w m) => (f -> f) -> m a ->  m a+censor tr = Control.Monad.Writer.censor (Data.Comp.ProjectionExt.modify @f tr)++get :: forall f s m. (f :<~ s, MonadState s m) => m f+get = pr @f <$> Control.Monad.State.get++put :: forall f s m. (f :<| s, MonadState s m) => f -> m ()+put f = Control.Monad.IMSOS.Monad.modify (const f)++modify :: forall f s m. (f :<| s, MonadState s m) => (f -> f) -> m ()+modify tr = Control.Monad.State.modify (Data.Comp.ProjectionExt.modify @f tr)++ask :: forall f r m. (f :<~ r, MonadReader r m) => m f+ask = pr @f <$> Control.Monad.Reader.ask++reader :: forall f r m a. (f :<| r, MonadReader r m) => (f -> a) -> m a+reader tr = Control.Monad.Reader.reader tr'+  where tr' r = tr (pr @f r)++local :: forall f r m a. (f :<| r, MonadReader r m) => (f -> f) -> m a -> m a+local tr = Control.Monad.Reader.local (Data.Comp.ProjectionExt.modify tr)
+ src/Control/Monad/IMSOS/Rules/LayeredStep.hs view
@@ -0,0 +1,200 @@+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE AllowAmbiguousTypes    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE ConstraintKinds        #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}++module Control.Monad.IMSOS.Rules.LayeredStep where++import Data.Comp.Multi.Ops      ((:+:)(..), (:<:))++import Control.Monad.IMSOS.Rules.Relations+import Data.Comp.ProjectionExt ((:<~), pr)+import Control.Monad.IMSOS.Monad (listen, get, MonadIMSOS)+import Control.Monad.IMSOS.Signatures+import Data.Kind (Type)+import Control.Monad.Error.Class (MonadError(throwError))+import Control.Monad.IMSOS.LayeredTerms (Term, unTerm, inject, project)+import Data.Maybe (isJust)+import Control.Applicative (Alternative(empty))++-- ───────────────────────────────────────────────+-- Rules+-- ───────────────────────────────────────────────++data StepRes (l :: Lang) (e :: Rel) (i :: Type) where+  -- | the constraint on NoStep ensures only value operators are used+  -- forcing the use of NoStep and ValOps mechanisms to be consistent+  NoStep :: (IsValOp e l i f) => f (Term l) i  -> StepRes l e i+  Step   :: (IsLangOp l i f)  => f (Term l) i  -> StepRes l e i++-- |+-- StepDefined is the main class to define by users to express I-MSOS rules+-- instances are identified by `l` (language), `e` (relation) and `f` (operator)+-- the sort `i` of the operator is implicit+-- note that in StepDefined the order of the `e` and `l` is purposefully different+-- compared to the helper functions defined below+--+class+  StepDefined (l :: Lang) (e :: Rel) (f :: Signature) where+  step :: forall i. f (Term l) i -> SemMonad l e (StepRes l e i)++premiseE :: forall e l i.+  ( e `GivesSemanticsTo` l+  , HasRulesErrors (SemError l e)+  , StepsAvailable e l i+  )+  => Term l i -> SemMonad l e (Term l i)+premiseE t = step @l @e t' >>= \case+  NoStep _  -> throwError (stepOnValueError (getRelID @e) t')+  Step t''  -> return (inject t'')+  where t' = unTerm t++premise :: forall e l i.+  ( e `GivesSemanticsTo` l+  , StepsAvailable e l i+  )+  => Term l i -> SemMonad l e (Term l i)+premise t = step @l @e t' >>= \case+  NoStep _  -> empty +  Step t''  -> return (inject t'')+  where t' = unTerm t++notrans :: forall e l i f. (e `GivesSemanticsTo` l, IsValOp e l i f)+  => f (Term l) i -> SemMonad l e (StepRes l e i)+notrans = return . NoStep++trans :: forall e l i f. (e `GivesSemanticsTo` l, IsLangOp l i f)+  => f (Term l) i -> SemMonad l e (StepRes l e i)+trans = return . Step++steps :: forall e l f i.+  ( e `GivesSemanticsTo` l+  , StepsAvailable e l i+  , IsValOp e l i f )+    => Term l i -> SemMonad l e (f (Term l) i)+steps t | Just v <- toValue @f @e @l t = return v+        | otherwise                    = premise @e @l t >>= steps @e @l++stepsOrHalt :: forall e h l f i.+  ( e `GivesSemanticsTo` l+  , StepsAvailable e l i+  , IsValOp e l i f+  , h :<~ SemWriter l e, Monoid h, Eq h+  )+    => Term l i -> SemMonad l e (Either (Term l i) (f (Term l) i))+stepsOrHalt = stepsOrHaltWhen @e @l @f predicate+  where predicate _ _ w = pr @h w /= mempty++stepsOrHaltWhen :: forall e l f i.+  ( e `GivesSemanticsTo` l+  , StepsAvailable e l i+  , IsValOp e l i f+  )+    => (Term l i -> SemState l e -> SemWriter l e -> Bool) -- predicate over an I-MSOS configuration+          -> Term l i                                  -- consisting of term after step, state and writer values+          -> SemMonad l e (Either (Term l i) (f (Term l) i))+stepsOrHaltWhen predicate t+  | Just v <- toValue @f @e @l t = return $ Right v+  | otherwise = do+            (t', w) <- listen @(SemWriter l e) (premise @e @l t)+            s <- get @(SemState l e)+            if predicate t' s w then return $ Left t'+                                else stepsOrHaltWhen @e @l predicate t'++instance+  ( StepDefined l e f+  , StepDefined l e g+  )+  => StepDefined l e (f :+: g) where+  step (Inl f) = step @l @e f+  step (Inr g) = step @l @e g+++-- | A transition relation identifies which subsignature of a language's+-- signature identify the value operations of a particular sort +-- this will be used to determine termination of computations+-- according to the relation+class (ValOps l e i :<: SubSig l i, ValOps l e i :<: Sig l, HasSubSig l i) =>+  HasValOps (l :: Lang) (e :: Rel) (i :: Sort) where+    type ValOps l e i :: Signature++-- | ValOp are those terms that are built only from value operators+-- on the outermost level. +-- Useful to build semantic entities. +-- Only outermost operator is considered to support thunk-like values+type ValOp l e i = ValOps l e i (Term l) i++-- | Tests whether a term is a ValOp and converts if possible +toValue :: forall f e l i.+  (HasValOps l e i, f :<: ValOps l e i, f :<: SubSig l i) =>+    Term l i -> Maybe (f (Term l) i)+toValue = project @f++-- | Determine whether a term is constructed by a value constructor+-- of the relevant sort `i` (for a given `e` and `l`)+isValue :: forall e l i.+  (HasValOps l e i)+  => Term l i -> Bool+isValue = isJust . toValue @(ValOps l e i) @e @l @i++-- ───────────────────────────────────────────────+-- Error handling+-- ───────────────────────────────────────────────++class HasRulesErrors e where+  ruleAssertionError      :: String -> e+  noApplicableRulesError  :: symb -> f (Term l) i -> e+  stepOnValueError        :: symb -> f (Term l) i -> e++instance (HasRulesErrors e, MonadError e (me e), Monoid w+         ,Traversable fl, Monad fl) =>+  MonadFail (MonadIMSOS r s w me e fl) where+  fail = throwError . ruleAssertionError @e++instance HasRulesErrors String where+  ruleAssertionError          = id+  noApplicableRulesError _ _  = "No rules applicable to term"+  stepOnValueError _ _        = "attempting to step on value term"++type StepAvailable e l i =+    ( RelID e+    , StepDefined l e (SubSig l i))++type StepsAvailable e l i =+    (StepAvailable e l i+    ,HasSubSig l i+    ,HasValOps l e i)++type StepsTo e l i f =+  (StepsAvailable e l i+  ,IsValOp e l i f)++type IsValOp e l i f =+  (f :<: ValOps l e i+  ,IsLangOp l i f)++type IsLangOp l i f =+  (f :<: Sig l+  ,f :<: SubSig l i+  ,HasSubSig l i)++type SharedSemEntities l (e :: Rel) (e' :: Rel) =+  ( SemEntities l e+  , SemEntities l e+  , SemAlternative l e ~ SemAlternative l e'+  , SemMonadError l e  ~ SemMonadError l e'+  , SemError l e       ~ SemError l e'+  , SemState l e       ~ SemState l e'+  , SemWriter l e      ~ SemWriter l e'+  , SemReader l e      ~ SemReader l e'+  )
+ src/Control/Monad/IMSOS/Rules/Relations.hs view
@@ -0,0 +1,68 @@+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE AllowAmbiguousTypes    #-}+{-# LANGUAGE ConstraintKinds        #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module Control.Monad.IMSOS.Rules.Relations where++--import Data.Comp.Multi.Term     (Term)++import Control.Monad.IMSOS.Monad (MonadIMSOS, runIMSOS)+import Control.Monad.IMSOS.Signatures+import Control.Applicative       (Alternative(..))+import Control.Monad.Error.Class (MonadError(..))+import Data.Kind (Type)++-- |+-- Type class for introducing symbols used to identify transition _relations_+--+type Rel = Type+class RelID e where+  getRelID :: e++-- | Tags are used to abstract over transition relations, independent of sort+type Tag = Type++-- | Type family that gives a specific Rel for a given Tag and Sort +class HasTaggedRel (tag :: Tag) (s :: Sort) (i :: Sort) where +  data TaggedRel tag s i :: Rel ++-- | Transition relations have associated semantic entities+-- and deal with non-determinism in a certain way (Alternative)+class ( Alternative (SemAlternative l e)+      , Monad (SemAlternative l e)+      , Traversable (SemAlternative l e)+      , MonadError (SemError l e) (SemMonadError l e (SemError l e))+      , Monoid (SemWriter l e)+      , HasDefaults l e+      ) => SemEntities (l :: Lang) (e :: Rel) where+  type SemReader       l e :: Type+  type SemState        l e :: Type+  type SemWriter       l e :: Type+  type SemAlternative  l e :: Type -> Type+  type SemError        l e :: Type+  type SemMonadError   l e :: Type -> Type -> Type++type SemMonad l e =+      MonadIMSOS (SemReader l e) (SemState l e) (SemWriter l e)+                 (SemMonadError l e) (SemError l e) (SemAlternative l e)++type GivesSemanticsTo e l = (SemEntities l e, Language l, RelID e)++class Monoid (SemWriter l e) => HasDefaults l e where+  defaultReader :: SemReader l e+  defaultState  :: SemState l e++runSem :: forall e l a.+  ( HasDefaults l e+  , SemEntities l e+  ) => SemMonad l e a -> SemMonadError l e (SemError l e) (SemAlternative l e (a, SemState l e, SemWriter l e))+runSem = runIMSOS (defaultReader @l @e) (defaultState @l @e)
+ src/Control/Monad/IMSOS/Rules/Step.hs view
@@ -0,0 +1,199 @@+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE AllowAmbiguousTypes    #-}+{-# LANGUAGE TypeApplications       #-}+{-# LANGUAGE ConstraintKinds        #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}++module Control.Monad.IMSOS.Rules.Step where++import Data.Comp.Multi.Ops      ((:+:)(..), (:<:))++import Control.Monad.IMSOS.Rules.Relations+import Data.Comp.ProjectionExt ((:<~), pr)+import Control.Monad.IMSOS.Monad (listen, get, MonadIMSOS)+import Control.Monad.IMSOS.Signatures+import Data.Kind (Type)+import Data.Comp.Multi.Term (Term)+import Control.Monad.Error.Class (MonadError(throwError))+import Data.Comp.Multi.Sum (inject)+import Data.Comp.Multi ( unTerm, project )+import Data.Maybe (isJust)+import Control.Applicative (Alternative(empty))++-- ───────────────────────────────────────────────+-- Rules+-- ───────────────────────────────────────────────++data StepRes (l :: Lang) (e :: Sort -> Rel) (i :: Type) where+  -- | the constraint on NoStep ensures only value operators are used+  -- forcing the use of NoStep and ValOps mechanisms to be consistent+  NoStep :: (IsValOp e l i f) => f (Term (Sig l)) i  -> StepRes l e i+  Step   :: (IsLangOp l i f)  => f (Term (Sig l)) i  -> StepRes l e i++-- |+-- StepDefined is the main class to define by users to express I-MSOS rules+-- instances are identified by `l` (language), `e` (relation) and `f` (operator)+-- the sort `i` of the operator is implicit+-- note that in StepDefined the order of the `e` and `l` is purposefully different+-- compared to the helper functions defined below+--+class+  StepDefined (l :: Lang) (t :: Type) (f :: Signature) where+  step :: forall i. f (TermL l) i -> SemMonad l (TaggedRel t i i) (StepRes l (TaggedRel t i) i)++premiseE :: forall t l i.+  ( StepAvailable t l i+  , HasRulesErrors (SemError l (TaggedRel t i i))+  , TaggedRel t i i `GivesSemanticsTo` l+  )+  => TermL l i -> SemMonad l (TaggedRel t i i) (TermL l i)+premiseE t = step @l @t t' >>= \case+  NoStep _  -> throwError (stepOnValueError (getRelID @(TaggedRel t i i)) t')+  Step t''  -> return (inject t'')+  where t' = unTerm t++premise :: forall t l i.+  ( StepAvailable t l i+  , TaggedRel t i i `GivesSemanticsTo` l+  )+  => TermL l i -> SemMonad l (TaggedRel t i i) (TermL l i)+premise t = step @l @t t' >>= \case+  NoStep _  -> empty+  Step t''  -> return (inject t'')+  where t' = unTerm t++notrans :: forall e l i f. (e i `GivesSemanticsTo` l, IsValOp e l i f)+  => f (TermL l) i -> SemMonad l (e i) (StepRes l e i)+notrans = return . NoStep++trans :: forall e l i f. (e i `GivesSemanticsTo` l, IsLangOp l i f)+  => f (TermL l) i -> SemMonad l (e i) (StepRes l e i)+trans = return . Step++steps :: forall (t :: Tag) l f i.+  ( TaggedRel t i i `GivesSemanticsTo` l+  , StepsAvailable t l i+  , IsValOp (TaggedRel t i) l i f )+    => TermL l i -> SemMonad l (TaggedRel t i i) (f (TermL l) i)+steps t | Just v <- toValue @f @t @l t = return v+        | otherwise                    = premise @t @l t >>= steps @t @l++stepsOrHalt :: forall (t :: Tag) h l f i.+  ( TaggedRel t i i `GivesSemanticsTo` l+  , StepsAvailable t l i+  , IsValOp (TaggedRel t i) l i f+  , h :<~ SemWriter l (TaggedRel t i i), Monoid h, Eq h+  )+    => TermL l i -> SemMonad l (TaggedRel t i i) (Either (TermL l i) (f (TermL l) i))+stepsOrHalt = stepsOrHaltWhen @t @l @f predicate+  where predicate _ _ w = pr @h w /= mempty++stepsOrHaltWhen :: forall (t :: Tag) l f i.+  ( TaggedRel t i i `GivesSemanticsTo` l+  , StepsAvailable t l i+  , IsValOp (TaggedRel t i) l i f+  )+    => (TermL l i -> SemState l (TaggedRel t i i) -> SemWriter l (TaggedRel t i i) -> Bool) -- predicate over an I-MSOS configuration+          -> TermL l i                                  -- consisting of term after step, state and writer values+          -> SemMonad l (TaggedRel t i i) (Either (TermL l i) (f (TermL l) i))+stepsOrHaltWhen predicate t+  | Just v <- toValue @f @t @l t = return $ Right v+  | otherwise = do+            (t', w) <- listen @(SemWriter l (TaggedRel t i i)) (premise @t @l t)+            s <- get @(SemState l (TaggedRel t i i))+            if predicate t' s w then return $ Left t'+                                else stepsOrHaltWhen @t @l predicate t'++instance+  ( StepDefined l e f+  , StepDefined l e g+  )+  => StepDefined l e (f :+: g) where+  step (Inl f) = step @l @e f+  step (Inr g) = step @l @e g+++-- | A transition relation identifies which subsignature of a language's+-- signature identify the value operations of a particular sort +-- this will be used to determine termination of computations+-- according to the relation+class (ValOps l e i :<: Sig l) =>+  HasValOps (l :: Lang) (e :: Sort -> Rel) (i :: Sort) where+    type ValOps l e i :: Signature++-- | ValOp are those terms that are built only from value operators+-- on the outermost level. +-- Useful to build semantic entities. +-- Only outermost operator is considered to support thunk-like values+type ValOp l e i = ValOps l e i (TermL l) i++-- | Tests whether a term is a ValOp and converts if possible +toValue :: forall f t l i.+  (HasValOps l (TaggedRel t i) i, f :<: ValOps l (TaggedRel t i) i, f :<: Sig l) =>+    TermL l i -> Maybe (f (TermL l) i)+toValue = project @f++-- | Determine whether a term is constructed by a value constructor+-- of the relevant sort `i` (for a given `e` and `l`)+isValue :: forall t l i.+  (HasValOps l (TaggedRel t i) i)+  => TermL l i -> Bool+isValue = isJust . toValue @(ValOps l (TaggedRel t i) i) @t @l @i++-- ───────────────────────────────────────────────+-- Error handling+-- ───────────────────────────────────────────────++class HasRulesErrors e where+  ruleAssertionError      :: String -> e+  noApplicableRulesError  :: symb -> f (Term g) i -> e+  stepOnValueError        :: symb -> f (Term g) i -> e++instance (HasRulesErrors e, MonadError e (me e), Monoid w+         ,Traversable fl, Monad fl) =>+  MonadFail (MonadIMSOS r s w me e fl) where+  fail = throwError . ruleAssertionError @e++instance HasRulesErrors String where+  ruleAssertionError          = id+  noApplicableRulesError _ _  = "No rules applicable to term"+  stepOnValueError _ _        = "attempting to step on value term"++type StepAvailable t l i =+    ( RelID (TaggedRel t i i)+    , StepDefined l t (Sig l))++type StepsAvailable t l i =+    (StepAvailable t l i+    ,HasValOps l (TaggedRel t i) i)++type StepsTo t l i f =+  (StepsAvailable t l i+  ,IsValOp (TaggedRel t i) l i f)++type IsValOp e l i f =+  (f :<: ValOps l e i+  ,IsLangOp l i f)++type IsLangOp l i f =+  (f :<: Sig l)++type SharedSemEntities l (t :: Tag) i j =+  ( SemEntities l (TaggedRel t i i)+  , SemEntities l (TaggedRel t j j)+  , SemAlternative l (TaggedRel t i i) ~ SemAlternative l (TaggedRel t j j)+  , SemMonadError l (TaggedRel t i i)  ~ SemMonadError l (TaggedRel t j j)+  , SemError l (TaggedRel t i i)       ~ SemError l (TaggedRel t j j)+  , SemState l (TaggedRel t i i)       ~ SemState l (TaggedRel t j j)+  , SemWriter l (TaggedRel t i i)      ~ SemWriter l (TaggedRel t j j)+  , SemReader l (TaggedRel t i i)      ~ SemReader l (TaggedRel t j j)+  )
+ src/Control/Monad/IMSOS/Signatures.hs view
@@ -0,0 +1,65 @@++{-# 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)"
+ src/Data/Comp/ProjectionExt.hs view
@@ -0,0 +1,374 @@+{-# LANGUAGE ConstraintKinds        #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE KindSignatures         #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+{-# LANGUAGE TypeApplications       #-}++-- ---------------------------------------------------------------------------+-- Module      :  Data.Comp.ProjectionExt+--+-- Extends Data.Comp.Projection with:+--+--   1. Support for (:*:) products alongside tuples (,).+--      Because Elem is a closed type family in the original module,+--      we re-implement it here with the extra cases, and re-derive+--      everything on top of it.  The original (:<) / pr are NOT+--      re-exported; use (:<~) and pr~ from this module instead.+--+--   2. uncons — projects a component AND returns the remainder+--      of the product with that component removed, as an abstract type.+--+--   3. recons — rebuilds the original product from a remainder+--      and a (possibly modified) projected component.+--+-- Supported product constructors:+--   (,)   — Haskell built-in pair+--   (:*:) — GHC.Generics / Data.Functor.Product style functor product+--           (used at kind Type by applying both sides to a common index)+--+-- Adding further product constructors (e.g. Data.Strict.Pair) requires+-- one new equation in Elem, one in Remainder2, and two new instances+-- each in Proj, ProjR, and Reconstruct.+-- ---------------------------------------------------------------------------++module Data.Comp.ProjectionExt+  ( -- * Constraint and plain projection (replaces :< / pr)+    (:<~), (:<|), (:*:)(..)+  , pr+    -- * Projection with remainder+  , RemainderOf+  , uncons+  , recons+  , modify+    -- * Re-exported position machinery (for advanced use)+  , Elem+  ) where++import Data.Comp.SubsumeCommon+import Data.Kind    (Type)++data a :*: b = a :*: b+infixr 6 :*:++-- ---------------------------------------------------------------------------+-- 1.  Elem — closed type family recognising BOTH (,) and (:*:)+--+-- The structure exactly mirrors the original Elem, with every+-- tuple case duplicated for (:*:).+-- ---------------------------------------------------------------------------++type family Elem (f :: Type) (g :: Type) :: Emb where++  -- Base: exact match+  Elem f f = 'Found 'Here++  -- LHS is a tuple-pair: look for each component independently in g+  Elem (f1, f2) g = Sum' (Elem f1 g) (Elem f2 g)++  -- LHS is a (:*:)-pair: same idea+  Elem (f1 :*: f2) g = Sum' (Elem f1 g) (Elem f2 g)++  -- RHS is a tuple-pair: choose which side f lives in+  Elem f (g1, g2) = Choose (Elem f g1) (Elem f g2)++  -- RHS is a (:*:)-pair: same idea+  Elem f (g1 :*: g2) = Choose (Elem f g1) (Elem f g2)++  -- No match+  Elem f g = 'NotFound++-- ---------------------------------------------------------------------------+-- 2.  Proj — plain projection, mirrors the original Proj class+--     but dispatches on both (,) and (:*:) at the value level.+-- ---------------------------------------------------------------------------++class Proj (e :: Emb) (p :: Type) (q :: Type) where+  proj' :: Proxy e -> q -> p++-- Base: p is q+instance Proj ('Found 'Here) f f where+  proj' _ x = x++-- p is in the left branch of a tuple+instance Proj ('Found pos) f g+    => Proj ('Found ('Le pos)) f (g, g') where+  proj' _ (l, _) = proj' (P :: Proxy ('Found pos)) l++-- p is in the right branch of a tuple+instance Proj ('Found pos) f g+    => Proj ('Found ('Ri pos)) f (g', g) where+  proj' _ (_, r) = proj' (P :: Proxy ('Found pos)) r++-- p is in the left branch of a (:*:)+instance Proj ('Found pos) f g+    => Proj ('Found ('Le pos)) f (g :*: g') where+  proj' _ (l :*: _) = proj' (P :: Proxy ('Found pos)) l++-- p is in the right branch of a (:*:)+instance Proj ('Found pos) f g+    => Proj ('Found ('Ri pos)) f (g' :*: g) where+  proj' _ (_ :*: r) = proj' (P :: Proxy ('Found pos)) r++-- p is a pair (f1, f2) scattered across q — tuple variant+instance ( Proj ('Found p1) f1 g+         , Proj ('Found p2) f2 g+         )+    => Proj ('Found ('Sum p1 p2)) (f1, f2) g where+  proj' _ x =+    ( proj' (P :: Proxy ('Found p1)) x+    , proj' (P :: Proxy ('Found p2)) x+    )++-- p is a pair (f1 :*: f2) scattered across q — (:*:) variant+instance ( Proj ('Found p1) f1 g+         , Proj ('Found p2) f2 g+         )+    => Proj ('Found ('Sum p1 p2)) (f1 :*: f2) g where+  proj' _ x =+    proj' (P :: Proxy ('Found p1)) x+    :*:+    proj' (P :: Proxy ('Found p2)) x++-- ---------------------------------------------------------------------------+-- 3.  Public constraint and projection function (replaces :< / pr)+-- ---------------------------------------------------------------------------++-- | @p :\<~ q@ means @p@ is a uniquely-occurring component of @q@,+-- where @q@ may be built from either @(,)@ or @(':*:')@ products.+type p :<~ q = Proj (ComprEmb (Elem p q)) p q++-- | Project component @p@ out of product @q@.+--   Generalises 'Data.Comp.Projection.pr' to also handle @(':*:')@.+pr :: forall p q. (p :<~ q) => q -> p+pr = proj' (P :: Proxy (ComprEmb (Elem p q)))++-- ---------------------------------------------------------------------------+-- 4.  Remainder type family+--+-- Remainder e p q  is the type of q with the component at position e+-- removed.  The result type depends on which product constructor was+-- used at each node, so we need cases for both (,) and (:*:).+-- ---------------------------------------------------------------------------++type family Remainder (e :: Emb) (p :: Type) (q :: Type) :: Type where++  -- Base: p was the whole product+  Remainder ('Found 'Here) p p = ()++  -- p was in the left branch of a tuple+  Remainder ('Found ('Le pos)) p (g, g') =+      (Remainder ('Found pos) p g, g')++  -- p was in the right branch of a tuple+  Remainder ('Found ('Ri pos)) p (g', g) =+      (g', Remainder ('Found pos) p g)++  -- p was in the left branch of a (:*:)+  Remainder ('Found ('Le pos)) p (g :*: g') =+      Remainder ('Found pos) p g :*: g'++  -- p was in the right branch of a (:*:)+  Remainder ('Found ('Ri pos)) p (g' :*: g) =+      g' :*: Remainder ('Found pos) p g++  -- p is a tuple-pair (f1, f2) scattered through q+  Remainder ('Found ('Sum pos1 pos2)) (f1, f2) q =+      Remainder ('Found pos2) f2 (Remainder ('Found pos1) f1 q)++  -- p is a (:*:)-pair (f1 :*: f2) scattered through q+  Remainder ('Found ('Sum pos1 pos2)) (f1 :*: f2) q =+      Remainder ('Found pos2) f2 (Remainder ('Found pos1) f1 q)++-- Convenience alias hiding the position evidence.+type RemainderOf p q = Remainder (ComprEmb (Elem p q)) p q++-- ---------------------------------------------------------------------------+-- 5.  ProjR — projection that also returns the remainder+-- ---------------------------------------------------------------------------++class ProjR (e :: Emb) (p :: Type) (q :: Type) where+  prR' :: Proxy e -> q -> (p, Remainder e p q)++-- Base+instance ProjR ('Found 'Here) f f where+  prR' _ x = (x, ())++-- Left branch of a tuple+instance ProjR ('Found pos) f g+    => ProjR ('Found ('Le pos)) f (g, g') where+  prR' _ (l, r) =+    let (p, remL) = prR' (P :: Proxy ('Found pos)) l+    in  (p, (remL, r))++-- Right branch of a tuple+instance ProjR ('Found pos) f g+    => ProjR ('Found ('Ri pos)) f (g', g) where+  prR' _ (l, r) =+    let (p, remR) = prR' (P :: Proxy ('Found pos)) r+    in  (p, (l, remR))++-- Left branch of a (:*:)+instance ProjR ('Found pos) f g+    => ProjR ('Found ('Le pos)) f (g :*: g') where+  prR' _ (l :*: r) =+    let (p, remL) = prR' (P :: Proxy ('Found pos)) l+    in  (p, remL :*: r)++-- Right branch of a (:*:)+instance ProjR ('Found pos) f g+    => ProjR ('Found ('Ri pos)) f (g' :*: g) where+  prR' _ (l :*: r) =+    let (p, remR) = prR' (P :: Proxy ('Found pos)) r+    in  (p, l :*: remR)++-- Scattered tuple-pair (f1, f2)+instance ( ProjR ('Found pos1) f1 q+         , ProjR ('Found pos2) f2 (Remainder ('Found pos1) f1 q)+         )+    => ProjR ('Found ('Sum pos1 pos2)) (f1, f2) q where+  prR' _ x =+    let (f1, rem1) = prR' (P :: Proxy ('Found pos1)) x+        (f2, rem2) = prR' (P :: Proxy ('Found pos2)) rem1+    in  ((f1, f2), rem2)++-- Scattered (:*:)-pair (f1 :*: f2)+instance ( ProjR ('Found pos1) f1 q+         , ProjR ('Found pos2) f2 (Remainder ('Found pos1) f1 q)+         )+    => ProjR ('Found ('Sum pos1 pos2)) (f1 :*: f2) q where+  prR' _ x =+    let (f1, rem1) = prR' (P :: Proxy ('Found pos1)) x+        (f2, rem2) = prR' (P :: Proxy ('Found pos2)) rem1+    in  (f1 :*: f2, rem2)++-- ---------------------------------------------------------------------------+-- 6.  Reconstruct — inverse of ProjR+-- ---------------------------------------------------------------------------++class Reconstruct (e :: Emb) (p :: Type) (q :: Type) where+  recons' :: Proxy e -> Remainder e p q -> p -> q++-- Base+instance Reconstruct ('Found 'Here) f f where+  recons' _ () x = x++-- Left branch of a tuple+instance Reconstruct ('Found pos) f g+    => Reconstruct ('Found ('Le pos)) f (g, g') where+  recons' _ (remL, r) p =+    (recons' (P :: Proxy ('Found pos)) remL p, r)++-- Right branch of a tuple+instance Reconstruct ('Found pos) f g+    => Reconstruct ('Found ('Ri pos)) f (g', g) where+  recons' _ (l, remR) p =+    (l, recons' (P :: Proxy ('Found pos)) remR p)++-- Left branch of a (:*:)+instance Reconstruct ('Found pos) f g+    => Reconstruct ('Found ('Le pos)) f (g :*: g') where+  recons' _ (remL :*: r) p =+    recons' (P :: Proxy ('Found pos)) remL p :*: r++-- Right branch of a (:*:)+instance Reconstruct ('Found pos) f g+    => Reconstruct ('Found ('Ri pos)) f (g' :*: g) where+  recons' _ (l :*: remR) p =+    l :*: recons' (P :: Proxy ('Found pos)) remR p++-- Scattered tuple-pair (f1, f2)+instance ( Reconstruct ('Found pos2) f2 (Remainder ('Found pos1) f1 q)+         , Reconstruct ('Found pos1) f1 q+         )+    => Reconstruct ('Found ('Sum pos1 pos2)) (f1, f2) q where+  recons' _ rem2 (f1, f2) =+    let rem1 = recons' (P :: Proxy ('Found pos2)) rem2 f2+    in  recons' (P :: Proxy ('Found pos1)) rem1 f1++-- Scattered (:*:)-pair (f1 :*: f2)+instance ( Reconstruct ('Found pos2) f2 (Remainder ('Found pos1) f1 q)+         , Reconstruct ('Found pos1) f1 q+         )+    => Reconstruct ('Found ('Sum pos1 pos2)) (f1 :*: f2) q where+  recons' _ rem2 (f1 :*: f2) =+    let rem1 = recons' (P :: Proxy ('Found pos2)) rem2 f2+    in  recons' (P :: Proxy ('Found pos1)) rem1 f1++-- ---------------------------------------------------------------------------+-- 7.  Public API+-- ---------------------------------------------------------------------------++-- | Bundles all constraints needed for 'uncons' and 'recons'.+type p :<| q =+  ( ProjR       (ComprEmb (Elem p q)) p q+  , Reconstruct (ComprEmb (Elem p q)) p q+  , p :<~ q+  )++-- | Project component @p@ from product @q@, also returning the remainder.+--+-- The remainder type is abstract — it should only be passed to 'recons'.+--+-- Law:  @uncurry (flip recons) (uncons x) == x@+--+-- Examples:+--   uncons @Int  (True, (42 :: Int, 'x'))  == (42,  (True, 'x'))+--   uncons @Bool (True :*: (42 :: Int))     == (True, () :*: 42)+uncons+  :: forall p q. (p :<| q)+  => q+  -> (p, RemainderOf p q)+uncons = prR' (P :: Proxy (ComprEmb (Elem p q)))++-- | Reconstruct the original product from a remainder and a+-- (possibly modified) projected component.+--+-- Examples:+--   let (n, rem) = uncons @Int (True, (42 :: Int, 'x'))+--   recons rem (n + 1)                    == (True, (43, 'x'))+--+--   let (b, rem) = uncons @Bool (True :*: (42 :: Int))+--   recons rem (not b)                    == (False :*: 42)+recons+  :: forall p q. (p :<| q)+  => RemainderOf p q+  -> p+  -> q+recons = recons' (P :: Proxy (ComprEmb (Elem p q)))++-- | Deconstruct and reconstruct a product, modifying a field+-- determined by the type of the given transformation function.+modify :: forall p q. (p :<| q)+  => (p -> p) -> q -> q+modify f q = recons rem (f p)+  where (p, rem) = uncons @p q++-- ---------------------------------------------------------------------------+-- 8.  Sanity checks (unexported; remove before packaging)+-- ---------------------------------------------------------------------------++-- Tuple-only product+_t1 :: (Bool, (Int, Char))+_t1 = let (n, rem) = uncons @Int (True, (42 :: Int, 'x'))+      in  recons rem (n + 1)           -- (True, (43, 'x'))++-- (:*:)-only product+_t2 :: Bool :*: Int+_t2 = let (b, rem) = uncons @Bool (True :*: (42 :: Int))+      in  recons rem (not b)           -- (False :*: 42)++-- Mixed: tuple on the outside, (:*:) on the inside+_t3 :: (Bool :*: Int, Char)+_t3 = let (n, rem) = uncons @Int ((True :*: (42 :: Int)), 'x')+      in  recons rem (n + 1)           -- ((True :*: 43), 'x')++-- Mixed: (:*:) on the outside, tuple on the inside+_t4 :: Bool :*: Int :*: Char+_t4 = let (b, rem) = uncons @Bool (True :*: (42 :: Int) :*: 'x')+      in  recons rem (not b)           -- ((False, 42) :*: 'x')
+ src/Data/Comp/SubsumeCommon.hs view
@@ -0,0 +1,168 @@+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE PolyKinds            #-}++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.SubsumeCommon+-- Copyright   :  (c) 2014 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Shared parts of the implementation of signature subsumption for+-- both the base and the multi library.+--+--------------------------------------------------------------------------------++module Data.Comp.SubsumeCommon+    ( ComprEmb+    , Pos (..)+    , Emb (..)+    , Choose+    , Sum'+    , Proxy (..)+    ) where++-- | This type is used in its promoted form only. It represents+-- pointers from the left-hand side of a subsumption to the right-hand+-- side.+data Pos = Here | Le Pos | Ri Pos | Sum Pos Pos++-- | This type is used in its promoted form only. It represents+-- possible results for checking for subsumptions. 'Found' indicates a+-- subsumption was found; 'NotFound' indicates no such subsumption was+-- found. 'Ambiguous' indicates that there are duplicates on the left-+-- or the right-hand side.+data Emb = Found Pos | NotFound | Ambiguous++data Proxy a = P+++type family Choose (e1 :: Emb) (r :: Emb) :: Emb where+    Choose (Found x) (Found y) = Ambiguous+    Choose Ambiguous y = Ambiguous+    Choose x Ambiguous = Ambiguous+    Choose (Found x) y = Found (Le x)+    Choose x (Found y) = Found (Ri y)+    Choose x y = NotFound+++type family Sum' (e1 :: Emb) (r :: Emb) :: Emb where+    Sum' (Found x) (Found y) = Found (Sum x y)+    Sum' Ambiguous y = Ambiguous+    Sum' x Ambiguous = Ambiguous+    Sum' NotFound y = NotFound+    Sum' x NotFound = NotFound+++-- | This type family takes a position type and compresses it. That+-- means it replaces each nested occurrence of+--+-- @+--   Sum (prefix (Le Here)) (prefix (Ri Here))@+-- @+---+-- with+--+-- @+--   prefix Here@+-- @+--+-- where @prefix@ is some composition of @Le@ and @Ri@. The rational+-- behind this type family is that it provides a more compact proof+-- term of a subsumption, and thus yields more efficient+-- implementations of 'inj' and 'prj'.++type family ComprPos (p :: Pos) :: Pos where+    ComprPos Here = Here+    ComprPos (Le p) = Le (ComprPos p)+    ComprPos (Ri p) = Ri (ComprPos p)+    ComprPos (Sum l r) = CombineRec (ComprPos l) (ComprPos r)+++-- | Helper type family for 'ComprPos'. Note that we could have+-- defined this as a type synonym. But if we do that, performance+-- becomes abysmal. I presume that the reason for this huge impact on+-- performance lies in the fact that right-hand side of the defining+-- equation duplicates the two arguments @l@ and @r@.+type family CombineRec l r where+    CombineRec l r = CombineMaybe (Sum l r) (Combine l r)++-- | Helper type family for 'ComprPos'.+type family CombineMaybe (p :: Pos) (p' :: Maybe Pos) where+    CombineMaybe p (Just p') = p'+    CombineMaybe p p'        = p+++-- | Helper type family for 'ComprPos'.+type family Combine (l :: Pos) (r :: Pos) :: Maybe Pos where+    Combine (Le l) (Le r) = Le' (Combine l r)+    Combine (Ri l) (Ri r) = Ri' (Combine l r)+    Combine (Le Here) (Ri Here) = Just Here+    Combine l r = Nothing++-- | 'Ri' lifted to 'Maybe'.+type family Ri' (p :: Maybe Pos) :: Maybe Pos where+    Ri' Nothing = Nothing+    Ri' (Just p) = Just (Ri p)++-- | 'Le' lifted to 'Maybe'.+type family Le' (p :: Maybe Pos) :: Maybe Pos where+    Le' Nothing = Nothing+    Le' (Just p) = Just (Le p)+++-- | If the argument is not 'Found', this type family is the+-- identity. Otherwise, the argument is of the form @Found p@, and+-- this type family does two things: (1) it checks whether @p@ the+-- contains duplicates; and (2) it compresses @p@ using 'ComprPos'. If+-- (1) finds no duplicates, @Found (ComprPos p)@ is returned;+-- otherwise @Ambiguous@ is returned.+--+-- For (1) it is assumed that @p@ does not contain 'Sum' nested+-- underneath a 'Le' or 'Ri' (i.e. only at the root or underneath a+-- 'Sum'). We will refer to such positions below as /atomic position/.+-- Positions not containing 'Sum' are called /simple positions/.+type family ComprEmb (e :: Emb) :: Emb where+    ComprEmb (Found p) = Check (Dupl p) (ComprPos p)+    ComprEmb e = e++-- | Helper type family for 'ComprEmb'.+type family Check (b :: Bool) (p :: Pos) where+    Check False p = Found p+    Check True  p = Ambiguous++-- | This type family turns a list of /atomic position/ into a list of+-- /simple positions/ by recursively splitting each position of the+-- form @Sum p1 p2@ into @p1@ and @p2@.+type family ToList (s :: [Pos]) :: [Pos] where+    ToList (Sum p1 p2 ': s) = ToList (p1 ': p2 ': s)+    ToList (p ': s) = p ': ToList s+    ToList '[] = '[]++-- | This type checks whether the argument (atomic) position has+-- duplicates.+type Dupl s = Dupl' (ToList '[s])++-- | This type family checks whether the list of positions given as an+-- argument contains any duplicates.+type family Dupl' (s :: [Pos]) :: Bool where+    Dupl' (p ': r) = OrDupl' (Find p r) r+    Dupl' '[] = False++-- | This type family checks whether its first argument is contained+-- its second argument.+type family Find (p :: Pos) (s :: [Pos]) :: Bool where+    Find p (p ': r)  = True+    Find p (p' ': r) = Find p r+    Find p '[] = False++-- | This type family returns @True@ if the first argument is true;+-- otherwise it checks the second argument for duplicates.+type family OrDupl' (a :: Bool) (b :: [Pos]) :: Bool where+    OrDupl'  True  c  = True+    OrDupl'  False c  = Dupl' c