8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder{- |

8a77240a809197c92c0736c431b4b88947a7bac1Christian MaederModule : $Header$

adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian MaederDescription : Coding of a CASL subset into SoftFOL

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiCopyright : (c) Klaus Luettich and Uni Bremen 2005

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : luecke@informatik.uni-bremen.de

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederStability : provisional

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiPortability : non-portable (imports Logic.Logic)

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederThe translating comorphism from a CASL subset to SoftFOL.

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-}

0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowski

adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maedermodule Comorphisms.SuleCFOL2SoftFOL

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski ( suleCFOL2SoftFOL

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski , suleCFOL2SoftFOLInduction

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , suleCFOL2SoftFOLInduction2

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ) where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Control.Exception (assert)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport Control.Monad (foldM)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Logic.Logic as Logic

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Logic.Comorphism

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Common.AS_Annotation

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Common.Id

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Common.Result

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport Common.DocUtils

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport Common.ProofTree

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Common.Lib.Rel as Rel

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport qualified Common.Lib.MapSet as MapSet

ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maeder

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport Text.ParserCombinators.Parsec

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport qualified Data.Map as Map

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport qualified Data.Set as Set

d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Data.List as List

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Data.Maybe

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Data.Char

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport CASL.Logic_CASL

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport CASL.AS_Basic_CASL

adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maederimport CASL.Sublogic as SL

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport CASL.Sign as CSign

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport CASL.Morphism

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport CASL.Quantification

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport CASL.Overload

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport CASL.Utils

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport CASL.Inject

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport CASL.Induction (generateInductionLemmas)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport CASL.Simplify

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport CASL.ToDoc

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport SoftFOL.Sign as SPSign

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport SoftFOL.Logic_SoftFOL

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport SoftFOL.Translate

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport SoftFOL.ParseTPTP

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata PlainSoftFOL = PlainSoftFOL

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Show PlainSoftFOL where

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski show PlainSoftFOL = "SoftFOL"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederdata SoftFOLInduction = SoftFOLInduction deriving Show

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederdata SoftFOLInduction2 = SoftFOLInduction2 deriving Show

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | The identity of the comorphisms

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata GenSuleCFOL2SoftFOL a = GenSuleCFOL2SoftFOL a deriving Show

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersuleCFOL2SoftFOL :: GenSuleCFOL2SoftFOL PlainSoftFOL

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersuleCFOL2SoftFOL = GenSuleCFOL2SoftFOL PlainSoftFOL

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersuleCFOL2SoftFOLInduction :: GenSuleCFOL2SoftFOL SoftFOLInduction

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskisuleCFOL2SoftFOLInduction = GenSuleCFOL2SoftFOL SoftFOLInduction

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskisuleCFOL2SoftFOLInduction2 :: GenSuleCFOL2SoftFOL SoftFOLInduction2

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersuleCFOL2SoftFOLInduction2 = GenSuleCFOL2SoftFOL SoftFOLInduction2

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | SoftFOL theories

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedertype SoftFOLTheory = (SPSign.Sign, [Named SPTerm])

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata CType = CSort

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder | CVar SORT

adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder | CPred CSign.PredType

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder | COp CSign.OpType

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski deriving (Eq, Ord, Show)

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskitoCKType :: CType -> CKType

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedertoCKType ct = case ct of

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski CSort -> CKSort

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder CVar _ -> CKVar

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder CPred _ -> CKPred

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder COp _ -> CKOp

e7d2b3903c7b44db432538b0d720c21062c24823Christian Maeder

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | CASL Ids with Types mapped to SPIdentifier

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskitype IdTypeSPIdMap = Map.Map Id (Map.Map CType SPIdentifier)

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | specialized lookup for IdTypeSPIdMap

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskilookupSPId :: Id -> CType -> IdTypeSPIdMap ->

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Maybe SPIdentifier

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskilookupSPId i t = maybe Nothing (Map.lookup t) . Map.lookup i

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | specialized insert (with error) for IdTypeSPIdMap

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiinsertSPId :: Id -> CType ->

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder SPIdentifier ->

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski IdTypeSPIdMap ->

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski IdTypeSPIdMap

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiinsertSPId i t spid m =

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski assert (checkIdentifier (toCKType t) $ show spid) $

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Map.insertWith (Map.unionWith err) i (Map.insert t spid Map.empty) m

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder where err = error ("SuleCFOL2SoftFOL: for Id \"" ++ show i ++

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu "\" the type \"" ++ show t ++

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu "\" can't be mapped to different SoftFOL identifiers")

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskideleteSPId :: Id -> CType ->

e7d2b3903c7b44db432538b0d720c21062c24823Christian Maeder IdTypeSPIdMap ->

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder IdTypeSPIdMap

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskideleteSPId i t m =

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski maybe m (\ m2 -> let m2' = Map.delete t m2

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski in if Map.null m2'

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder then Map.delete i m

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski else Map.insert i m2' m) $

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Map.lookup i m

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | specialized elems into a set for IdTypeSPIdMap

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederelemsSPIdSet :: IdTypeSPIdMap -> Set.Set SPIdentifier

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskielemsSPIdSet = Map.fold (\ m res -> Set.union res

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski (Set.fromList (Map.elems m)))

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Set.empty

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- extended signature translation

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskitype SignTranslator f e = CSign.Sign f e -> e -> SoftFOLTheory -> SoftFOLTheory

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- extended signature translation for CASL

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskisigTrCASL :: SignTranslator () ()

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedersigTrCASL _ _ = id

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- extended formula translation

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedertype FormulaTranslator f e =

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder CSign.Sign f e -> IdTypeSPIdMap -> f -> SPTerm

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- extended formula translation for CASL

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederformTrCASL :: FormulaTranslator () ()

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederformTrCASL _ _ = error "SuleCFOL2SoftFOL: No extended formulas allowed in CASL"

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance Show a => Language (GenSuleCFOL2SoftFOL a) where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder language_name (GenSuleCFOL2SoftFOL a) = "CASL2" ++ show a

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance Show a => Comorphism (GenSuleCFOL2SoftFOL a)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder CASL CASL_Sublogics

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder CASLSign

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder CASLMor

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder CSign.Symbol RawSymbol ProofTree

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder SoftFOL () () SPTerm () ()

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder SPSign.Sign

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder SoftFOLMorphism SFSymbol () ProofTree where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sourceLogic (GenSuleCFOL2SoftFOL _) = CASL

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sourceSublogic (GenSuleCFOL2SoftFOL a) = SL.cFol

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder { sub_features = LocFilSub

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , cons_features = emptyMapConsFeature

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , has_empty_sorts = show a == show PlainSoftFOL }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder targetLogic (GenSuleCFOL2SoftFOL _) = SoftFOL

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder mapSublogic cid sl =

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder if isSubElem sl $ sourceSublogic cid

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder then Just () else Nothing

c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder map_theory (GenSuleCFOL2SoftFOL a) = transTheory sigTrCASL formTrCASL

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder . case show a of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder str | str == show SoftFOLInduction -> generateInductionLemmas True

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder | str == show SoftFOLInduction2 -> generateInductionLemmas False

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder | otherwise -> id

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder map_sentence (GenSuleCFOL2SoftFOL _) sign =

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder return . mapSen (isSingleSorted sign) formTrCASL sign

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder extractModel (GenSuleCFOL2SoftFOL _) = extractCASLModel

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder has_model_expansion (GenSuleCFOL2SoftFOL _) = True

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- -------------------------- Signature -----------------------------

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedertransFuncMap :: IdTypeSPIdMap ->

a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowski CSign.Sign e f ->

4d7d53fec6b551333c79da6ae3b8ca2af0a741abChristian Maeder (FuncMap, IdTypeSPIdMap)

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedertransFuncMap idMap sign = Map.foldWithKey toSPOpType (Map.empty, idMap)

c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder . MapSet.toMap $ CSign.opMap sign

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder where toSPOpType iden typeSet (fm, im) =

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder if not (Set.null typeSet) && Set.null (Set.deleteMin typeSet) then

d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder let oType = Set.findMin typeSet

d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder sid' = sid fm oType

d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder in (Map.insert sid' (Set.singleton (transOpType oType)) fm,

d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder insertSPId iden (COp oType) sid' im)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder else Set.fold insOIdSet (fm, im) $

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder partOverload (leqF sign)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (partArities (length . CSign.opArgs) typeSet)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder where insOIdSet tset (fm', im') =

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let sid' = sid fm' (Set.findMax tset)

cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich in (Map.insert sid' (Set.map transOpType tset) fm',

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Set.fold (\ x -> insertSPId iden (COp x) sid')

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder im' tset)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sid fma t = disSPOId CKOp (transId CKOp iden)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (uType (transOpType t))

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Set.union (Map.keysSet fma)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (elemsSPIdSet idMap))

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder uType t = fst t ++ [snd t]

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- 1. devide into sets with different arities

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederpartArities :: (Ord a) => (a -> Int) -> Set.Set a -> Set.Set (Set.Set a)

e7d2b3903c7b44db432538b0d720c21062c24823Christian MaederpartArities len = part 0 Set.empty

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder where part i acc s

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder | Set.null s = acc

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder | otherwise =

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder case Set.partition (\ x -> len x == i) s of

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (ar_i, rest) ->

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder part (i + 1) (if Set.null ar_i

e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder then acc

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder else Set.insert ar_i acc) rest

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederpartOverload :: Ord a => (a -> a -> Bool) -> Set.Set (Set.Set a)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> Set.Set (Set.Set a)

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederpartOverload leq =

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Set.fold (Set.union . Set.fromList . Rel.partSet leq) Set.empty

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedertransPredMap :: IdTypeSPIdMap ->

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder CSign.Sign e f ->

cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich (SPSign.PredMap, IdTypeSPIdMap, [Named SPTerm])

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedertransPredMap idMap sign =

e7d2b3903c7b44db432538b0d720c21062c24823Christian Maeder Map.foldWithKey toSPPredType (Map.empty, idMap, []) . MapSet.toMap

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder $ CSign.predMap sign

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder where toSPPredType iden typeSet (fm, im, sen) =

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder if not (Set.null typeSet) && Set.null (Set.deleteMin typeSet) then

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let pType = Set.findMin typeSet

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sid' = sid fm pType

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder in (Map.insert sid' (Set.singleton (transPredType pType)) fm

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , insertSPId iden (CPred pType) sid' im

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , sen)

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder else case -- genPredImplicationDisjunctions sign $

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder partOverload (leqP sign)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (Set.singleton typeSet) of

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (splitTySet) ->

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let (fm', im') =

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Set.fold insOIdSet (fm, im) splitTySet

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder in (fm', im', sen)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder where insOIdSet tset (fm', im') =

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder let sid' = sid fm' (Set.findMax tset)

8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder in (Map.insert sid' (Set.map transPredType tset) fm',

8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder Set.fold (\ x -> insertSPId iden (CPred x) sid')

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder im' tset)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sid fma t = disSPOId CKPred (transId CKPred iden)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (transPredType t)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (Set.union (Map.keysSet fma)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (elemsSPIdSet idMap))

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- left typing implies right typing; explicit overloading sentences

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederare generated from these pairs, type TypePair = (CType,CType) -}

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu-- | disambiguation of SoftFOL Identifiers

a98fd29a06e80e447af26d898044c23497adbc73Mihai CodescudisSPOId :: CKType -- ^ Type of CASl identifier

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> SPIdentifier -- ^ translated CASL Identifier

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> [SPIdentifier] {- ^ translated Sort Symbols of the profile

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (maybe empty) -}

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -> Set.Set SPIdentifier -- ^ SoftFOL Identifiers already in use

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> SPIdentifier {- ^ fresh Identifier generated from second argument;

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if the identifier was not in the set this is just the second argument -}

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederdisSPOId cType sid ty idSet

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu | checkIdentifier cType (show sid) && not (lkup $ show sid) = sid

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu | otherwise = let nSid = disSPOId' $ show sid

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder in assert (checkIdentifier cType nSid) $ mkSimpleId nSid

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu where disSPOId' sid'

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder | not (lkup asid) = asid

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder | otherwise = addType asid 1

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder where asid = sid' ++ case cType of

e7d2b3903c7b44db432538b0d720c21062c24823Christian Maeder CKSort -> ""

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder CKVar -> ""

c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder x -> '_' : show (length ty - (case x of

c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder CKOp -> 1

c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder _ -> 0))

c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder addType res n =

c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder let nres = asid ++ '_' : fc n

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nres' = nres ++ '_' : show n

c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder in if nres == res

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then if nres' == res

c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder then error ("SuleCFOL2SoftFOL: "

c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder ++ "cannot calculate"

c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder ++ " unambiguous id for "

c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder ++ show sid ++ " with type "

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ++ show ty

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder ++ " and nres = " ++ nres

c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder ++ "\n with idSet "

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder ++ show idSet)

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder else if not (lkup nres')

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder then nres'

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder else addType nres (n + 1)

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder else if not (lkup nres)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder then nres

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder else addType nres (n + 1)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lkup x = Set.member (mkSimpleId x) idSet

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder fc n = concatMap (take n . show) ty

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedertransOpType :: CSign.OpType -> ([SPIdentifier], SPIdentifier)

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedertransOpType ot = (map transIdSort (CSign.opArgs ot),

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder transIdSort (CSign.opRes ot))

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedertransPredType :: CSign.PredType -> [SPIdentifier]

e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian MaedertransPredType = map transIdSort . CSign.predArgs

e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- | translate every Id as Sort

e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian MaedertransIdSort :: Id -> SPIdentifier

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaedertransIdSort = transId CKSort

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder

09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederintegrateGenerated :: IdTypeSPIdMap -> [Named (FORMULA f)] ->

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder SPSign.Sign ->

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Result (IdTypeSPIdMap, SPSign.Sign, [Named SPTerm])

cd6e5706893519bfcf24539afa252fcbed5097ddKlaus LuettichintegrateGenerated idMap genSens sign

cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich | null genSens = return (idMap, sign, [])

c40a1fdc8ec6978bd27240d6780d0e0a7b6b0056Dominik Luecke | otherwise =

cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich case partition isAxiom genSens of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (genAxs, genGoals) ->

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder case makeGenGoals sign idMap genGoals of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (newPredsMap, idMap', goalsAndSentences) ->

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -- makeGens must not invent new sorts

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder case makeGens sign idMap' genAxs of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Result dias mv ->

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder maybe (Result dias Nothing)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (\ (spSortMap_makeGens, newOpsMap, idMap'', exhaustSens) ->

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder let spSortMap' =

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Map.union spSortMap_makeGens (SPSign.sortMap sign)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder in assert (Map.size spSortMap' ==

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Map.size (SPSign.sortMap sign))

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (Result dias

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (Just (idMap'',

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign { sortMap = spSortMap'

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , funcMap =

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Map.union (funcMap sign)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder newOpsMap

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , SPSign.predMap =

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Map.union

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (SPSign.predMap sign)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder newPredsMap},

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder mkInjSentences idMap' newOpsMap ++

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder goalsAndSentences ++

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder exhaustSens))))

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder mv

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedermakeGenGoals :: SPSign.Sign -> IdTypeSPIdMap -> [Named (FORMULA f)]

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -> (SPSign.PredMap, IdTypeSPIdMap, [Named SPTerm])

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedermakeGenGoals sign idMap fs =

let Result _ res = makeGens sign idMap fs

in case res of

Nothing -> (Map.empty, idMap, [])

Just (_, _, idMap', fs') ->

let fs'' = map (\ s -> s {isAxiom = False}) fs'

in (Map.empty, idMap', fs'')

{- Sort_gen_ax as goals only implemented through a hack."

sketch of full implementation :

- 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

- prove forall x . P(x)

implementation is postponed as this translation does not produce

only one goal, but additional symbols, axioms and a goal

-}

makeGens :: SPSign.Sign -> IdTypeSPIdMap -> [Named (FORMULA f)]

-> Result (SortMap, FuncMap, IdTypeSPIdMap, [Named SPTerm])

{- ^ The list of SoftFOL sentences gives exhaustiveness for

generated sorts with only constant constructors

and\/or subsort injections, by simply translating

such sort generation constraints to disjunctions -}

makeGens sign idMap fs =

case foldl (makeGen sign) (return (Map.empty, idMap, [], [])) fs of

Result ds mv ->

maybe (Result ds Nothing)

(\ (opM, idMap', pairs, exhaustSens) ->

Result ds

(Just (foldr (uncurry Map.insert)

Map.empty pairs,

opM, idMap', exhaustSens)))

mv

makeGen :: SPSign.Sign

-> Result (FuncMap, IdTypeSPIdMap,

[(SPIdentifier, Maybe Generated)], [Named SPTerm])

-> Named (FORMULA f)

-> Result (FuncMap, IdTypeSPIdMap,

[(SPIdentifier, Maybe Generated)], [Named SPTerm])

makeGen sign 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',

rList ++ genPairs,

eSens ++ eSens')))

else mkError ("Sort generation constraints with " ++

"non-injective sort mappings cannot " ++

"be translated to SoftFOL") mp

where -- compute standard form of sort generation constraints

(srts, ops, mp) = recover_Sort_gen_ax constrs

-- test whether a constructor belongs to a specific sort

hasTheSort s (Qual_op_name _ ot _) = s == res_OP_TYPE ot

hasTheSort _ _ = error "SuleCFOL2SoftFOL.hasTheSort"

mkGen = Just . Generated free . map fst

-- translate constraint for one sort

makeGenP (opM, idMap, exSens) s = ((newOpMap, newIdMap,

exSens ++ eSen ops_of_s s),

(s', mkGen cons))

where ((newOpMap, newIdMap), cons) =

mapAccumL mkInjOp (opM, idMap) ops_of_s

ops_of_s = List.filter (hasTheSort s) ops

s' = fromMaybe (error $ "SuleCFOL2SoftFOL.makeGen: "

++ "No mapping found for '"

++ shows s "'")

(lookupSPId s CSort idMap)

{- is an operation a constant or an injection ?

(we currently can translate only these) -}

isConstorInj o =

nullArgs o || isInjName (opSymbName o)

-- generate sentences for one sort

eSen os s = [ makeNamed (newName s) (SPQuantTerm SPForall

[typedVarTerm var1

$ fromMaybe (error "lookup failed")

(lookupSPId s CSort iMap)] (disj var1 os))

| all isConstorInj os ]

-- generate sentences: compute one disjunct (for one alternative)

mkDisjunct v o@(Qual_op_name _ (Op_type _ args res _) _) =

-- a constant? then just compare with it

case args of

[] -> mkEq (varTerm v) $ varTerm $ transOPSYMB iMap o

{- an injection? then quantify existentially

(for the injection's argument)

since injections are identities, we can leave them out -}

[arg] -> let ta = transIdSort arg in SPQuantTerm SPExists

[ typedVarTerm var2 ta ]

$ mkEq (varTerm v)

$ if Rel.member ta (transIdSort res)

$ SPSign.sortRel sign

then varTerm var2

else compTerm (spSym $ transOPSYMB iMap o) [varTerm var2]

_ -> error "cannot handle ordinary constructors"

mkDisjunct _ _ = error "unqualified operation symbol"

-- make disjunction out of all the alternatives

disj v os = case map (mkDisjunct v) os of

[] -> error "SuleCFOL2SoftFOL: no constructors found"

[x] -> x

xs -> foldl1 mkDisj xs

-- generate enough variables

var = fromJust (find (\ x ->

not (Set.member (mkSimpleId x) usedIds))

("X" : ['X' : show i | i <- [(1 :: Int) ..]]))

var1 = mkSimpleId var

var2 = mkSimpleId $ var ++ "a"

varTerm = simpTerm . spSym

newName s = "ga_exhaustive_generated_sort_" ++ show (pretty s)

usedIds = elemsSPIdSet iMap

nullArgs o = case o of

Qual_op_name _ (Op_type _ args _ _) _ -> null args

_ -> error "SuleCFOL2SoftFOL: wrong constructor"

_ -> r

mkInjOp :: (FuncMap, IdTypeSPIdMap)

-> OP_SYMB

-> ((FuncMap, IdTypeSPIdMap),

(SPIdentifier, ([SPIdentifier], SPIdentifier)))

mkInjOp (opM, idMap) qo@(Qual_op_name i ot _) =

if isInjName i && isNothing lsid

then ((Map.insert i' (Set.singleton (transOpType ot')) opM,

insertSPId i (COp ot') i' idMap),

(i', transOpType ot'))

else ((opM, idMap),

(fromMaybe err lsid,

transOpType ot'))

where i' = disSPOId CKOp (transId CKOp i)

(utype (transOpType ot')) usedNames

ot' = CSign.toOpType ot

lsid = lookupSPId i (COp ot') idMap

usedNames = Map.keysSet opM

err = error ("SuleCFOL2SoftFOL.mkInjOp: Cannot find SPId for '"

++ show qo ++ "'")

utype t = fst t ++ [snd t]

mkInjOp _ _ = error "SuleCFOL2SoftFOL.mkInjOp: Wrong constructor!!"

mkInjSentences :: IdTypeSPIdMap

-> FuncMap

-> [Named SPTerm]

mkInjSentences idMap = Map.foldWithKey genInjs []

where genInjs k tset fs = Set.fold (genInj k) fs tset

genInj k (args, res) =

assert (length args == 1)

. (makeNamed (newName (show k) (show $ head args)

$ show res)

(SPQuantTerm SPForall

[typedVarTerm var $ head args]

(compTerm SPEqual

[compTerm (spSym k)

[simpTerm (spSym var)],

simpTerm (spSym var)])) :)

var = mkSimpleId $

fromJust (find (\ x -> not (Set.member (mkSimpleId x) usedIds))

("Y" : [ 'Y' : show i | i <- [(1 :: Int) ..]]))

newName o a r = "ga_" ++ o ++ '_' : a ++ '_' : r ++ "_id"

usedIds = elemsSPIdSet idMap

{- |

Translate a CASL signature into SoftFOL signature 'SoftFOL.Sign.Sign'.

Before translating, eqPredicate symbols where removed from signature.

-}

transSign :: CSign.Sign f e ->

(SPSign.Sign, IdTypeSPIdMap, [Named SPTerm])

transSign sign = (SPSign.emptySign { SPSign.sortRel =

Rel.map transIdSort (CSign.sortRel sign)

, sortMap = spSortMap

, funcMap = fMap

, SPSign.predMap = pMap

, singleSorted = isSingleSorted sign

}

, idMap''

, predImplications)

where (spSortMap, idMap) =

Set.fold (\ i (sm, im) ->

let sid = disSPOId CKSort (transIdSort i)

[mkSimpleId $ take 20 (cycle "So")]

(Map.keysSet sm)

in (Map.insert sid Nothing sm,

insertSPId i CSort sid im))

(Map.empty, Map.empty)

(CSign.sortSet sign)

(fMap, idMap') = transFuncMap idMap sign

(pMap, idMap'', predImplications) = transPredMap idMap' sign

nonEmptySortSens :: Set.Set SPIdentifier -> SortMap -> [Named SPTerm]

nonEmptySortSens emptySorts sm =

Map.foldWithKey

(\ s _ res ->

if s `Set.member` emptySorts then res else extSen s : res)

[] sm

where extSen s = makeNamed ("ga_non_empty_sort_" ++ show s) $ SPQuantTerm

SPExists [varTerm] $ compTerm (spSym s) [varTerm]

where varTerm = simpTerm $ spSym $ mkSimpleId $ newVar s

newVar s = fromJust $ find (/= show s)

$ "Y" : ['Y' : show i | i <- [(1 :: Int) ..]]

disjointTopSorts :: CSign.Sign f e -> IdTypeSPIdMap -> [Named SPTerm]

disjointTopSorts sign idMap = let

s = CSign.sortSet sign

sl = Rel.partSet (haveCommonSupersorts True sign) s

l = map (\ p -> case keepMinimals1 False sign id $ Set.toList p of

[e] -> e

_ -> error "disjointTopSorts") sl

pairs ls = case ls of

s1 : r -> map (\ s2 -> (s1, s2)) r ++ pairs r

_ -> []

v1 = simpTerm $ spSym $ mkSimpleId "Y1"

v2 = simpTerm $ spSym $ mkSimpleId "Y2"

in map (\ (t1, t2) ->

makeNamed ("disjoint_sorts_" ++ shows t1 "_" ++ show t2) $

SPQuantTerm SPForall

[ compTerm (spSym t1) [v1]

, compTerm (spSym t2) [v2]]

$ compTerm SPNot [mkEq v1 v2]) $ pairs $

map (\ t -> fromMaybe (transIdSort t)

$ lookupSPId t CSort idMap) l

transTheory :: (FormExtension f, Eq f) =>

SignTranslator f e

-> FormulaTranslator f e

-> (CSign.Sign f e, [Named (FORMULA f)])

-> Result SoftFOLTheory

transTheory trSig trForm (sign, sens) =

fmap (trSig sign (CSign.extendedInfo sign))

(case transSign (filterPreds $ foldl insInjOps sign genAxs) of

(tSign, idMap, sign_sens) ->

do (idMap', tSign', sentencesAndGoals) <-

integrateGenerated idMap genSens tSign

let tSignElim = if SPSign.singleSortNotGen tSign'

then tSign' {sortMap = Map.empty} else tSign'

emptySorts = Set.map transIdSort (emptySortSet sign)

return (tSignElim,

sign_sens ++

disjointTopSorts sign idMap' ++

sentencesAndGoals ++

nonEmptySortSens emptySorts (sortMap tSignElim) ++

map (mapNamed (transFORM (singleSortNotGen tSign') eqPreds

sign idMap' trForm))

realSens'))

where (genSens, realSens) =

partition (\ s -> case sentence s of

Sort_gen_ax _ _ -> True

_ -> False) sens

(eqPreds, realSens') = foldl findEqPredicates (Set.empty, []) realSens

(genAxs, _) = partition isAxiom genSens

insInjOps sig s =

case sentence s of

(Sort_gen_ax constrs _) ->

case recover_Sort_gen_ax constrs of

(_, ops, mp) -> assert (null mp) (insertInjOps sig ops)

_ -> error "SuleCFOL2SoftFOL.transTheory.insInjOps"

filterPreds sig =

sig { CSign.predMap = MapSet.difference

(CSign.predMap sig)

(Set.fold (\ pl -> case pl of

Pred_name pn -> MapSet.insert pn (PredType [])

Qual_pred_name pn pt _ ->

MapSet.insert pn $ CSign.toPredType pt)

MapSet.empty eqPreds) }

{- |

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 :: (Eq f) => (Set.Set PRED_SYMB, [Named (FORMULA f)])

-- ^ previous list of found predicates and valid sentences

-> Named (FORMULA f)

-- ^ sentence to check

-> (Set.Set PRED_SYMB, [Named (FORMULA f)])

findEqPredicates (eqPreds, sens) sen =

case sentence sen of

Quantification Universal var_decl quantFormula _ ->

isEquiv (foldl (\ vList (Var_decl v s _) ->

vList ++ map (\ vl -> (vl, s)) v)

[] var_decl)

quantFormula

_ -> validSens

where

validSens = (eqPreds, sens ++ [sen])

isEquiv vars qf =

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

then case qf of

Equivalence f1 f2 _ -> isStrong_eq vars f1 f2

_ -> validSens

else validSens

isStrong_eq vars f1 f2 =

let f1n = case f1 of

Strong_equation _ _ _ -> f1

_ -> f2

f2n = case f1 of

Strong_equation _ _ _ -> f2

_ -> f1

in case f1n of

Strong_equation eq_t1 eq_t2 _ -> case f2n of

Predication eq_pred_symb pterms _ ->

if (Map.toAscList (Map.fromList $ sortedVarTermList pterms)

== Map.toAscList (Map.fromList vars))

&& (Map.toAscList

(Map.fromList $ sortedVarTermList [eq_t1, eq_t2])

== Map.toAscList (Map.fromList vars))

then (Set.insert eq_pred_symb eqPreds, sens)

else validSens

_ -> validSens

_ -> validSens

{- |

Creates a list of (VAR, SORT) out of a list of TERMs. Only Qual_var TERMs

are inserted which will be checked using

'Comorphisms.SuleCFOL2SoftFOL.hasSortedVarTerm'.

-}

sortedVarTermList :: [TERM f] -> [(VAR, SORT)]

sortedVarTermList = mapMaybe hasSortedVarTerm

{- |

Finds a 'CASL.AS_Basic_CASL.Qual_var' term recursively if super term(s) is

'CASL.AS_Basic_CASL.Sorted_term' or 'CASL.AS_Basic_CASL.Cast'.

-}

hasSortedVarTerm :: TERM f -> Maybe (VAR, SORT)

hasSortedVarTerm t = case t of

Qual_var v s _ -> Just (v, s)

Sorted_term tx _ _ -> hasSortedVarTerm tx

Cast tx _ _ -> hasSortedVarTerm tx

_ -> Nothing

-- ---------------------------- Formulas ------------------------------

transOPSYMB :: IdTypeSPIdMap -> OP_SYMB -> SPIdentifier

transOPSYMB idMap ~qo@(Qual_op_name op ot _) =

fromMaybe (error $ "SuleCFOL2SoftFOL.transOPSYMB: unknown op: " ++ show qo)

(lookupSPId op (COp (CSign.toOpType ot)) idMap)

transPREDSYMB :: IdTypeSPIdMap -> PRED_SYMB -> SPIdentifier

transPREDSYMB idMap ~qp@(Qual_pred_name p pt _) = fromMaybe

(error $ "SuleCFOL2SoftFOL.transPREDSYMB: unknown pred: " ++ show qp)

(lookupSPId p (CPred (CSign.toPredType pt)) idMap)

-- | Translate the quantifier

quantify :: QUANTIFIER -> SPQuantSym

quantify q = case q of

Universal -> SPForall

Existential -> SPExists

Unique_existential ->

error "SuleCFOL2SoftFOL: no translation for existential quantification."

transVarTup :: (Set.Set SPIdentifier, IdTypeSPIdMap) ->

(VAR, SORT) ->

((Set.Set SPIdentifier, IdTypeSPIdMap),

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

((Set.insert sid usedIds,

insertSPId vi (CVar s) sid $ deleteSPId vi (CVar s) idMap)

, (sid, spSort))

where spSort = fromMaybe

(error $ "SuleCFOL2SoftFOL: translation of sort \"" ++

showDoc s "\" not found")

(lookupSPId s CSort idMap)

vi = simpleIdToId v

sid = disSPOId CKVar (transId CKVar vi)

[mkSimpleId $ "_Va_" ++ showDoc s "_Va"]

usedIds

mapSen :: (Eq f, FormExtension f) => Bool

-> FormulaTranslator f e

-> CSign.Sign f e -> FORMULA f -> SPTerm

mapSen siSo trForm sign = transFORM siSo Set.empty sign

((\ (_, x, _) -> x) (transSign sign))

trForm

transFORM :: (Eq f, FormExtension f) => Bool -- ^ single sorted flag

-> Set.Set PRED_SYMB -- ^ list of predicates to substitute

-> CSign.Sign f e

-> IdTypeSPIdMap -> FormulaTranslator f e

-> FORMULA f -> SPTerm

transFORM siSo eqPreds sign i tr phi = transFORMULA siSo sign i tr phi'

where phi' = codeOutConditionalF id

(codeOutUniqueExtF id id

(substEqPreds eqPreds id phi))

transFORMULA :: FormExtension f => Bool -> CSign.Sign f e -> IdTypeSPIdMap

-> FormulaTranslator f e -> FORMULA f -> SPTerm

transFORMULA siSo sign idMap tr form = case form of

Quantification qu vdecl phi _ ->

SPQuantTerm (quantify qu)

vList

(transFORMULA siSo sign idMap' tr phi)

where ((_, idMap'), vList) =

mapAccumL (\ acc e ->

let (acc', e') = transVarTup acc e

in (acc', (if siSo then simpTerm . spSym . fst

else uncurry typedVarTerm)

e'))

(sidSet, idMap) (flatVAR_DECLs vdecl)

sidSet = elemsSPIdSet idMap

Conjunction phis _ -> if null phis then simpTerm SPTrue else

foldl1 mkConj (map (transFORMULA siSo sign idMap tr) phis)

Disjunction phis _ -> if null phis then simpTerm SPFalse else

foldl1 mkDisj (map (transFORMULA siSo sign idMap tr) phis)

Implication phi1 phi2 _ _ -> compTerm SPImplies

[transFORMULA siSo sign idMap tr phi1, transFORMULA siSo sign idMap tr phi2]

Equivalence phi1 phi2 _ -> compTerm SPEquiv

[transFORMULA siSo sign idMap tr phi1, transFORMULA siSo sign idMap tr phi2]

Negation phi _ -> compTerm SPNot [transFORMULA siSo sign idMap tr phi]

True_atom _ -> simpTerm SPTrue

False_atom _ -> simpTerm SPFalse

Predication psymb args _ -> compTerm (spSym (transPREDSYMB idMap psymb))

(map (transTERM siSo sign idMap tr) args)

Existl_equation t1 t2 _ -> -- sortOfTerm t1 == sortOfTerm t2

mkEq (transTERM siSo sign idMap tr t1) (transTERM siSo sign idMap tr t2)

Strong_equation t1 t2 _ -> -- sortOfTerm t1 == sortOfTerm t2

mkEq (transTERM siSo sign idMap tr t1) (transTERM siSo sign idMap tr t2)

ExtFORMULA phi -> tr sign idMap phi

Definedness _ _ -> simpTerm SPTrue -- assume totality

Membership t s _ -> if siSo then simpTerm SPTrue else

maybe (error ("SuleCFOL2SoftFOL.tF: no SoftFOL Id found for \"" ++

showDoc s "\""))

(\ si -> compTerm (spSym si) [transTERM siSo sign idMap tr t])

(lookupSPId s CSort idMap)

Sort_gen_ax _ _ ->

error "SuleCFOL2SoftFOL.transFORMULA: Sort_gen_ax"

_ -> error

("SuleCFOL2SoftFOL.transFORMULA: unknown FORMULA '" ++ showDoc form "'")

transTERM :: FormExtension f => Bool -> CSign.Sign f e -> IdTypeSPIdMap

-> FormulaTranslator f e -> TERM f -> SPTerm

transTERM siSo sign idMap tr term = case term of

Qual_var v s _ -> maybe

(error

("SuleCFOL2SoftFOL.tT: no SoftFOL Id found for \"" ++ showDoc v "\""))

(simpTerm . spSym) (lookupSPId (simpleIdToId v) (CVar s) idMap)

Application opsymb args _ ->

compTerm (spSym (transOPSYMB idMap opsymb))

(map (transTERM siSo sign idMap tr) args)

Conditional _t1 _phi _t2 _ ->

error "SuleCFOL2SoftFOL.transTERM: Conditional terms must be coded out."

Sorted_term t _s _ -> -- sortOfTerm t isSubsortOf s

transTERM siSo sign idMap tr t

Cast t _s _ -> -- s isSubsortOf sortOfTerm t

transTERM siSo sign idMap tr t

_ -> error ("SuleCFOL2SoftFOL.transTERM: unknown TERM '" ++ showDoc term "'")

isSingleSorted :: CSign.Sign f e -> Bool

isSingleSorted sign =

Set.size (CSign.sortSet sign) == 1

&& Set.null (emptySortSet sign) -- empty sorts need relativization

-- * extract model out of darwin output stored in a proof tree

extractCASLModel :: CASLSign -> ProofTree

-> Result (CASLSign, [Named (FORMULA ())])

extractCASLModel sign (ProofTree output) =

case parse tptpModel "" output of

Right rfs -> do

let (_, idMap, _) = transSign sign

rMap = getSignMap idMap

(rs, fs1) = partition ((== "interpretation_atoms") . fst) rfs

(ds, fs2) = partition ((== "interpretation_domain") . fst) fs1

(dds, fs3) = partition

((== "interpretation_domain_distinct") . fst) fs2

(es, nm0) = foldl (\ (l, m) (_, s) -> let

(e, m2) = typeCheckForm False sign m s

in (l ++ e, m2)) ([], rMap) rs

nm = foldl (\ m (_, s) -> snd $ typeCheckForm True sign m s) nm0

$ fs3 ++ ds ++ dds

nops = Map.filter (\ v -> case v of

(COp _, Nothing) -> True

_ -> False) nm

os = opMap sign

nos = foldr (\ (i, ~(COp ot, _)) -> addOpTo (simpleIdToId i) ot) os

$ Map.toList nops

nsign = sign { opMap = nos }

mkWarn s = Diag Warning s nullRange

doms <- mapM (\ (n, f) -> do

diss <- getDomElems f

nf <- createDomain sign nm diss

return $ makeNamed n nf) ds

distfs <- mapM (\ (n, f) -> do

let fs = splitConjs f

ets = map (fst . typeCheckForm False sign nm) fs

cs = filter (null . fst) $ zip ets fs

dts <- foldM getUneqElems Set.empty fs

let ws = concatMap ((\ (s, _, _) -> s)

. typeCheckTerm sign Nothing nm)

$ Set.toList dts

Result (map mkWarn ws) $ Just ()

tfs <- mapM (toForm nsign nm . snd) cs

return $ makeNamed n $ simplifyFormula id $ conjunct tfs) dds

terms <- mapM (\ (n, f) -> do

let fs = splitConjs f

ets = map (fst . typeCheckForm False sign nm) fs

(cs, ws) = partition (null . fst) $ zip ets fs

Result (map mkWarn $ concatMap fst ws) $ Just ()

tfs <- mapM (toForm nsign nm . snd) cs

return $ makeNamed n $ simplifyFormula id $ conjunct tfs) fs3

sens <- mapM (\ (n, f) -> do

cf <- toForm nsign nm f

return $ makeNamed n $ simplifyFormula id cf) rs

Result (map mkWarn es) $ Just ()

return (nsign, doms ++ distfs ++ terms ++ sens)

Left err -> fail $ showErr err

type RMap = Map.Map SPIdentifier (CType, Maybe Id)

getSignMap :: IdTypeSPIdMap -> RMap

getSignMap =

foldr (\ (i, m) g -> foldr (\ (t, s) -> case t of

CSort -> Map.insert s (CPred $ PredType [i], Nothing)

_ -> Map.insert s (t, Just i)) g $ Map.toList m)

Map.empty . Map.toList

splitConjs :: SPTerm -> [SPTerm]

splitConjs trm = case trm of

SPComplexTerm SPAnd args ->

concatMap splitConjs args

_ -> [trm]

getUneqElems :: Set.Set SPTerm -> SPTerm -> Result (Set.Set SPTerm)

getUneqElems s trm = case trm of

SPComplexTerm SPNot [SPComplexTerm SPEqual [a1, a2]] ->

return $ Set.insert a2 $ Set.insert a1 s

_ -> fail $ "unexpected disjointness formula: " ++ showDoc trm ""

splitDisjs :: SPTerm -> [SPTerm]

splitDisjs trm = case trm of

SPComplexTerm SPOr args ->

concatMap splitDisjs args

_ -> [trm]

getDomElems :: SPTerm -> Result [SPTerm]

getDomElems trm = case trm of

SPQuantTerm SPForall [var] frm ->

mapM (\ t -> case t of

SPComplexTerm SPEqual [a1, a2]

| var == a1 -> return a2

| var == a2 -> return a1

_ -> fail $ "expecting equation with " ++ show var

++ ", got: " ++ showDoc t "") $ splitDisjs frm

_ -> fail $ "expecting simple quantified disjunction, got: "

++ showDoc trm ""

createDomain :: CASLSign -> RMap -> [SPTerm] -> Result (FORMULA ())

createDomain sign m l = do

let es = map ((\ (e, _, s) -> (e, s)) . typeCheckTerm sign Nothing m) l

tys <- mapM (\ (e, ms) -> case ms of

Just s -> return s

_ -> fail $ unlines e) es

cs <- mapM (\ ds -> do

ts@(trm : r) <- mapM (toTERM m . snd) ds

let mtys = keepMinimals sign id . Set.toList . foldl1 Set.intersection

$ map (\ (ty, _) -> Set.insert ty $ supersortsOf ty sign) ds

case mtys of

[] -> fail $ "no common supersort found for: " ++ showDoc ds ""

ty : _ -> do

let v = mkVarDeclStr "X" ty

return $ mkForall [v]

$ if null r then mkStEq (toQualVar v) trm else

disjunct $ map (mkStEq $ toQualVar v) ts)

. Rel.partList

(\ p1 p2 -> haveCommonSupersorts True sign (fst p1) $ fst p2)

$ zip tys l

return $ conjunct cs

typeCheckForm :: Bool -> CASLSign -> RMap -> SPTerm -> ([String], RMap)

typeCheckForm rev sign m trm =

let srts = sortSet sign

aty = if Set.size srts == 1 then Just $ Set.findMin srts else Nothing

in case trm of

SPQuantTerm _ vars frm -> let

vs = concatMap getVars vars

rm = foldr Map.delete m vs

(errs, nm) = typeCheckForm rev sign rm frm

m2 = foldr Map.delete nm vs

in (errs, Map.union m m2)

SPComplexTerm SPEqual [a1, a2] -> let

(r1, m1, ety) = typeCheckEq sign aty m a1 a2

in case ety of

Nothing -> (r1, m1)

Just _ -> let

(r2, m2, _) = typeCheckEq sign ety m1 a2 a1

in (r2, m2)

SPComplexTerm (SPCustomSymbol cst) args ->

case Map.lookup cst m of

Just (CPred pt, _) | length args == length (predArgs pt) ->

foldl (\ (b, p) (s, a) -> let

(nb, nm, _) = typeCheckTerm sign (Just s) p a

in (b ++ nb, nm))

([], m) $ zip (predArgs pt) args

_ -> (["unknown predicate: " ++ show cst], m)

SPComplexTerm _ args ->

foldl (\ (b, p) a -> let

(nb, nm) = typeCheckForm rev sign p a

in (b ++ nb, nm)) ([], m) $ if rev then reverse args else args

typeCheckEq :: CASLSign -> Maybe SORT -> RMap -> SPTerm -> SPTerm

-> ([String], RMap, Maybe SORT)

typeCheckEq sign aty m a1 a2 = let

(r1, m1, ty1) = typeCheckTerm sign aty m a1

(r2, m2, ty2) = typeCheckTerm sign aty m1 a2

in case (ty1, ty2) of

(Just s1, Just s2) ->

(r1 ++ r2

++ [ "different types " ++ show (s1, s2) ++ " in equation: "

++ showDoc a1 " = " ++ showDoc a2 ""

| not $ haveCommonSupersorts True sign s1 s2], m2, Nothing)

(Nothing, _) -> (r1, m2, ty2)

(_, Nothing) -> (r1 ++ r2, m2, ty1)

typeCheckTerm :: CASLSign -> Maybe SORT -> RMap -> SPTerm

-> ([String], RMap, Maybe SORT)

typeCheckTerm sign ty m trm =

let srts = sortSet sign

aty = if Set.size srts == 1 then Just $ Set.findMin srts else Nothing

in case trm of

SPComplexTerm (SPCustomSymbol cst) args -> case Map.lookup cst m of

Nothing -> let

(fb, fm, aTys) = foldr (\ a (b, p, tys) -> let

(nb, nm, tya) = typeCheckTerm sign aty p a

in (b ++ nb, nm, tya : tys)) ([], m, []) args

in case ty of

Just r | all isJust aTys ->

if null args && isVar cst then

(fb, Map.insert cst (CVar r, Nothing) fm, ty)

else (fb, Map.insert cst

(COp $ mkTotOpType (catMaybes aTys) r, Nothing) fm

, ty)

_ -> (["no type for: " ++ showDoc trm ""], fm, ty)

Just (COp ot, _) -> let

aTys = opArgs ot

rTy = opRes ot

(fb, fm) = foldl (\ (b, p) (s, a) -> let

(nb, nm, _) = typeCheckTerm sign (Just s) p a

in (b ++ nb, nm)) ([], m) $ zip aTys args

aTyL = length aTys

argL = length args

in (fb ++

["expected " ++ show aTyL ++ " arguments, but found "

++ show argL ++ " for: " ++ show cst | aTyL /= argL]

++ case ty of

Just r -> ["expected result sort " ++ show r ++ ", but found "

++ show rTy ++ " for: " ++ show cst | not $ leqSort sign rTy r ]

_ -> [], fm, Just rTy)

Just (CVar s2, _) ->

(["unexpected arguments for variable: " ++ show cst | not $ null args]

++ case ty of

Just r -> ["expected variable sort " ++ show r ++ ", but found "

++ show s2 ++ " for: " ++ show cst | not $ leqSort sign s2 r ]

_ -> [], m, Just s2)

_ -> (["unexpected predicate in term: " ++ showDoc trm ""], m, ty)

_ -> (["unexpected term: " ++ showDoc trm ""], m, ty)

toForm :: Monad m => CASLSign -> RMap -> SPTerm -> m (FORMULA ())

toForm sign m t = case t of

SPQuantTerm q vars frm -> do

let vs = concatMap getVars vars

rm = foldr Map.delete m vs

(b, nm) = typeCheckForm False sign rm frm

nvs = mapMaybe (toVar nm) vars

nf <- toForm sign nm frm

if null b then return $ Quantification (toQuant q) nvs nf nullRange

else fail $ unlines b

SPComplexTerm SPEqual [a1, a2] -> do

t1 <- toTERM m a1

t2 <- toTERM m a2

return $ mkStEq t1 t2

SPComplexTerm (SPCustomSymbol cst) args ->

case Map.lookup cst m of

Just (CPred pt, mi) | length args == length (predArgs pt) -> do

ts <- mapM (toTERM m) args

case mi of

Nothing -> case args of

[_] -> return (True_atom nullRange)

_ -> fail $ "unkown predicate: " ++ show cst

Just i -> return (Predication

(Qual_pred_name i (toPRED_TYPE pt) nullRange)

ts nullRange)

_ -> fail $ "inconsistent pred symbol: " ++ show cst

SPComplexTerm symb args -> do

fs <- mapM (toForm sign m) args

case (symb, fs) of

(SPNot, [f]) -> return (Negation f nullRange)

(SPImplies, [f1, f2]) -> return (mkImpl f1 f2)

(SPImplied, [f2, f1]) -> return (Implication f1 f2 False nullRange)

(SPEquiv, [f1, f2]) -> return (mkEqv f1 f2)

(SPAnd, _) -> return (conjunct fs)

(SPOr, _) -> return (Disjunction fs nullRange)

(SPTrue, []) -> return (True_atom nullRange)

(SPFalse, []) -> return (False_atom nullRange)

_ -> fail $ "wrong boolean formula: " ++ showDoc t ""

toTERM :: Monad m => RMap -> SPTerm -> m (TERM ())

toTERM m spt = case spt of

SPComplexTerm (SPCustomSymbol cst) args -> case Map.lookup cst m of

Just (CVar s, _) | null args -> return $ Qual_var cst s nullRange

Just (COp ot, mi) | length args == length (opArgs ot) -> do

ts <- mapM (toTERM m) args

return $ Application (Qual_op_name (case mi of

Just i -> i

_ -> simpleIdToId cst) (toOP_TYPE ot) nullRange)

ts nullRange

_ -> fail $ "cannot reconstruct term: " ++ showDoc spt ""

_ -> fail $ "cannot reconstruct term: " ++ showDoc spt ""

toQuant :: SPQuantSym -> QUANTIFIER

toQuant sp = case sp of

SPForall -> Universal

SPExists -> Existential

_ -> error "toQuant"

toVar :: Monad m => RMap -> SPTerm -> m VAR_DECL

toVar m sp = case sp of

SPComplexTerm (SPCustomSymbol cst) [] | isVar cst -> case Map.lookup cst m of

Just (CVar s, _) -> return $ Var_decl [cst] s nullRange

_ -> fail $ "unknown variable: " ++ show cst

_ -> fail $ "quantified term as variable: " ++ showDoc sp ""

isVar :: SPIdentifier -> Bool

isVar cst = case tokStr cst of

c : _ -> isUpper c

"" -> error "isVar"

getVars :: SPTerm -> [SPIdentifier]

getVars tm = case tm of

SPComplexTerm (SPCustomSymbol cst) args ->

if null args then [cst] else concatMap getVars args

_ -> []