| Copyright | (c) Martin Kuehl T. Mossakowski C. Maeder 2004-2007 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
CASL.Overload
Description
Overload resolution (injections are inserted separately) Follows Sect. III:3.3 of the CASL Reference Manual. The algorthim is from: Till Mossakowski, Kolyang, Bernd Krieg-Brueckner: Static semantic analysis and theorem proving for CASL. 12th Workshop on Algebraic Development Techniques, Tarquinia 1997, LNCS 1376, p. 333-348
Synopsis
- minExpFORMULA :: (FormExtension f, TermExtension f) => Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
- 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)
- minExpTerm :: (FormExtension f, TermExtension f) => Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
- isUnambiguous :: Pretty f => String -> GlobalAnnos -> f -> [[f]] -> Range -> Result f
- oneExpTerm :: (FormExtension f, TermExtension f) => Min f e -> Sign f e -> TERM f -> Result (TERM f)
- mkSorted :: TermExtension f => Sign f e -> TERM f -> SORT -> Range -> TERM f
- type Min f e = Sign f e -> f -> Result f
- leqF :: Sign f e -> OpType -> OpType -> Bool
- leqP :: Sign f e -> PredType -> PredType -> Bool
- leqSort :: Sign f e -> SORT -> SORT -> Bool
- minimalSupers :: Sign f e -> SORT -> SORT -> [SORT]
- maximalSubs :: Sign f e -> SORT -> SORT -> [SORT]
- haveCommonSupersorts :: Bool -> Sign f e -> SORT -> SORT -> Bool
- haveCommonSubsorts :: Sign f e -> SORT -> SORT -> Bool
- keepMinimals1 :: Bool -> Sign f e -> (a -> SORT) -> [a] -> [a]
- keepMinimals :: Sign f e -> (a -> SORT) -> [a] -> [a]
Documentation
minExpFORMULA :: (FormExtension f, TermExtension f) => Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f) Source #
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) Source #
minExpTerm :: (FormExtension f, TermExtension f) => Min f e -> Sign f e -> TERM f -> Result [[TERM f]] Source #
isUnambiguous :: Pretty f => String -> GlobalAnnos -> f -> [[f]] -> Range -> Result f Source #
check if there is a unique equivalence class
oneExpTerm :: (FormExtension f, TermExtension f) => Min f e -> Sign f e -> TERM f -> Result (TERM f) Source #
test if a term can be uniquely resolved
type Min f e = Sign f e -> f -> Result f Source #
the type of the type checking function of extensions
leqF :: Sign f e -> OpType -> OpType -> Bool Source #
True if both ops are in the overloading relation
leqP :: Sign f e -> PredType -> PredType -> Bool Source #
True if both preds are in the overloading relation
minimalSupers :: Sign f e -> SORT -> SORT -> [SORT] Source #
minimal common supersorts of the two input sorts
maximalSubs :: Sign f e -> SORT -> SORT -> [SORT] Source #
maximal common subsorts of the two input sorts
haveCommonSupersorts :: Bool -> Sign f e -> SORT -> SORT -> Bool Source #
True if both sorts have a common supersort
keepMinimals1 :: Bool -> Sign f e -> (a -> SORT) -> [a] -> [a] Source #
keepMinimals :: Sign f e -> (a -> SORT) -> [a] -> [a] Source #
only keep elements with minimal (and different) sorts