TypeCheck.hs revision b603f34b79bc0992e5d74f484e5bdc9f9c2346c6
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiMaintainer : maeder@tzi.de
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuStability : experimental
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedertype inference based on
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiPrincipal Type Schemes for Functional Programs with Overloading and
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederSubtyping, Geoffrey S. Smith, Science of Computer Programming 23(2-3),
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederpp. 197-226, December 1994
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Common.Lib.Map as Map
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Common.Lib.Set as Set
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Common.Lib.Rel as Rel
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedersubstTerm :: Subst -> Term -> Term
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedersubstTerm s = mapTerm (id, subst s)
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederresolveTerm :: GlobalAnnos -> Maybe Type -> Term -> State Env (Maybe Term)
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederresolveTerm ga mt trm = do
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder mtrm <- resolve ga trm
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder Nothing -> return Nothing
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder Just t -> typeCheck mt t
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederinstantiate :: TypeScheme -> State Env (Type, [Type], Constraints)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederinstantiate (TypeScheme tArgs t _) =
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder do let ls = leaves (< 0) t -- generic vars
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder vs = map snd ls
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder ts <- toEnvState $ mkSubst vs
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder let s = Map.fromList $ zip (map fst ls) ts
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder (ats, cs) = unzip $ mapArgs s (zip (map fst vs) ts) tArgs
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder return (subst s t, ats, Set.fromList cs)
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedermapArgs :: Subst -> [(Id, Type)] -> [TypeArg] -> [(Type, Constrain)]
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedermapArgs s ts = foldr ( \ (TypeArg i _ vk _ _ _ _) l ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder maybe l ( \ (_, t) -> (t, case vk of
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder MissingKind -> error "mapArgs"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder VarKind k -> Kinding t k
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Downset super -> Subtyping t $ subst s super) : l) $
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder find ( \ (j, _) -> i == j) ts) []
5e46b572ed576c0494768998b043d9d340594122Till MossakowskiinstOpInfo :: OpInfo -> State Env (Type, [Type], Constraints, OpInfo)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WanginstOpInfo oi = do
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder (ty, inst, cs) <- instantiate $ opType oi
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder return (ty, inst, cs, oi)
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian MaederlookupError :: Type -> [OpInfo] -> String
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WanglookupError ty ois =
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder " with (maximal) type: " ++ showDoc ty "\n"
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder ++ " known types:\n " ++
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder showSepList ("\n "++) (showDoc . opType) ois ""
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicheckList :: [Maybe Type] -> [Term]
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder -> State Env [(Subst, Constraints, [Type], [Term])]
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedercheckList [] [] = return [(eps, noC, [], [])]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedercheckList (ty : rty) (trm : rt) = do
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder fts <- infer ty trm >>= reduce False
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder combs <- mapM ( \ (sf, cs, tyf, tf) -> do
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich vs <- gets localVars
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder putLocalVars $ substVarTypes sf vs
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich rts <- checkList (map (fmap (subst sf)) rty) rt
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder putLocalVars vs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return $ map ( \ (sr, cr, tys, tts) ->
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (compSubst sf sr,
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu substC sr cs `joinC` cr,
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder subst sr tyf : tys,
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder tf : tts)) rts) fts
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ concat combs
8e80792f474d154ff11762fac081a422e34f1accChristian MaedercheckList _ _ = error "checkList"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- | reduce a substitution, if true try to find a monomorphic substitution
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederreduce :: Bool -> [(Subst, Constraints, Type, Term)]
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -> State Env [(Subst, Constraints, Type, Term)]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederreduce b alts = do
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder combs <- mapM ( \ (s, cr, ty, tr) -> do
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder Result ds mc <- toEnvState $ shapeRel te cr
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder addDiags $ map (improveDiag tr) ds
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder return $ case mc of
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Nothing -> []
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Just (cs, qs, trel) -> let
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder s1 = compSubst s cs
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder ms = if b then monoSubsts te
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder (Rel.transClosure $ Rel.union (fromTypeMap $ typeMap te)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder $ trel) (subst cs ty)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder s2 = compSubst s1 ms
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder in [(s2, substC ms $ foldr ( \ (a, t) -> insertC
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder (Subtyping a t))
e6dccba746efe07338d3107fed512e713fd50b28Christian Maeder qs $ Rel.toList trel, subst s2 ty,
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder substTerm s2 tr)]) alts
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder return $ concat combs
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaedertypeCheck :: Maybe Type -> Term -> State Env (Maybe Term)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedertypeCheck mt trm =
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder do alts <- infer mt trm >>= reduce True
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder let p = getRange trm
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maeder ga = globAnnos te
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder if null alts then
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder do addDiags [mkNiceDiag ga Error "no typing for" trm]
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder return Nothing
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder else if null $ tail alts then do
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder let (_, cs, ty, t) = head alts
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder (ds, rcs) = simplify te cs
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder es = map ( \ d -> d {diagKind = Hint, diagPos = p}) ds
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder if Set.null rcs then return ()
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder else addDiags [(mkDiag Error ("in term '"
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder ++ showGlobalDoc ga t "' of type '"
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder ++ showDoc ty "'\n unresolved constraints")
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder rcs){diagPos = p}]
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder return $ Just t
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder else let alts3 = filter ( \ (_, cs, _, _) ->
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder Set.null $ snd $ simplify te cs) alts
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder falts = typeNub te q2p alts3 in
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder if null falts then do
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder addDiags [mkNiceDiag ga Error
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder "no constraint resolution for" trm]
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder addDiags $ map (\ (_, cs, _, _) -> (mkDiag Hint
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder "simplification failed for" cs){diagPos = p}) alts
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder return Nothing
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder else if null $ tail falts then
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder let (_, _, _, t) = head falts in
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ Just t
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder do addDiags [Diag Error
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder ("ambiguous typings \n " ++
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder showSepList ("\n " ++)
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder ( \ (n, t) -> shows n . (". " ++) . showDoc t)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (zip [1..(5::Int)] $ map ( \ (_,_,_,t) ->
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder t) falts) "")
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder return Nothing
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederfreshTypeVar :: Range -> State Env Type
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederfreshTypeVar p =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do (var, c) <- toEnvState $ freshVar p
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return $ TypeName var rStar c
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskifreshVars :: [Term] -> State Env [Type]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskifreshVars l = mapM (freshTypeVar . getRange) l
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedersubstVarTypes :: Subst -> Map.Map Id VarDefn -> Map.Map Id VarDefn
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedersubstVarTypes s = Map.map ( \ (VarDefn t) -> VarDefn $ subst s t)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- | infer type of application, if true consider lifting for lazy types
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederinferAppl :: Range -> Maybe Type -> Term -> Term
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -> State Env [(Subst, Constraints, Type, Term)]
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederinferAppl ps mt t1 t2 = do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let origAppl = ApplTerm t1 t2 ps
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder aty <- freshTypeVar $ getRange t2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder rty <- case mt of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Nothing -> freshTypeVar $ getRange t1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Just ty -> return ty
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder ops <- infer (Just $ mkFunArrType aty PFunArr rty) t1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder >>= reduce False
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let ga = globAnnos te
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder combs <- mapM ( \ (sf, cf, funty, tf) -> do
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let (sfty, frty) = case getTypeAppl funty of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (topTy, [paty, prty]) |
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder lesserType te topTy (toType $ arrowId PFunArr) ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder _ -> (subst sf aty, subst sf rty)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder vs <- gets localVars
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder putLocalVars $ substVarTypes sf vs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder args <- infer (Just sfty) t2 >>= reduce False
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder putLocalVars vs
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski let combs2 = map ( \ (sa, ca, _, ta) ->
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder let sr = compSubst sf sa
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder nTy = subst sa frty in
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder [(sr, joinC ca $ substC sa cf, nTy,
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder TypedTerm (ApplTerm tf ta ps)
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Inferred nTy ps)]) args
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder return $ concat combs2) ops
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder let res = concat combs
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder if null res then
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz addDiags [case mt of
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Nothing -> mkNiceDiag ga Hint
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder "untypable application" origAppl
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz Just ty -> mkNiceDiag ga Hint
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder ("untypable application (with result type: "
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder ++ showDoc ty ")\n")
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder else return ()
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaedergetTypeOf :: Term -> Type
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaedergetTypeOf trm = case trm of
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder TypedTerm _ q t _ -> case q of InType -> unitType
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz QualVar (VarDecl _ t _ _) -> t
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz QualOp _ _ (TypeScheme [] t _) _ -> t
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz TupleTerm ts _ -> if null ts then unitType
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz else mkProductType (map getTypeOf ts)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder QuantifiedTerm _ _ t _ -> getTypeOf t
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder LetTerm _ _ t _ -> getTypeOf t
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder AsPattern _ p _ -> getTypeOf p
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder _ -> error "getTypeOf"
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- | infer type of term, if true consider lifting for lazy types
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maederinfer :: Maybe Type -> Term
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> State Env [(Subst, Constraints, Type, Term)]
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maederinfer mt trm = do
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder let tm = typeMap e
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder as = assumps e
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder vs = localVars e
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder ga = globAnnos e
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder qv@(QualVar (VarDecl _ t _ _)) -> return $
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Nothing -> [(eps, noC, t, qv)]
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Just ty -> [(eps, insertC (Subtyping t ty) noC, t, qv)]
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder QualOp br (InstOpId i ts qs) sc ps -> do
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder (ty, inst, cs) <- instantiate sc
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder let Result ds ms = mguList tm (if null ts then inst else ts) inst
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder addDiags $ map (improveDiag trm) ds
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder return $ case ms of
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Nothing -> []
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder let nTy = subst s ty
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder ncs = substC s cs
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder qv = TypedTerm (QualOp br
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder (InstOpId i (map (subst s) inst) qs) sc ps)
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder Inferred nTy ps
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder in case mt of
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Nothing -> [(s, ncs, nTy, qv)]
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder Just inTy -> [(s, insertC (Subtyping nTy $ subst s inTy)
4e144aa4be1f50519f8fa377a7883edfbc76d406Christian Maeder ncs, nTy, qv)]
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder ResolvedMixTerm i ts ps ->
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder if null ts then case Map.lookup i vs of
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Just (VarDefn t) -> infer mt $ QualVar $ VarDecl i t Other ps
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Nothing -> do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let ois = opInfos $ Map.findWithDefault (OpInfos []) i as
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder insts <- mapM instOpInfo ois
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let ls = map ( \ (ty, is, cs, oi) ->
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder (eps, ty, is, case mt of
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Just inTy -> insertC (Subtyping ty inTy) cs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Nothing -> cs, oi)) insts
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder if null ls then addDiags
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder ("no type match for: " ++ showId i "" ++ case mt of
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Nothing -> ""
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Just inTy -> '\n' : lookupError inTy ois) (posOfId i)]
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder else return ()
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder return $ typeNub e q2p $ map
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder ( \ (s, ty, is, cs, oi) ->
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder let od = opDefn oi
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder br = case od of
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder NoOpDefn v -> v
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Definition v _ -> v
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in (s, cs, ty, case opType oi of
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder sc@(TypeScheme [] sTy _) -> assert (sTy == ty) $
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder QualOp br (InstOpId i [] nullRange) sc ps
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder sc -> TypedTerm (QualOp br
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (InstOpId i is nullRange) sc ps)
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder Inferred ty ps)) ls
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder else inferAppl ps mt (ResolvedMixTerm i [] ps)
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder $ mkTupleTerm ts ps
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder ApplTerm t1 t2 ps -> inferAppl ps mt t1 t2
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder TupleTerm ts ps -> if null ts then return
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder [(eps, case mt of
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Nothing -> noC
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Just ty -> insertC (Subtyping unitType ty) noC,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder unitType, trm)]
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ls <- checkList (map (const Nothing) ts) ts
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder return $ map ( \ (su, cs, tys, trms) ->
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder let nTy = mkProductType tys in
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder (su, case mt of
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Nothing -> cs
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Just ty -> insertC (Subtyping nTy
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder $ subst su ty) cs, nTy,
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder assert (and $ zipWith (==) tys
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder $ map (subst su . getTypeOf) trms) $
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder mkTupleTerm trms ps)) ls
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder TypedTerm t qual ty ps -> do
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder vTy <- freshTypeVar ps
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder rs <- infer Nothing t
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder return $ map ( \ (s, cs, typ, tr) ->
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let sTy = subst s ty in
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (s, insertC (Subtyping sTy vTy)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder $ insertC (Subtyping typ vTy)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Nothing -> cs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Just jTy -> insertC (Subtyping (subst s jTy)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder unitType) cs,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder TypedTerm tr qual sTy ps)) rs
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder vTy <- freshTypeVar ps
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rs <- infer Nothing t
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return $ map ( \ (s, cs, typ, tr) ->
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let sTy = subst s ty in
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder (s, insertC (Subtyping sTy vTy)
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder $ insertC (Subtyping typ vTy)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Nothing -> cs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just jTy -> insertC (Subtyping sTy
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder $ subst s jTy) cs,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder sTy, TypedTerm tr qual sTy ps)) rs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rs <- infer (Just ty) t
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return $ map ( \ (s, cs, _, tr) ->
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let sTy = subst s ty in
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (s, case mt of
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Nothing -> cs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Just jTy -> insertC (Subtyping sTy
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder $ subst s jTy) cs,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder sTy, if getTypeOf tr == sTy then tr
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder else TypedTerm tr qual sTy ps)) rs
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder QuantifiedTerm quant decls t ps -> do
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder mapM_ addGenVarDecl decls
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rs <- infer (Just unitType) t
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder putLocalVars vs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder putTypeMap tm
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ map ( \ (s, cs, typ, tr) ->
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (s, case mt of
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Nothing -> cs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Just ty -> insertC (Subtyping (subst s ty)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder unitType) cs,
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder typ, QuantifiedTerm quant decls tr ps)) rs
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder LambdaTerm pats part resTrm ps -> do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder pvs <- freshVars pats
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rty <- freshTypeVar $ getRange resTrm
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let myty = getFunType rty part pvs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ls <- checkList (map Just pvs) pats
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rs <- mapM ( \ ( s, cs, _, nps) -> do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder mapM_ (addLocalVar True) $ concatMap extractVars nps
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder es <- infer (Just $ subst s rty) resTrm
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder putLocalVars vs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return $ map ( \ (s2, cr, _, rtm) ->
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let s3 = compSubst s s2
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder typ = subst s3 myty in
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (s3, joinC (substC s2 cs) $
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Nothing -> cr
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Just ty -> insertC (Subtyping typ
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder $ subst s3 ty) cr,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder typ, TypedTerm
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (LambdaTerm nps part rtm ps)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Inferred typ ps)) es) ls
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return $ concat rs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder CaseTerm ofTrm eqs ps -> do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ts <- infer Nothing ofTrm
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder rty <- case mt of
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder Nothing -> freshTypeVar $ getRange trm
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder Just ty -> return ty
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder if null ts then addDiags [mkNiceDiag ga Hint
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder "unresolved of-term in case" ofTrm]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder else return ()
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rs <- mapM ( \ (s1, cs, oty, otrm) -> do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder es <- inferCaseEqs oty (subst s1 rty) eqs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return $ map ( \ (s2, cr, _, ty, nes) ->
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (compSubst s1 s2,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder substC s2 cs `joinC` cr, ty,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder TypedTerm (CaseTerm otrm nes ps)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Inferred ty ps)) es) ts
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return $ concat rs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder LetTerm br eqs inTrm ps -> do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder es <- inferLetEqs eqs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rs <- mapM ( \ (s1, cs, _, nes) -> do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder mapM_ (addLocalVar True) $ concatMap
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ( \ (ProgEq p _ _) -> extractVars p) nes
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ts <- infer mt inTrm
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return $ map ( \ (s2, cr, ty, nt) ->
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (compSubst s1 s2,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder substC s2 cs `joinC` cr,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ty, assert (getTypeOf nt == ty) $
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder LetTerm br nes nt ps)) ts) es
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder putLocalVars vs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return $ concat rs
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder AsPattern (VarDecl v _ ok qs) pat ps -> do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder pats <- infer mt pat
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return $ map ( \ (s1, cs, t1, p1) -> (s1, cs, t1,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder AsPattern (VarDecl v t1 ok qs) p1 ps)) pats
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder _ -> do ty <- freshTypeVar $ getRange trm
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder addDiags [mkNiceDiag ga Error "unexpected term" trm]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return [(eps, noC, ty, trm)]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederinferLetEqs :: [ProgEq] -> State Env [(Subst, Constraints, [Type], [ProgEq])]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederinferLetEqs es = do
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder let pats = map (\ (ProgEq p _ _) -> p) es
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder trms = map (\ (ProgEq _ t _) -> t) es
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder qs = map (\ (ProgEq _ _ q) -> q) es
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder do vs <- gets localVars
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder newPats <- checkList (map (const Nothing) pats) pats
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder combs <- mapM ( \ (sf, pcs, tys, pps) -> do
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder mapM_ (addLocalVar True) $ concatMap extractVars pps
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder newTrms <- checkList (map Just tys) trms
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder return $ map ( \ (sr, tcs, tys2, tts ) ->
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder (compSubst sf sr,
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder joinC tcs $ substC sr pcs, tys2,
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder zipWith3 ( \ p t q -> ProgEq (substTerm sr p) t q)
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder pps tts qs)) newTrms) newPats
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder putLocalVars vs
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder return $ concat combs
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederinferCaseEq :: Type -> Type -> ProgEq
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -> State Env [(Subst, Constraints, Type, Type, ProgEq)]
a74f814d3b445eadad6f68737a98a7a303698affChristian MaederinferCaseEq pty tty (ProgEq pat trm ps) = do
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder pats1 <- infer (Just pty) pat >>= reduce False
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder let pats = filter ( \ (_, _, _, p) -> isPat e p) pats1
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder ga = globAnnos e
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder if null pats then addDiags [mkNiceDiag ga Hint
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder "unresolved case pattern" pat]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder else return ()
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder vs <- gets localVars
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder es <- mapM ( \ (s, cs, ty, p) -> do
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder mapM_ (addLocalVar True) $ extractVars p
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder ts <- infer (Just $ subst s tty) trm >>= reduce False
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder putLocalVars vs
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder return $ map ( \ (st, cr, tyt, t) ->
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder (compSubst s st,
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder substC st cs `joinC` cr,
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder subst st ty, tyt,
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder ProgEq p t ps)) ts) pats
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return $ concat es
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederinferCaseEqs :: Type -> Type -> [ProgEq]
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder -> State Env [(Subst, Constraints, Type, Type, [ProgEq])]
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaederinferCaseEqs pty tTy [] = return [(eps, noC, pty, tTy, [])]
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaederinferCaseEqs pty tty (eq:eqs) = do
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder fts <- inferCaseEq pty tty eq
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder rs <- mapM (\ (_, cs, pty1, tty1, ne) -> do
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder rts <- inferCaseEqs pty1 tty1 eqs
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder return $ map ( \ (s2, cr, pty2, tty2, nes) ->
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder substC s2 cs `joinC` cr,
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder pty2, tty2, ne:nes)) rts) fts
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return $ concat rs