2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : analyse operation declarations

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng JiangStability : experimental

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng JiangPortability : portable

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskianalyse operation declarations

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder-}

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiangmodule HasCASL.OpDecl

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder ( anaOpItem

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder , anaProgEq

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder , mkEnvForall

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder ) where

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maederimport Data.Maybe

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maederimport qualified Data.Set as Set

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiangimport qualified Data.Map as Map

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maederimport Text.ParserCombinators.Parsec (parse, eof)

729bcb10ecaad874ca91fe14a57011d2e254d8c5Christian Maederimport Control.Monad

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maederimport Common.Id

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederimport Common.Lib.State as State

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiangimport Common.Result

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maederimport Common.GlobalAnnotations

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiangimport Common.AS_Annotation

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maederimport Common.Doc

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederimport Common.Lexer (skip)

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiangimport Common.Parsec

729bcb10ecaad874ca91fe14a57011d2e254d8c5Christian Maeder

a208edf329751a734895216ad5b0e334a9ac6a44Christian Maederimport HasCASL.As

c698ca3d47b105a82ec1f19e8c6bc29ab1d1b63dChristian Maederimport HasCASL.HToken

c698ca3d47b105a82ec1f19e8c6bc29ab1d1b63dChristian Maederimport HasCASL.TypeAna

c698ca3d47b105a82ec1f19e8c6bc29ab1d1b63dChristian Maederimport HasCASL.VarDecl

eaf34cf96fbfcdcce7f3bdb322c4ea7ebd1fd220Liam O'Reillyimport HasCASL.Le

c698ca3d47b105a82ec1f19e8c6bc29ab1d1b63dChristian Maederimport HasCASL.Builtin

c698ca3d47b105a82ec1f19e8c6bc29ab1d1b63dChristian Maederimport HasCASL.AsUtils

c698ca3d47b105a82ec1f19e8c6bc29ab1d1b63dChristian Maederimport HasCASL.MixAna

def40d8182c4db2a91afaec94458809a7568baf3Liam O'Reillyimport HasCASL.TypeCheck

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederimport HasCASL.ProgEq

a208edf329751a734895216ad5b0e334a9ac6a44Christian Maederimport HasCASL.Unify

e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian Maeder

e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian MaederanaAttr :: TypeScheme -> OpAttr -> State Env (Maybe OpAttr)

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederanaAttr (TypeScheme tvs ty _) b = case b of

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang UnitOpAttr trm ps -> do

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder e <- get

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder let mTy = let (fty, fArgs) = getTypeAppl ty in case fArgs of

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder [arg, t3] | lesserType e fty (toFunType PFunArr)

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder -> let (pty, ts) = getTypeAppl arg in case ts of

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder [t1, t2] | lesserType e pty (toProdType 2 ps)

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder -> Just (t1,t2,t3)

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder _ -> Nothing

a208edf329751a734895216ad5b0e334a9ac6a44Christian Maeder _ -> Nothing

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder let tm = typeMap e

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder mapM_ (addTypeVarDecl False) tvs

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder case mTy of

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Nothing -> do addDiags [mkDiag Error

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder "unexpected type of operation" ty]

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder putTypeMap tm

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder return Nothing

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder Just (t1, t2, t3) ->

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder do unless (t1 == t2 && t2 == t3)

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder $ addDiags [mkDiag Error

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder "unexpected type components of operation" ty]

dade808234103ea180fa5a2457f2ee8ff76c8e1dChristian Maeder mt <- resolveTerm t3 trm

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang putTypeMap tm

c8ecc5578d32b222f35b625d4dfe7a3fd8bb4173Christian Maeder return $ case mt of

c8ecc5578d32b222f35b625d4dfe7a3fd8bb4173Christian Maeder Nothing -> Nothing

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang Just t -> Just $ UnitOpAttr t ps

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder _ -> return $ Just b

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian MaedertuplePatternToType :: [VarDecl] -> Type

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng JiangtuplePatternToType vds =

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder mkProductTypeWithRange (map ( \ (VarDecl _ t _ _) -> t) vds) $ getRange vds

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian MaederanaOpId :: OpBrand -> TypeScheme -> [OpAttr] -> PolyId -> State Env Bool

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian MaederanaOpId br sc attrs i@(PolyId j _ _) =

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder do mSc <- anaPolyId i sc

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder case mSc of

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang Nothing -> return False

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder Just newSc -> do

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder mAttrs <- mapM (anaAttr newSc) attrs

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang addOpId j newSc (Set.fromList $ catMaybes mAttrs) $ NoOpDefn br

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder

e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian Maeder-- | analyse an op-item

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederanaOpItem :: OpBrand -> Annoted OpItem -> State Env (Annoted (Maybe OpItem))

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian MaederanaOpItem br oi = do

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder let Result ds (Just bs) = extractBinders $ l_annos oi ++ r_annos oi

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder addDiags ds

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder case item oi of

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder OpDecl is sc attr ps -> do

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang case is of

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang [PolyId i _ _] -> mapM_ (addBinder i) bs

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder _ -> unless (null bs) $ addDiags

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang [mkDiag Warning "ignoring binder syntax" bs]

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder ois <- mapM (anaOpId br sc attr) is

e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian Maeder let us = map fst $ filter snd $ zip is ois

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder return $ replaceAnnoted (if null us then Nothing else

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder Just $ OpDecl us sc attr ps) oi

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder OpDefn p@(PolyId i _ _) oldPats rsc@(TypeScheme tArgs scTy qs) trm ps

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder -> do

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder mapM_ (addBinder i) bs

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski checkUniqueVars $ concat oldPats

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder tvs <- gets localTypeVars

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder mArgs <- mapM anaddTypeVarDecl tArgs

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder mPats <- mapM (mapM anaVarDecl) oldPats

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder let newPats = map catMaybes mPats

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder monoPats = map (map makeMonomorph) newPats

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder pats = map (\ l -> mkTupleTerm (map QualVar l) nullRange) monoPats

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder vs <- gets localVars

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder mapM_ (mapM_ $ addLocalVar True) monoPats

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder let newArgs = catMaybes mArgs

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder mty <- anaStarType scTy

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder mtrm <- resolve trm

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder case (mty, mtrm) of

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder (Just rty, Just rTrm) -> do

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder let (partial, ty) = case getTypeAppl rty of

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder (TypeName j _ _ , [lt]) | j == lazyTypeId -> (Partial, lt)

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder _ -> (Total, rty)

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder monoty = monoType ty

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder mt <- typeCheck monoty $ TypedTerm rTrm AsType monoty ps

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder e <- get

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder newSc <- generalizeS $ TypeScheme newArgs

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder (getFunType ty partial

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder $ map tuplePatternToType newPats) qs

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder putLocalVars vs

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder putLocalTypeVars tvs

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder case mt of

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder Just lastTrm0 -> do

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder let lastTrm = case lastTrm0 of

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder TypedTerm lTrm AsType rTy rs ->

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder case getTypeOf lTrm of

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder Just oTy | lesserType e oTy rTy ->

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder if oTy == rTy then lTrm else

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder TypedTerm lTrm Inferred rTy rs

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder _ -> lastTrm0

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder _ -> lastTrm0

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder lamTrm = case (pats, partial) of

a208edf329751a734895216ad5b0e334a9ac6a44Christian Maeder ([], Total) -> lastTrm

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder _ -> LambdaTerm pats partial lastTrm ps

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang ot = QualOp br p newSc [] Infer

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang nullRange

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder lhs = mkApplTerm ot pats

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder ef = if isPred br then

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder mkLogTerm eqvId ps lhs lastTrm

e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian Maeder else mkEqTerm eqId monoty ps lhs lastTrm

e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian Maeder f = mkEnvForall e ef ps

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder addOpId i newSc Set.empty $ Definition br lamTrm

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder appendSentences

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder [(makeNamed (getRLabel oi) $ Formula f)

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder { isDef = True }]

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder return $ replaceAnnoted

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder (Just $ OpDefn p oldPats rsc rTrm ps) oi

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski Nothing -> do

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder addOpId i newSc Set.empty $ NoOpDefn br

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder return $ replaceAnnoted

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder (Just $ OpDecl [p] newSc [] ps) oi

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder _ -> do

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder putLocalVars vs

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder putLocalTypeVars tvs

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder return $ replaceAnnoted Nothing oi

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder-- | analyse a program equation

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian MaederanaProgEq :: Annoted ProgEq -> State Env (Maybe ProgEq)

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian MaederanaProgEq ape = do

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder let pe@(ProgEq _ _ q) = item ape

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder rp <- resolve (LetTerm Program [pe] (BracketTerm Parens [] q) q)

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder case rp of

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder Just t@(LetTerm _ (rpe@(ProgEq _ _ _) : _) _ _) -> do

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder mp <- typeCheck unitType t

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder ga <- State.gets globAnnos

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder case mp of

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder Just (LetTerm _ (newPrg@(ProgEq newPat _ _) : _) _ _) ->

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder case getAppl newPat of

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder Just (i, sc, _) -> do

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder addOpId i sc Set.empty $ NoOpDefn Op

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder appendSentences [(makeNamed ("pe_" ++ showId i "")

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder $ ProgEqSen i sc newPrg)

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder { isDef = True }]

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder e <- get

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder unless (isLHS e newPat)

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder $ addDiags [mkNiceDiag ga Warning

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder "illegal lhs pattern" newPat]

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder return $ Just rpe

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder Nothing -> do addDiags [mkNiceDiag ga Error

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder "illegal toplevel pattern" newPat]

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder return Nothing

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder _ -> return Nothing

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder _ -> return Nothing

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian MaederextractBinderId :: Annotation -> Result Id

a208edf329751a734895216ad5b0e334a9ac6a44Christian MaederextractBinderId a = case a of

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder Unparsed_anno (Annote_word f@"binder") s r ->

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder case parse (skip >> opId << eof) f $ annoArg s of

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder Right i -> return i

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder Left err -> fatal_error (showErr err ++ "\nin " ++ show (annoDoc a)) r

2a0b5e7b246cc32d46b4ed4e53ab8e909e41c3d0Heng Jiang _ -> Result [] Nothing

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder

e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian MaederextractBinders :: [Annotation] -> Result [Id]

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederextractBinders as =

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder let rs = map extractBinderId as

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder ds = concatMap diags rs

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder in if null ds then return $ mapMaybe maybeResult rs

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder else Result ds $ Just []

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder

9b814d51dfcf9b22b391c99c0b08fc48efcafca2Christian MaederaddBinding :: Id -> Id -> State.State Env ()

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederaddBinding o b = do

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder addDiags $ getBinderDiags o b

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder State.modify $ \ e -> e { binders = Map.insert b o $ binders e }

9b814d51dfcf9b22b391c99c0b08fc48efcafca2Christian Maeder e <- State.get

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder let ga = globAnnos e

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder aa = assoc_annos ga

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder when (isInfix b && not (Map.member b aa)) $

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder State.put e { globAnnos = ga { assoc_annos = Map.insert b ARight aa }}

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian MaedergetBinderDiags :: Id -> Id -> [Diagnosis]

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaedergetBinderDiags o b =

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder let c = placeCount b

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder d = placeCount o + 1

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder str = "expected " ++ show (max 2 d) ++ " places in binder"

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder in if c < 2 then [mkDiag Error str b]

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder else if d /= c then

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder if isMixfix o then [mkDiag Warning str b]

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder else [mkDiag Hint ("non-mixfix-id '" ++ show o ++ "' for binder") b]

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder else []

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian Maeder

4fd9d02aaec1d0447c2897f977c4c48b0c7e5c20Christian MaederaddBinder :: Id -> Id -> State.State Env ()

addBinder o b = do

bs <- State.gets binders

as <- State.gets assumps

when (Map.member b as) $ addDiags

[mkDiag Warning "binder shadows shadows global name(s)" b]

case Map.lookup b bs of

Just o2 -> if o == o2 then do

addDiags [Diag Warning

("binder conflict for: " ++ show b ++ expected o2 o)

$ posOfId b]

addBinding o b

else addDiags [mkDiag Warning "repeated binder syntax" b]

Nothing -> addBinding o b