15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari Module : $Header$

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari Copyright : (c) Mingyi Liu and Till Mossakowski and Uni Bremen 2004

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari Maintainer : hets@tzi.de

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari Stability : provisional

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari Portability : portable

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari Check for truth in one-point model

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari with all predicates true, all functions total

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari-}

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari{-

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari todo:

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari-}

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegarimodule CASL.CCC.OnePoint where

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport CASL.Sign -- Sign, OpType

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport CASL.Morphism

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport CASL.AS_Basic_CASL -- FORMULA, OP_{NAME,SYMB}, TERM, SORT, VAR

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport qualified Common.Lib.Map as Map

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegariimport qualified Common.Lib.Set as Set

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegariimport qualified Common.Lib.Rel as Rel

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{-

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederWe use a three valued logic to evaluate a formula in a one-point expansion

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederof an unknown arbitrary model. This means that for new sorts and new predicates,

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederevery equation and predicate application holds, but for the old sorts and

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederpredicates, we do not know anything. The three valued logic is represented

76865b54ad4551e3956595cdbdcba9afe78c26adDaniel Calegariwith Maybe Bool. It has the following meaning:

76865b54ad4551e3956595cdbdcba9afe78c26adDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari Nothing * = unknown

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari Just True True

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Jast False False

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederThe connectives are as follows:

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariand t f *

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedert t f *

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederf f f f

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari* * f *

76865b54ad4551e3956595cdbdcba9afe78c26adDaniel Calegari

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegarior t f *

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegarit t t t

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegarif t f *

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari* t * *

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegariimplies t f *

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegarit t f *

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegarif t t t

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder* t * *

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederequivalent t f *

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedert t f *

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederf f t *

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder* * * *

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedernot t f *

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder f t *

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari(this is just Kleene's strong three-valued logic)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-}

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari

4c12187acb198e833aea3a634c4c259629c71a6dDaniel CalegarievaluateOnePoint :: Morphism f e m -> [FORMULA f] -> Maybe Bool

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePoint m fs =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let p = [evaluateOnePointFORMULA (imageOfMorphism m) f|f<-fs]

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari in if elem (Just False) p then Just False

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else if elem Nothing p then Nothing

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari else Just True

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari{-

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePoint :: Morphism f e m-> [FORMULA f] -> Maybe Bool

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePoint m fs = do

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari p <- mapM (evaluateOnePointFORMULA (imageOfMorphism m)) fs

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari return (all id p)

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari-}

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari

4c12187acb198e833aea3a634c4c259629c71a6dDaniel CalegarievaluateOnePointFORMULA :: Sign f e -> FORMULA f -> Maybe Bool

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePointFORMULA sig (Quantification _ _ f _) =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder evaluateOnePointFORMULA sig f

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePointFORMULA sig (Conjunction fs _)=

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let p=[evaluateOnePointFORMULA sig f|f<-fs]

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if elem (Just False) p then Just False

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari else if elem Nothing p then Nothing

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else Just True

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePointFORMULA sig (Disjunction fs _)=

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let p=[evaluateOnePointFORMULA sig f|f<-fs]

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if elem (Just True) p then Just True

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else if elem Nothing p then Nothing

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari else Just False

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePointFORMULA sig (Implication f1 f2 _ _)=

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let p1=evaluateOnePointFORMULA sig f1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder p2=evaluateOnePointFORMULA sig f2

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari in if p1==(Just False) || p2==(Just True) then Just True

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari else if p1==(Just True) && p2==(Just False) then Just False

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari else Nothing

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePointFORMULA sig (Equivalence f1 f2 _) =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let p1=evaluateOnePointFORMULA sig f1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder p2=evaluateOnePointFORMULA sig f2

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if p1==Nothing || p2==Nothing then Nothing

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else if p1==p2 then Just True

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else Just False

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePointFORMULA sig (Negation f _)=

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari case evaluateOnePointFORMULA sig f of

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari Just True -> Just False

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just False ->Just True

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari _ -> Nothing

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePointFORMULA _ (True_atom _)= Just True

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari

4c12187acb198e833aea3a634c4c259629c71a6dDaniel CalegarievaluateOnePointFORMULA _ (False_atom _)= Just False

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePointFORMULA sig (Predication pred_symb _ _)=

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case pred_symb of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Pred_name _ -> Nothing

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari Qual_pred_name pname ptype _ ->

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari case Map.lookup pname (predMap sig) of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> Just True

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just ptypes ->

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if toPredType ptype `Set.member` ptypes then Nothing

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else Just True

76865b54ad4551e3956595cdbdcba9afe78c26adDaniel Calegari

76865b54ad4551e3956595cdbdcba9afe78c26adDaniel CalegarievaluateOnePointFORMULA sig (Definedness (Sorted_term _ sort _) _)=

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case Set.member sort (sortSet sig) of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder True -> Nothing

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder False -> Just True

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel CalegarievaluateOnePointFORMULA sig (Existl_equation (Sorted_term _ sort1 _) (Sorted_term _ sort2 _) _)=

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari if (Set.member sort1 (sortSet sig)==False)

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari && (Set.member sort2 (sortSet sig)==False) then Just True

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari else Nothing

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePointFORMULA sig (Strong_equation (Sorted_term _ sort1 _) (Sorted_term _ sort2 _) _)=

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if (Set.member sort1 (sortSet sig)==False)

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari && (Set.member sort2 (sortSet sig)==False) then Just True

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else Nothing

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari-- todo: auch pruefen, ob Sorte von t in sortSet sig

4c12187acb198e833aea3a634c4c259629c71a6dDaniel CalegarievaluateOnePointFORMULA sig (Membership (Sorted_term _ sort1 _) sort2 _)=

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari if (Set.member sort1 (sortSet sig)==False)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder && (Set.member sort2 (sortSet sig)==False) then Just True

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else Nothing

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari

4c12187acb198e833aea3a634c4c259629c71a6dDaniel CalegarievaluateOnePointFORMULA _ (Mixfix_formula _)= error "Fehler Mixfix_formula"

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari

4c12187acb198e833aea3a634c4c259629c71a6dDaniel CalegarievaluateOnePointFORMULA _ (Unparsed_formula _ _)= error "Fehler Unparsed_formula"

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari{-

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder compute recover_Sort_gen_ax constr, get (srts,ops,maps)

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari check whether all srts are "new" (not in the image of the morphism)

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari check whether for all s in srts, there is a term,

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder using variables of sorts outside srts

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari using operation symbols from ops

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari Algorithm:

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder construct a list L of "inhabited" sorts

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder initially, the list L is empty

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder iteration step:

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder for each operation symbol in ops, such that

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder all argument sorts (opArgs)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder are either in the list L or are outside srts

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari add the results sort (opRes) to the list L of inhabited sorts

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari start with initial list, and iterate until iteration is stable

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder check whether srts is a sublist of the list resulting from the iteration

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari-}

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePointFORMULA sig (Sort_gen_ax constrs _)=

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let (srts,ops,_)=recover_Sort_gen_ax constrs

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sorts = sortSet sig

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder argsAndres=concat $ map (\os-> case os of

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari Op_name _->[]

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari Qual_op_name _ ot _->

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case ot of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Op_type _ args res _->[(args,res)]

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari ) ops

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari iterateInhabited l =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if l==newL then newL else iterateInhabited newL

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder where newL =foldr (\ (as,rs) l'->

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if (all (\s->elem s l') as)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder && (not (elem rs l'))

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then rs:l'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else l') l argsAndres

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- inhabited = iterateInhabited []

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder inhabited = iterateInhabited $ Set.toList sorts

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if any (\s->Set.member s sorts) srts then Nothing

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari else if all (\s->elem s inhabited) srts then Just True

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else Nothing

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel CalegarievaluateOnePointFORMULA _ (ExtFORMULA _)=error "Fehler ExtFORMULA"

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederevaluateOnePointFORMULA _ _=error "Fehler" -- or Just False

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | Compute the image of a signature morphism

4c12187acb198e833aea3a634c4c259629c71a6dDaniel CalegariimageOfMorphism :: Morphism f e m -> Sign f e

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederimageOfMorphism m =

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari sig {sortSet = Set.map (mapSort sortMap) (sortSet src),

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari sortRel = Rel.map (mapSort sortMap) (sortRel src),

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder opMap = Map.foldWithKey

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (\ident ots l ->

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari Set.fold (\ot l' -> insertOp

76865b54ad4551e3956595cdbdcba9afe78c26adDaniel Calegari (mapOpSym sortMap funMap (ident,ot)) l') l ots)

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari Map.empty (opMap src),

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari predMap = Map.foldWithKey

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (\ident pts l ->

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Set.fold (\pt l' -> insertPred

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (mapPredSym sortMap pMap (ident,pt)) l') l pts)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Map.empty (predMap src)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder where sig = mtarget m

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder src = msource m

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari sortMap = sort_map m

76865b54ad4551e3956595cdbdcba9afe78c26adDaniel Calegari funMap = fun_map m

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder insertOp (ident,ot) opM =

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari case Map.lookup ident opM of

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari Nothing -> Map.insert ident (Set.singleton ot) opM

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just ots -> Map.insert ident (Set.insert ot ots) opM

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pMap = pred_map m

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder insertPred (ident,pt) predM =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case Map.lookup ident predM of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> Map.insert ident (Set.singleton pt) predM

76865b54ad4551e3956595cdbdcba9afe78c26adDaniel Calegari Just pts -> Map.insert ident (Set.insert pt pts) predM

76865b54ad4551e3956595cdbdcba9afe78c26adDaniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | Test whether a signature morphism adds new supersorts

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaddsNewSupersorts :: Morphism f e m -> Bool

76865b54ad4551e3956595cdbdcba9afe78c26adDaniel CalegariaddsNewSupersorts m =

76865b54ad4551e3956595cdbdcba9afe78c26adDaniel Calegari any (\s->not $ Set.isSubsetOf (Set.insert s $ supersortsOf s sig) sorts)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder $ Set.toList sorts

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder where sig=imageOfMorphism m

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sorts=sortSet sig

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{-

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedercheck: is there a sort not in the image of the morphism, that is

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedersimultaneously s supersort of a sort that is in the image.

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedergo through all sorts in the image

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederfor each such sort s, comupte supersortsOf s

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertest whether a supersort is not in the image

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederif there is such a sort (i.e. supersort not in the image), then return True

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegariotherwise, return False

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari-}

4c12187acb198e833aea3a634c4c259629c71a6dDaniel Calegari