CASL2Prenex.hs revision e2fdd28e29f151215a081dd95fcc443a4c8ccf23
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuModule : $Header$
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuDescription : prenex normal form for sentences of a CASL theory
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuCopyright : (c) Mihai Codescu, 2016
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuLicense : GPLv2 or higher, see LICENSE.txt
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuMaintainer : codescu@iws.cs.uni-magdeburg.de
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuStability : provisional
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuPortability : non-portable (imports Logic.Comorphism)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuimport CASL.Sublogic as SL hiding (bottom)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuimport qualified Data.Set as Set
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescudata CASL2Prenex = CASL2Prenex deriving Show
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuinstance Language CASL2Prenex where
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu language_name CASL2Prenex = "CASL2Prenex"
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuinstance Comorphism CASL2Prenex
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu CASL CASL_Sublogics
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Symbol RawSymbol ProofTree
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu CASL CASL_Sublogics
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Symbol RawSymbol ProofTree where
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu sourceLogic CASL2Prenex = CASL
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sourceSublogic CASL2Prenex = SL.caslTop
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu targetLogic CASL2Prenex = CASL
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu mapSublogic CASL2Prenex sl = Just sl -- TODO
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu map_theory CASL2Prenex = mapTheory
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu map_morphism CASL2Prenex = return
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu map_sentence CASL2Prenex sig = return . (mapSentence sig)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu map_symbol CASL2Prenex _ = Set.singleton . id
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu has_model_expansion CASL2Prenex = True
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu is_weakly_amalgamable CASL2Prenex = True
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu-- remove equivalences
e8001d65a73bf355ac769f1a3c959bd949be5763mcodescupreprocessSen :: CASLFORMULA -> CASLFORMULA
e8001d65a73bf355ac769f1a3c959bd949be5763mcodescupreprocessSen sen = case sen of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls sen' r ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls (preprocessSen sen') r
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Junction j sens r ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Junction j (map preprocessSen sens) r
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation sen1 Equivalence sen2 _ -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sen1' = Relation sen1 Implication sen2 nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sen2' = Relation sen2 Implication sen1 nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in Junction Con [sen1', sen2'] nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation sen1 rel sen2 r ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation (preprocessSen sen1) rel
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (preprocessSen sen2) r
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Negation sen' r ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Negation (preprocessSen sen') r
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu-- make variables distinct:
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu-- if a variable v of sort s already appears in a formula
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu-- substitute it with a fresh variable
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescumkDistVars :: CASLFORMULA -> CASLFORMULA
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescumkDistVars sen =
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu let (_, _, sen') = mkDistVarsAux 0 [] sen
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescumkDistVarsAux :: Int -- first available suffix for vars
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu -> [(VAR, SORT)] -- vars encountered so far
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu -> CASLFORMULA
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu -> (Int, [(VAR, SORT)], CASLFORMULA)
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescumkDistVarsAux n vlist sen = case sen of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls form range -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu -- first make variables distinct for form
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu dvars = flatVAR_DECLs vdecls
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (n', _, form') = mkDistVarsAux n (dvars ++ vlist) form
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu -- here we are not interested in the variables generated for the quantified form, so we can forget them
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu replVarDecl vds oN nN s = reverse $
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu foldl (\usedD vd@(Var_decl names sort r) ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu if sort == s then -- found it, replace oN with nN in names
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu let vd' = Var_decl (map (\x -> if x == oN then nN else x) names) sort r
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in vd':usedD
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu else vd:usedD
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu checkAndReplace (n0, knownV, quantF, quants) (x, s) =
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu if (x,s) `elem` knownV
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu x' = genNumVar "x" n0
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu quants' = replVarDecl quants x x' s
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu quantF' = substitute x s (Qual_var x' s nullRange) quantF
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in (n0 + 1, (x', s):knownV, quantF', quants')
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu else (n0 , (x , s):knownV, quantF , quants )
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (n'', vlist', form'', vdecls') = foldl checkAndReplace (n', vlist, form', vdecls) dvars
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in (n'', vlist', Quantification q vdecls' form'' range)
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Junction j sens r -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (n', vlist', sens') = foldl (\(x, vs, osens) s ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (x', vs', s') = mkDistVarsAux x vs s
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in (x', vs', s':osens)) (n, vlist, []) sens
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in (n', vlist', Junction j (reverse sens') r)
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation sen1 rel sen2 r -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (n1, vlist1, sen1') = mkDistVarsAux n vlist sen1
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (n2, vlist2, sen2') = mkDistVarsAux n1 vlist1 sen2
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in (n2, vlist2, Relation sen1' rel sen2' r)
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Negation sen' r -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (n', vlist', sen'') = mkDistVarsAux n vlist sen'
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in (n', vlist', Negation sen'' r)
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu _ -> (n, vlist, sen)
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescucomputePNF :: CASLFORMULA -> CASLFORMULA
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescucomputePNF sen = case sen of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Negation nsen _ -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu nsen' = computePNF nsen
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in case nsen' of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls qsen _ ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification (dualQuant q) vdecls
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (computePNF $ Negation qsen nullRange) nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu _ -> Negation nsen' nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation sen1 Implication sen2 _ -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sen1' = computePNF sen1
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sen2' = computePNF sen2
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in case sen1' of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls qsen _ ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification (dualQuant q) vdecls (computePNF $ Relation qsen Implication sen2 nullRange) nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu _ -> case sen2' of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls qsen _ ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (computePNF $ Relation sen1' Implication qsen nullRange) nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu -- recursive call to catch multiple quantifiers for sen2'
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu _ -> -- no quantifications
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation sen1' Implication sen2' nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation sen1 RevImpl sen2 _ ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu computePNF $ Relation sen2 Implication sen1 nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls qsen _ ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls (computePNF qsen) nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Junction j sens _ -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sens' = map computePNF sens
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu processQuants asen = case asen of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls sen' _ -> Quantification q vdecls (processQuants sen') nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Junction j' jsens _ -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu nonQuantifiedSen (Quantification _ _ _ _) = False
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu nonQuantifiedSen _ = True
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (nonQuantJSens, remJSens) = span nonQuantifiedSen jsens
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in if nonQuantJSens == jsens then asen
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu else case remJSens of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (Quantification q vdecls qsen _):remJSens' ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls (processQuants $ Junction j' (nonQuantJSens ++ (qsen: remJSens')) nullRange) nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu _ -> error "computePNF" -- should not be possible
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in processQuants $ Junction j sens' nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescumapSentence :: CASLSign -> CASLFORMULA -> CASLFORMULA
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescumapSentence _ =
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu computePNF . mkDistVars . preprocessSen
a81a3e6bff3e7b764d78c2864a1324b15e4135famcodescumapTheory :: (CASLSign, [Named CASLFORMULA]) ->
a81a3e6bff3e7b764d78c2864a1324b15e4135famcodescu Result (CASLSign, [Named CASLFORMULA])
a81a3e6bff3e7b764d78c2864a1324b15e4135famcodescumapTheory (sig, nsens) = do
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu let nsens' = map (\nsen -> nsen{
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sentence = mapSentence sig $ sentence nsen
a81a3e6bff3e7b764d78c2864a1324b15e4135famcodescu return (sig, nsens')