{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : ./Comorphisms/ExtModal2HasCASL.hs

Copyright : (c) Christian Maeder, DFKI 2012

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : non-portable (MPTC-FD)

-}

module Comorphisms.ExtModal2HasCASL (ExtModal2HasCASL (..)) where

import Logic.Logic

import Logic.Comorphism

import Common.AS_Annotation

import Common.DocUtils

import Common.Id

import qualified Common.Lib.Rel as Rel

import qualified Common.Lib.MapSet as MapSet

import Comorphisms.CASL2HasCASL

import CASL.AS_Basic_CASL as CASL

import CASL.Fold

import CASL.Morphism as CASL

import CASL.Overload

import CASL.Sign as CASL

import CASL.Sublogic as CASL

import CASL.World

import Data.List

import Data.Maybe

import Data.Function

import qualified Data.Map as Map

import qualified Data.Set as Set

import ExtModal.Logic_ExtModal

import ExtModal.AS_ExtModal

import ExtModal.ExtModalSign

import ExtModal.Sublogic as EM

import HasCASL.Logic_HasCASL

import HasCASL.As as HC

import HasCASL.AsUtils as HC

import HasCASL.Builtin

import HasCASL.DataAna

import HasCASL.Le as HC

import HasCASL.Unify

import HasCASL.Sublogic as HC

data ExtModal2HasCASL = ExtModal2HasCASL deriving (Show)

instance Language ExtModal2HasCASL

instance Comorphism ExtModal2HasCASL

ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS

SYMB_MAP_ITEMS ExtModalSign ExtModalMorph

CASL.Symbol CASL.RawSymbol ()

HasCASL HC.Sublogic

BasicSpec Sentence SymbItems SymbMapItems

Env HC.Morphism HC.Symbol HC.RawSymbol () where

sourceLogic ExtModal2HasCASL = ExtModal

sourceSublogic ExtModal2HasCASL = mkTop maxSublogic

{ hasTransClos = False

, hasFixPoints = False }

targetLogic ExtModal2HasCASL = HasCASL

mapSublogic ExtModal2HasCASL sl = Just HC.caslLogic

{ HC.which_logic = HOL

, HC.has_sub = CASL.has_sub sl

, HC.has_part = CASL.has_part sl }

map_theory ExtModal2HasCASL (sig, allSens) = let

(frames, sens) = partition (isFrameAx . sentence) allSens

in case transSig sig sens of

(mme, s) -> return

(mme, map (\ (n, d) -> makeNamed n $ DatatypeSen [d])

[("natural numbers", natType), ("numbered worlds", worldType)]

++ s ++ transFrames sig frames

++ map (mapNamed $ toSen sig) sens)

has_model_expansion ExtModal2HasCASL = True

is_weakly_amalgamable ExtModal2HasCASL = True

nomName :: Id -> Id

nomName t = Id [genToken "N"] [t] $ rangeOfId t

nomOpType :: OpType

nomOpType = mkTotOpType [] world

mkOp :: Id -> Type -> Term

mkOp i = mkOpTerm i . simpleTypeScheme

mkNomAppl :: Id -> Term

mkNomAppl pn = mkOp (nomName pn) $ trOp nomOpType

eqWorld :: Id -> Term -> Term -> Term

eqWorld i = mkEqTerm i (toType world) nr

eqW :: Term -> Term -> Term

eqW = eqWorld eqId

mkNot :: Term -> Term

mkNot = mkTerm notId notType [] nr

mkConj :: [Term] -> Term

mkConj l = (if null l then unitTerm trueId else toBinJunctor andId l) nr

mkDisj :: [Term] -> Term

mkDisj l =

(if null l then unitTerm falseId else toBinJunctor orId l) nr

mkExQs :: [GenVarDecl] -> Term -> Term

mkExQs vs t =

QuantifiedTerm HC.Existential vs t nr

mkExQ :: VarDecl -> Term -> Term

mkExQ vd = mkExQs [GenVarDecl vd]

mkExConj :: VarDecl -> [Term] -> Term

mkExConj vd = mkExQ vd . mkConj

tauS :: String

tauS = "tau"

tauId :: Id

tauId = genName tauS

tauCaslTy :: PredType

tauCaslTy = PredType [world, world]

tauTy :: Type

tauTy = trPrSyn $ toPRED_TYPE tauCaslTy

{- | we now consider numbered worlds:

free type WN ::= mkWN World Nat -}

nWorldId :: SORT

nWorldId = genName "WN"

mkNWorldId :: Id

mkNWorldId = genName "mkWN"

nWorld :: Type

nWorld = toType nWorldId

binPredTy :: Type -> Type

binPredTy = getFunType unitType HC.Partial . replicate 2

isTransS :: String

isTransS = "isTrans"

isTransId :: Id

isTransId = genName isTransS

prOfBinPrTy :: Type -> Type

prOfBinPrTy = predType nr . binPredTy

prOfNwPrTy :: Type

prOfNwPrTy = prOfBinPrTy nWorld

containsS :: String

containsS = "contains"

containsId :: Id

containsId = genName containsS

transTy :: Type -> Type

transTy = getFunType unitType HC.Partial . replicate 2 . binPredTy

-- | mixfix names work for tuples and are lost after currying

trI :: Id -> Id

trI i = if isMixfix i then Id [genToken "C"] [i] $ rangeOfId i else i

trOpSyn :: OP_TYPE -> Type

trOpSyn (Op_type ok args res _) = let

(partial, total) = case ok of

CASL.Total -> (HC.Total, True)

CASL.Partial -> (HC.Partial, False)

resTy = toType res

in if null args then if total then resTy else mkLazyType resTy

else getFunType resTy partial $ map toType args

trOp :: OpType -> Type

trOp = trOpSyn . toOP_TYPE

trPrSyn :: PRED_TYPE -> Type

trPrSyn (Pred_type args ps) = let u = unitTypeWithRange ps in

if null args then mkLazyType u else

getFunType u HC.Partial $ map toType args

trPr :: PredType -> Type

trPr = trPrSyn . toPRED_TYPE

-- | add world arguments to flexible ops and preds; and add relations

transSig :: ExtModalSign -> [Named (FORMULA EM_FORMULA)]

-> (Env, [Named Sentence])

transSig sign sens = let

s1 = embedSign () sign

extInf = extendedInfo sign

flexibleOps = flexOps extInf

flexiblePreds = flexPreds extInf

flexOps' = addWorldOp world id flexibleOps

flexPreds' = addWorldPred world id flexiblePreds

rigOps' = diffOpMapSet (opMap sign) flexibleOps

rigPreds' = diffMapSet (predMap sign) flexiblePreds

noms = nominals extInf

noNomsPreds = Set.fold (`MapSet.delete` nomPType) rigPreds' noms

termMs = termMods extInf

timeMs = timeMods extInf

rels = Set.fold (\ m ->

insertModPred world (Set.member m timeMs) (Set.member m termMs) m)

MapSet.empty $ modalities extInf

nomOps = Set.fold (\ n -> addOpTo (nomName n) nomOpType) rigOps' noms

s2 = s1

{ sortRel = Rel.insertKey world $ sortRel sign

, opMap = addOpMapSet flexOps' nomOps

, predMap = addMapSet rels $ addMapSet flexPreds' noNomsPreds

}

env = mapSigAux trI trOp trPr (getConstructors sens) s2

mkOpInfo t = Set.singleton . OpInfo (simpleTypeScheme t) Set.empty

insOpInfo = Map.insertWith Set.union

insF (i, t) = insOpInfo i . mkOpInfo t $ NoOpDefn Fun

in ( env

{ assumps = foldr (uncurry insOpInfo)

(foldr insF (assumps env)

[ (tauId, tauTy)

, (isTransId, prOfNwPrTy)

, (reflexId, prOfNwPrTy)

, (irreflexId, prOfNwPrTy)

, (containsId, transTy nWorld)

, (transId, transTy nWorld)

, (transReflexId, transTy nWorld)

, (transLinearOrderId, prOfNwPrTy)

, (hasSuccessorId, hasSuccessorTy)

, (subsetOfTauId, prOfNwPrTy)

, (hasTauSucId, prOfNwPrTy)

, (superpathId, hasSuccessorTy)

, (pathId, hasSuccessorTy)

])

[ altToOpInfo natId zeroAlt

, altToOpInfo natId sucAlt

, altToOpInfo nWorldId worldAlt

, selWorldInfo getWorldSel

, selWorldInfo numSel

]

, typeMap = Map.insert nWorldId starTypeInfo

{ typeDefn = DatatypeDefn worldType }

. Map.insert natId starTypeInfo

{ typeDefn = DatatypeDefn natType }

$ typeMap env

}

, makeNamed "nat_induction" (Formula $ inductionScheme [natType])

: makeDataSelEqs (toDataPat worldType) [worldAlt]

++ map (\ (s, t) -> makeNamed s $ Formula t)

[ (tauS, tauDef termMs $ Set.toList timeMs)

, (isTransS, isTransDef nWorld)

, (reflexS, reflexDef True nWorld)

, (irreflexS, reflexDef False nWorld)

, (containsS, containsDef nWorld)

, (transS, someDef transId (transContainsDef nWorld) nWorld)

, (transReflexS, someDef transReflexId

(transReflexContainsDef nWorld) nWorld)

, (transLinearOrderS, transLinearOrderDef nWorld)

, (hasSuccessorS, hasSuccessorDef)

, (subsetOfTauS, subsetOfTauDef)

, (hasTauSucS, hasTauSucDefAny)

, (superpathS, superpathDef)

, (pathS, pathDef)

]

)

vQuad :: Type -> [VarDecl]

vQuad w = map (\ n -> hcVarDecl (genNumVar "v" n) w) [1, 2, 3, 4]

quadDs :: Type -> [GenVarDecl]

quadDs = map GenVarDecl . vQuad

tripDs :: Type -> [GenVarDecl]

tripDs = take 3 . quadDs

pairDs :: Type -> [GenVarDecl]

pairDs = take 2 . tripDs

tQuad :: Type -> [Term]

tQuad = map QualVar . vQuad

tTrip :: Type -> [Term]

tTrip = take 3 . tQuad

tPair :: Type -> [Term]

tPair = take 2 . tTrip

nr :: Range

nr = nullRange

worldTy :: Type

worldTy = toType world

tauDef :: Set.Set Id -> [Id] -> Term

tauDef termMs timeMs = let ts = tPair worldTy in

HC.mkForall (pairDs worldTy)

. mkLogTerm eqvId nr

(mkApplTerm (mkOp tauId tauTy) ts)

. mkDisj

$ map (\ tm ->

let v = varDecl (genToken "t") tm

term = Set.member tm termMs

in (if term then mkExQ v else id) $ mkApplTerm

(mkOp (relOfMod True term tm)

. trPr $ modPredType world term tm)

$ if term then QualVar v : ts else ts)

timeMs

pVar :: Type -> VarDecl

pVar = hcVarDecl (genToken "P") . binPredTy

isTransDef :: Type -> Term

isTransDef w = let

p = pVar w

pt = QualVar p

[t1, t2, t3] = tTrip w

in HC.mkForall [GenVarDecl p]

. mkLogTerm eqvId nr

(mkApplTerm (mkOp isTransId $ prOfBinPrTy w) [pt])

. HC.mkForall (tripDs w)

. mkLogTerm implId nr

(mkLogTerm andId nr

(mkApplTerm pt [t1, t2])

$ mkApplTerm pt [t2, t3])

$ mkApplTerm pt [t1, t3]

trichotomyDef :: Type -> Term -> Term -> Term -> Term

trichotomyDef w pt t1 t2 = mkLogTerm orId nr

(dichotomyDef pt t1 t2)

$ mkEqTerm eqId w nr t1 t2

dichotomyDef :: Term -> Term -> Term -> Term

dichotomyDef pt t1 t2 = mkLogTerm orId nr

(mkApplTerm pt [t1, t2])

$ mkApplTerm pt [t2, t1]

linearOrderDef :: Type -> Term -> Term

linearOrderDef w pt = let

[t1, t2, t3, t4] = tQuad w

in HC.mkForall (pairDs w)

. mkLogTerm implId nr

(mkExQs (drop 2 $ quadDs w)

. mkLogTerm andId nr

(dichotomyDef pt t1 t3)

$ dichotomyDef pt t2 t4)

$ trichotomyDef w pt t1 t2

transLinearOrderS :: String

transLinearOrderS = "trans_linear_order"

transLinearOrderId :: Id

transLinearOrderId = genName transLinearOrderS

transLinearOrderDef :: Type -> Term

transLinearOrderDef w = let

ps = rAndQ w

[pv, qv] = map GenVarDecl ps

ts@[pt, qt] = map QualVar ps

in HC.mkForall [pv]

. mkLogTerm eqvId nr

(mkApplTerm (mkOp transLinearOrderId $ prOfBinPrTy w) [pt])

. mkExQs [qv]

. mkLogTerm andId nr

(mkApplTerm (mkOp transId $ transTy w) ts)

$ linearOrderDef w qt

natId :: SORT

natId = stringToId "Nat"

natTy :: Type

natTy = toType natId

sucId :: Id

sucId = stringToId "suc"

zero :: Id

zero = stringToId "0"

natType :: DataEntry

natType =

DataEntry Map.empty natId Free [] rStar

$ Set.fromList [zeroAlt, sucAlt]

zeroAlt :: AltDefn

zeroAlt = Construct (Just zero) [] HC.Total []

sucAlt :: AltDefn

sucAlt = Construct (Just sucId) [natTy] HC.Total [typeToSelector Nothing natTy]

altToTy :: Id -> AltDefn -> Type

altToTy i (Construct _ ts p _) = getFunType (toType i) p ts

altToOpInfo :: Id -> AltDefn -> (Id, Set.Set OpInfo)

altToOpInfo i c@(Construct m _ _ _) = let Just n = m in

(n, Set.singleton .

OpInfo (simpleTypeScheme $ altToTy i c) Set.empty

$ ConstructData i)

getWorldId :: Id

getWorldId = genName "getWorld"

numId :: Id

numId = genName "num"

worldType :: DataEntry

worldType = DataEntry Map.empty nWorldId Free [] rStar $ Set.singleton worldAlt

worldAlt :: AltDefn

worldAlt = Construct (Just mkNWorldId) [worldTy, natTy] HC.Total

[getWorldSel, numSel]

getWorldSel :: [Selector]

getWorldSel = typeToSelector (Just getWorldId) worldTy

numSel :: [Selector]

numSel = typeToSelector (Just numId) natTy

nWorldTy :: Type

nWorldTy = altToTy nWorldId worldAlt

selWorldInfo :: [Selector] -> (Id, Set.Set OpInfo)

selWorldInfo = selToOpInfo nWorldId . Set.singleton . ConstrInfo mkNWorldId

$ simpleTypeScheme nWorldTy

selToTy :: Id -> [Selector] -> (Id, Type)

selToTy i s = let [Select (Just n) t p] = s in

(n, getFunType t p [toType i])

selToOpInfo :: Id -> Set.Set ConstrInfo -> [Selector] -> (Id, Set.Set OpInfo)

selToOpInfo i c s = let (n, ty) = selToTy i s in

(n, Set.singleton . OpInfo (simpleTypeScheme ty) Set.empty

$ SelectData c i)

rAndQ :: Type -> [VarDecl]

rAndQ w = map (\ c -> hcVarDecl (genToken [c]) $ binPredTy w) "RQ"

containsDef :: Type -> Term

containsDef w = let -- q contains r

ps = rAndQ w

ts@[pt, qt] = map QualVar ps

in HC.mkForall (map GenVarDecl ps)

. mkLogTerm eqvId nr

(mkApplTerm (mkOp containsId $ transTy w) ts)

$ containsDefAux False implId pt qt w

containsDefAux :: Bool -> Id -> Term -> Term -> Type -> Term

containsDefAux neg op pt qt w = let ts = tPair w in

HC.mkForall (pairDs w) . (if neg then mkNot else id)

. mkLogTerm op nr (mkApplTerm pt ts) $ mkApplTerm qt ts

someContainsDef :: (Term -> Term) -> Type -> Term -> Term -> Term

someContainsDef sPred w pt qt = let -- q fulfills sPred and contains r

ts = [pt, qt]

in mkLogTerm andId nr (sPred qt)

$ mkApplTerm (mkOp containsId $ transTy w) ts

transContainsDef :: Type -> Term -> Term -> Term

transContainsDef w = someContainsDef

(\ qt -> mkApplTerm (mkOp isTransId $ prOfBinPrTy w) [qt]) w

transReflexContainsDef :: Type -> Term -> Term -> Term

transReflexContainsDef w = someContainsDef

(\ qt -> mkLogTerm andId nr

(mkApplTerm (mkOp isTransId $ prOfBinPrTy w) [qt])

$ mkApplTerm (mkOp reflexId $ prOfBinPrTy w) [qt]) w

transS :: String

transS = "trans"

transId :: Id

transId = genName transS

transReflexS :: String

transReflexS = "trans_reflex"

transReflexId :: Id

transReflexId = genName transReflexS

someDef :: Id -> (Term -> Term -> Term) -> Type -> Term

someDef dId op w = let -- q is the (smallest) something containing r

ps = rAndQ w

ts@[pt, qt] = map QualVar ps

z = pVar w

zt = QualVar z

in HC.mkForall (map GenVarDecl ps)

. mkLogTerm eqvId nr

(mkApplTerm (mkOp dId $ transTy w) ts)

. mkLogTerm andId nr (op pt qt)

. HC.mkForall [GenVarDecl z]

. mkLogTerm implId nr (op pt zt)

$ mkApplTerm (mkOp containsId $ transTy w) [qt, zt]

reflexS :: String

reflexS = "reflex"

irreflexS :: String

irreflexS = "irreflex"

reflexId :: Id

reflexId = genName reflexS

irreflexId :: Id

irreflexId = genName irreflexS

reflexDef :: Bool -> Type -> Term

reflexDef refl w = let

x = hcVarDecl (genToken "x") w

p = pVar w

pt = QualVar p

in HC.mkForall [GenVarDecl p]

. mkLogTerm eqvId nr

(mkApplTerm (mkOp (if refl then reflexId else irreflexId)

$ prOfBinPrTy w) [pt])

. HC.mkForall [GenVarDecl x]

. (if refl then id else mkNot)

. mkApplTerm pt . replicate 2 $ QualVar x

varDecl :: Token -> SORT -> VarDecl

varDecl i = hcVarDecl i . toType

hcVarDecl :: Token -> Type -> VarDecl

hcVarDecl i t = VarDecl (simpleIdToId i) t Other nr

varTerm :: Token -> SORT -> Term

varTerm i = QualVar . varDecl i

typeToSelector :: Maybe Id -> Type -> [Selector]

typeToSelector m a = [Select m a HC.Total]

hasSuccessorS :: String

hasSuccessorS = "has_successor"

hasSuccessorId :: Id

hasSuccessorId = genName hasSuccessorS

hasSuccessorTy :: Type

hasSuccessorTy = getFunType unitType HC.Partial [worldTy, binPredTy nWorld]

tauApplTerm :: Term -> Term -> Term

tauApplTerm t1 t2 = mkApplTerm (mkOp tauId tauTy) [t1, t2]

zeroT :: Term

zeroT = mkOp zero natTy

hasSuccessorDef :: Term

hasSuccessorDef = let

[x0, p] = xZeroAndP

(tT, _, rT) = hasTauSucDefAux zeroT

in HC.mkForall (map GenVarDecl [x0, p])

. mkLogTerm eqvId nr

(mkApplTerm (mkOp hasSuccessorId hasSuccessorTy) $ map QualVar [x0, p])

$ mkLogTerm implId nr tT rT

xZeroAndP :: [VarDecl]

xZeroAndP = [hcVarDecl (genNumVar "x" 0) worldTy, pVar nWorld]

pairWorld :: Term -> Term -> Term

pairWorld t1 t2 = mkApplTerm (mkOp mkNWorldId nWorldTy) [t1, t2]

sucTy :: Type

sucTy = altToTy natId sucAlt

sucTerm :: Term -> Term

sucTerm t = mkApplTerm (mkOp sucId sucTy) [t]

hasTauSucDefAux :: Term -> (Term, Term, Term)

hasTauSucDefAux nT = let

x = hcVarDecl (genToken "x") worldTy

vs = xZeroAndP

[xt, xt0, pt] = map QualVar $ x : vs

tauAppl = tauApplTerm xt0 xt

pw = pairWorld xt0 nT

in (mkExQ x tauAppl, pw,

mkExQ x

. mkLogTerm andId nr tauAppl

$ mkApplTerm pt [pw, pairWorld xt $ sucTerm nT])

hasTauSucS :: String

hasTauSucS = "has_tau_suc"

hasTauSucId :: Id

hasTauSucId = genName hasTauSucS

hasTauSucDefAny :: Term

hasTauSucDefAny = let

nv = hcVarDecl (genToken "n") natTy

nt = QualVar nv

[x0, p] = xZeroAndP

(tT, pw, rT) = hasTauSucDefAux nt

y = hcVarDecl (genToken "y") nWorld

in HC.mkForall [GenVarDecl p]

. mkLogTerm eqvId nr

(mkApplTerm (mkOp hasTauSucId prOfNwPrTy) [QualVar p])

. HC.mkForall (map GenVarDecl [x0, nv])

$ mkLogTerm implId nr

(mkLogTerm andId nr

(mkExQ y $ mkApplTerm (QualVar p) [QualVar y, pw])

tT) rT

subsetOfTauS :: String

subsetOfTauS = "subset_of_tau"

subsetOfTauId :: Id

subsetOfTauId = genName subsetOfTauS

getWorld :: Term -> Term

getWorld t = mkApplTerm (uncurry mkOp $ selToTy nWorldId getWorldSel) [t]

subsetOfTauDef :: Term

subsetOfTauDef = let

p = pVar nWorld

pt = QualVar p

ts@[xt, yt] = tPair nWorld

in HC.mkForall [GenVarDecl p]

. mkLogTerm eqvId nr

(mkApplTerm (mkOp subsetOfTauId prOfNwPrTy) [pt])

. HC.mkForall (pairDs nWorld)

. mkLogTerm implId nr

(mkApplTerm pt ts)

. tauApplTerm (getWorld xt) $ getWorld yt

superpathS :: String

superpathS = "superpath"

superpathId :: Id

superpathId = genName superpathS

superpathDef :: Term

superpathDef = let

vs = xZeroAndP

ts@[_, pt] = map QualVar vs

in HC.mkForall (map GenVarDecl vs)

. mkLogTerm eqvId nr

(mkApplTerm (mkOp superpathId hasSuccessorTy) ts)

. mkConj

$ mkApplTerm (mkOp hasSuccessorId hasSuccessorTy) ts

: map (\ i -> mkApplTerm (mkOp i prOfNwPrTy) [pt])

[irreflexId, subsetOfTauId, hasTauSucId, transLinearOrderId]

pathS :: String

pathS = "path"

pathId :: Id

pathId = genName pathS

pathAppl :: [Term] -> Term

pathAppl = mkApplTerm $ mkOp pathId hasSuccessorTy

pathDef :: Term

pathDef = let

vs = xZeroAndP

[rv, qv] = rAndQ nWorld

[rt, qt] = map QualVar [rv, qv]

ts@[x0, pt] = map QualVar vs

in HC.mkForall (map GenVarDecl vs)

. mkLogTerm eqvId nr

(pathAppl ts)

. mkExQ rv

$ mkConj

[ mkApplTerm (mkOp superpathId hasSuccessorTy) [x0, rt]

, mkApplTerm (mkOp transReflexId $ transTy nWorld) [rt, pt]

, HC.mkForall [GenVarDecl qv]

. mkLogTerm implId nr

(mkApplTerm (mkOp superpathId hasSuccessorTy) [x0, qt])

. mkLogTerm orId nr

(containsDefAux True implId qt rt nWorld)

$ containsDefAux False eqvId qt rt nWorld

]

toSen :: ExtModalSign -> FORMULA EM_FORMULA -> Sentence

toSen msig f = case f of

Sort_gen_ax cs b -> let

(sorts, ops, smap) = recover_Sort_gen_ax cs

genKind = if b then Free else Generated

mapPart :: OpKind -> Partiality

mapPart cp = case cp of

CASL.Total -> HC.Total

CASL.Partial -> HC.Partial

in DatatypeSen $ map ( \ s ->

DataEntry (Map.fromList smap) s genKind [] rStar

$ Set.fromList $ map ( \ (i, t) ->

let args = map toType $ opArgs t in

Construct (if isInjName i then Nothing else Just i) args

(mapPart $ opKind t)

$ map (typeToSelector Nothing) args)

$ filter ( \ (_, t) -> opRes t == s)

$ map ( \ o -> case o of

Qual_op_name i t _ -> (trI i, toOpType t)

_ -> error "ExtModal2HasCASL.toSentence") ops) sorts

_ -> Formula $ transTop msig f

transFrames :: ExtModalSign -> [Named (FORMULA EM_FORMULA)] -> [Named Sentence]

transFrames sig = foldr (\ nf -> case sentence nf of

ExtFORMULA (ModForm (ModDefn _ _ _ fs _)) ->

(map (\ af -> let l = getRLabel af in

nf { sentence = Formula $ transTop sig (item af)

, senAttr = if null l then senAttr nf else l })

(concatMap (frameForms . item) fs) ++)

_ -> id) []

isFrameAx :: FORMULA EM_FORMULA -> Bool

isFrameAx f = case f of

ExtFORMULA (ModForm _) -> True

_ -> False

data Args = Args

{ sourceW, targetW, targetN :: Term

, nextW, freeC :: Int -- world variables

, freeZ :: Int -- path variable

, boundNoms :: [(Id, Term)]

, modSig :: ExtModalSign

}

startArgs :: ExtModalSign -> Args

startArgs msig = let

vt = varTerm (genNumVar "w" 1) world

in Args

{ sourceW = vt

, targetW = vt

, targetN = zeroT

, nextW = 1

, freeC = 1

, freeZ = 1

, boundNoms = []

, modSig = msig

}

zDecl :: Args -> VarDecl

zDecl as = hcVarDecl (genNumVar "Z" $ freeZ as) $ binPredTy nWorld

transTop :: ExtModalSign -> FORMULA EM_FORMULA -> Term

transTop msig f = let

as = startArgs msig

vs = [hcVarDecl (genNumVar "w" 1) worldTy, zDecl as]

in HC.mkForall (map GenVarDecl vs)

. mkLogTerm implId nr

(pathAppl $ map QualVar vs)

$ transMF as f

getTermOfNom :: Args -> Id -> Term

getTermOfNom as i = fromMaybe (mkNomAppl i) . lookup i $ boundNoms as

mkZPath :: Term -> Term -> Args -> Term

mkZPath v n as = mkApplTerm (QualVar $ zDecl as)

[pairWorld v n, pairWorld (targetW as) $ targetN as]

zPath :: Args -> Term

zPath as = mkZPath (sourceW as) zeroT as

trRecord :: Args -> String -> Record EM_FORMULA Term Term

trRecord as str = let

extInf = extendedInfo $ modSig as

currW = targetW as

andPath = mkLogTerm andId nr $ zPath as

typeTerm hty tr = case getTypeOf tr of

Just t | hty == t -> tr

_ -> TypedTerm tr Inferred hty nr

typeArgs = zipWith (typeTerm . toType)

in (transRecord str)

{ foldPredication = \ _ ps pargs _ -> let

Qual_pred_name pn pTy@(Pred_type srts q) _ = ps

args = typeArgs srts pargs

in andPath

$ typeTerm unitType

$ if MapSet.member pn (toPredType pTy) $ flexPreds extInf

then mkApplTerm

(mkOp (trI pn) . trPrSyn

$ Pred_type (world : srts) q) $ currW : args

else if null srts && Set.member pn (nominals extInf)

then eqW currW $ getTermOfNom as pn

else mkApplTerm

(mkOp (trI pn) $ trPrSyn pTy) args

, foldEquation = \ o t1 e t2 ps ->

let Equation c1 _ _ _ = o in

andPath $ mkEqTerm (if e == Existl then exEq else eqId)

(typeOfTerm c1) ps t1 t2

, foldDefinedness = \ o t ps ->

let Definedness c _ = o in

andPath $ mkTerm defId defType [typeOfTerm c] ps t

, foldExtFORMULA = \ _ f -> transEMF as f

, foldApplication = \ _ os oargs _ -> let

Qual_op_name opn oTy@(Op_type ok srts res q) _ = os

args = typeArgs srts oargs

in typeTerm (toType res)

$ if MapSet.member opn (toOpType oTy) $ flexOps extInf

then mkApplTerm

(mkOp (trI opn) . trOpSyn

$ Op_type ok (world : srts) res q) $ currW : args

else mkApplTerm

(mkOp (trI opn) $ trOpSyn oTy) args

}

transMF :: Args -> FORMULA EM_FORMULA -> Term

transMF a f = foldFormula (trRecord a $ showDoc f "") f

disjointVars :: [VarDecl] -> [Term]

disjointVars vs = case vs of

a : r@(b : _) -> mkNot

(on eqW QualVar a b) : disjointVars r

_ -> []

pathAppl2 :: Term -> VarDecl -> Term

pathAppl2 t v = pathAppl [t, QualVar v]

transEMF :: Args -> EM_FORMULA -> Term

transEMF as emf = let

fW = freeC as

pathAppl3 t = mkLogTerm implId nr . pathAppl2 t

is i = [fW + 1 .. fW + i]

mkVs c ty = map (\ n -> varDecl (genNumVar [c] n) ty) . is

vds = mkVs 'w' world

nds = mkVs 'n' natId

gvs = map GenVarDecl . vds

vt0 = targetW as

nt0 = targetN as

[v1] = vds 1

[n1] = nds 1

[vt1, nt1] = map QualVar [v1, n1]

gvs1 = map GenVarDecl [v1, n1]

mkEqNats = mkEqTerm eqId natTy nr

in case emf of

PrefixForm pf f r -> case pf of

BoxOrDiamond bOp m gEq i -> let

ex = bOp == Diamond

l = is i

gs = gvs i

nAs = as { freeC = fW + i }

tf n = let

vt = varTerm (genNumVar "w" n) world

newAs = nAs { freeZ = n }

zd = zDecl newAs

in HC.mkForall [GenVarDecl zd]

. pathAppl3 vt zd

$ transMF (resetArgs vt newAs) f

tM n = transMod nAs { nextW = n } m

conjF = mkConj $ map tM l ++ map tf l ++ disjointVars (vds i)

diam = BoxOrDiamond Diamond m True

tr b = transEMF as $ PrefixForm (BoxOrDiamond b m gEq i) f r

f1 = QuantifiedTerm HC.Existential gs conjF r

f2 = HC.mkForall gs conjF

in if gEq && i > 0 && (i == 1 || ex) then case bOp of

Diamond -> f1

Box -> f2

EBox -> mkConj [f1, f2]

else if i <= 0 && ex && gEq then unitTerm trueId r

else if bOp == EBox then mkConj $ map tr [Diamond, Box]

else if ex -- lEq

then transMF as . mkNeg . ExtFORMULA $ PrefixForm

(diam $ i + 1) f r

else if gEq -- Box

then transMF as . mkNeg . ExtFORMULA $ PrefixForm

(diam i) (mkNeg f) r

else transMF as . ExtFORMULA $ PrefixForm

(diam $ i + 1) (mkNeg f) r

Hybrid at i -> let ni = simpleIdToId i in

if at then let

ti = getTermOfNom as ni

nAs = as { freeC = fW + 1, freeZ = fW + 1 }

zd = zDecl nAs

in mkConj

[ zPath as, HC.mkForall [GenVarDecl zd]

. pathAppl3 ti zd $ transMF (resetArgs ti as) f ]

else let

vi = varDecl (genNumVar "i" $ fW + 1) world

ti = QualVar vi

in mkExConj vi

[ eqW ti vt0

, transMF as { boundNoms = (ni, ti) : boundNoms as

, targetW = ti

, freeC = fW + 1 } f ]

StateQuantification fut gen -> let

nAs = as { freeC = fW + 1, targetW = vt1, targetN = nt1 }

in mkLogTerm andId r (zPath as)

. (if gen then HC.mkForall else mkExQs) gvs1

. mkLogTerm (if gen then implId else andId) nr

(if fut then mkZPath vt0 nt0 nAs else mkZPath vt1 nt1 as)

$ transMF nAs f

PathQuantification gen -> if gen then let

ws = mkVs 'p' nWorldId 2

[w1, w2] = map QualVar ws

p = pairWorld vt0 nt0

nAs = as { freeC = fW + 2, freeZ = fW + 1 }

zd = zDecl nAs

zt = QualVar zd

z = QualVar $ zDecl as

in mkLogTerm andId r (zPath as)

. HC.mkForall [GenVarDecl zd]

. mkLogTerm implId r

(mkLogTerm andId r (pathAppl2 (sourceW as) zd)

. HC.mkForall gvs1

. mkLogTerm andId r

(mkLogTerm eqvId r

(mkZPath vt1 nt1 as) $ mkZPath vt1 nt1 nAs)

. HC.mkForall (map GenVarDecl ws)

. mkLogTerm implId r

(mkLogTerm andId r

(mkApplTerm z [w1, p])

$ mkApplTerm z [w2, p])

. mkLogTerm eqvId r

(mkApplTerm z [w1, w2])

$ mkApplTerm zt [w1, w2])

$ transMF nAs f

else transMF as . mkNeg . ExtFORMULA $ PrefixForm

(PathQuantification $ not gen) (mkNeg f) r

NextY next -> let

nAs = as { freeC = fW + 1, targetW = vt1 }

in mkLogTerm andId r (zPath as)

. mkExQs (if next then [GenVarDecl v1] else gvs1)

$ if next then let

as2 = nAs { targetN = sucTerm nt0 }

in mkLogTerm andId r (mkZPath vt0 nt0 as2)

$ transMF as2 f

else let

as2 = nAs { targetN = nt1 }

in mkConj

[ mkZPath vt1 nt1 as

, mkEqNats (sucTerm nt1) nt0

, transMF as2 f ]

FixedPoint _ _ -> error $ "transEMF: " ++ showDoc emf ""

UntilSince isUntil f1 f2 r -> let

nAs = as { freeC = fW + 2 }

[_, v2] = vds 2

[_, n2] = nds 2

[vt2, nt2] = map QualVar [v2, n2]

as1 = nAs { targetW = vt1, targetN = nt1 }

as2 = nAs { targetW = vt2, targetN = nt2 }

in mkLogTerm andId r (zPath as)

. mkExQs (map GenVarDecl [v1, n1])

$ mkConj

[ if isUntil then mkZPath vt0 nt0 as1 else mkZPath vt1 nt1 as

, transMF as1 f2

, HC.mkForall (map GenVarDecl [v2, n2])

. mkLogTerm orId r

(mkConj

[ mkLogTerm orId r

(if isUntil then mkZPath vt0 nt0 as2 else mkZPath vt2 nt2 as)

. mkLogTerm andId r (eqW vt0 vt2)

$ mkEqNats nt0 nt2

, if isUntil then mkZPath vt2 nt2 as1 else mkZPath vt1 nt1 as2 ])

$ transMF as2 f1 ]

ModForm md -> mkConj $ transModDefn as md

resetArgs :: Term -> Args -> Args

resetArgs t as = as

{ sourceW = t

, targetW = t

, targetN = zeroT }

transMod :: Args -> MODALITY -> Term

transMod as md = let

t1 = targetW as

t2 = varTerm (genNumVar "w" $ nextW as) world

vts = [t1, t2]

msig = modSig as

extInf = extendedInfo msig

timeMs = timeMods extInf

in case md of

SimpleMod i -> let ri = simpleIdToId i in mkApplTerm

(mkOp (relOfMod (Set.member ri timeMs) False ri)

. trPr $ modPredType world False ri) vts

TermMod t -> case optTermSort t of

Just srt -> case keepMinimals msig id . Set.toList

. Set.intersection (termMods extInf) . Set.insert srt

$ supersortsOf srt msig of

[] -> error $ "transMod1: " ++ showDoc t ""

st : _ -> mkApplTerm

(mkOp (relOfMod (Set.member st timeMs) True st)

. trPr $ modPredType world True st)

$ foldTerm (trRecord (resetArgs t1 as) $ showDoc t "") t : vts

_ -> error $ "transMod2: " ++ showDoc t ""

Guard f -> let

nf = freeC as + 1

newAs = as { freeC = nf, freeZ = nf }

zd = zDecl newAs

in mkConj [eqWorld exEq t1 t2, HC.mkForall [GenVarDecl zd] $ mkConj

[ pathAppl2 t1 zd, transMF (resetArgs t1 newAs) f ]]

ModOp mOp m1 m2 -> case mOp of

Composition -> let

nW = freeC as + 1

nAs = as { freeC = nW }

vd = varDecl (genNumVar "w" nW) world

in mkExConj vd

[ transMod nAs { nextW = nW } m1

, transMod nAs { targetW = QualVar vd } m2 ]

Intersection -> mkConj [transMod as m1, transMod as m2]

Union -> mkDisj [transMod as m1, transMod as m2]

OrElse -> mkDisj $ transOrElse [] as $ flatOrElse md

TransClos m -> transMod as m -- ignore transitivity for now

flatOrElse :: MODALITY -> [MODALITY]

flatOrElse md = case md of

ModOp OrElse m1 m2 -> flatOrElse m1 ++ flatOrElse m2

_ -> [md]

transOrElse :: [FORMULA EM_FORMULA] -> Args -> [MODALITY] -> [Term]

transOrElse nFs as ms = case ms of

[] -> []

md : r -> case md of

Guard f -> transMod as (Guard . conjunct $ f : nFs)

: transOrElse (mkNeg f : nFs) as r

_ -> transMod as md : transOrElse nFs as r

transModDefn :: Args -> ModDefn -> [Term]

transModDefn as (ModDefn _ _ _ fs _) =

concatMap (map (transMF as . item) . frameForms . item) fs