Substitution.hs

-- Note: this is an automatically generated file. Do not edit.
-- | Variable substitution in type and term expressions.

module Hydra.Substitution where
import qualified Hydra.Ast as Ast
import qualified Hydra.Coders as Coders
import qualified Hydra.Core as Core
import qualified Hydra.Error.Checking as Checking
import qualified Hydra.Error.Core as ErrorCore
import qualified Hydra.Error.Packaging as ErrorPackaging
import qualified Hydra.Errors as Errors
import qualified Hydra.Graph as Graph
import qualified Hydra.Json.Model as Model
import qualified Hydra.Haskell.Lib.Lists as Lists
import qualified Hydra.Haskell.Lib.Logic as Logic
import qualified Hydra.Haskell.Lib.Maps as Maps
import qualified Hydra.Haskell.Lib.Optionals as Optionals
import qualified Hydra.Haskell.Lib.Pairs as Pairs
import qualified Hydra.Haskell.Lib.Sets as Sets
import qualified Hydra.Packaging as Packaging
import qualified Hydra.Parsing as Parsing
import qualified Hydra.Paths as Paths
import qualified Hydra.Query as Query
import qualified Hydra.Relational as Relational
import qualified Hydra.Rewriting as Rewriting
import qualified Hydra.Tabular as Tabular
import qualified Hydra.Testing as Testing
import qualified Hydra.Topology as Topology
import qualified Hydra.Typed as Typed
import qualified Hydra.Typing as Typing
import qualified Hydra.Util as Util
import qualified Hydra.Validation as Validation
import qualified Hydra.Variables as Variables
import qualified Hydra.Variants as Variants
import Prelude hiding  (Enum, Ordering, decodeFloat, encodeFloat, fail, map, pure, sum)
import qualified Data.Scientific as Sci
import qualified Data.Map as M
-- | Compose two type substitutions
composeTypeSubst :: Typing.TypeSubst -> Typing.TypeSubst -> Typing.TypeSubst
composeTypeSubst s1 s2 =
    Logic.ifElse (Maps.null (Typing.unTypeSubst s1)) s2 (Logic.ifElse (Maps.null (Typing.unTypeSubst s2)) s1 (composeTypeSubstNonEmpty s1 s2))
-- | Compose a list of type substitutions
composeTypeSubstList :: [Typing.TypeSubst] -> Typing.TypeSubst
composeTypeSubstList = Lists.foldl composeTypeSubst idTypeSubst
-- | Compose two non-empty type substitutions (internal helper)
composeTypeSubstNonEmpty :: Typing.TypeSubst -> Typing.TypeSubst -> Typing.TypeSubst
composeTypeSubstNonEmpty s1 s2 =

      let isExtra = \k -> \v -> Optionals.isNone (Maps.lookup k (Typing.unTypeSubst s1))
          withExtra = Maps.filterWithKey isExtra (Typing.unTypeSubst s2)
      in (Typing.TypeSubst (Maps.union withExtra (Maps.map (substInType s2) (Typing.unTypeSubst s1))))
-- | The identity type substitution
idTypeSubst :: Typing.TypeSubst
idTypeSubst = Typing.TypeSubst Maps.empty
-- | Create a type substitution with a single variable mapping
singletonTypeSubst :: Core.Name -> Core.Type -> Typing.TypeSubst
singletonTypeSubst v t = Typing.TypeSubst (Maps.singleton v t)
-- | Apply a type substitution to class constraints, propagating to free variables
substInClassConstraints :: Typing.TypeSubst -> M.Map Core.Name Core.TypeVariableConstraints -> M.Map Core.Name Core.TypeVariableConstraints
substInClassConstraints subst constraints =

      let substMap = Typing.unTypeSubst subst
          insertOrMerge =
                  \varName -> \metadata -> \acc -> Optionals.cases (Maps.lookup varName acc) (Maps.insert varName metadata acc) (\existing ->
                    let merged =
                            Core.TypeVariableConstraints {
                              Core.typeVariableConstraintsClasses = (Lists.nub (Lists.concat2 (Core.typeVariableConstraintsClasses existing) (Core.typeVariableConstraintsClasses metadata)))}
                    in (Maps.insert varName merged acc))
      in (Lists.foldl (\acc -> \pair ->
        let varName = Pairs.first pair
            metadata = Pairs.second pair
        in (Optionals.cases (Maps.lookup varName substMap) (insertOrMerge varName metadata acc) (\targetType ->
          let freeVars = Sets.toList (Variables.freeVariablesInType targetType)
          in (Lists.foldl (\acc2 -> \freeVar -> insertOrMerge freeVar metadata acc2) acc freeVars)))) Maps.empty (Maps.toList constraints))
-- | Apply a type substitution to a graph's bound types and class constraints
substInContext :: Typing.TypeSubst -> Graph.Graph -> Graph.Graph
substInContext subst cx =

      let newBoundTypes = Maps.map (substInTypeScheme subst) (Graph.graphBoundTypes cx)
          newClassConstraints = substInClassConstraints subst (Graph.graphClassConstraints cx)
          cx2 =
                  Graph.Graph {
                    Graph.graphBoundTerms = (Graph.graphBoundTerms cx),
                    Graph.graphBoundTypes = newBoundTypes,
                    Graph.graphClassConstraints = (Graph.graphClassConstraints cx),
                    Graph.graphLambdaVariables = (Graph.graphLambdaVariables cx),
                    Graph.graphMetadata = (Graph.graphMetadata cx),
                    Graph.graphPrimitives = (Graph.graphPrimitives cx),
                    Graph.graphSchemaTypes = (Graph.graphSchemaTypes cx),
                    Graph.graphTypeVariables = (Graph.graphTypeVariables cx)}
      in Graph.Graph {
        Graph.graphBoundTerms = (Graph.graphBoundTerms cx2),
        Graph.graphBoundTypes = (Graph.graphBoundTypes cx2),
        Graph.graphClassConstraints = newClassConstraints,
        Graph.graphLambdaVariables = (Graph.graphLambdaVariables cx2),
        Graph.graphMetadata = (Graph.graphMetadata cx2),
        Graph.graphPrimitives = (Graph.graphPrimitives cx2),
        Graph.graphSchemaTypes = (Graph.graphSchemaTypes cx2),
        Graph.graphTypeVariables = (Graph.graphTypeVariables cx2)}
-- | Apply a type substitution to a type
substInType :: Typing.TypeSubst -> Core.Type -> Core.Type
substInType subst typ0 = Logic.ifElse (Maps.null (Typing.unTypeSubst subst)) typ0 (substInTypeNonEmpty subst typ0)
-- | Apply a non-empty type substitution to a type (internal helper)
substInTypeNonEmpty :: Typing.TypeSubst -> Core.Type -> Core.Type
substInTypeNonEmpty subst typ0 =

      let rewrite =
              \recurse -> \typ -> case typ of
                Core.TypeForall v0 -> Optionals.cases (Maps.lookup (Core.forallTypeParameter v0) (Typing.unTypeSubst subst)) (recurse typ) (\styp -> Core.TypeForall (Core.ForallType {
                  Core.forallTypeParameter = (Core.forallTypeParameter v0),
                  Core.forallTypeBody = (substInType (removeVar (Core.forallTypeParameter v0)) (Core.forallTypeBody v0))}))
                Core.TypeVariable v0 -> Optionals.cases (Maps.lookup v0 (Typing.unTypeSubst subst)) typ (\styp -> styp)
                _ -> recurse typ
          removeVar = \v -> Typing.TypeSubst (Maps.delete v (Typing.unTypeSubst subst))
      in (Rewriting.rewriteType rewrite typ0)
-- | Apply a type substitution to a type scheme. The scheme's quantifier variables shadow the substitution: any name in typeSchemeVariables is removed from subst before substituting into the body and constraints. Without this, a substitution like {t0 -> Foo} applied to `forall [t0]. t0 -> t0` would incorrectly replace the bound t0.
substInTypeScheme :: Typing.TypeSubst -> Core.TypeScheme -> Core.TypeScheme
substInTypeScheme subst ts =

      let scopedSubst =
              Typing.TypeSubst (Lists.foldl (\m -> \v -> Maps.delete v m) (Typing.unTypeSubst subst) (Core.typeSchemeVariables ts))
      in Core.TypeScheme {
        Core.typeSchemeVariables = (Core.typeSchemeVariables ts),
        Core.typeSchemeBody = (substInType scopedSubst (Core.typeSchemeBody ts)),
        Core.typeSchemeConstraints = (Optionals.map (substInClassConstraints scopedSubst) (Core.typeSchemeConstraints ts))}
-- | Apply a type substitution to the type annotations within a term
substTypesInTerm :: Typing.TypeSubst -> Core.Term -> Core.Term
substTypesInTerm subst term0 =

      let rewrite =
              \recurse -> \term ->
                let dflt = recurse term
                    forLambda =
                            \l -> Core.TermLambda (Core.Lambda {
                              Core.lambdaParameter = (Core.lambdaParameter l),
                              Core.lambdaDomain = (Optionals.map (substInType subst) (Core.lambdaDomain l)),
                              Core.lambdaBody = (substTypesInTerm subst (Core.lambdaBody l))})
                    forLet =
                            \l ->
                              let rewriteBinding =
                                      \b -> Core.Binding {
                                        Core.bindingName = (Core.bindingName b),
                                        Core.bindingTerm = (substTypesInTerm subst (Core.bindingTerm b)),
                                        Core.bindingTypeScheme = (Optionals.map (substInTypeScheme subst) (Core.bindingTypeScheme b))}
                              in (Core.TermLet (Core.Let {
                                Core.letBindings = (Lists.map rewriteBinding (Core.letBindings l)),
                                Core.letBody = (substTypesInTerm subst (Core.letBody l))}))
                    forTypeApplication =
                            \tt -> Core.TermTypeApplication (Core.TypeApplicationTerm {
                              Core.typeApplicationTermBody = (substTypesInTerm subst (Core.typeApplicationTermBody tt)),
                              Core.typeApplicationTermType = (substInType subst (Core.typeApplicationTermType tt))})
                    forTypeLambda =
                            \ta ->
                              let param = Core.typeLambdaParameter ta
                                  subst2 = Typing.TypeSubst (Maps.delete param (Typing.unTypeSubst subst))
                              in (Core.TermTypeLambda (Core.TypeLambda {
                                Core.typeLambdaParameter = param,
                                Core.typeLambdaBody = (substTypesInTerm subst2 (Core.typeLambdaBody ta))}))
                in case term of
                  Core.TermLambda v0 -> forLambda v0
                  Core.TermLet v0 -> forLet v0
                  Core.TermTypeApplication v0 -> forTypeApplication v0
                  Core.TermTypeLambda v0 -> forTypeLambda v0
                  _ -> dflt
      in (Rewriting.rewriteTerm rewrite term0)
-- | Apply a term substitution to a binding
substituteInBinding :: Typing.TermSubst -> Core.Binding -> Core.Binding
substituteInBinding subst b =
    Core.Binding {
      Core.bindingName = (Core.bindingName b),
      Core.bindingTerm = (substituteInTerm subst (Core.bindingTerm b)),
      Core.bindingTypeScheme = (Core.bindingTypeScheme b)}
-- | Apply a type substitution to a type constraint
substituteInConstraint :: Typing.TypeSubst -> Typing.TypeConstraint -> Typing.TypeConstraint
substituteInConstraint subst c =
    Typing.TypeConstraint {
      Typing.typeConstraintLeft = (substInType subst (Typing.typeConstraintLeft c)),
      Typing.typeConstraintRight = (substInType subst (Typing.typeConstraintRight c)),
      Typing.typeConstraintComment = (Typing.typeConstraintComment c)}
-- | Apply a type substitution to a list of type constraints
substituteInConstraints :: Typing.TypeSubst -> [Typing.TypeConstraint] -> [Typing.TypeConstraint]
substituteInConstraints subst cs = Lists.map (substituteInConstraint subst) cs
-- | Apply a term substitution to a term
substituteInTerm :: Typing.TermSubst -> Core.Term -> Core.Term
substituteInTerm subst term0 =

      let s = Typing.unTermSubst subst
          rewrite =
                  \recurse -> \term ->
                    let withLambda =
                            \l ->
                              let v = Core.lambdaParameter l
                                  subst2 = Typing.TermSubst (Maps.delete v s)
                              in (Core.TermLambda (Core.Lambda {
                                Core.lambdaParameter = v,
                                Core.lambdaDomain = (Core.lambdaDomain l),
                                Core.lambdaBody = (substituteInTerm subst2 (Core.lambdaBody l))}))
                        withLet =
                                \lt ->
                                  let bindings = Core.letBindings lt
                                      names = Sets.fromList (Lists.map Core.bindingName bindings)
                                      subst2 = Typing.TermSubst (Maps.filterWithKey (\k -> \v -> Logic.not (Sets.member k names)) s)
                                      rewriteBinding =
                                              \b -> Core.Binding {
                                                Core.bindingName = (Core.bindingName b),
                                                Core.bindingTerm = (substituteInTerm subst2 (Core.bindingTerm b)),
                                                Core.bindingTypeScheme = (Core.bindingTypeScheme b)}
                                  in (Core.TermLet (Core.Let {
                                    Core.letBindings = (Lists.map rewriteBinding bindings),
                                    Core.letBody = (substituteInTerm subst2 (Core.letBody lt))}))
                    in case term of
                      Core.TermLambda v0 -> withLambda v0
                      Core.TermLet v0 -> withLet v0
                      Core.TermVariable v0 -> Optionals.cases (Maps.lookup v0 s) (recurse term) (\sterm -> sterm)
                      _ -> recurse term
      in (Rewriting.rewriteTerm rewrite term0)