MixAna.hs revision 72b9099aeec0762bae4546db3bc4b48721027bf4
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder{- |
ca010363454de207082dfaa4b753531ce2a34551Christian MaederModule : $Header$
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederDescription : mixfix analysis for terms
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : experimental
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederPortability : portable
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian MaederMixfix analysis of terms and patterns, type annotations are also analysed
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder-}
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maedermodule HasCASL.MixAna
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder ( resolve
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder , anaPolyId
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder , makeRules
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder , getPolyIds
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder , iterateCharts
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder , toMixTerm
d27877901128f04518461d25b96d2d93a13f01e4Christian Maeder , uTok
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder ) where
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport Common.GlobalAnnotations
ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport Common.Result
ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport Common.Id
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport Common.DocUtils
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Common.Earley
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Common.Lexer
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Common.Prec
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederimport Common.ConvertMixfixToken
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport Common.Lib.State
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Common.AnnoState
bccea164bdfc2ddc3d1e20749bb5477a46eab3a6Christian Maederimport Common.AnnoParser
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maederimport qualified Data.Map as Map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederimport HasCASL.As
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport HasCASL.AsUtils
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maederimport HasCASL.PrintAs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport HasCASL.VarDecl
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederimport HasCASL.Le
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport HasCASL.ParseTerm
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport HasCASL.TypeAna
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport qualified Text.ParserCombinators.Parsec as P
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederimport Data.Maybe
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Control.Exception (assert)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maederimport Control.Monad
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType :: Term -> Term -> Term
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType _ _ = error "addType"
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder-- | try to reparse terms as a compound list
da2b959c50c95309d8eb8b24174249c2847e74b5Christian MaederisCompoundList :: Set.Set [Id] -> [Term] -> Bool
0a39036fa485579a7b7c81cdd44a412392571927Christian MaederisCompoundList compIds =
0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder maybe False (flip Set.member compIds) . mapM reparseAsId
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederisTypeList :: Env -> [Term] -> Bool
962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederisTypeList e l = case mapM termToType l of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> False
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just ts ->
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let Result ds ml = mapM ( \ t -> anaTypeM (Nothing, t) e) ts
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in isJust ml && not (hasErrors ds)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedertermToType :: Term -> Maybe Type
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedertermToType t = case P.runParser ((case getPosList t of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder [] -> return ()
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder p : _ -> P.setPosition $ fromPos p)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder >> parseType << P.eof) (emptyAnnos ()) "" $ showDoc t "" of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Right x -> Just x
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> Nothing
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederanaPolyId :: PolyId -> TypeScheme -> State Env (Maybe TypeScheme)
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederanaPolyId (PolyId i@(Id _ cs _) _ _) sc = do
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder mSc <- anaTypeScheme sc
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder case mSc of
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder Nothing -> return Nothing
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder Just newSc@(TypeScheme tvars _ _) -> do
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder e <- get
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder let ids = Set.unions
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder [ Map.keysSet $ classMap e
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder , Map.keysSet $ typeMap e
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder , Map.keysSet $ assumps e ]
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder es = filter (not . flip Set.member ids) cs
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder addDiags $ map (mkDiag Warning
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder "unexpected identifier in compound list") es
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder unless (null cs || null tvars)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder $ addDiags [mkDiag Hint "is polymorphic compound identifier" i]
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder return $ Just newSc
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederresolveQualOp :: PolyId -> TypeScheme -> State Env TypeScheme
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederresolveQualOp i@(PolyId j _ _) sc = do
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder mSc <- anaPolyId i sc
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder e <- get
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder case mSc of
c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder Nothing -> return sc -- and previous
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder Just nSc -> do
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder when (Set.null $ Set.filter ((== nSc) . opType)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder $ Map.findWithDefault Set.empty j $ assumps e)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder $ addDiags [mkDiag Error "operation not found" j]
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder return nSc
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian MaederiterateCharts :: GlobalAnnos -> Set.Set Id -> Set.Set [Id] -> [Term]
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder -> Chart Term -> State Env (Chart Term)
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian MaederiterateCharts ga sIds compIds terms chart = do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder e <- get
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder let self = iterateCharts ga sIds compIds
add9c81ed5250ba046a8581ff75b2284bd69e219Christian Maeder oneStep = nextChart addType (toMixTerm e) ga chart
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder vs = localVars e
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder tm = typeMap e
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder case terms of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder [] -> return chart
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder t : tt -> let recurse trm = self tt $ oneStep
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (trm, exprTok {tokPos = getRange trm}) in case t of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder MixfixTerm ts -> self (ts ++ tt) chart
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder MixTypeTerm q typ ps -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mTyp <- anaStarType typ
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder case mTyp of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> recurse t
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just nTyp -> self tt $ oneStep
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (MixTypeTerm q (monoType nTyp) ps, typeTok {tokPos = ps})
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder BracketTerm b ts ps ->
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let bres = self (expandPos TermToken
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (getBrackets b) ts ps ++ tt) chart in case (b, ts) of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (Squares, _ : _) -> if isCompoundList compIds ts then do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder addDiags [mkDiag Hint "is compound list" t]
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder bres
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder else if isTypeList e ts then do
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder let testChart = oneStep (t, typeInstTok {tokPos = ps})
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder if null $ solveDiags testChart then do
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder addDiags [mkDiag Hint "is type list" t]
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder self tt testChart
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder else bres
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder else bres
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder _ -> case (b, ts, tt) of
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder (Parens, [QualOp b2 v sc [] _ ps2], hd@(BracketTerm Squares
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder ts2@(_ : _) ps3) : rtt) | isTypeList e ts2 -> do
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder addDiags [mkDiag Hint "is type list" ts2]
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder nSc <- resolveQualOp v sc
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder self rtt $ oneStep
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder ( QualOp b2 v nSc (bracketTermToTypes e hd) UserGiven ps2
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder , exprTok {tokPos = appRange ps ps3})
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder _ -> bres
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder QualVar (VarDecl v typ ok ps) -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mTyp <- anaStarType typ
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder recurse $ maybe t ( \ nType -> QualVar $ VarDecl v (monoType nType)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ok ps) mTyp
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder QualOp b v sc [] k ps -> do
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder nSc <- resolveQualOp v sc
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder recurse $ QualOp b v nSc [] k ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder QuantifiedTerm quant decls hd ps -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder newDs <- mapM (anaddGenVarDecl False) decls
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mt <- resolve hd
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder putLocalVars vs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder putTypeMap tm
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder recurse $ QuantifiedTerm quant (catMaybes newDs) (fromMaybe hd mt) ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder LambdaTerm decls part hd ps -> do
d27877901128f04518461d25b96d2d93a13f01e4Christian Maeder mDecls <- mapM resolve decls
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let anaDecls = catMaybes mDecls
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder bs = concatMap extractVars anaDecls
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder checkUniqueVars bs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mapM_ (addLocalVar False) bs
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mt <- resolve hd
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder putLocalVars vs
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder recurse $ LambdaTerm anaDecls part (fromMaybe hd mt) ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder CaseTerm hd eqs ps -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mt <- resolve hd
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder newEs <- resolveCaseEqs eqs
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder recurse $ CaseTerm (fromMaybe hd mt) newEs ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder LetTerm b eqs hd ps -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder newEs <- resolveLetEqs eqs
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mt <- resolve hd
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder putLocalVars vs
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder recurse $ LetTerm b newEs (fromMaybe hd mt) ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder TermToken tok -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let (ds1, trm) = convertMixfixToken (literal_annos ga)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (flip ResolvedMixTerm []) TermToken tok
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder addDiags ds1
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder self tt $ oneStep $ case trm of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder TermToken _ -> (trm, tok)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> (trm, exprTok {tokPos = tokPos tok})
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder AsPattern vd p ps -> do
d27877901128f04518461d25b96d2d93a13f01e4Christian Maeder mp <- resolve p
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder recurse $ AsPattern vd (fromMaybe p mp) ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder TypedTerm trm k ty ps -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- assume that type is analysed
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mt <- resolve trm
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder recurse $ TypedTerm (fromMaybe trm mt) k ty ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> error ("iterCharts: " ++ show t)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- * equation stuff
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederresolveCaseEq :: ProgEq -> State Env (Maybe ProgEq)
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederresolveCaseEq (ProgEq p t ps) = do
d27877901128f04518461d25b96d2d93a13f01e4Christian Maeder mp <- resolve p
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder case mp of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> return Nothing
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just newP -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let bs = extractVars newP
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder checkUniqueVars bs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder vs <- gets localVars
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mapM_ (addLocalVar False) bs
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mtt <- resolve t
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder putLocalVars vs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder return $ case mtt of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> Nothing
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just newT -> Just $ ProgEq newP newT ps
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederresolveCaseEqs :: [ProgEq] -> State Env [ProgEq]
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederresolveCaseEqs eqs = case eqs of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder [] -> return []
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder eq : rt -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mEq <- resolveCaseEq eq
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder reqs <- resolveCaseEqs rt
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder return $ case mEq of
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder Nothing -> reqs
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder Just newEq -> newEq : reqs
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederresolveLetEqs :: [ProgEq] -> State Env [ProgEq]
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederresolveLetEqs eqs = case eqs of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder [] -> return []
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ProgEq pat trm ps : rt -> do
d27877901128f04518461d25b96d2d93a13f01e4Christian Maeder mPat <- resolve pat
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder case mPat of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder resolve trm
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder resolveLetEqs rt
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just newPat -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let bs = extractVars newPat
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder checkUniqueVars bs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mapM_ (addLocalVar False) bs
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mTrm <- resolve trm
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder case mTrm of
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder Nothing -> resolveLetEqs rt
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just newTrm -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder reqs <- resolveLetEqs rt
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder return $ ProgEq newPat newTrm ps : reqs
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskimkPatAppl :: Term -> Term -> Range -> Term
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedermkPatAppl op arg qs = case op of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder QualVar (VarDecl i (MixfixType []) _ _) -> ResolvedMixTerm i [] [arg] qs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> ApplTerm op arg qs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederbracketTermToTypes :: Env -> Term -> [Type]
962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederbracketTermToTypes e t = case t of
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder BracketTerm Squares tys _ ->
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder map (monoType . snd) $ fromMaybe (error "bracketTermToTypes")
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder $ maybeResult $ mapM ( \ ty -> anaTypeM (Nothing, ty) e)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder $ fromMaybe (error "bracketTermToTypes1") $ mapM termToType tys
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder _ -> error "bracketTermToTypes2"
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder
add9c81ed5250ba046a8581ff75b2284bd69e219Christian MaedertoMixTerm :: Env -> Id -> [Term] -> Range -> Term
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedertoMixTerm e i ar qs
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder | i == applId = assert (length ar == 2) $
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder let [op, arg] = ar in mkPatAppl op arg qs
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder | i == tupleId || i == unitId = mkTupleTerm ar qs
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder | otherwise = case unPolyId i of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just j@(Id ts _ _) -> if isMixfix j && isSingle ar then
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ResolvedMixTerm j (bracketTermToTypes e $ head ar) [] qs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder else assert (length ar == 1 + placeCount j) $
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let (far, tar : sar) =
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder splitAt (placeCount $ mkId $ fst $ splitMixToken ts) ar
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in ResolvedMixTerm j (bracketTermToTypes e tar) (far ++ sar) qs
add9c81ed5250ba046a8581ff75b2284bd69e219Christian Maeder _ -> ResolvedMixTerm i [] ar qs
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maeder
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaedergetKnowns :: Id -> Set.Set Token
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedergetKnowns (Id ts cs _) =
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Set.union (Set.fromList ts) $ Set.unions $ map getKnowns cs
46d766efdf8beaaadf3f34d99c305738064e9216Christian Maeder
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maederresolve :: Term -> State Env (Maybe Term)
d27877901128f04518461d25b96d2d93a13f01e4Christian Maederresolve trm = do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder e <- get
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let ass = assumps e
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder ga = globAnnos e
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder (addRule, ruleS, sIds) = makeRules ga (preIds e) (getPolyIds ass)
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder $ Set.union (Map.keysSet $ binders e)
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder $ Set.union (Map.keysSet ass)
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder $ Map.keysSet $ localVars e
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder chart <- iterateCharts ga sIds (getCompoundLists e) [trm]
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder $ initChart addRule ruleS
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let Result ds mr = getResolved (showDoc . parenTerm) (getRange trm)
add9c81ed5250ba046a8581ff75b2284bd69e219Christian Maeder (toMixTerm e) chart
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder addDiags ds
d27877901128f04518461d25b96d2d93a13f01e4Christian Maeder return mr
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedergetPolyIds :: Assumps -> Set.Set Id
ad187062b0009820118c1b773a232e29b879a2faChristian MaedergetPolyIds = Set.unions . map ( \ (i, s) ->
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Set.fold ( \ oi -> case opType oi of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder TypeScheme (_ : _) _ _ -> Set.insert i
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> id) Set.empty s) . Map.toList
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederuTok :: Token
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederuTok = mkSimpleId "_"
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds :: [Id]
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds = [unitId, parenId, tupleId, exprId, typeId, applId]
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedermakeRules :: GlobalAnnos -> (PrecMap, Set.Set Id) -> Set.Set Id
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder -> Set.Set Id -> (Token -> [Rule], Rules, Set.Set Id)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedermakeRules ga ps@(p, _) polyIds aIds =
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder let (sIds, ids) = Set.partition isSimpleId aIds
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder ks = Set.fold (Set.union . getKnowns) Set.empty ids
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder rIds = Set.union ids $ Set.intersection sIds $ Set.map simpleIdToId ks
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder m2 = maxWeight p + 2
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder in ( \ tok -> [(simpleIdToId tok, m2, [tok])
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder | isSimpleToken tok && not (Set.member tok ks)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder || tok == uTok ]
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder , partitionRules $ listRules m2 ga ++
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder initRules ps (Set.toList polyIds) builtinIds (Set.toList rIds)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder , sIds)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederinitRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Id] -> [Rule]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederinitRules (p, ps) polyIds bs is =
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder map ( \ i -> mixRule (getIdPrec p ps i) i)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (bs ++ is) ++
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder map ( \ i -> (protect i, maxWeight p + 3, getPlainTokenList i))
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (filter isMixfix is) ++
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- identifiers with a positive number of type arguments
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder map ( \ i -> ( polyId i, getIdPrec p ps i
f1ef1c750f805c1732b01001f2b157c0077b808eChristian Maeder , getPolyTokenList i)) polyIds ++
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder map ( \ i -> ( protect $ polyId i, maxWeight p + 3
f1ef1c750f805c1732b01001f2b157c0077b808eChristian Maeder , getPlainPolyTokenList i)) (filter isMixfix polyIds)