Overload.hs revision b32596e241446281ecf820b277f5b85466f99821
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 , haveCommonSubsorts
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder , keepMinimals1
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder , keepMinimals
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder ) where
62198789c7cb57cac13399055515921c0fe3483fChristian Maeder
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederimport CASL.ToDoc (FormExtension)
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maederimport CASL.Sign
62198789c7cb57cac13399055515921c0fe3483fChristian Maederimport CASL.AS_Basic_CASL
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maederimport qualified Common.Lib.MapSet as MapSet
62198789c7cb57cac13399055515921c0fe3483fChristian Maederimport qualified Common.Lib.Rel as Rel
a255351561838b3743d03c1629d335cfb8b83804Christian Maederimport Common.Lib.State
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maederimport Common.Id
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maederimport Common.GlobalAnnotations
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maederimport Common.DocUtils
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maederimport Common.Result
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maederimport Common.Partial
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maederimport Common.Utils
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maederimport Data.List
b502963581a463467939d578b211cb7a173c5428Christian Maederimport Data.Maybe
906f0b21e2dc78ee4f37f879518be018a0204cd9Christian Maederimport qualified Data.Map as Map
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederimport qualified Data.Set as Set
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederimport Control.Monad
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder-- | the type of the type checking function of extensions
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maedertype Min f e = Sign f e -> f -> Result f
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaedermkSorted :: TermExtension f => Sign f e -> TERM f -> SORT -> Range -> TERM f
eed6203a39f88e398d86431a66d367036a3d17baChristian MaedermkSorted sign t s r = let nt = Sorted_term t s r in case optTermSort t of
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder Nothing -> nt
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder Just srt -> if leqSort sign s srt then t else nt
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder{- ----------------------------------------------------------
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian 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.
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder * For atomic formulae, the following cases are implemented:
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder + Predication is handled by the dedicated expansion function
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski 'minExpFORMULApred'.
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder + Existl_equation and Strong_equation are handled by the dedicated
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder expansion function 'minExpFORMULAeq'.
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder + Definedness is handled by expanding the subterm.
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski + Membership is handled like Cast
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder---------------------------------------------------------- -}
a255351561838b3743d03c1629d335cfb8b83804Christian MaederminExpFORMULA
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder :: (FormExtension 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
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder case formula of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Quantification q vars f pos -> do
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder -- add 'vars' to signature
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski let sign' = execState (mapM_ addVars vars) sign0
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Result (envDiags sign') $ Just ()
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder f' <- minExpFORMULA mef sign' f
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski return (Quantification q vars f' pos)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder Junction j fs pos -> do
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski fs' <- mapR (minExpFORMULA mef sign) fs
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder return (Junction j fs' pos)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Relation f1 c f2 pos ->
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder joinResultWith (\ f1' f2' -> Relation f1' c f2' pos)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski (minExpFORMULA mef sign f1) $ minExpFORMULA mef sign f2
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder Negation f pos -> do
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder f' <- minExpFORMULA mef sign f
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return (Negation f' pos)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Predication (Pred_name ide) terms pos
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder -> 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)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski terms (pos1 `appRange` pos2)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Equation term1 e term2 pos
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder -> minExpFORMULAeq mef sign (`Equation` e) term1 term2 pos
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski Definedness term pos -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder t <- oneExpTerm mef sign term
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return (Definedness t pos)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Membership term srt pos -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder ts <- minExpTerm mef sign term
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let fs = map (concatMap ( \ t ->
906f0b21e2dc78ee4f37f879518be018a0204cd9Christian Maeder map ( \ c ->
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder Membership (mkSorted sign t c pos) srt pos)
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder $ maybe [srt] (minimalSupers sign srt)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder $ optTermSort t)) ts
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder isUnambiguous "" (globAnnos sign) formula fs pos
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder ExtFORMULA f -> fmap ExtFORMULA $ mef sign f
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder QuantOp o ty f -> do
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder let sign' = sign0 { opMap = addOpTo o (toOpType ty) $ opMap sign0 }
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Result (envDiags sign') $ Just ()
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder f' <- minExpFORMULA mef sign' f
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder return $ QuantOp o ty f'
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder QuantPred p ty f -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let pm = predMap sign0
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder sign' = sign0
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder { predMap = MapSet.insert p (toPredType ty) pm }
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Result (envDiags sign') $ Just ()
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder f' <- minExpFORMULA mef sign' f
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder return $ QuantPred p ty f'
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_formula term -> do
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder t <- oneExpTerm mef sign term
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder let Result ds mt = adjustPos (getRangeSpan term) $ termToFormula t
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder appendDiags ds
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder case mt of
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Nothing -> mkError "not a formula" term
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian 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 :: (FormExtension 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
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder{- ----------------------------------------------------------
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder - Minimal expansion of an equation formula -
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder see minExpTermCond
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder---------------------------------------------------------- -}
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaederminExpFORMULAeq :: (FormExtension f, TermExtension f)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder => Min f e -> Sign f e -> (TERM f -> TERM f -> Range -> FORMULA f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian 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)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder term1 term2 pos
a255351561838b3743d03c1629d335cfb8b83804Christian 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 => String -> GlobalAnnos -> f -> [[f]] -> Range
95936ba3a6577d40aae065aafac4147f5a308782Christian Maeder -> Result [[f]]
a255351561838b3743d03c1629d335cfb8b83804Christian MaederhasSolutions msg ga topterm ts pos = let terms = filter (not . null) ts in
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder if null terms then Result
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder [Diag Error ("no typing for: " ++ showGlobalDoc ga topterm "" ++ msg)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder pos] Nothing
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder else return terms
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder-- | check if there is a unique equivalence class
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaederisUnambiguous :: Pretty f => String -> GlobalAnnos -> f -> [[f]] -> Range
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder -> Result f
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaederisUnambiguous msg ga topterm ts pos = do
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder terms <- hasSolutions msg ga topterm ts pos
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder case terms of
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder [ term : _ ] -> return term
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder _ -> Result [Diag Error ("ambiguous term\n " ++
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder showSepList (showString "\n ") (showGlobalDoc ga)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder (take 5 $ map head terms) "") pos] Nothing
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder
26d3a8da6b4244d65614b5585927df4948e542a0Christian MaedercheckIdAndArgs :: Id -> [a] -> Range -> Result Int
26d3a8da6b4244d65614b5585927df4948e542a0Christian MaedercheckIdAndArgs ide args poss =
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder let nargs = length args
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder pargs = placeCount ide
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder in if isMixfix ide && pargs /= nargs then
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Result [Diag Error
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder ("expected " ++ shows pargs " argument(s) of mixfix identifier '"
dd836737068504898d4f7843ebd8a3df05f3067dChristian Maeder ++ showDoc ide "' but found " ++ shows nargs " argument(s)")
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder poss] Nothing
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder else return nargs
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedernoOpOrPredDiag :: Pretty t => [a] -> DiagKind -> String -> Maybe t -> Id
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder -> Range -> Int -> [Diagnosis]
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaedernoOpOrPredDiag ops k str mty ide pos nargs = case ops of
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder [] -> let
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder hd = "no " ++ str ++ " with "
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder ft = " found for '" ++ showDoc ide "'"
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in [Diag k (case mty of
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder Nothing -> hd ++ shows nargs " argument"
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder ++ (if nargs == 1 then "" else "s") ++ ft
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder Just ty -> hd ++ "profile '" ++ showDoc ty "'" ++ ft) pos]
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder _ -> []
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaedernoOpOrPred :: Pretty t => [a] -> String -> Maybe t -> Id -> Range -> Int
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder -> Result ()
9256f871e7dd915ccfb5969e2117f054306cd366Christian MaedernoOpOrPred ops str mty ide pos nargs = when (null ops) $ Result
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder (noOpOrPredDiag ops Error str mty ide pos nargs) Nothing
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder{- ----------------------------------------------------------
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder - Minimal expansion of a predication formula -
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder see minExpTermAppl
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder---------------------------------------------------------- -}
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaederminExpFORMULApred :: (FormExtension f, TermExtension f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder => Min f e -> Sign f e -> Id -> Maybe PredType -> [TERM f] -> Range
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder -> Result (FORMULA f)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederminExpFORMULApred mef sign ide mty args pos = do
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder nargs <- checkIdAndArgs ide args pos
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder let -- predicates matching that name in the current environment
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder preds' = Set.filter ((nargs ==) . length . predArgs) $
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder MapSet.lookup ide $ predMap sign
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder preds = case mty of
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Nothing -> map (pSortBy predArgs sign)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder $ Rel.leqClasses (leqP' sign) preds'
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Just ty -> [[ty] | Set.member ty preds']
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder boolAna l cmd = case mty of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Nothing | null l -> do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder appendDiags $ noOpOrPredDiag preds Hint
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder "matching predicate" mty ide pos nargs
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder minExpFORMULA mef sign $ Mixfix_formula
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder $ Application (Op_name ide) args pos
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder _ -> cmd
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder boolAna preds $ do
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder noOpOrPred preds "predicate" mty ide pos nargs
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder expansions <- mapM (minExpTerm mef sign) args
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let formCombs = concatMap (getCombs sign predArgs preds . combine)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder $ combine expansions
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder partCombs = map (partition $ \ (_, _, m) -> isNothing m) formCombs
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (goodCombs, badCombs) = unzip partCombs
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder badCs@(_ : _) = concat badCombs
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder maxArg = maximum $ map (\ (_, _, Just c) -> c) badCs
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder badCs2 = filter (\ (_, _, Just c) -> maxArg == c) badCs
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder expectedTs = keepMinimals1 False sign id
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder $ map (\ (a, _, _) -> predArgs a !! maxArg) badCs2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder foundTs = keepMinimals sign id
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder $ map (\ (_, ts, _) -> sortOfTerm $ ts !! maxArg) badCs2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder qualForms = qualifyGFs qualifyPred ide pos goodCombs
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder boolAna qualForms
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder $ isUnambiguous (missMsg maxArg ide foundTs expectedTs) (globAnnos sign)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (Predication (Pred_name ide) args pos) qualForms pos
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaedermissMsg :: Int -> Id -> [SORT] -> [SORT] -> String
a255351561838b3743d03c1629d335cfb8b83804Christian MaedermissMsg maxArg ide foundTs expectedTs =
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let showSort s = case s of
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder [ft] -> "a term of sort '" ++ shows ft "' was "
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder _ -> "terms of sorts " ++ showDoc s " were "
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder "\nin the " ++ show (maxArg + 1) ++ ". argument of '" ++ shows ide "'\n"
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ++ showSort foundTs ++ "found but\n"
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder ++ showSort expectedTs ++ "expected."
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian MaedergetCombs :: TermExtension f => Sign f e -> (a -> [SORT]) -> [[a]] -> [[TERM f]]
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder -> [[(a, [TERM f], Maybe Int)]]
a255351561838b3743d03c1629d335cfb8b83804Christian MaedergetCombs sign getArgs = flip $ map . \ cs fs ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder [ (f, ts, elemIndex False $ zipWith (leqSort sign) (map sortOfTerm ts)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder $ getArgs f) | f <- fs, ts <- cs ]
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian MaedergetProfiles :: TermExtension f => Sign f e -> (a -> [SORT]) -> [[a]]
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder -> [[TERM f]] -> [[(a, [TERM f])]]
a255351561838b3743d03c1629d335cfb8b83804Christian MaedergetProfiles sign getArgs = flip $ map . \ cs fs ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder [ (f, ts) | f <- fs, ts <- cs
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder , and $ zipWith (leqSort sign) (map sortOfTerm ts) (getArgs f) ]
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiqualifyGFs :: (Id -> Range -> (a, [TERM f]) -> b) -> Id -> Range
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder -> [[(a, [TERM f], Maybe Int)]] -> [[b]]
a255351561838b3743d03c1629d335cfb8b83804Christian MaederqualifyGFs f ide pos = map $ map (f ide pos . \ (a, b, _) -> (a, b))
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder
a255351561838b3743d03c1629d335cfb8b83804Christian MaederqualifyFs :: (Id -> Range -> (a, [TERM f]) -> b) -> Id -> Range
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder -> [[(a, [TERM f])]] -> [[b]]
a255351561838b3743d03c1629d335cfb8b83804Christian MaederqualifyFs f ide = map . map . f 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') =
Predication (Qual_pred_name ide (toPRED_TYPE pred') pos) terms' pos
-- | expansions of an equation formula or a conditional
minExpTermEq :: (FormExtension f, TermExtension f)
=> Min f e -> Sign f e -> TERM f -> TERM f -> Result [[(TERM f, TERM f)]]
minExpTermEq mef sign term1 term2 = do
exps1 <- minExpTerm mef sign term1
exps2 <- minExpTerm mef sign term2
return $ map (minimizeEq sign . getPairs) $ combine [exps1, exps2]
getPairs :: [[TERM f]] -> [(TERM f, TERM f)]
getPairs cs = [ (t1, t2) | [t1, t2] <- combine cs ]
minimizeEq :: TermExtension f => Sign f e -> [(TERM f, TERM f)]
-> [(TERM f, TERM f)]
minimizeEq s = keepMinimals s (sortOfTerm . snd)
. keepMinimals s (sortOfTerm . fst)
{- ----------------------------------------------------------
- Minimal expansion of a term -
Expand a given term by typing information.
* 'Qual_var' terms are handled by 'minExpTerm_var'
* 'Application' terms are handled by 'minExpTermOp'.
* 'Conditional' terms are handled by 'minExpTermCond'.
---------------------------------------------------------- -}
minExpTerm :: (FormExtension 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 srt _ -> let ts = minExpTermVar sign var (Just srt) 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 srt 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) srt)
. optSortOfTerm (const Nothing)))
expandedTerm
hasSolutions "" ga top (map (map (\ t ->
Sorted_term t srt pos)) validExps) pos
Cast term srt 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) srt pos)
$ maybe [srt] (minimalSupers sign srt)
$ 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 :: (FormExtension 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) $
MapSet.lookup 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 (mkTotal ty) ops' ]
noOpOrPred ops "operation" mty ide pos nargs
expansions <- mapM (minExpTerm mef sign) args
let -- generate profiles as descr. on p. 339 (Step 3)
qualTerms = qualifyFs qualifyOp ide pos
$ map (minimizeOp sign)
$ concatMap (getProfiles sign opArgs ops . combine)
$ combine expansions
hasSolutions "" (globAnnos sign)
(Application (Op_name ide) args pos) qualTerms pos
-- 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 :: (FormExtension 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 :: (FormExtension 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