MixAna.hs revision 6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1
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
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder , iterateCharts
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maederimport qualified Data.Map as Map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport qualified Text.ParserCombinators.Parsec as P
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType :: Term -> Term -> Term
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType _ _ = error "addType"
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 MaederisTypeList :: Env -> [Term] -> Bool
962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederisTypeList e l = case mapM termToType l of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> False
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let Result ds ml = mapM ( \ t -> anaTypeM (Nothing, t) e) ts
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in isJust ml && not (hasErrors ds)
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
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederanaPolyId :: PolyId -> TypeScheme -> State Env (Maybe TypeScheme)
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederanaPolyId (PolyId i@(Id _ cs _) _ _) sc = do
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder mSc <- anaTypeScheme sc
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder Nothing -> return Nothing
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder Just newSc@(TypeScheme tvars _ _) -> do
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder , Map.keysSet $ assumps e ]
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder es = filter (not . flip Set.member ids) cs
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder addDiags $ map (\ j -> mkDiag Warning
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder "unexpected identifier in compound list" j) es
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder if null cs || null tvars then return () else
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder addDiags [mkDiag Hint "is polymorphic compound identifier" i]
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder return $ Just newSc
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederresolveQualOp :: PolyId -> TypeScheme -> State Env TypeScheme
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederresolveQualOp i@(PolyId j _ _) sc = do
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder mSc <- anaPolyId i sc
c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder Nothing -> return sc -- and previous
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder Just nSc -> do
c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder if Set.null $ Set.filter ((== nSc) . opType)
c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder $ Map.findWithDefault Set.empty j $ assumps e
c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder then addDiags [mkDiag Error "operation not found" j]
c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder else return ()
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
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder let self = iterateCharts ga sIds compIds
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder oneStep = nextChart addType (toMixTerm sIds 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 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 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
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})
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)
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
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ QuantifiedTerm quant (catMaybes newDs) (maybe hd id mt) ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder LambdaTerm decls part hd ps -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mDecls <- mapM resolvePattern 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
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ LambdaTerm anaDecls part (maybe hd id mt) ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder CaseTerm hd eqs ps -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mt <- resolve hd
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder newEs <- resolveCaseEqs eqs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ CaseTerm (maybe hd id 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
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ LetTerm b newEs (maybe hd id mt) ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder TermToken tok -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let (ds1, trm) = convertMixfixToken (literal_annos ga)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (flip ResolvedMixTerm []) TermToken tok
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
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mp <- resolvePattern p
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ AsPattern vd (maybe p id mp) ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder TypedTerm trm k ty ps -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- assume that type is analysed
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mt <- resolve trm
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ TypedTerm (maybe trm id mt) k ty ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> error ("iterCharts: " ++ show t)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- * equation stuff
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederresolveCaseEq :: ProgEq -> State Env (Maybe ProgEq)
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederresolveCaseEq (ProgEq p t ps) = do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mp <- resolvePattern p
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
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
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederresolveLetEqs :: [ProgEq] -> State Env [ProgEq]
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederresolveLetEqs eqs = case eqs of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder [] -> return []
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ProgEq pat trm ps : rt -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder mPat <- resolvePattern pat
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> do
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
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder Nothing -> resolveLetEqs rt
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just newTrm -> do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder reqs <- resolveLetEqs rt
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder return $ ProgEq newPat newTrm ps : reqs
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
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"
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian MaedertoMixTerm :: Set.Set Id -> Env -> Id -> [Term] -> Range -> Term
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian MaedertoMixTerm sIds 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
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
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder _ -> let bs = binders e in case ar of
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder hd : tl | Map.member i bs ->
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder ResolvedMixTerm i [] (evalState (anaPattern sIds hd) e : tl) qs
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder _ -> ResolvedMixTerm i [] ar qs
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaedergetKnowns :: Id -> Set.Set Token
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedergetKnowns (Id ts cs _) =
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Set.union (Set.fromList ts) $ Set.unions $ map getKnowns cs
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederresolvePattern :: Term -> State Env (Maybe Term)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederresolvePattern = resolver True
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maederresolve :: Term -> State Env (Maybe Term)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederresolve = resolver False
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maederresolver :: Bool -> Term -> State Env (Maybe Term)
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maederresolver isPat trm = do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let ass = assumps e
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder ga = globAnnos e
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder (addRule, ruleS, sIds) = makeRules ga (preIds e) (getPolyIds 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)
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder (toMixTerm sIds e) chart
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder if isPat then case mr of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> return mr
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just pat -> fmap Just $ anaPattern sIds pat
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder else return mr
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
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
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)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- create fresh type vars for unknown ids tagged with type MixfixType [].
d1012ae182d765c4e6986029d210b9e7b48de205Christian MaederanaPattern :: Set.Set Id -> Term -> State Env Term
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederanaPattern s pat = case pat of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder QualVar vd -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder newVd <- checkVarDecl vd
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian 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
ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder (tvar, c) <- toEnvState $ freshVar 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
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder QualVar (VarDecl v (MixfixType []) ok qs) ->
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder return $ QualVar $ VarDecl v ty ok $ appRange qs ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder newP <- anaPattern s p
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian 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
ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder (tvar, c) <- toEnvState $ freshVar v
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ VarDecl v (TypeName tvar rStar c) ok ps
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder _ -> return vd