1b353d403dbdb365ae93a568f32b3ebf5698cab5Ewaryst SchulzDescription : OMDoc-to-CASL conversion
1a5414972199f27756b513d5cf515e4c0d688c08Ewaryst SchulzCopyright : (c) Ewaryst Schulz, DFKI Bremen 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
1a5414972199f27756b513d5cf515e4c0d688c08Ewaryst SchulzMaintainer : ewaryst.schulz@dfki.de
1a5414972199f27756b513d5cf515e4c0d688c08Ewaryst SchulzStability : provisional
1b353d403dbdb365ae93a568f32b3ebf5698cab5Ewaryst SchulzPortability : portable
1b353d403dbdb365ae93a568f32b3ebf5698cab5Ewaryst SchulzCASL implementation of the interface functions omdocToSym, omdocToSen
1b353d403dbdb365ae93a568f32b3ebf5698cab5Ewaryst Schulz, addOMadtToTheory, addOmdocToTheory from class Logic. The actual
1b353d403dbdb365ae93a568f32b3ebf5698cab5Ewaryst Schulzinstantiation can be found in module "CASL.Logic_CASL".
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz , addOMadtToTheory
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz , addOmdocToTheory
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst Schulzimport qualified Common.Lib.Rel as Rel
1a5414972199f27756b513d5cf515e4c0d688c08Ewaryst Schulzimport qualified Data.Map as Map
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz-- * Environment Interface
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulztype Env = SigMapI Symbol
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzsymbolToSort :: Symbol -> SORT
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzsymbolToSort (Symbol n SortAsItemType) = n
e34e60cc42e3a4bef64b18dbca61ff560d7cd279Ewaryst SchulzsymbolToSort s = error $ "symbolToSort: Nonsort encountered: " ++ show s
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzsymbolToOp :: Symbol -> (Id, OpType)
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzsymbolToOp (Symbol n (OpAsItemType ot)) = (n, ot)
e34e60cc42e3a4bef64b18dbca61ff560d7cd279Ewaryst SchulzsymbolToOp s = error $ "symbolToOp: Nonop encountered: " ++ show s
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzsymbolToPred :: Symbol -> (Id, PredType)
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzsymbolToPred (Symbol n (PredAsItemType pt)) = (n, pt)
e34e60cc42e3a4bef64b18dbca61ff560d7cd279Ewaryst SchulzsymbolToPred s = error $ "symbolToPred: Nonpred encountered: " ++ show s
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzlookupSymbol :: Env -> OMName -> Symbol
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzlookupSymbol e omn =
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz (error $ concat [ "lookupSymbol failed for: "
aae33d0d1a0f8174a7a704e2fdbb29482e0bf587Ewaryst Schulz , show omn, "\nmap: ", show $ sigMapISymbs e])
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz omn $ sigMapISymbs e
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzlookupSort :: Env -> OMName -> SORT
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzlookupSort e = symbolToSort . lookupSymbol e
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzlookupSortOMS :: String -> Env -> OMElement -> SORT
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzlookupSortOMS msg = lookupOMS lookupSort $ msg ++ "(SORT)"
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzlookupPred :: Env -> OMName -> (Id, PredType)
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzlookupPred e = symbolToPred . lookupSymbol e
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzlookupPredOMS :: String -> Env -> OMElement -> (Id, PredType)
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzlookupPredOMS msg = lookupOMS lookupPred $ msg ++ "(PRED)"
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulzlookupOp :: Env -> OMName -> (Id, OpType)
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulzlookupOp e = symbolToOp . lookupSymbol e
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulzlookupOpOMS :: String -> Env -> OMElement -> (Id, OpType)
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulzlookupOpOMS msg = lookupOMS lookupOp $ msg ++ "(Op)"
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzlookupOMS :: (Env -> OMName -> a) -> String -> Env -> OMElement -> a
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzlookupOMS f msg e oms@(OMS (cd, omn)) =
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz if cdIsEmpty cd then f e omn
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz else error $ concat [ msg, ": lookupOMS: Nonempty cd in const: "
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzlookupOMS _ msg _ ome =
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz error $ concat [msg, ": lookupOMS: Nonsymbol: ", show ome]
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulztoOpSymb :: (Id, OpType) -> OP_SYMB
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulztoOpSymb (i, t) = Qual_op_name i (toOP_TYPE t) nullRange
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulztoPredSymb :: (Id, PredType) -> PRED_SYMB
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulztoPredSymb (i, t) = Qual_pred_name i (toPRED_TYPE t) nullRange
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz-- * TOPLEVEL Interface
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz-- | A TCSymbols is transformed to a CASL symbol with given name.
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzomdocToSym :: Env -> TCElement -> String -> Result Symbol
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzomdocToSym e sym@(TCSymbol _ ctp srole _) n =
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz case srole of
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz Typ | ctp == const_sort -> return $ idToSortSymbol $ nameToId n
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz | otherwise -> fail $ "omdocToSym: No sorttype for " ++ show sym
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz Obj -> return $
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz case omdocToType e ctp of
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz Left ot -> idToOpSymbol (nameToId n) ot
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz Right pt -> idToPredSymbol (nameToId n) pt
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz _ -> fail $ concat [ "omdocToSym: only type or object are allowed as"
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz , " symbol roles, but found: ", show srole ]
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzomdocToSym _ sym _ = fail $ concat [ "omdocToSym: only TCSymbol is allowed,"
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz , " but found: ", show sym ]
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzomdocToSen :: Env -> TCElement -> String
1a5414972199f27756b513d5cf515e4c0d688c08Ewaryst Schulz -> Result (Maybe (Named (FORMULA f)))
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzomdocToSen e (TCSymbol _ t sr _) n =
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz case nameDecode n of
7191d84bd3c083d9abcf34a09390dc4e5f6079acEwaryst Schulz return Nothing -- don't translate encoded names here
7191d84bd3c083d9abcf34a09390dc4e5f6079acEwaryst Schulz let ns = makeNamed n $ omdocToFormula e t
7191d84bd3c083d9abcf34a09390dc4e5f6079acEwaryst Schulz res b = return $ Just $ ns { isAxiom = b }
7191d84bd3c083d9abcf34a09390dc4e5f6079acEwaryst Schulz in case sr of
7191d84bd3c083d9abcf34a09390dc4e5f6079acEwaryst Schulz Axiom -> res True
7191d84bd3c083d9abcf34a09390dc4e5f6079acEwaryst Schulz Theorem -> res False
7191d84bd3c083d9abcf34a09390dc4e5f6079acEwaryst Schulz _ -> return Nothing
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzomdocToSen _ sym _ = fail $ concat [ "omdocToSen: only TCSymbol is allowed,"
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz , " but found: ", show sym ]
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz-- | Sort generation constraints are added as named formulas.
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzaddOMadtToTheory :: Env
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz -> (Sign f e, [Named (FORMULA f)]) -> [[OmdADT]]
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz -> Result (Sign f e, [Named (FORMULA f)])
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzaddOMadtToTheory e (sig, nsens) adts = do
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz sgcs <- mapR (omdocToSortGenConstraint e) adts
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz return (sig, nsens ++ sgcs)
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz-- | The subsort relation is recovered from exported sentences.
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst SchulzaddOmdocToTheory :: Env -> (Sign f e, [Named (FORMULA f)]) -> [TCElement]
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz -> Result (Sign f e, [Named (FORMULA f)])
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst SchulzaddOmdocToTheory e (sig, nsens) tcs = do
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst Schulz srel <- omdocToSortRel e tcs
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder return (sig { sortRel = Rel.transClosure srel }, nsens)
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz-- * Algebraic Data Types
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzomdocToSortGenConstraint :: Env -> [OmdADT] -> Result (Named (FORMULA f))
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzomdocToSortGenConstraint e sortdefs = do
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz -- take the last type as the type of all constraints
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz let (t, cs) = mapAccumL (const $ mkConstraint e) Generated sortdefs
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz -- TODO: do we take newSort or origSort?
eae727f2a1203f1e3c86e40667fe6dfb1173abcbcmaeder return $ toSortGenNamed (mkSort_gen_ax cs $ t == Free) $ map newSort cs
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzmkConstraint :: Env -> OmdADT -> (ADTType, Constraint)
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzmkConstraint e (ADTSortDef nm t constrs) =
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz let s = lookupSort e $ mkSimpleName nm
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz l = map (mkConstructor e s) constrs
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz in (t, Constraint s l s)
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzmkConstraint _ _ = error "mkConstraint: Malformed ADT expression"
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzmkConstructor :: Env -> SORT -> OmdADT -> (OP_SYMB, [Int])
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzmkConstructor e s (ADTConstr nm args) =
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz let opn = nameToId $ lookupNotation e $ mkSimpleName nm
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz l = map (mkArg e) args
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz in (Qual_op_name opn (Op_type Total l s nullRange) nullRange, [0])
ad4da9d870c666f00992431e3badbbe9cc4f19aaChristian Maeder{- we have to create the name of this injection because we throw it away
ad4da9d870c666f00992431e3badbbe9cc4f19aaChristian Maederduring the export -}
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzmkConstructor e s (ADTInsort (_, omn)) =
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz let argsort = lookupSort e omn
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz opn = mkUniqueInjName argsort s
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz in (Qual_op_name opn (Op_type Total [argsort] s nullRange) nullRange, [0])
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzmkConstructor _ _ _ = error "mkConstructor: Malformed ADT expression"
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzmkArg :: Env -> OmdADT -> SORT
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzmkArg e (ADTArg oms _) = lookupSortOMS "mkArg" e oms
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst SchulzmkArg _ _ = error "mkArg: Malformed ADT expression"
59ff8134f94a323b1a6fe967bb687cccf068d9c2Ewaryst Schulz-- * Subsort Relation
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst SchulzomdocToSortRel :: Env -> [TCElement] -> Result (Rel.Rel SORT)
ad4da9d870c666f00992431e3badbbe9cc4f19aaChristian MaederomdocToSortRel e = foldM (addMaybeToSortRel e) Rel.empty
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst SchulzaddMaybeToSortRel :: Env -> Rel.Rel SORT -> TCElement -> Result (Rel.Rel SORT)
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst SchulzaddMaybeToSortRel e r (TCSymbol n (OMA [sof, oms1, oms2]) Axiom _) =
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst Schulz case nameDecode n of
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst Schulz Just ("ST", _)
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst Schulz | sof == const_subsortof ->
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst Schulz let s1 = lookupSortOMS "addMaybeToSortRel: s1" e oms1
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst Schulz s2 = lookupSortOMS "addMaybeToSortRel: s2" e oms2
59597e83448c2fc763557b56e0319615b33518d9Christian Maeder in return $ Rel.insertKeyOrPair s1 s2 r
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst Schulz | otherwise ->
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst Schulz warning () ("Use of subsortof in a non ST Statement: " ++ n)
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst Schulz _ -> return r
c86ab487b5998eb823a4c02ee66007403fb5ace5Ewaryst SchulzaddMaybeToSortRel _ r _ = return r
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzomdocToType :: Env -> OMElement -> Either OpType PredType
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzomdocToType e (OMA (c : args)) =
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz let sorts = map (lookupSortOMS "omdocToType" e) args
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz opargs = init sorts
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz oprange = last sorts
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz res | c == const_predtype = Right $ PredType sorts
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz | c == const_partialfuntype = Left $ OpType Partial opargs oprange
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz | c == const_funtype = Left $ OpType Total opargs oprange
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz | otherwise = error $ "omdocToType: unknown type constructor: "
341d12092c982c2d37e28f897d21cd3244e11005Ewaryst SchulzomdocToType e oms@(OMS _)
341d12092c982c2d37e28f897d21cd3244e11005Ewaryst Schulz | oms == const_predtype = Right $ PredType []
341d12092c982c2d37e28f897d21cd3244e11005Ewaryst Schulz | otherwise = Left $ OpType Total [] $ lookupSortOMS "omdocToType" e oms
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst SchulzomdocToType _ ome = error $ "omdocToType: Non-supported element: " ++ show ome
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz-- * Terms and Formulas
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulztype VarMap = Map.Map VAR SORT
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulztype TermEnv = (Env, VarMap)
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermkImplication, mkImplied, mkEquivalence
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz , mkNegation :: [FORMULA f] -> FORMULA f
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermkImplication [x, y] = mkImpl x y
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkImplication _ = error "Malformed implication"
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermkImplied [x, y] = mkRel RevImpl x y
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulzmkImplied _ = error "Malformed if"
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermkEquivalence [x, y] = mkEqv x y
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkEquivalence _ = error "Malformed equivalence"
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermkNegation [x] = mkNeg x
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkNegation _ = error "Malformed negation"
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkDefinedness, mkExistl_equation, mkStrong_equation
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz :: [TERM f] -> FORMULA f
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkDefinedness [x] = Definedness x nullRange
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkDefinedness _ = error "Malformed definedness"
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermkExistl_equation [x, y] = mkExEq x y
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkExistl_equation _ = error "Malformed existl equation"
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermkStrong_equation [x, y] = mkStEq x y
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkStrong_equation _ = error "Malformed strong equation"
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz-- Quantification, Predication and Membership are handled inside omdocToFormula
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz-- Term construction functions
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulzmkT2 :: (OMElement -> a) -> (OMElement -> b) -> (a -> b -> Range -> TERM f)
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz -> [OMElement] -> TERM f
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulzmkT2 f g c l = case l of
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz [x, y] -> c (f x) (g y) nullRange
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz _ -> error "mkT2: 2 arguments expected"
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulzmkT3 :: (OMElement -> a) -> (OMElement -> b) -> (OMElement -> c)
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz -> (a -> b -> c -> Range -> TERM f) -> [OMElement] -> TERM f
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulzmkT3 f g h c l = case l of
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz [x, y, z] -> c (f x) (g y) (h z) nullRange
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz _ -> error "mkT3: 3 arguments expected"
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz-- Formula construction functions
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkFF :: TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkFF e f l = f $ map (omdocToFormula' e) l
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkTF :: TermEnv -> ([TERM f] -> FORMULA f) -> [OMElement] -> FORMULA f
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkTF e f l = f $ map (omdocToTerm' e) l
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzgetQuantifier :: OMElement -> QUANTIFIER
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzgetQuantifier oms
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | oms == const_forall = Universal
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | oms == const_exists = Existential
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | oms == const_existsunique = Unique_existential
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | otherwise = error $ "getQuantifier: unrecognized quantifier " ++ show oms
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkBinder :: TermEnv -> QUANTIFIER -> [OMElement] -> OMElement -> FORMULA f
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzmkBinder te@(e, _) q vars body =
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz let (vm', vardecls) = toVarDecls te vars
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz bd = omdocToFormula' (e, vm') body
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz in Quantification q vardecls bd nullRange
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulztoVarDecls :: TermEnv -> [OMElement] -> (VarMap, [VAR_DECL])
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulztoVarDecls (e, vm) l =
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz let f acc x = let (v, s) = toVarDecl e x
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz acc' = Map.insert v s acc
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz in (acc', (v, s))
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz (vm', l') = mapAccumL f vm l
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz -- group by same sort
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder l'' = groupBy ((==) `Data.Function.on` snd) l'
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz -- the lists returned by groupBy are never empty, so head will succeed
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz g vsl = Var_decl (map fst vsl) (snd $ head vsl) nullRange
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz in (vm', map g l'')
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz-- in CASL we expect all bound vars to be attributed (typed)
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulztoVarDecl :: Env -> OMElement -> (VAR, SORT)
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulztoVarDecl e (OMATTT (OMV v) (OMAttr ct t))
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | ct == const_type = (nameToToken $ name v, lookupSortOMS "toVarDecl" e t)
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | otherwise = error $ "toVarDecl: unrecognized attribution " ++ show ct
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulztoVarDecl _ _ = error "toVarDecl: bound variables should be attributed."
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz-- Toplevel entry point
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzomdocToFormula :: Env -> OMElement -> FORMULA f
ad4da9d870c666f00992431e3badbbe9cc4f19aaChristian MaederomdocToFormula e = omdocToFormula' (e, Map.empty)
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz-- Functions with given VarMap
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz-- omdocToTerm has no toplevel entry point
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzomdocToTerm' :: TermEnv -> OMElement -> TERM f
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst SchulzomdocToTerm' e@(ie, vm) f =
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz OMA (h : args)
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz | h == const_cast ->
064d404172c333eb57e6580e38a078c159652834Ewaryst Schulz mkT2 (omdocToTerm' e) (lookupSortOMS "omdocToTerm: Cast" ie)
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz | h == const_if ->
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz mkT3 (omdocToTerm' e) (omdocToFormula' e) (omdocToTerm' e)
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz Conditional args
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz -- all other heads mean application
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz | otherwise ->
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz let os = toOpSymb $ lookupOpOMS "omdocToTerm" ie h
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz args' = map (omdocToTerm' e) args
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz in Application os args' nullRange
39f5e2f2029adad8b2ceac76a3b1c2f8babb9241Ewaryst Schulz OMS _ -> let os = toOpSymb $ lookupOpOMS "omdocToTerm-OMS:" ie f
39f5e2f2029adad8b2ceac76a3b1c2f8babb9241Ewaryst Schulz in Application os [] nullRange
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz OMV omn -> let var = nameToToken $ name omn
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz -- lookup the type of the variable in the varmap
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz (error $ concat [ "omdocToTerm': Variable not in "
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz , "varmap: ", show var ]) var vm
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz in Qual_var var s nullRange
ad4da9d870c666f00992431e3badbbe9cc4f19aaChristian Maeder OMATTT ome (OMAttr ct t)
064d404172c333eb57e6580e38a078c159652834Ewaryst Schulz | ct == const_type ->
064d404172c333eb57e6580e38a078c159652834Ewaryst Schulz -- same as cast
064d404172c333eb57e6580e38a078c159652834Ewaryst Schulz mkT2 (omdocToTerm' e) (lookupSortOMS "omdocToTerm: Sorted" ie)
064d404172c333eb57e6580e38a078c159652834Ewaryst Schulz Sorted_term [ome, t]
064d404172c333eb57e6580e38a078c159652834Ewaryst Schulz | otherwise -> error $ "omdocToTerm: unrecognized attribution "
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz _ -> error $ "omdocToTerm: no valid term " ++ show f
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzomdocToFormula' :: TermEnv -> OMElement -> FORMULA f
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst SchulzomdocToFormula' e@(ie, _) f =
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz OMA (h : args)
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | h == const_in ->
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz Membership (omdocToTerm' e x) (lookupSortOMS
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz "omdocToFormula"
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz ie s) nullRange
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz _ -> error "Malformed membership"
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | h == const_and ->
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder mkFF e conjunct args
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | h == const_or ->
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder mkFF e disjunct args
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | h == const_implies ->
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz mkFF e mkImplication args
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | h == const_implied ->
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz mkFF e mkImplied args
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | h == const_equivalent ->
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz mkFF e mkEquivalence args
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | h == const_not ->
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz mkFF e mkNegation args
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | h == const_def ->
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz mkTF e mkDefinedness args
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | h == const_eeq ->
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz mkTF e mkExistl_equation args
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | h == const_eq ->
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz mkTF e mkStrong_equation args
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz -- all other heads mean predication
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz | otherwise ->
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz let ps = toPredSymb $ lookupPredOMS "omdocToFormula" ie h
bc97d0dafa2cec17890802decf690ae8a1be03b7Ewaryst Schulz g l = Predication ps l nullRange in
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz mkTF e g args
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz OMBIND binder args body ->
97f3827decee427ef52fe8a382f159a81e2abdf1Ewaryst Schulz mkBinder e (getQuantifier binder) args body
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder OMS _ | f == const_true -> trueForm
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder | f == const_false -> falseForm
341d12092c982c2d37e28f897d21cd3244e11005Ewaryst Schulz -- Propositional Constants (0-ary predicates):
341d12092c982c2d37e28f897d21cd3244e11005Ewaryst Schulz | otherwise ->
341d12092c982c2d37e28f897d21cd3244e11005Ewaryst Schulz Predication (toPredSymb
341d12092c982c2d37e28f897d21cd3244e11005Ewaryst Schulz $ lookupPredOMS
341d12092c982c2d37e28f897d21cd3244e11005Ewaryst Schulz ("omdocToFormula: can't handle constant "
341d12092c982c2d37e28f897d21cd3244e11005Ewaryst Schulz ++ show f) ie f) [] nullRange
ad4da9d870c666f00992431e3badbbe9cc4f19aaChristian Maeder _ -> error $ "omdocToFormula: no valid formula " ++ show f