CASL2Prenex.hs revision 414029fc573cb2506241ed5a17643f9f721502b8
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettModule : $Header$
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettDescription : prenex normal form for sentences of a CASL theory
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettCopyright : (c) Mihai Codescu, 2016
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettLicense : GPLv2 or higher, see LICENSE.txt
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettMaintainer : codescu@iws.cs.uni-magdeburg.de
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettStability : provisional
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettPortability : non-portable (imports Logic.Comorphism)
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport CASL.Sublogic as SL hiding (bottom)
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblettimport qualified Data.Set as Set
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettdata CASL2Prenex = CASL2Prenex deriving Show
2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblettinstance Language CASL2Prenex where
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett language_name CASL2Prenex = "CASL2Prenex"
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettinstance Comorphism CASL2Prenex
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett CASL CASL_Sublogics
2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Symbol RawSymbol ProofTree
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett CASL CASL_Sublogics
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Symbol RawSymbol ProofTree where
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sourceLogic CASL2Prenex = CASL
8e97dcf353ac3afc326ecfd167abd47897215436Andy Gimblett sourceSublogic CASL2Prenex = SL.caslTop
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett targetLogic CASL2Prenex = CASL
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett mapSublogic CASL2Prenex sl =
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Just $ min sl (sl{SL.which_logic = SL.Prenex})
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett map_theory CASL2Prenex = mapTheory
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett map_morphism CASL2Prenex = return
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett map_sentence CASL2Prenex sig = return . (mapSentence sig)
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett map_symbol CASL2Prenex _ = Set.singleton . id
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett has_model_expansion CASL2Prenex = True
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett is_weakly_amalgamable CASL2Prenex = True
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett-- remove equivalences
34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettpreprocessSen :: CASLFORMULA -> CASLFORMULA
34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettpreprocessSen sen = case sen of
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Quantification q vdecls sen' r ->
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Quantification q vdecls (preprocessSen sen') r
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Junction j sens r ->
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Junction j (map preprocessSen sens) r
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Relation sen1 Equivalence sen2 _ -> let
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sen1' = Relation sen1 Implication sen2 nullRange
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett sen2' = Relation sen2 Implication sen1 nullRange
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett in Junction Con [sen1', sen2'] nullRange
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Relation sen1 rel sen2 r ->
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Relation (preprocessSen sen1) rel
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett (preprocessSen sen2) r
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Negation sen' r ->
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Negation (preprocessSen sen') r
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett-- make variables distinct:
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett-- if a variable v of sort s already appears in a formula
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett-- substitute it with a fresh variable
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy GimblettmkDistVars :: CASLFORMULA -> CASLFORMULA
2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy GimblettmkDistVars sen =
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett let (_, _, sen') = mkDistVarsAux 0 [] sen
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettmkDistVarsAux :: Int -- first available suffix for vars
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett -> [(VAR, SORT)] -- vars encountered so far
4690e532c5ebfbf9d71880a5c912ce09ab1fa2feAndy Gimblett -> CASLFORMULA
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett -> (Int, [(VAR, SORT)], CASLFORMULA)
34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettmkDistVarsAux n vlist sen = case sen of
bf7d1ec09971b005fff4133bb8b6964ab7d264e7Andy Gimblett Quantification q vdecls form range -> let
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett -- first make variables distinct for form
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett dvars = flatVAR_DECLs vdecls
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett (n', _, form') = mkDistVarsAux n (dvars ++ vlist) form
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett -- here we are not interested in the variables generated for the quantified form, so we can forget them
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett replVarDecl vds oN nN s = reverse $
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett foldl (\usedD vd@(Var_decl names sort r) ->
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett if sort == s then -- found it, replace oN with nN in names
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett let vd' = Var_decl (map (\x -> if x == oN then nN else x) names) sort r
9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett else vd:usedD
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett checkAndReplace (n0, knownV, quantF, quants) (x, s) =
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett if (x,s) `elem` knownV
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett x' = genNumVar "x" n0
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett quants' = replVarDecl quants x x' s
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett quantF' = substitute x s (Qual_var x' s nullRange) quantF
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett in (n0 + 1, (x', s):knownV, quantF', quants')
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett else (n0 , (x , s):knownV, quantF , quants )
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett (n'', vlist', form'', vdecls') = foldl checkAndReplace (n', vlist, form', vdecls) dvars
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett in (n'', vlist', Quantification q vdecls' form'' range)
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Junction j sens r -> let
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett (n', vlist', sens') = foldl (\(x, vs, osens) s ->
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett (x', vs', s') = mkDistVarsAux x vs s
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett in (x', vs', s':osens)) (n, vlist, []) sens
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett in (n', vlist', Junction j (reverse sens') r)
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Relation sen1 rel sen2 r -> let
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett (n1, vlist1, sen1') = mkDistVarsAux n vlist sen1
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett (n2, vlist2, sen2') = mkDistVarsAux n1 vlist1 sen2
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett in (n2, vlist2, Relation sen1' rel sen2' r)
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Negation sen' r -> let
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett (n', vlist', sen'') = mkDistVarsAux n vlist sen'
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett in (n', vlist', Negation sen'' r)
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett _ -> (n, vlist, sen)
34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettcomputePNF :: CASLFORMULA -> CASLFORMULA
29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy GimblettcomputePNF sen = case sen of
34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Negation nsen _ -> let
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett nsen' = computePNF nsen
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett in case nsen' of
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Quantification q vdecls qsen _ ->
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett Quantification (dualQuant q) vdecls
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett (computePNF $ Negation qsen nullRange) nullRange
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett _ -> Negation nsen' nullRange
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett Relation sen1 Implication sen2 _ -> let
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett sen1' = computePNF sen1
ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett sen2' = computePNF sen2
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett in case sen1' of
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Quantification q vdecls qsen _ ->
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Quantification (dualQuant q) vdecls (computePNF $ Relation qsen Implication sen2 nullRange) nullRange
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett _ -> case sen2' of
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett Quantification q vdecls qsen _ ->
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett Quantification q vdecls
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett (computePNF $ Relation sen1' Implication qsen nullRange) nullRange
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett -- recursive call to catch multiple quantifiers for sen2'
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett _ -> -- no quantifications
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett Relation sen1' Implication sen2' nullRange
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett -- During parsing, "f2 if f1" is saved as "Relation f1 RevImpl f2 _"
d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett Relation sen1 RevImpl sen2 _ ->
b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett computePNF $ Relation sen1 Implication sen2 nullRange
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Quantification q vdecls qsen _ ->
b34e5090387d45b3a35f88eaa23477a83d2a2962Andy Gimblett Quantification q vdecls (computePNF qsen) nullRange
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett Junction j sens _ -> let
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett sens' = map computePNF sens
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett collectQuants s = case s of
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Quantification q vd qs _ -> let (vs, qs') = collectQuants qs in ((q,vd):vs, qs')
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett (vdecls, sens'') = foldl (\(vs, ss) s -> case s of
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett Quantification q vd qs _ -> let (vs', qs') = collectQuants qs
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett in (vs' ++ (q,vd):vs, qs':ss)
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett _ -> (vs, s:ss))
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett ([], []) sens'
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett qsen = Junction j (reverse sens'') nullRange
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett rsen = foldl (\s (q, vd) -> Quantification q vd s nullRange) qsen vdecls
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy GimblettmapSentence :: CASLSign -> CASLFORMULA -> CASLFORMULA
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy GimblettmapSentence _ =
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett computePNF . mkDistVars . preprocessSen
bf7d1ec09971b005fff4133bb8b6964ab7d264e7Andy GimblettmapTheory :: (CASLSign, [Named CASLFORMULA]) ->
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett Result (CASLSign, [Named CASLFORMULA])
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy GimblettmapTheory (sig, nsens) = do
fe9b4842ac7b63bc2a5042ae829759e2874acd05Andy Gimblett let nsens' = map (\nsen -> nsen{
9890f5274aa35d7b8c073cd5bbc3c4028b18dc7dAndy Gimblett sentence = mapSentence sig $ sentence nsen
b6499fa6826cfdc288dc841be705aab6e4cc6c95Andy Gimblett return (sig, nsens')