content: {-# LANGUAGE OverloadedStrings #-}
  
  module Hydra.Sources.Kernel.Terms.Adapt.Terms where
  
  -- Standard imports for term-level kernel modules
  import Hydra.Kernel
  import Hydra.Sources.Libraries
  import qualified Hydra.Dsl.Accessors     as Accessors
  import qualified Hydra.Dsl.Ast           as Ast
  import qualified Hydra.Dsl.Coders        as Coders
  import qualified Hydra.Dsl.Compute       as Compute
  import qualified Hydra.Dsl.Core          as Core
  import qualified Hydra.Dsl.Grammar       as Grammar
  import qualified Hydra.Dsl.Graph         as Graph
  import qualified Hydra.Dsl.Json          as Json
  import qualified Hydra.Dsl.Lib.Chars     as Chars
  import qualified Hydra.Dsl.Lib.Equality  as Equality
  import qualified Hydra.Dsl.Lib.Flows     as Flows
  import qualified Hydra.Dsl.Lib.Lists     as Lists
  import qualified Hydra.Dsl.Lib.Literals  as Literals
  import qualified Hydra.Dsl.Lib.Logic     as Logic
  import qualified Hydra.Dsl.Lib.Maps      as Maps
  import qualified Hydra.Dsl.Lib.Math      as Math
  import qualified Hydra.Dsl.Lib.Optionals as Optionals
  import           Hydra.Dsl.Phantoms      as Phantoms
  import qualified Hydra.Dsl.Lib.Sets      as Sets
  import           Hydra.Dsl.Lib.Strings   as Strings
  import qualified Hydra.Dsl.Mantle        as Mantle
  import qualified Hydra.Dsl.Module        as Module
  import qualified Hydra.Dsl.TTerms        as TTerms
  import qualified Hydra.Dsl.TTypes        as TTypes
  import qualified Hydra.Dsl.Terms         as Terms
  import qualified Hydra.Dsl.Topology      as Topology
  import qualified Hydra.Dsl.Types         as Types
  import qualified Hydra.Dsl.Typing        as Typing
  import           Hydra.Sources.Kernel.Types.All
  import           Prelude hiding ((++))
  import qualified Data.Int                as I
  import qualified Data.List               as L
  import qualified Data.Map                as M
  import qualified Data.Set                as S
  import qualified Data.Maybe              as Y
  
  import qualified Hydra.Sources.Kernel.Terms.Adapt.Literals as AdaptLiterals
  import qualified Hydra.Sources.Kernel.Terms.Adapt.Utils as AdaptUtils
  import qualified Hydra.Sources.Kernel.Terms.Describe.Core as DescribeCore
  import qualified Hydra.Sources.Kernel.Terms.Extract.Core as ExtractCore
  import qualified Hydra.Sources.Kernel.Terms.Literals as Lits
  import qualified Hydra.Sources.Kernel.Terms.Monads as Monads
  import qualified Hydra.Sources.Kernel.Terms.Rewriting as Rewriting
  import qualified Hydra.Sources.Kernel.Terms.Schemas as Schemas
  import qualified Hydra.Sources.Kernel.Terms.Show.Core as ShowCore
  import qualified Hydra.Sources.Kernel.Terms.Annotations as Annotations
  import qualified Hydra.Sources.Kernel.Terms.Variants as Variants
  
  
  module_ :: Module
  module_ = Module (Namespace "hydra.adapt.terms") elements
      [ExtractCore.module_, AdaptLiterals.module_, Lits.module_, Rewriting.module_,
        Schemas.module_, ShowCore.module_]
      kernelTypesModules $
      Just "Adapter framework for types and terms"
    where
      elements = [
        el fieldAdapterDef,
        el forTypeReferenceDef,
        el functionProxyNameDef,
        el functionProxyTypeDef,
        el functionToUnionDef,
        el lambdaToMonotypeDef,
        el optionalToListDef,
        el passApplicationDef,
        el passFunctionDef,
        el passForallDef,
        el passLiteralDef,
        el passListDef,
        el passMapDef,
        el passOptionalDef,
        el passProductDef,
        el passRecordDef,
        el passSetDef,
        el passSumDef,
        el passUnionDef,
        el passUnitDef,
        el passWrappedDef,
        el setToListDef,
        el simplifyApplicationDef,
        el termAdapterDef,
        el unionToRecordDef,
        el unionTypeToRecordTypeDef,
        el unitToRecordDef,
        el wrapToUnwrappedDef,
        el withGraphContextDef]
  
  define :: String -> TTerm a -> TBinding a
  define = definitionInModule module_
  
  fieldAdapterDef :: TBinding (FieldType -> Flow AdapterContext (SymmetricAdapter AdapterContext FieldType Field))
  fieldAdapterDef = define "fieldAdapter" $
    doc "Create an adapter for field types" $
    lambda "ftyp" $
      Flows.bind (ref termAdapterDef @@ (Core.fieldTypeType $ var "ftyp")) $ lambda "ad" $
        Flows.pure $ Compute.adapter
          (Compute.adapterIsLossy $ var "ad")
          (var "ftyp")
          (Core.fieldType (Core.fieldTypeName $ var "ftyp") (Compute.adapterTarget $ var "ad"))
          (ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "field"] $ lets [
            "name">: Core.fieldName $ var "field",
            "term">: Core.fieldTerm $ var "field"] $
            Flows.map (lambda "newTerm" $ Core.field (var "name") (var "newTerm")) $
              ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ var "ad") @@ var "term"))
  
  forTypeReferenceDef :: TBinding (Name -> Flow AdapterContext (SymmetricAdapter AdapterContext Type Term))
  forTypeReferenceDef = define "forTypeReference" $
    doc "This function accounts for recursive type definitions" $
    lambda "name" $
    trace (Strings.cat2 (string "adapt named type ") (unwrap _Name @@ var "name")) $ lets [
    "lossy">: false,
    "placeholder">: Compute.adapter (var "lossy") (Core.typeVariable $ var "name") (Core.typeVariable $ var "name") $
      ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $
        bind "cx" (ref Monads.getStateDef) $ lets [
          "adapters">: Coders.adapterContextAdapters $ var "cx"] $
          Optionals.maybe
            (Flows.fail $ Strings.cat2 (string "no adapter for reference type ") (unwrap _Name @@ var "name"))
            (lambda "ad" $ ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ var "ad") @@ var "term")
            (Maps.lookup (var "name") (var "adapters")))] $
    bind "cx" (ref Monads.getStateDef) $ lets [
    "adapters">: Coders.adapterContextAdapters $ var "cx"] $
    Optionals.maybe
      (lets [
        "newAdapters">: Maps.insert (var "name") (var "placeholder") (var "adapters"),
        "newCx">: Coders.adapterContext
          (Coders.adapterContextGraph $ var "cx")
          (Coders.adapterContextLanguage $ var "cx")
          (var "newAdapters")] $
        Flows.bind (ref Monads.putStateDef @@ var "newCx") $ constant $
          bind "mt" (ref withGraphContextDef @@ (ref Schemas.resolveTypeDef @@ (Core.typeVariable $ var "name"))) $
            Optionals.maybe
              (Flows.pure $ Compute.adapter (var "lossy") (Core.typeVariable $ var "name") (Core.typeVariable $ var "name") $
                ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $ Flows.pure $ var "term"))
              (lambda "t" $
                bind "actual" (ref termAdapterDef @@ var "t") $ lets [
                  "finalAdapters">: Maps.insert (var "name") (var "actual") (var "adapters"),
                  "finalCx">: Coders.adapterContext
                    (Coders.adapterContextGraph $ var "cx")
                    (Coders.adapterContextLanguage $ var "cx")
                    (var "finalAdapters")] $
                Flows.bind (ref Monads.putStateDef @@ var "finalCx") $ constant $ Flows.pure $ var "actual")
              (var "mt"))
      (unaryFunction Flows.pure)
      (Maps.lookup (var "name") (var "adapters"))
  
  functionProxyNameDef :: TBinding Name
  functionProxyNameDef = define "functionProxyName" $
    Core.name "hydra.core.FunctionProxy"
  
  functionProxyTypeDef :: TBinding (a -> Type)
  functionProxyTypeDef = define "functionProxyType" $
    doc "Generate a function proxy type for a given domain type" $
    constant $ Core.typeUnion $ Core.rowType (ref functionProxyNameDef) $ list [
      Core.fieldType (Core.nameLift _Elimination_wrap) TTypes.string,
      Core.fieldType (Core.nameLift _Elimination_record) TTypes.string,
      Core.fieldType (Core.nameLift _Elimination_union) TTypes.string,
      Core.fieldType (Core.nameLift _Function_lambda) TTypes.string,
      Core.fieldType (Core.nameLift _Function_primitive) TTypes.string,
      Core.fieldType (Core.nameLift _Term_variable) TTypes.string]
  
  functionToUnionDef :: TBinding TypeAdapter
  functionToUnionDef = define "functionToUnion" $
    doc "Convert function types to union types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_function>>: lambda "ft" $ lets [
        "dom">: Core.functionTypeDomain $ var "ft",
        "cod">: Core.functionTypeCodomain $ var "ft",
        "unionType">:
          bind "domAd" (ref termAdapterDef @@ var "dom") $
          Flows.pure $ Core.typeUnion $ Core.rowType (ref functionProxyNameDef) $ list [
            Core.fieldType (Core.nameLift _Elimination_wrap) TTypes.string,
            Core.fieldType (Core.nameLift _Elimination_record) TTypes.string,
            Core.fieldType (Core.nameLift _Elimination_union) TTypes.string,
            Core.fieldType (Core.nameLift _Function_lambda) TTypes.string,
            Core.fieldType (Core.nameLift _Function_primitive) TTypes.string,
            Core.fieldType (Core.nameLift _Term_variable) TTypes.string],
        "encode">: lambdas ["ad", "term"] $ lets [
          "strippedTerm">: ref Rewriting.deannotateTermDef @@ var "term"] $
          Compute.coderEncode (Compute.adapterCoder $ var "ad") @@ (cases _Term (var "strippedTerm") Nothing [
            _Term_function>>: lambda "f" $ cases _Function (var "f") Nothing [
              _Function_elimination>>: lambda "e" $ cases _Elimination (var "e") Nothing [
                _Elimination_wrap>>: lambda "name" $ Core.termUnion $ Core.injection (ref functionProxyNameDef) $
                  Core.field (Core.nameLift _Elimination_wrap) $ TTerms.stringLift $ unwrap _Name @@ var "name",
                _Elimination_record>>: lambda "r" $ Core.termUnion $ Core.injection (ref functionProxyNameDef) $
                  Core.field (Core.nameLift _Elimination_record) $ TTerms.stringLift (ref ShowCore.termDef @@ var "term"),
                _Elimination_union>>: lambda "u" $ Core.termUnion $ Core.injection (ref functionProxyNameDef) $
                  Core.field (Core.nameLift _Elimination_union) $ TTerms.stringLift (ref ShowCore.termDef @@ var "term")],
              _Function_lambda>>: lambda "l" $ Core.termUnion $ Core.injection (ref functionProxyNameDef) $
                Core.field (Core.nameLift _Function_lambda) $ TTerms.stringLift (ref ShowCore.termDef @@ var "term"),
              _Function_primitive>>: lambda "name" $ Core.termUnion $ Core.injection (ref functionProxyNameDef) $
                Core.field (Core.nameLift _Function_primitive) $ TTerms.stringLift $ unwrap _Name @@ var "name"],
            _Term_variable>>: lambda "name" $
              Core.termUnion $ Core.injection (ref functionProxyNameDef) $ Core.field (Core.nameLift _Term_variable) $ TTerms.stringLift $ unwrap _Name @@ var "name"]),
        "decode">: lambdas ["ad", "term"] $ lets [
          "readFromString">: lambda "term" $
            bind "s" (ref ExtractCore.stringDef @@ var "term") $
              Optionals.maybe
                (Flows.fail $ Strings.cat2 ("failed to parse term: ") (var "s"))
                (unaryFunction Flows.pure)
                (ref ShowCore.readTermDef @@ var "s"),
          "notFound">: lambda "fname" $ Flows.fail $ Strings.cat2 (string "unexpected field: ") (unwrap _Name @@ var "fname"),
          "forCases">: lambda "fterm" $ ref withGraphContextDef @@ (var "readFromString" @@ var "fterm"),
          "forLambda">: lambda "fterm" $ ref withGraphContextDef @@ (var "readFromString" @@ var "fterm"),
          "forWrapped">: lambda "fterm" $ ref withGraphContextDef @@ (Flows.map (lambda "s" $ TTerms.unwrap $ Core.name $ var "s") (ref ExtractCore.stringDef @@ var "fterm")),
          "forPrimitive">: lambda "fterm" $ ref withGraphContextDef @@ (Flows.map (lambda "s" $ TTerms.primitiveLift $ Core.name $ var "s") (ref ExtractCore.stringDef @@ var "fterm")),
          "forProjection">: lambda "fterm" $ ref withGraphContextDef @@ (var "readFromString" @@ var "fterm"),
          "forVariable">: lambda "fterm" $ ref withGraphContextDef @@ (Flows.map (lambda "s" $ Core.termVariable $ Core.name $ var "s") (ref ExtractCore.stringDef @@ var "fterm"))] $
          bind "injTerm" (Compute.coderDecode (Compute.adapterCoder $ var "ad") @@ var "term") $
          bind "field" (ref withGraphContextDef @@ (ref ExtractCore.injectionDef @@ (ref functionProxyNameDef) @@ var "injTerm")) $ lets [
              "fname">: Core.fieldName $ var "field",
              "fterm">: Core.fieldTerm $ var "field"] $
              Optionals.fromMaybe (var "notFound" @@ var "fname") $ Maps.lookup (var "fname") $ Maps.fromList $ list [
                pair (Core.nameLift _Elimination_wrap) (var "forWrapped" @@ var "fterm"),
                pair (Core.nameLift _Elimination_record) (var "forProjection" @@ var "fterm"),
                pair (Core.nameLift _Elimination_union) (var "forCases" @@ var "fterm"),
                pair (Core.nameLift _Function_lambda) (var "forLambda" @@ var "fterm"),
                pair (Core.nameLift _Function_primitive) (var "forPrimitive" @@ var "fterm"),
                pair (Core.nameLift _Term_variable) (var "forVariable" @@ var "fterm")]] $
      bind "ut" (var "unionType") $
      bind "ad" (ref termAdapterDef @@ var "ut") $
      Flows.pure $ Compute.adapter
        (Compute.adapterIsLossy $ var "ad")
        (var "t")
        (Compute.adapterTarget $ var "ad")
        (Compute.coder (var "encode" @@ var "ad") (var "decode" @@ var "ad"))]
  
  lambdaToMonotypeDef :: TBinding TypeAdapter
  lambdaToMonotypeDef = define "lambdaToMonotype" $
    doc "Convert forall types to monotypes" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_forall>>: lambda "ft" $ lets [
          "body">: Core.forallTypeBody $ var "ft"] $
          bind "ad" (ref termAdapterDef @@ var "body") $
          Flows.pure $ Compute.adapter
            (Compute.adapterIsLossy $ var "ad")
            (var "t")
            (Compute.adapterTarget $ var "ad")
            (Compute.adapterCoder $ var "ad")]
  
  optionalToListDef :: TBinding TypeAdapter
  optionalToListDef = define "optionalToList" $
    doc "Convert optional types to list types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_optional>>: lambda "ot" $
        bind "ad" (ref termAdapterDef @@ var "ot") $ lets [
          "encode">: lambda "term" $ cases _Term (var "term") Nothing [
            _Term_optional>>: lambda "m" $ Optionals.maybe
              (Flows.pure $ TTerms.list [])
              (lambda "r" $
                bind "encoded" (Compute.coderEncode (Compute.adapterCoder $ var "ad") @@ var "r") $
                Flows.pure $ Core.termList $ list [var "encoded"])
              (var "m")],
          "decode">: lambda "term" $ cases _Term (var "term") Nothing [
            _Term_list>>: lambda "l" $ Flows.map (unaryFunction Core.termOptional) $ Logic.ifElse (Lists.null $ var "l")
              (Flows.pure $ nothing)
              (bind "decoded" (Compute.coderDecode (Compute.adapterCoder $ var "ad") @@ (Lists.head $ var "l")) $
                Flows.pure $ just $ var "decoded")]] $
        Flows.pure $ Compute.adapter
          false
          (var "t")
          (Core.typeList $ Compute.adapterTarget $ var "ad")
          (Compute.coder (var "encode") (var "decode"))]
  
  passApplicationDef :: TBinding TypeAdapter
  passApplicationDef = define "passApplication" $
    doc "Pass through application types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_application>>: lambda "at" $ lets [
          "lhs">: Core.applicationTypeFunction $ var "at",
          "rhs">: Core.applicationTypeArgument $ var "at"] $
          bind "lhsAd" (ref termAdapterDef @@ var "lhs") $
          bind "rhsAd" (ref termAdapterDef @@ var "rhs") $
          Flows.pure $ Compute.adapter
            (Logic.or (Compute.adapterIsLossy $ var "lhsAd") (Compute.adapterIsLossy $ var "rhsAd"))
            (var "t")
            (Core.typeApplication $ Core.applicationType (Compute.adapterTarget $ var "lhsAd") (Compute.adapterTarget $ var "rhsAd"))
            (ref AdaptUtils.bidirectionalDef @@
              (lambdas ["dir", "term"] $ ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ var "lhsAd") @@ var "term"))]
  
  passFunctionDef :: TBinding TypeAdapter
  passFunctionDef = define "passFunction" $
    doc "Pass through function types with adaptation" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_function >>: lambda "ft" $ lets [
        "dom">: Core.functionTypeDomain $ var "ft",
        "cod">: Core.functionTypeCodomain $ var "ft"] $
        bind "domAd" (ref termAdapterDef @@ var "dom") $
        bind "codAd" (ref termAdapterDef @@ var "cod") $
        bind "caseAds" (cases _Type (ref Rewriting.deannotateTypeDef @@ var "dom") (Just $ Flows.pure $ Maps.empty) [
          _Type_union >>: lambda "rt" $
            bind "pairs" (Flows.mapList
              (lambda "f" $
                bind "ad" (ref fieldAdapterDef @@ Core.fieldType
                  (Core.fieldTypeName $ var "f")
                  (Core.typeFunction $ Core.functionType
                    (Core.fieldTypeType $ var "f")
                    (var "cod")))
                $ Flows.pure $ pair (Core.fieldTypeName $ var "f") (var "ad"))
              (Core.rowTypeFields $ var "rt")) $
            Flows.pure $ Maps.fromList $ var "pairs"]) $
        bind "optionAd" (cases _Type (ref Rewriting.deannotateTypeDef @@ var "dom") (Just $ Flows.pure nothing) [
          _Type_optional >>: lambda "ot" $
            Flows.map (unaryFunction just) $ ref termAdapterDef @@ TTypes.function (var "ot") (var "cod")]) $ lets [
        "lossy">: Logic.or
          (Compute.adapterIsLossy $ var "codAd")
          (Logic.ors $ Lists.map (lambda "pair" $ Compute.adapterIsLossy $ second $ var "pair") $ Maps.toList $ var "caseAds"),
        "target">: TTypes.function (Compute.adapterTarget $ var "domAd") (Compute.adapterTarget $ var "codAd"),
        "getCoder">: lambda "fname" $ Optionals.maybe
          (ref AdaptUtils.idCoderDef)
          (unaryFunction Compute.adapterCoder)
          (Maps.lookup (var "fname") (var "caseAds"))] $
        Flows.pure $ Compute.adapter (var "lossy") (var "t") (var "target") $
          ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $
            cases _Term (ref Rewriting.deannotateTermDef @@ var "term") (Just $ Flows.pure $ var "term") [
              _Term_function >>: lambda "f" $
                Flows.map (unaryFunction Core.termFunction) $
                  cases _Function (var "f") Nothing [
                    _Function_elimination >>: lambda "e" $
                      Flows.map (unaryFunction Core.functionElimination) $
                        cases _Elimination (var "e") Nothing [
                          _Elimination_union >>: lambda "cs" $ lets [
                            "n">: Core.caseStatementTypeName $ var "cs",
                            "def">: Core.caseStatementDefault $ var "cs",
                            "cases">: Core.caseStatementCases $ var "cs"] $
                            bind "rcases" (Flows.mapList
                              (lambda "f" $ ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (var "getCoder" @@ Core.fieldName (var "f")) @@ var "f")
                              (var "cases")) $
                            bind "rdef" (Optionals.maybe
                              (Flows.pure nothing)
                              (lambda "d" $ Flows.map (unaryFunction just) $ ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ Compute.adapterCoder (var "codAd") @@ var "d")
                              (var "def")) $
                            Flows.pure $ Core.eliminationUnion $ Core.caseStatement (var "n") (var "rdef") (var "rcases")],
                    _Function_lambda >>: lambda "l" $ lets [
                      "var">: Core.lambdaParameter $ var "l",
                      "d" >: Core.lambdaDomain $ var "l",
                      "body">: Core.lambdaBody $ var "l"] $
                      bind "newBody" (ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ Compute.adapterCoder (var "codAd") @@ var "body") $
                      Flows.pure $ Core.functionLambda $ Core.lambda (var "var") (var "d") (var "newBody"),
                    _Function_primitive >>: lambda "name" $ Flows.pure $ Core.functionPrimitive $ var "name"]]
           )]
  
  passForallDef :: TBinding TypeAdapter
  passForallDef = define "passForall" $
    doc "Pass through forall types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_forall>>: lambda "ft" $ lets [
          "v">: Core.forallTypeParameter $ var "ft",
          "body">: Core.forallTypeBody $ var "ft"] $
          Flows.bind (ref termAdapterDef @@ var "body") $ lambda "ad" $
            Flows.pure $ Compute.adapter
              (Compute.adapterIsLossy $ var "ad")
              (var "t")
              (Core.typeForall $ Core.forallType (var "v") (Compute.adapterTarget $ var "ad"))
              (ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $
                ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ var "ad") @@ var "term"))]
  
  passLiteralDef :: TBinding TypeAdapter
  passLiteralDef = define "passLiteral" $
    doc "Pass through literal types with literal adaptation" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_literal>>: lambda "lt" $
        bind "ad" (ref AdaptLiterals.literalAdapterDef @@ var "lt") $ lets [
        "step">: ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $
          bind "l" (ref withGraphContextDef @@ (ref ExtractCore.literalDef @@ var "term")) $
          Flows.map (unaryFunction $ Core.termLiteral) (ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ var "ad") @@ var "l"))] $
        Flows.pure $ Compute.adapter
          (Compute.adapterIsLossy $ var "ad")
          (Core.typeLiteral $ Compute.adapterSource $ var "ad")
          (Core.typeLiteral $ Compute.adapterTarget $ var "ad")
          (var "step")]
  
  passListDef :: TBinding TypeAdapter
  passListDef = define "passList" $
    doc "Pass through list types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_list>>: lambda "lt" $
        bind "ad" (ref termAdapterDef @@ var "lt") $
        Flows.pure $ Compute.adapter
          (Compute.adapterIsLossy $ var "ad")
          (var "t")
          (TTypes.list $ Compute.adapterTarget $ var "ad")
          (ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $ cases _Term (var "term") Nothing [
            _Term_list>>: lambda "terms" $
              bind "newTerms" (Flows.mapList (ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ var "ad")) (var "terms")) $
              Flows.pure $ Core.termList $ var "newTerms"]))]
  
  passMapDef :: TBinding TypeAdapter
  passMapDef = define "passMap" $
    doc "Pass through map types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_map>>: lambda "mt" $ lets [
          "kt">: Core.mapTypeKeys $ var "mt",
          "vt">: Core.mapTypeValues $ var "mt"] $
            bind "kad" (ref termAdapterDef @@ var "kt") $
            bind "vad" (ref termAdapterDef @@ var "vt") $
            Flows.pure $ Compute.adapter
              (Logic.or (Compute.adapterIsLossy $ var "kad") (Compute.adapterIsLossy $ var "vad"))
              (var "t")
              (TTypes.map (Compute.adapterTarget $ var "kad") (Compute.adapterTarget $ var "vad"))
              (ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $ cases _Term (var "term") Nothing [
                _Term_map>>: lambda "m" $
                  bind "newPairs" (Flows.mapList
                    (lambda "pair" $ lets [
                      "k">: first $ var "pair",
                      "v">: second $ var "pair"] $
                        bind "newK" (ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ var "kad") @@ var "k") $
                        bind "newV" (ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ var "vad") @@ var "v") $
                        Flows.pure $ pair (var "newK") (var "newV"))
                    (Maps.toList $ var "m")) $
                  Flows.pure $ Core.termMap $ Maps.fromList $ var "newPairs"]))]
  
  passOptionalDef :: TBinding TypeAdapter
  passOptionalDef = define "passOptional" $
    doc "Pass through optional types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_optional>>: lambda "ot" $ lets [
        "mapTerm">: lambdas ["coder", "dir", "term"] $
          bind "opt" (ref withGraphContextDef @@ (ref ExtractCore.optionalDef @@ unaryFunction Flows.pure @@ var "term")) $
          bind "newOpt" (Flows.mapOptional (ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ var "coder") (var "opt")) $
          Flows.pure $ Core.termOptional $ var "newOpt"] $
        bind "adapter" (ref termAdapterDef @@ var "ot") $
          Flows.pure $ Compute.adapter
            (Compute.adapterIsLossy $ var "adapter")
            (var "t")
            (Core.typeOptional $ Compute.adapterTarget $ var "adapter")
            (ref AdaptUtils.bidirectionalDef @@ (var "mapTerm" @@ (Compute.adapterCoder $ var "adapter")))]
  
  passProductDef :: TBinding TypeAdapter
  passProductDef = define "passProduct" $
    doc "Pass through product types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_product>>: lambda "types" $
        Flows.bind (Flows.mapList (ref termAdapterDef) (var "types")) $ lambda "ads" $ lets [
          "lossy">: Logic.ors $ Lists.map (unaryFunction Compute.adapterIsLossy) (var "ads")] $
          Flows.pure $ Compute.adapter
            (var "lossy")
            (var "t")
            (Core.typeProduct $ Lists.map (unaryFunction Compute.adapterTarget) (var "ads"))
            (ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $ cases _Term (var "term") Nothing [
              _Term_product>>: lambda "tuple" $
                bind "newTuple" (Flows.sequence $ Lists.zipWith
                  (lambdas ["term", "ad"] $ ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ var "ad") @@ var "term")
                  (var "tuple")
                  (var "ads")) $ Flows.pure $ Core.termProduct $ var "newTuple"]))]
  
  passRecordDef :: TBinding TypeAdapter
  passRecordDef = define "passRecord" $
    doc "Pass through record types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_record>>: lambda "rt" $
        bind "adapters" (Flows.mapList (ref fieldAdapterDef) (Core.rowTypeFields $ var "rt")) $ lets [
          "lossy">: Logic.ors $ Lists.map (unaryFunction Compute.adapterIsLossy) (var "adapters"),
          "sfields'">: Lists.map (unaryFunction Compute.adapterTarget) (var "adapters")] $
          Flows.pure $ Compute.adapter
            (var "lossy")
            (var "t")
            (Core.typeRecord $ Core.rowType (Core.rowTypeTypeName $ var "rt") (var "sfields'"))
            (ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $ cases _Term (var "term") Nothing [
              _Term_record>>: lambda "rec" $ lets [
                "dfields">: Core.recordFields $ var "rec"] $
                bind "newFields" (Flows.sequence $ Lists.zipWith
                  (lambdas ["ad", "f"] $ ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ var "ad") @@ var "f" )
                  (var "adapters")
                  (var "dfields")) $
                  Flows.pure $ Core.termRecord $ Core.record (Core.rowTypeTypeName $ var "rt") (var "newFields")]))]
  
  passSetDef :: TBinding TypeAdapter
  passSetDef = define "passSet" $
    doc "Pass through set types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_set>>: lambda "st" $
        Flows.bind (ref termAdapterDef @@ var "st") $ lambda "ad" $
          Flows.pure $ Compute.adapter
            (Compute.adapterIsLossy $ var "ad")
            (var "t")
            (TTypes.set $ Compute.adapterTarget $ var "ad")
            (ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $ cases _Term (var "term") Nothing [
              _Term_set>>: lambda "terms" $
                bind "newTerms" (Flows.mapList (ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ var "ad")) (Sets.toList $ var "terms")) $
                Flows.pure $ Core.termSet $ Sets.fromList $ var "newTerms"]))]
  
  passSumDef :: TBinding TypeAdapter
  passSumDef = define "passSum" $
    doc "Pass through sum types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_sum>>: lambda "types" $
        Flows.bind (Flows.mapList (ref termAdapterDef) (var "types")) $ lambda "ads" $ lets [
          "lossy">: Logic.ors $ Lists.map (unaryFunction Compute.adapterIsLossy) (var "ads")] $
          Flows.pure $ Compute.adapter
            (var "lossy")
            (var "t")
            (Core.typeSum $ Lists.map (unaryFunction Compute.adapterTarget) (var "ads"))
            (ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $ cases _Term (var "term") Nothing [
              _Term_sum>>: lambda "s" $ lets [
                  "i">: Core.sumIndex $ var "s",
                  "n">: Core.sumSize $ var "s",
                  "term">: Core.sumTerm $ var "s"] $
                    bind "newTerm" (ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ Lists.at (var "i") (var "ads")) @@ var "term") $
                      Flows.pure $ Core.termSum $ Core.sum (var "i") (var "n") (var "newTerm")]))]
  
  passUnionDef :: TBinding TypeAdapter
  passUnionDef = define "passUnion" $
    doc "Pass through union types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_union>>: lambda "rt" $ lets [
        "sfields">: Core.rowTypeFields $ var "rt",
        "tname">: Core.rowTypeTypeName $ var "rt",
        "getAdapter">: lambdas ["adaptersMap", "f"] $
          Optionals.maybe
            (Flows.fail $ Strings.cat2 (string "no such field: ") (unwrap _Name @@ (Core.fieldName $ var "f")))
            (unaryFunction Flows.pure)
            (Maps.lookup (Core.fieldName $ var "f") (var "adaptersMap"))] $
        bind "adapters" (Flows.mapList
            (lambda "f" $ Flows.bind (ref fieldAdapterDef @@ var "f") $ lambda "ad" $
              Flows.pure $ pair (Core.fieldTypeName $ var "f") (var "ad"))
            (var "sfields")) $ lets [
            "adaptersMap">: Maps.fromList $ var "adapters",
            "lossy">: Logic.ors $ Lists.map (lambda "pair" $ Compute.adapterIsLossy $ second $ var "pair") (var "adapters"),
            "sfields'">: Lists.map (lambda "pair" $ Compute.adapterTarget $ second $ var "pair") (var "adapters")] $
          Flows.pure $ Compute.adapter
            (var "lossy")
            (var "t")
            (Core.typeUnion $ Core.rowType (var "tname") (var "sfields'"))
            (ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $
              -- Note: this is a shortcut, since we anticipate deprecating the current term adapter logic
              produce $ var "term"))]
            -- TODO: consider restoring the following
  --          (ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $
  --            "dfield" <<~ ref withGraphContextDef @@ (ref ExtractCore.injectionDef @@ var "tname" @@ var "term") $
  --            "ad" <<~ var "getAdapter" @@ var "adaptersMap" @@ var "dfield" $
  --            "newField" <<~ ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ var "ad") @@ var "dfield" $
  --            produce $ Core.termUnion $ Core.injection (var "tname") (var "newField")))]
  
  passUnitDef :: TBinding TypeAdapter
  passUnitDef = define "passUnit" $
    doc "Pass through unit types" $
    constant $ Flows.pure $ Compute.adapter false Core.typeUnit Core.typeUnit $
      Compute.coder
        (constant $ Flows.pure Core.termUnit)
        (constant $ Flows.pure Core.termUnit)
  
  passWrappedDef :: TBinding TypeAdapter
  passWrappedDef = define "passWrapped" $
    doc "Pass through wrapped types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_wrap>>: lambda "wt" $ lets [
          "tname">: Core.wrappedTypeTypeName $ var "wt",
          "ot">: Core.wrappedTypeObject $ var "wt",
          "mapTerm">: lambdas ["coder", "dir", "term"] $
            bind "unwrapped" (ref withGraphContextDef @@ (ref ExtractCore.wrapDef @@ var "tname" @@ var "term")) $
            bind "newTerm" (ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ var "coder" @@ var "unwrapped") $
            Flows.pure $ Core.termWrap $ Core.wrappedTerm (var "tname") (var "newTerm")] $
          bind "adapter" (ref termAdapterDef @@ var "ot") $
            Flows.pure $ Compute.adapter
              (Compute.adapterIsLossy $ var "adapter")
              (var "t")
              (Core.typeWrap $ Core.wrappedType (var "tname") (Compute.adapterTarget $ var "adapter"))
              (ref AdaptUtils.bidirectionalDef @@ (var "mapTerm" @@ (Compute.adapterCoder $ var "adapter")))]
  
  setToListDef :: TBinding TypeAdapter
  setToListDef = define "setToList" $
    doc "Convert set types to list types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_set>>: lambda "st" $ lets [
        "encode">: lambda "ad" $ lambda "term" $ cases _Term (var "term") Nothing [
          _Term_set>>: lambda "s" $ Compute.coderEncode (Compute.adapterCoder $ var "ad") @@ (Core.termList $ Sets.toList $ var "s")],
        "decode">:
          lambdas ["ad", "term"] $
          bind "listTerm" (Compute.coderDecode (Compute.adapterCoder $ var "ad") @@ var "term") $
            cases _Term (var "listTerm") Nothing [
              _Term_list>>: lambda "l" $ Flows.pure $ Core.termSet $ Sets.fromList $ var "l"]] $
        bind "ad" (ref termAdapterDef @@ (TTypes.list $ var "st")) $
        Flows.pure $ Compute.adapter
          (Compute.adapterIsLossy $ var "ad")
          (var "t")
          (Compute.adapterTarget $ var "ad")
          (Compute.coder (var "encode" @@ var "ad") (var "decode" @@ var "ad"))]
  
  simplifyApplicationDef :: TBinding TypeAdapter
  simplifyApplicationDef = define "simplifyApplication" $
    doc "Simplify application types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_application>>: lambda "at" $ lets [
          "lhs">: Core.applicationTypeFunction $ var "at"] $
          bind "ad" (ref termAdapterDef @@ var "lhs") $
            Flows.pure $ Compute.adapter
              false
              (var "t")
              (Compute.adapterTarget $ var "ad")
              (ref AdaptUtils.bidirectionalDef @@ (lambdas ["dir", "term"] $
                ref AdaptUtils.encodeDecodeDef @@ var "dir" @@ (Compute.adapterCoder $ var "ad") @@ var "term"))]
  
  unitToRecordDef :: TBinding TypeAdapter
  unitToRecordDef = define "unitToRecord" $
      doc "Convert unit terms to records" $
      constant $ Flows.pure $
        Compute.adapter false Core.typeUnit (Core.typeRecord $ Core.rowType unitName $ list []) $
          Compute.coder
            (constant $ Flows.pure $ Core.termRecord $ Core.record unitName $ list [])
            (constant $ Flows.pure Core.termUnit)
    where
      unitName = Core.name $ string "_Unit"
  
  unionToRecordDef :: TBinding TypeAdapter
  unionToRecordDef = define "unionToRecord" $
    doc "Convert union types to record types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_union>>: lambda "rt" $ lets [
        "nm">: Core.rowTypeTypeName $ var "rt",
        "sfields">: Core.rowTypeFields $ var "rt",
        "target">: Core.typeRecord $ ref unionTypeToRecordTypeDef @@ var "rt",
        "toRecordField">: lambdas ["term", "fn", "f"] $ lets [
            "fn'">: Core.fieldTypeName $ var "f"] $
            Core.field (var "fn'") $ Core.termOptional $ Logic.ifElse
              (Equality.equal (var "fn'") (var "fn"))
              (just $ var "term")
              nothing,
        "fromRecordFields">: lambdas ["term", "term'", "t'", "fields"] $ lets [
          "matches">: Optionals.mapMaybe
            (lambda "field" $ lets [
                "fn">: Core.fieldName $ var "field",
                "fterm">: Core.fieldTerm $ var "field"] $
                cases _Term (var "fterm") Nothing [
                  _Term_optional>>: lambda "opt" $ Optionals.bind (var "opt") $ lambda "t" $
                    just $ Core.field (var "fn") (var "t")])
            (var "fields")] $
          Logic.ifElse (Lists.null $ var "matches")
            (Flows.fail $ Strings.cat $ list [
              string "cannot convert term back to union: ",
              ref ShowCore.termDef @@ var "term",
              string " where type = ",
              ref ShowCore.typeDef @@ var "t",
              string "    and target type = ",
              ref ShowCore.typeDef @@ var "t'"])
            (Flows.pure $ Lists.head $ var "matches")] $
        bind "ad" (ref termAdapterDef @@ var "target") $
        Flows.pure $ Compute.adapter
          (Compute.adapterIsLossy $ var "ad")
          (var "t")
          (Compute.adapterTarget $ var "ad")
          (Compute.coder
            (lambda "term'" $
              bind "field" (ref withGraphContextDef @@ (ref ExtractCore.injectionDef @@ (Core.rowTypeTypeName $ var "rt") @@ var "term'")) $ lets [
                "fn">: Core.fieldName $ var "field",
                "term">: Core.fieldTerm $ var "field"] $
              Compute.coderEncode (Compute.adapterCoder $ var "ad") @@
                (Core.termRecord $ Core.record (var "nm") $ Lists.map (var "toRecordField" @@ var "term" @@ var "fn") (var "sfields")))
            (lambda "term" $
              bind "recTerm" (Compute.coderDecode (Compute.adapterCoder $ var "ad") @@ var "term") $
                cases _Term (var "recTerm") Nothing [
                  _Term_record>>: lambda "rec" $ lets [
                    "fields">: Core.recordFields $ var "rec"] $
                    bind "resultField"
                      (var "fromRecordFields"
                        @@ var "term"
                        @@ (Core.termRecord $ Core.record (var "nm") (var "fields"))
                        @@ (Compute.adapterTarget $ var "ad")
                        @@ var "fields") $
                    Flows.pure $ Core.termUnion $ Core.injection (var "nm") (var "resultField")]))]
  
  unionTypeToRecordTypeDef :: TBinding (RowType -> RowType)
  unionTypeToRecordTypeDef = define "unionTypeToRecordType" $
    doc "Convert a union row type to a record row type" $
    lambda "rt" $ lets [
      "makeOptional">: lambda "f" $ lets [
          "fn">: Core.fieldTypeName $ var "f",
          "ft">: Core.fieldTypeType $ var "f"] $
          Core.fieldType (var "fn") $ ref Rewriting.mapBeneathTypeAnnotationsDef @@ unaryFunction Core.typeOptional @@ var "ft"] $
      Core.rowType (Core.rowTypeTypeName $ var "rt") $ Lists.map (var "makeOptional") (Core.rowTypeFields $ var "rt")
  
  wrapToUnwrappedDef :: TBinding TypeAdapter
  wrapToUnwrappedDef = define "wrapToUnwrapped" $
    doc "Convert wrapped types to unwrapped types" $
    lambda "t" $ cases _Type (var "t") Nothing [
      _Type_wrap>>: lambda "wt" $ lets [
          "tname">: Core.wrappedTypeTypeName $ var "wt",
          "typ">: Core.wrappedTypeObject $ var "wt",
          "encode">: lambda "ad" $ lambda "term" $
            bind "unwrapped" (ref withGraphContextDef @@ (ref ExtractCore.wrapDef @@ var "tname" @@ var "term")) $
            Compute.coderEncode (Compute.adapterCoder $ var "ad") @@ var "unwrapped",
          "decode">: lambda "ad" $ lambda "term" $
            bind "decoded" (Compute.coderDecode (Compute.adapterCoder $ var "ad") @@ var "term") $
            Flows.pure $ Core.termWrap $ Core.wrappedTerm (var "tname") (var "decoded")] $
          bind "ad" (ref termAdapterDef @@ var "typ") $
            Flows.pure $ Compute.adapter
              false
              (var "t")
              (Compute.adapterTarget $ var "ad")
              (Compute.coder (var "encode" @@ var "ad") (var "decode" @@ var "ad"))]
  
  -- Note: those constructors which cannot be mapped meaningfully at this time are simply
  --       preserved as strings.
  termAdapterDef :: TBinding TypeAdapter
  termAdapterDef = define "termAdapter" $
    doc "Create an adapter for any type" $
    "typ" ~> lets [
      "constraints">: "cx" ~> Coders.languageConstraintsProjection $ Coders.adapterContextLanguage $ var "cx",
      "supported">: "cx" ~> ref AdaptUtils.typeIsSupportedDef @@ (var "constraints" @@ var "cx"),
      "variantIsSupported">: "cx" ~> "t" ~>
        Sets.member (ref Variants.typeVariantDef @@ var "t") $ Coders.languageConstraintsTypeVariants $ var "constraints" @@ var "cx",
      "supportedAtTopLevel">: "cx" ~> "t" ~> Logic.and
        (var "variantIsSupported" @@ var "cx" @@ var "t")
        (Coders.languageConstraintsTypes (var "constraints" @@ var "cx") @@ var "t"),
      "pass">: "t" ~> cases _TypeVariant (ref Variants.typeVariantDef @@ (ref Rewriting.deannotateTypeDef @@ var "t")) Nothing [
        _TypeVariant_application>>: constant $ list [ref passApplicationDef],
        _TypeVariant_forall>>: constant $ list [ref passForallDef],
        _TypeVariant_function>>: constant $ list [ref passFunctionDef],
        _TypeVariant_list>>: constant $ list [ref passListDef],
        _TypeVariant_literal>>: constant $ list [ref passLiteralDef],
        _TypeVariant_map>>: constant $ list [ref passMapDef],
        _TypeVariant_optional>>: constant $ list [ref passOptionalDef, ref optionalToListDef],
        _TypeVariant_product>>: constant $ list [ref passProductDef],
        _TypeVariant_record>>: constant $ list [ref passRecordDef],
        _TypeVariant_set>>: constant $ list [ref passSetDef],
        _TypeVariant_sum>>: constant $ list [ref passSumDef],
        _TypeVariant_union>>: constant $ list [ref passUnionDef],
        _TypeVariant_unit>>: constant $ list [ref passUnitDef],
        _TypeVariant_wrap>>: constant $ list [ref passWrappedDef]],
      "trySubstitution">: "t" ~> cases _TypeVariant (ref Variants.typeVariantDef @@ var "t")
        Nothing [
        _TypeVariant_application>>: constant $ list [ref simplifyApplicationDef],
        _TypeVariant_function>>: constant $ list [ref functionToUnionDef],
        _TypeVariant_forall>>: constant $ list [ref lambdaToMonotypeDef],
        _TypeVariant_optional>>: constant $ list [ref optionalToListDef],
        _TypeVariant_set>>: constant $ list [ref setToListDef],
        _TypeVariant_union>>: constant $ list [ref unionToRecordDef],
        _TypeVariant_unit>>: constant $ list [ref unitToRecordDef],
        _TypeVariant_wrap>>: constant $ list [ref wrapToUnwrappedDef]],
      "alts">: "cx" ~> "t" ~> Flows.mapList ("c" ~> var "c" @@ var "t") $
         Logic.ifElse (var "supportedAtTopLevel" @@ var "cx" @@ var "t")
           (var "pass" @@ var "t")
           (var "trySubstitution" @@ var "t")] $
      cases _Type (var "typ")
        (Just $
          trace (Strings.cat2 (string "adapter for ") (ref DescribeCore.typeDef @@ var "typ")) $
          cases _Type (var "typ")
            (Just $
              bind "cx" (ref Monads.getStateDef) $
              ref AdaptUtils.chooseAdapterDef
                @@ (var "alts" @@ var "cx")
                @@ (var "supported" @@ var "cx")
                @@ ref ShowCore.typeDef
                @@ (ref DescribeCore.typeDef)
                @@ (var "typ")) [
            -- Account for let-bound variables
            _Type_variable>>: "name" ~> ref forTypeReferenceDef @@ var "name"]) [
        _Type_annotated>>: "at" ~>
          bind "ad" (ref termAdapterDef @@ Core.annotatedTypeSubject (var "at")) $
          Flows.pure (Compute.adapterWithTarget (var "ad") $
            Core.typeAnnotated $ Core.annotatedType (Compute.adapterTarget $ var "ad") (Core.annotatedTypeAnnotation $ var "at"))]
  
  withGraphContextDef :: TBinding (Flow Graph a -> Flow AdapterContext a)
  withGraphContextDef = define "withGraphContext" $
    doc "Execute a flow with graph context" $
    "f" ~>
    "cx" <<~ ref Monads.getStateDef $
    ref Monads.withStateDef @@ (Coders.adapterContextGraph $ var "cx") @@ var "f"
  