Hets - the Heterogeneous Tool Set

Copyright(c) Martin Kuehl T. Mossakowski C. Maeder 2004-2007
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

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

Documentation

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

mkSorted :: TermExtension f => Sign f e -> TERM f -> SORT -> Range -> TERM f Source #

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

leqSort :: Sign f e -> SORT -> SORT -> Bool Source #

test if s1 < s2

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

haveCommonSubsorts :: Sign f e -> SORT -> SORT -> Bool Source #

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