5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster{- |

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterModule : $Header$

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterCopyright : (c) Zicheng Wang, C.Maeder Uni Bremen 2002-2006

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterMaintainer : Christian.Maeder@dfki.de

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterStability : provisional

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterPortability : non-portable (imports Logic.Comorphism)

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterCoding out partiality (SubPCFOL= -> SubCFOL=),

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster-}

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fostermodule Comorphisms.CASL2SubCFOL where

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport Logic.Logic

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport Logic.Comorphism

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster-- CASL

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport CASL.Logic_CASL

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport CASL.AS_Basic_CASL

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport CASL.Sign

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport CASL.Morphism

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport CASL.Sublogic as SL hiding(bottom)

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport CASL.Overload

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport CASL.Fold

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport CASL.Project

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport CASL.Simplify

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport Common.Id

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport qualified Data.Map as Map

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport qualified Data.Set as Set

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterimport qualified Common.Lib.Rel as Rel

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Lunaimport Common.AS_Annotation

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Lunaimport Common.ProofUtils

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Luna

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Lunaimport Data.List (zip)

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Luna

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster-- | The identity of the comorphism

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterdata CASL2SubCFOL = CASL2SubCFOL deriving (Show)

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterinstance Language CASL2SubCFOL -- default definition is okay

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterinstance Comorphism CASL2SubCFOL

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Luna CASL CASL_Sublogics

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster CASLSign

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Luna CASLMor

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Luna Symbol RawSymbol ()

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster CASL CASL_Sublogics

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster CASLSign

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster CASLMor

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster Symbol RawSymbol () where

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster sourceLogic CASL2SubCFOL = CASL

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster sourceSublogic CASL2SubCFOL = SL.top

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster targetLogic CASL2SubCFOL = CASL

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster mapSublogic CASL2SubCFOL sl = Just $ if has_part sl then sl

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster { has_part = False -- partiality is coded out

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster , has_pred = True

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster , which_logic = max Horn $ which_logic sl

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster , has_eq = True} else sl

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster map_theory CASL2SubCFOL (sig, sens) =

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster let bsrts = sortsWithBottom sig $ Set.unions $

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster map (botFormulaSorts . sentence) sens

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster sens1 = generateAxioms bsrts sig

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster sens2 = map (mapNamed (simplifyFormula id . codeFormula bsrts))

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster sens

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster in return (encodeSig bsrts sig, disambiguateSens Set.empty . nameSens

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster $ sens1 ++ sens2)

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster map_morphism CASL2SubCFOL mor@Morphism{msource = src, mtarget = tar} =

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster return

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster mor { msource = encodeSig (sortsWithBottom src Set.empty) src

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster , mtarget = encodeSig (sortsWithBottom tar Set.empty) tar

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster , fun_map = Map.map (\ (i, _) -> (i, Total)) $ fun_map mor }

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster map_sentence CASL2SubCFOL sig sen =

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster return $ simplifyFormula id $ codeFormula

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster (sortsWithBottom sig $ botFormulaSorts sen) sen

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster map_symbol CASL2SubCFOL s =

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster Set.singleton s { symbType = totalizeSymbType $ symbType s }

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster has_model_expansion CASL2SubCFOL = True

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster is_weakly_amalgamable CASL2SubCFOL = True

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FostertotalizeSymbType :: SymbType -> SymbType

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FostertotalizeSymbType t = case t of

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster OpAsItemType ot -> OpAsItemType ot { opKind = Total }

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster _ -> t

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FostersortsWithBottom :: Sign f e -> Set.Set SORT -> Set.Set SORT

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FostersortsWithBottom sign formBotSrts =

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster let ops = Map.elems $ opMap sign

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster -- all supersorts inherit the same bottom element

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster allSortsWithBottom s =

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster Set.unions $ s : map (flip supersortsOf sign) (Set.toList s)

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster resSortsOfPartialFcts =

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster allSortsWithBottom $ Set.unions $ formBotSrts :

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster map (Set.map opRes . Set.filter

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster ( \ t -> opKind t == Partial)) ops

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster collect given =

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster let more = allSortsWithBottom $

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster Set.unions $ map (Set.map opRes .

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster Set.filter ( \ t -> any

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster (flip Set.member given) $ opArgs t)) ops

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster in if Set.isSubsetOf more given then given

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster else collect $ Set.union more given

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster in collect resSortsOfPartialFcts

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterbottom :: Id

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterbottom = mkId[mkSimpleId $ genNamePrefix ++ "bottom"]

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterdefPred :: Id

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterdefPred = mkId[mkSimpleId $ genNamePrefix ++ "defined"]

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterdefined :: Set.Set SORT -> TERM f -> SORT -> Range -> FORMULA f

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Fosterdefined bsorts t s ps =

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster if Set.member s bsorts then Predication

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster (Qual_pred_name defPred (Pred_type [s] nullRange) nullRange) [t] ps

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster else True_atom ps

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterdefVards :: Set.Set SORT -> [VAR_DECL] -> FORMULA f

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterdefVards bs [vs@(Var_decl [_] _ _)] = head $ defVars bs vs

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterdefVards bs vs = Conjunction (concatMap (defVars bs) vs) nullRange

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterdefVars :: Set.Set SORT -> VAR_DECL -> [FORMULA f]

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterdefVars bs (Var_decl vns s _) = map (defVar bs s) vns

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterdefVar :: Set.Set SORT -> SORT -> Token -> FORMULA f

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterdefVar bs s v = defined bs (Qual_var v s nullRange) s nullRange

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Luna

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid LunatotalizeOpSymb :: OP_SYMB -> OP_SYMB

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid LunatotalizeOpSymb o = case o of

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

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Luna Qual_op_name i (Op_type Total args res ps) qs

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Luna _ -> o

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Luna

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid LunaaddBottomAlt :: Constraint -> Constraint

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosteraddBottomAlt c = c

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster { opSymbs = opSymbs c ++

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster [(Qual_op_name bottom

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster (Op_type Total [] (newSort c) nullRange)

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster nullRange, [])] }

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterargSorts :: Constraint -> Set.Set SORT

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterargSorts c = Set.unions $ map (argsOpSymb . fst) $ opSymbs c

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster where argsOpSymb op = case op of

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster Qual_op_name _ ot _ -> Set.fromList $ args_OP_TYPE ot

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster _ -> error "argSorts"

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FostertotalizeConstraint :: Set.Set SORT -> Constraint -> Constraint

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FostertotalizeConstraint bsrts c =

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

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

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster-- | Add projections to the signature

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterencodeSig :: Set.Set SORT -> Sign f e -> Sign f e

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FosterencodeSig bsorts sig = if Set.null bsorts then sig else

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster sig { opMap = projOpMap, predMap = newpredMap } where

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster newTotalMap = Map.map (Set.map $ makeTotal Total) $ opMap sig

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster botType x = OpType {opKind = Total, opArgs=[], opRes=x }

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster botTypes = Set.map botType bsorts

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster botOpMap = Map.insert bottom botTypes newTotalMap

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster defType x = PredType{predArgs=[x]}

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Luna defTypes = Set.map defType bsorts

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster newpredMap = Map.insert defPred defTypes $ predMap sig

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster rel = Rel.irreflex $ sortRel sig

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster total (s, s') = OpType{opKind = Total, opArgs = [s'], opRes = s}

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster setprojOptype = Set.map total $ Rel.toSet rel

c4329510051cce0c6b3efc1fae122ec4c5d61efaDavid Luna projOpMap = Set.fold ( \ t ->

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster Map.insert (uniqueProjName $ toOP_TYPE t)

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster $ Set.singleton t) botOpMap setprojOptype

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FostergenerateAxioms :: Set.Set SORT -> Sign f e -> [Named (FORMULA ())]

5c099afa7c9361afc2f4477fec0e3018588d7840Allan FostergenerateAxioms bsorts sig = filter (not . is_True_atom . sentence) $

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster map (mapNamed $ simplifyFormula id . rmDefs bsorts id) $

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster map (mapNamed $ renameFormula id) (concat

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster [inlineAxioms CASL

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster " sort s < s' \

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster \ op pr : s'->s \

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster \ pred d:s \

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

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster \ %(ga_projection_injectivity)% "

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster ++ inlineAxioms CASL

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster " sort s < s' \

5c099afa7c9361afc2f4477fec0e3018588d7840Allan Foster \ op pr : s'->s \

\ pred d:s \

\ forall x:s . d(x) => pr(x)=x %(ga_projection)% "

| s <- sortList, let y = mkSimpleId "y",

s' <- minSupers s])

++ concat([inlineAxioms CASL

" sort s \

\ pred d:s \

\ . exists x:s.d(x) %(ga_nonEmpty)%" ++

inlineAxioms CASL

" sort s \

\ op bottom:s \

\ pred d:s \

\ . not d(bottom) %(ga_notDefBottom)%"

| s <- sortList ] ++

[inlineAxioms CASL

" sort t \

\ sorts s_i \

\ sorts s_k \

\ op f:s_i->t \

\ var y_k:s_k \

\ forall y_i:s_i . def f(y_i) <=> def y_k /\\ def y_k %(ga_totality)%"

| (f,typ) <- opList, opKind typ == Total,

let s=opArgs typ; t=opRes typ; y= mkVars (length s) ] ++

[inlineAxioms CASL

" sort t \

\ sorts s_i \

\ sorts s_k \

\ op f:s_i->t \

\ var y_k:s_k \

\ forall y_i:s_i . def f(y_i) => def y_k /\\ def y_k %(ga_strictness)%"

| (f,typ) <- opList, opKind typ == Partial,

let s=opArgs typ; t=opRes typ; y= mkVars (length s) ] ++

[inlineAxioms CASL

" sorts s_i \

\ sorts s_k \

\ pred p:s_i \

\ var y_k:s_k \

\ forall y_i:s_i . p(y_i) => def y_k /\\ def y_k \

\ %(ga_predicate_strictness)%"

| (p,typ) <- predList, let s=predArgs typ; y=mkVars (length s) ] )

where

x = mkSimpleId "x"

pr = projName

minSupers so = keepMinimals sig2 id $ Set.toList $ Set.delete so

$ supersortsOf so sig2

sig2 = sig { sortRel = Rel.irreflex $ sortRel sig }

d = defPred

sortList = Set.toList bsorts

opList = [(f,t) | (f,types) <- Map.toList $ opMap sig,

t <- Set.toList types ]

predList = [(p,t) | (p,types) <- Map.toList $ predMap sig,

t <- Set.toList types ]

mkVars n = [mkSimpleId ("x_"++show i) | i<-[1..n]]

codeRecord :: Set.Set SORT -> (f -> f) -> Record f (FORMULA f) (TERM f)

codeRecord 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 = \ _ t ps -> defined bsrts t (term_sort t) ps

, foldExistl_equation = \ _ t1 t2 ps ->

Conjunction[Strong_equation t1 t2 ps,

defined bsrts t1 (term_sort t1) ps] ps

, foldMembership = \ _ t s ps ->

defined bsrts (projectUnique Total ps t s) s ps

, foldSort_gen_ax = \ _ cs b ->

Sort_gen_ax (map (totalizeConstraint bsrts) cs) b

, foldApplication = \ _ o args ps -> Application (totalizeOpSymb o) args ps

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

}

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

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

rmDefsRecord :: Set.Set SORT -> (f -> f) -> Record f (FORMULA f) (TERM f)

rmDefsRecord bsrts mf = (mapRecord mf)

{ foldDefinedness = \ _ t ps -> defined bsrts t (term_sort t) ps }

rmDefs :: Set.Set SORT -> (f -> f) -> FORMULA f -> FORMULA f

rmDefs bsrts = foldFormula . rmDefsRecord bsrts

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