Environment.hs

-- Note: this is an automatically generated file. Do not edit.

-- | Graph to type environment conversions

module Hydra.Environment where

import qualified Hydra.Ast as Ast
import qualified Hydra.Coders as Coders
import qualified Hydra.Core as Core
import qualified Hydra.Decode.Core as DecodeCore
import qualified Hydra.Docs as Docs
import qualified Hydra.Encode.Core as EncodeCore
import qualified Hydra.Error.Checking as Checking
import qualified Hydra.Error.Core as ErrorCore
import qualified Hydra.Error.File as ErrorFile
import qualified Hydra.Error.Packaging as ErrorPackaging
import qualified Hydra.Error.System as ErrorSystem
import qualified Hydra.Errors as Errors
import qualified Hydra.File as File
import qualified Hydra.Graph as Graph
import qualified Hydra.Json.Model as Model
import qualified Hydra.Lexical as Lexical
import qualified Hydra.Overlay.Haskell.Lib.Eithers as Eithers
import qualified Hydra.Overlay.Haskell.Lib.Equality as Equality
import qualified Hydra.Overlay.Haskell.Lib.Lists as Lists
import qualified Hydra.Overlay.Haskell.Lib.Logic as Logic
import qualified Hydra.Overlay.Haskell.Lib.Maps as Maps
import qualified Hydra.Overlay.Haskell.Lib.Optionals as Optionals
import qualified Hydra.Overlay.Haskell.Lib.Pairs as Pairs
import qualified Hydra.Overlay.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.Scoping as Scoping
import qualified Hydra.Sorting as Sorting
import qualified Hydra.Strip as Strip
import qualified Hydra.System as System
import qualified Hydra.Tabular as Tabular
import qualified Hydra.Testing as Testing
import qualified Hydra.Time as Time
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

-- | Convert a definition to a typed term
definitionAsTypeApplicationTerm :: Core.Binding -> Either Errors.Error Core.TypeApplicationTerm
definitionAsTypeApplicationTerm el =
    Optionals.cases (Core.bindingTypeScheme el) (Left (Errors.ErrorExtraction (Errors.ExtractionErrorUnexpectedShape (Errors.UnexpectedShapeError {
      Errors.unexpectedShapeErrorExpected = "typed binding",
      Errors.unexpectedShapeErrorActual = "untyped binding"})))) (\ts -> Right (Core.TypeApplicationTerm {
      Core.typeApplicationTermBody = (Core.bindingTerm el),
      Core.typeApplicationTermType = (Core.typeSchemeBody ts)}))

-- | Convert bindings and a body to a let expression
graphAsLet :: [Core.Binding] -> Core.Term -> Core.Let
graphAsLet bindings body =
    Core.Let {
      Core.letBindings = bindings,
      Core.letBody = body}

-- | Convert bindings and a body to a term, using let-term duality
graphAsTerm :: [Core.Binding] -> Core.Term -> Core.Term
graphAsTerm bindings body = Core.TermLet (graphAsLet bindings body)

-- | Decode a list of type-encoding bindings into a map of named types
graphAsTypes :: Graph.Graph -> [Core.Binding] -> Either Errors.DecodingError (M.Map Core.Name Core.Type)
graphAsTypes graph els =

      let toPair = \el -> Eithers.map (\typ -> (Core.bindingName el, typ)) (DecodeCore.type_ graph (Core.bindingTerm el))
      in (Eithers.map Maps.fromList (Eithers.mapList toPair els))

-- | Partition a list of definitions into type definitions and term definitions
partitionDefinitions :: [Packaging.Definition] -> ([Packaging.TypeDefinition], [Packaging.TermDefinition])
partitionDefinitions defs =

      let getType =
              \def -> case def of
                Packaging.DefinitionType v0 -> Just v0
                Packaging.DefinitionTerm _ -> Nothing
                Packaging.DefinitionPrimitive _ -> Nothing
          getTerm =
                  \def -> case def of
                    Packaging.DefinitionType _ -> Nothing
                    Packaging.DefinitionTerm v0 -> Just v0
                    Packaging.DefinitionPrimitive _ -> Nothing
      in (Optionals.cat (Lists.map getType defs), (Optionals.cat (Lists.map getTerm defs)))

-- | Reorder definitions: types first (with hydra.core.Name first among types), then topologically sorted terms
reorderDefs :: [Packaging.Definition] -> [Packaging.Definition]
reorderDefs defs =

      let partitioned = partitionDefinitions defs
          typeDefsRaw = Pairs.first partitioned
          nameFirst =
                  Lists.filter (\td -> Equality.equal (Packaging.typeDefinitionName td) (Core.Name "hydra.core.Name")) typeDefsRaw
          nameRest =
                  Lists.filter (\td -> Logic.not (Equality.equal (Packaging.typeDefinitionName td) (Core.Name "hydra.core.Name"))) typeDefsRaw
          typeDefs =
                  Lists.concat [
                    Lists.map (\td -> Packaging.DefinitionType td) nameFirst,
                    (Lists.map (\td -> Packaging.DefinitionType td) nameRest)]
          termDefsWrapped = Lists.map (\td -> Packaging.DefinitionTerm td) (Pairs.second partitioned)
          sortedTermDefs =
                  Lists.concat (Sorting.topologicalSortNodes (\d -> case d of
                    Packaging.DefinitionTerm v0 -> Packaging.termDefinitionName v0) (\d -> case d of
                    Packaging.DefinitionTerm v0 -> Sets.toList (Variables.freeVariablesInTerm (Packaging.termDefinitionBody v0))
                    _ -> []) termDefsWrapped)
      in (Lists.concat [
        typeDefs,
        sortedTermDefs])

-- | Convert a schema graph to a typing environment (Either version)
schemaGraphToTypingEnvironment :: Graph.Graph -> Either Errors.Error (M.Map Core.Name Core.TypeScheme)
schemaGraphToTypingEnvironment g =

      let toTypeScheme =
              \vars -> \typ -> case (Strip.deannotateType typ) of
                Core.TypeForall v0 -> toTypeScheme (Lists.cons (Core.forallTypeParameter v0) vars) (Core.forallTypeBody v0)
                _ -> Core.TypeScheme {
                  Core.typeSchemeVariables = (Lists.reverse vars),
                  Core.typeSchemeBody = typ,
                  Core.typeSchemeConstraints = Nothing}
          decodeType = \term -> Eithers.bimap (\_e -> Errors.ErrorDecoding _e) (\_a -> _a) (DecodeCore.type_ g term)
          decodeTypeScheme = \term -> Eithers.bimap (\_e -> Errors.ErrorDecoding _e) (\_a -> _a) (DecodeCore.typeScheme g term)
          toPair =
                  \el ->
                    let forTerm =
                            \term -> case term of
                              Core.TermRecord v0 -> Logic.ifElse (Equality.equal (Core.recordTypeName v0) (Core.Name "hydra.core.TypeScheme")) (Eithers.map Optionals.pure (decodeTypeScheme (Core.bindingTerm el))) (Right Nothing)
                              Core.TermInject v0 -> Logic.ifElse (Equality.equal (Core.injectionTypeName v0) (Core.Name "hydra.core.Type")) (Eithers.map (\decoded -> Just (toTypeScheme [] decoded)) (decodeType (Core.bindingTerm el))) (Right Nothing)
                              _ -> Right Nothing
                    in (Eithers.bind (Optionals.cases (Core.bindingTypeScheme el) (Eithers.map (\typ -> Just (Scoping.fTypeToTypeScheme typ)) (decodeType (Core.bindingTerm el))) (\ts -> Logic.ifElse (Equality.equal ts (Core.TypeScheme {
                      Core.typeSchemeVariables = [],
                      Core.typeSchemeBody = (Core.TypeVariable (Core.Name "hydra.core.TypeScheme")),
                      Core.typeSchemeConstraints = Nothing})) (Eithers.map Optionals.pure (decodeTypeScheme (Core.bindingTerm el))) (Logic.ifElse (Equality.equal ts (Core.TypeScheme {
                      Core.typeSchemeVariables = [],
                      Core.typeSchemeBody = (Core.TypeVariable (Core.Name "hydra.core.Type")),
                      Core.typeSchemeConstraints = Nothing})) (Eithers.map (\decoded -> Just (toTypeScheme [] decoded)) (decodeType (Core.bindingTerm el))) (forTerm (Strip.deannotateTerm (Core.bindingTerm el)))))) (\mts -> Right (Optionals.map (\ts -> (Core.bindingName el, ts)) mts)))
      in (Eithers.map (\mpairs -> Maps.fromList (Optionals.cat mpairs)) (Eithers.mapList toPair (Lexical.graphToBindings g)))

-- | Extract the bindings from a let term, or return an empty list for other terms
termAsBindings :: Core.Term -> [Core.Binding]
termAsBindings term =
    case (Strip.deannotateTerm term) of
      Core.TermLet v0 -> Core.letBindings v0
      _ -> []

-- | Encode a map of named types to a list of bindings
typesToDefinitions :: M.Map Core.Name Core.Type -> [Core.Binding]
typesToDefinitions typeMap =

      let toElement =
              \pair ->
                let name = Pairs.first pair
                in Core.Binding {
                  Core.bindingName = name,
                  Core.bindingTerm = (EncodeCore.type_ (Pairs.second pair)),
                  Core.bindingTypeScheme = Nothing}
      in (Lists.map toElement (Maps.toList typeMap))

-- | Execute a computation in the context of a lambda body, extending the type context with the lambda parameter
withLambdaContext :: (t0 -> Graph.Graph) -> (Graph.Graph -> t0 -> t1) -> t0 -> Core.Lambda -> (t1 -> t2) -> t2
withLambdaContext getContext setContext env lam body =

      let newContext = Scoping.extendGraphForLambda (getContext env) lam
      in (body (setContext newContext env))

-- | Execute a computation in the context of a let body, extending the type context with the let bindings
withLetContext :: (t0 -> Graph.Graph) -> (Graph.Graph -> t0 -> t1) -> (Graph.Graph -> Core.Binding -> Maybe Core.Term) -> t0 -> Core.Let -> (t1 -> t2) -> t2
withLetContext getContext setContext forBinding env letrec body =

      let newContext = Scoping.extendGraphForLet forBinding (getContext env) letrec
      in (body (setContext newContext env))

-- | Execute a computation in the context of a type lambda body, extending the type context with the type parameter
withTypeLambdaContext :: (t0 -> Graph.Graph) -> (Graph.Graph -> t0 -> t1) -> t0 -> Core.TypeLambda -> (t1 -> t2) -> t2
withTypeLambdaContext getContext setContext env tlam body =

      let newContext = Scoping.extendGraphForTypeLambda (getContext env) tlam
      in (body (setContext newContext env))