MixAna.hs revision fc8c6570c7b4ee13f375eb607bed2290438573bf
ca010363454de207082dfaa4b753531ce2a34551Christian MaederModule : $Header$
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian MaederMaintainer : maeder@tzi.de
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : experimental
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian MaederPortability : portable
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian MaederMixfix analysis of terms and patterns, type annotations are also analysed
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport qualified Common.Lib.Map as Map
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport qualified Common.Lib.Set as Set
b44c934092b277ea7fa55bdaa89f723384b0c23cChristian MaederopKindFilter :: Int -> Int -> Maybe Bool
b44c934092b277ea7fa55bdaa89f723384b0c23cChristian MaederopKindFilter arg op =
1bc3627bdb66ecc1efe23eeaeca0ee1f3151ab14Christian Maeder if op < arg then Just True
f7587308f5d51590cd61e4316f6a367156c45141Christian Maeder else if arg < op then Just False
1bc3627bdb66ecc1efe23eeaeca0ee1f3151ab14Christian MaedergetIdPrec :: PrecMap -> Set.Set Id -> Id -> Int
454b2a26b6ea95206df2f82768a8e12765f182bfChristian MaedergetIdPrec (pm, r, m) ps i = if i == applId then m + 1
454b2a26b6ea95206df2f82768a8e12765f182bfChristian Maeder (if begPlace i || endPlace i then if Set.member i ps then r else m
454b2a26b6ea95206df2f82768a8e12765f182bfChristian Maeder else m + 2) i pm
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType :: Term -> Term -> Term
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian MaederaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType _ _ = error "addType"
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maedertype TermChart = Chart Term
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederiterateCharts :: GlobalAnnos -> [Term] -> TermChart
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder -> State Env TermChart
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederiterateCharts ga terms chart =
b44c934092b277ea7fa55bdaa89f723384b0c23cChristian Maeder let self = iterateCharts ga
b44c934092b277ea7fa55bdaa89f723384b0c23cChristian Maeder oneStep = nextChart addType opKindFilter
0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maeder toMixTerm ga chart
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder as = assumps e
48708376ccab0e56251f53b0ec21499a277e9102Christian Maeder tm = typeMap e
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder if null terms then return chart else
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder do let t:tt = terms
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder recurse trm = self tt $
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder oneStep (trm, exprTok {tokPos = posOfTerm trm})
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder MixfixTerm ts -> self (ts ++ tt) chart
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian Maeder MixTypeTerm q typ ps -> do
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian Maeder mTyp <- anaStarType typ
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian Maeder Nothing -> recurse t
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian Maeder Just nTyp -> self tt $ oneStep
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian Maeder (MixTypeTerm q nTyp ps,
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian Maeder typeTok {tokPos = headPos ps})
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder BracketTerm b ts ps -> self
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder (expandPos TermToken (getBrackets b) ts ps ++ tt) chart
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder QualVar (VarDecl v typ ok ps) -> do
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mTyp <- anaStarType typ
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> recurse t
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Just nTyp -> do
cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder let mi = findOpId e v $ simpleTypeScheme nTyp
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> addDiags [mkDiag Error
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder "value not found" v]
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder _ -> return ()
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder recurse $ QualVar $ VarDecl v nTyp ok ps
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maeder QualOp b (InstOpId v ts qs) sc ps -> do
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maeder mSc <- anaTypeScheme sc
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maeder newTs <- anaInstTypes ts
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> recurse t
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maeder Just nSc -> do
cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder let mi = findOpId e v nSc
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> addDiags [mkDiag Error
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder "value not found" v]
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder _ -> return ()
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maeder recurse $ QualOp b (InstOpId v newTs qs) nSc ps
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder QuantifiedTerm quant decls hd ps -> do
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder newDs <- mapM anaGenVarDecl decls
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mt <- resolve ga hd
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder putAssumps as
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder putTypeMap tm
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder let newT = case mt of Just trm -> trm
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder recurse $ QuantifiedTerm quant (catMaybes newDs) newT ps
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder LambdaTerm decls part hd ps -> do
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder mDecls <- mapM (resolvePattern ga) decls
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder let newDecls = catMaybes mDecls
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder anaDecls <- mapM anaPattern newDecls
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder let bs = concatMap extractVars anaDecls
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder checkUniqueVars bs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mapM_ addVarDecl bs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mt <- resolve ga hd
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder putAssumps as
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder let newT = case mt of Just trm -> trm
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder recurse $ LambdaTerm anaDecls part newT ps
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder CaseTerm hd eqs ps -> do
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mt <- resolve ga hd
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder let newT = case mt of Just trm -> trm
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder newEs <- resolveCaseEqs ga eqs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder recurse $ CaseTerm newT newEs ps
64558a09e6f6b95d2689d02dd5251339f8ac505bChristian Maeder LetTerm b eqs hd ps -> do
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder newEs <- resolveLetEqs ga eqs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mt <- resolve ga hd
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder let newT = case mt of Just trm -> trm
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder putAssumps as
64558a09e6f6b95d2689d02dd5251339f8ac505bChristian Maeder recurse $ LetTerm b newEs newT ps
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder TermToken tok -> do
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder let (ds1, trm) = convertMixfixToken
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder (literal_annos ga)
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder ResolvedMixTerm TermToken tok
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder self tt $ oneStep $
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder TermToken _ -> (trm, tok)
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder _ -> (trm, exprTok
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder {tokPos = tokPos tok})
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder AsPattern vd p ps -> do
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder mp <- resolvePattern ga p
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder let newP = case mp of Just pat -> pat
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder recurse $ AsPattern vd newP ps
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder _ -> error ("iterCharts: " ++ show t)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder-- * equation stuff
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEq ga (ProgEq p t ps) =
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder do mp <- resolvePattern ga p
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> return Nothing
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Just np -> do
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder as <- gets assumps
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder newP <- anaPattern np
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder let bs = extractVars newP
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder checkUniqueVars bs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mapM_ addVarDecl bs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mtt <- resolve ga t
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder putAssumps as
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder return $ case mtt of
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> Nothing
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Just newT -> Just $ ProgEq newP newT ps
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEqs _ [] = return []
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEqs ga (eq:rt) =
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder do mEq <- resolveCaseEq ga eq
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder eqs <- resolveCaseEqs ga rt
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder return $ case mEq of
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder Nothing -> eqs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Just newEq -> newEq : eqs
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs _ [] = return []
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs ga (ProgEq pat trm ps : rt) =
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder do mPat <- resolvePattern ga pat
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> do resolve ga trm
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder resolveLetEqs ga rt
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Just nPat -> do
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder newPat <- anaPattern nPat
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder let bs = extractVars newPat
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder checkUniqueVars bs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mapM addVarDecl bs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mTrm <- resolve ga trm
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder Nothing -> resolveLetEqs ga rt
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Just newTrm -> do
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder eqs <- resolveLetEqs ga rt
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder return (ProgEq newPat newTrm ps : eqs)
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian MaedermkPatAppl :: Term -> Term -> [Pos] -> Term
53301de22afd7190981b363b57c48df86fcb50f7Christian MaedermkPatAppl op arg qs =
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder QualVar (VarDecl i (MixfixType []) _ _) ->
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder ResolvedMixTerm i [arg] qs
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder _ -> ApplTerm op arg qs
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian MaedertoMixTerm :: Id -> [Term] -> [Pos] -> Term
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian MaedertoMixTerm i ar qs =
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder if i == applId then assert (length ar == 2) $
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder let [op, arg] = ar in mkPatAppl op arg qs
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder else if i == tupleId || i == unitId then
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder mkTupleTerm ar qs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder else if isUnknownId i then
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder QualVar $ VarDecl (simpleIdToId $ unToken i)
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder (MixfixType []) Other qs
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder else ResolvedMixTerm i ar qs
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian MaedergetKnowns :: Id -> Knowns
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian MaedergetKnowns (Id ts cs _) = Set.union (Set.fromList (map tokStr ts)) $
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maeder Set.unions (map getKnowns cs)
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian MaederresolvePattern :: GlobalAnnos -> Term -> State Env (Maybe Term)
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederresolvePattern ga = resolver ga (unknownId : builtinIds)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolve ga = resolver ga builtinIds
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolver :: GlobalAnnos -> [Id] -> Term
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder -> State Env (Maybe Term)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolver ga bs trm =
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder do as <- gets assumps
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder ps@((_, _, m), _) <- gets preIds
a1d523aa255a291c0154af764fbdb8597c445918Christian Maeder ks = Set.union (Set.fromList (tokStr exprTok: inS :
a1d523aa255a291c0154af764fbdb8597c445918Christian Maeder map (:[]) ":{}[](),"))
48708376ccab0e56251f53b0ec21499a277e9102Christian Maeder $ Set.unions $ map getKnowns ids
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder chart<- iterateCharts ga [trm] $
454b2a26b6ea95206df2f82768a8e12765f182bfChristian Maeder initChart (listRules (m + 3) ga ++
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder (initRules ps bs
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder ids)) (if unknownId `elem` bs then ks else Set.empty)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder let Result ds mr = getResolved showPretty (posOfTerm trm)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder toMixTerm chart
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds :: [Id]
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds = [unitId, parenId, tupleId, exprId, typeId, applId]
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederinitRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Rule]
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederinitRules (pm@(_, _, m), ps) bs is =
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder map ( \ i -> mixRule (getIdPrec pm ps i) i)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder (bs ++ is) ++
454b2a26b6ea95206df2f82768a8e12765f182bfChristian Maeder map ( \ i -> (protect i, m + 3, getPlainTokenList i))
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder (filter isMixfix is)