TypeCheck.hs revision eca29a7be76eb73944ec19b06eda3d6a9e6e543d
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$
5ba323da9f037264b4a356085e844889aedeac23Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
c58a94c44b76b072ace930f2126c889c0b64cb2aChristian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederMaintainer : maeder@tzi.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : experimental
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : portable
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maedertype inference
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport qualified Common.Lib.Map as Map
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedersubstTerm :: Subst -> Term -> Term
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedersubstTerm s = mapTerm (id, subst s)
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian MaederresolveTerm :: GlobalAnnos -> Maybe Type -> Term -> State Env (Maybe Term)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederresolveTerm ga mt trm = do
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder mtrm <- resolve ga trm
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Nothing -> return Nothing
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder Just t -> typeCheck infer mt t
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedercheckPattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedercheckPattern ga pat = do
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder mPat <- resolvePattern ga pat
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder Nothing -> return Nothing
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder (np, _) <- extractBindings p
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder typeCheck inferPat Nothing np
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederfreshInstList :: TypeScheme -> State Int (Type, [Type])
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederfreshInstList (TypeScheme tArgs (_ :=> t) _) =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder do m <- mkSubst tArgs
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder return (subst (Map.fromList m) t, map snd m)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederinstantiate :: OpInfo -> State Env (Type, [Type], OpInfo)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederinstantiate oi = do
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder (ty, inst) <- toEnvState $ freshInstList $ opType oi
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder return (ty, inst, oi)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederlookupError :: Type -> [OpInfo] -> String
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederlookupError ty ois =
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder " with type: " ++ showPrettyWithPos ty "\n"
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder ++ " known types:\n " ++
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder showSepList ("\n "++) (showPrettyWithPos . opType) ois ""
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian MaedercheckList :: (Maybe Type -> a -> State Env [(Subst, Type, a)])
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder -> [Maybe Type] -> [a] -> State Env [(Subst, [Type], [a])]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedercheckList _ [] [] = return [(eps, [], [])]
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian MaedercheckList inf (ty : rty) (trm : rt) = do
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder fts <- inf ty trm
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder combs <- mapM ( \ (sf, tyf, tf) -> do
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder rts <- checkList inf (map (fmap (subst sf)) rty) rt
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder return $ map ( \ (sr, tys, tts) ->
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder (compSubst sf sr, subst sr tyf : tys,
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder tf : tts)) rts) fts
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder return $ concat combs
27912d626bf179b82fcb337077e5cd9653bb71cfChristian MaedercheckList _ _ _ = error "checkList"
cf3232cec840a6945667bdb06f5b47b22243bc8fChristian MaedertypeCheck :: (Maybe Type -> Term -> State Env [(Subst, Type, Term)])
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder -> Maybe Type -> Term -> State Env (Maybe Term)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedertypeCheck inf mt trm =
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder do alts <- inf mt trm
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder if null alts then
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder do addDiags [mkDiag Error "no typing for" trm]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder return Nothing
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder else if null $ tail alts then
5ba323da9f037264b4a356085e844889aedeac23Christian Maeder let (s,_,t) = head alts in
5ba323da9f037264b4a356085e844889aedeac23Christian Maeder return $ Just $ substTerm s t
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder else do addDiags [Diag Error
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder ("ambiguous typings \n " ++
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder showSepList ("\n "++)
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder showPrettyWithPos
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder (take 5 $ map ( \ (s,_,t) -> substTerm s t) alts) "")
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder $ getMyPos trm]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder return Nothing
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederfreshTypeVar :: State Env Type
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederfreshTypeVar = do var <- toEnvState freshVar
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return $ TypeName var star 1
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederfreshVars :: [a] -> State Env [Type]
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederfreshVars l = mapM (const freshTypeVar) l
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederinferAppl :: (Maybe Type -> Term -> State Env [(Subst, Type, Term)]) -> [Pos]
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian Maeder -> Maybe Type -> Term -> Term -> State Env [(Subst, Type, Term)]
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian MaederinferAppl inf ps mt t1 t2 = do
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian Maeder aty <- freshTypeVar
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian Maeder rty <- case mt of
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian Maeder Nothing -> freshTypeVar
230aa1e8c53fcaffd75814c7d86bd37c8012596aChristian Maeder Just ty -> return ty
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ops <- inf (Just $ FunType aty PFunArr rty []) t1
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder combs <- mapM ( \ (sf, _, tf) -> do
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder args <- inf (Just $ subst sf aty) t2
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder return $ map ( \ (sa, _, ta) ->
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder let s = compSubst sf sa in
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder (s, subst s rty,
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ApplTerm tf ta ps)) args) ops
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder let res = concat combs
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder origAppl = ApplTerm t1 t2 ps
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder if null res then
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder addDiags [case mt of
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder Nothing -> mkDiag Error
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder "wrongly typed application" origAppl
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder Just ty -> mkDiag Hint
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder ("wrong result type "
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ++ showPrettyWithPos ty "\n for application")
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder else return ()
7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maederinfer :: Maybe Type -> Term -> State Env [(Subst, Type, Term)]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederinfer mt trm = do
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder tm <- gets typeMap
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder let mUnify = mgu tm mt . Just
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder uniDiags = addDiags . map (improveDiag trm)
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder as <- gets assumps
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder QualVar v t ps -> do
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder let Result ds ms = mUnify t
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Nothing -> return []
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Just s -> let ty = (subst s t) in
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder return [(s, ty, QualVar v ty ps)]
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder QualOp b (InstOpId i ts qs) sc ps -> do
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder (ty, inst) <- toEnvState $ freshInstList sc
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder let Result ds ms = mgu tm (mt, if null ts then inst else ts)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder (Just ty, inst)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Nothing -> return []
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder Just s -> return [(s, subst s ty, QualOp b
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder (InstOpId i (map (subst s) inst) qs)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ResolvedMixTerm i ts ps ->
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder if null ts then do
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder let ois = opInfos $ Map.findWithDefault (OpInfos []) i as
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder insts <- mapM instantiate ois
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder ls <- case mt of
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder Nothing -> return $ map ( \ (ty, is, oi)
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder -> (eps, ty, is, oi)) insts
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Just inTy -> do
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder let rs = concatMap ( \ (ty, is, oi) ->
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder let Result _ ms = mgu tm inTy ty in
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder case ms of Nothing -> []
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Just s -> [(s, ty,
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder map (subst s) is
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , oi)]) insts
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder if null rs then
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder addDiags [Diag Hint
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ("no type match for: " ++ showId i "\n"
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ++ lookupError inTy ois)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder (posOfId i) ]
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder else return ()
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder return $ map ( \ (s, ty, is, oi) ->
c9892acbf03a509d874ac6d79b9a2cb09042e0dcChristian Maeder case opDefn oi of
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder VarDefn -> (s, ty, QualVar i ty ps)
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder x -> let br = case x of
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder NoOpDefn b -> b
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Definition b _ -> b
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder QualOp br (InstOpId i is [])
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder (opType oi) ps)) ls
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder else infer mt $ ApplTerm (ResolvedMixTerm i [] ps)
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder (mkTupleTerm ts ps) ps
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ApplTerm t1 t2 ps -> inferAppl infer ps
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder TupleTerm ts ps ->
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder Nothing -> do
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder ls <- checkList infer (map (const Nothing) ts) ts
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder return $ map ( \ (su, tys, trms) ->
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder (su, mkProductType tys ps,
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder mkTupleTerm trms ps)) ls
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder Just ty -> do
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder vs <- freshVars ts
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder let pt = mkProductType vs []
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder Result ds ms = mgu tm ty pt
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder Nothing -> return []
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ls <- checkList infer (map (Just . subst s) vs) ts
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder return $ map ( \ (su, tys, trms) ->
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder (compSubst s su, mkProductType tys ps,
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder mkTupleTerm trms ps)) ls
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder TypedTerm t qual ty ps -> do
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder let Result ds ms = mUnify ty
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Nothing -> return []
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder rs <- infer (Just $ subst s ty) t
facf15c975d25ca5d31d8f84bf48f09d1d951ad6Christian Maeder return $ map ( \ (s2, typ, tr) ->
facf15c975d25ca5d31d8f84bf48f09d1d951ad6Christian Maeder (compSubst s s2, typ,
facf15c975d25ca5d31d8f84bf48f09d1d951ad6Christian Maeder TypedTerm tr qual ty ps)) rs
facf15c975d25ca5d31d8f84bf48f09d1d951ad6Christian Maeder let Result ds ms = mUnify logicalType
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder Nothing -> return []
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder rs <- infer Nothing t -- Nothing
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder return $ map ( \ (s2, _, tr) ->
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder (compSubst s s2, logicalType,
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder TypedTerm tr qual ty ps)) rs
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder let Result ds ms = mUnify ty
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Nothing -> return []
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder rs <- infer Nothing t -- Nothing
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder return $ map ( \ (s2, _, tr) ->
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder (compSubst s s2, ty,
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder TypedTerm tr qual ty ps)) rs
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder QuantifiedTerm quant decls t ps -> do
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder mapM_ addGenVarDecl decls
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder let Result ds ms = mUnify logicalType
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Nothing -> return []
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder rs <- infer (Just logicalType) t
de2f13b8310de00ca228385b1530660e036054c2Christian Maeder putAssumps as
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder return $ map ( \ (s, typ, tr) ->
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder (s, typ, QuantifiedTerm quant decls tr ps)) rs
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder LambdaTerm pats part resTrm ps -> do
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder vs <- freshVars pats
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder rty <- freshTypeVar
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder let fty l = if null l then rty else
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder FunType (head l) PFunArr (fty $ tail l) []
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder myty = fty vs
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Result ds ms = mUnify myty
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder Nothing -> return []
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder ls <- checkList inferPat (map (Just . subst s) vs) pats
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder rs <- mapM ( \ ( s2, _, nps) -> do
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder bs <- mapM extractBindings nps
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder mapM_ addVarDecl (concatMap snd bs)
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder let newS = compSubst s s2
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder es <- infer (Just $ subst newS rty) resTrm
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder putAssumps as
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder return $ map ( \ (s3, _, rtm) ->
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder (compSubst newS s3,
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder subst s3 (subst newS myty),
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder LambdaTerm nps part rtm ps)) es) ls
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder return $ concat rs
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder CaseTerm ofTrm eqs ps -> do
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder ts <- infer Nothing ofTrm
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder rty <- case mt of
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Nothing -> freshTypeVar
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Just ty -> return ty
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder if null ts then addDiags [mkDiag Error
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder "unresolved of-term in case" ofTrm]
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder else return ()
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder rs <- mapM ( \ (s1, oty, otrm) -> do
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder es <- inferCaseEqs oty (subst s1 rty) eqs
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder return $ map ( \ (s2, _, ty, nes) ->
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder (compSubst s1 s2, ty,
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder CaseTerm otrm nes ps)) es) ts
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder return $ concat rs
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder LetTerm b eqs inTrm ps -> do
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder es <- checkList inferLetEq (map (const Nothing) eqs) eqs
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder rs <- mapM ( \ (s1, _, nes) -> do
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder ts <- infer mt inTrm
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder return $ map ( \ (s2, ty, nt) ->
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder (compSubst s1 s2, ty,
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder LetTerm b nes nt ps)) ts) es
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder putAssumps as
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder return $ concat rs
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder _ -> do ty <- freshTypeVar
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder addDiags [mkDiag Error "unexpected term" trm]
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder return [(eps, ty, trm)]
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaederinferLetEq :: Maybe Type -> ProgEq -> State Env [(Subst, Type, ProgEq)]
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaederinferLetEq _ (ProgEq pat trm ps) = do
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ts <- infer Nothing trm
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder nps <- mapM ( \ (s2, tyt, nt) -> do
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder pps <- inferPat (Just tyt) pat
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder mapM ( \ (s3, _, pp) -> do
f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu (_, nbs) <- extractBindings pp
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder mapM_ addVarDecl nbs
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder return (compSubst s2 s3, tyt, ProgEq pp nt ps)) pps) ts
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder return $ concat nps
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder-- | type check patterns
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederinferPat :: Maybe Type -> Pattern -> State Env [(Subst, Type, Pattern)]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederinferPat = infer
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederinferCaseEq :: Type -> Type -> ProgEq
f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu -> State Env [(Subst, Type, Type, ProgEq)]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederinferCaseEq pty tty (ProgEq pat trm ps) = do
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder as <- gets assumps
2faad0c99d17a6ef53a464864caccbb20cf48409Christian Maeder let newAs = filterAssumps ( \ o -> case opDefn o of
2faad0c99d17a6ef53a464864caccbb20cf48409Christian Maeder ConstructData _ -> True
2faad0c99d17a6ef53a464864caccbb20cf48409Christian Maeder VarDefn -> True
2faad0c99d17a6ef53a464864caccbb20cf48409Christian Maeder _ -> False) as
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder putAssumps newAs
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder pats <- inferPat (Just pty) pat
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder putAssumps as
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder if null pats then addDiags [mkDiag Error "unresolved case pattern" pat]
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder else return ()
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder es <- mapM ( \ (s, ty, p) -> do
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder (_, bs) <- extractBindings p
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder mapM_ addVarDecl bs
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder ts <- infer (Just $ subst s tty) trm
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder putAssumps as
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder return $ map ( \ (st, tyt, t) ->
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder (compSubst s st, subst st ty, tyt,
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder ProgEq p t ps)) ts) pats
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder return $ concat es
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederinferCaseEqs :: Type -> Type -> [ProgEq]
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder -> State Env [(Subst, Type, Type, [ProgEq])]
1a38107941725211e7c3f051f7a8f5e12199f03acmaederinferCaseEqs pty tTy [] = return [(eps, pty, tTy, [])]
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederinferCaseEqs pty tty (eq:eqs) = do
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder fts <- inferCaseEq pty tty eq
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder rs <- mapM (\ (_, pty1, tty1, ne) -> do
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder rts <- inferCaseEqs pty1 tty1 eqs
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder return $ map ( \ (s2, pty2, tty2, nes) ->
0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder (s2, pty2, tty2, ne:nes)) rts) fts
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder return $ concat rs