module CspCASLProver.TransProcesses
( transProcess
, VarSource (..)
) where
import qualified CASL.AS_Basic_CASL as CASL_AS_Basic_CASL
import CASL.Fold as CASL_Fold
import qualified CASL.Sign as CASL_Sign
import qualified CASL.Simplify as CASL_Simplify
import Common.Id (tokStr)
import Common.Result (propagateErrors)
import Common.Utils (number)
import qualified Comorphisms.CASL2PCFOL as CASL2PCFOL
import qualified Comorphisms.CASL2SubCFOL as CASL2SubCFOL
import qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL
import CspCASL.AS_CspCASL_Process
import CspCASL.SignCSP (CspCASLSign, ccSig2CASLSign)
import CspCASL.StatAnaCSP (getDeclaredChanSort)
import CspCASLProver.Consts
import CspCASLProver.CspProverConsts
import qualified Data.Set as Set
import qualified Data.Map as Map
import Isabelle.IsaSign
import Isabelle.IsaConsts
data VarSource
= PrefixChoice
| ChanSendOrRec CASL_AS_Basic_CASL.SORT
| GlobalParameter
data SortTarget
= NormalComm
| ChanComm CASL_AS_Basic_CASL.SORT
data TermTarget
= TermPrefix
| ChanSendOrParam CASL_AS_Basic_CASL.SORT
type VSM = Map.Map CASL_AS_Basic_CASL.VAR VarSource
transProcess :: CspCASLSign -> CASL_Sign.Sign () () ->
CASL_Sign.Sign () () -> VSM -> PROCESS -> Term
transProcess :: CspCASLSign -> Sign () () -> Sign () () -> VSM -> PROCESS -> Term
transProcess ccSign :: CspCASLSign
ccSign pcfolSign :: Sign () ()
pcfolSign cfolSign :: Sign () ()
cfolSign vsm :: VSM
vsm pr :: PROCESS
pr =
let
transFormula' :: VSM -> FORMULA () -> Term
transFormula' = Sign () () -> Sign () () -> VSM -> FORMULA () -> Term
transFormula Sign () ()
pcfolSign Sign () ()
cfolSign
transProcess' :: VSM -> PROCESS -> Term
transProcess' =
CspCASLSign -> Sign () () -> Sign () () -> VSM -> PROCESS -> Term
transProcess CspCASLSign
ccSign Sign () ()
pcfolSign Sign () ()
cfolSign
caslSign :: Sign () ()
caslSign = CspCASLSign -> Sign () ()
ccSig2CASLSign CspCASLSign
ccSign
in case PROCESS
pr of
Skip _ -> Term
cspProver_skipOp
Stop _ -> Term
cspProver_stopOp
Div _ -> Term
cspProver_divOp
Run _ _ -> String -> Term
conDouble "RunNotSupportedYet"
Chaos _ _ -> String -> Term
conDouble "ChaosNotSupportedYet"
NamedProcess fqpn :: FQ_PROCESS_NAME
fqpn fqParams :: [TERM ()]
fqParams _ ->
let
pnTerm :: Term
pnTerm = String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ FQ_PROCESS_NAME -> String
convertFQProcessName2String FQ_PROCESS_NAME
fqpn
transParam :: (TERM (), b) -> Term
transParam (term :: TERM ()
term, _) =
let termTar :: TermTarget
termTar = SORT -> TermTarget
ChanSendOrParam (SORT -> TermTarget) -> SORT -> TermTarget
forall a b. (a -> b) -> a -> b
$
String -> SORT
forall a. HasCallStack => String -> a
error "NYI: CspCASLProver.TransProcesses.transProcess: Not updated for new signatures yet"
in Sign () ()
-> Sign () () -> Sign () () -> VSM -> TermTarget -> TERM () -> Term
transCASLTerm Sign () ()
caslSign Sign () ()
pcfolSign Sign () ()
cfolSign
VSM
vsm TermTarget
termTar TERM ()
term
paramTerms :: [Term]
paramTerms = ((TERM (), Int) -> Term) -> [(TERM (), Int)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (TERM (), Int) -> Term
forall b. (TERM (), b) -> Term
transParam ([(TERM (), Int)] -> [Term]) -> [(TERM (), Int)] -> [Term]
forall a b. (a -> b) -> a -> b
$ [TERM ()] -> [(TERM (), Int)]
forall a. [a] -> [(a, Int)]
number [TERM ()]
fqParams
in Term -> Term
cspProver_NamedProcOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ if [TERM ()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TERM ()]
fqParams
then Term
pnTerm
else (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term -> Term -> Term
termAppl Term
pnTerm [Term]
paramTerms
ConditionalProcess fqFormula :: FORMULA ()
fqFormula p :: PROCESS
p q :: PROCESS
q _ ->
Term -> Term -> Term -> Term
cspProver_conditionalOp (VSM -> FORMULA () -> Term
transFormula' VSM
vsm FORMULA ()
fqFormula)
(VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
(VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
Hiding {} -> String -> Term
conDouble "HidingNotSupportedYet"
RenamingProcess {} -> String -> Term
conDouble "RenamingNotSupportedYet"
Sequential p :: PROCESS
p q :: PROCESS
q _ ->
Term -> Term -> Term
cspProver_sequenceOp (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p) (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
PrefixProcess ev :: EVENT
ev p :: PROCESS
p _ ->
CspCASLSign
-> Sign () () -> Sign () () -> VSM -> EVENT -> PROCESS -> Term
transEvent CspCASLSign
ccSign Sign () ()
pcfolSign Sign () ()
cfolSign VSM
vsm EVENT
ev PROCESS
p
InternalChoice p :: PROCESS
p q :: PROCESS
q _ ->
Term -> Term -> Term
cspProver_internal_choiceOp (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
(VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
ExternalChoice p :: PROCESS
p q :: PROCESS
q _ ->
Term -> Term -> Term
cspProver_external_choiceOp (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
(VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
Interleaving p :: PROCESS
p q :: PROCESS
q _ ->
Term -> Term -> Term
cspProver_interleavingOp (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
(VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
SynchronousParallel p :: PROCESS
p q :: PROCESS
q _ ->
Term -> Term -> Term
cspProver_synchronousOp (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
(VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
GeneralisedParallel p :: PROCESS
p es :: EVENT_SET
es q :: PROCESS
q _ ->
Term -> Term -> Term -> Term
cspProver_general_parallelOp (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
(EVENT_SET -> Term
transEventSet EVENT_SET
es)
(VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
AlphabetisedParallel p :: PROCESS
p les :: EVENT_SET
les res :: EVENT_SET
res q :: PROCESS
q _ ->
Term -> Term -> Term -> Term -> Term
cspProver_alphabetised_parallelOp (VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
(EVENT_SET -> Term
transEventSet EVENT_SET
les)
(EVENT_SET -> Term
transEventSet EVENT_SET
res)
(VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
q)
FQProcess p :: PROCESS
p _ _ ->
VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p
transEventSet :: EVENT_SET -> Term
transEventSet :: EVENT_SET -> Term
transEventSet (EventSet comms :: [CommType]
comms _) =
if [CommType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CommType]
comms then String -> Term
forall a. HasCallStack => String -> a
error "transEventSet" else
(Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Term -> Term -> Term
binUnion ((CommType -> Term) -> [CommType] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map CommType -> Term
transCommType [CommType]
comms)
transCommType :: CommType -> Term
transCommType :: CommType -> Term
transCommType comm :: CommType
comm =
case CommType
comm of
CommTypeSort sort :: SORT
sort -> SortTarget -> SORT -> Term
transSort SortTarget
NormalComm SORT
sort
CommTypeChan typedChanName :: TypedChanName
typedChanName ->
case TypedChanName
typedChanName of
TypedChanName cn :: SORT
cn _ -> Term -> Term
rangeOp (String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> String
convertChannelString SORT
cn)
transEvent :: CspCASLSign -> CASL_Sign.Sign () () ->
CASL_Sign.Sign () () -> VSM ->
EVENT -> PROCESS -> Term
transEvent :: CspCASLSign
-> Sign () () -> Sign () () -> VSM -> EVENT -> PROCESS -> Term
transEvent ccSign :: CspCASLSign
ccSign pcfolSign :: Sign () ()
pcfolSign cfolSign :: Sign () ()
cfolSign vsm :: VSM
vsm event :: EVENT
event p :: PROCESS
p =
let
transProcess' :: VSM -> PROCESS -> Term
transProcess' = CspCASLSign -> Sign () () -> Sign () () -> VSM -> PROCESS -> Term
transProcess CspCASLSign
ccSign Sign () ()
pcfolSign Sign () ()
cfolSign
caslSign :: Sign () ()
caslSign = CspCASLSign -> Sign () ()
ccSig2CASLSign CspCASLSign
ccSign
transCASLTerm' :: VSM -> TermTarget -> TERM () -> Term
transCASLTerm' = Sign () ()
-> Sign () () -> Sign () () -> VSM -> TermTarget -> TERM () -> Term
transCASLTerm Sign () ()
caslSign Sign () ()
pcfolSign Sign () ()
cfolSign
in case EVENT
event of
FQTermEvent t :: TERM ()
t _ ->
Term -> Term -> Term
cspProver_action_prefixOp (VSM -> TermTarget -> TERM () -> Term
transCASLTerm' VSM
vsm TermTarget
TermPrefix TERM ()
t)
(VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
FQExternalPrefixChoice fqVar :: TERM ()
fqVar _ ->
let (varName :: VAR
varName, varSort :: SORT
varSort) = TERM () -> (VAR, SORT)
splitCASLVar TERM ()
fqVar
in Term -> Term -> Term -> Term
cspProver_internal_prefix_choiceOp (VAR -> Term
transVar VAR
varName)
(SortTarget -> SORT -> Term
transSort SortTarget
NormalComm SORT
varSort)
(VSM -> PROCESS -> Term
transProcess' (VAR -> VarSource -> VSM -> VSM
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VAR
varName VarSource
PrefixChoice VSM
vsm) PROCESS
p)
FQInternalPrefixChoice fqVar :: TERM ()
fqVar _ ->
let (varName :: VAR
varName, varSort :: SORT
varSort) = TERM () -> (VAR, SORT)
splitCASLVar TERM ()
fqVar
in Term -> Term -> Term -> Term
cspProver_external_prefix_choiceOp (VAR -> Term
transVar VAR
varName)
(SortTarget -> SORT -> Term
transSort SortTarget
NormalComm SORT
varSort)
(VSM -> PROCESS -> Term
transProcess' (VAR -> VarSource -> VSM -> VSM
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VAR
varName VarSource
PrefixChoice VSM
vsm) PROCESS
p)
FQChanSend (chanName :: SORT
chanName, chanSort :: SORT
chanSort) t :: TERM ()
t _ ->
Term -> Term -> Term -> Term
cspProver_chan_sendOp (SORT -> Term
transChanName SORT
chanName)
(VSM -> TermTarget -> TERM () -> Term
transCASLTerm' VSM
vsm (SORT -> TermTarget
ChanSendOrParam SORT
chanSort) TERM ()
t)
(VSM -> PROCESS -> Term
transProcess' VSM
vsm PROCESS
p)
FQChanNonDetSend (chanName :: SORT
chanName, chanSort :: SORT
chanSort) fqVar :: TERM ()
fqVar _ ->
let declaredChanSort :: SORT
declaredChanSort = String -> Result SORT -> SORT
forall a. String -> Result a -> a
propagateErrors
"CspCASLProver.TransProcesses.transEvent1"
(Result SORT -> SORT) -> Result SORT -> SORT
forall a b. (a -> b) -> a -> b
$ (SORT, SORT) -> CspCASLSign -> Result SORT
getDeclaredChanSort (SORT
chanName, SORT
chanSort) CspCASLSign
ccSign
(varName :: VAR
varName, varSort :: SORT
varSort) = TERM () -> (VAR, SORT)
splitCASLVar TERM ()
fqVar
in Term -> Term -> Term -> Term -> Term
cspProver_chan_nondeterministic_sendOp (SORT -> Term
transChanName SORT
chanName)
(VAR -> Term
transVar VAR
varName)
(SortTarget -> SORT -> Term
transSort (SORT -> SortTarget
ChanComm SORT
declaredChanSort) SORT
varSort)
(VSM -> PROCESS -> Term
transProcess' (VAR -> VarSource -> VSM -> VSM
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VAR
varName
(SORT -> VarSource
ChanSendOrRec SORT
declaredChanSort) VSM
vsm) PROCESS
p)
FQChanRecv (chanName :: SORT
chanName, chanSort :: SORT
chanSort) fqVar :: TERM ()
fqVar _ ->
let declaredChanSort :: SORT
declaredChanSort = String -> Result SORT -> SORT
forall a. String -> Result a -> a
propagateErrors
"CspCASLProver.TransProcesses.transEvent2"
(Result SORT -> SORT) -> Result SORT -> SORT
forall a b. (a -> b) -> a -> b
$ (SORT, SORT) -> CspCASLSign -> Result SORT
getDeclaredChanSort (SORT
chanName, SORT
chanSort) CspCASLSign
ccSign
(varName :: VAR
varName, varSort :: SORT
varSort) = TERM () -> (VAR, SORT)
splitCASLVar TERM ()
fqVar
in Term -> Term -> Term -> Term -> Term
cspProver_chan_recOp (SORT -> Term
transChanName SORT
chanName) (VAR -> Term
transVar VAR
varName)
(SortTarget -> SORT -> Term
transSort (SORT -> SortTarget
ChanComm SORT
declaredChanSort) SORT
varSort)
(VSM -> PROCESS -> Term
transProcess' (VAR -> VarSource -> VSM -> VSM
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VAR
varName
(SORT -> VarSource
ChanSendOrRec SORT
declaredChanSort) VSM
vsm) PROCESS
p)
_ -> String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ "CspCASLProver.TransProcesses.transEvent: "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ "Expected a FQEvent not a non-FQEvent"
transVar :: CASL_AS_Basic_CASL.VAR -> Term
transVar :: VAR -> Term
transVar v :: VAR
v = String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ VAR -> String
tokStr VAR
v
transSort :: SortTarget -> CASL_AS_Basic_CASL.SORT -> Term
transSort :: SortTarget -> SORT -> Term
transSort target :: SortTarget
target s :: SORT
s =
let sBar :: Term
sBar = String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> String
mkSortBarString SORT
s
in case SortTarget
target of
NormalComm -> Term -> Term -> Term
binImageOp (String -> Term
conDouble String
flatS) Term
sBar
ChanComm t :: SORT
t -> Term -> Term -> Term
binImageOp
(String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> String
mkSortBarAbsString SORT
t) Term
sBar
transChanName :: CHANNEL_NAME -> Term
transChanName :: SORT -> Term
transChanName chanName :: SORT
chanName =
String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> String
convertChannelString SORT
chanName
cspCaslTransRecord :: CASL_Sign.Sign f e -> Set.Set String ->
CFOL2IsabelleHOL.FormulaTranslator f e ->
Set.Set String -> VSM -> Record f Term Term
cspCaslTransRecord :: Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> VSM
-> Record f Term Term
cspCaslTransRecord caslSign :: Sign f e
caslSign tyToks :: Set String
tyToks trForm :: FormulaTranslator f e
trForm strs :: Set String
strs vsm :: VSM
vsm =
(Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> Record f Term Term
forall f e.
Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> Record f Term Term
CFOL2IsabelleHOL.transRecord Sign f e
caslSign Set String
tyToks FormulaTranslator f e
trForm Set String
strs)
{ foldQual_var :: TERM f -> VAR -> SORT -> Range -> Term
foldQual_var = \ _ v :: VAR
v s :: SORT
s _ ->
let v' :: Term
v' = String -> Term
mkFree (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ Set String -> VAR -> String
CFOL2IsabelleHOL.transVar Set String
strs VAR
v
in case VAR -> VSM -> Maybe VarSource
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VAR
v VSM
vsm of
Nothing ->
String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ "CspCASLProver.TransProcesses.cspCaslTransRecord: Variable not found in vsm:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ VAR -> String
forall a. Show a => a -> String
show VAR
v
Just varSource :: VarSource
varSource ->
case VarSource
varSource of
PrefixChoice -> SORT -> Term -> Term
mkChooseFunOp SORT
s (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
projFlatOp Term
v'
ChanSendOrRec declaredChanSort :: SORT
declaredChanSort ->
SORT -> Term -> Term
mkChooseFunOp SORT
s (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> Term -> Term
mkSortBarRepOp SORT
declaredChanSort Term
v'
GlobalParameter -> SORT -> Term -> Term
mkChooseFunOp SORT
s (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> Term -> Term
mkSortBarRepOp SORT
s Term
v'
}
transCASLTerm :: CASL_Sign.Sign () () -> CASL_Sign.Sign () () ->
CASL_Sign.Sign () () -> VSM -> TermTarget ->
CASL_AS_Basic_CASL.TERM () -> Term
transCASLTerm :: Sign () ()
-> Sign () () -> Sign () () -> VSM -> TermTarget -> TERM () -> Term
transCASLTerm caslSign :: Sign () ()
caslSign pcfolSign :: Sign () ()
pcfolSign cfolSign :: Sign () ()
cfolSign vsm :: VSM
vsm termTarget :: TermTarget
termTarget caslTerm :: TERM ()
caslTerm =
let strs :: Set String
strs = Sign () () -> Set String
forall f e. Sign f e -> Set String
CFOL2IsabelleHOL.getAssumpsToks Sign () ()
caslSign
in case TERM ()
caslTerm of
CASL_AS_Basic_CASL.Qual_var v :: VAR
v s :: SORT
s _ ->
let v' :: Term
v' = String -> Term
mkFree (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ Set String -> VAR -> String
CFOL2IsabelleHOL.transVar Set String
strs VAR
v
in case TermTarget
termTarget of
TermPrefix ->
case VAR -> VSM -> Maybe VarSource
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VAR
v VSM
vsm of
Nothing -> String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$
"CspCASLProver.TransProcesses.transTerm: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
"Variable not found in vsm:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ VAR -> String
forall a. Show a => a -> String
show VAR
v
Just varSource :: VarSource
varSource ->
case VarSource
varSource of
PrefixChoice -> Term
v'
ChanSendOrRec declaredChanSort :: SORT
declaredChanSort ->
Term -> Term
flatOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> Term -> Term
mkSortBarRepOp SORT
declaredChanSort Term
v'
GlobalParameter -> Term -> Term
flatOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> Term -> Term
mkSortBarRepOp SORT
s Term
v'
ChanSendOrParam t :: SORT
t ->
case VAR -> VSM -> Maybe VarSource
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VAR
v VSM
vsm of
Nothing -> String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$
"CspCASLProver.TransProcesses.transTerm: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
"Variable not found in vsm:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ VAR -> String
forall a. Show a => a -> String
show VAR
v
Just varSource :: VarSource
varSource ->
case VarSource
varSource of
PrefixChoice ->
SORT -> Term -> Term
mkSortBarAbsOp SORT
t (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
projFlatOp Term
v'
ChanSendOrRec declaredChanSort :: SORT
declaredChanSort ->
if SORT
declaredChanSort SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
t
then Term
v'
else SORT -> Term -> Term
mkSortBarAbsOp SORT
t (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
SORT -> Term -> Term
mkSortBarRepOp SORT
declaredChanSort Term
v'
GlobalParameter ->
if SORT
s SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
t
then Term
v'
else SORT -> Term -> Term
mkSortBarAbsOp SORT
t (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
SORT -> Term -> Term
mkSortBarRepOp SORT
s Term
v'
_ -> let sort :: SORT
sort = TERM () -> SORT
forall f. TermExtension f => f -> SORT
CASL_Sign.sortOfTerm TERM ()
caslTerm
constructor :: Term -> Term
constructor = SORT -> Term -> Term
mkPreAlphabetConstructorOp SORT
sort
isaCaslTerm :: Term
isaCaslTerm = Term -> Term
classOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
constructor (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
Sign () () -> Sign () () -> VSM -> TERM () -> Term
transCaslTermComputation Sign () ()
pcfolSign Sign () ()
cfolSign
VSM
vsm TERM ()
caslTerm
in case TermTarget
termTarget of
TermPrefix -> Term -> Term
flatOp Term
isaCaslTerm
ChanSendOrParam t :: SORT
t -> SORT -> Term -> Term
mkSortBarAbsOp SORT
t Term
isaCaslTerm
transCaslTermComputation :: CASL_Sign.Sign () () -> CASL_Sign.Sign () () ->
VSM -> CASL_AS_Basic_CASL.TERM () -> Term
transCaslTermComputation :: Sign () () -> Sign () () -> VSM -> TERM () -> Term
transCaslTermComputation pcfolSign :: Sign () ()
pcfolSign cfolSign :: Sign () ()
cfolSign vsm :: VSM
vsm term :: TERM ()
term =
let
rmSub :: TERM () -> TERM ()
rmSub = TERM () -> TERM ()
forall f. TermExtension f => TERM f -> TERM f
CASL2PCFOL.t2Term
termNoSub :: TERM ()
termNoSub = TERM () -> TERM ()
rmSub TERM ()
term
b :: Bool
b = Bool
True
fbsrts :: Set SORT
fbsrts = TERM () -> Set SORT
forall f. TERM f -> Set SORT
CASL2SubCFOL.botTermSorts TERM ()
termNoSub
bsrts :: Set SORT
bsrts = FormulaTreatment -> Sign () () -> Set SORT -> Set SORT
forall f e. FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
CASL2SubCFOL.sortsWithBottom FormulaTreatment
CASL2SubCFOL.FormulaDependent
Sign () ()
pcfolSign Set SORT
fbsrts
rmPartial :: TERM () -> TERM ()
rmPartial = (() -> ()) -> TERM () -> TERM ()
forall f. Ord f => (f -> f) -> TERM f -> TERM f
CASL_Simplify.simplifyTerm () -> ()
forall a. a -> a
id (TERM () -> TERM ()) -> (TERM () -> TERM ()) -> TERM () -> TERM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Bool -> Set SORT -> TERM () -> TERM ()
CASL2SubCFOL.codeTerm Bool
b Set SORT
bsrts
tyToks :: Set String
tyToks = Sign () () -> Set String
forall f e. Sign f e -> Set String
CFOL2IsabelleHOL.typeToks Sign () ()
cfolSign
trForm :: FormulaTranslator () ()
trForm = FormulaTranslator () ()
CFOL2IsabelleHOL.formTrCASL
strs :: Set String
strs = Sign () () -> Set String
forall f e. Sign f e -> Set String
CFOL2IsabelleHOL.getAssumpsToks Sign () ()
cfolSign
toIsabelle :: TERM () -> Term
toIsabelle = Record () Term Term -> TERM () -> Term
forall f a b. Record f a b -> TERM f -> b
foldTerm (Record () Term Term -> TERM () -> Term)
-> Record () Term Term -> TERM () -> Term
forall a b. (a -> b) -> a -> b
$ Sign () ()
-> Set String
-> FormulaTranslator () ()
-> Set String
-> VSM
-> Record () Term Term
forall f e.
Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> VSM
-> Record f Term Term
cspCaslTransRecord Sign () ()
cfolSign
Set String
tyToks FormulaTranslator () ()
trForm Set String
strs VSM
vsm
in TERM () -> Term
toIsabelle (TERM () -> Term) -> TERM () -> Term
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM ()
rmPartial TERM ()
termNoSub
transFormula :: CASL_Sign.Sign () () -> CASL_Sign.Sign () () -> VSM ->
CASL_AS_Basic_CASL.FORMULA () -> Term
transFormula :: Sign () () -> Sign () () -> VSM -> FORMULA () -> Term
transFormula pcfolSign :: Sign () ()
pcfolSign cfolSign :: Sign () ()
cfolSign vsm :: VSM
vsm formula :: FORMULA ()
formula =
let
rmSub :: FORMULA () -> FORMULA ()
rmSub = FORMULA () -> FORMULA ()
forall f. TermExtension f => FORMULA f -> FORMULA f
CASL2PCFOL.f2Formula
formulaNoSub :: FORMULA ()
formulaNoSub = FORMULA () -> FORMULA ()
rmSub FORMULA ()
formula
b :: Bool
b = Bool
True
fbsrts :: Set SORT
fbsrts = FORMULA () -> Set SORT
forall f. FORMULA f -> Set SORT
CASL2SubCFOL.botFormulaSorts FORMULA ()
formulaNoSub
bsrts :: Set SORT
bsrts = FormulaTreatment -> Sign () () -> Set SORT -> Set SORT
forall f e. FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
CASL2SubCFOL.sortsWithBottom FormulaTreatment
CASL2SubCFOL.FormulaDependent
Sign () ()
pcfolSign Set SORT
fbsrts
rmPartial :: FORMULA () -> FORMULA ()
rmPartial = (() -> ()) -> FORMULA () -> FORMULA ()
forall f. Ord f => (f -> f) -> FORMULA f -> FORMULA f
CASL_Simplify.simplifyFormula () -> ()
forall a. a -> a
id (FORMULA () -> FORMULA ())
-> (FORMULA () -> FORMULA ()) -> FORMULA () -> FORMULA ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Bool -> Set SORT -> FORMULA () -> FORMULA ()
CASL2SubCFOL.codeFormula Bool
b Set SORT
bsrts
tyToks :: Set String
tyToks = Sign () () -> Set String
forall f e. Sign f e -> Set String
CFOL2IsabelleHOL.typeToks Sign () ()
cfolSign
trForm :: FormulaTranslator () ()
trForm = FormulaTranslator () ()
CFOL2IsabelleHOL.formTrCASL
strs :: Set String
strs = Sign () () -> Set String
forall f e. Sign f e -> Set String
CFOL2IsabelleHOL.getAssumpsToks Sign () ()
cfolSign
toIsabelle :: FORMULA () -> Term
toIsabelle = Record () Term Term -> FORMULA () -> Term
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record () Term Term -> FORMULA () -> Term)
-> Record () Term Term -> FORMULA () -> Term
forall a b. (a -> b) -> a -> b
$ Sign () ()
-> Set String
-> FormulaTranslator () ()
-> Set String
-> VSM
-> Record () Term Term
forall f e.
Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> VSM
-> Record f Term Term
cspCaslTransRecord Sign () ()
cfolSign
Set String
tyToks FormulaTranslator () ()
trForm Set String
strs VSM
vsm
in FORMULA () -> Term
toIsabelle (FORMULA () -> Term) -> FORMULA () -> Term
forall a b. (a -> b) -> a -> b
$ FORMULA () -> FORMULA ()
rmPartial FORMULA ()
formulaNoSub