The translating comorphism from CASL to SoftFOL.
(SuleCFOL2SoftFOL(..), SuleCFOL2SoftFOLInduction(..))
-- | The identity of the comorphisms
data SuleCFOL2SoftFOL = SuleCFOL2SoftFOL deriving (Show)
data SuleCFOL2SoftFOLInduction = SuleCFOL2SoftFOLInduction deriving (Show)
-- | CASL Ids with Types mapped to SPIdentifier
-- | specialized lookup for IdType_SPId_Map
lookupSPId :: Id -> CType -> IdType_SPId_Map ->
-- | specialized insert (with error) for IdType_SPId_Map
insertSPId :: Id -> CType ->
assert (checkIdentifier t spid) $
where err = error ("SuleCFOL2SoftFOL: for Id \""++show i ++
"\" the type \""++ show t ++
"\" can't be mapped to different SoftFOL identifiers")
deleteSPId :: Id -> CType ->
-- | specialized elems into a set for IdType_SPId_Map
elemsSPId_Set :: IdType_SPId_Map ->
Set.Set SPIdentifier
-- extended signature translation
type SignTranslator f e =
CSign.Sign f e -> e -> SoftFOLTheory -> SoftFOLTheory
-- extended signature translation for CASL
sigTrCASL :: SignTranslator () ()
-- extended formula translation
type FormulaTranslator f e =
-- extended formula translation for CASL
formTrCASL :: FormulaTranslator () ()
formTrCASL _ _ = error "SuleCFOL2SoftFOL: No extended formulas allowed in CASL"
instance Language SuleCFOL2SoftFOL -- default definition is okay
instance Language SuleCFOL2SoftFOLInduction -- default definition is okay
instance Comorphism SuleCFOL2SoftFOL
CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
SoftFOL () () SPTerm () ()
{ sub_features = LocFilSub,
cons_features = SortGen { emptyMapping = True,
map_theory _ = transTheory sigTrCASL formTrCASL
map_morphism = mapDefaultMorphism
return . mapSen (isSingleSorted sign) formTrCASL sign
map_symbol = errMapSymbol
instance Comorphism SuleCFOL2SoftFOLInduction
CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
SoftFOL () () SPTerm () ()
{ sub_features = LocFilSub,
cons_features = SortGen { emptyMapping = True,
map_theory _ = transTheory sigTrCASL formTrCASL . generateInductionLemmas
map_morphism = mapDefaultMorphism
return . mapSen (isSingleSorted sign) formTrCASL sign
map_symbol = errMapSymbol
---------------------------- Signature -----------------------------
transFuncMap :: IdType_SPId_Map ->
(FuncMap, IdType_SPId_Map)
transFuncMap idMap sign =
where toSPOpType iden typeSet (fm,im) =
error ("SuleCFOL2SoftFOL: empty sets are not "++
"allowed in OpMaps: " ++ show iden)
insertSPId iden (COp oType) sid' im)
where insOIdSet tset (fm',im') =
insertSPId iden (COp x) sid' y)
sid fma t = disSPOId (COp t) (transId (COp t) iden)
uType t = fst t ++ [snd t]
-- 1. devide into sets with different arities
partOverload :: (Show a,Ord a) => (a -> a -> Bool)
transPredMap :: IdType_SPId_Map ->
(PredMap, IdType_SPId_Map)
transPredMap idMap sign =
where toSPPredType iden typeSet (fm,im) =
error ("SuleCFOL2SoftFOL: empty sets are not "++
"allowed in PredMaps: " ++ show iden)
insertSPId iden (CPred pType) sid' im)
where insOIdSet tset (fm',im') =
insertSPId iden (CPred x) sid' y)
sid fma t = disSPOId (CPred t) (transId (CPred t) iden)
-- | disambiguation of SPASS Identifiers
disSPOId :: CType -- ^ Type of CASl identifier
-> SPIdentifier -- ^ translated CASL Identifier
-> [SPIdentifier] -- ^ translated Sort Symbols of the profile
->
Set.Set SPIdentifier -- ^ SPASS Identifiers already in use
-> SPIdentifier -- ^ fresh Identifier generated from second argument;
-- if the identifier was not in the set this is just the second argument
disSPOId cType sid ty idSet
| checkIdentifier cType sid && not (lkup sid) = sid
| otherwise = let nSid = disSPOId' sid
in assert (checkIdentifier cType nSid) nSid
| otherwise = addType asid 1
where asid = sid' ++ case cType of
x -> '_':show (length ty - (case x of
let nres = asid ++ '_':fc n
nres' = nres ++ '_':show n
then error ("SuleCFOL2SoftFOL: cannot calculate"
++ sid ++ " with type " ++ show ty
-- tr x = trace ("disSPOId: Input: "++show cType ++ ' ':show sid
-- ++ ' ':show ty ++ "\n Output: "++ show x) x
fc n = concatMap (take n) ty
transOpType ::
CSign.OpType -> ([SPIdentifier],SPIdentifier)
-- | translate every Id as Sort
transIdSort :: Id -> String
transIdSort = transId CSort
integrateGenerated :: (Pretty f, PosItem f) =>
IdType_SPId_Map -> [Named (FORMULA f)] ->
integrateGenerated idMap genSens sign
| null genSens = return (idMap,sign,[])
case partition isAxiom genSens of
case makeGenGoals idMap genGoals of
(newPredsMap,idMap',goalsAndSentences) ->
-- makeGens must not invent new sorts
case makeGens idMap' genAxs of
maybe (Result dias Nothing)
(\ (spSortMap_makeGens,newOpsMap,idMap'',exhaustSens) ->
sign { sortMap = spSortMap'
mkInjSentences idMap' newOpsMap++
makeGenGoals :: IdType_SPId_Map -> [Named (FORMULA f)]
-> (PredMap, IdType_SPId_Map, [Named SPTerm])
trace "SuleCFOL2SoftFOL: Warning: Sort_gen_ax as goals not implemented, yet."
{- implementation sketch:
- invent new predicate P that is supposed to hold on
every x in the (freely) generated sort.
- generate formulas with this predicate for each constructor.
- recursive constructors hold if the predicate holds on the variables
implementation is postponed as this translation does not produce
only one goal, but additional symbols, axioms and a goal
makeGens :: (Pretty f, PosItem f) =>
IdType_SPId_Map -> [Named (FORMULA f)]
-> Result (SortMap, FuncMap, IdType_SPId_Map,[Named SPTerm])
-- ^ The list of SoftFOL sentences gives exhaustiveness for
-- generated sorts with only constant constructors
case foldl makeGen (return (
Map.empty,idMap,[],[])) fs of
maybe (Result ds Nothing)
(\ (opMap,idMap',pairs,exhaustSens) ->
opMap,idMap',exhaustSens)))
makeGen :: (Pretty f, PosItem f) =>
Result (FuncMap, IdType_SPId_Map,
[(SPIdentifier,Maybe Generated)],[Named SPTerm])
-> Result (FuncMap, IdType_SPId_Map,
[(SPIdentifier,Maybe Generated)],[Named SPTerm])
makeGen r@(Result ods omv) nf =
maybe (Result ods Nothing) process omv where
process (oMap,iMap,rList,eSens) = case sentence nf of
Sort_gen_ax constrs free ->
if null mp then (case mapAccumL makeGenP (oMap,iMap,[]) srts of
((oMap',iMap',eSens'),genPairs) ->
Result ods (Just (oMap',iMap',
else mkError "Non injective sort mappings cannot \
\be translated to SoftFOL" (sentence nf)
where (srts,ops,mp) = recover_Sort_gen_ax constrs
hasTheSort s (Qual_op_name _ ot _) = s == res_OP_TYPE ot
mkGen = Just . Generated free . map fst
makeGenP (opMap,idMap,exSens) s = ((newOpMap, newIdMap,
exSens++eSen ops_of_s s),
where ((newOpMap,newIdMap),cons) =
mapAccumL mkInjOp (opMap,idMap) ops_of_s
\found for '"++show s++"'") id
(lookupSPId s CSort idMap)
eSen os s = if all nullArgs os
then [emptyName (newName s) (SPQuantTerm SPForall
maybe (error "lookup failed")
(lookupSPId s (CSort) iMap)]
disj v os = case map (\x -> mkEq (varTerm v)
(varTerm $ transOP_SYMB iMap x) ) os of
[] -> error "CASL2SPASS: no constructors found"
var = fromJust (find (\ x -> not (
Set.member x usedIds))
("X":["X"++show i | i <- [(1::Int)..]]))
varTerm v = simpTerm (spSym v)
newName s = "ga_exhaustive_generated_sort_"++(show $ pretty s)
usedIds = elemsSPId_Set iMap
Qual_op_name _ (Op_type _ args _ _) _ -> null args
_ -> error "CASL2SPASS: wrong constructor"
mkInjOp :: (FuncMap, IdType_SPId_Map)
-> ((FuncMap,IdType_SPId_Map),
(SPIdentifier,([SPIdentifier],SPIdentifier)))
mkInjOp (opMap,idMap) qo@(Qual_op_name i ot _) =
if i == injName && isNothing lsid
insertSPId i (COp ot') i' idMap),
where i' = disSPOId (COp ot') (transId (COp ot') i)
(utype (transOpType ot')) usedNames
lsid = lookupSPId i (COp ot') idMap
utype t = fst t ++ [snd t]
mkInjSentences :: IdType_SPId_Map
where genInjs k tset fs =
Set.fold (genInj k) fs tset
assert (length args == 1)
$ emptyName (newName k (head args) res)
(SPQuantTerm SPForall [typedVarTerm var (head args)]
simpTerm (spSym var)])) : fs
var = fromJust (find (\ x -> not (
Set.member x usedIds))
("x":["x"++show i | i <- [(1::Int)..]]))
newName o a r = "ga_"++o++'_':a++'_':r++"_id"
usedIds = elemsSPId_Set idMap
Before translating, eqPredicate symbols where removed from signature.
, singleSorted = isSingleSorted sign
where (spSortMap,idMap) =
let sid = disSPOId CSort (transIdSort i)
insertSPId i CSort sid im))
(fMap,idMap') = transFuncMap idMap sign
(pMap,idMap'') = transPredMap idMap' sign
nonEmptySortSens :: SortMap -> [Named SPTerm]
where extSen s = emptyName ("ga_non_empty_sort_" ++ s) $ SPQuantTerm
SPExists [varTerm] $ compTerm (spSym s) [varTerm]
where varTerm = simpTerm $ spSym $ newVar s
newVar s = fromJust $ find (\ x -> x /= s)
$ "X" : ["X"++show i | i <- [(1::Int)..]]
transTheory :: (Pretty f, PosItem f, Eq f) =>
transTheory trSig trForm (sign,sens) =
(case transSign (filterPreds $ foldl insInjOps sign genAxs) of
do (idMap',tSign',sentencesAndGoals) <-
integrateGenerated idMap genSens tSign
then tSign' {sortMap =
Map.empty} else tSign'
nonEmptySortSens (sortMap tSignElim) ++
map (mapNamed (transFORM (singleSortNotGen tSign') eqPreds
where (genSens,realSens) =
partition (\ s -> case sentence s of
(eqPreds, realSens') = foldl findEqPredicates (
Set.empty, []) realSens
(genAxs,_) = partition isAxiom genSens
(Sort_gen_ax constrs _) ->
case recover_Sort_gen_ax constrs of
(_,ops,mp) -> assert (null mp) (insertInjOps sig ops)
++showDoc f "\" slipped through filter.")
Pred_name pn -> insertPredToSet pn
(Pred_type [] nullRange) newMap
Qual_pred_name pn pt _ -> insertPredToSet pn pt newMap)
insertPredToSet pId pType pMap =
Finds definitions (Equivalences) where one side is a binary predicate
and the other side is a built-in equality application (Strong_equation).
The given Named (FORMULA f) is checked for this and if so, will be put
into the set of such predicates.
findEqPredicates :: (Show f, Eq f) => (
Set.Set PRED_SYMB, [Named (FORMULA f)])
-- ^ previous list of found predicates and valid sentences
-> (
Set.Set PRED_SYMB, [Named (FORMULA f)])
findEqPredicates (eqPreds, sens) sen =
Quantification Universal var_decl quantFormula _ ->
isEquiv (foldl (\ vList (Var_decl v s _) ->
vList ++ map (\vl -> (vl, s)) v)
validSens = (eqPreds, sens ++ [sen])
-- Exact two variables are checked if they have the same Sort.
-- If more than two variables should be compared, use foldl.
if (length vars == 2) && (snd (head vars) == snd (vars !! 1))
Equivalence f1 f2 _-> isStrong_eq vars f1 f2
Strong_equation _ _ _ -> f1
Strong_equation _ _ _ -> f2
Strong_equation eq_t1 eq_t2 _ -> case f2n of
Predication eq_pred_symb pterms _ ->
Creates a list of (VAR, SORT) out of a list of TERMs. Only Qual_var TERMs
are inserted which will be checked using
sortedVarTermList :: [TERM f]
sortedVarTermList ts = mapMaybe hasSortedVarTerm ts
hasSortedVarTerm :: TERM f
hasSortedVarTerm t = case t of
Qual_var v s _ -> Just (v,s)
Sorted_term tx _ _ -> hasSortedVarTerm tx
Cast tx _ _ -> hasSortedVarTerm tx
------------------------------ Formulas ------------------------------
transOP_SYMB :: IdType_SPId_Map -> OP_SYMB -> SPIdentifier
transOP_SYMB idMap qo@(Qual_op_name op ot _) =
transOP_SYMB _ (Op_name _) = error "SuleCFOL2SoftFOL: unqualified operation"
transPRED_SYMB :: IdType_SPId_Map -> PRED_SYMB -> SPIdentifier
transPRED_SYMB idMap qp@(Qual_pred_name p pt _) =
transPRED_SYMB _ (Pred_name _) = error "SuleCFOL2SoftFOL: unqualified predicate"
-- Translate the quantifier
quantify :: QUANTIFIER -> SPQuantSym
error "SuleCFOL2SoftFOL: no translation for existential quantification."
transVarTup :: (
Set.Set SPIdentifier,IdType_SPId_Map) ->
((
Set.Set SPIdentifier,IdType_SPId_Map),
(SPIdentifier,SPIdentifier))
-- ^ ((new set of used Ids,new map of Ids to original Ids),
-- (var as sp_Id,sort as sp_Id))
transVarTup (usedIds,idMap) (v,s) =
insertSPId vi (CVar s) sid $ deleteSPId vi (CVar s) idMap)
where spSort = maybe (error ("SuleCFOL2SoftFOL: translation of sort \""++
showDoc s "\" not found"))
id (lookupSPId s CSort idMap)
sid = disSPOId (CVar s) (transId (CVar s) vi)
["_Va_"++ showDoc s "_Va"]
typedVarTerm :: SPIdentifier -> SPIdentifier -> SPTerm
typedVarTerm spVar spSort = compTerm (spSym spSort) [simpTerm (spSym spVar)]
spSym :: SPIdentifier -> SPSymbol
compTerm :: SPSymbol -> [SPTerm] -> SPTerm
simpTerm :: SPSymbol -> SPTerm
mkConj :: SPTerm -> SPTerm -> SPTerm
mkConj t1 t2 = compTerm SPAnd [t1,t2]
mkDisj :: SPTerm -> SPTerm -> SPTerm
mkDisj t1 t2 = compTerm SPOr [t1,t2]
mkEq :: SPTerm -> SPTerm -> SPTerm
mkEq t1 t2 = compTerm SPEqual [t1,t2]
mapSen :: (Eq f, Pretty f) => Bool
mapSen siSo trForm sign phi = transFORM siSo (
Set.empty) sign
(snd (transSign sign)) trForm phi
transFORM :: (Eq f, Pretty f) => Bool -- ^ single sorted flag
->
Set.Set PRED_SYMB -- ^ list of predicates to substitute
-> IdType_SPId_Map -> FormulaTranslator f e
transFORM siSo eqPreds sign i tr phi = transFORMULA siSo sign i tr phi'
where phi' = codeOutConditionalF id
(substEqPreds eqPreds id phi))
transFORMULA :: Pretty f => Bool ->
CSign.Sign f e -> IdType_SPId_Map
-> FormulaTranslator f e -> FORMULA f -> SPTerm
transFORMULA siSo sign idMap tr (Quantification qu vdecl phi _) =
SPQuantTerm (quantify qu)
(transFORMULA siSo sign idMap' tr phi)
where ((_,idMap'),vList) =
let (acc',e') = transVarTup acc e
in (acc', (if siSo then simpTerm . spSym . fst
else uncurry typedVarTerm)
(sidSet,idMap) (flatVAR_DECLs vdecl)
sidSet = elemsSPId_Set idMap
transFORMULA siSo sign idMap tr (Conjunction phis _) =
if null phis then SPSimpleTerm SPTrue
else foldl1 mkConj (map (transFORMULA siSo sign idMap tr) phis)
transFORMULA siSo sign idMap tr (Disjunction phis _) =
if null phis then SPSimpleTerm SPFalse
else foldl1 mkDisj (map (transFORMULA siSo sign idMap tr) phis)
transFORMULA siSo sign idMap tr (Implication phi1 phi2 _ _) =
compTerm SPImplies [transFORMULA siSo sign idMap tr phi1,
transFORMULA siSo sign idMap tr phi2]
transFORMULA siSo sign idMap tr (Equivalence phi1 phi2 _) =
compTerm SPEquiv [transFORMULA siSo sign idMap tr phi1,
transFORMULA siSo sign idMap tr phi2]
transFORMULA siSo sign idMap tr (Negation phi _) =
compTerm SPNot [transFORMULA siSo sign idMap tr phi]
transFORMULA _siSo _sign _idMap _tr (True_atom _) = SPSimpleTerm SPTrue
transFORMULA _siSo _sign _idMap _tr (False_atom _) = SPSimpleTerm SPFalse
transFORMULA siSo sign idMap tr (Predication psymb args _) =
compTerm (spSym (transPRED_SYMB idMap psymb))
(map (transTERM siSo sign idMap tr) args)
transFORMULA siSo sign idMap tr (Existl_equation t1 t2 _)
| term_sort t1 == term_sort t2 =
mkEq (transTERM siSo sign idMap tr t1) (transTERM siSo sign idMap tr t2)
transFORMULA siSo sign idMap tr (Strong_equation t1 t2 _)
| term_sort t1 == term_sort t2 =
mkEq (transTERM siSo sign idMap tr t1) (transTERM siSo sign idMap tr t2)
transFORMULA _siSo sign idMap tr (ExtFORMULA phi) = tr sign idMap phi
transFORMULA _ _ _ _ (Definedness _ _) = SPSimpleTerm SPTrue -- totality assumed
transFORMULA siSo sign idMap tr (Membership t s _) =
if siSo then SPSimpleTerm SPTrue
(\si -> compTerm (spSym si) [transTERM siSo sign idMap tr t])
(lookupSPId s CSort idMap)
transFORMULA _ _ _ _ (Sort_gen_ax _ _) =
\ supported at this point!"
transTERM :: Pretty f => Bool ->
CSign.Sign f e -> IdType_SPId_Map
-> FormulaTranslator f e -> TERM f -> SPTerm
transTERM _siSo _sign idMap _tr (Qual_var v s _) =
(simpTerm . spSym) (lookupSPId (simpleIdToId v) (CVar s) idMap)
transTERM siSo sign idMap tr (Application opsymb args _) =
compTerm (spSym (transOP_SYMB idMap opsymb))
(map (transTERM siSo sign idMap tr) args)
transTERM _siSo _sign _idMap _tr (Conditional _t1 _phi _t2 _) =
transTERM siSo sign idMap tr t'@(Sorted_term t s _)
| term_sort t == s = recRes
assert (trace ("Please check sorted term: '"++showDoc t' ""++
"' with sorts '"++show (term_sort t)++
where recRes = transTERM siSo sign idMap tr t
transTERM siSo sign idMap tr t'@(Cast t s _)
| term_sort t == s = recRes
assert (trace ("Please check cast term: '"++showDoc t' ""++
"' with sorts '"++show s++
"' <= '"++show (term_sort t)++"'")
where recRes = transTERM siSo sign idMap tr t
transTERM _siSo _sign _idMap _tr t =