-- | Entry point for Hydra's adapter (type/term rewriting) framework.
--   An adapter takes a type expression which is supported in a source language, and rewrites it to a type which is supported by a target language.
--   In parallel, terms conforming to the original type are rewritten. Both levels of the transformation are bidirectional.

module Hydra.Adapters where

import Hydra.TermAdapters
import Hydra.Printing
import Hydra.Coders
import Hydra.Compute
import Hydra.Core
import Hydra.Schemas
import Hydra.CoreLanguage
import Hydra.Graph
import Hydra.Lexical
import Hydra.Mantle
import Hydra.Module
import Hydra.Strip
import Hydra.TermAdapters
import Hydra.AdapterUtils
import Hydra.Reduction
import Hydra.Tier1
import Hydra.Tier2

import qualified Control.Monad as CM
import qualified Data.List as L
import qualified Data.Map as M
import qualified Data.Set as S


adaptAndEncodeType :: Language -> (Type -> Flow Graph t) -> Type -> Flow Graph t
adaptAndEncodeType :: forall t.
Language -> (Type -> Flow Graph t) -> Type -> Flow Graph t
adaptAndEncodeType Language
lang Type -> Flow Graph t
enc Type
typ = case Type -> Type
stripType Type
typ of
  TypeVariable Name
_ -> Type -> Flow Graph t
enc Type
typ
  Type
_ -> Language -> Type -> Flow Graph Type
adaptType Language
lang Type
typ Flow Graph Type -> (Type -> Flow Graph t) -> Flow Graph t
forall a b. Flow Graph a -> (a -> Flow Graph b) -> Flow Graph b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Flow Graph t
enc

-- | Given a target language and a source type, find the target type to which the latter will be adapted.
adaptType :: Language -> Type -> Flow Graph Type
adaptType :: Language -> Type -> Flow Graph Type
adaptType Language
lang Type
typ = Adapter Graph Graph Type Type Term Term -> Type
forall s1 s2 t1 t2 v1 v2. Adapter s1 s2 t1 t2 v1 v2 -> t2
adapterTarget (Adapter Graph Graph Type Type Term Term -> Type)
-> Flow Graph (Adapter Graph Graph Type Type Term Term)
-> Flow Graph Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Language
-> Type -> Flow Graph (Adapter Graph Graph Type Type Term Term)
languageAdapter Language
lang Type
typ

-- | Given a target language, a unidirectional last-mile encoding, and a source type,
--   construct a unidirectional adapting coder for terms of that type. Terms will be rewritten according to the type and
--   according to the constraints of the target language, then carried by the last mile into the final representation
constructCoder :: Language
  -> (Term -> Flow Graph c)
  -> Type
  -> Flow Graph (Coder Graph Graph Term c)
constructCoder :: forall c.
Language
-> (Term -> Flow Graph c)
-> Type
-> Flow Graph (Coder Graph Graph Term c)
constructCoder Language
lang Term -> Flow Graph c
encodeTerm Type
typ = String
-> Flow Graph (Coder Graph Graph Term c)
-> Flow Graph (Coder Graph Graph Term c)
forall s a. String -> Flow s a -> Flow s a
withTrace (String
"coder for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
describeType Type
typ) (Flow Graph (Coder Graph Graph Term c)
 -> Flow Graph (Coder Graph Graph Term c))
-> Flow Graph (Coder Graph Graph Term c)
-> Flow Graph (Coder Graph Graph Term c)
forall a b. (a -> b) -> a -> b
$ do
    Adapter Graph Graph Type Type Term Term
adapter <- Language
-> Type -> Flow Graph (Adapter Graph Graph Type Type Term Term)
languageAdapter Language
lang Type
typ
    Coder Graph Graph Term c -> Flow Graph (Coder Graph Graph Term c)
forall a. a -> Flow Graph a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coder Graph Graph Term c -> Flow Graph (Coder Graph Graph Term c))
-> Coder Graph Graph Term c
-> Flow Graph (Coder Graph Graph Term c)
forall a b. (a -> b) -> a -> b
$ Coder Graph Graph Term Term
-> Coder Graph Graph Term c -> Coder Graph Graph Term c
forall s a b c. Coder s s a b -> Coder s s b c -> Coder s s a c
composeCoders (Adapter Graph Graph Type Type Term Term
-> Coder Graph Graph Term Term
forall s1 s2 t1 t2 v1 v2.
Adapter s1 s2 t1 t2 v1 v2 -> Coder s1 s2 v1 v2
adapterCoder Adapter Graph Graph Type Type Term Term
adapter) ((Term -> Flow Graph c) -> Coder Graph Graph Term c
forall a s b. (a -> Flow s b) -> Coder s s a b
unidirectionalCoder Term -> Flow Graph c
encodeTerm)

-- | Given a target language and a source type, produce an adapter,
--   which rewrites the type and its terms according to the language's constraints
languageAdapter :: Language -> Type -> Flow Graph (SymmetricAdapter Graph Type Term)
languageAdapter :: Language
-> Type -> Flow Graph (Adapter Graph Graph Type Type Term Term)
languageAdapter Language
lang Type
typ0 = do
  -- TODO: rather than beta-reducing types all at once, we should incrementally extend the environment when application types are adapted
  -- typ <- betaReduceType typ0
  let typ :: Type
typ = Type
typ0

  Graph
g  <- Flow Graph Graph
forall s. Flow s s
getState
  -- Provide an initial adapter context
  let cx0 :: AdapterContext
cx0 = Graph
-> Language
-> Map
     Name (Adapter AdapterContext AdapterContext Type Type Term Term)
-> AdapterContext
AdapterContext Graph
g Language
lang Map
  Name (Adapter AdapterContext AdapterContext Type Type Term Term)
forall k a. Map k a
M.empty
  -- Construct the term adapter, and capture the populated adapter context
  (Adapter AdapterContext AdapterContext Type Type Term Term
adapter, AdapterContext
cx) <- AdapterContext
-> Flow
     AdapterContext
     (Adapter AdapterContext AdapterContext Type Type Term Term,
      AdapterContext)
-> Flow
     Graph
     (Adapter AdapterContext AdapterContext Type Type Term Term,
      AdapterContext)
forall s1 a s2. s1 -> Flow s1 a -> Flow s2 a
withState AdapterContext
cx0 (Flow
   AdapterContext
   (Adapter AdapterContext AdapterContext Type Type Term Term,
    AdapterContext)
 -> Flow
      Graph
      (Adapter AdapterContext AdapterContext Type Type Term Term,
       AdapterContext))
-> Flow
     AdapterContext
     (Adapter AdapterContext AdapterContext Type Type Term Term,
      AdapterContext)
-> Flow
     Graph
     (Adapter AdapterContext AdapterContext Type Type Term Term,
      AdapterContext)
forall a b. (a -> b) -> a -> b
$ do
    Adapter AdapterContext AdapterContext Type Type Term Term
ad <- TypeAdapter
termAdapter Type
typ
    AdapterContext
cx <- Flow AdapterContext AdapterContext
forall s. Flow s s
getState -- The state has been mutated to hold adapters for type elements
    (Adapter AdapterContext AdapterContext Type Type Term Term,
 AdapterContext)
-> Flow
     AdapterContext
     (Adapter AdapterContext AdapterContext Type Type Term Term,
      AdapterContext)
forall a. a -> Flow AdapterContext a
forall (m :: * -> *) a. Monad m => a -> m a
return (Adapter AdapterContext AdapterContext Type Type Term Term
ad, AdapterContext
cx)
  -- Wrap terms in the adapter context as they pass through the adapter coder
  let ac :: Coder s1 s2 Term Term
ac = (Term -> Flow s1 Term)
-> (Term -> Flow s2 Term) -> Coder s1 s2 Term Term
forall s1 s2 v1 v2.
(v1 -> Flow s1 v2) -> (v2 -> Flow s2 v1) -> Coder s1 s2 v1 v2
Coder Term -> Flow s1 Term
forall {s2}. Term -> Flow s2 Term
encode Term -> Flow s2 Term
forall {s2}. Term -> Flow s2 Term
decode
        where
          encode :: Term -> Flow s2 Term
encode = AdapterContext -> Flow AdapterContext Term -> Flow s2 Term
forall s1 a s2. s1 -> Flow s1 a -> Flow s2 a
withState AdapterContext
cx (Flow AdapterContext Term -> Flow s2 Term)
-> (Term -> Flow AdapterContext Term) -> Term -> Flow s2 Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coder AdapterContext AdapterContext Term Term
-> Term -> Flow AdapterContext Term
forall s1 s2 v1 v2. Coder s1 s2 v1 v2 -> v1 -> Flow s1 v2
coderEncode (Adapter AdapterContext AdapterContext Type Type Term Term
-> Coder AdapterContext AdapterContext Term Term
forall s1 s2 t1 t2 v1 v2.
Adapter s1 s2 t1 t2 v1 v2 -> Coder s1 s2 v1 v2
adapterCoder Adapter AdapterContext AdapterContext Type Type Term Term
adapter)
          decode :: Term -> Flow s2 Term
decode = AdapterContext -> Flow AdapterContext Term -> Flow s2 Term
forall s1 a s2. s1 -> Flow s1 a -> Flow s2 a
withState AdapterContext
cx (Flow AdapterContext Term -> Flow s2 Term)
-> (Term -> Flow AdapterContext Term) -> Term -> Flow s2 Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coder AdapterContext AdapterContext Term Term
-> Term -> Flow AdapterContext Term
forall s1 s2 v1 v2. Coder s1 s2 v1 v2 -> v2 -> Flow s2 v1
coderDecode (Adapter AdapterContext AdapterContext Type Type Term Term
-> Coder AdapterContext AdapterContext Term Term
forall s1 s2 t1 t2 v1 v2.
Adapter s1 s2 t1 t2 v1 v2 -> Coder s1 s2 v1 v2
adapterCoder Adapter AdapterContext AdapterContext Type Type Term Term
adapter)
  Adapter Graph Graph Type Type Term Term
-> Flow Graph (Adapter Graph Graph Type Type Term Term)
forall a. a -> Flow Graph a
forall (m :: * -> *) a. Monad m => a -> m a
return (Adapter Graph Graph Type Type Term Term
 -> Flow Graph (Adapter Graph Graph Type Type Term Term))
-> Adapter Graph Graph Type Type Term Term
-> Flow Graph (Adapter Graph Graph Type Type Term Term)
forall a b. (a -> b) -> a -> b
$ Adapter AdapterContext AdapterContext Type Type Term Term
adapter {adapterCoder = ac}

-- | Given a target language, a unidirectional last mile encoding, and an intermediate helper function,
--   transform a given module into a target representation
transformModule :: Language
  -> (Term -> Flow Graph e)
  -> (Module -> M.Map Type (Coder Graph Graph Term e) -> [(Element, TypedTerm)] -> Flow Graph d)
  -> Module -> Flow Graph d
transformModule :: forall e d.
Language
-> (Term -> Flow Graph e)
-> (Module
    -> Map Type (Coder Graph Graph Term e)
    -> [(Element, TypedTerm)]
    -> Flow Graph d)
-> Module
-> Flow Graph d
transformModule Language
lang Term -> Flow Graph e
encodeTerm Module
-> Map Type (Coder Graph Graph Term e)
-> [(Element, TypedTerm)]
-> Flow Graph d
createModule Module
mod = String -> Flow Graph d -> Flow Graph d
forall s a. String -> Flow s a -> Flow s a
withTrace (String
"transform module " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Namespace -> String
unNamespace (Module -> Namespace
moduleNamespace Module
mod)) (Flow Graph d -> Flow Graph d) -> Flow Graph d -> Flow Graph d
forall a b. (a -> b) -> a -> b
$ do
    [TypedTerm]
tterms <- Flow Graph [TypedTerm] -> Flow Graph [TypedTerm]
forall x. Flow Graph x -> Flow Graph x
withSchemaContext (Flow Graph [TypedTerm] -> Flow Graph [TypedTerm])
-> Flow Graph [TypedTerm] -> Flow Graph [TypedTerm]
forall a b. (a -> b) -> a -> b
$ (Element -> Flow Graph TypedTerm)
-> [Element] -> Flow Graph [TypedTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
CM.mapM Element -> Flow Graph TypedTerm
elementAsTypedTerm [Element]
els
    let types :: [Type]
types = [Type] -> [Type]
forall a. Eq a => [a] -> [a]
L.nub (TypedTerm -> Type
typedTermType (TypedTerm -> Type) -> [TypedTerm] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TypedTerm]
tterms)
    Map Type (Coder Graph Graph Term e)
coders <- [Type] -> Flow Graph (Map Type (Coder Graph Graph Term e))
codersFor [Type]
types
    Module
-> Map Type (Coder Graph Graph Term e)
-> [(Element, TypedTerm)]
-> Flow Graph d
createModule Module
mod Map Type (Coder Graph Graph Term e)
coders ([(Element, TypedTerm)] -> Flow Graph d)
-> [(Element, TypedTerm)] -> Flow Graph d
forall a b. (a -> b) -> a -> b
$ [Element] -> [TypedTerm] -> [(Element, TypedTerm)]
forall a b. [a] -> [b] -> [(a, b)]
L.zip [Element]
els [TypedTerm]
tterms
  where
    els :: [Element]
els = Module -> [Element]
moduleElements Module
mod

    codersFor :: [Type] -> Flow Graph (Map Type (Coder Graph Graph Term e))
codersFor [Type]
types = do
      [Coder Graph Graph Term e]
cdrs <- (Type -> Flow Graph (Coder Graph Graph Term e))
-> [Type] -> Flow Graph [Coder Graph Graph Term e]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
CM.mapM (Language
-> (Term -> Flow Graph e)
-> Type
-> Flow Graph (Coder Graph Graph Term e)
forall c.
Language
-> (Term -> Flow Graph c)
-> Type
-> Flow Graph (Coder Graph Graph Term c)
constructCoder Language
lang Term -> Flow Graph e
encodeTerm) [Type]
types
      Map Type (Coder Graph Graph Term e)
-> Flow Graph (Map Type (Coder Graph Graph Term e))
forall a. a -> Flow Graph a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Type (Coder Graph Graph Term e)
 -> Flow Graph (Map Type (Coder Graph Graph Term e)))
-> Map Type (Coder Graph Graph Term e)
-> Flow Graph (Map Type (Coder Graph Graph Term e))
forall a b. (a -> b) -> a -> b
$ [(Type, Coder Graph Graph Term e)]
-> Map Type (Coder Graph Graph Term e)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Type, Coder Graph Graph Term e)]
 -> Map Type (Coder Graph Graph Term e))
-> [(Type, Coder Graph Graph Term e)]
-> Map Type (Coder Graph Graph Term e)
forall a b. (a -> b) -> a -> b
$ [Type]
-> [Coder Graph Graph Term e] -> [(Type, Coder Graph Graph Term e)]
forall a b. [a] -> [b] -> [(a, b)]
L.zip [Type]
types [Coder Graph Graph Term e]
cdrs