{-# LANGUAGE RankNTypes #-}
-- | Invertible mappings between named pattern kinds.
--
-- A 'RepresentationMap' names a pair of compatible structural transforms between
-- two 'PatternKind's. The map itself carries only executable behavior and its
-- round-trip witness. Explanatory metadata about how a map works is deferred for
-- a later design that can express declarative, checkable claims rather than
-- inline prose attached to the value.
module Pattern.RepresentationMap
  ( RepresentationMap(..)
  , compose
  )
where

import Pattern.Core (Pattern, PatternKind, ScopeQuery, kindName)

-- | A named, invertible mapping between two pattern kinds.
--
-- A 'RepresentationMap' is the executable form of an isomorphism between named
-- shapes. 'forward' and 'inverse' are the two morphism components, while
-- 'roundTrip' is the machine-checkable witness that the mapping preserves
-- information on the domain kind.
--
-- Invariants for domain-kind inputs:
--
-- * 'forward' should produce a pattern accepted by 'codomain'.
-- * 'roundTrip' should hold.
-- * When 'roundTrip' holds, @(inverse m q . forward m q) p == p@ structurally.
--
-- Notes:
--
-- * Scope remains polymorphic, so maps are not tied to a particular backing
--   representation.
-- * Declarative, machine-checkable claims about map-specific encoding choices
--   are deferred; for now those details live in documentation and tests next to
--   concrete maps.
data RepresentationMap v = RepresentationMap
  { forall v. RepresentationMap v -> String
repMapName :: String
    -- ^ Unique human-readable name for the map.
  , forall v. RepresentationMap v -> PatternKind v
repMapDomain :: PatternKind v
    -- ^ Source kind. 'forward' is intended for patterns of this kind.
  , forall v. RepresentationMap v -> PatternKind v
repMapCodomain :: PatternKind v
    -- ^ Target kind. 'forward' should produce patterns of this kind.
  , forall v.
RepresentationMap v
-> forall (q :: * -> *).
   ScopeQuery q v =>
   q v -> Pattern v -> Pattern v
repMapForward :: forall q. ScopeQuery q v => q v -> Pattern v -> Pattern v
    -- ^ Domain-to-codomain transform, polymorphic over any valid scope.
  , forall v.
RepresentationMap v
-> forall (q :: * -> *).
   ScopeQuery q v =>
   q v -> Pattern v -> Pattern v
repMapInverse :: forall q. ScopeQuery q v => q v -> Pattern v -> Pattern v
    -- ^ Codomain-to-domain transform, polymorphic over any valid scope.
  , forall v.
RepresentationMap v
-> forall (q :: * -> *). ScopeQuery q v => q v -> Pattern v -> Bool
repMapRoundTrip :: forall q. ScopeQuery q v => q v -> Pattern v -> Bool
    -- ^ Isomorphism witness for domain-kind inputs at a given scope.
  }

-- | Compose two compatible representation maps.
--
-- Composition is defined only when the codomain kind of the first map has the
-- same 'kindName' as the domain kind of the second. The resulting map keeps
-- the first domain, the second codomain, composes 'forward' left-to-right,
-- composes 'inverse' right-to-left, and preserves round-trip validation in the
-- same order.
--
-- Categorical note: this is morphism composition for the category whose
-- objects are 'PatternKind's and whose isomorphisms are 'RepresentationMap's.
compose :: RepresentationMap v -> RepresentationMap v -> Either String (RepresentationMap v)
compose :: forall v.
RepresentationMap v
-> RepresentationMap v -> Either String (RepresentationMap v)
compose RepresentationMap v
m1 RepresentationMap v
m2
  | PatternKind v -> String
forall v. PatternKind v -> String
kindName (RepresentationMap v -> PatternKind v
forall v. RepresentationMap v -> PatternKind v
repMapCodomain RepresentationMap v
m1) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= PatternKind v -> String
forall v. PatternKind v -> String
kindName (RepresentationMap v -> PatternKind v
forall v. RepresentationMap v -> PatternKind v
repMapDomain RepresentationMap v
m2) =
      String -> Either String (RepresentationMap v)
forall a b. a -> Either a b
Left (String -> Either String (RepresentationMap v))
-> String -> Either String (RepresentationMap v)
forall a b. (a -> b) -> a -> b
$
        String
"compose: codomain of '" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> RepresentationMap v -> String
forall v. RepresentationMap v -> String
repMapName RepresentationMap v
m1
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"' (" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> PatternKind v -> String
forall v. PatternKind v -> String
kindName (RepresentationMap v -> PatternKind v
forall v. RepresentationMap v -> PatternKind v
repMapCodomain RepresentationMap v
m1)
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
") does not match domain of '" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> RepresentationMap v -> String
forall v. RepresentationMap v -> String
repMapName RepresentationMap v
m2
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"' (" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> PatternKind v -> String
forall v. PatternKind v -> String
kindName (RepresentationMap v -> PatternKind v
forall v. RepresentationMap v -> PatternKind v
repMapDomain RepresentationMap v
m2) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")"
  | Bool
otherwise =
      RepresentationMap v -> Either String (RepresentationMap v)
forall a b. b -> Either a b
Right
        RepresentationMap
          { repMapName :: String
repMapName = RepresentationMap v -> String
forall v. RepresentationMap v -> String
repMapName RepresentationMap v
m1 String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" >>> " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> RepresentationMap v -> String
forall v. RepresentationMap v -> String
repMapName RepresentationMap v
m2
          , repMapDomain :: PatternKind v
repMapDomain = RepresentationMap v -> PatternKind v
forall v. RepresentationMap v -> PatternKind v
repMapDomain RepresentationMap v
m1
          , repMapCodomain :: PatternKind v
repMapCodomain = RepresentationMap v -> PatternKind v
forall v. RepresentationMap v -> PatternKind v
repMapCodomain RepresentationMap v
m2
          , repMapForward :: forall (q :: * -> *).
ScopeQuery q v =>
q v -> Pattern v -> Pattern v
repMapForward = \q v
q Pattern v
p -> RepresentationMap v
-> forall (q :: * -> *).
   ScopeQuery q v =>
   q v -> Pattern v -> Pattern v
forall v.
RepresentationMap v
-> forall (q :: * -> *).
   ScopeQuery q v =>
   q v -> Pattern v -> Pattern v
repMapForward RepresentationMap v
m2 q v
q (RepresentationMap v
-> forall (q :: * -> *).
   ScopeQuery q v =>
   q v -> Pattern v -> Pattern v
forall v.
RepresentationMap v
-> forall (q :: * -> *).
   ScopeQuery q v =>
   q v -> Pattern v -> Pattern v
repMapForward RepresentationMap v
m1 q v
q Pattern v
p)
          , repMapInverse :: forall (q :: * -> *).
ScopeQuery q v =>
q v -> Pattern v -> Pattern v
repMapInverse = \q v
q Pattern v
p -> RepresentationMap v
-> forall (q :: * -> *).
   ScopeQuery q v =>
   q v -> Pattern v -> Pattern v
forall v.
RepresentationMap v
-> forall (q :: * -> *).
   ScopeQuery q v =>
   q v -> Pattern v -> Pattern v
repMapInverse RepresentationMap v
m1 q v
q (RepresentationMap v
-> forall (q :: * -> *).
   ScopeQuery q v =>
   q v -> Pattern v -> Pattern v
forall v.
RepresentationMap v
-> forall (q :: * -> *).
   ScopeQuery q v =>
   q v -> Pattern v -> Pattern v
repMapInverse RepresentationMap v
m2 q v
q Pattern v
p)
          , repMapRoundTrip :: forall (q :: * -> *). ScopeQuery q v => q v -> Pattern v -> Bool
repMapRoundTrip =
              \q v
q Pattern v
p -> RepresentationMap v
-> forall (q :: * -> *). ScopeQuery q v => q v -> Pattern v -> Bool
forall v.
RepresentationMap v
-> forall (q :: * -> *). ScopeQuery q v => q v -> Pattern v -> Bool
repMapRoundTrip RepresentationMap v
m1 q v
q Pattern v
p Bool -> Bool -> Bool
&& RepresentationMap v
-> forall (q :: * -> *). ScopeQuery q v => q v -> Pattern v -> Bool
forall v.
RepresentationMap v
-> forall (q :: * -> *). ScopeQuery q v => q v -> Pattern v -> Bool
repMapRoundTrip RepresentationMap v
m2 q v
q (RepresentationMap v
-> forall (q :: * -> *).
   ScopeQuery q v =>
   q v -> Pattern v -> Pattern v
forall v.
RepresentationMap v
-> forall (q :: * -> *).
   ScopeQuery q v =>
   q v -> Pattern v -> Pattern v
repMapForward RepresentationMap v
m1 q v
q Pattern v
p)
          }