a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder{- |

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederModule : $Header$

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederDescription : Overload resolution

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederCopyright : (c) Martin Kuehl, T. Mossakowski, C. Maeder, 2004-2007

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederMaintainer : Christian.Maeder@dfki.de

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederStability : provisional

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederPortability : portable

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederOverload resolution (injections are inserted separately)

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder Follows Sect. III:3.3 of the CASL Reference Manual.

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder The algorthim is from:

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder Till Mossakowski, Kolyang, Bernd Krieg-Brueckner:

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder Static semantic analysis and theorem proving for CASL.

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder 12th Workshop on Algebraic Development Techniques, Tarquinia 1997,

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder LNCS 1376, p. 333-348

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder-}

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maedermodule CASL.Overload

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder ( minExpFORMULA

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , minExpFORMULAeq

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , minExpTerm

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , isUnambiguous

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , oneExpTerm

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , mkSorted

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , Min

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , leqF

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , leqP

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , leqSort

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , minimalSupers

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , maximalSubs

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , haveCommonSupersorts

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , haveCommonSubsorts

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , keepMinimals1

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder , keepMinimals

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder ) where

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport CASL.ToDoc (FormExtension)

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport CASL.Sign

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maederimport CASL.AS_Basic_CASL

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maederimport qualified Common.Lib.MapSet as MapSet

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maederimport qualified Common.Lib.Rel as Rel

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maederimport Common.Lib.State

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maederimport Common.Id

06f58a67e6df999858bf4f97d5e0786956562d29Christian Maederimport Common.GlobalAnnotations

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maederimport Common.DocUtils

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maederimport Common.Result

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maederimport Common.Partial

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maederimport Common.Utils

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maederimport Data.List

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maederimport Data.Maybe

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maederimport qualified Data.Map as Map

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maederimport qualified Data.Set as Set

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport Control.Monad

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder-- | the type of the type checking function of extensions

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maedertype Min f e = Sign f e -> f -> Result f

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian MaedermkSorted :: TermExtension f => Sign f e -> TERM f -> SORT -> Range -> TERM f

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian MaedermkSorted sign t s r = let nt = Sorted_term t s r in case optTermSort t of

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder Nothing -> nt

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder Just srt -> if leqSort sign s srt then t else nt

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder

bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder{- ----------------------------------------------------------

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder - Minimal expansion of a formula -

bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder Expand a given formula by typing information.

bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder * For non-atomic formulae, recurse through subsentences.

bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder * For trival atomic formulae, no expansion is neccessary.

bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder * For atomic formulae, the following cases are implemented:

bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder + Predication is handled by the dedicated expansion function

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder 'minExpFORMULApred'.

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder + Existl_equation and Strong_equation are handled by the dedicated

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder expansion function 'minExpFORMULAeq'.

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder + Definedness is handled by expanding the subterm.

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder + Membership is handled like Cast

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder---------------------------------------------------------- -}

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian MaederminExpFORMULA

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder :: (FormExtension f, TermExtension f)

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder => Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian MaederminExpFORMULA mef sign formula = let sign0 = sign { envDiags = [] } in

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder case formula of

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder Quantification q vars f pos -> do

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder -- add 'vars' to signature

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder let sign' = execState (mapM_ addVars vars) sign0

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder Result (envDiags sign') $ Just ()

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder f' <- minExpFORMULA mef sign' f

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder return (Quantification q vars f' pos)

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder Junction j fs pos -> do

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder fs' <- mapR (minExpFORMULA mef sign) fs

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder return (Junction j fs' pos)

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder Relation f1 c f2 pos ->

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder joinResultWith (\ f1' f2' -> Relation f1' c f2' pos)

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder (minExpFORMULA mef sign f1) $ minExpFORMULA mef sign f2

d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder Negation f pos -> do

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder f' <- minExpFORMULA mef sign f

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder return (Negation f' pos)

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder Predication (Pred_name ide) terms pos

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder -> minExpFORMULApred mef sign ide Nothing terms pos

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder Predication (Qual_pred_name ide ty pos1) terms pos2

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder -> minExpFORMULApred mef sign ide (Just $ toPredType ty)

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder terms (pos1 `appRange` pos2)

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder Equation term1 e term2 pos

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder -> minExpFORMULAeq mef sign (`Equation` e) term1 term2 pos

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Definedness term pos -> do

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder t <- oneExpTerm mef sign term

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder return (Definedness t pos)

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Membership term srt pos -> do

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder ts <- minExpTerm mef sign term

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder let fs = map (concatMap ( \ t ->

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder map ( \ c ->

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Membership (mkSorted sign t c pos) srt pos)

36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder $ maybe [srt] (minimalSupers sign srt)

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder $ optTermSort t)) ts

7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder isUnambiguous "" (globAnnos sign) formula fs pos

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder ExtFORMULA f -> fmap ExtFORMULA $ mef sign f

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder QuantOp o ty f -> do

13140d161d2d2d11d87283d01d57ee3a738a833dChristian Maeder let sign' = sign0 { opMap = addOpTo o (toOpType ty) $ opMap sign0 }

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder Result (envDiags sign') $ Just ()

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder f' <- minExpFORMULA mef sign' f

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder return $ QuantOp o ty f'

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder QuantPred p ty f -> do

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder let pm = predMap sign0

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder sign' = sign0

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder { predMap = MapSet.insert p (toPredType ty) pm }

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder Result (envDiags sign') $ Just ()

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder f' <- minExpFORMULA mef sign' f

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder return $ QuantPred p ty f'

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Mixfix_formula term -> do

38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder t <- oneExpTerm mef sign term

13140d161d2d2d11d87283d01d57ee3a738a833dChristian Maeder let Result ds mt = adjustPos (getRangeSpan term) $ termToFormula t

13140d161d2d2d11d87283d01d57ee3a738a833dChristian Maeder appendDiags ds

13140d161d2d2d11d87283d01d57ee3a738a833dChristian Maeder case mt of

13140d161d2d2d11d87283d01d57ee3a738a833dChristian Maeder Nothing -> mkError "not a formula" term

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder Just f -> return f

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder _ -> return formula -- do not fail even for unresolved cases

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder

0c92a39a4adf3c1cbe173e3b16c65c159a1ce612Christian Maeder-- | test if a term can be uniquely resolved

13140d161d2d2d11d87283d01d57ee3a738a833dChristian MaederoneExpTerm :: (FormExtension f, TermExtension f)

=> Min f e -> Sign f e -> TERM f -> Result (TERM f)

oneExpTerm minF sign term = do

ts <- minExpTerm minF sign term

isUnambiguous "" (globAnnos sign) term ts nullRange

{- ----------------------------------------------------------

- Minimal expansion of an equation formula -

see minExpTermCond

---------------------------------------------------------- -}

minExpFORMULAeq :: (FormExtension f, TermExtension f)

=> Min f e -> Sign f e -> (TERM f -> TERM f -> Range -> FORMULA f)

-> TERM f -> TERM f -> Range -> Result (FORMULA f)

minExpFORMULAeq mef sign eq term1 term2 pos = do

(ps, msg) <- minExpTermCond mef sign ( \ t1 t2 -> eq t1 t2 pos)

term1 term2 pos

isUnambiguous msg (globAnnos sign) (eq term1 term2 pos) ps pos

-- | check if there is at least one solution

hasSolutions :: Pretty f => String -> GlobalAnnos -> f -> [[f]] -> Range

-> Result [[f]]

hasSolutions msg ga topterm ts pos = let terms = filter (not . null) ts in

if null terms then Result

[Diag Error ("no typing for: " ++ showGlobalDoc ga topterm "" ++ msg)

pos] Nothing

else return terms

-- | check if there is a unique equivalence class

isUnambiguous :: Pretty f => String -> GlobalAnnos -> f -> [[f]] -> Range

-> Result f

isUnambiguous msg ga topterm ts pos = do

terms <- hasSolutions msg ga topterm ts pos

case terms of

[ term : _ ] -> return term

_ -> Result [Diag Error ("ambiguous term\n " ++

showSepList (showString "\n ") (showGlobalDoc ga)

(take 5 $ map head terms) "") pos] Nothing

checkIdAndArgs :: Id -> [a] -> Range -> Result Int

checkIdAndArgs ide args poss =

let nargs = length args

pargs = placeCount ide

in if isMixfix ide && pargs /= nargs then

Result [Diag Error

("expected " ++ shows pargs " argument(s) of mixfix identifier '"

++ showDoc ide "' but found " ++ shows nargs " argument(s)")

poss] Nothing

else return nargs

noOpOrPredDiag :: Pretty t => [a] -> DiagKind -> String -> Maybe t -> Id

-> Range -> Int -> [Diagnosis]

noOpOrPredDiag ops k str mty ide pos nargs = case ops of

[] -> let

hd = "no " ++ str ++ " with "

ft = " found for '" ++ showDoc ide "'"

in [Diag k (case mty of

Nothing -> hd ++ shows nargs " argument"

++ (if nargs == 1 then "" else "s") ++ ft

Just ty -> hd ++ "profile '" ++ showDoc ty "'" ++ ft) pos]

_ -> []

noOpOrPred :: Pretty t => [a] -> String -> Maybe t -> Id -> Range -> Int

-> Result ()

noOpOrPred ops str mty ide pos nargs = when (null ops) $ Result

(noOpOrPredDiag ops Error str mty ide pos nargs) Nothing

{- ----------------------------------------------------------

- Minimal expansion of a predication formula -

see minExpTermAppl

---------------------------------------------------------- -}

minExpFORMULApred :: (FormExtension f, TermExtension f)

=> Min f e -> Sign f e -> Id -> Maybe PredType -> [TERM f] -> Range

-> Result (FORMULA f)

minExpFORMULApred mef sign ide mty args pos = do

nargs <- checkIdAndArgs ide args pos

let -- predicates matching that name in the current environment

preds' = Set.filter ((nargs ==) . length . predArgs) $

MapSet.lookup ide $ predMap sign

preds = case mty of

Nothing -> map (pSortBy predArgs sign)

$ Rel.leqClasses (leqP' sign) preds'

Just ty -> [[ty] | Set.member ty preds']

boolAna l cmd = case mty of

Nothing | null l -> do

appendDiags $ noOpOrPredDiag preds Hint

"matching predicate" mty ide pos nargs

minExpFORMULA mef sign $ Mixfix_formula

$ Application (Op_name ide) args pos

_ -> cmd

boolAna preds $ do

noOpOrPred preds "predicate" mty ide pos nargs

tts <- mapM (minExpTerm mef sign) args

let (goodCombs, msg) = getAllCombs sign nargs ide predArgs preds tts

qualForms = qualifyGFs qualifyPred ide pos goodCombs

boolAna qualForms

$ isUnambiguous msg (globAnnos sign)

(Predication (Pred_name ide) args pos) qualForms pos

showSort :: [SORT] -> String

showSort s = case s of

[ft] -> "a term of sort '" ++ shows ft "' was "

_ -> "terms of sorts " ++ showDoc s " were "

missMsg :: Bool -> Int -> Id -> [[SORT]] -> [SORT] -> [SORT] -> String

missMsg singleArg maxArg ide args foundTs expectedTs =

"\nin the "

++ (if singleArg then "" else show (maxArg + 1) ++ ". ")

++ "argument of '" ++ show ide

++ (if singleArg then "'\n" else case args of

[arg] -> " : " ++ showDoc (PredType arg) "'\n"

_ -> "'\n with argument sorts " ++ showDoc (map PredType args) "\n")

++ showSort foundTs ++ "found but\n"

++ showSort expectedTs ++ "expected."

getAllCombs :: TermExtension f => Sign f e -> Int -> Id -> (a -> [SORT])

-> [[a]] -> [[[TERM f]]] -> ([[(a, [TERM f], Maybe Int)]], String)

getAllCombs sign nargs ide getArgs fs expansions =

let formCombs = concatMap (getCombs sign getArgs fs . combine)

$ combine expansions

partCombs = map (partition $ \ (_, _, m) -> isNothing m) formCombs

(goodCombs, badCombs) = unzip partCombs

badCs = concat badCombs

in if null badCs then (goodCombs, "") else let

maxArg = maximum $ map (\ (_, _, Just c) -> c) badCs

badCs2 = filter (\ (_, _, Just c) -> maxArg == c) badCs

args = Set.toList . Set.fromList

$ map (\ (a, _, _) -> getArgs a) badCs2

foundTs = keepMinimals sign id

$ map (\ (_, ts, _) -> sortOfTerm $ ts !! maxArg) badCs2

expectedTs = keepMinimals1 False sign id $ map (!! maxArg) args

in (goodCombs, missMsg (nargs == 1) maxArg ide args foundTs expectedTs)

getCombs :: TermExtension f => Sign f e -> (a -> [SORT]) -> [[a]] -> [[TERM f]]

-> [[(a, [TERM f], Maybe Int)]]

getCombs sign getArgs = flip $ map . \ cs fs ->

[ (f, ts, elemIndex False $ zipWith (leqSort sign) (map sortOfTerm ts)

$ getArgs f) | f <- fs, ts <- cs ]

qualifyGFs :: (Id -> Range -> (a, [TERM f]) -> b) -> Id -> Range

-> [[(a, [TERM f], Maybe Int)]] -> [[b]]

qualifyGFs f ide pos = map $ map (f ide pos . \ (a, b, _) -> (a, b))

-- | qualify a single pred, given by its signature and its arguments

qualifyPred :: Id -> Range -> (PredType, [TERM f]) -> FORMULA f

qualifyPred 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)

. optTermSort))

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, msg) <- minExpTermCond mef sign ( \ t1 t2 -> Conditional t1 f t2 pos)

term1 term2 pos

hasSolutions msg 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)

(goodCombs, msg) = getAllCombs sign nargs ide opArgs ops expansions

qualTerms = qualifyGFs qualifyOp ide pos

$ map (minimizeOp sign) goodCombs

hasSolutions msg (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]], String)

minExpTermCond mef sign f term1 term2 pos = do

pairs <- minExpTermEq mef sign term1 term2

let (lhs, rhs) = unzip $ concat pairs

mins = keepMinimals sign id . map sortOfTerm

ds = "\n" ++ showSort (mins lhs) ++ "on the lhs but\n"

++ showSort (mins rhs) ++ "on the rhs."

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, ds)

{- ----------------------------------------------------------

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], a)] -> [(OpType, [TERM f], a)]

minimizeOp sign = keepMinimals sign (opRes . \ (a, _, _) -> a)

-- | 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