e47d29b522739fbf08aac80c6faa447dde113fbcChristian MaederDescription : analyse operation declarations
11d6ec73ee5550e00cb56b221bdbeb709142e779Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : experimental
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederanalyse operation declarations
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder , mkEnvForall
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maederimport qualified Data.Set as Set
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maederimport qualified Data.Map as Map
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maederimport Text.ParserCombinators.Parsec (parse, eof)
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederanaAttr :: TypeScheme -> OpAttr -> State Env (Maybe OpAttr)
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederanaAttr (TypeScheme tvs ty _) b = case b of
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder UnitOpAttr trm ps -> do
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder let mTy = let (fty, fArgs) = getTypeAppl ty in case fArgs of
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder [arg, t3] | lesserType e fty (toFunType PFunArr)
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder -> let (pty, ts) = getTypeAppl arg in case ts of
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder [t1, t2] | lesserType e pty (toProdType 2 ps)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> Just (t1, t2, t3)
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder let tm = typeMap e
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder mapM_ (addTypeVarDecl False) tvs
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder Nothing -> do addDiags [mkDiag Error
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder "unexpected type of operation" ty]
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder putTypeMap tm
5e538f0d5fb2768e25a1f300b094bc07ac2a835bChristian Maeder return Nothing
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder Just (t1, t2, t3) ->
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder do unless (t1 == t2 && t2 == t3)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder $ addDiags [mkDiag Error
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder "unexpected type components of operation" ty]
5e538f0d5fb2768e25a1f300b094bc07ac2a835bChristian Maeder mt <- resolveTerm t3 trm
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder putTypeMap tm
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder return $ case mt of
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder Nothing -> Nothing
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder Just t -> Just $ UnitOpAttr t ps
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder _ -> return $ Just b
25612a7b3ce708909298d5426406592473880a20Christian MaedertuplePatternToType :: [VarDecl] -> Type
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedertuplePatternToType vds =
61e38a4f194d3adc66646326c938eb9263a2f39bChristian Maeder mkProductTypeWithRange (map ( \ (VarDecl _ t _ _) -> t) vds) $ getRange vds
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederanaOpId :: OpBrand -> TypeScheme -> [OpAttr] -> PolyId -> State Env Bool
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederanaOpId br sc attrs i@(PolyId j _ _) =
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder do mSc <- anaPolyId i sc
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Nothing -> return False
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder Just newSc -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mAttrs <- mapM (anaAttr newSc) attrs
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder addOpId j newSc (Set.fromList $ catMaybes mAttrs) $ NoOpDefn br
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder-- | analyse an op-item
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederanaOpItem :: OpBrand -> Annoted OpItem -> State Env (Annoted (Maybe OpItem))
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederanaOpItem br oi = do
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder let Result ds (Just bs) = extractBinders $ l_annos oi ++ r_annos oi
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder case item oi of
0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder OpDecl is sc attr ps -> do
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder [PolyId i _ _] -> mapM_ (addBinder i) bs
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder _ -> unless (null bs) $ addDiags
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder [mkDiag Warning "ignoring binder syntax" bs]
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ois <- mapM (anaOpId br sc attr) is
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder let us = map fst $ filter snd $ zip is ois
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder return $ replaceAnnoted (if null us then Nothing else
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder Just $ OpDecl us sc attr ps) oi
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder OpDefn p@(PolyId i _ _) oldPats rsc@(TypeScheme tArgs scTy qs) trm ps
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder mapM_ (addBinder i) bs
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder checkUniqueVars $ concat oldPats
11d6ec73ee5550e00cb56b221bdbeb709142e779Christian Maeder tvs <- gets localTypeVars
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder mArgs <- mapM anaddTypeVarDecl tArgs
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder mPats <- mapM (mapM anaVarDecl) oldPats
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder let newPats = map catMaybes mPats
18b709ce961d68328da768318dcc70067f066d86Christian Maeder monoPats = map (map makeMonomorph) newPats
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski pats = map (\ l -> mkTupleTerm (map QualVar l) nullRange) monoPats
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder vs <- gets localVars
b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder mapM_ (mapM_ $ addLocalVar True) monoPats
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder let newArgs = catMaybes mArgs
18b709ce961d68328da768318dcc70067f066d86Christian Maeder mty <- anaStarType scTy
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mtrm <- resolve trm
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder case (mty, mtrm) of
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder (Just rty, Just rTrm) -> do
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder let (partial, ty) = case getTypeAppl rty of
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder (TypeName j _ _ , [lt]) | j == lazyTypeId -> (Partial, lt)
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder _ -> (Total, rty)
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder monoty = monoType ty
5e538f0d5fb2768e25a1f300b094bc07ac2a835bChristian Maeder mt <- typeCheck monoty $ TypedTerm rTrm AsType monoty ps
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder newSc <- generalizeS $ TypeScheme newArgs
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder (getFunType ty partial
d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maeder $ map tuplePatternToType newPats) qs
22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian Maeder putLocalVars vs
22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian Maeder putLocalTypeVars tvs
e4f3c121d197ca18cd8f67deaabdddf7f6bdb7e9Christian Maeder Just lastTrm0 -> do
e4f3c121d197ca18cd8f67deaabdddf7f6bdb7e9Christian Maeder let lastTrm = case lastTrm0 of
fd6adc3ab7bab87f889110d57df038f83947ccb3Christian Maeder TypedTerm lTrm AsType rTy rs ->
e4f3c121d197ca18cd8f67deaabdddf7f6bdb7e9Christian Maeder case getTypeOf lTrm of
fd6adc3ab7bab87f889110d57df038f83947ccb3Christian Maeder Just oTy | lesserType e oTy rTy ->
fd6adc3ab7bab87f889110d57df038f83947ccb3Christian Maeder if oTy == rTy then lTrm else
fd6adc3ab7bab87f889110d57df038f83947ccb3Christian Maeder TypedTerm lTrm Inferred rTy rs
e4f3c121d197ca18cd8f67deaabdddf7f6bdb7e9Christian Maeder _ -> lastTrm0
e4f3c121d197ca18cd8f67deaabdddf7f6bdb7e9Christian Maeder _ -> lastTrm0
e4f3c121d197ca18cd8f67deaabdddf7f6bdb7e9Christian Maeder lamTrm = case (pats, partial) of
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder ([], Total) -> lastTrm
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder _ -> LambdaTerm pats partial lastTrm ps
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder ot = QualOp br p newSc [] Infer
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder lhs = mkApplTerm ot pats
f7e1f97078161269a7f99a0520cc421d171bb0daChristian Maeder ef = if isPred br then
f7e1f97078161269a7f99a0520cc421d171bb0daChristian Maeder mkLogTerm eqvId ps lhs lastTrm
f7e1f97078161269a7f99a0520cc421d171bb0daChristian Maeder else mkEqTerm eqId monoty ps lhs lastTrm
c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder f = mkEnvForall e ef ps
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder addOpId i newSc Set.empty $ Definition br lamTrm
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder appendSentences
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder [(makeNamed (getRLabel oi) $ Formula f)
e1fd2026bcd805296762eaa97090f7a29819d9f2Christian Maeder { isDef = True }]
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder return $ replaceAnnoted
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder (Just $ OpDefn p oldPats rsc rTrm ps) oi
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder Nothing -> do
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder addOpId i newSc Set.empty $ NoOpDefn br
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder return $ replaceAnnoted
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder (Just $ OpDecl [p] newSc [] ps) oi
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder putLocalVars vs
11d6ec73ee5550e00cb56b221bdbeb709142e779Christian Maeder putLocalTypeVars tvs
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder return $ replaceAnnoted Nothing oi
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder-- | analyse a program equation
4bae958647dc527f8114d3882bdfda1c2a354ffaChristian MaederanaProgEq :: Annoted ProgEq -> State Env (Maybe ProgEq)
4bae958647dc527f8114d3882bdfda1c2a354ffaChristian MaederanaProgEq ape = do
4bae958647dc527f8114d3882bdfda1c2a354ffaChristian Maeder let pe@(ProgEq _ _ q) = item ape
4bae958647dc527f8114d3882bdfda1c2a354ffaChristian Maeder rp <- resolve (LetTerm Program [pe] (BracketTerm Parens [] q) q)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just t@(LetTerm _ (rpe@(ProgEq {}) : _) _ _) -> do
5e538f0d5fb2768e25a1f300b094bc07ac2a835bChristian Maeder mp <- typeCheck unitType t
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ga <- State.gets globAnnos
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder Just (LetTerm _ (newPrg@(ProgEq newPat _ _) : _) _ _) ->
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder case getAppl newPat of
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder Just (i, sc, _) -> do
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder addOpId i sc Set.empty $ NoOpDefn Op
b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder appendSentences [(makeNamed ("pe_" ++ showId i "")
65835942d66905c377fa503e0d577df5aade58feChristian Maeder $ ProgEqSen i sc newPrg)
e1fd2026bcd805296762eaa97090f7a29819d9f2Christian Maeder { isDef = True }]
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder unless (isLHS e newPat)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder $ addDiags [mkNiceDiag ga Warning
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder "illegal lhs pattern" newPat]
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder return $ Just rpe
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder Nothing -> do addDiags [mkNiceDiag ga Error
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder "illegal toplevel pattern" newPat]
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder return Nothing
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder _ -> return Nothing
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder _ -> return Nothing
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederextractBinderId :: Annotation -> Result Id
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederextractBinderId a = case a of
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder Unparsed_anno (Annote_word f@"binder") s r ->
20ba5fe63cd6e2b5cbed5323d47842fac2f40cd7Christian Maeder case parse (skip >> opId << eof) f $ annoArg s of
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder Right i -> return i
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder Left err -> fatal_error (showErr err ++ "\nin " ++ show (annoDoc a)) r
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder _ -> Result [] Nothing
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederextractBinders :: [Annotation] -> Result [Id]
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederextractBinders as =
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder let rs = map extractBinderId as
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder ds = concatMap diags rs
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder in if null ds then return $ mapMaybe maybeResult rs
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder else Result ds $ Just []
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederaddBinding :: Id -> Id -> State.State Env ()
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederaddBinding o b = do
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder addDiags $ getBinderDiags o b
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder State.modify $ \ e -> e { binders = Map.insert b o $ binders e }
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder let ga = globAnnos e
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder aa = assoc_annos ga
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder when (isInfix b && not (Map.member b aa)) $
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder State.put e { globAnnos = ga { assoc_annos = Map.insert b ARight aa }}
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaedergetBinderDiags :: Id -> Id -> [Diagnosis]
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaedergetBinderDiags o b =
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder let c = placeCount b
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder d = placeCount o + 1
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder str = "expected " ++ show (max 2 d) ++ " places in binder"
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder in if c < 2 then [mkDiag Error str b]
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder else if d /= c then
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder if isMixfix o then [mkDiag Warning str b]
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder else [mkDiag Hint ("non-mixfix-id '" ++ show o ++ "' for binder") b]
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederaddBinder :: Id -> Id -> State.State Env ()
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederaddBinder o b = do
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder when (Map.member b as) $ addDiags
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder [mkDiag Warning "binder shadows shadows global name(s)" b]
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder Just o2 -> if o == o2 then do
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder addDiags [Diag Warning
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder ("binder conflict for: " ++ show b ++ expected o2 o)
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder addBinding o b
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder else addDiags [mkDiag Warning "repeated binder syntax" b]
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder Nothing -> addBinding o b