hydra-0.13.0: src/gen-main/haskell/Hydra/Inference.hs
-- Note: this is an automatically generated file. Do not edit.
-- | Type inference following Algorithm W, extended for nominal terms and types
module Hydra.Inference where
import qualified Hydra.Annotations as Annotations
import qualified Hydra.Checking as Checking
import qualified Hydra.Compute as Compute
import qualified Hydra.Core as Core
import qualified Hydra.Extract.Core as Core_
import qualified Hydra.Graph as Graph
import qualified Hydra.Lexical as Lexical
import qualified Hydra.Lib.Eithers as Eithers
import qualified Hydra.Lib.Equality as Equality
import qualified Hydra.Lib.Flows as Flows
import qualified Hydra.Lib.Lists as Lists
import qualified Hydra.Lib.Literals as Literals
import qualified Hydra.Lib.Logic as Logic
import qualified Hydra.Lib.Maps as Maps
import qualified Hydra.Lib.Math as Math
import qualified Hydra.Lib.Maybes as Maybes
import qualified Hydra.Lib.Pairs as Pairs
import qualified Hydra.Lib.Sets as Sets
import qualified Hydra.Lib.Strings as Strings
import qualified Hydra.Monads as Monads
import qualified Hydra.Reflect as Reflect
import qualified Hydra.Rewriting as Rewriting
import qualified Hydra.Schemas as Schemas
import qualified Hydra.Show.Core as Core__
import qualified Hydra.Show.Typing as Typing
import qualified Hydra.Sorting as Sorting
import qualified Hydra.Substitution as Substitution
import qualified Hydra.Typing as Typing_
import qualified Hydra.Unification as Unification
import Prelude hiding (Enum, Ordering, decodeFloat, encodeFloat, fail, map, pure, sum)
import qualified Data.ByteString as B
import qualified Data.Int as I
import qualified Data.List as L
import qualified Data.Map as M
import qualified Data.Set as S
-- | Bind type constraints and continue with substitution
bindConstraints :: (Typing_.InferenceContext -> (Typing_.TypeSubst -> Compute.Flow t0 t1) -> [Typing_.TypeConstraint] -> Compute.Flow t0 t1)
bindConstraints cx f constraints = (Flows.bind (Unification.unifyTypeConstraints (Typing_.inferenceContextSchemaTypes cx) constraints) (\s -> Flows.bind (Checking.checkTypeSubst cx s) (\_ -> f s)))
-- | Place unbound type variables appearing anywhere under a typed let binding in the type scheme of that binding. These variables may appear in the binding type scheme itself or in that of a subterm, in domain types attached to functions, and in type abstraction and type application terms. This process attempts to capture type variables which have escaped unification, e.g. due to unused code. However, unbound type variables not appearing beneath any typed let binding remain unbound.
bindUnboundTypeVariables :: (Typing_.InferenceContext -> Core.Term -> Core.Term)
bindUnboundTypeVariables cx term0 =
let svars = (Sets.fromList (Maps.keys (Typing_.inferenceContextSchemaTypes cx)))
in
let rewrite = (\recurse -> \term -> (\x -> case x of
Core.TermLet v1 ->
let forBinding = (\b ->
let bname = (Core.bindingName b)
in
let bterm = (Core.bindingTerm b)
in (Maybes.maybe (Core.Binding {
Core.bindingName = bname,
Core.bindingTerm = (bindUnboundTypeVariables cx bterm),
Core.bindingType = Nothing}) (\ts ->
let bvars = (Sets.fromList (Core.typeSchemeVariables ts))
in
let unboundInType = (Rewriting.freeVariablesInType (Core.typeSchemeType ts))
in
let unboundInTerm = (Rewriting.freeTypeVariablesInTerm bterm)
in
let unbound = (Sets.toList (Sets.difference (Sets.union unboundInType unboundInTerm) (Sets.union svars bvars)))
in
let ts2 = Core.TypeScheme {
Core.typeSchemeVariables = (Lists.concat2 (Core.typeSchemeVariables ts) unbound),
Core.typeSchemeType = (Core.typeSchemeType ts),
Core.typeSchemeConstraints = (Core.typeSchemeConstraints ts)}
in
let bterm2 = (Lists.foldl (\t -> \v -> Core.TermTypeLambda (Core.TypeLambda {
Core.typeLambdaParameter = v,
Core.typeLambdaBody = t})) bterm unbound)
in Core.Binding {
Core.bindingName = bname,
Core.bindingTerm = bterm2,
Core.bindingType = (Just ts2)}) (Core.bindingType b)))
in (Core.TermLet (Core.Let {
Core.letBindings = (Lists.map forBinding (Core.letBindings v1)),
Core.letBody = (bindUnboundTypeVariables cx (Core.letBody v1))}))
_ -> (recurse term)) term)
in (Rewriting.rewriteTerm rewrite term0)
-- | Fold a list of type variables over a term to build a type application term
buildTypeApplicationTerm :: ([Core.Name] -> Core.Term -> Core.Term)
buildTypeApplicationTerm tvars body = (Lists.foldl (\t -> \v -> Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = t,
Core.typeApplicationTermType = (Core.TypeVariable v)})) body tvars)
-- | An empty inference context
emptyInferenceContext :: Typing_.InferenceContext
emptyInferenceContext = Typing_.InferenceContext {
Typing_.inferenceContextSchemaTypes = Maps.empty,
Typing_.inferenceContextPrimitiveTypes = Maps.empty,
Typing_.inferenceContextDataTypes = Maps.empty,
Typing_.inferenceContextClassConstraints = Maps.empty,
Typing_.inferenceContextDebug = False}
-- | Add (term variable, type scheme) pairs to the typing environment
extendContext :: ([(Core.Name, Core.TypeScheme)] -> Typing_.InferenceContext -> Typing_.InferenceContext)
extendContext pairs cx = Typing_.InferenceContext {
Typing_.inferenceContextSchemaTypes = (Typing_.inferenceContextSchemaTypes cx),
Typing_.inferenceContextPrimitiveTypes = (Typing_.inferenceContextPrimitiveTypes cx),
Typing_.inferenceContextDataTypes = (Maps.union (Maps.fromList pairs) (Typing_.inferenceContextDataTypes cx)),
Typing_.inferenceContextClassConstraints = (Typing_.inferenceContextClassConstraints cx),
Typing_.inferenceContextDebug = (Typing_.inferenceContextDebug cx)}
-- | Finalize an inferred term by checking for unbound type variables, then normalizing type variables
finalizeInferredTerm :: (Typing_.InferenceContext -> Core.Term -> Compute.Flow t0 Core.Term)
finalizeInferredTerm cx term =
let term2 = (bindUnboundTypeVariables cx term)
in (Flows.bind (Checking.checkForUnboundTypeVariables cx term2) (\_ -> Flows.pure (Rewriting.normalizeTypeVariablesInTerm term2)))
-- | Infer a term's type and map over the result
forInferredTerm :: (Typing_.InferenceContext -> Core.Term -> String -> (Typing_.InferenceResult -> t0) -> Compute.Flow t1 t0)
forInferredTerm cx term desc f = (Flows.map f (inferTypeOfTerm cx term desc))
-- | Get all free variables in an inference context
freeVariablesInContext :: (Typing_.InferenceContext -> S.Set Core.Name)
freeVariablesInContext cx = (Lists.foldl Sets.union Sets.empty (Lists.map Rewriting.freeVariablesInTypeSchemeSimple (Maps.elems (Typing_.inferenceContextDataTypes cx))))
-- | Generate a fresh type variable
freshVariableType :: (Compute.Flow t0 Core.Type)
freshVariableType = (Flows.map (\x -> Core.TypeVariable x) Schemas.freshName)
-- | Generalize a type to a type scheme
generalize :: (Typing_.InferenceContext -> Core.Type -> Core.TypeScheme)
generalize cx typ =
let isTypeVarName = (\name ->
let parts = (Strings.splitOn "." (Core.unName name))
in (Equality.lte (Lists.length parts) 1))
in
let vars = (Lists.nub (Lists.filter (\v -> Logic.and (isUnbound cx v) (isTypeVarName v)) (Rewriting.freeVariablesInTypeOrdered typ)))
in
let allConstraints = (Typing_.inferenceContextClassConstraints cx)
in
let relevantConstraints = (Maps.fromList (Maybes.cat (Lists.map (\v -> Maybes.map (\meta -> (v, meta)) (Maps.lookup v allConstraints)) vars)))
in
let constraintsMaybe = (Logic.ifElse (Maps.null relevantConstraints) Nothing (Just relevantConstraints))
in Core.TypeScheme {
Core.typeSchemeVariables = vars,
Core.typeSchemeType = typ,
Core.typeSchemeConstraints = constraintsMaybe}
-- | Infer types for all elements in a graph
inferGraphTypes :: (Graph.Graph -> Compute.Flow t0 Graph.Graph)
inferGraphTypes g0 =
let fromLetTerm = (\l ->
let bindings = (Core.letBindings l)
in
let body = (Core.letBody l)
in Graph.Graph {
Graph.graphElements = bindings,
Graph.graphEnvironment = Maps.empty,
Graph.graphTypes = Maps.empty,
Graph.graphBody = body,
Graph.graphPrimitives = (Graph.graphPrimitives g0),
Graph.graphSchema = (Graph.graphSchema g0)})
in
let toLetTerm = (\g ->
let toBinding = (\el -> Core.Binding {
Core.bindingName = (Core.bindingName el),
Core.bindingTerm = (Core.bindingTerm el),
Core.bindingType = (Core.bindingType el)})
in (Core.TermLet (Core.Let {
Core.letBindings = (Lists.map toBinding (Graph.graphElements g)),
Core.letBody = (Graph.graphBody g)})))
in
let forFinal = (\finalized -> (\x -> case x of
Core.TermLet v1 -> (Flows.pure (fromLetTerm v1))
Core.TermVariable _ -> (Flows.fail "Expected inferred graph as let term")) finalized)
in (Monads.withTrace "graph inference" (Flows.bind (Schemas.graphToInferenceContext g0) (\cx -> Flows.bind (inferTypeOfTerm cx (toLetTerm g0) "graph term") (\result ->
let term = (Typing_.inferenceResultTerm result)
in
let ts = (Typing_.inferenceResultType result)
in (Flows.bind (finalizeInferredTerm cx term) (\finalized -> forFinal finalized))))))
-- | Infer the type of a term in graph context
inferInGraphContext :: (Core.Term -> Compute.Flow Graph.Graph Typing_.InferenceResult)
inferInGraphContext term = (Flows.bind Monads.getState (\g -> Flows.bind (Schemas.graphToInferenceContext g) (\cx -> inferTypeOfTerm cx term "single term")))
-- | Infer types for multiple terms
inferMany :: (Typing_.InferenceContext -> [(Core.Term, String)] -> Compute.Flow t0 ([Core.Term], ([Core.Type], Typing_.TypeSubst)))
inferMany cx pairs =
let dflt =
let e = (Pairs.first (Lists.head pairs))
in
let desc = (Pairs.second (Lists.head pairs))
in
let tl = (Lists.tail pairs)
in (Flows.bind (inferTypeOfTerm cx e desc) (\result1 ->
let e1 = (Typing_.inferenceResultTerm result1)
in
let t1 = (Typing_.inferenceResultType result1)
in
let s1 = (Typing_.inferenceResultSubst result1)
in (Flows.bind (inferMany (Substitution.substInContext s1 cx) tl) (\result2 ->
let e2 = (Pairs.first result2)
in
let t2 = (Pairs.first (Pairs.second result2))
in
let s2 = (Pairs.second (Pairs.second result2))
in (Flows.pure (Lists.cons (Substitution.substTypesInTerm s2 e1) e2, (Lists.cons (Substitution.substInType s2 t1) t2, (Substitution.composeTypeSubst s1 s2))))))))
in (Logic.ifElse (Lists.null pairs) (Flows.pure ([], ([], Substitution.idTypeSubst))) dflt)
-- | Infer the type of an annotated term
inferTypeOfAnnotatedTerm :: (Typing_.InferenceContext -> Core.AnnotatedTerm -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfAnnotatedTerm cx at =
let term = (Core.annotatedTermBody at)
in
let ann = (Core.annotatedTermAnnotation at)
in (Flows.bind (inferTypeOfTerm cx term "annotated term") (\result ->
let iterm = (Typing_.inferenceResultTerm result)
in
let itype = (Typing_.inferenceResultType result)
in
let isubst = (Typing_.inferenceResultSubst result)
in
let iconstraints = (Typing_.inferenceResultClassConstraints result)
in (Flows.pure (Typing_.InferenceResult {
Typing_.inferenceResultTerm = (Core.TermAnnotated (Core.AnnotatedTerm {
Core.annotatedTermBody = iterm,
Core.annotatedTermAnnotation = ann})),
Typing_.inferenceResultType = itype,
Typing_.inferenceResultSubst = isubst,
Typing_.inferenceResultClassConstraints = iconstraints}))))
-- | Infer the type of a function application
inferTypeOfApplication :: (Typing_.InferenceContext -> Core.Application -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfApplication cx app =
let e0 = (Core.applicationFunction app)
in
let e1 = (Core.applicationArgument app)
in (Flows.bind (inferTypeOfTerm cx e0 "lhs") (\lhsResult ->
let a = (Typing_.inferenceResultTerm lhsResult)
in
let t0 = (Typing_.inferenceResultType lhsResult)
in
let s0 = (Typing_.inferenceResultSubst lhsResult)
in
let c0 = (Typing_.inferenceResultClassConstraints lhsResult)
in (Flows.bind (inferTypeOfTerm (Substitution.substInContext s0 cx) e1 "rhs") (\rhsResult ->
let b = (Typing_.inferenceResultTerm rhsResult)
in
let t1 = (Typing_.inferenceResultType rhsResult)
in
let s1 = (Typing_.inferenceResultSubst rhsResult)
in
let c1 = (Typing_.inferenceResultClassConstraints rhsResult)
in (Flows.bind Schemas.freshName (\v -> Flows.bind (Unification.unifyTypes (Typing_.inferenceContextSchemaTypes cx) (Substitution.substInType s1 t0) (Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = t1,
Core.functionTypeCodomain = (Core.TypeVariable v)})) "application lhs") (\s2 -> Flows.bind (Checking.checkTypeSubst cx s2) (\_ ->
let rExpr = (Core.TermApplication (Core.Application {
Core.applicationFunction = (Substitution.substTypesInTerm (Substitution.composeTypeSubst s1 s2) a),
Core.applicationArgument = (Substitution.substTypesInTerm s2 b)}))
in
let rType = (Substitution.substInType s2 (Core.TypeVariable v))
in
let rSubst = (Substitution.composeTypeSubstList [
s0,
s1,
s2])
in
let c0Subst = (Substitution.substInClassConstraints s2 (Substitution.substInClassConstraints s1 c0))
in
let c1Subst = (Substitution.substInClassConstraints s2 c1)
in
let rConstraints = (mergeClassConstraints c0Subst c1Subst)
in (Flows.pure (Typing_.InferenceResult {
Typing_.inferenceResultTerm = rExpr,
Typing_.inferenceResultType = rType,
Typing_.inferenceResultSubst = rSubst,
Typing_.inferenceResultClassConstraints = rConstraints}))))))))))
-- | Infer the type of a case statement
inferTypeOfCaseStatement :: (Typing_.InferenceContext -> Core.CaseStatement -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfCaseStatement cx caseStmt =
let tname = (Core.caseStatementTypeName caseStmt)
in
let dflt = (Core.caseStatementDefault caseStmt)
in
let cases = (Core.caseStatementCases caseStmt)
in
let fnames = (Lists.map Core.fieldName cases)
in (Flows.bind (Schemas.requireSchemaType cx tname) (\schemaType ->
let svars = (Core.typeSchemeVariables schemaType)
in
let stype = (Core.typeSchemeType schemaType)
in (Flows.bind (Core_.unionType tname stype) (\sfields -> Flows.bind (Flows.mapMaybe (\t -> inferTypeOfTerm cx t (Strings.cat [
"case ",
(Core.unName tname),
".<default>"])) dflt) (\dfltResult -> Flows.bind (inferMany cx (Lists.map (\f -> (Core.fieldTerm f, (Strings.cat [
"case ",
(Core.unName tname),
".",
(Core.unName (Core.fieldName f))]))) cases)) (\caseResults ->
let iterms = (Pairs.first caseResults)
in
let itypes = (Pairs.first (Pairs.second caseResults))
in
let isubst = (Pairs.second (Pairs.second caseResults))
in (Flows.bind Schemas.freshName (\codv ->
let cod = (Core.TypeVariable codv)
in
let caseMap = (Maps.fromList (Lists.map (\ft -> (Core.fieldTypeName ft, (Core.fieldTypeType ft))) sfields))
in
let dfltConstraints = (Monads.maybeToList (Maybes.map (\r -> Typing_.TypeConstraint {
Typing_.typeConstraintLeft = cod,
Typing_.typeConstraintRight = (Substitution.substInType isubst (Typing_.inferenceResultType r)),
Typing_.typeConstraintComment = "match default"}) dfltResult))
in
let caseConstraints = (Maybes.cat (Lists.zipWith (\fname -> \itype -> Maybes.map (\ftype -> Typing_.TypeConstraint {
Typing_.typeConstraintLeft = itype,
Typing_.typeConstraintRight = (Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = ftype,
Core.functionTypeCodomain = cod})),
Typing_.typeConstraintComment = "case type"}) (Maps.lookup fname caseMap)) fnames itypes))
in (mapConstraints cx (\subst -> yield (buildTypeApplicationTerm svars (Core.TermFunction (Core.FunctionElimination (Core.EliminationUnion (Core.CaseStatement {
Core.caseStatementTypeName = tname,
Core.caseStatementDefault = (Maybes.map Typing_.inferenceResultTerm dfltResult),
Core.caseStatementCases = (Lists.zipWith (\n -> \t -> Core.Field {
Core.fieldName = n,
Core.fieldTerm = t}) fnames iterms)}))))) (Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = (Schemas.nominalApplication tname (Lists.map (\x -> Core.TypeVariable x) svars)),
Core.functionTypeCodomain = cod})) (Substitution.composeTypeSubstList (Lists.concat [
Monads.maybeToList (Maybes.map Typing_.inferenceResultSubst dfltResult),
[
isubst,
subst]]))) (Lists.concat [
dfltConstraints,
caseConstraints]))))))))))
-- | Infer the type of a collection
inferTypeOfCollection :: (Typing_.InferenceContext -> (Core.Type -> Core.Type) -> ([Core.Term] -> Core.Term) -> String -> [Core.Term] -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfCollection cx typCons trmCons desc els = (Flows.bind Schemas.freshName (\var -> Logic.ifElse (Lists.null els) (Flows.pure (yield (buildTypeApplicationTerm [
var] (trmCons [])) (typCons (Core.TypeVariable var)) Substitution.idTypeSubst)) (Flows.bind (inferMany cx (Lists.zip els (Lists.map (\i -> Strings.cat [
"#",
(Literals.showInt32 i)]) (Math.range 1 (Math.add (Lists.length els) 1))))) (\results ->
let terms = (Pairs.first results)
in
let types = (Pairs.first (Pairs.second results))
in
let subst1 = (Pairs.second (Pairs.second results))
in
let constraints = (Lists.map (\t -> Typing_.TypeConstraint {
Typing_.typeConstraintLeft = (Core.TypeVariable var),
Typing_.typeConstraintRight = t,
Typing_.typeConstraintComment = desc}) types)
in (mapConstraints cx (\subst2 ->
let iterm = (trmCons terms)
in
let itype = (typCons (Core.TypeVariable var))
in
let isubst = (Substitution.composeTypeSubst subst1 subst2)
in (yield iterm itype isubst)) constraints)))))
-- | Infer the type of a term and return a type scheme
inferTypeOf :: (Typing_.InferenceContext -> Core.Term -> Compute.Flow t0 (Core.Term, Core.TypeScheme))
inferTypeOf cx term =
let letTerm = (Core.TermLet (Core.Let {
Core.letBindings = [
Core.Binding {
Core.bindingName = (Core.Name "ignoredVariableName"),
Core.bindingTerm = term,
Core.bindingType = Nothing}],
Core.letBody = (Core.TermLiteral (Core.LiteralString "ignoredBody"))}))
in
let forBindings = (\bindings ->
let binding = (Lists.head bindings)
in
let term1 = (Core.bindingTerm binding)
in
let mts = (Core.bindingType binding)
in (Maybes.maybe (Flows.fail "Expected a type scheme") (\ts -> Flows.pure (term1, ts)) mts))
in
let unifyAndSubst = (\result ->
let subst = (Typing_.inferenceResultSubst result)
in (Flows.bind (finalizeInferredTerm cx (Typing_.inferenceResultTerm result)) (\finalized -> Flows.bind (Lexical.withEmptyGraph (Core_.let_ finalized)) (\letResult ->
let bindings = (Core.letBindings letResult)
in (Logic.ifElse (Equality.equal 1 (Lists.length bindings)) (forBindings bindings) (Flows.fail (Strings.cat [
"Expected a single binding with a type scheme, but got: ",
(Literals.showInt32 (Lists.length bindings)),
" bindings"])))))))
in (Flows.bind (inferTypeOfTerm cx letTerm "infer type of term") (\result -> unifyAndSubst result))
-- | Infer the type of an either value
inferTypeOfEither :: (Typing_.InferenceContext -> Either Core.Term Core.Term -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfEither cx e = (Eithers.either (\l -> Flows.bind (inferTypeOfTerm cx l "either left value") (\r1 ->
let iterm = (Typing_.inferenceResultTerm r1)
in
let leftType = (Typing_.inferenceResultType r1)
in
let subst = (Typing_.inferenceResultSubst r1)
in (Flows.bind freshVariableType (\rightType ->
let eitherTerm = (Core.TermEither (Left iterm))
in
let termWithLeftType = (Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = eitherTerm,
Core.typeApplicationTermType = leftType}))
in
let termWithBothTypes = (Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = termWithLeftType,
Core.typeApplicationTermType = rightType}))
in
let eitherType = (Core.TypeEither (Core.EitherType {
Core.eitherTypeLeft = leftType,
Core.eitherTypeRight = rightType}))
in (yieldChecked termWithBothTypes eitherType subst))))) (\r -> Flows.bind (inferTypeOfTerm cx r "either right value") (\r1 ->
let iterm = (Typing_.inferenceResultTerm r1)
in
let rightType = (Typing_.inferenceResultType r1)
in
let subst = (Typing_.inferenceResultSubst r1)
in (Flows.bind freshVariableType (\leftType ->
let eitherTerm = (Core.TermEither (Right iterm))
in
let termWithLeftType = (Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = eitherTerm,
Core.typeApplicationTermType = leftType}))
in
let termWithBothTypes = (Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = termWithLeftType,
Core.typeApplicationTermType = rightType}))
in
let eitherType = (Core.TypeEither (Core.EitherType {
Core.eitherTypeLeft = leftType,
Core.eitherTypeRight = rightType}))
in (yieldChecked termWithBothTypes eitherType subst))))) e)
-- | Infer the type of an elimination
inferTypeOfElimination :: (Typing_.InferenceContext -> Core.Elimination -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfElimination cx elm = ((\x -> case x of
Core.EliminationRecord v1 -> (inferTypeOfProjection cx v1)
Core.EliminationUnion v1 -> (inferTypeOfCaseStatement cx v1)
Core.EliminationWrap v1 -> (inferTypeOfUnwrap cx v1)) elm)
-- | Infer the type of a function
inferTypeOfFunction :: (Typing_.InferenceContext -> Core.Function -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfFunction cx f = ((\x -> case x of
Core.FunctionElimination v1 -> (inferTypeOfElimination cx v1)
Core.FunctionLambda v1 -> (inferTypeOfLambda cx v1)
Core.FunctionPrimitive v1 -> (inferTypeOfPrimitive cx v1)) f)
-- | Infer the type of a union injection
inferTypeOfInjection :: (Typing_.InferenceContext -> Core.Injection -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfInjection cx injection =
let tname = (Core.injectionTypeName injection)
in
let field = (Core.injectionField injection)
in
let fname = (Core.fieldName field)
in
let term = (Core.fieldTerm field)
in (Flows.bind (inferTypeOfTerm cx term "injected term") (\result -> Flows.bind (Schemas.requireSchemaType cx tname) (\schemaType ->
let svars = (Core.typeSchemeVariables schemaType)
in
let stype = (Core.typeSchemeType schemaType)
in
let iterm = (Typing_.inferenceResultTerm result)
in
let ityp = (Typing_.inferenceResultType result)
in
let isubst = (Typing_.inferenceResultSubst result)
in (Flows.bind (Core_.unionType tname stype) (\sfields -> Flows.bind (Schemas.findFieldType fname sfields) (\ftyp -> mapConstraints cx (\subst -> yield (buildTypeApplicationTerm svars (Core.TermUnion (Core.Injection {
Core.injectionTypeName = tname,
Core.injectionField = Core.Field {
Core.fieldName = fname,
Core.fieldTerm = iterm}}))) (Schemas.nominalApplication tname (Lists.map (\x -> Core.TypeVariable x) svars)) (Substitution.composeTypeSubst isubst subst)) [
Typing_.TypeConstraint {
Typing_.typeConstraintLeft = ftyp,
Typing_.typeConstraintRight = ityp,
Typing_.typeConstraintComment = "schema type of injected field"}]))))))
-- | Infer the type of a lambda function
inferTypeOfLambda :: (Typing_.InferenceContext -> Core.Lambda -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfLambda cx lambda =
let var = (Core.lambdaParameter lambda)
in
let body = (Core.lambdaBody lambda)
in (Flows.bind Schemas.freshName (\vdom ->
let dom = (Core.TypeVariable vdom)
in
let cx2 = (extendContext [
(var, Core.TypeScheme {
Core.typeSchemeVariables = [],
Core.typeSchemeType = dom,
Core.typeSchemeConstraints = Nothing})] cx)
in (Flows.bind (inferTypeOfTerm cx2 body "lambda body") (\result ->
let iterm = (Typing_.inferenceResultTerm result)
in
let icod = (Typing_.inferenceResultType result)
in
let isubst = (Typing_.inferenceResultSubst result)
in
let rdom = (Substitution.substInType isubst dom)
in
let rterm = (Core.TermFunction (Core.FunctionLambda (Core.Lambda {
Core.lambdaParameter = var,
Core.lambdaDomain = (Just rdom),
Core.lambdaBody = iterm})))
in
let rtype = (Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = rdom,
Core.functionTypeCodomain = icod}))
in
let vars = (Sets.unions [
Rewriting.freeVariablesInType rdom,
(Rewriting.freeVariablesInType icod),
(freeVariablesInContext (Substitution.substInContext isubst cx2))])
in
let cx3 = (Substitution.substInContext isubst cx)
in
let iconstraints = (Substitution.substInClassConstraints isubst (Typing_.inferenceResultClassConstraints result))
in (Flows.pure (Typing_.InferenceResult {
Typing_.inferenceResultTerm = rterm,
Typing_.inferenceResultType = rtype,
Typing_.inferenceResultSubst = isubst,
Typing_.inferenceResultClassConstraints = iconstraints}))))))
-- | Infer the type of a let (letrec) term which is already in a normal form
inferTypeOfLetNormalized :: (Typing_.InferenceContext -> Core.Let -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfLetNormalized cx0 letTerm =
let bins0 = (Core.letBindings letTerm)
in
let body0 = (Core.letBody letTerm)
in
let bnames = (Lists.map Core.bindingName bins0)
in (Flows.bind (Schemas.freshNames (Lists.length bins0)) (\bvars ->
let tbins0 = (Lists.map (\x -> Core.TypeVariable x) bvars)
in
let cx1 = (extendContext (Lists.zip bnames (Lists.map (\t -> Core.TypeScheme {
Core.typeSchemeVariables = [],
Core.typeSchemeType = t,
Core.typeSchemeConstraints = Nothing}) tbins0)) cx0)
in (Flows.bind (inferTypesOfTemporaryBindings cx1 bins0) (\inferredResult ->
let bterms1 = (Pairs.first inferredResult)
in
let tbins1 = (Pairs.first (Pairs.second inferredResult))
in
let substAndConstraints = (Pairs.second (Pairs.second inferredResult))
in
let s1 = (Pairs.first substAndConstraints)
in
let inferredConstraints = (Pairs.second substAndConstraints)
in (Flows.bind (Unification.unifyTypeLists (Typing_.inferenceContextSchemaTypes cx0) (Lists.map (Substitution.substInType s1) tbins0) tbins1 "temporary type bindings") (\s2 -> Flows.bind (Checking.checkTypeSubst cx0 s2) (\_ ->
let g2base = (Substitution.substInContext (Substitution.composeTypeSubst s1 s2) cx0)
in
let constraintsWithS2 = (Substitution.substInClassConstraints s2 inferredConstraints)
in
let composedSubst = (Substitution.composeTypeSubst s1 s2)
in
let originalBindingConstraints = (Lists.foldl (\acc -> \b -> Maybes.maybe acc (\ts -> Maybes.maybe acc (\c -> mergeClassConstraints acc c) (Core.typeSchemeConstraints ts)) (Core.bindingType b)) Maps.empty bins0)
in
let originalConstraintsSubst = (Substitution.substInClassConstraints composedSubst originalBindingConstraints)
in
let allInferredConstraints = (mergeClassConstraints constraintsWithS2 originalConstraintsSubst)
in
let mergedConstraints = (mergeClassConstraints (Typing_.inferenceContextClassConstraints g2base) allInferredConstraints)
in
let g2 = Typing_.InferenceContext {
Typing_.inferenceContextSchemaTypes = (Typing_.inferenceContextSchemaTypes g2base),
Typing_.inferenceContextPrimitiveTypes = (Typing_.inferenceContextPrimitiveTypes g2base),
Typing_.inferenceContextDataTypes = (Typing_.inferenceContextDataTypes g2base),
Typing_.inferenceContextClassConstraints = mergedConstraints,
Typing_.inferenceContextDebug = (Typing_.inferenceContextDebug g2base)}
in
let bterms1Subst = (Lists.map (Substitution.substTypesInTerm s2) bterms1)
in
let tsbins1 = (Lists.zip bnames (Lists.map (\t -> generalize g2 (Substitution.substInType s2 t)) tbins1))
in (Flows.bind (inferTypeOfTerm (extendContext tsbins1 g2) body0 "let body") (\bodyResult ->
let body1 = (Typing_.inferenceResultTerm bodyResult)
in
let tbody = (Typing_.inferenceResultType bodyResult)
in
let sbody = (Typing_.inferenceResultSubst bodyResult)
in
let st1 = (Typing_.TermSubst (Maps.fromList (Lists.map (\pair ->
let name = (Pairs.first pair)
in
let ts = (Pairs.second pair)
in (name, (buildTypeApplicationTerm (Core.typeSchemeVariables ts) (Core.TermVariable name)))) tsbins1)))
in
let createBinding = (\bindingPair ->
let nameTsPair = (Pairs.first bindingPair)
in
let term = (Pairs.second bindingPair)
in
let name = (Pairs.first nameTsPair)
in
let ts = (Pairs.second nameTsPair)
in
let finalTs = (Substitution.substInTypeScheme sbody ts)
in
let typeLambdaTerm = (Lists.foldl (\b -> \v -> Core.TermTypeLambda (Core.TypeLambda {
Core.typeLambdaParameter = v,
Core.typeLambdaBody = b})) (Substitution.substituteInTerm st1 term) (Lists.reverse (Core.typeSchemeVariables finalTs)))
in Core.Binding {
Core.bindingName = name,
Core.bindingTerm = (Substitution.substTypesInTerm (Substitution.composeTypeSubst sbody s2) typeLambdaTerm),
Core.bindingType = (Just finalTs)})
in
let bins1 = (Lists.map createBinding (Lists.zip tsbins1 bterms1Subst))
in
let bodyConstraints = (Substitution.substInClassConstraints sbody (Typing_.inferenceResultClassConstraints bodyResult))
in
let bindingConstraintsSubst = (Substitution.substInClassConstraints sbody constraintsWithS2)
in
let allConstraints = (mergeClassConstraints bindingConstraintsSubst bodyConstraints)
in
let ret = Typing_.InferenceResult {
Typing_.inferenceResultTerm = (Core.TermLet (Core.Let {
Core.letBindings = bins1,
Core.letBody = body1})),
Typing_.inferenceResultType = tbody,
Typing_.inferenceResultSubst = (Substitution.composeTypeSubstList [
s1,
s2,
sbody]),
Typing_.inferenceResultClassConstraints = allConstraints}
in (Flows.pure ret))))))))))
-- | Normalize a let term before inferring its type
inferTypeOfLet :: (Typing_.InferenceContext -> Core.Let -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfLet cx let0 =
let bindings0 = (Core.letBindings let0)
in
let body0 = (Core.letBody let0)
in
let names = (Lists.map Core.bindingName bindings0)
in
let nameSet = (Sets.fromList names)
in
let toPair = (\binding ->
let name = (Core.bindingName binding)
in
let term = (Core.bindingTerm binding)
in (name, (Lists.filter (\n -> Sets.member n nameSet) (Sets.toList (Rewriting.freeVariablesInTerm term)))))
in
let adjList = (Lists.map toPair bindings0)
in
let groups = (Sorting.topologicalSortComponents adjList)
in
let bindingMap = (Maps.fromList (Lists.zip names bindings0))
in
let createLet = (\e -> \group -> Core.TermLet (Core.Let {
Core.letBindings = (Maybes.cat (Lists.map (\n -> Maps.lookup n bindingMap) group)),
Core.letBody = e}))
in
let rewrittenLet = (Lists.foldl createLet body0 (Lists.reverse groups))
in
let restoreLet = (\iterm ->
let helper = (\level -> \bins -> \term ->
let nonzero = (\term -> (\x -> case x of
Core.TermLet v1 ->
let bs = (Core.letBindings v1)
in
let letBody = (Core.letBody v1)
in (helper (Math.sub level 1) (Lists.concat [
bs,
bins]) letBody)) term)
in (Logic.ifElse (Equality.equal level 0) (bins, term) (nonzero term)))
in
let result = (helper (Lists.length groups) [] iterm)
in
let bindingList = (Pairs.first result)
in
let e = (Pairs.second result)
in
let bindingMap2 = (Maps.fromList (Lists.map (\b -> (Core.bindingName b, b)) bindingList))
in (Core.TermLet (Core.Let {
Core.letBindings = (Maybes.cat (Lists.map (\n -> Maps.lookup n bindingMap2) names)),
Core.letBody = e})))
in
let rewriteResult = (\result ->
let iterm = (Typing_.inferenceResultTerm result)
in
let itype = (Typing_.inferenceResultType result)
in
let isubst = (Typing_.inferenceResultSubst result)
in
let iconstraints = (Typing_.inferenceResultClassConstraints result)
in Typing_.InferenceResult {
Typing_.inferenceResultTerm = (restoreLet iterm),
Typing_.inferenceResultType = itype,
Typing_.inferenceResultSubst = isubst,
Typing_.inferenceResultClassConstraints = iconstraints})
in
let res = ((\x -> case x of
Core.TermLet v1 -> (inferTypeOfLetNormalized cx v1)
_ -> (inferTypeOfTerm cx rewrittenLet "empty let term")) rewrittenLet)
in (Flows.map rewriteResult res)
-- | Infer the type of a list
inferTypeOfList :: (Typing_.InferenceContext -> [Core.Term] -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfList cx = (inferTypeOfCollection cx (\x -> Core.TypeList x) (\x -> Core.TermList x) "list element")
-- | Infer the type of a literal
inferTypeOfLiteral :: (t0 -> Core.Literal -> Compute.Flow t1 Typing_.InferenceResult)
inferTypeOfLiteral _ lit = (Flows.pure (Typing_.InferenceResult {
Typing_.inferenceResultTerm = (Core.TermLiteral lit),
Typing_.inferenceResultType = (Core.TypeLiteral (Reflect.literalType lit)),
Typing_.inferenceResultSubst = Substitution.idTypeSubst,
Typing_.inferenceResultClassConstraints = Maps.empty}))
-- | Infer the type of a map
inferTypeOfMap :: (Typing_.InferenceContext -> M.Map Core.Term Core.Term -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfMap cx m = (Flows.bind Schemas.freshName (\kvar -> Flows.bind Schemas.freshName (\vvar -> Logic.ifElse (Maps.null m) (Flows.pure (yield (buildTypeApplicationTerm [
kvar,
vvar] (Core.TermMap Maps.empty)) (Core.TypeMap (Core.MapType {
Core.mapTypeKeys = (Core.TypeVariable kvar),
Core.mapTypeValues = (Core.TypeVariable vvar)})) Substitution.idTypeSubst)) (Flows.bind (inferMany cx (Lists.map (\k -> (k, "map key")) (Maps.keys m))) (\kresults ->
let kterms = (Pairs.first kresults)
in
let ktypes = (Pairs.first (Pairs.second kresults))
in
let ksubst = (Pairs.second (Pairs.second kresults))
in (Flows.bind (inferMany cx (Lists.map (\v -> (v, "map value")) (Maps.elems m))) (\vresults ->
let vterms = (Pairs.first vresults)
in
let vtypes = (Pairs.first (Pairs.second vresults))
in
let vsubst = (Pairs.second (Pairs.second vresults))
in
let kcons = (Lists.map (\t -> Typing_.TypeConstraint {
Typing_.typeConstraintLeft = (Core.TypeVariable kvar),
Typing_.typeConstraintRight = t,
Typing_.typeConstraintComment = "map key"}) ktypes)
in
let vcons = (Lists.map (\t -> Typing_.TypeConstraint {
Typing_.typeConstraintLeft = (Core.TypeVariable vvar),
Typing_.typeConstraintRight = t,
Typing_.typeConstraintComment = "map value"}) vtypes)
in (mapConstraints cx (\subst -> yield (Core.TermMap (Maps.fromList (Lists.zip kterms vterms))) (Core.TypeMap (Core.MapType {
Core.mapTypeKeys = (Core.TypeVariable kvar),
Core.mapTypeValues = (Core.TypeVariable vvar)})) (Substitution.composeTypeSubstList [
ksubst,
vsubst,
subst])) (Lists.concat [
kcons,
vcons])))))))))
-- | Infer the type of an optional
inferTypeOfOptional :: (Typing_.InferenceContext -> Maybe Core.Term -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfOptional cx m =
let trmCons = (\terms -> Logic.ifElse (Lists.null terms) (Core.TermMaybe Nothing) (Core.TermMaybe (Just (Lists.head terms))))
in (inferTypeOfCollection cx (\x -> Core.TypeMaybe x) trmCons "optional element" (Maybes.maybe [] Lists.singleton m))
-- | Infer the type of a pair
inferTypeOfPair :: (Typing_.InferenceContext -> (Core.Term, Core.Term) -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfPair cx p = (Flows.map (\results ->
let iterms = (Pairs.first results)
in
let itypes = (Pairs.first (Pairs.second results))
in
let isubst = (Pairs.second (Pairs.second results))
in
let ifst = (Lists.head iterms)
in
let isnd = (Lists.head (Lists.tail iterms))
in
let tyFst = (Lists.head itypes)
in
let tySnd = (Lists.head (Lists.tail itypes))
in
let pairTerm = (Core.TermPair (ifst, isnd))
in
let termWithTypes = (Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = (Core.TermTypeApplication (Core.TypeApplicationTerm {
Core.typeApplicationTermBody = pairTerm,
Core.typeApplicationTermType = tyFst})),
Core.typeApplicationTermType = tySnd}))
in (yield termWithTypes (Core.TypePair (Core.PairType {
Core.pairTypeFirst = tyFst,
Core.pairTypeSecond = tySnd})) isubst)) (inferMany cx [
(Pairs.first p, "pair first element"),
(Pairs.second p, "pair second element")]))
-- | Infer the type of a primitive function. Class constraints from the primitive's type scheme are propagated to the inference result.
inferTypeOfPrimitive :: (Typing_.InferenceContext -> Core.Name -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfPrimitive cx name = (Maybes.maybe (Flows.fail (Strings.cat2 "No such primitive: " (Core.unName name))) (\scheme -> Flows.bind (Schemas.instantiateTypeScheme scheme) (\ts ->
let constraints = (Maybes.fromMaybe Maps.empty (Core.typeSchemeConstraints ts))
in (yieldCheckedWithConstraints (buildTypeApplicationTerm (Core.typeSchemeVariables ts) (Core.TermFunction (Core.FunctionPrimitive name))) (Core.typeSchemeType ts) Substitution.idTypeSubst constraints))) (Maps.lookup name (Typing_.inferenceContextPrimitiveTypes cx)))
-- | Infer the type of a record projection
inferTypeOfProjection :: (Typing_.InferenceContext -> Core.Projection -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfProjection cx proj =
let tname = (Core.projectionTypeName proj)
in
let fname = (Core.projectionField proj)
in (Flows.bind (Schemas.requireSchemaType cx tname) (\schemaType ->
let svars = (Core.typeSchemeVariables schemaType)
in
let stype = (Core.typeSchemeType schemaType)
in (Flows.bind (Core_.recordType tname stype) (\sfields -> Flows.bind (Schemas.findFieldType fname sfields) (\ftyp -> Flows.pure (yield (buildTypeApplicationTerm svars (Core.TermFunction (Core.FunctionElimination (Core.EliminationRecord (Core.Projection {
Core.projectionTypeName = tname,
Core.projectionField = fname}))))) (Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = (Schemas.nominalApplication tname (Lists.map (\x -> Core.TypeVariable x) svars)),
Core.functionTypeCodomain = ftyp})) Substitution.idTypeSubst))))))
-- | Infer the type of a record
inferTypeOfRecord :: (Typing_.InferenceContext -> Core.Record -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfRecord cx record =
let tname = (Core.recordTypeName record)
in
let fields = (Core.recordFields record)
in
let fnames = (Lists.map Core.fieldName fields)
in (Flows.bind (Schemas.requireSchemaType cx tname) (\schemaType -> Flows.bind (inferMany cx (Lists.map (\f -> (Core.fieldTerm f, (Strings.cat2 "field " (Core.unName (Core.fieldName f))))) fields)) (\results ->
let svars = (Core.typeSchemeVariables schemaType)
in
let stype = (Core.typeSchemeType schemaType)
in
let iterms = (Pairs.first results)
in
let itypes = (Pairs.first (Pairs.second results))
in
let isubst = (Pairs.second (Pairs.second results))
in
let ityp = (Core.TypeRecord (Core.RowType {
Core.rowTypeTypeName = tname,
Core.rowTypeFields = (Lists.zipWith (\n -> \t -> Core.FieldType {
Core.fieldTypeName = n,
Core.fieldTypeType = t}) fnames itypes)}))
in (mapConstraints cx (\subst -> yield (buildTypeApplicationTerm svars (Core.TermRecord (Core.Record {
Core.recordTypeName = tname,
Core.recordFields = (Lists.zipWith (\n -> \t -> Core.Field {
Core.fieldName = n,
Core.fieldTerm = t}) fnames iterms)}))) (Schemas.nominalApplication tname (Lists.map (\x -> Core.TypeVariable x) svars)) (Substitution.composeTypeSubst isubst subst)) [
Typing_.TypeConstraint {
Typing_.typeConstraintLeft = stype,
Typing_.typeConstraintRight = ityp,
Typing_.typeConstraintComment = "schema type of record"}]))))
-- | Infer the type of a set
inferTypeOfSet :: (Typing_.InferenceContext -> S.Set Core.Term -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfSet cx s = (inferTypeOfCollection cx (\x -> Core.TypeSet x) (\terms -> Core.TermSet (Sets.fromList terms)) "set element" (Sets.toList s))
-- | Infer the type of a given term
inferTypeOfTerm :: (Typing_.InferenceContext -> Core.Term -> String -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfTerm cx term desc =
let matchTerm = ((\x -> case x of
Core.TermAnnotated v1 -> (inferTypeOfAnnotatedTerm cx v1)
Core.TermApplication v1 -> (inferTypeOfApplication cx v1)
Core.TermEither v1 -> (inferTypeOfEither cx v1)
Core.TermFunction v1 -> (inferTypeOfFunction cx v1)
Core.TermLet v1 -> (inferTypeOfLet cx v1)
Core.TermList v1 -> (inferTypeOfList cx v1)
Core.TermLiteral v1 -> (inferTypeOfLiteral cx v1)
Core.TermMap v1 -> (inferTypeOfMap cx v1)
Core.TermMaybe v1 -> (inferTypeOfOptional cx v1)
Core.TermPair v1 -> (inferTypeOfPair cx v1)
Core.TermRecord v1 -> (inferTypeOfRecord cx v1)
Core.TermSet v1 -> (inferTypeOfSet cx v1)
Core.TermTypeApplication v1 -> (inferTypeOfTypeApplication cx v1)
Core.TermTypeLambda v1 -> (inferTypeOfTypeLambda cx v1)
Core.TermUnion v1 -> (inferTypeOfInjection cx v1)
Core.TermUnit -> (Flows.pure inferTypeOfUnit)
Core.TermVariable v1 -> (inferTypeOfVariable cx v1)
Core.TermWrap v1 -> (inferTypeOfWrappedTerm cx v1)) term)
in (Monads.withTrace desc matchTerm)
-- | Infer the type of a type abstraction; just pass through to the lambda body.
inferTypeOfTypeLambda :: (Typing_.InferenceContext -> Core.TypeLambda -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfTypeLambda cx ta = (inferTypeOfTerm cx (Core.typeLambdaBody ta) "type abstraction")
-- | Infer the type of a type application; just pass through to the inner term.
inferTypeOfTypeApplication :: (Typing_.InferenceContext -> Core.TypeApplicationTerm -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfTypeApplication cx tt = (inferTypeOfTerm cx (Core.typeApplicationTermBody tt) "type application term")
-- | The trivial inference rule for the unit term
inferTypeOfUnit :: Typing_.InferenceResult
inferTypeOfUnit = Typing_.InferenceResult {
Typing_.inferenceResultTerm = Core.TermUnit,
Typing_.inferenceResultType = Core.TypeUnit,
Typing_.inferenceResultSubst = Substitution.idTypeSubst,
Typing_.inferenceResultClassConstraints = Maps.empty}
-- | Infer the type of an unwrap operation
inferTypeOfUnwrap :: (Typing_.InferenceContext -> Core.Name -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfUnwrap cx tname = (Flows.bind (Schemas.requireSchemaType cx tname) (\schemaType ->
let svars = (Core.typeSchemeVariables schemaType)
in
let stype = (Core.typeSchemeType schemaType)
in (Flows.bind (Core_.wrappedType tname stype) (\wtyp -> Flows.pure (yield (buildTypeApplicationTerm svars (Core.TermFunction (Core.FunctionElimination (Core.EliminationWrap tname)))) (Core.TypeFunction (Core.FunctionType {
Core.functionTypeDomain = (Schemas.nominalApplication tname (Lists.map (\x -> Core.TypeVariable x) svars)),
Core.functionTypeCodomain = wtyp})) Substitution.idTypeSubst)))))
-- | Infer the type of a variable
inferTypeOfVariable :: (Typing_.InferenceContext -> Core.Name -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfVariable cx name = (Maybes.maybe (Flows.fail (Strings.cat2 "Variable not bound to type: " (Core.unName name))) (\scheme -> Flows.bind (Schemas.instantiateTypeScheme scheme) (\ts ->
let constraints = (Maybes.fromMaybe Maps.empty (Core.typeSchemeConstraints ts))
in (Flows.pure (Typing_.InferenceResult {
Typing_.inferenceResultTerm = (buildTypeApplicationTerm (Core.typeSchemeVariables ts) (Core.TermVariable name)),
Typing_.inferenceResultType = (Core.typeSchemeType ts),
Typing_.inferenceResultSubst = Substitution.idTypeSubst,
Typing_.inferenceResultClassConstraints = constraints})))) (Maps.lookup name (Typing_.inferenceContextDataTypes cx)))
-- | Infer the type of a wrapped term
inferTypeOfWrappedTerm :: (Typing_.InferenceContext -> Core.WrappedTerm -> Compute.Flow t0 Typing_.InferenceResult)
inferTypeOfWrappedTerm cx wt =
let tname = (Core.wrappedTermTypeName wt)
in
let term = (Core.wrappedTermBody wt)
in (Flows.bind (Schemas.requireSchemaType cx tname) (\schemaType -> Flows.bind (inferTypeOfTerm cx term "wrapped term") (\result ->
let svars = (Core.typeSchemeVariables schemaType)
in
let stype = (Core.typeSchemeType schemaType)
in
let iterm = (Typing_.inferenceResultTerm result)
in
let itype = (Typing_.inferenceResultType result)
in
let isubst = (Typing_.inferenceResultSubst result)
in
let ityp = (Core.TypeWrap (Core.WrappedType {
Core.wrappedTypeTypeName = tname,
Core.wrappedTypeBody = itype}))
in (mapConstraints cx (\subst -> yield (buildTypeApplicationTerm svars (Core.TermWrap (Core.WrappedTerm {
Core.wrappedTermTypeName = tname,
Core.wrappedTermBody = iterm}))) (Schemas.nominalApplication tname (Lists.map (\x -> Core.TypeVariable x) svars)) (Substitution.composeTypeSubst isubst subst)) [
Typing_.TypeConstraint {
Typing_.typeConstraintLeft = stype,
Typing_.typeConstraintRight = ityp,
Typing_.typeConstraintComment = "schema type of wrapper"}]))))
-- | Infer types for temporary let bindings. Returns a 4-tuple of (terms, types, substitution, accumulated constraints)
inferTypesOfTemporaryBindings :: (Typing_.InferenceContext -> [Core.Binding] -> Compute.Flow t0 ([Core.Term], ([Core.Type], (Typing_.TypeSubst, (M.Map Core.Name Core.TypeVariableMetadata)))))
inferTypesOfTemporaryBindings cx bins =
let dflt =
let binding = (Lists.head bins)
in
let k = (Core.bindingName binding)
in
let v = (Core.bindingTerm binding)
in
let tl = (Lists.tail bins)
in (Flows.bind (inferTypeOfTerm cx v (Strings.cat [
"temporary let binding '",
(Core.unName k),
"'"])) (\result1 ->
let j = (Typing_.inferenceResultTerm result1)
in
let u_prime = (Typing_.inferenceResultType result1)
in
let u = (Typing_.inferenceResultSubst result1)
in
let c1Inferred = (Typing_.inferenceResultClassConstraints result1)
in (Flows.bind (Maybes.maybe (Flows.pure Maps.empty) (\ts -> Flows.bind (Schemas.instantiateTypeScheme ts) (\instantiatedTs ->
let freshConstraints = (Maybes.fromMaybe Maps.empty (Core.typeSchemeConstraints instantiatedTs))
in (Flows.bind (Unification.unifyTypes (Typing_.inferenceContextSchemaTypes cx) (Core.typeSchemeType instantiatedTs) u_prime "original binding type") (\unifySubst -> Flows.pure (Substitution.substInClassConstraints unifySubst freshConstraints))))) (Core.bindingType binding)) (\originalBindingConstraints ->
let c1 = (mergeClassConstraints c1Inferred originalBindingConstraints)
in (Flows.bind (inferTypesOfTemporaryBindings (Substitution.substInContext u cx) tl) (\result2 ->
let h = (Pairs.first result2)
in
let r_prime = (Pairs.first (Pairs.second result2))
in
let restPair = (Pairs.second (Pairs.second result2))
in
let r = (Pairs.first restPair)
in
let c2 = (Pairs.second restPair)
in
let c1Subst = (Substitution.substInClassConstraints r c1)
in
let mergedConstraints = (mergeClassConstraints c1Subst c2)
in (Flows.pure (Lists.cons (Substitution.substTypesInTerm r j) h, (Lists.cons (Substitution.substInType r u_prime) r_prime, (Substitution.composeTypeSubst u r, mergedConstraints))))))))))
in (Logic.ifElse (Lists.null bins) (Flows.pure ([], ([], (Substitution.idTypeSubst, Maps.empty)))) dflt)
-- | Create an initial type context from a graph
initialTypeContext :: (Graph.Graph -> Compute.Flow t0 Typing_.TypeContext)
initialTypeContext g =
let toPair = (\el ->
let name = (Core.bindingName el)
in (Maybes.maybe (Flows.fail (Strings.cat2 "untyped element: " (Core.unName name))) (\ts -> Flows.pure (name, (Schemas.typeSchemeToFType ts))) (Core.bindingType el)))
in (Flows.bind (Schemas.graphToInferenceContext g) (\ix -> Flows.bind (Flows.map Maps.fromList (Flows.mapList toPair (Graph.graphElements g))) (\types -> Flows.pure (Typing_.TypeContext {
Typing_.typeContextTypes = types,
Typing_.typeContextMetadata = Maps.empty,
Typing_.typeContextTypeVariables = Sets.empty,
Typing_.typeContextLambdaVariables = Sets.empty,
Typing_.typeContextLetVariables = Sets.empty,
Typing_.typeContextInferenceContext = ix}))))
-- | Check if a variable is unbound in context
isUnbound :: (Typing_.InferenceContext -> Core.Name -> Bool)
isUnbound cx v = (Logic.and (Logic.not (Sets.member v (freeVariablesInContext cx))) (Logic.not (Maps.member v (Typing_.inferenceContextSchemaTypes cx))))
-- | Map over type constraints after unification
mapConstraints :: (Typing_.InferenceContext -> (Typing_.TypeSubst -> t0) -> [Typing_.TypeConstraint] -> Compute.Flow t1 t0)
mapConstraints cx f constraints = (Flows.bind (Unification.unifyTypeConstraints (Typing_.inferenceContextSchemaTypes cx) constraints) (\s -> Flows.bind (Checking.checkTypeSubst cx s) (\_ -> Flows.pure (f s))))
-- | Merge two maps of class constraints. When both maps have constraints for the same variable, union the class sets.
mergeClassConstraints :: Ord t0 => (M.Map t0 Core.TypeVariableMetadata -> M.Map t0 Core.TypeVariableMetadata -> M.Map t0 Core.TypeVariableMetadata)
mergeClassConstraints m1 m2 = (Lists.foldl (\acc -> \pair ->
let k = (Pairs.first pair)
in
let v = (Pairs.second pair)
in (Maybes.maybe (Maps.insert k v acc) (\existing ->
let merged = Core.TypeVariableMetadata {
Core.typeVariableMetadataClasses = (Sets.union (Core.typeVariableMetadataClasses existing) (Core.typeVariableMetadataClasses v))}
in (Maps.insert k merged acc)) (Maps.lookup k acc))) m1 (Maps.toList m2))
-- | Show an inference result for debugging
showInferenceResult :: (Typing_.InferenceResult -> String)
showInferenceResult result =
let term = (Typing_.inferenceResultTerm result)
in
let typ = (Typing_.inferenceResultType result)
in
let subst = (Typing_.inferenceResultSubst result)
in (Strings.cat [
"{term=",
(Core__.term term),
", type=",
(Core__.type_ typ),
", subst=",
(Typing.typeSubst subst),
"}"])
-- | Create an inference result with no class constraints
yield :: (Core.Term -> Core.Type -> Typing_.TypeSubst -> Typing_.InferenceResult)
yield term typ subst = Typing_.InferenceResult {
Typing_.inferenceResultTerm = (Substitution.substTypesInTerm subst term),
Typing_.inferenceResultType = (Substitution.substInType subst typ),
Typing_.inferenceResultSubst = subst,
Typing_.inferenceResultClassConstraints = Maps.empty}
-- | Create a checked inference result
yieldChecked :: (Core.Term -> Core.Type -> Typing_.TypeSubst -> Compute.Flow t0 Typing_.InferenceResult)
yieldChecked term typ subst =
let iterm = (Substitution.substTypesInTerm subst term)
in
let itype = (Substitution.substInType subst typ)
in (Flows.pure (Typing_.InferenceResult {
Typing_.inferenceResultTerm = iterm,
Typing_.inferenceResultType = itype,
Typing_.inferenceResultSubst = subst,
Typing_.inferenceResultClassConstraints = Maps.empty}))
-- | Create a checked inference result with class constraints
yieldCheckedWithConstraints :: (Core.Term -> Core.Type -> Typing_.TypeSubst -> M.Map Core.Name Core.TypeVariableMetadata -> Compute.Flow t0 Typing_.InferenceResult)
yieldCheckedWithConstraints term typ subst constraints =
let iterm = (Substitution.substTypesInTerm subst term)
in
let itype = (Substitution.substInType subst typ)
in
let iconstraints = (Substitution.substInClassConstraints subst constraints)
in (Flows.pure (Typing_.InferenceResult {
Typing_.inferenceResultTerm = iterm,
Typing_.inferenceResultType = itype,
Typing_.inferenceResultSubst = subst,
Typing_.inferenceResultClassConstraints = iconstraints}))
-- | Create an inference result with debug output
yieldDebug :: (t0 -> t1 -> Core.Term -> Core.Type -> Typing_.TypeSubst -> Compute.Flow t2 Typing_.InferenceResult)
yieldDebug cx debugId term typ subst =
let rterm = (Substitution.substTypesInTerm subst term)
in
let rtyp = (Substitution.substInType subst typ)
in (Flows.bind (Annotations.debugIf debugId (Strings.cat [
"\n\tterm: ",
(Core__.term term),
"\n\ttyp: ",
(Core__.type_ typ),
"\n\tsubst: ",
(Typing.typeSubst subst),
"\n\trterm: ",
(Core__.term rterm),
"\n\trtyp: ",
(Core__.type_ rtyp)])) (\result -> Flows.pure (Typing_.InferenceResult {
Typing_.inferenceResultTerm = rterm,
Typing_.inferenceResultType = rtyp,
Typing_.inferenceResultSubst = subst,
Typing_.inferenceResultClassConstraints = Maps.empty})))
-- | Create an inference result with class constraints
yieldWithConstraints :: (Core.Term -> Core.Type -> Typing_.TypeSubst -> M.Map Core.Name Core.TypeVariableMetadata -> Typing_.InferenceResult)
yieldWithConstraints term typ subst constraints = Typing_.InferenceResult {
Typing_.inferenceResultTerm = (Substitution.substTypesInTerm subst term),
Typing_.inferenceResultType = (Substitution.substInType subst typ),
Typing_.inferenceResultSubst = subst,
Typing_.inferenceResultClassConstraints = constraints}