MixAna.hs revision adfdcfa67b7f12df6df7292e238c3f9a4b637980
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
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
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maederimport Common.Anno_Parser
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
975642b989852fc24119c59cf40bc1af653608ffChristian Maederimport HasCASL.Unify
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)
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
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaederanaPolyId :: PolyId -> TypeScheme -> State Env (Maybe (PolyId, TypeScheme))
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian MaederanaPolyId (PolyId i@(Id _ cs ps) tys rs) (TypeScheme targs ty qs) = do
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder mSc <- anaTypeScheme $ TypeScheme (tys ++ targs) ty $ appRange ps qs
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
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder [ Map.keysSet $ classMap e
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder , Map.keysSet $ typeMap e
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian 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]
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder return $ Just (PolyId i [] rs, newSc)
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaederresolveQualOp :: PolyId -> TypeScheme -> State Env (PolyId, TypeScheme)
d591a82b32594f0992b27477cacb00b97226c9c8Christian MaederresolveQualOp i sc = do
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder mSc <- anaPolyId i sc
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder e <- get
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder case mSc of
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder Nothing -> return (i, sc)
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder Just p@(PolyId j _ _, nSc) -> do
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder case findOpId e j nSc of
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder Nothing -> addDiags [mkDiag Error "operation not found" j]
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder _ -> return ()
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder return p
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder
da2b959c50c95309d8eb8b24174249c2847e74b5Christian MaederiterateCharts :: GlobalAnnos -> Set.Set [Id] -> [Term] -> Chart Term
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder -> State Env (Chart Term)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederiterateCharts ga compIds terms chart = do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder e <- get
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let self = iterateCharts ga compIds
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian 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]
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder (j, nSc) <- resolveQualOp v sc
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder self rtt $ oneStep
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder ( QualOp b2 j 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
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ maybe t ( \ nType -> QualVar $ VarDecl v (monoType nType)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ok ps) mTyp
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder QualOp b v sc [] k ps -> do
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder (j, nSc) <- resolveQualOp v sc
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder recurse $ QualOp b j nSc [] k ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder QuantifiedTerm quant decls hd ps -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder newDs <- mapM (anaddGenVarDecl False) decls
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mt <- resolve ga 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
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mDecls <- mapM (resolvePattern ga) decls
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let anaDecls = catMaybes mDecls
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder bs = concatMap extractVars anaDecls
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder checkUniqueVars bs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mapM_ (addLocalVar False) bs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mt <- resolve ga hd
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder putLocalVars vs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ LambdaTerm anaDecls part (maybe hd id mt) ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder CaseTerm hd eqs ps -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mt <- resolve ga hd
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder newEs <- resolveCaseEqs ga eqs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ CaseTerm (maybe hd id mt) newEs ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder LetTerm b eqs hd ps -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder newEs <- resolveLetEqs ga eqs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mt <- resolve ga 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 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
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mp <- resolvePattern ga 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
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mt <- resolve ga trm
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ TypedTerm (maybe trm id mt) k ty ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> error ("iterCharts: " ++ show t)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- * equation stuff
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederresolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederresolveCaseEq ga (ProgEq p t ps) = do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mp <- resolvePattern ga 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
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mtt <- resolve ga 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
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederresolveCaseEqs ga eqs = case eqs of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder [] -> return []
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder eq : rt -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mEq <- resolveCaseEq ga eq
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder reqs <- resolveCaseEqs ga rt
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder return $ case mEq of
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder Nothing -> reqs
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder Just newEq -> newEq : reqs
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs _ [] = return []
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederresolveLetEqs ga eqs = case eqs of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder [] -> return []
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ProgEq pat trm ps : rt -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mPat <- resolvePattern ga pat
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder case mPat of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder resolve ga trm
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder resolveLetEqs ga rt
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just newPat -> do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let bs = extractVars newPat
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder checkUniqueVars bs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mapM_ (addLocalVar False) bs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mTrm <- resolve ga trm
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder case mTrm of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> resolveLetEqs ga rt
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just newTrm -> do
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder reqs <- resolveLetEqs ga 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 _ ->
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"
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder
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
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
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian 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
d1012ae182d765c4e6986029d210b9e7b48de205Christian MaederresolvePattern :: GlobalAnnos -> Term -> State Env (Maybe Term)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederresolvePattern = resolver True
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederresolve = resolver False
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederresolver :: Bool -> GlobalAnnos -> Term -> State Env (Maybe Term)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederresolver isPat ga trm = do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder e <- get
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let ass = assumps e
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder vs = localVars e
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ps = preIds e
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder compIds = getCompoundLists e
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (addRule, ruleS, sIds) = makeRules ga ps (getPolyIds ass)
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder $ Set.union (Map.keysSet ass) $ Map.keysSet vs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder chart <- iterateCharts ga compIds [trm] $ initChart addRule ruleS
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let Result ds mr = getResolved (showDoc . parenTerm) (getRange trm)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (toMixTerm e) chart
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder addDiags ds
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
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
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)
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)
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder
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
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case p of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder QualVar (VarDecl v (MixfixType []) ok qs) ->
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder return $ QualVar $ VarDecl v ty ok $ appRange qs ps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> do
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