MixAna.hs revision 962036a37b92afb04ac0725cde9f20e599c04c5f
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
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : experimental
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederPortability : portable
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian MaederMixfix analysis of terms and patterns, type annotations are also analysed
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maederimport qualified Data.Map as Map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport qualified Text.ParserCombinators.Parsec as P
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Data.List (partition)
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType :: Term -> Term -> Term
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType _ _ = error "addType"
da2b959c50c95309d8eb8b24174249c2847e74b5Christian MaederisCompoundList :: Set.Set [Id] -> [Term] -> Bool
da2b959c50c95309d8eb8b24174249c2847e74b5Christian MaederisCompoundList compIds l =
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder maybe False (flip Set.member compIds) $ mapM termToId l
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederisTypeList :: Env -> [Term] -> Bool
962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederisTypeList e l = case mapM termToType l of
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Nothing -> False
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder let Result ds ml =
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder mapM ( \ t -> anaTypeM (Nothing, t) e) ts
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder in isJust ml && not (hasErrors ds)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedertermToType :: Term -> Maybe Type
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedertermToType t =
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder case P.runParser ((case getPosList t of
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder [] -> return ()
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder p : _ -> P.setPosition $ fromPos p)
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder >> parseType << P.eof) (emptyAnnos ()) "" $ showDoc t "" of
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Right x -> Just x
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedertermToId :: Term -> Maybe Id
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedertermToId t = case P.parse (uninstOpId << P.eof) "" $ showDoc t "" of
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Right x -> Just x
da2b959c50c95309d8eb8b24174249c2847e74b5Christian MaederiterateCharts :: GlobalAnnos -> Set.Set [Id] -> [Term] -> Chart Term
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder -> State Env (Chart Term)
da2b959c50c95309d8eb8b24174249c2847e74b5Christian MaederiterateCharts ga compIds terms chart =
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder let self = iterateCharts ga compIds
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder oneStep = nextChart addType (toMixTerm e) ga chart
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder vs = localVars e
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder tm = typeMap e
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case terms of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder [] -> return chart
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder let recurse trm = self tt $
d48085f765fca838c1d972d2123601997174583dChristian Maeder oneStep (trm, exprTok {tokPos = getRange trm})
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder MixfixTerm ts -> self (ts ++ tt) chart
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder MixTypeTerm q typ ps -> do
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mTyp <- anaStarType typ
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Nothing -> recurse t
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Just nTyp -> self tt $ oneStep
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (MixTypeTerm q (monoType nTyp) ps,
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder typeTok {tokPos = ps})
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder BracketTerm b ts ps ->
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder let bres = self (expandPos TermToken
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (getBrackets b) ts ps ++ tt) chart
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder in case (b, ts) of
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (Squares, _ : _) ->
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder if isCompoundList compIds ts then do
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder addDiags [mkDiag Hint "is compound list" t]
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder else if isTypeList e ts then do
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder addDiags [mkDiag Hint "is type list" t]
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder self tt $ oneStep (t, typeInstTok {tokPos = ps})
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder QualVar (VarDecl v typ ok ps) -> do
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mTyp <- anaStarType typ
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Nothing -> recurse t
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Just nType -> recurse $ QualVar $
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder VarDecl v (monoType nType) ok ps
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder QualOp b (InstOpId v ts qs) sc ps -> do
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mSc <- anaTypeScheme sc
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder newTs <- anaInstTypes ts
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Nothing -> recurse t
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Just nSc -> do
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case findOpId e v nSc of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Nothing -> addDiags [mkDiag Error
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder "operation not found" v]
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder _ -> return ()
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder recurse $ QualOp b (InstOpId v newTs qs) nSc ps
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder QuantifiedTerm quant decls hd ps -> do
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder newDs <- mapM (anaddGenVarDecl False) decls
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mt <- resolve ga hd
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder putLocalVars vs
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder putTypeMap tm
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder let newT = case mt of Just trm -> trm
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder recurse $ QuantifiedTerm quant (catMaybes newDs) newT ps
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder LambdaTerm decls part hd ps -> do
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mDecls <- mapM (resolvePattern ga) decls
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder let anaDecls = catMaybes mDecls
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder bs = concatMap extractVars anaDecls
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder checkUniqueVars bs
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder mapM_ (addLocalVar False) bs
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mt <- resolve ga hd
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder putLocalVars vs
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder recurse $ LambdaTerm anaDecls part (maybe hd id mt) ps
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder CaseTerm hd eqs ps -> do
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder mt <- resolve ga hd
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder newEs <- resolveCaseEqs ga eqs
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder recurse $ CaseTerm (maybe hd id mt) newEs ps
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder LetTerm b eqs hd ps -> do
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder newEs <- resolveLetEqs ga eqs
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder mt <- resolve ga hd
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder putLocalVars vs
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder recurse $ LetTerm b newEs (maybe hd id mt) ps
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder TermToken tok -> do
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder let (ds1, trm) = convertMixfixToken
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (literal_annos ga)
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder (flip ResolvedMixTerm [])
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder TermToken tok
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder self tt $ oneStep $
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder TermToken _ -> (trm, tok)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder _ -> (trm, exprTok
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder {tokPos = tokPos tok})
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder AsPattern vd p ps -> do
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mp <- resolvePattern ga p
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder let newP = case mp of Just pat -> pat
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder recurse $ AsPattern vd newP ps
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder TypedTerm trm k ty ps -> do
3f7009c892b16d172314abbba83d663fa0d87a65Christian Maeder -- assume that type is analysed
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mt <- resolve ga trm
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder recurse $ TypedTerm (maybe trm id mt) k ty ps
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder _ -> error ("iterCharts: " ++ show t)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- * equation stuff
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederresolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederresolveCaseEq ga (ProgEq p t ps) =
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder do mp <- resolvePattern ga p
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> return Nothing
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Just newP -> do
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder let bs = extractVars newP
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder checkUniqueVars bs
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder vs <- gets localVars
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder mapM_ (addLocalVar False) bs
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mtt <- resolve ga t
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder putLocalVars vs
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder return $ case mtt of
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Nothing -> Nothing
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Just newT -> Just $ ProgEq newP newT ps
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEqs _ [] = return []
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederresolveCaseEqs ga (eq : rt) =
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder do mEq <- resolveCaseEq ga eq
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder eqs <- resolveCaseEqs ga rt
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder return $ case mEq of
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Nothing -> eqs
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Just newEq -> newEq : eqs
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs _ [] = return []
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederresolveLetEqs ga (ProgEq pat trm ps : rt) =
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder do mPat <- resolvePattern ga pat
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Nothing -> do resolve ga trm
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder resolveLetEqs ga rt
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Just newPat -> do
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder let bs = extractVars newPat
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder checkUniqueVars bs
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder mapM_ (addLocalVar False) bs
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mTrm <- resolve ga trm
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Nothing -> resolveLetEqs ga rt
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Just newTrm -> do
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder eqs <- resolveLetEqs ga rt
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder return (ProgEq newPat newTrm ps : eqs)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskimkPatAppl :: Term -> Term -> Range -> Term
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedermkPatAppl op arg qs =
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder QualVar (VarDecl i (MixfixType []) _ _) ->
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ResolvedMixTerm i [] [arg] qs
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder _ -> ApplTerm op arg qs
962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederbracketTermToTypes :: Env -> Term -> [Type]
962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederbracketTermToTypes e t = case t of
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder BracketTerm Squares tys _ ->
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder map (monoType . snd) $ maybe (error "bracketTermToTypes") id $
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder maybeResult $ mapM ( \ ty -> anaTypeM (Nothing, ty) e) $
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder maybe (error "bracketTermToTypes1") id $ mapM termToType tys
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder _ -> error "bracketTermToTypes2"
962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaedertoMixTerm :: Env -> Id -> [Term] -> Range -> Term
962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaedertoMixTerm e i ar qs =
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder if i == applId then assert (length ar == 2) $
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder let [op, arg] = ar in mkPatAppl op arg qs
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder else if i == tupleId || i == unitId then
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder mkTupleTerm ar qs
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder else case unPolyId i of
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Just j@(Id ts [] ps) ->
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder if isMixfix j && isSingle ar then
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder ResolvedMixTerm j (bracketTermToTypes e $ head ar) [] qs
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder else assert (length ar == 1 + placeCount j) $
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder let (toks, _) = splitMixToken ts
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder (far, tar : sar) =
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder splitAt (placeCount $ Id toks [] ps) ar
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder in ResolvedMixTerm j (bracketTermToTypes e tar) (far ++ sar) qs
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder _ -> ResolvedMixTerm i [] ar qs
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaedergetKnowns :: Id -> Set.Set Token
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaedergetKnowns (Id ts cs _) = Set.union (Set.fromList ts) $
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Set.unions (map getKnowns cs)
975642b989852fc24119c59cf40bc1af653608ffChristian MaederresolvePattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederresolvePattern = resolver True
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederresolve = resolver False
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederresolver :: Bool -> GlobalAnnos -> Term -> State Env (Maybe Term)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederresolver isPat ga trm =
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder let ass = assumps e
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder vs = localVars e
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder ps = preIds e
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder compIds = getCompoundLists e
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder let (addRule, ruleS, sIds) = makeRules ga ps (getPolyIds ass)
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder $ Set.union (Map.keysSet ass) $ Map.keysSet vs
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder chart <- iterateCharts ga compIds [trm] $ initChart addRule ruleS
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder let Result ds mr = getResolved
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder (showDoc . parenTerm) (getRange trm)
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder (toMixTerm e) chart
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder if isPat then case mr of
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder Nothing -> return mr
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder Just pat -> fmap Just $ anaPattern sIds pat
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder else return mr
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedergetPolyIds :: Assumps -> Set.Set Id
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedergetPolyIds = Set.unions . map ( \ (i, OpInfos l) ->
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder foldr ( \ oi s -> case opType oi of
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder TypeScheme (_ : _) _ _ -> Set.insert i s
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Map.filterWithKey ( \ (Id _ cs _) _ -> null cs)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedergetCompound :: Id -> [Id]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedergetCompound (Id _ cs _) = cs
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedergetCompoundLists :: Env -> Set.Set [Id]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedergetCompoundLists e = Set.delete [] $ Set.map getCompound $ Set.union
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (Map.keysSet $ assumps e) $ Map.keysSet $ typeMap e
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederuTok = mkSimpleId "_"
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds :: [Id]
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds = [unitId, parenId, tupleId, exprId, typeId, applId]
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
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder in ( \ tok -> if isSimpleToken tok
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder && not (Set.member tok ks)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder || tok == uTok then
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder [(simpleIdToId tok, m2, [tok])] else []
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder , partitionRules $ listRules m2 ga ++
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder initRules ps (Set.toList polyIds) builtinIds (Set.toList rIds)
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
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder map ( \ i -> let j = polyId i in
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (j, getIdPrec p ps i, getTokenPlaceList j)) polyIds ++
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder map ( \ i -> let j = polyId i in
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (protect j, maxWeight p + 3, getPlainTokenList j))
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (filter isMixfix polyIds)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederpolyId :: Id -> Id
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederpolyId (Id ts _ ps) = let (toks, pls) = splitMixToken ts in
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Id (toks ++ [typeInstTok] ++ pls) [] ps
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederunPolyId :: Id -> Maybe Id
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederunPolyId (Id ts cs ps) = let (ft, rt) = partition (== typeInstTok) ts in
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder [_] -> Just $ Id rt cs ps
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- create fresh type vars for unknown ids tagged with type MixfixType [].
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederanaPattern :: Set.Set Id -> Pattern -> State Env Pattern
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederanaPattern s pat = case pat of
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder QualVar vd -> do newVd <- checkVarDecl vd
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ QualVar newVd
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ResolvedMixTerm i tys pats ps | null pats && null tys &&
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder (isSimpleId i || i == simpleIdToId uTok) &&
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder not (Set.member i s) -> do
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder (tvar, c) <- toEnvState $ freshVar $ posOfId i
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder return $ QualVar $ VarDecl i (TypeName tvar rStar c) Other ps
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder | otherwise -> do
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder l <- mapM (anaPattern s) pats
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder return $ ResolvedMixTerm i tys l ps
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder ApplTerm p1 p2 ps -> do
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder p3 <- anaPattern s p1
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder p4 <- anaPattern s p2
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ ApplTerm p3 p4 ps
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder TupleTerm pats ps -> do
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder l <- mapM (anaPattern s) pats
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ TupleTerm l ps
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder TypedTerm p q ty ps -> do
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder QualVar (VarDecl v (MixfixType []) ok qs) ->
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder let newVd = VarDecl v ty ok (qs `appRange` ps) in
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ QualVar newVd
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder _ -> do newP <- anaPattern s p
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ TypedTerm newP q ty ps
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder AsPattern vd p2 ps -> do
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder newVd <- checkVarDecl vd
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder p4 <- anaPattern s p2
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ AsPattern newVd p4 ps
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder _ -> return pat
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder where checkVarDecl vd@(VarDecl v t ok ps) = case t of
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder MixfixType [] -> do
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder (tvar, c) <- toEnvState $ freshVar $ posOfId v
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ VarDecl v (TypeName tvar rStar c) ok ps
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder _ -> return vd