Overload.hs revision eb0ef4c8002fdf0d3c87b08a772258289833e046
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder{- |
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederModule : $Header$
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederDescription : Overload resolution
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederCopyright : (c) Martin Kuehl, T. Mossakowski, C. Maeder, 2004-2007
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
ea9ad77838dce923ced1df2ac09a7f0226363593Christian Maeder
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : Christian.Maeder@dfki.de
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederStability : provisional
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederOverload resolution (injections are inserted separately)
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder Follows Sect. III:3.3 of the CASL Reference Manual.
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder The algorthim is from:
ea9ad77838dce923ced1df2ac09a7f0226363593Christian Maeder Till Mossakowski, Kolyang, Bernd Krieg-Brueckner:
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder Static semantic analysis and theorem proving for CASL.
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder 12th Workshop on Algebraic Development Techniques, Tarquinia 1997,
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder LNCS 1376, p. 333-348
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder-}
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maedermodule CASL.Overload
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder ( minExpFORMULA
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , minExpFORMULAeq
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , minExpTerm
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder , isUnambiguous
dd836737068504898d4f7843ebd8a3df05f3067dChristian Maeder , oneExpTerm
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder , mkSorted
95936ba3a6577d40aae065aafac4147f5a308782Christian Maeder , Min
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder , leqF
dd836737068504898d4f7843ebd8a3df05f3067dChristian Maeder , leqP
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder , leqSort
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder , minimalSupers
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder , maximalSubs
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder , haveCommonSupersorts
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder , keepMinimals1
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder , keepMinimals
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder ) where
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder
62198789c7cb57cac13399055515921c0fe3483fChristian Maederimport CASL.Sign
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederimport CASL.AS_Basic_CASL
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder
62198789c7cb57cac13399055515921c0fe3483fChristian Maederimport qualified Common.Lib.Rel as Rel
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederimport Common.Lib.State
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maederimport Common.Id
62198789c7cb57cac13399055515921c0fe3483fChristian Maederimport Common.GlobalAnnotations
a255351561838b3743d03c1629d335cfb8b83804Christian Maederimport Common.DocUtils
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maederimport Common.Result
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maederimport Common.Partial
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maederimport Common.Utils
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maeder
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maederimport qualified Data.Map as Map
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maederimport qualified Data.Set as Set
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maederimport Control.Monad
b502963581a463467939d578b211cb7a173c5428Christian Maeder
906f0b21e2dc78ee4f37f879518be018a0204cd9Christian Maeder-- | the type of the type checking function of extensions
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maedertype Min f e = Sign f e -> f -> Result f
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaedermkSorted :: TermExtension f => Sign f e -> TERM f -> SORT -> Range -> TERM f
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaedermkSorted sign t s r = let nt = Sorted_term t s r in case optTermSort t of
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder Nothing -> nt
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder Just sort -> if leqSort sign s sort then t else nt
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder{- ----------------------------------------------------------
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder - Minimal expansion of a formula -
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder Expand a given formula by typing information.
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder * For non-atomic formulae, recurse through subsentences.
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder * For trival atomic formulae, no expansion is neccessary.
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder * For atomic formulae, the following cases are implemented:
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder + Predication is handled by the dedicated expansion function
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder 'minExpFORMULApred'.
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder + Existl_equation and Strong_equation are handled by the dedicated
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder expansion function 'minExpFORMULAeq'.
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder + Definedness is handled by expanding the subterm.
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder + Membership is handled like Cast
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski---------------------------------------------------------- -}
9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaederminExpFORMULA
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder :: (GetRange f, Pretty f, TermExtension f)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder => Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiminExpFORMULA mef sign formula = let sign0 = sign { envDiags = [] } in
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder case formula of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Quantification q vars f pos -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder -- add 'vars' to signature
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let sign' = execState (mapM_ addVars vars) sign0
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski Result (envDiags sign') $ Just ()
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder f' <- minExpFORMULA mef sign' f
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return (Quantification q vars f' pos)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder Conjunction fs pos -> do
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski fs' <- mapR (minExpFORMULA mef sign) fs
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder return (Conjunction fs' pos)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Disjunction fs pos -> do
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski fs' <- mapR (minExpFORMULA mef sign) fs
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder return (Disjunction fs' pos)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski Implication f1 f2 b pos ->
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder joinResultWith (\ f1' f2' -> Implication f1' f2' b pos)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder (minExpFORMULA mef sign f1) $ minExpFORMULA mef sign f2
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Equivalence f1 f2 pos ->
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski joinResultWith (\ f1' f2' -> Equivalence f1' f2' pos)
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder (minExpFORMULA mef sign f1) $ minExpFORMULA mef sign f2
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder Negation f pos -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder f' <- minExpFORMULA mef sign f
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return (Negation f' pos)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder Predication (Pred_name ide) terms pos
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski -> minExpFORMULApred mef sign ide Nothing terms pos
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski Predication (Qual_pred_name ide ty pos1) terms pos2
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski -> minExpFORMULApred mef sign ide (Just $ toPredType ty)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder terms (pos1 `appRange` pos2)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder Existl_equation term1 term2 pos
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski -> minExpFORMULAeq mef sign Existl_equation term1 term2 pos
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Strong_equation term1 term2 pos
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder -> minExpFORMULAeq mef sign Strong_equation term1 term2 pos
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Definedness term pos -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder t <- oneExpTerm mef sign term
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder return (Definedness t pos)
906f0b21e2dc78ee4f37f879518be018a0204cd9Christian Maeder Membership term sort pos -> do
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder ts <- minExpTerm mef sign term
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder let fs = map (concatMap ( \ t ->
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder map ( \ c ->
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Membership (mkSorted sign t c pos) sort pos)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder $ maybe [sort] (minimalSupers sign sort)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder $ optTermSort t)) ts
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder isUnambiguous (globAnnos sign) formula fs pos
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder ExtFORMULA f -> fmap ExtFORMULA $ mef sign f
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder QuantOp o ty f -> do
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder let sign' = sign0 { opMap = addOpTo o (toOpType ty) $ opMap sign0 }
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Result (envDiags sign') $ Just ()
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder f' <- minExpFORMULA mef sign' f
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder return $ QuantOp o ty f'
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder QuantPred p ty f -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let pm = predMap sign0
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder ptys = Map.findWithDefault Set.empty p pm
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder sign' = sign0
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder { predMap = Map.insert p (Set.insert (toPredType ty) ptys) pm }
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder Result (envDiags sign') $ Just ()
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder f' <- minExpFORMULA mef sign' f
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ QuantPred p ty f'
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_formula term -> do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder t <- oneExpTerm mef sign term
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder let Result ds mt = adjustPos (getRangeSpan term) $ termToFormula t
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder appendDiags ds
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder case mt of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Nothing -> mkError "not a formula" term
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Just f -> return f
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder _ -> return formula -- do not fail even for unresolved cases
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder-- | test if a term can be uniquely resolved
a255351561838b3743d03c1629d335cfb8b83804Christian MaederoneExpTerm :: (GetRange f, Pretty f, TermExtension f)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder => Min f e -> Sign f e -> TERM f -> Result (TERM f)
a255351561838b3743d03c1629d335cfb8b83804Christian MaederoneExpTerm minF sign term = do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder ts <- minExpTerm minF sign term
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder isUnambiguous (globAnnos sign) term ts nullRange
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder{- ----------------------------------------------------------
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder - Minimal expansion of an equation formula -
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder see minExpTermCond
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder---------------------------------------------------------- -}
a255351561838b3743d03c1629d335cfb8b83804Christian MaederminExpFORMULAeq :: (GetRange f, Pretty f, TermExtension f)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder => Min f e -> Sign f e -> (TERM f -> TERM f -> Range -> FORMULA f)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder -> TERM f -> TERM f -> Range -> Result (FORMULA f)
a255351561838b3743d03c1629d335cfb8b83804Christian MaederminExpFORMULAeq mef sign eq term1 term2 pos = do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder ps <- minExpTermCond mef sign ( \ t1 t2 -> eq t1 t2 pos)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder term1 term2 pos
95936ba3a6577d40aae065aafac4147f5a308782Christian Maeder isUnambiguous (globAnnos sign) (eq term1 term2 pos) ps pos
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder-- | check if there is at least one solution
a255351561838b3743d03c1629d335cfb8b83804Christian MaederhasSolutions :: Pretty f => GlobalAnnos -> f -> [[f]] -> Range
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder -> Result [[f]]
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaederhasSolutions ga topterm ts pos = let terms = filter (not . null) ts in
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder if null terms then Result
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder [Diag Error ("no typing for: " ++ showGlobalDoc ga topterm "")
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder pos] Nothing
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder else return terms
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder-- | check if there is a unique equivalence class
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaederisUnambiguous :: Pretty f => GlobalAnnos -> f -> [[f]] -> Range
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder -> Result f
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaederisUnambiguous ga topterm ts pos = do
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder terms <- hasSolutions ga topterm ts pos
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder case terms of
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder [ term : _ ] -> return term
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder _ -> Result [Diag Error ("ambiguous term\n " ++
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder showSepList (showString "\n ") (showGlobalDoc ga)
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder (take 5 $ map head terms) "") pos] Nothing
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder
26d3a8da6b4244d65614b5585927df4948e542a0Christian MaedercheckIdAndArgs :: Id -> [a] -> Range -> Result Int
a255351561838b3743d03c1629d335cfb8b83804Christian MaedercheckIdAndArgs ide args poss =
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder let nargs = length args
dd836737068504898d4f7843ebd8a3df05f3067dChristian Maeder pargs = placeCount ide
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder in if isMixfix ide && pargs /= nargs then
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder Result [Diag Error
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder ("expected " ++ shows pargs " argument(s) of mixfix identifier '"
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder ++ showDoc ide "' but found " ++ shows nargs " argument(s)")
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder poss] Nothing
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder else return nargs
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaedernoOpOrPredDiag :: Pretty t => [a] -> DiagKind -> String -> Maybe t -> Id
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder -> Range -> Int -> [Diagnosis]
a255351561838b3743d03c1629d335cfb8b83804Christian MaedernoOpOrPredDiag ops k str mty ide pos nargs = case ops of
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder [] -> let
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder hd = "no " ++ str ++ " with "
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder ft = " found for '" ++ showDoc ide "'"
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder in [Diag k (case mty of
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder Nothing -> hd ++ shows nargs " argument"
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder ++ (if nargs == 1 then "" else "s") ++ ft
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Just ty -> hd ++ "profile '" ++ showDoc ty "'" ++ ft) pos]
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder _ -> []
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaedernoOpOrPred :: Pretty t => [a] -> String -> Maybe t -> Id -> Range -> Int
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder -> Result ()
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaedernoOpOrPred ops str mty ide pos nargs = when (null ops) $ Result
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder (noOpOrPredDiag ops Error str mty ide pos nargs) Nothing
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder{- ----------------------------------------------------------
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder - Minimal expansion of a predication formula -
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder see minExpTermAppl
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder---------------------------------------------------------- -}
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaederminExpFORMULApred :: (GetRange f, Pretty f, TermExtension f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder => Min f e -> Sign f e -> Id -> Maybe PredType -> [TERM f] -> Range
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder -> Result (FORMULA f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaederminExpFORMULApred mef sign ide mty args pos = do
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder nargs <- checkIdAndArgs ide args pos
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let -- predicates matching that name in the current environment
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder preds' = Set.filter ((nargs ==) . length . predArgs) $
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Map.findWithDefault Set.empty ide $ predMap sign
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder preds = case mty of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Nothing -> map (pSortBy predArgs sign)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder $ Rel.leqClasses (leqP' sign) preds'
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder Just ty -> [[ty] | Set.member ty preds']
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder boolAna l cmd = case mty of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Nothing | null l -> do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder appendDiags $ noOpOrPredDiag preds Warning
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder "matching predicate" mty ide pos nargs
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder minExpFORMULA mef sign $ Mixfix_formula
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder $ Application (Op_name ide) args pos
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder _ -> cmd
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder boolAna preds $ do
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder noOpOrPred preds "predicate" mty ide pos nargs
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder expansions <- mapM (minExpTerm mef sign) args
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let getProfiles cs = map (getProfile cs) preds
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder getProfile cs ps = [ (pred', ts) |
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder pred' <- ps,
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder ts <- cs,
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder and $ zipWith (leqSort sign)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (map sortOfTerm ts)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (predArgs pred') ]
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder qualForms = qualifyPreds ide pos
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder $ concatMap (getProfiles . combine)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder $ combine expansions
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder boolAna qualForms
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder $ isUnambiguous (globAnnos sign)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (Predication (Pred_name ide) args pos) qualForms pos
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian MaederqualifyPreds :: Id -> Range -> [[(PredType, [TERM f])]] -> [[FORMULA f]]
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaederqualifyPreds ide = map . map . qualifyPred ide
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder-- | qualify a single pred, given by its signature and its arguments
a255351561838b3743d03c1629d335cfb8b83804Christian MaederqualifyPred :: Id -> Range -> (PredType, [TERM f]) -> FORMULA f
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaederqualifyPred ide pos (pred', terms') =
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Predication (Qual_pred_name ide (toPRED_TYPE pred') pos) terms' pos
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder-- | expansions of an equation formula or a conditional
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaederminExpTermEq :: (GetRange f, Pretty f, TermExtension f)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder => Min f e -> Sign f e -> TERM f -> TERM f -> Result [[(TERM f, TERM f)]]
a255351561838b3743d03c1629d335cfb8b83804Christian MaederminExpTermEq mef sign term1 term2 = do
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder exps1 <- minExpTerm mef sign term1
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder exps2 <- minExpTerm mef sign term2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ map (minimizeEq sign . getPairs) $ combine [exps1, exps2]
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian MaedergetPairs :: [[TERM f]] -> [(TERM f, TERM f)]
a255351561838b3743d03c1629d335cfb8b83804Christian MaedergetPairs cs = [ (t1, t2) | [t1, t2] <- combine cs ]
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian MaederminimizeEq :: TermExtension f => Sign f e -> [(TERM f, TERM f)]
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski -> [(TERM f, TERM f)]
a255351561838b3743d03c1629d335cfb8b83804Christian MaederminimizeEq s = keepMinimals s (sortOfTerm . snd)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder . keepMinimals s (sortOfTerm . fst)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder{- ----------------------------------------------------------
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder - Minimal expansion of a term -
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Expand a given term by typing information.
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder * 'Qual_var' terms are handled by 'minExpTerm_var'
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder * 'Application' terms are handled by 'minExpTermOp'.
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder * 'Conditional' terms are handled by 'minExpTermCond'.
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder---------------------------------------------------------- -}
minExpTerm :: (GetRange f, Pretty f, TermExtension f)
=> Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
minExpTerm mef sign top = let ga = globAnnos sign in case top of
Qual_var var sort _ -> let ts = minExpTermVar sign var (Just sort) in
if null ts then mkError "no matching qualified variable found" var
else return ts
Application op terms pos -> minExpTermOp mef sign op terms pos
Sorted_term term sort pos -> do
expandedTerm <- minExpTerm mef sign term
-- choose expansions that fit the given signature, then qualify
let validExps =
map (filter (maybe True (flip (leqSort sign) sort)
. optSortOfTerm (const Nothing)))
expandedTerm
hasSolutions ga top (map (map (\ t ->
Sorted_term t sort pos)) validExps) pos
Cast term sort pos -> do
expandedTerm <- minExpTerm mef sign term
-- find a unique minimal common supersort
let ts = map (concatMap (\ t ->
map ( \ c ->
Cast (mkSorted sign t c pos) sort pos)
$ maybe [sort] (minimalSupers sign sort)
$ optTermSort t)) expandedTerm
hasSolutions ga top ts pos
Conditional term1 formula term2 pos -> do
f <- minExpFORMULA mef sign formula
ts <- minExpTermCond mef sign ( \ t1 t2 -> Conditional t1 f t2 pos)
term1 term2 pos
hasSolutions ga (Conditional term1 formula term2 pos) ts pos
ExtTERM t -> do
nt <- mef sign t
return [[ExtTERM nt]]
_ -> mkError "unexpected kind of term" top
-- | Minimal expansion of a possibly qualified variable identifier
minExpTermVar :: Sign f e -> Token -> Maybe SORT -> [[TERM f]]
minExpTermVar sign tok ms = case Map.lookup tok $ varMap sign of
Nothing -> []
Just s -> let qv = [[Qual_var tok s nullRange]] in
case ms of
Nothing -> qv
Just s2 -> if s == s2 then qv else []
-- | minimal expansion of an (possibly qualified) operator application
minExpTermAppl :: (GetRange f, Pretty f, TermExtension f)
=> Min f e -> Sign f e -> Id -> Maybe OpType -> [TERM f] -> Range
-> Result [[TERM f]]
minExpTermAppl mef sign ide mty args pos = do
nargs <- checkIdAndArgs ide args pos
let -- functions matching that name in the current environment
ops' = Set.filter ( \ o -> length (opArgs o) == nargs) $
Map.findWithDefault Set.empty ide $ opMap sign
ops = case mty of
Nothing -> map (pSortBy opArgs sign)
$ Rel.leqClasses (leqF' sign) ops'
Just ty -> [[ty] | Set.member ty ops' ||
-- might be known to be total
Set.member ty {opKind = Total} ops' ]
noOpOrPred ops "operation" mty ide pos nargs
expansions <- mapM (minExpTerm mef sign) args
let -- generate profiles as descr. on p. 339 (Step 3)
getProfiles cs = map (getProfile cs) ops
getProfile cs os = [ (op', ts) |
op' <- os,
ts <- cs,
and $ zipWith (leqSort sign)
(map sortOfTerm ts)
(opArgs op') ]
qualTerms = qualifyOps ide pos
$ map (minimizeOp sign)
$ concatMap (getProfiles . combine)
$ combine expansions
hasSolutions (globAnnos sign)
(Application (Op_name ide) args pos) qualTerms pos
qualifyOps :: Id -> Range -> [[(OpType, [TERM f])]] -> [[TERM f]]
qualifyOps ide = map . map . qualifyOp ide
-- qualify a single op, given by its signature and its arguments
qualifyOp :: Id -> Range -> (OpType, [TERM f]) -> TERM f
qualifyOp ide pos (op', terms') =
Application (Qual_op_name ide (toOP_TYPE op') pos) terms' pos
{- ----------------------------------------------------------
- Minimal expansion of a function application or a variable -
Expand a function application by typing information.
1. First expand all argument subterms.
2. Combine these expansions so we compute the set of tuples
{ (C_1, ..., C_n) | (C_1, ..., C_n) \in
minExpTerm(t_1) x ... x minExpTerm(t_n) }
where t_1, ..., t_n are the given argument terms.
3. For each element of this set compute the set of possible profiles
(as described on p. 339).
4. Define an equivalence relation ~ on these profiles
(as described on p. 339).
5. Separate each profile into equivalence classes by the relation ~
and take the unification of these sets.
6. Minimize each element of this unified set (as described on p. 339).
7. Transform each term in the minimized set into a qualified function
application term.
---------------------------------------------------------- -}
minExpTermOp :: (GetRange f, Pretty f, TermExtension f)
=> Min f e -> Sign f e -> OP_SYMB -> [TERM f] -> Range -> Result [[TERM f]]
minExpTermOp mef sign osym args pos = case osym of
Op_name ide@(Id ts _ _) ->
let res = minExpTermAppl mef sign ide Nothing args pos in
if null args && isSimpleId ide then
let vars = minExpTermVar sign (head ts) Nothing
in if null vars then res else
case maybeResult res of
Nothing -> return vars
Just ops -> return $ ops ++ vars
else res
Qual_op_name ide ty pos1 ->
if length args /= length (args_OP_TYPE ty) then
mkError "type qualification does not match number of arguments" ide
else minExpTermAppl mef sign ide (Just $ toOpType ty) args
(pos1 `appRange` pos)
{- ----------------------------------------------------------
- Minimal expansion of a conditional -
Expand a conditional by typing information (see minExpTermEq)
First expand the subterms and subformula. Then calculate a profile
P(C_1, C_2) for each (C_1, C_2) \in minExpTerm(t1) x minExpTerm(t_2).
Separate these profiles into equivalence classes and take the
unification of all these classes. Minimize each equivalence class.
Finally transform the eq. classes into lists of
conditionals with equally sorted terms.
---------------------------------------------------------- -}
minExpTermCond :: (GetRange f, Pretty f, TermExtension f)
=> Min f e -> Sign f e -> (TERM f -> TERM f -> a) -> TERM f -> TERM f
-> Range -> Result [[a]]
minExpTermCond mef sign f term1 term2 pos = do
pairs <- minExpTermEq mef sign term1 term2
return $ map (concatMap ( \ (t1, t2) ->
let s1 = sortOfTerm t1
s2 = sortOfTerm t2
in map ( \ s -> f (mkSorted sign t1 s pos)
(mkSorted sign t2 s pos))
$ minimalSupers sign s1 s2)) pairs
{- ----------------------------------------------------------
Let P be a set of equivalence classes of qualified terms.
For each C \in P, let C' choose _one_
t:s \in C for each s minimal such that t:s \in C.
That is, discard all terms whose sort is a supersort of
any other term in the same equivalence class.
---------------------------------------------------------- -}
minimizeOp :: Sign f e -> [(OpType, [TERM f])] -> [(OpType, [TERM f])]
minimizeOp sign = keepMinimals sign (opRes . fst)
-- | the (possibly incomplete) list of supersorts common to both sorts
commonSupersorts :: Bool -> Sign f e -> SORT -> SORT -> [SORT]
commonSupersorts b sign s1 s2 =
if s1 == s2 then [s1] else
let l1 = supersortsOf s1 sign
l2 = supersortsOf s2 sign in
if Set.member s2 l1 then if b then [s2] else [s1] else
if Set.member s1 l2 then if b then [s1] else [s2] else
Set.toList $ if b then Set.intersection l1 l2
else Set.intersection (subsortsOf s1 sign)
$ subsortsOf s2 sign
-- | True if both sorts have a common supersort
haveCommonSupersorts :: Bool -> Sign f e -> SORT -> SORT -> Bool
haveCommonSupersorts b s s1 = not . null . commonSupersorts b s s1
-- True if both sorts have a common subsort
haveCommonSubsorts :: Sign f e -> SORT -> SORT -> Bool
haveCommonSubsorts = haveCommonSupersorts False
-- | if True test if s1 > s2
geqSort :: Bool -> Sign f e -> SORT -> SORT -> Bool
geqSort b sign s1 s2 = s1 == s2 || let rel = sortRel sign in
if b then Rel.member s2 s1 rel else Rel.member s1 s2 rel
-- | test if s1 < s2
leqSort :: Sign f e -> SORT -> SORT -> Bool
leqSort = geqSort False
-- | minimal common supersorts of the two input sorts
minimalSupers :: Sign f e -> SORT -> SORT -> [SORT]
minimalSupers = minimalSupers1 True
minimalSupers1 :: Bool -> Sign f e -> SORT -> SORT -> [SORT]
minimalSupers1 b s s1 = keepMinimals1 b s id . commonSupersorts b s s1
-- | maximal common subsorts of the two input sorts
maximalSubs :: Sign f e -> SORT -> SORT -> [SORT]
maximalSubs = minimalSupers1 False
-- | only keep elements with minimal (and different) sorts
keepMinimals :: Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals = keepMinimals1 True
keepMinimals1 :: Bool -> Sign f e -> (a -> SORT) -> [a] -> [a]
keepMinimals1 b s f = let lt x y = geqSort b s (f y) (f x) in keepMins lt
-- | True if both ops are in the overloading relation
leqF :: Sign f e -> OpType -> OpType -> Bool
leqF sign o1 o2 = length (opArgs o1) == length (opArgs o2) && leqF' sign o1 o2
leqF' :: Sign f e -> OpType -> OpType -> Bool
leqF' sign o1 o2 = haveCommonSupersorts True sign (opRes o1) (opRes o2) &&
and (zipWith (haveCommonSubsorts sign) (opArgs o1) (opArgs o2))
-- | True if both preds are in the overloading relation
leqP :: Sign f e -> PredType -> PredType -> Bool
leqP sign p1 p2 = length (predArgs p1) == length (predArgs p2)
&& leqP' sign p1 p2
leqP' :: Sign f e -> PredType -> PredType -> Bool
leqP' sign p1 =
and . zipWith (haveCommonSubsorts sign) (predArgs p1) . predArgs
cmpSubsort :: Sign f e -> POrder SORT
cmpSubsort sign s1 s2 =
if s1 == s2 then Just EQ else
let l1 = supersortsOf s1 sign
l2 = supersortsOf s2 sign
b = Set.member s1 l2 in
if Set.member s2 l1 then
if b then Just EQ
else Just LT
else if b then Just GT else Nothing
cmpSubsorts :: Sign f e -> POrder [SORT]
cmpSubsorts sign l1 l2 =
let l = zipWith (cmpSubsort sign) l1 l2
in if null l then Just EQ else foldr1
( \ c1 c2 -> if c1 == c2 then c1 else case (c1, c2) of
(Just EQ, _) -> c2
(_, Just EQ) -> c1
_ -> Nothing) l
pSortBy :: (a -> [SORT]) -> Sign f e -> [a] -> [a]
pSortBy f sign = let pOrd a b = cmpSubsorts sign (f a) (f b)
in concat . rankBy pOrd