66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{- |

81d182b21020b815887e9057959228546cf61b6bChristian MaederModule : $Header$

81d182b21020b815887e9057959228546cf61b6bChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003

a39175891082dc8a598e5630e5558cb08b84ac0aChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederMaintainer : maeder@tzi.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : experimental

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederPortability : portable

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maedertype inference based on

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder<http://www.cs.fiu.edu/~smithg/papers/>

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder

5553cf7e344c2b385a72e1244b419e9986042b8eChristian MaederPrincipal Type Schemes for Functional Programs with Overloading and

5553cf7e344c2b385a72e1244b419e9986042b8eChristian MaederSubtyping, Geoffrey S. Smith, Science of Computer Programming 23(2-3),

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maederpp. 197-226, December 1994

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder-}

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maedermodule HasCASL.TypeCheck where

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederimport HasCASL.Unify

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederimport HasCASL.AsUtils

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maederimport HasCASL.Merge

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maederimport HasCASL.VarDecl

34b55522ba6fe2601e4ee37a9ba1fc4b1a0bf50bChristian Maederimport HasCASL.As

34b55522ba6fe2601e4ee37a9ba1fc4b1a0bf50bChristian Maederimport HasCASL.Le

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maederimport HasCASL.MixAna

34b55522ba6fe2601e4ee37a9ba1fc4b1a0bf50bChristian Maederimport HasCASL.TypeAna

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederimport HasCASL.MapTerm

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.Constrain

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maederimport HasCASL.ProgEq

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.MinType

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport qualified Common.Lib.Map as Map

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederimport qualified Common.Lib.Set as Set

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport qualified Common.Lib.Rel as Rel

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maederimport Common.Id

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Common.Result

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maederimport Common.PrettyPrint

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederimport Common.GlobalAnnotations

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.Lib.State

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Data.List as List

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Control.Exception(assert)

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersubstTerm :: Subst -> Term -> Term

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedersubstTerm s = mapTerm (id, subst s)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederresolveTerm :: GlobalAnnos -> Maybe Type -> Term -> State Env (Maybe Term)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederresolveTerm ga mt trm = do

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mtrm <- resolve ga trm

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case mtrm of

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder Nothing -> return Nothing

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder Just t -> typeCheck mt t

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaedercheckPattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)

6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaedercheckPattern ga pat = do

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder mPat <- resolvePattern ga pat

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder case mPat of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> return Nothing

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just np -> typeCheck Nothing np

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinstantiate :: TypeScheme -> State Env (Type, [Type], Constraints)

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maederinstantiate (TypeScheme tArgs t _) =

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do let ls = leaves (< 0) t -- generic vars

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder vs = map snd ls

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder ts <- toEnvState $ mkSubst vs

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder let s = Map.fromList $ zip (map fst ls) ts

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder (ats, cs) = unzip $ mapArgs s (zip (map fst vs) ts) tArgs

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder return (subst s t, ats, Set.fromList cs)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapArgs :: Subst -> [(Id, Type)] -> [TypeArg] -> [(Type, Constrain)]

f6fc70956d64365527d77a521a96f54a1cc18f91Christian MaedermapArgs s ts = foldr ( \ (TypeArg i _ vk _ _ _ _) l ->

51c65d5fb2d720dc77bc5cca15640cfa09711986Christian Maeder maybe l ( \ (_, t) -> (t, case vk of

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder MissingKind -> error "mapArgs"

51c65d5fb2d720dc77bc5cca15640cfa09711986Christian Maeder VarKind k -> Kinding t k

51c65d5fb2d720dc77bc5cca15640cfa09711986Christian Maeder Downset super -> Subtyping t $ subst s super) : l) $

51c65d5fb2d720dc77bc5cca15640cfa09711986Christian Maeder find ( \ (j, _) -> i == j) ts) []

f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederinstOpInfo :: OpInfo -> State Env (Type, [Type], Constraints, OpInfo)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederinstOpInfo oi = do

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder (ty, inst, cs) <- instantiate $ opType oi

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return (ty, inst, cs, oi)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederlookupError :: Type -> [OpInfo] -> String

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederlookupError ty ois =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder " with (maximal) type: " ++ showPretty ty "\n"

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ++ " known types:\n " ++

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder showSepList ("\n "++) (showPretty . opType) ois ""

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercheckList :: [Maybe Type] -> [Term]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -> State Env [(Subst, Constraints, [Type], [Term])]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercheckList [] [] = return [(eps, noC, [], [])]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercheckList (ty : rty) (trm : rt) = do

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fts <- infer ty trm >>= reduce False

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder combs <- mapM ( \ (sf, cs, tyf, tf) -> do

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder vs <- gets localVars

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder putLocalVars $ substVarTypes sf vs

998747cb2ee575cccdd7d865c95d0ef07516a6a5Christian Maeder rts <- checkList (map (fmap (subst sf)) rty) rt

07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder putLocalVars vs

07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder return $ map ( \ (sr, cr, tys, tts) ->

07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder (compSubst sf sr,

07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder substC sr cs `joinC` cr,

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder subst sr tyf : tys,

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder tf : tts)) rts) fts

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder return $ concat combs

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian MaedercheckList _ _ = error "checkList"

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder-- | reduce a substitution, if true try to find a monomorphic substitution

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maederreduce :: Bool -> [(Subst, Constraints, Type, Term)]

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder -> State Env [(Subst, Constraints, Type, Term)]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederreduce b alts = do

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder te <- get

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder combs <- mapM ( \ (s, cr, ty, tr) -> do

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder Result ds mc <- toEnvState $ shapeRel te cr

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder addDiags $ map (improveDiag tr) ds

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder return $ case mc of

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder Nothing -> []

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just (cs, qs, trel) -> let

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder s1 = compSubst s cs

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder ms = if b then monoSubsts te

fb8645096eb70aa243c146abe31d4173cfbe6e1aChristian Maeder (Rel.transClosure $ Rel.union (fromTypeMap $ typeMap te)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $ trel) (subst cs ty)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else eps

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder s2 = compSubst s1 ms

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder in [(s2, substC ms $ foldr ( \ (a, t) -> insertC

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder (Subtyping a t))

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder qs $ Rel.toList trel, subst s2 ty,

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder substTerm s2 tr)]) alts

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder return $ concat combs

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder

6b23467258cdc15e05f1845cd400d60ca6eba966Christian MaedertypeCheck :: Maybe Type -> Term -> State Env (Maybe Term)

6b23467258cdc15e05f1845cd400d60ca6eba966Christian MaedertypeCheck mt trm =

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder do alts <- infer mt trm >>= reduce True

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder te <- get

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let p = getRange trm

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if null alts then

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Error "no typing for" trm]

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return Nothing

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder else if null $ tail alts then do

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let (_, cs, ty, t) = head alts

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (ds, rcs) = simplify te cs

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder es = map ( \ d -> d {diagKind = Hint, diagPos = p}) ds

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder addDiags es

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder if Set.null rcs then return ()

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else addDiags [(mkDiag Error ("in term'"

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder ++ showPretty t "' of type '"

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder ++ showPretty ty "'\n unresolved constraints")

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder rcs){diagPos = p}]

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder return $ Just t

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else let alts3 = filter ( \ (_, cs, _, _) ->

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder Set.null $ snd $ simplify te cs) alts

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder falts = typeNub te q2p alts3 in

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder if null falts then do

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder addDiags [mkDiag Error "no constraint resolution for" trm]

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder addDiags $ map (\ (_, cs, _, _) -> (mkDiag Hint

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder "simplification failed for" cs){diagPos = p}) alts

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder return Nothing

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else if null $ tail falts then

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder let (_, _, _, t) = head falts in

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder return $ Just t

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder do addDiags [Diag Error

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder ("ambiguous typings \n " ++

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder showSepList ("\n " ++)

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder ( \ (n, t) -> shows n . (". " ++) . showPretty t)

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder (zip [1..(5::Int)] $ map ( \ (_,_,_,t) ->

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder t) falts) "")

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder p]

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder return Nothing

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaederfreshTypeVar :: Range -> State Env Type

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaederfreshTypeVar p =

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder do (var, c) <- toEnvState $ freshVar p

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder return $ TypeName var rStar c

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaederfreshVars :: [Term] -> State Env [Type]

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaederfreshVars l = mapM (freshTypeVar . getRange) l

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedersubstVarTypes :: Subst -> Map.Map Id VarDefn -> Map.Map Id VarDefn

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedersubstVarTypes s = Map.map ( \ (VarDefn t) -> VarDefn $ subst s t)

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder-- | infer type of application, if true consider lifting for lazy types

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaederinferAppl :: Range -> Maybe Type -> Term -> Term

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder -> State Env [(Subst, Constraints, Type, Term)]

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaederinferAppl ps mt t1 t2 = do

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder let origAppl = ApplTerm t1 t2 ps

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder aty <- freshTypeVar $ getRange t2

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder rty <- case mt of

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder Nothing -> freshTypeVar $ getRange t1

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder Just ty -> return ty

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder ops <- infer (Just $ mkFunArrType aty PFunArr rty) t1

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder >>= reduce False

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder te <- get

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder combs <- mapM ( \ (sf, cf, funty, tf) -> do

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder let (sfty, frty) = case getTypeAppl funty of

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder (topTy, [paty, prty]) |

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder lesserType te topTy (toType $ arrowId PFunArr) ->

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (paty, prty)

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder _ -> (subst sf aty, subst sf rty)

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder vs <- gets localVars

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder putLocalVars $ substVarTypes sf vs

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder args <- infer (Just sfty) t2 >>= reduce False

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder putLocalVars vs

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder let combs2 = map ( \ (sa, ca, _, ta) ->

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder let sr = compSubst sf sa

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder nTy = subst sa frty in

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder [(sr, joinC ca $ substC sa cf, nTy,

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder TypedTerm (ApplTerm tf ta ps)

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder Inferred nTy ps)]) args

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder return $ concat combs2) ops

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder let res = concat combs

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder if null res then

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder addDiags [case mt of

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder Nothing -> mkDiag Hint

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder "untypable application" origAppl

a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder Just ty -> mkDiag Hint

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder ("untypable application (with result type: "

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ++ showPretty ty ")\n")

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder origAppl]

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder else return ()

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder return res

6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedergetTypeOf :: Term -> Type

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedergetTypeOf trm = case trm of

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder TypedTerm _ q t _ -> case q of InType -> unitType

08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder _ -> t

34b55522ba6fe2601e4ee37a9ba1fc4b1a0bf50bChristian Maeder QualVar (VarDecl _ t _ _) -> t

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder QualOp _ _ (TypeScheme [] t _) _ -> t

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder TupleTerm ts _ -> if null ts then unitType

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else mkProductType (map getTypeOf ts)

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder QuantifiedTerm _ _ t _ -> getTypeOf t

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder LetTerm _ _ t _ -> getTypeOf t

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder AsPattern _ p _ -> getTypeOf p

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder _ -> error "getTypeOf"

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder-- | infer type of term, if true consider lifting for lazy types

34b55522ba6fe2601e4ee37a9ba1fc4b1a0bf50bChristian Maederinfer :: Maybe Type -> Term

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder -> State Env [(Subst, Constraints, Type, Term)]

167b6ed8639bce096380defb7311ded501ebb5daChristian Maederinfer mt trm = do

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder e <- get

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder tm <- gets typeMap

34b55522ba6fe2601e4ee37a9ba1fc4b1a0bf50bChristian Maeder as <- gets assumps

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder vs <- gets localVars

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder case trm of

a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder qv@(QualVar (VarDecl _ t _ _)) -> return $

a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder case mt of

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder Nothing -> [(eps, noC, t, qv)]

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder Just ty -> [(eps, insertC (Subtyping t ty) noC, t, qv)]

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder QualOp br (InstOpId i ts qs) sc ps -> do

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder (ty, inst, cs) <- instantiate sc

a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder let Result ds ms = mguList tm (if null ts then inst else ts) inst

a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder addDiags $ map (improveDiag trm) ds

a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder return $ case ms of

a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder Nothing -> []

a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder Just s ->

a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder let nTy = subst s ty

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ncs = substC s cs

a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder qv = TypedTerm (QualOp br

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (InstOpId i (map (subst s) inst) qs) sc ps)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Inferred nTy ps

a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder in case mt of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> [(s, ncs, nTy, qv)]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just inTy -> [(s, insertC (Subtyping nTy $ subst s inTy)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ncs, nTy, qv)]

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder ResolvedMixTerm i ts ps ->

f9d358050e368eef1dcb45565b921a70bc68ef2dMihai Codescu if null ts then case Map.lookup i vs of

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder Just (VarDefn t) -> infer mt $ QualVar $ VarDecl i t Other ps

d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder Nothing -> do

d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder let ois = opInfos $ Map.findWithDefault (OpInfos []) i as

a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder insts <- mapM instOpInfo ois

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder let ls = map ( \ (ty, is, cs, oi) ->

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder (eps, ty, is, case mt of

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder Just inTy -> insertC (Subtyping ty inTy) cs

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder Nothing -> cs, oi)) insts

405b95208385572f491e1e0207d8d14e31022fa6Christian Maeder if null ls then addDiags

f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu [Diag Hint

f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu ("no type match for: " ++ showId i "" ++ case mt of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> ""

8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian Maeder Just inTy -> '\n' : lookupError inTy ois) (posOfId i)]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else return ()

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return $ typeNub e q2p $ map

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ( \ (s, ty, is, cs, oi) ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let od = opDefn oi

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder br = case od of

599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder NoOpDefn v -> v

599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder Definition v _ -> v

599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder _ -> Op

599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder in (s, cs, ty, case opType oi of

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder sc@(TypeScheme [] sTy _) -> assert (sTy == ty) $

599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder QualOp br (InstOpId i [] nullRange) sc ps

599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder sc -> TypedTerm (QualOp br

599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder (InstOpId i is nullRange) sc ps)

599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder Inferred ty ps)) ls

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder else inferAppl ps mt (ResolvedMixTerm i [] ps)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $ mkTupleTerm ts ps

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ApplTerm t1 t2 ps -> inferAppl ps mt t1 t2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TupleTerm ts ps -> if null ts then return

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [(eps, case mt of

d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder Nothing -> noC

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just ty -> insertC (Subtyping unitType ty) noC,

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder unitType, trm)]

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder else do

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder ls <- checkList (map (const Nothing) ts) ts

d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder return $ map ( \ (su, cs, tys, trms) ->

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder let nTy = mkProductType tys in

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder (su, case mt of

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder Nothing -> cs

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder Just ty -> insertC (Subtyping nTy

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder $ subst su ty) cs, nTy,

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder assert (and $ zipWith (==) tys

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder $ map (subst su . getTypeOf) trms) $

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder mkTupleTerm trms ps)) ls

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder TypedTerm t qual ty ps -> do

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder case qual of

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder InType -> do

72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder vTy <- freshTypeVar ps

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder rs <- infer Nothing t

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder return $ map ( \ (s, cs, typ, tr) ->

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder let sTy = subst s ty in

d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder (s, insertC (Subtyping sTy vTy)

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder $ insertC (Subtyping typ vTy)

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder $ case mt of

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder Nothing -> cs

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder Just jTy -> insertC (Subtyping (subst s jTy)

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder unitType) cs,

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder unitType,

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder TypedTerm tr qual sTy ps)) rs

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder AsType -> do

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder vTy <- freshTypeVar ps

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder rs <- infer Nothing t

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder return $ map ( \ (s, cs, typ, tr) ->

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder let sTy = subst s ty in

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder (s, insertC (Subtyping sTy vTy)

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder $ insertC (Subtyping typ vTy)

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder $ case mt of

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder Nothing -> cs

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder Just jTy -> insertC (Subtyping sTy

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder $ subst s jTy) cs,

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder sTy, TypedTerm tr qual sTy ps)) rs

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder _ -> do

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder rs <- infer (Just ty) t

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder return $ map ( \ (s, cs, _, tr) ->

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder let sTy = subst s ty in

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder (s, case mt of

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder Nothing -> cs

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder Just jTy -> insertC (Subtyping sTy

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder $ subst s jTy) cs,

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder sTy, if getTypeOf tr == sTy then tr

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder else TypedTerm tr qual sTy ps)) rs

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder QuantifiedTerm quant decls t ps -> do

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder mapM_ addGenVarDecl decls

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder rs <- infer (Just unitType) t

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder putLocalVars vs

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder putTypeMap tm

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder return $ map ( \ (s, cs, typ, tr) ->

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder (s, case mt of

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder Nothing -> cs

0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian Maeder Just ty -> insertC (Subtyping (subst s ty)

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder unitType) cs,

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder typ, QuantifiedTerm quant decls tr ps)) rs

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder LambdaTerm pats part resTrm ps -> do

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder pvs <- freshVars pats

rty <- freshTypeVar $ getRange resTrm

let myty = getFunType rty part pvs

ls <- checkList (map Just pvs) pats

rs <- mapM ( \ ( s, cs, _, nps) -> do

mapM_ (addLocalVar True) $ concatMap extractVars nps

es <- infer (Just $ subst s rty) resTrm

putLocalVars vs

return $ map ( \ (s2, cr, _, rtm) ->

let s3 = compSubst s s2

typ = subst s3 myty in

(s3, joinC (substC s2 cs) $

case mt of

Nothing -> cr

Just ty -> insertC (Subtyping typ

$ subst s3 ty) cr,

typ, TypedTerm

(LambdaTerm nps part rtm ps)

Inferred typ ps)) es) ls

return $ concat rs

CaseTerm ofTrm eqs ps -> do

ts <- infer Nothing ofTrm

rty <- case mt of

Nothing -> freshTypeVar $ getRange trm

Just ty -> return ty

if null ts then addDiags [mkDiag Hint

"unresolved of-term in case" ofTrm]

else return ()

rs <- mapM ( \ (s1, cs, oty, otrm) -> do

es <- inferCaseEqs oty (subst s1 rty) eqs

return $ map ( \ (s2, cr, _, ty, nes) ->

(compSubst s1 s2,

substC s2 cs `joinC` cr, ty,

TypedTerm (CaseTerm otrm nes ps)

Inferred ty ps)) es) ts

return $ concat rs

LetTerm br eqs inTrm ps -> do

es <- inferLetEqs eqs

rs <- mapM ( \ (s1, cs, _, nes) -> do

mapM_ (addLocalVar True) $ concatMap

( \ (ProgEq p _ _) -> extractVars p) nes

ts <- infer mt inTrm

return $ map ( \ (s2, cr, ty, nt) ->

(compSubst s1 s2,

substC s2 cs `joinC` cr,

ty, assert (getTypeOf nt == ty) $

LetTerm br nes nt ps)) ts) es

putLocalVars vs

return $ concat rs

AsPattern (VarDecl v _ ok qs) pat ps -> do

pats <- infer mt pat

return $ map ( \ (s1, cs, t1, p1) -> (s1, cs, t1,

AsPattern (VarDecl v t1 ok qs) p1 ps)) pats

_ -> do ty <- freshTypeVar $ getRange trm

addDiags [mkDiag Error "unexpected term" trm]

return [(eps, noC, ty, trm)]

inferLetEqs :: [ProgEq] -> State Env [(Subst, Constraints, [Type], [ProgEq])]

inferLetEqs es = do

let pats = map (\ (ProgEq p _ _) -> p) es

trms = map (\ (ProgEq _ t _) -> t) es

qs = map (\ (ProgEq _ _ q) -> q) es

do vs <- gets localVars

newPats <- checkList (map (const Nothing) pats) pats

combs <- mapM ( \ (sf, pcs, tys, pps) -> do

mapM_ (addLocalVar True) $ concatMap extractVars pps

newTrms <- checkList (map Just tys) trms

return $ map ( \ (sr, tcs, tys2, tts ) ->

(compSubst sf sr,

joinC tcs $ substC sr pcs, tys2,

zipWith3 ( \ p t q -> ProgEq (substTerm sr p) t q)

pps tts qs)) newTrms) newPats

putLocalVars vs

return $ concat combs

inferCaseEq :: Type -> Type -> ProgEq

-> State Env [(Subst, Constraints, Type, Type, ProgEq)]

inferCaseEq pty tty (ProgEq pat trm ps) = do

pats1 <- infer (Just pty) pat >>= reduce False

e <- get

let pats = filter ( \ (_, _, _, p) -> isPat e p) pats1

if null pats then addDiags [mkDiag Hint "unresolved case pattern" pat]

else return ()

vs <- gets localVars

es <- mapM ( \ (s, cs, ty, p) -> do

mapM_ (addLocalVar True) $ extractVars p

ts <- infer (Just $ subst s tty) trm >>= reduce False

putLocalVars vs

return $ map ( \ (st, cr, tyt, t) ->

(compSubst s st,

substC st cs `joinC` cr,

subst st ty, tyt,

ProgEq p t ps)) ts) pats

return $ concat es

inferCaseEqs :: Type -> Type -> [ProgEq]

-> State Env [(Subst, Constraints, Type, Type, [ProgEq])]

inferCaseEqs pty tTy [] = return [(eps, noC, pty, tTy, [])]

inferCaseEqs pty tty (eq:eqs) = do

fts <- inferCaseEq pty tty eq

rs <- mapM (\ (_, cs, pty1, tty1, ne) -> do

rts <- inferCaseEqs pty1 tty1 eqs

return $ map ( \ (s2, cr, pty2, tty2, nes) ->

(s2,

substC s2 cs `joinC` cr,

pty2, tty2, ne:nes)) rts) fts

return $ concat rs