4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk{- |

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkModule : $Header$

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkDescription : coding out partiality

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkCopyright : (c) Zicheng Wang, C.Maeder Uni Bremen 2002-2009

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkLicense : GPLv2 or higher, see LICENSE.txt

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkMaintainer : Christian.Maeder@dfki.de

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkStability : provisional

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkPortability : non-portable (imports Logic.Comorphism)

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkCoding out partiality (SubPCFOL= -> SubCFOL=) while keeping subsorting.

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkWithout unique bottoms sort generation axioms are not allowed.

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkThen we have (SubPFOL= -> SubFOL=).

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk-}

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkmodule Comorphisms.CASL2SubCFOL where

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport Logic.Logic

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport Logic.Comorphism

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport CASL.Logic_CASL

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport CASL.AS_Basic_CASL

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport CASL.Sign

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport CASL.Morphism

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport CASL.Sublogic as SL hiding (bottom)

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport CASL.Fold

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport CASL.Project

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport CASL.Simplify

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport Common.Id

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport Common.DocUtils

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport qualified Data.Map as Map

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport qualified Data.Set as Set

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport qualified Common.Lib.Rel as Rel

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport qualified Common.Lib.MapSet as MapSet

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport Common.AS_Annotation

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport Common.ProofUtils

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport Common.ProofTree

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkimport Common.Utils

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk-- | determine the need for bottom constants

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenkdata FormulaTreatment =

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk NoMembershipOrCast

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk | FormulaDependent

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk | SubsortBottoms

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk | AllSortBottoms

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk deriving Show

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk-- | a case selector for formula treatment

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenktreatFormula :: FormulaTreatment -> a -> a -> a -> a -> a

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenktreatFormula g a b c d = case g of

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk NoMembershipOrCast -> a

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk FormulaDependent -> b

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk SubsortBottoms -> c

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk AllSortBottoms -> d

4b8d88eb610aa1e0bb6ec632f792744b3d6b5f22jeff.schenk

{- | The identity of the comorphism depending on parameters.

'NoMembershipOrCast' reject membership test or cast to non-bottom sorts.

. 'FormulaDependent' creates a formula dependent signature translation.

'SubsortBottoms' creates bottoms for all proper subsorts. -}

data CASL2SubCFOL = CASL2SubCFOL

{ uniqueBottom :: Bool -- ^ removes free types

, formulaTreatment :: FormulaTreatment

-- ^ deal with membership tests and casts

} deriving Show

{- | create unique bottoms, sorts with bottom depend on membership

and casts in theory sentences. -}

defaultCASL2SubCFOL :: CASL2SubCFOL

defaultCASL2SubCFOL = CASL2SubCFOL True FormulaDependent

instance Language CASL2SubCFOL where

language_name (CASL2SubCFOL _ m) = "CASL2SubCFOL"

++ treatFormula m (show m) "" (show m) (show m)

instance Comorphism CASL2SubCFOL

CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree

CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree where

sourceLogic (CASL2SubCFOL _ _) = CASL

sourceSublogic (CASL2SubCFOL b _) =

if b then SL.caslTop else SL.caslTop { cons_features = NoSortGen }

targetLogic (CASL2SubCFOL _ _) = CASL

mapSublogic (CASL2SubCFOL _ _) sl = Just $ if has_part sl then sl

{ has_part = False -- partiality is coded out

, has_pred = True

, which_logic = max Horn $ which_logic sl

, has_eq = True} else sl

map_theory (CASL2SubCFOL b m) (sig, sens) =

let fbsrts = Set.unions $ map (botFormulaSorts . sentence) sens

bsrts = sortsWithBottom m sig fbsrts

sens1 = generateAxioms b bsrts sig

sens2 =

map (mapNamed (simplifyFormula id . codeFormula b bsrts)) sens

in case m of

NoMembershipOrCast

| not $ Set.null $ Set.difference fbsrts bsrts ->

fail "CASL2SubCFOL: unexpected membership test or cast"

_ -> return

( encodeSig bsrts sig

, nameAndDisambiguate $ sens1 ++ sens2)

map_morphism (CASL2SubCFOL _ m) mor@Morphism {msource = src, mtarget = tar}

= return

mor { msource = encodeSig (sortsWithBottom m src Set.empty) src

, mtarget = encodeSig (sortsWithBottom m tar Set.empty) tar

, op_map = Map.map (\ (i, _) -> (i, Total)) $ op_map mor }

map_sentence (CASL2SubCFOL b m) sig sen = let

fbsrts = botFormulaSorts sen

bsrts = sortsWithBottom m sig fbsrts

in case m of

NoMembershipOrCast

| not $ Set.null $ Set.difference fbsrts bsrts ->

fail $ "CASL2SubCFOL: unexpected membership test or cast:\n"

++ showDoc sen ""

_ -> return $ simplifyFormula id $ codeFormula b bsrts sen

map_symbol (CASL2SubCFOL _ _) _ s =

Set.singleton s { symbType = totalizeSymbType $ symbType s }

has_model_expansion (CASL2SubCFOL _ _) = True

is_weakly_amalgamable (CASL2SubCFOL _ _) = True

totalizeSymbType :: SymbType -> SymbType

totalizeSymbType t = case t of

OpAsItemType ot -> OpAsItemType $ mkTotal ot

_ -> t

sortsWithBottom :: FormulaTreatment -> Sign f e -> Set.Set SORT -> Set.Set SORT

sortsWithBottom m sig formBotSrts =

let bsrts = treatFormula m Set.empty formBotSrts

(Rel.keysSet $ sortRel sig) (sortSet sig)

ops = MapSet.elems $ opMap sig

-- all supersorts inherit the same bottom element

allSortsWithBottom s =

Set.unions $ s : map (`supersortsOf` sig) (Set.toList s)

resSortsOfPartialFcts =

allSortsWithBottom . Set.union bsrts

. Set.map opRes $ Set.filter isPartial ops

collect given =

let more = allSortsWithBottom . Set.map opRes $ Set.filter

(any (`Set.member` given) . opArgs) ops

in if Set.isSubsetOf more given then given

else collect $ Set.union more given

in collect resSortsOfPartialFcts

defPred :: Id

defPred = genName "defined"

defined :: TermExtension f => Set.Set SORT -> TERM f -> Range -> FORMULA f

defined bsorts t ps = let s = sortOfTerm t in

if Set.member s bsorts then Predication

(Qual_pred_name defPred (Pred_type [s] nullRange) nullRange) [t] ps

else True_atom ps

defVards :: TermExtension f => Set.Set SORT -> [VAR_DECL] -> FORMULA f

defVards bs = conjunct . concatMap (defVars bs)

defVars :: TermExtension f => Set.Set SORT -> VAR_DECL -> [FORMULA f]

defVars bs (Var_decl vns s _) = map (defVar bs s) vns

defVar :: TermExtension f => Set.Set SORT -> SORT -> Token -> FORMULA f

defVar bs s v = defined bs (Qual_var v s nullRange) nullRange

totalizeOpSymb :: OP_SYMB -> OP_SYMB

totalizeOpSymb o = case o of

Qual_op_name i (Op_type _ args res ps) qs ->

Qual_op_name i (Op_type Total args res ps) qs

_ -> o

addBottomAlt :: Constraint -> Constraint

addBottomAlt c = let t = Op_type Total [] (newSort c) nullRange in c

{opSymbs = opSymbs c ++ [(Qual_op_name (uniqueBotName t) t nullRange, [])]}

argSorts :: Constraint -> Set.Set SORT

argSorts c = Set.unions $ map (argsOpSymb . fst) $ opSymbs c

where argsOpSymb op = case op of

Qual_op_name _ ot _ -> Set.fromList $ args_OP_TYPE ot

_ -> error "argSorts"

totalizeConstraint :: Set.Set SORT -> Constraint -> Constraint

totalizeConstraint bsrts c =

(if Set.member (newSort c) bsrts then addBottomAlt else id)

c { opSymbs = map ( \ (o, is) -> (totalizeOpSymb o, is)) $ opSymbs c }

botType :: SORT -> OpType

botType = sortToOpType

-- | Add projections to the signature

encodeSig :: Set.Set SORT -> Sign f e -> Sign f e

encodeSig bsorts sig = if Set.null bsorts then sig else

sig { opMap = projOpMap, predMap = newpredMap } where

newTotalMap = MapSet.map mkTotal $ opMap sig

botOpMap = Set.fold (\ bt -> addOpTo (uniqueBotName $ toOP_TYPE bt) bt)

newTotalMap $ Set.map botType bsorts

defType x = PredType {predArgs = [x]}

defTypes = Set.map defType bsorts

newpredMap = MapSet.update (const defTypes) defPred $ predMap sig

rel = sortRel sig

total (s, s') = mkTotOpType [s'] s

setprojOptype = Set.map total $ Set.filter ( \ (s, _) ->

Set.member s bsorts) $ Rel.toSet rel

projOpMap = Set.fold (\ t -> addOpTo (uniqueProjName $ toOP_TYPE t) t)

botOpMap setprojOptype

-- | Make the name for the non empty axiom from s to s' to s''

mkNonEmptyAxiomName :: SORT -> String

mkNonEmptyAxiomName = mkAxNameSingle "nonEmpty"

-- | Make the name for the not defined bottom axiom

mkNotDefBotAxiomName :: SORT -> String

mkNotDefBotAxiomName = mkAxNameSingle "notDefBottom"

-- | Make the name for the totality axiom

mkTotalityAxiomName :: OP_NAME -> String

mkTotalityAxiomName f = "ga_strictness_" ++ show f

generateAxioms :: Bool -> Set.Set SORT -> Sign f e -> [Named (FORMULA ())]

generateAxioms uniqBot bsorts sig = concatMap (\ s -> let

vx = mkVarDeclStr "x" s

xt = toQualVar vx

hasBot = Set.member s bsorts

prj z = projectUnique Total nullRange z s

df z = defined bsorts z nullRange

in concatMap (\ s' ->

[makeNamed (mkAxName "total_projection_injectivity" s' s)

$ let xv = mkVarDeclStr "x" s'

yv = mkVarDeclStr "y" s'

tx = toQualVar xv

ty = toQualVar yv

px = prj tx

py = prj ty

epxy = mkStEq px py

-- forall x,y:s' . d(pr(x)) /\\ d(pr(y)) /\\ pr(x)=pr(y) => x=y

in mkForall [xv, yv]

$ mkImpl (if hasBot then conjunct [df px, df py, epxy]

else epxy) $ mkStEq tx ty

-- forall x:s . d(x) => pr(x)=x

, makeNamed (mkAxName "total_projection" s' s)

$ let eq = mkStEq (prj $ Sorted_term xt s' nullRange) xt

in mkForall [vx]

$ if hasBot then mkImpl (df xt) eq else eq]) (minSupers s)

-- exists x:s . d(x)

++ [makeNamed (mkNonEmptyAxiomName s)

$ Quantification Existential [vx] (df xt) nullRange

| hasBot]

++ [makeNamed (mkNotDefBotAxiomName s)

$ let bty = toOP_TYPE $ botType s

bt = mkAppl (mkQualOp (uniqueBotName bty) bty) []

in if uniqBot then

-- forall x:s . not d(x) <=> x=bottom

mkForall [vx]

$ mkEqv (mkNeg $ df xt) $ mkStEq xt bt

else mkNeg $ df bt -- not d(bottom)

| hasBot]) sortList

++ filter (not . is_True_atom . sentence)

(map (mapNamed $ simplifyFormula id)

$ map (\ (f, typ) ->

let vs = map (\ (s, i) -> mkVarDeclStr ("x_" ++ show i) s)

$ number $ opArgs typ

in makeNamed (mkTotalityAxiomName f)

-- forall x_i:s_i . d f(x_1, ..., x_n) {<}=> d x_1 /\\ ... /\\ d x_n

$ mkForall vs

$ (if isTotal typ then mkEqv else mkImpl)

(defined bsorts

(mkAppl (mkQualOp f $ toOP_TYPE $ mkTotal typ)

$ map toQualVar vs) nullRange)

$ defVards bsorts vs) opList

++ map (\ (p, typ) ->

let vs = map (\ (s, i) -> mkVarDeclStr ("x_" ++ show i) s)

$ number $ predArgs typ

in makeNamed ("ga_predicate_strictness_" ++ show p)

-- forall x_i:s_i . p(x_1, ..., x_n) => d x_1 /\\ ... /\\ d x_n

$ mkForall vs

$ mkImpl

(Predication (Qual_pred_name p (toPRED_TYPE typ) nullRange)

(map toQualVar vs) nullRange)

$ defVards bsorts vs) predList)

where

rel1 = Rel.transClosure $ sortRel sig

sccs = Rel.sccOfClosure rel1

rel2 = Rel.transReduce $ Rel.collaps sccs rel1

isos so = Set.insert so $ Set.unions $ filter (Set.member so) sccs

minSupers so = Set.toList $ Set.delete so $ Set.union (isos so)

$ Set.unions $ map isos $ Set.toList $ Rel.succs rel2 so

sortList = Set.toList bsorts

opList = mapSetToList $ opMap sig

predList = mapSetToList $ predMap sig

codeRecord :: TermExtension f => Bool -> Set.Set SORT -> (f -> f)

-> Record f (FORMULA f) (TERM f)

codeRecord uniBot bsrts mf = (mapRecord mf)

{ foldQuantification = \ _ q vs qf ps ->

case q of

Universal ->

Quantification q vs (Implication (defVards bsrts vs) qf True ps) ps

_ -> Quantification q vs (Conjunction [defVards bsrts vs, qf] ps) ps

, foldDefinedness = const $ defined bsrts

, foldExistl_equation = \ _ t1 t2 ps ->

Conjunction [Strong_equation t1 t2 ps,

defined bsrts t1 ps] ps

, foldMembership = \ _ t s ps ->

defined bsrts (projectUnique Total ps t s) ps

, foldSort_gen_ax = \ _ cs b -> if uniBot then

Sort_gen_ax (map (totalizeConstraint bsrts) cs)

$ Set.null (Set.intersection bsrts

$ Set.fromList $ map newSort cs) && b

else error "SubPFOL2SubFOL: unexpected Sort_gen_ax"

, foldApplication = const $ Application . totalizeOpSymb

, foldCast = \ _ t s ps -> projectUnique Total ps t s }

codeFormula :: Bool -> Set.Set SORT -> FORMULA () -> FORMULA ()

codeFormula b bsorts = foldFormula (codeRecord b bsorts $ error "CASL2SubCFol")

codeTerm :: Bool -> Set.Set SORT -> TERM () -> TERM ()

codeTerm b bsorts = foldTerm (codeRecord b bsorts $ error "CASL2SubCFol")

-- | find sorts that need a bottom in membership formulas and casts

botSorts :: (f -> Set.Set SORT) -> Record f (Set.Set SORT) (Set.Set SORT)

botSorts mf = (constRecord mf Set.unions Set.empty)

{ foldMembership = \ _ _ s _ -> Set.singleton s

, foldCast = \ _ _ s _ -> Set.singleton s }

botFormulaSorts :: FORMULA f -> Set.Set SORT

botFormulaSorts = foldFormula (botSorts $ const Set.empty)

botTermSorts :: TERM f -> Set.Set SORT

botTermSorts = foldTerm (botSorts $ const Set.empty)