{-# 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 (Int -> ExtModal2HasCASL -> ShowS
[ExtModal2HasCASL] -> ShowS
ExtModal2HasCASL -> String
(Int -> ExtModal2HasCASL -> ShowS)
-> (ExtModal2HasCASL -> String)
-> ([ExtModal2HasCASL] -> ShowS)
-> Show ExtModal2HasCASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExtModal2HasCASL] -> ShowS
$cshowList :: [ExtModal2HasCASL] -> ShowS
show :: ExtModal2HasCASL -> String
$cshow :: ExtModal2HasCASL -> String
showsPrec :: Int -> ExtModal2HasCASL -> ShowS
$cshowsPrec :: Int -> ExtModal2HasCASL -> ShowS
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
sourceLogic ExtModal2HasCASL = ExtModal
ExtModal
    sourceSublogic :: ExtModal2HasCASL -> ExtModalSL
sourceSublogic ExtModal2HasCASL = Sublogic -> ExtModalSL
forall a. a -> CASL_SL a
mkTop Sublogic
maxSublogic
        { hasTransClos :: Bool
hasTransClos = Bool
False
        , hasFixPoints :: Bool
hasFixPoints = Bool
False }
    targetLogic :: ExtModal2HasCASL -> HasCASL
targetLogic ExtModal2HasCASL = HasCASL
HasCASL
    mapSublogic :: ExtModal2HasCASL -> ExtModalSL -> Maybe Sublogic
mapSublogic ExtModal2HasCASL sl :: ExtModalSL
sl = Sublogic -> Maybe Sublogic
forall a. a -> Maybe a
Just Sublogic
HC.caslLogic
      { which_logic :: Formulas
HC.which_logic = Formulas
HOL
      , has_sub :: Bool
HC.has_sub = ExtModalSL -> Bool
forall a. CASL_SL a -> Bool
CASL.has_sub ExtModalSL
sl
      , has_part :: Bool
HC.has_part = ExtModalSL -> Bool
forall a. CASL_SL a -> Bool
CASL.has_part ExtModalSL
sl }
    map_theory :: ExtModal2HasCASL
-> (ExtModalSign, [Named ExtModalFORMULA])
-> Result (Env, [Named Sentence])
map_theory ExtModal2HasCASL (sig :: ExtModalSign
sig, allSens :: [Named ExtModalFORMULA]
allSens) = let
      (frames :: [Named ExtModalFORMULA]
frames, sens :: [Named ExtModalFORMULA]
sens) = (Named ExtModalFORMULA -> Bool)
-> [Named ExtModalFORMULA]
-> ([Named ExtModalFORMULA], [Named ExtModalFORMULA])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (ExtModalFORMULA -> Bool
isFrameAx (ExtModalFORMULA -> Bool)
-> (Named ExtModalFORMULA -> ExtModalFORMULA)
-> Named ExtModalFORMULA
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named ExtModalFORMULA -> ExtModalFORMULA
forall s a. SenAttr s a -> s
sentence) [Named ExtModalFORMULA]
allSens
      in case ExtModalSign -> [Named ExtModalFORMULA] -> (Env, [Named Sentence])
transSig ExtModalSign
sig [Named ExtModalFORMULA]
sens of
      (mme :: Env
mme, s :: [Named Sentence]
s) -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return
        (Env
mme, ((String, DataEntry) -> Named Sentence)
-> [(String, DataEntry)] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: String
n, d :: DataEntry
d) -> String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
n (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ [DataEntry] -> Sentence
DatatypeSen [DataEntry
d])
           [("natural numbers", DataEntry
natType), ("numbered worlds", DataEntry
worldType)]
           [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
s [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ ExtModalSign -> [Named ExtModalFORMULA] -> [Named Sentence]
transFrames ExtModalSign
sig [Named ExtModalFORMULA]
frames
              [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ (Named ExtModalFORMULA -> Named Sentence)
-> [Named ExtModalFORMULA] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map ((ExtModalFORMULA -> Sentence)
-> Named ExtModalFORMULA -> Named Sentence
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((ExtModalFORMULA -> Sentence)
 -> Named ExtModalFORMULA -> Named Sentence)
-> (ExtModalFORMULA -> Sentence)
-> Named ExtModalFORMULA
-> Named Sentence
forall a b. (a -> b) -> a -> b
$ ExtModalSign -> ExtModalFORMULA -> Sentence
toSen ExtModalSign
sig) [Named ExtModalFORMULA]
sens)
    has_model_expansion :: ExtModal2HasCASL -> Bool
has_model_expansion ExtModal2HasCASL = Bool
True
    is_weakly_amalgamable :: ExtModal2HasCASL -> Bool
is_weakly_amalgamable ExtModal2HasCASL = Bool
True

nomName :: Id -> Id
nomName :: Id -> Id
nomName t :: Id
t = [Token] -> [Id] -> Range -> Id
Id [String -> Token
genToken "N"] [Id
t] (Range -> Id) -> Range -> Id
forall a b. (a -> b) -> a -> b
$ Id -> Range
rangeOfId Id
t

nomOpType :: OpType
nomOpType :: OpType
nomOpType = [Id] -> Id -> OpType
mkTotOpType [] Id
world

mkOp :: Id -> Type -> Term
mkOp :: Id -> Type -> Term
mkOp i :: Id
i = Id -> TypeScheme -> Term
mkOpTerm Id
i (TypeScheme -> Term) -> (Type -> TypeScheme) -> Type -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TypeScheme
simpleTypeScheme

mkNomAppl :: Id -> Term
mkNomAppl :: Id -> Term
mkNomAppl pn :: Id
pn = Id -> Type -> Term
mkOp (Id -> Id
nomName Id
pn) (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ OpType -> Type
trOp OpType
nomOpType

eqWorld :: Id -> Term -> Term -> Term
eqWorld :: Id -> Term -> Term -> Term
eqWorld i :: Id
i = Id -> Type -> Range -> Term -> Term -> Term
mkEqTerm Id
i (Id -> Type
toType Id
world) Range
nr

eqW :: Term -> Term -> Term
eqW :: Term -> Term -> Term
eqW = Id -> Term -> Term -> Term
eqWorld Id
eqId

mkNot :: Term -> Term
mkNot :: Term -> Term
mkNot = Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm Id
notId TypeScheme
notType [] Range
nr

mkConj :: [Term] -> Term
mkConj :: [Term] -> Term
mkConj l :: [Term]
l = (if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
l then Id -> Range -> Term
unitTerm Id
trueId else Id -> [Term] -> Range -> Term
toBinJunctor Id
andId [Term]
l) Range
nr

mkDisj :: [Term] -> Term
mkDisj :: [Term] -> Term
mkDisj l :: [Term]
l =
  (if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
l then Id -> Range -> Term
unitTerm Id
falseId else Id -> [Term] -> Range -> Term
toBinJunctor Id
orId [Term]
l) Range
nr

mkExQs :: [GenVarDecl] -> Term -> Term
mkExQs :: [GenVarDecl] -> Term -> Term
mkExQs vs :: [GenVarDecl]
vs t :: Term
t =
  Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
HC.Existential [GenVarDecl]
vs Term
t Range
nr

mkExQ :: VarDecl -> Term -> Term
mkExQ :: VarDecl -> Term -> Term
mkExQ vd :: VarDecl
vd = [GenVarDecl] -> Term -> Term
mkExQs [VarDecl -> GenVarDecl
GenVarDecl VarDecl
vd]

mkExConj :: VarDecl -> [Term] -> Term
mkExConj :: VarDecl -> [Term] -> Term
mkExConj vd :: VarDecl
vd = VarDecl -> Term -> Term
mkExQ VarDecl
vd (Term -> Term) -> ([Term] -> Term) -> [Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> Term
mkConj

tauS :: String
tauS :: String
tauS = "tau"

tauId :: Id
tauId :: Id
tauId = String -> Id
genName String
tauS

tauCaslTy :: PredType
tauCaslTy :: PredType
tauCaslTy = [Id] -> PredType
PredType [Id
world, Id
world]

tauTy :: Type
tauTy :: Type
tauTy = PRED_TYPE -> Type
trPrSyn (PRED_TYPE -> Type) -> PRED_TYPE -> Type
forall a b. (a -> b) -> a -> b
$ PredType -> PRED_TYPE
toPRED_TYPE PredType
tauCaslTy

{- | we now consider numbered worlds:
     free type WN ::= mkWN World Nat -}
nWorldId :: SORT
nWorldId :: Id
nWorldId = String -> Id
genName "WN"

mkNWorldId :: Id
mkNWorldId :: Id
mkNWorldId = String -> Id
genName "mkWN"

nWorld :: Type
nWorld :: Type
nWorld = Id -> Type
toType Id
nWorldId

binPredTy :: Type -> Type
binPredTy :: Type -> Type
binPredTy = Type -> Partiality -> [Type] -> Type
getFunType Type
unitType Partiality
HC.Partial ([Type] -> Type) -> (Type -> [Type]) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Type -> [Type]
forall a. Int -> a -> [a]
replicate 2

isTransS :: String
isTransS :: String
isTransS = "isTrans"

isTransId :: Id
isTransId :: Id
isTransId = String -> Id
genName String
isTransS

prOfBinPrTy :: Type -> Type
prOfBinPrTy :: Type -> Type
prOfBinPrTy = Range -> Type -> Type
predType Range
nr (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
binPredTy

prOfNwPrTy :: Type
prOfNwPrTy :: Type
prOfNwPrTy = Type -> Type
prOfBinPrTy Type
nWorld

containsS :: String
containsS :: String
containsS = "contains"

containsId :: Id
containsId :: Id
containsId = String -> Id
genName String
containsS

transTy :: Type -> Type
transTy :: Type -> Type
transTy = Type -> Partiality -> [Type] -> Type
getFunType Type
unitType Partiality
HC.Partial ([Type] -> Type) -> (Type -> [Type]) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Type -> [Type]
forall a. Int -> a -> [a]
replicate 2 (Type -> [Type]) -> (Type -> Type) -> Type -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
binPredTy

-- | mixfix names work for tuples and are lost after currying
trI :: Id -> Id
trI :: Id -> Id
trI i :: Id
i = if Id -> Bool
isMixfix Id
i then [Token] -> [Id] -> Range -> Id
Id [String -> Token
genToken "C"] [Id
i] (Range -> Id) -> Range -> Id
forall a b. (a -> b) -> a -> b
$ Id -> Range
rangeOfId Id
i else Id
i

trOpSyn :: OP_TYPE -> Type
trOpSyn :: OP_TYPE -> Type
trOpSyn (Op_type ok :: OpKind
ok args :: [Id]
args res :: Id
res _) = let
  (partial :: Partiality
partial, total :: Bool
total) = case OpKind
ok of
    CASL.Total -> (Partiality
HC.Total, Bool
True)
    CASL.Partial -> (Partiality
HC.Partial, Bool
False)
  resTy :: Type
resTy = Id -> Type
toType Id
res
  in if [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
args then if Bool
total then Type
resTy else Type -> Type
mkLazyType Type
resTy
  else Type -> Partiality -> [Type] -> Type
getFunType Type
resTy Partiality
partial ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
toType [Id]
args

trOp :: OpType -> Type
trOp :: OpType -> Type
trOp = OP_TYPE -> Type
trOpSyn (OP_TYPE -> Type) -> (OpType -> OP_TYPE) -> OpType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> OP_TYPE
toOP_TYPE

trPrSyn :: PRED_TYPE -> Type
trPrSyn :: PRED_TYPE -> Type
trPrSyn (Pred_type args :: [Id]
args ps :: Range
ps) = let u :: Type
u = Range -> Type
unitTypeWithRange Range
ps in
   if [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
args then Type -> Type
mkLazyType Type
u else
   Type -> Partiality -> [Type] -> Type
getFunType Type
u Partiality
HC.Partial ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
toType [Id]
args

trPr :: PredType -> Type
trPr :: PredType -> Type
trPr = PRED_TYPE -> Type
trPrSyn (PRED_TYPE -> Type) -> (PredType -> PRED_TYPE) -> PredType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> PRED_TYPE
toPRED_TYPE

-- | add world arguments to flexible ops and preds; and add relations
transSig :: ExtModalSign -> [Named (FORMULA EM_FORMULA)]
  -> (Env, [Named Sentence])
transSig :: ExtModalSign -> [Named ExtModalFORMULA] -> (Env, [Named Sentence])
transSig sign :: ExtModalSign
sign sens :: [Named ExtModalFORMULA]
sens = let
    s1 :: Sign f ()
s1 = () -> ExtModalSign -> Sign f ()
forall e f1 e1 f. e -> Sign f1 e1 -> Sign f e
embedSign () ExtModalSign
sign
    extInf :: EModalSign
extInf = ExtModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo ExtModalSign
sign
    flexibleOps :: OpMap
flexibleOps = EModalSign -> OpMap
flexOps EModalSign
extInf
    flexiblePreds :: PredMap
flexiblePreds = EModalSign -> PredMap
flexPreds EModalSign
extInf
    flexOps' :: OpMap
flexOps' = Id -> (Id -> Id) -> OpMap -> OpMap
addWorldOp Id
world Id -> Id
forall a. a -> a
id OpMap
flexibleOps
    flexPreds' :: PredMap
flexPreds' = Id -> (Id -> Id) -> PredMap -> PredMap
addWorldPred Id
world Id -> Id
forall a. a -> a
id PredMap
flexiblePreds
    rigOps' :: OpMap
rigOps' = OpMap -> OpMap -> OpMap
diffOpMapSet (ExtModalSign -> OpMap
forall f e. Sign f e -> OpMap
opMap ExtModalSign
sign) OpMap
flexibleOps
    rigPreds' :: PredMap
rigPreds' = PredMap -> PredMap -> PredMap
diffMapSet (ExtModalSign -> PredMap
forall f e. Sign f e -> PredMap
predMap ExtModalSign
sign) PredMap
flexiblePreds
    noms :: Set Id
noms = EModalSign -> Set Id
nominals EModalSign
extInf
    noNomsPreds :: PredMap
noNomsPreds = (Id -> PredMap -> PredMap) -> PredMap -> Set Id -> PredMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Id -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
`MapSet.delete` PredType
nomPType) PredMap
rigPreds' Set Id
noms
    termMs :: Set Id
termMs = EModalSign -> Set Id
termMods EModalSign
extInf
    timeMs :: Set Id
timeMs = EModalSign -> Set Id
timeMods EModalSign
extInf
    rels :: PredMap
rels = (Id -> PredMap -> PredMap) -> PredMap -> Set Id -> PredMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ m :: Id
m ->
      Id -> Bool -> Bool -> Id -> PredMap -> PredMap
insertModPred Id
world (Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
m Set Id
timeMs) (Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
m Set Id
termMs) Id
m)
      PredMap
forall a b. MapSet a b
MapSet.empty (Set Id -> PredMap) -> Set Id -> PredMap
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
modalities EModalSign
extInf
    nomOps :: OpMap
nomOps = (Id -> OpMap -> OpMap) -> OpMap -> Set Id -> OpMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ n :: Id
n -> Id -> OpType -> OpMap -> OpMap
addOpTo (Id -> Id
nomName Id
n) OpType
nomOpType) OpMap
rigOps' Set Id
noms
    s2 :: Sign f ()
s2 = Sign f ()
forall f. Sign f ()
s1
      { sortRel :: Rel Id
sortRel = Id -> Rel Id -> Rel Id
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey Id
world (Rel Id -> Rel Id) -> Rel Id -> Rel Id
forall a b. (a -> b) -> a -> b
$ ExtModalSign -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel ExtModalSign
sign
      , opMap :: OpMap
opMap = OpMap -> OpMap -> OpMap
addOpMapSet OpMap
flexOps' OpMap
nomOps
      , predMap :: PredMap
predMap = PredMap -> PredMap -> PredMap
addMapSet PredMap
rels (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ PredMap -> PredMap -> PredMap
addMapSet PredMap
flexPreds' PredMap
noNomsPreds
      }
    env :: Env
env = (Id -> Id)
-> (OpType -> Type)
-> (PredType -> Type)
-> Set (Id, OpType)
-> Sign Any ()
-> Env
forall f e.
(Id -> Id)
-> (OpType -> Type)
-> (PredType -> Type)
-> Set (Id, OpType)
-> Sign f e
-> Env
mapSigAux Id -> Id
trI OpType -> Type
trOp PredType -> Type
trPr ([Named ExtModalFORMULA] -> Set (Id, OpType)
forall f. [Named (FORMULA f)] -> Set (Id, OpType)
getConstructors [Named ExtModalFORMULA]
sens) Sign Any ()
forall f. Sign f ()
s2
    mkOpInfo :: Type -> OpDefn -> Set OpInfo
mkOpInfo t :: Type
t = OpInfo -> Set OpInfo
forall a. a -> Set a
Set.singleton (OpInfo -> Set OpInfo)
-> (OpDefn -> OpInfo) -> OpDefn -> Set OpInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeScheme -> Set OpAttr -> OpDefn -> OpInfo
OpInfo (Type -> TypeScheme
simpleTypeScheme Type
t) Set OpAttr
forall a. Set a
Set.empty
    insOpInfo :: Id -> Set OpInfo -> Map Id (Set OpInfo) -> Map Id (Set OpInfo)
insOpInfo = (Set OpInfo -> Set OpInfo -> Set OpInfo)
-> Id -> Set OpInfo -> Map Id (Set OpInfo) -> Map Id (Set OpInfo)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set OpInfo -> Set OpInfo -> Set OpInfo
forall a. Ord a => Set a -> Set a -> Set a
Set.union
    insF :: (Id, Type) -> Map Id (Set OpInfo) -> Map Id (Set OpInfo)
insF (i :: Id
i, t :: Type
t) = Id -> Set OpInfo -> Map Id (Set OpInfo) -> Map Id (Set OpInfo)
insOpInfo Id
i (Set OpInfo -> Map Id (Set OpInfo) -> Map Id (Set OpInfo))
-> (OpDefn -> Set OpInfo)
-> OpDefn
-> Map Id (Set OpInfo)
-> Map Id (Set OpInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> OpDefn -> Set OpInfo
mkOpInfo Type
t (OpDefn -> Map Id (Set OpInfo) -> Map Id (Set OpInfo))
-> OpDefn -> Map Id (Set OpInfo) -> Map Id (Set OpInfo)
forall a b. (a -> b) -> a -> b
$ OpBrand -> OpDefn
NoOpDefn OpBrand
Fun
    in ( Env
env
         { assumps :: Map Id (Set OpInfo)
assumps = ((Id, Set OpInfo) -> Map Id (Set OpInfo) -> Map Id (Set OpInfo))
-> Map Id (Set OpInfo) -> [(Id, Set OpInfo)] -> Map Id (Set OpInfo)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Id -> Set OpInfo -> Map Id (Set OpInfo) -> Map Id (Set OpInfo))
-> (Id, Set OpInfo) -> Map Id (Set OpInfo) -> Map Id (Set OpInfo)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Id -> Set OpInfo -> Map Id (Set OpInfo) -> Map Id (Set OpInfo)
insOpInfo)
             (((Id, Type) -> Map Id (Set OpInfo) -> Map Id (Set OpInfo))
-> Map Id (Set OpInfo) -> [(Id, Type)] -> Map Id (Set OpInfo)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Id, Type) -> Map Id (Set OpInfo) -> Map Id (Set OpInfo)
insF (Env -> Map Id (Set OpInfo)
assumps Env
env)
             [ (Id
tauId, Type
tauTy)
             , (Id
isTransId, Type
prOfNwPrTy)
             , (Id
reflexId, Type
prOfNwPrTy)
             , (Id
irreflexId, Type
prOfNwPrTy)
             , (Id
containsId, Type -> Type
transTy Type
nWorld)
             , (Id
transId, Type -> Type
transTy Type
nWorld)
             , (Id
transReflexId, Type -> Type
transTy Type
nWorld)
             , (Id
transLinearOrderId, Type
prOfNwPrTy)
             , (Id
hasSuccessorId, Type
hasSuccessorTy)
             , (Id
subsetOfTauId, Type
prOfNwPrTy)
             , (Id
hasTauSucId, Type
prOfNwPrTy)
             , (Id
superpathId, Type
hasSuccessorTy)
             , (Id
pathId, Type
hasSuccessorTy)
             ])
             [ Id -> AltDefn -> (Id, Set OpInfo)
altToOpInfo Id
natId AltDefn
zeroAlt
             , Id -> AltDefn -> (Id, Set OpInfo)
altToOpInfo Id
natId AltDefn
sucAlt
             , Id -> AltDefn -> (Id, Set OpInfo)
altToOpInfo Id
nWorldId AltDefn
worldAlt
             , [Selector] -> (Id, Set OpInfo)
selWorldInfo [Selector]
getWorldSel
             , [Selector] -> (Id, Set OpInfo)
selWorldInfo [Selector]
numSel
             ]
         , typeMap :: TypeMap
typeMap = Id -> TypeInfo -> TypeMap -> TypeMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
nWorldId TypeInfo
starTypeInfo
                       { typeDefn :: TypeDefn
typeDefn = DataEntry -> TypeDefn
DatatypeDefn DataEntry
worldType }
                     (TypeMap -> TypeMap) -> (TypeMap -> TypeMap) -> TypeMap -> TypeMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> TypeInfo -> TypeMap -> TypeMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
natId TypeInfo
starTypeInfo
                       { typeDefn :: TypeDefn
typeDefn = DataEntry -> TypeDefn
DatatypeDefn DataEntry
natType }
                     (TypeMap -> TypeMap) -> TypeMap -> TypeMap
forall a b. (a -> b) -> a -> b
$ Env -> TypeMap
typeMap Env
env
         }
       , String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "nat_induction" (Term -> Sentence
Formula (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ [DataEntry] -> Term
inductionScheme [DataEntry
natType])
         Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: DataPat -> [AltDefn] -> [Named Sentence]
makeDataSelEqs (DataEntry -> DataPat
toDataPat DataEntry
worldType) [AltDefn
worldAlt]
         [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ ((String, Term) -> Named Sentence)
-> [(String, Term)] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, t :: Term
t) -> String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
s (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
Formula Term
t)
         [ (String
tauS, Set Id -> [Id] -> Term
tauDef Set Id
termMs ([Id] -> Term) -> [Id] -> Term
forall a b. (a -> b) -> a -> b
$ Set Id -> [Id]
forall a. Set a -> [a]
Set.toList Set Id
timeMs)
         , (String
isTransS, Type -> Term
isTransDef Type
nWorld)
         , (String
reflexS, Bool -> Type -> Term
reflexDef Bool
True Type
nWorld)
         , (String
irreflexS, Bool -> Type -> Term
reflexDef Bool
False Type
nWorld)
         , (String
containsS, Type -> Term
containsDef Type
nWorld)
         , (String
transS, Id -> (Term -> Term -> Term) -> Type -> Term
someDef Id
transId (Type -> Term -> Term -> Term
transContainsDef Type
nWorld) Type
nWorld)
         , (String
transReflexS, Id -> (Term -> Term -> Term) -> Type -> Term
someDef Id
transReflexId
                        (Type -> Term -> Term -> Term
transReflexContainsDef Type
nWorld) Type
nWorld)
         , (String
transLinearOrderS, Type -> Term
transLinearOrderDef Type
nWorld)
         , (String
hasSuccessorS, Term
hasSuccessorDef)
         , (String
subsetOfTauS, Term
subsetOfTauDef)
         , (String
hasTauSucS, Term
hasTauSucDefAny)
         , (String
superpathS, Term
superpathDef)
         , (String
pathS, Term
pathDef)
         ]
       )

vQuad :: Type -> [VarDecl]
vQuad :: Type -> [VarDecl]
vQuad w :: Type
w = (Int -> VarDecl) -> [Int] -> [VarDecl]
forall a b. (a -> b) -> [a] -> [b]
map (\ n :: Int
n -> Token -> Type -> VarDecl
hcVarDecl (String -> Int -> Token
genNumVar "v" Int
n) Type
w) [1, 2, 3, 4]

quadDs :: Type -> [GenVarDecl]
quadDs :: Type -> [GenVarDecl]
quadDs = (VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl ([VarDecl] -> [GenVarDecl])
-> (Type -> [VarDecl]) -> Type -> [GenVarDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [VarDecl]
vQuad

tripDs :: Type -> [GenVarDecl]
tripDs :: Type -> [GenVarDecl]
tripDs = Int -> [GenVarDecl] -> [GenVarDecl]
forall a. Int -> [a] -> [a]
take 3 ([GenVarDecl] -> [GenVarDecl])
-> (Type -> [GenVarDecl]) -> Type -> [GenVarDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [GenVarDecl]
quadDs

pairDs :: Type -> [GenVarDecl]
pairDs :: Type -> [GenVarDecl]
pairDs = Int -> [GenVarDecl] -> [GenVarDecl]
forall a. Int -> [a] -> [a]
take 2 ([GenVarDecl] -> [GenVarDecl])
-> (Type -> [GenVarDecl]) -> Type -> [GenVarDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [GenVarDecl]
tripDs

tQuad :: Type -> [Term]
tQuad :: Type -> [Term]
tQuad = (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar ([VarDecl] -> [Term]) -> (Type -> [VarDecl]) -> Type -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [VarDecl]
vQuad

tTrip :: Type -> [Term]
tTrip :: Type -> [Term]
tTrip = Int -> [Term] -> [Term]
forall a. Int -> [a] -> [a]
take 3 ([Term] -> [Term]) -> (Type -> [Term]) -> Type -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Term]
tQuad

tPair :: Type -> [Term]
tPair :: Type -> [Term]
tPair = Int -> [Term] -> [Term]
forall a. Int -> [a] -> [a]
take 2 ([Term] -> [Term]) -> (Type -> [Term]) -> Type -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Term]
tTrip

nr :: Range
nr :: Range
nr = Range
nullRange

worldTy :: Type
worldTy :: Type
worldTy = Id -> Type
toType Id
world

tauDef :: Set.Set Id -> [Id] -> Term
tauDef :: Set Id -> [Id] -> Term
tauDef termMs :: Set Id
termMs timeMs :: [Id]
timeMs = let ts :: [Term]
ts = Type -> [Term]
tPair Type
worldTy in
         [GenVarDecl] -> Term -> Term
HC.mkForall (Type -> [GenVarDecl]
pairDs Type
worldTy)
           (Term -> Term) -> ([Term] -> Term) -> [Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
nr
           (Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
tauId Type
tauTy) [Term]
ts)
           (Term -> Term) -> ([Term] -> Term) -> [Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> Term
mkDisj
           ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ (Id -> Term) -> [Id] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\ tm :: Id
tm ->
            let v :: VarDecl
v = Token -> Id -> VarDecl
varDecl (String -> Token
genToken "t") Id
tm
                term :: Bool
term = Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
tm Set Id
termMs
            in (if Bool
term then VarDecl -> Term -> Term
mkExQ VarDecl
v else Term -> Term
forall a. a -> a
id) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm
               (Id -> Type -> Term
mkOp (Bool -> Bool -> Id -> Id
relOfMod Bool
True Bool
term Id
tm)
                (Type -> Term) -> (PredType -> Type) -> PredType -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> Type
trPr (PredType -> Term) -> PredType -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Bool -> Id -> PredType
modPredType Id
world Bool
term Id
tm)
               ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ if Bool
term then VarDecl -> Term
QualVar VarDecl
v Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
ts else [Term]
ts)
           [Id]
timeMs

pVar :: Type -> VarDecl
pVar :: Type -> VarDecl
pVar = Token -> Type -> VarDecl
hcVarDecl (String -> Token
genToken "P") (Type -> VarDecl) -> (Type -> Type) -> Type -> VarDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
binPredTy

isTransDef :: Type -> Term
isTransDef :: Type -> Term
isTransDef w :: Type
w = let
  p :: VarDecl
p = Type -> VarDecl
pVar Type
w
  pt :: Term
pt = VarDecl -> Term
QualVar VarDecl
p
  [t1 :: Term
t1, t2 :: Term
t2, t3 :: Term
t3] = Type -> [Term]
tTrip Type
w
  in [GenVarDecl] -> Term -> Term
HC.mkForall [VarDecl -> GenVarDecl
GenVarDecl VarDecl
p]
         (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
nr
             (Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
isTransId (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
prOfBinPrTy Type
w) [Term
pt])
             (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenVarDecl] -> Term -> Term
HC.mkForall (Type -> [GenVarDecl]
tripDs Type
w)
             (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nr
               (Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
nr
                (Term -> [Term] -> Term
mkApplTerm Term
pt [Term
t1, Term
t2])
                (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm Term
pt [Term
t2, Term
t3])
             (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm Term
pt [Term
t1, Term
t3]

trichotomyDef :: Type -> Term -> Term -> Term -> Term
trichotomyDef :: Type -> Term -> Term -> Term -> Term
trichotomyDef w :: Type
w pt :: Term
pt t1 :: Term
t1 t2 :: Term
t2 = Id -> Range -> Term -> Term -> Term
mkLogTerm Id
orId Range
nr
         (Term -> Term -> Term -> Term
dichotomyDef Term
pt Term
t1 Term
t2)
         (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Type -> Range -> Term -> Term -> Term
mkEqTerm Id
eqId Type
w Range
nr Term
t1 Term
t2

dichotomyDef :: Term -> Term -> Term -> Term
dichotomyDef :: Term -> Term -> Term -> Term
dichotomyDef pt :: Term
pt t1 :: Term
t1 t2 :: Term
t2 = Id -> Range -> Term -> Term -> Term
mkLogTerm Id
orId Range
nr
         (Term -> [Term] -> Term
mkApplTerm Term
pt [Term
t1, Term
t2])
         (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm Term
pt [Term
t2, Term
t1]

linearOrderDef :: Type -> Term -> Term
linearOrderDef :: Type -> Term -> Term
linearOrderDef w :: Type
w pt :: Term
pt = let
  [t1 :: Term
t1, t2 :: Term
t2, t3 :: Term
t3, t4 :: Term
t4] = Type -> [Term]
tQuad Type
w
  in [GenVarDecl] -> Term -> Term
HC.mkForall (Type -> [GenVarDecl]
pairDs Type
w)
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nr
       ([GenVarDecl] -> Term -> Term
mkExQs (Int -> [GenVarDecl] -> [GenVarDecl]
forall a. Int -> [a] -> [a]
drop 2 ([GenVarDecl] -> [GenVarDecl]) -> [GenVarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> a -> b
$ Type -> [GenVarDecl]
quadDs Type
w)
        (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
nr
          (Term -> Term -> Term -> Term
dichotomyDef Term
pt Term
t1 Term
t3)
          (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term -> Term
dichotomyDef Term
pt Term
t2 Term
t4)
       (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> Term -> Term
trichotomyDef Type
w Term
pt Term
t1 Term
t2

transLinearOrderS :: String
transLinearOrderS :: String
transLinearOrderS = "trans_linear_order"

transLinearOrderId :: Id
transLinearOrderId :: Id
transLinearOrderId = String -> Id
genName String
transLinearOrderS

transLinearOrderDef :: Type -> Term
transLinearOrderDef :: Type -> Term
transLinearOrderDef w :: Type
w = let
  ps :: [VarDecl]
ps = Type -> [VarDecl]
rAndQ Type
w
  [pv :: GenVarDecl
pv, qv :: GenVarDecl
qv] = (VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl]
ps
  ts :: [Term]
ts@[pt :: Term
pt, qt :: Term
qt] = (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl]
ps
  in [GenVarDecl] -> Term -> Term
HC.mkForall [GenVarDecl
pv]
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
nr
       (Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
transLinearOrderId (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
prOfBinPrTy Type
w) [Term
pt])
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenVarDecl] -> Term -> Term
mkExQs [GenVarDecl
qv]
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
nr
       (Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
transId (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
transTy Type
w) [Term]
ts)
     (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term
linearOrderDef Type
w Term
qt

natId :: SORT
natId :: Id
natId = String -> Id
stringToId "Nat"

natTy :: Type
natTy :: Type
natTy = Id -> Type
toType Id
natId

sucId :: Id
sucId :: Id
sucId = String -> Id
stringToId "suc"

zero :: Id
zero :: Id
zero = String -> Id
stringToId "0"

natType :: DataEntry
natType :: DataEntry
natType =
  IdMap
-> Id
-> GenKind
-> [TypeArg]
-> RawKind
-> Set AltDefn
-> DataEntry
DataEntry IdMap
forall k a. Map k a
Map.empty Id
natId GenKind
Free [] RawKind
rStar
  (Set AltDefn -> DataEntry) -> Set AltDefn -> DataEntry
forall a b. (a -> b) -> a -> b
$ [AltDefn] -> Set AltDefn
forall a. Ord a => [a] -> Set a
Set.fromList [AltDefn
zeroAlt, AltDefn
sucAlt]

zeroAlt :: AltDefn
zeroAlt :: AltDefn
zeroAlt = Maybe Id -> [Type] -> Partiality -> [[Selector]] -> AltDefn
Construct (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
zero) [] Partiality
HC.Total []

sucAlt :: AltDefn
sucAlt :: AltDefn
sucAlt = Maybe Id -> [Type] -> Partiality -> [[Selector]] -> AltDefn
Construct (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
sucId) [Type
natTy] Partiality
HC.Total [Maybe Id -> Type -> [Selector]
typeToSelector Maybe Id
forall a. Maybe a
Nothing Type
natTy]

altToTy :: Id -> AltDefn -> Type
altToTy :: Id -> AltDefn -> Type
altToTy i :: Id
i (Construct _ ts :: [Type]
ts p :: Partiality
p _) = Type -> Partiality -> [Type] -> Type
getFunType (Id -> Type
toType Id
i) Partiality
p [Type]
ts

altToOpInfo :: Id -> AltDefn -> (Id, Set.Set OpInfo)
altToOpInfo :: Id -> AltDefn -> (Id, Set OpInfo)
altToOpInfo i :: Id
i c :: AltDefn
c@(Construct m :: Maybe Id
m _ _ _) = let Just n :: Id
n = Maybe Id
m in
    (Id
n, OpInfo -> Set OpInfo
forall a. a -> Set a
Set.singleton (OpInfo -> Set OpInfo)
-> (OpDefn -> OpInfo) -> OpDefn -> Set OpInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      TypeScheme -> Set OpAttr -> OpDefn -> OpInfo
OpInfo (Type -> TypeScheme
simpleTypeScheme (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Id -> AltDefn -> Type
altToTy Id
i AltDefn
c) Set OpAttr
forall a. Set a
Set.empty
    (OpDefn -> Set OpInfo) -> OpDefn -> Set OpInfo
forall a b. (a -> b) -> a -> b
$ Id -> OpDefn
ConstructData Id
i)

getWorldId :: Id
getWorldId :: Id
getWorldId = String -> Id
genName "getWorld"

numId :: Id
numId :: Id
numId = String -> Id
genName "num"

worldType :: DataEntry
worldType :: DataEntry
worldType = IdMap
-> Id
-> GenKind
-> [TypeArg]
-> RawKind
-> Set AltDefn
-> DataEntry
DataEntry IdMap
forall k a. Map k a
Map.empty Id
nWorldId GenKind
Free [] RawKind
rStar (Set AltDefn -> DataEntry) -> Set AltDefn -> DataEntry
forall a b. (a -> b) -> a -> b
$ AltDefn -> Set AltDefn
forall a. a -> Set a
Set.singleton AltDefn
worldAlt

worldAlt :: AltDefn
worldAlt :: AltDefn
worldAlt = Maybe Id -> [Type] -> Partiality -> [[Selector]] -> AltDefn
Construct (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
mkNWorldId) [Type
worldTy, Type
natTy] Partiality
HC.Total
    [[Selector]
getWorldSel, [Selector]
numSel]

getWorldSel :: [Selector]
getWorldSel :: [Selector]
getWorldSel = Maybe Id -> Type -> [Selector]
typeToSelector (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
getWorldId) Type
worldTy

numSel :: [Selector]
numSel :: [Selector]
numSel = Maybe Id -> Type -> [Selector]
typeToSelector (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
numId) Type
natTy

nWorldTy :: Type
nWorldTy :: Type
nWorldTy = Id -> AltDefn -> Type
altToTy Id
nWorldId AltDefn
worldAlt

selWorldInfo :: [Selector] -> (Id, Set.Set OpInfo)
selWorldInfo :: [Selector] -> (Id, Set OpInfo)
selWorldInfo = Id -> Set ConstrInfo -> [Selector] -> (Id, Set OpInfo)
selToOpInfo Id
nWorldId (Set ConstrInfo -> [Selector] -> (Id, Set OpInfo))
-> (TypeScheme -> Set ConstrInfo)
-> TypeScheme
-> [Selector]
-> (Id, Set OpInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstrInfo -> Set ConstrInfo
forall a. a -> Set a
Set.singleton (ConstrInfo -> Set ConstrInfo)
-> (TypeScheme -> ConstrInfo) -> TypeScheme -> Set ConstrInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> TypeScheme -> ConstrInfo
ConstrInfo Id
mkNWorldId
  (TypeScheme -> [Selector] -> (Id, Set OpInfo))
-> TypeScheme -> [Selector] -> (Id, Set OpInfo)
forall a b. (a -> b) -> a -> b
$ Type -> TypeScheme
simpleTypeScheme Type
nWorldTy

selToTy :: Id -> [Selector] -> (Id, Type)
selToTy :: Id -> [Selector] -> (Id, Type)
selToTy i :: Id
i s :: [Selector]
s = let [Select (Just n :: Id
n) t :: Type
t p :: Partiality
p] = [Selector]
s in
  (Id
n, Type -> Partiality -> [Type] -> Type
getFunType Type
t Partiality
p [Id -> Type
toType Id
i])

selToOpInfo :: Id -> Set.Set ConstrInfo -> [Selector] -> (Id, Set.Set OpInfo)
selToOpInfo :: Id -> Set ConstrInfo -> [Selector] -> (Id, Set OpInfo)
selToOpInfo i :: Id
i c :: Set ConstrInfo
c s :: [Selector]
s = let (n :: Id
n, ty :: Type
ty) = Id -> [Selector] -> (Id, Type)
selToTy Id
i [Selector]
s in
  (Id
n, OpInfo -> Set OpInfo
forall a. a -> Set a
Set.singleton (OpInfo -> Set OpInfo)
-> (OpDefn -> OpInfo) -> OpDefn -> Set OpInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeScheme -> Set OpAttr -> OpDefn -> OpInfo
OpInfo (Type -> TypeScheme
simpleTypeScheme Type
ty) Set OpAttr
forall a. Set a
Set.empty
      (OpDefn -> Set OpInfo) -> OpDefn -> Set OpInfo
forall a b. (a -> b) -> a -> b
$ Set ConstrInfo -> Id -> OpDefn
SelectData Set ConstrInfo
c Id
i)

rAndQ :: Type -> [VarDecl]
rAndQ :: Type -> [VarDecl]
rAndQ w :: Type
w = (Char -> VarDecl) -> String -> [VarDecl]
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Char
c -> Token -> Type -> VarDecl
hcVarDecl (String -> Token
genToken [Char
c]) (Type -> VarDecl) -> Type -> VarDecl
forall a b. (a -> b) -> a -> b
$ Type -> Type
binPredTy Type
w) "RQ"

containsDef :: Type -> Term
containsDef :: Type -> Term
containsDef w :: Type
w = let -- q contains r
  ps :: [VarDecl]
ps = Type -> [VarDecl]
rAndQ Type
w
  ts :: [Term]
ts@[pt :: Term
pt, qt :: Term
qt] = (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl]
ps
  in [GenVarDecl] -> Term -> Term
HC.mkForall ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl]
ps)
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
nr
       (Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
containsId (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
transTy Type
w) [Term]
ts)
     (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Bool -> Id -> Term -> Term -> Type -> Term
containsDefAux Bool
False Id
implId Term
pt Term
qt Type
w

containsDefAux :: Bool -> Id -> Term -> Term -> Type -> Term
containsDefAux :: Bool -> Id -> Term -> Term -> Type -> Term
containsDefAux neg :: Bool
neg op :: Id
op pt :: Term
pt qt :: Term
qt w :: Type
w = let ts :: [Term]
ts = Type -> [Term]
tPair Type
w in
  [GenVarDecl] -> Term -> Term
HC.mkForall (Type -> [GenVarDecl]
pairDs Type
w) (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if Bool
neg then Term -> Term
mkNot else Term -> Term
forall a. a -> a
id)
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
op Range
nr (Term -> [Term] -> Term
mkApplTerm Term
pt [Term]
ts) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm Term
qt [Term]
ts

someContainsDef :: (Term -> Term) -> Type -> Term -> Term -> Term
someContainsDef :: (Term -> Term) -> Type -> Term -> Term -> Term
someContainsDef sPred :: Term -> Term
sPred w :: Type
w pt :: Term
pt qt :: Term
qt = let -- q fulfills sPred and contains r
  ts :: [Term]
ts = [Term
pt, Term
qt]
  in Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
nr (Term -> Term
sPred Term
qt)
       (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
containsId (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
transTy Type
w) [Term]
ts

transContainsDef :: Type -> Term -> Term -> Term
transContainsDef :: Type -> Term -> Term -> Term
transContainsDef w :: Type
w = (Term -> Term) -> Type -> Term -> Term -> Term
someContainsDef
  (\ qt :: Term
qt -> Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
isTransId (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
prOfBinPrTy Type
w) [Term
qt]) Type
w

transReflexContainsDef :: Type -> Term -> Term -> Term
transReflexContainsDef :: Type -> Term -> Term -> Term
transReflexContainsDef w :: Type
w = (Term -> Term) -> Type -> Term -> Term -> Term
someContainsDef
  (\ qt :: Term
qt -> Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
nr
           (Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
isTransId (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
prOfBinPrTy Type
w) [Term
qt])
           (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
reflexId (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
prOfBinPrTy Type
w) [Term
qt]) Type
w

transS :: String
transS :: String
transS = "trans"

transId :: Id
transId :: Id
transId = String -> Id
genName String
transS

transReflexS :: String
transReflexS :: String
transReflexS = "trans_reflex"

transReflexId :: Id
transReflexId :: Id
transReflexId = String -> Id
genName String
transReflexS

someDef :: Id -> (Term -> Term -> Term) -> Type -> Term
someDef :: Id -> (Term -> Term -> Term) -> Type -> Term
someDef dId :: Id
dId op :: Term -> Term -> Term
op w :: Type
w = let -- q is the (smallest) something containing r
  ps :: [VarDecl]
ps = Type -> [VarDecl]
rAndQ Type
w
  ts :: [Term]
ts@[pt :: Term
pt, qt :: Term
qt] = (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl]
ps
  z :: VarDecl
z = Type -> VarDecl
pVar Type
w
  zt :: Term
zt = VarDecl -> Term
QualVar VarDecl
z
  in [GenVarDecl] -> Term -> Term
HC.mkForall ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl]
ps)
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
nr
       (Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
dId (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
transTy Type
w) [Term]
ts)
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
nr (Term -> Term -> Term
op Term
pt Term
qt)
       (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenVarDecl] -> Term -> Term
HC.mkForall [VarDecl -> GenVarDecl
GenVarDecl VarDecl
z]
       (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nr (Term -> Term -> Term
op Term
pt Term
zt)
         (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
containsId (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
transTy Type
w) [Term
qt, Term
zt]

reflexS :: String
reflexS :: String
reflexS = "reflex"

irreflexS :: String
irreflexS :: String
irreflexS = "irreflex"

reflexId :: Id
reflexId :: Id
reflexId = String -> Id
genName String
reflexS

irreflexId :: Id
irreflexId :: Id
irreflexId = String -> Id
genName String
irreflexS

reflexDef :: Bool -> Type -> Term
reflexDef :: Bool -> Type -> Term
reflexDef refl :: Bool
refl w :: Type
w = let
  x :: VarDecl
x = Token -> Type -> VarDecl
hcVarDecl (String -> Token
genToken "x") Type
w
  p :: VarDecl
p = Type -> VarDecl
pVar Type
w
  pt :: Term
pt = VarDecl -> Term
QualVar VarDecl
p
  in [GenVarDecl] -> Term -> Term
HC.mkForall [VarDecl -> GenVarDecl
GenVarDecl VarDecl
p]
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
nr
       (Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp (if Bool
refl then Id
reflexId else Id
irreflexId)
                   (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
prOfBinPrTy Type
w) [Term
pt])
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenVarDecl] -> Term -> Term
HC.mkForall [VarDecl -> GenVarDecl
GenVarDecl VarDecl
x]
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if Bool
refl then Term -> Term
forall a. a -> a
id else Term -> Term
mkNot)
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> [Term] -> Term
mkApplTerm Term
pt ([Term] -> Term) -> (Term -> [Term]) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> [Term]
forall a. Int -> a -> [a]
replicate 2 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ VarDecl -> Term
QualVar VarDecl
x

varDecl :: Token -> SORT -> VarDecl
varDecl :: Token -> Id -> VarDecl
varDecl i :: Token
i = Token -> Type -> VarDecl
hcVarDecl Token
i (Type -> VarDecl) -> (Id -> Type) -> Id -> VarDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
toType

hcVarDecl :: Token -> Type -> VarDecl
hcVarDecl :: Token -> Type -> VarDecl
hcVarDecl i :: Token
i t :: Type
t = Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl (Token -> Id
simpleIdToId Token
i) Type
t SeparatorKind
Other Range
nr

varTerm :: Token -> SORT -> Term
varTerm :: Token -> Id -> Term
varTerm i :: Token
i = VarDecl -> Term
QualVar (VarDecl -> Term) -> (Id -> VarDecl) -> Id -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> Id -> VarDecl
varDecl Token
i

typeToSelector :: Maybe Id -> Type -> [Selector]
typeToSelector :: Maybe Id -> Type -> [Selector]
typeToSelector m :: Maybe Id
m a :: Type
a = [Maybe Id -> Type -> Partiality -> Selector
Select Maybe Id
m Type
a Partiality
HC.Total]

hasSuccessorS :: String
hasSuccessorS :: String
hasSuccessorS = "has_successor"

hasSuccessorId :: Id
hasSuccessorId :: Id
hasSuccessorId = String -> Id
genName String
hasSuccessorS

hasSuccessorTy :: Type
hasSuccessorTy :: Type
hasSuccessorTy = Type -> Partiality -> [Type] -> Type
getFunType Type
unitType Partiality
HC.Partial [Type
worldTy, Type -> Type
binPredTy Type
nWorld]

tauApplTerm :: Term -> Term -> Term
tauApplTerm :: Term -> Term -> Term
tauApplTerm t1 :: Term
t1 t2 :: Term
t2 = Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
tauId Type
tauTy) [Term
t1, Term
t2]

zeroT :: Term
zeroT :: Term
zeroT = Id -> Type -> Term
mkOp Id
zero Type
natTy

hasSuccessorDef :: Term
hasSuccessorDef :: Term
hasSuccessorDef = let
  [x0 :: VarDecl
x0, p :: VarDecl
p] = [VarDecl]
xZeroAndP
  (tT :: Term
tT, _, rT :: Term
rT) = Term -> (Term, Term, Term)
hasTauSucDefAux Term
zeroT
  in [GenVarDecl] -> Term -> Term
HC.mkForall ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl
x0, VarDecl
p])
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
nr
       (Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
hasSuccessorId Type
hasSuccessorTy) ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl
x0, VarDecl
p])
     (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nr Term
tT Term
rT

xZeroAndP :: [VarDecl]
xZeroAndP :: [VarDecl]
xZeroAndP = [Token -> Type -> VarDecl
hcVarDecl (String -> Int -> Token
genNumVar "x" 0) Type
worldTy, Type -> VarDecl
pVar Type
nWorld]

pairWorld :: Term -> Term -> Term
pairWorld :: Term -> Term -> Term
pairWorld t1 :: Term
t1 t2 :: Term
t2 = Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
mkNWorldId Type
nWorldTy) [Term
t1, Term
t2]

sucTy :: Type
sucTy :: Type
sucTy = Id -> AltDefn -> Type
altToTy Id
natId AltDefn
sucAlt

sucTerm :: Term -> Term
sucTerm :: Term -> Term
sucTerm t :: Term
t = Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
sucId Type
sucTy) [Term
t]

hasTauSucDefAux :: Term -> (Term, Term, Term)
hasTauSucDefAux :: Term -> (Term, Term, Term)
hasTauSucDefAux nT :: Term
nT = let
  x :: VarDecl
x = Token -> Type -> VarDecl
hcVarDecl (String -> Token
genToken "x") Type
worldTy
  vs :: [VarDecl]
vs = [VarDecl]
xZeroAndP
  [xt :: Term
xt, xt0 :: Term
xt0, pt :: Term
pt] = (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar ([VarDecl] -> [Term]) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> a -> b
$ VarDecl
x VarDecl -> [VarDecl] -> [VarDecl]
forall a. a -> [a] -> [a]
: [VarDecl]
vs
  tauAppl :: Term
tauAppl = Term -> Term -> Term
tauApplTerm Term
xt0 Term
xt
  pw :: Term
pw = Term -> Term -> Term
pairWorld Term
xt0 Term
nT
  in (VarDecl -> Term -> Term
mkExQ VarDecl
x Term
tauAppl, Term
pw,
     VarDecl -> Term -> Term
mkExQ VarDecl
x
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
nr Term
tauAppl
     (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm Term
pt [Term
pw, Term -> Term -> Term
pairWorld Term
xt (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
sucTerm Term
nT])

hasTauSucS :: String
hasTauSucS :: String
hasTauSucS = "has_tau_suc"

hasTauSucId :: Id
hasTauSucId :: Id
hasTauSucId = String -> Id
genName String
hasTauSucS

hasTauSucDefAny :: Term
hasTauSucDefAny :: Term
hasTauSucDefAny = let
  nv :: VarDecl
nv = Token -> Type -> VarDecl
hcVarDecl (String -> Token
genToken "n") Type
natTy
  nt :: Term
nt = VarDecl -> Term
QualVar VarDecl
nv
  [x0 :: VarDecl
x0, p :: VarDecl
p] = [VarDecl]
xZeroAndP
  (tT :: Term
tT, pw :: Term
pw, rT :: Term
rT) = Term -> (Term, Term, Term)
hasTauSucDefAux Term
nt
  y :: VarDecl
y = Token -> Type -> VarDecl
hcVarDecl (String -> Token
genToken "y") Type
nWorld
  in [GenVarDecl] -> Term -> Term
HC.mkForall [VarDecl -> GenVarDecl
GenVarDecl VarDecl
p]
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
nr
       (Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
hasTauSucId Type
prOfNwPrTy) [VarDecl -> Term
QualVar VarDecl
p])
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenVarDecl] -> Term -> Term
HC.mkForall ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl
x0, VarDecl
nv])
     (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nr
       (Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
nr
        (VarDecl -> Term -> Term
mkExQ VarDecl
y (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm (VarDecl -> Term
QualVar VarDecl
p) [VarDecl -> Term
QualVar VarDecl
y, Term
pw])
        Term
tT) Term
rT

subsetOfTauS :: String
subsetOfTauS :: String
subsetOfTauS = "subset_of_tau"

subsetOfTauId :: Id
subsetOfTauId :: Id
subsetOfTauId = String -> Id
genName String
subsetOfTauS

getWorld :: Term -> Term
getWorld :: Term -> Term
getWorld t :: Term
t = Term -> [Term] -> Term
mkApplTerm ((Id -> Type -> Term) -> (Id, Type) -> Term
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Id -> Type -> Term
mkOp ((Id, Type) -> Term) -> (Id, Type) -> Term
forall a b. (a -> b) -> a -> b
$ Id -> [Selector] -> (Id, Type)
selToTy Id
nWorldId [Selector]
getWorldSel) [Term
t]

subsetOfTauDef :: Term
subsetOfTauDef :: Term
subsetOfTauDef = let
  p :: VarDecl
p = Type -> VarDecl
pVar Type
nWorld
  pt :: Term
pt = VarDecl -> Term
QualVar VarDecl
p
  ts :: [Term]
ts@[xt :: Term
xt, yt :: Term
yt] = Type -> [Term]
tPair Type
nWorld
  in [GenVarDecl] -> Term -> Term
HC.mkForall [VarDecl -> GenVarDecl
GenVarDecl VarDecl
p]
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
nr
       (Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
subsetOfTauId Type
prOfNwPrTy) [Term
pt])
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenVarDecl] -> Term -> Term
HC.mkForall (Type -> [GenVarDecl]
pairDs Type
nWorld)
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nr
       (Term -> [Term] -> Term
mkApplTerm Term
pt [Term]
ts)
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term -> Term
tauApplTerm (Term -> Term
getWorld Term
xt) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
getWorld Term
yt

superpathS :: String
superpathS :: String
superpathS = "superpath"

superpathId :: Id
superpathId :: Id
superpathId = String -> Id
genName String
superpathS

superpathDef :: Term
superpathDef :: Term
superpathDef = let
  vs :: [VarDecl]
vs = [VarDecl]
xZeroAndP
  ts :: [Term]
ts@[_, pt :: Term
pt] = (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl]
vs
  in [GenVarDecl] -> Term -> Term
HC.mkForall ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl]
vs)
     (Term -> Term) -> ([Term] -> Term) -> [Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
nr
       (Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
superpathId Type
hasSuccessorTy) [Term]
ts)
     (Term -> Term) -> ([Term] -> Term) -> [Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> Term
mkConj
     ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
hasSuccessorId Type
hasSuccessorTy) [Term]
ts
      Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: (Id -> Term) -> [Id] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\ i :: Id
i -> Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
i Type
prOfNwPrTy) [Term
pt])
        [Id
irreflexId, Id
subsetOfTauId, Id
hasTauSucId, Id
transLinearOrderId]

pathS :: String
pathS :: String
pathS = "path"

pathId :: Id
pathId :: Id
pathId = String -> Id
genName String
pathS

pathAppl :: [Term] -> Term
pathAppl :: [Term] -> Term
pathAppl = Term -> [Term] -> Term
mkApplTerm (Term -> [Term] -> Term) -> Term -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Type -> Term
mkOp Id
pathId Type
hasSuccessorTy

pathDef :: Term
pathDef :: Term
pathDef = let
  vs :: [VarDecl]
vs = [VarDecl]
xZeroAndP
  [rv :: VarDecl
rv, qv :: VarDecl
qv] = Type -> [VarDecl]
rAndQ Type
nWorld
  [rt :: Term
rt, qt :: Term
qt] = (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl
rv, VarDecl
qv]
  ts :: [Term]
ts@[x0 :: Term
x0, pt :: Term
pt] = (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl]
vs
  in [GenVarDecl] -> Term -> Term
HC.mkForall ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl]
vs)
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
nr
       ([Term] -> Term
pathAppl [Term]
ts)
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDecl -> Term -> Term
mkExQ VarDecl
rv
     (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
mkConj
       [ Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
superpathId Type
hasSuccessorTy) [Term
x0, Term
rt]
       , Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
transReflexId (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
transTy Type
nWorld) [Term
rt, Term
pt]
       , [GenVarDecl] -> Term -> Term
HC.mkForall [VarDecl -> GenVarDecl
GenVarDecl VarDecl
qv]
         (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nr
           (Term -> [Term] -> Term
mkApplTerm (Id -> Type -> Term
mkOp Id
superpathId Type
hasSuccessorTy) [Term
x0, Term
qt])
         (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
orId Range
nr
           (Bool -> Id -> Term -> Term -> Type -> Term
containsDefAux Bool
True Id
implId Term
qt Term
rt Type
nWorld)
           (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Bool -> Id -> Term -> Term -> Type -> Term
containsDefAux Bool
False Id
eqvId Term
qt Term
rt Type
nWorld
       ]

toSen :: ExtModalSign -> FORMULA EM_FORMULA -> Sentence
toSen :: ExtModalSign -> ExtModalFORMULA -> Sentence
toSen msig :: ExtModalSign
msig f :: ExtModalFORMULA
f = case ExtModalFORMULA
f of
   Sort_gen_ax cs :: [Constraint]
cs b :: Bool
b -> let
       (sorts :: [Id]
sorts, ops :: [OP_SYMB]
ops, smap :: [(Id, Id)]
smap) = [Constraint] -> ([Id], [OP_SYMB], [(Id, Id)])
recover_Sort_gen_ax [Constraint]
cs
       genKind :: GenKind
genKind = if Bool
b then GenKind
Free else GenKind
Generated
       mapPart :: OpKind -> Partiality
       mapPart :: OpKind -> Partiality
mapPart cp :: OpKind
cp = case OpKind
cp of
                CASL.Total -> Partiality
HC.Total
                CASL.Partial -> Partiality
HC.Partial
       in [DataEntry] -> Sentence
DatatypeSen ([DataEntry] -> Sentence) -> [DataEntry] -> Sentence
forall a b. (a -> b) -> a -> b
$ (Id -> DataEntry) -> [Id] -> [DataEntry]
forall a b. (a -> b) -> [a] -> [b]
map ( \ s :: Id
s ->
          IdMap
-> Id
-> GenKind
-> [TypeArg]
-> RawKind
-> Set AltDefn
-> DataEntry
DataEntry ([(Id, Id)] -> IdMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Id, Id)]
smap) Id
s GenKind
genKind [] RawKind
rStar
          (Set AltDefn -> DataEntry) -> Set AltDefn -> DataEntry
forall a b. (a -> b) -> a -> b
$ [AltDefn] -> Set AltDefn
forall a. Ord a => [a] -> Set a
Set.fromList ([AltDefn] -> Set AltDefn) -> [AltDefn] -> Set AltDefn
forall a b. (a -> b) -> a -> b
$ ((Id, OpType) -> AltDefn) -> [(Id, OpType)] -> [AltDefn]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: Id
i, t :: OpType
t) ->
            let args :: [Type]
args = (Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
toType ([Id] -> [Type]) -> [Id] -> [Type]
forall a b. (a -> b) -> a -> b
$ OpType -> [Id]
opArgs OpType
t in
            Maybe Id -> [Type] -> Partiality -> [[Selector]] -> AltDefn
Construct (if Id -> Bool
isInjName Id
i then Maybe Id
forall a. Maybe a
Nothing else Id -> Maybe Id
forall a. a -> Maybe a
Just Id
i) [Type]
args
              (OpKind -> Partiality
mapPart (OpKind -> Partiality) -> OpKind -> Partiality
forall a b. (a -> b) -> a -> b
$ OpType -> OpKind
opKind OpType
t)
              ([[Selector]] -> AltDefn) -> [[Selector]] -> AltDefn
forall a b. (a -> b) -> a -> b
$ (Type -> [Selector]) -> [Type] -> [[Selector]]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Id -> Type -> [Selector]
typeToSelector Maybe Id
forall a. Maybe a
Nothing) [Type]
args)
          ([(Id, OpType)] -> [AltDefn]) -> [(Id, OpType)] -> [AltDefn]
forall a b. (a -> b) -> a -> b
$ ((Id, OpType) -> Bool) -> [(Id, OpType)] -> [(Id, OpType)]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ (_, t :: OpType
t) -> OpType -> Id
opRes OpType
t Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
s)
                ([(Id, OpType)] -> [(Id, OpType)])
-> [(Id, OpType)] -> [(Id, OpType)]
forall a b. (a -> b) -> a -> b
$ (OP_SYMB -> (Id, OpType)) -> [OP_SYMB] -> [(Id, OpType)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ o :: OP_SYMB
o -> case OP_SYMB
o of
                        Qual_op_name i :: Id
i t :: OP_TYPE
t _ -> (Id -> Id
trI Id
i, OP_TYPE -> OpType
toOpType OP_TYPE
t)
                        _ -> String -> (Id, OpType)
forall a. HasCallStack => String -> a
error "ExtModal2HasCASL.toSentence") [OP_SYMB]
ops) [Id]
sorts
   _ -> Term -> Sentence
Formula (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ ExtModalSign -> ExtModalFORMULA -> Term
transTop ExtModalSign
msig ExtModalFORMULA
f

transFrames :: ExtModalSign -> [Named (FORMULA EM_FORMULA)] -> [Named Sentence]
transFrames :: ExtModalSign -> [Named ExtModalFORMULA] -> [Named Sentence]
transFrames sig :: ExtModalSign
sig = (Named ExtModalFORMULA -> [Named Sentence] -> [Named Sentence])
-> [Named Sentence] -> [Named ExtModalFORMULA] -> [Named Sentence]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ nf :: Named ExtModalFORMULA
nf -> case Named ExtModalFORMULA -> ExtModalFORMULA
forall s a. SenAttr s a -> s
sentence Named ExtModalFORMULA
nf of
  ExtFORMULA (ModForm (ModDefn _ _ _ fs :: [Annoted FrameForm]
fs _)) ->
     ((Annoted ExtModalFORMULA -> Named Sentence)
-> [Annoted ExtModalFORMULA] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (\ af :: Annoted ExtModalFORMULA
af -> let l :: String
l = Annoted ExtModalFORMULA -> String
forall a. Annoted a -> String
getRLabel Annoted ExtModalFORMULA
af in
           Named ExtModalFORMULA
nf { sentence :: Sentence
sentence = Term -> Sentence
Formula (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ ExtModalSign -> ExtModalFORMULA -> Term
transTop ExtModalSign
sig (Annoted ExtModalFORMULA -> ExtModalFORMULA
forall a. Annoted a -> a
item Annoted ExtModalFORMULA
af)
              , senAttr :: String
senAttr = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
l then Named ExtModalFORMULA -> String
forall s a. SenAttr s a -> a
senAttr Named ExtModalFORMULA
nf else String
l })
     ((Annoted FrameForm -> [Annoted ExtModalFORMULA])
-> [Annoted FrameForm] -> [Annoted ExtModalFORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FrameForm -> [Annoted ExtModalFORMULA]
frameForms (FrameForm -> [Annoted ExtModalFORMULA])
-> (Annoted FrameForm -> FrameForm)
-> Annoted FrameForm
-> [Annoted ExtModalFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted FrameForm -> FrameForm
forall a. Annoted a -> a
item) [Annoted FrameForm]
fs) [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++)
  _ -> [Named Sentence] -> [Named Sentence]
forall a. a -> a
id) []

isFrameAx :: FORMULA EM_FORMULA -> Bool
isFrameAx :: ExtModalFORMULA -> Bool
isFrameAx f :: ExtModalFORMULA
f = case ExtModalFORMULA
f of
  ExtFORMULA (ModForm _) -> Bool
True
  _ -> Bool
False

data Args = Args
  { Args -> Term
sourceW, Args -> Term
targetW, Args -> Term
targetN :: Term
  , Args -> Int
nextW, Args -> Int
freeC :: Int  -- world variables
  , Args -> Int
freeZ :: Int -- path variable
  , Args -> [(Id, Term)]
boundNoms :: [(Id, Term)]
  , Args -> ExtModalSign
modSig :: ExtModalSign
  }

startArgs :: ExtModalSign -> Args
startArgs :: ExtModalSign -> Args
startArgs msig :: ExtModalSign
msig = let
  vt :: Term
vt = Token -> Id -> Term
varTerm (String -> Int -> Token
genNumVar "w" 1) Id
world
  in Args :: Term
-> Term
-> Term
-> Int
-> Int
-> Int
-> [(Id, Term)]
-> ExtModalSign
-> Args
Args
  { sourceW :: Term
sourceW = Term
vt
  , targetW :: Term
targetW = Term
vt
  , targetN :: Term
targetN = Term
zeroT
  , nextW :: Int
nextW = 1
  , freeC :: Int
freeC = 1
  , freeZ :: Int
freeZ = 1
  , boundNoms :: [(Id, Term)]
boundNoms = []
  , modSig :: ExtModalSign
modSig = ExtModalSign
msig
  }

zDecl :: Args -> VarDecl
zDecl :: Args -> VarDecl
zDecl as :: Args
as = Token -> Type -> VarDecl
hcVarDecl (String -> Int -> Token
genNumVar "Z" (Int -> Token) -> Int -> Token
forall a b. (a -> b) -> a -> b
$ Args -> Int
freeZ Args
as) (Type -> VarDecl) -> Type -> VarDecl
forall a b. (a -> b) -> a -> b
$ Type -> Type
binPredTy Type
nWorld

transTop :: ExtModalSign -> FORMULA EM_FORMULA -> Term
transTop :: ExtModalSign -> ExtModalFORMULA -> Term
transTop msig :: ExtModalSign
msig f :: ExtModalFORMULA
f = let
  as :: Args
as = ExtModalSign -> Args
startArgs ExtModalSign
msig
  vs :: [VarDecl]
vs = [Token -> Type -> VarDecl
hcVarDecl (String -> Int -> Token
genNumVar "w" 1) Type
worldTy, Args -> VarDecl
zDecl Args
as]
  in [GenVarDecl] -> Term -> Term
HC.mkForall ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl]
vs)
     (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nr
     ([Term] -> Term
pathAppl ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl]
vs)
     (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Args -> ExtModalFORMULA -> Term
transMF Args
as ExtModalFORMULA
f

getTermOfNom :: Args -> Id -> Term
getTermOfNom :: Args -> Id -> Term
getTermOfNom as :: Args
as i :: Id
i = Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe (Id -> Term
mkNomAppl Id
i) (Maybe Term -> Term)
-> ([(Id, Term)] -> Maybe Term) -> [(Id, Term)] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> [(Id, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Id
i ([(Id, Term)] -> Term) -> [(Id, Term)] -> Term
forall a b. (a -> b) -> a -> b
$ Args -> [(Id, Term)]
boundNoms Args
as

mkZPath :: Term -> Term -> Args -> Term
mkZPath :: Term -> Term -> Args -> Term
mkZPath v :: Term
v n :: Term
n as :: Args
as = Term -> [Term] -> Term
mkApplTerm (VarDecl -> Term
QualVar (VarDecl -> Term) -> VarDecl -> Term
forall a b. (a -> b) -> a -> b
$ Args -> VarDecl
zDecl Args
as)
    [Term -> Term -> Term
pairWorld Term
v Term
n, Term -> Term -> Term
pairWorld (Args -> Term
targetW Args
as) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Args -> Term
targetN Args
as]

zPath :: Args -> Term
zPath :: Args -> Term
zPath as :: Args
as = Term -> Term -> Args -> Term
mkZPath (Args -> Term
sourceW Args
as) Term
zeroT Args
as

trRecord :: Args -> String -> Record EM_FORMULA Term Term
trRecord :: Args -> String -> Record EM_FORMULA Term Term
trRecord as :: Args
as str :: String
str = let
    extInf :: EModalSign
extInf = ExtModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo (ExtModalSign -> EModalSign) -> ExtModalSign -> EModalSign
forall a b. (a -> b) -> a -> b
$ Args -> ExtModalSign
modSig Args
as
    currW :: Term
currW = Args -> Term
targetW Args
as
    andPath :: Term -> Term
andPath = Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
nr (Term -> Term -> Term) -> Term -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Args -> Term
zPath Args
as
    typeTerm :: Type -> Term -> Term
typeTerm hty :: Type
hty tr :: Term
tr = case Term -> Maybe Type
forall (m :: * -> *). MonadFail m => Term -> m Type
getTypeOf Term
tr of
      Just t :: Type
t | Type
hty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t -> Term
tr
      _ -> Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
tr TypeQual
Inferred Type
hty Range
nr
    typeArgs :: [Id] -> [Term] -> [Term]
typeArgs = (Id -> Term -> Term) -> [Id] -> [Term] -> [Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Type -> Term -> Term
typeTerm (Type -> Term -> Term) -> (Id -> Type) -> Id -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
toType)
    in (String -> Record EM_FORMULA Term Term
forall f. TermExtension f => String -> Record f Term Term
transRecord String
str)
  { foldPredication :: ExtModalFORMULA -> PRED_SYMB -> [Term] -> Range -> Term
foldPredication = \ _ ps :: PRED_SYMB
ps pargs :: [Term]
pargs _ -> let
      Qual_pred_name pn :: Id
pn pTy :: PRED_TYPE
pTy@(Pred_type srts :: [Id]
srts q :: Range
q) _ = PRED_SYMB
ps
      args :: [Term]
args = [Id] -> [Term] -> [Term]
typeArgs [Id]
srts [Term]
pargs
      in Term -> Term
andPath
         (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term
typeTerm Type
unitType
         (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ if Id -> PredType -> PredMap -> Bool
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> Bool
MapSet.member Id
pn (PRED_TYPE -> PredType
toPredType PRED_TYPE
pTy) (PredMap -> Bool) -> PredMap -> Bool
forall a b. (a -> b) -> a -> b
$ EModalSign -> PredMap
flexPreds EModalSign
extInf
         then Term -> [Term] -> Term
mkApplTerm
            (Id -> Type -> Term
mkOp (Id -> Id
trI Id
pn) (Type -> Term) -> (PRED_TYPE -> Type) -> PRED_TYPE -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRED_TYPE -> Type
trPrSyn
            (PRED_TYPE -> Term) -> PRED_TYPE -> Term
forall a b. (a -> b) -> a -> b
$ [Id] -> Range -> PRED_TYPE
Pred_type (Id
world Id -> [Id] -> [Id]
forall a. a -> [a] -> [a]
: [Id]
srts) Range
q) ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ Term
currW Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
args
         else if [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
srts Bool -> Bool -> Bool
&& Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
pn (EModalSign -> Set Id
nominals EModalSign
extInf)
              then Term -> Term -> Term
eqW Term
currW (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Args -> Id -> Term
getTermOfNom Args
as Id
pn
         else Term -> [Term] -> Term
mkApplTerm
            (Id -> Type -> Term
mkOp (Id -> Id
trI Id
pn) (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ PRED_TYPE -> Type
trPrSyn PRED_TYPE
pTy) [Term]
args
  , foldEquation :: ExtModalFORMULA -> Term -> Equality -> Term -> Range -> Term
foldEquation = \ o :: ExtModalFORMULA
o t1 :: Term
t1 e :: Equality
e t2 :: Term
t2 ps :: Range
ps ->
        let Equation c1 :: TERM EM_FORMULA
c1 _ _ _ = ExtModalFORMULA
o in
        Term -> Term
andPath (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Type -> Range -> Term -> Term -> Term
mkEqTerm (if Equality
e Equality -> Equality -> Bool
forall a. Eq a => a -> a -> Bool
== Equality
Existl then Id
exEq else Id
eqId)
                     (TERM EM_FORMULA -> Type
forall f. TermExtension f => TERM f -> Type
typeOfTerm TERM EM_FORMULA
c1) Range
ps Term
t1 Term
t2
  , foldDefinedness :: ExtModalFORMULA -> Term -> Range -> Term
foldDefinedness = \ o :: ExtModalFORMULA
o t :: Term
t ps :: Range
ps ->
        let Definedness c :: TERM EM_FORMULA
c _ = ExtModalFORMULA
o in
        Term -> Term
andPath (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm Id
defId TypeScheme
defType [TERM EM_FORMULA -> Type
forall f. TermExtension f => TERM f -> Type
typeOfTerm TERM EM_FORMULA
c] Range
ps Term
t
  , foldExtFORMULA :: ExtModalFORMULA -> EM_FORMULA -> Term
foldExtFORMULA = \ _ f :: EM_FORMULA
f -> Args -> EM_FORMULA -> Term
transEMF Args
as EM_FORMULA
f
  , foldApplication :: TERM EM_FORMULA -> OP_SYMB -> [Term] -> Range -> Term
foldApplication = \ _ os :: OP_SYMB
os oargs :: [Term]
oargs _ -> let
      Qual_op_name opn :: Id
opn oTy :: OP_TYPE
oTy@(Op_type ok :: OpKind
ok srts :: [Id]
srts res :: Id
res q :: Range
q) _ = OP_SYMB
os
      args :: [Term]
args = [Id] -> [Term] -> [Term]
typeArgs [Id]
srts [Term]
oargs
      in Type -> Term -> Term
typeTerm (Id -> Type
toType Id
res)
         (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ if Id -> OpType -> OpMap -> Bool
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> Bool
MapSet.member Id
opn (OP_TYPE -> OpType
toOpType OP_TYPE
oTy) (OpMap -> Bool) -> OpMap -> Bool
forall a b. (a -> b) -> a -> b
$ EModalSign -> OpMap
flexOps EModalSign
extInf
         then Term -> [Term] -> Term
mkApplTerm
            (Id -> Type -> Term
mkOp (Id -> Id
trI Id
opn) (Type -> Term) -> (OP_TYPE -> Type) -> OP_TYPE -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OP_TYPE -> Type
trOpSyn
            (OP_TYPE -> Term) -> OP_TYPE -> Term
forall a b. (a -> b) -> a -> b
$ OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
ok (Id
world Id -> [Id] -> [Id]
forall a. a -> [a] -> [a]
: [Id]
srts) Id
res Range
q) ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ Term
currW Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
args
         else Term -> [Term] -> Term
mkApplTerm
            (Id -> Type -> Term
mkOp (Id -> Id
trI Id
opn) (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> Type
trOpSyn OP_TYPE
oTy) [Term]
args
  }

transMF :: Args -> FORMULA EM_FORMULA -> Term
transMF :: Args -> ExtModalFORMULA -> Term
transMF a :: Args
a f :: ExtModalFORMULA
f = Record EM_FORMULA Term Term -> ExtModalFORMULA -> Term
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Args -> String -> Record EM_FORMULA Term Term
trRecord Args
a (String -> Record EM_FORMULA Term Term)
-> String -> Record EM_FORMULA Term Term
forall a b. (a -> b) -> a -> b
$ ExtModalFORMULA -> ShowS
forall a. Pretty a => a -> ShowS
showDoc ExtModalFORMULA
f "") ExtModalFORMULA
f

disjointVars :: [VarDecl] -> [Term]
disjointVars :: [VarDecl] -> [Term]
disjointVars vs :: [VarDecl]
vs = case [VarDecl]
vs of
  a :: VarDecl
a : r :: [VarDecl]
r@(b :: VarDecl
b : _) -> Term -> Term
mkNot
    ((Term -> Term -> Term)
-> (VarDecl -> Term) -> VarDecl -> VarDecl -> Term
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on Term -> Term -> Term
eqW VarDecl -> Term
QualVar VarDecl
a VarDecl
b) Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [VarDecl] -> [Term]
disjointVars [VarDecl]
r
  _ -> []

pathAppl2 :: Term -> VarDecl -> Term
pathAppl2 :: Term -> VarDecl -> Term
pathAppl2 t :: Term
t v :: VarDecl
v = [Term] -> Term
pathAppl [Term
t, VarDecl -> Term
QualVar VarDecl
v]

transEMF :: Args -> EM_FORMULA -> Term
transEMF :: Args -> EM_FORMULA -> Term
transEMF as :: Args
as emf :: EM_FORMULA
emf = let
  fW :: Int
fW = Args -> Int
freeC Args
as
  pathAppl3 :: Term -> VarDecl -> Term -> Term
pathAppl3 t :: Term
t = Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
nr (Term -> Term -> Term)
-> (VarDecl -> Term) -> VarDecl -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> VarDecl -> Term
pathAppl2 Term
t
  is :: Int -> [Int]
is i :: Int
i = [Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 .. Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i]
  mkVs :: Char -> Id -> Int -> [VarDecl]
mkVs c :: Char
c ty :: Id
ty = (Int -> VarDecl) -> [Int] -> [VarDecl]
forall a b. (a -> b) -> [a] -> [b]
map (\ n :: Int
n -> Token -> Id -> VarDecl
varDecl (String -> Int -> Token
genNumVar [Char
c] Int
n) Id
ty) ([Int] -> [VarDecl]) -> (Int -> [Int]) -> Int -> [VarDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Int]
is
  vds :: Int -> [VarDecl]
vds = Char -> Id -> Int -> [VarDecl]
mkVs 'w' Id
world
  nds :: Int -> [VarDecl]
nds = Char -> Id -> Int -> [VarDecl]
mkVs 'n' Id
natId
  gvs :: Int -> [GenVarDecl]
gvs = (VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl ([VarDecl] -> [GenVarDecl])
-> (Int -> [VarDecl]) -> Int -> [GenVarDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [VarDecl]
vds
  vt0 :: Term
vt0 = Args -> Term
targetW Args
as
  nt0 :: Term
nt0 = Args -> Term
targetN Args
as
  [v1 :: VarDecl
v1] = Int -> [VarDecl]
vds 1
  [n1 :: VarDecl
n1] = Int -> [VarDecl]
nds 1
  [vt1 :: Term
vt1, nt1 :: Term
nt1] = (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl
v1, VarDecl
n1]
  gvs1 :: [GenVarDecl]
gvs1 = (VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl
v1, VarDecl
n1]
  mkEqNats :: Term -> Term -> Term
mkEqNats = Id -> Type -> Range -> Term -> Term -> Term
mkEqTerm Id
eqId Type
natTy Range
nr
  in case EM_FORMULA
emf of
  PrefixForm pf :: FormPrefix
pf f :: ExtModalFORMULA
f r :: Range
r -> case FormPrefix
pf of
    BoxOrDiamond bOp :: BoxOp
bOp m :: MODALITY
m gEq :: Bool
gEq i :: Int
i -> let
      ex :: Bool
ex = BoxOp
bOp BoxOp -> BoxOp -> Bool
forall a. Eq a => a -> a -> Bool
== BoxOp
Diamond
      l :: [Int]
l = Int -> [Int]
is Int
i
      gs :: [GenVarDecl]
gs = Int -> [GenVarDecl]
gvs Int
i
      nAs :: Args
nAs = Args
as { freeC :: Int
freeC = Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i }
      tf :: Int -> Term
tf n :: Int
n = let
        vt :: Term
vt = Token -> Id -> Term
varTerm (String -> Int -> Token
genNumVar "w" Int
n) Id
world
        newAs :: Args
newAs = Args
nAs { freeZ :: Int
freeZ = Int
n }
        zd :: VarDecl
zd = Args -> VarDecl
zDecl Args
newAs
        in [GenVarDecl] -> Term -> Term
HC.mkForall [VarDecl -> GenVarDecl
GenVarDecl VarDecl
zd]
           (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> VarDecl -> Term -> Term
pathAppl3 Term
vt VarDecl
zd
            (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Args -> ExtModalFORMULA -> Term
transMF (Term -> Args -> Args
resetArgs Term
vt Args
newAs) ExtModalFORMULA
f
      tM :: Int -> Term
tM n :: Int
n = Args -> MODALITY -> Term
transMod Args
nAs { nextW :: Int
nextW = Int
n } MODALITY
m
      conjF :: Term
conjF = [Term] -> Term
mkConj ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
tM [Int]
l [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
tf [Int]
l [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [VarDecl] -> [Term]
disjointVars (Int -> [VarDecl]
vds Int
i)
      diam :: Int -> FormPrefix
diam = BoxOp -> MODALITY -> Bool -> Int -> FormPrefix
BoxOrDiamond BoxOp
Diamond MODALITY
m Bool
True
      tr :: BoxOp -> Term
tr b :: BoxOp
b = Args -> EM_FORMULA -> Term
transEMF Args
as (EM_FORMULA -> Term) -> EM_FORMULA -> Term
forall a b. (a -> b) -> a -> b
$ FormPrefix -> ExtModalFORMULA -> Range -> EM_FORMULA
PrefixForm (BoxOp -> MODALITY -> Bool -> Int -> FormPrefix
BoxOrDiamond BoxOp
b MODALITY
m Bool
gEq Int
i) ExtModalFORMULA
f Range
r
      f1 :: Term
f1 = Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
HC.Existential [GenVarDecl]
gs Term
conjF Range
r
      f2 :: Term
f2 = [GenVarDecl] -> Term -> Term
HC.mkForall [GenVarDecl]
gs Term
conjF
      in if Bool
gEq Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 Bool -> Bool -> Bool
&& (Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 Bool -> Bool -> Bool
|| Bool
ex) then case BoxOp
bOp of
           Diamond -> Term
f1
           Box -> Term
f2
           EBox -> [Term] -> Term
mkConj [Term
f1, Term
f2]
         else if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 Bool -> Bool -> Bool
&& Bool
ex Bool -> Bool -> Bool
&& Bool
gEq then Id -> Range -> Term
unitTerm Id
trueId Range
r
         else if BoxOp
bOp BoxOp -> BoxOp -> Bool
forall a. Eq a => a -> a -> Bool
== BoxOp
EBox then [Term] -> Term
mkConj ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ (BoxOp -> Term) -> [BoxOp] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map BoxOp -> Term
tr [BoxOp
Diamond, BoxOp
Box]
         else if Bool
ex -- lEq
              then Args -> ExtModalFORMULA -> Term
transMF Args
as (ExtModalFORMULA -> Term)
-> (EM_FORMULA -> ExtModalFORMULA) -> EM_FORMULA -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtModalFORMULA -> ExtModalFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg (ExtModalFORMULA -> ExtModalFORMULA)
-> (EM_FORMULA -> ExtModalFORMULA) -> EM_FORMULA -> ExtModalFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EM_FORMULA -> ExtModalFORMULA
forall f. f -> FORMULA f
ExtFORMULA (EM_FORMULA -> Term) -> EM_FORMULA -> Term
forall a b. (a -> b) -> a -> b
$ FormPrefix -> ExtModalFORMULA -> Range -> EM_FORMULA
PrefixForm
                       (Int -> FormPrefix
diam (Int -> FormPrefix) -> Int -> FormPrefix
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) ExtModalFORMULA
f Range
r
         else if Bool
gEq -- Box
              then Args -> ExtModalFORMULA -> Term
transMF Args
as (ExtModalFORMULA -> Term)
-> (EM_FORMULA -> ExtModalFORMULA) -> EM_FORMULA -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtModalFORMULA -> ExtModalFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg (ExtModalFORMULA -> ExtModalFORMULA)
-> (EM_FORMULA -> ExtModalFORMULA) -> EM_FORMULA -> ExtModalFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EM_FORMULA -> ExtModalFORMULA
forall f. f -> FORMULA f
ExtFORMULA (EM_FORMULA -> Term) -> EM_FORMULA -> Term
forall a b. (a -> b) -> a -> b
$ FormPrefix -> ExtModalFORMULA -> Range -> EM_FORMULA
PrefixForm
                       (Int -> FormPrefix
diam Int
i) (ExtModalFORMULA -> ExtModalFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg ExtModalFORMULA
f) Range
r
              else Args -> ExtModalFORMULA -> Term
transMF Args
as (ExtModalFORMULA -> Term)
-> (EM_FORMULA -> ExtModalFORMULA) -> EM_FORMULA -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EM_FORMULA -> ExtModalFORMULA
forall f. f -> FORMULA f
ExtFORMULA (EM_FORMULA -> Term) -> EM_FORMULA -> Term
forall a b. (a -> b) -> a -> b
$ FormPrefix -> ExtModalFORMULA -> Range -> EM_FORMULA
PrefixForm
                       (Int -> FormPrefix
diam (Int -> FormPrefix) -> Int -> FormPrefix
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (ExtModalFORMULA -> ExtModalFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg ExtModalFORMULA
f) Range
r
    Hybrid at :: Bool
at i :: Token
i -> let ni :: Id
ni = Token -> Id
simpleIdToId Token
i in
      if Bool
at then let
           ti :: Term
ti = Args -> Id -> Term
getTermOfNom Args
as Id
ni
           nAs :: Args
nAs = Args
as { freeC :: Int
freeC = Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1, freeZ :: Int
freeZ = Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }
           zd :: VarDecl
zd = Args -> VarDecl
zDecl Args
nAs
           in [Term] -> Term
mkConj
           [ Args -> Term
zPath Args
as, [GenVarDecl] -> Term -> Term
HC.mkForall [VarDecl -> GenVarDecl
GenVarDecl VarDecl
zd]
           (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> VarDecl -> Term -> Term
pathAppl3 Term
ti VarDecl
zd (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Args -> ExtModalFORMULA -> Term
transMF (Term -> Args -> Args
resetArgs Term
ti Args
as) ExtModalFORMULA
f ]
      else let
      vi :: VarDecl
vi = Token -> Id -> VarDecl
varDecl (String -> Int -> Token
genNumVar "i" (Int -> Token) -> Int -> Token
forall a b. (a -> b) -> a -> b
$ Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Id
world
      ti :: Term
ti = VarDecl -> Term
QualVar VarDecl
vi
      in VarDecl -> [Term] -> Term
mkExConj VarDecl
vi
           [ Term -> Term -> Term
eqW Term
ti Term
vt0
           , Args -> ExtModalFORMULA -> Term
transMF Args
as { boundNoms :: [(Id, Term)]
boundNoms = (Id
ni, Term
ti) (Id, Term) -> [(Id, Term)] -> [(Id, Term)]
forall a. a -> [a] -> [a]
: Args -> [(Id, Term)]
boundNoms Args
as
                        , targetW :: Term
targetW = Term
ti
                        , freeC :: Int
freeC = Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 } ExtModalFORMULA
f ]
    StateQuantification fut :: Bool
fut gen :: Bool
gen -> let
      nAs :: Args
nAs = Args
as { freeC :: Int
freeC = Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1, targetW :: Term
targetW = Term
vt1, targetN :: Term
targetN = Term
nt1 }
      in Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
r (Args -> Term
zPath Args
as)
         (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if Bool
gen then [GenVarDecl] -> Term -> Term
HC.mkForall else [GenVarDecl] -> Term -> Term
mkExQs) [GenVarDecl]
gvs1
         (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm (if Bool
gen then Id
implId else Id
andId) Range
nr
           (if Bool
fut then Term -> Term -> Args -> Term
mkZPath Term
vt0 Term
nt0 Args
nAs else Term -> Term -> Args -> Term
mkZPath Term
vt1 Term
nt1 Args
as)
           (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Args -> ExtModalFORMULA -> Term
transMF Args
nAs ExtModalFORMULA
f
    PathQuantification gen :: Bool
gen -> if Bool
gen then let
      ws :: [VarDecl]
ws = Char -> Id -> Int -> [VarDecl]
mkVs 'p' Id
nWorldId 2
      [w1 :: Term
w1, w2 :: Term
w2] = (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl]
ws
      p :: Term
p = Term -> Term -> Term
pairWorld Term
vt0 Term
nt0
      nAs :: Args
nAs = Args
as { freeC :: Int
freeC = Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 2, freeZ :: Int
freeZ = Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 }
      zd :: VarDecl
zd = Args -> VarDecl
zDecl Args
nAs
      zt :: Term
zt = VarDecl -> Term
QualVar VarDecl
zd
      z :: Term
z = VarDecl -> Term
QualVar (VarDecl -> Term) -> VarDecl -> Term
forall a b. (a -> b) -> a -> b
$ Args -> VarDecl
zDecl Args
as
      in Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
r (Args -> Term
zPath Args
as)
         (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenVarDecl] -> Term -> Term
HC.mkForall [VarDecl -> GenVarDecl
GenVarDecl VarDecl
zd]
         (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
r
           (Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
r (Term -> VarDecl -> Term
pathAppl2 (Args -> Term
sourceW Args
as) VarDecl
zd)
            (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenVarDecl] -> Term -> Term
HC.mkForall [GenVarDecl]
gvs1
            (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
r
              (Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
r
               (Term -> Term -> Args -> Term
mkZPath Term
vt1 Term
nt1 Args
as) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Args -> Term
mkZPath Term
vt1 Term
nt1 Args
nAs)
            (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenVarDecl] -> Term -> Term
HC.mkForall ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl]
ws)
            (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
implId Range
r
              (Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
r
               (Term -> [Term] -> Term
mkApplTerm Term
z [Term
w1, Term
p])
               (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm Term
z [Term
w2, Term
p])
            (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
r
              (Term -> [Term] -> Term
mkApplTerm Term
z [Term
w1, Term
w2])
              (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm Term
zt [Term
w1, Term
w2])
         (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Args -> ExtModalFORMULA -> Term
transMF Args
nAs ExtModalFORMULA
f
      else Args -> ExtModalFORMULA -> Term
transMF Args
as (ExtModalFORMULA -> Term)
-> (EM_FORMULA -> ExtModalFORMULA) -> EM_FORMULA -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtModalFORMULA -> ExtModalFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg (ExtModalFORMULA -> ExtModalFORMULA)
-> (EM_FORMULA -> ExtModalFORMULA) -> EM_FORMULA -> ExtModalFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EM_FORMULA -> ExtModalFORMULA
forall f. f -> FORMULA f
ExtFORMULA (EM_FORMULA -> Term) -> EM_FORMULA -> Term
forall a b. (a -> b) -> a -> b
$ FormPrefix -> ExtModalFORMULA -> Range -> EM_FORMULA
PrefixForm
               (Bool -> FormPrefix
PathQuantification (Bool -> FormPrefix) -> Bool -> FormPrefix
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
gen) (ExtModalFORMULA -> ExtModalFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg ExtModalFORMULA
f) Range
r
    NextY next :: Bool
next -> let
      nAs :: Args
nAs = Args
as { freeC :: Int
freeC = Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1, targetW :: Term
targetW = Term
vt1 }
      in Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
r (Args -> Term
zPath Args
as)
         (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenVarDecl] -> Term -> Term
mkExQs (if Bool
next then [VarDecl -> GenVarDecl
GenVarDecl VarDecl
v1] else [GenVarDecl]
gvs1)
         (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ if Bool
next then let
               as2 :: Args
as2 = Args
nAs { targetN :: Term
targetN = Term -> Term
sucTerm Term
nt0 }
               in Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
r (Term -> Term -> Args -> Term
mkZPath Term
vt0 Term
nt0 Args
as2)
                  (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Args -> ExtModalFORMULA -> Term
transMF Args
as2 ExtModalFORMULA
f
           else let
               as2 :: Args
as2 = Args
nAs { targetN :: Term
targetN = Term
nt1 }
               in [Term] -> Term
mkConj
               [ Term -> Term -> Args -> Term
mkZPath Term
vt1 Term
nt1 Args
as
               , Term -> Term -> Term
mkEqNats (Term -> Term
sucTerm Term
nt1) Term
nt0
               , Args -> ExtModalFORMULA -> Term
transMF Args
as2 ExtModalFORMULA
f ]
    FixedPoint _ _ -> String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ "transEMF: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ EM_FORMULA -> ShowS
forall a. Pretty a => a -> ShowS
showDoc EM_FORMULA
emf ""
  UntilSince isUntil :: Bool
isUntil f1 :: ExtModalFORMULA
f1 f2 :: ExtModalFORMULA
f2 r :: Range
r -> let
    nAs :: Args
nAs = Args
as { freeC :: Int
freeC = Int
fW Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 2 }
    [_, v2 :: VarDecl
v2] = Int -> [VarDecl]
vds 2
    [_, n2 :: VarDecl
n2] = Int -> [VarDecl]
nds 2
    [vt2 :: Term
vt2, nt2 :: Term
nt2] = (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl
v2, VarDecl
n2]
    as1 :: Args
as1 = Args
nAs { targetW :: Term
targetW = Term
vt1, targetN :: Term
targetN = Term
nt1 }
    as2 :: Args
as2 = Args
nAs { targetW :: Term
targetW = Term
vt2, targetN :: Term
targetN = Term
nt2 }
    in Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
r (Args -> Term
zPath Args
as)
      (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [GenVarDecl] -> Term -> Term
mkExQs ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl
v1, VarDecl
n1])
      (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
mkConj
      [ if Bool
isUntil then Term -> Term -> Args -> Term
mkZPath Term
vt0 Term
nt0 Args
as1 else Term -> Term -> Args -> Term
mkZPath Term
vt1 Term
nt1 Args
as
      , Args -> ExtModalFORMULA -> Term
transMF Args
as1 ExtModalFORMULA
f2
      , [GenVarDecl] -> Term -> Term
HC.mkForall ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl [VarDecl
v2, VarDecl
n2])
        (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
orId Range
r
        ([Term] -> Term
mkConj
        [ Id -> Range -> Term -> Term -> Term
mkLogTerm Id
orId Range
r
          (if Bool
isUntil then Term -> Term -> Args -> Term
mkZPath Term
vt0 Term
nt0 Args
as2 else Term -> Term -> Args -> Term
mkZPath Term
vt2 Term
nt2 Args
as)
          (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId Range
r (Term -> Term -> Term
eqW Term
vt0 Term
vt2)
          (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
mkEqNats Term
nt0 Term
nt2
        , if Bool
isUntil then Term -> Term -> Args -> Term
mkZPath Term
vt2 Term
nt2 Args
as1 else Term -> Term -> Args -> Term
mkZPath Term
vt1 Term
nt1 Args
as2 ])
        (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Args -> ExtModalFORMULA -> Term
transMF Args
as2 ExtModalFORMULA
f1 ]
  ModForm md :: ModDefn
md -> [Term] -> Term
mkConj ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ Args -> ModDefn -> [Term]
transModDefn Args
as ModDefn
md

resetArgs :: Term -> Args -> Args
resetArgs :: Term -> Args -> Args
resetArgs t :: Term
t as :: Args
as = Args
as
  { sourceW :: Term
sourceW = Term
t
  , targetW :: Term
targetW = Term
t
  , targetN :: Term
targetN = Term
zeroT }

transMod :: Args -> MODALITY -> Term
transMod :: Args -> MODALITY -> Term
transMod as :: Args
as md :: MODALITY
md = let
  t1 :: Term
t1 = Args -> Term
targetW Args
as
  t2 :: Term
t2 = Token -> Id -> Term
varTerm (String -> Int -> Token
genNumVar "w" (Int -> Token) -> Int -> Token
forall a b. (a -> b) -> a -> b
$ Args -> Int
nextW Args
as) Id
world
  vts :: [Term]
vts = [Term
t1, Term
t2]
  msig :: ExtModalSign
msig = Args -> ExtModalSign
modSig Args
as
  extInf :: EModalSign
extInf = ExtModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo ExtModalSign
msig
  timeMs :: Set Id
timeMs = EModalSign -> Set Id
timeMods EModalSign
extInf
  in case MODALITY
md of
  SimpleMod i :: Token
i -> let ri :: Id
ri = Token -> Id
simpleIdToId Token
i in Term -> [Term] -> Term
mkApplTerm
    (Id -> Type -> Term
mkOp (Bool -> Bool -> Id -> Id
relOfMod (Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
ri Set Id
timeMs) Bool
False Id
ri)
                    (Type -> Term) -> (PredType -> Type) -> PredType -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> Type
trPr (PredType -> Term) -> PredType -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Bool -> Id -> PredType
modPredType Id
world Bool
False Id
ri) [Term]
vts
  TermMod t :: TERM EM_FORMULA
t -> case TERM EM_FORMULA -> Maybe Id
forall f. TermExtension f => f -> Maybe Id
optTermSort TERM EM_FORMULA
t of
    Just srt :: Id
srt -> case ExtModalSign -> (Id -> Id) -> [Id] -> [Id]
forall f e a. Sign f e -> (a -> Id) -> [a] -> [a]
keepMinimals ExtModalSign
msig Id -> Id
forall a. a -> a
id ([Id] -> [Id]) -> (Set Id -> [Id]) -> Set Id -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Id -> [Id]
forall a. Set a -> [a]
Set.toList
      (Set Id -> [Id]) -> (Set Id -> Set Id) -> Set Id -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (EModalSign -> Set Id
termMods EModalSign
extInf) (Set Id -> Set Id) -> (Set Id -> Set Id) -> Set Id -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert Id
srt
      (Set Id -> [Id]) -> Set Id -> [Id]
forall a b. (a -> b) -> a -> b
$ Id -> ExtModalSign -> Set Id
forall f e. Id -> Sign f e -> Set Id
supersortsOf Id
srt ExtModalSign
msig of
      [] -> String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ "transMod1: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TERM EM_FORMULA -> ShowS
forall a. Pretty a => a -> ShowS
showDoc TERM EM_FORMULA
t ""
      st :: Id
st : _ -> Term -> [Term] -> Term
mkApplTerm
        (Id -> Type -> Term
mkOp (Bool -> Bool -> Id -> Id
relOfMod (Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
st Set Id
timeMs) Bool
True Id
st)
         (Type -> Term) -> (PredType -> Type) -> PredType -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> Type
trPr (PredType -> Term) -> PredType -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Bool -> Id -> PredType
modPredType Id
world Bool
True Id
st)
        ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ Record EM_FORMULA Term Term -> TERM EM_FORMULA -> Term
forall f a b. Record f a b -> TERM f -> b
foldTerm (Args -> String -> Record EM_FORMULA Term Term
trRecord (Term -> Args -> Args
resetArgs Term
t1 Args
as) (String -> Record EM_FORMULA Term Term)
-> String -> Record EM_FORMULA Term Term
forall a b. (a -> b) -> a -> b
$ TERM EM_FORMULA -> ShowS
forall a. Pretty a => a -> ShowS
showDoc TERM EM_FORMULA
t "") TERM EM_FORMULA
t Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
vts
    _ -> String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ "transMod2: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TERM EM_FORMULA -> ShowS
forall a. Pretty a => a -> ShowS
showDoc TERM EM_FORMULA
t ""
  Guard f :: ExtModalFORMULA
f -> let
    nf :: Int
nf = Args -> Int
freeC Args
as Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
    newAs :: Args
newAs = Args
as { freeC :: Int
freeC = Int
nf, freeZ :: Int
freeZ = Int
nf }
    zd :: VarDecl
zd = Args -> VarDecl
zDecl Args
newAs
    in [Term] -> Term
mkConj [Id -> Term -> Term -> Term
eqWorld Id
exEq Term
t1 Term
t2, [GenVarDecl] -> Term -> Term
HC.mkForall [VarDecl -> GenVarDecl
GenVarDecl VarDecl
zd] (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
mkConj
         [ Term -> VarDecl -> Term
pathAppl2 Term
t1 VarDecl
zd, Args -> ExtModalFORMULA -> Term
transMF (Term -> Args -> Args
resetArgs Term
t1 Args
newAs) ExtModalFORMULA
f ]]
  ModOp mOp :: ModOp
mOp m1 :: MODALITY
m1 m2 :: MODALITY
m2 -> case ModOp
mOp of
    Composition -> let
      nW :: Int
nW = Args -> Int
freeC Args
as Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
      nAs :: Args
nAs = Args
as { freeC :: Int
freeC = Int
nW }
      vd :: VarDecl
vd = Token -> Id -> VarDecl
varDecl (String -> Int -> Token
genNumVar "w" Int
nW) Id
world
      in VarDecl -> [Term] -> Term
mkExConj VarDecl
vd
           [ Args -> MODALITY -> Term
transMod Args
nAs { nextW :: Int
nextW = Int
nW } MODALITY
m1
           , Args -> MODALITY -> Term
transMod Args
nAs { targetW :: Term
targetW = VarDecl -> Term
QualVar VarDecl
vd } MODALITY
m2 ]
    Intersection -> [Term] -> Term
mkConj [Args -> MODALITY -> Term
transMod Args
as MODALITY
m1, Args -> MODALITY -> Term
transMod Args
as MODALITY
m2]
    Union -> [Term] -> Term
mkDisj [Args -> MODALITY -> Term
transMod Args
as MODALITY
m1, Args -> MODALITY -> Term
transMod Args
as MODALITY
m2]
    OrElse -> [Term] -> Term
mkDisj ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ [ExtModalFORMULA] -> Args -> [MODALITY] -> [Term]
transOrElse [] Args
as ([MODALITY] -> [Term]) -> [MODALITY] -> [Term]
forall a b. (a -> b) -> a -> b
$ MODALITY -> [MODALITY]
flatOrElse MODALITY
md
  TransClos m :: MODALITY
m -> Args -> MODALITY -> Term
transMod Args
as MODALITY
m -- ignore transitivity for now

flatOrElse :: MODALITY -> [MODALITY]
flatOrElse :: MODALITY -> [MODALITY]
flatOrElse md :: MODALITY
md = case MODALITY
md of
  ModOp OrElse m1 :: MODALITY
m1 m2 :: MODALITY
m2 -> MODALITY -> [MODALITY]
flatOrElse MODALITY
m1 [MODALITY] -> [MODALITY] -> [MODALITY]
forall a. [a] -> [a] -> [a]
++ MODALITY -> [MODALITY]
flatOrElse MODALITY
m2
  _ -> [MODALITY
md]

transOrElse :: [FORMULA EM_FORMULA] -> Args -> [MODALITY] -> [Term]
transOrElse :: [ExtModalFORMULA] -> Args -> [MODALITY] -> [Term]
transOrElse nFs :: [ExtModalFORMULA]
nFs as :: Args
as ms :: [MODALITY]
ms = case [MODALITY]
ms of
  [] -> []
  md :: MODALITY
md : r :: [MODALITY]
r -> case MODALITY
md of
    Guard f :: ExtModalFORMULA
f -> Args -> MODALITY -> Term
transMod Args
as (ExtModalFORMULA -> MODALITY
Guard (ExtModalFORMULA -> MODALITY)
-> ([ExtModalFORMULA] -> ExtModalFORMULA)
-> [ExtModalFORMULA]
-> MODALITY
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ExtModalFORMULA] -> ExtModalFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct ([ExtModalFORMULA] -> MODALITY) -> [ExtModalFORMULA] -> MODALITY
forall a b. (a -> b) -> a -> b
$ ExtModalFORMULA
f ExtModalFORMULA -> [ExtModalFORMULA] -> [ExtModalFORMULA]
forall a. a -> [a] -> [a]
: [ExtModalFORMULA]
nFs)
      Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [ExtModalFORMULA] -> Args -> [MODALITY] -> [Term]
transOrElse (ExtModalFORMULA -> ExtModalFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg ExtModalFORMULA
f ExtModalFORMULA -> [ExtModalFORMULA] -> [ExtModalFORMULA]
forall a. a -> [a] -> [a]
: [ExtModalFORMULA]
nFs) Args
as [MODALITY]
r
    _ -> Args -> MODALITY -> Term
transMod Args
as MODALITY
md Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [ExtModalFORMULA] -> Args -> [MODALITY] -> [Term]
transOrElse [ExtModalFORMULA]
nFs Args
as [MODALITY]
r

transModDefn :: Args -> ModDefn -> [Term]
transModDefn :: Args -> ModDefn -> [Term]
transModDefn as :: Args
as (ModDefn _ _ _ fs :: [Annoted FrameForm]
fs _) =
  (Annoted FrameForm -> [Term]) -> [Annoted FrameForm] -> [Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Annoted ExtModalFORMULA -> Term)
-> [Annoted ExtModalFORMULA] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Args -> ExtModalFORMULA -> Term
transMF Args
as (ExtModalFORMULA -> Term)
-> (Annoted ExtModalFORMULA -> ExtModalFORMULA)
-> Annoted ExtModalFORMULA
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted ExtModalFORMULA -> ExtModalFORMULA
forall a. Annoted a -> a
item) ([Annoted ExtModalFORMULA] -> [Term])
-> (Annoted FrameForm -> [Annoted ExtModalFORMULA])
-> Annoted FrameForm
-> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FrameForm -> [Annoted ExtModalFORMULA]
frameForms (FrameForm -> [Annoted ExtModalFORMULA])
-> (Annoted FrameForm -> FrameForm)
-> Annoted FrameForm
-> [Annoted ExtModalFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted FrameForm -> FrameForm
forall a. Annoted a -> a
item) [Annoted FrameForm]
fs