CASL_DL2CASL.hs revision 5bed2c62278d4f062c980a72c631578a9ee4a608
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer{- |
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerModule : Comorphisms/CASL_DL2CASL.hs
6b26240dca29e026900a83d51c75ca230a072a16Thiemo WiedemeyerDescription : Inclusion of CASL_DL into CASL
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerCopyright : (c) Uni Bremen 2007
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerLicense : similar to LGPL, see HetCATS/LICENSE.txt
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : luecke@informatik.uni-bremen.de
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerStability : provisional
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerPortability : non-portable (via Logic.Logic)
7520452bb30b5abbd471f82352fc4c1c937e02c5Till Mossakowski
7520452bb30b5abbd471f82352fc4c1c937e02c5Till Mossakowski-}
7520452bb30b5abbd471f82352fc4c1c937e02c5Till Mossakowski
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyermodule Comorphisms.CASL_DL2CASL
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer CASL_DL2CASL(..)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer )
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer where
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Logic.Logic
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Logic.Comorphism
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Common.Id
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified Data.Set as Set
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified Common.Lib.Rel as Rel
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified Data.Map as Map
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Common.AS_Annotation
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Data.List
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Common.Result
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maederimport CASL_DL.PredefinedCASLAxioms
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder--CASL_DL = domain
9a9860760c6f30558e5e60049692b6fc63904590Markus Grossimport CASL_DL.Logic_CASL_DL
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport CASL_DL.AS_CASL_DL
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyerimport CASL_DL.Sign()
0193c86704431f83731015a77cb613d67ae4e3c2Thiemo Wiedemeyerimport CASL_DL.PredefinedSign
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyerimport CASL_DL.StatAna -- DLSign
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyerimport CASL_DL.PredefinedSign
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer--CASL = codomain
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyerimport CASL.Logic_CASL
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyerimport CASL.AS_Basic_CASL
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyerimport CASL.Sign
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyerimport CASL.Morphism
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo Wiedemeyerimport CASL.Sublogic as Sublogic
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerdata CASL_DL2CASL = CASL_DL2CASL deriving Show
02a84229da51532505a93fc2abfca1ccf81b4446Razvan Pascanu
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerinstance Language CASL_DL2CASL
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerinstance Comorphism
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer CASL_DL2CASL -- comorphism
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer CASL_DL -- lid domain
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder () -- sublogics domain
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer DL_BASIC_SPEC -- Basic spec domain
b6a59f004903ac7bc96323ee3ef09c01fd221157Christian Maeder DLFORMULA -- sentence domain
8a1077f446e5a0e127e0805e2c1efe6bf5eeb0d8Christian Maeder SYMB_ITEMS -- symbol items domain
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer SYMB_MAP_ITEMS -- symbol map items domain
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer DLSign -- signature domain
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer DLMor -- morphism domain
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Symbol -- symbol domain
36f69d35e01d2d6b6bdc165b49661f2a80af8687Mihai Codescu RawSymbol -- rawsymbol domain
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer () -- proof tree codomain
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer CASL -- lid codomain
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer CASL_Sublogics -- sublogics codomain
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer CASLBasicSpec -- Basic spec codomain
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer CASLFORMULA -- sentence codomain
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer SYMB_ITEMS -- symbol items codomain
4e9e95ba35a68f3c767bc0b23ebf9e904e442517Christian Maeder SYMB_MAP_ITEMS -- symbol map items codomain
4e9e95ba35a68f3c767bc0b23ebf9e904e442517Christian Maeder CASLSign -- signature codomain
4e9e95ba35a68f3c767bc0b23ebf9e904e442517Christian Maeder CASLMor -- morphism codomain
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Symbol -- symbol codomain
79d103748927615310322af6f7806c7cef11a802Christian Maeder RawSymbol -- rawsymbol codomain
ecd98975b8a8ab5a7bc075562bdab51cf47d2a90Christian Maeder Q_ProofTree -- proof tree domain
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder where
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder sourceLogic CASL_DL2CASL = CASL_DL
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder targetLogic CASL_DL2CASL = CASL
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer sourceSublogic CASL_DL2CASL = ()
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder mapSublogic CASL_DL2CASL _ = Just $ Sublogic.top
f456529a89bfb620d39e5fd5b0a53b24643db96dDominik Luecke { sub_features = LocFilSub,
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer has_part = True,
4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maeder cons_features = SortGen { emptyMapping = True,
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer onlyInjConstrs = False},
c745add71930134bc085a544783213179bd3e734Thiemo Wiedemeyer has_eq = True,
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer has_pred = True,
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer which_logic = FOL
93eeaffa1087fc6eae3f19b8ca5affb7802799fdThiemo Wiedemeyer }
02a84229da51532505a93fc2abfca1ccf81b4446Razvan Pascanu map_symbol CASL_DL2CASL s = Set.singleton s
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder map_sentence CASL_DL2CASL = trSentence
2028dc2c091bb60343e15985948a59b955276cbfChristian Maeder map_morphism CASL_DL2CASL = mapMor
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer map_theory CASL_DL2CASL = trTheory
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer
16e45483b5ce48f0b92d01c817242a8c9b8bae02Christian Maeder-- ^ mapping of morphims, we just forget the
40b73e7d13a858afeac95321fcdb9ac216bfbf01Thiemo Wiedemeyer-- ^ additional features
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo WiedemeyermapMor :: DLMor -> Result CASLMor
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyermapMor inMor =
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder let
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ms = trSign $ msource inMor
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu mt = trSign $ mtarget inMor
02a84229da51532505a93fc2abfca1ccf81b4446Razvan Pascanu sm = sort_map inMor
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu fm = fun_map inMor
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer pm = pred_map inMor
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer in
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer return $ Morphism
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer {
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer msource = ms
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer , mtarget = mt
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer , sort_map = sm
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer , fun_map = fm
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer , pred_map = pm
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer , extended_map = ()
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer }
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer-- ^ we forget additional information in the signature
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo WiedemeyerprojectToCASL :: DLSign -> CASLSign
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo WiedemeyerprojectToCASL dls = dls
03bbcb1fefdbd8bc4e8329ca2688809d84aff0a9Christian Maeder {
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer sentences = []
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder , extendedInfo = ()
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer }
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer-- ^ Thing is established as the TopSort of all sorts
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer-- ^ defined in the CASL_DL spec, a predefined signature
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu-- ^ is added
0b8b26a22f136a9b2a8e99d655f6fe6b0b96008cThiemo WiedemeyertrSign :: DLSign -> CASLSign
0b8b26a22f136a9b2a8e99d655f6fe6b0b96008cThiemo WiedemeyertrSign inSig =
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer inC = (makeCardResSignature $ projectToCASL inSig) `uniteCASLSign` predefSign
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer inD = projectToCASL predefinedSign
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer mergedS = inC `uniteCASLSign` inD
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer inSorts = sortSet inSig
0b8b26a22f136a9b2a8e99d655f6fe6b0b96008cThiemo Wiedemeyer inData = sortSet dataSig_CASL
0b8b26a22f136a9b2a8e99d655f6fe6b0b96008cThiemo Wiedemeyer in
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer mergedS
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer {
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer sortRel = Rel.delete topSortD topSortD $
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer Set.fold (\x -> Rel.insert x topSortD)
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer (Set.fold (\x -> Rel.insert x topSort)
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer (sortRel inC) inSorts)
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer inData
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer }
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer-- ^ this adds the signature for cardinality restrictions
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo WiedemeyermakeCardResSignature :: CASLSign -> CASLSign
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo WiedemeyermakeCardResSignature cSign =
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer let
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer pm = predMap cSign
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer in
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer Map.foldWithKey (\k a b -> uniteCASLSign (addCardResOps k a) b) cSign pm
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo WiedemeyeraddCardResOps :: Id -> Set.Set PredType -> Sign () ()
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo WiedemeyeraddCardResOps myId spt =
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer let
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer inOps = map (\x -> addCardResOp myId x)
0b8b26a22f136a9b2a8e99d655f6fe6b0b96008cThiemo Wiedemeyer $ filter (\x -> (length $ predArgs x) == 2) $ Set.toList spt
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer in
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer foldl (uniteCASLSign) (emptySign ()) inOps
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer-- ^ this adds the axioms for cardinality restrictions
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo WiedemeyermakeCardAxioms :: CASLSign -> [(Named (FORMULA()))] -> [(Named (FORMULA()))]
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo WiedemeyermakeCardAxioms cSign cAxs =
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer let
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer pm = predMap cSign
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer in
86b2d79be961f0247a2eed10ed4f86d8d6a7639dChristian Maeder Map.foldWithKey (\k a b -> (++) (addCardResAxx k a) b) cAxs pm
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo WiedemeyeraddCardResAxx :: Id -> Set.Set PredType -> [(Named (FORMULA()))]
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo WiedemeyeraddCardResAxx myId spt =
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer let
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer inOps = map (\x -> addCardResAx myId x)
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer $ filter (\x -> (length $ predArgs x) == 2) $ Set.toList spt
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer in
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer foldl (++) [] inOps
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer-- ^ translation of the signature
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer-- ^ predefined axioms are added
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo WiedemeyerrtrSign :: DLSign -> Result CASLSign
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo WiedemeyerrtrSign inSig = return $ trSign inSig
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer-- Translation of theories
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo WiedemeyertrTheory :: (DLSign, [Named (FORMULA DL_FORMULA)]) ->
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer Result (CASLSign, [Named (FORMULA ())])
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo WiedemeyertrTheory (inSig, inForms) =
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer do
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer outForms <- mapR (\x -> trNamedSentence inSig x) inForms
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer outSig <- rtrSign inSig
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer return (outSig, predefinedAxioms ++ (makeCardAxioms (projectToCASL inSig) outForms))
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer-- ^ translation of named sentences
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo WiedemeyertrNamedSentence :: DLSign -> Named (FORMULA DL_FORMULA) ->
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer Result (Named (FORMULA ()))
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo WiedemeyertrNamedSentence inSig inForm =
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer let
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer inAttL = senAttr inForm
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer isAxL = isAxiom inForm
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer isDefL = isDef inForm
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer wasThL = wasTheorem inForm
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer simpAL = simpAnno inForm
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer inSenL = sentence inForm
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer in
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer do
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer outSen <- trSentence inSig inSenL
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer return SenAttr
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer {
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer senAttr = inAttL
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer , isAxiom = isAxL
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer , isDef = isDefL
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer , wasTheorem = wasThL
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer , simpAnno = simpAL
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer , sentence = outSen
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer }
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer-- ^ translation of sentences
92e96be605537638d75e9d3023ab698bd89cf889Thiemo WiedemeyertrSentence :: DLSign -> FORMULA DL_FORMULA -> Result (FORMULA ())
92e96be605537638d75e9d3023ab698bd89cf889Thiemo WiedemeyertrSentence inSig inF =
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer case inF of
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer Quantification qf vs frm rn ->
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer do
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer outF <- trSentence inSig frm
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer return (Quantification qf vs (outF) rn)
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer Conjunction fns rn ->
92e96be605537638d75e9d3023ab698bd89cf889Thiemo Wiedemeyer do
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer outF <- mapR (\x -> trSentence inSig x) fns
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer return (Conjunction outF rn)
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer Disjunction fns rn ->
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer do
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer outF <- mapR (\x -> trSentence inSig x) fns
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer return (Disjunction outF rn)
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer Implication f1 f2 b rn ->
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer do
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer out1 <- trSentence inSig f1
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer out2 <- trSentence inSig f2
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer return (Implication out1 out2 b rn)
aa21e7aa42fef563dea0cc77edbde76f66cdbe88Thiemo Wiedemeyer Equivalence f1 f2 rn ->
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer do
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer out1 <- trSentence inSig f1
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer out2 <- trSentence inSig f2
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer return (Equivalence out1 out2 rn)
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer Negation frm rn ->
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer do
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer outF <- trSentence inSig frm
d9f20cf968e246ec283f0c09f60af4b47b174398Thiemo Wiedemeyer return (Negation outF rn)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer True_atom rn -> do return (True_atom rn)
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer False_atom rn -> do return (False_atom rn)
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer Predication pr trm rn ->
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer do
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer ot <- mapR (\x -> trTerm inSig x) trm
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer return (Predication pr ot rn)
3e3efd4ce838940032e875e6d08712a177c9c1d0Thiemo Wiedemeyer Definedness tm rn ->
3e3efd4ce838940032e875e6d08712a177c9c1d0Thiemo Wiedemeyer do
3e3efd4ce838940032e875e6d08712a177c9c1d0Thiemo Wiedemeyer ot <- trTerm inSig tm
3e3efd4ce838940032e875e6d08712a177c9c1d0Thiemo Wiedemeyer return (Definedness ot rn)
3e3efd4ce838940032e875e6d08712a177c9c1d0Thiemo Wiedemeyer Existl_equation t1 t2 rn ->
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer do
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer ot1 <- trTerm inSig t1
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer ot2 <- trTerm inSig t2
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder return (Existl_equation ot1 ot2 rn)
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder Strong_equation t1 t2 rn ->
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer do
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer ot1 <- trTerm inSig t1
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder ot2 <- trTerm inSig t2
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer return (Strong_equation ot1 ot2 rn)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Membership t1 st rn ->
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder do
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer ot <- trTerm inSig t1
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer return (Membership ot st rn)
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer Mixfix_formula trm ->
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer do
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer ot <- trTerm inSig trm
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer return (Mixfix_formula ot)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Unparsed_formula str rn ->
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer do return (Unparsed_formula str rn)
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer Sort_gen_ax cstr ft ->
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer do return (Sort_gen_ax cstr ft)
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer ExtFORMULA form ->
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer case form of
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Cardinality CExact ps trm1 trm2 _ -> makeEqCardinality inSig ps trm1 trm2
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Cardinality CMin ps trm1 trm2 _ -> makeMinCardinality inSig ps trm1 trm2
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Cardinality CMax ps trm1 trm2 _ -> makeMaxCardinality inSig ps trm1 trm2
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer
1ac36418f204bbe56f4cd951a979180721758999Christian MaedermakeMinCardinality :: DLSign
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer -> PRED_SYMB
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer -> TERM DL_FORMULA
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer -> TERM DL_FORMULA
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer -> Result (FORMULA ())
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo WiedemeyermakeMinCardinality inSig ps trm1 trm2 =
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer let
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (pn, pt) =
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer case ps of
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer Pred_name _ -> error "I sense a disturbance in the force during analysis"
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer Qual_pred_name pname ptype _ -> (pname, ptype)
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer gn_Subject = case pt of Pred_type lst _ -> head $ lst
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder gn_Object = case pt of Pred_type lst _ -> head $ tail $ lst
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer in
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer do
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer tv <- trTerm inSig trm1
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer cnt <- trTerm inSig trm2
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer return $ (Implication
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer (Definedness
545d0cd78159cade346b579d06052638b19b0f72Thiemo Wiedemeyer (Application
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo Wiedemeyer (Qual_op_name
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo Wiedemeyer (Id{getTokens =
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer [Token{tokStr = "gn_setOfPred", tokPos = nullRange},
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Token{tokStr = "__", tokPos = nullRange}],
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu getComps =
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder [pn],
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu rangeOfId = nullRange})
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Op_type Partial
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu [gn_Subject]
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer (Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer getComps =
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu [gn_Object],
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu rangeOfId = nullRange})
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu nullRange)
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer nullRange)
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo Wiedemeyer [tv]
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo Wiedemeyer nullRange)
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer nullRange)
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer (Predication
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer (Qual_pred_name
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer (Id{getTokens =
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer [Token{tokStr = "__", tokPos = nullRange},
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian Token{tokStr = ">=", tokPos = nullRange},
da955132262baab309a50fdffe228c9efe68251dCui Jian Token{tokStr = "__", tokPos = nullRange}],
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian getComps = [], rangeOfId = nullRange})
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian (Pred_type
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian [Id{getTokens =
37e30366abd83c00a5d5447b45694627fd783de8Cui Jian [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange},
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer Id{getTokens =
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange}]
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer nullRange)
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder nullRange)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [Application
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer (Qual_op_name
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer (Id{getTokens =
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer [Token{tokStr = "gn_card", tokPos = nullRange},
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Token{tokStr = "__", tokPos = nullRange}],
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder getComps = [], rangeOfId = nullRange})
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Op_type Total
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder [Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu getComps =
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [gn_Object],
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer rangeOfId = nullRange}]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (Id{getTokens =
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer getComps = [], rangeOfId = nullRange})
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer nullRange)
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer nullRange)
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer [Application
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Qual_op_name
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder (Id{getTokens =
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu [Token{tokStr = "gn_setOfPred", tokPos = nullRange},
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Token{tokStr = "__", tokPos = nullRange}],
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer getComps =
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [pn],
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer rangeOfId = nullRange})
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer (Op_type Partial
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [gn_Subject]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer getComps =
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [gn_Object],
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer rangeOfId = nullRange})
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer nullRange)
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer nullRange)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [tv]
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer nullRange]
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer nullRange,
5107ba7da675778f2fded68493512b60eff8a455Christian Maeder cnt]
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer nullRange)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu True
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu nullRange)
5107ba7da675778f2fded68493512b60eff8a455Christian Maeder
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanumakeEqCardinality :: DLSign
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu -> PRED_SYMB
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu -> TERM DL_FORMULA
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer -> TERM DL_FORMULA
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian Maeder -> Result (FORMULA ())
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian MaedermakeEqCardinality inSig ps trm1 trm2 =
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer let
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer (pn, pt) =
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer case ps of
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Pred_name _ -> error "I sense a disturbance in the force during analysis"
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Qual_pred_name pname ptype _ -> (pname, ptype)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer gn_Subject = case pt of Pred_type lst _ -> head $ lst
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder gn_Object = case pt of Pred_type lst _ -> head $ tail $ lst
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer in
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder do
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder tv <- trTerm inSig trm1
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer cnt <- trTerm inSig trm2
370e81d7af7821f0ac6ee0643613e87a727841e7Thiemo Wiedemeyer return $ (Strong_equation
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer (Application
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer (Qual_op_name
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder (Id{getTokens =
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu [Token{tokStr = "gn_card", tokPos = nullRange},
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder Token{tokStr = "__", tokPos = nullRange}],
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu getComps = [], rangeOfId = nullRange})
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Op_type Total
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu [Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu getComps =
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer [gn_Object],
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder rangeOfId = nullRange}]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (Id{getTokens =
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange})
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer nullRange)
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder nullRange)
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer [Application
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer (Qual_op_name
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Id{getTokens =
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder [Token{tokStr = "gn_setOfPred", tokPos = nullRange},
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder Token{tokStr = "__", tokPos = nullRange}],
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer getComps =
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer [pn],
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer rangeOfId = nullRange})
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer (Op_type Partial
79d103748927615310322af6f7806c7cef11a802Christian Maeder [gn_Subject]
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer (Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer getComps =
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder [gn_Object],
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder rangeOfId = nullRange})
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu nullRange)
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder nullRange)
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder [tv]
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder nullRange]
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder nullRange)
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder (cnt)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu nullRange)
d71a37fb09bce02af6c98e7a5ab0aa5639058e4fThiemo Wiedemeyer
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer-- ^ predefined axioms for cardinality restrictions
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo WiedemeyermakeMaxCardinality :: DLSign
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder -> PRED_SYMB
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer -> TERM DL_FORMULA
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer -> TERM DL_FORMULA
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer -> Result (FORMULA ())
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo WiedemeyermakeMaxCardinality inSig ps trm1 trm2 =
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer let
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder (pn, pt) =
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder case ps of
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer Pred_name _ -> error "I sense a disturbance in the force during analysis"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Qual_pred_name pname ptype _ -> (pname, ptype)
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder gn_Subject = case pt of Pred_type lst _ -> head $ lst
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder gn_Object = case pt of Pred_type lst _ -> head $ tail $ lst
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder in
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder do
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian Maeder tv <- trTerm inSig trm1
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder cnt <- trTerm inSig trm2
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder return $ (Predication
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (Qual_pred_name
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder (Id{getTokens =
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder [Token{tokStr = "__", tokPos = nullRange},
836aa06d367f900bee9aa762250471bcd00b5a9dChristian Maeder Token{tokStr = "<=", tokPos = nullRange},
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer Token{tokStr = "__", tokPos = nullRange}],
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange})
66b035879accdc5f8337726173f800286a87fd78Christian Maeder (Pred_type
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder [Id{getTokens =
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder getComps = [], rangeOfId = nullRange},
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Id{getTokens =
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange}]
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder nullRange)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu nullRange)
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder [Application
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Qual_op_name
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Id{getTokens =
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder [Token{tokStr = "gn_card", tokPos = nullRange},
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder Token{tokStr = "__", tokPos = nullRange}],
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder getComps = [], rangeOfId = nullRange})
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder (Op_type Total
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder [Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer getComps =
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [gn_Object],
83263d411f611d9902ef4d98c93be6ad9361c833Christian Maeder rangeOfId = nullRange}]
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (Id{getTokens =
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange})
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu nullRange)
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder nullRange)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu [Application
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Qual_op_name
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Id{getTokens =
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder [Token{tokStr = "gn_setOfPred", tokPos = nullRange},
6c08e47c4275556c18f4f89521bf21fe94c28dd5Christian Maeder Token{tokStr = "__", tokPos = nullRange}],
6c08e47c4275556c18f4f89521bf21fe94c28dd5Christian Maeder getComps =
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [pn],
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer rangeOfId = nullRange})
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (Op_type Partial
66b035879accdc5f8337726173f800286a87fd78Christian Maeder [gn_Subject]
66b035879accdc5f8337726173f800286a87fd78Christian Maeder (Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer getComps =
66b035879accdc5f8337726173f800286a87fd78Christian Maeder [gn_Object],
66b035879accdc5f8337726173f800286a87fd78Christian Maeder rangeOfId = nullRange})
66b035879accdc5f8337726173f800286a87fd78Christian Maeder nullRange)
66b035879accdc5f8337726173f800286a87fd78Christian Maeder nullRange)
66b035879accdc5f8337726173f800286a87fd78Christian Maeder [tv]
66b035879accdc5f8337726173f800286a87fd78Christian Maeder nullRange]
66b035879accdc5f8337726173f800286a87fd78Christian Maeder nullRange,
66b035879accdc5f8337726173f800286a87fd78Christian Maeder cnt]
66b035879accdc5f8337726173f800286a87fd78Christian Maeder nullRange)
66b035879accdc5f8337726173f800286a87fd78Christian Maeder
66b035879accdc5f8337726173f800286a87fd78Christian Maeder-- ^ translation of terms
66b035879accdc5f8337726173f800286a87fd78Christian MaedertrTerm :: DLSign -> TERM DL_FORMULA -> Result (TERM ())
9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo WiedemeyertrTerm inSig inF =
03bbcb1fefdbd8bc4e8329ca2688809d84aff0a9Christian Maeder case inF of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Simple_id sid -> return (Simple_id sid)
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder Qual_var v s rn -> return (Qual_var v s rn)
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder Application os tms rn ->
66b035879accdc5f8337726173f800286a87fd78Christian Maeder do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ot <- mapR (\x -> trTerm inSig x) tms
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer return (Application os ot rn)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Sorted_term trm st rn ->
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer do
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer ot <- trTerm inSig trm
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer return (Sorted_term ot st rn)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Cast trm st rn ->
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ot <- trTerm inSig trm
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer return (Cast ot st rn)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Conditional t1 frm t2 rn ->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ot1 <- trTerm inSig t1
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ot2 <- trTerm inSig t2
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer of1 <- trSentence inSig frm
c41a1c38edbd787d8fd12b9b5f11b73a37dafe0fChristian Maeder return (Conditional ot1 of1 ot2 rn)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Unparsed_term str rn -> do return (Unparsed_term str rn)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Mixfix_qual_pred ps -> do return (Mixfix_qual_pred ps)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Mixfix_term trm ->
c41a1c38edbd787d8fd12b9b5f11b73a37dafe0fChristian Maeder do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ot <- mapR (\x -> trTerm inSig x) trm
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer return (Mixfix_term ot)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Mixfix_token tok -> do return (Mixfix_token tok)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Mixfix_sorted_term st rn -> do return (Mixfix_sorted_term st rn)
c41a1c38edbd787d8fd12b9b5f11b73a37dafe0fChristian Maeder Mixfix_cast st rn -> do return (Mixfix_cast st rn)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Mixfix_parenthesized trm rn ->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ot <- mapR (\x -> trTerm inSig x) trm
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder return (Mixfix_parenthesized ot rn)
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder Mixfix_bracketed trm rn ->
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder do
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder ot <- mapR (\x -> trTerm inSig x) trm
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder return (Mixfix_bracketed ot rn)
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder Mixfix_braced trm rn ->
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu do
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu ot <- mapR (\x -> trTerm inSig x) trm
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer return (Mixfix_braced ot rn)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder-- ^ a lot of predefined code for cardinality restrictions,
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer-- ^ the predefined natural numbers are used here
dda4e358a429dc24dd09d42b409d709a19eff159Christian MaederaddCardResOp :: Id -> PredType -> Sign () ()
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan PascanuaddCardResOp gn_predicate pt =
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu let
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder gn_Subject = head $ predArgs pt
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer gn_Object = head $ tail $ predArgs pt
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder in
e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder (emptySign ()){sortSet =
e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder Set.fromList
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder [Id [Token "gn_Set" nullRange]
63324a97283728a30932828a612c7b0b0f687624Christian Maeder [gn_Object]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder nullRange],
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder sortRel = Rel.fromList [],
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder opMap =
40b73e7d13a858afeac95321fcdb9ac216bfbf01Thiemo Wiedemeyer Map.fromList
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder [(Id [Token "gn_card" nullRange, Token "__" nullRange] []
16e45483b5ce48f0b92d01c817242a8c9b8bae02Christian Maeder nullRange,
e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder Set.fromList
16e45483b5ce48f0b92d01c817242a8c9b8bae02Christian Maeder [OpType Total
9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer [Id [Token "gn_Set" nullRange]
e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder [gn_Object]
e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder nullRange]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (Id [Token "nonNegativeInteger" nullRange] [] nullRange)]),
8244e8866cad2be73b7e2b76a6659535f0f728ccChristian Maeder (Id [Token "gn_eset" nullRange] [] nullRange,
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder Set.fromList
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder [OpType Total []
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder (Id [Token "gn_Set" nullRange]
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder [gn_Object]
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder nullRange)]),
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder (Id [Token "gn_insert" nullRange] [] nullRange,
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Set.fromList
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer [OpType Total
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder [Id [Token "gn_Set" nullRange]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder [gn_Object]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder nullRange,
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder gn_Object]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder (Id [Token "gn_Set" nullRange]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder [gn_Object]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder nullRange)]),
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder (Id [Token "gn_setOfPred" nullRange, Token "__" nullRange]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder [gn_predicate]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder nullRange,
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder Set.fromList
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder [OpType Partial [gn_Subject]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder (Id [Token "gn_Set" nullRange]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder [gn_Object]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder nullRange)])],
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder assocOps = Map.fromList [],
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder predMap =
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder Map.fromList
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder [(Id [Token "gn_contained" nullRange] [] nullRange,
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder Set.fromList
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder [PredType
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder [gn_Object,
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder Id [Token "gn_Set" nullRange]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder [gn_Object]
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder nullRange]]),
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder (gn_predicate,
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder Set.fromList
25f12ad1e6606d5ff6c43a9cae2fa51bd6f6efeaThiemo Wiedemeyer [PredType
25f12ad1e6606d5ff6c43a9cae2fa51bd6f6efeaThiemo Wiedemeyer [gn_Subject,
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder gn_Object]])]}
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder
95cb954c00f873306bf1a60b62d3209d3cff4102Christian MaederaddCardResAx :: Id -> PredType -> [(Named (FORMULA()))]
966a6c024c828387023fccb0cd0049f78687e5dcThiemo WiedemeyeraddCardResAx predicate pt =
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross let
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross gn_Subject = tokStr $ head $ getTokens $ head $ predArgs pt
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross gn_Object = tokStr $ head $ getTokens $ head $ tail $ predArgs pt
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross gn_Predicate = Id{getTokens =
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross (map (\x -> Token{tokStr = tokStr x, tokPos = nullRange}) (getTokens predicate)),
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross getComps = [], rangeOfId = nullRange}
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross axName = "_" ++ show gn_Predicate ++ "_" ++ gn_Subject ++ "_" ++ gn_Object
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross in
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross [SenAttr{senAttr = "ga_generated_gn_Set[" ++ gn_Object ++ "]", isAxiom = True,
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross isDef = False, wasTheorem = False, simpAnno = Nothing,
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross sentence =
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross Sort_gen_ax
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross [Constraint{newSort =
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross getComps =
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross [Id{getTokens =
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross [Token{tokStr = gn_Object, tokPos = nullRange}],
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross getComps = [], rangeOfId = nullRange}],
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross rangeOfId = nullRange},
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross opSymbs =
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross [(Qual_op_name
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross (Id{getTokens = [Token{tokStr = "gn_eset", tokPos = nullRange}],
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross getComps = [], rangeOfId = nullRange})
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross (Op_type Total []
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross (Id{getTokens =
9a9860760c6f30558e5e60049692b6fc63904590Markus Gross [Token{tokStr = "gn_Set", tokPos = nullRange}],
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder getComps =
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder [Id{getTokens =
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder [Token{tokStr = gn_Object, tokPos = nullRange}],
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder getComps = [], rangeOfId = nullRange}],
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder rangeOfId = nullRange})
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder nullRange)
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder nullRange,
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder []),
888fefaddbeb8d75a861b1d689b191b44d1853e1Thiemo Wiedemeyer (Qual_op_name
9b01b265715d725c17d51619d297bbb97f37d1b5Thiemo Wiedemeyer (Id{getTokens =
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder [Token{tokStr = "gn_insert", tokPos = nullRange}],
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder getComps = [], rangeOfId = nullRange})
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (Op_type Total
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder [Id{getTokens =
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder [Token{tokStr = "gn_Set", tokPos = nullRange}],
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder getComps =
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder [Id{getTokens =
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder [Token{tokStr = gn_Object, tokPos = nullRange}],
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder getComps = [], rangeOfId = nullRange}],
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder rangeOfId = nullRange},
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder Id{getTokens =
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder [Token{tokStr = gn_Object, tokPos = nullRange}],
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder getComps = [], rangeOfId = nullRange}]
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder (Id{getTokens =
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder [Token{tokStr = "gn_Set", tokPos = nullRange}],
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder getComps =
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder [Id{getTokens =
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder [Token{tokStr = gn_Object, tokPos = nullRange}],
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder getComps = [], rangeOfId = nullRange}],
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder rangeOfId = nullRange})
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder nullRange)
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder nullRange,
28ca54b0d63d1d26a991711c8c7e85c474994715Christian Maeder [0, - 1])],
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder origSort =
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
25f12ad1e6606d5ff6c43a9cae2fa51bd6f6efeaThiemo Wiedemeyer getComps =
25f12ad1e6606d5ff6c43a9cae2fa51bd6f6efeaThiemo Wiedemeyer [Id{getTokens =
25f12ad1e6606d5ff6c43a9cae2fa51bd6f6efeaThiemo Wiedemeyer [Token{tokStr = gn_Object, tokPos = nullRange}],
8618f6dc90d5392c661114468b47c71e4ae4e9beChristian Maeder getComps = [], rangeOfId = nullRange}],
f456529a89bfb620d39e5fd5b0a53b24643db96dDominik Luecke rangeOfId = nullRange}}]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer False},
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer SenAttr{senAttr = "Ax1"++axName, isAxiom = True, isDef = False,
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer wasTheorem = False, simpAnno = Nothing,
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer sentence =
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu Quantification Universal
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder [Var_decl [Token{tokStr = "gn_x", tokPos = nullRange}]
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu getComps = [], rangeOfId = nullRange})
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer nullRange]
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Negation
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Predication
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Qual_pred_name
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu (Id{getTokens =
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer [Token{tokStr = "gn_contained", tokPos = nullRange}],
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian Maeder getComps = [], rangeOfId = nullRange})
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian Maeder (Pred_type
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer [Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange},
0dba5bbaaef2f620f3b83a16ab6b229c3dd50c98Christian Maeder Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer getComps =
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer [Id{getTokens =
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer [Token{tokStr = gn_Object, tokPos = nullRange}],
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange}],
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer rangeOfId = nullRange}]
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer nullRange)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer nullRange)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer [Qual_var (Token{tokStr = "gn_x", tokPos = nullRange})
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer getComps = [], rangeOfId = nullRange})
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer nullRange,
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer Application
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer (Qual_op_name
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer (Id{getTokens = [Token{tokStr = "gn_eset", tokPos = nullRange}],
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer getComps = [], rangeOfId = nullRange})
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer (Op_type Total []
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer (Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder getComps =
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer [Id{getTokens =
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer [Token{tokStr = gn_Object, tokPos = nullRange}],
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer getComps = [], rangeOfId = nullRange}],
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer rangeOfId = nullRange})
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer nullRange)
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer nullRange)
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer []
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer nullRange]
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer nullRange)
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer nullRange)
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer nullRange},
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer SenAttr{senAttr = "Ax2"++axName, isAxiom = True, isDef = False,
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer wasTheorem = False, simpAnno = Nothing,
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer sentence =
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer Quantification Universal
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer [Var_decl
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer [Token{tokStr = "gn_x", tokPos = nullRange},
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer Token{tokStr = "gn_y", tokPos = nullRange}]
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer (Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer getComps = [], rangeOfId = nullRange})
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer nullRange,
1e3aca4178372af672efb237d16087c603fe5564Christian Maeder Var_decl [Token{tokStr = "gn_M", tokPos = nullRange}]
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer (Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer getComps =
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer [Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer getComps = [], rangeOfId = nullRange}],
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer rangeOfId = nullRange})
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer nullRange]
b021998bf955c87c7cdcc69f0667dc2880b3ce1fThiemo Wiedemeyer (Equivalence
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu (Predication
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer (Qual_pred_name
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer (Id{getTokens =
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer [Token{tokStr = "gn_contained", tokPos = nullRange}],
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange})
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer (Pred_type
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer [Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange},
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer getComps =
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu [Id{getTokens =
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder [Token{tokStr = gn_Object, tokPos = nullRange}],
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu getComps = [], rangeOfId = nullRange}],
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer rangeOfId = nullRange}]
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer nullRange)
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer nullRange)
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer [Qual_var (Token{tokStr = "gn_x", tokPos = nullRange})
d1066b8fb69179973dcab47154858d77e72760a7Thiemo Wiedemeyer (Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu getComps = [], rangeOfId = nullRange})
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu nullRange,
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Application
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (Qual_op_name
93eeaffa1087fc6eae3f19b8ca5affb7802799fdThiemo Wiedemeyer (Id{getTokens = [Token{tokStr = "gn_insert", tokPos = nullRange}],
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange})
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer (Op_type Total
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer [Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer getComps =
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer [Id{getTokens =
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer [Token{tokStr = gn_Object, tokPos = nullRange}],
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange}],
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer rangeOfId = nullRange},
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu getComps = [], rangeOfId = nullRange}]
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder (Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu getComps =
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu [Id{getTokens =
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu [Token{tokStr = gn_Object, tokPos = nullRange}],
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange}],
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu rangeOfId = nullRange})
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer nullRange)
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu nullRange)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer [Qual_var (Token{tokStr = "gn_M", tokPos = nullRange})
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer getComps =
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu [Id{getTokens =
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer [Token{tokStr = gn_Object, tokPos = nullRange}],
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange}],
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer rangeOfId = nullRange})
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer nullRange,
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Qual_var (Token{tokStr = "gn_y", tokPos = nullRange})
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange})
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer nullRange]
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer nullRange]
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer nullRange)
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer (Disjunction
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer [Strong_equation
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer (Qual_var (Token{tokStr = "gn_x", tokPos = nullRange})
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer (Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder getComps = [], rangeOfId = nullRange})
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer nullRange)
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder (Qual_var (Token{tokStr = "gn_y", tokPos = nullRange})
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer (Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange})
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer nullRange)
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer nullRange,
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer Predication
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer (Qual_pred_name
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer (Id{getTokens =
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer [Token{tokStr = "gn_contained", tokPos = nullRange}],
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu getComps = [], rangeOfId = nullRange})
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder (Pred_type
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu [Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
a4e6fb26100f53e3b1e9f5b97c2e0a0c129294e5Christian Maeder getComps = [], rangeOfId = nullRange},
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder getComps =
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder [Id{getTokens =
44c1fff98bd6c54db237bef5030657d3f47058a5Thiemo Wiedemeyer [Token{tokStr = gn_Object, tokPos = nullRange}],
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder getComps = [], rangeOfId = nullRange}],
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder rangeOfId = nullRange}]
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder nullRange)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer nullRange)
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer [Qual_var (Token{tokStr = "gn_x", tokPos = nullRange})
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer (Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer getComps = [], rangeOfId = nullRange})
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer nullRange,
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Qual_var (Token{tokStr = "gn_M", tokPos = nullRange})
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer (Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer getComps =
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer [Id{getTokens =
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer [Token{tokStr = gn_Object, tokPos = nullRange}],
84ba39232a012abf2085c8a421ebce6abc52d56eThiemo Wiedemeyer getComps = [], rangeOfId = nullRange}],
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer rangeOfId = nullRange})
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer nullRange]
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder nullRange]
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder nullRange)
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer nullRange)
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder nullRange},
8f5219469b89a15dc6d4c2c30463775975f5841cRazvan Pascanu SenAttr{senAttr = "Ax3"++axName, isAxiom = True, isDef = False,
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer wasTheorem = False, simpAnno = Nothing,
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder sentence =
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer Quantification Universal
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer [Var_decl
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer [Token{tokStr = "gn_M", tokPos = nullRange},
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer Token{tokStr = "gn_N", tokPos = nullRange}]
ea76e25262c3325f293fbdd6560f180ca18f9be4Thiemo Wiedemeyer (Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
f5b31c8df89d0c8898cfabe0bd6c671e8285c0f1Christian Maeder getComps =
79d103748927615310322af6f7806c7cef11a802Christian Maeder [Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange]
(Equivalence
(Strong_equation
(Qual_var (Token{tokStr = "gn_M", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange)
(Qual_var (Token{tokStr = "gn_N", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange)
nullRange)
(Quantification Universal
[Var_decl [Token{tokStr = "gn_z", tokPos = nullRange}]
(Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange]
(Equivalence
(Predication
(Qual_pred_name
(Id{getTokens =
[Token{tokStr = "gn_contained", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
(Pred_type
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange},
Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange}]
nullRange)
nullRange)
[Qual_var (Token{tokStr = "gn_z", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange,
Qual_var (Token{tokStr = "gn_M", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange]
nullRange)
(Predication
(Qual_pred_name
(Id{getTokens =
[Token{tokStr = "gn_contained", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
(Pred_type
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange},
Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange}]
nullRange)
nullRange)
[Qual_var (Token{tokStr = "gn_z", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange,
Qual_var (Token{tokStr = "gn_N", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange]
nullRange)
nullRange)
nullRange)
nullRange)
nullRange},
SenAttr{senAttr = "Ax4"++axName, isAxiom = True, isDef = False,
wasTheorem = False, simpAnno = Nothing,
sentence =
Strong_equation
(Application
(Qual_op_name
(Id{getTokens =
[Token{tokStr = "gn_card", tokPos = nullRange},
Token{tokStr = "__", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
(Op_type Total
[Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange}]
(Id{getTokens = [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange)
nullRange)
[Application
(Qual_op_name
(Id{getTokens = [Token{tokStr = "gn_eset", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
(Op_type Total []
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange)
nullRange)
[]
nullRange]
nullRange)
(Application
(Qual_op_name
(Id{getTokens = [Token{tokStr = "0", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
(Op_type Total []
(Id{getTokens = [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange)
nullRange)
[]
nullRange)
nullRange},
SenAttr{senAttr = "Ax5"++axName, isAxiom = True, isDef = False,
wasTheorem = False, simpAnno = Nothing,
sentence =
Quantification Universal
[Var_decl [Token{tokStr = "gn_x", tokPos = nullRange}]
(Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange,
Var_decl [Token{tokStr = "gn_M", tokPos = nullRange}]
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange]
(Strong_equation
(Application
(Qual_op_name
(Id{getTokens =
[Token{tokStr = "gn_card", tokPos = nullRange},
Token{tokStr = "__", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
(Op_type Total
[Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange}]
(Id{getTokens = [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange)
nullRange)
[Application
(Qual_op_name
(Id{getTokens = [Token{tokStr = "gn_insert", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
(Op_type Total
[Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange},
Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}]
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange)
nullRange)
[Qual_var (Token{tokStr = "gn_M", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange,
Qual_var (Token{tokStr = "gn_x", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange]
nullRange]
nullRange)
(Conditional
(Application
(Qual_op_name
(Id{getTokens =
[Token{tokStr = "gn_card", tokPos = nullRange},
Token{tokStr = "__", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
(Op_type Total
[Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange}]
(Id{getTokens = [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange)
nullRange)
[Qual_var (Token{tokStr = "gn_M", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange]
nullRange)
(Predication
(Qual_pred_name
(Id{getTokens =
[Token{tokStr = "gn_contained", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
(Pred_type
[Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange},
Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange}]
nullRange)
nullRange)
[Qual_var (Token{tokStr = "gn_x", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange,
Qual_var (Token{tokStr = "gn_M", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange]
nullRange)
(Application
(Qual_op_name
(Id{getTokens = [Token{tokStr = "suc", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
(Op_type Total
[Id{getTokens = [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}]
(Id{getTokens = [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange)
nullRange)
[Application
(Qual_op_name
(Id{getTokens =
[Token{tokStr = "gn_card", tokPos = nullRange},
Token{tokStr = "__", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
(Op_type Total
[Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange}]
(Id{getTokens = [Token{tokStr = "nonNegativeInteger", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange)
nullRange)
[Qual_var (Token{tokStr = "gn_M", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange]
nullRange]
nullRange)
nullRange)
nullRange)
nullRange},
SenAttr{senAttr = "Ax6"++axName, isAxiom = True, isDef = False,
wasTheorem = False, simpAnno = Nothing,
sentence =
Quantification Universal
[Var_decl [Token{tokStr = "x", tokPos = nullRange}]
(Id{getTokens = [Token{tokStr = gn_Subject, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange]
(Equivalence
(Definedness
(Application
(Qual_op_name
(Id{getTokens =
[Token{tokStr = "gn_setOfPred", tokPos = nullRange},
Token{tokStr = "__", tokPos = nullRange}],
getComps =
[gn_Predicate],
rangeOfId = nullRange})
(Op_type Partial
[Id{getTokens = [Token{tokStr = gn_Subject, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}]
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange)
nullRange)
[Qual_var (Token{tokStr = "x", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = gn_Subject, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange]
nullRange)
nullRange)
(Quantification Existential
[Var_decl [Token{tokStr = "s", tokPos = nullRange}]
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange]
(Quantification Universal
[Var_decl [Token{tokStr = "y", tokPos = nullRange}]
(Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange]
(Equivalence
(Predication
(Qual_pred_name
(gn_Predicate)
(Pred_type
[Id{getTokens =
[Token{tokStr = gn_Subject, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange},
Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}]
nullRange)
nullRange)
[Qual_var (Token{tokStr = "x", tokPos = nullRange})
(Id{getTokens =
[Token{tokStr = gn_Subject, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange,
Qual_var (Token{tokStr = "y", tokPos = nullRange})
(Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange]
nullRange)
(Predication
(Qual_pred_name
(Id{getTokens =
[Token{tokStr = "gn_contained", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
(Pred_type
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange},
Id{getTokens =
[Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange}]
nullRange)
nullRange)
[Qual_var (Token{tokStr = "y", tokPos = nullRange})
(Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange,
Qual_var (Token{tokStr = "s", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange]
nullRange)
nullRange)
nullRange)
nullRange)
nullRange)
nullRange},
SenAttr{senAttr = "Ax7"++axName, isAxiom = True, isDef = False,
wasTheorem = False, simpAnno = Nothing,
sentence =
Quantification Universal
[Var_decl [Token{tokStr = "x", tokPos = nullRange}]
(Id{getTokens = [Token{tokStr = gn_Subject, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange]
(Implication
(Definedness
(Application
(Qual_op_name
(Id{getTokens =
[Token{tokStr = "gn_setOfPred", tokPos = nullRange},
Token{tokStr = "__", tokPos = nullRange}],
getComps =
[gn_Predicate],
rangeOfId = nullRange})
(Op_type Partial
[Id{getTokens = [Token{tokStr = gn_Subject, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}]
(Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange)
nullRange)
[Qual_var (Token{tokStr = "x", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = gn_Subject, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange]
nullRange)
nullRange)
(Quantification Universal
[Var_decl [Token{tokStr = "y", tokPos = nullRange}]
(Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange]
(Equivalence
(Predication
(Qual_pred_name
(gn_Predicate)
(Pred_type
[Id{getTokens =
[Token{tokStr = gn_Subject, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange},
Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}]
nullRange)
nullRange)
[Qual_var (Token{tokStr = "x", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = gn_Subject, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange,
Qual_var (Token{tokStr = "y", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange]
nullRange)
(Predication
(Qual_pred_name
(Id{getTokens =
[Token{tokStr = "gn_contained", tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
(Pred_type
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange},
Id{getTokens = [Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange}]
nullRange)
nullRange)
[Qual_var (Token{tokStr = "y", tokPos = nullRange})
(Id{getTokens = [Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange,
Application
(Qual_op_name
(Id{getTokens =
[Token{tokStr = "gn_setOfPred", tokPos = nullRange},
Token{tokStr = "__", tokPos = nullRange}],
getComps =
[gn_Predicate],
rangeOfId = nullRange})
(Op_type Partial
[Id{getTokens =
[Token{tokStr = gn_Subject, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}]
(Id{getTokens =
[Token{tokStr = "gn_Set", tokPos = nullRange}],
getComps =
[Id{getTokens =
[Token{tokStr = gn_Object, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange}],
rangeOfId = nullRange})
nullRange)
nullRange)
[Qual_var (Token{tokStr = "x", tokPos = nullRange})
(Id{getTokens =
[Token{tokStr = gn_Subject, tokPos = nullRange}],
getComps = [], rangeOfId = nullRange})
nullRange]
nullRange]
nullRange)
nullRange)
nullRange)
True
nullRange)
nullRange}]