CASL2Prenex.hs revision ea5605cd49a0f959f75fd90137e9d25e1235c0e8
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)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuas described in
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuhttp://resources.mpi-inf.mpg.de/departments/rg1/teaching/autrea-ss10/script/lecture10.pdf
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
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu sourceSublogic CASL2Prenex = SL.caslTop --TODO
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu targetLogic CASL2Prenex = CASL
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu mapSublogic CASL2Prenex sl = Just sl -- TODO
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu map_theory CASL2Prenex = mapTheory
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu map_morphism CASL2Prenex = error "nyi"
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu map_sentence CASL2Prenex _ _ = error "nyi"
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu map_symbol CASL2Prenex _ = Set.singleton . id
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu has_model_expansion CASL2Prenex = True -- check
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu is_weakly_amalgamable CASL2Prenex = True --check
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- 1. F <-> G becomes F -> G and G -> F
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- 2. not (Q x . F) becomes (dual Q) x . not F
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- 3. (Q x . F) conn G becomes
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- Q y . (F[y/x] conn G)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- where y is fresh, conn is /\ or \/
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- 4. (Q x .F) => G becomes
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- (dual Q) y . (F[y/x] => G)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- where y is fresh
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- 5. F conn (Q x . G) becomes
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- Q y (F conn G[y/x])
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- with y fresh and conn in {/\,\/,->}
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- starting index for fresh variables
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- signature
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu-- formula that we compute normal form of
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuprenexNormalForm :: Int -> CASLSign -> CASLFORMULA -> (Int,CASLFORMULA)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuprenexNormalForm n sig sen = case sen of
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu -- this covers 1.
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Relation sen1 Equivalence sen2 _ -> let sen1' = Relation sen1 Implication sen2 nullRange
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu sen2' = Relation sen2 Implication sen1 nullRange
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu in trace "1" $ prenexNormalForm n sig $ Junction Con [sen1', sen2'] nullRange
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu -- this covers 2.
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Negation (Quantification q vdecls qsen _) _ -> let
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu (n', qsen') = prenexNormalForm n sig $ Negation qsen nullRange
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu in trace "2" $ (n', Quantification (dualQuant q) vdecls qsen' nullRange)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu -- in the remanining cases for negation, apply recursion
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Negation nsen _ -> let
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu (n', nsen') = prenexNormalForm n sig nsen
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu in trace "ng rec" $ (n', Negation nsen' nullRange)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu -- this covers 3.
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Junction j ((Quantification q vdecls qsen _):sens) _ ->
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu vars = flatVAR_DECLs vdecls
4c11424ec962479c1086f066f83976f05adb4064mcodescu (n', vars') = getFreshVars vars n
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu vdecls' = map (\(v,s) -> mkVarDecl v s) $ map fst vars'
4c11424ec962479c1086f066f83976f05adb4064mcodescu qsen' = foldl (\f (v,s,t)-> substitute v s t f) qsen $ map (\((x,y),(z,t)) -> (z, t, Qual_var x y nullRange)) vars'
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu (n'', jsen) = prenexNormalForm n' sig $ Junction j (qsen':sens) nullRange
4c11424ec962479c1086f066f83976f05adb4064mcodescu in trace "3" $ (n'', Quantification q vdecls' jsen nullRange)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu -- this covers 5. for conjunction and disjunction
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Junction j (nqsen:(Quantification q vdecls qsen _):sens) _ -> let
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu vars = flatVAR_DECLs vdecls
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu (n', vars') = getFreshVars vars n
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu vdecls' = map (\(v,s) -> mkVarDecl v s) $ map fst vars'
73aa270e722a8f046d7a281044e44720208a3884mcodescu qsen' = foldl (\f (v,s,t)-> substitute v s t f) qsen $ map (\((x,y),(z,t)) -> (z, t, Qual_var x y nullRange)) vars'
73aa270e722a8f046d7a281044e44720208a3884mcodescu (n'', jsen) = prenexNormalForm n' sig $
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu Junction j (nqsen:qsen':sens) nullRange
19be6554ade5f957a520c6553b957df8cc66ae77mcodescu in trace "5 conj & disj" $ (n'', Quantification q vdecls' jsen nullRange)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu -- don't forget recursion for other cases
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Junction j jsens _ -> let
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu (n', jsens') = foldl (\(x,sens0) s -> let (x',s') = prenexNormalForm x sig s
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu in trace ("in foldl junction:" ++ show s) $ (x', s':sens0))
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu (n, []) jsens
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu in trace ("junction recursion:" ++ show jsens ++ "\n") $ (n', Junction j jsens' nullRange)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu -- both two next cases cover 4.
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Relation (Quantification q vdecls qsen _) Implication sen2 _ -> let
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu vars = flatVAR_DECLs vdecls
16271fe9bde093c159c6961d703247a53739790amcodescu (n', vars') = getFreshVars vars n
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu vdecls' = map (\(v,s) -> mkVarDecl v s) $ map fst vars'
16271fe9bde093c159c6961d703247a53739790amcodescu qsen' = foldl (\f (v,s,t)-> substitute v s t f) qsen $ map (\((x,y),(z,t)) -> (z, t, Qual_var x y nullRange)) vars'
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu (n'', implSen) = prenexNormalForm n' sig $ Relation qsen' Implication sen2 nullRange
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu in trace "4.1" $ (n'', Quantification (dualQuant q) vdecls' implSen nullRange)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Relation sen1 RevImpl (Quantification q vdecls qsen _) _ -> let
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu vars = flatVAR_DECLs vdecls
16271fe9bde093c159c6961d703247a53739790amcodescu (n', vars') = getFreshVars vars n
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu vdecls' = map (\(v,s) -> mkVarDecl v s) $ map fst vars'
16271fe9bde093c159c6961d703247a53739790amcodescu qsen' = foldl (\f (v,s,t)-> substitute v s t f) qsen $ map (\((x,y),(z,t)) -> (z, t, Qual_var x y nullRange)) vars'
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu (n'', revImplSen) = prenexNormalForm n' sig $ Relation sen1 RevImpl qsen' nullRange
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu in trace "4.2" $ (n'', Quantification (dualQuant q) vdecls' revImplSen nullRange)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu -- next two cases cover 5. for implication
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Relation sen1 Implication (Quantification q vdecls qsen _) _ -> let
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu vars = flatVAR_DECLs vdecls
dc444ff12d28d0a535431580c679fb6c903c2900mcodescu (n', vars') = getFreshVars vars n'
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu vdecls' = map (\(v,s) -> mkVarDecl v s) $ map fst vars'
dc444ff12d28d0a535431580c679fb6c903c2900mcodescu qsen' = foldl (\f (v,s,t)-> substitute v s t f) qsen $ map (\((x,y),(z,t)) -> (z, t, Qual_var x y nullRange)) vars'
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu (n'', implSen) = prenexNormalForm n' sig $ Relation sen1 Implication qsen' nullRange
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu in trace "5.1" $ (n'', Quantification q vdecls' implSen nullRange)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Relation (Quantification q vdecls qsen _) RevImpl sen2 _ -> let
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu vars = flatVAR_DECLs vdecls
dc444ff12d28d0a535431580c679fb6c903c2900mcodescu (n', vars') = getFreshVars vars n
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu vdecls' = map (\(v,s) -> mkVarDecl v s) $ map fst vars'
dc444ff12d28d0a535431580c679fb6c903c2900mcodescu qsen' = foldl (\f (v,s,t)-> substitute v s t f) qsen $ map (\((x,y),(z,t)) -> (z, t, Qual_var x y nullRange)) vars'
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu (n'', revImplSen) = prenexNormalForm n' sig $ Relation qsen' RevImpl sen2 nullRange
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu in trace "5.2" $ (n'', Quantification q vdecls' revImplSen nullRange)
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu -- recursion for other cases
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Relation sen1 rel sen2 _ -> let
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu (n', sen1') = prenexNormalForm n sig sen1
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu (n'', sen2') = prenexNormalForm n' sig sen2
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu in trace ("recursion impl") $ (n'', Relation sen1' rel sen2' nullRange)
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu -- for quantification, recursive call for the quantified formula
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Quantification q vars qsen _ -> let
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu (n', qsen') = prenexNormalForm n sig qsen
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu in trace "recursion quant" $ (n', Quantification q vars qsen' nullRange)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu -- for atoms and similars, do nothing
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu x -> trace "atoms" $ (n, x)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescugetFreshVars :: [(VAR,SORT)] -> Int -> (Int, [((VAR,SORT),(VAR,SORT))])
4c11424ec962479c1086f066f83976f05adb4064mcodescugetFreshVars oldVars n = let
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu (n', newVars) = foldl (\(x, vs) (_, s) -> (x+1, (genNumVar "x" n, s):vs)) (n, []) $ oldVars
4c11424ec962479c1086f066f83976f05adb4064mcodescu in (n', zip newVars $ reverse oldVars)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescumapTheory :: (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA])
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescumapTheory (sig, nsens) = do
ea5605cd49a0f959f75fd90137e9d25e1235c0e8mcodescu let sens = foldl (\sens0 s -> let (_, s') = prenexNormalForm 0 sig $ negationNormalForm s -- no sense to call miniscope here
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu in s':sens0) [] $ map sentence nsens
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu return (sig, map (makeNamed "") sens)
4c11424ec962479c1086f066f83976f05adb4064mcodescu-- this should go some place where it's available for all comorphisms
4c11424ec962479c1086f066f83976f05adb4064mcodescunegationNormalForm :: CASLFORMULA -> CASLFORMULA
4c11424ec962479c1086f066f83976f05adb4064mcodescunegationNormalForm sen = case sen of
4c11424ec962479c1086f066f83976f05adb4064mcodescu Quantification q vars qsen _ -> Quantification q vars (negationNormalForm qsen) nullRange
4c11424ec962479c1086f066f83976f05adb4064mcodescu Junction j sens _ -> Junction j (map negationNormalForm sens) nullRange
4c11424ec962479c1086f066f83976f05adb4064mcodescu Relation sen1 Implication sen2 _ -> let sen1' = negationNormalForm $ Negation (negationNormalForm sen1) nullRange
4c11424ec962479c1086f066f83976f05adb4064mcodescu sen2' = negationNormalForm sen2
4c11424ec962479c1086f066f83976f05adb4064mcodescu in Junction Dis [sen1', sen2'] nullRange
4c11424ec962479c1086f066f83976f05adb4064mcodescu Relation sen1 RevImpl sen2 _ -> let sen2' = negationNormalForm $ Negation (negationNormalForm sen2) nullRange
4c11424ec962479c1086f066f83976f05adb4064mcodescu sen1' = negationNormalForm sen1
4c11424ec962479c1086f066f83976f05adb4064mcodescu in Junction Dis [sen1', sen2'] nullRange
4c11424ec962479c1086f066f83976f05adb4064mcodescu Relation sen1 Equivalence sen2 _ -> let sen1' = Relation sen1 Implication sen2 nullRange
4c11424ec962479c1086f066f83976f05adb4064mcodescu sen2' = Relation sen2 Implication sen1 nullRange
4c11424ec962479c1086f066f83976f05adb4064mcodescu in negationNormalForm $ Junction Con [sen1', sen2'] nullRange
4c11424ec962479c1086f066f83976f05adb4064mcodescu Negation (Negation sen' _) _ -> negationNormalForm sen'
4c11424ec962479c1086f066f83976f05adb4064mcodescu Negation (Junction Con sens _) _ -> Junction Dis (map (\x -> negationNormalForm $ Negation x nullRange) sens) nullRange
4c11424ec962479c1086f066f83976f05adb4064mcodescu Negation (Junction Dis sens _) _ -> Junction Con (map (\x -> negationNormalForm $ Negation x nullRange) sens) nullRange
4c11424ec962479c1086f066f83976f05adb4064mcodescu Negation (Quantification Unique_existential _vars _sen _) _-> error "nyi"
4c11424ec962479c1086f066f83976f05adb4064mcodescu Negation (Quantification q vars qsen _) _ -> Quantification (dualQuant q) vars (negationNormalForm $ Negation qsen nullRange) nullRange